1(* res_quanLib.sml - simpsets, tactics, etc. for restricted quantification 2 3FILE: res_rules.ml DATE: 1 Aug 92 BY: Wai Wong 4TRANSLATED DATE: 28 May 93 BY: Paul Curzon 5UPDATED DATE: 30 Oct 01 BY: Joe Hurd 6UPDATED DATE: 20 Oct 17 BY: Mario Castel��n Castro UOK 7 8This file as a whole is assumed to be under the license in the file 9"COPYRIGHT" in the HOL4 distribution (note added by Mario Castel��n UOK 10Castro). 11 12For the avoidance of legal uncertainty, I (Mario Castel��n Castro) hereby UOK 13place my modifications to this file in the public domain per the Creative 14Commons CC0 public domain dedication <https://creativecommons.org/publicdo 15main/zero/1.0/legalcode>. This should not be interpreted as a personal 16endorsement of permissive (non-Copyleft) licenses. 17 18============================================================================*) 19 20structure res_quanLib :> res_quanLib = 21struct 22 23open HolKernel Parse Drule Conv Tactic Tactical Thm_cont 24 Rewrite boolSyntax res_quanTheory boolTheory simpLib Cond_rewrite; 25 26infix THENR ORELSER ++ ||; 27 28local (* Fix the grammar used by this file *) 29 val ambient_grammars = Parse.current_grammars(); 30 val _ = Parse.temp_set_grammars boolTheory.bool_grammars 31in 32 33val bool_ss = boolSimps.bool_ss; 34val op++ = op THEN; 35val op|| = op ORELSE; 36fun f THENR g = g o f; 37fun f ORELSER g = fn x => f x handle HOL_ERR _ => g x; 38 39val ERR = mk_HOL_ERR "res_quanTools"; 40 41(* ===================================================================== *) 42(* Syntactic operations on restricted quantifications. *) 43(* These ought to be generalised to all kinds of restrictions, *) 44(* but one thing at a time. *) 45(* (These now all come from boolSyntax.) *) 46(* --------------------------------------------------------------------- *) 47 48 49 50(* ===================================================================== *) 51(* Conversions *) 52(* --------------------------------------------------------------------- *) 53 54local 55 fun RES_QUAN_CONV c tm = 56 let 57 val b = snd (dest_comb tm) 58 in 59 (if is_abs b then 60 let 61 val v = fst (dest_abs b) 62 in 63 c 64 THENC RAND_CONV (ALPHA_CONV v) 65 THENC RAND_CONV (ABS_CONV (RAND_CONV BETA_CONV)) 66 end 67 else c) tm 68 end; 69in 70 val RES_FORALL_CONV = RES_QUAN_CONV (REWR_CONV RES_FORALL); 71 val RES_EXISTS_CONV = RES_QUAN_CONV (REWR_CONV RES_EXISTS); 72 val RES_SELECT_CONV = RES_QUAN_CONV (REWR_CONV RES_SELECT); 73end; 74 75val RES_EXISTS_UNIQUE_CONV = 76 REWR_CONV RES_EXISTS_UNIQUE THENC 77 TRY_CONV 78 (LAND_CONV (RAND_CONV (ABS_CONV BETA_CONV)) THENC 79 RAND_CONV 80 (RAND_CONV 81 (ABS_CONV 82 (RAND_CONV 83 (ABS_CONV 84 (LAND_CONV ((LAND_CONV BETA_CONV) THENC (RAND_CONV BETA_CONV)))))))); 85 86(* --------------------------------------------------------------------- *) 87(* If conversion c maps term (--`\i.t1`--) to theorem |- (\i.t1) = (\i'.t1'),*) 88(* then RF_BODY_CONV c (--`!i :: P. t1`--) returns the theorem *) 89(* |- (!i :: P. t1) = (!i' :: P. t1') *) 90(* *) 91(* If conversion c maps term (--`t1`--) to the theorem |- t1 = t1', *) 92(* then RF_CONV c (--`!i :: P. t1`--) returns the theorem *) 93(* |- (!i :: P. t1) = (!i :: P. t1') *) 94(* --------------------------------------------------------------------- *) 95 96fun BOTH_CONV c = (LAND_CONV c THENC RAND_CONV c); 97fun LEFT_THENC_RIGHT c1 c2 = (LAND_CONV c1 THENC RAND_CONV c2); 98 99val RF_BODY_CONV = RAND_CONV; 100val RF_PRED_CONV = (RATOR_CONV o RAND_CONV); 101val RF_CONV = (RAND_CONV o ABS_CONV); 102fun PRED_THENC_BODY c1 c2 = 103 (((RATOR_CONV o RAND_CONV) c1) THENC ((RAND_CONV o ABS_CONV) c2)); 104 105(* --------------------------------------------------------------------- *) 106(* IMP_RES_FORALL_CONV (--`!x. P x ==> t[x]`--) *) 107(* |- !x. P x ==> t[x] = !x :: P. t[x] *) 108(* --------------------------------------------------------------------- *) 109 110val IMP_RES_FORALL_CONV = (fn tm => 111 let val dthm = res_quanTheory.RES_FORALL 112 val (var, a) = dest_forall tm 113 val (ante,t) = dest_imp a 114 val (pred,v) = dest_comb ante 115 in 116 if not(var = v) 117 then raise ERR "IMP_RES_FORALL_CONV" "term not in the correct form" 118 else 119 SYM (RIGHT_CONV_RULE ((GEN_ALPHA_CONV var) THENC 120 (ONCE_DEPTH_CONV BETA_CONV)) 121 (ISPECL [pred,mk_abs(var,t)] dthm)) 122 end 123 handle HOL_ERR _ => 124 raise ERR "IMP_RES_FORALL_CONV" "") 125 :conv; 126 127(* --------------------------------------------------------------------- *) 128(* RES_FORALL_AND_CONV (--`!i :: P. t1 /\ t2`--) = *) 129(* |- (!i :: P. t1 /\ t2) = (!i :: P. t1) /\ (!i :: P. t2) *) 130(* --------------------------------------------------------------------- *) 131 132val RES_FORALL_AND_CONV = (fn tm => 133 let val rthm = res_quanTheory.RES_FORALL_CONJ_DIST 134 val (var,pred,conj) = dest_res_forall tm 135 val (left,right) = dest_conj conj 136 val left_pred = mk_abs(var,left) 137 val right_pred = mk_abs(var,right) 138 val thm = ISPECL [pred, left_pred, right_pred] rthm 139 val c = LEFT_THENC_RIGHT 140 (RF_CONV(BOTH_CONV BETA_CONV)) (BOTH_CONV(RF_CONV BETA_CONV)) 141 in 142 CONV_RULE c thm 143 end 144 handle HOL_ERR _ => 145 raise ERR "RES_FORALL_AND_CONV" "") 146 :conv; 147 148(* --------------------------------------------------------------------- *) 149(* AND_RES_FORALL_CONV (--`(!i :: P. t1) /\ (!i :: P. t2)`--) = *) 150(* |- (!i :: P. t1) /\ (!i :: P. t2) = (!i :: P. t1 /\ t2) *) 151(* --------------------------------------------------------------------- *) 152 153val AND_RES_FORALL_CONV = (fn tm => 154 let val rthm = res_quanTheory.RES_FORALL_CONJ_DIST 155 val conj1 = rand(rator tm) and conj2 = rand tm 156 val (var1,pred1,body1) = dest_res_forall conj1 157 val (var2,pred2,body2) = dest_res_forall conj2 158 val thm = SYM( 159 ISPECL[pred1, mk_abs(var1,body1), mk_abs(var2,body2)] rthm) 160 val c = LEFT_THENC_RIGHT 161 (BOTH_CONV(RF_CONV BETA_CONV)) (RF_CONV(BOTH_CONV BETA_CONV)) 162 in 163 CONV_RULE c thm 164 end 165 handle HOL_ERR _ => 166 raise ERR "AND_RES_FORALL_CONV" "") 167 :conv; 168 169(* --------------------------------------------------------------------- *) 170(* RES_FORALL_SWAP_CONV (--`!i :: P. !j :: Q. R`--) = *) 171(* |- (!i :: P. !j :: Q. R) = (!j :: Q. !i :: P. R) *) 172(* --------------------------------------------------------------------- *) 173 174val RES_FORALL_SWAP_CONV = (fn tm => 175 let val rthm = res_quanTheory.RES_FORALL_REORDER 176 val (i,P,body) = dest_res_forall tm 177 val (j,Q,R) = dest_res_forall body 178 val thm1 = ISPECL [P,Q,mk_abs(i, mk_abs(j, R))] rthm 179 (* Reduce the two beta-redexes on either side of the equation. *) 180 val c1 = RF_CONV(RF_CONV(RATOR_CONV BETA_CONV THENC BETA_CONV)) 181 val thm2 = CONV_RULE (LAND_CONV c1 THENC RAND_CONV c1) thm1 182 (* Rename the bound variables in the quantifications. *) 183 val c2 = 184 LAND_CONV(RF_CONV(RF_BODY_CONV(ALPHA_CONV j)) THENC 185 RF_BODY_CONV(ALPHA_CONV i)) THENC 186 RAND_CONV(RF_CONV(RF_BODY_CONV(ALPHA_CONV i)) THENC 187 RF_BODY_CONV(ALPHA_CONV j)) 188 in 189 if i=j orelse free_in i Q orelse free_in j P 190 then raise ERR "RES_FORALL_SWAP" "" 191 else CONV_RULE c2 thm2 192 end 193 handle HOL_ERR _ => 194 raise ERR "RES_FORALL_SWAP" "") 195 :conv; 196 197(* --------------------------------------------------------------------- *) 198(* RESQ_REWRITE1_CONV : thm list -> thm -> conv *) 199(* RESQ_REWRITE1_CONV thms thm tm *) 200(* The input theorem thm should be restricted quantified equational *) 201(* theorem ie. the form suitable for RESQ_REWRITE_TAC. The input term tm *) 202(* should be an instance of the left-hand side of the conclusion of thm. *) 203(* The theorem list thms should contains theorems matching the conditions*) 204(* in the input thm. They are used to discharge the conditions. The *) 205(* conditions which cannot be discharged by matching theorems will be *) 206(* left in the assumption. *) 207(* --------------------------------------------------------------------- *) 208 209fun RESQ_REWRITE1_CONV thms th = 210 (fn tm => 211 let val th' = CONV_RULE ((TOP_DEPTH_CONV RES_FORALL_CONV) 212 THENC (TOP_DEPTH_CONV RIGHT_IMP_FORALL_CONV)) th 213 in 214 COND_REWRITE1_CONV thms th' tm 215 end):conv; 216 217(* ===================================================================== *) 218(* Derived rules *) 219(* --------------------------------------------------------------------- *) 220 221(* --------------------------------------------------------------------- *) 222(* Rule to specialize a restricted universal quantification. *) 223(* *) 224(* A |- !x :: P. M x *) 225(* ------------------- RESQ_HALF_SPEC *) 226(* A |- t IN P ==> M [t/x] *) 227(* *) 228(* --------------------------------------------------------------------- *) 229 230fun RESQ_HALF_SPEC tm = CONV_RULE RES_FORALL_CONV THENR SPEC tm; 231 232(* --------------------------------------------------------------------- *) 233(* Specialize a list of universal quantifiers which may be a mixture *) 234(* of ordinary or restricted in any order. *) 235(* --------------------------------------------------------------------- *) 236 237fun GEN_RESQ_HALF_SPECL spec res_spec = 238 let 239 fun half_specl asms [] th = foldl (uncurry DISCH) th asms 240 | half_specl asms (s :: rest) th = 241 if is_res_forall (concl th) then 242 let 243 val th = res_spec s th 244 val (a, _) = dest_imp (concl th) 245 in 246 half_specl (a :: asms) rest (UNDISCH th) 247 end 248 else if is_forall (concl th) then half_specl asms rest (spec s th) 249 else raise ERR "GEN_RESQ_HALF_SPECL" "not a universal quantifier" 250 in 251 half_specl [] 252 end; 253 254val RESQ_HALF_SPECL = GEN_RESQ_HALF_SPECL SPEC RESQ_HALF_SPEC; 255 256(* --------------------------------------------------------------------- *) 257(* Rule to specialize a possibly restricted universal quantification. *) 258(* *) 259(* A |- !x :: P. M x A |- !x. M x *) 260(* ------------------- -------------- RESQ_SPEC ``t`` *) 261(* A, t IN P |- M t A |- M t *) 262(* *) 263(* --------------------------------------------------------------------- *) 264 265fun RESQ_SPEC tm = (RESQ_HALF_SPEC tm THENR UNDISCH) ORELSER SPEC tm; 266 267(* ---------------------------------------------------------------------*) 268(* RESQ_SPECL : term list -> thm -> thm *) 269(* An analogy to SPECL as RESQ_SEPC to SPEC. *) 270(* Instatiate a list of possibly restricted universal quantifiers. *) 271(* ---------------------------------------------------------------------*) 272 273val RESQ_SPECL = C (foldl (uncurry RESQ_SPEC)); 274 275(* --------------------------------------------------------------------- *) 276(* RESQ_MATCH_MP : thm -> thm -> thm *) 277(* RESQ_MATCH_MP (|- !x :: P. Q x) (|- t IN P) returns |- Q t *) 278(* --------------------------------------------------------------------- *) 279 280fun RESQ_MATCH_MP th1 th2 = MATCH_MP (CONV_RULE RES_FORALL_CONV th1) th2; 281 282(* --------------------------------------------------------------------- *) 283(* RESQ_REWR_CANON : thm -> thm *) 284(* convert a theorem into a canonical form for COND_REWR_TAC *) 285(* --------------------------------------------------------------------- *) 286 287val RESQ_REWR_CANON = 288 COND_REWR_CANON o (CONV_RULE ((TOP_DEPTH_CONV RES_FORALL_CONV))); 289 290(* ===================================================================== *) 291(* Tactics *) 292(* --------------------------------------------------------------------- *) 293 294(* --------------------------------------------------------------------- *) 295(* Tactic to strip off a restricted existential quantification. *) 296(* *) 297(* A ?- ?x :: P. t *) 298(* =================== RESQ_EXISTS_TAC (--`x'`--) *) 299(* A ?- x' IN P /\ t *) 300(* *) 301(* --------------------------------------------------------------------- *) 302 303fun RESQ_EXISTS_TAC tm = CONV_TAC RES_EXISTS_CONV ++ EXISTS_TAC tm; 304 305(* --------------------------------------------------------------------- *) 306(* Tactic to strip off a restricted universal quantification. *) 307(* User supplies a thm tactic for the x IN P theorem that results. *) 308(* --------------------------------------------------------------------- *) 309 310fun RESQ_GEN_THEN ttac = 311 CONV_TAC RES_FORALL_CONV ++ GEN_TAC ++ DISCH_THEN ttac; 312 313(* --------------------------------------------------------------------- *) 314(* A restricted quantification version of STRIP_TAC. *) 315(* --------------------------------------------------------------------- *) 316 317fun RESQ_HALF_EXISTS_THEN (ttac : thm_tactic) = 318 ttac o CONV_RULE RES_EXISTS_CONV; 319 320val RESQ_CHOOSE_THEN = 321 RESQ_HALF_EXISTS_THEN THEN_TCL CHOOSE_THEN THEN_TCL CONJUNCTS_THEN; 322 323val RESQ_STRIP_THM_THEN = STRIP_THM_THEN ORELSE_TCL RESQ_CHOOSE_THEN; 324 325fun RESQ_STRIP_GOAL_THEN ttac = STRIP_GOAL_THEN ttac || RESQ_GEN_THEN ttac; 326 327val RESQ_STRIP_ASSUME_TAC = REPEAT_TCL RESQ_STRIP_THM_THEN CHECK_ASSUME_TAC; 328 329val RESQ_STRIP_TAC = RESQ_STRIP_GOAL_THEN RESQ_STRIP_ASSUME_TAC; 330 331(* --------------------------------------------------------------------- *) 332(* Tactic to strip off a restricted universal quantification. *) 333(* Uses RESQ_STRIP_ASSUME_TAC to add |- x IN P to the assumptions. *) 334(* *) 335(* A ?- !x :: P. t *) 336(* =================== RESQ_GEN_TAC *) 337(* A, x IN P ?- t *) 338(* *) 339(* --------------------------------------------------------------------- *) 340 341val RESQ_GEN_TAC = RESQ_GEN_THEN RESQ_STRIP_ASSUME_TAC; 342 343(* --------------------------------------------------------------------- *) 344(* RESOLUTION *) 345(* --------------------------------------------------------------------- *) 346 347(* --------------------------------------------------------------------- *) 348(* check st l : Fail with st if l is empty, otherwise return l. *) 349(* --------------------------------------------------------------------- *) 350 351local fun check st l = if null l then raise ERR "check" st else l 352 353(* --------------------------------------------------------------------- *) 354(* check_res th : Fail if th is not in the form: *) 355(* !x0 ... xn. !y :: P. t otherwise, it returns the following theorem *) 356(* !x0 ... xn y. P ==> t. *) 357(* --------------------------------------------------------------------- *) 358 359and check_res th = 360 if is_forall (concl th) then 361 GEN_ALL (CONV_RULE RES_FORALL_CONV (SPEC_ALL th)) 362 else CONV_RULE RES_FORALL_CONV th 363 handle _ => raise ERR "check_res" "not restricted forall"; 364in 365 366(* --------------------------------------------------------------------- *) 367(* RESQ_IMP_RES_THEN : Resolve a restricted quantified theorem against *) 368(* the assumptions. *) 369(* --------------------------------------------------------------------- *) 370 371fun RESQ_IMP_RES_THEN ttac resth = 372 let val th = check_res resth 373 in IMP_RES_THEN ttac th 374 end 375 handle HOL_ERR{message = s,...} => 376 raise ERR "RESQ_IMP_RES_THEN" s 377 378(* --------------------------------------------------------------------- *) 379(* RESQ_RES_THEN : Resolve all restricted universally quantified *) 380(* assumptions against the rest. *) 381(* --------------------------------------------------------------------- *) 382 383and RESQ_RES_THEN (ttac:thm_tactic) (asl,g) = 384 let val a = map ASSUME asl 385 val ths = mapfilter check_res a 386 val imps = check "RESQ_RES_THEN: no restricted quantification " ths 387 val l = itlist (fn th=>append (mapfilter (MATCH_MP th) a)) imps [] 388 val res = check "RESQ_RES_THEN: no resolvents " l 389 val tacs = check "RESQ_RES_THEN: no tactics" (mapfilter ttac res) 390 in 391 EVERY tacs (asl,g) 392 end 393end; 394 395fun RESQ_IMP_RES_TAC th g = 396 RESQ_IMP_RES_THEN (REPEAT_GTCL RESQ_IMP_RES_THEN STRIP_ASSUME_TAC) th g 397 handle _ => ALL_TAC g; 398 399fun RESQ_RES_TAC g = 400 RESQ_RES_THEN (REPEAT_GTCL RESQ_IMP_RES_THEN STRIP_ASSUME_TAC) g 401 handle _ => ALL_TAC g; 402 403(* --------------------------------------------------------------------- *) 404(* RESQ_REWRITE1_TAC : thm_tactic *) 405(* RESQ_REWRITE1_TAC |- !x::P. u[x] = v[x] *) 406(* transforms the input restricted quantified theorem to implicative *) 407(* form then do conditional rewriting. *) 408(* --------------------------------------------------------------------- *) 409 410fun RESQ_REWRITE1_TAC th' = 411 let val th = RESQ_REWR_CANON th' 412 in 413 COND_REWR_TAC search_top_down th 414 end; 415 416(* --------------------------------------------------------------------- *) 417(* Restricted quantifier elimination using the simplifier. *) 418(* --------------------------------------------------------------------- *) 419 420val ELIM_RESQ_ss = named_rewrites "ELIM_RESQ_ss" [ 421 RES_FORALL, RES_EXISTS, RES_EXISTS_UNIQUE, RES_SELECT]; 422 423val resq_SS = 424 simpLib.SSFRAG 425 {name=SOME"resq", 426 ac = [], congs = [], 427 convs = 428 [{conv = K (K RES_FORALL_CONV), 429 key = SOME ([], Term `RES_FORALL (p:'a -> bool) m`), 430 name = "RES_FORALL_CONV", trace = 2}, 431 {conv = K (K RES_EXISTS_CONV), 432 key = SOME ([], Term `RES_EXISTS (p:'a -> bool) m`), 433 name = "RES_EXISTS_CONV", trace = 2}, 434 {conv = K (K RES_SELECT_CONV), 435 key = SOME ([], Term `RES_SELECT (p:'a -> bool) m`), 436 name = "RES_SELECT_CONV", trace = 2}, 437 {conv = K (K RES_EXISTS_UNIQUE_CONV), 438 key = SOME ([], Term `RES_EXISTS_UNIQUE (p:'a -> bool) m`), 439 name = "RES_EXISTS_UNIQUE_CONV", trace = 2}], 440 dprocs = [], filter = NONE, rewrs = []}; 441 442val resq_ss = simpLib.++ (bool_ss, resq_SS); 443 444val RESQ_TAC = 445 FULL_SIMP_TAC resq_ss [] THEN 446 POP_ASSUM_LIST (EVERY o map STRIP_ASSUME_TAC o rev); 447 448(* Each row is a set of analogus rewrite rules; an additional level of 449indentation means that a row continues the previous one. *) 450val RICH_RESQ_ss = named_rewrites "RICH_RESQ" [ 451 (* Unconditional facts that can be simplifier to a boolean value. *) 452 RES_FORALL_T, RES_EXISTS_F, RES_EXISTS_UNIQUE_F, 453 RES_FORALL_EMPTY, RES_EXISTS_EMPTY, RES_EXISTS_UNIQUE_EMPTY, 454 455 (* Unconditional rewriting rules. *) 456 RES_FORALL_UNIV, RES_EXISTS_UNIV, RES_EXISTS_UNIQUE_UNIV, 457 NOT_RES_FORALL, NOT_RES_EXISTS, 458 RES_FORALL_UNIQUE, RES_EXISTS_EQUAL, 459 RES_FORALL_F, RES_EXISTS_T, RES_EXISTS_UNIQUE_T, 460 RES_FORALL_NULL, RES_EXISTS_NULL, RES_EXISTS_UNIQUE_NULL, 461 462 (* Conditional rewriting rules and facts. *) 463 RES_FORALL_SUBSET, RES_EXISTS_SUBSET]; 464 465val RESQ_PRED_SET_ss = named_rewrites "RESQ_PRED_SET_ss" [ 466 RES_FORALL_UNION, RES_EXISTS_UNION, 467 RES_FORALL_DIFF, RES_EXISTS_DIFF, 468 IN_BIGINTER_RES_FORALL, IN_BIGUNION_RES_EXISTS, 469 RES_FORALL_BIGUNION, RES_EXISTS_BIGUNION, 470 RES_FORALL_BIGINTER, RES_EXISTS_BIGINTER]; 471 472(* ===================================================================== *) 473(* Functions for making definition with restrict universal quantified *) 474(* variables. *) 475(* The auxiliary functions used here are taken from the system directly. *) 476(* --------------------------------------------------------------------- *) 477 478(* check that tm is a <varstruct> where: 479 480 <varstruct> ::= <var> | (<varstruct>,...,<varstruct>) 481 482 and that there are no repeated variables. Return list of variables. 483*) 484 485fun check_varstruct tm = 486 if is_var tm 487 then [tm] 488 else 489 let val (t1,t2) = pairSyntax.dest_pair tm 490 handle _ => raise ERR "check_varstruct" "bad varstruct" 491 492 val l1 = check_varstruct t1 493 val l2 = check_varstruct t2 494 in 495 if intersect l1 l2 = [] 496 then l1@l2 497 else raise ERR "check_varstruct" "repeated variable in varstruct" 498 end; 499 500(* check that tm is a <lhs> where: 501 502 <lhs> ::= <var> | <lhs> <varstruct> 503 504 and that no variables are repeated. Return list of variables. 505*) 506 507fun check_lhs tm = 508 if is_var tm then [tm] else 509 if is_const tm 510 then raise ERR "check_lhs" ("attempt to redefine the constant " ^ 511 fst (dest_const tm)) 512 else if not(is_comb tm) 513 then raise ERR "check_lhs" "lhs not of form (--`x = ...`--) or (--`f x = ... `--)" 514 else 515 let val (t1,t2) = dest_comb tm 516 val l1 = check_lhs t1 517 val l2 = check_varstruct t2 518 in 519 if intersect l1 l2 = [] 520 then l1@l2 521 else raise ERR "check_lhs" "var used twice" 522 end; 523 524(* if (--`C ... = (...:ty)`--) then (get_type (--`C ...`--) ty) gives the 525 type of C. 526*) 527 528fun get_type left rightty = 529 if is_var left then rightty 530 else get_type (rator left) (type_of(rand left) --> rightty) 531 handle _ => raise ERR "get_type" "bad lhs"; 532 533(* ---------------------------------------------------------------------*) 534(* RESQ_DEF_EXISTS_RULE `!x1::P1. ... !xn::Pn. *) 535(* C y x1 ... xn z = t[y,x1,...,xn,z]`returns a theorem which is *) 536(* suitable to be used in new_specification *) 537(* If there are free variables in Pi, then Skolem conversion will be *) 538(* done, so the constant C will become C' m where m is free in Pi. *) 539(* ---------------------------------------------------------------------*) 540 541fun RESQ_DEF_EXISTS_RULE tm = 542 let val (gvars,tm') = strip_forall tm 543 val (ress,(lh,rh)) = ((I ## dest_eq) o strip_res_forall) tm' 544 handle _ => raise ERR "RESQ_DEF_EXISTS_RULE" "definition not an equation" 545 val leftvars = check_lhs lh 546 val cty = get_type lh (type_of rh) 547 val rightvars = free_vars rh 548 val resvars = map fst ress 549 val finpred = mk_set (flatten (map (free_vars o snd) ress)) 550 val pConst = hd leftvars 551 val cname = fst(dest_var pConst) 552 in 553 if not(Lexis.allowed_term_constant cname) then 554 raise ERR "RESQ_DEF_EXISTS_RULE" (cname^" is not allowed as a constant name") 555 else if (mem pConst resvars) then 556 raise ERR "RESQ_DEF_EXISTS_RULE" (cname^" is restrict bound") 557 else if not(all (fn x => mem x leftvars) resvars) then 558 raise ERR "RESQ_DEF_EXISTS_RULE" "restrict bound var not in lhs" 559 else if not(set_eq(intersect 560 (union finpred leftvars) rightvars)rightvars) then 561 raise ERR "RESQ_DEF_EXISTS_RULE" "unbound var in rhs" 562 else if mem(hd leftvars)rightvars then 563 raise ERR "RESQ_DEF_EXISTS_RULE" "recursive definitions not allowed" 564 else if not(null(subtract (type_vars_in_term rh) 565 (type_vars_in_term pConst))) then 566 raise ERR "RESQ_DEF_EXISTS_RULE" 567 (dest_vartype(hd(subtract (type_vars_in_term rh) 568 (type_vars_in_term pConst))) ^ 569 "an unbound type variable in definition") 570 else 571 let val gl = list_mk_forall (finpred, 572 mk_exists(pConst, list_mk_res_forall 573 (ress, list_mk_forall 574 (subtract(tl leftvars) resvars, mk_eq(lh,rh))))) 575 val ex = list_mk_abs((tl leftvars), rh) 576 val defthm = prove(gl, 577 REPEAT GEN_TAC THEN EXISTS_TAC ex THEN BETA_TAC 578 THEN REPEAT RESQ_GEN_TAC THEN REPEAT GEN_TAC THEN REFL_TAC) 579 in 580 if is_forall(concl defthm) 581 then CONV_RULE SKOLEM_CONV defthm 582 else defthm 583 end 584 end 585 handle HOL_ERR {message = s,...} => 586 raise ERR "RESQ_DEF_EXISTS_RULE" s; 587 588(* --------------------------------------------------------------------- *) 589(* new_gen_resq_definition flag (name, (--`!x1::P1. ... !xn::Pn. *) 590(* C y x1 ... xn z = t[y,x1,...,xn,z]`--)) *) 591(* This makes a new constant definition via new_specification. *) 592(* The definition is stored in the current theory under the give name. *) 593(* flag specifies the syntactic status of the new constant. It should *) 594(* be either "constant", or "infix" or "binder". *) 595(* --------------------------------------------------------------------- *) 596 597open Parse 598 599fun new_gen_resq_definition flag (name, tm) = let 600 val def_thm = RESQ_DEF_EXISTS_RULE tm 601 val cname = (fst o dest_var o fst o dest_exists o concl) def_thm 602in 603 604 Rsyntax.new_specification {name=name, 605 consts= [{fixity = flag, const_name = cname}], 606 sat_thm = def_thm} 607end; 608 609val new_resq_definition = new_gen_resq_definition NONE; 610 611fun new_infixl_resq_definition (name,tm,fix) = 612 new_gen_resq_definition (SOME (Infixl fix)) (name,tm); 613fun new_infixr_resq_definition (name,tm,fix) = 614 new_gen_resq_definition (SOME (Infixr fix)) (name,tm); 615 616val new_binder_resq_definition = new_gen_resq_definition (SOME Binder); 617 618(* --------------------------------------------------------------------- *) 619(* Some restricted quantifier functions using term quotations *) 620(* --------------------------------------------------------------------- *) 621 622fun Q_RESQ_EXISTS_TAC tm = CONV_TAC RES_EXISTS_CONV ++ Q.EXISTS_TAC tm; 623fun Q_RESQ_HALF_SPEC tm = CONV_RULE RES_FORALL_CONV THENR Q.SPEC tm; 624val Q_RESQ_HALF_SPECL = GEN_RESQ_HALF_SPECL Q.SPEC Q_RESQ_HALF_SPEC; 625fun Q_RESQ_SPEC tm = (Q_RESQ_HALF_SPEC tm THENR UNDISCH) ORELSER Q.SPEC tm; 626val Q_RESQ_SPECL = C (foldl (uncurry Q_RESQ_SPEC)); 627fun Q_RESQ_HALF_ISPEC tm = CONV_RULE RES_FORALL_CONV THENR Q.ISPEC tm; 628val Q_RESQ_HALF_ISPECL = GEN_RESQ_HALF_SPECL Q.ISPEC Q_RESQ_HALF_ISPEC; 629fun Q_RESQ_ISPEC tm = (Q_RESQ_HALF_ISPEC tm THENR UNDISCH) ORELSER Q.ISPEC tm; 630val Q_RESQ_ISPECL = C (foldl (uncurry Q_RESQ_ISPEC)); 631 632val _ = Parse.temp_set_grammars ambient_grammars 633 634end; 635end; (* res_quanLib *) 636 637(* Local Variables: *) 638(* fill-column: 78 *) 639(* indent-tabs-mode: nil *) 640(* End: *) 641