1(* ===================================================================== *) 2(* FILE : Conv.sml *) 3(* DESCRIPTION : Many conversions. A conversion is an ML function of *) 4(* type :term -> thm. The theorem is an equality whose *) 5(* lhs is the argument term. Translated from hol88. *) 6(* *) 7(* AUTHORS : (c) Many people at Cambridge: *) 8(* Larry Paulson *) 9(* Mike Gordon *) 10(* Richard Boulton and *) 11(* Tom Melham, University of Cambridge plus *) 12(* Paul Loewenstein, for hol88 *) 13(* TRANSLATOR : Konrad Slind, University of Calgary *) 14(* DATE : September 11, 1991 *) 15(* Many micro-optimizations added, February 24, 1992, KLS *) 16(* ===================================================================== *) 17 18structure lzConv :> lzConv = 19struct 20 21open HolKernel Parse boolTheory Drule boolSyntax Abbrev lazyTools Conv Rsyntax 22 23exception UNCHANGED 24 25fun QCONV c tm = c tm handle UNCHANGED => REFL tm 26 27val ERR = mk_HOL_ERR "lzConv"; 28 29 30(* ---------------------------------------------------------------------*) 31(* Conversion for rewrite rules of the form |- !x1 ... xn. t == u *) 32(* Matches x1 ... xn : t' ----> |- t' == u' *) 33(* Matches all types in conclusion except those mentioned in hypotheses.*) 34(* *) 35(* Rewritten such that the lhs of |- t' = u' is syntactically equal to *) 36(* the input term, not just alpha-equivalent. [TFM 90.07.11] *) 37(* *) 38(* OLD CODE: *) 39(* *) 40(* let REWRITE_CONV = *) 41(* set_fail_prefix `REWRITE_CONV` *) 42(* (PART_MATCH (fst o dest_eq));; *) 43(* ---------------------------------------------------------------------*) 44 45fun REWR_CONV0 (part_matcher,fn_name) th = 46 let val instth = part_matcher lhs th handle e 47 => raise (wrap_exn "lzConv" 48 (fn_name^": bad theorem argument: " 49 ^term_to_string (concl th)) e) 50 in fn tm => 51 let val eqn = instth tm 52 val l = lhs(concl eqn) 53 in if l = tm then eqn else TRANS (ALPHA tm l) eqn 54 end 55 handle HOL_ERR _ => raise ERR fn_name "lhs of thm doesn't match term" 56 end; 57 58val REWR_CONV = REWR_CONV0 (PART_MATCH, "REWR_CONV") 59val HO_REWR_CONV = REWR_CONV0 (HO_PART_MATCH, "HO_REWR_CONV"); 60 61 62(* ---------------------------------------------------------------------*) 63(* RAND_CONV conv "t1 t2" applies conv to t2 *) 64(* *) 65(* Added TFM 88.03.31 *) 66(* Revised TFM 91.03.08 *) 67(* Revised RJB 91.04.17 *) 68(* Revised Michael Norrish 2000.03.27 *) 69(* now passes on information about nested failure *) 70(* ---------------------------------------------------------------------*) 71 72fun RAND_CONV conv tm = let 73 val {Rator,Rand} = 74 dest_comb tm handle (HOL_ERR _) => raise ERR "RAND_CONV" "not a comb" 75 val newrand = conv Rand 76 handle HOL_ERR {origin_function, message, origin_structure} => 77 if Lib.mem origin_function ["RAND_CONV", "RATOR_CONV", "ABS_CONV"] 78 andalso origin_structure = "lzConv" 79 then 80 raise ERR "RAND_CONV" message 81 else 82 raise ERR "RAND_CONV" (origin_function ^ ": " ^ message) 83in 84 AP_TERM Rator newrand handle (HOL_ERR {message,...}) => 85 raise ERR "RAND_CONV" ("Application of AP_TERM failed: "^message) 86end 87 88 89(* ---------------------------------------------------------------------*) 90(* RATOR_CONV conv "t1 t2" applies conv to t1 *) 91(* *) 92(* Added TFM 88.03.31 *) 93(* Revised TFM 91.03.08 *) 94(* Revised RJB 91.04.17 *) 95(* Revised Michael Norrish 2000.03.27 *) 96(* now passes on information about nested failure *) 97(* ---------------------------------------------------------------------*) 98 99fun RATOR_CONV conv tm = let 100 val {Rator,Rand} = 101 dest_comb tm handle (HOL_ERR _) => raise ERR "RATOR_CONV" "not a comb" 102 val newrator = conv Rator 103 handle HOL_ERR {origin_function, origin_structure, message} => 104 if Lib.mem origin_function ["RAND_CONV", "RATOR_CONV", "ABS_CONV"] 105 andalso origin_structure = "lzConv" 106 then 107 raise ERR "RATOR_CONV" message 108 else 109 raise ERR "RATOR_CONV" (origin_function ^ ": " ^ message) 110in 111 AP_THM newrator Rand handle (HOL_ERR {message,...}) => 112 raise ERR "RATOR_CONV" ("Application of AP_THM failed: "^message) 113end 114 115(* remember this as "left-hand conv", where RAND_CONV is "right-hand conv". *) 116fun LAND_CONV c = RATOR_CONV (RAND_CONV c) 117 118(* ---------------------------------------------------------------------- 119 ABS_CONV conv "\x. t[x]" applies conv to t[x] 120 121 Added TFM 88.03.31 122 Revised RJB 91.04.17 123 Revised Michael Norrish 2000.03.27 124 now passes on information about nested failure 125 Revised Michael Norrish 2003.03.20 126 now does SUB_CONV-like tricks to handle ABS failing 127 ---------------------------------------------------------------------- *) 128 129fun ABS_CONV conv tm = 130 case dest_term tm of 131 LAMB{Bvar,Body} => let 132 val newbody = conv Body 133 in 134 ABS Bvar newbody 135 handle HOL_ERR _ => (* this can happen if Bvar is now free in the assumptions to newbody *) 136 let 137 (* this is buggy: 138 - fun foo_conv tm = List.foldl (fn (th,ath) => ADD_ASSUM (concl th) ath) 139 (REFL tm) (List.map REFL (free_vars tm)); 140 > val foo_conv = fn : term -> thm 141 - foo_conv ``x``; 142 <<HOL message: inventing new type variable names: 'a>> 143 > val it = [x = x] |- x = x : thm 144 - ABS_CONV foo_conv ``\x.x`` handle ex => Raise ex; 145 <<HOL message: inventing new type variable names: 'a>> 146 Exception raised at Conv.ABS_CONV: 147 ABS: The variable is free in the assumptions 148 ! Uncaught exception: 149 ! HOL_ERR 150 151 in fact with 152 fun foo_conv tm = (ADD_ASSUM ``x:bool`` (REFL (mk_conj(``x:bool``,tm)))); is fails on TRANS rather an ABS 153 so definitely a bug *) 154 val v = genvar (type_of Bvar) 155 val th1 = ALPHA_CONV v tm 156 val r = rhs (concl th1) 157 val {Body = Body',...} = dest_abs r 158 val eq_thm' = ABS v (conv Body') 159 val at = rhs (concl eq_thm') 160 val v' = variant (HOLset.listItems (FVL (hyp newbody) empty_varset)) Bvar (*variant (free_vars at) Bvar*) 161 val th2 = ALPHA_CONV v' at 162 in 163 TRANS (TRANS th1 eq_thm') th2 164 end 165 handle HOL_ERR {origin_function, origin_structure, message} => 166 if Lib.mem origin_function ["RAND_CONV", "RATOR_CONV", 167 "ABS_CONV"] 168 andalso origin_structure = "lzConv" 169 then 170 raise ERR "ABS_CONV" message 171 else 172 raise ERR "ABS_CONV" 173 (origin_function ^ ": " ^ message) 174 end 175 | _ => raise ERR "ABS_CONV" "Term not an abstraction" 176 177(* -------------------------------------------------------------------- *) 178(* LHS_CONV conv "t1 = t2" applies conv to t1 *) 179(* *) 180(* Added MN 99.06.14 *) 181(* -------------------------------------------------------------------- *) 182 183fun LHS_CONV conv tm = 184 if not (is_eq tm) then 185 raise ERR "LHS_CONV" "not an equality" 186 else 187 RATOR_CONV (RAND_CONV conv) tm 188 189(* -------------------------------------------------------------------- *) 190(* RHS_CONV conv "t1 = t2" applies conv to t2 *) 191(* *) 192(* Added MN 99.06.14 *) 193(* -------------------------------------------------------------------- *) 194 195fun RHS_CONV conv tm = 196 if not (is_eq tm) then 197 raise ERR "RHS_CONV" "not an equality" 198 else 199 RAND_CONV conv tm 200 201 202 203(*--------------------------------------------------------------------------- 204 * Conversion that always fails; identity element for ORELSEC. 205 *---------------------------------------------------------------------------*) 206 207fun NO_CONV _ = raise ERR "NO_CONV" ""; 208 209(* ---------------------------------------------------------------------- 210 Conversion that always succeeds, but does nothing. 211 Indicates this by raising the UNCHANGED exception. 212 ---------------------------------------------------------------------- *) 213 214fun ALL_CONV t = raise UNCHANGED 215 216(* ---------------------------------------------------------------------- 217 Apply two conversions in succession; fail if either does. Handle 218 UNCHANGED appropriately. 219 ---------------------------------------------------------------------- *) 220 221fun (conv1 THENC conv2) t = let 222 val th1 = conv1 t 223in 224 TRANS th1 (conv2 (rhs (concl th1))) handle UNCHANGED => th1 225end handle UNCHANGED => conv2 t 226 227(* ---------------------------------------------------------------------- 228 Apply conv1; if it raises a HOL_ERR then apply conv2. Note that 229 interrupts and other exceptions (including UNCHANGED) will sail on 230 through. 231 ---------------------------------------------------------------------- *) 232 233fun (conv1 ORELSEC conv2) t = conv1 t handle HOL_ERR _ => conv2 t; 234 235 236(*---------------------------------------------------------------------------* 237 * Perform the first successful conversion of those in the list. * 238 *---------------------------------------------------------------------------*) 239 240fun FIRST_CONV [] tm = NO_CONV tm 241 | FIRST_CONV (c::rst) tm = c tm handle (HOL_ERR _) => FIRST_CONV rst tm; 242 243(*--------------------------------------------------------------------------- 244 * Perform every conversion in the list. 245 *---------------------------------------------------------------------------*) 246 247fun EVERY_CONV convl tm = 248 itlist (curry (op THENC)) convl ALL_CONV tm 249 handle HOL_ERR _ => raise ERR "EVERY_CONV" ""; 250 251 252(*--------------------------------------------------------------------------- 253 * Cause the conversion to fail if it does not change its input. 254 *---------------------------------------------------------------------------*) 255 256fun CHANGED_CONV conv tm = 257 let val th = conv tm 258 handle UNCHANGED => raise ERR "CHANGED_CONV" "Input term unchanged" 259 val {lhs,rhs} = dest_eq (concl th) 260 in if aconv lhs rhs then raise ERR"CHANGED_CONV" "Input term unchanged" 261 else th 262 end; 263 264(* ---------------------------------------------------------------------- 265 Cause a failure if the conversion causes the UNCHANGED exception to 266 be raised. Doesn't "waste time" doing an equality check. Mnemonic: 267 "quick changed_conv". 268 ---------------------------------------------------------------------- *) 269 270fun QCHANGED_CONV conv tm = 271 conv tm 272 handle UNCHANGED => raise ERR "QCHANGED_CONV" "Input term unchanged" 273 274(*--------------------------------------------------------------------------- 275 * Apply a conversion zero or more times. 276 *---------------------------------------------------------------------------*) 277 278fun REPEATC conv t = 279 ((QCHANGED_CONV conv THENC (REPEATC conv)) ORELSEC ALL_CONV) t; 280 281fun TRY_CONV conv = conv ORELSEC ALL_CONV; 282 283fun COMB_CONV conv tm = let 284 val {Rator, Rand} = dest_comb tm 285in 286 let 287 val th = conv Rator 288 in 289 MK_COMB (th, conv Rand) handle UNCHANGED => AP_THM th Rand 290 end handle UNCHANGED => AP_TERM Rator (conv Rand) 291end 292 293fun SUB_CONV conv = 294 TRY_CONV (COMB_CONV conv ORELSEC ABS_CONV conv) 295 296fun FORK_CONV (conv1,conv2) tm = let 297 open Term (* get rid of overlying Rsyntax *) 298 val (fx,y) = with_exn dest_comb tm (ERR "FORK_CONV" "term not a comb") 299 val (f,x) = with_exn dest_comb fx (ERR "FORK_CONV" "term not f x y") 300in 301 let val th = AP_TERM f (conv1 x) 302 in MK_COMB (th,conv2 y) handle UNCHANGED => AP_THM th y 303 end handle UNCHANGED => AP_TERM fx (conv2 y) 304 end; 305 306fun BINOP_CONV conv tm = FORK_CONV (conv,conv) tm; 307 308val OR_CLAUSES' = 309 map GEN_ALL (CONJUNCTS (SPEC_ALL boolTheory.OR_CLAUSES)) 310val T_or = List.nth(OR_CLAUSES', 0); 311val or_T = List.nth(OR_CLAUSES', 1); 312val F_or = List.nth(OR_CLAUSES', 2); 313val or_F = List.nth(OR_CLAUSES', 3); 314 315 316fun EVERY_DISJ_CONV c tm = let 317in 318 if is_disj tm then 319 LAND_CONV (EVERY_DISJ_CONV c) THENC 320 (REWR_CONV T_or ORELSEC 321 (REWR_CONV F_or THENC EVERY_DISJ_CONV c) ORELSEC 322 (RAND_CONV (EVERY_DISJ_CONV c) THENC 323 TRY_CONV (REWR_CONV or_T ORELSEC REWR_CONV or_F))) 324 else c 325end tm 326 327val AND_CLAUSES' = map GEN_ALL (CONJUNCTS (SPEC_ALL AND_CLAUSES)) 328val T_and = List.nth(AND_CLAUSES', 0) 329val and_T = List.nth(AND_CLAUSES', 1) 330val F_and = List.nth(AND_CLAUSES', 2) 331val and_F = List.nth(AND_CLAUSES', 3) 332 333fun EVERY_CONJ_CONV c tm = let 334in 335 if is_conj tm then 336 LAND_CONV (EVERY_CONJ_CONV c) THENC 337 (REWR_CONV F_and ORELSEC 338 (REWR_CONV T_and THENC EVERY_DISJ_CONV c) ORELSEC 339 (RAND_CONV (EVERY_CONJ_CONV c) THENC 340 TRY_CONV (REWR_CONV and_F ORELSEC REWR_CONV or_T))) 341 else c 342end tm 343 344fun QUANT_CONV conv = RAND_CONV(ABS_CONV conv); 345fun BINDER_CONV conv = ABS_CONV conv ORELSEC QUANT_CONV conv; 346 347fun STRIP_BINDER_CONV opt conv tm = let 348 val (vlist,M) = strip_binder opt tm 349in 350 GEN_ABS opt vlist (conv M) 351 handle HOL_ERR _ => let 352 val gvs = map (genvar o type_of) vlist 353 fun rename vs t = 354 case vs of 355 [] => ALL_CONV t 356 | (v::vs) => 357 (GEN_ALPHA_CONV v THENC BINDER_CONV (rename vs)) t 358 fun variant_list acc avds [] = List.rev acc 359 | variant_list acc avds (v::vs) = let 360 val v' = variant avds v 361 in 362 variant_list (v'::acc) (v'::avds) vs 363 end 364 val th1 = rename gvs tm 365 val {rhs,...} = Rsyntax.dest_eq(Thm.concl th1) 366 val (_, M') = strip_binder opt rhs (* v = Bvar *) 367 val eq_thm' = GEN_ABS opt gvs (conv M') 368 val at = #rhs(Rsyntax.dest_eq(concl eq_thm')) 369 val vs' = variant_list [] (free_vars at) vlist 370 val th2 = rename vs' at 371 in 372 TRANS (TRANS th1 eq_thm') th2 373 end 374end 375 376 377fun STRIP_QUANT_CONV conv tm = 378 (if is_forall tm then STRIP_BINDER_CONV (SOME boolSyntax.universal) else 379 if is_exists tm then STRIP_BINDER_CONV (SOME boolSyntax.existential) else 380 if is_select tm then STRIP_BINDER_CONV (SOME boolSyntax.select) else 381 if is_exists1 tm then STRIP_BINDER_CONV (SOME boolSyntax.exists1) 382 else K conv) conv tm; 383 384fun LAST_EXISTS_CONV c tm = let 385 val (bv, body) = Psyntax.dest_exists tm 386in 387 if is_exists body then BINDER_CONV (LAST_EXISTS_CONV c) tm 388 else c tm 389end 390 391fun LAST_FORALL_CONV c tm = 392 if is_forall (#2 (Psyntax.dest_forall tm)) then 393 BINDER_CONV (LAST_FORALL_CONV c) tm 394 else c tm 395 396(* ---------------------------------------------------------------------- 397 traversal conversionals. 398 399 DEPTH_CONV c 400 bottom-up, recurse over sub-terms, and then repeatedly apply c at 401 top-level. 402 403 REDEPTH_CONV c 404 bottom-up. recurse over sub-terms, apply c at top, and if this 405 succeeds, repeat from start. 406 407 TOP_DEPTH_CONV c 408 top-down. Repeatdly apply c at top-level, then descend. If descending 409 doesn't change anything then stop. If there was a change then 410 come back to top and try c once more at top-level. If this succeeds 411 repeat. 412 413 TOP_SWEEP_CONV c 414 top-down. Like TOP_DEPTH_CONV but only makes one pass over the term, 415 never coming back to the top level once descent starts. 416 417 ONCE_DEPTH_CONV c 418 top-down (confusingly). Descends term looking for position at 419 which c works. Does this "in parallel", so c may be applied multiple 420 times at highest possible positions in distinct sub-terms. 421 422 ---------------------------------------------------------------------- *) 423 424 425fun DEPTH_CONV conv tm = 426 (SUB_CONV (DEPTH_CONV conv) THENC REPEATC conv) tm 427 428fun REDEPTH_CONV conv tm = 429 (SUB_CONV (REDEPTH_CONV conv) THENC 430 TRY_CONV (conv THENC REDEPTH_CONV conv)) tm 431 432fun TOP_DEPTH_CONV conv tm = 433 (REPEATC conv THENC 434 TRY_CONV (CHANGED_CONV (SUB_CONV (TOP_DEPTH_CONV conv)) THENC 435 TRY_CONV (conv THENC TOP_DEPTH_CONV conv))) tm 436 437fun ONCE_DEPTH_CONV conv tm = 438 TRY_CONV (conv ORELSEC SUB_CONV (ONCE_DEPTH_CONV conv)) tm 439 440fun TOP_SWEEP_CONV conv tm = 441 (REPEATC conv THENC SUB_CONV (TOP_SWEEP_CONV conv)) tm 442 443(*---------------------------------------------------------------------------* 444 * Convert a conversion to a rule * 445 *---------------------------------------------------------------------------*) 446 447fun CONV_RULE conv th = EQ_MP (conv(concl th)) th handle UNCHANGED => th 448 449(*---------------------------------------------------------------------------* 450 * Rule for beta-reducing on all beta-redexes * 451 *---------------------------------------------------------------------------*) 452 453val BETA_RULE = CONV_RULE(DEPTH_CONV BETA_CONV) 454 455fun UNBETA_CONV arg_t t = let 456 open Term (* counteract prevailing Rsyntax *) 457in 458 if is_var arg_t then 459 SYM (BETA_CONV (mk_comb(mk_abs(arg_t,t), arg_t))) 460 else let 461 (* find all instances of arg_t in t, and convert t 462 to (\v. t[v/arg_t]) arg_t 463 v can be a genvar because we expect to get rid of it later. *) 464 val gv = genvar (type_of arg_t) 465 val newbody = Term.subst [arg_t |-> gv] t 466 in 467 SYM (BETA_CONV (Term.mk_comb(mk_abs(gv,newbody), arg_t))) 468 end 469end 470 471(* =====================================================================*) 472(* What follows is a complete set of conversions for moving ! and ? into*) 473(* and out of the basic logical connectives ~, /\, \/, ==>, and =. *) 474(* *) 475(* Naming scheme: *) 476(* *) 477(* 1: for moving quantifiers inwards: <quant>_<conn>_CONV *) 478(* *) 479(* 2: for moving quantifiers outwards: [dir]_<conn>_<quant>_CONV *) 480(* *) 481(* where *) 482(* *) 483(* <quant> := FORALL | EXISTS *) 484(* <conn> := NOT | AND | OR | IMP | EQ *) 485(* [dir] := LEFT | RIGHT (optional) *) 486(* *) 487(* *) 488(* [TFM 90.11.09] *) 489(* =====================================================================*) 490 491(* ---------------------------------------------------------------------*) 492(* NOT_FORALL_CONV, implements the following axiom scheme: *) 493(* *) 494(* |- (~!x.tm) = (?x.~tm) *) 495(* *) 496(* ---------------------------------------------------------------------*) 497fun NOT_FORALL_CONV tm = 498 let val all = dest_neg tm 499 val {Bvar,Body} = dest_forall all 500 val exists = mk_exists{Bvar = Bvar, Body = mk_neg Body} 501 val nott = ASSUME (mk_neg Body) 502 val not_all = mk_neg all 503 val th1 = DISCH all (MP nott (SPEC Bvar (ASSUME all))) 504 val imp1 = DISCH exists (CHOOSE (Bvar, ASSUME exists) (NOT_INTRO th1)) 505 val th2 = CCONTR Body (MP (ASSUME(mk_neg exists)) 506 (EXISTS(exists,Bvar) nott)) 507 val th3 = CCONTR exists (MP (ASSUME not_all) (GEN Bvar th2)) 508 in 509 IMP_ANTISYM_RULE (DISCH not_all th3) imp1 510 end 511 handle HOL_ERR _ => raise ERR "NOT_FORALL_CONV" ""; 512 513(* ---------------------------------------------------------------------*) 514(* NOT_EXISTS_CONV, implements the following axiom scheme. *) 515(* *) 516(* |- (~?x.tm) = (!x.~tm) *) 517(* *) 518(* ---------------------------------------------------------------------*) 519fun NOT_EXISTS_CONV tm = 520 let val {Bvar,Body} = dest_exists (dest_neg tm) 521 val all = mk_forall{Bvar=Bvar, Body=mk_neg Body} 522 val rand_tm = rand tm 523 val asm1 = ASSUME Body 524 val thm1 = MP (ASSUME tm) (EXISTS (rand_tm, Bvar) asm1) 525 val imp1 = DISCH tm (GEN Bvar (NOT_INTRO (DISCH Body thm1))) 526 val asm2 = ASSUME all 527 and asm3 = ASSUME rand_tm 528 val thm2 = DISCH rand_tm (CHOOSE (Bvar,asm3) (MP (SPEC Bvar asm2) asm1)) 529 val imp2 = DISCH all (NOT_INTRO thm2) 530 in 531 IMP_ANTISYM_RULE imp1 imp2 532 end 533 handle HOL_ERR _ => raise ERR "NOT_EXISTS_CONV" ""; 534 535(* ---------------------------------------------------------------------*) 536(* EXISTS_NOT_CONV, implements the following axiom scheme. *) 537(* *) 538(* |- (?x.~tm) = (~!x.tm) *) 539(* *) 540(* ---------------------------------------------------------------------*) 541fun EXISTS_NOT_CONV tm = 542 let val {Bvar,Body} = dest_exists tm 543 in 544 SYM(NOT_FORALL_CONV (mk_neg (mk_forall{Bvar=Bvar, Body=dest_neg Body}))) 545 end 546 handle HOL_ERR _ => raise ERR "EXISTS_NOT_CONV" ""; 547 548(* ---------------------------------------------------------------------*) 549(* FORALL_NOT_CONV, implements the following axiom scheme. *) 550(* *) 551(* |- (!x.~tm) = (~?x.tm) *) 552(* *) 553(* ---------------------------------------------------------------------*) 554fun FORALL_NOT_CONV tm = 555 let val {Bvar,Body} = dest_forall tm 556 in 557 SYM (NOT_EXISTS_CONV (mk_neg (mk_exists{Bvar=Bvar,Body=dest_neg Body}))) 558 end 559 handle HOL_ERR _ => raise ERR "FORALL_NOT_CONV" ""; 560 561(* ---------------------------------------------------------------------*) 562(* FORALL_AND_CONV : move universal quantifiers into conjunction. *) 563(* *) 564(* A call to FORALL_AND_CONV "!x. P /\ Q" returns: *) 565(* *) 566(* |- (!x. P /\ Q) = (!x.P) /\ (!x.Q) *) 567(* ---------------------------------------------------------------------*) 568fun FORALL_AND_CONV tm = 569 let val {Bvar,Body} = dest_forall tm 570 val {...} = dest_conj Body 571 val (Pth,Qth) = CONJ_PAIR (SPEC Bvar (ASSUME tm)) 572 val imp1 = DISCH tm (CONJ (GEN Bvar Pth) (GEN Bvar Qth)) 573 val xtm = rand(concl imp1) 574 val spec_bv = SPEC Bvar 575 val (t1,t2) = (spec_bv##spec_bv) (CONJ_PAIR (ASSUME xtm)) 576 in 577 IMP_ANTISYM_RULE imp1 (DISCH xtm (GEN Bvar (CONJ t1 t2))) 578 end 579 handle HOL_ERR _ => raise ERR "FORALL_AND_CONV" ""; 580 581(* ---------------------------------------------------------------------*) 582(* EXISTS_OR_CONV : move existential quantifiers into disjunction. *) 583(* *) 584(* A call to EXISTS_OR_CONV "?x. P \/ Q" returns: *) 585(* *) 586(* |- (?x. P \/ Q) = (?x.P) \/ (?x.Q) *) 587(* ---------------------------------------------------------------------*) 588(* 589fun EXISTS_OR_CONV tm = 590 let val {Bvar,Body} = dest_exists tm 591 val {disj1,disj2} = dest_disj Body 592 val ep = mk_exists{Bvar=Bvar, Body=disj1} 593 and eq = mk_exists{Bvar=Bvar, Body=disj2} 594 val ep_or_eq = mk_disj{disj1=ep, disj2=eq} 595 val aP = ASSUME disj1 596 val aQ = ASSUME disj2 597 val Pth = EXISTS(ep,Bvar) aP 598 and Qth = EXISTS(eq,Bvar) aQ 599 val thm1 = DISJ_CASES_UNION (ASSUME Body) Pth Qth 600 val imp1 = DISCH tm (CHOOSE (Bvar,ASSUME tm) thm1) 601 val t1 = DISJ1 aP disj2 602 and t2 = DISJ2 disj1 aQ 603 val th1 = EXISTS(tm,Bvar) t1 604 and th2 = EXISTS(tm,Bvar) t2 605 val e1 = CHOOSE (Bvar,ASSUME ep) th1 606 and e2 = CHOOSE (Bvar,ASSUME eq) th2 607 in 608 IMP_ANTISYM_RULE imp1 (DISCH ep_or_eq (DISJ_CASES (ASSUME ep_or_eq) e1 e2)) 609 end 610 handle HOL_ERR _ => raise ERR "EXISTS_OR_CONV" ""; 611*) 612 613local val alpha = Type.alpha 614 val spotBeta = FORK_CONV (QUANT_CONV (BINOP_CONV BETA_CONV), 615 BINOP_CONV (QUANT_CONV BETA_CONV)) 616 open boolTheory 617 val [P0,Q0] = fst(strip_forall(concl EXISTS_OR_THM)) 618 val thm0 = SPEC Q0 (SPEC P0 EXISTS_OR_THM) 619 val Pname = #Name(dest_var P0) 620 val Qname = #Name(dest_var Q0) 621in 622fun EXISTS_OR_CONV tm = 623 let val {Bvar,Body} = dest_exists tm 624 val thm = CONV_RULE (RAND_CONV (BINOP_CONV (GEN_ALPHA_CONV Bvar))) 625 (INST_TYPE [alpha |-> type_of Bvar] thm0) 626 val ty = type_of Bvar --> Type.bool 627 val P = mk_var{Name=Pname, Ty=ty} 628 val Q = mk_var{Name=Qname, Ty=ty} 629 val {disj1,disj2} = dest_disj Body 630 val lamP = mk_abs{Bvar=Bvar, Body=disj1} 631 val lamQ = mk_abs{Bvar=Bvar, Body=disj2} 632 in 633 CONV_RULE spotBeta (INST [P |-> lamP, Q |-> lamQ] thm) 634 end 635 handle HOL_ERR _ => raise ERR "EXISTS_OR_CONV" ""; 636end; 637 638(* ---------------------------------------------------------------------*) 639(* AND_FORALL_CONV : move universal quantifiers out of conjunction. *) 640(* *) 641(* A call to AND_FORALL_CONV "(!x. P) /\ (!x. Q)" returns: *) 642(* *) 643(* |- (!x.P) /\ (!x.Q) = (!x. P /\ Q) *) 644(* ---------------------------------------------------------------------*) 645 646fun AND_FORALL_CONV tm = 647 let val {conj1,conj2} = dest_conj tm 648 val {Bvar=x, Body=P} = dest_forall conj1 649 val {Bvar=y, Body=Q} = dest_forall conj2 650 in 651 if (not (x=y)) 652 then raise ERR "AND_FORALL_CONV" "forall'ed variables not the same" 653 else let val specx = SPEC x 654 val (t1,t2) = (specx##specx) (CONJ_PAIR (ASSUME tm)) 655 val imp1 = DISCH tm (GEN x (CONJ t1 t2)) 656 val rtm = rand(concl imp1) 657 val (Pth,Qth) = CONJ_PAIR (SPEC x (ASSUME rtm)) 658 in 659 IMP_ANTISYM_RULE imp1 (DISCH rtm (CONJ (GEN x Pth) (GEN x Qth))) 660 end 661 end 662 handle HOL_ERR _ => raise ERR "AND_FORALL_CONV" ""; 663 664 665(* ---------------------------------------------------------------------*) 666(* LEFT_AND_FORALL_CONV : move universal quantifier out of conjunction. *) 667(* *) 668(* A call to LEFT_AND_FORALL_CONV "(!x.P) /\ Q" returns: *) 669(* *) 670(* |- (!x.P) /\ Q = (!x'. P[x'/x] /\ Q) *) 671(* *) 672(* Where x' is a primed variant of x not free in the input term *) 673(* ---------------------------------------------------------------------*) 674fun LEFT_AND_FORALL_CONV tm = 675 let val {conj1,...} = dest_conj tm 676 val {Bvar,...} = dest_forall conj1 677 val x' = variant (free_vars tm) Bvar 678 val specx' = SPEC x' 679 and genx' = GEN x' 680 val (t1,t2) = (specx' ## I) (CONJ_PAIR (ASSUME tm)) 681 val imp1 = DISCH tm (genx' (CONJ t1 t2)) 682 val rtm = rand(concl imp1) 683 val (Pth,Qth) = CONJ_PAIR (specx' (ASSUME rtm)) 684 in 685 IMP_ANTISYM_RULE imp1 (DISCH rtm (CONJ (genx' Pth) Qth)) 686 end 687 handle HOL_ERR _ => raise ERR "LEFT_AND_FORALL_CONV" ""; 688 689(* ---------------------------------------------------------------------*) 690(* RIGHT_AND_FORALL_CONV : move universal quantifier out of conjunction.*) 691(* *) 692(* A call to RIGHT_AND_FORALL_CONV "P /\ (!x.Q)" returns: *) 693(* *) 694(* |- P /\ (!x.Q) = (!x'. P /\ Q[x'/x]) *) 695(* *) 696(* where x' is a primed variant of x not free in the input term *) 697(* ---------------------------------------------------------------------*) 698fun RIGHT_AND_FORALL_CONV tm = 699 let val {conj2, ...} = dest_conj tm 700 val {Bvar,...} = dest_forall conj2 701 val x' = variant (free_vars tm) Bvar 702 val specx' = SPEC x' 703 val genx' = GEN x' 704 val (t1,t2) = (I ## specx') (CONJ_PAIR (ASSUME tm)) 705 val imp1 = DISCH tm (genx' (CONJ t1 t2)) 706 val rtm = rand(concl imp1) 707 val (Pth,Qth) = CONJ_PAIR (specx' (ASSUME rtm)) 708 in 709 IMP_ANTISYM_RULE imp1 (DISCH rtm (CONJ Pth (genx' Qth))) 710 end 711 handle HOL_ERR _ => raise ERR "RIGHT_AND_FORALL_CONV" ""; 712 713(* ---------------------------------------------------------------------*) 714(* OR_EXISTS_CONV : move existential quantifiers out of disjunction. *) 715(* *) 716(* A call to OR_EXISTS_CONV "(?x. P) \/ (?x. Q)" returns: *) 717(* *) 718(* |- (?x.P) \/ (?x.Q) = (?x. P \/ Q) *) 719(* ---------------------------------------------------------------------*) 720fun OR_EXISTS_CONV tm = 721 let val {disj1,disj2} = dest_disj tm 722 val {Bvar=x, Body=P} = dest_exists disj1 723 val {Bvar=y, Body=Q} = dest_exists disj2 724 in 725 if (not (x=y)) then raise ERR "OR_EXISTS_CONV" "" 726 else let val aP = ASSUME P 727 and aQ = ASSUME Q 728 and P_or_Q = mk_disj{disj1 = P, disj2 = Q} 729 val otm = mk_exists {Bvar = x, Body = P_or_Q} 730 val t1 = DISJ1 aP Q 731 and t2 = DISJ2 P aQ 732 val eotm = EXISTS(otm,x) 733 val e1 = CHOOSE (x,ASSUME disj1) (eotm t1) 734 and e2 = CHOOSE (x,ASSUME disj2) (eotm t2) 735 val thm1 = DISJ_CASES (ASSUME tm) e1 e2 736 val imp1 = DISCH tm thm1 737 val Pth = EXISTS(disj1,x) aP 738 and Qth = EXISTS(disj2,x) aQ 739 val thm2 = DISJ_CASES_UNION (ASSUME P_or_Q) Pth Qth 740 in 741 IMP_ANTISYM_RULE imp1 (DISCH otm (CHOOSE (x,ASSUME otm) thm2)) 742 end 743 end 744 handle HOL_ERR _ => raise ERR "OR_EXISTS_CONV" ""; 745 746(* ---------------------------------------------------------------------*) 747(* LEFT_OR_EXISTS_CONV : move existential quantifier out of disjunction.*) 748(* *) 749(* A call to LEFT_OR_EXISTS_CONV "(?x.P) \/ Q" returns: *) 750(* *) 751(* |- (?x.P) \/ Q = (?x'. P[x'/x] \/ Q) *) 752(* *) 753(* Where x' is a primed variant of x not free in the input term *) 754(* ---------------------------------------------------------------------*) 755 756fun LEFT_OR_EXISTS_CONV tm = 757 let val {disj1,disj2} = dest_disj tm 758 val {Bvar,Body} = dest_exists disj1 759 val x' = variant (free_vars tm) Bvar 760 val newp = subst[Bvar |-> x'] Body 761 val newp_thm = ASSUME newp 762 val new_disj = mk_disj {disj1=newp, disj2=disj2} 763 val otm = mk_exists {Bvar=x', Body=new_disj} 764 and Qth = ASSUME disj2 765 val t1 = DISJ1 newp_thm disj2 766 and t2 = DISJ2 newp (ASSUME disj2) 767 val th1 = EXISTS(otm,x') t1 768 and th2 = EXISTS(otm,x') t2 769 val thm1 = DISJ_CASES (ASSUME tm) (CHOOSE(x',ASSUME disj1)th1) th2 770 val imp1 = DISCH tm thm1 771 val Pth = EXISTS(disj1,x') newp_thm 772 val thm2 = DISJ_CASES_UNION (ASSUME new_disj) Pth Qth 773 in 774 IMP_ANTISYM_RULE imp1 (DISCH otm (CHOOSE (x',ASSUME otm) thm2)) 775 end 776 handle HOL_ERR _ => raise ERR "LEFT_OR_EXISTS_CONV" ""; 777 778(* ---------------------------------------------------------------------*) 779(* RIGHT_OR_EXISTS_CONV: move existential quantifier out of disjunction.*) 780(* *) 781(* A call to RIGHT_OR_EXISTS_CONV "P \/ (?x.Q)" returns: *) 782(* *) 783(* |- P \/ (?x.Q) = (?x'. P \/ Q[x'/x]) *) 784(* *) 785(* where x' is a primed variant of x not free in the input term *) 786(* ---------------------------------------------------------------------*) 787fun RIGHT_OR_EXISTS_CONV tm = 788 let val {disj1,disj2} = dest_disj tm 789 val {Bvar,Body} = dest_exists disj2 790 val x' = variant (free_vars tm) Bvar 791 val newq = subst[Bvar |-> x'] Body 792 val newq_thm = ASSUME newq 793 and Pth = ASSUME disj1 794 val P_or_newq = mk_disj{disj1 = disj1, disj2 = newq} 795 val otm = mk_exists{Bvar = x',Body = P_or_newq} 796 val eotm' = EXISTS(otm,x') 797 val th1 = eotm' (DISJ2 disj1 newq_thm) 798 and th2 = eotm' (DISJ1 Pth newq) 799 val thm1 = DISJ_CASES (ASSUME tm) th2 (CHOOSE(x',ASSUME disj2) th1) 800 val imp1 = DISCH tm thm1 801 val Qth = EXISTS(disj2,x') newq_thm 802 val thm2 = DISJ_CASES_UNION (ASSUME P_or_newq) Pth Qth 803 in 804 IMP_ANTISYM_RULE imp1 (DISCH otm (CHOOSE (x',ASSUME otm) thm2)) 805 end 806 handle HOL_ERR _ => raise ERR "RIGHT_OR_EXISTS_CONV" ""; 807 808(* ---------------------------------------------------------------------*) 809(* EXISTS_AND_CONV : move existential quantifier into conjunction. *) 810(* *) 811(* A call to EXISTS_AND_CONV "?x. P /\ Q" returns: *) 812(* *) 813(* |- (?x. P /\ Q) = (?x.P) /\ Q [x not free in Q] *) 814(* |- (?x. P /\ Q) = P /\ (?x.Q) [x not free in P] *) 815(* |- (?x. P /\ Q) = (?x.P) /\ (?x.Q) [x not free in P /\ Q] *) 816(* ---------------------------------------------------------------------*) 817fun EXISTS_AND_CONV tm = 818 let val {Bvar, Body} = dest_exists tm handle HOL_ERR _ 819 => raise ERR"EXISTS_AND_CONV" "expecting `?x. P /\\ Q`" 820 val {conj1,conj2} = dest_conj Body handle HOL_ERR _ 821 => raise ERR "EXISTS_AND_CONV" "expecting `?x. P /\\ Q`" 822 val fP = free_in Bvar conj1 823 and fQ = free_in Bvar conj2 824 in 825 if (fP andalso fQ) 826 then raise ERR"EXISTS_AND_CONV" 827 ("`"^(#Name(dest_var Bvar))^ "` free in both conjuncts") 828 else let val (t1,t2) = CONJ_PAIR(ASSUME Body) 829 val econj1 = mk_exists{Bvar = Bvar, Body = conj1} 830 val econj2 = mk_exists{Bvar = Bvar, Body = conj2} 831 val eP = if fQ then t1 else EXISTS (econj1,Bvar) t1 832 and eQ = if fP then t2 else EXISTS (econj2,Bvar) t2 833 val imp1 = DISCH tm (CHOOSE(Bvar,ASSUME tm) (CONJ eP eQ)) 834 val th = EXISTS (tm,Bvar) (CONJ(ASSUME conj1) (ASSUME conj2)) 835 val th1 = if (fP orelse (not fQ)) 836 then CHOOSE(Bvar,ASSUME econj1)th 837 else th 838 val thm1 = if (fQ orelse (not fP)) 839 then CHOOSE(Bvar,ASSUME econj2)th1 840 else th1 841 val otm = rand(concl imp1) 842 val (t1,t2) = CONJ_PAIR(ASSUME otm) 843 val thm2 = PROVE_HYP t1 (PROVE_HYP t2 thm1) 844 in 845 IMP_ANTISYM_RULE imp1 (DISCH otm thm2) 846 end 847 end 848 handle (e as HOL_ERR{origin_structure = "lzConv", 849 origin_function = "EXISTS_AND_CONV",...}) => raise e 850 | HOL_ERR _ => raise ERR"EXISTS_AND_CONV" ""; 851 852(* ---------------------------------------------------------------------*) 853(* AND_EXISTS_CONV : move existential quantifier out of conjunction. *) 854(* *) 855(* |- (?x.P) /\ (?x.Q) = (?x. P /\ Q) *) 856(* *) 857(* provided x is free in neither P nor Q. *) 858(* ---------------------------------------------------------------------*) 859local val AE_ERR = ERR"AND_EXISTS_CONV" "expecting `(?x.P) /\\ (?x.Q)`" 860in 861fun AND_EXISTS_CONV tm = 862 let val {conj1,conj2} = dest_conj tm handle HOL_ERR _ => raise AE_ERR 863 val {Bvar=x, Body=P} = dest_exists conj1 handle HOL_ERR _ => raise AE_ERR 864 val {Bvar=y, Body=Q} = dest_exists conj2 handle HOL_ERR_ => raise AE_ERR 865 in 866 if (not(x=y)) then raise AE_ERR else 867 if (free_in x P orelse free_in x Q) 868 then raise ERR "AND_EXISTS_CONV" 869 ("`"^(#Name(dest_var x))^"` free in conjunct(s)") 870 else SYM (EXISTS_AND_CONV 871 (mk_exists{Bvar=x, Body=mk_conj{conj1=P, conj2=Q}})) 872 end 873 handle (e as HOL_ERR{origin_structure = "lzConv", 874 origin_function = "AND_EXISTS_CONV",...}) => raise e 875 | HOL_ERR _ => raise ERR"AND_EXISTS_CONV" "" 876end; 877 878(* ---------------------------------------------------------------------*) 879(* LEFT_AND_EXISTS_CONV: move existential quantifier out of conjunction *) 880(* *) 881(* A call to LEFT_AND_EXISTS_CONV "(?x.P) /\ Q" returns: *) 882(* *) 883(* |- (?x.P) /\ Q = (?x'. P[x'/x] /\ Q) *) 884(* *) 885(* Where x' is a primed variant of x not free in the input term *) 886(* ---------------------------------------------------------------------*) 887fun LEFT_AND_EXISTS_CONV tm = 888 let val {conj1,conj2} = dest_conj tm 889 val {Bvar,Body} = dest_exists conj1 890 val x' = variant (free_vars tm) Bvar 891 val newp = subst[Bvar |-> x'] Body 892 val new_conj = mk_conj {conj1 = newp, conj2 = conj2} 893 val otm = mk_exists{Bvar = x', Body = new_conj} 894 val (EP,Qth) = CONJ_PAIR(ASSUME tm) 895 val thm1 = EXISTS(otm,x')(CONJ(ASSUME newp)(ASSUME conj2)) 896 val imp1 = DISCH tm (MP (DISCH conj2 (CHOOSE(x',EP)thm1)) Qth) 897 val (t1,t2) = CONJ_PAIR (ASSUME new_conj) 898 val thm2 = CHOOSE (x',ASSUME otm) (CONJ (EXISTS (conj1,x') t1) t2) 899 in 900 IMP_ANTISYM_RULE imp1 (DISCH otm thm2) 901 end 902 handle HOL_ERR _ => raise ERR "LEFT_AND_EXISTS_CONV" ""; 903 904(* ---------------------------------------------------------------------*) 905(* RIGHT_AND_EXISTS_CONV: move existential quantifier out of conjunction*) 906(* *) 907(* A call to RIGHT_AND_EXISTS_CONV "P /\ (?x.Q)" returns: *) 908(* *) 909(* |- P /\ (?x.Q) = (?x'. P /\ (Q[x'/x]) *) 910(* *) 911(* where x' is a primed variant of x not free in the input term *) 912(* ---------------------------------------------------------------------*) 913fun RIGHT_AND_EXISTS_CONV tm = 914 let val {conj1,conj2} = dest_conj tm 915 val {Bvar,Body} = dest_exists conj2 916 val x' = variant (free_vars tm) Bvar 917 val newq = subst[Bvar |-> x'] Body 918 val new_conj = mk_conj{conj1 = conj1,conj2 = newq} 919 val otm = mk_exists{Bvar = x',Body = new_conj} 920 val (Pth,EQ) = CONJ_PAIR(ASSUME tm) 921 val thm1 = EXISTS(otm,x')(CONJ(ASSUME conj1)(ASSUME newq)) 922 val imp1 = DISCH tm (MP (DISCH conj1 (CHOOSE(x',EQ)thm1)) Pth) 923 val (t1,t2) = CONJ_PAIR (ASSUME new_conj) 924 val thm2 = CHOOSE (x',ASSUME otm) (CONJ t1 (EXISTS (conj2,x') t2)) 925 in 926 IMP_ANTISYM_RULE imp1 (DISCH otm thm2) 927 end 928 handle HOL_ERR _ => raise ERR "RIGHT_AND_EXISTS_CONV" ""; 929 930 931(* ---------------------------------------------------------------------*) 932(* FORALL_OR_CONV : move universal quantifier into disjunction. *) 933(* *) 934(* A call to FORALL_OR_CONV "!x. P \/ Q" returns: *) 935(* *) 936(* |- (!x. P \/ Q) = (!x.P) \/ Q [if x not free in Q] *) 937(* |- (!x. P \/ Q) = P \/ (!x.Q) [if x not free in P] *) 938(* |- (!x. P \/ Q) = (!x.P) \/ (!x.Q) [if x free in neither P nor Q] *) 939(* ---------------------------------------------------------------------*) 940local val FO_ERR = ERR"FORALL_OR_CONV" "expecting `!x. P \\/ Q`" 941in 942fun FORALL_OR_CONV tm = 943 let val {Bvar,Body} = dest_forall tm handle HOL_ERR _ => raise FO_ERR 944 val {disj1,disj2} = dest_disj Body handle HOL_ERR _ => raise FO_ERR 945 val fdisj1 = free_in Bvar disj1 946 and fdisj2 = free_in Bvar disj2 947 in 948 if (fdisj1 andalso fdisj2) 949 then raise ERR "FORALL_OR_CONV" 950 ("`"^(#Name(dest_var Bvar))^"` free in both disjuncts") 951 else 952 let val disj1_thm = ASSUME disj1 953 val disj2_thm = ASSUME disj2 954 val thm1 = SPEC Bvar (ASSUME tm) 955 val imp1 = 956 if fdisj1 957 then let val thm2 = CONTR disj1 (MP (ASSUME (mk_neg disj2)) disj2_thm) 958 val thm3 = DISJ1(GEN Bvar(DISJ_CASES thm1 disj1_thm thm2)) disj2 959 val thm4 = DISJ2(mk_forall{Bvar=Bvar, Body=disj1})(ASSUME disj2) 960 in 961 DISCH tm (DISJ_CASES(SPEC disj2 EXCLUDED_MIDDLE) thm4 thm3) 962 end 963 else 964 if fdisj2 965 then let val thm2 = CONTR disj2(MP (ASSUME (mk_neg disj1)) (ASSUME disj1)) 966 val thm3 = DISJ2 disj1 (GEN Bvar(DISJ_CASES thm1 thm2 disj2_thm)) 967 val thm4 = DISJ1(ASSUME disj1)(mk_forall{Bvar=Bvar, Body=disj2}) 968 in 969 DISCH tm (DISJ_CASES (SPEC disj1 EXCLUDED_MIDDLE) thm4 thm3) 970 end 971 else 972 let val t1 = GEN Bvar(ASSUME disj1) 973 val t2 = GEN Bvar(ASSUME disj2) 974 in 975 DISCH tm (DISJ_CASES_UNION thm1 t1 t2) 976 end 977 val otm = rand(concl imp1) 978 val {disj1,disj2} = dest_disj otm 979 val thm5 = (if (fdisj1 orelse (not fdisj2)) then SPEC Bvar else I) 980 (ASSUME disj1) 981 val thm6 = (if (fdisj2 orelse (not fdisj1)) then SPEC Bvar else I) 982 (ASSUME disj2) 983 val imp2 = GEN Bvar (DISJ_CASES_UNION (ASSUME otm) thm5 thm6) 984 in 985 IMP_ANTISYM_RULE imp1 (DISCH otm imp2) 986 end 987 end 988 handle (e as HOL_ERR{origin_structure = "lzConv", 989 origin_function = "FORALL_OR_CONV",...}) => raise e 990 | HOL_ERR _ => raise ERR "FORALL_OR_CONV" "" 991end; 992 993(* ---------------------------------------------------------------------*) 994(* OR_FORALL_CONV : move existential quantifier out of conjunction. *) 995(* *) 996(* |- (!x.P) \/ (!x.Q) = (!x. P \/ Q) *) 997(* *) 998(* provided x is free in neither P nor Q. *) 999(* ---------------------------------------------------------------------*) 1000local val OF_ERR = ERR "OR_FORALL_CONV" "expecting `(!x.P) \\/ (!x.Q)`" 1001in 1002fun OR_FORALL_CONV tm = 1003 let val {disj1,disj2} = dest_disj tm handle HOL_ERR _ => raise OF_ERR 1004 val {Bvar=x, Body=P} = dest_forall disj1 handle HOL_ERR _ => raise OF_ERR 1005 val {Bvar=y, Body=Q} = dest_forall disj2 handle HOL_ERR _ => raise OF_ERR 1006 in 1007 if not(x=y) then raise OF_ERR else 1008 if (free_in x P orelse free_in x Q) 1009 then raise ERR"OR_FORALL_CONV" 1010 ("`"^(#Name(dest_var x))^ "` free in disjuncts(s)") 1011 else SYM(FORALL_OR_CONV(mk_forall{Bvar=x,Body=mk_disj{disj1=P,disj2=Q}})) 1012 end 1013 handle (e as HOL_ERR{origin_structure = "lzConv", 1014 origin_function = "OR_FORALL_CONV",...}) => raise e 1015 | HOL_ERR _ => raise ERR "OR_FORALL_CONV" "" 1016end; 1017 1018(* ---------------------------------------------------------------------*) 1019(* LEFT_OR_FORALL_CONV : move universal quantifier out of conjunction. *) 1020(* *) 1021(* A call to LEFT_OR_FORALL_CONV "(!x.P) \/ Q" returns: *) 1022(* *) 1023(* |- (!x.P) \/ Q = (!x'. P[x'/x] \/ Q) *) 1024(* *) 1025(* Where x' is a primed variant of x not free in the input term *) 1026(* ---------------------------------------------------------------------*) 1027fun LEFT_OR_FORALL_CONV tm = 1028 let val {disj1,disj2} = dest_disj tm 1029 val {Bvar,Body} = dest_forall disj1 1030 val x' = variant (free_vars tm) Bvar 1031 val newp = subst[Bvar |-> x'] Body 1032 val aQ = ASSUME disj2 1033 val Pth = DISJ1 (SPEC x' (ASSUME disj1)) disj2 1034 val Qth = DISJ2 newp aQ 1035 val imp1 = DISCH tm (GEN x' (DISJ_CASES (ASSUME tm) Pth Qth)) 1036 val otm = rand(concl imp1) 1037 val thm1 = SPEC x' (ASSUME otm) 1038 val thm2 = CONTR newp (MP(ASSUME(mk_neg disj2)) aQ) 1039 val thm3 = DISJ1 (GEN x' (DISJ_CASES thm1 (ASSUME newp) thm2)) disj2 1040 val thm4 = DISJ2 disj1 aQ 1041 val imp2 = DISCH otm(DISJ_CASES(SPEC disj2 EXCLUDED_MIDDLE)thm4 thm3) 1042 in 1043 IMP_ANTISYM_RULE imp1 imp2 1044 end 1045 handle HOL_ERR _ => raise ERR "LEFT_OR_FORALL_CONV" ""; 1046 1047(* ---------------------------------------------------------------------*) 1048(* RIGHT_OR_FORALL_CONV : move universal quantifier out of conjunction. *) 1049(* *) 1050(* A call to RIGHT_OR_FORALL_CONV "P \/ (!x.Q)" returns: *) 1051(* *) 1052(* |- P \/ (!x.Q) = (!x'. P \/ (Q[x'/x]) *) 1053(* *) 1054(* where x' is a primed variant of x not free in the input term *) 1055(* ---------------------------------------------------------------------*) 1056fun RIGHT_OR_FORALL_CONV tm = 1057 let val {disj1,disj2} = dest_disj tm 1058 val {Bvar,Body} = dest_forall disj2 1059 val x' = variant (free_vars tm) Bvar 1060 val newq = subst[Bvar |-> x'] Body 1061 val Qth = DISJ2 disj1 (SPEC x' (ASSUME disj2)) 1062 val Pthm = ASSUME disj1 1063 val Pth = DISJ1 Pthm newq 1064 val imp1 = DISCH tm (GEN x' (DISJ_CASES (ASSUME tm) Pth Qth)) 1065 val otm = rand(concl imp1) 1066 val thm1 = SPEC x' (ASSUME otm) 1067 val thm2 = CONTR newq (MP(ASSUME(mk_neg disj1)) Pthm) 1068 val thm3 = DISJ2 disj1 (GEN x' (DISJ_CASES thm1 thm2 (ASSUME newq))) 1069 val thm4 = DISJ1 Pthm disj2 1070 val imp2 = DISCH otm(DISJ_CASES(SPEC disj1 EXCLUDED_MIDDLE)thm4 thm3) 1071 in 1072 IMP_ANTISYM_RULE imp1 imp2 1073 end 1074 handle HOL_ERR _ => raise ERR "RIGHT_OR_FORALL_CONV" ""; 1075 1076(* ---------------------------------------------------------------------*) 1077(* lzFORALL_IMP_CONV, implements the following axiom schemes. *) 1078(* *) 1079(* |- (!x. P[x]==>Q) = ((?x.P[x]) ==> Q) [x not free in Q] *) 1080(* *) 1081(* |- (!x. P==>Q[x]) = (P ==> (!x.Q[x])) [x not free in P] *) 1082(* *) 1083(* |- (!x. P==>Q) = ((?x.P) ==> (!x.Q)) [x not free in P==>Q] *) 1084(* *) 1085(* ---------------------------------------------------------------------*) 1086local val FI_ERR = ERR "lzFORALL_IMP_CONV" "expecting `!x. P ==> Q`" 1087in 1088fun lzFORALL_IMP_CONV tm = 1089 let val {Bvar,Body} = dest_forall tm handle HOL_ERR _ => raise FI_ERR 1090 val {ant,conseq} = dest_imp Body handle HOL_ERR _ => raise FI_ERR 1091 val fant = free_in Bvar ant 1092 and fconseq = free_in Bvar conseq 1093 in 1094 if (fant andalso fconseq) 1095 then raise ERR "lzFORALL_IMP_CONV" 1096 ("`"^(#Name(dest_var Bvar))^"` free on both sides of `==>`") 1097 else let val ltm = 1098 if fant then boolSyntax.mk_imp(boolSyntax.mk_exists(Bvar,ant),conseq) 1099 else if fconseq then boolSyntax.mk_imp(ant,boolSyntax.mk_forall(Bvar,conseq)) 1100 else boolSyntax.mk_imp(boolSyntax.mk_exists(Bvar,ant),boolSyntax.mk_forall(Bvar,conseq)) 1101 val jf = (fn _ => Conv.FORALL_IMP_CONV tm) 1102 in mk_lthm (fn _ => (boolSyntax.mk_eq(tm,ltm),jf)) jf end 1103 end 1104 handle (e as HOL_ERR{origin_structure = "lzConv", 1105 origin_function = "lzFORALL_IMP_CONV",...}) => raise e 1106 | HOL_ERR _ => raise ERR"lzFORALL_IMP_CONV" "" 1107end; 1108 1109(* ---------------------------------------------------------------------*) 1110(* LEFT_IMP_EXISTS_CONV, implements the following theorem-scheme: *) 1111(* *) 1112(* |- (?x. t1[x]) ==> t2 = !x'. t1[x'] ==> t2 *) 1113(* *) 1114(* where x' is a variant of x chosen not to be free in (?x.t1[x])==>t2 *) 1115(* *) 1116(* Author: Tom Melham *) 1117(* Revised: [TFM 90.07.01] *) 1118(*----------------------------------------------------------------------*) 1119fun LEFT_IMP_EXISTS_CONV tm = 1120 let val {ant, ...} = dest_imp tm 1121 val {Bvar,Body} = dest_exists ant 1122 val x' = variant (free_vars tm) Bvar 1123 val t' = subst [Bvar |-> x'] Body 1124 val th1 = GEN x' (DISCH t'(MP(ASSUME tm)(EXISTS(ant,x')(ASSUME t')))) 1125 val rtm = concl th1 1126 val th2 = CHOOSE (x',ASSUME ant) (UNDISCH(SPEC x'(ASSUME rtm))) 1127 in 1128 IMP_ANTISYM_RULE (DISCH tm th1) (DISCH rtm (DISCH ant th2)) 1129 end 1130 handle HOL_ERR _ => raise ERR "LEFT_IMP_EXISTS_CONV" ""; 1131 1132(* ---------------------------------------------------------------------*) 1133(* RIGHT_IMP_FORALL_CONV, implements the following theorem-scheme: *) 1134(* *) 1135(* |- (t1 ==> !x. t2) = !x'. t1 ==> t2[x'/x] *) 1136(* *) 1137(* where x' is a variant of x chosen not to be free in the input term. *) 1138(*----------------------------------------------------------------------*) 1139fun RIGHT_IMP_FORALL_CONV tm = 1140 let val {ant,conseq} = dest_imp tm 1141 val {Bvar,Body} = dest_forall conseq 1142 val x' = variant (free_vars tm) Bvar 1143 val t' = subst [Bvar |-> x'] Body 1144 val imp1 = DISCH tm (GEN x' (DISCH ant(SPEC x'(UNDISCH(ASSUME tm))))) 1145 val ctm = rand(concl imp1) 1146 val alph = GEN_ALPHA_CONV Bvar (mk_forall{Bvar = x', Body = t'}) 1147 val thm1 = EQ_MP alph (GEN x'(UNDISCH (SPEC x' (ASSUME ctm)))) 1148 val imp2 = DISCH ctm (DISCH ant thm1) 1149 in 1150 IMP_ANTISYM_RULE imp1 imp2 1151 end 1152 handle HOL_ERR _ => raise ERR "RIGHT_IMP_FORALL_CONV" ""; 1153 1154 1155(* ---------------------------------------------------------------------*) 1156(* EXISTS_IMP_CONV, implements the following axiom schemes. *) 1157(* *) 1158(* |- (?x. P==>Q[x]) = (P ==> (?x.Q[x])) [x not free in P] *) 1159(* *) 1160(* |- (?x. P[x]==>Q) = ((!x.P[x]) ==> Q) [x not free in Q] *) 1161(* *) 1162(* |- (?x. P==>Q) = ((!x.P) ==> (?x.Q)) [x not free in P==>Q] *) 1163(* ---------------------------------------------------------------------*) 1164local val EI_ERR = ERR"EXISTS_IMP_CONV" "expecting `?x. P ==> Q`" 1165in 1166fun EXISTS_IMP_CONV tm = 1167 let val {Bvar,Body} = dest_exists tm handle HOL_ERR _ => raise EI_ERR 1168 val {ant = P,conseq = Q} = dest_imp Body handle HOL_ERR _ => raise EI_ERR 1169 val fP = free_in Bvar P 1170 and fQ = free_in Bvar Q 1171 in 1172 if (fP andalso fQ) then raise ERR "EXISTS_IMP_CONV" 1173 ("`"^(#Name(dest_var Bvar))^ "` free on both sides of `==>`") else 1174 if fP 1175 then let val allp = mk_forall{Bvar = Bvar, Body = P} 1176 val th1 = SPEC Bvar (ASSUME allp) 1177 val thm1 = MP (ASSUME Body) th1 1178 val imp1 = DISCH tm (CHOOSE(Bvar,ASSUME tm)(DISCH allp thm1)) 1179 val otm = rand(concl imp1) 1180 val thm2 = EXISTS(tm,Bvar)(DISCH P (UNDISCH(ASSUME otm))) 1181 val notP = mk_neg P 1182 val notP_thm = ASSUME notP 1183 val nex = mk_exists{Bvar = Bvar, Body = notP} 1184 val asm1 = EXISTS (nex, Bvar) notP_thm 1185 val th2 = CCONTR P (MP (ASSUME (mk_neg nex)) asm1) 1186 val th3 = CCONTR nex (MP (ASSUME (mk_neg allp)) (GEN Bvar th2)) 1187 val thm4 = DISCH P (CONTR Q (UNDISCH notP_thm)) 1188 val thm5 = CHOOSE(Bvar,th3)(EXISTS(tm,Bvar)thm4) 1189 val thm6 = DISJ_CASES (SPEC allp EXCLUDED_MIDDLE) thm2 thm5 1190 in 1191 IMP_ANTISYM_RULE imp1 (DISCH otm thm6) 1192 end 1193 else 1194 if fQ 1195 then let val thm1 = EXISTS (mk_exists{Bvar=Bvar, Body=Q},Bvar) 1196 (UNDISCH(ASSUME Body)) 1197 val imp1 = DISCH tm (CHOOSE(Bvar,ASSUME tm) (DISCH P thm1)) 1198 val thm2 = UNDISCH (ASSUME (rand(concl imp1))) 1199 val thm3 = CHOOSE(Bvar,thm2) (EXISTS(tm,Bvar)(DISCH P(ASSUME Q))) 1200 val thm4 = EXISTS(tm,Bvar) 1201 (DISCH P (CONTR Q(UNDISCH(ASSUME(mk_neg P))))) 1202 val thm5 = DISJ_CASES (SPEC P EXCLUDED_MIDDLE) thm3 thm4 1203 in 1204 IMP_ANTISYM_RULE imp1 (DISCH(rand(concl imp1)) thm5) 1205 end 1206 else let val eQ = mk_exists{Bvar = Bvar, Body = Q} 1207 and aP = mk_forall{Bvar = Bvar, Body = P} 1208 val thm1 = EXISTS(eQ,Bvar)(UNDISCH(ASSUME Body)) 1209 val thm2 = DISCH aP (PROVE_HYP (SPEC Bvar (ASSUME aP)) thm1) 1210 val imp1 = DISCH tm (CHOOSE(Bvar,ASSUME tm) thm2) 1211 val thm2 = CHOOSE(Bvar,UNDISCH(ASSUME(rand(concl imp1))))(ASSUME Q) 1212 val thm3 = DISCH P (PROVE_HYP (GEN Bvar (ASSUME P)) thm2) 1213 val imp2 = DISCH (rand(concl imp1)) (EXISTS(tm,Bvar) thm3) 1214 in 1215 IMP_ANTISYM_RULE imp1 imp2 1216 end 1217 end 1218 handle (e as HOL_ERR{origin_structure = "lzConv", 1219 origin_function = "EXISTS_IMP_CONV",...}) => raise e 1220 | HOL_ERR _ => raise ERR"EXISTS_IMP_CONV" "" 1221end; 1222 1223(* ---------------------------------------------------------------------*) 1224(* LEFT_IMP_FORALL_CONV, implements the following theorem-scheme: *) 1225(* *) 1226(* |- (!x. t1[x]) ==> t2 = ?x'. t1[x'] ==> t2 *) 1227(* *) 1228(* where x' is a variant of x chosen not to be free in the input term *) 1229(*----------------------------------------------------------------------*) 1230fun LEFT_IMP_FORALL_CONV tm = 1231 let val {ant,conseq} = dest_imp tm 1232 val {Bvar,Body} = dest_forall ant 1233 val x' = variant (free_vars tm) Bvar 1234 val t1' = subst [Bvar |-> x'] Body 1235 val not_t1'_thm = ASSUME (mk_neg t1') 1236 val th1 = SPEC x' (ASSUME ant) 1237 val new_imp = mk_imp{ant = t1', conseq = conseq} 1238 val thm1 = MP (ASSUME new_imp) th1 1239 val otm = mk_exists{Bvar = x', Body = new_imp} 1240 val imp1 = DISCH otm (CHOOSE(x',ASSUME otm)(DISCH ant thm1)) 1241 val thm2 = EXISTS(otm,x') (DISCH t1' (UNDISCH(ASSUME tm))) 1242 val nex = mk_exists{Bvar = x', Body = mk_neg t1'} 1243 val asm1 = EXISTS (nex, x') not_t1'_thm 1244 val th2 = CCONTR t1' (MP (ASSUME (mk_neg nex)) asm1) 1245 val th3 = CCONTR nex (MP(ASSUME(mk_neg ant)) (GEN x' th2)) 1246 val thm4 = DISCH t1' (CONTR conseq (UNDISCH not_t1'_thm)) 1247 val thm5 = CHOOSE(x',th3) 1248 (EXISTS(mk_exists{Bvar = x',Body = concl thm4},x')thm4) 1249 val thm6 = DISJ_CASES (SPEC ant EXCLUDED_MIDDLE) thm2 thm5 1250 in 1251 IMP_ANTISYM_RULE (DISCH tm thm6) imp1 1252 end 1253 handle HOL_ERR _ => raise ERR "LEFT_IMP_FORALL_CONV" ""; 1254 1255(* ---------------------------------------------------------------------*) 1256(* RIGHT_IMP_EXISTS_CONV, implements the following theorem-scheme: *) 1257(* *) 1258(* |- (t1 ==> ?x. t2) = ?x'. t1 ==> t2[x'/x] *) 1259(* *) 1260(* where x' is a variant of x chosen not to be free in the input term. *) 1261(*----------------------------------------------------------------------*) 1262fun RIGHT_IMP_EXISTS_CONV tm = 1263 let val {ant,conseq} = dest_imp tm 1264 val {Bvar,Body} = dest_exists conseq 1265 val x' = variant (free_vars tm) Bvar 1266 val t2' = subst [Bvar |-> x'] Body 1267 val new_imp = mk_imp{ant = ant, conseq = t2'} 1268 val otm = mk_exists{Bvar = x', Body = new_imp} 1269 val thm1 = EXISTS(conseq,x')(UNDISCH(ASSUME new_imp)) 1270 val imp1 = DISCH otm (CHOOSE(x',ASSUME otm) (DISCH ant thm1)) 1271 val thm2 = UNDISCH (ASSUME tm) 1272 val thm3 = CHOOSE (x',thm2) (EXISTS (otm,x') (DISCH ant (ASSUME t2'))) 1273 val thm4 = DISCH ant (CONTR t2'(UNDISCH(ASSUME(mk_neg ant)))) 1274 val thm5 = EXISTS(otm,x') thm4 1275 val thm6 = DISJ_CASES (SPEC ant EXCLUDED_MIDDLE) thm3 thm5 1276 in 1277 IMP_ANTISYM_RULE (DISCH tm thm6) imp1 1278 end 1279 handle HOL_ERR _ => raise ERR "RIGHT_IMP_EXISTS_CONV" ""; 1280 1281(* ---------------------------------------------------------------------*) 1282(* X_SKOLEM_CONV : introduce a skolem function. *) 1283(* *) 1284(* |- (!x1...xn. ?y. tm[x1,...,xn,y]) *) 1285(* = *) 1286(* (?f. !x1...xn. tm[x1,..,xn,f x1 ... xn] *) 1287(* *) 1288(* The first argument is the function f. *) 1289(* ---------------------------------------------------------------------*) 1290 1291fun X_SKOLEM_CONV v = 1292 if not(is_var v) 1293 then raise ERR "X_SKOLEM_CONV" "first argument not a variable" 1294 else 1295 fn tm => 1296 let val (xs,ex) = strip_forall tm 1297 val (ab as {Bvar,Body}) = dest_exists ex handle HOL_ERR _ 1298 => raise ERR "X_SKOLEM_CONV" "expecting `!x1...xn. ?y.tm`" 1299 val fx = Term.list_mk_comb(v,xs) handle HOL_ERR _ 1300 => raise ERR "X_SKOLEM_CONV" "function variable has wrong type" 1301 in 1302 if free_in v tm then raise ERR"X_SKOLEM_CONV" 1303 ("`"^(#Name(dest_var v))^"` free in the input term") 1304 else let val pat_bod = list_mk_forall(xs,subst[Bvar |-> fx]Body) 1305 val pat = mk_exists{Bvar = v, Body = pat_bod} 1306 val fnn = list_mk_abs(xs,mk_select ab) 1307 val bth = SYM(LIST_BETA_CONV (Term.list_mk_comb(fnn,xs))) 1308 val thm1 = SUBST [Bvar |-> bth] Body 1309 (SELECT_RULE (SPECL xs (ASSUME tm))) 1310 val imp1 = DISCH tm (EXISTS (pat,fnn) (GENL xs thm1)) 1311 val thm2 = SPECL xs (ASSUME pat_bod) 1312 val thm3 = GENL xs (EXISTS (ex,fx) thm2) 1313 val imp2 = DISCH pat (CHOOSE (v,ASSUME pat) thm3) 1314 in 1315 IMP_ANTISYM_RULE imp1 imp2 1316 end 1317 end 1318 handle (e as HOL_ERR{origin_structure = "lzConv", 1319 origin_function = "X_SKOLEM_CONV",...}) => raise e 1320 | HOL_ERR _ => raise ERR "X_SKOLEM_CONV" ""; 1321 1322(* ---------------------------------------------------------------------*) 1323(* SKOLEM_CONV : introduce a skolem function. *) 1324(* *) 1325(* |- (!x1...xn. ?y. tm[x1,...,xn,y]) *) 1326(* = *) 1327(* (?y'. !x1...xn. tm[x1,..,xn,y' x1 ... xn] *) 1328(* *) 1329(* Where y' is a primed variant of y not free in the input term. *) 1330(* ---------------------------------------------------------------------*) 1331 1332local fun mkfty tm ty = type_of tm --> ty 1333in 1334fun SKOLEM_CONV tm = 1335 let val (xs,ex) = strip_forall tm 1336 val {Bvar, ...} = dest_exists ex 1337 val {Name,Ty} = dest_var Bvar 1338 val fv = mk_var{Name=Name, Ty = itlist mkfty xs Ty} 1339 in 1340 X_SKOLEM_CONV (variant (free_vars tm) fv) tm 1341 end 1342 handle HOL_ERR _ => raise ERR "SKOLEM_CONV" "" 1343end; 1344 1345 1346(*----------------------------------------------------------------------*) 1347(* SYM_CONV : a conversion for symmetry of equality. *) 1348(* *) 1349(* e.g. SYM_CONV "x=y" ----> (x=y) = (y=x). *) 1350(*----------------------------------------------------------------------*) 1351 1352fun SYM_CONV tm = 1353 let val {lhs,rhs} = dest_eq tm 1354 val th = INST_TYPE [Type.alpha |-> type_of lhs] EQ_SYM_EQ 1355 in 1356 SPECL [lhs,rhs] th 1357 end 1358 handle HOL_ERR _ => raise ERR "SYM_CONV" ""; 1359 1360 1361(*--------------------------------------------------------------------------- 1362 * 1363 * A |- t1 = t2 1364 * -------------- (t2' got from t2 using a conversion) 1365 * A |- t1 = t2' 1366 *---------------------------------------------------------------------------*) 1367 1368fun RIGHT_CONV_RULE conv th = 1369 TRANS th (conv(rhs(concl th))) handle UNCHANGED => th 1370 1371(* ---------------------------------------------------------------------*) 1372(* FUN_EQ_CONV "f = g" returns: |- (f = g) = !x. (f x = g x). *) 1373(* *) 1374(* Notes: f and g must be functions. The conversion choses an "x" not *) 1375(* free in f or g. This conversion just states that functions are equal *) 1376(* IFF the results of applying them to an arbitrary value are equal. *) 1377(* *) 1378(* New version: TFM 88.03.31 *) 1379(* ---------------------------------------------------------------------*) 1380fun FUN_EQ_CONV tm = 1381 let val (ty1,_) = dom_rng(type_of (lhs tm)) 1382 val vars = free_vars tm 1383 val varnm = if Type.is_vartype ty1 then "x" 1384 else Char.toString (Lib.trye hd 1385 (String.explode (fst(Type.dest_type ty1)))) 1386 val x = variant vars (mk_var{Name=varnm, Ty=ty1}) 1387 val imp1 = DISCH_ALL (GEN x (AP_THM (ASSUME tm) x)) 1388 val asm = ASSUME (concl (GEN x (AP_THM (ASSUME tm) x))) 1389 in 1390 IMP_ANTISYM_RULE imp1 (DISCH_ALL (EXT asm)) 1391 end 1392 handle HOL_ERR _ => raise ERR "FUN_EQ_CONV" ""; 1393 1394 1395(* --------------------------------------------------------------------- *) 1396(* X_FUN_EQ_CONV "x" "f = g" *) 1397(* *) 1398(* yields |- (f = g) = !x. f x = g x *) 1399(* *) 1400(* fails if x free in f or g, or x not of the right type. *) 1401(* --------------------------------------------------------------------- *) 1402 1403fun X_FUN_EQ_CONV x tm = 1404 if not(is_var x) 1405 then raise ERR "X_FUN_EQ_CONV" "first arg is not a variable" 1406 else 1407 if mem x (free_vars tm) 1408 then raise ERR"X_FUN_EQ_CONV" (#Name(dest_var x)^" is a free variable") 1409 else 1410 let val (ty,_) = with_exn dom_rng(type_of(lhs tm)) 1411 (ERR "X_FUN_EQ_CONV" "lhs and rhs not functions") 1412 in 1413 if ty = type_of x 1414 then let val imp1 = DISCH_ALL (GEN x (AP_THM (ASSUME tm) x)) 1415 val asm = ASSUME (concl (GEN x (AP_THM (ASSUME tm) x))) 1416 in IMP_ANTISYM_RULE imp1 (DISCH_ALL (EXT asm)) 1417 end 1418 else raise ERR "X_FUN_EQ_CONV" (#Name(dest_var x)^" has the wrong type") 1419 end 1420 handle e => raise (wrap_exn "lzConv" "X_FUN_EQ_CONV" e); 1421 1422(* ---------------------------------------------------------------------*) 1423(* SELECT_CONV: a conversion for introducing "?" when P [@x.P[x]]. *) 1424(* *) 1425(* SELECT_CONV "P [@x.P [x]]" ---> |- P [@x.P [x]] = ?x. P[x] *) 1426(* *) 1427(* Added: TFM 88.03.31 *) 1428(* ---------------------------------------------------------------------*) 1429(* fun SELECT_CONV tm = 1430** let val epsl = find_terms is_select tm 1431** fun findfn t = (tm = subst [{redex = #Bvar (dest_select t), 1432** residue = t}] 1433** (#Body (dest_select t))) 1434** val sel = first findfn epsl 1435** val ex = mk_exists(dest_select sel) 1436** val imp1 = DISCH_ALL (SELECT_RULE (ASSUME ex)) 1437** and imp2 = DISCH_ALL (EXISTS (ex,sel) (ASSUME tm)) 1438** in 1439** IMP_ANTISYM_RULE imp2 imp1 1440** end 1441** handle _ => raise ERR{function = "SELECT_CONV", message = ""}; 1442*) 1443 1444local val f = mk_var{Name="f",Ty=alpha-->bool} 1445 val th1 = AP_THM EXISTS_DEF f 1446 val th2 = CONV_RULE (RAND_CONV BETA_CONV) th1 1447 val tyv = Type.mk_vartype "'a" 1448 fun EXISTS_CONV{Bvar,Body} = 1449 let val ty = type_of Bvar 1450 val ins = INST_TYPE [tyv |-> ty] th2 1451 val theta = [inst [tyv |-> ty] f |-> mk_abs{Bvar=Bvar,Body=Body}] 1452 val th = INST theta ins 1453 in 1454 CONV_RULE (RAND_CONV BETA_CONV) th 1455 end 1456 fun find_first p tm = 1457 if (p tm) then tm 1458 else if (is_abs tm) 1459 then find_first p (body tm) 1460 else if is_comb tm 1461 then let val {Rator,Rand} = dest_comb tm 1462 in find_first p Rator 1463 handle HOL_ERR _ => find_first p Rand 1464 end 1465 else raise ERR"SELECT_CONV.find_first" "" 1466in 1467fun SELECT_CONV tm = 1468 let fun right t = 1469 let val {Bvar,Body} = dest_select t 1470 in Term.aconv (subst[Bvar |-> t] Body) tm 1471 end handle HOL_ERR _ => false 1472 val epi = find_first right tm 1473 in 1474 SYM (EXISTS_CONV (dest_select epi)) 1475 end 1476 handle HOL_ERR _ => raise ERR "SELECT_CONV" "" 1477end; 1478 1479(* ---------------------------------------------------------------------*) 1480(* CONTRAPOS_CONV: convert an implication to its contrapositive. *) 1481(* *) 1482(* CONTRAPOS_CONV "a ==> b" --> |- (a ==> b) = (~b ==> ~a) *) 1483(* *) 1484(* Added: TFM 88.03.31 *) 1485(* Revised: TFM 90.07.13 *) 1486(* ---------------------------------------------------------------------*) 1487 1488fun CONTRAPOS_CONV tm = 1489 let val {ant,conseq} = dest_imp tm 1490 val negc = mk_neg conseq 1491 and contra = mk_imp{ant = mk_neg conseq, conseq = mk_neg ant} 1492 val imp1 = DISCH negc (NOT_INTRO(IMP_TRANS(ASSUME tm)(ASSUME negc))) 1493 and imp2 = DISCH ant (CCONTR conseq (UNDISCH (UNDISCH (ASSUME contra)))) 1494 in 1495 IMP_ANTISYM_RULE (DISCH tm imp1) (DISCH contra imp2) 1496 end 1497 handle HOL_ERR _ => raise ERR "CONTRAPOS_CONV" ""; 1498 1499(* ---------------------------------------------------------------------*) 1500(* ANTE_CONJ_CONV: convert an implication with conjuncts in its *) 1501(* antecedant to a series of implications. *) 1502(* *) 1503(* ANTE_CONJ_CONV "a1 /\ a2 ==> c" *) 1504(* ----> |- a1 /\ a2 ==> c = (a1 ==> (a2 ==> c)) *) 1505(* *) 1506(* Added: TFM 88.03.31 *) 1507(* ---------------------------------------------------------------------*) 1508 1509fun ANTE_CONJ_CONV tm = 1510 let val {ant,conseq} = dest_imp tm 1511 val {conj1,conj2} = dest_conj ant 1512 val ant_thm = ASSUME ant 1513 val imp1 = MP (ASSUME tm) (CONJ (ASSUME conj1) (ASSUME conj2)) 1514 and imp2 = LIST_MP [CONJUNCT1 ant_thm,CONJUNCT2 ant_thm] 1515 (ASSUME (mk_imp{ant=conj1, 1516 conseq=mk_imp{ant=conj2, conseq=conseq}})) 1517 in 1518 IMP_ANTISYM_RULE 1519 (DISCH_ALL (DISCH conj1 (DISCH conj2 imp1))) 1520 (DISCH_ALL (DISCH ant imp2)) 1521 end 1522 handle HOL_ERR _ => raise ERR "ANTE_CONJ_CONV" ""; 1523 1524 1525(* ---------------------------------------------------------------------*) 1526(* SWAP_EXISTS_CONV: swap the order of existentially quantified vars. *) 1527(* *) 1528(* SWAP_EXISTS_CONV "?x y.t[x,y]" ---> |- ?x y.t[x,y] = ?y x.t[x,y] *) 1529(* *) 1530(* AUTHOR: Paul Loewenstein 3 May 1988 *) 1531(* ---------------------------------------------------------------------*) 1532 1533fun SWAP_EXISTS_CONV xyt = 1534 let val {Bvar=x, Body=yt} = dest_exists xyt 1535 val {Bvar=y, Body=t} = dest_exists yt 1536 val xt = mk_exists {Bvar=x, Body=t} 1537 val yxt = mk_exists{Bvar=y, Body=xt} 1538 val t_thm = ASSUME t 1539 in 1540 IMP_ANTISYM_RULE 1541 (DISCH xyt (CHOOSE (x,ASSUME xyt) (CHOOSE (y, (ASSUME yt)) 1542 (EXISTS (yxt,y) (EXISTS (xt,x) t_thm))))) 1543 (DISCH yxt (CHOOSE (y,ASSUME yxt) (CHOOSE (x, (ASSUME xt)) 1544 (EXISTS (xyt,x) (EXISTS (yt,y) t_thm))))) 1545 end 1546 handle HOL_ERR _ => raise ERR "SWAP_EXISTS_CONV" ""; 1547 1548 1549(* ---------------------------------------------------------------------*) 1550(* bool_EQ_CONV: conversion for boolean equality. *) 1551(* *) 1552(* bool_EQ_CONV "b1 = b2" returns: *) 1553(* *) 1554(* |- (b1 = b2) = T if b1 and b2 are identical boolean terms *) 1555(* |- (b1 = b2) = b2 if b1 = "T" *) 1556(* |- (b1 = b2) = b1 if b2 = "T" *) 1557(* *) 1558(* Added TFM 88.03.31 *) 1559(* Revised TFM 90.07.24 *) 1560(* ---------------------------------------------------------------------*) 1561 1562local val (Tb::bT::_) = map (GEN (--`b:bool`--)) 1563 (CONJUNCTS (SPEC (--`b:bool`--) EQ_CLAUSES)) 1564in 1565fun bool_EQ_CONV tm = 1566 let val {lhs,rhs} = dest_eq tm 1567 val _ = if type_of rhs = Type.bool then () 1568 else raise ERR"bool_EQ_CONV" "does not have boolean type" 1569 in if lhs=rhs then EQT_INTRO (REFL lhs) else 1570 if lhs=T then SPEC rhs Tb else 1571 if rhs=T then SPEC lhs bT 1572 else raise ERR"bool_EQ_CONV" "inapplicable" 1573 end 1574 handle e => raise (wrap_exn "lzConv" "bool_EQ_CONV" e) 1575end; 1576 1577(* ---------------------------------------------------------------------*) 1578(* EXISTS_UNIQUE_CONV: expands with the definition of unique existence. *) 1579(* *) 1580(* *) 1581(* EXISTS_UNIQUE_CONV "?!x.P[x]" yields the theorem: *) 1582(* *) 1583(* |- ?!x.P[x] = ?x.P[x] /\ !x y. P[x] /\ P[y] ==> (x=y) *) 1584(* *) 1585(* ADDED: TFM 90.05.06 *) 1586(* *) 1587(* REVISED: now uses a variant of x for y in 2nd conjunct [TFM 90.06.11]*) 1588(* ---------------------------------------------------------------------*) 1589 1590local val v = genvar Type.bool 1591 val AND = boolSyntax.conjunction 1592 val IMP = boolSyntax.implication 1593 val check = assert boolSyntax.is_exists1 1594 fun MK_BIN f (e1,e2) = MK_COMB((AP_TERM f e1),e2) 1595 val rule = CONV_RULE o RAND_CONV o GEN_ALPHA_CONV 1596 fun MK_ALL x y tm = rule y (FORALL_EQ x tm) 1597 fun handle_ant{conj1, conj2} = (BETA_CONV conj1, BETA_CONV conj2) 1598 fun conv (nx,ny) t = 1599 case strip_forall t 1600 of ([ox,oy],imp) => 1601 let val {ant,conseq} = dest_imp imp 1602 val ant' = MK_BIN AND (handle_ant (dest_conj ant)) 1603 in MK_ALL ox nx 1604 (MK_ALL oy ny (MK_BIN IMP (ant',REFL conseq))) 1605 end 1606 | otherwise => raise ERR "EXISTS_UNIQUE" "" 1607in 1608fun EXISTS_UNIQUE_CONV tm = 1609 let val _ = check tm 1610 val {Rator,Rand} = dest_comb tm 1611 val (ab as {Bvar,Body}) = dest_abs Rand 1612 val def = INST_TYPE [alpha |-> type_of Bvar] EXISTS_UNIQUE_DEF 1613 val exp = RIGHT_BETA(AP_THM def Rand) 1614 and y = variant (all_vars Body) Bvar 1615 in 1616 SUBST [v |-> conv (Bvar,y) (rand(rand(concl exp)))] 1617 (mk_eq{lhs=tm, rhs=mk_conj{conj1=mk_exists ab, conj2=v}}) exp 1618 end 1619 handle HOL_ERR _ => raise ERR "EXISTS_UNIQUE_CONV" "" 1620end; 1621 1622 1623(* ---------------------------------------------------------------------*) 1624(* COND_CONV: conversion for simplifying conditionals: *) 1625(* *) 1626(* --------------------------- COND_CONV "T => u | v" *) 1627(* |- (T => u | v) = u *) 1628(* *) 1629(* *) 1630(* --------------------------- COND_CONV "F => u | v" *) 1631(* |- (F => u | v) = v *) 1632(* *) 1633(* *) 1634(* --------------------------- COND_CONV "b => u | u" *) 1635(* |- (b => u | u) = u *) 1636(* *) 1637(* --------------------------- COND_CONV "b => u | v" (u =alpha v) *) 1638(* |- (b => u | v) = u *) 1639(* *) 1640(* COND_CONV "P=>u|v" fails if P is neither "T" nor "F" and u =/= v. *) 1641(* ---------------------------------------------------------------------*) 1642 1643local val vt = genvar alpha 1644 and vf = genvar alpha 1645 val gen = GENL [vt,vf] 1646 val (CT,CF) = (gen ## gen) (CONJ_PAIR (SPECL [vt,vf] COND_CLAUSES)) 1647in 1648fun COND_CONV tm = 1649 let val {cond,larm,rarm} = dest_cond tm 1650 val INST_TYPE' = INST_TYPE [alpha |-> type_of larm] 1651 in 1652 if (cond=T) then SPEC rarm (SPEC larm (INST_TYPE' CT)) else 1653 if (cond=F) then SPEC rarm (SPEC larm (INST_TYPE' CF)) else 1654 if (larm=rarm) then SPEC larm (SPEC cond (INST_TYPE' COND_ID)) else 1655 if (aconv larm rarm) 1656 then let val cnd = AP_TERM (rator tm) (ALPHA rarm larm) 1657 val th = SPEC larm (SPEC cond (INST_TYPE' COND_ID)) 1658 in TRANS cnd th 1659 end 1660 else raise ERR "" "" 1661 end 1662 handle HOL_ERR _ => raise ERR "COND_CONV" "" 1663end; 1664 1665 1666(* ===================================================================== *) 1667(* A rule defined using conversions. *) 1668(* ===================================================================== *) 1669 1670 1671(* ---------------------------------------------------------------------*) 1672(* EXISTENCE: derives existence from unique existence: *) 1673(* *) 1674(* |- ?!x. P[x] *) 1675(* -------------------- *) 1676(* |- ?x. P[x] *) 1677(* *) 1678(* ---------------------------------------------------------------------*) 1679 1680local val EXISTS_UNIQUE_DEF = boolTheory.EXISTS_UNIQUE_DEF 1681 val P = mk_var{Name="P", Ty=alpha-->bool} 1682 val th1 = SPEC P (CONV_RULE (X_FUN_EQ_CONV P) EXISTS_UNIQUE_DEF) 1683 val th2 = CONJUNCT1(UNDISCH(fst(EQ_IMP_RULE(RIGHT_BETA th1)))) 1684 val ex1P = mk_comb{Rator=boolSyntax.exists1, Rand=P} 1685 1686in 1687fun EXISTENCE th = 1688 let val _ = assert boolSyntax.is_exists1 (concl th) 1689 val {Rator,Rand} = dest_comb(concl th) 1690 val {Bvar,...} = dest_abs Rand 1691 in 1692 MP (SPEC Rand (INST_TYPE [alpha |-> type_of Bvar] 1693 (GEN P (DISCH ex1P th2)))) th 1694 end 1695 handle HOL_ERR _ => raise ERR "EXISTENCE" "" 1696end; 1697 1698 1699(*-----------------------------------------------------------------------*) 1700(* AC_CONV - Prove equality using associative + commutative laws *) 1701(* *) 1702(* The conversion is given an associative and commutative law (it deduces*) 1703(* the relevant operator and type from these) in the form of the inbuilt *) 1704(* ones, and an equation to prove. It will try to prove this. Example: *) 1705(* *) 1706(* AC_CONV(ADD_ASSOC,ADD_SYM) "(1 + 3) + (2 + 4) = 4 + (3 + (2 + 1))" *) 1707(* [JRH 91.07.17] *) 1708(*-----------------------------------------------------------------------*) 1709 1710fun AC_CONV(associative,commutative) = 1711 let val opr = (rator o rator o lhs o snd o strip_forall o concl) commutative 1712 val ty = (hd o #Args o dest_type o type_of) opr 1713 val x = mk_var{Name="x",Ty=ty} 1714 and y = mk_var{Name="y",Ty=ty} 1715 and z = mk_var{Name="z",Ty=ty} 1716 val xy = mk_comb{Rator=mk_comb{Rator=opr,Rand=x},Rand=y} 1717 and yz = mk_comb{Rator=mk_comb{Rator=opr,Rand=y},Rand=z} 1718 and yx = mk_comb{Rator=mk_comb{Rator=opr,Rand=y},Rand=x} 1719 val comm = PART_MATCH I commutative (mk_eq{lhs=xy,rhs=yx}) 1720 and ass = PART_MATCH I (SYM (SPEC_ALL associative)) 1721 (mk_eq{lhs=mk_comb{Rator=mk_comb{Rator=opr,Rand=xy},Rand=z}, 1722 rhs=mk_comb{Rator=mk_comb{Rator=opr,Rand=x},Rand=yz}}) 1723 val asc = TRANS (SUBS [comm] (SYM ass)) (INST [y |-> x, x |-> y] ass) 1724 1725 fun bubble head expr = 1726 let val {Rator,Rand=r} = dest_comb expr 1727 val {Rator=xopr, Rand = l} = dest_comb Rator 1728 in 1729 if term_eq xopr opr 1730 then if term_eq l head then REFL expr 1731 else if term_eq r head then INST [x |-> l, y |-> r] comm 1732 else let val subb = bubble head r 1733 val eqv = AP_TERM (mk_comb{Rator=xopr,Rand=l}) subb 1734 val {Rator,Rand=r'} = dest_comb(#rhs(dest_eq(concl subb))) 1735 val {Rator=yopr,Rand=l'} = dest_comb Rator 1736 in 1737 TRANS eqv (INST[x |-> l, y |-> l', z |-> r'] asc) 1738 end 1739 else raise ERR"AC_CONV" "bubble" 1740 end 1741 1742 fun asce {lhs,rhs} = 1743 if term_eq lhs rhs then REFL lhs 1744 else let val {Rator,Rand=r'} = dest_comb lhs 1745 val {Rator=zopr,Rand=l'} = dest_comb Rator 1746 in 1747 if term_eq zopr opr 1748 then let val beq = bubble l' rhs 1749 val rt = boolSyntax.rhs (concl beq) 1750 in TRANS (AP_TERM (mk_comb{Rator=opr,Rand=l'}) 1751 (asce{lhs=rand lhs, rhs=rand rt})) 1752 (SYM beq) 1753 end 1754 else raise ERR"AC_CONV" "asce" 1755 end 1756 in 1757 fn tm => 1758 let val init = QCONV (TOP_DEPTH_CONV (REWR_CONV ass)) tm 1759 val gl = rhs (concl init) 1760 in EQT_INTRO (EQ_MP (SYM init) (asce (dest_eq gl))) 1761 end 1762 end 1763 handle e => raise (wrap_exn "lzConv" "AC_CONV" e); 1764 1765(*-----------------------------------------------------------------------*) 1766(* GSYM - General symmetry rule *) 1767(* *) 1768(* Reverses the first equation(s) encountered in a top-down search. *) 1769(* *) 1770(* [JRH 92.03.28] *) 1771(*-----------------------------------------------------------------------*) 1772 1773val GSYM = CONV_RULE(ONCE_DEPTH_CONV SYM_CONV); 1774 1775(*--------------------------------------------------------------------------- 1776 Conversions for messing with bound variables. 1777 1778 RENAME_VARS_CONV renames variables under \ ! ? ?! or @ . 1779 SWAP_VARS_CONV swaps variables under ! and ?, 1780 e.g, given !x y. ... gives !y x. ... 1781 ---------------------------------------------------------------------------*) 1782local 1783 fun rename vname t = let 1784 val (accessor, C_ACC) = 1785 if is_exists t orelse is_forall t orelse is_select t orelse 1786 is_exists1 t 1787 then (rand, RAND_CONV) 1788 else if is_abs t then (I, I) 1789 else raise ERR "rename_vars" "Term not a binder" 1790 val (ty, _) = dom_rng (type_of (accessor t)) 1791 val newv = mk_var{Name=vname, Ty=ty} 1792 in 1793 C_ACC (ALPHA_CONV newv) t 1794 end 1795in 1796 fun RENAME_VARS_CONV varlist = 1797 case varlist of 1798 [] => REFL 1799 | (v::vs) => rename v THENC BINDER_CONV (RENAME_VARS_CONV vs) 1800 1801 1802 fun lzSWAP_VARS_CONV term = 1803 let val (l,bod) = strip_forall term 1804 (*val _ = DMSG (TM (list_mk_forall([hd(tl l),hd l]@List.drop(l,2),bod))) dbglzc(*DBG*)*) 1805 val jf = (fn _ => let val (dest, list_mk, qvar_thm) = 1806 if (is_exists term) then 1807 (dest_exists, LIST_MK_EXISTS, boolTheory.SWAP_EXISTS_THM) 1808 else 1809 (dest_forall, C (foldr(uncurry FORALL_EQ)), boolTheory.SWAP_FORALL_THM) 1810 val {Bvar = fst_var, Body = fst_body} = dest term 1811 val {Bvar = snd_var, Body = snd_body} = dest fst_body 1812 val fnc = list_mk_abs ([fst_var,snd_var], snd_body) 1813 val fn_rewrite = 1814 SYM (LIST_BETA_CONV (list_mk_comb (fnc, [fst_var,snd_var]))) 1815 val ex_rewrite = list_mk [fst_var,snd_var] fn_rewrite 1816 val inst_thm = ISPEC fnc qvar_thm 1817 val final_thm = 1818 TRANS inst_thm 1819 (RENAME_VARS_CONV (map (#Name o dest_var) [snd_var,fst_var]) 1820 (rhs (concl inst_thm))) 1821 in 1822 (* must do precisely two beta reductions on the right hand side of the 1823 theorem *) 1824 CONV_RULE (RAND_CONV (BINDER_CONV (BINDER_CONV LIST_BETA_CONV))) 1825 (SUBS [final_thm] ex_rewrite) 1826 end) 1827 val res = mk_lthm (fn _ => (boolSyntax.mk_eq(term,list_mk_forall([hd(tl l),hd l]@List.drop(l,2),bod)),jf)) jf 1828 (*val _ = DMSG (TH res) dbglzc(*DBG*)*) 1829 in res end 1830end 1831 1832 1833end (* lzConv *) 1834