normalFormsContextScript.sml

1Theory normalFormsContext[bare]
2Ancestors
3  combin normalForms
4Libs
5  HolKernel Parse boolLib simpLib boolSimps tautLib Canon
6
7(* ------------------------------------------------------------------------- *)
8(* Lemmas normalForms.sml formerly proved as it loaded.                      *)
9(* ------------------------------------------------------------------------- *)
10
11(* MK_CONJ_EQ, CONJ_RASSOC_CONV, DISJ_RASSOC_CONV support *)
12
13Theorem NF_MK_CONJ_EQ: (a <=> b) /\ (c <=> d) ==> (a /\ c <=> b /\ d)
14Proof tautLib.TAUT_TAC
15QED
16
17Theorem NF_CONJ_RASSOC: (a /\ b) /\ c <=> b /\ (a /\ c)
18Proof tautLib.TAUT_TAC
19QED
20
21Theorem NF_DISJ_RASSOC: (a \/ b) \/ c <=> b \/ (a \/ c)
22Proof tautLib.TAUT_TAC
23QED
24
25(* SKI / SKICo conversions *)
26
27Theorem MK_S:
28  !x y. (\v. (x v) (y v)) = S (x:'a->'b->'c) y
29Proof
30  REPEAT STRIP_TAC THEN CONV_TAC FUN_EQ_CONV THEN
31  SIMP_TAC boolSimps.bool_ss [combinTheory.S_DEF, combinTheory.K_DEF]
32QED
33
34Theorem MK_K:
35  !x. (\v. x) = (K:'a->'b->'a) x
36Proof
37  REPEAT STRIP_TAC THEN CONV_TAC FUN_EQ_CONV THEN
38  SIMP_TAC boolSimps.bool_ss [combinTheory.S_DEF, combinTheory.K_DEF]
39QED
40
41Theorem MK_I:
42  (\v. v) = (I:'a->'a)
43Proof
44  REPEAT STRIP_TAC THEN CONV_TAC FUN_EQ_CONV THEN
45  SIMP_TAC boolSimps.bool_ss
46    [combinTheory.S_DEF, combinTheory.K_DEF, combinTheory.I_THM]
47QED
48
49Theorem MK_C:
50  !x y. (\v. (x v) y) = combin$C (x:'a->'b->'c) y
51Proof
52  REPEAT STRIP_TAC THEN CONV_TAC FUN_EQ_CONV THEN
53  SIMP_TAC boolSimps.bool_ss
54    [combinTheory.S_DEF, combinTheory.K_DEF, combinTheory.C_DEF]
55QED
56
57Theorem MK_o:
58  !x y. (\v:'a. x (y v)) = (x:'b->'c) o y
59Proof
60  REPEAT STRIP_TAC THEN CONV_TAC FUN_EQ_CONV THEN
61  SIMP_TAC boolSimps.bool_ss
62    [combinTheory.S_DEF, combinTheory.K_DEF, combinTheory.o_DEF]
63QED
64
65Theorem FUN_EQ:
66  !(f : 'a -> 'b) g. (!x. f x = g x) <=> (f = g)
67Proof
68  CONV_TAC (DEPTH_CONV FUN_EQ_CONV) THEN REWRITE_TAC []
69QED
70
71(* NNF pushes *)
72
73Theorem NOT_TRUE: ~T <=> F
74Proof tautLib.TAUT_TAC
75QED
76
77Theorem NOT_FALSE: ~F <=> T
78Proof tautLib.TAUT_TAC
79QED
80
81Theorem IMP_DISJ_THM': !x y. x ==> y <=> y \/ ~x
82Proof tautLib.TAUT_TAC
83QED
84
85Theorem NIMP_CONJ_THM: !x y. ~(x ==> y) <=> x /\ ~y
86Proof tautLib.TAUT_TAC
87QED
88
89Theorem EQ_EXPAND': !x y. (x <=> y) <=> (x \/ ~y) /\ (~x \/ y)
90Proof tautLib.TAUT_TAC
91QED
92
93Theorem NEQ_EXPAND: !x y. ~(x <=> y) <=> (x \/ y) /\ (~x \/ ~y)
94Proof tautLib.TAUT_TAC
95QED
96
97Theorem COND_EXPAND': !c a b. (if c then a else b) <=> ((~c \/ a) /\ (c \/ b))
98Proof tautLib.TAUT_TAC
99QED
100
101Theorem NCOND_EXPAND: !c a b. ~(if c then a else b) <=> ((~c \/ ~a) /\ (c \/ ~b))
102Proof tautLib.TAUT_TAC
103QED
104
105Theorem DE_MORGAN_THM1: !x y. ~(x /\ y) <=> (~x \/ ~y)
106Proof tautLib.TAUT_TAC
107QED
108
109Theorem DE_MORGAN_THM2: !x y. ~(x \/ y) <=> (~x /\ ~y)
110Proof tautLib.TAUT_TAC
111QED
112
113Theorem NNF_EXISTS_UNIQUE:
114  !p. $?! p <=> ((?(x:'a). p x) /\ !x y. p x /\ p y ==> (x = y))
115Proof
116  GEN_TAC THEN
117  KNOW_TAC ``$?! p = ?!(x:'a). p x`` THEN1
118    (CONV_TAC (DEPTH_CONV ETA_CONV) THEN REWRITE_TAC []) THEN
119  DISCH_THEN (fn th => REWRITE_TAC [th]) THEN
120  REWRITE_TAC [boolTheory.EXISTS_UNIQUE_THM]
121QED
122
123Theorem NOT_EXISTS_UNIQUE:
124  !p. ~($?! p) <=> ((!(x:'a). ~p x) \/ ?x y. p x /\ p y /\ ~(x = y))
125Proof
126  REWRITE_TAC [NNF_EXISTS_UNIQUE, DE_MORGAN_THM1] THEN
127  CONV_TAC (TOP_DEPTH_CONV (NOT_EXISTS_CONV ORELSEC NOT_FORALL_CONV)) THEN
128  REWRITE_TAC [NOT_IMP, CONJ_ASSOC]
129QED
130
131Theorem RES_FORALL_THM:
132  !p m. RES_FORALL p m <=> !(x:'a). x IN p ==> m x
133Proof
134  REWRITE_TAC [RES_FORALL_DEF] THEN BETA_TAC THEN REWRITE_TAC []
135QED
136
137Theorem RES_EXISTS_THM:
138  !p m. RES_EXISTS p m <=> ?(x:'a). x IN p /\ m x
139Proof
140  REWRITE_TAC [RES_EXISTS_DEF] THEN BETA_TAC THEN REWRITE_TAC []
141QED
142
143Theorem NOT_RES_FORALL:
144  !p m. ~RES_FORALL p m <=> ?(x:'a). x IN p /\ ~m x
145Proof
146  REWRITE_TAC [RES_FORALL_THM] THEN
147  CONV_TAC (DEPTH_CONV NOT_FORALL_CONV) THEN
148  REWRITE_TAC [IMP_DISJ_THM, DE_MORGAN_THM2]
149QED
150
151Theorem NOT_RES_EXISTS:
152  !p m. ~RES_EXISTS p m <=> !(x:'a). x IN p ==> ~m x
153Proof
154  REWRITE_TAC [RES_EXISTS_THM] THEN
155  CONV_TAC (DEPTH_CONV NOT_EXISTS_CONV) THEN
156  REWRITE_TAC [IMP_DISJ_THM, DE_MORGAN_THM2, DE_MORGAN_THM1]
157QED
158
159(* TAUTOLOGY_CONV / CONTRACT_CONV support *)
160
161Theorem BOOL_CASES: !a b. (a ==> b) /\ (~a ==> b) ==> b
162Proof tautLib.TAUT_TAC
163QED
164
165Theorem T_OR: !t. T \/ t <=> T
166Proof tautLib.TAUT_TAC
167QED
168
169Theorem OR_T: !t. t \/ T <=> T
170Proof tautLib.TAUT_TAC
171QED
172
173Theorem T_AND: !t. T /\ t <=> t
174Proof tautLib.TAUT_TAC
175QED
176
177Theorem AND_T: !t. t /\ T <=> t
178Proof tautLib.TAUT_TAC
179QED
180
181Theorem OR_F: !t. t \/ F <=> t
182Proof tautLib.TAUT_TAC
183QED
184
185Theorem CONTRACT_DISJ: !a b b'. (~a ==> (b <=> b')) ==> (~a ==> (a \/ b <=> b'))
186Proof tautLib.TAUT_TAC
187QED
188
189Theorem DISJ_CONGRUENCE: !a b b'. (~a ==> (b <=> b')) ==> (a \/ b <=> a \/ b')
190Proof tautLib.TAUT_TAC
191QED
192
193Theorem NEG_EQ: !a b. ~(a <=> b) <=> (a <=> ~b)
194Proof tautLib.TAUT_TAC
195QED
196
197(* Definitional CNF forms; Canon.CNF_CONV is used *)
198
199Theorem EQ_DEFCNF:
200  !x y z.
201     (x <=> (y <=> z)) <=>
202     (z \/ ~y \/ ~x) /\ (y \/ ~z \/ ~x) /\ (x \/ ~y \/ ~z) /\ (x \/ y \/ z)
203Proof tautLib.TAUT_TAC
204QED
205
206Theorem AND_DEFCNF:
207  !x y z. (x <=> (y /\ z)) <=> (y \/ ~x) /\ (z \/ ~x) /\ (x \/ ~y \/ ~z)
208Proof tautLib.TAUT_TAC
209QED
210
211Theorem OR_DEFCNF:
212  !x y z. (x <=> (y \/ z)) <=> (y \/ z \/ ~x) /\ (x \/ ~y) /\ (x \/ ~z)
213Proof tautLib.TAUT_TAC
214QED
215
216(* Lambda elimination *)
217
218Theorem LAMB_EQ_ELIM:
219  !(s:'a -> 'b) t. ((\x. s x) = t) <=> (!x. s x = t x)
220Proof
221  CONV_TAC (DEPTH_CONV FUN_EQ_CONV) THEN SIMP_TAC boolSimps.bool_ss []
222QED
223
224Theorem EQ_LAMB_ELIM:
225  !(s:'a -> 'b) t. (s = (\x. t x)) <=> (!x. s x = t x)
226Proof
227  CONV_TAC (DEPTH_CONV FUN_EQ_CONV) THEN SIMP_TAC boolSimps.bool_ss []
228QED
229
230(* condify_SS support *)
231
232Theorem COND_SIMP:
233  !a f g. (if a then f a else g a):'a = (if a then f T else g F)
234Proof SIMP_TAC boolSimps.bool_ss []
235QED
236
237Theorem COND_NOT: !a. ~a <=> if a then F else T
238Proof SIMP_TAC boolSimps.bool_ss []
239QED
240
241Theorem COND_AND: !a b. a /\ b <=> (if a then b else F)
242Proof SIMP_TAC boolSimps.bool_ss []
243QED
244
245Theorem COND_OR: !a b. a \/ b <=> if a then T else b
246Proof SIMP_TAC boolSimps.bool_ss []
247QED
248
249Theorem COND_IMP: !a b. a ==> b <=> if a then b else T
250Proof SIMP_TAC boolSimps.bool_ss []
251QED
252
253Theorem COND_EQ: !a b. (a <=> b) <=> if a then b else ~b
254Proof
255  SIMP_TAC boolSimps.bool_ss [EQ_IMP_THM, COND_EXPAND] THEN tautLib.TAUT_TAC
256QED
257
258Theorem COND_COND:
259  !a b c x y.
260    (if (if a then b else c) then (x:'a) else y) =
261    (if a then (if b then x else y) else (if c then x else y))
262Proof
263  STRIP_TAC THEN MP_TAC (SPEC ``a:bool`` EXCLUDED_MIDDLE) THEN
264  STRIP_TAC THEN ASM_SIMP_TAC boolSimps.bool_ss []
265QED
266
267Theorem COND_ETA: !a. (if a then T else F) = a
268Proof SIMP_TAC boolSimps.bool_ss []
269QED
270
271Theorem COND_BOOL: !c. (if c then T else F) = c
272Proof tautLib.TAUT_TAC
273QED
274
275(* CONDS_ELIM_CONV / CONDS_CELIM_CONV support *)
276
277Theorem TH_COND:
278  ((b <=> F) ==> x = x0) /\ ((b <=> T) ==> x = x1)
279    ==> x = (b /\ x1 \/ ~b /\ x0)
280Proof BOOL_CASES_TAC ``b:bool`` THEN ASM_REWRITE_TAC []
281QED
282
283Theorem TH_COND':
284  ((b <=> F) ==> x = x0) /\ ((b <=> T) ==> x = x1)
285    ==> x = ((~b \/ x1) /\ (b \/ x0))
286Proof BOOL_CASES_TAC ``b:bool`` THEN ASM_REWRITE_TAC []
287QED
288
289(* GEN_NNF_CONV support *)
290
291Theorem PTHS_CONJ:
292  (~((!) P) <=> ?x:'a. ~(P x)) /\
293  (~((?) P) <=> !x:'a. ~(P x)) /\
294  (~((?!) P) <=> (!x:'a. ~(P x)) \/ ?x y. P x /\ P y /\ ~(y = x))
295Proof
296  REPEAT CONJ_TAC THEN
297  GEN_REWRITE_TAC (LAND_CONV o funpow 2 RAND_CONV) empty_rewrites [GSYM ETA_AX] THEN
298  SIMP_TAC boolSimps.bool_ss
299    [NOT_EXISTS_THM, NOT_FORALL_THM, boolTheory.EXISTS_UNIQUE_DEF,
300     DE_MORGAN_THM, NOT_IMP, GSYM CONJ_ASSOC] THEN
301  GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV) empty_rewrites [EQ_SYM_EQ] THEN
302  REWRITE_TAC []
303QED
304
305Theorem PTH_EXU:
306  ((?!) P) <=> (?x:'a. P x) /\ !x y. ~(P x) \/ ~(P y) \/ (y = x)
307Proof
308  GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) empty_rewrites [GSYM ETA_AX] THEN
309  SIMP_TAC boolSimps.bool_ss
310    [boolTheory.EXISTS_UNIQUE_DEF, tautLib.TAUT `a /\ b ==> c <=> ~a \/ ~b \/ c`] THEN
311  GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV) empty_rewrites [EQ_SYM_EQ] THEN
312  REWRITE_TAC []
313QED