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