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