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