boolScript.sml
1(* ===================================================================== *)
2(* FILE : boolScript.sml *)
3(* DESCRIPTION : Definition of the logical constants and assertion of *)
4(* the axioms. *)
5(* AUTHORS : (c) Mike Gordon, University of Cambridge *)
6(* Tom Melham, Richard Boulton, John Harrison, *)
7(* Konrad Slind, Michael Norrish, Jim Grundy, Joe Hurd *)
8(* and probably others that don't immediately come to *)
9(* mind. *)
10(* ===================================================================== *)
11
12Theory bool[bare]
13Libs
14 HolKernel Parse TexTokenMap Portable GrammarSpecials[qualified]
15 boolpp[qualified]
16
17open Unicode
18
19(*---------------------------------------------------------------------------*
20 * BASIC DEFINITIONS *
21 *---------------------------------------------------------------------------*)
22
23(* parsing/printing support for theory min *)
24val _ = unicode_version {u = UChar.imp, tmnm = "==>"}
25val _ = TeX_notation {hol = "==>", TeX = ("\\HOLTokenImp{}", 1)}
26val _ = TeX_notation {hol = UChar.imp, TeX = ("\\HOLTokenImp{}", 1)}
27
28val _ = TeX_notation {hol = "\\", TeX = ("\\HOLTokenLambda{}", 1)}
29val _ = TeX_notation {hol = UChar.lambda, TeX = ("\\HOLTokenLambda{}", 1)}
30
31val _ = TeX_notation {hol = "@", TeX = ("\\HOLTokenHilbert{}", 1)}
32
33(* iff *)
34Overload "<=>" = “(=) : bool -> bool -> bool”
35val _ = set_fixity "<=>" (Infix(NONASSOC, 100))
36val _ = unicode_version {u = UChar.iff, tmnm = "<=>"}
37val _ = TeX_notation {hol = "<=>", TeX = ("\\HOLTokenEquiv{}",3)}
38val _ = TeX_notation {hol = UChar.iff, TeX = ("\\HOLTokenEquiv{}",3)}
39
40(* records *)
41val _ = TeX_notation {hol = "<|", TeX = ("\\HOLTokenLeftrec{}", 2)}
42val _ = TeX_notation {hol = "|>", TeX = ("\\HOLTokenRightrec{}", 2)}
43
44(* case expressions *)
45val _ = TeX_notation {hol = "case", TeX = ("\\HOLKeyword{case}", 4)}
46val _ = TeX_notation {hol = "of", TeX = ("\\HOLKeyword{of}", 2)}
47val _ = TeX_notation {hol = "=>", TeX = ("\\HOLTokenImp{}", 1)}
48
49(* let expressions *)
50val _ = TeX_notation {hol = "let", TeX = ("\\HOLKeyword{let}", 3)}
51val _ = TeX_notation {hol = "and", TeX = ("\\HOLKeyword{and}", 2)}
52val _ = TeX_notation {hol = "in", TeX = ("\\HOLKeyword{in}", 2)}
53
54(* if statements *)
55val _ = TeX_notation {hol = "if", TeX = ("\\HOLKeyword{if}", 2)}
56val _ = TeX_notation {hol = "then", TeX = ("\\HOLKeyword{then}", 4)}
57val _ = TeX_notation {hol = "else", TeX = ("\\HOLKeyword{else}", 4)}
58
59(* type syntax *)
60val _ = TeX_notation {hol = "->", TeX = ("\\HOLTokenMap{}", 1)}
61val _ = TeX_notation {hol = "'a", TeX = ("\\alpha{}", 1)}
62val _ = TeX_notation {hol = "'b", TeX = ("\\beta{}", 1)}
63val _ = TeX_notation {hol = "'c", TeX = ("\\gamma{}", 1)}
64val _ = TeX_notation {hol = "'d", TeX = ("\\delta{}", 1)}
65val _ = TeX_notation {hol = "'e", TeX = ("\\epsilon{}", 1)}
66(* past this point the Greek letters are likely to be more confusing than
67 helpful *)
68
69fun mkloc(s,n) = DB_dtype.mkloc(s,n,true)
70fun def l (n,t) = Definition.located_new_definition {loc=mkloc l,name=n,def=t}
71fun thm l (n,th) = Theory.gen_save_thm{loc=mkloc l,name=n,private=false,thm=th}
72fun ax l (n,t) = Theory.gen_new_axiom(n,t,mkloc l)
73val T_DEF = def (#(FILE),#(LINE))
74 ("T_DEF",
75 “T = ((\x:bool. x) = \x:bool. x)”);
76val _ = Thm.register_T T_DEF;
77
78val FORALL_DEF = def (#(FILE), #(LINE))
79 ("FORALL_DEF", “! = \P:'a->bool. P = \x. T”)
80val _ = Thm.register_forall FORALL_DEF;
81
82val _ = set_fixity "!" Binder
83val _ = unicode_version {u = UChar.forall, tmnm = "!"};
84val _ = TeX_notation {hol = "!", TeX = ("\\HOLTokenForall{}",1)}
85val _ = TeX_notation {hol = UChar.forall, TeX = ("\\HOLTokenForall{}",1)}
86
87val EXISTS_DEF = def (#(FILE), #(LINE))
88 ("EXISTS_DEF", “? = \P:'a->bool. P ($@ P)”);
89val _ = Thm.register_exists EXISTS_DEF;
90
91val _ = set_fixity "?" Binder
92val _ = unicode_version {u = UChar.exists, tmnm = "?"}
93val _ = TeX_notation {hol = "?", TeX = ("\\HOLTokenExists{}",1)}
94val _ = TeX_notation {hol = UChar.exists, TeX = ("\\HOLTokenExists{}",1)}
95
96val AND_DEF = def (#(FILE), #(LINE))
97 ("AND_DEF", “/\ = \t1 t2. !t. (t1 ==> t2 ==> t) ==> t”);
98val _ = Thm.register_conj AND_DEF;
99
100val _ = set_fixity "/\\" (Infixr 400);
101val _ = unicode_version {u = UChar.conj, tmnm = "/\\"};
102val _ = TeX_notation {hol = "/\\", TeX = ("\\HOLTokenConj{}",1)}
103val _ = TeX_notation {hol = UChar.conj, TeX = ("\\HOLTokenConj{}",1)}
104
105
106val OR_DEF = def (#(FILE), #(LINE))
107 ("OR_DEF", “\/ = \t1 t2. !t. (t1 ==> t) ==> (t2 ==> t) ==> t”)
108val _ = Thm.register_disj OR_DEF;
109
110val _ = set_fixity "\\/" (Infixr 300)
111val _ = unicode_version {u = UChar.disj, tmnm = "\\/"}
112val _ = TeX_notation {hol = "\\/", TeX = ("\\HOLTokenDisj{}",1)}
113val _ = TeX_notation {hol = UChar.disj, TeX = ("\\HOLTokenDisj{}",1)}
114
115
116val F_DEF = def (#(FILE), #(LINE))
117 ("F_DEF", “F = !t. t”);
118val _ = Thm.register_F F_DEF;
119
120val NOT_DEF = def (#(FILE), #(LINE))
121 ("NOT_DEF", “~ = \t. t ==> F”);
122val _ = Thm.register_neg NOT_DEF;
123
124(* now allows parsing of not equal *)
125Overload "<>" = “\x:'a y:'a. ~(x = y)”
126val _ = set_fixity "<>" (Infix(NONASSOC, 450))
127val _ = TeX_notation {hol="<>", TeX = ("\\HOLTokenNotEqual{}",1)}
128
129val _ = set_fixity UChar.neq (Infix(NONASSOC, 450))
130val _ = overload_on (UChar.neq, “\x:'a y:'a. ~(x = y)”)
131val _ = TeX_notation {hol=UChar.neq, TeX = ("\\HOLTokenNotEqual{}",1)}
132
133
134
135val EXISTS_UNIQUE_DEF = def (#(FILE), #(LINE))
136 ("EXISTS_UNIQUE_DEF",
137 “?! = \P:'a->bool. $? P /\ !x y. P x /\ P y ==> (x=y)”);
138
139val _ = set_fixity "?!" Binder
140
141val _ = unicode_version { u = UChar.exists ^ "!", tmnm = "?!"}
142val _ = TeX_notation {hol = "?!", TeX = ("\\HOLTokenUnique{}",2)}
143val _ = TeX_notation {hol = UChar.exists ^ "!", TeX = ("\\HOLTokenUnique{}",2)}
144
145val LET_DEF = def (#(FILE), #(LINE))
146 ("LET_DEF", “LET = λ(f:'a->'b) x. f x”);
147
148val COND_DEF = def (#(FILE), #(LINE))
149 ("COND_DEF", “COND = \t t1 t2.
150 @x:'a. ((t=T) ==> (x=t1)) /\
151 ((t=F) ==> (x=t2))”);
152Overload case = “COND”
153
154val ONE_ONE_DEF = def (#(FILE), #(LINE))
155 ("ONE_ONE_DEF", “ONE_ONE = \f:'a->'b. !x1 x2.
156 (f x1 = f x2) ==> (x1 = x2)”);
157
158val ONTO_DEF = def (#(FILE), #(LINE))
159 ("ONTO_DEF", “ONTO = \f:'a->'b. !y. ?x. y = f x”);
160
161val TYPE_DEFINITION = def (#(FILE), #(LINE))
162 ("TYPE_DEFINITION",
163 “TYPE_DEFINITION = \P:'a->bool. \rep:'b->'a.
164 (!x' x''. (rep x' = rep x'') ==> (x' = x'')) /\
165 (!x. P x = (?x'. x = rep x'))”);
166val _ = Thm.register_type_definition TYPE_DEFINITION;
167
168
169(*---------------------------------------------------------------------------*
170 * Parsing directives for some of the basic operators. *
171 *---------------------------------------------------------------------------*)
172
173Overload "~" = “~”
174Overload "¬" = “~”
175val _ = add_rule {term_name = "~",
176 fixity = Prefix 900,
177 pp_elements = [TOK "~"],
178 paren_style = OnlyIfNecessary,
179 block_style = (AroundEachPhrase, (CONSISTENT, 0))};
180val _ = add_rule {term_name = UChar.neg,
181 fixity = Prefix 900,
182 pp_elements = [TOK UChar.neg],
183 paren_style = OnlyIfNecessary,
184 block_style = (AroundEachPhrase, (CONSISTENT, 0))};
185val _ = TeX_notation {hol = "~", TeX = ("\\HOLTokenNeg{}",1)}
186val _ = TeX_notation {hol = UChar.neg, TeX = ("\\HOLTokenNeg{}",1)}
187
188(* prettyprinting information here for "let" and "and" is completely ignored;
189 the pretty-printer handles these specially. These declarations are only
190 for the parser's benefit. *)
191val _ = add_rule {
192 pp_elements = [TOK "let",
193 ListForm {
194 separator = [TOK ";"],
195 cons = GrammarSpecials.letcons_special,
196 nilstr = GrammarSpecials.letnil_special,
197 block_info = (INCONSISTENT, 0)
198 },
199 TOK "in"],
200 term_name = GrammarSpecials.let_special,
201 paren_style = OnlyIfNecessary, fixity = Prefix 8,
202 block_style = (AroundEachPhrase, (CONSISTENT, 0))};
203
204val _ = add_rule {term_name = GrammarSpecials.and_special,
205 fixity = Infixl 9,
206 pp_elements = [TOK "and"],
207 paren_style = OnlyIfNecessary,
208 block_style = (AroundEachPhrase, (INCONSISTENT, 0))}
209
210val _ = add_rule{term_name = "COND",
211 fixity = Prefix 70,
212 pp_elements = [PPBlock([TOK "if", BreakSpace(1,2), TM,
213 BreakSpace(1,0),
214 TOK "then"], (CONSISTENT, 0)),
215 BreakSpace(1,2), TM, BreakSpace(1,0),
216 TOK "else", BreakSpace(1,2)],
217 paren_style = OnlyIfNecessary,
218 block_style = (AroundEachPhrase, (CONSISTENT, 0))};
219
220
221(*---------------------------------------------------------------------------*
222 * AXIOMS *
223 * *
224 * Bruno Barras noticed that the axiom IMP_ANTISYM_AX from the original *
225 * HOL logic was provable. *
226 *---------------------------------------------------------------------------*)
227
228val BOOL_CASES_AX = ax(#(FILE), #(LINE))
229 ("BOOL_CASES_AX", “!t. (t=T) \/ (t=F)”);
230
231val ETA_AX = ax(#(FILE), #(LINE))
232 ("ETA_AX", “!t:'a->'b. (\x. t x) = t”);
233
234val SELECT_AX = ax(#(FILE), #(LINE))
235 ("SELECT_AX", “!(P:'a->bool) x. P x ==> P ($@ P)”);
236
237val INFINITY_AX = ax(#(FILE), #(LINE))
238 ("INFINITY_AX", “?f:ind->ind. ONE_ONE f /\ ~ONTO f”);
239
240
241(*---------------------------------------------------------------------------*
242 * Miscellaneous utility definitions, of use in some packages. *
243 *---------------------------------------------------------------------------*)
244
245val arb = new_constant("ARB",alpha); (* Doesn't have to be defined at all. *)
246
247val literal_case_DEF = def (#(FILE), #(LINE))
248 ("literal_case_DEF", “literal_case = λ(f:'a->'b) x. f x”);
249
250Overload case = “bool$literal_case”
251
252val IN_DEF = def (#(FILE), #(LINE))
253 ("IN_DEF", “IN = \x (f:'a->bool). f x”);
254
255val _ = set_fixity "IN" (Infix(NONASSOC, 425))
256val _ = unicode_version {u = UChar.setelementof, tmnm = "IN"};
257val _ = TeX_notation {hol = "IN", TeX = ("\\HOLTokenIn{}",1)}
258val _ = TeX_notation {hol = UChar.setelementof, TeX = ("\\HOLTokenIn{}",1)}
259
260val RES_FORALL_DEF = def (#(FILE), #(LINE))
261 ("RES_FORALL_DEF", “RES_FORALL = \p m. !x : 'a. x IN p ==> m x”);
262
263val _ = associate_restriction ("!", "RES_FORALL")
264
265val RES_EXISTS_DEF = def (#(FILE), #(LINE))
266 ("RES_EXISTS_DEF", “RES_EXISTS = \p m. ?x : 'a. x IN p /\ m x”);
267
268val _ = associate_restriction ("?", "RES_EXISTS")
269
270val RES_EXISTS_UNIQUE_DEF = def (#(FILE), #(LINE))
271 ("RES_EXISTS_UNIQUE_DEF",
272 “RES_EXISTS_UNIQUE =
273 \p m. (?(x : 'a) :: p. m x) /\ !x y :: p. m x /\ m y ==> (x = y)”);
274
275val _ = associate_restriction ("?!", "RES_EXISTS_UNIQUE");
276
277val RES_SELECT_DEF = def (#(FILE), #(LINE))
278 ("RES_SELECT_DEF", “RES_SELECT = \p m. @x : 'a. x IN p /\ m x”);
279
280val _ = associate_restriction ("@", "RES_SELECT")
281
282(* Note: RES_ABSTRACT comes later, defined by new_specification *)
283
284(*---------------------------------------------------------------------------*)
285(* Experimental rewriting directives *)
286(*---------------------------------------------------------------------------*)
287
288val BOUNDED_DEF = def (#(FILE), #(LINE))
289 ("BOUNDED_DEF",
290 “BOUNDED = λ(v:bool). T”);
291
292(*---------------------------------------------------------------------------*)
293(* Support for detecting datatypes in theory files *)
294(*---------------------------------------------------------------------------*)
295
296val DATATYPE_TAG_DEF = def (#(FILE), #(LINE))
297 ("DATATYPE_TAG_DEF",
298 “DATATYPE = \x. T”);
299
300(*---------------------------------------------------------------------------*
301 * THEOREMS *
302 *---------------------------------------------------------------------------*)
303
304val op --> = Type.-->
305
306val ERR = Feedback.mk_HOL_ERR "boolScript"
307
308val F = “F”
309val T = “T”;
310val implication = prim_mk_const{Name="==>", Thy="min"}
311val select = prim_mk_const{Name="@", Thy="min"}
312val conjunction = prim_mk_const{Name="/\\", Thy="bool"}
313val disjunction = prim_mk_const{Name="\\/", Thy="bool"}
314val negation = prim_mk_const{Name="~", Thy="bool"}
315val universal = prim_mk_const{Name="!", Thy="bool"}
316val existential = prim_mk_const{Name="?", Thy="bool"}
317val exists1 = prim_mk_const{Name="?!", Thy="bool"}
318val in_tm = prim_mk_const{Name="IN", Thy="bool"};
319
320
321val dest_neg = sdest_monop("~","bool") (ERR"dest_neg" "");
322val dest_eq = sdest_binop("=","min") (ERR"dest_eq" "");
323val dest_disj = sdest_binop("\\/","bool") (ERR"dest_disj" "");
324val dest_conj = sdest_binop("/\\","bool") (ERR"dest_conj" "");
325val dest_forall = sdest_binder("!","bool") (ERR"dest_forall" "");
326val dest_exists = sdest_binder("?","bool") (ERR"dest_exists" "");
327fun strip_forall fm =
328 if can dest_forall fm
329 then let val (Bvar,Body) = dest_forall fm
330 val (bvs,core) = strip_forall Body
331 in ((Bvar::bvs), core)
332 end
333 else ([],fm);
334val lhs = fst o dest_eq;
335val rhs = snd o dest_eq;
336
337
338local val imp = “$==>” val notc = “$~”
339in
340fun dest_imp M =
341 let val (Rator,conseq) = dest_comb M
342 in if is_comb Rator
343 then let val (Rator,ant) = dest_comb Rator
344 in if aconv Rator imp then (ant,conseq)
345 else raise Fail "dest_imp"
346 end
347 else if aconv Rator notc then (conseq,F) else raise Fail "dest_imp"
348 end
349end
350
351fun mk_neg M = “~^M”;
352fun mk_eq(lhs,rhs) = “^lhs = ^rhs”;
353fun mk_imp(ant,conseq) = “^ant ==> ^conseq”;
354fun mk_conj(conj1,conj2) = “^conj1 /\ ^conj2”;
355fun mk_disj(disj1,disj2) = “^disj1 \/ ^disj2”;
356fun mk_forall(Bvar,Body) = “!^Bvar. ^Body”
357fun mk_exists(Bvar,Body) = “?^Bvar. ^Body”
358fun mk_exists1(Bvar,Body) = “?!^Bvar. ^Body”
359
360val list_mk_forall = itlist (curry mk_forall)
361val list_mk_exists = itlist (curry mk_exists)
362
363(* also implemented in Drule *)
364fun ETA_CONV t =
365 let val (var, cmb) = dest_abs t
366 val tysubst = [alpha |-> type_of var, beta |-> type_of cmb]
367 val th = SPEC (rator cmb) (INST_TYPE tysubst ETA_AX)
368 in
369 TRANS (ALPHA t (lhs (concl th))) th
370 end;
371
372fun EXT th =
373 let val (Bvar,_) = dest_forall(concl th)
374 val th1 = SPEC Bvar th
375 val (t1x, t2x) = dest_eq(concl th1)
376 val x = rand t1x
377 val th2 = ABS x th1
378 in
379 TRANS (TRANS(SYM(ETA_CONV (mk_abs(x, t1x)))) th2)
380 (ETA_CONV (mk_abs(x,t2x)))
381 end;
382
383fun DISCH_ALL th = DISCH_ALL (DISCH (hd (hyp th)) th) handle _ => th;
384
385fun PROVE_HYP ath bth = MP (DISCH (concl ath) bth) ath;
386
387fun CONV_RULE conv th = EQ_MP (conv(concl th)) th;
388
389fun RAND_CONV conv tm =
390 let val (Rator,Rand) = dest_comb tm
391 in AP_TERM Rator (conv Rand)
392 end;
393
394fun RATOR_CONV conv tm =
395 let val (Rator,Rand) = dest_comb tm in AP_THM (conv Rator) Rand end;
396
397fun ABS_CONV conv tm =
398 let val (Bvar,Body) = dest_abs tm in ABS Bvar (conv Body) end;
399
400fun QUANT_CONV conv = RAND_CONV(ABS_CONV conv);
401
402fun RIGHT_BETA th = TRANS th (BETA_CONV(snd(dest_eq(concl th))));
403
404fun UNDISCH th = MP th (ASSUME(fst(dest_imp(concl th))));
405
406fun FALSITY_CONV tm = DISCH F (SPEC tm (EQ_MP F_DEF (ASSUME F)))
407
408fun UNFOLD_OR_CONV tm =
409 let val (disj1,disj2) = dest_disj tm in
410 RIGHT_BETA(AP_THM (RIGHT_BETA(AP_THM OR_DEF disj1)) disj2)
411 end;
412
413(* common variables used throughout what follows *)
414fun Av s = mk_var(s, alpha)
415fun Bv s = mk_var(s, bool)
416val tb = Bv "t"
417val t1b = Bv "t1"
418val t2b = Bv "t2"
419val Pb = Bv "P"
420val Qb = Bv "Q"
421val Pab = mk_var("P", alpha --> bool)
422val Qab = mk_var("Q", alpha --> bool)
423
424val fabt = mk_var("f", alpha --> beta)
425val xa = Av "x"
426val ya = Av "y"
427
428(*---------------------------------------------------------------------------
429 * |- T
430 *---------------------------------------------------------------------------*)
431
432val TRUTH = thm (#(FILE),#(LINE))
433 ("TRUTH", EQ_MP (SYM T_DEF) (REFL “\x:bool. x”));
434
435fun EQT_ELIM th = EQ_MP (SYM th) TRUTH;
436
437(* SPEC could be built here. *)
438(* GEN could be built here. *)
439
440(* auxiliary functions to do bool case splitting *)
441(* maps thm |- P[x\t] to |- y=t ==> P[x\y] *)
442fun CUT_EQUAL P x y t thm =
443 let val e = mk_eq(y,t) in
444 DISCH e (SUBST [(x|->SYM (ASSUME e))] P thm)
445 end;
446
447(* given proofs of P[x\T] and P[x\F], proves P[x\t] *)
448fun BOOL_CASE P x t pt pf =
449 let val th0 = SPEC t BOOL_CASES_AX
450 val th1 = EQ_MP (UNFOLD_OR_CONV (concl th0)) th0
451 val th2 = SPEC (subst[(x|->t)] P) th1 in
452 MP (MP th2 (CUT_EQUAL P x t T pt)) (CUT_EQUAL P x t F pf)
453 end;
454
455fun EQT_INTRO th =
456 let val t = concl th
457 val x = genvar bool
458 in
459 BOOL_CASE “^x=T” x t (REFL T)
460 (MP (FALSITY_CONV “F=T”) (EQ_MP (ASSUME“^t=F”) th))
461 end;
462
463(*---------------------------------------------------------------------------
464 * |- !t1 t2. (t1 ==> t2) ==> (t2 ==> t1) ==> (t1 = t2)
465 *---------------------------------------------------------------------------*)
466
467infixr ==>
468val op==> = mk_imp
469infix ==
470val op== = mk_eq
471val IMP_ANTISYM_AX = thm (#(FILE), #(LINE))(
472 "IMP_ANTISYM_AX",
473 let fun dsch t1 t2 th = DISCH (t2 ==> t1) (DISCH (t1 ==> t2) th)
474 fun sch t1 t2 = (t1==>t2) ==> (t2==>t1) ==> (t1 == t2)
475 val abs = MP (FALSITY_CONV (F == T)) (MP (ASSUME (T ==> F)) TRUTH)
476 val tht = BOOL_CASE (sch T t2b) t2b t2b
477 (dsch T T (REFL T)) (dsch F T (SYM abs))
478 val thf = BOOL_CASE (sch F t2b) t2b t2b
479 (dsch T F abs) (dsch F F (REFL F))
480 in
481 GEN t1b (GEN t2b (BOOL_CASE (sch t1b t2b) t1b t1b tht thf))
482 end);
483
484fun IMP_ANTISYM_RULE th1 th2 =
485 let val (ant,conseq) = dest_imp(concl th1)
486 in
487 MP (MP (SPEC conseq (SPEC ant IMP_ANTISYM_AX)) th1) th2
488 end;
489
490
491(*---------------------------------------------------------------------------
492 * |- !t. F ==> t
493 *---------------------------------------------------------------------------*)
494
495val FALSITY = thm (#(FILE), #(LINE))("FALSITY", GEN tb (FALSITY_CONV tb))
496
497fun CONTR tm th = MP (SPEC tm FALSITY) th
498
499fun DISJ_IMP dth =
500 let val (disj1,disj2) = dest_disj (concl dth)
501 val nota = mk_neg disj1
502 in
503 DISCH nota
504 (DISJ_CASES dth
505 (CONTR disj2 (MP (ASSUME nota) (ASSUME disj1)))
506 (ASSUME disj2))
507 end
508
509fun EQF_INTRO th = IMP_ANTISYM_RULE (NOT_ELIM th)
510 (DISCH “F” (CONTR (dest_neg (concl th)) (ASSUME “F”)));
511
512fun SELECT_EQ x =
513 let val ty = type_of x
514 val choose = mk_const("@", (ty --> Type.bool) --> ty)
515 in
516 fn th => AP_TERM choose (ABS x th)
517 end
518
519fun GENL varl thm = itlist GEN varl thm;
520
521fun SPECL tm_list th = rev_itlist SPEC tm_list th
522
523fun GEN_ALL th =
524 itlist GEN (op_set_diff aconv (free_vars(concl th)) (free_varsl (hyp th))) th;
525
526local fun f v (vs,l) = let val v' = variant vs v in (v'::vs, v'::l) end
527in
528fun SPEC_ALL th =
529 let val (hvs,con) = (free_varsl ## I) (hyp th, concl th)
530 val fvs = free_vars con
531 and vars = fst(strip_forall con)
532 in
533 SPECL (snd(itlist f vars (hvs@fvs,[]))) th
534 end
535end;
536
537fun SUBST_CONV theta template tm =
538 let fun retheta {redex,residue} = (redex |-> genvar(type_of redex))
539 val theta0 = map retheta theta
540 val theta1 = map (op |-> o (#residue ## #residue)) (zip theta0 theta)
541 in
542 SUBST theta1 (mk_eq(tm,subst theta0 template)) (REFL tm)
543 end;
544
545local fun combine [] [] = []
546 | combine (v::rst1) (t::rst2) = (v |-> t) :: combine rst1 rst2
547 | combine _ _ = raise Fail "SUBS"
548in
549fun SUBS ths th =
550 let val ls = map (lhs o concl) ths
551 val vars = map (genvar o type_of) ls
552 val w = subst (combine ls vars) (concl th)
553 in
554 SUBST (combine vars ths) w th
555 end
556end;
557
558fun IMP_TRANS th1 th2 =
559 let val (ant,conseq) = dest_imp(concl th1)
560 in DISCH ant (MP th2 (MP th1 (ASSUME ant))) end;
561
562fun ADD_ASSUM t th = MP (DISCH t th) (ASSUME t);
563
564fun SPEC_VAR th =
565 let val (Bvar,_) = dest_forall (concl th)
566 val bv' = variant (free_varsl (hyp th)) Bvar
567 in (bv', SPEC bv' th)
568 end;
569
570fun MK_EXISTS bodyth =
571 let val (x, sth) = SPEC_VAR bodyth
572 val (a,b) = dest_eq (concl sth)
573 val (abimp,baimp) = EQ_IMP_RULE sth
574 fun HALF (p,q) pqimp =
575 let val xp = mk_exists(x,p)
576 and xq = mk_exists(x,q)
577 in DISCH xp
578 (CHOOSE (x, ASSUME xp) (EXISTS (xq,x) (MP pqimp (ASSUME p))))
579 end
580 in
581 IMP_ANTISYM_RULE (HALF (a,b) abimp) (HALF (b,a) baimp)
582 end;
583
584fun SELECT_RULE th =
585 let val (tm as (Bvar, Body)) = dest_exists(concl th)
586 val v = genvar(type_of Bvar)
587 val P = mk_abs tm
588 val SELECT_AX' = INST_TYPE[alpha |-> type_of Bvar] SELECT_AX
589 val th1 = SPEC v (SPEC P SELECT_AX')
590 val (ant,conseq) = dest_imp(concl th1)
591 val th2 = BETA_CONV ant
592 and th3 = BETA_CONV conseq
593 val th4 = EQ_MP th3 (MP th1 (EQ_MP(SYM th2) (ASSUME (rhs(concl th2)))))
594 in
595 CHOOSE (v,th) th4
596 end;
597
598
599(*---------------------------------------------------------------------------
600 ETA_THM = |- !M. (\x. M x) = M
601 ---------------------------------------------------------------------------*)
602
603val ETA_THM = thm (#(FILE), #(LINE))
604 ("ETA_THM", GEN_ALL(ETA_CONV “\x:'a. (M x:'b)”));
605
606(*---------------------------------------------------------------------------
607 * |- !t. t \/ ~t
608 *---------------------------------------------------------------------------*)
609
610val EXCLUDED_MIDDLE = thm (#(FILE), #(LINE))(
611 "EXCLUDED_MIDDLE",
612 let val th1 = RIGHT_BETA(AP_THM NOT_DEF tb)
613 val th2 = DISJ1 (EQT_ELIM (ASSUME (tb == T))) (mk_neg tb)
614 and th3 = DISJ2 tb (EQ_MP (SYM th1)
615 (DISCH tb (EQ_MP (ASSUME (tb == F))
616 (ASSUME tb))))
617 in
618 GEN tb (DISJ_CASES (SPEC tb BOOL_CASES_AX) th2 th3)
619 end)
620
621fun IMP_ELIM th =
622 let val (ant,conseq) = dest_imp (concl th)
623 val not_t1 = mk_neg ant
624 in
625 DISJ_CASES (SPEC ant EXCLUDED_MIDDLE)
626 (DISJ2 not_t1 (MP th (ASSUME ant)))
627 (DISJ1 (ASSUME not_t1) conseq)
628 end;
629
630(*---------------------------------------------------------------------------*
631 * |- !f y. (\x. f x) y = f y *
632 *---------------------------------------------------------------------------*)
633
634val BETA_THM = thm (#(FILE), #(LINE))(
635 "BETA_THM",
636 GENL [fabt, ya] (BETA_CONV “(\x. (f:'a->'b) x) y”))
637
638(*---------------------------------------------------------------------------
639 LET_THM = |- !f x. LET f x = f x
640 ---------------------------------------------------------------------------*)
641
642val LET_THM = thm (#(FILE), #(LINE))(
643 "LET_THM",
644 GEN fabt (GEN xa
645 (RIGHT_BETA(AP_THM (RIGHT_BETA(AP_THM LET_DEF fabt)) xa))))
646
647(* |- $! f <=> !x. f x *)
648val FORALL_THM = thm (#(FILE), #(LINE))(
649 "FORALL_THM",
650 SYM (AP_TERM “$! :('a->bool)->bool”
651 (ETA_CONV “\x:'a. f x:bool”)))
652
653(* |- $? f <=> ?x. f x *)
654val EXISTS_THM = thm (#(FILE), #(LINE))(
655 "EXISTS_THM",
656 SYM (AP_TERM “$? :('a->bool)->bool”
657 (ETA_CONV “\x:'a. f x:bool”)));
658
659(*---------------------------------------------------------------------------*
660 * |- !t1:'a. !t2:'b. (\x. t1) t2 = t1 *
661 *---------------------------------------------------------------------------*)
662
663val ABS_SIMP = thm (#(FILE), #(LINE))("ABS_SIMP",
664 GENL [“t1:'a”, “t2:'b”]
665 (BETA_CONV “(\x:'b. t1:'a) t2”));
666
667(*---------------------------------------------------------------------------
668 * |- !t. (!x.t) = t
669 *---------------------------------------------------------------------------*)
670
671val FORALL_SIMP = thm (#(FILE), #(LINE))(
672 "FORALL_SIMP",
673 GEN tb (IMP_ANTISYM_RULE
674 (DISCH “!^xa. ^tb” (SPEC xa (ASSUME “!^xa.^tb”)))
675 (DISCH tb (GEN xa (ASSUME tb)))));
676
677(*---------------------------------------------------------------------------
678 * |- !t. (?x.t) = t
679 *---------------------------------------------------------------------------*)
680
681val EXISTS_SIMP = thm (#(FILE), #(LINE))(
682 "EXISTS_SIMP",
683 let val ext = mk_exists(xa,tb)
684 in
685 GEN tb (IMP_ANTISYM_RULE
686 (DISCH ext (CHOOSE(Av "p", ASSUME ext) (ASSUME tb)))
687 (DISCH tb (EXISTS(ext, Av "r") (ASSUME tb))))
688 end);
689
690(*---------------------------------------------------------------------------
691 * |- !t1 t2. t1 ==> t2 ==> t1 /\ t2
692 *---------------------------------------------------------------------------*)
693
694val AND_INTRO_THM = thm (#(FILE), #(LINE))(
695 "AND_INTRO_THM",
696 let val t12 = t1b ==> t2b ==> tb
697 val th1 = GEN tb (DISCH t12 (MP (MP (ASSUME t12)
698 (ASSUME t1b))
699 (ASSUME t2b)))
700 val th2 = RIGHT_BETA(AP_THM (RIGHT_BETA(AP_THM AND_DEF t1b)) t2b)
701 in
702 GEN t1b (GEN t2b (DISCH t1b (DISCH t2b (EQ_MP (SYM th2) th1))))
703 end);
704
705(*---------------------------------------------------------------------------
706 * |- !t1 t2. t1 /\ t2 ==> t1
707 *---------------------------------------------------------------------------*)
708
709val AND1_THM = thm (#(FILE), #(LINE))(
710 "AND1_THM",
711 let val t12 = mk_conj(t1b, t2b)
712 val th2 = RIGHT_BETA(AP_THM (RIGHT_BETA(AP_THM AND_DEF t1b)) t2b)
713 val th3 = SPEC t1b (EQ_MP th2 (ASSUME t12))
714 val th4 = DISCH t1b (DISCH t2b (ADD_ASSUM t2b (ASSUME t1b)))
715 in
716 GEN t1b (GEN t2b (DISCH t12 (MP th3 th4)))
717 end);
718
719(*---------------------------------------------------------------------------
720 * |- !t1 t2. t1 /\ t2 ==> t2
721 *---------------------------------------------------------------------------*)
722
723val AND2_THM = thm (#(FILE), #(LINE))("AND2_THM",
724 let val t1 = “t1:bool”
725 and t2 = “t2:bool”
726 val th1 = ASSUME “^t1 /\ ^t2”
727 val th2 = RIGHT_BETA(AP_THM (RIGHT_BETA(AP_THM AND_DEF t1)) t2)
728 val th3 = SPEC t2 (EQ_MP th2 th1)
729 val th4 = DISCH t1 (DISCH t2 (ADD_ASSUM t1 (ASSUME t2)))
730 in
731 GEN t1 (GEN t2 (DISCH “^t1 /\ ^t2” (MP th3 th4)))
732 end);
733
734(* CONJ, CONJUNCT1 and CONJUNCT2 should be built here.*)
735
736fun CONJ_PAIR thm = (CONJUNCT1 thm, CONJUNCT2 thm);
737
738fun CONJUNCTS th =
739 (CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th)) handle _ => [th];
740
741val LIST_CONJ = end_itlist CONJ
742
743(*---------------------------------------------------------------------------
744 * |- !t1 t2. (t1 /\ t2) = (t2 /\ t1)
745 *---------------------------------------------------------------------------*)
746
747val CONJ_SYM = thm (#(FILE), #(LINE))("CONJ_SYM",
748 let val t1 = “t1:bool”
749 and t2 = “t2:bool”
750 val th1 = ASSUME “^t1 /\ ^t2”
751 and th2 = ASSUME “^t2 /\ ^t1”
752 in
753 GEN t1 (GEN t2 (IMP_ANTISYM_RULE
754 (DISCH “^t1 /\ ^t2”
755 (CONJ(CONJUNCT2 th1)(CONJUNCT1 th1)))
756 (DISCH “^t2 /\ ^t1”
757 (CONJ(CONJUNCT2 th2)(CONJUNCT1 th2)))))
758 end);
759
760val _ = thm (#(FILE), #(LINE))("CONJ_COMM", CONJ_SYM);
761
762(*---------------------------------------------------------------------------
763 * |- !t1 t2 t3. t1 /\ (t2 /\ t3) = (t1 /\ t2) /\ t3
764 *---------------------------------------------------------------------------*)
765
766val CONJ_ASSOC = thm (#(FILE), #(LINE))("CONJ_ASSOC",
767 let val t1 = “t1:bool”
768 and t2 = “t2:bool”
769 and t3 = “t3:bool”
770 val th1 = ASSUME “^t1 /\ (^t2 /\ ^t3)”
771 val th2 = ASSUME “(^t1 /\ ^t2) /\ ^t3”
772 val th3 = DISCH “^t1 /\ (^t2 /\ ^t3)”
773 (CONJ (CONJ(CONJUNCT1 th1)
774 (CONJUNCT1(CONJUNCT2 th1)))
775 (CONJUNCT2(CONJUNCT2 th1)))
776 and th4 = DISCH “(^t1 /\ ^t2) /\ ^t3”
777 (CONJ (CONJUNCT1(CONJUNCT1 th2))
778 (CONJ(CONJUNCT2(CONJUNCT1 th2))
779 (CONJUNCT2 th2)))
780 in
781 GEN t1 (GEN t2 (GEN t3 (IMP_ANTISYM_RULE th3 th4)))
782 end);
783
784(*---------------------------------------------------------------------------
785 * |- !t1 t2. t1 ==> t1 \/ t2
786 *---------------------------------------------------------------------------*)
787
788val OR_INTRO_THM1 = thm (#(FILE), #(LINE))("OR_INTRO_THM1",
789 let val t = “t:bool”
790 and t1 = “t1:bool”
791 and t2 = “t2:bool”
792 val th1 = ADD_ASSUM “^t2 ==> ^t” (MP (ASSUME “^t1 ==> ^t”)
793 (ASSUME t1))
794 val th2 = GEN t (DISCH “^t1 ==> ^t” (DISCH “^t2 ==> ^t” th1))
795 val th3 = RIGHT_BETA(AP_THM (RIGHT_BETA(AP_THM OR_DEF t1)) t2)
796 in
797 GEN t1 (GEN t2 (DISCH t1 (EQ_MP (SYM th3) th2)))
798 end);
799
800(*---------------------------------------------------------------------------
801 * |- !t1 t2. t2 ==> t1 \/ t2
802 *---------------------------------------------------------------------------*)
803
804val OR_INTRO_THM2 = thm (#(FILE), #(LINE))("OR_INTRO_THM2",
805 let val t = “t:bool”
806 and t1 = “t1:bool”
807 and t2 = “t2:bool”
808 val th1 = ADD_ASSUM “^t1 ==> ^t”
809 (MP (ASSUME “^t2 ==> ^t”) (ASSUME t2))
810 val th2 = GEN t (DISCH “^t1 ==> ^t” (DISCH “^t2 ==> ^t” th1))
811 val th3 = RIGHT_BETA(AP_THM (RIGHT_BETA(AP_THM OR_DEF t1)) t2)
812 in
813 GEN t1 (GEN t2 (DISCH t2 (EQ_MP (SYM th3) th2)))
814 end);
815
816(*---------------------------------------------------------------------------
817 * |- !t t1 t2. (t1 \/ t2) ==> (t1 ==> t) ==> (t2 ==> t) ==> t
818 *---------------------------------------------------------------------------*)
819
820val OR_ELIM_THM = thm (#(FILE), #(LINE))("OR_ELIM_THM",
821 let val t = “t:bool”
822 and t1 = “t1:bool”
823 and t2 = “t2:bool”
824 val th1 = ASSUME “^t1 \/ ^t2”
825 val th2 = UNFOLD_OR_CONV (concl th1)
826 val th3 = SPEC t (EQ_MP th2 th1)
827 val th4 = MP (MP th3 (ASSUME “^t1 ==> ^t”))
828 (ASSUME “^t2 ==> ^t”)
829 val th4 = DISCH “^t1 ==> ^t” (DISCH “^t2 ==> ^t” th4)
830 in
831 GEN t (GEN t1 (GEN t2 (DISCH “^t1 \/ ^t2” th4)))
832 end);
833
834(* DISJ1, DISJ2, DISJ_CASES should be built here. *)
835
836fun DISJ_CASES_UNION dth ath bth =
837 DISJ_CASES dth (DISJ1 ath (concl bth)) (DISJ2 (concl ath) bth);
838
839(*---------------------------------------------------------------------------
840 * |- !t. (t ==> F) ==> ~t
841 *---------------------------------------------------------------------------*)
842
843val IMP_F = thm (#(FILE), #(LINE))("IMP_F",
844 let val t = “t:bool”
845 val th1 = RIGHT_BETA (AP_THM NOT_DEF t)
846 in
847 GEN t (DISCH “^t ==> F”
848 (EQ_MP (SYM th1) (ASSUME “^t ==> F”)))
849 end);
850
851(*---------------------------------------------------------------------------
852 * |- !t. ~t ==> (t ==> F)
853 *---------------------------------------------------------------------------*)
854
855val F_IMP = thm (#(FILE), #(LINE))("F_IMP",
856 let val t = “t:bool”
857 val th1 = RIGHT_BETA(AP_THM NOT_DEF t)
858 in
859 GEN t (DISCH “~^t”
860 (EQ_MP th1 (ASSUME “~^t”)))
861 end);
862
863(*---------------------------------------------------------------------------
864 * |- !t. ~t ==> (t=F)
865 *---------------------------------------------------------------------------*)
866
867val NOT_F = thm (#(FILE), #(LINE))("NOT_F",
868 let val t = “t:bool”
869 val th1 = MP (SPEC t F_IMP) (ASSUME “~ ^t”)
870 and th2 = SPEC t FALSITY
871 val th3 = IMP_ANTISYM_RULE th1 th2
872 in
873 GEN t (DISCH “~^t” th3)
874 end);
875
876(*---------------------------------------------------------------------------
877 * |- !t. ~(t /\ ~t)
878 *---------------------------------------------------------------------------*)
879
880val NOT_AND = thm (#(FILE), #(LINE))("NOT_AND",
881 let val th = ASSUME “t /\ ~t”
882 in NOT_INTRO(DISCH “t /\ ~t” (MP (CONJUNCT2 th) (CONJUNCT1 th)))
883 end);
884
885(*---------------------------------------------------------------------------
886 * |- !t. (T /\ t) = t
887 *---------------------------------------------------------------------------*)
888
889val AND_CLAUSE1 =
890 let val t = “t:bool”
891 val th1 = DISCH “T /\ ^t” (CONJUNCT2(ASSUME “T /\ ^t”))
892 and th2 = DISCH t (CONJ TRUTH (ASSUME t))
893 in
894 GEN t (IMP_ANTISYM_RULE th1 th2)
895 end;
896
897(*---------------------------------------------------------------------------
898 * |- !t. (t /\ T) = t
899 *---------------------------------------------------------------------------*)
900
901val AND_CLAUSE2 =
902 let val t = “t:bool”
903 val th1 = DISCH “^t /\ T” (CONJUNCT1(ASSUME “^t /\ T”))
904 and th2 = DISCH t (CONJ (ASSUME t) TRUTH)
905 in
906 GEN t (IMP_ANTISYM_RULE th1 th2)
907 end;
908
909(*---------------------------------------------------------------------------
910 * |- !t. (F /\ t) = F
911 *---------------------------------------------------------------------------*)
912
913val AND_CLAUSE3 =
914 let val t = “t:bool”
915 val th1 = IMP_TRANS (SPEC t (SPEC “F” AND1_THM))
916 (SPEC “F” FALSITY)
917 and th2 = SPEC “F /\ ^t” FALSITY
918 in
919 GEN t (IMP_ANTISYM_RULE th1 th2)
920 end;
921
922(*---------------------------------------------------------------------------
923 * |- !t. (t /\ F) = F
924 *---------------------------------------------------------------------------*)
925
926val AND_CLAUSE4 =
927 let val t = “t:bool”
928 val th1 = IMP_TRANS (SPEC “F” (SPEC t AND2_THM))
929 (SPEC “F” FALSITY)
930 and th2 = SPEC “^t /\ F” FALSITY
931 in
932 GEN t (IMP_ANTISYM_RULE th1 th2)
933 end;
934
935(*---------------------------------------------------------------------------
936 * |- !t. (t /\ t) = t
937 *---------------------------------------------------------------------------*)
938
939val AND_CLAUSE5 =
940 let val t = “t:bool”
941 val th1 = DISCH “^t /\ ^t” (CONJUNCT1(ASSUME “^t /\ ^t”))
942 and th2 = DISCH t (CONJ(ASSUME t)(ASSUME t))
943 in
944 GEN t (IMP_ANTISYM_RULE th1 th2)
945 end;
946
947(*---------------------------------------------------------------------------
948 * |- !t. (T /\ t) = t /\
949 * (t /\ T) = t /\
950 * (F /\ t) = F /\
951 * (t /\ F) = F /\
952 * (t /\ t) = t
953 *---------------------------------------------------------------------------*)
954
955val AND_CLAUSES = thm (#(FILE), #(LINE))("AND_CLAUSES",
956 let val t = “t:bool”
957 in
958 GEN t (LIST_CONJ [SPEC t AND_CLAUSE1, SPEC t AND_CLAUSE2,
959 SPEC t AND_CLAUSE3, SPEC t AND_CLAUSE4,
960 SPEC t AND_CLAUSE5])
961 end);
962
963(*---------------------------------------------------------------------------
964 * |- !t. (T \/ t) = T
965 *---------------------------------------------------------------------------*)
966
967val OR_CLAUSE1 =
968 let val t = “t:bool”
969 val th1 = DISCH “T \/ ^t” TRUTH
970 and th2 = DISCH “T” (DISJ1 TRUTH t)
971 in
972 GEN t (IMP_ANTISYM_RULE th1 th2)
973 end;
974
975(*---------------------------------------------------------------------------
976 * |- !t. (t \/ T) = T
977 *---------------------------------------------------------------------------*)
978
979val OR_CLAUSE2 =
980 let val t = “t:bool”
981 val th1 = DISCH “^t \/ T” TRUTH
982 and th2 = DISCH “T” (DISJ2 t TRUTH)
983 in
984 GEN t (IMP_ANTISYM_RULE th1 th2)
985 end;
986
987(*---------------------------------------------------------------------------
988 * |- (F \/ t) = t
989 *---------------------------------------------------------------------------*)
990
991val OR_CLAUSE3 =
992 let val t = “t:bool”
993 val th1 = DISCH “F \/ ^t” (DISJ_CASES (ASSUME “F \/ ^t”)
994 (UNDISCH (SPEC t FALSITY))
995 (ASSUME t))
996 and th2 = SPEC t (SPEC “F” OR_INTRO_THM2)
997 in
998 GEN t (IMP_ANTISYM_RULE th1 th2)
999 end;
1000
1001(*---------------------------------------------------------------------------
1002 * |- !t. (t \/ F) = t
1003 *---------------------------------------------------------------------------*)
1004
1005val OR_CLAUSE4 =
1006 let val t = “t:bool”
1007 val th1 = DISCH “^t \/ F” (DISJ_CASES (ASSUME “^t \/ F”)
1008 (ASSUME t)
1009 (UNDISCH (SPEC t FALSITY)))
1010 and th2 = SPEC “F” (SPEC t OR_INTRO_THM1)
1011 in
1012 GEN t (IMP_ANTISYM_RULE th1 th2)
1013 end;
1014
1015(*---------------------------------------------------------------------------
1016 * |- !t. (t \/ t) = t
1017 *---------------------------------------------------------------------------*)
1018
1019val OR_CLAUSE5 =
1020 let val t = “t:bool”
1021 val th1 = DISCH “^t \/ ^t”
1022 (DISJ_CASES(ASSUME “^t \/ ^t”) (ASSUME t) (ASSUME t))
1023 and th2 = DISCH t (DISJ1(ASSUME t)t)
1024 in
1025 GEN t (IMP_ANTISYM_RULE th1 th2)
1026 end;
1027
1028(*---------------------------------------------------------------------------
1029 * |- !t. (T \/ t) = T /\
1030 * (t \/ T) = T /\
1031 * (F \/ t) = t /\
1032 * (t \/ F) = t /\
1033 * (t \/ t) = t
1034 *---------------------------------------------------------------------------*)
1035
1036val OR_CLAUSES = thm (#(FILE), #(LINE))("OR_CLAUSES",
1037 let val t = “t:bool”
1038 in
1039 GEN t (LIST_CONJ [SPEC t OR_CLAUSE1, SPEC t OR_CLAUSE2,
1040 SPEC t OR_CLAUSE3, SPEC t OR_CLAUSE4,
1041 SPEC t OR_CLAUSE5])
1042 end);
1043
1044(*---------------------------------------------------------------------------
1045 * |- !t. (T ==> t) = t
1046 *---------------------------------------------------------------------------*)
1047
1048val IMP_CLAUSE1 =
1049 let val t = “t:bool”
1050 val th1 = DISCH “T ==> ^t” (MP (ASSUME “T ==> ^t”) TRUTH)
1051 and th2 = DISCH t (DISCH “T” (ADD_ASSUM “T” (ASSUME t)))
1052 in
1053 GEN t (IMP_ANTISYM_RULE th1 th2)
1054 end;
1055
1056(*---------------------------------------------------------------------------
1057 * |- !t. (F ==> t) = T
1058 *---------------------------------------------------------------------------*)
1059
1060val IMP_CLAUSE2 =
1061 let val t = “t:bool”
1062 in GEN t (EQT_INTRO(SPEC t FALSITY))
1063 end;
1064
1065(*---------------------------------------------------------------------------
1066 * |- !t. (t ==> T) = T
1067 *---------------------------------------------------------------------------*)
1068
1069val IMP_CLAUSE3 =
1070 let val t = “t:bool”
1071 in GEN t (EQT_INTRO(DISCH t (ADD_ASSUM t TRUTH)))
1072 end;
1073
1074(*---------------------------------------------------------------------------
1075 * |- ((T ==> F) = F) /\ ((F ==> F) = T)
1076 *---------------------------------------------------------------------------*)
1077val IMP_CLAUSE4 =
1078 let val th1 = DISCH “T ==> F” (MP (ASSUME “T ==> F”) TRUTH)
1079 and th2 = SPEC “T ==> F” FALSITY
1080 and th3 = EQT_INTRO(DISCH “F” (ASSUME “F”))
1081 in
1082 CONJ(IMP_ANTISYM_RULE th1 th2) th3
1083 end;
1084
1085(*---------------------------------------------------------------------------
1086 * |- !t. (t ==> F) = ~t
1087 *---------------------------------------------------------------------------*)
1088
1089val IMP_CLAUSE5 =
1090 let val t = “t:bool”
1091 val th1 = SPEC t IMP_F
1092 and th2 = SPEC t F_IMP
1093 in
1094 GEN t (IMP_ANTISYM_RULE th1 th2)
1095 end;
1096
1097(*---------------------------------------------------------------------------
1098 * |- !t. (T ==> t) = t /\
1099 * (t ==> T) = T /\
1100 * (F ==> t) = T /\
1101 * (t ==> t) = t /\
1102 * (t ==> F) = ~t
1103 *---------------------------------------------------------------------------*)
1104
1105val IMP_CLAUSES = thm (#(FILE), #(LINE))("IMP_CLAUSES",
1106 let val t = “t:bool”
1107 in GEN t
1108 (LIST_CONJ [SPEC t IMP_CLAUSE1, SPEC t IMP_CLAUSE3,
1109 SPEC t IMP_CLAUSE2, EQT_INTRO(DISCH t (ASSUME t)),
1110 SPEC t IMP_CLAUSE5])
1111 end);
1112
1113(* ----------------------------------------------------------------------
1114 |- !t1 t2. (t1 <=> t2) ==> (t1 ==> t2)
1115 ---------------------------------------------------------------------- *)
1116
1117val EQ_IMPLIES =
1118 let
1119 val impt1 = REFL $ mk_comb(implication, t1b)
1120 val eqt = mk_eq(t1b,t2b)
1121 val t1_eq_t2 = ASSUME eqt
1122 val th0 = MK_COMB(impt1,t1_eq_t2)
1123 val imp_refl = IMP_CLAUSES |> SPEC t1b |> CONJUNCTS |> el 4 |> EQT_ELIM
1124 in
1125 thm (#(FILE), #(LINE))(
1126 "EQ_IMPLIES", EQ_MP th0 imp_refl |> DISCH eqt |> GENL [t1b,t2b]
1127 )
1128 end
1129
1130
1131(*----------------------------------------------------------------------------
1132 * |- (~~t = t) /\ (~T = F) /\ (~F = T)
1133 *---------------------------------------------------------------------------*)
1134
1135val NOT_CLAUSES = thm (#(FILE), #(LINE))("NOT_CLAUSES",
1136 CONJ
1137 (GEN “t:bool”
1138 (IMP_ANTISYM_RULE
1139 (DISJ_IMP(IMP_ELIM(DISCH “t:bool” (ASSUME “t:bool”))))
1140 (DISCH “t:bool”
1141 (NOT_INTRO(DISCH “~t” (UNDISCH (NOT_ELIM(ASSUME “~t”))))))))
1142 (CONJ (IMP_ANTISYM_RULE
1143 (DISCH “~T”
1144 (MP (MP (SPEC “T” F_IMP) (ASSUME “~T”)) TRUTH))
1145 (SPEC “~T” FALSITY))
1146 (IMP_ANTISYM_RULE (DISCH “~F” TRUTH)
1147 (DISCH “T” (MP (SPEC “F” IMP_F)
1148 (SPEC “F” FALSITY))))));
1149
1150(*---------------------------------------------------------------------------
1151 * |- !x. x=x
1152 *---------------------------------------------------------------------------*)
1153
1154val EQ_REFL = thm (#(FILE), #(LINE))("EQ_REFL", GEN “x : 'a” (REFL “x : 'a”));
1155
1156(*---------------------------------------------------------------------------
1157 * |- !x. (x=x) = T
1158 *---------------------------------------------------------------------------*)
1159
1160val REFL_CLAUSE = thm (#(FILE), #(LINE))("REFL_CLAUSE",
1161 GEN “x: 'a” (EQT_INTRO(SPEC “x:'a” EQ_REFL)));
1162
1163(*---------------------------------------------------------------------------
1164 * |- !x y. x=y ==> y=x
1165 *---------------------------------------------------------------------------*)
1166
1167val EQ_SYM = thm (#(FILE), #(LINE))("EQ_SYM",
1168 let val x = “x:'a”
1169 and y = “y:'a”
1170 in
1171 GEN x (GEN y (DISCH “^x = ^y” (SYM(ASSUME “^x = ^y”))))
1172 end);
1173
1174(*---------------------------------------------------------------------------
1175 * |- !x y. (x = y) = (y = x)
1176 *---------------------------------------------------------------------------*)
1177
1178val EQ_SYM_EQ = thm (#(FILE), #(LINE))("EQ_SYM_EQ",
1179 GEN “x:'a”
1180 (GEN “y:'a”
1181 (IMP_ANTISYM_RULE (SPEC “y:'a” (SPEC “x:'a” EQ_SYM))
1182 (SPEC “x:'a” (SPEC “y:'a” EQ_SYM)))));
1183
1184(*---------------------------------------------------------------------------
1185 * |- !f g. (!x. f x = g x) ==> f=g
1186 *---------------------------------------------------------------------------*)
1187
1188val EQ_EXT = thm (#(FILE), #(LINE))("EQ_EXT",
1189 let val f = “f:'a->'b”
1190 and g = “g: 'a -> 'b”
1191 in
1192 GEN f (GEN g (DISCH “!x:'a. ^f (x:'a) = ^g (x:'a)”
1193 (EXT(ASSUME “!x:'a. ^f (x:'a) = ^g (x:'a)”))))
1194 end);
1195
1196(*---------------------------------------------------------------------------
1197 FUN_EQ_THM |- !f g. (f = g) = !x. f x = g x
1198 ---------------------------------------------------------------------------*)
1199
1200val FUN_EQ_THM = thm (#(FILE), #(LINE))("FUN_EQ_THM",
1201 let val f = mk_var("f", Type.alpha --> Type.beta)
1202 val g = mk_var("g", Type.alpha --> Type.beta)
1203 val x = mk_var("x", Type.alpha)
1204 val f_eq_g = mk_eq(f,g)
1205 val fx_eq_gx = mk_eq(mk_comb(f,x),mk_comb(g,x))
1206 val uq_f_eq_g = mk_forall(x,fx_eq_gx)
1207 val th1 = GEN x (AP_THM (ASSUME f_eq_g) x);
1208 val th2 = MP (SPEC_ALL EQ_EXT) (ASSUME uq_f_eq_g);
1209 in
1210 GEN f (GEN g
1211 (IMP_ANTISYM_RULE (DISCH_ALL th1) (DISCH_ALL th2)))
1212 end);
1213
1214(*---------------------------------------------------------------------------
1215 * |- !x y z. x=y /\ y=z ==> x=z
1216 *---------------------------------------------------------------------------*)
1217
1218val EQ_TRANS = thm (#(FILE), #(LINE))("EQ_TRANS",
1219 let val x = “x:'a”
1220 and y = “y:'a”
1221 and z = “z:'a”
1222 val xyyz = “(^x = ^y) /\ (^y = ^z)”
1223 in
1224 GEN x
1225 (GEN y
1226 (GEN z
1227 (DISCH xyyz
1228 (TRANS (CONJUNCT1(ASSUME xyyz))
1229 (CONJUNCT2(ASSUME xyyz))))))
1230 end);
1231
1232(*---------------------------------------------------------------------------
1233 * |- ~(T=F) /\ ~(F=T)
1234 *---------------------------------------------------------------------------*)
1235
1236val BOOL_EQ_DISTINCT = thm (#(FILE), #(LINE))("BOOL_EQ_DISTINCT",
1237 let val TF = “T = F”
1238 and FT = “F = T”
1239 in
1240 CONJ
1241 (NOT_INTRO(DISCH TF (EQ_MP (ASSUME TF) TRUTH)))
1242 (NOT_INTRO(DISCH FT (EQ_MP (SYM(ASSUME FT)) TRUTH)))
1243 end);
1244
1245(*---------------------------------------------------------------------------
1246 * |- !t. (T = t) = t
1247 *---------------------------------------------------------------------------*)
1248
1249val EQ_CLAUSE1 =
1250 let val t = “t:bool”
1251 val Tt = “T = ^t”
1252 val th1 = DISCH Tt (EQ_MP (ASSUME Tt) TRUTH)
1253 and th2 = DISCH t (SYM(EQT_INTRO(ASSUME t)))
1254 in
1255 GEN t (IMP_ANTISYM_RULE th1 th2)
1256 end;
1257
1258(*---------------------------------------------------------------------------
1259 * |- !t. (t = T) = t
1260 *---------------------------------------------------------------------------*)
1261
1262val EQ_CLAUSE2 =
1263 let val t = “t:bool”
1264 val tT = “^t = T”
1265 val th1 = DISCH tT (EQ_MP (SYM (ASSUME tT)) TRUTH)
1266 and th2 = DISCH t (EQT_INTRO(ASSUME t))
1267 in
1268 GEN t (IMP_ANTISYM_RULE th1 th2)
1269 end;
1270
1271(*---------------------------------------------------------------------------
1272 * |- !t. (F = t) = ~t
1273 *---------------------------------------------------------------------------*)
1274
1275val EQ_CLAUSE3 =
1276 let val t = “t:bool”
1277 val Ft = “F = ^t”
1278 val tF = “^t = F”
1279 val th1 = DISCH Ft (MP (SPEC t IMP_F)
1280 (DISCH t (EQ_MP(SYM(ASSUME Ft))
1281 (ASSUME t))))
1282 and th2 = IMP_TRANS (SPEC t NOT_F)
1283 (DISCH tF (SYM(ASSUME tF)))
1284 in
1285 GEN t (IMP_ANTISYM_RULE th1 th2)
1286 end;
1287
1288(*---------------------------------------------------------------------------
1289 * |- !t. (t = F) = ~t
1290 *---------------------------------------------------------------------------*)
1291
1292val EQ_CLAUSE4 =
1293 let val t = “t:bool”
1294 val tF = “^t = F”
1295 val th1 = DISCH tF (MP (SPEC t IMP_F)
1296 (DISCH t (EQ_MP(ASSUME tF)
1297 (ASSUME t))))
1298 and th2 = SPEC t NOT_F
1299 in
1300 GEN t (IMP_ANTISYM_RULE th1 th2)
1301 end;
1302
1303(*---------------------------------------------------------------------------
1304 * |- !t. (T = t) = t /\
1305 * (t = T) = t /\
1306 * (F = t) = ~t /\
1307 * (t = F) = ~t
1308 *---------------------------------------------------------------------------*)
1309
1310val EQ_CLAUSES = thm (#(FILE), #(LINE))("EQ_CLAUSES",
1311 let val t = “t:bool”
1312 in
1313 GEN t (LIST_CONJ [SPEC t EQ_CLAUSE1, SPEC t EQ_CLAUSE2,
1314 SPEC t EQ_CLAUSE3, SPEC t EQ_CLAUSE4])
1315 end);
1316
1317(*---------------------------------------------------------------------------
1318 * |- !t1 t2 :'a. COND T t1 t2 = t1
1319 *---------------------------------------------------------------------------*)
1320
1321val COND_CLAUSE1 =
1322 let val (x,t1,t2,v) = (“x:'a”, “t1:'a”,
1323 “t2:'a”, genvar Type.bool)
1324 val th1 = RIGHT_BETA(AP_THM
1325 (RIGHT_BETA(AP_THM
1326 (RIGHT_BETA(AP_THM COND_DEF “T”)) t1))t2)
1327 val TT = EQT_INTRO(REFL “T”)
1328 val th2 = SUBST [v |-> SYM TT]
1329 “(^v ==> (^x=^t1)) = (^x=^t1)”
1330 (CONJUNCT1 (SPEC “^x=^t1” IMP_CLAUSES))
1331 and th3 = DISCH “T=F”
1332 (MP (SPEC “^x=^t2” FALSITY)
1333 (UNDISCH(MP (SPEC “T=F” F_IMP)
1334 (CONJUNCT1 BOOL_EQ_DISTINCT))))
1335 val th4 = DISCH “^x=^t1”
1336 (CONJ(EQ_MP(SYM th2)(ASSUME “^x=^t1”))th3)
1337 and th5 = DISCH “((T=T) ==> (^x=^t1))/\((T=F) ==> (^x=^t2))”
1338 (MP (CONJUNCT1(ASSUME “((T=T) ==> (^x=^t1))/\
1339 ((T=F) ==> (^x=^t2))”))
1340 (REFL “T”))
1341 val th6 = IMP_ANTISYM_RULE th4 th5
1342 val th7 = TRANS th1 (SYM(SELECT_EQ x th6))
1343 val th8 = EQ_MP (SYM(BETA_CONV “(\ ^x.^x = ^t1) ^t1”)) (REFL t1)
1344 val th9 = MP (SPEC t1 (SPEC “\ ^x.^x = ^t1” SELECT_AX)) th8
1345 in
1346 GEN t1 (GEN t2 (TRANS th7 (EQ_MP (BETA_CONV(concl th9)) th9)))
1347 end;
1348
1349(*---------------------------------------------------------------------------
1350 * |- !tm1 tm2:'a. COND F tm1 tm2 = tm2
1351 *
1352 * Note that there is a bound variable conflict if we use use t1
1353 * and t2 as the variable names. That would be a good test of the
1354 * substitution algorithm.
1355 *---------------------------------------------------------------------------*)
1356
1357val COND_CLAUSE2 =
1358 let val (x,t1,t2,v) = (“x:'a”, “tm1:'a”, “tm2:'a”,
1359 genvar Type.bool)
1360 val th1 = RIGHT_BETA(AP_THM
1361 (RIGHT_BETA(AP_THM
1362 (RIGHT_BETA(AP_THM COND_DEF “F”)) t1))t2)
1363 val FF = EQT_INTRO(REFL “F”)
1364 val th2 = SUBST [v |-> SYM FF]
1365 “(^v ==> (^x=^t2))=(^x=^t2)”
1366 (CONJUNCT1(SPEC “^x=^t2” IMP_CLAUSES))
1367 and th3 = DISCH “F=T” (MP (SPEC “^x=^t1” FALSITY)
1368 (UNDISCH (MP (SPEC “F=T” F_IMP)
1369 (CONJUNCT2 BOOL_EQ_DISTINCT))))
1370 val th4 = DISCH “^x=^t2”
1371 (CONJ th3 (EQ_MP(SYM th2)(ASSUME “^x=^t2”)))
1372 and th5 = DISCH “((F=T) ==> (^x=^t1)) /\ ((F=F) ==> (^x=^t2))”
1373 (MP (CONJUNCT2(ASSUME “((F=T) ==> (^x=^t1)) /\
1374 ((F=F) ==> (^x=^t2))”))
1375 (REFL “F”))
1376 val th6 = IMP_ANTISYM_RULE th4 th5
1377 val th7 = TRANS th1 (SYM(SELECT_EQ x th6))
1378 val th8 = EQ_MP (SYM(BETA_CONV “(\ ^x.^x = ^t2) ^t2”))
1379 (REFL t2)
1380 val th9 = MP (SPEC t2 (SPEC “\ ^x.^x = ^t2” SELECT_AX)) th8
1381 in
1382 GEN t1 (GEN t2 (TRANS th7 (EQ_MP (BETA_CONV(concl th9)) th9)))
1383 end;
1384
1385(*---------------------------------------------------------------------------
1386 * |- !t1:'a.!t2:'a. ((T => t1 | t2) = t1) /\ ((F => t1 | t2) = t2)
1387 *---------------------------------------------------------------------------*)
1388
1389val COND_CLAUSES = thm (#(FILE), #(LINE))("COND_CLAUSES",
1390 let val (t1,t2) = (“t1:'a”, “t2:'a”)
1391 in
1392 GEN t1 (GEN t2 (CONJ(SPEC t2(SPEC t1 COND_CLAUSE1))
1393 (SPEC t2(SPEC t1 COND_CLAUSE2))))
1394 end);
1395
1396(*--------------------------------------------------------------------- *)
1397(* |- b. !t. (b => t | t) = t *)
1398(* TFM 90.07.23 *)
1399(*--------------------------------------------------------------------- *)
1400
1401val COND_ID = thm (#(FILE), #(LINE))("COND_ID",
1402 let val b = “b:bool”
1403 and t = “t:'a”
1404 val def = INST_TYPE [beta |-> alpha] COND_DEF
1405 val th1 = itlist (fn x => RIGHT_BETA o (C AP_THM x))
1406 [t,t,b] def
1407 val p = genvar bool
1408 val asm1 = ASSUME “((^b=T)==>^p) /\ ((^b=F)==>^p)”
1409 val th2 = DISJ_CASES (SPEC b BOOL_CASES_AX)
1410 (UNDISCH (CONJUNCT1 asm1))
1411 (UNDISCH (CONJUNCT2 asm1))
1412 val imp1 = DISCH (concl asm1) th2
1413 val asm2 = ASSUME p
1414 val imp2 = DISCH p (CONJ (DISCH “^b=T”
1415 (ADD_ASSUM “^b=T” asm2))
1416 (DISCH “^b=F”
1417 (ADD_ASSUM “^b=F” asm2)))
1418 val lemma = SPEC “x:'a = ^t”
1419 (GEN p (IMP_ANTISYM_RULE imp1 imp2))
1420 val th3 = TRANS th1 (SELECT_EQ “x:'a” lemma)
1421 val th4 = EQ_MP (SYM(BETA_CONV “(\x.x = ^t) ^t”))
1422 (REFL t)
1423 val th5 = MP (SPEC t (SPEC “\x.x = ^t” SELECT_AX)) th4
1424 val lemma2 = EQ_MP (BETA_CONV(concl th5)) th5
1425 in
1426 GEN b (GEN t (TRANS th3 lemma2))
1427 end);
1428
1429(*---------------------------------------------------------------------------
1430 SELECT_THM = |- !P. P (@x. P x) = ?x. P x
1431 ---------------------------------------------------------------------------*)
1432
1433val SELECT_THM = thm (#(FILE), #(LINE))("SELECT_THM",
1434 GEN “P:'a->bool”
1435 (SYM (RIGHT_BETA(RIGHT_BETA
1436 (AP_THM EXISTS_DEF “\x:'a. P x:bool”)))));
1437
1438(* ---------------------------------------------------------------------*)
1439(* SELECT_REFL = |- !x. (@y. y = x) = x *)
1440(* ---------------------------------------------------------------------*)
1441
1442val SELECT_REFL = thm (#(FILE), #(LINE))("SELECT_REFL",
1443 let val th1 = SPEC “x:'a” (SPEC “\y:'a. y = x” SELECT_AX)
1444 val ths = map BETA_CONV [“(\y:'a. y = x) x”,
1445 “(\y:'a. y = x)(@y. y = x)”]
1446 val th2 = SUBST[“u:bool” |-> el 1 ths, “v:bool” |-> el 2 ths]
1447 “u ==> v” th1
1448 in
1449 GEN “x:'a” (MP th2 (REFL “x:'a”))
1450 end);
1451
1452val SELECT_REFL_2 = thm (#(FILE), #(LINE))("SELECT_REFL_2",
1453 let val x = mk_var("x", Type.alpha)
1454 val y = mk_var("y", Type.alpha)
1455 val th1 = REFL x
1456 val th2 = EXISTS (mk_exists(y,mk_eq(x,y)),x) th1
1457 val th3 = SPEC y (SPEC (mk_abs(y,mk_eq(x,y))) SELECT_AX)
1458 val th4 = UNDISCH th3
1459 val th5 = DISCH_ALL(SYM (EQ_MP (BETA_CONV (concl th4)) th4))
1460 val th6 = UNDISCH(CONV_RULE (RATOR_CONV (RAND_CONV BETA_CONV)) th5)
1461 in
1462 GEN x (CHOOSE(y,th2) th6)
1463 end);
1464
1465(*---------------------------------------------------------------------------*)
1466(* SELECT_UNIQUE = |- !P x. (!y. P y = (y = x)) ==> ($@ P = x) *)
1467(*---------------------------------------------------------------------------*)
1468
1469val SELECT_UNIQUE = thm (#(FILE), #(LINE))("SELECT_UNIQUE",
1470 let fun mksym tm = DISCH tm (SYM(ASSUME tm))
1471 val th0 = IMP_ANTISYM_RULE (mksym “y:'a = x”)
1472 (mksym “x:'a = y”)
1473 val th1 = SPEC “y:'a” (ASSUME “!y:'a. P y = (y = x)”)
1474 val th2 = EXT(GEN “y:'a” (TRANS th1 th0))
1475 val th3 = AP_TERM “$@ :('a->bool)->'a” th2
1476 val th4 = TRANS (BETA_CONV “(\y:'a. y = x) y”) th0
1477 val th5 = AP_TERM “$@ :('a->bool)->'a” (EXT(GEN “y:'a” th4))
1478 val th6 = TRANS (TRANS th3 (SYM th5)) (SPEC “x:'a” SELECT_REFL)
1479 in
1480 GENL [“P:'a->bool”, “x:'a”]
1481 (DISCH “!y:'a. P y = (y = x)” th6)
1482 end);
1483
1484(* ----------------------------------------------------------------------
1485 SELECT_ELIM_THM = |- !P Q. (?x. P x) /\ (!x. P x ==> Q x) ==> Q ($@ P)
1486 ---------------------------------------------------------------------- *)
1487
1488val SELECT_ELIM_THM = let
1489 val P = mk_var("P", alpha --> bool)
1490 val Q = mk_var("Q", alpha --> bool)
1491 val x = mk_var("x", alpha)
1492 val Px = mk_comb(P, x)
1493 val Qx = mk_comb(Q, x)
1494 val PimpQ = mk_imp(Px, Qx)
1495 val allPimpQ = mk_forall(x, PimpQ)
1496 val exPx = mk_exists (x, Px)
1497 val selP = mk_comb(prim_mk_const{Thy = "min", Name = "@"}, P)
1498 val asm_t = mk_conj(exPx, allPimpQ)
1499 val asm = ASSUME asm_t
1500 val (ex_th, forall_th) = CONJ_PAIR asm
1501 val imp_th = SPEC selP forall_th
1502 val Px_th = ASSUME Px
1503 val PselP_th0 = UNDISCH (SPEC_ALL SELECT_AX)
1504 val PselP_th = CHOOSE(x, ex_th) PselP_th0
1505in
1506 thm (#(FILE), #(LINE))(
1507 "SELECT_ELIM_THM",
1508 GENL [P, Q] (DISCH_ALL (MP imp_th PselP_th))
1509 )
1510end
1511
1512(* -------------------------------------------------------------------------*)
1513(* NOT_FORALL_THM = |- !P. ~(!x. P x) = ?x. ~P x *)
1514(* -------------------------------------------------------------------------*)
1515
1516val NOT_FORALL_THM = thm (#(FILE), #(LINE))("NOT_FORALL_THM",
1517 let val f = “P:'a->bool”
1518 val x = “x:'a”
1519 val t = mk_comb(f,x)
1520 val all = mk_forall(x,t)
1521 and exists = mk_exists(x,mk_neg t)
1522 val nott = ASSUME (mk_neg t)
1523 val th1 = DISCH all (MP nott (SPEC x (ASSUME all)))
1524 val imp1 = DISCH exists (CHOOSE (x, ASSUME exists) (NOT_INTRO th1))
1525 val th2 = CCONTR t (MP (ASSUME(mk_neg exists)) (EXISTS(exists,x)nott))
1526 val th3 = CCONTR exists (MP (ASSUME (mk_neg all)) (GEN x th2))
1527 val imp2 = DISCH (mk_neg all) th3
1528 in
1529 GEN f (IMP_ANTISYM_RULE imp2 imp1)
1530 end);
1531
1532(* ------------------------------------------------------------------------- *)
1533(* NOT_EXISTS_THM = |- !P. ~(?x. P x) = (!x. ~P x) *)
1534(* ------------------------------------------------------------------------- *)
1535
1536val NOT_EXISTS_THM = thm (#(FILE), #(LINE))("NOT_EXISTS_THM",
1537 let val f = “P:'a->bool”
1538 val x = “x:'a”
1539 val t = mk_comb(f,x)
1540 val tm = mk_neg(mk_exists(x,t))
1541 val all = mk_forall(x,mk_neg t)
1542 val asm1 = ASSUME t
1543 val thm1 = MP (ASSUME tm) (EXISTS (rand tm, x) asm1)
1544 val imp1 = DISCH tm (GEN x (NOT_INTRO (DISCH t thm1)))
1545 val asm2 = ASSUME all and asm3 = ASSUME (rand tm)
1546 val thm2 = DISCH (rand tm) (CHOOSE (x,asm3) (MP (SPEC x asm2) asm1))
1547 val imp2 = DISCH all (NOT_INTRO thm2)
1548 in
1549 GEN f (IMP_ANTISYM_RULE imp1 imp2)
1550 end);
1551
1552(* ------------------------------------------------------------------------- *)
1553(* FORALL_AND_THM |- !P Q. (!x. P x /\ Q x) = ((!x. P x) /\ (!x. Q x)) *)
1554(* ------------------------------------------------------------------------- *)
1555
1556val FORALL_AND_THM = thm (#(FILE), #(LINE))("FORALL_AND_THM",
1557 let val f = “P:'a->bool”
1558 val g = “Q:'a->bool”
1559 val x = “x:'a”
1560 val th1 = ASSUME “!x:'a. (P x) /\ (Q x)”
1561 val imp1 = (uncurry CONJ) ((GEN x ## GEN x) (CONJ_PAIR (SPEC x th1)))
1562 val th2 = ASSUME “(!x:'a. P x) /\ (!x:'a. Q x)”
1563 val imp2 = GEN x (uncurry CONJ ((SPEC x ## SPEC x) (CONJ_PAIR th2)))
1564 in
1565 GENL [f,g] (IMP_ANTISYM_RULE (DISCH_ALL imp1) (DISCH_ALL imp2))
1566 end);
1567
1568(* ------------------------------------------------------------------------- *)
1569(* LEFT_AND_FORALL_THM = |- !P Q. (!x. P x) /\ Q = (!x. P x /\ Q) *)
1570(* ------------------------------------------------------------------------- *)
1571
1572val LEFT_AND_FORALL_THM = thm (#(FILE), #(LINE))("LEFT_AND_FORALL_THM",
1573 let val x = “x:'a”
1574 val f = “P:'a->bool”
1575 val Q = “Q:bool”
1576 val th1 = ASSUME “(!x:'a. P x) /\ Q”
1577 val imp1 = GEN x ((uncurry CONJ) ((SPEC x ## I) (CONJ_PAIR th1)))
1578 val th2 = ASSUME “!x:'a. P x /\ Q”
1579 val imp2 = (uncurry CONJ) ((GEN x ## I) (CONJ_PAIR (SPEC x th2)))
1580 in
1581 GENL [f,Q] (IMP_ANTISYM_RULE (DISCH_ALL imp1) (DISCH_ALL imp2))
1582 end);
1583
1584(* ------------------------------------------------------------------------- *)
1585(* RIGHT_AND_FORALL_THM = |- !P Q. P /\ (!x. Q x) = (!x. P /\ Q x) *)
1586(* ------------------------------------------------------------------------- *)
1587
1588val RIGHT_AND_FORALL_THM = thm (#(FILE), #(LINE))("RIGHT_AND_FORALL_THM",
1589 let val x = “x:'a”
1590 val P = “P:bool”
1591 val g = “Q:'a->bool”
1592 val th1 = ASSUME “P /\ (!x:'a. Q x)”
1593 val imp1 = GEN x ((uncurry CONJ) ((I ## SPEC x) (CONJ_PAIR th1)))
1594 val th2 = ASSUME “!x:'a. P /\ Q x”
1595 val imp2 = (uncurry CONJ) ((I ## GEN x) (CONJ_PAIR (SPEC x th2)))
1596 in
1597 GENL [P,g] (IMP_ANTISYM_RULE (DISCH_ALL imp1) (DISCH_ALL imp2))
1598 end);
1599
1600(* ------------------------------------------------------------------------- *)
1601(* EXISTS_OR_THM |- !P Q. (?x. P x \/ Q x) = ((?x. P x) \/ (?x. Q x)) *)
1602(* ------------------------------------------------------------------------- *)
1603
1604val EXISTS_OR_THM = thm (#(FILE), #(LINE))("EXISTS_OR_THM",
1605 let val f = “P:'a->bool”
1606 val g = “Q:'a->bool”
1607 val x = “x:'a”
1608 val P = mk_comb(f,x)
1609 val Q = mk_comb(g,x)
1610 val tm = mk_exists (x,mk_disj(P,Q))
1611 val ep = mk_exists (x,P)
1612 and eq = mk_exists(x,Q)
1613 val Pth = EXISTS(ep,x)(ASSUME P)
1614 and Qth = EXISTS(eq,x)(ASSUME Q)
1615 val thm1 = DISJ_CASES_UNION (ASSUME(mk_disj(P,Q))) Pth Qth
1616 val imp1 = DISCH tm (CHOOSE (x,ASSUME tm) thm1)
1617 val t1 = DISJ1 (ASSUME P) Q and t2 = DISJ2 P (ASSUME Q)
1618 val th1 = EXISTS(tm,x) t1 and th2 = EXISTS(tm,x) t2
1619 val e1 = CHOOSE (x,ASSUME ep) th1 and e2 = CHOOSE (x,ASSUME eq) th2
1620 val thm2 = DISJ_CASES (ASSUME(mk_disj(ep,eq))) e1 e2
1621 val imp2 = DISCH (mk_disj(ep,eq)) thm2
1622 in
1623 GENL [f,g] (IMP_ANTISYM_RULE imp1 imp2)
1624 end);
1625
1626(* ------------------------------------------------------------------------- *)
1627(* LEFT_OR_EXISTS_THM = |- (?x. P x) \/ Q = (?x. P x \/ Q) *)
1628(* ------------------------------------------------------------------------- *)
1629
1630val LEFT_OR_EXISTS_THM = thm (#(FILE), #(LINE))("LEFT_OR_EXISTS_THM",
1631 let val x = “x:'a”
1632 val Q = “Q:bool”
1633 val f = “P:'a->bool”
1634 val P = mk_comb(f,x)
1635 val ep = mk_exists(x,P)
1636 val tm = mk_disj(ep,Q)
1637 val otm = mk_exists(x,mk_disj(P,Q))
1638 val t1 = DISJ1 (ASSUME P) Q
1639 val t2 = DISJ2 P (ASSUME Q)
1640 val th1 = EXISTS(otm,x) t1 and th2 = EXISTS(otm,x) t2
1641 val thm1 = DISJ_CASES (ASSUME tm) (CHOOSE(x,ASSUME ep)th1) th2
1642 val imp1 = DISCH tm thm1
1643 val Pth = EXISTS(ep,x)(ASSUME P) and Qth = ASSUME Q
1644 val thm2 = DISJ_CASES_UNION (ASSUME(mk_disj(P,Q))) Pth Qth
1645 val imp2 = DISCH otm (CHOOSE (x,ASSUME otm) thm2)
1646 in
1647 GENL [f,Q] (IMP_ANTISYM_RULE imp1 imp2)
1648 end);
1649
1650(* ------------------------------------------------------------------------- *)
1651(* RIGHT_OR_EXISTS_THM = |- P \/ (?x. Q x) = (?x. P \/ Q x) *)
1652(* ------------------------------------------------------------------------- *)
1653
1654val RIGHT_OR_EXISTS_THM = thm (#(FILE), #(LINE))("RIGHT_OR_EXISTS_THM",
1655 let val x = “x:'a”
1656 val P = “P:bool”
1657 val g = “Q:'a->bool”
1658 val Q = mk_comb(g,x)
1659 val eq = mk_exists(x,Q)
1660 val tm = mk_disj(P,eq)
1661 val otm = mk_exists(x,mk_disj(P,Q))
1662 val t1 = DISJ1 (ASSUME P) Q and t2 = DISJ2 P (ASSUME Q)
1663 val th1 = EXISTS(otm,x) t1 and th2 = EXISTS(otm,x) t2
1664 val thm1 = DISJ_CASES (ASSUME tm) th1 (CHOOSE(x,ASSUME eq)th2)
1665 val imp1 = DISCH tm thm1
1666 val Qth = EXISTS(eq,x)(ASSUME Q) and Pth = ASSUME P
1667 val thm2 = DISJ_CASES_UNION (ASSUME(mk_disj(P,Q))) Pth Qth
1668 val imp2 = DISCH otm (CHOOSE (x,ASSUME otm) thm2)
1669 in
1670 GENL [P,g] (IMP_ANTISYM_RULE imp1 imp2)
1671 end);
1672
1673(* ------------------------------------------------------------------------- *)
1674(* BOTH_EXISTS_AND_THM = |- !P Q. (?x. P /\ Q) = (?x. P) /\ (?x. Q) *)
1675(* ------------------------------------------------------------------------- *)
1676
1677val BOTH_EXISTS_AND_THM = thm (#(FILE), #(LINE))("BOTH_EXISTS_AND_THM",
1678 let val x = “x:'a”
1679 val P = “P:bool”
1680 val Q = “Q:bool”
1681 val t = mk_conj(P,Q)
1682 val exi = mk_exists(x,t)
1683 val (t1,t2) = CONJ_PAIR (ASSUME t)
1684 val t11 = EXISTS ((mk_exists(x,P)),x) t1
1685 val t21 = EXISTS ((mk_exists(x,Q)),x) t2
1686 val imp1 = DISCH_ALL (CHOOSE (x,
1687 ASSUME (mk_exists(x,mk_conj(P,Q))))
1688 (CONJ t11 t21))
1689 val th21 = EXISTS (exi,x) (CONJ (ASSUME P) (ASSUME Q))
1690 val th22 = CHOOSE(x,ASSUME(mk_exists(x,P))) th21
1691 val th23 = CHOOSE(x,ASSUME(mk_exists(x,Q))) th22
1692 val (u1,u2) =
1693 CONJ_PAIR (ASSUME (mk_conj(mk_exists(x,P),mk_exists(x,Q))))
1694 val th24 = PROVE_HYP u1 (PROVE_HYP u2 th23)
1695 val imp2 = DISCH_ALL th24
1696 in
1697 GENL [P,Q] (IMP_ANTISYM_RULE imp1 imp2)
1698 end);
1699
1700(* ------------------------------------------------------------------------- *)
1701(* LEFT_EXISTS_AND_THM = |- !P Q. (?x. P x /\ Q) = (?x. P x) /\ Q *)
1702(* ------------------------------------------------------------------------- *)
1703
1704val LEFT_EXISTS_AND_THM = thm (#(FILE), #(LINE))("LEFT_EXISTS_AND_THM",
1705 let val x = “x:'a”
1706 val f = “P:'a->bool”
1707 val P = mk_comb(f,x)
1708 val Q = “Q:bool”
1709 val t = mk_conj(P,Q)
1710 val exi = mk_exists(x,t)
1711 val (t1,t2) = CONJ_PAIR (ASSUME t)
1712 val t11 = EXISTS ((mk_exists(x,P)),x) t1
1713 val imp1 =
1714 DISCH_ALL
1715 (CHOOSE
1716 (x, ASSUME (mk_exists(x,mk_conj(P,Q))))
1717 (CONJ t11 t2))
1718 val th21 = EXISTS (exi,x) (CONJ (ASSUME P) (ASSUME Q))
1719 val th22 = CHOOSE(x,ASSUME(mk_exists(x,P))) th21
1720 val (u1,u2) = CONJ_PAIR(ASSUME(mk_conj(mk_exists(x,P), Q)))
1721 val th23 = PROVE_HYP u1 (PROVE_HYP u2 th22)
1722 val imp2 = DISCH_ALL th23
1723 in
1724 GENL [f,Q] (IMP_ANTISYM_RULE imp1 imp2)
1725 end);
1726
1727(* ------------------------------------------------------------------------- *)
1728(* RIGHT_EXISTS_AND_THM = |- !P Q. (?x. P /\ Q x) = P /\ (?x. Q x) *)
1729(* ------------------------------------------------------------------------- *)
1730
1731val RIGHT_EXISTS_AND_THM = thm (#(FILE), #(LINE))("RIGHT_EXISTS_AND_THM",
1732 let val x = “x:'a”
1733 val P = “P:bool”
1734 val g = “Q:'a->bool”
1735 val Q = mk_comb(g,x)
1736 val t = mk_conj(P,Q)
1737 val exi = mk_exists(x,t)
1738 val (t1,t2) = CONJ_PAIR (ASSUME t)
1739 val t21 = EXISTS ((mk_exists(x,Q)),x) t2
1740 val imp1 =
1741 DISCH_ALL
1742 (CHOOSE
1743 (x, ASSUME (mk_exists(x,mk_conj(P,Q)))) (CONJ t1 t21))
1744 val th21 = EXISTS (exi,x) (CONJ (ASSUME P) (ASSUME Q))
1745 val th22 = CHOOSE(x,ASSUME(mk_exists(x,Q))) th21
1746 val (u1,u2) = CONJ_PAIR (ASSUME (mk_conj(P, mk_exists(x,Q))))
1747 val th23 = PROVE_HYP u1 (PROVE_HYP u2 th22)
1748 val imp2 = DISCH_ALL th23
1749 in
1750 GENL [P,g] (IMP_ANTISYM_RULE imp1 imp2)
1751 end);
1752
1753(* ------------------------------------------------------------------------- *)
1754(* BOTH_FORALL_OR_THM = |- !P Q. (!x. P \/ Q) = (!x. P) \/ (!x. Q) *)
1755(* ------------------------------------------------------------------------- *)
1756
1757val BOTH_FORALL_OR_THM = thm (#(FILE), #(LINE))("BOTH_FORALL_OR_THM",
1758 let val x = “x:'a”
1759 val P = “P:bool”
1760 val Q = “Q:bool”
1761 val imp11 = DISCH_ALL (SPEC x (ASSUME (mk_forall(x,P))))
1762 val imp12 = DISCH_ALL (GEN x (ASSUME P))
1763 val fath = IMP_ANTISYM_RULE imp11 imp12
1764 val th1 = REFL (mk_forall(x,mk_disj(P,Q)))
1765 val th2 = CONV_RULE (RAND_CONV
1766 (K (INST [P |-> mk_disj(P,Q)] fath))) th1
1767 val th3 = CONV_RULE(RAND_CONV(RATOR_CONV(RAND_CONV(K(SYM fath))))) th2
1768 val th4 = CONV_RULE(RAND_CONV(RAND_CONV(K(SYM(INST[P|->Q] fath))))) th3
1769 in
1770 GENL [P,Q] th4
1771 end);
1772
1773(* ------------------------------------------------------------------------- *)
1774(* LEFT_FORALL_OR_THM = |- !P Q. (!x. P x \/ Q) = (!x. P x) \/ Q *)
1775(* ------------------------------------------------------------------------- *)
1776
1777val LEFT_FORALL_OR_THM = thm (#(FILE), #(LINE))("LEFT_FORALL_OR_THM",
1778 let val x = “x:'a”
1779 val f = “P:'a->bool”
1780 val P = mk_comb(f,x)
1781 val Q = “Q:bool”
1782 val tm = mk_forall(x,mk_disj(P,Q))
1783 val thm1 = SPEC x (ASSUME tm)
1784 val thm2 = CONTR P (MP (ASSUME (mk_neg Q)) (ASSUME Q))
1785 val thm3 = DISJ1 (GEN x (DISJ_CASES thm1 (ASSUME P) thm2)) Q
1786 val thm4 = DISJ2 (mk_forall(x,P)) (ASSUME Q)
1787 val imp1 = DISCH tm (DISJ_CASES (SPEC Q EXCLUDED_MIDDLE) thm4 thm3)
1788 val thm5 = SPEC x (ASSUME (mk_forall(x,P)))
1789 val thm6 = ASSUME Q
1790 val imp2 = DISCH_ALL (GEN x (DISJ_CASES_UNION
1791 (ASSUME(mk_disj(mk_forall(x,P), Q))) thm5 thm6))
1792 in
1793 GENL [f,Q] (IMP_ANTISYM_RULE imp1 imp2)
1794 end);
1795
1796(* ------------------------------------------------------------------------- *)
1797(* RIGHT_FORALL_OR_THM = |- !P Q. (!x. P \/ Q x) = P \/ (!x. Q x) *)
1798(* ------------------------------------------------------------------------- *)
1799
1800val RIGHT_FORALL_OR_THM = thm (#(FILE), #(LINE))("RIGHT_FORALL_OR_THM",
1801 let val x = “x:'a”
1802 val P = “P:bool”
1803 val g = “Q:'a->bool”
1804 val Q = mk_comb(g,x)
1805 val tm = mk_forall(x,mk_disj(P,Q))
1806 val thm1 = SPEC x (ASSUME tm)
1807 val thm2 = CONTR Q (MP (ASSUME (mk_neg P)) (ASSUME P))
1808 val thm3 = DISJ2 P (GEN x (DISJ_CASES thm1 thm2 (ASSUME Q)))
1809 val thm4 = DISJ1 (ASSUME P) (mk_forall(x,Q))
1810 val imp1 = DISCH tm (DISJ_CASES (SPEC P EXCLUDED_MIDDLE) thm4 thm3)
1811 val thm5 = ASSUME P
1812 val thm6 = SPEC x (ASSUME (mk_forall(x,Q)))
1813 val imp2 = DISCH_ALL (GEN x (DISJ_CASES_UNION
1814 (ASSUME (mk_disj(P, mk_forall(x,Q))))
1815 thm5 thm6))
1816 in
1817 GENL [P,g] (IMP_ANTISYM_RULE imp1 imp2)
1818 end);
1819
1820(* ------------------------------------------------------------------------- *)
1821(* BOTH_FORALL_IMP_THM = |- (!x. P ==> Q) = ((?x.P) ==> (!x.Q)) *)
1822(* ------------------------------------------------------------------------- *)
1823
1824val BOTH_FORALL_IMP_THM = thm (#(FILE), #(LINE))("BOTH_FORALL_IMP_THM",
1825 let val x = “x:'a”
1826 val P = “P:bool”
1827 val Q = “Q:bool”
1828 val tm = mk_forall(x, mk_imp(P,Q))
1829 val asm = mk_exists(x,P)
1830 val th1 = GEN x (CHOOSE(x,ASSUME asm)(UNDISCH(SPEC x (ASSUME tm))))
1831 val imp1 = DISCH tm (DISCH asm th1)
1832 val cncl = rand(concl imp1)
1833 val th2 = SPEC x (MP (ASSUME cncl) (EXISTS (asm,x) (ASSUME P)))
1834 val imp2 = DISCH cncl (GEN x (DISCH P th2))
1835 in
1836 GENL [P,Q] (IMP_ANTISYM_RULE imp1 imp2)
1837 end);
1838
1839(* ------------------------------------------------------------------------- *)
1840(* LEFT_FORALL_IMP_THM = |- (!x. P[x]==>Q) = ((?x.P[x]) ==> Q) *)
1841(* ------------------------------------------------------------------------- *)
1842
1843val LEFT_FORALL_IMP_THM = thm (#(FILE), #(LINE))("LEFT_FORALL_IMP_THM",
1844 let val x = “x:'a”
1845 val f = “P:'a->bool”
1846 val P = mk_comb(f,x)
1847 val Q = “Q:bool”
1848 val tm = mk_forall(x, mk_imp(P,Q))
1849 val asm = mk_exists(x,P)
1850 val th1 = CHOOSE(x,ASSUME asm)(UNDISCH(SPEC x (ASSUME tm)))
1851 val imp1 = DISCH tm (DISCH asm th1)
1852 val cncl = rand(concl imp1)
1853 val th2 = MP (ASSUME cncl) (EXISTS (asm,x) (ASSUME P))
1854 val imp2 = DISCH cncl (GEN x (DISCH P th2))
1855 in
1856 GENL [f,Q] (IMP_ANTISYM_RULE imp1 imp2)
1857 end);
1858
1859(* ------------------------------------------------------------------------- *)
1860(* RIGHT_FORALL_IMP_THM = |- (!x. P==>Q[x]) = (P ==> (!x.Q[x])) *)
1861(* ------------------------------------------------------------------------- *)
1862
1863val RIGHT_FORALL_IMP_THM = thm (#(FILE), #(LINE))("RIGHT_FORALL_IMP_THM",
1864 let val x = “x:'a”
1865 val P = “P:bool”
1866 val g = “Q:'a->bool”
1867 val Q = mk_comb(g,x)
1868 val tm = mk_forall(x, mk_imp(P,Q))
1869 val imp1 = DISCH P(GEN x(UNDISCH(SPEC x(ASSUME tm))))
1870 val cncl = concl imp1
1871 val imp2 = GEN x (DISCH P(SPEC x(UNDISCH (ASSUME cncl))))
1872 in
1873 GENL [P,g] (IMP_ANTISYM_RULE (DISCH tm imp1) (DISCH cncl imp2))
1874 end);
1875
1876(* ------------------------------------------------------------------------- *)
1877(* BOTH_EXISTS_IMP_THM = |- (?x. P ==> Q) = ((!x.P) ==> (?x.Q)) *)
1878(* ------------------------------------------------------------------------- *)
1879
1880val BOTH_EXISTS_IMP_THM = thm (#(FILE), #(LINE))("BOTH_EXISTS_IMP_THM",
1881 let val x = “x:'a”
1882 val P = “P:bool”
1883 val Q = “Q:bool”
1884 val tm = mk_exists(x,mk_imp(P,Q))
1885 val eQ = mk_exists(x,Q)
1886 val aP = mk_forall(x,P)
1887 val thm1 = EXISTS(eQ,x)(UNDISCH(ASSUME(mk_imp(P,Q))))
1888 val thm2 = DISCH aP (PROVE_HYP (SPEC x (ASSUME aP)) thm1)
1889 val imp1 = DISCH tm (CHOOSE(x,ASSUME tm) thm2)
1890 val thm2 = CHOOSE(x,UNDISCH (ASSUME (rand(concl imp1)))) (ASSUME Q)
1891 val thm3 = DISCH P (PROVE_HYP (GEN x (ASSUME P)) thm2)
1892 val imp2 = DISCH (rand(concl imp1)) (EXISTS(tm,x) thm3)
1893 in
1894 GENL [P,Q] (IMP_ANTISYM_RULE imp1 imp2)
1895 end);
1896
1897(* ------------------------------------------------------------------------- *)
1898(* LEFT_EXISTS_IMP_THM = |- (?x. P[x] ==> Q) = ((!x.P[x]) ==> Q) *)
1899(* ------------------------------------------------------------------------- *)
1900
1901val LEFT_EXISTS_IMP_THM = thm (#(FILE), #(LINE))("LEFT_EXISTS_IMP_THM",
1902 let val x = “x:'a”
1903 val f = “P:'a->bool”
1904 val P = mk_comb(f,x)
1905 val Q = “Q:bool”
1906 val tm = mk_exists(x, mk_imp(P,Q))
1907 val allp = mk_forall(x,P)
1908 val th1 = SPEC x (ASSUME allp)
1909 val thm1 = MP (ASSUME(mk_imp(P,Q))) th1
1910 val imp1 = DISCH tm (CHOOSE(x,ASSUME tm)(DISCH allp thm1))
1911 val otm = rand(concl imp1)
1912 val thm2 = EXISTS(tm,x)(DISCH P (UNDISCH(ASSUME otm)))
1913 val nex = mk_exists(x,mk_neg P)
1914 val asm1 = EXISTS (nex, x) (ASSUME (mk_neg P))
1915 val th2 = CCONTR P (MP (ASSUME (mk_neg nex)) asm1)
1916 val th3 = CCONTR nex (MP (ASSUME (mk_neg allp)) (GEN x th2))
1917 val thm4 = DISCH P (CONTR Q (UNDISCH (ASSUME (mk_neg P))))
1918 val thm5 = CHOOSE(x,th3)(EXISTS(tm,x)thm4)
1919 val thm6 = DISJ_CASES (SPEC allp EXCLUDED_MIDDLE) thm2 thm5
1920 val imp2 = DISCH otm thm6
1921 in
1922 GENL [f, Q] (IMP_ANTISYM_RULE imp1 imp2)
1923 end);
1924
1925(* ------------------------------------------------------------------------- *)
1926(* RIGHT_EXISTS_IMP_THM = |- (?x. P ==> Q[x]) = (P ==> (?x.Q[x])) *)
1927(* ------------------------------------------------------------------------- *)
1928
1929val RIGHT_EXISTS_IMP_THM = thm (#(FILE), #(LINE))("RIGHT_EXISTS_IMP_THM",
1930 let val x = “x:'a”
1931 val P = “P:bool”
1932 val g = “Q:'a->bool”
1933 val Q = mk_comb(g,x)
1934 val tm = mk_exists(x,mk_imp(P,Q))
1935 val thm1 = EXISTS (mk_exists(x,Q),x)
1936 (UNDISCH(ASSUME(mk_imp(P,Q))))
1937 val imp1 = DISCH tm (CHOOSE(x,ASSUME tm) (DISCH P thm1))
1938 val thm2 = UNDISCH (ASSUME (rand(concl imp1)))
1939 val thm3 = CHOOSE (x,thm2) (EXISTS (tm,x) (DISCH P (ASSUME Q)))
1940 val thm4 = EXISTS(tm,x)(DISCH P(CONTR Q(UNDISCH(ASSUME(mk_neg P)))))
1941 val thm5 = DISJ_CASES (SPEC P EXCLUDED_MIDDLE) thm3 thm4
1942 val imp2 = DISCH(rand(concl imp1)) thm5
1943 in
1944 GENL [P,g] (IMP_ANTISYM_RULE imp1 imp2)
1945 end);
1946
1947(* --------------------------------------------------------------------- *)
1948(* OR_IMP_THM = |- !A B. (A = B \/ A) = (B ==> A) *)
1949(* [TFM 90.06.28] *)
1950(* --------------------------------------------------------------------- *)
1951
1952val OR_IMP_THM = thm (#(FILE), #(LINE))("OR_IMP_THM",
1953 let val t1 = “A:bool” and t2 = “B:bool”
1954 val asm1 = ASSUME “^t1 = (^t2 \/ ^t1)”
1955 and asm2 = EQT_INTRO(ASSUME t2)
1956 val th1 = SUBST [t2 |-> asm2] (concl asm1) asm1
1957 val th2 = TRANS th1 (CONJUNCT1 (SPEC t1 OR_CLAUSES))
1958 val imp1 = DISCH (concl asm1) (DISCH t2 (EQT_ELIM th2))
1959 val asm3 = ASSUME “^t2 ==> ^t1”
1960 and asm4 = ASSUME “^t2 \/ ^t1”
1961 val th3 = DISJ_CASES asm4 (MP asm3 (ASSUME t2)) (ASSUME t1)
1962 val th4 = DISCH (concl asm4) th3
1963 and th5 = DISCH t1 (DISJ2 t2 (ASSUME t1))
1964 val imp2 = DISCH “^t2 ==> ^t1” (IMP_ANTISYM_RULE th5 th4)
1965 in
1966 GEN t1 (GEN t2 (IMP_ANTISYM_RULE imp1 imp2))
1967 end);
1968
1969(* --------------------------------------------------------------------- *)
1970(* NOT_IMP = |- !A B. ~(A ==> B) = A /\ ~B *)
1971(* [TFM 90.07.09] *)
1972(* --------------------------------------------------------------------- *)
1973
1974val NOT_IMP = thm (#(FILE), #(LINE))("NOT_IMP",
1975let val t1 = “A:bool” and t2 = “B:bool”
1976 val asm1 = ASSUME “~(^t1 ==> ^t2)”
1977 val thm1 = SUBST [t1 |-> EQF_INTRO (ASSUME (mk_neg t1))] (concl asm1) asm1
1978 val thm2 = CCONTR t1 (MP thm1 (DISCH“F”(CONTR t2 (ASSUME“F”))))
1979 val thm3 = SUBST [t2 |-> EQT_INTRO (ASSUME t2)] (concl asm1) asm1
1980 val thm4 = NOT_INTRO(DISCH t2 (MP thm3 (DISCH t1 (ADD_ASSUM t1 TRUTH))))
1981 val imp1 = DISCH (concl asm1) (CONJ thm2 thm4)
1982 val conj = ASSUME “^t1 /\ ~^t2”
1983 val (asm2,asm3) = (CONJUNCT1 conj, CONJUNCT2 conj)
1984 val asm4 = ASSUME “^t1 ==> ^t2”
1985 val thm5 = MP (SUBST [t2 |-> EQF_INTRO asm3] (concl asm4) asm4) asm2
1986 val imp2 = DISCH “^t1 /\ ~ ^t2”
1987 (NOT_INTRO(DISCH “^t1 ==> ^t2” thm5))
1988 in
1989 GEN t1 (GEN t2 (IMP_ANTISYM_RULE imp1 imp2))
1990 end);
1991
1992(* --------------------------------------------------------------------- *)
1993(* DISJ_ASSOC: |- !A B C. A \/ B \/ C = (A \/ B) \/ C *)
1994(* --------------------------------------------------------------------- *)
1995
1996val DISJ_ASSOC = thm (#(FILE), #(LINE))("DISJ_ASSOC",
1997let val t1 = “A:bool” and t2 = “B:bool” and t3 = “C:bool”
1998 val at1 = DISJ1 (DISJ1 (ASSUME t1) t2) t3 and
1999 at2 = DISJ1 (DISJ2 t1 (ASSUME t2)) t3 and
2000 at3 = DISJ2 (mk_disj(t1,t2)) (ASSUME t3)
2001 val thm = DISJ_CASES (ASSUME (mk_disj(t2,t3))) at2 at3
2002 val thm1 = DISJ_CASES (ASSUME (mk_disj(t1,mk_disj(t2,t3)))) at1 thm
2003 val at1 = DISJ1 (ASSUME t1) (mk_disj(t2,t3)) and
2004 at2 = DISJ2 t1 (DISJ1 (ASSUME t2) t3) and
2005 at3 = DISJ2 t1 (DISJ2 t2 (ASSUME t3))
2006 val thm = DISJ_CASES (ASSUME (mk_disj(t1,t2))) at1 at2
2007 val thm2 = DISJ_CASES (ASSUME (mk_disj(mk_disj(t1,t2),t3))) thm at3
2008 val imp1 = DISCH (mk_disj(t1,mk_disj(t2,t3))) thm1 and
2009 imp2 = DISCH (mk_disj(mk_disj(t1,t2),t3)) thm2
2010 in
2011 GENL [t1,t2,t3] (IMP_ANTISYM_RULE imp1 imp2)
2012 end);
2013
2014(* --------------------------------------------------------------------- *)
2015(* DISJ_SYM: |- !A B. A \/ B = B \/ A *)
2016(* --------------------------------------------------------------------- *)
2017
2018val DISJ_SYM = thm (#(FILE), #(LINE))("DISJ_SYM",
2019let val t1 = “A:bool” and t2 = “B:bool”
2020 val th1 = DISJ1 (ASSUME t1) t2 and th2 = DISJ2 t1 (ASSUME t2)
2021 val thm1 = DISJ_CASES (ASSUME(mk_disj(t2,t1))) th2 th1
2022 val th1 = DISJ1 (ASSUME t2) t1 and th2 = DISJ2 t2 (ASSUME t1)
2023 val thm2 = DISJ_CASES (ASSUME(mk_disj(t1,t2))) th2 th1
2024 val imp1 = DISCH (mk_disj(t2,t1)) thm1 and
2025 imp2 = DISCH (mk_disj(t1,t2)) thm2
2026 in
2027 GENL [t1,t2] (IMP_ANTISYM_RULE imp2 imp1)
2028 end);
2029
2030val _ = thm (#(FILE), #(LINE))("DISJ_COMM", DISJ_SYM);
2031
2032(* --------------------------------------------------------------------- *)
2033(* DE_MORGAN_THM: *)
2034(* |- !A B. (~(t1 /\ t2) = ~t1 \/ ~t2) /\ (~(t1 \/ t2) = ~t1 /\ ~t2) *)
2035(* --------------------------------------------------------------------- *)
2036
2037val DE_MORGAN_THM = thm (#(FILE), #(LINE))("DE_MORGAN_THM",
2038let val t1 = “A:bool” and t2 = “B:bool”
2039 val thm1 =
2040 let val asm1 = ASSUME “~(^t1 /\ ^t2)”
2041 val cnj = MP asm1 (CONJ (ASSUME t1) (ASSUME t2))
2042 val imp1 =
2043 let val case1 = DISJ2 “~^t1” (NOT_INTRO(DISCH t2 cnj))
2044 val case2 = DISJ1 (ASSUME “~ ^t1”) “~ ^t2”
2045 in DISJ_CASES (SPEC t1 EXCLUDED_MIDDLE) case1 case2
2046 end
2047 val th1 = MP (ASSUME “~^t1”)
2048 (CONJUNCT1 (ASSUME “^t1 /\ ^t2”))
2049 val th2 = MP (ASSUME “~^t2”)
2050 (CONJUNCT2 (ASSUME “^t1 /\ ^t2”))
2051 val imp2 =
2052 let val fth = DISJ_CASES (ASSUME “~^t1 \/ ~^t2”) th1 th2
2053 in DISCH “~^t1 \/ ~^t2”
2054 (NOT_INTRO(DISCH “^t1 /\ ^t2” fth))
2055 end
2056 in
2057 IMP_ANTISYM_RULE (DISCH “~(^t1 /\ ^t2)” imp1) imp2
2058 end
2059 val thm2 =
2060 let val asm1 = ASSUME “~(^t1 \/ ^t2)”
2061 val imp1 =
2062 let val th1 = NOT_INTRO (DISCH t1(MP asm1 (DISJ1 (ASSUME t1) t2)))
2063 val th2 = NOT_INTRO (DISCH t2 (MP asm1 (DISJ2 t1 (ASSUME t2))))
2064 in DISCH “~(^t1 \/ ^t2)” (CONJ th1 th2)
2065 end
2066 val imp2 =
2067 let val asm = ASSUME “^t1 \/ ^t2”
2068 val a1 = CONJUNCT1(ASSUME “~^t1 /\ ~^t2”) and
2069 a2 = CONJUNCT2(ASSUME “~^t1 /\ ~^t2”)
2070 val fth = DISJ_CASES asm (UNDISCH a1) (UNDISCH a2)
2071 in DISCH “~^t1 /\ ~^t2”
2072 (NOT_INTRO(DISCH “^t1 \/ ^t2” fth))
2073 end
2074 in IMP_ANTISYM_RULE imp1 imp2
2075 end
2076 in GEN t1 (GEN t2 (CONJ thm1 thm2))
2077 end);
2078
2079(* -------------------------------------------------------------------------*)
2080(* Distributive laws: *)
2081(* *)
2082(* LEFT_AND_OVER_OR |- !A B C. A /\ (B \/ C) = A /\ B \/ A /\ C *)
2083(* *)
2084(* RIGHT_AND_OVER_OR |- !A B C. (B \/ C) /\ A = B /\ A \/ C /\ A *)
2085(* *)
2086(* LEFT_OR_OVER_AND |- !A B C. A \/ B /\ C = (A \/ B) /\ (A \/ C) *)
2087(* *)
2088(* RIGHT_OR_OVER_AND |- !A B C. B /\ C \/ A = (B \/ A) /\ (C \/ A) *)
2089(* -------------------------------------------------------------------------*)
2090
2091val LEFT_AND_OVER_OR = thm (#(FILE), #(LINE))("LEFT_AND_OVER_OR",
2092 let val t1 = “A:bool”
2093 and t2 = “B:bool”
2094 and t3 = “C:bool”
2095 val (th1,th2) = CONJ_PAIR(ASSUME (mk_conj(t1,mk_disj(t2,t3))))
2096 val th3 = CONJ th1 (ASSUME t2) and th4 = CONJ th1 (ASSUME t3)
2097 val th5 = DISJ_CASES_UNION th2 th3 th4
2098 val imp1 = DISCH (mk_conj(t1,mk_disj(t2,t3))) th5
2099 val (th1,th2) = (I ## C DISJ1 t3) (CONJ_PAIR (ASSUME (mk_conj(t1,t2))))
2100 val (th3,th4) = (I ## DISJ2 t2) (CONJ_PAIR (ASSUME (mk_conj(t1,t3))))
2101 val th5 = CONJ th1 th2 and th6 = CONJ th3 th4
2102 val th6 = DISJ_CASES (ASSUME (rand(concl imp1))) th5 th6
2103 val imp2 = DISCH (rand(concl imp1)) th6
2104 in
2105 GEN t1 (GEN t2 (GEN t3 (IMP_ANTISYM_RULE imp1 imp2)))
2106 end);
2107
2108val RIGHT_AND_OVER_OR = thm (#(FILE), #(LINE))("RIGHT_AND_OVER_OR",
2109 let val t1 = “A:bool”
2110 and t2 = “B:bool”
2111 and t3 = “C:bool”
2112 val (th1,th2) = CONJ_PAIR(ASSUME (mk_conj(mk_disj(t2,t3),t1)))
2113 val th3 = CONJ (ASSUME t2) th2 and th4 = CONJ (ASSUME t3) th2
2114 val th5 = DISJ_CASES_UNION th1 th3 th4
2115 val imp1 = DISCH (mk_conj(mk_disj(t2,t3),t1)) th5
2116 val (th1,th2) = (C DISJ1 t3 ## I) (CONJ_PAIR (ASSUME (mk_conj(t2,t1))))
2117 val (th3,th4) = (DISJ2 t2 ## I) (CONJ_PAIR (ASSUME (mk_conj(t3,t1))))
2118 val th5 = CONJ th1 th2 and th6 = CONJ th3 th4
2119 val th6 = DISJ_CASES (ASSUME (rand(concl imp1))) th5 th6
2120 val imp2 = DISCH (rand(concl imp1)) th6
2121 in
2122 GEN t1 (GEN t2 (GEN t3 (IMP_ANTISYM_RULE imp1 imp2)))
2123 end);
2124
2125val LEFT_OR_OVER_AND = thm (#(FILE), #(LINE))("LEFT_OR_OVER_AND",
2126 let val t1 = “A:bool”
2127 and t2 = “B:bool”
2128 and t3 = “C:bool”
2129 val th1 = ASSUME (mk_disj(t1,mk_conj(t2,t3)))
2130 val th2 = CONJ (DISJ1 (ASSUME t1) t2) (DISJ1 (ASSUME t1) t3)
2131 val (th3,th4) = CONJ_PAIR (ASSUME(mk_conj(t2,t3)))
2132 val th5 = CONJ (DISJ2 t1 th3) (DISJ2 t1 th4)
2133 val imp1 = DISCH (concl th1) (DISJ_CASES th1 th2 th5)
2134 val (th1,th2) = CONJ_PAIR (ASSUME (rand(concl imp1)))
2135 val th3 = DISJ1 (ASSUME t1) (mk_conj(t2,t3))
2136 val (th4,th5) = CONJ_PAIR (ASSUME (mk_conj(t2,t3)))
2137 val th4 = DISJ2 t1 (CONJ (ASSUME t2) (ASSUME t3))
2138 val th5 = DISJ_CASES th2 th3 (DISJ_CASES th1 th3 th4)
2139 val imp2 = DISCH (rand(concl imp1)) th5
2140 in
2141 GEN t1 (GEN t2 (GEN t3 (IMP_ANTISYM_RULE imp1 imp2)))
2142 end);
2143
2144val RIGHT_OR_OVER_AND = thm (#(FILE), #(LINE))("RIGHT_OR_OVER_AND",
2145 let val t1 = “A:bool”
2146 and t2 = “B:bool”
2147 and t3 = “C:bool”
2148 val th1 = ASSUME (mk_disj(mk_conj(t2,t3),t1))
2149 val th2 = CONJ (DISJ2 t2 (ASSUME t1)) (DISJ2 t3 (ASSUME t1))
2150 val (th3,th4) = CONJ_PAIR (ASSUME(mk_conj(t2,t3)))
2151 val th5 = CONJ (DISJ1 th3 t1) (DISJ1 th4 t1)
2152 val imp1 = DISCH (concl th1) (DISJ_CASES th1 th5 th2)
2153 val (th1,th2) = CONJ_PAIR (ASSUME (rand(concl imp1)))
2154 val th3 = DISJ2 (mk_conj(t2,t3)) (ASSUME t1)
2155 val (th4,th5) = CONJ_PAIR (ASSUME (mk_conj(t2,t3)))
2156 val th4 = DISJ1 (CONJ (ASSUME t2) (ASSUME t3)) t1
2157 val th5 = DISJ_CASES th2 (DISJ_CASES th1 th4 th3) th3
2158 val imp2 = DISCH (rand(concl imp1)) th5
2159 in
2160 GEN t1 (GEN t2 (GEN t3 (IMP_ANTISYM_RULE imp1 imp2)))
2161 end);
2162
2163(*---------------------------------------------------------------------------*
2164 * IMP_DISJ_THM = |- !A B. A ==> B = ~A \/ B *
2165 *---------------------------------------------------------------------------*)
2166
2167val IMP_DISJ_THM = thm (#(FILE), #(LINE))("IMP_DISJ_THM",
2168let val A = “A:bool”
2169 val B = “B:bool”
2170 val th1 = ASSUME “A ==> B”
2171 val th2 = ASSUME A
2172 val th3 = MP th1 th2
2173 val th4 = DISJ2 “~A” th3
2174 val th5 = ASSUME “~A”;
2175 val th6 = ADD_ASSUM “A ==> B” th5
2176 val th7 = DISJ1 th6 B
2177 val th8 = SPEC A EXCLUDED_MIDDLE
2178 val th9 = DISJ_CASES th8 th4 th7
2179 val th10 = EQT_INTRO th2
2180 val th11 = ASSUME “~A \/ B”
2181 val th12 = SUBST [A |-> th10] (concl th11) th11
2182 val th13 = CONJUNCT1 (CONJUNCT2 NOT_CLAUSES)
2183 val th14 = SUBST [A |-> th13] (subst [“~T” |-> A] (concl th12)) th12
2184 val th15 = CONJUNCT1 (CONJUNCT2(CONJUNCT2 (SPEC B OR_CLAUSES)))
2185 val th16 = SUBST [A |-> th15] A th14
2186 val th17 = DISCH A th16
2187 val th18 = DISCH (concl th11) th17
2188 in
2189 GENL [A,B] (IMP_ANTISYM_RULE (DISCH (hd(hyp th9)) th9) th18)
2190 end);
2191
2192(*----------------------------------------------------------------------*)
2193(* DISJ_IMP_THM = |- !P Q R. P \/ Q ==> R = (P ==> R) /\ (Q ==> R) *)
2194(* MN 99.05.06 *)
2195(*----------------------------------------------------------------------*)
2196
2197val DISJ_IMP_THM = let
2198 val P = “P:bool”
2199 val Q = “Q:bool”
2200 val R = “R:bool”
2201 val lhs = “P \/ Q ==> R”
2202 val rhs = “(P ==> R) /\ (Q ==> R)”
2203 val ass_lhs = ASSUME lhs
2204 val ass_P = ASSUME P
2205 val ass_Q = ASSUME Q
2206 val p_imp_r = DISCH P (MP ass_lhs (DISJ1 ass_P Q))
2207 val q_imp_r = DISCH Q (MP ass_lhs (DISJ2 P ass_Q))
2208 val lr_imp = DISCH lhs (CONJ p_imp_r q_imp_r)
2209 (* half way there! *)
2210 val ass_rhs = ASSUME rhs
2211 val porq = “P \/ Q”
2212 val ass_porq = ASSUME porq
2213 val my_and1 = SPECL [“P ==> R”, “Q ==> R”] AND1_THM
2214 val p_imp_r = MP my_and1 ass_rhs
2215 val r_from_p = MP p_imp_r ass_P
2216 val my_and2 = SPECL [“P ==> R”, “Q ==> R”] AND2_THM
2217 val q_imp_r = MP my_and2 ass_rhs
2218 val r_from_q = MP q_imp_r ass_Q
2219 val rl_imp = DISCH rhs (DISCH porq (DISJ_CASES ass_porq r_from_p r_from_q))
2220in
2221 thm (#(FILE), #(LINE))("DISJ_IMP_THM",
2222 GENL [P,Q,R] (IMP_ANTISYM_RULE lr_imp rl_imp))
2223end
2224
2225(* ----------------------------------------------------------------------
2226 IMP_CONJ_THM = |- !P Q R. P ==> Q /\ R = (P ==> Q) /\ (P ==> R)
2227 MN 2002.10.06
2228 ---------------------------------------------------------------------- *)
2229
2230val IMP_CONJ_THM = let
2231 val P = mk_var("P", bool)
2232 val Q = mk_var("Q", bool)
2233 val R = mk_var("R", bool)
2234 val QandR = mk_conj(Q,R)
2235 val PimpQandR = mk_imp(P, QandR)
2236 val PiQaR_th = ASSUME PimpQandR
2237 val P_th = ASSUME P
2238 val QaR_th = MP PiQaR_th P_th
2239 val (Q_th, R_th) = CONJ_PAIR QaR_th
2240 val PQ_th = DISCH P Q_th
2241 val PR_th = DISCH P R_th
2242 val L2R = DISCH PimpQandR (CONJ PQ_th PR_th)
2243 val PiQ = mk_imp(P, Q)
2244 val PiR = mk_imp(P, R)
2245 val PiQaPiR = mk_conj(PiQ, PiR)
2246 val PiQaPiR_th = ASSUME PiQaPiR
2247 val (PiQ_th, PiR_th) = CONJ_PAIR PiQaPiR_th
2248 val Q_th = MP PiQ_th P_th
2249 val R_th = MP PiR_th P_th
2250 val QaR_th = CONJ Q_th R_th
2251 val R2L = DISCH PiQaPiR (DISCH P QaR_th)
2252in
2253 thm (#(FILE), #(LINE))("IMP_CONJ_THM",
2254 GENL [P,Q,R] (IMP_ANTISYM_RULE L2R R2L))
2255end
2256
2257(* ---------------------------------------------------------------------*)
2258(* IMP_F_EQ_F *)
2259(* *)
2260(* |- !t. t ==> F = (t = F) *)
2261(* RJB 92.09.26 *)
2262(* ---------------------------------------------------------------------*)
2263
2264local fun nthCONJUNCT n cth =
2265 let val th = funpow (n-1) CONJUNCT2 cth
2266 in if (can dest_conj (concl th))
2267 then CONJUNCT1 th else th
2268 end
2269in
2270val IMP_F_EQ_F = thm (#(FILE), #(LINE))("IMP_F_EQ_F",
2271 GEN “t:bool”
2272 (TRANS (nthCONJUNCT 5 (SPEC_ALL IMP_CLAUSES))
2273 (SYM (nthCONJUNCT 4 (SPEC_ALL EQ_CLAUSES)))))
2274end;
2275
2276(* ---------------------------------------------------------------------*)
2277(* AND_IMP_INTRO *)
2278(* *)
2279(* |- !t1 t2 t3. t1 ==> t2 ==> t3 = t1 /\ t2 ==> t3 *)
2280(* RJB 92.09.26 *)
2281(* ---------------------------------------------------------------------*)
2282
2283val AND_IMP_INTRO = thm (#(FILE), #(LINE))("AND_IMP_INTRO",
2284let val t1 = “t1:bool”
2285 and t2 = “t2:bool”
2286 and t3 = “t3:bool”
2287 and imp = “$==>”
2288 val [IMP1,IMP2,IMP3,_,IMP4] = map GEN_ALL(CONJUNCTS (SPEC_ALL IMP_CLAUSES))
2289 and [AND1,AND2,AND3,AND4,_] = map GEN_ALL(CONJUNCTS (SPEC_ALL AND_CLAUSES))
2290 val thTl = SPEC “t2 ==> t3” IMP1
2291 and thFl = SPEC “t2 ==> t3” IMP3
2292 val thTr = AP_THM (AP_TERM imp (SPEC t2 AND1)) t3
2293 and thFr = TRANS (AP_THM (AP_TERM imp (SPEC t2 AND3)) t3)(SPEC t3 IMP3)
2294 val thT1 = TRANS thTl (SYM thTr)
2295 and thF1 = TRANS thFl (SYM thFr)
2296 val tm = “t1 ==> t2 ==> t3 <=> t1 /\ t2 ==> t3”
2297 val thT2 = SUBST_CONV [t1 |-> ASSUME “t1 = T”] tm tm
2298 and thF2 = SUBST_CONV [t1 |-> ASSUME “t1 = F”] tm tm
2299 val thT3 = EQ_MP (SYM thT2) thT1
2300 and thF3 = EQ_MP (SYM thF2) thF1
2301 in
2302 GENL [t1,t2,t3] (DISJ_CASES (SPEC t1 BOOL_CASES_AX) thT3 thF3)
2303 end);
2304
2305(* ---------------------------------------------------------------------*)
2306(* EQ_IMP_THM *)
2307(* *)
2308(* |- !t1 t2. (t1 = t2) = (t1 ==> t2) /\ (t2 ==> t1) *)
2309(* *)
2310(* RJB 92.09.26 *)
2311(* ---------------------------------------------------------------------*)
2312
2313val EQ_IMP_THM = thm (#(FILE), #(LINE))("EQ_IMP_THM",
2314let val t1 = “t1:bool”
2315 and t2 = “t2:bool”
2316 val conj = “$/\”
2317 val [IMP1,IMP2,IMP3,_,IMP4] = map GEN_ALL(CONJUNCTS (SPEC_ALL IMP_CLAUSES))
2318 and [AND1,AND2,AND3,AND4,_] = map GEN_ALL(CONJUNCTS (SPEC_ALL AND_CLAUSES))
2319 and [EQ1,EQ2,EQ3,EQ4] = map GEN_ALL (CONJUNCTS (SPEC_ALL EQ_CLAUSES))
2320 val thTl = SPEC t2 EQ1
2321 and thFl = SPEC t2 EQ3
2322 val thTr = TRANS (MK_COMB (AP_TERM conj (SPEC t2 IMP1), SPEC t2 IMP2))
2323 (SPEC t2 AND2)
2324 and thFr = TRANS (MK_COMB (AP_TERM conj (SPEC t2 IMP3), SPEC t2 IMP4))
2325 (SPEC (mk_neg t2) AND1)
2326 val thT1 = TRANS thTl (SYM thTr)
2327 and thF1 = TRANS thFl (SYM thFr)
2328 val tm = “(t1 = t2) <=> (t1 ==> t2) /\ (t2 ==> t1)”
2329 val thT2 = SUBST_CONV [t1 |-> ASSUME “t1 = T”] tm tm
2330 and thF2 = SUBST_CONV [t1 |-> ASSUME “t1 = F”] tm tm
2331 val thT3 = EQ_MP (SYM thT2) thT1
2332 and thF3 = EQ_MP (SYM thF2) thF1
2333 in
2334 GENL [t1,t2] (DISJ_CASES (SPEC t1 BOOL_CASES_AX) thT3 thF3)
2335 end);
2336
2337(* ---------------------------------------------------------------------*)
2338(* EQ_EXPAND = |- !t1 t2. (t1 = t2) = ((t1 /\ t2) \/ (~t1 /\ ~t2)) *)
2339(* RJB 92.09.26 *)
2340(* ---------------------------------------------------------------------*)
2341
2342val EQ_EXPAND = thm (#(FILE), #(LINE))("EQ_EXPAND",
2343let val t1 = “t1:bool” and t2 = “t2:bool”
2344 val conj = “$/\” and disj = “$\/”
2345 val [NOT1,NOT2] = tl (CONJUNCTS NOT_CLAUSES)
2346 and [EQ1,EQ2,EQ3,EQ4] = map GEN_ALL (CONJUNCTS (SPEC_ALL EQ_CLAUSES))
2347 and [OR1,OR2,OR3,OR4,_] = map GEN_ALL (CONJUNCTS (SPEC_ALL OR_CLAUSES))
2348 and [AND1,AND2,AND3,AND4,_] = map GEN_ALL (CONJUNCTS(SPEC_ALL AND_CLAUSES))
2349 val thTl = SPEC t2 EQ1
2350 and thFl = SPEC t2 EQ3
2351 val thTr = TRANS (MK_COMB (AP_TERM disj (SPEC t2 AND1),
2352 TRANS (AP_THM (AP_TERM conj NOT1) (mk_neg t2))
2353 (SPEC (mk_neg t2) AND3)))
2354 (SPEC t2 OR4)
2355 and thFr = TRANS (MK_COMB (AP_TERM disj (SPEC t2 AND3),
2356 TRANS (AP_THM (AP_TERM conj NOT2) (mk_neg t2))
2357 (SPEC (mk_neg t2) AND1)))
2358 (SPEC (mk_neg t2) OR3)
2359 val thT1 = TRANS thTl (SYM thTr)
2360 and thF1 = TRANS thFl (SYM thFr)
2361 val tm = “(t1 = t2) <=> (t1 /\ t2) \/ (~t1 /\ ~t2)”
2362 val thT2 = SUBST_CONV [t1 |-> ASSUME “t1 = T”] tm tm
2363 and thF2 = SUBST_CONV [t1 |-> ASSUME “t1 = F”] tm tm
2364 val thT3 = EQ_MP (SYM thT2) thT1
2365 and thF3 = EQ_MP (SYM thF2) thF1
2366 in
2367 GENL [t1,t2] (DISJ_CASES (SPEC t1 BOOL_CASES_AX) thT3 thF3)
2368 end);
2369
2370(* ---------------------------------------------------------------------*)
2371(* COND_RATOR |- !b (f:'a->'b) g x. (b => f | g) x = (b => f x | g x) *)
2372(* *)
2373(* RJB 92.09.26 *)
2374(* ---------------------------------------------------------------------*)
2375
2376val COND_RATOR = thm (#(FILE), #(LINE))("COND_RATOR",
2377let val f = “f: 'a -> 'b”
2378 val g = “g: 'a -> 'b”
2379 val x = “x:'a”
2380 and b = “b:bool”
2381 val fx = “^f ^x” and gx = “^g ^x”
2382 val t1 = “t1:'a”
2383 val t2 = “t2:'a”
2384 val theta1 = [“:'a” |-> “:'a -> 'b”]
2385 val theta2 = [“:'a” |-> “:'b”]
2386 val (COND_T,COND_F) = (GENL[t1,t2]##GENL[t1,t2])
2387 (CONJ_PAIR(SPEC_ALL COND_CLAUSES))
2388 val thTl = AP_THM (SPECL [f,g] (INST_TYPE theta1 COND_T)) x
2389 and thFl = AP_THM (SPECL [f,g] (INST_TYPE theta1 COND_F)) x
2390 val thTr = SPECL [fx,gx] (INST_TYPE theta2 COND_T)
2391 and thFr = SPECL [fx,gx] (INST_TYPE theta2 COND_F)
2392 val thT1 = TRANS thTl (SYM thTr)
2393 and thF1 = TRANS thFl (SYM thFr)
2394 val tm = “(if b then (f:'a->'b ) else g) x = (if b then f x else g x)”
2395 val thT2 = SUBST_CONV [b |-> ASSUME “b = T”] tm tm
2396 and thF2 = SUBST_CONV [b |-> ASSUME “b = F”] tm tm
2397 val thT3 = EQ_MP (SYM thT2) thT1
2398 and thF3 = EQ_MP (SYM thF2) thF1
2399 in
2400 GENL [b,f,g,x] (DISJ_CASES (SPEC b BOOL_CASES_AX) thT3 thF3)
2401 end);
2402
2403(* ---------------------------------------------------------------------*)
2404(* COND_RAND *)
2405(* *)
2406(* |- !(f:'a->'b) b x y. f (b => x | y) = (b => f x | f y) *)
2407(* *)
2408(* RJB 92.09.26 *)
2409(* ---------------------------------------------------------------------*)
2410
2411val COND_RAND = thm (#(FILE), #(LINE))("COND_RAND",
2412let val f = “f: 'a -> 'b”
2413 val x = “x:'a”
2414 val y = “y:'a”
2415 and b = “b:bool”
2416 val fx = “^f ^x” and fy = “^f ^y”
2417 val t1 = “t1:'a”
2418 val t2 = “t2:'a”
2419 val theta = [Type.alpha |-> Type.beta]
2420 val (COND_T,COND_F) = (GENL[t1,t2]##GENL[t1,t2])
2421 (CONJ_PAIR (SPEC_ALL COND_CLAUSES))
2422 val thTl = AP_TERM f (SPECL [x,y] COND_T)
2423 and thFl = AP_TERM f (SPECL [x,y] COND_F)
2424 val thTr = SPECL [fx,fy] (INST_TYPE theta COND_T)
2425 and thFr = SPECL [fx,fy] (INST_TYPE theta COND_F)
2426 val thT1 = TRANS thTl (SYM thTr)
2427 and thF1 = TRANS thFl (SYM thFr)
2428 val tm = “(f:'a->'b ) (if b then x else y) = (if b then f x else f y)”
2429 val thT2 = SUBST_CONV [b |-> ASSUME “b = T”] tm tm
2430 and thF2 = SUBST_CONV [b |-> ASSUME “b = F”] tm tm
2431 val thT3 = EQ_MP (SYM thT2) thT1
2432 and thF3 = EQ_MP (SYM thF2) thF1
2433 in
2434 GENL [f,b,x,y] (DISJ_CASES (SPEC b BOOL_CASES_AX) thT3 thF3)
2435 end);
2436
2437(* ---------------------------------------------------------------------*)
2438(* COND_ABS *)
2439(* *)
2440(* |- !b (f:'a->'b) g. (\x. (b => f(x) | g(x))) = (b => f | g) *)
2441(* *)
2442(* RJB 92.09.26 *)
2443(* ---------------------------------------------------------------------*)
2444
2445val COND_ABS = thm (#(FILE), #(LINE))("COND_ABS",
2446let val b = “b:bool”
2447 val f = “f:'a->'b”
2448 val g = “g:'a->'b”
2449 val x = “x:'a”
2450 in
2451 GENL [b,f,g]
2452 (TRANS (ABS x (SYM (SPECL [b,f,g,x] COND_RATOR)))
2453 (ETA_CONV “\ ^x. (if ^b then ^f else ^g) ^x”))
2454 end);
2455
2456(* ---------------------------------------------------------------------*)
2457(* COND_EXPAND *)
2458(* *)
2459(* |- !b t1 t2. (b => t1 | t2) = ((~b \/ t1) /\ (b \/ t2)) *)
2460(* *)
2461(* RJB 92.09.26 *)
2462(* ---------------------------------------------------------------------*)
2463
2464val COND_EXPAND = thm (#(FILE), #(LINE))("COND_EXPAND",
2465let val b = “b:bool”
2466 val t1 = “t1:bool”
2467 val t2 = “t2:bool”
2468 val conj = “$/\”
2469 val disj = “$\/”
2470 val theta = [“:'a” |-> Type.bool]
2471 val (COND_T,COND_F) =
2472 let val t1 = “t1:'a” and t2 = “t2:'a”
2473 in (GENL[t1,t2]##GENL[t1,t2]) (CONJ_PAIR(SPEC_ALL COND_CLAUSES))
2474 end
2475 and [NOT1,NOT2] = tl (CONJUNCTS NOT_CLAUSES)
2476 and [OR1,OR2,OR3,OR4,_] = map GEN_ALL (CONJUNCTS (SPEC_ALL OR_CLAUSES))
2477 and [AND1,AND2,AND3,AND4,_] = map GEN_ALL (CONJUNCTS(SPEC_ALL AND_CLAUSES))
2478 val thTl = SPECL [t1,t2] (INST_TYPE theta COND_T)
2479 and thFl = SPECL [t1,t2] (INST_TYPE theta COND_F)
2480 val thTr =
2481 let val th1 = TRANS (AP_THM (AP_TERM disj NOT1) t1) (SPEC t1 OR3)
2482 and th2 = SPEC t2 OR1
2483 in
2484 TRANS (MK_COMB (AP_TERM conj th1,th2)) (SPEC t1 AND2)
2485 end
2486 and thFr =
2487 let val th1 = TRANS (AP_THM (AP_TERM disj NOT2) t1) (SPEC t1 OR1)
2488 and th2 = SPEC t2 OR3
2489 in
2490 TRANS (MK_COMB (AP_TERM conj th1,th2)) (SPEC t2 AND1)
2491 end
2492 val thT1 = TRANS thTl (SYM thTr)
2493 and thF1 = TRANS thFl (SYM thFr)
2494 val tm = “(if b then t1 else t2) = ((~b \/ t1) /\ (b \/ t2))”
2495 val thT2 = SUBST_CONV [b |-> ASSUME “b = T”] tm tm
2496 and thF2 = SUBST_CONV [b |-> ASSUME “b = F”] tm tm
2497 val thT3 = EQ_MP (SYM thT2) thT1
2498 and thF3 = EQ_MP (SYM thF2) thF1
2499 in
2500 GENL [b, t1, t2] (DISJ_CASES (SPEC b BOOL_CASES_AX) thT3 thF3)
2501 end);
2502
2503(* ---------------------------------------------------------------------*)
2504(* COND_EXPAND_IMP *)
2505(* *)
2506(* |- !b t1 t2. (b => t1 | t2) = ((b ==> t1) /\ (~b ==> t2)) *)
2507(* *)
2508(* TT 09.03.18 *)
2509(* ---------------------------------------------------------------------*)
2510
2511val COND_EXPAND_IMP = thm (#(FILE), #(LINE))("COND_EXPAND_IMP",
2512let val b = “b:bool”
2513 val t1 = “t1:bool”
2514 val t2 = “t2:bool”
2515 val nb = mk_neg b;
2516 val nnb = mk_neg nb;
2517 val imp_th1 = SPECL [b, t1] IMP_DISJ_THM;
2518 val imp_th2a = SPECL [nb, t2] IMP_DISJ_THM
2519 val imp_th2b = SUBST_CONV [nnb |-> (SPEC b (CONJUNCT1 NOT_CLAUSES))]
2520 (mk_disj (nnb, t2)) (mk_disj (nnb, t2))
2521 val imp_th2 = TRANS imp_th2a imp_th2b
2522 val new_rhs = “(b ==> t1) /\ (~b ==> t2)”;
2523 val subst = [mk_imp(b,t1) |-> imp_th1,
2524 mk_imp(nb,t2) |-> imp_th2]
2525 val th1 = SUBST_CONV subst new_rhs new_rhs
2526 val th2 = TRANS (SPECL [b,t1,t2] COND_EXPAND) (SYM th1)
2527in
2528 GENL [b,t1,t2] th2
2529end);
2530
2531(* ---------------------------------------------------------------------*)
2532(* COND_EXPAND_OR *)
2533(* *)
2534(* |- !b t1 t2. (b => t1 | t2) = ((b /\ t1) \/ (~b /\ t2)) *)
2535(* *)
2536(* TT 09.03.18 *)
2537(* ---------------------------------------------------------------------*)
2538
2539val COND_EXPAND_OR = thm (#(FILE), #(LINE))("COND_EXPAND_OR",
2540let val b = “b:bool”
2541 val t1 = “t1:bool”
2542 val t2 = “t2:bool”
2543 val conj = “$/\”
2544 val disj = “$\/”
2545 val theta = [“:'a” |-> Type.bool]
2546 val (COND_T,COND_F) =
2547 let val t1 = “t1:'a” and t2 = “t2:'a”
2548 in (GENL[t1,t2]##GENL[t1,t2]) (CONJ_PAIR(SPEC_ALL COND_CLAUSES))
2549 end
2550 and [NOT1,NOT2] = tl (CONJUNCTS NOT_CLAUSES)
2551 and [OR1,OR2,OR3,OR4,_] = map GEN_ALL (CONJUNCTS (SPEC_ALL OR_CLAUSES))
2552 and [AND1,AND2,AND3,AND4,_] = map GEN_ALL (CONJUNCTS(SPEC_ALL AND_CLAUSES))
2553 val thTl = SPECL [t1,t2] (INST_TYPE theta COND_T)
2554 and thFl = SPECL [t1,t2] (INST_TYPE theta COND_F)
2555 val thTr =
2556 let val th2 = TRANS (AP_THM (AP_TERM conj NOT1) t2) (SPEC t2 AND3)
2557 and th1 = SPEC t1 AND1
2558 in
2559 TRANS (MK_COMB (AP_TERM disj th1,th2)) (SPEC t1 OR4)
2560 end
2561 and thFr =
2562 let val th2 = TRANS (AP_THM (AP_TERM conj NOT2) t2) (SPEC t2 AND1)
2563 and th1 = SPEC t1 AND3
2564 in
2565 TRANS (MK_COMB (AP_TERM disj th1,th2)) (SPEC t2 OR3)
2566 end
2567 val thT1 = TRANS thTl (SYM thTr)
2568 and thF1 = TRANS thFl (SYM thFr)
2569 val tm = “(if b then t1 else t2) = ((b /\ t1) \/ (~b /\ t2))”
2570 val thT2 = SUBST_CONV [b |-> ASSUME “b = T”] tm tm
2571 and thF2 = SUBST_CONV [b |-> ASSUME “b = F”] tm tm
2572 val thT3 = EQ_MP (SYM thT2) thT1
2573 and thF3 = EQ_MP (SYM thF2) thF1
2574 in
2575 GENL [b, t1, t2] (DISJ_CASES (SPEC b BOOL_CASES_AX) thT3 thF3)
2576 end);
2577
2578
2579val TYPE_DEFINITION_THM = thm (#(FILE), #(LINE))("TYPE_DEFINITION_THM",
2580 let val P = “P:'a-> bool”
2581 val rep = “rep :'b -> 'a”
2582 in
2583 GEN P (GEN rep
2584 (RIGHT_BETA(AP_THM
2585 (RIGHT_BETA (AP_THM TYPE_DEFINITION P)) rep)))
2586 end);
2587
2588val ONTO_THM = thm (#(FILE), #(LINE))(
2589 "ONTO_THM",
2590 let val f = mk_var("f", Type.alpha --> Type.beta)
2591 in
2592 GEN f (RIGHT_BETA (AP_THM ONTO_DEF f))
2593 end);
2594
2595val ONE_ONE_THM = thm (#(FILE), #(LINE))(
2596 "ONE_ONE_THM",
2597 let val f = mk_var("f", Type.alpha --> Type.beta)
2598 in
2599 GEN f (RIGHT_BETA (AP_THM ONE_ONE_DEF f))
2600 end);
2601
2602(*---------------------------------------------------------------------------*
2603 * ABS_REP_THM *
2604 * |- !P. (?rep. TYPE_DEFINITION P rep) ==> *
2605 * ?rep abs. (!a. abs (rep a) = a) /\ !r. P r = (rep (abs r) = r) *
2606 *---------------------------------------------------------------------------*)
2607
2608val ABS_REP_THM = thm (#(FILE), #(LINE))("ABS_REP_THM",
2609 let val th1 = ASSUME “?rep:'b->'a. TYPE_DEFINITION P rep”
2610 val th2 = MK_EXISTS (SPEC “P:'a->bool” TYPE_DEFINITION_THM)
2611 val def = EQ_MP th2 th1
2612 val asm = ASSUME (snd(dest_exists(concl def)))
2613 val (asm1,asm2) = CONJ_PAIR asm
2614 val rep_eq =
2615 let val th1 = DISCH “a:'b=a'”
2616 (AP_TERM “rep:'b->'a” (ASSUME “a:'b=a'”))
2617 in IMP_ANTISYM_RULE (SPECL [“a:'b”,“a':'b”] asm1) th1
2618 end
2619 val ABS = “\r:'a. @a:'b. r = rep a”
2620 val absd = RIGHT_BETA (AP_THM (REFL ABS) “rep (a:'b):'a”)
2621 val lem = SYM(SELECT_RULE(EXISTS (“?a':'b.a=a'”,“a:'b”)
2622 (REFL “a:'b”)))
2623 val TH1 = GEN “a:'b”
2624 (TRANS(TRANS absd (SELECT_EQ “a':'b” rep_eq)) lem)
2625 val t1 = SELECT_RULE(EQ_MP (SPEC “r:'a” asm2)
2626 (ASSUME “(P:'a->bool) r”))
2627 val absd2 = RIGHT_BETA (AP_THM (REFL ABS) “r:'a”)
2628 val v = mk_var("v",type_of(rhs (concl absd2)))
2629 val (t1l,t1r) = dest_eq (concl t1)
2630 (* val rep = fst(strip_comb t1r) *)
2631 val rep = rator t1r
2632 val template = mk_eq(t1l, mk_comb(rep,v))
2633 val imp1 = DISCH “(P:'a->bool) r”
2634 (SYM (SUBST [v |-> SYM absd2] template t1))
2635 val t2 = EXISTS (“?a:'b. r:'a = rep a”, “^ABS r”)
2636 (SYM(ASSUME “rep(^ABS (r:'a):'b) = r”))
2637 val imp2 = DISCH “rep(^ABS (r:'a):'b) = r”
2638 (EQ_MP (SYM (SPEC “r:'a” asm2)) t2)
2639 val TH2 = GEN “r:'a” (IMP_ANTISYM_RULE imp1 imp2)
2640 val CTH = CONJ TH1 TH2
2641 val ath = subst [ABS |-> “abs:'a->'b”] (concl CTH)
2642 val eth1 = EXISTS (“?abs:'a->'b. ^ath”, ABS) CTH
2643 val eth2 = EXISTS (“?rep:'b->'a. ^(concl eth1)”,
2644 “rep:'b->'a”) eth1
2645 val result = DISCH (concl th1) (CHOOSE (“rep:'b->'a”,def) eth2)
2646 in
2647 GEN “P:'a->bool” result
2648 end);
2649
2650(*---------------------------------------------------------------------------
2651 LET_RAND = P (let x = M in N x) = (let x = M in P (N x))
2652 ---------------------------------------------------------------------------*)
2653
2654val LET_RAND = thm (#(FILE), #(LINE))("LET_RAND",
2655 let val tm1 = “\x:'a. P (N x:'b):bool”
2656 val tm2 = “M:'a”
2657 val tm3 = “\x:'a. N x:'b”
2658 val P = “P:'b -> bool”
2659 val LET_THM1 = RIGHT_BETA (SPEC tm2 (SPEC tm1
2660 (Thm.INST_TYPE [beta |-> bool] LET_THM)))
2661 val LET_THM2 = AP_TERM P (RIGHT_BETA (SPEC tm2 (SPEC tm3 LET_THM)))
2662 in TRANS LET_THM2 (SYM LET_THM1)
2663 end);
2664
2665
2666(*---------------------------------------------------------------------------
2667 LET_RATOR = (let x = M in N x) b = (let x = M in N x b)
2668 ---------------------------------------------------------------------------*)
2669
2670val LET_RATOR = thm (#(FILE), #(LINE))("LET_RATOR",
2671 let val M = “M:'a”
2672 val b = “b:'b”
2673 val tm1 = “\x:'a. N x:'b->'c”
2674 val tm2 = “\x:'a. N x ^b:'c”
2675 val LET_THM1 = AP_THM (RIGHT_BETA (SPEC M (SPEC tm1
2676 (Thm.INST_TYPE [beta |-> (beta --> gamma)] LET_THM)))) b
2677 val LET_THM2 = RIGHT_BETA (SPEC M (SPEC tm2
2678 (Thm.INST_TYPE [beta |-> gamma] LET_THM)))
2679 in TRANS LET_THM1 (SYM LET_THM2)
2680 end);
2681
2682
2683(*---------------------------------------------------------------------------
2684 !P. (!x y. P x y) = (!y x. P x y)
2685 ---------------------------------------------------------------------------*)
2686
2687val SWAP_FORALL_THM = thm (#(FILE), #(LINE))("SWAP_FORALL_THM",
2688 let val P = mk_var("P", “:'a->'b->bool”)
2689 val x = mk_var("x", Type.alpha)
2690 val y = mk_var("y", Type.beta)
2691 val Pxy = list_mk_comb (P,[x,y])
2692 val th1 = ASSUME (list_mk_forall [x,y] Pxy)
2693 val th2 = DISCH_ALL (GEN y (GEN x (SPEC y (SPEC x th1))))
2694 val th3 = ASSUME (list_mk_forall [y,x] Pxy)
2695 val th4 = DISCH_ALL (GEN x (GEN y (SPEC x (SPEC y th3))))
2696 in
2697 GEN P (IMP_ANTISYM_RULE th2 th4)
2698 end);
2699
2700(*---------------------------------------------------------------------------
2701 !P. (?x y. P x y) = (?y x. P x y)
2702 ---------------------------------------------------------------------------*)
2703
2704val SWAP_EXISTS_THM = thm (#(FILE), #(LINE))("SWAP_EXISTS_THM",
2705 let val P = mk_var("P", “:'a->'b->bool”)
2706 val x = mk_var("x", Type.alpha)
2707 val y = mk_var("y", Type.beta)
2708 val Pxy = list_mk_comb (P,[x,y])
2709 val tm1 = list_mk_exists[x] Pxy
2710 val tm2 = list_mk_exists[y] tm1
2711 val tm3 = list_mk_exists[y] Pxy
2712 val tm4 = list_mk_exists[x] tm3
2713 val th1 = ASSUME Pxy
2714 val th2 = EXISTS(tm2,y) (EXISTS (tm1,x) th1)
2715 val th3 = ASSUME (list_mk_exists [y] Pxy)
2716 val th4 = CHOOSE(y,th3) th2
2717 val th5 = CHOOSE(x,ASSUME (list_mk_exists [x,y] Pxy)) th4
2718 val th6 = EXISTS(tm4,x) (EXISTS (tm3,y) th1)
2719 val th7 = ASSUME (list_mk_exists[x] Pxy)
2720 val th8 = CHOOSE(x,th7) th6
2721 val th9 = CHOOSE(y,ASSUME (list_mk_exists [y,x] Pxy)) th8
2722 in
2723 GEN P (IMP_ANTISYM_RULE (DISCH_ALL th5) (DISCH_ALL th9))
2724 end);
2725
2726(*---------------------------------------------------------------------------
2727 EXISTS_UNIQUE_THM
2728
2729 (?!x. P x) = (?x. P x) /\ (!x y. P x /\ P y ==> (x = y))
2730 ---------------------------------------------------------------------------*)
2731
2732val EXISTS_UNIQUE_THM = thm (#(FILE), #(LINE))("EXISTS_UNIQUE_THM",
2733 let val th1 = RIGHT_BETA (AP_THM EXISTS_UNIQUE_DEF “\x:'a. P x:bool”)
2734 val th2 = CONV_RULE (RAND_CONV (RAND_CONV
2735 (QUANT_CONV (QUANT_CONV (RATOR_CONV
2736 (RAND_CONV (RAND_CONV BETA_CONV))))))) th1
2737 in
2738 CONV_RULE (RAND_CONV (RAND_CONV (QUANT_CONV (QUANT_CONV (RATOR_CONV
2739 (RAND_CONV (RATOR_CONV (RAND_CONV BETA_CONV)))))))) th2
2740 end);
2741
2742(* ----------------------------------------------------------------------
2743 EXISTS_UNIQUE_ALT'
2744
2745 |- !P. (?!x. P x) <=> ?x. !y. P y <=> (y = x)
2746 ---------------------------------------------------------------------- *)
2747
2748val EXISTS_UNIQUE_ALT' = thm (#(FILE), #(LINE))(
2749 "EXISTS_UNIQUE_ALT'",
2750 let
2751 val eu_r = ASSUME (rhs (concl EXISTS_UNIQUE_THM))
2752 val (eu1, eu2) = CONJ_PAIR eu_r
2753 val P = mk_var("P", alpha --> bool)
2754 val x = mk_var("x", alpha)
2755 val y = mk_var("y", alpha)
2756 val c = mk_var("c", alpha)
2757 val yeqx = mk_eq(y,x)
2758 val Px = mk_comb(P, x)
2759 val Py = mk_comb(P, y)
2760 val th1a = MP (SPECL [y,x] eu2) (CONJ (ASSUME Py) (ASSUME Px)) |> DISCH Py
2761 val th1b = EQ_MP (SYM (AP_TERM P (ASSUME yeqx))) (ASSUME Px) |> DISCH yeqx
2762 val th1_noex = IMP_ANTISYM_RULE th1a th1b |> GEN y
2763 val th1_noch = EXISTS(mk_exists(x,concl th1_noex), x) th1_noex
2764 val th1 = CHOOSE(x,eu1) th1_noch
2765 val pyyeq = concl th1
2766 val pyyeqc = subst [x |-> c] (#2 (dest_exists pyyeq))
2767 val pyyeqc_th = ASSUME pyyeqc
2768 val th2a = pyyeqc_th |> SPEC c |> C EQ_MP (REFL c) o SYM
2769 |> EXISTS(mk_exists(x,Px), c)
2770 val (pxy_x,pxy_y) = ASSUME (mk_conj(Px,Py)) |> CONJ_PAIR
2771 val th2b1 = pyyeqc_th |> SPEC x |> C EQ_MP (ASSUME Px) |> PROVE_HYP pxy_x
2772 val th2b2 = pyyeqc_th |> SPEC y |> C EQ_MP (ASSUME Py) |> PROVE_HYP pxy_y
2773 val th2b = TRANS th2b1 (SYM th2b2) |> DISCH (mk_conj(Px,Py)) |> GENL [x,y]
2774 val th2 = CHOOSE (c, ASSUME pyyeq) (CONJ th2a th2b)
2775 val eqn = IMP_ANTISYM_RULE (DISCH_ALL th1) (DISCH_ALL th2)
2776 in
2777 TRANS EXISTS_UNIQUE_THM eqn
2778 end);
2779
2780
2781(*---------------------------------------------------------------------------
2782 LET_CONG =
2783 |- !f g M N. (M = N) /\ (!x. (x = N) ==> (f x = g x))
2784 ==>
2785 (LET f M = LET g N)
2786 ---------------------------------------------------------------------------*)
2787
2788val LET_CONG = thm (#(FILE), #(LINE))("LET_CONG",
2789 let val f = mk_var("f",alpha-->beta)
2790 val g = mk_var("g",alpha-->beta)
2791 val M = mk_var("M",alpha)
2792 val N = mk_var("N",alpha)
2793 val x = mk_var ("x",alpha)
2794 val MeqN = mk_eq(M,N)
2795 val x_eq_N = mk_eq(x,N)
2796 val fx_eq_gx = mk_eq(mk_comb(f,x),mk_comb(g,x))
2797 val ctm = mk_forall(x, mk_imp(x_eq_N,fx_eq_gx))
2798 val th = RIGHT_BETA(AP_THM(RIGHT_BETA(AP_THM LET_DEF f)) M)
2799 val th1 = ASSUME MeqN
2800 val th2 = MP (SPEC N (ASSUME ctm)) (REFL N)
2801 val th3 = SUBS [SYM th1] th2
2802 val th4 = TRANS (TRANS th th3) (MK_COMB (REFL g,th1))
2803 val th5 = RIGHT_BETA(AP_THM(RIGHT_BETA(AP_THM LET_DEF g)) N)
2804 val th6 = TRANS th4 (SYM th5)
2805 val th7 = SUBS [SPECL [MeqN, ctm, concl th6] AND_IMP_INTRO]
2806 (DISCH MeqN (DISCH ctm th6))
2807 in
2808 GENL [f,g,M,N] th7
2809 end);
2810
2811(*---------------------------------------------------------------------------
2812 IMP_CONG =
2813 |- !x x' y y'. (x = x') /\ (x' ==> (y = y'))
2814 ==>
2815 (x ==> y = x' ==> y')
2816 ---------------------------------------------------------------------------*)
2817
2818val IMP_CONG = thm (#(FILE), #(LINE))("IMP_CONG",
2819 let val x = mk_var("x",Type.bool)
2820 val x' = mk_var("x'",Type.bool)
2821 val y = mk_var("y",Type.bool)
2822 val y' = mk_var("y'",Type.bool)
2823 val x_eq_x' = mk_eq(x,x')
2824 val ctm = mk_imp(x', mk_eq(y,y'))
2825 val x_imp_y = mk_imp(x,y)
2826 val x'_imp_y' = mk_imp(x',y')
2827 val th = ASSUME x_eq_x'
2828 val th1 = UNDISCH(ASSUME ctm)
2829 val th2 = ASSUME x_imp_y
2830 val th3 = DISCH x_imp_y (DISCH x' (UNDISCH(SUBS [th,th1] th2)))
2831 val th4 = ASSUME x'_imp_y'
2832 val th5 = UNDISCH (SUBS [SYM th] (DISCH x' th1))
2833 val th6 = DISCH x'_imp_y' (DISCH x (UNDISCH(SUBS [SYM th,SYM th5] th4)))
2834 val th7 = IMP_ANTISYM_RULE th3 th6
2835 val th8 = DISCH x_eq_x' (DISCH ctm th7)
2836 val th9 = SUBS [SPECL [x_eq_x', ctm, concl th7] AND_IMP_INTRO] th8
2837 in
2838 GENL [x,x',y,y'] th9
2839 end);
2840
2841(*---------------------------------------------------------------------------
2842 AND_CONG = |- !P P' Q Q'.
2843 (Q ==> (P = P')) /\ (P' ==> (Q = Q'))
2844 ==>
2845 (P /\ Q = P' /\ Q')
2846 ---------------------------------------------------------------------------*)
2847
2848val AND_CONG = thm (#(FILE), #(LINE))("AND_CONG",
2849 let val P = mk_var("P",Type.bool)
2850 val P' = mk_var("P'",Type.bool)
2851 val Q = mk_var("Q",Type.bool)
2852 val Q' = mk_var("Q'",Type.bool)
2853 val PandQ = mk_conj(P,Q)
2854 val P'andQ' = mk_conj(P',Q')
2855 val ctm1 = mk_imp(Q, mk_eq(P,P'))
2856 val ctm2 = mk_imp(P', mk_eq(Q,Q'))
2857 val th1 = ASSUME PandQ
2858 val th2 = MP (ASSUME ctm1) (CONJUNCT2 th1)
2859 val th3 = MP (ASSUME ctm2) (SUBS [th2] (CONJUNCT1 th1))
2860 val th4 = DISCH PandQ (SUBS[th2,th3] th1)
2861 val th5 = ASSUME P'andQ'
2862 val th6 = MP (ASSUME ctm2) (CONJUNCT1 th5)
2863 val th7 = MP (ASSUME ctm1) (SUBS [SYM th6] (CONJUNCT2 th5))
2864 val th8 = DISCH P'andQ' (SUBS[SYM th6,SYM th7] th5)
2865 val th9 = IMP_ANTISYM_RULE th4 th8
2866 val th10 = SUBS [SPECL [ctm1,ctm2,concl th9] AND_IMP_INTRO]
2867 (DISCH ctm1 (DISCH ctm2 th9))
2868 in
2869 GENL [P,P',Q,Q'] th10
2870 end);
2871
2872(*---------------------------------------------------------------------------
2873 LEFT_AND_CONG =
2874 |- !P P' Q Q'.
2875 (P = P') /\ (P' ==> (Q = Q'))
2876 ==>
2877 (P /\ Q = P' /\ Q')
2878 ---------------------------------------------------------------------------*)
2879
2880val LEFT_AND_CONG = thm (#(FILE), #(LINE))("LEFT_AND_CONG",
2881 let val P = mk_var("P",Type.bool)
2882 val P' = mk_var("P'",Type.bool)
2883 val Q = mk_var("Q",Type.bool)
2884 val Q' = mk_var("Q'",Type.bool)
2885 val PandQ = mk_conj(P,Q)
2886 val P'andQ' = mk_conj(P',Q')
2887 val ctm1 = mk_eq(P,P')
2888 val ctm2 = mk_imp(P', mk_eq(Q,Q'))
2889 val th1 = ASSUME PandQ
2890 val th2 = ASSUME ctm1
2891 val th3 = SUBS [th2] (CONJUNCT1 th1)
2892 val th3a = MP (ASSUME ctm2) th3
2893 val th4 = DISCH PandQ (SUBS[th2,th3a] th1)
2894 val th5 = ASSUME P'andQ'
2895 val th6 = SUBS [SYM th2] (CONJUNCT1 th5)
2896 val th7 = SYM(MP (ASSUME ctm2) (CONJUNCT1 th5))
2897 val th8 = DISCH P'andQ' (SUBS[SYM th2,th7] th5)
2898 val th9 = IMP_ANTISYM_RULE th4 th8
2899 val th10 = SUBS [SPECL [ctm1,ctm2,concl th9] AND_IMP_INTRO]
2900 (DISCH ctm1 (DISCH ctm2 th9))
2901 in
2902 GENL [P,P',Q,Q'] th10
2903 end);
2904
2905(*---------------------------------------------------------------------------
2906 val OR_CONG =
2907 |- !P P' Q Q'.
2908 (~Q ==> (P = P')) /\ (~P' ==> (Q = Q'))
2909 ==>
2910 (P \/ Q = P' \/ Q')
2911 ---------------------------------------------------------------------------*)
2912
2913val OR_CONG = thm (#(FILE), #(LINE))("OR_CONG",
2914 let val P = mk_var("P",Type.bool)
2915 val P' = mk_var("P'",Type.bool)
2916 val Q = mk_var("Q",Type.bool)
2917 val Q' = mk_var("Q'",Type.bool)
2918 val notQ = mk_neg Q
2919 val notP' = mk_neg P'
2920 val PorQ = mk_disj(P,Q)
2921 val P'orQ' = mk_disj(P',Q')
2922 val PeqP'= mk_eq(P,P')
2923 val QeqQ'= mk_eq(Q,Q')
2924 val ctm1 = mk_imp(notQ,PeqP')
2925 val ctm2 = mk_imp(notP',QeqQ')
2926 val th1 = ASSUME PorQ
2927 val th2 = ASSUME P
2928 val th3 = ASSUME Q
2929 val th4 = ASSUME ctm1
2930 val th5 = ASSUME ctm2
2931 val th6 = SUBS [SPEC Q (CONJUNCT1 NOT_CLAUSES)]
2932 (SUBS [SPECL[notQ, PeqP'] IMP_DISJ_THM] th4)
2933 val th7 = SUBS [SPEC P' (CONJUNCT1 NOT_CLAUSES)]
2934 (SUBS [SPECL[notP', QeqQ'] IMP_DISJ_THM] th5)
2935 val th8 = ASSUME P'
2936 val th9 = DISJ1 th8 Q'
2937 val th10 = ASSUME QeqQ'
2938 val th11 = SUBS [th10] th3
2939 val th12 = DISJ2 P' th11
2940 val th13 = ASSUME PeqP'
2941 val th14 = MK_COMB(REFL(mk_const("\\/",bool-->bool-->bool)),th13)
2942 val th15 = EQ_MP (MK_COMB (th14,th10)) th1
2943 val th16 = DISJ_CASES th6 th12 th15
2944 val th17 = DISCH PorQ (DISJ_CASES th7 th9 th16)
2945 val th18 = ASSUME P'orQ'
2946 val th19 = DISJ2 P th3
2947 val th20 = DISJ1 (SUBS [SYM th13] th8) Q
2948 val th21 = EQ_MP (SYM (MK_COMB(th14,th10))) th18
2949 val th22 = DISJ_CASES th7 th20 th21
2950 val th23 = DISCH P'orQ' (DISJ_CASES th6 th19 th22)
2951 val th24 = IMP_ANTISYM_RULE th17 th23
2952 val th25 = SUBS [SPECL [ctm1,ctm2,concl th24] AND_IMP_INTRO]
2953 (DISCH ctm1 (DISCH ctm2 th24))
2954 in
2955 GENL [P,P',Q,Q'] th25
2956 end);
2957
2958(*---------------------------------------------------------------------------
2959 val LEFT_OR_CONG =
2960 |- !P P' Q Q'.
2961 (P = P') /\ (~P' ==> (Q = Q'))
2962 ==>
2963 (P \/ Q = P' \/ Q')
2964 ---------------------------------------------------------------------------*)
2965
2966val LEFT_OR_CONG = thm (#(FILE), #(LINE))("LEFT_OR_CONG",
2967 let fun mk_boolvar s = mk_var(s,Type.bool)
2968 val [P,P',Q,Q'] = map mk_boolvar ["P","P'","Q","Q'"]
2969 val notP = mk_neg P
2970 val notP' = mk_neg P'
2971 val PorQ = mk_disj(P,Q)
2972 val P'orQ' = mk_disj(P',Q')
2973 val PeqP' = mk_eq(P,P')
2974 val ctm = mk_imp(notP',mk_eq(Q,Q'))
2975 val th1 = ASSUME ctm
2976 val th2 = ASSUME PeqP'
2977 val th3 = DISJ1 (SUBS [th2] (ASSUME P)) Q'
2978 val th4 = MP th1 (SUBS [th2] (ASSUME notP))
2979 val th5 = DISJ2 P' (SUBS [th4] (ASSUME Q))
2980 val th6 = DISJ_CASES (SPEC P EXCLUDED_MIDDLE) th3 th5
2981 val th7 = DISCH PorQ (DISJ_CASES (ASSUME PorQ) th3 th6)
2982 val th8 = DISJ1 (SUBS [SYM th2] (ASSUME P')) Q
2983 val th9 = MP th1 (ASSUME notP')
2984 val th10 = DISJ2 P (SUBS [SYM th9] (ASSUME Q'))
2985 val th11 = DISJ_CASES (SPEC P' EXCLUDED_MIDDLE) th8 th10
2986 val th12 = DISCH P'orQ' (DISJ_CASES (ASSUME P'orQ') th8 th11)
2987 val th13 = DISCH PeqP' (DISCH ctm (IMP_ANTISYM_RULE th7 th12))
2988 val th14 = SUBS[SPECL [PeqP',ctm,mk_eq(PorQ,P'orQ')] AND_IMP_INTRO] th13
2989 in
2990 GENL [P,P',Q,Q'] th14
2991 end);
2992
2993(*---------------------------------------------------------------------------
2994 val COND_CONG =
2995 |- !P Q x x' y y'.
2996 (P = Q) /\ (Q ==> (x = x')) /\ (~Q ==> (y = y'))
2997 ==>
2998 ((if P then x else y) = (if Q then x' else y'))
2999 ---------------------------------------------------------------------------*)
3000
3001fun mk_cond {cond,larm,rarm} = “if ^cond then ^larm else ^rarm”;
3002
3003val COND_CONG = thm (#(FILE), #(LINE))("COND_CONG",
3004 let val P = mk_var("P",Type.bool)
3005 val Q = mk_var("Q",Type.bool)
3006 val x = mk_var("x",alpha)
3007 val x' = mk_var("x'",alpha)
3008 val y = mk_var("y",alpha)
3009 val y' = mk_var("y'",alpha)
3010 val PeqQ = mk_eq(P,Q)
3011 val ctm1 = mk_imp(Q, mk_eq(x,x'))
3012 val ctm2 = mk_imp(mk_neg Q, mk_eq(y,y'))
3013 val target = mk_eq(mk_cond{cond=P,larm=x,rarm=y},
3014 mk_cond{cond=Q,larm=x',rarm=y'})
3015 val OR_ELIM = MP (SPECL[target,P,mk_neg P] OR_ELIM_THM)
3016 (SPEC P EXCLUDED_MIDDLE)
3017 val th1 = ASSUME P
3018 val th2 = EQT_INTRO th1
3019 val th3 = CONJUNCT1 (SPECL [x,y] COND_CLAUSES)
3020 val th3a = CONJUNCT1 (SPECL [x',y'] COND_CLAUSES)
3021 val th4 = SUBS [SYM th2] th3
3022 val th4a = SUBS [SYM th2] th3a
3023 val th5 = ASSUME PeqQ
3024 val th6 = ASSUME ctm1
3025 val th7 = ASSUME ctm2
3026 val th8 = UNDISCH (SUBS [SYM th5] th6)
3027 val th9 = TRANS th4 th8
3028 val th10 = TRANS th9 (SYM (SUBS [th5] th4a))
3029 val th11 = EQF_INTRO (ASSUME (mk_neg P))
3030 val th12 = CONJUNCT2 (SPECL [x,y] COND_CLAUSES)
3031 val th13 = CONJUNCT2 (SPECL [x',y'] COND_CLAUSES)
3032 val th14 = SUBS [SYM th11] th12
3033 val th15 = SUBS [SYM th11] th13
3034 val th16 = UNDISCH (SUBS [SYM th5] th7)
3035 val th17 = TRANS th14 th16
3036 val th18 = TRANS th17 (SYM (SUBS [th5] th15))
3037 val th19 = MP (MP OR_ELIM (DISCH P th10)) (DISCH (mk_neg P) th18)
3038 val th20 = DISCH PeqQ (DISCH ctm1 (DISCH ctm2 th19))
3039 val th21 = SUBS [SPECL [ctm1, ctm2,concl th19] AND_IMP_INTRO] th20
3040 val cnj = mk_conj(ctm1,ctm2)
3041 val th22 = SUBS [SPECL [PeqQ,cnj,concl th19] AND_IMP_INTRO] th21
3042 in
3043 GENL [P,Q,x,x',y,y'] th22
3044 end);
3045
3046(* ----------------------------------------------------------------------
3047
3048 RES_FORALL_CONG
3049 |- (P = Q) ==> (!x. x IN Q ==> (f x = g x)) ==>
3050 (RES_FORALL P f = RES_FORALL Q g)
3051
3052 RES_EXISTS_CONG
3053 |- (P = Q) ==> (!x. x IN Q ==> (f x = g x)) ==>
3054 (RES_EXISTS P f = RES_EXISTS P g)
3055 ---------------------------------------------------------------------- *)
3056
3057val (RES_FORALL_CONG, RES_EXISTS_CONG) = let
3058 (* stuff in common to both *)
3059 val aset_ty = alpha --> bool
3060 val [P,Q,f,g] = map (fn s => mk_var(s, aset_ty)) ["P", "Q", "f", "g"]
3061 val PeqQ_t = mk_eq(P, Q)
3062 val PeqQ_th = ASSUME PeqQ_t
3063 val x = mk_var("x", alpha)
3064 val fx_t = mk_comb(f, x)
3065 val gx_t = mk_comb(g, x)
3066 val IN_t = prim_mk_const {Thy = "bool", Name = "IN"}
3067 val xINP_t = list_mk_comb(IN_t, [x, P])
3068 val xINP_th = ASSUME xINP_t
3069 val xINQ_t = list_mk_comb(IN_t, [x, Q])
3070 val xINQ_th = ASSUME xINQ_t
3071 val xINP_eq_xINQ_th = AP_TERM (mk_comb(IN_t, x)) PeqQ_th
3072 val (xINP_imp_xINQ, xINQ_imp_xINP) = EQ_IMP_RULE xINP_eq_xINQ_th
3073 val feqg_t = mk_forall(x, mk_imp(xINQ_t, mk_eq(mk_comb(f,x), mk_comb(g, x))))
3074 val feqg_th = SPEC x (ASSUME feqg_t)
3075 val feqg_th = MP feqg_th xINQ_th
3076 val (f_imp_g_th, g_imp_f_th) = EQ_IMP_RULE feqg_th
3077
3078 fun mk_res th args =
3079 List.foldl (RIGHT_BETA o uncurry (C AP_THM)) th args
3080
3081 (* forall thm *)
3082 val resfa_t = prim_mk_const {Thy = "bool", Name = "RES_FORALL"}
3083 val res_pf_t = list_mk_comb(resfa_t, [P, f])
3084 val res_qg_t = list_mk_comb(resfa_t, [Q, g])
3085 val resfa_pf_eqn = mk_res RES_FORALL_DEF [P, f]
3086 val resfa_qg_eqn = mk_res RES_FORALL_DEF [Q, g]
3087
3088 val resfa_pf_eq_th = SPEC x (EQ_MP resfa_pf_eqn (ASSUME res_pf_t))
3089 val g_th = MP f_imp_g_th (MP resfa_pf_eq_th xINP_th)
3090 val xinq_imp_g_th =
3091 GEN x (DISCH xINQ_t (PROVE_HYP (UNDISCH xINQ_imp_xINP) g_th))
3092 val rfa_pf_imp_rfa_qg =
3093 DISCH res_pf_t (EQ_MP (SYM resfa_qg_eqn) xinq_imp_g_th)
3094
3095 val resfa_qg_eq_th = SPEC x (EQ_MP resfa_qg_eqn (ASSUME res_qg_t))
3096 val f_th = MP g_imp_f_th (MP resfa_qg_eq_th xINQ_th)
3097 val xinp_imp_f_th =
3098 GEN x (DISCH xINP_t (PROVE_HYP (UNDISCH xINP_imp_xINQ) f_th))
3099 val rfa_qg_imp_rfa_pf =
3100 DISCH res_qg_t (EQ_MP (SYM resfa_pf_eqn) xinp_imp_f_th)
3101 val fa_eqn = IMP_ANTISYM_RULE rfa_pf_imp_rfa_qg rfa_qg_imp_rfa_pf
3102
3103 (* exists thm *)
3104 val resex_t = prim_mk_const {Thy = "bool", Name = "RES_EXISTS"}
3105 val res_pf_t = list_mk_comb(resex_t, [P, f])
3106 val res_qg_t = list_mk_comb(resex_t, [Q, g])
3107 val resex_pf_eqn = mk_res RES_EXISTS_DEF [P, f]
3108 val resex_qg_eqn = mk_res RES_EXISTS_DEF [Q, g]
3109
3110 val pf_exbody_th = EQ_MP resex_pf_eqn (ASSUME res_pf_t)
3111 val pf_body_th = ASSUME(mk_conj(xINP_t, fx_t))
3112 val (new_xINP_th, fx_th) = CONJ_PAIR pf_body_th
3113 val new_xINQ_th = MP xINP_imp_xINQ new_xINP_th
3114 val new_gx_th = PROVE_HYP new_xINQ_th (MP f_imp_g_th fx_th)
3115 val qg_exists =
3116 EXISTS(rhs (concl resex_qg_eqn), x) (CONJ new_xINQ_th new_gx_th)
3117 val pf_chosen = CHOOSE(x,EQ_MP resex_pf_eqn (ASSUME res_pf_t)) qg_exists
3118 val ex_pf_imp_qg = DISCH res_pf_t (EQ_MP (SYM resex_qg_eqn) pf_chosen)
3119
3120 val qg_exbody_th = EQ_MP resex_qg_eqn (ASSUME res_qg_t)
3121 val qg_body_th = ASSUME(mk_conj(xINQ_t, gx_t))
3122 val (new_xINQ_th, gx_th) = CONJ_PAIR qg_body_th
3123 val new_xINP_th = MP xINQ_imp_xINP new_xINQ_th
3124 val new_fx_th = PROVE_HYP new_xINQ_th (MP g_imp_f_th gx_th)
3125 val pf_exists =
3126 EXISTS (rhs (concl resex_pf_eqn), x) (CONJ new_xINP_th new_fx_th)
3127 val qg_chosen = CHOOSE(x, EQ_MP resex_qg_eqn (ASSUME res_qg_t)) pf_exists
3128 val ex_qg_imp_pf = DISCH res_qg_t (EQ_MP (SYM resex_pf_eqn) qg_chosen)
3129
3130 val ex_eqn = IMP_ANTISYM_RULE ex_pf_imp_qg ex_qg_imp_pf
3131
3132in
3133 (thm (#(FILE), #(LINE))("RES_FORALL_CONG",
3134 DISCH PeqQ_t (DISCH feqg_t fa_eqn)),
3135 thm (#(FILE), #(LINE))("RES_EXISTS_CONG",
3136 DISCH PeqQ_t (DISCH feqg_t ex_eqn)))
3137end
3138
3139(* ------------------------------------------------------------------------- *)
3140(* Monotonicity. *)
3141(* ------------------------------------------------------------------------- *)
3142
3143
3144(* ------------------------------------------------------------------------- *)
3145(* MONO_AND |- (x ==> y) /\ (z ==> w) ==> (x /\ z ==> y /\ w) *)
3146(* ------------------------------------------------------------------------- *)
3147
3148val MONO_AND = thm (#(FILE), #(LINE))("MONO_AND",
3149 let val tm1 = “x ==> y”
3150 val tm2 = “z ==> w”
3151 val tm3 = “x /\ z”
3152 val tm4 = “y /\ w”
3153 val th1 = ASSUME tm1
3154 val th2 = ASSUME tm2
3155 val th3 = ASSUME tm3
3156 val th4 = CONJUNCT1 th3
3157 val th5 = CONJUNCT2 th3
3158 val th6 = MP th1 th4
3159 val th7 = MP th2 th5
3160 val th8 = CONJ th6 th7
3161 val th9 = itlist DISCH [tm1,tm2,tm3] th8
3162 val th10 = SPEC “^tm3 ==> ^tm4” (SPEC tm2 (SPEC tm1 AND_IMP_INTRO))
3163 in
3164 EQ_MP th10 th9
3165 end);
3166
3167(* ------------------------------------------------------------------------- *)
3168(* MONO_OR |- (x ==> y) /\ (z ==> w) ==> (x \/ z ==> y \/ w) *)
3169(* ------------------------------------------------------------------------- *)
3170
3171val MONO_OR = thm (#(FILE), #(LINE))("MONO_OR",
3172 let val tm1 = “x ==> y”
3173 val tm2 = “z ==> w”
3174 val tm3 = “x \/ z”
3175 val tm4 = “y \/ w”
3176 val th1 = ASSUME tm1
3177 val th2 = ASSUME tm2
3178 val th3 = ASSUME tm3
3179 val th4 = DISJ1 (MP th1 (ASSUME “x:bool”)) “w:bool”
3180 val th5 = DISJ2 “y:bool” (MP th2 (ASSUME “z:bool”))
3181 val th6 = DISJ_CASES th3 th4 th5
3182 val th7 = DISCH tm1 (DISCH tm2 (DISCH tm3 th6))
3183 val th8 = SPEC “^tm3 ==> ^tm4” (SPEC tm2 (SPEC tm1 AND_IMP_INTRO))
3184 in
3185 EQ_MP th8 th7
3186 end);
3187
3188(* ------------------------------------------------------------------------- *)
3189(* MONO_IMP |- (y ==> x) /\ (z ==> w) ==> ((x ==> z) ==> (y ==> w)) *)
3190(* ------------------------------------------------------------------------- *)
3191
3192val MONO_IMP = thm (#(FILE), #(LINE))("MONO_IMP",
3193 let val tm1 = “y ==> x”
3194 val tm2 = “z ==> w”
3195 val tm3 = “x ==> z”
3196 val tm4 = “y ==> w”
3197 val tm5 = “y:bool”
3198 val th1 = ASSUME tm1
3199 val th2 = ASSUME tm2
3200 val th3 = ASSUME tm3
3201 val th4 = MP th1 (ASSUME tm5)
3202 val th5 = MP th3 th4
3203 val th6 = MP th2 th5
3204 val th7 = DISCH tm1 (DISCH tm2 (DISCH tm3 (DISCH tm5 th6)))
3205 val th8 = SPEC “^tm3 ==> ^tm4” (SPEC tm2 (SPEC tm1 AND_IMP_INTRO))
3206 in
3207 EQ_MP th8 th7
3208 end);
3209
3210(* ------------------------------------------------------------------------- *)
3211(* MONO_NOT |- (y ==> x) ==> (~x ==> ~y) *)
3212(* ------------------------------------------------------------------------- *)
3213
3214val MONO_NOT = thm (#(FILE), #(LINE))("MONO_NOT",
3215 let val tm1 = “y ==> x”
3216 val tm2 = “~x”
3217 val tm3 = “y:bool”
3218 val th1 = ASSUME tm1
3219 val th2 = ASSUME tm2
3220 val th3 = ASSUME tm3
3221 val th4 = MP th1 th3
3222 val th5 = DISCH tm3 (MP th2 th4)
3223 val th6 = EQ_MP (SYM (RIGHT_BETA (AP_THM NOT_DEF tm3))) th5
3224 in
3225 DISCH tm1 (DISCH tm2 th6)
3226 end);
3227
3228(* ------------------------------------------------------------------------- *)
3229(* MONO_NOT_EQ |- (y ==> x) = (~x ==> ~y) *)
3230(* ------------------------------------------------------------------------- *)
3231
3232val MONO_NOT_EQ = thm (#(FILE), #(LINE))("MONO_NOT_EQ",
3233 let val tm1 = “x:bool”
3234 val tm2 = “y:bool”
3235 val th1 = INST [tm1 |-> mk_neg tm2, tm2 |-> mk_neg tm1] MONO_NOT
3236
3237 val th2 = SUBST [“x1:bool” |-> SPEC tm1 (CONJUNCT1 NOT_CLAUSES),
3238 “x2:bool” |-> SPEC tm2 (CONJUNCT1 NOT_CLAUSES)]
3239 “(~x ==> ~y) ==> (x2 ==> x1)” th1
3240
3241 val th3 = IMP_ANTISYM_RULE MONO_NOT th2
3242 in
3243 th3
3244 end);
3245
3246(* ------------------------------------------------------------------------- *)
3247(* MONO_ALL |- (!x. P x ==> Q x) ==> (!x. P x) ==> !x. Q x *)
3248(* ------------------------------------------------------------------------- *)
3249
3250val MONO_ALL = thm (#(FILE), #(LINE))("MONO_ALL",
3251 let val tm1 = “!x:'a. P x ==> Q x”
3252 val tm2 = “!x:'a. P x”
3253 val tm3 = “x:'a”
3254 val th1 = ASSUME tm1
3255 val th2 = ASSUME tm2
3256 val th3 = SPEC tm3 th1
3257 val th4 = SPEC tm3 th2
3258 val th5 = GEN tm3 (MP th3 th4)
3259 in
3260 DISCH tm1 (DISCH tm2 th5)
3261 end);
3262
3263(* ------------------------------------------------------------------------- *)
3264(* MONO_EXISTS = [] |- (!x. P x ==> Q x) ==> (?x. P x) ==> ?x. Q x *)
3265(* ------------------------------------------------------------------------- *)
3266
3267val MONO_EXISTS = thm (#(FILE), #(LINE))("MONO_EXISTS",
3268 let val tm1 = “!x:'a. P x ==> Q x”
3269 val tm2 = “?x:'a. P x”
3270 val tm3 = “@x:'a. P x”
3271 val tm4 = “\x:'a. P x:bool”
3272 val th1 = ASSUME tm1
3273 val th2 = ASSUME tm2
3274 val th3 = SPEC tm3 th1
3275 val th4 = RIGHT_BETA(RIGHT_BETA (AP_THM EXISTS_DEF tm4))
3276 val th5 = EQ_MP th4 th2
3277 val th6 = MP th3 th5
3278 in
3279 DISCH tm1 (DISCH tm2 (EXISTS (“?x:'a. Q x”, tm3) th6))
3280 end);
3281
3282(* ------------------------------------------------------------------------- *)
3283(* MONO_COND |- (x ==> y) ==> (z ==> w) *)
3284(* ==> (if b then x else z) ==> (if b then y else w) *)
3285(* ------------------------------------------------------------------------- *)
3286
3287val MONO_COND = thm (#(FILE), #(LINE))("MONO_COND",
3288 let val tm1 = “x ==> y”
3289 val tm2 = “z ==> w”
3290 val tm3 = “if b then x else z:bool”
3291 val tm4 = “b:bool”
3292 val tm5 = “x:bool”
3293 val tm6 = “z:bool”
3294 val tm7 = “y:bool”
3295 val tm8 = “w:bool”
3296 val th1 = ASSUME tm1
3297 val th2 = ASSUME tm2
3298 val th3 = ASSUME tm3
3299 val th4 = SPEC tm6 (SPEC tm5 (INST_TYPE [alpha |-> bool] COND_CLAUSES))
3300 val th5 = CONJUNCT1 th4
3301 val th6 = CONJUNCT2 th4
3302 val th7 = SPEC tm4 BOOL_CASES_AX
3303 val th8 = ASSUME “b = T”
3304 val th9 = ASSUME “b = F”
3305 val th10 = SUBST [tm4 |-> th8] (concl th3) th3
3306 val th11 = SUBST [tm4 |-> th9] (concl th3) th3
3307 val th12 = EQ_MP th5 th10
3308 val th13 = EQ_MP th6 th11
3309 val th14 = MP th1 th12
3310 val th15 = MP th2 th13
3311 val th16 = INST [tm5 |-> tm7, tm6 |-> tm8] th4
3312 val th17 = SYM (CONJUNCT1 th16)
3313 val th18 = SYM (CONJUNCT2 th16)
3314 val th19 = EQ_MP th17 th14
3315 val th20 = EQ_MP th18 th15
3316 val th21 = DISCH tm3 th19
3317 val th22 = DISCH tm3 th20
3318 val th23 = SUBST [tm4 |-> th8] (concl th21) th21
3319 val th24 = SUBST [tm4 |-> th9] (concl th22) th22
3320 val v = “v:bool”
3321 val T = mk_const("T",bool)
3322 val template = subst [T |-> v] (concl th23)
3323 val th25 = SUBST [v |-> SYM th8] template th23
3324 val th26 = SUBST [v |-> SYM th9] template th24
3325 in
3326 DISCH tm1 (DISCH tm2 (DISJ_CASES th7 th25 th26))
3327 end);
3328
3329(* ------------------------------------------------------------------------- *)
3330(* EXISTS_REFL |- !a. ?x. x = a *)
3331(* ------------------------------------------------------------------------- *)
3332
3333val EXISTS_REFL = thm (#(FILE), #(LINE))("EXISTS_REFL",
3334 let val a = “a:'a”
3335 val th1 = REFL a
3336 val th2 = EXISTS (“?x:'a. x = a”, a) th1
3337 in GEN a th2
3338 end);
3339
3340(* ------------------------------------------------------------------------- *)
3341(* EXISTS_UNIQUE_REFL |- !a. ?!x. x = a *)
3342(* ------------------------------------------------------------------------- *)
3343
3344val EXISTS_UNIQUE_REFL = thm (#(FILE), #(LINE))("EXISTS_UNIQUE_REFL",
3345 let val a = “a:'a”
3346 val P = “\x:'a. x = a”
3347 val tmx = “^P x”
3348 val tmy= “^P y”
3349 val ex = “?x. ^P x”
3350 val th1 = SPEC a EXISTS_REFL
3351 val th2 = ABS “x:'a” (BETA_CONV tmx)
3352 val th3 = AP_TERM “$? :('a->bool)->bool” th2
3353 val th4 = EQ_MP (SYM th3) th1
3354 val th5 = ASSUME (mk_conj(tmx,tmy))
3355 val th6 = CONJUNCT1 th5
3356 val th7 = CONJUNCT2 th5
3357 val th8 = EQ_MP (BETA_CONV (concl th6)) th6
3358 val th9 = EQ_MP (BETA_CONV (concl th7)) th7
3359 val th10 = TRANS th8 (SYM th9)
3360 val th11 = DISCH (hd(hyp th10)) th10
3361 val th12 = GEN “x:'a” (GEN “y:'a” th11)
3362 val th13 = INST [“P:'a->bool” |-> P] EXISTS_UNIQUE_THM
3363 val th14 = EQ_MP (SYM th13) (CONJ th4 th12)
3364 val th15 = AP_TERM “$?! :('a->bool)->bool” th2
3365 in
3366 GEN a (EQ_MP th15 th14)
3367 end);
3368
3369(* ----------------------------------------------------------------------
3370 EXISTS_UNIQUE_FALSE |- (?!x. F) <=> F
3371 ---------------------------------------------------------------------- *)
3372
3373val EXISTS_UNIQUE_FALSE = thm (#(FILE), #(LINE))("EXISTS_UNIQUE_FALSE",
3374 let
3375 val BINDER_CONV = RAND_CONV o ABS_CONV
3376 val LAND_CONV = RATOR_CONV o RAND_CONV
3377 val P = mk_var("P", alpha --> bool)
3378 val x = mk_var("x", alpha)
3379 val th1 = INST [P |-> mk_abs(x, F)] EXISTS_UNIQUE_THM
3380 val th2 = CONV_RULE(RAND_CONV (LAND_CONV (BINDER_CONV BETA_CONV))) th1
3381 val th3 = CONV_RULE(LAND_CONV (BINDER_CONV BETA_CONV)) th2
3382 val uniqueness_t = th3 |> concl |> rhs |> rand
3383 val simp1 = AP_THM (AP_TERM conjunction (SPEC F EXISTS_SIMP)) uniqueness_t
3384 val th4 = TRANS th3 simp1
3385 val simp2 = AND_CLAUSES |> SPEC uniqueness_t |> CONJUNCTS |> el 3
3386 in
3387 TRANS th4 simp2
3388 end);
3389
3390(* ------------------------------------------------------------------------- *)
3391(* Unwinding. *)
3392(* ------------------------------------------------------------------------- *)
3393
3394
3395(* ------------------------------------------------------------------------- *)
3396(* UNWIND1_THM |- !P a. (?x. (a = x) /\ P x) = P a *)
3397(* ------------------------------------------------------------------------- *)
3398
3399val UNWIND_THM1 = thm (#(FILE), #(LINE))("UNWIND_THM1",
3400 let val P = “P:'a->bool”
3401 val a = “a:'a”
3402 val Pa = “^P ^a”
3403 val v = “v:'a”
3404 val tm1 = “?x:'a. (a = x) /\ P x”
3405 val th1 = ASSUME tm1
3406 val th2 = ASSUME “(a:'a = v) /\ P v”
3407 val th3 = CONJUNCT1 th2
3408 val th4 = CONJUNCT2 th2
3409 val th5 = SUBST [v |-> SYM th3] (concl th4) th4
3410 val th6 = DISCH tm1 (CHOOSE (v,th1) th5)
3411 val th7 = ASSUME Pa
3412 val th8 = CONJ (REFL a) th7
3413 val th9 = EXISTS (tm1,a) th8
3414 val th10 = DISCH Pa th9
3415 val th11 = SPEC Pa (SPEC tm1 IMP_ANTISYM_AX)
3416 in
3417 GEN P (GEN a (MP (MP th11 th6) th10))
3418 end);
3419
3420
3421(* ------------------------------------------------------------------------- *)
3422(* UNWIND_THM2 |- !P a. (?x. (x = a) /\ P x) = P a *)
3423(* ------------------------------------------------------------------------- *)
3424
3425val UNWIND_THM2 = thm (#(FILE), #(LINE))("UNWIND_THM2",
3426 let val P = “P:'a->bool”
3427 val a = “a:'a”
3428 val Px = “^P x”
3429 val Pa = “^P ^a”
3430 val u = “u:'a”
3431 val v = “v:'a”
3432 val a_eq_x = “a:'a = x”
3433 val x_eq_a = “x:'a = a”
3434 val th1 = SPEC a (SPEC P UNWIND_THM1)
3435 val th2 = REFL Pa
3436 val th3 = DISCH a_eq_x (SYM (ASSUME a_eq_x))
3437 val th4 = DISCH x_eq_a (SYM (ASSUME x_eq_a))
3438 val th5 = SPEC a_eq_x (SPEC x_eq_a IMP_ANTISYM_AX)
3439 val th6 = MP (MP th5 th4) th3
3440 val th7 = MK_COMB (MK_COMB (REFL “$/\”, th6), REFL Px)
3441 val th8 = MK_COMB (REFL“$? :('a->bool)->bool”,
3442 ABS “x:'a” th7)
3443 val th9 = MK_COMB(MK_COMB (REFL“$= :bool->bool->bool”, th8),th2)
3444 val th10 = EQ_MP (SYM th9) th1
3445 in
3446 GEN P (GEN a th10)
3447 end);
3448
3449
3450(* ------------------------------------------------------------------------- *)
3451(* UNWIND_FORALL_THM1 |- !f v. (!x. (v = x) ==> f x) = f v *)
3452(* ------------------------------------------------------------------------- *)
3453
3454val UNWIND_FORALL_THM1 = thm (#(FILE), #(LINE))("UNWIND_FORALL_THM1",
3455 let val f = “f : 'a -> bool”
3456 val v = “v:'a”
3457 val fv = “^f ^v”
3458 val tm1 = “!x:'a. (v = x) ==> f x”
3459 val tm2 = “v:'a = x”
3460 val th1 = ASSUME tm1
3461 val th2 = ASSUME fv
3462 val th3 = DISCH tm1 (MP (SPEC v th1) (REFL v))
3463 val th4 = ASSUME tm2
3464 val th5 = SUBST [v |-> th4] (concl th2) th2
3465 val th6 = DISCH fv (GEN “x:'a” (DISCH tm2 th5))
3466 val th7 = MP (MP (SPEC tm1 (SPEC fv IMP_ANTISYM_AX)) th6) th3
3467 in
3468 GEN f (GEN v (SYM th7))
3469 end);
3470
3471
3472(* ------------------------------------------------------------------------- *)
3473(* UNWIND_FORALL_THM2 |- !f v. (!x. (x = v) ==> f x) = f v *)
3474(* ------------------------------------------------------------------------- *)
3475
3476val UNWIND_FORALL_THM2 = thm (#(FILE), #(LINE))("UNWIND_FORALL_THM2",
3477 let val f = “f:'a->bool”
3478 val v = “v:'a”
3479 val fv = “^f ^v”
3480 val tm1 = “!x:'a. (x = v) ==> f x”
3481 val tm2 = “x:'a = v”
3482 val th1 = ASSUME tm1
3483 val th2 = ASSUME fv
3484 val th3 = DISCH tm1 (MP (SPEC v th1) (REFL v))
3485 val th4 = ASSUME tm2
3486 val th5 = SUBST [v |-> SYM th4] (concl th2) th2
3487 val th6 = DISCH fv (GEN “x:'a” (DISCH tm2 th5))
3488 val th7 = MP (MP (SPEC tm1 (SPEC fv IMP_ANTISYM_AX)) th6) th3
3489 in
3490 GEN f (GEN v (SYM th7))
3491 end);
3492
3493
3494(* ------------------------------------------------------------------------- *)
3495(* Skolemization: |- !P. (!x. ?y. P x y) <=> ?f. !x. P x (f x) *)
3496(* ------------------------------------------------------------------------- *)
3497
3498val SKOLEM_THM = thm (#(FILE), #(LINE))("SKOLEM_THM",
3499 let val P = “P:'a -> 'b -> bool”
3500 val x = “x:'a”
3501 val y = “y:'b”
3502 val f = “f:'a->'b”
3503 val tm1 = “!x. ?y. ^P x y”
3504 val tm2 = “?f. !x. ^P x (f x)”
3505 val tm4 = “\x. @y. ^P x y”
3506 val tm5 = “(\x. @y. ^P x y) x”
3507 val th1 = ASSUME tm1
3508 val th2 = ASSUME tm2
3509 val th3 = SPEC x th1
3510 val th4 = INST_TYPE [alpha |-> beta] SELECT_AX
3511 val th5 = SPEC y (SPEC “\y. ^P x y” th4)
3512 val th6 = BETA_CONV (fst(dest_imp(concl th5)))
3513 val th7 = BETA_CONV (snd(dest_imp(concl th5)))
3514 val th8 = MK_COMB (MK_COMB (REFL “$==>”,th6),th7)
3515 val th9 = EQ_MP th8 th5
3516 val th10 = MP th9 (ASSUME(fst(dest_imp(concl th9))))
3517 val th11 = CHOOSE (y,th3) th10
3518 val th12 = SYM (BETA_CONV tm5)
3519 val th13 = SUBST [“v:'b” |-> th12] “^P x v” th11
3520 val th14 = DISCH tm1 (EXISTS (tm2,tm4) (GEN x th13))
3521 val th15 = ASSUME “!x. ^P x (f x)”
3522 val th16 = SPEC x th15
3523 val th17 = GEN x (EXISTS(“?y. ^P x y”,“f (x:'a):'b”) th16)
3524 val th18 = DISCH tm2 (CHOOSE (f,th2) th17)
3525 val th19 = MP (MP (SPEC tm1 (SPEC tm2 IMP_ANTISYM_AX)) th18) th14
3526 in
3527 GEN P (SYM th19)
3528 end);
3529
3530
3531(*---------------------------------------------------------------------------
3532 Support for pattern matching on booleans.
3533
3534 bool_case_thm =
3535 |- (!e0 e1. bool_case e0 e1 T = e0) /\
3536 !e0 e1. bool_case e0 e1 F = e1
3537 ---------------------------------------------------------------------------*)
3538
3539val bool_case_thm = let
3540 val (vs,_) = strip_forall (concl COND_CLAUSES)
3541in
3542 thm (#(FILE), #(LINE))("bool_case_thm",
3543 COND_CLAUSES |> SPECL vs |> CONJUNCTS |> map (GENL vs) |> LIST_CONJ)
3544end
3545
3546
3547(*---------------------------------------------------------------------------
3548 bool_case_eq =
3549 |- (bool_case t1 t2 x = v) <=>
3550 (x <=> T) /\ t1 = v \/ (x <=> F) /\ t2 = v
3551 ---------------------------------------------------------------------------*)
3552val bool_case_eq = thm (#(FILE), #(LINE))("bool_case_eq",
3553let val x = “x:bool”
3554 val t1 = “t1:'a”
3555 val t2 = “t2:'a”
3556 val v = “v:'a”
3557 val eq = “$=”
3558 val conj = “$/\”
3559 val disj = “$\/”
3560 val tm1 = “t1 = v”
3561 val tm2 = “t2 = v”
3562 val [COND1, COND2] = (CONJUNCTS (SPEC t2 (SPEC t1 COND_CLAUSES)))
3563 and [OR1,OR2,OR3,OR4,_] = map GEN_ALL (CONJUNCTS (SPEC_ALL OR_CLAUSES))
3564 and [AND1,AND2,AND3,AND4,_] = map GEN_ALL (CONJUNCTS(SPEC_ALL AND_CLAUSES))
3565 val thmT1 = AP_THM (AP_TERM eq COND1) v
3566 val thmF1 = AP_THM (AP_TERM eq COND2) v
3567 val [TF,FT] = map EQF_INTRO (CONJUNCTS BOOL_EQ_DISTINCT)
3568 val [TT,FF] = map (EQT_INTRO o REFL) [“T”,“F”]
3569 val thmT2 =
3570 let
3571 val thml1 = AP_THM (AP_TERM conj TT) tm1
3572 val thml2 = SPEC tm1 AND1
3573 val thml = TRANS thml1 thml2
3574 val thmr1 = AP_THM (AP_TERM conj TF) tm2
3575 val thmr2 = SPEC tm2 AND3
3576 val thmr = TRANS thmr1 thmr2
3577 val thm1 = MK_COMB (AP_TERM disj thml, thmr)
3578 in
3579 TRANS thm1 (SPEC tm1 OR4)
3580 end
3581 val thmF2 =
3582 let
3583 val thmr1 = AP_THM (AP_TERM conj FF) tm2
3584 val thmr2 = SPEC tm2 AND1
3585 val thmr = TRANS thmr1 thmr2
3586 val thml1 = AP_THM (AP_TERM conj FT) tm1
3587 val thml2 = SPEC tm1 AND3
3588 val thml = TRANS thml1 thml2
3589 val thm1 = MK_COMB (AP_TERM disj thml, thmr)
3590 in
3591 TRANS thm1 (SPEC tm2 OR3)
3592 end
3593 val thmT3 = TRANS thmT1 (SYM thmT2)
3594 val thmF3 = TRANS thmF1 (SYM thmF2)
3595 val tm = “(if x then t1 else t2) = v <=> (((x <=> T) /\ t1 = v) \/ ((x <=> F) /\ t2 = v))”
3596 val thT4 = SUBST_CONV [x |-> ASSUME “x = T”] tm tm
3597 and thF4 = SUBST_CONV [x |-> ASSUME “x = F”] tm tm
3598 val thmT = EQ_MP (SYM thT4) thmT3
3599 val thmF = EQ_MP (SYM thF4) thmF3
3600 in
3601 DISJ_CASES (SPEC x BOOL_CASES_AX) thmT thmF
3602 end);
3603
3604(* ------------------------------------------------------------------------- *)
3605(* bool_case_ID = |- !x. (x => T | F) = x *)
3606(* ------------------------------------------------------------------------- *)
3607val bool_case_ID = thm (#(FILE), #(LINE))("bool_case_ID",
3608let val x = “x:bool”
3609 val (CONDT,CONDF) = INST_TYPE [alpha |-> bool] COND_CLAUSES
3610 |> SPECL [T,F]
3611 |> CONJ_PAIR
3612 val tm = “(if x then T else F) = x”
3613 val thT1 = SUBST_CONV [x |-> ASSUME “x = T”] tm tm
3614 val thF1 = SUBST_CONV [x |-> ASSUME “x = F”] tm tm
3615 val thmT = EQ_MP (SYM thT1) CONDT
3616 val thmF = EQ_MP (SYM thF1) CONDF
3617in
3618 GEN x (DISJ_CASES (SPEC x BOOL_CASES_AX) thmT thmF)
3619end);
3620(* ------------------------------------------------------------------------- *)
3621(* bool_case_CONST = |- !x b. bool_case x x b = x *)
3622(* ------------------------------------------------------------------------- *)
3623
3624val bool_case_CONST = thm (#(FILE), #(LINE))("bool_case_CONST", COND_ID)
3625
3626
3627(* ------------------------------------------------------------------------- *)
3628(* boolAxiom |- !e0 e1. ?fn. (fn T = e0) /\ (fn F = e1) *)
3629(* ------------------------------------------------------------------------- *)
3630
3631val boolAxiom = thm (#(FILE), #(LINE))("boolAxiom",
3632 let
3633 val ([e0,e1], _) = strip_forall (concl COND_CLAUSES)
3634 val (th2, th3) = CONJ_PAIR (SPECL [e0, e1] COND_CLAUSES)
3635 val f_t = “\b. if b then ^e0 else ^e1”
3636 val f_T = TRANS (BETA_CONV (mk_comb(f_t, T))) th2
3637 val f_F = TRANS (BETA_CONV (mk_comb(f_t, F))) th3
3638 val th4 = CONJ f_T f_F
3639 val th5 = EXISTS (“?fn. (fn T = ^e0) /\ (fn F = ^e1)”, f_t) th4
3640 in
3641 GEN e0 (GEN e1 th5)
3642 end);
3643
3644(* ------------------------------------------------------------------------- *)
3645(* bool_INDUCT |- !P. P T /\ P F ==> !b. P b *)
3646(* ------------------------------------------------------------------------- *)
3647
3648val bool_INDUCT = thm (#(FILE), #(LINE))("bool_INDUCT",
3649 let val P = “P:bool -> bool”
3650 val b = “b:bool”
3651 val v = “v:bool”
3652 val tm1 = “^P T /\ ^P F”
3653 val th1 = SPEC b BOOL_CASES_AX
3654 val th2 = ASSUME tm1
3655 val th3 = CONJUNCT1 th2
3656 val th4 = CONJUNCT2 th2
3657 val th5 = ASSUME “b = T”
3658 val th6 = ASSUME “b = F”
3659 val th7 = SUBST [v |-> SYM th5] “^P ^v” th3
3660 val th8 = SUBST [v |-> SYM th6] “^P ^v” th4
3661 val th9 = GEN b (DISJ_CASES th1 th7 th8)
3662 in
3663 GEN P (DISCH tm1 th9)
3664 end);
3665
3666(* ---------------------------------------------------------------------------
3667 |- !P Q x x' y y'.
3668 (P = Q) /\ (Q ==> (x = x')) /\ (~Q ==> (y = y')) ==>
3669 ((case P of T -> x || F -> y) = (case Q of T -> x' || F -> y'))
3670 --------------------------------------------------------------------------- *)
3671
3672val bool_case_CONG = thm (#(FILE), #(LINE))("bool_case_CONG", COND_CONG)
3673
3674val FORALL_BOOL = thm (#(FILE), #(LINE))
3675("FORALL_BOOL",
3676 let val tm1 = “!b:bool. P b”
3677 val tm2 = “P T /\ P F”
3678 val th1 = ASSUME tm1
3679 val th2 = CONJ (SPEC T th1) (SPEC F th1)
3680 val th3 = DISCH tm1 th2
3681 val th4 = ASSUME tm2
3682 val th5 = MP (SPEC “P:bool->bool” bool_INDUCT) th4
3683 val th6 = DISCH tm2 th5
3684 in
3685 IMP_ANTISYM_RULE th3 th6
3686 end);
3687
3688
3689(*---------------------------------------------------------------------------
3690 Results about Unique existence.
3691 ---------------------------------------------------------------------------*)
3692
3693local
3694 val LAND_CONV = RATOR_CONV o RAND_CONV
3695 val P = mk_var("P", Type.alpha --> Type.bool)
3696 val p = mk_var("p", Type.bool)
3697 val q = mk_var("q", Type.bool)
3698 val Q = mk_var("Q", Type.alpha --> Type.bool)
3699 val x = mk_var("x", Type.alpha)
3700 val y = mk_var("y", Type.alpha)
3701 val Px = mk_comb(P, x)
3702 val Py = mk_comb(P, y)
3703 val Qx = mk_comb(Q, x)
3704 val Qy = mk_comb(Q, y)
3705 val uex_t = mk_const("?!", (alpha --> bool) --> bool)
3706 val exP = mk_exists(x, Px)
3707 val exQ = mk_exists(x, Qx)
3708 val uexP = mk_exists1(x, Px)
3709 val uexQ = mk_exists1(x, Qx)
3710 val pseudo_mp = let
3711 val lhs_t = mk_conj(p, mk_imp(p, q))
3712 val rhs_t = mk_conj(p, q)
3713 val lhs_thm = ASSUME lhs_t
3714 val (p_thm, pimpq) = CONJ_PAIR lhs_thm
3715 val dir1 = DISCH_ALL (CONJ p_thm (MP pimpq p_thm))
3716 val rhs_thm = ASSUME rhs_t
3717 val (p_thm, q_thm) = CONJ_PAIR rhs_thm
3718 val dir2 = DISCH_ALL (CONJ p_thm (DISCH p q_thm))
3719 in
3720 IMP_ANTISYM_RULE dir1 dir2
3721 end
3722in
3723 val UEXISTS_OR_THM = let
3724 val subdisj_t = mk_abs(x, mk_disj(Px, Qx))
3725 val lhs_t = mk_comb(uex_t, subdisj_t)
3726 val lhs_thm = ASSUME lhs_t
3727 val lhs_eq = AP_THM EXISTS_UNIQUE_DEF subdisj_t
3728 val lhs_expanded = CONV_RULE BETA_CONV (EQ_MP lhs_eq lhs_thm)
3729 val (expq0, univ) = CONJ_PAIR lhs_expanded
3730 val expq = EQ_MP (SPEC_ALL EXISTS_OR_THM) expq0
3731 val univ1 = SPEC_ALL univ
3732 val univ2 = CONV_RULE (LAND_CONV (LAND_CONV BETA_CONV)) univ1
3733 val univ3 = CONV_RULE (LAND_CONV (RAND_CONV BETA_CONV)) univ2
3734 val P_half = let
3735 val asm = ASSUME (mk_conj(Px,Py))
3736 val (Px_thm, Py_thm) = CONJ_PAIR asm
3737 val PxQx_thm = DISJ1 Px_thm Qx
3738 val PyQy_thm = DISJ1 Py_thm Qy
3739 val resolvent = CONJ PxQx_thm PyQy_thm
3740 val rhs =
3741 GENL [x,y]
3742 (DISCH (mk_conj(Px,Py)) (PROVE_HYP resolvent (UNDISCH univ3)))
3743 in
3744 DISJ1 (EQ_MP (SYM EXISTS_UNIQUE_THM) (CONJ (ASSUME exP) rhs)) uexQ
3745 end
3746 val Q_half = let
3747 val asm = ASSUME (mk_conj(Qx,Qy))
3748 val (Qx_thm, Qy_thm) = CONJ_PAIR asm
3749 val PxQx_thm = DISJ2 Px Qx_thm
3750 val PyQy_thm = DISJ2 Py Qy_thm
3751 val resolvent = CONJ PxQx_thm PyQy_thm
3752 val rhs =
3753 GENL [x,y]
3754 (DISCH (mk_conj(Qx,Qy)) (PROVE_HYP resolvent (UNDISCH univ3)))
3755 val uex_expanded = SYM (INST [P |-> Q] EXISTS_UNIQUE_THM)
3756 in
3757 DISJ2 uexP (EQ_MP uex_expanded (CONJ (ASSUME exQ) rhs))
3758 end
3759 in
3760 thm (#(FILE), #(LINE))(
3761 "UEXISTS_OR_THM",
3762 GENL [P, Q] (DISCH_ALL (DISJ_CASES expq P_half Q_half))
3763 )
3764 end;
3765
3766 val UEXISTS_SIMP = let
3767 fun mCONV_RULE c thm = TRANS thm (c (rhs (concl thm)))
3768 val xeqy = mk_eq(x,y)
3769 val t = mk_var("t", bool)
3770 val abst = mk_abs(x, t)
3771 val uext_t = mk_exists1(x,t)
3772 val exp0 = AP_THM EXISTS_UNIQUE_DEF abst
3773 val exp1 = mCONV_RULE BETA_CONV exp0
3774 val exp2 = mCONV_RULE (LAND_CONV (K (SPEC t EXISTS_SIMP))) exp1
3775 val exp3 =
3776 mCONV_RULE (RAND_CONV
3777 (QUANT_CONV
3778 (QUANT_CONV (LAND_CONV (LAND_CONV BETA_CONV))))) exp2
3779 val exp4 =
3780 mCONV_RULE (RAND_CONV
3781 (QUANT_CONV
3782 (QUANT_CONV (LAND_CONV (RAND_CONV BETA_CONV))))) exp3
3783 val exp5 =
3784 mCONV_RULE (RAND_CONV
3785 (QUANT_CONV
3786 (QUANT_CONV (LAND_CONV (K (SPEC t AND_CLAUSE5)))))) exp4
3787 val pushy0 =
3788 SPECL [t, mk_abs(y,xeqy)]
3789 RIGHT_FORALL_IMP_THM
3790 val pushy1 =
3791 CONV_RULE (LAND_CONV (QUANT_CONV (RAND_CONV BETA_CONV))) pushy0
3792 val pushy2 =
3793 CONV_RULE (RAND_CONV (RAND_CONV (QUANT_CONV BETA_CONV))) pushy1
3794 val exp6 =
3795 mCONV_RULE (RAND_CONV (QUANT_CONV (K pushy2))) exp5
3796 val pushx0 = SPECL [t, mk_abs(x, mk_forall(y,xeqy))]
3797 RIGHT_FORALL_IMP_THM
3798 val pushx1 =
3799 CONV_RULE (LAND_CONV (QUANT_CONV (RAND_CONV BETA_CONV))) pushx0
3800 val pushx2 =
3801 CONV_RULE (RAND_CONV (RAND_CONV (QUANT_CONV BETA_CONV))) pushx1
3802 val exp7 =
3803 mCONV_RULE (RAND_CONV (K pushx2)) exp6
3804 val mp' = Thm.INST [p |-> t, q |-> list_mk_forall [x,y] xeqy] pseudo_mp
3805 in
3806 thm (#(FILE), #(LINE))("UEXISTS_SIMP", mCONV_RULE (K mp') exp7)
3807 end
3808end
3809
3810
3811(*---------------------------------------------------------------------------
3812 The definition of restricted abstraction.
3813 ---------------------------------------------------------------------------*)
3814
3815val RES_ABSTRACT_EXISTS =
3816 let
3817 fun B_CONV n = funpow n RATOR_CONV BETA_CONV
3818 fun RHS th = rhs (concl th)
3819 val p = “p : 'a -> bool”
3820 val m = “m : 'a -> 'b”
3821 val m1 = “m1 : 'a -> 'b”
3822 val m2 = “m2 : 'a -> 'b”
3823 val x = “x : 'a”
3824 val witness = “\p m x. if x IN p then ^m x else ARB x”
3825 val A1 = B_CONV 2 “^witness ^p ^m ^x”
3826 val A2 = TRANS A1 (B_CONV 1 (RHS A1))
3827 val A3 = TRANS A2 (BETA_CONV (RHS A2))
3828 val A4 = EQT_INTRO (ASSUME “^x IN ^p”)
3829 val A5 = RATOR_CONV (RATOR_CONV (RAND_CONV (K A4))) (RHS A3)
3830 val A6 = INST_TYPE [alpha |-> beta] COND_CLAUSE1
3831 val A7 = SPECL [“^m ^x”, “ARB ^x : 'b”] A6
3832 val A8 = DISCH “^x IN ^p” (TRANS (TRANS A3 A5) A7)
3833 val A9 = GENL [“^p”, “^m”, “^x”] A8
3834 (* Completed the first clause of the definition *)
3835 val B1 = SPEC “^x IN ^p” EXCLUDED_MIDDLE
3836 val B2 = UNDISCH A8
3837 val B3 = INST [m |-> m1] B2
3838 val B4 = INST [m |-> m2] B2
3839 val B5 = SPEC_ALL (ASSUME “!x. x IN ^p ==> (^m1 x = ^m2 x)”)
3840 val B6 = TRANS B3 (TRANS (UNDISCH B5) (SYM B4))
3841 val B7 = INST [m |-> m1] A3
3842 val B8 = INST [m |-> m2] A3
3843 val B9 = SYM (SPEC “^x IN ^p” EQ_CLAUSE4)
3844 val B10 = EQ_MP B9 (ASSUME “~(^x IN ^p)”)
3845 val B11 = INST_TYPE [alpha |-> beta] COND_CLAUSE2
3846 val B12 = RATOR_CONV (RATOR_CONV (RAND_CONV (K B10))) (RHS B7)
3847 val B13 = TRANS B12 (SPECL [“^m1 ^x”, “ARB ^x : 'b”] B11)
3848 val B14 = RATOR_CONV (RATOR_CONV (RAND_CONV (K B10))) (RHS B8)
3849 val B15 = TRANS B14 (SPECL [“^m2 ^x”, “ARB ^x : 'b”] B11)
3850 val B16 = TRANS (TRANS B7 B13) (SYM (TRANS B8 B15))
3851 val B17 = DISJ_CASES B1 B6 B16
3852 val B18 = ABS x B17
3853 val B19 = CONV_RULE (RATOR_CONV (RAND_CONV ETA_CONV)) B18
3854 val B20 = CONV_RULE (RAND_CONV ETA_CONV) B19
3855 val B21 = DISCH “!x. x IN ^p ==> (^m1 x = ^m2 x)” B20
3856 val B22 = GENL [p, m1, m2] B21
3857 (* Cleaning up *)
3858 val C1 = CONJ A9 B22
3859 val C2 = EXISTS
3860 (“?f.
3861 (!p (m : 'a -> 'b) x. x IN p ==> (f p m x = m x)) /\
3862 (!p m1 m2.
3863 (!x. x IN p ==> (m1 x = m2 x)) ==> (f p m1 = f p m2))”,
3864 “\p (m : 'a -> 'b) x. (if x IN p then m x else ARB x)”) C1
3865 in
3866 C2
3867 end;
3868
3869val RES_ABSTRACT_DEF =
3870 Definition.new_specification
3871 ("RES_ABSTRACT_DEF", ["RES_ABSTRACT"], RES_ABSTRACT_EXISTS);
3872
3873val _ = associate_restriction ("\\", "RES_ABSTRACT");
3874
3875
3876val (RES_FORALL_THM, RES_EXISTS_THM, RES_EXISTS_UNIQUE_THM, RES_SELECT_THM) =
3877 let
3878 val Pf = map (fn s => mk_var(s, alpha --> bool)) ["P", "f"]
3879 fun mk_eq th =
3880 GENL Pf (List.foldl (RIGHT_BETA o uncurry (C AP_THM)) th Pf)
3881 in
3882 (thm (#(FILE), #(LINE))("RES_FORALL_THM", mk_eq RES_FORALL_DEF),
3883 thm (#(FILE), #(LINE))("RES_EXISTS_THM", mk_eq RES_EXISTS_DEF),
3884 thm (#(FILE), #(LINE))("RES_EXISTS_UNIQUE_THM",
3885 mk_eq RES_EXISTS_UNIQUE_DEF),
3886 thm (#(FILE), #(LINE))("RES_SELECT_THM", mk_eq RES_SELECT_DEF))
3887 end
3888
3889
3890(* (!x::P. T) = T *)
3891val RES_FORALL_TRUE = let
3892 val x = mk_var("x", alpha)
3893 val T = concl TRUTH
3894 val KT = mk_abs(x, T)
3895 val P = mk_var("P", alpha --> bool)
3896 val th0 = SPECL[P,KT] RES_FORALL_THM
3897 val th1 = CONV_RULE (RAND_CONV (QUANT_CONV (RAND_CONV BETA_CONV))) th0
3898 val xINP_t = (rand o rator o #2 o dest_forall o rhs o concl) th1
3899 val timpT_th = List.nth(CONJUNCTS (SPEC xINP_t IMP_CLAUSES), 1)
3900 val th2 = CONV_RULE (RAND_CONV (QUANT_CONV (K timpT_th))) th1
3901in
3902 thm (#(FILE), #(LINE))("RES_FORALL_TRUE", TRANS th2 (SPEC T FORALL_SIMP))
3903end
3904
3905(* (?x::P. F) = F *)
3906val RES_EXISTS_FALSE = let
3907 val x = mk_var("x", alpha)
3908 val F = prim_mk_const{Thy = "bool", Name = "F"}
3909 val KF = mk_abs(x, F)
3910 val P = mk_var("P", alpha --> bool)
3911 val th0 = SPECL [P, KF] RES_EXISTS_THM
3912 val th1 = CONV_RULE (RAND_CONV (QUANT_CONV (RAND_CONV BETA_CONV))) th0
3913 val xINP_t = (rand o rator o #2 o dest_exists o rhs o concl) th1
3914 val tandF_th = List.nth(CONJUNCTS (SPEC xINP_t AND_CLAUSES), 3)
3915 val th2 = CONV_RULE (RAND_CONV (QUANT_CONV (K tandF_th))) th1
3916in
3917 thm (#(FILE), #(LINE))("RES_EXISTS_FALSE", TRANS th2 (SPEC F EXISTS_SIMP))
3918end
3919
3920(*---------------------------------------------------------------------------
3921 From Joe Hurd : case analysis on the (4) functions in the
3922 type :bool -> bool.
3923
3924 val BOOL_FUN_CASES_THM =
3925 |- !f. (f = \b. T) \/ (f = \b. F) \/ (f = \b. b) \/ (f = \b. ~b)
3926 ---------------------------------------------------------------------------*)
3927
3928val BOOL_FUN_CASES_THM =
3929 let val x = mk_var("x",bool)
3930 val f = mk_var("f",bool-->bool)
3931 val KF = “\b:bool.F”
3932 val KT = “\b:bool.T”
3933 val Ibool = “\b:bool.b”
3934 val dual = “\b. ~b”
3935 val fT = mk_comb(f,T)
3936 val fF = mk_comb(f,F)
3937 val fT_eq_T = mk_eq(fT,T)
3938 val fF_eq_T = mk_eq(fF,T)
3939 val fT_eq_F = mk_eq(fT,F)
3940 val fF_eq_F = mk_eq(fF,F)
3941 val final = “(f = ^KT) \/ (f = ^KF) \/ (f = ^Ibool) \/ (f = ^dual)”
3942 val a0 = TRANS (ASSUME fT_eq_T) (SYM (BETA_CONV (mk_comb(KT,T))))
3943 val a1 = TRANS (ASSUME fF_eq_T) (SYM (BETA_CONV (mk_comb(KT,F))))
3944 val a2 = BOOL_CASE “f x = ^KT x” x x a0 a1
3945 val a3 = EXT (GEN x a2)
3946 val a = DISJ1 a3 “(f = \b. F) \/ (f = \b. b) \/ (f = \b. ~b)”
3947 val b0 = TRANS (ASSUME fT_eq_F) (SYM (BETA_CONV (mk_comb(KF,T))))
3948 val b1 = TRANS (ASSUME fF_eq_F) (SYM (BETA_CONV (mk_comb(KF,F))))
3949 val b2 = BOOL_CASE “f x = ^KF x” x x b0 b1
3950 val b3 = EXT (GEN x b2)
3951 val b4 = DISJ1 b3 “(f = ^Ibool) \/ (f = \b. ~b)”
3952 val b = DISJ2 “f = ^KT” b4
3953 val c0 = TRANS (ASSUME fT_eq_T) (SYM (BETA_CONV (mk_comb(Ibool,T))))
3954 val c1 = TRANS (ASSUME fF_eq_F) (SYM (BETA_CONV (mk_comb(Ibool,F))))
3955 val c2 = BOOL_CASE “f x = ^Ibool x” x x c0 c1
3956 val c3 = EXT (GEN x c2)
3957 val c4 = DISJ1 c3 “f = ^dual”
3958 val c5 = DISJ2 “f = ^KF” c4
3959 val c = DISJ2 “f = ^KT” c5
3960 val d0 = TRANS (ASSUME fT_eq_F)
3961 (TRANS (SYM (CONJUNCT1 (CONJUNCT2 NOT_CLAUSES)))
3962 (SYM (BETA_CONV (mk_comb(dual,T)))))
3963 val d1 = TRANS (ASSUME fF_eq_T)
3964 (TRANS (SYM (CONJUNCT2 (CONJUNCT2 NOT_CLAUSES)))
3965 (SYM (BETA_CONV (mk_comb(dual,F)))))
3966 val d2 = BOOL_CASE “f x = ^dual x” x x d0 d1
3967 val d3 = EXT (GEN x d2)
3968 val d4 = DISJ2 “f = ^Ibool” d3
3969 val d5 = DISJ2 “f = ^KF” d4
3970 val d = DISJ2 “f = ^KT” d5
3971 val ad0 = DISCH fT_eq_T a
3972 val ad1 = DISCH fT_eq_F d
3973 val ad2 = BOOL_CASE “(f T = x) ==> ^final” x x ad0 ad1
3974 val ad3 = SPEC fT (GEN x ad2)
3975 val ad = MP ad3 (REFL fT)
3976 val bc0 = DISCH fT_eq_T c
3977 val bc1 = DISCH fT_eq_F b
3978 val bc2 = BOOL_CASE “(f T = x) ==> ^final” x x bc0 bc1
3979 val bc3 = SPEC fT (GEN x bc2)
3980 val bc = MP bc3 (REFL fT)
3981 val abcd0 = DISCH fF_eq_T ad
3982 val abcd1 = DISCH fF_eq_F bc
3983 val abcd2 = BOOL_CASE “(f F = x) ==> ^final” x x abcd0 abcd1
3984 val abcd3 = SPEC fF (GEN x abcd2)
3985 val abcd = MP abcd3 (REFL fF)
3986in
3987 thm (#(FILE), #(LINE))("BOOL_FUN_CASES_THM", GEN f abcd)
3988end;
3989
3990(*---------------------------------------------------------------------------
3991 Another from Joe Hurd : consequence of BOOL_FUN_CASES_THM
3992
3993 BOOL_FUN_INDUCT =
3994 |- !P. P (\b. T) /\ P (\b. F) /\ P (\b. b) /\ P (\b. ~b) ==> !f. P f
3995 ---------------------------------------------------------------------------*)
3996
3997 fun or_imp th0 =
3998 let val (disj1, disj2) = dest_disj (concl th0)
3999 val th1 = SYM (SPEC disj1 (CONJUNCT1 NOT_CLAUSES))
4000 val th2 = MK_COMB (REFL disjunction, th1)
4001 val th3 = MK_COMB (th2, REFL disj2)
4002 val th4 = EQ_MP th3 th0
4003 val th5 = SYM (SPECL [mk_neg disj1, disj2] IMP_DISJ_THM)
4004 in
4005 EQ_MP th5 th4
4006 end
4007
4008 fun imp_and th0 =
4009 let val (ant, conseq) = dest_imp (concl th0)
4010 val (ant', conseq') = dest_imp conseq
4011 val th1 = SPECL [ant, ant', conseq'] AND_IMP_INTRO
4012 in
4013 EQ_MP th1 th0
4014 end
4015
4016
4017val BOOL_FUN_INDUCT =
4018 let val f = mk_var("f",bool-->bool)
4019 val g = mk_var("g",bool-->bool)
4020 val f_eq_g = mk_eq(f,g)
4021 val P = mk_var("P",(bool-->bool) --> bool)
4022 val KF = “\b:bool.F”
4023 val KT = “\b:bool.T”
4024 val Ibool = “\b:bool.b”
4025 val dual = “\b. ~b”
4026 val f0 = ASSUME (mk_neg(mk_comb(P,f)))
4027 val f1 = ASSUME (mk_neg(mk_neg(f_eq_g)))
4028 val f2 = EQ_MP (SPEC f_eq_g (CONJUNCT1 NOT_CLAUSES)) f1
4029 val f3 = MK_COMB (REFL P, f2)
4030 val f4 = MK_COMB (REFL negation, f3)
4031 val f5 = UNDISCH (NOT_ELIM (EQ_MP f4 f0))
4032 val f6 = CCONTR (mk_neg(f_eq_g)) f5
4033 val f7 = GEN g (DISCH (mk_comb(P,g)) f6)
4034 val a0 = SPEC f BOOL_FUN_CASES_THM
4035 val a1 = MP (or_imp a0) (UNDISCH (SPEC KT f7))
4036 val a2 = MP (or_imp a1) (UNDISCH (SPEC KF f7))
4037 val a3 = MP (or_imp a2) (UNDISCH (SPEC Ibool f7))
4038 val a = MP (NOT_ELIM (UNDISCH (SPEC dual f7))) a3
4039 val b0 = CCONTR (mk_comb(P,f)) a
4040 val b1 = GEN f b0
4041 val b2 = DISCH (mk_comb(P,dual)) b1
4042 val b3 = imp_and (DISCH (mk_comb(P,Ibool)) b2)
4043 val b4 = imp_and (DISCH (mk_comb(P,KF)) b3)
4044 val b = imp_and (DISCH (mk_comb(P,KT)) b4)
4045in
4046 thm (#(FILE), #(LINE))("BOOL_FUN_INDUCT", GEN P b)
4047end;
4048
4049(*---------------------------------------------------------------------------
4050 literal_case_THM = |- !f x. literal_case f x = f x
4051 ---------------------------------------------------------------------------*)
4052
4053val literal_case_THM = thm (#(FILE), #(LINE))("literal_case_THM",
4054 let val f = “f:'a->'b”
4055 val x = “x:'a”
4056 in
4057 GEN f (GEN x
4058 (RIGHT_BETA(AP_THM (RIGHT_BETA(AP_THM literal_case_DEF f)) x)))
4059 end);
4060
4061(*---------------------------------------------------------------------------*)
4062(* literal_case_RAND = *)
4063(* |- P (literal_case (\x. N x) M) = (literal_case (\x. P (N x)) M) *)
4064(*---------------------------------------------------------------------------*)
4065
4066val literal_case_RAND = thm (#(FILE), #(LINE))("literal_case_RAND",
4067 let val tm1 = “\x:'a. P (N x:'b):'c”
4068 val tm2 = “M:'a”
4069 val tm3 = “\x:'a. N x:'b”
4070 val P = “P:'b ->'c”
4071 val literal_case_THM1 = RIGHT_BETA (SPEC tm2 (SPEC tm1
4072 (Thm.INST_TYPE [beta |-> gamma] literal_case_THM)))
4073 val literal_case_THM2 = AP_TERM P (RIGHT_BETA (SPEC tm2 (SPEC tm3 literal_case_THM)))
4074 in TRANS literal_case_THM2 (SYM literal_case_THM1)
4075 end);
4076
4077(*---------------------------------------------------------------------------*)
4078(* literal_case_RATOR = *)
4079(* |- (literal_case (\x. N x) M) b = (literal_case (\x. N x b) M) *)
4080(*---------------------------------------------------------------------------*)
4081
4082val literal_case_RATOR = thm (#(FILE), #(LINE))("literal_case_RATOR",
4083 let val M = “M:'a”
4084 val b = “b:'b”
4085 val tm1 = “\x:'a. N x:'b->'c”
4086 val tm2 = “\x:'a. N x ^b:'c”
4087 val literal_case_THM1 = AP_THM (RIGHT_BETA (SPEC M (SPEC tm1
4088 (Thm.INST_TYPE [beta |-> (beta --> gamma)] literal_case_THM)))) b
4089 val literal_case_THM2 = RIGHT_BETA (SPEC M (SPEC tm2
4090 (Thm.INST_TYPE [beta |-> gamma] literal_case_THM)))
4091 in TRANS literal_case_THM1 (SYM literal_case_THM2)
4092 end);
4093
4094(*---------------------------------------------------------------------------
4095 literal_case_CONG =
4096 |- !f g M N. (M = N) /\ (!x. (x = N) ==> (f x = g x))
4097 ==>
4098 (literal_case f M = literal_case g N)
4099 ---------------------------------------------------------------------------*)
4100
4101val literal_case_CONG = thm (#(FILE), #(LINE))("literal_case_CONG",
4102 let val f = mk_var("f",alpha-->beta)
4103 val g = mk_var("g",alpha-->beta)
4104 val M = mk_var("M",alpha)
4105 val N = mk_var("N",alpha)
4106 val x = mk_var ("x",alpha)
4107 val MeqN = mk_eq(M,N)
4108 val x_eq_N = mk_eq(x,N)
4109 val fx_eq_gx = mk_eq(mk_comb(f,x),mk_comb(g,x))
4110 val ctm = mk_forall(x, mk_imp(x_eq_N,fx_eq_gx))
4111 val th = RIGHT_BETA(AP_THM(RIGHT_BETA(AP_THM literal_case_DEF f)) M)
4112 val th1 = ASSUME MeqN
4113 val th2 = MP (SPEC N (ASSUME ctm)) (REFL N)
4114 val th3 = SUBS [SYM th1] th2
4115 val th4 = TRANS (TRANS th th3) (MK_COMB (REFL g,th1))
4116 val th5 = RIGHT_BETA(AP_THM(RIGHT_BETA(AP_THM literal_case_DEF g)) N)
4117 val th6 = TRANS th4 (SYM th5)
4118 val th7 = SUBS [SPECL [MeqN, ctm, concl th6] AND_IMP_INTRO]
4119 (DISCH MeqN (DISCH ctm th6))
4120 in
4121 GENL [f,g,M,N] th7
4122 end);
4123
4124(*---------------------------------------------------------------------------*)
4125(* Sometime useful rewrite, but you will want a higher-order version. *)
4126(* |- literal_case (\x. bool_case t u (x=a)) a = t *)
4127(*---------------------------------------------------------------------------*)
4128
4129val literal_case_id = thm (#(FILE), #(LINE))
4130("literal_case_id",
4131 let val a = mk_var("a", alpha)
4132 val x = mk_var("x", alpha)
4133 val t = mk_var("t",beta)
4134 val u = mk_var("u",beta)
4135 val eq = mk_eq(x,a)
4136 val bcase = inst [alpha |-> beta]
4137 (prim_mk_const{Name = "COND",Thy="bool"})
4138 val g = mk_abs(x,list_mk_comb(bcase,[eq, t, u]))
4139 val lit_thm = RIGHT_BETA(SPEC a (SPEC g literal_case_THM))
4140 val Teq = SYM (EQT_INTRO(REFL a))
4141 val ifT = CONJUNCT1(SPECL[t,u] (INST_TYPE[alpha |-> beta] COND_CLAUSES))
4142 val ifeq = SUBS [Teq] ifT
4143 in
4144 TRANS lit_thm ifeq
4145 end);
4146
4147(*---------------------------------------------------------------------------
4148 Support for parsing "case" expressions
4149 ---------------------------------------------------------------------------*)
4150
4151val _ = new_constant(GrammarSpecials.core_case_special,
4152 “:'a -> ('a -> 'b) -> 'b”);
4153val _ = new_constant(GrammarSpecials.case_split_special,
4154 “:('a -> 'b) -> ('a -> 'b) -> 'a -> 'b”);
4155val _ = new_constant(GrammarSpecials.case_arrow_special,
4156 “:'a -> 'b -> 'a -> 'b”);
4157
4158val _ = app (fn s => remove_ovl_mapping s {Name=s,Thy="bool"})
4159 [GrammarSpecials.case_split_special,
4160 GrammarSpecials.case_arrow_special]
4161
4162val _ = add_rule{pp_elements = [HardSpace 1, TOK "=>", BreakSpace(1,2)],
4163 fixity = Infix(NONASSOC, 12),
4164 (* allowing for insertion of .| infix at looser precedence
4165 level *)
4166 block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)),
4167 paren_style = OnlyIfNecessary,
4168 term_name = GrammarSpecials.case_arrow_special}
4169
4170val _ = add_rule{pp_elements = [PPBlock([TOK "case", BreakSpace(1,2),
4171 TM, BreakSpace(1,2), TOK "of"],
4172 (PP.CONSISTENT, 0)),
4173 BreakSpace(1,2)],
4174 fixity = Prefix 1,
4175 block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)),
4176 paren_style = Always,
4177 term_name = GrammarSpecials.core_case_special};
4178
4179val _ = add_rule{pp_elements = [PPBlock([TOK "case", BreakSpace(1,2),
4180 TM, BreakSpace(1,2), TOK "of"],
4181 (PP.CONSISTENT, 0)),
4182 BreakSpace(1,2), TM, BreakSpace(1,0),
4183 TOK "|", HardSpace 1],
4184 fixity = Prefix 1,
4185 block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)),
4186 paren_style = Always,
4187 term_name = GrammarSpecials.core_case_special};
4188
4189val _ = add_rule{pp_elements = [PPBlock([TOK "case", BreakSpace(1,2),
4190 TM, BreakSpace(1,2), TOK "of"],
4191 (PP.CONSISTENT, 0)),
4192 TOK "|", HardSpace 1],
4193 fixity = Prefix 1,
4194 block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)),
4195 paren_style = Always,
4196 term_name = GrammarSpecials.core_case_special};
4197
4198
4199val _ = add_rule{pp_elements = [PPBlock([TOK "case", BreakSpace(1,2),
4200 TM, BreakSpace(1,2), TOK "of"],
4201 (PP.CONSISTENT, 0)),
4202 BreakSpace(1,2), TM, BreakSpace(1,0),
4203 TOK "|", HardSpace 1, TM, BreakSpace(1,0),
4204 TOK "|", HardSpace 1],
4205 fixity = Prefix 1,
4206 block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)),
4207 paren_style = Always,
4208 term_name = GrammarSpecials.core_case_special};
4209
4210val BOUNDED_THM = thm (#(FILE), #(LINE))("BOUNDED_THM",
4211 let val v = “v:bool”
4212 in
4213 GEN v (RIGHT_BETA(AP_THM BOUNDED_DEF v))
4214 end);
4215
4216(*---------------------------------------------------------------------------*)
4217(* LCOMM_THM : derive "left-commutativity" from associativity and *)
4218(* commutativity. Used in permutative rewriting, e.g., simpLib entrypoints *)
4219(* *)
4220(* LCOMM_THM |- !f. (!x y. f x y = f y x) ==> *)
4221(* (!x y z. f x (f y z) = f (f x y) z) ==> *)
4222(* (!x y z. f x (f y z) = f y (f x z)) *)
4223(*---------------------------------------------------------------------------*)
4224
4225val LCOMM_THM = thm (#(FILE), #(LINE))("LCOMM_THM",
4226 let val x = mk_var("x",alpha)
4227 val y = mk_var("y",alpha)
4228 val z = mk_var("z",alpha)
4229 val f = mk_var("f",alpha --> alpha --> alpha)
4230 val comm = “!x y. ^f x y = f y x”
4231 val assoc = “!x y z. ^f x (f y z) = f (f x y) z”
4232 val comm_thm = ASSUME comm
4233 val assoc_thm = ASSUME assoc
4234 val th0 = SPEC (list_mk_comb(f,[y,z])) (SPEC x comm_thm)
4235 val th1 = SYM (SPECL [y,z,x] assoc_thm)
4236 val th2 = TRANS th0 th1
4237 val th3 = AP_TERM (mk_comb(f,y)) (SPECL[z,x] comm_thm)
4238 in
4239 GEN f (DISCH assoc (DISCH comm (GENL [x,y,z] (TRANS th2 th3))))
4240 end);
4241
4242
4243val DATATYPE_TAG_THM = thm (#(FILE), #(LINE))("DATATYPE_TAG_THM",
4244 let val x = mk_var("x",alpha)
4245 in GEN x (RIGHT_BETA (AP_THM DATATYPE_TAG_DEF x))
4246 end);
4247
4248
4249val DATATYPE_BOOL = thm (#(FILE), #(LINE))("DATATYPE_BOOL",
4250 let val thm1 = INST_TYPE [alpha |-> bool] DATATYPE_TAG_THM
4251 val bvar = mk_var("bool",bool--> bool-->bool)
4252 in
4253 SPEC (list_mk_comb(bvar,[T,F])) thm1
4254 end);
4255
4256(* ----------------------------------------------------------------------
4257 Set up the "itself" type constructor and its one value
4258 ---------------------------------------------------------------------- *)
4259
4260val ITSELF_TYPE_DEF = let
4261 val itself_exists = SPEC “ARB:'a” EXISTS_REFL
4262 val eq_sym_eq' =
4263 AP_TERM “$? :('a -> bool) -> bool”
4264 (ABS “x:'a” (SPECL [“x:'a”, “ARB:'a”] EQ_SYM_EQ))
4265in
4266 new_type_definition("itself", EQ_MP eq_sym_eq' itself_exists)
4267end
4268val _ = new_constant("the_value", “:'a itself”)
4269
4270(* prove uniqueness of the itself value:
4271 |- !i:'a itself. i = (:'a)
4272*)
4273val ITSELF_UNIQUE = let
4274 val typedef_asm = ASSUME (#2 (dest_exists (concl ITSELF_TYPE_DEF)))
4275 val typedef_eq0 =
4276 AP_THM (INST_TYPE [beta |-> “:'a itself”] TYPE_DEFINITION)
4277 “$= (ARB:'a)”
4278 val typedef_eq0 = RIGHT_BETA typedef_eq0
4279 val typedef_eq = AP_THM typedef_eq0 “rep:'a itself -> 'a”
4280 val typedef_eq = RIGHT_BETA typedef_eq
4281 val (typedef_11, typedef_onto) = CONJ_PAIR (EQ_MP typedef_eq typedef_asm)
4282 val onto' = INST [“x:'a” |-> “(rep:'a itself -> 'a) i”]
4283 (#2 (EQ_IMP_RULE (SPEC_ALL typedef_onto)))
4284 val allreps_arb = let
4285 val ex' = EXISTS (“?x':'a itself. rep i = rep x':'a”, “i:'a itself”)
4286 (REFL “(rep:'a itself -> 'a) i”)
4287 in
4288 SYM (MP onto' ex')
4289 end
4290 val allreps_repthevalue =
4291 TRANS allreps_arb
4292 (SYM (INST [“i:'a itself” |-> “bool$the_value”] allreps_arb))
4293 val all_eq_thevalue =
4294 GEN_ALL (MP (SPECL [“i:'a itself”, “bool$the_value”] typedef_11)
4295 allreps_repthevalue)
4296in
4297 thm (#(FILE), #(LINE))("ITSELF_UNIQUE",
4298 CHOOSE (“rep:'a itself -> 'a”, ITSELF_TYPE_DEF) all_eq_thevalue)
4299end
4300
4301(* ITSELF_EQN_RWT = |- f (:'a) = e <=> !x. f x = e *)
4302val ITSELF_EQN_RWT = let
4303 fun mk_itty ty = mk_thy_type{Args = [ty], Thy = "bool", Tyop = "itself"}
4304 val aitty = mk_itty alpha
4305 val f = mk_var("f", aitty --> beta)
4306 val e = mk_var("e", beta)
4307 val x = mk_var("x", aitty)
4308 val r = mk_forall(x, mk_eq(mk_comb(f,x), e))
4309 val itv = mk_thy_const{Name = "the_value", Thy = "bool", Ty = aitty}
4310 val l = mk_eq(mk_comb(f,itv), e)
4311 val r2l = SPEC itv (ASSUME r) |> DISCH r
4312 val l2r = SPEC x ITSELF_UNIQUE |> AP_TERM f |> C TRANS (ASSUME l) |> GEN x
4313 |> DISCH l
4314in
4315 thm (#(FILE), #(LINE))(
4316 "ITSELF_EQN_RWT",
4317 GENL [f,e] $ IMP_ANTISYM_RULE l2r r2l
4318 )
4319end
4320
4321(* prove a datatype axiom for the type, allowing definitions of the form
4322 f (:'a) = ...
4323*)
4324val itself_Axiom = let
4325 val witness = “(\x:'a itself. e : 'b)”
4326 val fn_behaves = BETA_CONV (mk_comb(witness, “(:'a)”))
4327 val fn_exists = EXISTS (“?f:'a itself -> 'b. f (:'a) = e”, witness)
4328 fn_behaves
4329in
4330 thm (#(FILE), #(LINE))("itself_Axiom", GEN_ALL fn_exists)
4331end
4332
4333(* prove induction *)
4334val itself_induction = let
4335 val pval = ASSUME “P (:'a) : bool”
4336 val pi =
4337 EQ_MP (SYM (AP_TERM “P:'a itself -> bool” (SPEC_ALL ITSELF_UNIQUE)))
4338 pval
4339in
4340 thm (#(FILE), #(LINE))("itself_induction", GEN_ALL (DISCH_ALL (GEN_ALL pi)))
4341end
4342
4343(* define case operator *)
4344val itself_case_thm = let
4345 val witness = “λ(i:'a itself) (b:'b). b”
4346 val witness_applied1 = BETA_CONV (mk_comb(witness, “(:'a)”))
4347 val witness_applied2 = RIGHT_BETA (AP_THM witness_applied1 “b:'b”)
4348in
4349 located_new_specification{
4350 name = "itself_case_thm",
4351 constnames = ["itself_case"],
4352 witness = EXISTS (“?f:'a itself -> 'b -> 'b. !b. f (:'a) b = b”, witness)
4353 (GEN_ALL witness_applied2),
4354 loc = mkloc(#(FILE), #(LINE)-5)
4355 }
4356end
4357Overload case = “itself_case”
4358
4359(* FORALL_itself : |- (!x:'a itself. P x) <=> P (:'a)
4360 EXISTS_itself : |- (?x:'a itself. P x) <=> P (:'a)
4361*)
4362local
4363 val P = mk_var("P", “:'a itself -> bool”)
4364 val x = mk_var("x", “:'a itself”)
4365 val Px = mk_comb(P, x)
4366 val APx = mk_forall(x, Px)
4367 val itself = “(:'a)”
4368 val Pitself = mk_comb(P, itself)
4369 val imp1 = APx |> ASSUME |> SPEC itself |> DISCH_ALL
4370 val unique = AP_TERM P (ITSELF_UNIQUE |> SPEC x |> SYM)
4371 val imp2 = EQ_MP unique (ASSUME Pitself) |> GEN x |> DISCH_ALL
4372 val fa = IMP_ANTISYM_RULE imp1 imp2
4373 val not_not = NOT_CLAUSES |> CONJUNCT1 |> SPEC Px
4374 (* exists half *)
4375 val imp1 = CHOOSE (x, ASSUME (mk_exists(x,Px)))
4376 (EQ_MP (SYM unique) (ASSUME Px)) |> DISCH_ALL
4377 val imp2 = EXISTS(mk_exists(x,Px),itself) (ASSUME Pitself) |> DISCH_ALL
4378in
4379 val FORALL_itself = thm (#(FILE), #(LINE))("FORALL_itself", fa)
4380 val EXISTS_itself = thm (#(FILE), #(LINE))
4381 ("EXISTS_itself", IMP_ANTISYM_RULE imp1 imp2)
4382end;
4383
4384
4385(*---------------------------------------------------------------------------*)
4386(* Pulling FORALL and EXISTS up through /\ and ==> *)
4387(*---------------------------------------------------------------------------*)
4388
4389local
4390 val flip = INST [Pb |-> Qb, Qab |-> Pab]
4391 val PULL_EXISTS1 = LEFT_FORALL_IMP_THM |> SPEC_ALL |> SYM
4392 val PULL_EXISTS2 = LEFT_EXISTS_AND_THM |> SPEC_ALL |> SYM
4393 val PULL_EXISTS3 = RIGHT_EXISTS_AND_THM |> SPEC_ALL |> SYM |> flip
4394 val PULL_FORALL1 = RIGHT_FORALL_IMP_THM |> SPEC_ALL |> SYM |> flip
4395 val PULL_FORALL2 = LEFT_AND_FORALL_THM |> SPEC_ALL
4396 val PULL_FORALL3 = RIGHT_AND_FORALL_THM |> SPEC_ALL |> flip
4397in
4398 val PULL_EXISTS = thm (#(FILE), #(LINE))("PULL_EXISTS",
4399 LIST_CONJ [PULL_EXISTS1, PULL_EXISTS2, PULL_EXISTS3] |> GENL [Pab, Qb])
4400 val PULL_FORALL = thm (#(FILE), #(LINE))("PULL_FORALL",
4401 LIST_CONJ [PULL_FORALL1, PULL_FORALL2, PULL_FORALL3] |> GENL [Pab, Qb])
4402end
4403
4404(*---------------------------------------------------------------------------*)
4405(* PEIRCE = |- ((P ==> Q) ==> P) ==> P *)
4406(*---------------------------------------------------------------------------*)
4407
4408val PEIRCE = thm (#(FILE), #(LINE))
4409("PEIRCE",
4410 let val th1 = ASSUME “(P ==> Q) ==> P”
4411 val th2 = ASSUME “P:bool”
4412 val th3 = ASSUME “~P”
4413 val th4 = MP th3 th2
4414 val th5 = MP (SPEC “Q:bool” FALSITY) th4
4415 val th6 = DISCH “P:bool” th5
4416 val th7 = MP th1 th6
4417 val th8 = MP th3 th7
4418 val th9 = DISCH “~P” th8
4419 val th10 = MP (SPEC “~P” IMP_F) th9
4420 val th11 = SUBS [SPEC “P:bool” (CONJUNCT1 NOT_CLAUSES)] th10
4421 in
4422 DISCH “(P ==> Q) ==> P” th11
4423 end);
4424
4425(* ----------------------------------------------------------------------
4426 JRH_INDUCT_UTIL : !P t. (!x. (x = t) ==> P x) ==> $? P
4427
4428 Used multiple times in places relevant to inductive definitions and/or
4429 algebraic types.
4430 ---------------------------------------------------------------------- *)
4431
4432val JRH_INDUCT_UTIL = let
4433 val asm_t = “!x:'a. (x = t) ==> P x”
4434 val asm = ASSUME asm_t
4435 val t = “t:'a”
4436 val P = “P : 'a -> bool”
4437 val Pt = MP (SPEC t asm) (REFL t)
4438 val ExPx = EXISTS (“?x:'a. P x”, t) Pt
4439 val P_eta = SPEC P (INST_TYPE [beta |-> bool] ETA_AX)
4440 val ExP_eta = AP_TERM “(?) : ('a -> bool) -> bool” P_eta
4441in
4442 thm (#(FILE), #(LINE))("JRH_INDUCT_UTIL",
4443 GENL [P, t] (DISCH asm_t (EQ_MP ExP_eta ExPx)))
4444end
4445
4446(* Parsing additions *)
4447(* not an element of *)
4448Overload NOTIN = “\x:'a y:('a -> bool). ~(x IN y)”
4449val _ = set_fixity "NOTIN" (Infix(NONASSOC, 425))
4450val _ = unicode_version {u = UChar.not_elementof, tmnm = "NOTIN"}
4451val _ = TeX_notation {hol="NOTIN", TeX = ("\\HOLTokenNotIn{}",1)}
4452val _ = TeX_notation {hol=UChar.not_elementof,
4453 TeX = ("\\HOLTokenNotIn{}",1)}
4454
4455(* not iff *)
4456Overload "<=/=>" = “$<> : bool -> bool -> bool”
4457val _ = set_fixity "<=/=>" (Infix(NONASSOC, 100))
4458val _ = unicode_version {u = UChar.not_iff, tmnm = "<=/=>"}
4459val _ = TeX_notation {hol="<=/=>", TeX = ("\\HOLTokenNotEquiv{}",3)}
4460val _ = TeX_notation {hol=UChar.not_iff,
4461 TeX = ("\\HOLTokenNotEquiv{}",3)}
4462
4463val _ = add_ML_dependency "boolpp"
4464val _ = add_user_printer ("bool.COND", “COND gd tr fl”)
4465val _ = add_user_printer ("bool.LET", “LET f x”)
4466val _ = add_absyn_postprocessor "bool.LET"
4467
4468(* |- |- !A B. A \/ B <=> ~A ==> B *)
4469val DISJ_EQ_IMP = thm (#(FILE), #(LINE))("DISJ_EQ_IMP",
4470 let
4471 val lemma = NOT_CLAUSES |> CONJUNCT1 |> SPEC ``A:bool``
4472 in
4473 IMP_DISJ_THM
4474 |> SPECL [``~A:bool``,``B:bool``]
4475 |> SYM
4476 |> CONV_RULE
4477 ((RATOR_CONV o RAND_CONV o RATOR_CONV o RAND_CONV)
4478 (fn tm => lemma))
4479 |> GENL [``A:bool``,``B:bool``]
4480 end);
4481
4482(* ------------------------------------------------------------------------- *)
4483(* CONTRAPOS_THM |- !t1 t2. (~t1 ==> ~t2) <=> (t2 ==> t1) *)
4484(* (HOL-Light compatible) *)
4485(* ------------------------------------------------------------------------- *)
4486
4487val CONTRAPOS_THM = thm (#(FILE), #(LINE)) ("CONTRAPOS_THM",
4488 MONO_NOT_EQ |> SYM
4489 |> INST [“x:bool” |-> “t1:bool”, “y:bool” |-> “t2:bool”]
4490 |> GENL [“t1:bool”, “t2:bool”]);