ConseqConvScript.sml
1Theory ConseqConv[bare]
2Ancestors
3 bool
4Libs
5 HolKernel Parse boolLib tautLib
6
7Theorem forall_eq_thm:
8 (!s:'a. (P s = Q s)) ==> ((!s. P s) = (!s. Q s))
9Proof
10 STRIP_TAC THEN ASM_REWRITE_TAC[]
11QED
12
13Theorem exists_eq_thm:
14 (!s:'a. (P s = Q s)) ==> ((?s. P s) = (?s. Q s))
15Proof
16 STRIP_TAC THEN ASM_REWRITE_TAC[]
17QED
18
19Theorem true_imp: !t. t ==> T
20Proof REWRITE_TAC[]
21QED
22Theorem false_imp: !t. F ==> t
23Proof REWRITE_TAC[]
24QED
25
26val NOT_CLAUSES_THML = CONJUNCTS NOT_CLAUSES
27Theorem NOT_CLAUSES_X = el 1 NOT_CLAUSES_THML
28Theorem NOT_CLAUSES_T = el 2 NOT_CLAUSES_THML
29Theorem NOT_CLAUSES_F = el 3 NOT_CLAUSES_THML
30
31Theorem IMP_CONG_conj_strengthen = TAUT_PROVE “
32 !x x' y y'.
33 (y ==> x' ==> x) /\ (x' ==> y' ==> y) ==>
34 (x' /\ y' ==> x /\ y)”
35
36Theorem IMP_CONG_conj_weaken = TAUT_PROVE “
37 !x x' y y'.
38 (y ==> x ==> x') /\ (x' ==> y ==> y') ==>
39 (x /\ y ==> x' /\ y')”
40
41
42val AND_CLAUSES_THML =
43 (CONJUNCTS (Ho_Rewrite.PURE_REWRITE_RULE [FORALL_AND_THM] AND_CLAUSES))
44
45Theorem AND_CLAUSES_TX = el 1 AND_CLAUSES_THML;
46Theorem AND_CLAUSES_XT = el 2 AND_CLAUSES_THML;
47Theorem AND_CLAUSES_FX = el 3 AND_CLAUSES_THML;
48Theorem AND_CLAUSES_XF = el 4 AND_CLAUSES_THML;
49Theorem AND_CLAUSES_XX = el 5 AND_CLAUSES_THML;
50
51
52Theorem IMP_CONG_disj_strengthen = TAUT_PROVE “
53 !x x' y y'.
54 (~y ==> x' ==> x) /\ (~x' ==> y' ==> y) ==>
55 (x' \/ y' ==> x \/ y)”
56
57
58Theorem IMP_CONG_disj_weaken = TAUT_PROVE “
59 !x x' y y'.
60 (~y ==> x ==> x') /\ (~x' ==> y ==> y') ==>
61 (x \/ y ==> x' \/ y')”
62
63
64val OR_CLAUSES_THML =
65 (CONJUNCTS (Ho_Rewrite.PURE_REWRITE_RULE [FORALL_AND_THM] OR_CLAUSES))
66
67Theorem OR_CLAUSES_TX = el 1 OR_CLAUSES_THML
68Theorem OR_CLAUSES_XT = el 2 OR_CLAUSES_THML
69Theorem OR_CLAUSES_FX = el 3 OR_CLAUSES_THML
70Theorem OR_CLAUSES_XF = el 4 OR_CLAUSES_THML
71Theorem OR_CLAUSES_XX = el 5 OR_CLAUSES_THML
72
73
74
75
76val IMP_CONG_imp_strengthen = store_thm ("IMP_CONG_imp_strengthen",
77``!x x' y y'.
78 ((x ==> (y' ==> y)) /\ (~y' ==> (x ==> x'))) ==>
79 ((x' ==> y') ==> (x ==> y))``,
80 Ho_Rewrite.REWRITE_TAC [FORALL_BOOL]);
81
82val IMP_CONG_imp_weaken = store_thm ("IMP_CONG_imp_weaken",
83``!x x' y y'.
84 ((x ==> (y ==> y')) /\ (~y' ==> (x' ==> x))) ==>
85 ((x ==> y) ==> (x' ==> y'))``,
86 Ho_Rewrite.REWRITE_TAC [FORALL_BOOL]);
87
88
89val IMP_CONG_simple_imp_strengthen = store_thm ("IMP_CONG_simple_imp_strengthen",
90``!x x' y y'.
91 ((x ==> x') /\ (x' ==> (y' ==> y))) ==>
92 ((x' ==> y') ==> (x ==> y))``,
93 Ho_Rewrite.REWRITE_TAC [FORALL_BOOL]);
94
95val IMP_CONG_simple_imp_weaken = store_thm ("IMP_CONG_simple_imp_weaken",
96``!x x' y y'.
97 ((x' ==> x) /\ (x' ==> (y ==> y'))) ==>
98 ((x ==> y) ==> (x' ==> y'))``,
99 Ho_Rewrite.REWRITE_TAC [FORALL_BOOL]);
100
101
102val IMP_CLAUSES_THML =
103 (CONJUNCTS (Ho_Rewrite.PURE_REWRITE_RULE [FORALL_AND_THM] IMP_CLAUSES))
104
105Theorem IMP_CLAUSES_TX = el 1 IMP_CLAUSES_THML
106Theorem IMP_CLAUSES_XT = el 2 IMP_CLAUSES_THML
107Theorem IMP_CLAUSES_FX = el 3 IMP_CLAUSES_THML
108Theorem IMP_CLAUSES_XX = el 4 IMP_CLAUSES_THML
109Theorem IMP_CLAUSES_XF = el 5 IMP_CLAUSES_THML
110
111
112
113val IMP_CONG_cond_simple = store_thm ("IMP_CONG_cond_simple",
114``!c x x' y y'.
115 ((x' ==> x) /\ (y' ==> y)) ==>
116 ((if c then x' else y') ==> (if c then x else y))``,
117Ho_Rewrite.REWRITE_TAC [FORALL_BOOL]);
118
119val IMP_CONG_cond = store_thm ("IMP_CONG_cond",
120``!c x x' y y'.
121 ((c ==> (x' ==> x)) /\ (~c ==> (y' ==> y))) ==>
122 ((if c then x' else y') ==> (if c then x else y))``,
123Ho_Rewrite.REWRITE_TAC [FORALL_BOOL]);
124
125
126
127val COND_CLAUSES_THML =
128 (CONJUNCTS (Ho_Rewrite.PURE_REWRITE_RULE [FORALL_AND_THM] COND_CLAUSES))
129fun bool_save_thm (s,t) = store_thm (s, t, Ho_Rewrite.REWRITE_TAC [FORALL_BOOL])
130
131Theorem COND_CLAUSES_CT = el 1 COND_CLAUSES_THML
132Theorem COND_CLAUSES_CF = el 2 COND_CLAUSES_THML
133Theorem COND_CLAUSES_ID = COND_ID
134val COND_CLAUSES_TT = bool_save_thm ("COND_CLAUSES_TT",
135 ``!c x. (if c then T else x) = (~c ==> x)``)
136val COND_CLAUSES_FT = bool_save_thm ("COND_CLAUSES_FT",
137 ``!c x. (if c then x else T) = (c ==> x)``)
138val COND_CLAUSES_TF = bool_save_thm ("COND_CLAUSES_TF",
139 ``!c x. (if c then F else x) = (~c /\ x)``)
140val COND_CLAUSES_FF = bool_save_thm ("COND_CLAUSES_FF",
141 ``!c x. (if c then x else F) = (c /\ x)``)
142
143
144Definition ASM_MARKER_DEF[nocompute]:
145 ASM_MARKER = (\ (y:bool) x:bool. x)
146End
147
148Theorem ASM_MARKER_THM: !y x. ASM_MARKER y x = x
149Proof
150 REWRITE_TAC[ASM_MARKER_DEF] THEN
151 BETA_TAC THEN REWRITE_TAC []
152QED