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(* ===================================================================== *) 18 19structure Conv :> Conv = 20struct 21 22open HolKernel Parse boolTheory Drule boolSyntax Rsyntax Abbrev 23 24exception UNCHANGED 25 26fun QCONV c tm = c tm handle UNCHANGED => REFL tm 27 28val ERR = mk_HOL_ERR "Conv" 29fun w nm c t = c t handle UNCHANGED => raise UNCHANGED 30 | e as HOL_ERR _ => Portable.reraise e 31 | Fail s => raise Fail (s ^ " --> " ^ nm) 32 | e => raise Fail (nm ^ ": " ^ General.exnMessage e) 33 34(*----------------------------------------------------------------------* 35 * Conversion for rewrite rules of the form |- !x1 ... xn. t == u * 36 * Matches x1 ... xn : t' ----> |- t' == u' * 37 * Matches all types in conclusion except those mentioned in hypotheses.* 38 * * 39 * Rewritten such that the lhs of |- t' = u' is syntactically equal to * 40 * the input term, not just alpha-equivalent. [TFM 90.07.11] * 41 * * 42 * OLD CODE: * 43 * * 44 * let REWRITE_CONV = * 45 * set_fail_prefix `REWRITE_CONV` * 46 * (PART_MATCH (fst o dest_eq));; * 47 *----------------------------------------------------------------------*) 48 49 50fun REWR_CONV0 (part_matcher, fn_name) th = 51 let 52 val instth = part_matcher lhs th 53 handle e => 54 raise (wrap_exn "Conv" 55 (fn_name ^ ": bad theorem argument: " ^ 56 trace ("PP.avoid_unicode", 1) 57 term_to_string (concl th)) e) 58 in 59 fn tm => 60 let 61 val eqn = instth tm 62 val l = lhs (concl eqn) 63 in 64 if identical l tm then eqn else TRANS (ALPHA tm l) eqn 65 end 66 handle HOL_ERR _ => raise ERR fn_name "lhs of thm doesn't match term" 67 end 68 69val REWR_CONV = REWR_CONV0 (PART_MATCH, "REWR_CONV") 70val HO_REWR_CONV = REWR_CONV0 (HO_PART_MATCH, "HO_REWR_CONV") 71val REWR_CONV_A = REWR_CONV0 (PART_MATCH_A, "REWR_CONV_A") 72 73(*----------------------------------------------------------------------* 74 * RAND_CONV conv "t1 t2" applies conv to t2 * 75 * * 76 * Added TFM 88.03.31 * 77 * Revised TFM 91.03.08 * 78 * Revised RJB 91.04.17 * 79 * Revised Michael Norrish 2000.03.27 * 80 * now passes on information about nested failure * 81 *----------------------------------------------------------------------*) 82 83fun RAND_CONV conv tm = 84 let 85 val {Rator, Rand} = 86 dest_comb tm handle HOL_ERR _ => raise ERR "RAND_CONV" "not a comb" 87 val newrand = 88 conv Rand 89 handle HOL_ERR {origin_function, message, origin_structure} => 90 if Lib.mem origin_function ["RAND_CONV", "RATOR_CONV", "ABS_CONV"] 91 andalso origin_structure = "Conv" 92 then raise ERR "RAND_CONV" message 93 else raise ERR "RAND_CONV" (origin_function ^ ": " ^ message) 94 in 95 AP_TERM Rator newrand 96 handle HOL_ERR {message, ...} => 97 raise ERR "RAND_CONV" ("Application of AP_TERM failed: " ^ message) 98 end 99 100(*----------------------------------------------------------------------* 101 * RATOR_CONV conv "t1 t2" applies conv to t1 * 102 * * 103 * Added TFM 88.03.31 * 104 * Revised TFM 91.03.08 * 105 * Revised RJB 91.04.17 * 106 * Revised Michael Norrish 2000.03.27 * 107 * now passes on information about nested failure * 108 *----------------------------------------------------------------------*) 109 110fun RATOR_CONV conv tm = 111 let 112 val {Rator, Rand} = 113 dest_comb tm handle HOL_ERR _ => raise ERR "RATOR_CONV" "not a comb" 114 val newrator = 115 conv Rator 116 handle HOL_ERR {origin_function, origin_structure, message} => 117 if Lib.mem origin_function ["RAND_CONV", "RATOR_CONV", "ABS_CONV"] 118 andalso origin_structure = "Conv" 119 then raise ERR "RATOR_CONV" message 120 else raise ERR "RATOR_CONV" (origin_function ^ ": " ^ message) 121 in 122 AP_THM newrator Rand 123 handle HOL_ERR {message, ...} => 124 raise ERR "RATOR_CONV" ("Application of AP_THM failed: " ^ message) 125 end 126 127(* remember this as "left-hand conv", where RAND_CONV is "right-hand conv". *) 128fun LAND_CONV c = RATOR_CONV (RAND_CONV c) 129 130(*----------------------------------------------------------------------* 131 * ABS_CONV conv "\x. t[x]" applies conv to t[x] * 132 * * 133 * Added TFM 88.03.31 * 134 * Revised RJB 91.04.17 * 135 * Revised Michael Norrish 2000.03.27 * 136 * now passes on information about nested failure * 137 * Revised Michael Norrish 2003.03.20 * 138 * now does SUB_CONV-like tricks to handle ABS failing * 139 *----------------------------------------------------------------------*) 140 141fun ABS_CONV conv tm = 142 case dest_term tm of 143 LAMB {Bvar, Body} => 144 let 145 val newbody = conv Body 146 in 147 ABS Bvar newbody 148 handle HOL_ERR _ => 149 let 150 val v = genvar (type_of Bvar) 151 val th1 = ALPHA_CONV v tm 152 val r = rhs (concl th1) 153 val {Body = Body', ...} = dest_abs r 154 val eq_thm' = ABS v (conv Body') 155 val at = rhs (concl eq_thm') 156 val v' = variant (free_vars at) Bvar 157 val th2 = ALPHA_CONV v' at 158 in 159 TRANS (TRANS th1 eq_thm') th2 160 end 161 handle HOL_ERR {origin_function, origin_structure, message} => 162 if Lib.mem origin_function 163 ["RAND_CONV", "RATOR_CONV", "ABS_CONV"] 164 andalso origin_structure = "Conv" 165 then raise ERR "ABS_CONV" message 166 else raise ERR "ABS_CONV" 167 (origin_function ^ ": " ^ message) 168 end 169 | _ => raise ERR "ABS_CONV" "Term not an abstraction" 170 171(*----------------------------------------------------------------------* 172 * LHS_CONV conv "t1 = t2" applies conv to t1 * 173 * * 174 * Added MN 99.06.14 * 175 *----------------------------------------------------------------------*) 176 177fun LHS_CONV conv tm = 178 if not (is_eq tm) 179 then raise ERR "LHS_CONV" "not an equality" 180 else LAND_CONV conv tm 181 182(*----------------------------------------------------------------------* 183 * RHS_CONV conv "t1 = t2" applies conv to t2 * 184 * * 185 * Added MN 99.06.14 * 186 *----------------------------------------------------------------------*) 187 188fun RHS_CONV conv tm = 189 if not (is_eq tm) 190 then raise ERR "RHS_CONV" "not an equality" 191 else RAND_CONV conv tm 192 193(*----------------------------------------------------------------------* 194 * Conversion that always fails; identity element for ORELSEC. * 195 *----------------------------------------------------------------------*) 196 197fun NO_CONV _ = raise ERR "NO_CONV" "" 198 199(*----------------------------------------------------------------------* 200 * Conversion that always succeeds, but does nothing. * 201 * Indicates this by raising the UNCHANGED exception. * 202 *----------------------------------------------------------------------*) 203 204fun ALL_CONV t = raise UNCHANGED 205 206(*----------------------------------------------------------------------* 207 * Apply two conversions in succession; fail if either does. Handle * 208 * UNCHANGED appropriately. * 209 *----------------------------------------------------------------------*) 210 211fun (conv1 THENC conv2) t = 212 let 213 val th1 = conv1 t 214 in 215 TRANS th1 (conv2 (rhs (concl th1))) handle UNCHANGED => th1 216 end 217 handle UNCHANGED => conv2 t 218 219(*----------------------------------------------------------------------* 220 * Apply conv1; if it raises a HOL_ERR then apply conv2. Note that * 221 * interrupts and other exceptions (including UNCHANGED) will sail on * 222 * through. * 223 *----------------------------------------------------------------------*) 224 225fun (conv1 ORELSEC conv2) t = conv1 t handle HOL_ERR _ => conv2 t 226 227(*----------------------------------------------------------------------* 228 * Perform the first successful conversion of those in the list. * 229 *----------------------------------------------------------------------*) 230 231fun FIRST_CONV [] tm = NO_CONV tm 232 | FIRST_CONV (c :: rst) tm = c tm handle HOL_ERR _ => FIRST_CONV rst tm 233 234(*----------------------------------------------------------------------* 235 * Perform every conversion in the list. * 236 *----------------------------------------------------------------------*) 237 238fun EVERY_CONV convl tm = 239 List.foldr (op THENC) ALL_CONV convl tm 240 handle HOL_ERR _ => raise ERR "EVERY_CONV" "" 241 242(*----------------------------------------------------------------------* 243 * Cause the conversion to fail if it does not change its input. * 244 *----------------------------------------------------------------------*) 245 246fun CHANGED_CONV conv tm = 247 let 248 val th = conv tm 249 handle UNCHANGED => 250 raise ERR "CHANGED_CONV" "Input term unchanged" 251 val {lhs, rhs} = dest_eq (concl th) 252 in 253 if aconv lhs rhs 254 then raise ERR "CHANGED_CONV" "Input term unchanged" 255 else th 256 end 257 258(* val CHANGED_CONV = fn c => w "Conv.CHANGED_CONV" (CHANGED_CONV c) *) 259 260(*----------------------------------------------------------------------* 261 * Cause a failure if the conversion causes the UNCHANGED exception to * 262 * be raised. Doesn't "waste time" doing an equality check. * 263 * Mnemonic: "quick changed_conv". * 264 *----------------------------------------------------------------------*) 265 266fun QCHANGED_CONV conv tm = 267 conv tm handle UNCHANGED => raise ERR "QCHANGED_CONV" "Input term unchanged" 268 269fun testconv (f:conv) x = 270 SOME (SOME (f x)) 271 handle UNCHANGED => SOME NONE 272 | HOL_ERR _ => NONE 273 274fun IFC (conv1:conv) conv2 conv3 tm = 275 case testconv conv1 tm of 276 SOME (SOME th) => 277 (TRANS th (conv2 (rhs (concl th))) handle UNCHANGED => th) 278 | SOME NONE => conv2 tm 279 | NONE => conv3 tm 280 281(*----------------------------------------------------------------------* 282 * Apply a conversion zero or more times. * 283 *----------------------------------------------------------------------*) 284 285fun REPEATC conv tm = 286 let 287 fun loop thm = 288 case (testconv conv o rhs o concl) thm of 289 SOME (SOME thm') => loop (TRANS thm thm') 290 | _ => thm 291 in 292 case testconv conv tm of 293 SOME (SOME thm) => loop thm 294 | _ => raise UNCHANGED 295 end 296 297fun TRY_CONV conv = conv ORELSEC ALL_CONV 298 299fun COMB2_CONV (c1,c2) tm = 300 let 301 val {Rator, Rand} = dest_comb tm 302 in 303 let 304 val th = c1 Rator 305 in 306 MK_COMB (th, c2 Rand) handle UNCHANGED => AP_THM th Rand 307 end 308 handle UNCHANGED => AP_TERM Rator (c2 Rand) 309 end 310 311fun COMB_CONV c = COMB2_CONV(c,c) 312 313fun SUB_CONV conv = TRY_CONV (COMB_CONV conv ORELSEC ABS_CONV conv) 314 315fun FORK_CONV (conv1, conv2) tm = 316 let 317 open Term (* get rid of overlying Rsyntax *) 318 val (fx, y) = with_exn dest_comb tm (ERR "FORK_CONV" "term not a comb") 319 val (f, x) = with_exn dest_comb fx (ERR "FORK_CONV" "term not f x y") 320 in 321 let 322 val th = AP_TERM f (conv1 x) 323 in 324 MK_COMB (th, conv2 y) handle UNCHANGED => AP_THM th y 325 end 326 handle UNCHANGED => AP_TERM fx (conv2 y) 327 end 328 329fun BINOP_CONV conv = FORK_CONV (conv, conv) 330 331val OR_CLAUSES' = map GEN_ALL (CONJUNCTS (SPEC_ALL boolTheory.OR_CLAUSES)) 332val T_or = List.nth (OR_CLAUSES', 0) 333val or_T = List.nth (OR_CLAUSES', 1) 334val F_or = List.nth (OR_CLAUSES', 2) 335val or_F = List.nth (OR_CLAUSES', 3) 336 337fun EVERY_DISJ_CONV c tm = 338 (if is_disj tm 339 then LAND_CONV (EVERY_DISJ_CONV c) THENC 340 (REWR_CONV T_or ORELSEC 341 (REWR_CONV F_or THENC EVERY_DISJ_CONV c) ORELSEC 342 (RAND_CONV (EVERY_DISJ_CONV c) THENC 343 TRY_CONV (REWR_CONV or_T ORELSEC REWR_CONV or_F))) 344 else c) tm 345 346val AND_CLAUSES' = map GEN_ALL (CONJUNCTS (SPEC_ALL AND_CLAUSES)) 347val T_and = List.nth (AND_CLAUSES', 0) 348val and_T = List.nth (AND_CLAUSES', 1) 349val F_and = List.nth (AND_CLAUSES', 2) 350val and_F = List.nth (AND_CLAUSES', 3) 351 352fun EVERY_CONJ_CONV c tm = 353 (if is_conj tm 354 then LAND_CONV (EVERY_CONJ_CONV c) THENC 355 (REWR_CONV F_and ORELSEC 356 (REWR_CONV T_and THENC EVERY_CONJ_CONV c) ORELSEC 357 (RAND_CONV (EVERY_CONJ_CONV c) THENC 358 TRY_CONV (REWR_CONV and_F ORELSEC REWR_CONV and_T))) 359 else c) tm 360 361fun QUANT_CONV conv = RAND_CONV (ABS_CONV conv) 362fun BINDER_CONV conv = ABS_CONV conv ORELSEC QUANT_CONV conv 363 364fun STRIP_BINDER_CONV opt conv tm = 365 let 366 val (vlist, M) = strip_binder opt tm 367 in 368 GEN_ABS opt vlist (conv M) 369 handle HOL_ERR _ => 370 let 371 val gvs = map (genvar o type_of) vlist 372 fun rename vs = 373 case vs of 374 [] => ALL_CONV 375 | (v :: vs) => GEN_ALPHA_CONV v THENC BINDER_CONV (rename vs) 376 fun variant_list acc avds [] = List.rev acc 377 | variant_list acc avds (v :: vs) = 378 let 379 val v' = variant avds v 380 in 381 variant_list (v' :: acc) (v' :: avds) vs 382 end 383 val th1 = rename gvs tm 384 val {rhs, ...} = Rsyntax.dest_eq (Thm.concl th1) 385 val (_, M') = strip_binder opt rhs (* v = Bvar *) 386 val eq_thm' = GEN_ABS opt gvs (conv M') 387 val at = #rhs (Rsyntax.dest_eq (concl eq_thm')) 388 val vs' = variant_list [] (free_vars at) vlist 389 val th2 = rename vs' at 390 in 391 TRANS (TRANS th1 eq_thm') th2 392 end 393 end 394 395fun STRIP_QUANT_CONV conv tm = 396 (if is_forall tm 397 then STRIP_BINDER_CONV (SOME boolSyntax.universal) 398 else if is_exists tm 399 then STRIP_BINDER_CONV (SOME boolSyntax.existential) 400 else if is_select tm 401 then STRIP_BINDER_CONV (SOME boolSyntax.select) 402 else if is_exists1 tm 403 then STRIP_BINDER_CONV (SOME boolSyntax.exists1) 404 else K conv) conv tm 405 406fun LAST_EXISTS_CONV c tm = 407 let 408 val (bv, body) = Psyntax.dest_exists tm 409 in 410 if is_exists body 411 then BINDER_CONV (LAST_EXISTS_CONV c) tm 412 else c tm 413 end 414 415fun LAST_FORALL_CONV c tm = 416 if is_forall (#2 (Psyntax.dest_forall tm)) 417 then BINDER_CONV (LAST_FORALL_CONV c) tm 418 else c tm 419 420(* ---------------------------------------------------------------------- 421 traversal conversionals. 422 423 DEPTH_CONV c 424 bottom-up, recurse over sub-terms, and then repeatedly apply c at 425 top-level. 426 427 REDEPTH_CONV c 428 bottom-up. recurse over sub-terms, apply c at top, and if this 429 succeeds, repeat from start. 430 431 TOP_DEPTH_CONV c 432 top-down. Repeatedly apply c at top-level, then descend. If descending 433 doesn't change anything then stop. If there was a change then 434 come back to top and try c once more at top-level. If this succeeds 435 repeat. 436 437 TOP_SWEEP_CONV c 438 top-down. Like TOP_DEPTH_CONV but only makes one pass over the term, 439 never coming back to the top level once descent starts. 440 441 ONCE_DEPTH_CONV c 442 top-down (confusingly). Descends term looking for position at 443 which c works. Does this "in parallel", so c may be applied multiple 444 times at highest possible positions in distinct sub-terms. 445 446 ---------------------------------------------------------------------- *) 447 448fun DEPTH_CONV conv tm = (SUB_CONV (DEPTH_CONV conv) THENC REPEATC conv) tm 449 450fun REDEPTH_CONV conv tm = 451 (SUB_CONV (REDEPTH_CONV conv) THENC 452 TRY_CONV (conv THENC REDEPTH_CONV conv)) tm 453 454fun TOP_DEPTH_CONV conv tm = 455 (REPEATC conv THENC 456 TRY_CONV (CHANGED_CONV (SUB_CONV (TOP_DEPTH_CONV conv)) THENC 457 TRY_CONV (conv THENC TOP_DEPTH_CONV conv))) tm 458 459fun ONCE_DEPTH_CONV conv tm = 460 TRY_CONV (conv ORELSEC SUB_CONV (ONCE_DEPTH_CONV conv)) tm 461 462fun TOP_SWEEP_CONV conv tm = 463 (REPEATC conv THENC SUB_CONV (TOP_SWEEP_CONV conv)) tm 464 465(*------------------------------------------------------------------------* 466 * Convert a conversion to a rule * 467 *------------------------------------------------------------------------*) 468 469fun CONV_RULE conv th = EQ_MP (conv (concl th)) th handle UNCHANGED => th 470 471(*------------------------------------------------------------------------* 472 * Apply a conversion to the hypotheses of a theorem * 473 * hypsel selects hypotheses to be dealt with; * 474 * error if a conversion fails (as distinct from raising UNCHANGED) * 475 *------------------------------------------------------------------------*) 476 477fun HYP_CONV_RULE hypsel conv th = 478 let fun get_eq_thm h = 479 if hypsel h then SOME (conv h) handle UNCHANGED => NONE 480 else NONE ; 481 val hyp_eq_thms = List.mapPartial get_eq_thm (hyp th) ; 482 val hyp_imp_thms = map (UNDISCH o #2 o EQ_IMP_RULE) hyp_eq_thms ; 483 val new_th = Lib.itlist PROVE_HYP hyp_imp_thms th ; 484 in new_th end ; 485 486(*------------------------------------------------------------------------* 487 * Rule for beta-reducing on all beta-redexes * 488 *------------------------------------------------------------------------*) 489 490val BETA_RULE = CONV_RULE (DEPTH_CONV BETA_CONV) 491 492fun UNBETA_CONV arg_t t = 493 let 494 open Term (* counteract prevailing Rsyntax *) 495 in 496 if is_var arg_t 497 then SYM (BETA_CONV (mk_comb (mk_abs (arg_t, t), arg_t))) 498 else let 499 (* find all instances of arg_t in t, and convert t 500 to (\v. t[v/arg_t]) arg_t 501 v can be a genvar because we expect to get rid of it later. *) 502 val gv = genvar (type_of arg_t) 503 val newbody = Term.subst [arg_t |-> gv] t 504 in 505 SYM (BETA_CONV (Term.mk_comb (mk_abs (gv, newbody), arg_t))) 506 end 507 end 508 509(* =====================================================================* 510 * What follows is a complete set of conversions for moving ! and ? into* 511 * and out of the basic logical connectives ~, /\, \/, ==>, and =. * 512 * * 513 * Naming scheme: * 514 * * 515 * 1: for moving quantifiers inwards: <quant>_<conn>_CONV * 516 * * 517 * 2: for moving quantifiers outwards: [dir]_<conn>_<quant>_CONV * 518 * * 519 * where * 520 * * 521 * <quant> := FORALL | EXISTS * 522 * <conn> := NOT | AND | OR | IMP | EQ * 523 * [dir] := LEFT | RIGHT (optional) * 524 * * 525 * * 526 * [TFM 90.11.09] * 527 * =====================================================================*) 528 529(*----------------------------------------------------------------------* 530 * NOT_FORALL_CONV, implements the following axiom scheme: * 531 * * 532 * |- (~!x.tm) = (?x.~tm) * 533 * * 534 *----------------------------------------------------------------------*) 535 536fun NOT_FORALL_CONV tm = 537 let 538 val all = dest_neg tm 539 val {Bvar, Body} = dest_forall all 540 val exists = mk_exists {Bvar = Bvar, Body = mk_neg Body} 541 val nott = ASSUME (mk_neg Body) 542 val not_all = mk_neg all 543 val th1 = DISCH all (MP nott (SPEC Bvar (ASSUME all))) 544 val imp1 = DISCH exists (CHOOSE (Bvar, ASSUME exists) (NOT_INTRO th1)) 545 val th2 = CCONTR Body (MP (ASSUME (mk_neg exists)) 546 (EXISTS (exists, Bvar) nott)) 547 val th3 = CCONTR exists (MP (ASSUME not_all) (GEN Bvar th2)) 548 in 549 IMP_ANTISYM_RULE (DISCH not_all th3) imp1 550 end 551 handle HOL_ERR _ => raise ERR "NOT_FORALL_CONV" "" 552 553(*----------------------------------------------------------------------* 554 * NOT_EXISTS_CONV, implements the following axiom scheme. * 555 * * 556 * |- (~?x.tm) = (!x.~tm) * 557 * * 558 *----------------------------------------------------------------------*) 559 560fun NOT_EXISTS_CONV tm = 561 let 562 val {Bvar, Body} = dest_exists (dest_neg tm) 563 val all = mk_forall {Bvar = Bvar, Body = mk_neg Body} 564 val rand_tm = rand tm 565 val asm1 = ASSUME Body 566 val thm1 = MP (ASSUME tm) (EXISTS (rand_tm, Bvar) asm1) 567 val imp1 = DISCH tm (GEN Bvar (NOT_INTRO (DISCH Body thm1))) 568 val asm2 = ASSUME all 569 and asm3 = ASSUME rand_tm 570 val thm2 = DISCH rand_tm (CHOOSE (Bvar, asm3) (MP (SPEC Bvar asm2) asm1)) 571 val imp2 = DISCH all (NOT_INTRO thm2) 572 in 573 IMP_ANTISYM_RULE imp1 imp2 574 end 575 handle HOL_ERR _ => raise ERR "NOT_EXISTS_CONV" "" 576 577(*----------------------------------------------------------------------* 578 * EXISTS_NOT_CONV, implements the following axiom scheme. * 579 * * 580 * |- (?x.~tm) = (~!x.tm) * 581 * * 582 *----------------------------------------------------------------------*) 583 584fun EXISTS_NOT_CONV tm = 585 let 586 val {Bvar, Body} = dest_exists tm 587 in 588 SYM (NOT_FORALL_CONV 589 (mk_neg (mk_forall {Bvar = Bvar, Body = dest_neg Body}))) 590 end 591 handle HOL_ERR _ => raise ERR "EXISTS_NOT_CONV" "" 592 593(*----------------------------------------------------------------------* 594 * FORALL_NOT_CONV, implements the following axiom scheme. * 595 * * 596 * |- (!x.~tm) = (~?x.tm) * 597 * * 598 *----------------------------------------------------------------------*) 599 600fun FORALL_NOT_CONV tm = 601 let 602 val {Bvar, Body} = dest_forall tm 603 in 604 SYM (NOT_EXISTS_CONV 605 (mk_neg (mk_exists {Bvar = Bvar, Body = dest_neg Body}))) 606 end 607 handle HOL_ERR _ => raise ERR "FORALL_NOT_CONV" "" 608 609(*----------------------------------------------------------------------* 610 * FORALL_AND_CONV : move universal quantifiers into conjunction. * 611 * * 612 * A call to FORALL_AND_CONV "!x. P /\ Q" returns: * 613 * * 614 * |- (!x. P /\ Q) = (!x.P) /\ (!x.Q) * 615 *----------------------------------------------------------------------*) 616 617fun FORALL_AND_CONV tm = 618 let 619 val {Bvar, Body} = dest_forall tm 620 val {...} = dest_conj Body 621 val (Pth, Qth) = CONJ_PAIR (SPEC Bvar (ASSUME tm)) 622 val imp1 = DISCH tm (CONJ (GEN Bvar Pth) (GEN Bvar Qth)) 623 val xtm = rand (concl imp1) 624 val spec_bv = SPEC Bvar 625 val (t1, t2) = (spec_bv ## spec_bv) (CONJ_PAIR (ASSUME xtm)) 626 in 627 IMP_ANTISYM_RULE imp1 (DISCH xtm (GEN Bvar (CONJ t1 t2))) 628 end 629 handle HOL_ERR _ => raise ERR "FORALL_AND_CONV" "" 630 631(*----------------------------------------------------------------------* 632 * EXISTS_OR_CONV : move existential quantifiers into disjunction. * 633 * * 634 * A call to EXISTS_OR_CONV "?x. P \/ Q" returns: * 635 * * 636 * |- (?x. P \/ Q) = (?x.P) \/ (?x.Q) * 637 *----------------------------------------------------------------------*) 638 639(* 640** fun EXISTS_OR_CONV tm = 641** let val {Bvar, Body} = dest_exists tm 642** val {disj1, disj2} = dest_disj Body 643** val ep = mk_exists {Bvar = Bvar, Body = disj1} 644** and eq = mk_exists {Bvar = Bvar, Body = disj2} 645** val ep_or_eq = mk_disj {disj1 = ep, disj2 = eq} 646** val aP = ASSUME disj1 647** val aQ = ASSUME disj2 648** val Pth = EXISTS (ep, Bvar) aP 649** and Qth = EXISTS (eq, Bvar) aQ 650** val thm1 = DISJ_CASES_UNION (ASSUME Body) Pth Qth 651** val imp1 = DISCH tm (CHOOSE (Bvar, ASSUME tm) thm1) 652** val t1 = DISJ1 aP disj2 653** and t2 = DISJ2 disj1 aQ 654** val th1 = EXISTS (tm, Bvar) t1 655** and th2 = EXISTS (tm, Bvar) t2 656** val e1 = CHOOSE (Bvar, ASSUME ep) th1 657** and e2 = CHOOSE (Bvar, ASSUME eq) th2 658** in 659** IMP_ANTISYM_RULE imp1 660** (DISCH ep_or_eq (DISJ_CASES (ASSUME ep_or_eq) e1 e2)) 661** end 662** handle HOL_ERR _ => raise ERR "EXISTS_OR_CONV" "" 663*) 664 665local 666 val alpha = Type.alpha 667 val spotBeta = FORK_CONV (QUANT_CONV (BINOP_CONV BETA_CONV), 668 BINOP_CONV (QUANT_CONV BETA_CONV)) 669 open boolTheory 670 val [P0, Q0] = fst (strip_forall (concl EXISTS_OR_THM)) 671 val thm0 = SPEC Q0 (SPEC P0 EXISTS_OR_THM) 672 val Pname = #Name (dest_var P0) 673 val Qname = #Name (dest_var Q0) 674in 675 fun EXISTS_OR_CONV tm = 676 let 677 val {Bvar, Body} = dest_exists tm 678 val thm = CONV_RULE (RAND_CONV (BINOP_CONV (GEN_ALPHA_CONV Bvar))) 679 (INST_TYPE [alpha |-> type_of Bvar] thm0) 680 val ty = type_of Bvar --> Type.bool 681 val P = mk_var {Name = Pname, Ty = ty} 682 val Q = mk_var {Name = Qname, Ty = ty} 683 val {disj1, disj2} = dest_disj Body 684 val lamP = mk_abs {Bvar = Bvar, Body = disj1} 685 val lamQ = mk_abs {Bvar = Bvar, Body = disj2} 686 in 687 CONV_RULE spotBeta (INST [P |-> lamP, Q |-> lamQ] thm) 688 end 689 handle HOL_ERR _ => raise ERR "EXISTS_OR_CONV" "" 690end 691 692(*----------------------------------------------------------------------* 693 * AND_FORALL_CONV : move universal quantifiers out of conjunction. * 694 * * 695 * A call to AND_FORALL_CONV "(!x. P) /\ (!x. Q)" returns: * 696 * * 697 * |- (!x.P) /\ (!x.Q) = (!x. P /\ Q) * 698 *----------------------------------------------------------------------*) 699 700fun AND_FORALL_CONV tm = 701 let 702 val {conj1, conj2} = dest_conj tm 703 val {Bvar = x, Body = P} = dest_forall conj1 704 val {Bvar = y, Body = Q} = dest_forall conj2 705 in 706 if not (aconv x y) 707 then raise ERR "AND_FORALL_CONV" "forall'ed variables not the same" 708 else let 709 val specx = SPEC x 710 val (t1, t2) = (specx ## specx) (CONJ_PAIR (ASSUME tm)) 711 val imp1 = DISCH tm (GEN x (CONJ t1 t2)) 712 val rtm = rand (concl imp1) 713 val (Pth, Qth) = CONJ_PAIR (SPEC x (ASSUME rtm)) 714 in 715 IMP_ANTISYM_RULE imp1 (DISCH rtm (CONJ (GEN x Pth) (GEN x Qth))) 716 end 717 end 718 handle HOL_ERR _ => raise ERR "AND_FORALL_CONV" "" 719 720(*----------------------------------------------------------------------* 721 * LEFT_AND_FORALL_CONV : move universal quantifier out of conjunction. * 722 * * 723 * A call to LEFT_AND_FORALL_CONV "(!x.P) /\ Q" returns: * 724 * * 725 * |- (!x.P) /\ Q = (!x'. P[x'/x] /\ Q) * 726 * * 727 * Where x' is a primed variant of x not free in the input term * 728 *----------------------------------------------------------------------*) 729 730fun LEFT_AND_FORALL_CONV tm = 731 let 732 val {conj1, ...} = dest_conj tm 733 val {Bvar, ...} = dest_forall conj1 734 val x' = variant (free_vars tm) Bvar 735 val specx' = SPEC x' 736 and genx' = GEN x' 737 val (t1, t2) = (specx' ## I) (CONJ_PAIR (ASSUME tm)) 738 val imp1 = DISCH tm (genx' (CONJ t1 t2)) 739 val rtm = rand (concl imp1) 740 val (Pth, Qth) = CONJ_PAIR (specx' (ASSUME rtm)) 741 in 742 IMP_ANTISYM_RULE imp1 (DISCH rtm (CONJ (genx' Pth) Qth)) 743 end 744 handle HOL_ERR _ => raise ERR "LEFT_AND_FORALL_CONV" "" 745 746(*----------------------------------------------------------------------* 747 * RIGHT_AND_FORALL_CONV : move universal quantifier out of conjunction.* 748 * * 749 * A call to RIGHT_AND_FORALL_CONV "P /\ (!x.Q)" returns: * 750 * * 751 * |- P /\ (!x.Q) = (!x'. P /\ Q[x'/x]) * 752 * * 753 * where x' is a primed variant of x not free in the input term * 754 *----------------------------------------------------------------------*) 755 756fun RIGHT_AND_FORALL_CONV tm = 757 let 758 val {conj2, ...} = dest_conj tm 759 val {Bvar, ...} = dest_forall conj2 760 val x' = variant (free_vars tm) Bvar 761 val specx' = SPEC x' 762 val genx' = GEN x' 763 val (t1, t2) = (I ## specx') (CONJ_PAIR (ASSUME tm)) 764 val imp1 = DISCH tm (genx' (CONJ t1 t2)) 765 val rtm = rand (concl imp1) 766 val (Pth, Qth) = CONJ_PAIR (specx' (ASSUME rtm)) 767 in 768 IMP_ANTISYM_RULE imp1 (DISCH rtm (CONJ Pth (genx' Qth))) 769 end 770 handle HOL_ERR _ => raise ERR "RIGHT_AND_FORALL_CONV" "" 771 772(*----------------------------------------------------------------------* 773 * OR_EXISTS_CONV : move existential quantifiers out of disjunction. * 774 * * 775 * A call to OR_EXISTS_CONV "(?x. P) \/ (?x. Q)" returns: * 776 * * 777 * |- (?x.P) \/ (?x.Q) = (?x. P \/ Q) * 778 *----------------------------------------------------------------------*) 779 780fun OR_EXISTS_CONV tm = 781 let 782 val {disj1, disj2} = dest_disj tm 783 val {Bvar = x, Body = P} = dest_exists disj1 784 val {Bvar = y, Body = Q} = dest_exists disj2 785 in 786 if not (aconv x y) then 787 raise ERR "OR_EXISTS_CONV" "Variables not the same" 788 else let 789 val aP = ASSUME P 790 and aQ = ASSUME Q 791 and P_or_Q = mk_disj {disj1 = P, disj2 = Q} 792 val otm = mk_exists {Bvar = x, Body = P_or_Q} 793 val t1 = DISJ1 aP Q 794 and t2 = DISJ2 P aQ 795 val eotm = EXISTS (otm, x) 796 val e1 = CHOOSE (x, ASSUME disj1) (eotm t1) 797 and e2 = CHOOSE (x, ASSUME disj2) (eotm t2) 798 val thm1 = DISJ_CASES (ASSUME tm) e1 e2 799 val imp1 = DISCH tm thm1 800 val Pth = EXISTS (disj1, x) aP 801 and Qth = EXISTS (disj2, x) aQ 802 val thm2 = DISJ_CASES_UNION (ASSUME P_or_Q) Pth Qth 803 in 804 IMP_ANTISYM_RULE imp1 (DISCH otm (CHOOSE (x, ASSUME otm) thm2)) 805 end 806 end 807 handle HOL_ERR _ => raise ERR "OR_EXISTS_CONV" "" 808 809(*----------------------------------------------------------------------* 810 * LEFT_OR_EXISTS_CONV : move existential quantifier out of disjunction.* 811 * * 812 * A call to LEFT_OR_EXISTS_CONV "(?x.P) \/ Q" returns: * 813 * * 814 * |- (?x.P) \/ Q = (?x'. P[x'/x] \/ Q) * 815 * * 816 * Where x' is a primed variant of x not free in the input term * 817 *----------------------------------------------------------------------*) 818 819fun LEFT_OR_EXISTS_CONV tm = 820 let 821 val {disj1, disj2} = dest_disj tm 822 val {Bvar, Body} = dest_exists disj1 823 val x' = variant (free_vars tm) Bvar 824 val newp = subst[Bvar |-> x'] Body 825 val newp_thm = ASSUME newp 826 val new_disj = mk_disj {disj1 = newp, disj2 = disj2} 827 val otm = mk_exists {Bvar = x', Body = new_disj} 828 and Qth = ASSUME disj2 829 val t1 = DISJ1 newp_thm disj2 830 and t2 = DISJ2 newp (ASSUME disj2) 831 val th1 = EXISTS (otm, x') t1 832 and th2 = EXISTS (otm, x') t2 833 val thm1 = DISJ_CASES (ASSUME tm) (CHOOSE (x', ASSUME disj1) th1) th2 834 val imp1 = DISCH tm thm1 835 val Pth = EXISTS (disj1, x') newp_thm 836 val thm2 = DISJ_CASES_UNION (ASSUME new_disj) Pth Qth 837 in 838 IMP_ANTISYM_RULE imp1 (DISCH otm (CHOOSE (x', ASSUME otm) thm2)) 839 end 840 handle HOL_ERR _ => raise ERR "LEFT_OR_EXISTS_CONV" "" 841 842(*----------------------------------------------------------------------* 843 * RIGHT_OR_EXISTS_CONV: move existential quantifier out of disjunction.* 844 * * 845 * A call to RIGHT_OR_EXISTS_CONV "P \/ (?x.Q)" returns: * 846 * * 847 * |- P \/ (?x.Q) = (?x'. P \/ Q[x'/x]) * 848 * * 849 * where x' is a primed variant of x not free in the input term * 850 *----------------------------------------------------------------------*) 851 852fun RIGHT_OR_EXISTS_CONV tm = 853 let 854 val {disj1, disj2} = dest_disj tm 855 val {Bvar, Body} = dest_exists disj2 856 val x' = variant (free_vars tm) Bvar 857 val newq = subst[Bvar |-> x'] Body 858 val newq_thm = ASSUME newq 859 and Pth = ASSUME disj1 860 val P_or_newq = mk_disj {disj1 = disj1, disj2 = newq} 861 val otm = mk_exists {Bvar = x', Body = P_or_newq} 862 val eotm' = EXISTS (otm, x') 863 val th1 = eotm' (DISJ2 disj1 newq_thm) 864 and th2 = eotm' (DISJ1 Pth newq) 865 val thm1 = DISJ_CASES (ASSUME tm) th2 (CHOOSE (x', ASSUME disj2) th1) 866 val imp1 = DISCH tm thm1 867 val Qth = EXISTS (disj2, x') newq_thm 868 val thm2 = DISJ_CASES_UNION (ASSUME P_or_newq) Pth Qth 869 in 870 IMP_ANTISYM_RULE imp1 (DISCH otm (CHOOSE (x', ASSUME otm) thm2)) 871 end 872 handle HOL_ERR _ => raise ERR "RIGHT_OR_EXISTS_CONV" "" 873 874(*----------------------------------------------------------------------* 875 * EXISTS_AND_CONV : move existential quantifier into conjunction. * 876 * * 877 * A call to EXISTS_AND_CONV "?x. P /\ Q" returns: * 878 * * 879 * |- (?x. P /\ Q) = (?x.P) /\ Q [x not free in Q] * 880 * |- (?x. P /\ Q) = P /\ (?x.Q) [x not free in P] * 881 * |- (?x. P /\ Q) = (?x.P) /\ (?x.Q) [x not free in P /\ Q] * 882 *----------------------------------------------------------------------*) 883 884local 885 fun err () = raise ERR "EXISTS_AND_CONV" "expecting `?x. P /\\ Q`" 886in 887 fun EXISTS_AND_CONV tm = 888 let 889 val {Bvar, Body} = dest_exists tm handle HOL_ERR _ => err () 890 val {conj1, conj2} = dest_conj Body handle HOL_ERR _ => err () 891 val fP = free_in Bvar conj1 892 and fQ = free_in Bvar conj2 893 in 894 if fP andalso fQ 895 then raise ERR "EXISTS_AND_CONV" 896 ("`" ^ (#Name (dest_var Bvar)) ^ 897 "` free in both conjuncts") 898 else let 899 val (t1, t2) = CONJ_PAIR (ASSUME Body) 900 val econj1 = mk_exists {Bvar = Bvar, Body = conj1} 901 val econj2 = mk_exists {Bvar = Bvar, Body = conj2} 902 val eP = if fQ then t1 else EXISTS (econj1, Bvar) t1 903 and eQ = if fP then t2 else EXISTS (econj2, Bvar) t2 904 val imp1 = DISCH tm (CHOOSE (Bvar, ASSUME tm) (CONJ eP eQ)) 905 val th = EXISTS (tm, Bvar) (CONJ (ASSUME conj1) (ASSUME conj2)) 906 val th1 = if fP orelse not fQ 907 then CHOOSE (Bvar, ASSUME econj1) th 908 else th 909 val thm1 = if fQ orelse not fP 910 then CHOOSE (Bvar, ASSUME econj2) th1 911 else th1 912 val otm = rand (concl imp1) 913 val (t1, t2) = CONJ_PAIR (ASSUME otm) 914 val thm2 = PROVE_HYP t1 (PROVE_HYP t2 thm1) 915 in 916 IMP_ANTISYM_RULE imp1 (DISCH otm thm2) 917 end 918 end 919 handle e as HOL_ERR {origin_structure = "Conv", 920 origin_function = "EXISTS_AND_CONV", ...} => raise e 921 | HOL_ERR _ => raise ERR "EXISTS_AND_CONV" "" 922end 923 924(*----------------------------------------------------------------------* 925 * AND_EXISTS_CONV : move existential quantifier out of conjunction. * 926 * * 927 * |- (?x.P) /\ (?x.Q) = (?x. P /\ Q) * 928 * * 929 * provided x is free in neither P nor Q. * 930 *----------------------------------------------------------------------*) 931 932local 933 val AE_ERR = ERR "AND_EXISTS_CONV" "expecting `(?x.P) /\\ (?x.Q)`" 934in 935 fun AND_EXISTS_CONV tm = 936 let 937 val {conj1, conj2} = dest_conj tm handle HOL_ERR _ => raise AE_ERR 938 val {Bvar = x, Body = P} = dest_exists conj1 939 handle HOL_ERR _ => raise AE_ERR 940 val {Bvar = y, Body = Q} = dest_exists conj2 941 handle HOL_ERR_ => raise AE_ERR 942 in 943 if not (aconv x y) then raise AE_ERR 944 else if free_in x P orelse free_in x Q 945 then raise ERR "AND_EXISTS_CONV" 946 ("`" ^ (#Name (dest_var x)) ^ "` free in conjunct(s)") 947 else SYM (EXISTS_AND_CONV 948 (mk_exists {Bvar = x, 949 Body = mk_conj {conj1 = P, conj2 = Q}})) 950 end 951 handle e as HOL_ERR {origin_structure = "Conv", 952 origin_function = "AND_EXISTS_CONV", ...} => raise e 953 | HOL_ERR _ => raise ERR "AND_EXISTS_CONV" "" 954end 955 956(*----------------------------------------------------------------------* 957 * LEFT_AND_EXISTS_CONV: move existential quantifier out of conjunction * 958 * * 959 * A call to LEFT_AND_EXISTS_CONV "(?x.P) /\ Q" returns: * 960 * * 961 * |- (?x.P) /\ Q = (?x'. P[x'/x] /\ Q) * 962 * * 963 * Where x' is a primed variant of x not free in the input term * 964 *----------------------------------------------------------------------*) 965 966fun LEFT_AND_EXISTS_CONV tm = 967 let 968 val {conj1, conj2} = dest_conj tm 969 val {Bvar, Body} = dest_exists conj1 970 val x' = variant (free_vars tm) Bvar 971 val newp = subst [Bvar |-> x'] Body 972 val new_conj = mk_conj {conj1 = newp, conj2 = conj2} 973 val otm = mk_exists {Bvar = x', Body = new_conj} 974 val (EP, Qth) = CONJ_PAIR (ASSUME tm) 975 val thm1 = EXISTS (otm, x') (CONJ (ASSUME newp) (ASSUME conj2)) 976 val imp1 = DISCH tm (MP (DISCH conj2 (CHOOSE (x', EP) thm1)) Qth) 977 val (t1, t2) = CONJ_PAIR (ASSUME new_conj) 978 val thm2 = CHOOSE (x', ASSUME otm) (CONJ (EXISTS (conj1, x') t1) t2) 979 in 980 IMP_ANTISYM_RULE imp1 (DISCH otm thm2) 981 end 982 handle HOL_ERR _ => raise ERR "LEFT_AND_EXISTS_CONV" "" 983 984(*----------------------------------------------------------------------* 985 * RIGHT_AND_EXISTS_CONV: move existential quantifier out of conjunction* 986 * * 987 * A call to RIGHT_AND_EXISTS_CONV "P /\ (?x.Q)" returns: * 988 * * 989 * |- P /\ (?x.Q) = (?x'. P /\ (Q[x'/x]) * 990 * * 991 * where x' is a primed variant of x not free in the input term * 992 *----------------------------------------------------------------------*) 993 994fun RIGHT_AND_EXISTS_CONV tm = 995 let 996 val {conj1, conj2} = dest_conj tm 997 val {Bvar, Body} = dest_exists conj2 998 val x' = variant (free_vars tm) Bvar 999 val newq = subst [Bvar |-> x'] Body 1000 val new_conj = mk_conj {conj1 = conj1, conj2 = newq} 1001 val otm = mk_exists {Bvar = x', Body = new_conj} 1002 val (Pth, EQ) = CONJ_PAIR (ASSUME tm) 1003 val thm1 = EXISTS (otm, x') (CONJ (ASSUME conj1) (ASSUME newq)) 1004 val imp1 = DISCH tm (MP (DISCH conj1 (CHOOSE (x', EQ) thm1)) Pth) 1005 val (t1, t2) = CONJ_PAIR (ASSUME new_conj) 1006 val thm2 = CHOOSE (x', ASSUME otm) (CONJ t1 (EXISTS (conj2, x') t2)) 1007 in 1008 IMP_ANTISYM_RULE imp1 (DISCH otm thm2) 1009 end 1010 handle HOL_ERR _ => raise ERR "RIGHT_AND_EXISTS_CONV" "" 1011 1012(*----------------------------------------------------------------------* 1013 * FORALL_OR_CONV : move universal quantifier into disjunction. * 1014 * * 1015 * A call to FORALL_OR_CONV "!x. P \/ Q" returns: * 1016 * * 1017 * |- (!x. P \/ Q) = (!x.P) \/ Q [if x not free in Q] * 1018 * |- (!x. P \/ Q) = P \/ (!x.Q) [if x not free in P] * 1019 * |- (!x. P \/ Q) = (!x.P) \/ (!x.Q) [if x free in neither P nor Q] * 1020 *----------------------------------------------------------------------*) 1021 1022local 1023 val FO_ERR = ERR "FORALL_OR_CONV" "expecting `!x. P \\/ Q`" 1024in 1025 fun FORALL_OR_CONV tm = 1026 let 1027 val {Bvar, Body} = dest_forall tm handle HOL_ERR _ => raise FO_ERR 1028 val {disj1, disj2} = dest_disj Body handle HOL_ERR _ => raise FO_ERR 1029 val fdisj1 = free_in Bvar disj1 1030 and fdisj2 = free_in Bvar disj2 1031 in 1032 if fdisj1 andalso fdisj2 1033 then raise ERR "FORALL_OR_CONV" 1034 ("`" ^ (#Name (dest_var Bvar)) ^ 1035 "` free in both disjuncts") 1036 else 1037 let 1038 val disj1_thm = ASSUME disj1 1039 val disj2_thm = ASSUME disj2 1040 val thm1 = SPEC Bvar (ASSUME tm) 1041 val imp1 = 1042 if fdisj1 1043 then let 1044 val thm2 = CONTR disj1 (MP (ASSUME (mk_neg disj2)) 1045 disj2_thm) 1046 val thm3 = 1047 DISJ1 1048 (GEN Bvar (DISJ_CASES thm1 disj1_thm thm2)) 1049 disj2 1050 val thm4 = 1051 DISJ2 1052 (mk_forall {Bvar = Bvar, Body = disj1}) 1053 (ASSUME disj2) 1054 in 1055 DISCH tm 1056 (DISJ_CASES 1057 (SPEC disj2 EXCLUDED_MIDDLE) thm4 thm3) 1058 end 1059 else if fdisj2 1060 then let 1061 val thm2 = CONTR disj2 (MP (ASSUME (mk_neg disj1)) 1062 (ASSUME disj1)) 1063 val thm3 = 1064 DISJ2 disj1 1065 (GEN Bvar (DISJ_CASES thm1 thm2 disj2_thm)) 1066 val thm4 = 1067 DISJ1 (ASSUME disj1) 1068 (mk_forall {Bvar = Bvar, Body = disj2}) 1069 in 1070 DISCH tm 1071 (DISJ_CASES 1072 (SPEC disj1 EXCLUDED_MIDDLE) thm4 thm3) 1073 end 1074 else let 1075 val t1 = GEN Bvar (ASSUME disj1) 1076 val t2 = GEN Bvar (ASSUME disj2) 1077 in 1078 DISCH tm (DISJ_CASES_UNION thm1 t1 t2) 1079 end 1080 val otm = rand (concl imp1) 1081 val {disj1, disj2} = dest_disj otm 1082 val thm5 = (if fdisj1 orelse not fdisj2 then SPEC Bvar else I) 1083 (ASSUME disj1) 1084 val thm6 = (if fdisj2 orelse not fdisj1 then SPEC Bvar else I) 1085 (ASSUME disj2) 1086 val imp2 = GEN Bvar (DISJ_CASES_UNION (ASSUME otm) thm5 thm6) 1087 in 1088 IMP_ANTISYM_RULE imp1 (DISCH otm imp2) 1089 end 1090 end 1091 handle e as HOL_ERR {origin_structure = "Conv", 1092 origin_function = "FORALL_OR_CONV", ...} => raise e 1093 | HOL_ERR _ => raise ERR "FORALL_OR_CONV" "" 1094end 1095 1096(*----------------------------------------------------------------------* 1097 * OR_FORALL_CONV : move existential quantifier out of conjunction. * 1098 * * 1099 * |- (!x.P) \/ (!x.Q) = (!x. P \/ Q) * 1100 * * 1101 * provided x is free in neither P nor Q. * 1102 *----------------------------------------------------------------------*) 1103 1104local 1105 val OF_ERR = ERR "OR_FORALL_CONV" "expecting `(!x.P) \\/ (!x.Q)`" 1106in 1107 fun OR_FORALL_CONV tm = 1108 let 1109 val {disj1, disj2} = dest_disj tm handle HOL_ERR _ => raise OF_ERR 1110 val {Bvar = x, Body = P} = dest_forall disj1 1111 handle HOL_ERR _ => raise OF_ERR 1112 val {Bvar = y, Body = Q} = dest_forall disj2 1113 handle HOL_ERR _ => raise OF_ERR 1114 in 1115 if not (aconv x y) then raise OF_ERR 1116 else if free_in x P orelse free_in x Q 1117 then raise ERR "OR_FORALL_CONV" 1118 ("`" ^ (#Name (dest_var x)) ^ "` free in disjuncts(s)") 1119 else SYM (FORALL_OR_CONV 1120 (mk_forall {Bvar = x, Body = mk_disj {disj1 = P, disj2 = Q}})) 1121 end 1122 handle e as HOL_ERR {origin_structure = "Conv", 1123 origin_function = "OR_FORALL_CONV", ...} => raise e 1124 | HOL_ERR _ => raise ERR "OR_FORALL_CONV" "" 1125end 1126 1127(*----------------------------------------------------------------------* 1128 * LEFT_OR_FORALL_CONV : move universal quantifier out of conjunction. * 1129 * * 1130 * A call to LEFT_OR_FORALL_CONV "(!x.P) \/ Q" returns: * 1131 * * 1132 * |- (!x.P) \/ Q = (!x'. P[x'/x] \/ Q) * 1133 * * 1134 * Where x' is a primed variant of x not free in the input term * 1135 *----------------------------------------------------------------------*) 1136 1137fun LEFT_OR_FORALL_CONV tm = 1138 let 1139 val {disj1, disj2} = dest_disj tm 1140 val {Bvar, Body} = dest_forall disj1 1141 val x' = variant (free_vars tm) Bvar 1142 val newp = subst [Bvar |-> x'] Body 1143 val aQ = ASSUME disj2 1144 val Pth = DISJ1 (SPEC x' (ASSUME disj1)) disj2 1145 val Qth = DISJ2 newp aQ 1146 val imp1 = DISCH tm (GEN x' (DISJ_CASES (ASSUME tm) Pth Qth)) 1147 val otm = rand (concl imp1) 1148 val thm1 = SPEC x' (ASSUME otm) 1149 val thm2 = CONTR newp (MP (ASSUME (mk_neg disj2)) aQ) 1150 val thm3 = DISJ1 (GEN x' (DISJ_CASES thm1 (ASSUME newp) thm2)) disj2 1151 val thm4 = DISJ2 disj1 aQ 1152 val imp2 = DISCH otm (DISJ_CASES (SPEC disj2 EXCLUDED_MIDDLE) thm4 thm3) 1153 in 1154 IMP_ANTISYM_RULE imp1 imp2 1155 end 1156 handle HOL_ERR _ => raise ERR "LEFT_OR_FORALL_CONV" "" 1157 1158(*----------------------------------------------------------------------* 1159 * RIGHT_OR_FORALL_CONV : move universal quantifier out of conjunction. * 1160 * * 1161 * A call to RIGHT_OR_FORALL_CONV "P \/ (!x.Q)" returns: * 1162 * * 1163 * |- P \/ (!x.Q) = (!x'. P \/ (Q[x'/x]) * 1164 * * 1165 * where x' is a primed variant of x not free in the input term * 1166 *----------------------------------------------------------------------*) 1167 1168fun RIGHT_OR_FORALL_CONV tm = 1169 let 1170 val {disj1, disj2} = dest_disj tm 1171 val {Bvar, Body} = dest_forall disj2 1172 val x' = variant (free_vars tm) Bvar 1173 val newq = subst [Bvar |-> x'] Body 1174 val Qth = DISJ2 disj1 (SPEC x' (ASSUME disj2)) 1175 val Pthm = ASSUME disj1 1176 val Pth = DISJ1 Pthm newq 1177 val imp1 = DISCH tm (GEN x' (DISJ_CASES (ASSUME tm) Pth Qth)) 1178 val otm = rand (concl imp1) 1179 val thm1 = SPEC x' (ASSUME otm) 1180 val thm2 = CONTR newq (MP (ASSUME (mk_neg disj1)) Pthm) 1181 val thm3 = DISJ2 disj1 (GEN x' (DISJ_CASES thm1 thm2 (ASSUME newq))) 1182 val thm4 = DISJ1 Pthm disj2 1183 val imp2 = DISCH otm (DISJ_CASES (SPEC disj1 EXCLUDED_MIDDLE) thm4 thm3) 1184 in 1185 IMP_ANTISYM_RULE imp1 imp2 1186 end 1187 handle HOL_ERR _ => raise ERR "RIGHT_OR_FORALL_CONV" "" 1188 1189(*----------------------------------------------------------------------* 1190 * FORALL_IMP_CONV, implements the following axiom schemes. * 1191 * * 1192 * |- (!x. P==>Q[x]) = (P ==> (!x.Q[x])) [x not free in P] * 1193 * * 1194 * |- (!x. P[x]==>Q) = ((?x.P[x]) ==> Q) [x not free in Q] * 1195 * * 1196 * |- (!x. P==>Q) = ((?x.P) ==> (!x.Q)) [x not free in P==>Q] * 1197 *----------------------------------------------------------------------*) 1198 1199local 1200 val FI_ERR = ERR "FORALL_IMP_CONV" "expecting `!x. P ==> Q`" 1201in 1202 fun FORALL_IMP_CONV tm = 1203 let 1204 val {Bvar, Body} = dest_forall tm handle HOL_ERR _ => raise FI_ERR 1205 val {ant, conseq} = dest_imp Body handle HOL_ERR _ => raise FI_ERR 1206 val fant = free_in Bvar ant 1207 and fconseq = free_in Bvar conseq 1208 val ant_thm = ASSUME ant 1209 val tm_thm = ASSUME tm 1210 in 1211 if fant andalso fconseq 1212 then raise ERR "FORALL_IMP_CONV" 1213 ("`" ^ (#Name (dest_var Bvar)) ^ 1214 "` free on both sides of `==>`") 1215 else if fant 1216 then let 1217 val asm = mk_exists {Bvar = Bvar, Body = ant} 1218 val th1 = 1219 CHOOSE (Bvar, ASSUME asm) (UNDISCH (SPEC Bvar tm_thm)) 1220 val imp1 = DISCH tm (DISCH asm th1) 1221 val cncl = rand (concl imp1) 1222 val th2 = MP (ASSUME cncl) (EXISTS (asm, Bvar) ant_thm) 1223 val imp2 = DISCH cncl (GEN Bvar (DISCH ant th2)) 1224 in 1225 IMP_ANTISYM_RULE imp1 imp2 1226 end 1227 else if fconseq 1228 then let 1229 val imp1 = DISCH ant (GEN Bvar (UNDISCH (SPEC Bvar tm_thm))) 1230 val cncl = concl imp1 1231 val imp2 = 1232 GEN Bvar (DISCH ant (SPEC Bvar (UNDISCH (ASSUME cncl)))) 1233 in 1234 IMP_ANTISYM_RULE (DISCH tm imp1) (DISCH cncl imp2) 1235 end 1236 else let 1237 val asm = mk_exists {Bvar = Bvar, Body = ant} 1238 val tmp = UNDISCH (SPEC Bvar tm_thm) 1239 val th1 = GEN Bvar (CHOOSE (Bvar, ASSUME asm) tmp) 1240 val imp1 = DISCH tm (DISCH asm th1) 1241 val cncl = rand (concl imp1) 1242 val th2 = 1243 SPEC Bvar (MP (ASSUME cncl) (EXISTS (asm, Bvar) ant_thm)) 1244 val imp2 = DISCH cncl (GEN Bvar (DISCH ant th2)) 1245 in 1246 IMP_ANTISYM_RULE imp1 imp2 1247 end 1248 end 1249 handle e as HOL_ERR {origin_structure = "Conv", 1250 origin_function = "FORALL_IMP_CONV", ...} => raise e 1251 | HOL_ERR _ => raise ERR "FORALL_IMP_CONV" "" 1252end 1253 1254(*----------------------------------------------------------------------* 1255 * LEFT_IMP_EXISTS_CONV, implements the following theorem-scheme: * 1256 * * 1257 * |- (?x. t1[x]) ==> t2 = !x'. t1[x'] ==> t2 * 1258 * * 1259 * where x' is a variant of x chosen not to be free in (?x.t1[x])==>t2 * 1260 * * 1261 * Author: Tom Melham * 1262 * Revised: [TFM 90.07.01] * 1263 *----------------------------------------------------------------------*) 1264 1265fun LEFT_IMP_EXISTS_CONV tm = 1266 let 1267 val {ant, ...} = dest_imp tm 1268 val {Bvar, Body} = dest_exists ant 1269 val x' = variant (free_vars tm) Bvar 1270 val t' = subst [Bvar |-> x'] Body 1271 val th1 = GEN x' (DISCH t'(MP (ASSUME tm) (EXISTS (ant, x') (ASSUME t')))) 1272 val rtm = concl th1 1273 val th2 = CHOOSE (x', ASSUME ant) (UNDISCH (SPEC x'(ASSUME rtm))) 1274 in 1275 IMP_ANTISYM_RULE (DISCH tm th1) (DISCH rtm (DISCH ant th2)) 1276 end 1277 handle HOL_ERR _ => raise ERR "LEFT_IMP_EXISTS_CONV" "" 1278 1279(*----------------------------------------------------------------------* 1280 * RIGHT_IMP_FORALL_CONV, implements the following theorem-scheme: * 1281 * * 1282 * |- (t1 ==> !x. t2) = !x'. t1 ==> t2[x'/x] * 1283 * * 1284 * where x' is a variant of x chosen not to be free in the input term. * 1285 *----------------------------------------------------------------------*) 1286 1287fun RIGHT_IMP_FORALL_CONV tm = 1288 let 1289 val {ant, conseq} = dest_imp tm 1290 val {Bvar, Body} = dest_forall conseq 1291 val x' = variant (free_vars tm) Bvar 1292 val t' = subst [Bvar |-> x'] Body 1293 val imp1 = DISCH tm (GEN x' (DISCH ant (SPEC x'(UNDISCH (ASSUME tm))))) 1294 val ctm = rand (concl imp1) 1295 val alph = GEN_ALPHA_CONV Bvar (mk_forall {Bvar = x', Body = t'}) 1296 val thm1 = EQ_MP alph (GEN x'(UNDISCH (SPEC x' (ASSUME ctm)))) 1297 val imp2 = DISCH ctm (DISCH ant thm1) 1298 in 1299 IMP_ANTISYM_RULE imp1 imp2 1300 end 1301 handle HOL_ERR _ => raise ERR "RIGHT_IMP_FORALL_CONV" "" 1302 1303(*----------------------------------------------------------------------* 1304 * EXISTS_IMP_CONV, implements the following axiom schemes. * 1305 * * 1306 * |- (?x. P==>Q[x]) = (P ==> (?x.Q[x])) [x not free in P] * 1307 * * 1308 * |- (?x. P[x]==>Q) = ((!x.P[x]) ==> Q) [x not free in Q] * 1309 * * 1310 * |- (?x. P==>Q) = ((!x.P) ==> (?x.Q)) [x not free in P==>Q] * 1311 *----------------------------------------------------------------------*) 1312 1313local 1314 val EI_ERR = ERR "EXISTS_IMP_CONV" "expecting `?x. P ==> Q`" 1315in 1316 fun EXISTS_IMP_CONV tm = 1317 let 1318 val {Bvar, Body} = dest_exists tm handle HOL_ERR _ => raise EI_ERR 1319 val {ant = P, conseq = Q} = dest_imp Body handle HOL_ERR _ => raise EI_ERR 1320 val fP = free_in Bvar P 1321 and fQ = free_in Bvar Q 1322 in 1323 if fP andalso fQ 1324 then raise ERR "EXISTS_IMP_CONV" 1325 ("`" ^ (#Name (dest_var Bvar)) ^ 1326 "` free on both sides of `==>`") 1327 else if fP 1328 then let 1329 val allp = mk_forall {Bvar = Bvar, Body = P} 1330 val th1 = SPEC Bvar (ASSUME allp) 1331 val thm1 = MP (ASSUME Body) th1 1332 val imp1 = 1333 DISCH tm (CHOOSE (Bvar, ASSUME tm) (DISCH allp thm1)) 1334 val otm = rand (concl imp1) 1335 val thm2 = EXISTS (tm, Bvar) (DISCH P (UNDISCH (ASSUME otm))) 1336 val notP = mk_neg P 1337 val notP_thm = ASSUME notP 1338 val nex = mk_exists {Bvar = Bvar, Body = notP} 1339 val asm1 = EXISTS (nex, Bvar) notP_thm 1340 val th2 = CCONTR P (MP (ASSUME (mk_neg nex)) asm1) 1341 val th3 = CCONTR nex (MP (ASSUME (mk_neg allp)) (GEN Bvar th2)) 1342 val thm4 = DISCH P (CONTR Q (UNDISCH notP_thm)) 1343 val thm5 = CHOOSE (Bvar, th3) (EXISTS (tm, Bvar) thm4) 1344 val thm6 = DISJ_CASES (SPEC allp EXCLUDED_MIDDLE) thm2 thm5 1345 in 1346 IMP_ANTISYM_RULE imp1 (DISCH otm thm6) 1347 end 1348 else if fQ 1349 then let 1350 val thm1 = EXISTS (mk_exists {Bvar = Bvar, Body = Q}, Bvar) 1351 (UNDISCH (ASSUME Body)) 1352 val imp1 = DISCH tm (CHOOSE (Bvar, ASSUME tm) (DISCH P thm1)) 1353 val thm2 = UNDISCH (ASSUME (rand (concl imp1))) 1354 val thm3 = 1355 CHOOSE (Bvar, thm2) (EXISTS (tm, Bvar) (DISCH P (ASSUME Q))) 1356 val thm4 = 1357 EXISTS (tm, Bvar) 1358 (DISCH P (CONTR Q (UNDISCH (ASSUME (mk_neg P))))) 1359 val thm5 = DISJ_CASES (SPEC P EXCLUDED_MIDDLE) thm3 thm4 1360 in 1361 IMP_ANTISYM_RULE imp1 (DISCH (rand (concl imp1)) thm5) 1362 end 1363 else let 1364 val eQ = mk_exists {Bvar = Bvar, Body = Q} 1365 and aP = mk_forall {Bvar = Bvar, Body = P} 1366 val thm1 = EXISTS (eQ, Bvar) (UNDISCH (ASSUME Body)) 1367 val thm2 = DISCH aP (PROVE_HYP (SPEC Bvar (ASSUME aP)) thm1) 1368 val imp1 = DISCH tm (CHOOSE (Bvar, ASSUME tm) thm2) 1369 val thm2 = CHOOSE (Bvar, UNDISCH (ASSUME (rand (concl imp1)))) 1370 (ASSUME Q) 1371 val thm3 = DISCH P (PROVE_HYP (GEN Bvar (ASSUME P)) thm2) 1372 val imp2 = DISCH (rand (concl imp1)) (EXISTS (tm, Bvar) thm3) 1373 in 1374 IMP_ANTISYM_RULE imp1 imp2 1375 end 1376 end 1377 handle e as HOL_ERR {origin_structure = "Conv", 1378 origin_function = "EXISTS_IMP_CONV", ...} => raise e 1379 | HOL_ERR _ => raise ERR "EXISTS_IMP_CONV" "" 1380end 1381 1382(*----------------------------------------------------------------------* 1383 * LEFT_IMP_FORALL_CONV, implements the following theorem-scheme: * 1384 * * 1385 * |- (!x. t1[x]) ==> t2 = ?x'. t1[x'] ==> t2 * 1386 * * 1387 * where x' is a variant of x chosen not to be free in the input term * 1388 *----------------------------------------------------------------------*) 1389 1390fun LEFT_IMP_FORALL_CONV tm = 1391 let 1392 val {ant, conseq} = dest_imp tm 1393 val {Bvar, Body} = dest_forall ant 1394 val x' = variant (free_vars tm) Bvar 1395 val t1' = subst [Bvar |-> x'] Body 1396 val not_t1'_thm = ASSUME (mk_neg t1') 1397 val th1 = SPEC x' (ASSUME ant) 1398 val new_imp = mk_imp {ant = t1', conseq = conseq} 1399 val thm1 = MP (ASSUME new_imp) th1 1400 val otm = mk_exists {Bvar = x', Body = new_imp} 1401 val imp1 = DISCH otm (CHOOSE (x', ASSUME otm) (DISCH ant thm1)) 1402 val thm2 = EXISTS (otm, x') (DISCH t1' (UNDISCH (ASSUME tm))) 1403 val nex = mk_exists {Bvar = x', Body = mk_neg t1'} 1404 val asm1 = EXISTS (nex, x') not_t1'_thm 1405 val th2 = CCONTR t1' (MP (ASSUME (mk_neg nex)) asm1) 1406 val th3 = CCONTR nex (MP (ASSUME (mk_neg ant)) (GEN x' th2)) 1407 val thm4 = DISCH t1' (CONTR conseq (UNDISCH not_t1'_thm)) 1408 val thm5 = CHOOSE (x', th3) 1409 (EXISTS (mk_exists {Bvar = x', Body = concl thm4}, x') thm4) 1410 val thm6 = DISJ_CASES (SPEC ant EXCLUDED_MIDDLE) thm2 thm5 1411 in 1412 IMP_ANTISYM_RULE (DISCH tm thm6) imp1 1413 end 1414 handle HOL_ERR _ => raise ERR "LEFT_IMP_FORALL_CONV" "" 1415 1416(*----------------------------------------------------------------------* 1417 * RIGHT_IMP_EXISTS_CONV, implements the following theorem-scheme: * 1418 * * 1419 * |- (t1 ==> ?x. t2) = ?x'. t1 ==> t2[x'/x] * 1420 * * 1421 * where x' is a variant of x chosen not to be free in the input term. * 1422 *----------------------------------------------------------------------*) 1423 1424fun RIGHT_IMP_EXISTS_CONV tm = 1425 let 1426 val {ant, conseq} = dest_imp tm 1427 val {Bvar, Body} = dest_exists conseq 1428 val x' = variant (free_vars tm) Bvar 1429 val t2' = subst [Bvar |-> x'] Body 1430 val new_imp = mk_imp {ant = ant, conseq = t2'} 1431 val otm = mk_exists {Bvar = x', Body = new_imp} 1432 val thm1 = EXISTS (conseq, x') (UNDISCH (ASSUME new_imp)) 1433 val imp1 = DISCH otm (CHOOSE (x', ASSUME otm) (DISCH ant thm1)) 1434 val thm2 = UNDISCH (ASSUME tm) 1435 val thm3 = CHOOSE (x', thm2) (EXISTS (otm, x') (DISCH ant (ASSUME t2'))) 1436 val thm4 = DISCH ant (CONTR t2'(UNDISCH (ASSUME (mk_neg ant)))) 1437 val thm5 = EXISTS (otm, x') thm4 1438 val thm6 = DISJ_CASES (SPEC ant EXCLUDED_MIDDLE) thm3 thm5 1439 in 1440 IMP_ANTISYM_RULE (DISCH tm thm6) imp1 1441 end 1442 handle HOL_ERR _ => raise ERR "RIGHT_IMP_EXISTS_CONV" "" 1443 1444(*----------------------------------------------------------------------* 1445 * X_SKOLEM_CONV : introduce a skolem function. * 1446 * * 1447 * |- (!x1...xn. ?y. tm[x1,...,xn,y]) * 1448 * = * 1449 * (?f. !x1...xn. tm[x1,..,xn,f x1 ... xn] * 1450 * * 1451 * The first argument is the function f. * 1452 *----------------------------------------------------------------------*) 1453 1454local 1455 fun err s = raise ERR "X_SKOLEM_CONV" s 1456in 1457 fun X_SKOLEM_CONV v = 1458 if not (is_var v) 1459 then raise ERR "X_SKOLEM_CONV" "first argument not a variable" 1460 else 1461 fn tm => 1462 let 1463 val (xs, ex) = strip_forall tm 1464 val ab as {Bvar, Body} = 1465 dest_exists ex 1466 handle HOL_ERR _ => err "expecting `!x1...xn. ?y.tm`" 1467 val fx = 1468 Term.list_mk_comb (v, xs) 1469 handle HOL_ERR _ => err "function variable has wrong type" 1470 in 1471 if free_in v tm 1472 then err ("`" ^ (#Name (dest_var v)) ^ 1473 "` free in the input term") 1474 else let 1475 val pat_bod = 1476 list_mk_forall (xs, subst [Bvar |-> fx] Body) 1477 val pat = mk_exists {Bvar = v, Body = pat_bod} 1478 val fnn = list_mk_abs (xs, mk_select ab) 1479 val bth = 1480 SYM (LIST_BETA_CONV (Term.list_mk_comb (fnn, xs))) 1481 val thm1 = SUBST [Bvar |-> bth] Body 1482 (SELECT_RULE (SPECL xs (ASSUME tm))) 1483 val imp1 = DISCH tm (EXISTS (pat, fnn) (GENL xs thm1)) 1484 val thm2 = SPECL xs (ASSUME pat_bod) 1485 val thm3 = GENL xs (EXISTS (ex, fx) thm2) 1486 val imp2 = DISCH pat (CHOOSE (v, ASSUME pat) thm3) 1487 in 1488 IMP_ANTISYM_RULE imp1 imp2 1489 end 1490 end 1491 handle e as HOL_ERR 1492 {origin_structure = "Conv", 1493 origin_function = "X_SKOLEM_CONV", ...} => raise e 1494 | HOL_ERR _ => err "" 1495 (* val X_SKOLEM_CONV = w "X_SKOLEM_CONV" X_SKOLEM_CONV *) 1496end 1497 1498(*----------------------------------------------------------------------* 1499 * SKOLEM_CONV : introduce a skolem function. * 1500 * * 1501 * |- (!x1...xn. ?y. tm[x1,...,xn,y]) * 1502 * = * 1503 * (?y'. !x1...xn. tm[x1,..,xn,y' x1 ... xn] * 1504 * * 1505 * Where y' is a primed variant of y not free in the input term. * 1506 *----------------------------------------------------------------------*) 1507 1508local 1509 fun mkfty (tm, ty) = type_of tm --> ty 1510in 1511 fun SKOLEM_CONV tm = 1512 let 1513 val (xs, ex) = strip_forall tm 1514 val {Bvar, ...} = dest_exists ex 1515 val {Name, Ty} = dest_var Bvar 1516 val fv = mk_var {Name = Name, Ty = List.foldr mkfty Ty xs} 1517 in 1518 X_SKOLEM_CONV (variant (free_vars tm) fv) tm 1519 end 1520 handle HOL_ERR _ => raise ERR "SKOLEM_CONV" "" 1521 (* val SKOLEM_CONV = w "SKOLEM_CONV" SKOLEM_CONV *) 1522end 1523 1524(*----------------------------------------------------------------------* 1525 * SYM_CONV : a conversion for symmetry of equality. * 1526 * * 1527 * e.g. SYM_CONV "x=y" ----> (x=y) = (y=x). * 1528 *----------------------------------------------------------------------*) 1529 1530fun SYM_CONV tm = 1531 let 1532 val {lhs, rhs} = dest_eq tm 1533 val th = INST_TYPE [Type.alpha |-> type_of lhs] EQ_SYM_EQ 1534 in 1535 SPECL [lhs, rhs] th 1536 end 1537 handle HOL_ERR _ => raise ERR "SYM_CONV" "" 1538 1539(*-----------------------------------------------------------------------* 1540 * GSYM - General symmetry rule * 1541 * * 1542 * Reverses the first equation(s) encountered in a top-down search. * 1543 * * 1544 * [JRH 92.03.28] * 1545 *-----------------------------------------------------------------------*) 1546 1547val GSYM = CONV_RULE (ONCE_DEPTH_CONV SYM_CONV) 1548 1549(*----------------------------------------------------------------------* 1550 * A |- t1 = t2 * 1551 * -------------- (t2' got from t2 using a conversion) * 1552 * A |- t1 = t2' * 1553 *----------------------------------------------------------------------*) 1554 1555fun RIGHT_CONV_RULE conv th = 1556 TRANS th (conv (rhs (concl th))) handle UNCHANGED => th 1557 1558(*----------------------------------------------------------------------* 1559 * FUN_EQ_CONV "f = g" returns: |- (f = g) = !x. (f x = g x). * 1560 * * 1561 * Notes: f and g must be functions. The conversion choses an "x" not * 1562 * free in f or g. This conversion just states that functions are equal * 1563 * IFF the results of applying them to an arbitrary value are equal. * 1564 * * 1565 * New version: TFM 88.03.31 * 1566 *----------------------------------------------------------------------*) 1567 1568fun FUN_EQ_CONV tm = 1569 let 1570 val (ty1, _) = dom_rng (type_of (lhs tm)) 1571 val vars = free_vars tm 1572 val varnm = 1573 if Type.is_vartype ty1 1574 then "x" 1575 else Char.toString 1576 (Lib.trye hd (String.explode (fst (Type.dest_type ty1)))) 1577 val x = variant vars (mk_var {Name = varnm, Ty = ty1}) 1578 val imp1 = DISCH_ALL (GEN x (AP_THM (ASSUME tm) x)) 1579 val asm = ASSUME (concl (GEN x (AP_THM (ASSUME tm) x))) 1580 in 1581 IMP_ANTISYM_RULE imp1 (DISCH_ALL (EXT asm)) 1582 end 1583 handle HOL_ERR _ => raise ERR "FUN_EQ_CONV" "" 1584 1585(*-----------------------------------------------------------------------* 1586 * X_FUN_EQ_CONV "x" "f = g" * 1587 * * 1588 * yields |- (f = g) = !x. f x = g x * 1589 * * 1590 * fails if x free in f or g, or x not of the right type. * 1591 *-----------------------------------------------------------------------*) 1592 1593local 1594 fun err s = raise ERR "X_FUN_EQ_CONV" s 1595in 1596 fun X_FUN_EQ_CONV x tm = 1597 if not (is_var x) 1598 then err "first arg is not a variable" 1599 else if op_mem aconv x (free_vars tm) 1600 then err (#Name (dest_var x) ^ " is a free variable") 1601 else let 1602 val (ty, _) = with_exn dom_rng (type_of (lhs tm)) 1603 (ERR "X_FUN_EQ_CONV" "lhs and rhs not functions") 1604 in 1605 if ty = type_of x 1606 then let 1607 val imp1 = DISCH_ALL (GEN x (AP_THM (ASSUME tm) x)) 1608 val asm = ASSUME (concl (GEN x (AP_THM (ASSUME tm) x))) 1609 in 1610 IMP_ANTISYM_RULE imp1 (DISCH_ALL (EXT asm)) 1611 end 1612 else err (#Name (dest_var x) ^ " has the wrong type") 1613 end 1614 handle e => raise (wrap_exn "Conv" "X_FUN_EQ_CONV" e) 1615end 1616 1617(*----------------------------------------------------------------------* 1618 * SELECT_CONV: a conversion for introducing "?" when P [@x.P[x]]. * 1619 * * 1620 * SELECT_CONV "P [@x.P [x]]" ---> |- P [@x.P [x]] = ?x. P[x] * 1621 * * 1622 * Added: TFM 88.03.31 * 1623 *----------------------------------------------------------------------*) 1624 1625(* fun SELECT_CONV tm = 1626** let val epsl = find_terms is_select tm 1627** fun findfn t = (tm = subst [{redex = #Bvar (dest_select t), 1628** residue = t}] 1629** (#Body (dest_select t))) 1630** val sel = first findfn epsl 1631** val ex = mk_exists(dest_select sel) 1632** val imp1 = DISCH_ALL (SELECT_RULE (ASSUME ex)) 1633** and imp2 = DISCH_ALL (EXISTS (ex,sel) (ASSUME tm)) 1634** in 1635** IMP_ANTISYM_RULE imp2 imp1 1636** end 1637** handle _ => raise ERR{function = "SELECT_CONV", message = ""}; 1638*) 1639 1640local 1641 val f = mk_var {Name = "f", Ty = alpha --> bool} 1642 val th1 = AP_THM EXISTS_DEF f 1643 val th2 = CONV_RULE (RAND_CONV BETA_CONV) th1 1644 val tyv = Type.mk_vartype "'a" 1645 fun EXISTS_CONV {Bvar, Body} = 1646 let 1647 val ty = type_of Bvar 1648 val ins = INST_TYPE [tyv |-> ty] th2 1649 val theta = [inst [tyv |-> ty] f |-> mk_abs {Bvar = Bvar, Body = Body}] 1650 val th = INST theta ins 1651 in 1652 CONV_RULE (RAND_CONV BETA_CONV) th 1653 end 1654 fun find_first p tm = 1655 if p tm 1656 then tm 1657 else if is_abs tm 1658 then find_first p (body tm) 1659 else if is_comb tm 1660 then let 1661 val {Rator, Rand} = dest_comb tm 1662 in 1663 find_first p Rator handle HOL_ERR _ => find_first p Rand 1664 end 1665 else raise ERR "SELECT_CONV.find_first" "" 1666in 1667 fun SELECT_CONV tm = 1668 let 1669 fun right t = 1670 let 1671 val {Bvar, Body} = dest_select t 1672 in 1673 Term.aconv (subst [Bvar |-> t] Body) tm 1674 end 1675 handle HOL_ERR _ => false 1676 val epi = find_first right tm 1677 in 1678 SYM (EXISTS_CONV (dest_select epi)) 1679 end 1680 handle HOL_ERR _ => raise ERR "SELECT_CONV" "" 1681end 1682 1683(*----------------------------------------------------------------------* 1684 * SPLICE_CONJ_CONV: Normalize to right associativity a conjunction * 1685 * without recursing in the right conjunct. * 1686 * * 1687 * SPLICE_CONJ_CONV "(a1 /\ a2 /\ ...) /\ b" * 1688 * --> |- = "(a1 /\ a2 /\ ...) /\ b = a1 /\ a2 /\ ... /\ b" * 1689 * * 1690 * Fails if the term is not a conjunction. * 1691 *----------------------------------------------------------------------*) 1692local 1693 val conv = REWR_CONV (GSYM CONJ_ASSOC) 1694in 1695fun SPLICE_CONJ_CONV t = 1696 let 1697 fun recurse t = IFC conv (RAND_CONV recurse) ALL_CONV t 1698 in 1699 if is_conj t then 1700 recurse t 1701 else 1702 raise mk_HOL_ERR "Conv" "SPLICE_CONJ_CONV" "Not a conjunction" 1703 end 1704end (* local *) 1705 1706(*----------------------------------------------------------------------* 1707 * CONTRAPOS_CONV: convert an implication to its contrapositive. * 1708 * * 1709 * CONTRAPOS_CONV "a ==> b" --> |- (a ==> b) = (~b ==> ~a) * 1710 * * 1711 * Added: TFM 88.03.31 * 1712 * Revised: TFM 90.07.13 * 1713 *----------------------------------------------------------------------*) 1714 1715fun CONTRAPOS_CONV tm = 1716 let 1717 val {ant, conseq} = dest_imp tm 1718 val negc = mk_neg conseq 1719 and contra = mk_imp {ant = mk_neg conseq, conseq = mk_neg ant} 1720 val imp1 = DISCH negc (NOT_INTRO (IMP_TRANS (ASSUME tm) (ASSUME negc))) 1721 and imp2 = DISCH ant (CCONTR conseq (UNDISCH (UNDISCH (ASSUME contra)))) 1722 in 1723 IMP_ANTISYM_RULE (DISCH tm imp1) (DISCH contra imp2) 1724 end 1725 handle HOL_ERR _ => raise ERR "CONTRAPOS_CONV" "" 1726 1727(*----------------------------------------------------------------------* 1728 * ANTE_CONJ_CONV: convert an implication with conjuncts in its * 1729 * antecedant to a series of implications. * 1730 * * 1731 * ANTE_CONJ_CONV "a1 /\ a2 ==> c" * 1732 * ----> |- a1 /\ a2 ==> c = (a1 ==> (a2 ==> c)) * 1733 * * 1734 * Added: TFM 88.03.31 * 1735 *----------------------------------------------------------------------*) 1736 1737val ANTE_CONJ_CONV = 1738 REWR_CONV (CONV_RULE (ONCE_DEPTH_CONV SYM_CONV) AND_IMP_INTRO) 1739 1740(*----------------------------------------------------------------------* 1741 * AND_IMP_INTRO_CONV: convert a series of implications to an * 1742 * implication with conjuncts in its antecedent * 1743 * * 1744 * AND_IMP_INTRO_CONV "a1 ==> a2 ==> c" * 1745 * ----> |- (a1 ==> (a2 ==> c)) = (a1 /\ a2 ==> c) * 1746 * * 1747 * Added: Thomas Tuerk, 2nd August 2010 * 1748 *----------------------------------------------------------------------*) 1749 1750val AND_IMP_INTRO_CONV = REWR_CONV AND_IMP_INTRO 1751 1752(*----------------------------------------------------------------------* 1753 * SWAP_EXISTS_CONV: swap the order of existentially quantified vars. * 1754 * * 1755 * SWAP_EXISTS_CONV "?x y.t[x,y]" ---> |- ?x y.t[x,y] = ?y x.t[x,y] * 1756 * * 1757 * AUTHOR: Paul Loewenstein 3 May 1988 * 1758 *----------------------------------------------------------------------*) 1759 1760fun SWAP_EXISTS_CONV xyt = 1761 let 1762 val {Bvar = x, Body = yt} = dest_exists xyt 1763 val {Bvar = y, Body = t} = dest_exists yt 1764 val xt = mk_exists {Bvar = x, Body = t} 1765 val yxt = mk_exists {Bvar = y, Body = xt} 1766 val t_thm = ASSUME t 1767 in 1768 IMP_ANTISYM_RULE 1769 (DISCH xyt (CHOOSE (x, ASSUME xyt) (CHOOSE (y, (ASSUME yt)) 1770 (EXISTS (yxt, y) (EXISTS (xt, x) t_thm))))) 1771 (DISCH yxt (CHOOSE (y, ASSUME yxt) (CHOOSE (x, (ASSUME xt)) 1772 (EXISTS (xyt, x) (EXISTS (yt, y) t_thm))))) 1773 end 1774 handle HOL_ERR _ => raise ERR "SWAP_EXISTS_CONV" "" 1775 1776(*----------------------------------------------------------------------* 1777 * EXISTS_SIMP_CONV: gets rid of unused allquantification * 1778 * * 1779 * |- ?x. P = P * 1780 *----------------------------------------------------------------------*) 1781 1782fun EXISTS_SIMP_CONV xt = 1783 let 1784 val {Bvar = x, Body = t} = dest_exists xt 1785 in 1786 IMP_ANTISYM_RULE 1787 (DISCH xt (CHOOSE (x, ASSUME xt) (ASSUME t))) 1788 (DISCH t (EXISTS (xt, x) (ASSUME t))) 1789 end 1790 1791(*----------------------------------------------------------------------* 1792 * RESORT_EXISTS_CONV: resorts the order of existentially quantified * 1793 * vars, as specified by a given resort function * 1794 * * 1795 * RESORT_EXISTS_CONV rev "?x1 x2 x3. t" ---> |- * 1796 * ?x1 x2 x3. t = ?x3 x2 x1. t * 1797 * * 1798 * The standard use of this conversion is with a resort function, that * 1799 * returns a permutation of the original variables. However, it can * 1800 * also introduce or eliminate variables, provided that these variables * 1801 * are not free in t. * 1802 * * 1803 * RESORT_EXISTS_CONV (K [``x2``, ``new``]) ``?x1 x2 x3. t`` ---> * 1804 * |- ?x1 x2 x3. t = ?x2 new. t * 1805 *----------------------------------------------------------------------*) 1806 1807local 1808 fun mk_list_exists_thm ys xs t = 1809 let 1810 val thm1 = 1811 foldr (fn (v, thm) => 1812 EXISTS (mk_exists {Bvar = v, Body = concl thm}, v) thm) 1813 (ASSUME t) xs 1814 val (t', thm2) = 1815 foldr (fn (v, (t, thm)) => 1816 let 1817 val t' = mk_exists {Bvar = v, Body = t} 1818 in 1819 (t', CHOOSE (v, ASSUME t') thm) 1820 end) (t, thm1) ys 1821 in 1822 DISCH t' thm2 1823 end 1824in 1825 fun RESORT_EXISTS_CONV rs xst = 1826 let 1827 val (xs, t) = strip_exists xst 1828 val ys = rs xs 1829 in 1830 IMP_ANTISYM_RULE (mk_list_exists_thm xs ys t) 1831 (mk_list_exists_thm ys xs t) 1832 end 1833end 1834 1835(*----------------------------------------------------------------------* 1836 * SWAP_FORALL_CONV: swap the order of existentially quantified vars. * 1837 * * 1838 * SWAP_FORALL_CONV "!x y.t[x,y]" ---> |- !x y.t[x,y] = !y x.t[x,y] * 1839 *----------------------------------------------------------------------*) 1840 1841fun SWAP_FORALL_CONV xyt = 1842 let 1843 val {Bvar = x, Body = yt} = dest_forall xyt 1844 val {Bvar = y, Body = t} = dest_forall yt 1845 val xt = mk_forall {Bvar = x, Body = t} 1846 val yxt = mk_forall {Bvar = y, Body = xt} 1847 in 1848 IMP_ANTISYM_RULE 1849 (DISCH xyt (GENL [y, x] (SPECL [x, y] (ASSUME xyt)))) 1850 (DISCH yxt (GENL [x, y] (SPECL [y, x] (ASSUME yxt)))) 1851 end 1852 1853(*----------------------------------------------------------------------* 1854 * RESORT_FORALL_CONV: resorts the order of allquantified vars, as * 1855 * specified by a given resort function * 1856 * * 1857 * RESORT_FORALL_CONV rev "!x1 x2 x3. t" ---> |- * 1858 * !x1 x2 x3. t = !x3 x2 x1. t * 1859 * * 1860 * The standard use of this conversion is with a resort function, that * 1861 * returns a permutation of the original variables. However, it can * 1862 * also introduce or eliminate variables, provided that these variables * 1863 * are not free in t. * 1864 * * 1865 * RESORT_FORALL_CONV (K [``x2``, ``new``]) ``!x1 x2 x3. t`` ---> * 1866 * |- !x1 x2 x3. t = !x2 new. t * 1867 *----------------------------------------------------------------------*) 1868 1869fun RESORT_FORALL_CONV rs xst = 1870 let 1871 val (xs, t) = strip_forall xst 1872 val ys = rs xs 1873 val yst = list_mk_forall (ys, t) 1874 in 1875 IMP_ANTISYM_RULE 1876 (DISCH xst (GENL ys (SPECL xs (ASSUME xst)))) 1877 (DISCH yst (GENL xs (SPECL ys (ASSUME yst)))) 1878 end 1879 1880(*----------------------------------------------------------------------* 1881 * FORALL_SIMP_CONV: gets rid of unused allquantification * 1882 * * 1883 * |- !x. P = P * 1884 *----------------------------------------------------------------------*) 1885 1886fun FORALL_SIMP_CONV xt = 1887 let 1888 val {Bvar = x, Body = t} = dest_forall xt 1889 in 1890 IMP_ANTISYM_RULE (DISCH xt (SPEC x (ASSUME xt))) 1891 (DISCH t (GEN x (ASSUME t))) 1892 end 1893 1894(*----------------------------------------------------------------------* 1895 * LIST version of some conversions defined above. The final goal is * 1896 * to minimise the scope of universal quantifiers. * 1897 *----------------------------------------------------------------------*) 1898 1899local 1900 fun FORALL_DEPTH_CONV c t = 1901 let 1902 val (_, body) = Psyntax.dest_forall t 1903 in 1904 if is_forall body 1905 then (QUANT_CONV (FORALL_DEPTH_CONV c) THENC c) t 1906 else c t 1907 end 1908 fun NUM_QUANT_CONV n = funpow n QUANT_CONV 1909in 1910 (* -------------------------------------------------- * 1911 * Gets rid of unused quantifiers * 1912 * * 1913 * ``!x1 x2 x3. P x2`` --> ``!x2. P x2`` * 1914 * -------------------------------------------------- *) 1915 1916 fun LIST_FORALL_SIMP_CONV t = 1917 let 1918 val (vs, body) = strip_forall t 1919 val _ = if null vs then Feedback.fail () else () 1920 val fv_set = FVL [body] empty_tmset 1921 val (vs_free, vs_rest) = 1922 partition (fn v => HOLset.member (fv_set, v)) vs 1923 val _ = if null vs_rest then Feedback.fail () else () 1924 val thm = RESORT_FORALL_CONV (K vs_free) t 1925 in 1926 thm 1927 end 1928 1929 (* -------------------------------------------------- * 1930 * Moves over conjunctions * 1931 * * 1932 * ``!x1 x2 x3. P1 /\ P2`` --> * 1933 * ``!x1 x2 x3. P1 /\ !x1 x2 x3. P2`` * 1934 * -------------------------------------------------- *) 1935 1936 val LIST_FORALL_AND_CONV = FORALL_DEPTH_CONV FORALL_AND_CONV 1937 1938 (* -------------------------------------------------- * 1939 * Moves over implications * 1940 * * 1941 * ``!x1 x2 x3. P1 x1 x2 ==> P2 x2 x3`` --> * 1942 * ``!x2. (?x1. P1 x1 x2) ==> (!x3. P2 x2 x3)`` or * 1943 * ``!x1 x2. P1 x1 x2) ==> (!x3. P2 x2 x3)`` * 1944 * depending on the value of exists_intro * 1945 * -------------------------------------------------- *) 1946 1947 fun LIST_FORALL_IMP_CONV exists_intro t = 1948 let 1949 val (vs, body) = strip_forall t 1950 val (b1, b2) = Psyntax.dest_imp_only body 1951 val fvs_1 = FVL [b1] empty_tmset 1952 val fvs_2 = FVL [b2] empty_tmset 1953 val (vs_b1x, vs_rest) = partition (fn v => HOLset.member (fvs_1, v)) vs 1954 val (vs_b12, vs_b1) = 1955 partition (fn v => HOLset.member (fvs_2, v)) vs_b1x 1956 val (vs_b2, _) = partition (fn v => HOLset.member (fvs_2, v)) vs_rest 1957 val _ = if null vs_b2 andalso 1958 (not exists_intro orelse null vs_b1) then 1959 raise UNCHANGED else () 1960 val (n, rs) = if exists_intro 1961 then (length vs_b12, vs_b12 @ vs_b1 @ vs_b2) 1962 else (length vs_b1x, vs_b1x @ vs_b2) 1963 val conv1 = RESORT_FORALL_CONV (K rs) 1964 val conv2 = NUM_QUANT_CONV n (FORALL_DEPTH_CONV FORALL_IMP_CONV) 1965 in 1966 (conv1 THENC conv2) t 1967 end 1968 1969 (* -------------------------------------------------- * 1970 * Moves over or * 1971 * * 1972 * ``!x1 x2 x3. P1 x1 x2 \/ P2 x2 x3`` --> * 1973 * ``!x2. (!x1. P1 x1 x2) \/ (!x3. P2 x2 x3)`` * 1974 * -------------------------------------------------- *) 1975 1976 fun LIST_FORALL_OR_CONV t = 1977 let 1978 val (vs, body) = strip_forall t 1979 val (b1, b2) = Psyntax.dest_disj body 1980 val fvs_1 = FVL [b1] empty_tmset 1981 val fvs_2 = FVL [b2] empty_tmset 1982 val (vs_b1x, vs_rest) = partition (fn v => HOLset.member (fvs_1, v)) vs 1983 val (vs_b12, vs_b1) = 1984 partition (fn v => HOLset.member (fvs_2, v)) vs_b1x 1985 val (vs_b2, _) = partition (fn v => HOLset.member (fvs_2, v)) vs_rest 1986 val _ = if null vs_b1 andalso null vs_b2 then raise UNCHANGED else () 1987 val conv1 = RESORT_FORALL_CONV (K (vs_b12 @ vs_b1 @ vs_b2)) 1988 val conv2 = 1989 NUM_QUANT_CONV (length vs_b12) (FORALL_DEPTH_CONV FORALL_OR_CONV) 1990 in 1991 (conv1 THENC conv2) t 1992 end 1993 1994 (* -------------------------------------------------- * 1995 * Moves over negation * 1996 * * 1997 * ``!x1 x2 x3. ~P1`` --> ``~?x1 x2 x3. P1`` * 1998 * -------------------------------------------------- *) 1999 2000 val LIST_FORALL_NOT_CONV = FORALL_DEPTH_CONV FORALL_NOT_CONV 2001 2002 (* -------------------------------------------------- * 2003 * Tries to minimise the scope of universal * 2004 * quantifiers using all the conversions above * 2005 * -------------------------------------------------- *) 2006 2007 fun MINISCOPE_FORALL_CONV exists_intro t = 2008 let 2009 val (vs, body) = strip_forall t 2010 val _ = if null vs then raise UNCHANGED else () 2011 in 2012 (if is_conj body 2013 then LIST_FORALL_AND_CONV 2014 else if is_disj body 2015 then LIST_FORALL_OR_CONV 2016 else if is_imp_only body 2017 then LIST_FORALL_IMP_CONV exists_intro 2018 else if is_neg body andalso exists_intro 2019 then LIST_FORALL_NOT_CONV 2020 else LIST_FORALL_SIMP_CONV) t 2021 end 2022end 2023 2024(*----------------------------------------------------------------------* 2025 * LIST version of some conversions defined above. The final goal is * 2026 * to minimise the scope of existential quantifiers. * 2027 *----------------------------------------------------------------------*) 2028 2029local 2030 fun EXISTS_DEPTH_CONV c t = 2031 let 2032 val (_, body) = Psyntax.dest_exists t 2033 in 2034 if is_exists body 2035 then (QUANT_CONV (EXISTS_DEPTH_CONV c) THENC c) t 2036 else c t 2037 end 2038 fun NUM_QUANT_CONV n = funpow n QUANT_CONV 2039in 2040 (* -------------------------------------------------- * 2041 * Gets rid of unused quantifiers * 2042 * * 2043 * ``?x1 x2 x3. P x2`` --> ``?x2. P x2`` * 2044 * -------------------------------------------------- *) 2045 2046 fun LIST_EXISTS_SIMP_CONV t = 2047 let 2048 val (vs, body) = strip_exists t 2049 val _ = if null vs then Feedback.fail () else () 2050 val fv_set = FVL [body] empty_tmset 2051 val (vs_free, vs_rest) = 2052 partition (fn v => HOLset.member (fv_set, v)) vs 2053 val _ = if null vs_rest then Feedback.fail () else () 2054 val thm = RESORT_EXISTS_CONV (K vs_free) t 2055 in 2056 thm 2057 end 2058 2059 (* -------------------------------------------------- * 2060 * Moves over disjunctions * 2061 * * 2062 * ``?x1 x2 x3. P1 \/ P2`` --> * 2063 * ``?x1 x2 x3. P1 \/ ?x1 x2 x3. P2`` * 2064 * -------------------------------------------------- *) 2065 2066 val LIST_EXISTS_OR_CONV = EXISTS_DEPTH_CONV EXISTS_OR_CONV 2067 2068 (* -------------------------------------------------- * 2069 * Moves over implications * 2070 * * 2071 * ``?x1 x2 x3. P1 x1 x2 ==> P2 x2 x3`` --> * 2072 * ``?x2. (!x1. P1 x1 x2) ==> (?x3. P2 x2 x3)`` or * 2073 * ``?x1 x2. P1 x1 x2) ==> (?x3. P2 x2 x3)`` * 2074 * depending on the value of forall_intro * 2075 * -------------------------------------------------- *) 2076 2077 fun LIST_EXISTS_IMP_CONV forall_intro t = 2078 let 2079 val (vs, body) = strip_exists t 2080 val (b1, b2) = Psyntax.dest_imp_only body 2081 val fvs_1 = FVL [b1] empty_tmset 2082 val fvs_2 = FVL [b2] empty_tmset 2083 val (vs_b1x, vs_rest) = partition (fn v => HOLset.member (fvs_1, v)) vs 2084 val (vs_b12, vs_b1) = 2085 partition (fn v => HOLset.member (fvs_2, v)) vs_b1x 2086 val (vs_b2, _) = partition (fn v => HOLset.member (fvs_2, v)) vs_rest 2087 val _ = if null vs_b2 andalso 2088 (not forall_intro orelse null vs_b1) 2089 then raise UNCHANGED 2090 else () 2091 val (n, rs) = if forall_intro 2092 then (length vs_b12, vs_b12 @ vs_b1 @ vs_b2) 2093 else (length vs_b1x, vs_b1x @ vs_b2) 2094 val conv1 = RESORT_EXISTS_CONV (K rs) 2095 val conv2 = NUM_QUANT_CONV n (EXISTS_DEPTH_CONV EXISTS_IMP_CONV) 2096 in 2097 (conv1 THENC conv2) t 2098 end 2099 2100 (* ---------------------------------------------------------------------* 2101 * BOTH_EXISTS_IMP_CONV, implements the following axiom scheme. * 2102 * * 2103 * |- (?x. P[x]==>Q[x]) = ((!x.P[x]) ==> (?x.Q[x]) * 2104 * * 2105 * Thus, it handles thes missing case of EXISTS_IMP_CONV, where * 2106 * x is free in both P an Q * 2107 * ---------------------------------------------------------------------*) 2108 2109 val BOTH_EXISTS_IMP_CONV = 2110 let 2111 val conv1 = QUANT_CONV (PART_MATCH lhs boolTheory.IMP_DISJ_THM) 2112 val conv2 = EXISTS_OR_CONV 2113 val conv3 = (RATOR_CONV o RAND_CONV) EXISTS_NOT_CONV 2114 val conv4 = 2115 PART_MATCH lhs 2116 (CONV_RULE (ONCE_DEPTH_CONV SYM_CONV) boolTheory.IMP_DISJ_THM) 2117 in 2118 conv1 THENC conv2 THENC conv3 THENC conv4 2119 end 2120 2121 (* -------------------------------------------------- * 2122 * Moves over conjunctions * 2123 * * 2124 * ``?x1 x2 x3. P1 x1 x2 /\ P2 x2 x3`` --> * 2125 * ``?x2. (?x1. P1 x1 x2) /\ (?x3. P2 x2 x3)`` * 2126 * -------------------------------------------------- *) 2127 2128 fun LIST_EXISTS_AND_CONV t = 2129 let 2130 val (vs, body) = strip_exists t 2131 val (b1, b2) = Psyntax.dest_conj body 2132 val fvs_1 = FVL [b1] empty_tmset 2133 val fvs_2 = FVL [b2] empty_tmset 2134 val (vs_b1x, vs_rest) = partition (fn v => HOLset.member (fvs_1, v)) vs 2135 val (vs_b12, vs_b1) = 2136 partition (fn v => HOLset.member (fvs_2, v)) vs_b1x 2137 val (vs_b2, _) = partition (fn v => HOLset.member (fvs_2, v)) vs_rest 2138 val _ = if null vs_b1 andalso null vs_b2 2139 then raise UNCHANGED 2140 else () 2141 val conv1 = RESORT_EXISTS_CONV (K (vs_b12 @ vs_b1 @ vs_b2)) 2142 val conv2 = 2143 NUM_QUANT_CONV (length vs_b12) (EXISTS_DEPTH_CONV EXISTS_AND_CONV) 2144 in 2145 (conv1 THENC conv2) t 2146 end 2147 2148 (* -------------------------------------------------- * 2149 * Moves over negation * 2150 * * 2151 * ``?x1 x2 x3. ~P1`` --> ``~!x1 x2 x3. P1`` * 2152 * -------------------------------------------------- *) 2153 2154 val LIST_EXISTS_NOT_CONV = EXISTS_DEPTH_CONV EXISTS_NOT_CONV 2155 2156 (* -------------------------------------------------- * 2157 * Tries to minimise the scope of universal * 2158 * quantifiers using all the conversions above * 2159 * -------------------------------------------------- *) 2160 2161 fun MINISCOPE_EXISTS_CONV forall_intro t = 2162 let 2163 val (vs, body) = strip_exists t 2164 val _ = if null vs then raise UNCHANGED else () 2165 in 2166 (if is_disj body 2167 then LIST_EXISTS_OR_CONV 2168 else if is_conj body 2169 then LIST_EXISTS_AND_CONV 2170 else if is_imp_only body 2171 then LIST_EXISTS_IMP_CONV forall_intro 2172 else if is_neg body andalso forall_intro 2173 then LIST_EXISTS_NOT_CONV 2174 else 2175 LIST_EXISTS_SIMP_CONV) t 2176 end 2177end 2178 2179(*----------------------------------------------------------------------* 2180 * bool_EQ_CONV: conversion for boolean equality. * 2181 * * 2182 * bool_EQ_CONV "b1 = b2" returns: * 2183 * * 2184 * |- (b1 = b2) = T if b1 and b2 are identical boolean terms * 2185 * |- (b1 = b2) = b2 if b1 = "T" * 2186 * |- (b1 = b2) = b1 if b2 = "T" * 2187 * * 2188 * Added TFM 88.03.31 * 2189 * Revised TFM 90.07.24 * 2190 *----------------------------------------------------------------------*) 2191 2192local 2193 val b = Term.mk_var ("b", Type.bool) 2194 val (Tb :: bT :: _) = map (GEN b) (CONJUNCTS (SPEC b EQ_CLAUSES)) 2195in 2196 fun bool_EQ_CONV tm = 2197 let 2198 val {lhs, rhs} = dest_eq tm 2199 val _ = if type_of rhs = Type.bool 2200 then () 2201 else raise ERR "bool_EQ_CONV" "does not have boolean type" 2202 in 2203 if aconv lhs rhs then EQT_INTRO (REFL lhs) 2204 else if aconv lhs T then SPEC rhs Tb 2205 else if aconv rhs T then SPEC lhs bT 2206 else raise ERR "bool_EQ_CONV" "inapplicable" 2207 end 2208 handle e => raise (wrap_exn "Conv" "bool_EQ_CONV" e) 2209end 2210 2211(*----------------------------------------------------------------------* 2212 * EXISTS_UNIQUE_CONV: expands with the definition of unique existence. * 2213 * * 2214 * * 2215 * EXISTS_UNIQUE_CONV "?!x.P[x]" yields the theorem: * 2216 * * 2217 * |- ?!x.P[x] = ?x.P[x] /\ !x y. P[x] /\ P[y] ==> (x=y) * 2218 * * 2219 * ADDED: TFM 90.05.06 * 2220 * * 2221 * REVISED: now uses a variant of x for y in 2nd conjunct [TFM 90.06.11]* 2222 *----------------------------------------------------------------------*) 2223 2224local 2225 val v = genvar Type.bool 2226 val AND = boolSyntax.conjunction 2227 val IMP = boolSyntax.implication 2228 val check = assert boolSyntax.is_exists1 2229 fun MK_BIN f (e1, e2) = MK_COMB ((AP_TERM f e1), e2) 2230 val rule = CONV_RULE o RAND_CONV o GEN_ALPHA_CONV 2231 fun MK_ALL x y tm = rule y (FORALL_EQ x tm) 2232 fun handle_ant {conj1, conj2} = (BETA_CONV conj1, BETA_CONV conj2) 2233 fun conv (nx, ny) t = 2234 case strip_forall t of 2235 ([ox, oy], imp) => 2236 let 2237 val {ant, conseq} = dest_imp imp 2238 val ant' = MK_BIN AND (handle_ant (dest_conj ant)) 2239 in 2240 MK_ALL ox nx (MK_ALL oy ny (MK_BIN IMP (ant', REFL conseq))) 2241 end 2242 | _ => raise ERR "EXISTS_UNIQUE" "" 2243in 2244 fun EXISTS_UNIQUE_CONV tm = 2245 let 2246 val _ = check tm 2247 val {Rator, Rand} = dest_comb tm 2248 val (ab as {Bvar, Body}) = dest_abs Rand 2249 val def = INST_TYPE [alpha |-> type_of Bvar] EXISTS_UNIQUE_DEF 2250 val exp = RIGHT_BETA (AP_THM def Rand) 2251 and y = variant (all_vars Body) Bvar 2252 in 2253 SUBST [v |-> conv (Bvar, y) (rand (rand (concl exp)))] 2254 (mk_eq {lhs = tm, 2255 rhs = mk_conj {conj1 = mk_exists ab, conj2 = v}}) exp 2256 end 2257 handle HOL_ERR _ => raise ERR "EXISTS_UNIQUE_CONV" "" 2258end 2259 2260(*----------------------------------------------------------------------* 2261 * COND_CONV: conversion for simplifying conditionals: * 2262 * * 2263 * --------------------------- COND_CONV "T => u | v" * 2264 * |- (T => u | v) = u * 2265 * * 2266 * * 2267 * --------------------------- COND_CONV "F => u | v" * 2268 * |- (F => u | v) = v * 2269 * * 2270 * * 2271 * --------------------------- COND_CONV "b => u | u" * 2272 * |- (b => u | u) = u * 2273 * * 2274 * --------------------------- COND_CONV "b => u | v" (u =alpha v) * 2275 * |- (b => u | v) = u * 2276 * * 2277 * COND_CONV "P=>u|v" fails if P is neither "T" nor "F" and u =/= v. * 2278 *----------------------------------------------------------------------*) 2279 2280local 2281 val vt = genvar alpha 2282 and vf = genvar alpha 2283 val gen = GENL [vt, vf] 2284 val (CT, CF) = (gen ## gen) (CONJ_PAIR (SPECL [vt, vf] COND_CLAUSES)) 2285in 2286 fun COND_CONV tm = 2287 let 2288 val {cond, larm, rarm} = dest_cond tm 2289 val INST_TYPE' = INST_TYPE [alpha |-> type_of larm] 2290 in 2291 if aconv cond T then SPEC rarm (SPEC larm (INST_TYPE' CT)) 2292 else if aconv cond F then SPEC rarm (SPEC larm (INST_TYPE' CF)) 2293 else if aconv larm rarm then SPEC larm (SPEC cond (INST_TYPE' COND_ID)) 2294 else raise ERR "" "" 2295 end 2296 handle HOL_ERR _ => raise ERR "COND_CONV" "" 2297end 2298 2299(* ===================================================================== * 2300 * A rule defined using conversions. * 2301 * ===================================================================== *) 2302 2303(*----------------------------------------------------------------------* 2304 * EXISTENCE: derives existence from unique existence: * 2305 * * 2306 * |- ?!x. P[x] * 2307 * -------------------- * 2308 * |- ?x. P[x] * 2309 * * 2310 *----------------------------------------------------------------------*) 2311 2312local 2313 val EXISTS_UNIQUE_DEF = boolTheory.EXISTS_UNIQUE_DEF 2314 val P = mk_var {Name = "P", Ty = alpha-->bool} 2315 val th1 = SPEC P (CONV_RULE (X_FUN_EQ_CONV P) EXISTS_UNIQUE_DEF) 2316 val th2 = CONJUNCT1 (UNDISCH (fst (EQ_IMP_RULE (RIGHT_BETA th1)))) 2317 val ex1P = mk_comb {Rator = boolSyntax.exists1, Rand = P} 2318in 2319 fun EXISTENCE th = 2320 let 2321 val _ = assert boolSyntax.is_exists1 (concl th) 2322 val {Rator, Rand} = dest_comb (concl th) 2323 val {Bvar, ...} = dest_abs Rand 2324 in 2325 MP (SPEC Rand 2326 (INST_TYPE [alpha |-> type_of Bvar] (GEN P (DISCH ex1P th2)))) 2327 th 2328 end 2329 handle HOL_ERR _ => raise ERR "EXISTENCE" "" 2330end 2331 2332(*-----------------------------------------------------------------------* 2333 * AC_CONV - Prove equality using associative + commutative laws * 2334 * * 2335 * The conversion is given an associative and commutative law (it deduces* 2336 * the relevant operator and type from these) in the form of the inbuilt * 2337 * ones, and an equation to prove. It will try to prove this. Example: * 2338 * * 2339 * AC_CONV(ADD_ASSOC,ADD_SYM) "(1 + 3) + (2 + 4) = 4 + (3 + (2 + 1))" * 2340 * [JRH 91.07.17] * 2341 *-----------------------------------------------------------------------*) 2342 2343fun AC_CONV (associative, commutative) = 2344 let 2345 val opr = (rator o rator o lhs o snd o strip_forall o concl) commutative 2346 val ty = (hd o #Args o dest_type o type_of) opr 2347 val x = mk_var {Name = "x", Ty = ty} 2348 and y = mk_var {Name = "y", Ty = ty} 2349 and z = mk_var {Name = "z", Ty = ty} 2350 val xy = mk_comb {Rator = mk_comb {Rator = opr, Rand = x}, Rand = y} 2351 and yz = mk_comb {Rator = mk_comb {Rator = opr, Rand = y}, Rand = z} 2352 and yx = mk_comb {Rator = mk_comb {Rator = opr, Rand = y}, Rand = x} 2353 val comm = PART_MATCH I commutative (mk_eq {lhs = xy, rhs = yx}) 2354 and ass = 2355 PART_MATCH I (SYM (SPEC_ALL associative)) 2356 (mk_eq {lhs = mk_comb {Rator = mk_comb {Rator = opr, Rand = xy}, 2357 Rand = z}, 2358 rhs = mk_comb {Rator = mk_comb {Rator = opr, Rand = x}, 2359 Rand = yz}}) 2360 val asc = TRANS (SUBS [comm] (SYM ass)) (INST [y |-> x, x |-> y] ass) 2361 2362 fun bubble head expr = 2363 let 2364 val {Rator, Rand = r} = dest_comb expr 2365 val {Rator = xopr, Rand = l} = dest_comb Rator 2366 in 2367 if term_eq xopr opr 2368 then if term_eq l head 2369 then REFL expr 2370 else if term_eq r head 2371 then INST [x |-> l, y |-> r] comm 2372 else let 2373 val subb = bubble head r 2374 val eqv = 2375 AP_TERM (mk_comb {Rator = xopr, Rand = l}) subb 2376 val {Rator, Rand = r'} = 2377 dest_comb (#rhs (dest_eq (concl subb))) 2378 val {Rator = yopr, Rand = l'} = dest_comb Rator 2379 in 2380 TRANS eqv (INST [x |-> l, y |-> l', z |-> r'] asc) 2381 end 2382 else raise ERR "AC_CONV" "bubble" 2383 end 2384 2385 fun asce {lhs, rhs} = 2386 if term_eq lhs rhs 2387 then REFL lhs 2388 else let 2389 val {Rator, Rand = r'} = dest_comb lhs 2390 val {Rator = zopr, Rand = l'} = dest_comb Rator 2391 in 2392 if term_eq zopr opr 2393 then let 2394 val beq = bubble l' rhs 2395 val rt = boolSyntax.rhs (concl beq) 2396 in 2397 TRANS (AP_TERM 2398 (mk_comb {Rator = opr, Rand = l'}) 2399 (asce {lhs = rand lhs, rhs = rand rt})) 2400 (SYM beq) 2401 end 2402 else raise ERR "AC_CONV" "asce" 2403 end 2404 in 2405 fn tm => 2406 let 2407 val init = QCONV (TOP_DEPTH_CONV (REWR_CONV ass)) tm 2408 val gl = rhs (concl init) 2409 in 2410 EQT_INTRO (EQ_MP (SYM init) (asce (dest_eq gl))) 2411 end 2412 end 2413 handle e => raise (wrap_exn "Conv" "AC_CONV" e) 2414 2415(*--------------------------------------------------------------------------* 2416 * Conversions for messing with bound variables. * 2417 * * 2418 * RENAME_VARS_CONV renames variables under \ ! ? ?! or @ . * 2419 * SWAP_VARS_CONV swaps variables under ! and ?, * 2420 * e.g, given !x y. ... gives !y x. ... * 2421 *--------------------------------------------------------------------------*) 2422 2423local 2424 fun rename vname t = 2425 let 2426 val (accessor, C_ACC) = 2427 if is_exists t orelse is_forall t orelse is_select t 2428 orelse is_exists1 t 2429 then (rand, RAND_CONV) 2430 else if is_abs t 2431 then (I, I) 2432 else raise ERR "rename_vars" "Term not a binder" 2433 val (ty, _) = dom_rng (type_of (accessor t)) 2434 val newv = mk_var {Name = vname, Ty = ty} 2435 in 2436 C_ACC (ALPHA_CONV newv) t 2437 end 2438in 2439 fun RENAME_VARS_CONV varlist = 2440 case varlist of 2441 [] => REFL 2442 | (v :: vs) => rename v THENC BINDER_CONV (RENAME_VARS_CONV vs) 2443 2444 fun SWAP_VARS_CONV t = 2445 if is_exists t then SWAP_EXISTS_CONV t else SWAP_FORALL_CONV t 2446end 2447 2448(*--------------------------------------------------------------------------* 2449 * EXISTS_AND_REORDER_CONV * 2450 * * 2451 * moves an existential quantifier into a conjunctive body, first sorting * 2452 * the body so that conjuncts where the bound variable appears are * 2453 * put first. * 2454 *--------------------------------------------------------------------------*) 2455 2456fun EXISTS_AND_REORDER_CONV t = 2457 let 2458 open Psyntax 2459 val (var, body) = dest_exists t 2460 handle HOL_ERR _ => raise ERR "EXISTS_AND_REORDER_CONV" 2461 "Term not an existential" 2462 val conjs = strip_conj body 2463 val _ = length conjs > 1 orelse raise UNCHANGED 2464 val (there, notthere) = partition (free_in var) conjs 2465 val _ = not (null notthere) andalso not (null there) 2466 orelse raise UNCHANGED 2467 val newbody = mk_conj (list_mk_conj notthere, list_mk_conj there) 2468 val bodies_eq_thm = 2469 EQT_ELIM (AC_CONV (CONJ_ASSOC, CONJ_COMM) (mk_eq (body, newbody))) 2470 in 2471 (QUANT_CONV (K bodies_eq_thm) THENC EXISTS_AND_CONV) t 2472 end 2473 2474(*---------------------------------------------------------------------------* 2475 * Support for debugging complicated conversions * 2476 *---------------------------------------------------------------------------*) 2477 2478fun PRINT_CONV tm = (Parse.print_term tm; print "\n"; ALL_CONV tm) 2479 2480(*---------------------------------------------------------------------------* 2481 * Map a conversion over a theorem, preserving order of hypotheses. * 2482 *---------------------------------------------------------------------------*) 2483 2484local 2485 fun cnvMP eqth impth = 2486 let 2487 open boolSyntax 2488 val tm = snd (dest_imp (concl impth)) 2489 val imp_refl = REFL implication 2490 in 2491 UNDISCH (EQ_MP (MK_COMB (MK_COMB (imp_refl, eqth), REFL tm)) impth) 2492 end 2493in 2494 fun MAP_THM cnv th = 2495 let 2496 val (hyps, c) = dest_thm th 2497 val cth = cnv c 2498 val hypths = map cnv hyps 2499 in 2500 itlist cnvMP hypths (DISCH_ALL (EQ_MP cth th)) 2501 end 2502 handle HOL_ERR _ => raise ERR "MAP_THM" "" 2503end 2504 2505val PAT_CONV = let 2506 fun PCONV (xs, pat) conv = 2507 if op_mem aconv pat xs then conv 2508 else if not(exists (fn x => free_in x pat) xs) then ALL_CONV 2509 else if is_comb pat then 2510 COMB2_CONV (PCONV (xs, rator pat) conv, PCONV (xs, rand pat) conv) 2511 else 2512 ABS_CONV (PCONV (xs, body pat) conv) 2513in 2514 fn pat => PCONV (strip_abs pat) 2515end 2516 2517fun PATH_CONV path c = 2518 let 2519 val limit = size path 2520 fun recurse i = 2521 if i = limit then c 2522 else 2523 case String.sub(path, i) of 2524 #"a" => ABS_CONV (recurse (i + 1)) 2525 | #"b" => BINDER_CONV (recurse (i + 1)) 2526 | #"l" => RATOR_CONV (recurse (i + 1)) 2527 | #"r" => RAND_CONV (recurse (i + 1)) 2528 | c => raise ERR 2529 "PATH_CONV" 2530 ("Illegal character '"^str c^ "' in path") 2531 in 2532 recurse 0 2533 end 2534 2535(* -------------------------------------------------------------------------- 2536 Helper function for memoizing conversions through the use of a Redblackmap. 2537 -------------------------------------------------------------------------- *) 2538 2539fun memoize dst tree accept err (cnv: conv) = 2540 let 2541 val map = ref tree 2542 in 2543 fn tm => 2544 case dst tm of 2545 SOME x => 2546 (case Redblackmap.peek (!map, x) of 2547 SOME th => th 2548 | NONE => 2549 let 2550 val th = cnv tm 2551 in 2552 if accept (boolSyntax.rhs (Thm.concl th)) 2553 then (map := Redblackmap.insert (!map, x, th); th) 2554 else raise err 2555 end) 2556 | NONE => raise err 2557 end 2558 2559end (* Conv *) 2560