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
2579(* ---------------------------------------------------------------------*)
2580(* COND_BOOL_CLAUSES *)
2581(* *)
2582(* |- (!b e. (if b then T else e) = (b \/ e)) /\ *)
2583(* (!b t. (if b then t else T) = (b ==> t)) /\ *)
2584(* (!b e. (if b then F else e) = (~b /\ e)) /\ *)
2585(* (!b t. (if b then t else F) = (b /\ t)) *)
2586(* *)
2587(* Each conjunct is one of the COND_EXPAND family with a T or an F for *)
2588(* one of the arms, tidied up with the relevant *_CLAUSES. *)
2589(* ---------------------------------------------------------------------*)
2590
2591val COND_BOOL_CLAUSES = thm (#(FILE), #(LINE))("COND_BOOL_CLAUSES",
2592let val b = “b:bool”
2593 val e = “e:bool”
2594 val t = “t:bool”
2595 val [AND1,AND2,_,AND4,_] = map GEN_ALL (CONJUNCTS (SPEC_ALL AND_CLAUSES))
2596 and [_,OR2,OR3,OR4,_] = map GEN_ALL (CONJUNCTS (SPEC_ALL OR_CLAUSES))
2597 and [_,IMP2,_,_,_] = map GEN_ALL (CONJUNCTS (SPEC_ALL IMP_CLAUSES))
2598 val cnj1 =
2599 let val th = SUBS [SPEC (mk_neg b) OR2] (SPECL [b,“T”,e] COND_EXPAND)
2600 in GENL [b,e] (SUBS [SPEC (mk_disj(b,e)) AND1] th)
2601 end
2602 val cnj2 =
2603 let val th = SUBS [SPEC (mk_neg b) IMP2]
2604 (SPECL [b,t,“T”] COND_EXPAND_IMP)
2605 in GENL [b,t] (SUBS [SPEC (mk_imp(b,t)) AND2] th)
2606 end
2607 val cnj3 =
2608 let val th = SUBS [SPEC b AND4] (SPECL [b,“F”,e] COND_EXPAND_OR)
2609 in GENL [b,e] (SUBS [SPEC (mk_conj(mk_neg b,e)) OR3] th)
2610 end
2611 val cnj4 =
2612 let val th = SUBS [SPEC (mk_neg b) AND4] (SPECL [b,t,“F”] COND_EXPAND_OR)
2613 in GENL [b,t] (SUBS [SPEC (mk_conj(b,t)) OR4] th)
2614 end
2615in
2616 CONJ cnj1 (CONJ cnj2 (CONJ cnj3 cnj4))
2617end);
2618
2619(* ---------------------------------------------------------------------*)
2620(* IF_THEN_T_IMP *)
2621(* *)
2622(* |- !b e. (if b then T else e) = (~b ==> e) *)
2623(* ---------------------------------------------------------------------*)
2624
2625val IF_THEN_T_IMP = thm (#(FILE), #(LINE))("IF_THEN_T_IMP",
2626let val b = “b:bool”
2627 val e = “e:bool”
2628 val AND1 = GEN_ALL (CONJUNCT1 (SPEC_ALL AND_CLAUSES))
2629 val IMP2 = GEN_ALL (el 2 (CONJUNCTS (SPEC_ALL IMP_CLAUSES)))
2630 val th = SUBS [SPEC b IMP2] (SPECL [b,“T”,e] COND_EXPAND_IMP)
2631in
2632 GENL [b,e] (SUBS [SPEC (mk_imp(mk_neg b,e)) AND1] th)
2633end);
2634
2635val TYPE_DEFINITION_THM = thm (#(FILE), #(LINE))("TYPE_DEFINITION_THM",
2636 let val P = “P:'a-> bool”
2637 val rep = “rep :'b -> 'a”
2638 in
2639 GEN P (GEN rep
2640 (RIGHT_BETA(AP_THM
2641 (RIGHT_BETA (AP_THM TYPE_DEFINITION P)) rep)))
2642 end);
2643
2644val ONTO_THM = thm (#(FILE), #(LINE))(
2645 "ONTO_THM",
2646 let val f = mk_var("f", Type.alpha --> Type.beta)
2647 in
2648 GEN f (RIGHT_BETA (AP_THM ONTO_DEF f))
2649 end);
2650
2651val ONE_ONE_THM = thm (#(FILE), #(LINE))(
2652 "ONE_ONE_THM",
2653 let val f = mk_var("f", Type.alpha --> Type.beta)
2654 in
2655 GEN f (RIGHT_BETA (AP_THM ONE_ONE_DEF f))
2656 end);
2657
2658(*---------------------------------------------------------------------------*
2659 * ABS_REP_THM *
2660 * |- !P. (?rep. TYPE_DEFINITION P rep) ==> *
2661 * ?rep abs. (!a. abs (rep a) = a) /\ !r. P r = (rep (abs r) = r) *
2662 *---------------------------------------------------------------------------*)
2663
2664val ABS_REP_THM = thm (#(FILE), #(LINE))("ABS_REP_THM",
2665 let val th1 = ASSUME “?rep:'b->'a. TYPE_DEFINITION P rep”
2666 val th2 = MK_EXISTS (SPEC “P:'a->bool” TYPE_DEFINITION_THM)
2667 val def = EQ_MP th2 th1
2668 val asm = ASSUME (snd(dest_exists(concl def)))
2669 val (asm1,asm2) = CONJ_PAIR asm
2670 val rep_eq =
2671 let val th1 = DISCH “a:'b=a'”
2672 (AP_TERM “rep:'b->'a” (ASSUME “a:'b=a'”))
2673 in IMP_ANTISYM_RULE (SPECL [“a:'b”,“a':'b”] asm1) th1
2674 end
2675 val ABS = “\r:'a. @a:'b. r = rep a”
2676 val absd = RIGHT_BETA (AP_THM (REFL ABS) “rep (a:'b):'a”)
2677 val lem = SYM(SELECT_RULE(EXISTS (“?a':'b.a=a'”,“a:'b”)
2678 (REFL “a:'b”)))
2679 val TH1 = GEN “a:'b”
2680 (TRANS(TRANS absd (SELECT_EQ “a':'b” rep_eq)) lem)
2681 val t1 = SELECT_RULE(EQ_MP (SPEC “r:'a” asm2)
2682 (ASSUME “(P:'a->bool) r”))
2683 val absd2 = RIGHT_BETA (AP_THM (REFL ABS) “r:'a”)
2684 val v = mk_var("v",type_of(rhs (concl absd2)))
2685 val (t1l,t1r) = dest_eq (concl t1)
2686 (* val rep = fst(strip_comb t1r) *)
2687 val rep = rator t1r
2688 val template = mk_eq(t1l, mk_comb(rep,v))
2689 val imp1 = DISCH “(P:'a->bool) r”
2690 (SYM (SUBST [v |-> SYM absd2] template t1))
2691 val t2 = EXISTS (“?a:'b. r:'a = rep a”, “^ABS r”)
2692 (SYM(ASSUME “rep(^ABS (r:'a):'b) = r”))
2693 val imp2 = DISCH “rep(^ABS (r:'a):'b) = r”
2694 (EQ_MP (SYM (SPEC “r:'a” asm2)) t2)
2695 val TH2 = GEN “r:'a” (IMP_ANTISYM_RULE imp1 imp2)
2696 val CTH = CONJ TH1 TH2
2697 val ath = subst [ABS |-> “abs:'a->'b”] (concl CTH)
2698 val eth1 = EXISTS (“?abs:'a->'b. ^ath”, ABS) CTH
2699 val eth2 = EXISTS (“?rep:'b->'a. ^(concl eth1)”,
2700 “rep:'b->'a”) eth1
2701 val result = DISCH (concl th1) (CHOOSE (“rep:'b->'a”,def) eth2)
2702 in
2703 GEN “P:'a->bool” result
2704 end);
2705
2706(*---------------------------------------------------------------------------
2707 LET_RAND = P (let x = M in N x) = (let x = M in P (N x))
2708 ---------------------------------------------------------------------------*)
2709
2710val LET_RAND = thm (#(FILE), #(LINE))("LET_RAND",
2711 let val tm1 = “\x:'a. P (N x:'b):bool”
2712 val tm2 = “M:'a”
2713 val tm3 = “\x:'a. N x:'b”
2714 val P = “P:'b -> bool”
2715 val LET_THM1 = RIGHT_BETA (SPEC tm2 (SPEC tm1
2716 (Thm.INST_TYPE [beta |-> bool] LET_THM)))
2717 val LET_THM2 = AP_TERM P (RIGHT_BETA (SPEC tm2 (SPEC tm3 LET_THM)))
2718 in TRANS LET_THM2 (SYM LET_THM1)
2719 end);
2720
2721
2722(*---------------------------------------------------------------------------
2723 LET_RATOR = (let x = M in N x) b = (let x = M in N x b)
2724 ---------------------------------------------------------------------------*)
2725
2726val LET_RATOR = thm (#(FILE), #(LINE))("LET_RATOR",
2727 let val M = “M:'a”
2728 val b = “b:'b”
2729 val tm1 = “\x:'a. N x:'b->'c”
2730 val tm2 = “\x:'a. N x ^b:'c”
2731 val LET_THM1 = AP_THM (RIGHT_BETA (SPEC M (SPEC tm1
2732 (Thm.INST_TYPE [beta |-> (beta --> gamma)] LET_THM)))) b
2733 val LET_THM2 = RIGHT_BETA (SPEC M (SPEC tm2
2734 (Thm.INST_TYPE [beta |-> gamma] LET_THM)))
2735 in TRANS LET_THM1 (SYM LET_THM2)
2736 end);
2737
2738
2739(*---------------------------------------------------------------------------
2740 !P. (!x y. P x y) = (!y x. P x y)
2741 ---------------------------------------------------------------------------*)
2742
2743val SWAP_FORALL_THM = thm (#(FILE), #(LINE))("SWAP_FORALL_THM",
2744 let val P = mk_var("P", “:'a->'b->bool”)
2745 val x = mk_var("x", Type.alpha)
2746 val y = mk_var("y", Type.beta)
2747 val Pxy = list_mk_comb (P,[x,y])
2748 val th1 = ASSUME (list_mk_forall [x,y] Pxy)
2749 val th2 = DISCH_ALL (GEN y (GEN x (SPEC y (SPEC x th1))))
2750 val th3 = ASSUME (list_mk_forall [y,x] Pxy)
2751 val th4 = DISCH_ALL (GEN x (GEN y (SPEC x (SPEC y th3))))
2752 in
2753 GEN P (IMP_ANTISYM_RULE th2 th4)
2754 end);
2755
2756(*---------------------------------------------------------------------------
2757 !P. (?x y. P x y) = (?y x. P x y)
2758 ---------------------------------------------------------------------------*)
2759
2760val SWAP_EXISTS_THM = thm (#(FILE), #(LINE))("SWAP_EXISTS_THM",
2761 let val P = mk_var("P", “:'a->'b->bool”)
2762 val x = mk_var("x", Type.alpha)
2763 val y = mk_var("y", Type.beta)
2764 val Pxy = list_mk_comb (P,[x,y])
2765 val tm1 = list_mk_exists[x] Pxy
2766 val tm2 = list_mk_exists[y] tm1
2767 val tm3 = list_mk_exists[y] Pxy
2768 val tm4 = list_mk_exists[x] tm3
2769 val th1 = ASSUME Pxy
2770 val th2 = EXISTS(tm2,y) (EXISTS (tm1,x) th1)
2771 val th3 = ASSUME (list_mk_exists [y] Pxy)
2772 val th4 = CHOOSE(y,th3) th2
2773 val th5 = CHOOSE(x,ASSUME (list_mk_exists [x,y] Pxy)) th4
2774 val th6 = EXISTS(tm4,x) (EXISTS (tm3,y) th1)
2775 val th7 = ASSUME (list_mk_exists[x] Pxy)
2776 val th8 = CHOOSE(x,th7) th6
2777 val th9 = CHOOSE(y,ASSUME (list_mk_exists [y,x] Pxy)) th8
2778 in
2779 GEN P (IMP_ANTISYM_RULE (DISCH_ALL th5) (DISCH_ALL th9))
2780 end);
2781
2782(*---------------------------------------------------------------------------
2783 EXISTS_UNIQUE_THM
2784
2785 (?!x. P x) = (?x. P x) /\ (!x y. P x /\ P y ==> (x = y))
2786 ---------------------------------------------------------------------------*)
2787
2788val EXISTS_UNIQUE_THM = thm (#(FILE), #(LINE))("EXISTS_UNIQUE_THM",
2789 let val th1 = RIGHT_BETA (AP_THM EXISTS_UNIQUE_DEF “\x:'a. P x:bool”)
2790 val th2 = CONV_RULE (RAND_CONV (RAND_CONV
2791 (QUANT_CONV (QUANT_CONV (RATOR_CONV
2792 (RAND_CONV (RAND_CONV BETA_CONV))))))) th1
2793 in
2794 CONV_RULE (RAND_CONV (RAND_CONV (QUANT_CONV (QUANT_CONV (RATOR_CONV
2795 (RAND_CONV (RATOR_CONV (RAND_CONV BETA_CONV)))))))) th2
2796 end);
2797
2798(* ----------------------------------------------------------------------
2799 EXISTS_UNIQUE_ALT'
2800
2801 |- !P. (?!x. P x) <=> ?x. !y. P y <=> (y = x)
2802 ---------------------------------------------------------------------- *)
2803
2804val EXISTS_UNIQUE_ALT' = thm (#(FILE), #(LINE))(
2805 "EXISTS_UNIQUE_ALT'",
2806 let
2807 val eu_r = ASSUME (rhs (concl EXISTS_UNIQUE_THM))
2808 val (eu1, eu2) = CONJ_PAIR eu_r
2809 val P = mk_var("P", alpha --> bool)
2810 val x = mk_var("x", alpha)
2811 val y = mk_var("y", alpha)
2812 val c = mk_var("c", alpha)
2813 val yeqx = mk_eq(y,x)
2814 val Px = mk_comb(P, x)
2815 val Py = mk_comb(P, y)
2816 val th1a = MP (SPECL [y,x] eu2) (CONJ (ASSUME Py) (ASSUME Px)) |> DISCH Py
2817 val th1b = EQ_MP (SYM (AP_TERM P (ASSUME yeqx))) (ASSUME Px) |> DISCH yeqx
2818 val th1_noex = IMP_ANTISYM_RULE th1a th1b |> GEN y
2819 val th1_noch = EXISTS(mk_exists(x,concl th1_noex), x) th1_noex
2820 val th1 = CHOOSE(x,eu1) th1_noch
2821 val pyyeq = concl th1
2822 val pyyeqc = subst [x |-> c] (#2 (dest_exists pyyeq))
2823 val pyyeqc_th = ASSUME pyyeqc
2824 val th2a = pyyeqc_th |> SPEC c |> C EQ_MP (REFL c) o SYM
2825 |> EXISTS(mk_exists(x,Px), c)
2826 val (pxy_x,pxy_y) = ASSUME (mk_conj(Px,Py)) |> CONJ_PAIR
2827 val th2b1 = pyyeqc_th |> SPEC x |> C EQ_MP (ASSUME Px) |> PROVE_HYP pxy_x
2828 val th2b2 = pyyeqc_th |> SPEC y |> C EQ_MP (ASSUME Py) |> PROVE_HYP pxy_y
2829 val th2b = TRANS th2b1 (SYM th2b2) |> DISCH (mk_conj(Px,Py)) |> GENL [x,y]
2830 val th2 = CHOOSE (c, ASSUME pyyeq) (CONJ th2a th2b)
2831 val eqn = IMP_ANTISYM_RULE (DISCH_ALL th1) (DISCH_ALL th2)
2832 in
2833 TRANS EXISTS_UNIQUE_THM eqn
2834 end);
2835
2836(* ----------------------------------------------------------------------
2837 EXISTS_UNIQUE_ALT
2838
2839 |- !P. (?!x. P x) <=> ?x. !y. P y <=> (x = y)
2840
2841 EXISTS_UNIQUE_ALT' with the witness equation the other way round.
2842 ---------------------------------------------------------------------- *)
2843
2844val EXISTS_UNIQUE_ALT = thm (#(FILE), #(LINE))(
2845 "EXISTS_UNIQUE_ALT",
2846 let
2847 val P = mk_var("P", alpha --> bool)
2848 val x = mk_var("x", alpha)
2849 val y = mk_var("y", alpha)
2850 val Py = mk_comb(P,y)
2851 val body = AP_TERM (rator (mk_eq(Py,Py))) (SPECL [y,x] EQ_SYM_EQ)
2852 val inner = AP_TERM (rator (mk_forall(y,Py))) (ABS y body)
2853 in
2854 GEN P (TRANS EXISTS_UNIQUE_ALT' (MK_EXISTS (GEN x inner)))
2855 end);
2856
2857
2858(*---------------------------------------------------------------------------
2859 LET_CONG =
2860 |- !f g M N. (M = N) /\ (!x. (x = N) ==> (f x = g x))
2861 ==>
2862 (LET f M = LET g N)
2863 ---------------------------------------------------------------------------*)
2864
2865val LET_CONG = thm (#(FILE), #(LINE))("LET_CONG",
2866 let val f = mk_var("f",alpha-->beta)
2867 val g = mk_var("g",alpha-->beta)
2868 val M = mk_var("M",alpha)
2869 val N = mk_var("N",alpha)
2870 val x = mk_var ("x",alpha)
2871 val MeqN = mk_eq(M,N)
2872 val x_eq_N = mk_eq(x,N)
2873 val fx_eq_gx = mk_eq(mk_comb(f,x),mk_comb(g,x))
2874 val ctm = mk_forall(x, mk_imp(x_eq_N,fx_eq_gx))
2875 val th = RIGHT_BETA(AP_THM(RIGHT_BETA(AP_THM LET_DEF f)) M)
2876 val th1 = ASSUME MeqN
2877 val th2 = MP (SPEC N (ASSUME ctm)) (REFL N)
2878 val th3 = SUBS [SYM th1] th2
2879 val th4 = TRANS (TRANS th th3) (MK_COMB (REFL g,th1))
2880 val th5 = RIGHT_BETA(AP_THM(RIGHT_BETA(AP_THM LET_DEF g)) N)
2881 val th6 = TRANS th4 (SYM th5)
2882 val th7 = SUBS [SPECL [MeqN, ctm, concl th6] AND_IMP_INTRO]
2883 (DISCH MeqN (DISCH ctm th6))
2884 in
2885 GENL [f,g,M,N] th7
2886 end);
2887
2888(*---------------------------------------------------------------------------
2889 IMP_CONG =
2890 |- !x x' y y'. (x = x') /\ (x' ==> (y = y'))
2891 ==>
2892 (x ==> y = x' ==> y')
2893 ---------------------------------------------------------------------------*)
2894
2895val IMP_CONG = thm (#(FILE), #(LINE))("IMP_CONG",
2896 let val x = mk_var("x",Type.bool)
2897 val x' = mk_var("x'",Type.bool)
2898 val y = mk_var("y",Type.bool)
2899 val y' = mk_var("y'",Type.bool)
2900 val x_eq_x' = mk_eq(x,x')
2901 val ctm = mk_imp(x', mk_eq(y,y'))
2902 val x_imp_y = mk_imp(x,y)
2903 val x'_imp_y' = mk_imp(x',y')
2904 val th = ASSUME x_eq_x'
2905 val th1 = UNDISCH(ASSUME ctm)
2906 val th2 = ASSUME x_imp_y
2907 val th3 = DISCH x_imp_y (DISCH x' (UNDISCH(SUBS [th,th1] th2)))
2908 val th4 = ASSUME x'_imp_y'
2909 val th5 = UNDISCH (SUBS [SYM th] (DISCH x' th1))
2910 val th6 = DISCH x'_imp_y' (DISCH x (UNDISCH(SUBS [SYM th,SYM th5] th4)))
2911 val th7 = IMP_ANTISYM_RULE th3 th6
2912 val th8 = DISCH x_eq_x' (DISCH ctm th7)
2913 val th9 = SUBS [SPECL [x_eq_x', ctm, concl th7] AND_IMP_INTRO] th8
2914 in
2915 GENL [x,x',y,y'] th9
2916 end);
2917
2918(*---------------------------------------------------------------------------
2919 AND_CONG = |- !P P' Q Q'.
2920 (Q ==> (P = P')) /\ (P' ==> (Q = Q'))
2921 ==>
2922 (P /\ Q = P' /\ Q')
2923 ---------------------------------------------------------------------------*)
2924
2925val AND_CONG = thm (#(FILE), #(LINE))("AND_CONG",
2926 let val P = mk_var("P",Type.bool)
2927 val P' = mk_var("P'",Type.bool)
2928 val Q = mk_var("Q",Type.bool)
2929 val Q' = mk_var("Q'",Type.bool)
2930 val PandQ = mk_conj(P,Q)
2931 val P'andQ' = mk_conj(P',Q')
2932 val ctm1 = mk_imp(Q, mk_eq(P,P'))
2933 val ctm2 = mk_imp(P', mk_eq(Q,Q'))
2934 val th1 = ASSUME PandQ
2935 val th2 = MP (ASSUME ctm1) (CONJUNCT2 th1)
2936 val th3 = MP (ASSUME ctm2) (SUBS [th2] (CONJUNCT1 th1))
2937 val th4 = DISCH PandQ (SUBS[th2,th3] th1)
2938 val th5 = ASSUME P'andQ'
2939 val th6 = MP (ASSUME ctm2) (CONJUNCT1 th5)
2940 val th7 = MP (ASSUME ctm1) (SUBS [SYM th6] (CONJUNCT2 th5))
2941 val th8 = DISCH P'andQ' (SUBS[SYM th6,SYM th7] th5)
2942 val th9 = IMP_ANTISYM_RULE th4 th8
2943 val th10 = SUBS [SPECL [ctm1,ctm2,concl th9] AND_IMP_INTRO]
2944 (DISCH ctm1 (DISCH ctm2 th9))
2945 in
2946 GENL [P,P',Q,Q'] th10
2947 end);
2948
2949(*---------------------------------------------------------------------------
2950 LEFT_AND_CONG =
2951 |- !P P' Q Q'.
2952 (P = P') /\ (P' ==> (Q = Q'))
2953 ==>
2954 (P /\ Q = P' /\ Q')
2955 ---------------------------------------------------------------------------*)
2956
2957val LEFT_AND_CONG = thm (#(FILE), #(LINE))("LEFT_AND_CONG",
2958 let val P = mk_var("P",Type.bool)
2959 val P' = mk_var("P'",Type.bool)
2960 val Q = mk_var("Q",Type.bool)
2961 val Q' = mk_var("Q'",Type.bool)
2962 val PandQ = mk_conj(P,Q)
2963 val P'andQ' = mk_conj(P',Q')
2964 val ctm1 = mk_eq(P,P')
2965 val ctm2 = mk_imp(P', mk_eq(Q,Q'))
2966 val th1 = ASSUME PandQ
2967 val th2 = ASSUME ctm1
2968 val th3 = SUBS [th2] (CONJUNCT1 th1)
2969 val th3a = MP (ASSUME ctm2) th3
2970 val th4 = DISCH PandQ (SUBS[th2,th3a] th1)
2971 val th5 = ASSUME P'andQ'
2972 val th6 = SUBS [SYM th2] (CONJUNCT1 th5)
2973 val th7 = SYM(MP (ASSUME ctm2) (CONJUNCT1 th5))
2974 val th8 = DISCH P'andQ' (SUBS[SYM th2,th7] th5)
2975 val th9 = IMP_ANTISYM_RULE th4 th8
2976 val th10 = SUBS [SPECL [ctm1,ctm2,concl th9] AND_IMP_INTRO]
2977 (DISCH ctm1 (DISCH ctm2 th9))
2978 in
2979 GENL [P,P',Q,Q'] th10
2980 end);
2981
2982(*---------------------------------------------------------------------------
2983 val OR_CONG =
2984 |- !P P' Q Q'.
2985 (~Q ==> (P = P')) /\ (~P' ==> (Q = Q'))
2986 ==>
2987 (P \/ Q = P' \/ Q')
2988 ---------------------------------------------------------------------------*)
2989
2990val OR_CONG = thm (#(FILE), #(LINE))("OR_CONG",
2991 let val P = mk_var("P",Type.bool)
2992 val P' = mk_var("P'",Type.bool)
2993 val Q = mk_var("Q",Type.bool)
2994 val Q' = mk_var("Q'",Type.bool)
2995 val notQ = mk_neg Q
2996 val notP' = mk_neg P'
2997 val PorQ = mk_disj(P,Q)
2998 val P'orQ' = mk_disj(P',Q')
2999 val PeqP'= mk_eq(P,P')
3000 val QeqQ'= mk_eq(Q,Q')
3001 val ctm1 = mk_imp(notQ,PeqP')
3002 val ctm2 = mk_imp(notP',QeqQ')
3003 val th1 = ASSUME PorQ
3004 val th2 = ASSUME P
3005 val th3 = ASSUME Q
3006 val th4 = ASSUME ctm1
3007 val th5 = ASSUME ctm2
3008 val th6 = SUBS [SPEC Q (CONJUNCT1 NOT_CLAUSES)]
3009 (SUBS [SPECL[notQ, PeqP'] IMP_DISJ_THM] th4)
3010 val th7 = SUBS [SPEC P' (CONJUNCT1 NOT_CLAUSES)]
3011 (SUBS [SPECL[notP', QeqQ'] IMP_DISJ_THM] th5)
3012 val th8 = ASSUME P'
3013 val th9 = DISJ1 th8 Q'
3014 val th10 = ASSUME QeqQ'
3015 val th11 = SUBS [th10] th3
3016 val th12 = DISJ2 P' th11
3017 val th13 = ASSUME PeqP'
3018 val th14 = MK_COMB(REFL(mk_const("\\/",bool-->bool-->bool)),th13)
3019 val th15 = EQ_MP (MK_COMB (th14,th10)) th1
3020 val th16 = DISJ_CASES th6 th12 th15
3021 val th17 = DISCH PorQ (DISJ_CASES th7 th9 th16)
3022 val th18 = ASSUME P'orQ'
3023 val th19 = DISJ2 P th3
3024 val th20 = DISJ1 (SUBS [SYM th13] th8) Q
3025 val th21 = EQ_MP (SYM (MK_COMB(th14,th10))) th18
3026 val th22 = DISJ_CASES th7 th20 th21
3027 val th23 = DISCH P'orQ' (DISJ_CASES th6 th19 th22)
3028 val th24 = IMP_ANTISYM_RULE th17 th23
3029 val th25 = SUBS [SPECL [ctm1,ctm2,concl th24] AND_IMP_INTRO]
3030 (DISCH ctm1 (DISCH ctm2 th24))
3031 in
3032 GENL [P,P',Q,Q'] th25
3033 end);
3034
3035(*---------------------------------------------------------------------------
3036 val LEFT_OR_CONG =
3037 |- !P P' Q Q'.
3038 (P = P') /\ (~P' ==> (Q = Q'))
3039 ==>
3040 (P \/ Q = P' \/ Q')
3041 ---------------------------------------------------------------------------*)
3042
3043val LEFT_OR_CONG = thm (#(FILE), #(LINE))("LEFT_OR_CONG",
3044 let fun mk_boolvar s = mk_var(s,Type.bool)
3045 val [P,P',Q,Q'] = map mk_boolvar ["P","P'","Q","Q'"]
3046 val notP = mk_neg P
3047 val notP' = mk_neg P'
3048 val PorQ = mk_disj(P,Q)
3049 val P'orQ' = mk_disj(P',Q')
3050 val PeqP' = mk_eq(P,P')
3051 val ctm = mk_imp(notP',mk_eq(Q,Q'))
3052 val th1 = ASSUME ctm
3053 val th2 = ASSUME PeqP'
3054 val th3 = DISJ1 (SUBS [th2] (ASSUME P)) Q'
3055 val th4 = MP th1 (SUBS [th2] (ASSUME notP))
3056 val th5 = DISJ2 P' (SUBS [th4] (ASSUME Q))
3057 val th6 = DISJ_CASES (SPEC P EXCLUDED_MIDDLE) th3 th5
3058 val th7 = DISCH PorQ (DISJ_CASES (ASSUME PorQ) th3 th6)
3059 val th8 = DISJ1 (SUBS [SYM th2] (ASSUME P')) Q
3060 val th9 = MP th1 (ASSUME notP')
3061 val th10 = DISJ2 P (SUBS [SYM th9] (ASSUME Q'))
3062 val th11 = DISJ_CASES (SPEC P' EXCLUDED_MIDDLE) th8 th10
3063 val th12 = DISCH P'orQ' (DISJ_CASES (ASSUME P'orQ') th8 th11)
3064 val th13 = DISCH PeqP' (DISCH ctm (IMP_ANTISYM_RULE th7 th12))
3065 val th14 = SUBS[SPECL [PeqP',ctm,mk_eq(PorQ,P'orQ')] AND_IMP_INTRO] th13
3066 in
3067 GENL [P,P',Q,Q'] th14
3068 end);
3069
3070(*---------------------------------------------------------------------------
3071 val COND_CONG =
3072 |- !P Q x x' y y'.
3073 (P = Q) /\ (Q ==> (x = x')) /\ (~Q ==> (y = y'))
3074 ==>
3075 ((if P then x else y) = (if Q then x' else y'))
3076 ---------------------------------------------------------------------------*)
3077
3078fun mk_cond {cond,larm,rarm} = “if ^cond then ^larm else ^rarm”;
3079
3080val COND_CONG = thm (#(FILE), #(LINE))("COND_CONG",
3081 let val P = mk_var("P",Type.bool)
3082 val Q = mk_var("Q",Type.bool)
3083 val x = mk_var("x",alpha)
3084 val x' = mk_var("x'",alpha)
3085 val y = mk_var("y",alpha)
3086 val y' = mk_var("y'",alpha)
3087 val PeqQ = mk_eq(P,Q)
3088 val ctm1 = mk_imp(Q, mk_eq(x,x'))
3089 val ctm2 = mk_imp(mk_neg Q, mk_eq(y,y'))
3090 val target = mk_eq(mk_cond{cond=P,larm=x,rarm=y},
3091 mk_cond{cond=Q,larm=x',rarm=y'})
3092 val OR_ELIM = MP (SPECL[target,P,mk_neg P] OR_ELIM_THM)
3093 (SPEC P EXCLUDED_MIDDLE)
3094 val th1 = ASSUME P
3095 val th2 = EQT_INTRO th1
3096 val th3 = CONJUNCT1 (SPECL [x,y] COND_CLAUSES)
3097 val th3a = CONJUNCT1 (SPECL [x',y'] COND_CLAUSES)
3098 val th4 = SUBS [SYM th2] th3
3099 val th4a = SUBS [SYM th2] th3a
3100 val th5 = ASSUME PeqQ
3101 val th6 = ASSUME ctm1
3102 val th7 = ASSUME ctm2
3103 val th8 = UNDISCH (SUBS [SYM th5] th6)
3104 val th9 = TRANS th4 th8
3105 val th10 = TRANS th9 (SYM (SUBS [th5] th4a))
3106 val th11 = EQF_INTRO (ASSUME (mk_neg P))
3107 val th12 = CONJUNCT2 (SPECL [x,y] COND_CLAUSES)
3108 val th13 = CONJUNCT2 (SPECL [x',y'] COND_CLAUSES)
3109 val th14 = SUBS [SYM th11] th12
3110 val th15 = SUBS [SYM th11] th13
3111 val th16 = UNDISCH (SUBS [SYM th5] th7)
3112 val th17 = TRANS th14 th16
3113 val th18 = TRANS th17 (SYM (SUBS [th5] th15))
3114 val th19 = MP (MP OR_ELIM (DISCH P th10)) (DISCH (mk_neg P) th18)
3115 val th20 = DISCH PeqQ (DISCH ctm1 (DISCH ctm2 th19))
3116 val th21 = SUBS [SPECL [ctm1, ctm2,concl th19] AND_IMP_INTRO] th20
3117 val cnj = mk_conj(ctm1,ctm2)
3118 val th22 = SUBS [SPECL [PeqQ,cnj,concl th19] AND_IMP_INTRO] th21
3119 in
3120 GENL [P,Q,x,x',y,y'] th22
3121 end);
3122
3123(* ----------------------------------------------------------------------
3124
3125 RES_FORALL_CONG
3126 |- (P = Q) ==> (!x. x IN Q ==> (f x = g x)) ==>
3127 (RES_FORALL P f = RES_FORALL Q g)
3128
3129 RES_EXISTS_CONG
3130 |- (P = Q) ==> (!x. x IN Q ==> (f x = g x)) ==>
3131 (RES_EXISTS P f = RES_EXISTS P g)
3132 ---------------------------------------------------------------------- *)
3133
3134val (RES_FORALL_CONG, RES_EXISTS_CONG) = let
3135 (* stuff in common to both *)
3136 val aset_ty = alpha --> bool
3137 val [P,Q,f,g] = map (fn s => mk_var(s, aset_ty)) ["P", "Q", "f", "g"]
3138 val PeqQ_t = mk_eq(P, Q)
3139 val PeqQ_th = ASSUME PeqQ_t
3140 val x = mk_var("x", alpha)
3141 val fx_t = mk_comb(f, x)
3142 val gx_t = mk_comb(g, x)
3143 val IN_t = prim_mk_const {Thy = "bool", Name = "IN"}
3144 val xINP_t = list_mk_comb(IN_t, [x, P])
3145 val xINP_th = ASSUME xINP_t
3146 val xINQ_t = list_mk_comb(IN_t, [x, Q])
3147 val xINQ_th = ASSUME xINQ_t
3148 val xINP_eq_xINQ_th = AP_TERM (mk_comb(IN_t, x)) PeqQ_th
3149 val (xINP_imp_xINQ, xINQ_imp_xINP) = EQ_IMP_RULE xINP_eq_xINQ_th
3150 val feqg_t = mk_forall(x, mk_imp(xINQ_t, mk_eq(mk_comb(f,x), mk_comb(g, x))))
3151 val feqg_th = SPEC x (ASSUME feqg_t)
3152 val feqg_th = MP feqg_th xINQ_th
3153 val (f_imp_g_th, g_imp_f_th) = EQ_IMP_RULE feqg_th
3154
3155 fun mk_res th args =
3156 List.foldl (RIGHT_BETA o uncurry (C AP_THM)) th args
3157
3158 (* forall thm *)
3159 val resfa_t = prim_mk_const {Thy = "bool", Name = "RES_FORALL"}
3160 val res_pf_t = list_mk_comb(resfa_t, [P, f])
3161 val res_qg_t = list_mk_comb(resfa_t, [Q, g])
3162 val resfa_pf_eqn = mk_res RES_FORALL_DEF [P, f]
3163 val resfa_qg_eqn = mk_res RES_FORALL_DEF [Q, g]
3164
3165 val resfa_pf_eq_th = SPEC x (EQ_MP resfa_pf_eqn (ASSUME res_pf_t))
3166 val g_th = MP f_imp_g_th (MP resfa_pf_eq_th xINP_th)
3167 val xinq_imp_g_th =
3168 GEN x (DISCH xINQ_t (PROVE_HYP (UNDISCH xINQ_imp_xINP) g_th))
3169 val rfa_pf_imp_rfa_qg =
3170 DISCH res_pf_t (EQ_MP (SYM resfa_qg_eqn) xinq_imp_g_th)
3171
3172 val resfa_qg_eq_th = SPEC x (EQ_MP resfa_qg_eqn (ASSUME res_qg_t))
3173 val f_th = MP g_imp_f_th (MP resfa_qg_eq_th xINQ_th)
3174 val xinp_imp_f_th =
3175 GEN x (DISCH xINP_t (PROVE_HYP (UNDISCH xINP_imp_xINQ) f_th))
3176 val rfa_qg_imp_rfa_pf =
3177 DISCH res_qg_t (EQ_MP (SYM resfa_pf_eqn) xinp_imp_f_th)
3178 val fa_eqn = IMP_ANTISYM_RULE rfa_pf_imp_rfa_qg rfa_qg_imp_rfa_pf
3179
3180 (* exists thm *)
3181 val resex_t = prim_mk_const {Thy = "bool", Name = "RES_EXISTS"}
3182 val res_pf_t = list_mk_comb(resex_t, [P, f])
3183 val res_qg_t = list_mk_comb(resex_t, [Q, g])
3184 val resex_pf_eqn = mk_res RES_EXISTS_DEF [P, f]
3185 val resex_qg_eqn = mk_res RES_EXISTS_DEF [Q, g]
3186
3187 val pf_exbody_th = EQ_MP resex_pf_eqn (ASSUME res_pf_t)
3188 val pf_body_th = ASSUME(mk_conj(xINP_t, fx_t))
3189 val (new_xINP_th, fx_th) = CONJ_PAIR pf_body_th
3190 val new_xINQ_th = MP xINP_imp_xINQ new_xINP_th
3191 val new_gx_th = PROVE_HYP new_xINQ_th (MP f_imp_g_th fx_th)
3192 val qg_exists =
3193 EXISTS(rhs (concl resex_qg_eqn), x) (CONJ new_xINQ_th new_gx_th)
3194 val pf_chosen = CHOOSE(x,EQ_MP resex_pf_eqn (ASSUME res_pf_t)) qg_exists
3195 val ex_pf_imp_qg = DISCH res_pf_t (EQ_MP (SYM resex_qg_eqn) pf_chosen)
3196
3197 val qg_exbody_th = EQ_MP resex_qg_eqn (ASSUME res_qg_t)
3198 val qg_body_th = ASSUME(mk_conj(xINQ_t, gx_t))
3199 val (new_xINQ_th, gx_th) = CONJ_PAIR qg_body_th
3200 val new_xINP_th = MP xINQ_imp_xINP new_xINQ_th
3201 val new_fx_th = PROVE_HYP new_xINQ_th (MP g_imp_f_th gx_th)
3202 val pf_exists =
3203 EXISTS (rhs (concl resex_pf_eqn), x) (CONJ new_xINP_th new_fx_th)
3204 val qg_chosen = CHOOSE(x, EQ_MP resex_qg_eqn (ASSUME res_qg_t)) pf_exists
3205 val ex_qg_imp_pf = DISCH res_qg_t (EQ_MP (SYM resex_pf_eqn) qg_chosen)
3206
3207 val ex_eqn = IMP_ANTISYM_RULE ex_pf_imp_qg ex_qg_imp_pf
3208
3209in
3210 (thm (#(FILE), #(LINE))("RES_FORALL_CONG",
3211 DISCH PeqQ_t (DISCH feqg_t fa_eqn)),
3212 thm (#(FILE), #(LINE))("RES_EXISTS_CONG",
3213 DISCH PeqQ_t (DISCH feqg_t ex_eqn)))
3214end
3215
3216(* ------------------------------------------------------------------------- *)
3217(* Monotonicity. *)
3218(* ------------------------------------------------------------------------- *)
3219
3220
3221(* ------------------------------------------------------------------------- *)
3222(* MONO_AND |- (x ==> y) /\ (z ==> w) ==> (x /\ z ==> y /\ w) *)
3223(* ------------------------------------------------------------------------- *)
3224
3225val MONO_AND = thm (#(FILE), #(LINE))("MONO_AND",
3226 let val tm1 = “x ==> y”
3227 val tm2 = “z ==> w”
3228 val tm3 = “x /\ z”
3229 val tm4 = “y /\ w”
3230 val th1 = ASSUME tm1
3231 val th2 = ASSUME tm2
3232 val th3 = ASSUME tm3
3233 val th4 = CONJUNCT1 th3
3234 val th5 = CONJUNCT2 th3
3235 val th6 = MP th1 th4
3236 val th7 = MP th2 th5
3237 val th8 = CONJ th6 th7
3238 val th9 = itlist DISCH [tm1,tm2,tm3] th8
3239 val th10 = SPEC “^tm3 ==> ^tm4” (SPEC tm2 (SPEC tm1 AND_IMP_INTRO))
3240 in
3241 EQ_MP th10 th9
3242 end);
3243
3244(* ------------------------------------------------------------------------- *)
3245(* MONO_OR |- (x ==> y) /\ (z ==> w) ==> (x \/ z ==> y \/ w) *)
3246(* ------------------------------------------------------------------------- *)
3247
3248val MONO_OR = thm (#(FILE), #(LINE))("MONO_OR",
3249 let val tm1 = “x ==> y”
3250 val tm2 = “z ==> w”
3251 val tm3 = “x \/ z”
3252 val tm4 = “y \/ w”
3253 val th1 = ASSUME tm1
3254 val th2 = ASSUME tm2
3255 val th3 = ASSUME tm3
3256 val th4 = DISJ1 (MP th1 (ASSUME “x:bool”)) “w:bool”
3257 val th5 = DISJ2 “y:bool” (MP th2 (ASSUME “z:bool”))
3258 val th6 = DISJ_CASES th3 th4 th5
3259 val th7 = DISCH tm1 (DISCH tm2 (DISCH tm3 th6))
3260 val th8 = SPEC “^tm3 ==> ^tm4” (SPEC tm2 (SPEC tm1 AND_IMP_INTRO))
3261 in
3262 EQ_MP th8 th7
3263 end);
3264
3265(* ------------------------------------------------------------------------- *)
3266(* MONO_IMP |- (y ==> x) /\ (z ==> w) ==> ((x ==> z) ==> (y ==> w)) *)
3267(* ------------------------------------------------------------------------- *)
3268
3269val MONO_IMP = thm (#(FILE), #(LINE))("MONO_IMP",
3270 let val tm1 = “y ==> x”
3271 val tm2 = “z ==> w”
3272 val tm3 = “x ==> z”
3273 val tm4 = “y ==> w”
3274 val tm5 = “y:bool”
3275 val th1 = ASSUME tm1
3276 val th2 = ASSUME tm2
3277 val th3 = ASSUME tm3
3278 val th4 = MP th1 (ASSUME tm5)
3279 val th5 = MP th3 th4
3280 val th6 = MP th2 th5
3281 val th7 = DISCH tm1 (DISCH tm2 (DISCH tm3 (DISCH tm5 th6)))
3282 val th8 = SPEC “^tm3 ==> ^tm4” (SPEC tm2 (SPEC tm1 AND_IMP_INTRO))
3283 in
3284 EQ_MP th8 th7
3285 end);
3286
3287(* ------------------------------------------------------------------------- *)
3288(* MONO_NOT |- (y ==> x) ==> (~x ==> ~y) *)
3289(* ------------------------------------------------------------------------- *)
3290
3291val MONO_NOT = thm (#(FILE), #(LINE))("MONO_NOT",
3292 let val tm1 = “y ==> x”
3293 val tm2 = “~x”
3294 val tm3 = “y:bool”
3295 val th1 = ASSUME tm1
3296 val th2 = ASSUME tm2
3297 val th3 = ASSUME tm3
3298 val th4 = MP th1 th3
3299 val th5 = DISCH tm3 (MP th2 th4)
3300 val th6 = EQ_MP (SYM (RIGHT_BETA (AP_THM NOT_DEF tm3))) th5
3301 in
3302 DISCH tm1 (DISCH tm2 th6)
3303 end);
3304
3305(* ------------------------------------------------------------------------- *)
3306(* MONO_NOT_EQ |- (y ==> x) = (~x ==> ~y) *)
3307(* ------------------------------------------------------------------------- *)
3308
3309val MONO_NOT_EQ = thm (#(FILE), #(LINE))("MONO_NOT_EQ",
3310 let val tm1 = “x:bool”
3311 val tm2 = “y:bool”
3312 val th1 = INST [tm1 |-> mk_neg tm2, tm2 |-> mk_neg tm1] MONO_NOT
3313
3314 val th2 = SUBST [“x1:bool” |-> SPEC tm1 (CONJUNCT1 NOT_CLAUSES),
3315 “x2:bool” |-> SPEC tm2 (CONJUNCT1 NOT_CLAUSES)]
3316 “(~x ==> ~y) ==> (x2 ==> x1)” th1
3317
3318 val th3 = IMP_ANTISYM_RULE MONO_NOT th2
3319 in
3320 th3
3321 end);
3322
3323(* ------------------------------------------------------------------------- *)
3324(* MONO_ALL |- (!x. P x ==> Q x) ==> (!x. P x) ==> !x. Q x *)
3325(* ------------------------------------------------------------------------- *)
3326
3327val MONO_ALL = thm (#(FILE), #(LINE))("MONO_ALL",
3328 let val tm1 = “!x:'a. P x ==> Q x”
3329 val tm2 = “!x:'a. P x”
3330 val tm3 = “x:'a”
3331 val th1 = ASSUME tm1
3332 val th2 = ASSUME tm2
3333 val th3 = SPEC tm3 th1
3334 val th4 = SPEC tm3 th2
3335 val th5 = GEN tm3 (MP th3 th4)
3336 in
3337 DISCH tm1 (DISCH tm2 th5)
3338 end);
3339
3340(* ------------------------------------------------------------------------- *)
3341(* MONO_EXISTS = [] |- (!x. P x ==> Q x) ==> (?x. P x) ==> ?x. Q x *)
3342(* ------------------------------------------------------------------------- *)
3343
3344val MONO_EXISTS = thm (#(FILE), #(LINE))("MONO_EXISTS",
3345 let val tm1 = “!x:'a. P x ==> Q x”
3346 val tm2 = “?x:'a. P x”
3347 val tm3 = “@x:'a. P x”
3348 val tm4 = “\x:'a. P x:bool”
3349 val th1 = ASSUME tm1
3350 val th2 = ASSUME tm2
3351 val th3 = SPEC tm3 th1
3352 val th4 = RIGHT_BETA(RIGHT_BETA (AP_THM EXISTS_DEF tm4))
3353 val th5 = EQ_MP th4 th2
3354 val th6 = MP th3 th5
3355 in
3356 DISCH tm1 (DISCH tm2 (EXISTS (“?x:'a. Q x”, tm3) th6))
3357 end);
3358
3359(* ------------------------------------------------------------------------- *)
3360(* MONO_COND |- (x ==> y) ==> (z ==> w) *)
3361(* ==> (if b then x else z) ==> (if b then y else w) *)
3362(* ------------------------------------------------------------------------- *)
3363
3364val MONO_COND = thm (#(FILE), #(LINE))("MONO_COND",
3365 let val tm1 = “x ==> y”
3366 val tm2 = “z ==> w”
3367 val tm3 = “if b then x else z:bool”
3368 val tm4 = “b:bool”
3369 val tm5 = “x:bool”
3370 val tm6 = “z:bool”
3371 val tm7 = “y:bool”
3372 val tm8 = “w:bool”
3373 val th1 = ASSUME tm1
3374 val th2 = ASSUME tm2
3375 val th3 = ASSUME tm3
3376 val th4 = SPEC tm6 (SPEC tm5 (INST_TYPE [alpha |-> bool] COND_CLAUSES))
3377 val th5 = CONJUNCT1 th4
3378 val th6 = CONJUNCT2 th4
3379 val th7 = SPEC tm4 BOOL_CASES_AX
3380 val th8 = ASSUME “b = T”
3381 val th9 = ASSUME “b = F”
3382 val th10 = SUBST [tm4 |-> th8] (concl th3) th3
3383 val th11 = SUBST [tm4 |-> th9] (concl th3) th3
3384 val th12 = EQ_MP th5 th10
3385 val th13 = EQ_MP th6 th11
3386 val th14 = MP th1 th12
3387 val th15 = MP th2 th13
3388 val th16 = INST [tm5 |-> tm7, tm6 |-> tm8] th4
3389 val th17 = SYM (CONJUNCT1 th16)
3390 val th18 = SYM (CONJUNCT2 th16)
3391 val th19 = EQ_MP th17 th14
3392 val th20 = EQ_MP th18 th15
3393 val th21 = DISCH tm3 th19
3394 val th22 = DISCH tm3 th20
3395 val th23 = SUBST [tm4 |-> th8] (concl th21) th21
3396 val th24 = SUBST [tm4 |-> th9] (concl th22) th22
3397 val v = “v:bool”
3398 val T = mk_const("T",bool)
3399 val template = subst [T |-> v] (concl th23)
3400 val th25 = SUBST [v |-> SYM th8] template th23
3401 val th26 = SUBST [v |-> SYM th9] template th24
3402 in
3403 DISCH tm1 (DISCH tm2 (DISJ_CASES th7 th25 th26))
3404 end);
3405
3406(* ------------------------------------------------------------------------- *)
3407(* EXISTS_REFL |- !a. ?x. x = a *)
3408(* ------------------------------------------------------------------------- *)
3409
3410val EXISTS_REFL = thm (#(FILE), #(LINE))("EXISTS_REFL",
3411 let val a = “a:'a”
3412 val th1 = REFL a
3413 val th2 = EXISTS (“?x:'a. x = a”, a) th1
3414 in GEN a th2
3415 end);
3416
3417(* ------------------------------------------------------------------------- *)
3418(* EXISTS_UNIQUE_REFL |- !a. ?!x. x = a *)
3419(* ------------------------------------------------------------------------- *)
3420
3421val EXISTS_UNIQUE_REFL = thm (#(FILE), #(LINE))("EXISTS_UNIQUE_REFL",
3422 let val a = “a:'a”
3423 val P = “\x:'a. x = a”
3424 val tmx = “^P x”
3425 val tmy= “^P y”
3426 val ex = “?x. ^P x”
3427 val th1 = SPEC a EXISTS_REFL
3428 val th2 = ABS “x:'a” (BETA_CONV tmx)
3429 val th3 = AP_TERM “$? :('a->bool)->bool” th2
3430 val th4 = EQ_MP (SYM th3) th1
3431 val th5 = ASSUME (mk_conj(tmx,tmy))
3432 val th6 = CONJUNCT1 th5
3433 val th7 = CONJUNCT2 th5
3434 val th8 = EQ_MP (BETA_CONV (concl th6)) th6
3435 val th9 = EQ_MP (BETA_CONV (concl th7)) th7
3436 val th10 = TRANS th8 (SYM th9)
3437 val th11 = DISCH (hd(hyp th10)) th10
3438 val th12 = GEN “x:'a” (GEN “y:'a” th11)
3439 val th13 = INST [“P:'a->bool” |-> P] EXISTS_UNIQUE_THM
3440 val th14 = EQ_MP (SYM th13) (CONJ th4 th12)
3441 val th15 = AP_TERM “$?! :('a->bool)->bool” th2
3442 in
3443 GEN a (EQ_MP th15 th14)
3444 end);
3445
3446(* ----------------------------------------------------------------------
3447 EXISTS_UNIQUE_FALSE |- (?!x. F) <=> F
3448 ---------------------------------------------------------------------- *)
3449
3450val EXISTS_UNIQUE_FALSE = thm (#(FILE), #(LINE))("EXISTS_UNIQUE_FALSE",
3451 let
3452 val BINDER_CONV = RAND_CONV o ABS_CONV
3453 val LAND_CONV = RATOR_CONV o RAND_CONV
3454 val P = mk_var("P", alpha --> bool)
3455 val x = mk_var("x", alpha)
3456 val th1 = INST [P |-> mk_abs(x, F)] EXISTS_UNIQUE_THM
3457 val th2 = CONV_RULE(RAND_CONV (LAND_CONV (BINDER_CONV BETA_CONV))) th1
3458 val th3 = CONV_RULE(LAND_CONV (BINDER_CONV BETA_CONV)) th2
3459 val uniqueness_t = th3 |> concl |> rhs |> rand
3460 val simp1 = AP_THM (AP_TERM conjunction (SPEC F EXISTS_SIMP)) uniqueness_t
3461 val th4 = TRANS th3 simp1
3462 val simp2 = AND_CLAUSES |> SPEC uniqueness_t |> CONJUNCTS |> el 3
3463 in
3464 TRANS th4 simp2
3465 end);
3466
3467(* ------------------------------------------------------------------------- *)
3468(* Unwinding. *)
3469(* ------------------------------------------------------------------------- *)
3470
3471
3472(* ------------------------------------------------------------------------- *)
3473(* UNWIND1_THM |- !P a. (?x. (a = x) /\ P x) = P a *)
3474(* ------------------------------------------------------------------------- *)
3475
3476val UNWIND_THM1 = thm (#(FILE), #(LINE))("UNWIND_THM1",
3477 let val P = “P:'a->bool”
3478 val a = “a:'a”
3479 val Pa = “^P ^a”
3480 val v = “v:'a”
3481 val tm1 = “?x:'a. (a = x) /\ P x”
3482 val th1 = ASSUME tm1
3483 val th2 = ASSUME “(a:'a = v) /\ P v”
3484 val th3 = CONJUNCT1 th2
3485 val th4 = CONJUNCT2 th2
3486 val th5 = SUBST [v |-> SYM th3] (concl th4) th4
3487 val th6 = DISCH tm1 (CHOOSE (v,th1) th5)
3488 val th7 = ASSUME Pa
3489 val th8 = CONJ (REFL a) th7
3490 val th9 = EXISTS (tm1,a) th8
3491 val th10 = DISCH Pa th9
3492 val th11 = SPEC Pa (SPEC tm1 IMP_ANTISYM_AX)
3493 in
3494 GEN P (GEN a (MP (MP th11 th6) th10))
3495 end);
3496
3497
3498(* ------------------------------------------------------------------------- *)
3499(* UNWIND_THM2 |- !P a. (?x. (x = a) /\ P x) = P a *)
3500(* ------------------------------------------------------------------------- *)
3501
3502val UNWIND_THM2 = thm (#(FILE), #(LINE))("UNWIND_THM2",
3503 let val P = “P:'a->bool”
3504 val a = “a:'a”
3505 val Px = “^P x”
3506 val Pa = “^P ^a”
3507 val u = “u:'a”
3508 val v = “v:'a”
3509 val a_eq_x = “a:'a = x”
3510 val x_eq_a = “x:'a = a”
3511 val th1 = SPEC a (SPEC P UNWIND_THM1)
3512 val th2 = REFL Pa
3513 val th3 = DISCH a_eq_x (SYM (ASSUME a_eq_x))
3514 val th4 = DISCH x_eq_a (SYM (ASSUME x_eq_a))
3515 val th5 = SPEC a_eq_x (SPEC x_eq_a IMP_ANTISYM_AX)
3516 val th6 = MP (MP th5 th4) th3
3517 val th7 = MK_COMB (MK_COMB (REFL “$/\”, th6), REFL Px)
3518 val th8 = MK_COMB (REFL“$? :('a->bool)->bool”,
3519 ABS “x:'a” th7)
3520 val th9 = MK_COMB(MK_COMB (REFL“$= :bool->bool->bool”, th8),th2)
3521 val th10 = EQ_MP (SYM th9) th1
3522 in
3523 GEN P (GEN a th10)
3524 end);
3525
3526
3527(* ------------------------------------------------------------------------- *)
3528(* UNWIND_FORALL_THM1 |- !f v. (!x. (v = x) ==> f x) = f v *)
3529(* ------------------------------------------------------------------------- *)
3530
3531val UNWIND_FORALL_THM1 = thm (#(FILE), #(LINE))("UNWIND_FORALL_THM1",
3532 let val f = “f : 'a -> bool”
3533 val v = “v:'a”
3534 val fv = “^f ^v”
3535 val tm1 = “!x:'a. (v = x) ==> f x”
3536 val tm2 = “v:'a = x”
3537 val th1 = ASSUME tm1
3538 val th2 = ASSUME fv
3539 val th3 = DISCH tm1 (MP (SPEC v th1) (REFL v))
3540 val th4 = ASSUME tm2
3541 val th5 = SUBST [v |-> th4] (concl th2) th2
3542 val th6 = DISCH fv (GEN “x:'a” (DISCH tm2 th5))
3543 val th7 = MP (MP (SPEC tm1 (SPEC fv IMP_ANTISYM_AX)) th6) th3
3544 in
3545 GEN f (GEN v (SYM th7))
3546 end);
3547
3548
3549(* ------------------------------------------------------------------------- *)
3550(* UNWIND_FORALL_THM2 |- !f v. (!x. (x = v) ==> f x) = f v *)
3551(* ------------------------------------------------------------------------- *)
3552
3553val UNWIND_FORALL_THM2 = thm (#(FILE), #(LINE))("UNWIND_FORALL_THM2",
3554 let val f = “f:'a->bool”
3555 val v = “v:'a”
3556 val fv = “^f ^v”
3557 val tm1 = “!x:'a. (x = v) ==> f x”
3558 val tm2 = “x:'a = v”
3559 val th1 = ASSUME tm1
3560 val th2 = ASSUME fv
3561 val th3 = DISCH tm1 (MP (SPEC v th1) (REFL v))
3562 val th4 = ASSUME tm2
3563 val th5 = SUBST [v |-> SYM th4] (concl th2) th2
3564 val th6 = DISCH fv (GEN “x:'a” (DISCH tm2 th5))
3565 val th7 = MP (MP (SPEC tm1 (SPEC fv IMP_ANTISYM_AX)) th6) th3
3566 in
3567 GEN f (GEN v (SYM th7))
3568 end);
3569
3570
3571(* ------------------------------------------------------------------------- *)
3572(* Skolemization: |- !P. (!x. ?y. P x y) <=> ?f. !x. P x (f x) *)
3573(* ------------------------------------------------------------------------- *)
3574
3575val SKOLEM_THM = thm (#(FILE), #(LINE))("SKOLEM_THM",
3576 let val P = “P:'a -> 'b -> bool”
3577 val x = “x:'a”
3578 val y = “y:'b”
3579 val f = “f:'a->'b”
3580 val tm1 = “!x. ?y. ^P x y”
3581 val tm2 = “?f. !x. ^P x (f x)”
3582 val tm4 = “\x. @y. ^P x y”
3583 val tm5 = “(\x. @y. ^P x y) x”
3584 val th1 = ASSUME tm1
3585 val th2 = ASSUME tm2
3586 val th3 = SPEC x th1
3587 val th4 = INST_TYPE [alpha |-> beta] SELECT_AX
3588 val th5 = SPEC y (SPEC “\y. ^P x y” th4)
3589 val th6 = BETA_CONV (fst(dest_imp(concl th5)))
3590 val th7 = BETA_CONV (snd(dest_imp(concl th5)))
3591 val th8 = MK_COMB (MK_COMB (REFL “$==>”,th6),th7)
3592 val th9 = EQ_MP th8 th5
3593 val th10 = MP th9 (ASSUME(fst(dest_imp(concl th9))))
3594 val th11 = CHOOSE (y,th3) th10
3595 val th12 = SYM (BETA_CONV tm5)
3596 val th13 = SUBST [“v:'b” |-> th12] “^P x v” th11
3597 val th14 = DISCH tm1 (EXISTS (tm2,tm4) (GEN x th13))
3598 val th15 = ASSUME “!x. ^P x (f x)”
3599 val th16 = SPEC x th15
3600 val th17 = GEN x (EXISTS(“?y. ^P x y”,“f (x:'a):'b”) th16)
3601 val th18 = DISCH tm2 (CHOOSE (f,th2) th17)
3602 val th19 = MP (MP (SPEC tm1 (SPEC tm2 IMP_ANTISYM_AX)) th18) th14
3603 in
3604 GEN P (SYM th19)
3605 end);
3606
3607
3608(* ------------------------------------------------------------------------- *)
3609(* UNIQUE_SKOLEM_ALT *)
3610(* *)
3611(* Intuitionistic + intensional form of Skolem for unique existence: *)
3612(* |- !P. (!x. ?!y. P x y) <=> ?f. !x y. P x y <=> (f x = y) *)
3613(* ------------------------------------------------------------------------- *)
3614
3615val UNIQUE_SKOLEM_ALT = thm (#(FILE), #(LINE))("UNIQUE_SKOLEM_ALT",
3616 let val P = mk_var("P", alpha --> beta --> bool)
3617 val x = mk_var("x", alpha)
3618 val y = mk_var("y", beta)
3619 val g = mk_var("g", beta)
3620 val Pxy = mk_comb(mk_comb(P,x),y)
3621 val Q = mk_abs(x, mk_abs(g, mk_forall(y, mk_eq(Pxy, mk_eq(g,y)))))
3622 (* (?!y. P x y) <=> ?g. !y. P x y <=> (g = y), generalised over x *)
3623 val inner = SPEC (mk_comb(P,x))
3624 (INST_TYPE [alpha |-> beta] EXISTS_UNIQUE_ALT)
3625 val stepA = AP_TERM (rator (mk_forall(x,tb))) (ABS x inner)
3626 (* Skolemise the inner existential; the instance needs two betas at
3627 each of the two quantified positions. *)
3628 fun BETA2 tm =
3629 let val th = RATOR_CONV BETA_CONV tm
3630 in TRANS th (BETA_CONV (rhs (concl th)))
3631 end
3632 val SK = SPEC Q SKOLEM_THM
3633 val (skl,skr) = dest_eq (concl SK)
3634 val stepB = TRANS (SYM (QUANT_CONV (QUANT_CONV BETA2) skl))
3635 (TRANS SK (QUANT_CONV (QUANT_CONV BETA2) skr))
3636 val f = mk_var("f", alpha --> beta)
3637 val target =
3638 mk_eq(mk_forall(x, mk_exists1(y, Pxy)),
3639 mk_exists(f, mk_forall(x, mk_forall(y,
3640 mk_eq(Pxy, mk_eq(mk_comb(f,x), y))))))
3641 val th = TRANS stepA stepB
3642 in
3643 GEN P (EQ_MP (ALPHA (concl th) target) th)
3644 end);
3645
3646(* ------------------------------------------------------------------------- *)
3647(* UNIQUE_SKOLEM_THM *)
3648(* *)
3649(* Intuitionistic + extensional form of Skolem for unique existence: *)
3650(* |- !P. (!x. ?!y. P x y) <=> ?!f. !x. P x (f x) *)
3651(* *)
3652(* Both sides are put into the ALT form; what is left to prove is *)
3653(* (?f. !x y. P x y <=> f x = y) <=> (?g. !h. (!x. P x (h x)) <=> g = h) *)
3654(* whose right-to-left half is the one that has to perturb a Skolem *)
3655(* function at a single point. *)
3656(* ------------------------------------------------------------------------- *)
3657
3658val UNIQUE_SKOLEM_THM = thm (#(FILE), #(LINE))("UNIQUE_SKOLEM_THM",
3659 let val P = mk_var("P", alpha --> beta --> bool)
3660 val x = mk_var("x", alpha)
3661 val z = mk_var("z", alpha)
3662 val y = mk_var("y", beta)
3663 val f = mk_var("f", alpha --> beta)
3664 val g = mk_var("g", alpha --> beta)
3665 val h = mk_var("h", alpha --> beta)
3666 fun Pap s t = mk_comb(mk_comb(P,s),t)
3667 fun pointwise k = mk_forall(x, Pap x (mk_comb(k,x)))
3668 val condths = INST_TYPE [alpha |-> beta] COND_CLAUSES
3669 fun COND_T l r = CONJUNCT1 (SPECL [l,r] condths)
3670 fun COND_F l r = CONJUNCT2 (SPECL [l,r] condths)
3671 val Abody = mk_forall(x, mk_forall(y, mk_eq(Pap x y,
3672 mk_eq(mk_comb(f,x), y))))
3673 val A = mk_exists(f, Abody)
3674 val Bbody = mk_forall(h, mk_eq(pointwise h, mk_eq(g,h)))
3675 val B = mk_exists(g, Bbody)
3676 (* left to right: the Skolem function is the unique one *)
3677 val af = ASSUME Abody
3678 val d1 =
3679 let val ph = pointwise h
3680 val feqh = mk_eq(f,h)
3681 val eqv = SPECL [x, mk_comb(h,x)] af
3682 val d1a = DISCH ph
3683 (EQ_MP (SYM (SPECL [f,h] FUN_EQ_THM))
3684 (GEN x (EQ_MP eqv (SPEC x (ASSUME ph)))))
3685 val d1b = DISCH feqh
3686 (GEN x (EQ_MP (SYM eqv) (AP_THM (ASSUME feqh) x)))
3687 in
3688 DISCH A (CHOOSE (f, ASSUME A)
3689 (EXISTS (B,f) (GEN h (IMP_ANTISYM_RULE d1a d1b))))
3690 end
3691 (* right to left: a unique Skolem function pins down each point *)
3692 val bg = ASSUME Bbody
3693 val Rg = EQ_MP (SYM (SPEC g bg)) (REFL g)
3694 val d2 =
3695 let val gxy = mk_eq(mk_comb(g,x), y)
3696 val pxy = Pap x y
3697 val d2b = DISCH gxy (SUBS [ASSUME gxy] (SPEC x Rg))
3698 (* h is g, moved to y at x; it is pointwise good, so it is g *)
3699 val hdef = mk_abs(z, mk_cond{cond = mk_eq(z,x), larm = y,
3700 rarm = mk_comb(g,z)})
3701 val zeqx = mk_eq(z,x)
3702 val betaz = BETA_CONV (mk_comb(hdef,z))
3703 val thT =
3704 let val asm = ASSUME (mk_eq(zeqx,“T”))
3705 val hz = TRANS (SUBS [asm] betaz) (COND_T y (mk_comb(g,z)))
3706 val pzy = EQ_MP (SYM (AP_THM (AP_TERM P (EQT_ELIM asm)) y))
3707 (ASSUME pxy)
3708 in SUBS [SYM hz] pzy
3709 end
3710 val thF =
3711 let val asm = ASSUME (mk_eq(zeqx,“F”))
3712 val hz = TRANS (SUBS [asm] betaz) (COND_F y (mk_comb(g,z)))
3713 in SUBS [SYM hz] (SPEC z Rg)
3714 end
3715 val geqh = EQ_MP (SPEC hdef bg)
3716 (GEN z (DISJ_CASES (SPEC zeqx BOOL_CASES_AX) thT thF))
3717 val hx = TRANS (SUBS [EQT_INTRO (REFL x)]
3718 (BETA_CONV (mk_comb(hdef,x))))
3719 (COND_T y (mk_comb(g,x)))
3720 val d2a = DISCH pxy (TRANS (AP_THM geqh x) hx)
3721 in
3722 DISCH B (CHOOSE (g, ASSUME B)
3723 (EXISTS (A,g) (GENL [x,y] (IMP_ANTISYM_RULE d2a d2b))))
3724 end
3725 (* both sides in ALT form *)
3726 val lhs_alt = SPEC P UNIQUE_SKOLEM_ALT
3727 val rhs_alt =
3728 let val Pf = mk_abs(f, pointwise f)
3729 val th0 = SPEC Pf (INST_TYPE [alpha |-> (alpha --> beta)]
3730 EXISTS_UNIQUE_ALT)
3731 val (l0,r0) = dest_eq (concl th0)
3732 in
3733 TRANS (SYM (QUANT_CONV BETA_CONV l0))
3734 (TRANS th0 (QUANT_CONV
3735 (QUANT_CONV (RATOR_CONV (RAND_CONV BETA_CONV)))
3736 r0))
3737 end
3738 val th = TRANS lhs_alt (TRANS (IMP_ANTISYM_RULE d1 d2) (SYM rhs_alt))
3739 val target = mk_eq(mk_forall(x, mk_exists1(y, Pap x y)),
3740 mk_exists1(f, pointwise f))
3741 in
3742 GEN P (EQ_MP (ALPHA (concl th) target) th)
3743 end);
3744
3745(*---------------------------------------------------------------------------
3746 Support for pattern matching on booleans.
3747
3748 bool_case_thm =
3749 |- (!e0 e1. bool_case e0 e1 T = e0) /\
3750 !e0 e1. bool_case e0 e1 F = e1
3751 ---------------------------------------------------------------------------*)
3752
3753val bool_case_thm = let
3754 val (vs,_) = strip_forall (concl COND_CLAUSES)
3755in
3756 thm (#(FILE), #(LINE))("bool_case_thm",
3757 COND_CLAUSES |> SPECL vs |> CONJUNCTS |> map (GENL vs) |> LIST_CONJ)
3758end
3759
3760
3761(*---------------------------------------------------------------------------
3762 bool_case_eq =
3763 |- (bool_case t1 t2 x = v) <=>
3764 (x <=> T) /\ t1 = v \/ (x <=> F) /\ t2 = v
3765 ---------------------------------------------------------------------------*)
3766val bool_case_eq = thm (#(FILE), #(LINE))("bool_case_eq",
3767let val x = “x:bool”
3768 val t1 = “t1:'a”
3769 val t2 = “t2:'a”
3770 val v = “v:'a”
3771 val eq = “$=”
3772 val conj = “$/\”
3773 val disj = “$\/”
3774 val tm1 = “t1 = v”
3775 val tm2 = “t2 = v”
3776 val [COND1, COND2] = (CONJUNCTS (SPEC t2 (SPEC t1 COND_CLAUSES)))
3777 and [OR1,OR2,OR3,OR4,_] = map GEN_ALL (CONJUNCTS (SPEC_ALL OR_CLAUSES))
3778 and [AND1,AND2,AND3,AND4,_] = map GEN_ALL (CONJUNCTS(SPEC_ALL AND_CLAUSES))
3779 val thmT1 = AP_THM (AP_TERM eq COND1) v
3780 val thmF1 = AP_THM (AP_TERM eq COND2) v
3781 val [TF,FT] = map EQF_INTRO (CONJUNCTS BOOL_EQ_DISTINCT)
3782 val [TT,FF] = map (EQT_INTRO o REFL) [“T”,“F”]
3783 val thmT2 =
3784 let
3785 val thml1 = AP_THM (AP_TERM conj TT) tm1
3786 val thml2 = SPEC tm1 AND1
3787 val thml = TRANS thml1 thml2
3788 val thmr1 = AP_THM (AP_TERM conj TF) tm2
3789 val thmr2 = SPEC tm2 AND3
3790 val thmr = TRANS thmr1 thmr2
3791 val thm1 = MK_COMB (AP_TERM disj thml, thmr)
3792 in
3793 TRANS thm1 (SPEC tm1 OR4)
3794 end
3795 val thmF2 =
3796 let
3797 val thmr1 = AP_THM (AP_TERM conj FF) tm2
3798 val thmr2 = SPEC tm2 AND1
3799 val thmr = TRANS thmr1 thmr2
3800 val thml1 = AP_THM (AP_TERM conj FT) tm1
3801 val thml2 = SPEC tm1 AND3
3802 val thml = TRANS thml1 thml2
3803 val thm1 = MK_COMB (AP_TERM disj thml, thmr)
3804 in
3805 TRANS thm1 (SPEC tm2 OR3)
3806 end
3807 val thmT3 = TRANS thmT1 (SYM thmT2)
3808 val thmF3 = TRANS thmF1 (SYM thmF2)
3809 val tm = “(if x then t1 else t2) = v <=>
3810 (((x <=> T) /\ t1 = v) \/ ((x <=> F) /\ t2 = v))”
3811 val thT4 = SUBST_CONV [x |-> ASSUME “x = T”] tm tm
3812 and thF4 = SUBST_CONV [x |-> ASSUME “x = F”] tm tm
3813 val thmT = EQ_MP (SYM thT4) thmT3
3814 val thmF = EQ_MP (SYM thF4) thmF3
3815 in
3816 DISJ_CASES (SPEC x BOOL_CASES_AX) thmT thmF
3817 end);
3818
3819(* ------------------------------------------------------------------------- *)
3820(* bool_case_ID = |- !x. (x => T | F) = x *)
3821(* ------------------------------------------------------------------------- *)
3822val bool_case_ID = thm (#(FILE), #(LINE))("bool_case_ID",
3823let val x = “x:bool”
3824 val (CONDT,CONDF) = INST_TYPE [alpha |-> bool] COND_CLAUSES
3825 |> SPECL [T,F]
3826 |> CONJ_PAIR
3827 val tm = “(if x then T else F) = x”
3828 val thT1 = SUBST_CONV [x |-> ASSUME “x = T”] tm tm
3829 val thF1 = SUBST_CONV [x |-> ASSUME “x = F”] tm tm
3830 val thmT = EQ_MP (SYM thT1) CONDT
3831 val thmF = EQ_MP (SYM thF1) CONDF
3832in
3833 GEN x (DISJ_CASES (SPEC x BOOL_CASES_AX) thmT thmF)
3834end);
3835(* ------------------------------------------------------------------------- *)
3836(* bool_case_CONST = |- !x b. bool_case x x b = x *)
3837(* ------------------------------------------------------------------------- *)
3838
3839val bool_case_CONST = thm (#(FILE), #(LINE))("bool_case_CONST", COND_ID)
3840
3841
3842(* ------------------------------------------------------------------------- *)
3843(* boolAxiom |- !e0 e1. ?fn. (fn T = e0) /\ (fn F = e1) *)
3844(* ------------------------------------------------------------------------- *)
3845
3846val boolAxiom = thm (#(FILE), #(LINE))("boolAxiom",
3847 let
3848 val ([e0,e1], _) = strip_forall (concl COND_CLAUSES)
3849 val (th2, th3) = CONJ_PAIR (SPECL [e0, e1] COND_CLAUSES)
3850 val f_t = “\b. if b then ^e0 else ^e1”
3851 val f_T = TRANS (BETA_CONV (mk_comb(f_t, T))) th2
3852 val f_F = TRANS (BETA_CONV (mk_comb(f_t, F))) th3
3853 val th4 = CONJ f_T f_F
3854 val th5 = EXISTS (“?fn. (fn T = ^e0) /\ (fn F = ^e1)”, f_t) th4
3855 in
3856 GEN e0 (GEN e1 th5)
3857 end);
3858
3859(* ------------------------------------------------------------------------- *)
3860(* bool_INDUCT |- !P. P T /\ P F ==> !b. P b *)
3861(* ------------------------------------------------------------------------- *)
3862
3863val bool_INDUCT = thm (#(FILE), #(LINE))("bool_INDUCT",
3864 let val P = “P:bool -> bool”
3865 val b = “b:bool”
3866 val v = “v:bool”
3867 val tm1 = “^P T /\ ^P F”
3868 val th1 = SPEC b BOOL_CASES_AX
3869 val th2 = ASSUME tm1
3870 val th3 = CONJUNCT1 th2
3871 val th4 = CONJUNCT2 th2
3872 val th5 = ASSUME “b = T”
3873 val th6 = ASSUME “b = F”
3874 val th7 = SUBST [v |-> SYM th5] “^P ^v” th3
3875 val th8 = SUBST [v |-> SYM th6] “^P ^v” th4
3876 val th9 = GEN b (DISJ_CASES th1 th7 th8)
3877 in
3878 GEN P (DISCH tm1 th9)
3879 end);
3880
3881(* ---------------------------------------------------------------------------
3882 |- !P Q x x' y y'.
3883 (P = Q) /\ (Q ==> (x = x')) /\ (~Q ==> (y = y')) ==>
3884 ((case P of T -> x || F -> y) = (case Q of T -> x' || F -> y'))
3885 --------------------------------------------------------------------------- *)
3886
3887val bool_case_CONG = thm (#(FILE), #(LINE))("bool_case_CONG", COND_CONG)
3888
3889val FORALL_BOOL = thm (#(FILE), #(LINE))
3890("FORALL_BOOL",
3891 let val tm1 = “!b:bool. P b”
3892 val tm2 = “P T /\ P F”
3893 val th1 = ASSUME tm1
3894 val th2 = CONJ (SPEC T th1) (SPEC F th1)
3895 val th3 = DISCH tm1 th2
3896 val th4 = ASSUME tm2
3897 val th5 = MP (SPEC “P:bool->bool” bool_INDUCT) th4
3898 val th6 = DISCH tm2 th5
3899 in
3900 IMP_ANTISYM_RULE th3 th6
3901 end);
3902
3903
3904(*---------------------------------------------------------------------------
3905 Results about Unique existence.
3906 ---------------------------------------------------------------------------*)
3907
3908local
3909 val LAND_CONV = RATOR_CONV o RAND_CONV
3910 val P = mk_var("P", Type.alpha --> Type.bool)
3911 val p = mk_var("p", Type.bool)
3912 val q = mk_var("q", Type.bool)
3913 val Q = mk_var("Q", Type.alpha --> Type.bool)
3914 val x = mk_var("x", Type.alpha)
3915 val y = mk_var("y", Type.alpha)
3916 val Px = mk_comb(P, x)
3917 val Py = mk_comb(P, y)
3918 val Qx = mk_comb(Q, x)
3919 val Qy = mk_comb(Q, y)
3920 val uex_t = mk_const("?!", (alpha --> bool) --> bool)
3921 val exP = mk_exists(x, Px)
3922 val exQ = mk_exists(x, Qx)
3923 val uexP = mk_exists1(x, Px)
3924 val uexQ = mk_exists1(x, Qx)
3925 val pseudo_mp = let
3926 val lhs_t = mk_conj(p, mk_imp(p, q))
3927 val rhs_t = mk_conj(p, q)
3928 val lhs_thm = ASSUME lhs_t
3929 val (p_thm, pimpq) = CONJ_PAIR lhs_thm
3930 val dir1 = DISCH_ALL (CONJ p_thm (MP pimpq p_thm))
3931 val rhs_thm = ASSUME rhs_t
3932 val (p_thm, q_thm) = CONJ_PAIR rhs_thm
3933 val dir2 = DISCH_ALL (CONJ p_thm (DISCH p q_thm))
3934 in
3935 IMP_ANTISYM_RULE dir1 dir2
3936 end
3937in
3938 val UEXISTS_OR_THM = let
3939 val subdisj_t = mk_abs(x, mk_disj(Px, Qx))
3940 val lhs_t = mk_comb(uex_t, subdisj_t)
3941 val lhs_thm = ASSUME lhs_t
3942 val lhs_eq = AP_THM EXISTS_UNIQUE_DEF subdisj_t
3943 val lhs_expanded = CONV_RULE BETA_CONV (EQ_MP lhs_eq lhs_thm)
3944 val (expq0, univ) = CONJ_PAIR lhs_expanded
3945 val expq = EQ_MP (SPEC_ALL EXISTS_OR_THM) expq0
3946 val univ1 = SPEC_ALL univ
3947 val univ2 = CONV_RULE (LAND_CONV (LAND_CONV BETA_CONV)) univ1
3948 val univ3 = CONV_RULE (LAND_CONV (RAND_CONV BETA_CONV)) univ2
3949 val P_half = let
3950 val asm = ASSUME (mk_conj(Px,Py))
3951 val (Px_thm, Py_thm) = CONJ_PAIR asm
3952 val PxQx_thm = DISJ1 Px_thm Qx
3953 val PyQy_thm = DISJ1 Py_thm Qy
3954 val resolvent = CONJ PxQx_thm PyQy_thm
3955 val rhs =
3956 GENL [x,y]
3957 (DISCH (mk_conj(Px,Py)) (PROVE_HYP resolvent (UNDISCH univ3)))
3958 in
3959 DISJ1 (EQ_MP (SYM EXISTS_UNIQUE_THM) (CONJ (ASSUME exP) rhs)) uexQ
3960 end
3961 val Q_half = let
3962 val asm = ASSUME (mk_conj(Qx,Qy))
3963 val (Qx_thm, Qy_thm) = CONJ_PAIR asm
3964 val PxQx_thm = DISJ2 Px Qx_thm
3965 val PyQy_thm = DISJ2 Py Qy_thm
3966 val resolvent = CONJ PxQx_thm PyQy_thm
3967 val rhs =
3968 GENL [x,y]
3969 (DISCH (mk_conj(Qx,Qy)) (PROVE_HYP resolvent (UNDISCH univ3)))
3970 val uex_expanded = SYM (INST [P |-> Q] EXISTS_UNIQUE_THM)
3971 in
3972 DISJ2 uexP (EQ_MP uex_expanded (CONJ (ASSUME exQ) rhs))
3973 end
3974 in
3975 thm (#(FILE), #(LINE))(
3976 "UEXISTS_OR_THM",
3977 GENL [P, Q] (DISCH_ALL (DISJ_CASES expq P_half Q_half))
3978 )
3979 end;
3980
3981 val UEXISTS_SIMP = let
3982 fun mCONV_RULE c thm = TRANS thm (c (rhs (concl thm)))
3983 val xeqy = mk_eq(x,y)
3984 val t = mk_var("t", bool)
3985 val abst = mk_abs(x, t)
3986 val uext_t = mk_exists1(x,t)
3987 val exp0 = AP_THM EXISTS_UNIQUE_DEF abst
3988 val exp1 = mCONV_RULE BETA_CONV exp0
3989 val exp2 = mCONV_RULE (LAND_CONV (K (SPEC t EXISTS_SIMP))) exp1
3990 val exp3 =
3991 mCONV_RULE (RAND_CONV
3992 (QUANT_CONV
3993 (QUANT_CONV (LAND_CONV (LAND_CONV BETA_CONV))))) exp2
3994 val exp4 =
3995 mCONV_RULE (RAND_CONV
3996 (QUANT_CONV
3997 (QUANT_CONV (LAND_CONV (RAND_CONV BETA_CONV))))) exp3
3998 val exp5 =
3999 mCONV_RULE (RAND_CONV
4000 (QUANT_CONV
4001 (QUANT_CONV (LAND_CONV (K (SPEC t AND_CLAUSE5)))))) exp4
4002 val pushy0 =
4003 SPECL [t, mk_abs(y,xeqy)]
4004 RIGHT_FORALL_IMP_THM
4005 val pushy1 =
4006 CONV_RULE (LAND_CONV (QUANT_CONV (RAND_CONV BETA_CONV))) pushy0
4007 val pushy2 =
4008 CONV_RULE (RAND_CONV (RAND_CONV (QUANT_CONV BETA_CONV))) pushy1
4009 val exp6 =
4010 mCONV_RULE (RAND_CONV (QUANT_CONV (K pushy2))) exp5
4011 val pushx0 = SPECL [t, mk_abs(x, mk_forall(y,xeqy))]
4012 RIGHT_FORALL_IMP_THM
4013 val pushx1 =
4014 CONV_RULE (LAND_CONV (QUANT_CONV (RAND_CONV BETA_CONV))) pushx0
4015 val pushx2 =
4016 CONV_RULE (RAND_CONV (RAND_CONV (QUANT_CONV BETA_CONV))) pushx1
4017 val exp7 =
4018 mCONV_RULE (RAND_CONV (K pushx2)) exp6
4019 val mp' = Thm.INST [p |-> t, q |-> list_mk_forall [x,y] xeqy] pseudo_mp
4020 in
4021 thm (#(FILE), #(LINE))("UEXISTS_SIMP", mCONV_RULE (K mp') exp7)
4022 end
4023end
4024
4025
4026(*---------------------------------------------------------------------------
4027 The definition of restricted abstraction.
4028 ---------------------------------------------------------------------------*)
4029
4030val RES_ABSTRACT_EXISTS =
4031 let
4032 fun B_CONV n = funpow n RATOR_CONV BETA_CONV
4033 fun RHS th = rhs (concl th)
4034 val p = “p : 'a -> bool”
4035 val m = “m : 'a -> 'b”
4036 val m1 = “m1 : 'a -> 'b”
4037 val m2 = “m2 : 'a -> 'b”
4038 val x = “x : 'a”
4039 val witness = “\p m x. if x IN p then ^m x else ARB x”
4040 val A1 = B_CONV 2 “^witness ^p ^m ^x”
4041 val A2 = TRANS A1 (B_CONV 1 (RHS A1))
4042 val A3 = TRANS A2 (BETA_CONV (RHS A2))
4043 val A4 = EQT_INTRO (ASSUME “^x IN ^p”)
4044 val A5 = RATOR_CONV (RATOR_CONV (RAND_CONV (K A4))) (RHS A3)
4045 val A6 = INST_TYPE [alpha |-> beta] COND_CLAUSE1
4046 val A7 = SPECL [“^m ^x”, “ARB ^x : 'b”] A6
4047 val A8 = DISCH “^x IN ^p” (TRANS (TRANS A3 A5) A7)
4048 val A9 = GENL [“^p”, “^m”, “^x”] A8
4049 (* Completed the first clause of the definition *)
4050 val B1 = SPEC “^x IN ^p” EXCLUDED_MIDDLE
4051 val B2 = UNDISCH A8
4052 val B3 = INST [m |-> m1] B2
4053 val B4 = INST [m |-> m2] B2
4054 val B5 = SPEC_ALL (ASSUME “!x. x IN ^p ==> (^m1 x = ^m2 x)”)
4055 val B6 = TRANS B3 (TRANS (UNDISCH B5) (SYM B4))
4056 val B7 = INST [m |-> m1] A3
4057 val B8 = INST [m |-> m2] A3
4058 val B9 = SYM (SPEC “^x IN ^p” EQ_CLAUSE4)
4059 val B10 = EQ_MP B9 (ASSUME “~(^x IN ^p)”)
4060 val B11 = INST_TYPE [alpha |-> beta] COND_CLAUSE2
4061 val B12 = RATOR_CONV (RATOR_CONV (RAND_CONV (K B10))) (RHS B7)
4062 val B13 = TRANS B12 (SPECL [“^m1 ^x”, “ARB ^x : 'b”] B11)
4063 val B14 = RATOR_CONV (RATOR_CONV (RAND_CONV (K B10))) (RHS B8)
4064 val B15 = TRANS B14 (SPECL [“^m2 ^x”, “ARB ^x : 'b”] B11)
4065 val B16 = TRANS (TRANS B7 B13) (SYM (TRANS B8 B15))
4066 val B17 = DISJ_CASES B1 B6 B16
4067 val B18 = ABS x B17
4068 val B19 = CONV_RULE (RATOR_CONV (RAND_CONV ETA_CONV)) B18
4069 val B20 = CONV_RULE (RAND_CONV ETA_CONV) B19
4070 val B21 = DISCH “!x. x IN ^p ==> (^m1 x = ^m2 x)” B20
4071 val B22 = GENL [p, m1, m2] B21
4072 (* Cleaning up *)
4073 val C1 = CONJ A9 B22
4074 val C2 = EXISTS
4075 (“?f.
4076 (!p (m : 'a -> 'b) x. x IN p ==> (f p m x = m x)) /\
4077 (!p m1 m2.
4078 (!x. x IN p ==> (m1 x = m2 x)) ==> (f p m1 = f p m2))”,
4079 “\p (m : 'a -> 'b) x. (if x IN p then m x else ARB x)”) C1
4080 in
4081 C2
4082 end;
4083
4084val RES_ABSTRACT_DEF =
4085 Definition.new_specification
4086 ("RES_ABSTRACT_DEF", ["RES_ABSTRACT"], RES_ABSTRACT_EXISTS);
4087
4088val _ = associate_restriction ("\\", "RES_ABSTRACT");
4089
4090
4091val (RES_FORALL_THM, RES_EXISTS_THM, RES_EXISTS_UNIQUE_THM, RES_SELECT_THM) =
4092 let
4093 val Pf = map (fn s => mk_var(s, alpha --> bool)) ["P", "f"]
4094 fun mk_eq th =
4095 GENL Pf (List.foldl (RIGHT_BETA o uncurry (C AP_THM)) th Pf)
4096 in
4097 (thm (#(FILE), #(LINE))("RES_FORALL_THM", mk_eq RES_FORALL_DEF),
4098 thm (#(FILE), #(LINE))("RES_EXISTS_THM", mk_eq RES_EXISTS_DEF),
4099 thm (#(FILE), #(LINE))("RES_EXISTS_UNIQUE_THM",
4100 mk_eq RES_EXISTS_UNIQUE_DEF),
4101 thm (#(FILE), #(LINE))("RES_SELECT_THM", mk_eq RES_SELECT_DEF))
4102 end
4103
4104
4105(* (!x::P. T) = T *)
4106val RES_FORALL_TRUE = let
4107 val x = mk_var("x", alpha)
4108 val T = concl TRUTH
4109 val KT = mk_abs(x, T)
4110 val P = mk_var("P", alpha --> bool)
4111 val th0 = SPECL[P,KT] RES_FORALL_THM
4112 val th1 = CONV_RULE (RAND_CONV (QUANT_CONV (RAND_CONV BETA_CONV))) th0
4113 val xINP_t = (rand o rator o #2 o dest_forall o rhs o concl) th1
4114 val timpT_th = List.nth(CONJUNCTS (SPEC xINP_t IMP_CLAUSES), 1)
4115 val th2 = CONV_RULE (RAND_CONV (QUANT_CONV (K timpT_th))) th1
4116in
4117 thm (#(FILE), #(LINE))("RES_FORALL_TRUE", TRANS th2 (SPEC T FORALL_SIMP))
4118end
4119
4120(* (?x::P. F) = F *)
4121val RES_EXISTS_FALSE = let
4122 val x = mk_var("x", alpha)
4123 val F = prim_mk_const{Thy = "bool", Name = "F"}
4124 val KF = mk_abs(x, F)
4125 val P = mk_var("P", alpha --> bool)
4126 val th0 = SPECL [P, KF] RES_EXISTS_THM
4127 val th1 = CONV_RULE (RAND_CONV (QUANT_CONV (RAND_CONV BETA_CONV))) th0
4128 val xINP_t = (rand o rator o #2 o dest_exists o rhs o concl) th1
4129 val tandF_th = List.nth(CONJUNCTS (SPEC xINP_t AND_CLAUSES), 3)
4130 val th2 = CONV_RULE (RAND_CONV (QUANT_CONV (K tandF_th))) th1
4131in
4132 thm (#(FILE), #(LINE))("RES_EXISTS_FALSE", TRANS th2 (SPEC F EXISTS_SIMP))
4133end
4134
4135(*---------------------------------------------------------------------------
4136 From Joe Hurd : case analysis on the (4) functions in the
4137 type :bool -> bool.
4138
4139 val BOOL_FUN_CASES_THM =
4140 |- !f. (f = \b. T) \/ (f = \b. F) \/ (f = \b. b) \/ (f = \b. ~b)
4141 ---------------------------------------------------------------------------*)
4142
4143val BOOL_FUN_CASES_THM =
4144 let val x = mk_var("x",bool)
4145 val f = mk_var("f",bool-->bool)
4146 val KF = “\b:bool.F”
4147 val KT = “\b:bool.T”
4148 val Ibool = “\b:bool.b”
4149 val dual = “\b. ~b”
4150 val fT = mk_comb(f,T)
4151 val fF = mk_comb(f,F)
4152 val fT_eq_T = mk_eq(fT,T)
4153 val fF_eq_T = mk_eq(fF,T)
4154 val fT_eq_F = mk_eq(fT,F)
4155 val fF_eq_F = mk_eq(fF,F)
4156 val final = “(f = ^KT) \/ (f = ^KF) \/ (f = ^Ibool) \/ (f = ^dual)”
4157 val a0 = TRANS (ASSUME fT_eq_T) (SYM (BETA_CONV (mk_comb(KT,T))))
4158 val a1 = TRANS (ASSUME fF_eq_T) (SYM (BETA_CONV (mk_comb(KT,F))))
4159 val a2 = BOOL_CASE “f x = ^KT x” x x a0 a1
4160 val a3 = EXT (GEN x a2)
4161 val a = DISJ1 a3 “(f = \b. F) \/ (f = \b. b) \/ (f = \b. ~b)”
4162 val b0 = TRANS (ASSUME fT_eq_F) (SYM (BETA_CONV (mk_comb(KF,T))))
4163 val b1 = TRANS (ASSUME fF_eq_F) (SYM (BETA_CONV (mk_comb(KF,F))))
4164 val b2 = BOOL_CASE “f x = ^KF x” x x b0 b1
4165 val b3 = EXT (GEN x b2)
4166 val b4 = DISJ1 b3 “(f = ^Ibool) \/ (f = \b. ~b)”
4167 val b = DISJ2 “f = ^KT” b4
4168 val c0 = TRANS (ASSUME fT_eq_T) (SYM (BETA_CONV (mk_comb(Ibool,T))))
4169 val c1 = TRANS (ASSUME fF_eq_F) (SYM (BETA_CONV (mk_comb(Ibool,F))))
4170 val c2 = BOOL_CASE “f x = ^Ibool x” x x c0 c1
4171 val c3 = EXT (GEN x c2)
4172 val c4 = DISJ1 c3 “f = ^dual”
4173 val c5 = DISJ2 “f = ^KF” c4
4174 val c = DISJ2 “f = ^KT” c5
4175 val d0 = TRANS (ASSUME fT_eq_F)
4176 (TRANS (SYM (CONJUNCT1 (CONJUNCT2 NOT_CLAUSES)))
4177 (SYM (BETA_CONV (mk_comb(dual,T)))))
4178 val d1 = TRANS (ASSUME fF_eq_T)
4179 (TRANS (SYM (CONJUNCT2 (CONJUNCT2 NOT_CLAUSES)))
4180 (SYM (BETA_CONV (mk_comb(dual,F)))))
4181 val d2 = BOOL_CASE “f x = ^dual x” x x d0 d1
4182 val d3 = EXT (GEN x d2)
4183 val d4 = DISJ2 “f = ^Ibool” d3
4184 val d5 = DISJ2 “f = ^KF” d4
4185 val d = DISJ2 “f = ^KT” d5
4186 val ad0 = DISCH fT_eq_T a
4187 val ad1 = DISCH fT_eq_F d
4188 val ad2 = BOOL_CASE “(f T = x) ==> ^final” x x ad0 ad1
4189 val ad3 = SPEC fT (GEN x ad2)
4190 val ad = MP ad3 (REFL fT)
4191 val bc0 = DISCH fT_eq_T c
4192 val bc1 = DISCH fT_eq_F b
4193 val bc2 = BOOL_CASE “(f T = x) ==> ^final” x x bc0 bc1
4194 val bc3 = SPEC fT (GEN x bc2)
4195 val bc = MP bc3 (REFL fT)
4196 val abcd0 = DISCH fF_eq_T ad
4197 val abcd1 = DISCH fF_eq_F bc
4198 val abcd2 = BOOL_CASE “(f F = x) ==> ^final” x x abcd0 abcd1
4199 val abcd3 = SPEC fF (GEN x abcd2)
4200 val abcd = MP abcd3 (REFL fF)
4201in
4202 thm (#(FILE), #(LINE))("BOOL_FUN_CASES_THM", GEN f abcd)
4203end;
4204
4205(*---------------------------------------------------------------------------
4206 Another from Joe Hurd : consequence of BOOL_FUN_CASES_THM
4207
4208 BOOL_FUN_INDUCT =
4209 |- !P. P (\b. T) /\ P (\b. F) /\ P (\b. b) /\ P (\b. ~b) ==> !f. P f
4210 ---------------------------------------------------------------------------*)
4211
4212 fun or_imp th0 =
4213 let val (disj1, disj2) = dest_disj (concl th0)
4214 val th1 = SYM (SPEC disj1 (CONJUNCT1 NOT_CLAUSES))
4215 val th2 = MK_COMB (REFL disjunction, th1)
4216 val th3 = MK_COMB (th2, REFL disj2)
4217 val th4 = EQ_MP th3 th0
4218 val th5 = SYM (SPECL [mk_neg disj1, disj2] IMP_DISJ_THM)
4219 in
4220 EQ_MP th5 th4
4221 end
4222
4223 fun imp_and th0 =
4224 let val (ant, conseq) = dest_imp (concl th0)
4225 val (ant', conseq') = dest_imp conseq
4226 val th1 = SPECL [ant, ant', conseq'] AND_IMP_INTRO
4227 in
4228 EQ_MP th1 th0
4229 end
4230
4231
4232val BOOL_FUN_INDUCT =
4233 let val f = mk_var("f",bool-->bool)
4234 val g = mk_var("g",bool-->bool)
4235 val f_eq_g = mk_eq(f,g)
4236 val P = mk_var("P",(bool-->bool) --> bool)
4237 val KF = “\b:bool.F”
4238 val KT = “\b:bool.T”
4239 val Ibool = “\b:bool.b”
4240 val dual = “\b. ~b”
4241 val f0 = ASSUME (mk_neg(mk_comb(P,f)))
4242 val f1 = ASSUME (mk_neg(mk_neg(f_eq_g)))
4243 val f2 = EQ_MP (SPEC f_eq_g (CONJUNCT1 NOT_CLAUSES)) f1
4244 val f3 = MK_COMB (REFL P, f2)
4245 val f4 = MK_COMB (REFL negation, f3)
4246 val f5 = UNDISCH (NOT_ELIM (EQ_MP f4 f0))
4247 val f6 = CCONTR (mk_neg(f_eq_g)) f5
4248 val f7 = GEN g (DISCH (mk_comb(P,g)) f6)
4249 val a0 = SPEC f BOOL_FUN_CASES_THM
4250 val a1 = MP (or_imp a0) (UNDISCH (SPEC KT f7))
4251 val a2 = MP (or_imp a1) (UNDISCH (SPEC KF f7))
4252 val a3 = MP (or_imp a2) (UNDISCH (SPEC Ibool f7))
4253 val a = MP (NOT_ELIM (UNDISCH (SPEC dual f7))) a3
4254 val b0 = CCONTR (mk_comb(P,f)) a
4255 val b1 = GEN f b0
4256 val b2 = DISCH (mk_comb(P,dual)) b1
4257 val b3 = imp_and (DISCH (mk_comb(P,Ibool)) b2)
4258 val b4 = imp_and (DISCH (mk_comb(P,KF)) b3)
4259 val b = imp_and (DISCH (mk_comb(P,KT)) b4)
4260in
4261 thm (#(FILE), #(LINE))("BOOL_FUN_INDUCT", GEN P b)
4262end;
4263
4264(*---------------------------------------------------------------------------
4265 literal_case_THM = |- !f x. literal_case f x = f x
4266 ---------------------------------------------------------------------------*)
4267
4268val literal_case_THM = thm (#(FILE), #(LINE))("literal_case_THM",
4269 let val f = “f:'a->'b”
4270 val x = “x:'a”
4271 in
4272 GEN f (GEN x
4273 (RIGHT_BETA(AP_THM (RIGHT_BETA(AP_THM literal_case_DEF f)) x)))
4274 end);
4275
4276(*---------------------------------------------------------------------------*)
4277(* literal_case_RAND = *)
4278(* |- P (literal_case (\x. N x) M) = (literal_case (\x. P (N x)) M) *)
4279(*---------------------------------------------------------------------------*)
4280
4281val literal_case_RAND = thm (#(FILE), #(LINE))("literal_case_RAND",
4282 let val tm1 = “\x:'a. P (N x:'b):'c”
4283 val tm2 = “M:'a”
4284 val tm3 = “\x:'a. N x:'b”
4285 val P = “P:'b ->'c”
4286 val literal_case_THM1 = RIGHT_BETA (SPEC tm2 (SPEC tm1
4287 (Thm.INST_TYPE [beta |-> gamma] literal_case_THM)))
4288 val literal_case_THM2 =
4289 AP_TERM P (RIGHT_BETA (SPEC tm2 (SPEC tm3 literal_case_THM)))
4290 in TRANS literal_case_THM2 (SYM literal_case_THM1)
4291 end);
4292
4293(*---------------------------------------------------------------------------*)
4294(* literal_case_RATOR = *)
4295(* |- (literal_case (\x. N x) M) b = (literal_case (\x. N x b) M) *)
4296(*---------------------------------------------------------------------------*)
4297
4298val literal_case_RATOR = thm (#(FILE), #(LINE))("literal_case_RATOR",
4299 let val M = “M:'a”
4300 val b = “b:'b”
4301 val tm1 = “\x:'a. N x:'b->'c”
4302 val tm2 = “\x:'a. N x ^b:'c”
4303 val literal_case_THM1 =
4304 AP_THM
4305 (RIGHT_BETA
4306 (SPEC M (SPEC tm1
4307 (Thm.INST_TYPE [beta |-> (beta --> gamma)] literal_case_THM))))
4308 b
4309 val literal_case_THM2 = RIGHT_BETA (SPEC M (SPEC tm2
4310 (Thm.INST_TYPE [beta |-> gamma] literal_case_THM)))
4311 in TRANS literal_case_THM1 (SYM literal_case_THM2)
4312 end);
4313
4314(*---------------------------------------------------------------------------
4315 literal_case_CONG =
4316 |- !f g M N. (M = N) /\ (!x. (x = N) ==> (f x = g x))
4317 ==>
4318 (literal_case f M = literal_case g N)
4319 ---------------------------------------------------------------------------*)
4320
4321val literal_case_CONG = thm (#(FILE), #(LINE))("literal_case_CONG",
4322 let val f = mk_var("f",alpha-->beta)
4323 val g = mk_var("g",alpha-->beta)
4324 val M = mk_var("M",alpha)
4325 val N = mk_var("N",alpha)
4326 val x = mk_var ("x",alpha)
4327 val MeqN = mk_eq(M,N)
4328 val x_eq_N = mk_eq(x,N)
4329 val fx_eq_gx = mk_eq(mk_comb(f,x),mk_comb(g,x))
4330 val ctm = mk_forall(x, mk_imp(x_eq_N,fx_eq_gx))
4331 val th = RIGHT_BETA(AP_THM(RIGHT_BETA(AP_THM literal_case_DEF f)) M)
4332 val th1 = ASSUME MeqN
4333 val th2 = MP (SPEC N (ASSUME ctm)) (REFL N)
4334 val th3 = SUBS [SYM th1] th2
4335 val th4 = TRANS (TRANS th th3) (MK_COMB (REFL g,th1))
4336 val th5 = RIGHT_BETA(AP_THM(RIGHT_BETA(AP_THM literal_case_DEF g)) N)
4337 val th6 = TRANS th4 (SYM th5)
4338 val th7 = SUBS [SPECL [MeqN, ctm, concl th6] AND_IMP_INTRO]
4339 (DISCH MeqN (DISCH ctm th6))
4340 in
4341 GENL [f,g,M,N] th7
4342 end);
4343
4344(*---------------------------------------------------------------------------*)
4345(* Sometime useful rewrite, but you will want a higher-order version. *)
4346(* |- literal_case (\x. bool_case t u (x=a)) a = t *)
4347(*---------------------------------------------------------------------------*)
4348
4349val literal_case_id = thm (#(FILE), #(LINE))
4350("literal_case_id",
4351 let val a = mk_var("a", alpha)
4352 val x = mk_var("x", alpha)
4353 val t = mk_var("t",beta)
4354 val u = mk_var("u",beta)
4355 val eq = mk_eq(x,a)
4356 val bcase = inst [alpha |-> beta]
4357 (prim_mk_const{Name = "COND",Thy="bool"})
4358 val g = mk_abs(x,list_mk_comb(bcase,[eq, t, u]))
4359 val lit_thm = RIGHT_BETA(SPEC a (SPEC g literal_case_THM))
4360 val Teq = SYM (EQT_INTRO(REFL a))
4361 val ifT = CONJUNCT1(SPECL[t,u] (INST_TYPE[alpha |-> beta] COND_CLAUSES))
4362 val ifeq = SUBS [Teq] ifT
4363 in
4364 TRANS lit_thm ifeq
4365 end);
4366
4367(*---------------------------------------------------------------------------
4368 Support for parsing "case" expressions
4369 ---------------------------------------------------------------------------*)
4370
4371val _ = new_constant(GrammarSpecials.core_case_special,
4372 “:'a -> ('a -> 'b) -> 'b”);
4373val _ = new_constant(GrammarSpecials.case_split_special,
4374 “:('a -> 'b) -> ('a -> 'b) -> 'a -> 'b”);
4375val _ = new_constant(GrammarSpecials.case_arrow_special,
4376 “:'a -> 'b -> 'a -> 'b”);
4377
4378val _ = app (fn s => remove_ovl_mapping s {Name=s,Thy="bool"})
4379 [GrammarSpecials.case_split_special,
4380 GrammarSpecials.case_arrow_special]
4381
4382val _ = add_rule{pp_elements = [HardSpace 1, TOK "=>", BreakSpace(1,2)],
4383 fixity = Infix(NONASSOC, 12),
4384 (* allowing for insertion of .| infix at looser precedence
4385 level *)
4386 block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)),
4387 paren_style = OnlyIfNecessary,
4388 term_name = GrammarSpecials.case_arrow_special}
4389
4390val _ = add_rule{pp_elements = [PPBlock([TOK "case", BreakSpace(1,2),
4391 TM, BreakSpace(1,2), TOK "of"],
4392 (PP.CONSISTENT, 0)),
4393 BreakSpace(1,2)],
4394 fixity = Prefix 1,
4395 block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)),
4396 paren_style = Always,
4397 term_name = GrammarSpecials.core_case_special};
4398
4399val _ = add_rule{pp_elements = [PPBlock([TOK "case", BreakSpace(1,2),
4400 TM, BreakSpace(1,2), TOK "of"],
4401 (PP.CONSISTENT, 0)),
4402 BreakSpace(1,2), TM, BreakSpace(1,0),
4403 TOK "|", HardSpace 1],
4404 fixity = Prefix 1,
4405 block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)),
4406 paren_style = Always,
4407 term_name = GrammarSpecials.core_case_special};
4408
4409val _ = add_rule{pp_elements = [PPBlock([TOK "case", BreakSpace(1,2),
4410 TM, BreakSpace(1,2), TOK "of"],
4411 (PP.CONSISTENT, 0)),
4412 TOK "|", HardSpace 1],
4413 fixity = Prefix 1,
4414 block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)),
4415 paren_style = Always,
4416 term_name = GrammarSpecials.core_case_special};
4417
4418
4419val _ = add_rule{pp_elements = [PPBlock([TOK "case", BreakSpace(1,2),
4420 TM, BreakSpace(1,2), TOK "of"],
4421 (PP.CONSISTENT, 0)),
4422 BreakSpace(1,2), TM, BreakSpace(1,0),
4423 TOK "|", HardSpace 1, TM, BreakSpace(1,0),
4424 TOK "|", HardSpace 1],
4425 fixity = Prefix 1,
4426 block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)),
4427 paren_style = Always,
4428 term_name = GrammarSpecials.core_case_special};
4429
4430val BOUNDED_THM = thm (#(FILE), #(LINE))("BOUNDED_THM",
4431 let val v = “v:bool”
4432 in
4433 GEN v (RIGHT_BETA(AP_THM BOUNDED_DEF v))
4434 end);
4435
4436(*---------------------------------------------------------------------------*)
4437(* LCOMM_THM : derive "left-commutativity" from associativity and *)
4438(* commutativity. Used in permutative rewriting, e.g., simpLib entrypoints *)
4439(* *)
4440(* LCOMM_THM |- !f. (!x y. f x y = f y x) ==> *)
4441(* (!x y z. f x (f y z) = f (f x y) z) ==> *)
4442(* (!x y z. f x (f y z) = f y (f x z)) *)
4443(*---------------------------------------------------------------------------*)
4444
4445val LCOMM_THM = thm (#(FILE), #(LINE))("LCOMM_THM",
4446 let val x = mk_var("x",alpha)
4447 val y = mk_var("y",alpha)
4448 val z = mk_var("z",alpha)
4449 val f = mk_var("f",alpha --> alpha --> alpha)
4450 val comm = “!x y. ^f x y = f y x”
4451 val assoc = “!x y z. ^f x (f y z) = f (f x y) z”
4452 val comm_thm = ASSUME comm
4453 val assoc_thm = ASSUME assoc
4454 val th0 = SPEC (list_mk_comb(f,[y,z])) (SPEC x comm_thm)
4455 val th1 = SYM (SPECL [y,z,x] assoc_thm)
4456 val th2 = TRANS th0 th1
4457 val th3 = AP_TERM (mk_comb(f,y)) (SPECL[z,x] comm_thm)
4458 in
4459 GEN f (DISCH assoc (DISCH comm (GENL [x,y,z] (TRANS th2 th3))))
4460 end);
4461
4462
4463val DATATYPE_TAG_THM = thm (#(FILE), #(LINE))("DATATYPE_TAG_THM",
4464 let val x = mk_var("x",alpha)
4465 in GEN x (RIGHT_BETA (AP_THM DATATYPE_TAG_DEF x))
4466 end);
4467
4468
4469val DATATYPE_BOOL = thm (#(FILE), #(LINE))("DATATYPE_BOOL",
4470 let val thm1 = INST_TYPE [alpha |-> bool] DATATYPE_TAG_THM
4471 val bvar = mk_var("bool",bool--> bool-->bool)
4472 in
4473 SPEC (list_mk_comb(bvar,[T,F])) thm1
4474 end);
4475
4476(* ----------------------------------------------------------------------
4477 Set up the "itself" type constructor and its one value
4478 ---------------------------------------------------------------------- *)
4479
4480val ITSELF_TYPE_DEF = let
4481 val itself_exists = SPEC “ARB:'a” EXISTS_REFL
4482 val eq_sym_eq' =
4483 AP_TERM “$? :('a -> bool) -> bool”
4484 (ABS “x:'a” (SPECL [“x:'a”, “ARB:'a”] EQ_SYM_EQ))
4485in
4486 new_type_definition("itself", EQ_MP eq_sym_eq' itself_exists)
4487end
4488val _ = new_constant("the_value", “:'a itself”)
4489
4490(* prove uniqueness of the itself value:
4491 |- !i:'a itself. i = (:'a)
4492*)
4493val ITSELF_UNIQUE = let
4494 val typedef_asm = ASSUME (#2 (dest_exists (concl ITSELF_TYPE_DEF)))
4495 val typedef_eq0 =
4496 AP_THM (INST_TYPE [beta |-> “:'a itself”] TYPE_DEFINITION)
4497 “$= (ARB:'a)”
4498 val typedef_eq0 = RIGHT_BETA typedef_eq0
4499 val typedef_eq = AP_THM typedef_eq0 “rep:'a itself -> 'a”
4500 val typedef_eq = RIGHT_BETA typedef_eq
4501 val (typedef_11, typedef_onto) = CONJ_PAIR (EQ_MP typedef_eq typedef_asm)
4502 val onto' = INST [“x:'a” |-> “(rep:'a itself -> 'a) i”]
4503 (#2 (EQ_IMP_RULE (SPEC_ALL typedef_onto)))
4504 val allreps_arb = let
4505 val ex' = EXISTS (“?x':'a itself. rep i = rep x':'a”, “i:'a itself”)
4506 (REFL “(rep:'a itself -> 'a) i”)
4507 in
4508 SYM (MP onto' ex')
4509 end
4510 val allreps_repthevalue =
4511 TRANS allreps_arb
4512 (SYM (INST [“i:'a itself” |-> “bool$the_value”] allreps_arb))
4513 val all_eq_thevalue =
4514 GEN_ALL (MP (SPECL [“i:'a itself”, “bool$the_value”] typedef_11)
4515 allreps_repthevalue)
4516in
4517 thm (#(FILE), #(LINE))("ITSELF_UNIQUE",
4518 CHOOSE (“rep:'a itself -> 'a”, ITSELF_TYPE_DEF) all_eq_thevalue)
4519end
4520
4521(* ITSELF_EQN_RWT = |- f (:'a) = e <=> !x. f x = e *)
4522val ITSELF_EQN_RWT = let
4523 fun mk_itty ty = mk_thy_type{Args = [ty], Thy = "bool", Tyop = "itself"}
4524 val aitty = mk_itty alpha
4525 val f = mk_var("f", aitty --> beta)
4526 val e = mk_var("e", beta)
4527 val x = mk_var("x", aitty)
4528 val r = mk_forall(x, mk_eq(mk_comb(f,x), e))
4529 val itv = mk_thy_const{Name = "the_value", Thy = "bool", Ty = aitty}
4530 val l = mk_eq(mk_comb(f,itv), e)
4531 val r2l = SPEC itv (ASSUME r) |> DISCH r
4532 val l2r = SPEC x ITSELF_UNIQUE |> AP_TERM f |> C TRANS (ASSUME l) |> GEN x
4533 |> DISCH l
4534in
4535 thm (#(FILE), #(LINE))(
4536 "ITSELF_EQN_RWT",
4537 GENL [f,e] $ IMP_ANTISYM_RULE l2r r2l
4538 )
4539end
4540
4541(* prove a datatype axiom for the type, allowing definitions of the form
4542 f (:'a) = ...
4543*)
4544val itself_Axiom = let
4545 val witness = “(\x:'a itself. e : 'b)”
4546 val fn_behaves = BETA_CONV (mk_comb(witness, “(:'a)”))
4547 val fn_exists = EXISTS (“?f:'a itself -> 'b. f (:'a) = e”, witness)
4548 fn_behaves
4549in
4550 thm (#(FILE), #(LINE))("itself_Axiom", GEN_ALL fn_exists)
4551end
4552
4553(* prove induction *)
4554val itself_induction = let
4555 val pval = ASSUME “P (:'a) : bool”
4556 val pi =
4557 EQ_MP (SYM (AP_TERM “P:'a itself -> bool” (SPEC_ALL ITSELF_UNIQUE)))
4558 pval
4559in
4560 thm (#(FILE), #(LINE))("itself_induction", GEN_ALL (DISCH_ALL (GEN_ALL pi)))
4561end
4562
4563(* define case operator *)
4564val itself_case_thm = let
4565 val witness = “λ(i:'a itself) (b:'b). b”
4566 val witness_applied1 = BETA_CONV (mk_comb(witness, “(:'a)”))
4567 val witness_applied2 = RIGHT_BETA (AP_THM witness_applied1 “b:'b”)
4568in
4569 located_new_specification{
4570 name = "itself_case_thm",
4571 constnames = ["itself_case"],
4572 witness = EXISTS (“?f:'a itself -> 'b -> 'b. !b. f (:'a) b = b”, witness)
4573 (GEN_ALL witness_applied2),
4574 loc = mkloc(#(FILE), #(LINE)-5)
4575 }
4576end
4577Overload case = “itself_case”
4578
4579(* FORALL_itself : |- (!x:'a itself. P x) <=> P (:'a)
4580 EXISTS_itself : |- (?x:'a itself. P x) <=> P (:'a)
4581*)
4582local
4583 val P = mk_var("P", “:'a itself -> bool”)
4584 val x = mk_var("x", “:'a itself”)
4585 val Px = mk_comb(P, x)
4586 val APx = mk_forall(x, Px)
4587 val itself = “(:'a)”
4588 val Pitself = mk_comb(P, itself)
4589 val imp1 = APx |> ASSUME |> SPEC itself |> DISCH_ALL
4590 val unique = AP_TERM P (ITSELF_UNIQUE |> SPEC x |> SYM)
4591 val imp2 = EQ_MP unique (ASSUME Pitself) |> GEN x |> DISCH_ALL
4592 val fa = IMP_ANTISYM_RULE imp1 imp2
4593 val not_not = NOT_CLAUSES |> CONJUNCT1 |> SPEC Px
4594 (* exists half *)
4595 val imp1 = CHOOSE (x, ASSUME (mk_exists(x,Px)))
4596 (EQ_MP (SYM unique) (ASSUME Px)) |> DISCH_ALL
4597 val imp2 = EXISTS(mk_exists(x,Px),itself) (ASSUME Pitself) |> DISCH_ALL
4598in
4599 val FORALL_itself = thm (#(FILE), #(LINE))("FORALL_itself", fa)
4600 val EXISTS_itself = thm (#(FILE), #(LINE))
4601 ("EXISTS_itself", IMP_ANTISYM_RULE imp1 imp2)
4602end;
4603
4604
4605(*---------------------------------------------------------------------------*)
4606(* Pulling FORALL and EXISTS up through /\ and ==> *)
4607(*---------------------------------------------------------------------------*)
4608
4609local
4610 val flip = INST [Pb |-> Qb, Qab |-> Pab]
4611 val PULL_EXISTS1 = LEFT_FORALL_IMP_THM |> SPEC_ALL |> SYM
4612 val PULL_EXISTS2 = LEFT_EXISTS_AND_THM |> SPEC_ALL |> SYM
4613 val PULL_EXISTS3 = RIGHT_EXISTS_AND_THM |> SPEC_ALL |> SYM |> flip
4614 val PULL_FORALL1 = RIGHT_FORALL_IMP_THM |> SPEC_ALL |> SYM |> flip
4615 val PULL_FORALL2 = LEFT_AND_FORALL_THM |> SPEC_ALL
4616 val PULL_FORALL3 = RIGHT_AND_FORALL_THM |> SPEC_ALL |> flip
4617in
4618 val PULL_EXISTS = thm (#(FILE), #(LINE))("PULL_EXISTS",
4619 LIST_CONJ [PULL_EXISTS1, PULL_EXISTS2, PULL_EXISTS3] |> GENL [Pab, Qb])
4620 val PULL_FORALL = thm (#(FILE), #(LINE))("PULL_FORALL",
4621 LIST_CONJ [PULL_FORALL1, PULL_FORALL2, PULL_FORALL3] |> GENL [Pab, Qb])
4622end
4623
4624(*---------------------------------------------------------------------------*)
4625(* PEIRCE = |- ((P ==> Q) ==> P) ==> P *)
4626(*---------------------------------------------------------------------------*)
4627
4628val PEIRCE = thm (#(FILE), #(LINE))
4629("PEIRCE",
4630 let val th1 = ASSUME “(P ==> Q) ==> P”
4631 val th2 = ASSUME “P:bool”
4632 val th3 = ASSUME “~P”
4633 val th4 = MP th3 th2
4634 val th5 = MP (SPEC “Q:bool” FALSITY) th4
4635 val th6 = DISCH “P:bool” th5
4636 val th7 = MP th1 th6
4637 val th8 = MP th3 th7
4638 val th9 = DISCH “~P” th8
4639 val th10 = MP (SPEC “~P” IMP_F) th9
4640 val th11 = SUBS [SPEC “P:bool” (CONJUNCT1 NOT_CLAUSES)] th10
4641 in
4642 DISCH “(P ==> Q) ==> P” th11
4643 end);
4644
4645(* ----------------------------------------------------------------------
4646 JRH_INDUCT_UTIL : !P t. (!x. (x = t) ==> P x) ==> $? P
4647
4648 Used multiple times in places relevant to inductive definitions and/or
4649 algebraic types.
4650 ---------------------------------------------------------------------- *)
4651
4652val JRH_INDUCT_UTIL = let
4653 val asm_t = “!x:'a. (x = t) ==> P x”
4654 val asm = ASSUME asm_t
4655 val t = “t:'a”
4656 val P = “P : 'a -> bool”
4657 val Pt = MP (SPEC t asm) (REFL t)
4658 val ExPx = EXISTS (“?x:'a. P x”, t) Pt
4659 val P_eta = SPEC P (INST_TYPE [beta |-> bool] ETA_AX)
4660 val ExP_eta = AP_TERM “(?) : ('a -> bool) -> bool” P_eta
4661in
4662 thm (#(FILE), #(LINE))("JRH_INDUCT_UTIL",
4663 GENL [P, t] (DISCH asm_t (EQ_MP ExP_eta ExPx)))
4664end
4665
4666(* Parsing additions *)
4667(* not an element of *)
4668Overload NOTIN = “\x:'a y:('a -> bool). ~(x IN y)”
4669val _ = set_fixity "NOTIN" (Infix(NONASSOC, 425))
4670val _ = unicode_version {u = UChar.not_elementof, tmnm = "NOTIN"}
4671val _ = TeX_notation {hol="NOTIN", TeX = ("\\HOLTokenNotIn{}",1)}
4672val _ = TeX_notation {hol=UChar.not_elementof,
4673 TeX = ("\\HOLTokenNotIn{}",1)}
4674
4675(* not iff *)
4676Overload "<=/=>" = “$<> : bool -> bool -> bool”
4677val _ = set_fixity "<=/=>" (Infix(NONASSOC, 100))
4678val _ = unicode_version {u = UChar.not_iff, tmnm = "<=/=>"}
4679val _ = TeX_notation {hol="<=/=>", TeX = ("\\HOLTokenNotEquiv{}",3)}
4680val _ = TeX_notation {hol=UChar.not_iff,
4681 TeX = ("\\HOLTokenNotEquiv{}",3)}
4682
4683val _ = add_ML_dependency "boolpp"
4684val _ = add_user_printer ("bool.COND", “COND gd tr fl”)
4685val _ = add_user_printer ("bool.LET", “LET f x”)
4686val _ = add_absyn_postprocessor "bool.LET"
4687
4688(* |- |- !A B. A \/ B <=> ~A ==> B *)
4689val DISJ_EQ_IMP = thm (#(FILE), #(LINE))("DISJ_EQ_IMP",
4690 let
4691 val lemma = NOT_CLAUSES |> CONJUNCT1 |> SPEC ``A:bool``
4692 in
4693 IMP_DISJ_THM
4694 |> SPECL [``~A:bool``,``B:bool``]
4695 |> SYM
4696 |> CONV_RULE
4697 ((RATOR_CONV o RAND_CONV o RATOR_CONV o RAND_CONV)
4698 (fn tm => lemma))
4699 |> GENL [``A:bool``,``B:bool``]
4700 end);
4701
4702(* ------------------------------------------------------------------------- *)
4703(* CONTRAPOS_THM |- !t1 t2. (~t1 ==> ~t2) <=> (t2 ==> t1) *)
4704(* (HOL-Light compatible) *)
4705(* ------------------------------------------------------------------------- *)
4706
4707val CONTRAPOS_THM = thm (#(FILE), #(LINE)) ("CONTRAPOS_THM",
4708 MONO_NOT_EQ |> SYM
4709 |> INST [“x:bool” |-> “t1:bool”, “y:bool” |-> “t2:bool”]
4710 |> GENL [“t1:bool”, “t2:bool”]);