1structure PairRules :> PairRules = 2struct 3 4open HolKernel Parse boolLib pairSyntax; 5 6val ERR = mk_HOL_ERR "PairRules" 7 8 9(* structure Pair_basic :> Pair_basic = struct *) 10 11fun MK_PAIR (t1,t2) = 12 let val y1 = type_of (rand (concl t1)) 13 val y2 = type_of (rand (concl t2)) 14 val icomma = inst [alpha |-> y1, beta |-> y2] comma_tm 15 in 16 MK_COMB (AP_TERM icomma t1,t2) 17 end; 18 19(* ------------------------------------------------------------------------- *) 20(* Paired abstraction *) 21(* *) 22(* A |- t1 = t2 *) 23(* ----------------------- (provided p is not free in A) *) 24(* A |- (\p.t1) = (\p.t2) *) 25(* ------------------------------------------------------------------------- *) 26 27fun PABS p th = 28 if is_var p then ABS p th 29 else (* is_pair *) 30 let val (p1,p2) = dest_pair p 31 val t1 = PABS p2 th 32 val t2 = PABS p1 t1 33 val pty = type_of p 34 val p1ty = type_of p1 35 val p2ty = type_of p2 36 val cty = type_of (rand (concl th)) 37 in 38 AP_TERM 39 (inst [alpha |-> p1ty, beta |-> p2ty,gamma |-> cty] uncurry_tm) t2 40 end 41 handle HOL_ERR _ => failwith "PABS"; 42 43(* ----------------------------------------------------------------------- *) 44(* PABS_CONV conv "\p. t[p]" applies conv to t[p] *) 45(* ----------------------------------------------------------------------- *) 46 47fun PABS_CONV conv tm = 48 let val (Bvar,Body) = with_exn dest_pabs tm (ERR "PABS_CONV" "") 49 val bodyth = conv Body 50 in 51 PABS Bvar bodyth handle HOL_ERR _ => failwith "PABS_CONV" 52 end; 53 54(* ----------------------------------------------------------------------- *) 55(* PSUB_CONV conv tm: applies conv to the subterms of tm. *) 56(* ----------------------------------------------------------------------- *) 57 58fun PSUB_CONV conv tm = 59 if is_pabs tm then PABS_CONV conv tm else 60 if is_comb tm 61 then let val (Rator,Rand) = dest_comb tm 62 in MK_COMB (conv Rator, conv Rand) 63 end 64 else ALL_CONV tm; 65 66(* ------------------------------------------------------------------------- *) 67(* CURRY_CONV "(\(x,y).f)(a,b)" = (|- ((\(x,y).f)(a,b)) = ((\x y. f) a b)) *) 68(* ------------------------------------------------------------------------- *) 69 70val UNCURRY_DEF = pairTheory.UNCURRY_DEF; 71val CURRY_DEF = pairTheory.CURRY_DEF; 72val PAIR = pairTheory.PAIR; 73 74val CURRY_CONV = 75 let val gfty = alpha --> beta --> gamma 76 and gxty = alpha 77 and gyty = beta 78 and gpty = mk_prod(alpha,beta) 79 and grange = gamma 80 val gf = genvar gfty 81 and gx = genvar gxty 82 and gy = genvar gyty 83 and gp = genvar gpty 84 val uncurry_thm = SPECL [gf,gx,gy] UNCURRY_DEF 85 and pair_thm = SYM (SPEC gp PAIR) 86 val (fgp,sgp) = dest_pair (rand (concl pair_thm)) 87 val pair_uncurry_thm = 88 (CONV_RULE 89 ((RATOR_CONV o RAND_CONV o RAND_CONV) (K (SYM pair_thm)))) 90 (SPECL [gf,fgp,sgp]UNCURRY_DEF) 91 in 92 fn tm => 93 let val (Rator,p) = dest_comb tm 94 val f = rand Rator 95 val fty = type_of f 96 val rnge = hd(tl(snd(dest_type(hd(tl(snd(dest_type fty))))))) 97 val gfinst = mk_var(fst(dest_var gf),fty) 98 in 99 if is_pair p then 100 let val (x,y) = dest_pair p 101 val xty = type_of x 102 and yty = type_of y 103 val gxinst = mk_var(fst(dest_var gx),xty) 104 and gyinst = mk_var(fst(dest_var gy),yty) 105 in 106 INST_TY_TERM 107 ([gfinst |-> f, gxinst |-> x, gyinst |-> y], 108 [gxty |-> xty, gyty |-> yty, grange |-> rnge]) 109 uncurry_thm 110 end 111 else 112 let val pty = type_of p 113 val gpinst = mk_var(fst (dest_var gp),pty) 114 val (xty,yty) = dest_prod pty 115 in 116 (INST_TY_TERM 117 ([gfinst |-> f, gpinst |-> p], 118 [gxty |-> xty, gyty |-> yty, grange |-> rnge]) 119 pair_uncurry_thm) 120 end 121 end 122 end 123handle HOL_ERR _ => failwith "CURRY_CONV" ; 124 125(* ------------------------------------------------------------------------- *) 126(* UNCURRY_CONV "(\x y. f) a b" = (|- ((\x y. f) a b) = ((\(x,y).f)(x,y))) *) 127(* ------------------------------------------------------------------------- *) 128 129val UNCURRY_CONV = 130 let val gfty = alpha --> beta --> gamma 131 and gxty = alpha 132 and gyty = beta 133 and grange = gamma 134 val gf = genvar gfty 135 and gx = genvar gxty 136 and gy = genvar gyty 137 val uncurry_thm = SYM (SPECL [gf,gx,gy] UNCURRY_DEF) 138 in 139 fn tm => 140 let val (Rator,y) = dest_comb tm 141 val (f,x) = dest_comb Rator 142 val fty = type_of f 143 val rnge = hd(tl(snd(dest_type(hd(tl(snd(dest_type fty))))))) 144 val gfinst = mk_var(fst(dest_var gf), fty) 145 val xty = type_of x 146 and yty = type_of y 147 val gxinst = mk_var(fst(dest_var gx), xty) 148 and gyinst = mk_var(fst(dest_var gy), yty) 149 in 150 INST_TY_TERM 151 ([gfinst |-> f,gxinst |-> x, gyinst |-> y], 152 [gxty |-> xty,gyty |-> yty, grange |-> rnge]) 153 uncurry_thm 154 end 155 end 156handle HOL_ERR _ => failwith "UNCURRY_CONV" ; 157 158(* ------------------------------------------------------------------------- *) 159(* PBETA_CONV "(\p1.t)p2" = (|- (\p1.t)p2 = t[p2/p1]) *) 160(* ------------------------------------------------------------------------- *) 161 162val PBETA_CONV = 163 (* pairlike p x: takes a pair structure p and a term x. *) 164 (* It returns the struture ((change, thm), assoclist) *) 165 (* where change is true if x does not have the same structure as p. *) 166 (* if changes is true then thm is a theorem of the form (|-x'=x) *) 167 (* where x' is of the same structure as p, created by making terms *) 168 (* into pairs of the form (FST t,SND t). *) 169 (* assoc thm list is a list of theorms for all the subpairs of x that *) 170 (* required changing along the correspoing subpair from p. *) 171 let val pairlike = 172 let fun int_pairlike p x = 173 if is_pair p 174 then let val (p1,p2) = dest_pair p 175 in 176 if is_pair x 177 then let val (x1,x2) = dest_pair x 178 val ((cl,lt),pl) = int_pairlike p1 x1 179 val ((cr,rt),pr) = int_pairlike p2 x2 180 val (c,t) = if cl andalso cr then (true,MK_PAIR(lt,rt)) 181 else if cl 182 then let val ty1 = type_of x1 183 and ty2 = type_of x2 184 in (true, 185 AP_THM (AP_TERM 186 (inst[alpha|->ty1, beta|->ty2] comma_tm) 187 lt) x2) 188 end 189 else if cr 190 then let val ty1 = type_of x1 191 val ty2 = type_of x2 192 in (true, 193 AP_TERM (mk_comb (inst 194 [alpha|->ty1,beta|->ty2]comma_tm,x1)) 195 rt) 196 end 197 else (false,TRUTH) 198 in if c then ((true,t),((p,t)::(pl@pr))) 199 else ((false,TRUTH),[]) 200 end 201 else 202 let val th1 = ISPEC x PAIR 203 val x' = rand (rator (concl th1)) 204 val (x'1,x'2) = dest_pair x' 205 val ((cl,lt),pl) = (int_pairlike p1 x'1) 206 val ((cr,rt),pr) = (int_pairlike p2 x'2) 207 val t = if cl andalso cr then TRANS (MK_PAIR(lt,rt)) th1 208 else if cl 209 then let val ty1 = type_of x'1 210 and ty2 = type_of x'2 211 in TRANS(AP_THM (AP_TERM 212 (inst[alpha|->ty1,beta|->ty2]comma_tm) 213 lt) x'2) th1 214 end 215 else if cr 216 then let val ty1 = type_of x'1 217 val ty2 = type_of x'2 218 in 219 TRANS(AP_TERM (mk_comb 220 (inst[alpha|->ty1,beta|->ty2]comma_tm, 221 x'1)) rt) 222 th1 223 end 224 else th1 225 in 226 ((true,t),((p,t)::(pl@pr))) 227 end 228 end (* let val (p1,p2) = ... *) 229 else 230 ((false,TRUTH),[]) 231 in 232 int_pairlike 233 end 234 (* find_CONV mask assl: *) 235 (* mask is the body of the original abstraction, containing *) 236 (* instances of the bound pair p and it subcomponents. *) 237 (* assl is the theorem list generated by pairlike that will allow *) 238 (* us to find these pairs and map them back into nonpairs where *) 239 (* possible. *) 240 fun find_CONV mask assl = 241 let fun search m pthl = 242 (true, (K (op_assoc aconv m assl))) 243 handle HOL_ERR _ 244 => if is_comb m then 245 let val (f,b) = dest_comb m 246 val (ff,fc) = search f pthl 247 and (bf,bc) = search b pthl 248 in 249 (if (ff andalso bf) then 250 (true, (RATOR_CONV fc) THENC (RAND_CONV bc)) 251 else if ff then 252 (true, (RATOR_CONV fc)) 253 else if bf then 254 (true, (RAND_CONV bc)) 255 else 256 (false, ALL_CONV)) 257 end 258 else if is_abs m then 259 let val (v,b) = dest_abs m 260 val pthl' = filter(fn (p,_) => not (free_in v p)) pthl 261 in 262 if null pthl' then 263 (false, ALL_CONV) 264 else 265 let val (bf,bc) = search b pthl' 266 in 267 if bf then 268 (true, ABS_CONV bc) 269 else 270 (false, ALL_CONV) 271 end 272 end 273 else 274 (false, ALL_CONV) 275 in 276 snd (search mask assl) 277 end 278 fun INT_PBETA_CONV tm = 279 let val (Rator,a) = dest_comb tm 280 val (p,b) = dest_pabs Rator 281 in 282 if is_var p then BETA_CONV tm 283 else (* is_pair p *) 284 (CURRY_CONV THENC 285 (RATOR_CONV INT_PBETA_CONV) THENC 286 INT_PBETA_CONV 287 ) tm 288 end 289 in 290 fn tm => 291 let val (Rator,a) = dest_comb tm 292 val (p,b) = dest_pabs Rator 293 val ((dif,difthm),assl) = pairlike p a 294 in 295 if dif 296 then (RAND_CONV (K (SYM difthm)) 297 THENC INT_PBETA_CONV THENC find_CONV b assl) tm 298 else INT_PBETA_CONV tm 299 end 300 end; 301 302val PBETA_RULE = CONV_RULE (DEPTH_CONV PBETA_CONV) 303and PBETA_TAC = CONV_TAC (DEPTH_CONV PBETA_CONV) ; 304 305fun RIGHT_PBETA th = 306 TRANS th (PBETA_CONV (rhs (concl th))) 307 handle HOL_ERR _ => failwith "RIGHT_PBETA"; 308 309fun LIST_PBETA_CONV tm = 310 let val (f,a) = dest_comb tm 311 in 312 RIGHT_PBETA (AP_THM (LIST_PBETA_CONV f) a) 313 end 314handle HOL_ERR _ => REFL tm; 315 316fun RIGHT_LIST_PBETA th = 317 TRANS th (LIST_PBETA_CONV (rhs (concl th))); 318 319fun LEFT_PBETA th = 320 CONV_RULE (RATOR_CONV (RAND_CONV PBETA_CONV)) th 321 handle HOL_ERR _ => failwith "LEFT_PBETA"; 322 323fun LEFT_LIST_PBETA th = 324 CONV_RULE (RATOR_CONV (RAND_CONV LIST_PBETA_CONV)) th 325handle HOL_ERR _ => failwith "LEFT_LIST_PBETA";; 326 327(* ------------------------------------------------------------------------- *) 328(* UNPBETA_CONV "p" "t" = (|- t = (\p.t)p) *) 329(* ------------------------------------------------------------------------- *) 330 331fun UNPBETA_CONV v tm = 332 SYM (PBETA_CONV (mk_comb(mk_pabs(v,tm),v))) 333 handle HOL_ERR _ => failwith "UNPBETA_CONV"; 334 335(* ------------------------------------------------------------------------- *) 336(* PETA_CONV "\ p. f p" = (|- (\p. f p) = t) *) 337(* ------------------------------------------------------------------------- *) 338 339fun occs_in p t = (* should use set operations for better speed *) 340 if is_vstruct p then 341 let 342 fun set_diff s v = HOLset.delete(s,v) handle HOLset.NotFound => s 343 fun check V tm = 344 if is_const tm then false else 345 if is_var tm then HOLset.member(V,tm) else 346 if is_comb tm then check V (rand tm) orelse check V (rator tm) else 347 if is_abs tm then check (set_diff V (bvar tm)) (body tm) 348 else raise ERR "occs_in" "malformed term" 349 in 350 check (FVL [p] empty_tmset) t 351 end 352 else raise ERR "occs_in" "varstruct expected in first argument"; 353 354fun PETA_CONV tm = 355 let val (p,fp) = dest_pabs tm 356 val (f,p') = dest_comb fp 357 val x = genvar (type_of p) 358 in 359 if aconv p p' andalso not (occs_in p f) 360 then EXT (GEN x (PBETA_CONV (mk_comb(tm,x)))) 361 else failwith "" 362 end 363handle HOL_ERR _ => failwith "PETA_CONV"; 364 365(* ------------------------------------------------------------------------- *) 366(* PALPHA_CONV p2 "\p1. t" = (|- (\p1. t) = (\p2. t[p2/p1])) *) 367(* ------------------------------------------------------------------------- *) 368 369fun PALPHA_CONV np tm = 370 let val (opr,_) = dest_pabs tm 371 in if is_var np 372 then if is_var opr then ALPHA_CONV np tm 373 else (* is_pair opr *) 374 let val np' = genvar (type_of np) 375 val t1 = PBETA_CONV (mk_comb(tm, np')) 376 val t2 = ABS np' t1 377 val t3 = CONV_RULE (RATOR_CONV (RAND_CONV ETA_CONV)) t2 378 in 379 CONV_RULE (RAND_CONV (ALPHA_CONV np)) t3 380 end 381 else (* is_pair np *) 382 if is_var opr 383 then let val np' = genvarstruct (type_of np) 384 val t1 = PBETA_CONV (mk_comb(tm, np')) 385 val t2 = PABS np' t1 386 val th3 = CONV_RULE (RATOR_CONV (RAND_CONV PETA_CONV)) t2 387 in 388 CONV_RULE (RAND_CONV (PALPHA_CONV np)) th3 389 end 390 else (* is_pair opr *) 391 let val (np1,np2) = dest_pair np 392 in CONV_RULE (RAND_CONV (RAND_CONV (PABS_CONV (PALPHA_CONV np2)))) 393 ((RAND_CONV (PALPHA_CONV np1)) tm) 394 end 395 end 396 handle HOL_ERR _ => failwith "PALPHA_CONV" ; 397 398(* ------------------------------------------------------------------------- *) 399(* For any binder B: *) 400(* GEN_PALPHA_CONV p2 "B p1. t" = (|- (B p1. t) = (B p2. t[p2/p1])) *) 401(* ------------------------------------------------------------------------- *) 402 403fun GEN_PALPHA_CONV p tm = 404 if is_pabs tm then 405 PALPHA_CONV p tm 406 else 407 AP_TERM (rator tm) (PALPHA_CONV p (rand tm)) 408 handle HOL_ERR _ => failwith "GEN_PALPHA_CONV"; 409 410(* ------------------------------------------------------------------------- *) 411(* Iff t1 and t2 are alpha convertable then *) 412(* PALPHA t1 t2 = (|- t1 = t2) *) 413(* *) 414(* Note the PALPHA considers "(\x.x)" and "\(a,b).(a,b)" to be *) 415(* alpha convertable where ALPHA does not. *) 416(* ------------------------------------------------------------------------- *) 417 418fun PALPHA t1 t2 = 419 if t1 = t2 then REFL t1 else 420 if (is_pabs t1) andalso (is_pabs t2) 421 then let val (p1,b1) = dest_pabs t1 422 val (p2,b2) = dest_pabs t2 423 in if is_var p1 424 then let val th1 = PALPHA_CONV p1 t2 425 val b2' = pbody (rand (concl th1)) 426 in 427 TRANS(PABS p1 (PALPHA b1 b2'))(SYM th1) 428 end 429 else let val th1 = PALPHA_CONV p2 t1 430 val b1' = pbody (rand (concl th1)) 431 in 432 TRANS th1 (PABS p2 (PALPHA b2 b1')) 433 end 434 end 435 else if (is_comb t1) andalso(is_comb t2) 436 then let val (t1f,t1a) = dest_comb t1 437 val (t2f,t2a) = dest_comb t2 438 val thf = PALPHA t1f t2f 439 val tha = PALPHA t1a t2a 440 in 441 TRANS (AP_THM thf t1a) (AP_TERM t2f tha) 442 end 443 else failwith "PALPHA"; 444 445val paconv = curry (can (uncurry PALPHA)); 446 447(* ------------------------------------------------------------------------- *) 448(* PAIR_CONV : conv -> conv *) 449(* *) 450(* If the argument of the resulting conversion is a pair, this conversion *) 451(* recursively applies itself to both sides of the pair. *) 452(* Otherwise the basic conversion is applied to the argument. *) 453(* ------------------------------------------------------------------------- *) 454 455fun PAIR_CONV c t = 456 if is_pair t 457 then let val (fst,snd) = dest_pair t 458 in MK_PAIR(PAIR_CONV c fst,PAIR_CONV c snd) 459 end 460 else c t; 461 462(* end Pair_basic *) 463 464(* structure Pair_conv :> Pair_conv = struct *) 465 466 467val RIGHT_EXISTS_IMP_THM = boolTheory.RIGHT_EXISTS_IMP_THM; 468val LEFT_EXISTS_IMP_THM = boolTheory.LEFT_EXISTS_IMP_THM; 469val BOTH_EXISTS_IMP_THM = boolTheory.BOTH_EXISTS_IMP_THM; 470val RIGHT_FORALL_IMP_THM = boolTheory.RIGHT_FORALL_IMP_THM; 471val LEFT_FORALL_IMP_THM = boolTheory.LEFT_FORALL_IMP_THM; 472val BOTH_FORALL_IMP_THM = boolTheory.BOTH_FORALL_IMP_THM; 473val RIGHT_FORALL_OR_THM = boolTheory.RIGHT_FORALL_OR_THM; 474val LEFT_FORALL_OR_THM = boolTheory.LEFT_FORALL_OR_THM; 475val BOTH_FORALL_OR_THM = boolTheory.BOTH_FORALL_OR_THM; 476val RIGHT_EXISTS_AND_THM = boolTheory.RIGHT_EXISTS_AND_THM; 477val LEFT_EXISTS_AND_THM = boolTheory.LEFT_EXISTS_AND_THM; 478val BOTH_EXISTS_AND_THM = boolTheory.BOTH_EXISTS_AND_THM; 479val RIGHT_OR_EXISTS_THM = boolTheory.RIGHT_OR_EXISTS_THM; 480val LEFT_OR_EXISTS_THM = boolTheory.LEFT_OR_EXISTS_THM; 481val RIGHT_AND_FORALL_THM = boolTheory.RIGHT_AND_FORALL_THM; 482val LEFT_AND_FORALL_THM = boolTheory.LEFT_AND_FORALL_THM; 483val EXISTS_OR_THM = boolTheory.EXISTS_OR_THM; 484val FORALL_AND_THM = boolTheory.FORALL_AND_THM; 485val NOT_EXISTS_THM = boolTheory.NOT_EXISTS_THM; 486val NOT_FORALL_THM = boolTheory.NOT_FORALL_THM; 487 488 489(* ------------------------------------------------------------------------- *) 490(* NOT_PFORALL_CONV "~!p.t" = |- (~!p.t) = (?p.~t) *) 491(* ------------------------------------------------------------------------- *) 492 493fun NOT_PFORALL_CONV tm = 494 let val (p,_) = dest_pforall (dest_neg tm) 495 val f = rand (rand tm) 496 val th = ISPEC f NOT_FORALL_THM 497 val th1 = CONV_RULE (RATOR_CONV (RAND_CONV (RAND_CONV (RAND_CONV 498 ETA_CONV)))) th 499 val th2 = CONV_RULE (RAND_CONV (RAND_CONV (PALPHA_CONV p))) th1 500 in 501 CONV_RULE 502 (RAND_CONV (RAND_CONV (PABS_CONV (RAND_CONV PBETA_CONV)))) 503 th2 504 end 505handle HOL_ERR _ => raise ERR "NOT_PFORALL_CONV" 506 "argument must have the form `~!p.tm`"; 507 508(* ------------------------------------------------------------------------- *) 509(* NOT_PEXISTS_CONV "~?p.t" = |- (~?p.t) = (!p.~t) *) 510(* ------------------------------------------------------------------------- *) 511 512fun NOT_PEXISTS_CONV tm = 513 let val (p,_) = dest_pexists (dest_neg tm) 514 val f = rand (rand tm) 515 val th = ISPEC f NOT_EXISTS_THM 516 val th1 = CONV_RULE (RATOR_CONV (RAND_CONV (RAND_CONV (RAND_CONV 517 ETA_CONV)))) th 518 val th2 = CONV_RULE (RAND_CONV (RAND_CONV (PALPHA_CONV p))) th1 519 in 520 CONV_RULE 521 (RAND_CONV (RAND_CONV (PABS_CONV (RAND_CONV PBETA_CONV)))) 522 th2 523 end 524handle HOL_ERR _ => raise ERR "NOT_PEXISTS_CONV" 525 "argument must have the form `~!p.tm`"; 526 527 528(* ------------------------------------------------------------------------- *) 529(* PEXISTS_NOT_CONV "?p.~t" = |- (?p.~t) = (~!p.t) *) 530(* ------------------------------------------------------------------------- *) 531 532fun PEXISTS_NOT_CONV tm = 533 let val (Bvar,Body) = dest_pexists tm 534 val xtm = mk_pforall (Bvar,dest_neg Body) 535 in 536 SYM (NOT_PFORALL_CONV (mk_neg xtm)) 537 end 538handle HOL_ERR _ => raise ERR "PEXISTS_NOT_CONV" 539 "argument must have the form `?x.~tm`"; 540 541(* ------------------------------------------------------------------------- *) 542(* PFORALL_NOT_CONV "!p.~t" = |- (!p.~t) = (~?p.t) *) 543(* ------------------------------------------------------------------------- *) 544 545fun PFORALL_NOT_CONV tm = 546 let val (Bvar,Body) = dest_pforall tm 547 val xtm = mk_pexists (Bvar,dest_neg Body) 548 in 549 SYM (NOT_PEXISTS_CONV (mk_neg xtm)) 550 end 551handle HOL_ERR _ => raise ERR "PFORALL_NOT_CONV" 552 "argument must have the form `!x.~tm`"; 553 554 555(* ------------------------------------------------------------------------- *) 556(* PFORALL_AND_CONV "!x. P /\ Q" = |- (!x. P /\ Q) = (!x.P) /\ (!x.Q) *) 557(* ------------------------------------------------------------------------- *) 558 559fun PFORALL_AND_CONV tm = 560 let val (x,Body) = dest_pforall tm 561 val (P,Q) = dest_conj Body 562 val f = mk_pabs(x,P) 563 val g = mk_pabs(x,Q) 564 val th = ISPECL [f,g] FORALL_AND_THM 565 val th1 = 566 CONV_RULE 567 (RATOR_CONV (RAND_CONV (RAND_CONV 568 (PALPHA_CONV x)))) 569 th 570 val th2 = 571 CONV_RULE 572 (RATOR_CONV (RAND_CONV (RAND_CONV (PABS_CONV 573 (RATOR_CONV (RAND_CONV PBETA_CONV)))))) 574 th1 575 val th3 = 576 CONV_RULE 577 (RATOR_CONV (RAND_CONV (RAND_CONV (PABS_CONV 578 (RAND_CONV PBETA_CONV))))) 579 th2 580 val th4 = 581 CONV_RULE 582 (RAND_CONV (RATOR_CONV (RAND_CONV (RAND_CONV ETA_CONV)))) 583 th3 584 in 585 (CONV_RULE (RAND_CONV (RAND_CONV (RAND_CONV ETA_CONV)))) th4 586 end 587handle HOL_ERR _ => raise ERR "PFORALL_AND_CONV" 588 "argument must have the form `!p. P /\\ Q`"; 589 590 591(* ------------------------------------------------------------------------- *) 592(* PEXISTS_OR_CONV "?x. P \/ Q" = |- (?x. P \/ Q) = (?x.P) \/ (?x.Q) *) 593(* ------------------------------------------------------------------------- *) 594 595fun PEXISTS_OR_CONV tm = 596 let val (x,Body) = dest_pexists tm 597 val (P,Q) = dest_disj Body 598 val f = mk_pabs(x,P) 599 val g = mk_pabs(x,Q) 600 val th = ISPECL [f,g] EXISTS_OR_THM 601 val th1 = (CONV_RULE (RATOR_CONV (RAND_CONV (RAND_CONV 602 (PALPHA_CONV x))))) th 603 val th2 = (CONV_RULE (RATOR_CONV (RAND_CONV (RAND_CONV (PABS_CONV 604 (RATOR_CONV (RAND_CONV PBETA_CONV))))))) th1 605 val th3 = (CONV_RULE (RATOR_CONV (RAND_CONV (RAND_CONV (PABS_CONV 606 (RAND_CONV PBETA_CONV)))))) th2 607 val th4 = (CONV_RULE (RAND_CONV (RATOR_CONV (RAND_CONV (RAND_CONV 608 ETA_CONV))))) th3 609 in 610 (CONV_RULE (RAND_CONV (RAND_CONV (RAND_CONV ETA_CONV)))) th4 611 end 612handle HOL_ERR _ => raise ERR"PEXISTS_OR_CONV" 613 "argument must have the form `?p. P \\/ Q`"; 614 615 616(* ------------------------------------------------------------------------- *) 617(* AND_PFORALL_CONV "(!x. P) /\ (!x. Q)" = |- (!x.P)/\(!x.Q) = (!x. P /\ Q) *) 618(* ------------------------------------------------------------------------- *) 619 620fun AND_PFORALL_CONV tm = 621 let val (conj1,conj2) = dest_conj tm 622 val (x,P) = dest_pforall conj1 623 and (y,Q) = dest_pforall conj2 624 in 625 if (not (x=y)) then failwith"" 626 else 627 let val f = mk_pabs (x,P) 628 val g = mk_pabs(x,Q) 629 val th = SYM (ISPECL [f,g] FORALL_AND_THM) 630 val th1 = (CONV_RULE (RATOR_CONV (RAND_CONV (RATOR_CONV 631 (RAND_CONV (RAND_CONV ETA_CONV)))))) th 632 val th2 = (CONV_RULE (RATOR_CONV (RAND_CONV (RAND_CONV 633 (RAND_CONV ETA_CONV))))) th1 634 val th3 = (CONV_RULE(RAND_CONV(RAND_CONV(PALPHA_CONV x)))) th2 635 val th4 = (CONV_RULE (RAND_CONV (RAND_CONV (PABS_CONV 636 (RATOR_CONV (RAND_CONV PBETA_CONV)))))) th3 637 in 638 (CONV_RULE (RAND_CONV(RAND_CONV(PABS_CONV(RAND_CONV 639 PBETA_CONV))))) th4 640 end 641 end 642handle HOL_ERR _ => raise ERR "AND_PFORALL_CONV" 643 "arguments must have form `(!p.P)/\\(!p.Q)`"; 644 645 646 647(* ------------------------------------------------------------------------- *) 648(* LEFT_AND_PFORALL_CONV "(!x.P) /\ Q" = *) 649(* |- (!x.P) /\ Q = (!x'. P[x'/x] /\ Q) *) 650(* ------------------------------------------------------------------------- *) 651 652fun LEFT_AND_PFORALL_CONV tm = 653 let val (conj1,Q) = dest_conj tm 654 val (x,P) = dest_pforall conj1 655 val f = mk_pabs(x,P) 656 val th = ISPECL [Q,f] LEFT_AND_FORALL_THM 657 val th1 = (CONV_RULE (RATOR_CONV (RAND_CONV (RATOR_CONV (RAND_CONV 658 (RAND_CONV ETA_CONV)))))) th 659 val th2 = (CONV_RULE (RAND_CONV (RAND_CONV (PALPHA_CONV x)))) th1 660 in 661 (CONV_RULE (RAND_CONV (RAND_CONV (PABS_CONV (RATOR_CONV (RAND_CONV 662 PBETA_CONV)))))) th2 663 end 664handle HOL_ERR _ => raise ERR "LEFT_AND_PFORALL_CONV" 665 "expecting `(!p.P) /\\ Q`"; 666 667(* ------------------------------------------------------------------------- *) 668(* RIGHT_AND_PFORALL_CONV "P /\ (!x.Q)" = *) 669(* |- P /\ (!x.Q) = (!x'. P /\ Q[x'/x]) *) 670(* ------------------------------------------------------------------------- *) 671 672fun RIGHT_AND_PFORALL_CONV tm = 673 let val (P,conj2) = dest_conj tm 674 val (x,Q) = dest_pforall conj2 675 val g = mk_pabs(x,Q) 676 val th = (ISPECL [P,g] RIGHT_AND_FORALL_THM) 677 val th1 = (CONV_RULE (RATOR_CONV (RAND_CONV (RAND_CONV 678 (RAND_CONV ETA_CONV))))) th 679 val th2 = (CONV_RULE (RAND_CONV (RAND_CONV (PALPHA_CONV x)))) th1 680 in 681 CONV_RULE 682 (RAND_CONV (RAND_CONV (PABS_CONV (RAND_CONV PBETA_CONV)))) 683 th2 684 end 685handle HOL_ERR _ => raise ERR "RIGHT_AND_PFORALL_CONV" 686 "expecting `P /\\ (!p.Q)`"; 687 688(* ------------------------------------------------------------------------- *) 689(* OR_PEXISTS_CONV "(?x. P) \/ (?x. Q)" = |- (?x.P) \/ (?x.Q) = (?x. P \/ Q) *) 690(* ------------------------------------------------------------------------- *) 691 692fun OR_PEXISTS_CONV tm = 693 let val (disj1,disj2) = dest_disj tm 694 val (x,P) = dest_pexists disj1 695 and (y,Q) = dest_pexists disj2 696 in 697 if (not (x=y)) then failwith"" 698 else 699 let val f = mk_pabs(x,P) 700 val g = mk_pabs(x,Q) 701 val th = SYM (ISPECL [f,g] EXISTS_OR_THM) 702 val th1 = (CONV_RULE (RATOR_CONV (RAND_CONV (RATOR_CONV 703 (RAND_CONV (RAND_CONV ETA_CONV)))))) th 704 val th2 = (CONV_RULE (RATOR_CONV (RAND_CONV (RAND_CONV 705 (RAND_CONV ETA_CONV))))) th1 706 val th3 = (CONV_RULE(RAND_CONV(RAND_CONV(PALPHA_CONV x)))) th2 707 val th4 = (CONV_RULE (RAND_CONV (RAND_CONV (PABS_CONV 708 (RATOR_CONV (RAND_CONV PBETA_CONV)))))) th3 709 in 710 (CONV_RULE (RAND_CONV (RAND_CONV (PABS_CONV(RAND_CONV 711 PBETA_CONV))))) th4 712 end 713 end 714handle HOL_ERR _ => raise ERR "OR_PEXISTS_CONV" 715 "arguments must have form `(!p.P) \\/ (!p.Q)`"; 716 717 718 719(* ------------------------------------------------------------------------- *) 720(* LEFT_OR_PEXISTS_CONV ���(?x.P) \/ Q��� = *) 721(* |- (?x.P) \/ Q = (?x'. P[x'/x] \/ Q) *) 722(* ------------------------------------------------------------------------- *) 723 724fun LEFT_OR_PEXISTS_CONV tm = 725 let val (disj1,Q) = dest_disj tm 726 val (x,P) = dest_pexists disj1 727 val f = mk_pabs(x,P) 728 val th = ISPECL [Q,f] LEFT_OR_EXISTS_THM 729 val th1 = (CONV_RULE (RATOR_CONV (RAND_CONV (RATOR_CONV (RAND_CONV 730 (RAND_CONV ETA_CONV)))))) th 731 val th2 = (CONV_RULE (RAND_CONV (RAND_CONV (PALPHA_CONV x)))) th1 732 in 733 CONV_RULE 734 (RAND_CONV (RAND_CONV (PABS_CONV (RATOR_CONV (RAND_CONV 735 PBETA_CONV))))) 736 th2 737 end 738handle HOL_ERR _ => raise ERR "LEFT_OR_PEXISTS_CONV" 739 "expecting `(?p.P) \\/ Q`"; 740 741(* ------------------------------------------------------------------------- *) 742(* RIGHT_OR_PEXISTS_CONV ���P \/ (?x.Q)��� = *) 743(* |- P \/ (?x.Q) = (?x'. P \/ Q[x'/x]) *) 744(* ------------------------------------------------------------------------- *) 745 746fun RIGHT_OR_PEXISTS_CONV tm = 747 let val (P,disj2) = dest_disj tm 748 val (x,Q) = dest_pexists disj2 749 val g = mk_pabs(x,Q) 750 val th = (ISPECL [P, g] RIGHT_OR_EXISTS_THM) 751 val th1 = (CONV_RULE (RATOR_CONV (RAND_CONV (RAND_CONV (RAND_CONV 752 ETA_CONV))))) th 753 val th2 = (CONV_RULE (RAND_CONV (RAND_CONV (PALPHA_CONV x)))) th1 754 in 755 CONV_RULE 756 (RAND_CONV (RAND_CONV (PABS_CONV (RAND_CONV PBETA_CONV)))) 757 th2 758 end 759handle HOL_ERR _ => raise ERR "RIGHT_OR_PEXISTS_CONV" 760 "expecting `P \\/ (?p.Q)`"; 761 762 763 764(* ------------------------------------------------------------------------- *) 765(* PEXISTS_AND_CONV : move existential quantifier into conjunction. *) 766(* *) 767(* A call to PEXISTS_AND_CONV "?x. P /\ Q" returns: *) 768(* *) 769(* |- (?x. P /\ Q) = (?x.P) /\ Q [x not free in Q] *) 770(* |- (?x. P /\ Q) = P /\ (?x.Q) [x not free in P] *) 771(* |- (?x. P /\ Q) = (?x.P) /\ (?x.Q) [x not free in P /\ Q] *) 772(* ------------------------------------------------------------------------- *) 773 774fun PEXISTS_AND_CONV tm = 775 let val (x,Body) = dest_pexists tm 776 handle HOL_ERR _ => failwith "expecting `?x. P /\\ Q`" 777 val (P,Q) = dest_conj Body 778 handle HOL_ERR _ => failwith "expecting `?x. P /\\ Q`" 779 val oP = occs_in x P and oQ = occs_in x Q 780 in 781 if (oP andalso oQ) then 782 failwith "bound pair occurs in both conjuncts" 783 else if ((not oP) andalso (not oQ)) then 784 let val th1 = INST_TYPE[alpha |-> type_of x ] BOTH_EXISTS_AND_THM 785 val th2 = SPECL [P,Q] th1 786 val th3 = 787 CONV_RULE 788 (RATOR_CONV (RAND_CONV (RAND_CONV (PALPHA_CONV x)))) 789 th2 790 val th4 = 791 CONV_RULE 792 (RAND_CONV (RATOR_CONV (RAND_CONV (RAND_CONV 793 (PALPHA_CONV x))))) 794 th3 795 val th5 = 796 CONV_RULE 797 (RAND_CONV (RAND_CONV (RAND_CONV (PALPHA_CONV x))))th4 798 in 799 th5 800 end 801 else if oP then (* not free in Q *) 802 let val f = mk_pabs(x,P) 803 val th1 = ISPECL [Q,f] LEFT_EXISTS_AND_THM 804 val th2 = CONV_RULE 805 (RATOR_CONV (RAND_CONV (RAND_CONV (PALPHA_CONV x)))) 806 th1 807 val th3 = CONV_RULE 808 (RATOR_CONV (RAND_CONV (RAND_CONV 809 (PABS_CONV (RATOR_CONV (RAND_CONV PBETA_CONV)))))) 810 th2 811 val th4 = 812 CONV_RULE 813 (RAND_CONV 814 (RATOR_CONV (RAND_CONV (RAND_CONV ETA_CONV)))) 815 th3 816 in 817 th4 818 end 819 else (* not free in P*) 820 let val g = mk_pabs(x,Q) 821 val th1 = ISPECL [P,g] RIGHT_EXISTS_AND_THM 822 val th2 = 823 CONV_RULE 824 (RATOR_CONV (RAND_CONV (RAND_CONV (PALPHA_CONV x)))) 825 th1 826 val th3 = 827 CONV_RULE 828 (RATOR_CONV (RAND_CONV (RAND_CONV 829 (PABS_CONV (RAND_CONV PBETA_CONV))))) 830 th2 831 val th4 = 832 CONV_RULE (RAND_CONV (RAND_CONV (RAND_CONV ETA_CONV))) th3 833 in 834 th4 835 end 836 end 837handle e => raise (wrap_exn "PEXISTS_AND_CONV" "" e); 838 839(* ------------------------------------------------------------------------- *) 840(* AND_PEXISTS_CONV "(?x.P) /\ (?x.Q)" = |- (?x.P) /\ (?x.Q) = (?x. P /\ Q) *) 841(* ------------------------------------------------------------------------- *) 842 843fun AND_PEXISTS_CONV tm = 844 let val (conj1,conj2) = dest_conj tm 845 handle HOL_ERR _ => failwith "expecting `(?x.P) /\\ (?x.Q)`" 846 val (x,P) = dest_pexists conj1 847 handle HOL_ERR _ => failwith "expecting `(?x.P) /\\ (?x.Q)`" 848 val (y,Q) = dest_pexists conj2 849 handle HOL_ERR _ => failwith "expecting `(?x.P) /\\ (?x.Q)`" 850 in 851 if not (x=y) then 852 failwith "expecting `(?x.P) /\\ (?x.Q)`" 853 else if (occs_in x P) orelse (occs_in x Q) then 854 failwith ("`" ^ (fst(dest_var x)) ^ "` free in conjunct(s)") 855 else 856 SYM (PEXISTS_AND_CONV (mk_pexists (x,mk_conj(P,Q)))) 857 end 858handle e => raise (wrap_exn "AND_EXISTS_CONV" "" e); 859 860(* ------------------------------------------------------------------------- *) 861(* LEFT_AND_PEXISTS_CONV "(?x.P) /\ Q" = *) 862(* |- (?x.P) /\ Q = (?x'. P[x'/x] /\ Q) *) 863(* ------------------------------------------------------------------------- *) 864 865fun LEFT_AND_PEXISTS_CONV tm = 866 let val (conj1,Q) = dest_conj tm 867 val (x,P) = dest_pexists conj1 868 val f = mk_pabs(x,P) 869 val th1 = SYM (ISPECL [Q,f] LEFT_EXISTS_AND_THM) 870 val th2 = 871 CONV_RULE 872 (RATOR_CONV (RAND_CONV (RATOR_CONV (RAND_CONV (RAND_CONV 873 ETA_CONV))))) 874 th1 875 val th3 = (CONV_RULE (RAND_CONV (RAND_CONV (PALPHA_CONV x)))) th2 876 val th4 = 877 CONV_RULE 878 (RAND_CONV (RAND_CONV (PABS_CONV (RATOR_CONV (RAND_CONV 879 PBETA_CONV))))) 880 th3 881 in 882 th4 883 end 884handle HOL_ERR _ => raise (ERR "LEFT_AND_PEXISTS_CONV" 885 "expecting `(?x.P) /\\ Q`"); 886 887(* ------------------------------------------------------------------------- *) 888(* RIGHT_AND_PEXISTS_CONV "P /\ (?x.Q)" = *) 889(* |- P /\ (?x.Q) = (?x'. P /\ (Q[x'/x]) *) 890(* ------------------------------------------------------------------------- *) 891 892fun RIGHT_AND_PEXISTS_CONV tm = 893 let val (P,conj2) = dest_conj tm 894 val (x,Q) = dest_pexists conj2 895 val g = mk_pabs(x,Q) 896 val th1 = SYM (ISPECL [P,g] RIGHT_EXISTS_AND_THM) 897 val th2 = 898 CONV_RULE 899 (RATOR_CONV (RAND_CONV (RAND_CONV (RAND_CONV ETA_CONV)))) 900 th1 901 val th3 = CONV_RULE (RAND_CONV (RAND_CONV (PALPHA_CONV x))) th2 902 val th4 = 903 CONV_RULE 904 (RAND_CONV (RAND_CONV (PABS_CONV (RAND_CONV PBETA_CONV)))) 905 th3 906 in 907 th4 908 end 909handle HOL_ERR _ => raise ERR "RIGHT_AND_EXISTS_CONV" 910 "expecting `P /\\ (?x.Q)`"; 911 912 913(* ------------------------------------------------------------------------- *) 914(* PFORALL_OR_CONV : move universal quantifier into disjunction. *) 915(* *) 916(* A call to PFORALL_OR_CONV "!x. P \/ Q" returns: *) 917(* *) 918(* |- (!x. P \/ Q) = (!x.P) \/ Q [if x not free in Q] *) 919(* |- (!x. P \/ Q) = P \/ (!x.Q) [if x not free in P] *) 920(* |- (!x. P \/ Q) = (!x.P) \/ (!x.Q) [if x free in neither P nor Q] *) 921(* ------------------------------------------------------------------------- *) 922 923fun PFORALL_OR_CONV tm = 924 let val (x,Body) = dest_forall tm 925 handle HOL_ERR _ => failwith "expecting `!x. P \\/ Q`" 926 val (P,Q) = dest_disj Body 927 handle HOL_ERR _ => failwith "expecting `!x. P \\/ Q`" 928 val oP = occs_in x P and oQ = occs_in x Q 929 in 930 if (oP andalso oQ) then 931 failwith "bound pair occurs in both conjuncts" 932 else if ((not oP) andalso (not oQ)) then 933 let val th1 = 934 INST_TYPE [alpha |-> type_of x] BOTH_FORALL_OR_THM 935 val th2 = SPECL [P,Q] th1 936 val th3 = 937 CONV_RULE 938 (RATOR_CONV (RAND_CONV (RAND_CONV (PALPHA_CONV x)))) 939 th2 940 val th4 = 941 CONV_RULE 942 (RAND_CONV (RATOR_CONV (RAND_CONV (RAND_CONV 943 (PALPHA_CONV x))))) 944 th3 945 val th5 = 946 CONV_RULE 947 (RAND_CONV (RAND_CONV (RAND_CONV (PALPHA_CONV x)))) 948 th4 949 in 950 th5 951 end 952 else if oP then (* not free in Q *) 953 let val f = mk_pabs(x,P) 954 val th1 = ISPECL [Q,f] LEFT_FORALL_OR_THM 955 val th2 = 956 CONV_RULE 957 (RATOR_CONV (RAND_CONV (RAND_CONV (PALPHA_CONV x)))) 958 th1 959 val th3 = 960 CONV_RULE 961 (RATOR_CONV (RAND_CONV (RAND_CONV 962 (PABS_CONV (RATOR_CONV (RAND_CONV PBETA_CONV)))))) 963 th2 964 val th4 = 965 CONV_RULE 966 (RAND_CONV 967 (RATOR_CONV (RAND_CONV (RAND_CONV ETA_CONV)))) 968 th3 969 in 970 th4 971 end 972 else (* not free in P*) 973 let val g = mk_pabs(x,Q) 974 val th1 = ISPECL [P,g] RIGHT_FORALL_OR_THM 975 val th2 = CONV_RULE 976 (RATOR_CONV (RAND_CONV (RAND_CONV (PALPHA_CONV x)))) 977 th1 978 val th3 = 979 (CONV_RULE (RATOR_CONV (RAND_CONV (RAND_CONV 980 (PABS_CONV (RAND_CONV PBETA_CONV)))))) 981 th2 982 val th4 = (CONV_RULE (RAND_CONV 983 (RAND_CONV (RAND_CONV ETA_CONV)))) 984 th3 985 in 986 th4 987 end 988 end 989handle e => raise (wrap_exn "PFORALL_OR_CONV" "" e); 990 991(* ------------------------------------------------------------------------- *) 992(* OR_PFORALL_CONV "(!x.P) \/ (!x.Q)" = |- (!x.P) \/ (!x.Q) = (!x. P \/ Q) *) 993(* ------------------------------------------------------------------------- *) 994 995fun OR_PFORALL_CONV tm = 996 let val ((x,P),(y,Q)) = 997 let val (disj1,disj2) = dest_disj tm 998 val (x,P) = dest_pforall disj1 999 and (y,Q) = dest_pforall disj2 1000 in 1001 ((x,P),(y,Q)) 1002 end 1003 handle HOL_ERR _ => failwith "expecting `(!x.P) \\/ (!x.Q)`" 1004 in 1005 if not (x=y) then 1006 failwith "expecting `(!x.P) \\/ (!x.Q)'" 1007 else if (occs_in x P) orelse (occs_in x Q) then 1008 failwith "quantified variables free in disjuncts(s)" 1009 else 1010 SYM (PFORALL_OR_CONV (mk_pforall (x, mk_disj(P,Q)))) 1011 end 1012handle e => raise (wrap_exn "OR_FORALL_CONV" "" e); 1013 1014 1015(* ------------------------------------------------------------------------- *) 1016(* LEFT_OR_PFORALL_CONV "(!x.P) \/ Q" = *) 1017(* |- (!x.P) \/ Q = (!x'. P[x'/x] \/ Q) *) 1018(* ------------------------------------------------------------------------- *) 1019 1020fun LEFT_OR_PFORALL_CONV tm = 1021 let val ((x,P),Q) = 1022 let val (disj1,Q) = dest_disj tm 1023 val (x,P) = dest_pforall disj1 1024 in 1025 ((x,P),Q) 1026 end 1027 val f = mk_pabs(x,P) 1028 val th1 = SYM (ISPECL [Q,f] LEFT_FORALL_OR_THM) 1029 val th2 = 1030 CONV_RULE 1031 (RATOR_CONV (RAND_CONV (RATOR_CONV (RAND_CONV (RAND_CONV 1032 ETA_CONV))))) 1033 th1 1034 val th3 = CONV_RULE (RAND_CONV (RAND_CONV (PALPHA_CONV x))) th2 1035 val th4 = 1036 CONV_RULE 1037 (RAND_CONV (RAND_CONV (PABS_CONV (RATOR_CONV (RAND_CONV 1038 PBETA_CONV))))) 1039 th3 1040 in 1041 th4 1042 end 1043handle HOL_ERR _ => raise (ERR "LEFT_OR_PFORALL_CONV" 1044 "expecting `(!x.P) \\/ Q`"); 1045 1046 1047(* ------------------------------------------------------------------------- *) 1048(* RIGHT_OR_PFORALL_CONV "P \/ (!x.Q)" = *) 1049(* |- P \/ (!x.Q) = (!x'. P \/ (Q[x'/x]) *) 1050(* ------------------------------------------------------------------------- *) 1051 1052fun RIGHT_OR_PFORALL_CONV tm = 1053 let val (P,(x,Q)) = 1054 let val (P,disj2) = dest_disj tm 1055 val (x,Q) = dest_pforall disj2 1056 in 1057 (P,(x,Q)) 1058 end 1059 val g = mk_pabs(x,Q) 1060 val th1 = SYM (ISPECL [P,g] RIGHT_FORALL_OR_THM) 1061 val th2 = 1062 CONV_RULE 1063 (RATOR_CONV (RAND_CONV (RAND_CONV (RAND_CONV ETA_CONV)))) 1064 th1 1065 val th3 = CONV_RULE (RAND_CONV (RAND_CONV (PALPHA_CONV x))) th2 1066 val th4 = 1067 CONV_RULE 1068 (RAND_CONV (RAND_CONV (PABS_CONV (RAND_CONV PBETA_CONV)))) 1069 th3 1070 in 1071 th4 1072 end 1073handle HOL_ERR _ => raise (ERR "RIGHT_OR_FORALL_CONV" 1074 "expecting `P \\/ (!x.Q)`"); 1075 1076 1077(* ------------------------------------------------------------------------- *) 1078(* PFORALL_IMP_CONV, implements the following axiom schemes. *) 1079(* *) 1080(* |- (!x. P==>Q[x]) = (P ==> (!x.Q[x])) [x not free in P] *) 1081(* *) 1082(* |- (!x. P[x]==>Q) = ((?x.P[x]) ==> Q) [x not free in Q] *) 1083(* *) 1084(* |- (!x. P==>Q) = ((?x.P) ==> (!x.Q)) [x not free in P==>Q] *) 1085(* ------------------------------------------------------------------------- *) 1086 1087fun PFORALL_IMP_CONV tm = 1088 let val (x,(P,Q)) = 1089 let val (Bvar,Body) = dest_pforall tm 1090 val (ant,conseq) = dest_imp Body 1091 in 1092 (Bvar,(ant,conseq)) 1093 end 1094 handle HOL_ERR _ => failwith "expecting `!x. P ==> Q`" 1095 val oP = occs_in x P and oQ = occs_in x Q 1096 in 1097 if (oP andalso oQ) then 1098 failwith "bound pair occurs in both sides of `==>`" 1099 else if ((not oP) andalso (not oQ)) then 1100 let val th1 = INST_TYPE[alpha |-> type_of x] BOTH_FORALL_IMP_THM 1101 val th2 = SPECL [P,Q] th1 1102 val th3 = 1103 CONV_RULE 1104 (RATOR_CONV (RAND_CONV (RAND_CONV (PALPHA_CONV x)))) 1105 th2 1106 val th4 = 1107 CONV_RULE 1108 (RAND_CONV (RATOR_CONV (RAND_CONV (RAND_CONV 1109 (PALPHA_CONV x))))) 1110 th3 1111 val th5 = 1112 CONV_RULE 1113 (RAND_CONV (RAND_CONV (RAND_CONV (PALPHA_CONV x)))) 1114 th4 1115 in 1116 th5 1117 end 1118 else if oP then (* not free in Q *) 1119 let val f = mk_pabs(x,P) 1120 val th1 = ISPECL [Q,f] LEFT_FORALL_IMP_THM 1121 val th2 = 1122 CONV_RULE 1123 (RATOR_CONV(RAND_CONV (RAND_CONV (PALPHA_CONV x)))) 1124 th1 1125 val th3 = 1126 CONV_RULE 1127 (RATOR_CONV (RAND_CONV (RAND_CONV 1128 (PABS_CONV(RATOR_CONV(RAND_CONV PBETA_CONV)))))) 1129 th2 1130 val th4 = CONV_RULE 1131 (RAND_CONV(RATOR_CONV (RAND_CONV (RAND_CONV ETA_CONV)))) 1132 th3 1133 in 1134 th4 1135 end 1136 else (* not free in P*) 1137 let val g = mk_pabs(x,Q) 1138 val th1 = ISPECL [P,g] RIGHT_FORALL_IMP_THM 1139 val th2 = CONV_RULE 1140 (RATOR_CONV(RAND_CONV (RAND_CONV (PALPHA_CONV x)))) 1141 th1 1142 val th3 = 1143 CONV_RULE 1144 (RATOR_CONV (RAND_CONV (RAND_CONV (PABS_CONV 1145 (RAND_CONV PBETA_CONV))))) 1146 th2 1147 val th4 = 1148 CONV_RULE (RAND_CONV (RAND_CONV (RAND_CONV ETA_CONV))) 1149 th3 1150 in 1151 th4 1152 end 1153 end 1154handle e => raise (wrap_exn "PFORALL_IMP_CONV" "" e); 1155 1156(* ------------------------------------------------------------------------- *) 1157(* LEFT_IMP_PEXISTS_CONV "(?x.P) ==> Q" = *) 1158(* |- ((?x.P) ==> Q) = (!x'. P[x'/x] ==> Q) *) 1159(* ------------------------------------------------------------------------- *) 1160 1161fun LEFT_IMP_PEXISTS_CONV tm = 1162 let val ((x,P),Q) = 1163 let val (ant,conseq) = dest_imp tm 1164 val (Bvar,Body) = dest_pexists ant 1165 in 1166 ((Bvar,Body),conseq) 1167 end 1168 val f = mk_pabs(x,P) 1169 val th = SYM (ISPECL [Q,f] LEFT_FORALL_IMP_THM) 1170 val th1 = 1171 CONV_RULE 1172 (RATOR_CONV (RAND_CONV (RATOR_CONV (RAND_CONV 1173 (RAND_CONV ETA_CONV))))) 1174 th 1175 val th2 = CONV_RULE (RAND_CONV (RAND_CONV (PALPHA_CONV x))) th1 1176 in 1177 CONV_RULE 1178 (RAND_CONV (RAND_CONV (PABS_CONV 1179 (RATOR_CONV (RAND_CONV PBETA_CONV))))) 1180 th2 1181 end 1182handle HOL_ERR _ => raise (ERR "LEFT_IMP_PEXISTS_CONV" 1183 "expecting `(?p.P) ==> Q`"); 1184 1185 1186(* ------------------------------------------------------------------------- *) 1187(* RIGHT_IMP_PFORALL_CONV "P ==> (!x.Q)" = *) 1188(* |- (P ==> (!x.Q)) = (!x'. P ==> (Q[x'/x]) *) 1189(* ------------------------------------------------------------------------- *) 1190 1191fun RIGHT_IMP_PFORALL_CONV tm = 1192 let val (P,(x,Q)) = 1193 let val (ant,conseq) = dest_imp tm 1194 val (Bvar,Body) = dest_pforall conseq 1195 in 1196 (ant,(Bvar,Body)) 1197 end 1198 val g = mk_pabs(x,Q) 1199 val th1 = SYM (ISPECL [P,g] RIGHT_FORALL_IMP_THM) 1200 val th2 = 1201 CONV_RULE 1202 (RATOR_CONV (RAND_CONV (RAND_CONV (RAND_CONV ETA_CONV)))) 1203 th1 1204 val th3 = CONV_RULE (RAND_CONV (RAND_CONV (PALPHA_CONV x))) th2 1205 val th4 = 1206 CONV_RULE 1207 (RAND_CONV (RAND_CONV (PABS_CONV (RAND_CONV PBETA_CONV)))) 1208 th3 1209 in 1210 th4 1211 end 1212handle HOL_ERR _ => raise (ERR "RIGHT_IMP_FORALL_CONV" 1213 "expecting `P ==> (!x.Q)`"); 1214 1215 1216(* ------------------------------------------------------------------------- *) 1217(* PEXISTS_IMP_CONV, implements the following axiom schemes. *) 1218(* *) 1219(* |- (?x. P==>Q[x]) = (P ==> (?x.Q[x])) [x not free in P] *) 1220(* *) 1221(* |- (?x. P[x]==>Q) = ((!x.P[x]) ==> Q) [x not free in Q] *) 1222(* *) 1223(* |- (?x. P==>Q) = ((!x.P) ==> (?x.Q)) [x not free in P==>Q] *) 1224(* ------------------------------------------------------------------------- *) 1225 1226fun PEXISTS_IMP_CONV tm = 1227 let val (x,(P,Q)) = 1228 let val (Bvar,Body) = dest_pexists tm 1229 val (ant,conseq) = dest_imp Body 1230 in 1231 (Bvar,(ant,conseq)) 1232 end 1233 handle HOL_ERR _ => failwith "expecting `?x. P ==> Q`" 1234 val oP = occs_in x P and oQ = occs_in x Q 1235 in 1236 if (oP andalso oQ) then 1237 failwith "bound pair occurs in both sides of `==>`" 1238 else if ((not oP) andalso (not oQ)) then 1239 let val th1 = INST_TYPE[alpha |-> type_of x] BOTH_EXISTS_IMP_THM 1240 val th2 = SPECL [P,Q] th1 1241 val th3 = 1242 CONV_RULE 1243 (RATOR_CONV (RAND_CONV (RAND_CONV (PALPHA_CONV x)))) 1244 th2 1245 val th4 = 1246 CONV_RULE 1247 (RAND_CONV (RATOR_CONV (RAND_CONV (RAND_CONV 1248 (PALPHA_CONV x))))) 1249 th3 1250 val th5 = 1251 CONV_RULE 1252 (RAND_CONV (RAND_CONV (RAND_CONV (PALPHA_CONV x)))) 1253 th4 1254 in 1255 th5 1256 end 1257 else if oP then (* not free in Q *) 1258 let val f = mk_pabs(x,P) 1259 val th1 = ISPECL [Q,f] LEFT_EXISTS_IMP_THM 1260 val th2 = 1261 CONV_RULE 1262 (RATOR_CONV (RAND_CONV (RAND_CONV(PALPHA_CONV x)))) 1263 th1 1264 val th3 = 1265 CONV_RULE 1266 (RATOR_CONV (RAND_CONV (RAND_CONV 1267 (PABS_CONV(RATOR_CONV(RAND_CONV PBETA_CONV)))))) 1268 th2 1269 val th4 = 1270 CONV_RULE 1271 (RAND_CONV (RATOR_CONV (RAND_CONV (RAND_CONV 1272 ETA_CONV)))) 1273 th3 1274 in 1275 th4 1276 end 1277 else (* not free in P*) 1278 let val g = mk_pabs(x,Q) 1279 val th1 = ISPECL [P,g] RIGHT_EXISTS_IMP_THM 1280 val th2 = CONV_RULE 1281 (RATOR_CONV (RAND_CONV (RAND_CONV (PALPHA_CONV x)))) 1282 th1 1283 val th3 = 1284 CONV_RULE 1285 (RATOR_CONV (RAND_CONV (RAND_CONV 1286 (PABS_CONV (RAND_CONV PBETA_CONV))))) 1287 th2 1288 val th4 = 1289 CONV_RULE (RAND_CONV (RAND_CONV 1290 (RAND_CONV ETA_CONV))) th3 1291 in 1292 th4 1293 end 1294 end 1295handle e => raise (wrap_exn "PEXISTS_IMP_CONV" "" e); 1296 1297 1298(* ------------------------------------------------------------------------- *) 1299(* LEFT_IMP_PFORALL_CONV "(!x. t1[x]) ==> t2" = *) 1300(* |- (!x. t1[x]) ==> t2 = (?x'. t1[x'] ==> t2) *) 1301(* ------------------------------------------------------------------------- *) 1302 1303fun LEFT_IMP_PFORALL_CONV tm = 1304 let val ((x,P),Q) = 1305 let val (ant,conseq) = dest_imp tm 1306 val (Bvar,Body) = dest_pforall ant 1307 in 1308 ((Bvar,Body),conseq) 1309 end 1310 val f = mk_pabs(x,P) 1311 val th1 = SYM (ISPECL [Q,f] LEFT_EXISTS_IMP_THM) 1312 val th2 = 1313 CONV_RULE 1314 (RATOR_CONV (RAND_CONV (RATOR_CONV (RAND_CONV (RAND_CONV 1315 ETA_CONV))))) 1316 th1 1317 val th3 = CONV_RULE (RAND_CONV (RAND_CONV (PALPHA_CONV x))) th2 1318 val th4 = 1319 CONV_RULE 1320 (RAND_CONV (RAND_CONV (PABS_CONV 1321 (RATOR_CONV (RAND_CONV PBETA_CONV))))) 1322 th3 1323 in 1324 th4 1325 end 1326handle HOL_ERR _ => raise (ERR "LEFT_IMP_PFORALL_CONV" 1327 "expecting `(!x.P) ==> Q`"); 1328 1329(* ------------------------------------------------------------------------- *) 1330(* RIGHT_IMP_EXISTS_CONV "t1 ==> (?x. t2)" = *) 1331(* |- (t1 ==> ?x. t2) = (?x'. t1 ==> t2[x'/x]) *) 1332(* ------------------------------------------------------------------------- *) 1333 1334fun RIGHT_IMP_PEXISTS_CONV tm = 1335 let val (P,(x,Q)) = 1336 let val (ant,conseq) = dest_imp tm 1337 val (Bvar,Body) = dest_pexists conseq 1338 in 1339 (ant,(Bvar,Body)) 1340 end 1341 val g = mk_pabs(x,Q) 1342 val th1 = SYM (ISPECL [P,g] RIGHT_EXISTS_IMP_THM) 1343 val th2 = 1344 CONV_RULE 1345 (RATOR_CONV (RAND_CONV (RAND_CONV (RAND_CONV ETA_CONV)))) 1346 th1 1347 val th3 = CONV_RULE (RAND_CONV (RAND_CONV (PALPHA_CONV x))) th2 1348 val th4 = 1349 CONV_RULE 1350 (RAND_CONV (RAND_CONV (PABS_CONV (RAND_CONV PBETA_CONV)))) 1351 th3 1352 in 1353 th4 1354 end 1355handle HOL_ERR _ => raise (ERR "RIGHT_IMP_PEXISTS_CONV" 1356 "expecting `P ==> (!x.Q)`"); 1357 1358(* end Pair_conv *) 1359 1360(* ---------------------------------------------------------------------*) 1361(* CONTENTS: functions which are common to paired universal and *) 1362(* existential quantifications. *) 1363(* ---------------------------------------------------------------------*) 1364 1365(* structure Pair_both1 :> Pair_both1 = struct *) 1366 1367 1368fun mk_fun(y1,y2) = y1 --> y2; 1369fun comma(ty1,ty2) = Term.inst[alpha |-> ty1, beta |-> ty2]pairSyntax.comma_tm 1370 1371val PFORALL_THM = pairTheory.PFORALL_THM; 1372val PEXISTS_THM = pairTheory.PEXISTS_THM; 1373 1374(* ------------------------------------------------------------------------- *) 1375(* CURRY_FORALL_CONV "!(x,y).t" = (|- (!(x,y).t) = (!x y.t)) *) 1376(* ------------------------------------------------------------------------- *) 1377 1378 1379fun CURRY_FORALL_CONV tm = 1380 let val (xy,bod) = dest_pforall tm 1381 val (x,y) = pairSyntax.dest_pair xy 1382 val result = list_mk_pforall ([x,y],bod) 1383 val f = rand (rand tm) 1384 val th1 = RAND_CONV (PABS_CONV (UNPBETA_CONV xy)) tm 1385 val th2 = CONV_RULE (RAND_CONV (RAND_CONV (PABS_CONV CURRY_CONV))) th1 1386 val th3 = (SYM (ISPEC f PFORALL_THM)) 1387 val th4 = CONV_RULE (RATOR_CONV (RAND_CONV (GEN_PALPHA_CONV xy))) th3 1388 val th5 = CONV_RULE (RAND_CONV (GEN_PALPHA_CONV x)) (TRANS th2 th4) 1389 val th6 = CONV_RULE (RAND_CONV (RAND_CONV (PABS_CONV 1390 (GEN_PALPHA_CONV y)))) th5 1391 val th7 = CONV_RULE(RAND_CONV(RAND_CONV(PABS_CONV (RAND_CONV 1392 (PABS_CONV(RATOR_CONV PBETA_CONV)))))) th6 1393 val th8 = 1394 CONV_RULE (RAND_CONV (RAND_CONV (PABS_CONV (RAND_CONV 1395 (PABS_CONV PBETA_CONV))))) th7 1396 in 1397 TRANS th8 (REFL result) 1398 end 1399 handle HOL_ERR _ => failwith "CURRY_FORALL_CONV" ; 1400 1401(* ------------------------------------------------------------------------- *) 1402(* CURRY_EXISTS_CONV "?(x,y).t" = (|- (?(x,y).t) = (?x y.t)) *) 1403(* ------------------------------------------------------------------------- *) 1404 1405fun CURRY_EXISTS_CONV tm = 1406 let val (xy,bod) = dest_pexists tm 1407 val (x,y) = pairSyntax.dest_pair xy 1408 val result = list_mk_pexists ([x,y],bod) 1409 val f = rand (rand tm) 1410 val th1 = RAND_CONV (PABS_CONV (UNPBETA_CONV xy)) tm 1411 val th2 = CONV_RULE (RAND_CONV (RAND_CONV (PABS_CONV CURRY_CONV))) th1 1412 val th3 = (SYM (ISPEC f PEXISTS_THM)) 1413 val th4 = CONV_RULE (RATOR_CONV (RAND_CONV (GEN_PALPHA_CONV xy))) th3 1414 val th5 = CONV_RULE (RAND_CONV (GEN_PALPHA_CONV x)) (TRANS th2 th4) 1415 val th6 = CONV_RULE (RAND_CONV (RAND_CONV (PABS_CONV 1416 (GEN_PALPHA_CONV y)))) th5 1417 val th7 = CONV_RULE (RAND_CONV (RAND_CONV (PABS_CONV (RAND_CONV 1418 (PABS_CONV (RATOR_CONV PBETA_CONV)))))) th6 1419 val th8 = CONV_RULE (RAND_CONV (RAND_CONV (PABS_CONV 1420 (RAND_CONV (PABS_CONV PBETA_CONV))))) th7 1421 in 1422 TRANS th8 (REFL result) 1423 end 1424handle HOL_ERR _ => failwith "CURRY_EXISTS_CONV" ; 1425 1426(* ------------------------------------------------------------------------- *) 1427(* UNCURRY_FORALL_CONV "!x y.t" = (|- (!x y.t) = (!(x,y).t)) *) 1428(* ------------------------------------------------------------------------- *) 1429 1430fun UNCURRY_FORALL_CONV tm = 1431 let val (x,Body) = dest_pforall tm 1432 val (y,bod) = dest_pforall Body 1433 val xy = pairSyntax.mk_pair(x,y) 1434 val result = mk_pforall (xy,bod) 1435 val th1 = (RAND_CONV (PABS_CONV (RAND_CONV (PABS_CONV 1436 (UNPBETA_CONV xy))))) tm 1437 val f = rand (rator (pbody (rand (pbody (rand (rand (concl th1))))))) 1438 val th2 = CONV_RULE (RAND_CONV (RAND_CONV (PABS_CONV 1439 (RAND_CONV (PABS_CONV CURRY_CONV))))) th1 1440 val th3 = ISPEC f PFORALL_THM 1441 val th4 = CONV_RULE (RATOR_CONV (RAND_CONV (GEN_PALPHA_CONV x))) th3 1442 val th5 = CONV_RULE (RATOR_CONV (RAND_CONV (RAND_CONV (PABS_CONV 1443 (GEN_PALPHA_CONV y))))) th4 1444 val th6 = CONV_RULE (RAND_CONV (GEN_PALPHA_CONV xy)) (TRANS th2 th5) 1445 val th7 = CONV_RULE (RAND_CONV (RAND_CONV (PABS_CONV (RATOR_CONV 1446 PBETA_CONV)))) th6 1447 val th8 = CONV_RULE (RAND_CONV (RAND_CONV (PABS_CONV PBETA_CONV))) th7 1448 in 1449 TRANS th8 (REFL result) 1450 end 1451handle HOL_ERR _ => failwith "UNCURRY_FORALL_CONV"; 1452 1453(* ------------------------------------------------------------------------- *) 1454(* UNCURRY_EXISTS_CONV "?x y.t" = (|- (?x y.t) = (?(x,y).t)) *) 1455(* ------------------------------------------------------------------------- *) 1456 1457fun UNCURRY_EXISTS_CONV tm = 1458 let val (x,Body) = dest_pexists tm 1459 val (y,bod) = dest_pexists Body 1460 val xy = pairSyntax.mk_pair(x,y) 1461 val result = mk_pexists (xy,bod) 1462 val th1 = (RAND_CONV (PABS_CONV (RAND_CONV (PABS_CONV 1463 (UNPBETA_CONV xy))))) tm 1464 val f = rand (rator (pbody (rand (pbody (rand (rand (concl th1))))))) 1465 val th2 = CONV_RULE (RAND_CONV (RAND_CONV (PABS_CONV 1466 (RAND_CONV (PABS_CONV CURRY_CONV))))) th1 1467 val th3 = ISPEC f PEXISTS_THM 1468 val th4 = CONV_RULE (RATOR_CONV (RAND_CONV (GEN_PALPHA_CONV x))) th3 1469 val th5 = CONV_RULE (RATOR_CONV (RAND_CONV (RAND_CONV (PABS_CONV 1470 (GEN_PALPHA_CONV y))))) th4 1471 val th6 = CONV_RULE (RAND_CONV (GEN_PALPHA_CONV xy)) (TRANS th2 th5) 1472 val th7 = CONV_RULE (RAND_CONV (RAND_CONV 1473 (PABS_CONV (RATOR_CONV PBETA_CONV)))) th6 1474 val th8 = CONV_RULE (RAND_CONV (RAND_CONV (PABS_CONV PBETA_CONV))) th7 1475 in 1476 TRANS th8 (REFL result) 1477 end 1478 handle HOL_ERR _ => failwith "UNCURRY_EXISTS_CONV"; 1479 1480(* end; Pair_both1 *) 1481 1482(* ---------------------------------------------------------------------*) 1483(* CONTENTS: functions for dealing with paired universal quantification.*) 1484(* ---------------------------------------------------------------------*) 1485 1486(* ------------------------------------------------------------------------- *) 1487(* Paired Specialisation: *) 1488(* A |- !p.t *) 1489(* ------------- PSPEC c [where c is free for p in t] *) 1490(* A |- t[c/p] *) 1491(* ------------------------------------------------------------------------- *) 1492 1493(* structure Pair_forall :> Pair_forall = struct *) 1494 1495val FORALL_DEF = boolTheory.FORALL_DEF; 1496 1497val PSPEC = let 1498 val spec_thm = (* !x f. $! f ==> f x *) 1499 let 1500 val f = mk_var("f", alpha --> bool) 1501 val x = mk_var("x", alpha) 1502 val fa = mk_thy_const{Name = "!", Thy = "bool", 1503 Ty = (alpha --> bool) --> bool} 1504 in 1505 AP_THM FORALL_DEF f 1506 |> RIGHT_BETA |> C EQ_MP (ASSUME (mk_comb(fa,f))) |> C AP_THM x 1507 |> RIGHT_BETA |> EQT_ELIM |> DISCH_ALL |> GENL [x,f] 1508 end 1509 val gxty = Type.alpha 1510 val gfty = alpha --> bool 1511 val gx = genvar gxty 1512 val gf = genvar gfty 1513 val sth = ISPECL [gx,gf] spec_thm 1514in 1515 fn x => 1516 fn th => 1517 let val f = rand (concl th) 1518 val xty = type_of x 1519 and fty = type_of f 1520 val gxinst = mk_var((fst o dest_var) gx, xty) 1521 and gfinst = mk_var((fst o dest_var) gf, fty) 1522 in 1523 (CONV_RULE PBETA_CONV) 1524 (MP (INST_TY_TERM ([{residue=x,redex=gxinst}, 1525 {residue=f,redex=gfinst}], 1526 [{residue=xty,redex=gxty}]) sth) th) 1527 end 1528 end 1529handle HOL_ERR _ => failwith "PSPEC"; 1530 1531fun PSPECL xl th = rev_itlist PSPEC xl th; 1532 1533fun IPSPEC x th = 1534 let val (p,tm) = with_exn dest_pforall(concl th) 1535 (ERR"IPSPEC" "input theorem not universally quantified") 1536 val (_,inst) = match_term p x 1537 handle HOL_ERR _ => raise (ERR "IPSPEC" 1538 "can't type-instantiate input theorem") 1539 in 1540 PSPEC x (INST_TYPE inst th) handle HOL_ERR _ => 1541 raise (ERR "IPSPEC" "type variable free in assumptions") 1542 end; 1543 1544val IPSPECL = 1545 let val tup = end_itlist (curry mk_pair) 1546 fun strip [] = K [] 1547 | strip (_::ts) = fn t => 1548 let val (Bvar,Body) = dest_pforall t in Bvar::(strip ts Body) end 1549 in 1550 fn xl => 1551 if (null xl) then I 1552 else let val tupxl = tup xl 1553 val striper = strip xl 1554 in 1555 fn th => 1556 let val pl = with_exn striper (concl th) 1557 (ERR "IPSPECL" 1558 "list of terms too long for theorem") 1559 val (_,inst) = match_term (tup pl) tupxl handle HOL_ERR _ => 1560 raise (ERR "IPSPECL" 1561 "can't type-instantiate input theorem") 1562 in 1563 PSPECL xl (INST_TYPE inst th) handle HOL_ERR _ => 1564 raise (ERR "IPSPECL" "type variable free in assumptions") 1565 end 1566 end 1567 end; 1568 1569 1570val pvariant = 1571 let fun uniq [] = [] 1572 | uniq (h::t) = h::uniq (filter (not o equal h) t) 1573 fun variantl avl [] = [] 1574 | variantl avl (h::t) = 1575 let val h' = variant (avl@(filter is_var t)) h 1576 in {residue=h',redex=h}::(variantl (h'::avl) t) 1577 end 1578 in 1579 fn pl => 1580 fn p => 1581 let val avoid = (flatten (map ((map (assert is_var)) o strip_pair) pl)) 1582 val originals = uniq (map (assert (fn p => is_var p orelse is_const p)) 1583 (strip_pair p)) 1584 val subl = variantl avoid originals 1585 in 1586 subst subl p 1587 end end; 1588 1589fun PSPEC_PAIR th = 1590 let val (p,_) = dest_pforall (concl th) 1591 val p' = pvariant (free_varsl (hyp th)) p 1592 in 1593 (p', PSPEC p' th) 1594 end; 1595 1596val PSPEC_ALL = 1597 let fun f p (ps,l) = 1598 let val p' = pvariant ps p 1599 in 1600 ((free_vars p')@ps,p'::l) 1601 end 1602 in 1603 fn th => 1604 let val (hxs,con) = (free_varsl ## I) (dest_thm th) 1605 val fxs = free_vars con 1606 and pairs = fst(strip_pforall con) 1607 in 1608 PSPECL (snd(itlist f pairs (hxs @ fxs,[]))) th 1609 end 1610 end; 1611 1612fun GPSPEC th = 1613 let val (_,t) = dest_thm th 1614 in 1615 if is_pforall t then 1616 GPSPEC (PSPEC 1617 (genvarstruct (type_of (fst (dest_pforall t)))) th) 1618 else 1619 th 1620 end; 1621 1622 1623fun PSPEC_TAC (t,x) = 1624 if (not (is_pair t)) andalso (is_var x) then 1625 SPEC_TAC (t,x) 1626 else if (is_pair t) andalso (is_pair x) then 1627 let val (t1,t2) = dest_pair t 1628 val (x1,x2) = dest_pair x 1629 in 1630 (PSPEC_TAC (t2,x2)) THEN 1631 (PSPEC_TAC (t1,x1)) THEN 1632 (CONV_TAC UNCURRY_FORALL_CONV) 1633 end 1634 else if (not (is_pair t)) andalso (is_pair x) then 1635 let val x' = genvar (type_of x) 1636 in 1637 (SPEC_TAC (t,x')) THEN 1638 (CONV_TAC (GEN_PALPHA_CONV x)) 1639 end 1640 else (* (is_pair t) & (is_var x) *) 1641 let val (fst,snd) = dest_pair t 1642 val x' = mk_pair(genvar(type_of fst), genvar(type_of snd)) 1643 in 1644 (PSPEC_TAC (t,x')) THEN 1645 (CONV_TAC (GEN_PALPHA_CONV x)) 1646 end 1647 handle HOL_ERR _ => failwith "PSPEC_TAC"; 1648 1649(* ------------------------------------------------------------------------- *) 1650(* Paired Generalisation: *) 1651(* A |- t *) 1652(* ----------- PGEN p [where p is not free in A] *) 1653(* A |- !p.t *) 1654(* ------------------------------------------------------------------------- *) 1655 1656fun PGEN p th = 1657 if is_var p then 1658 GEN p th 1659 else (* is_pair p *) 1660 let val (v1, v2) = dest_pair p 1661 in 1662 CONV_RULE UNCURRY_FORALL_CONV (PGEN v1 (PGEN v2 th)) 1663 end 1664 handle HOL_ERR _ => failwith "PGEN" ; 1665 1666fun PGENL xl th = itlist PGEN xl th;; 1667 1668fun P_PGEN_TAC p :tactic = fn (a,t) => 1669 let val (x,b) = with_exn dest_pforall t 1670 (ERR "P_PGEN_TAC" "Goal not universally quantified") 1671 in 1672 if (is_var x) andalso (is_var p) then 1673 X_GEN_TAC p (a,t) 1674 else if (is_pair x) andalso (is_pair p) then 1675 let val (p1,p2) = dest_pair p 1676 in 1677 ((CONV_TAC CURRY_FORALL_CONV) THEN 1678 (P_PGEN_TAC p1) THEN 1679 (P_PGEN_TAC p2)) (a,t) 1680 end 1681 else if (is_var p) andalso (is_pair x) then 1682 let val x' = genvar (type_of p) 1683 in 1684 ((CONV_TAC (GEN_PALPHA_CONV x')) THEN 1685 (X_GEN_TAC p)) (a,t) 1686 end 1687 else (*(is_pair p) & (is_var x)*) 1688 let val (fst,snd) = dest_pair p 1689 val x' = mk_pair(genvar(type_of fst),genvar(type_of snd)) 1690 in 1691 ((CONV_TAC (GEN_PALPHA_CONV x')) THEN 1692 (P_PGEN_TAC p)) (a,t) 1693 end 1694 end 1695handle HOL_ERR _ => failwith "P_PGEN_TAC" ; 1696 1697val PGEN_TAC : tactic = fn (a,t) => 1698 let val (x,b) = with_exn dest_pforall t 1699 (ERR "PGEN_TAC" "Goal not universally quantified") 1700 in 1701 P_PGEN_TAC (pvariant (free_varsl(t::a)) x) (a,t) 1702 end; 1703 1704fun FILTER_PGEN_TAC tm : tactic = fn (a,t) => 1705 if (is_pforall t) andalso (not (tm = (fst (dest_pforall t)))) then 1706 PGEN_TAC (a,t) 1707 else 1708 failwith "FILTER_PGEN_TAC"; 1709(* end; Pair_forall *) 1710 1711(* ---------------------------------------------------------------------*) 1712(* CONTENTS: functions for paired existential quantifications. *) 1713(* ---------------------------------------------------------------------*) 1714 1715(* structure Pair_exists :> Pair_exists = struct *) 1716 1717val EXISTS_DEF = boolTheory.EXISTS_DEF; 1718val EXISTS_UNIQUE_DEF = boolTheory.EXISTS_UNIQUE_DEF; 1719 1720fun mk_fun(y1,y2) = (y1 --> y2) 1721 1722val PEXISTS_CONV = 1723 let val f = mk_var("f", alpha --> bool) 1724 val th1 = AP_THM EXISTS_DEF f 1725 val th2 = GEN f ((CONV_RULE (RAND_CONV BETA_CONV)) th1) 1726 in 1727 fn tm => 1728 let val (p,b) = dest_pexists tm 1729 val g = mk_pabs(p,b) 1730 in 1731 (CONV_RULE (RAND_CONV PBETA_CONV)) (ISPEC g th2) 1732 end 1733 end 1734handle HOL_ERR _ => failwith "PEXISTS_CONV" ; 1735 1736(* ------------------------------------------------------------------------- *) 1737(* A |- ?p. t[p] *) 1738(* ------------------ PSELECT_RULE *) 1739(* A |- t[@p .t[p]] *) 1740(* ------------------------------------------------------------------------- *) 1741 1742val PSELECT_RULE = CONV_RULE PEXISTS_CONV ; 1743 1744(* ------------------------------------------------------------------------- *) 1745(* PSELECT_CONV "t [@p. t[p]]" = (|- (t [@p. t[p]]) = (?p. t[p])) *) 1746(* ------------------------------------------------------------------------- *) 1747 1748val PSELECT_CONV = 1749 let fun find_first p tm = 1750 if p tm then 1751 tm 1752 else if is_abs tm then 1753 find_first p (body tm) 1754 else if is_comb tm then 1755 let val (f,a) = dest_comb tm 1756 in 1757 (find_first p f) handle HOL_ERR _ => (find_first p a) 1758 end 1759 else 1760 failwith"" 1761 in 1762 fn tm => 1763 let fun right t = is_pselect t andalso 1764 (rhs (concl (PBETA_CONV (mk_comb(rand t,t)))) = tm) 1765 val epi = find_first right tm 1766 val (p,b) = dest_pselect epi 1767 in 1768 SYM (PEXISTS_CONV (mk_pexists(p,b))) 1769 end 1770 end 1771handle HOL_ERR _ => failwith "PSELECT_CONV" ; 1772 1773 1774(* ------------------------------------------------------------------------- *) 1775(* A |- t[@p .t[p]] *) 1776(* ------------------ PEXISTS_RULE *) 1777(* A |- ?p. t[p] *) 1778(* ------------------------------------------------------------------------- *) 1779 1780val PEXISTS_RULE = CONV_RULE PSELECT_CONV ; 1781 1782(* ------------------------------------------------------------------------- *) 1783(* A |- P t *) 1784(* -------------- PSELECT_INTRO *) 1785(* A |- P($@ P) *) 1786(* ------------------------------------------------------------------------- *) 1787 1788val PSELECT_INTRO = SELECT_INTRO ; 1789 1790(* ------------------------------------------------------------------------- *) 1791(* A1 |- f($@ f) , A2, f p |- t *) 1792(* -------------------------------- PSELECT_ELIM th1 ("p", th2) [p not free] *) 1793(* A1 u A2 |- t *) 1794(* ------------------------------------------------------------------------- *) 1795 1796fun PSELECT_ELIM th1 (v,th2) = 1797 let val (f,sf) = dest_comb (concl th1) 1798 val t1 = MP (PSPEC sf (PGEN v (DISCH (mk_comb(f,v)) th2))) th1 1799 val t2 = ALPHA (concl t1) (concl th2) 1800 in 1801 EQ_MP t2 t1 1802 end 1803handle HOL_ERR _ => failwith "PSELECT_ELIM" ; 1804 1805(* ------------------------------------------------------------------------- *) 1806(* A |- t[q] *) 1807(* ----------------- PEXISTS ("?p. t[p]", "q") *) 1808(* A |- ?p. t[p] *) 1809(* ------------------------------------------------------------------------- *) 1810 1811fun PEXISTS (fm,tm) th = 1812 let val (p,b) = dest_pexists fm 1813 val th1 = PBETA_CONV (mk_comb(mk_pabs(p,b),tm)) 1814 val th2 = EQ_MP (SYM th1) th 1815 val th3 = PSELECT_INTRO th2 1816 val th4 = AP_THM(INST_TYPE [alpha |-> type_of p] EXISTS_DEF) 1817 (mk_pabs(p, b)) 1818 val th5 = TRANS th4 (BETA_CONV(rhs(concl th4))) 1819 in 1820 EQ_MP (SYM th5) th3 1821 end 1822handle HOL_ERR _ => failwith "PEXISTS" ; 1823 1824(* ------------------------------------------------------------------------- *) 1825(* A1 |- ?p. t[p] , A2, t[v] |- u *) 1826(* ---------------------------------- PCHOOSE (v,th1) th2 [v not free] *) 1827(* A1 u A2 |- u *) 1828(* ------------------------------------------------------------------------- *) 1829 1830val PCHOOSE = 1831 let val f = mk_var("f", alpha --> bool) 1832 val t1 = AP_THM EXISTS_DEF f 1833 val t2 = GEN f ((CONV_RULE (RAND_CONV BETA_CONV)) t1) 1834 in 1835 fn (v,th1) => 1836 fn th2 => 1837 let val p = rand (concl th1) 1838 val th1' = EQ_MP (ISPEC p t2) th1 1839 val u1 = UNDISCH (fst 1840 (EQ_IMP_RULE (PBETA_CONV (mk_comb(p,v))))) 1841 val th2' = PROVE_HYP u1 th2 1842 in 1843 PSELECT_ELIM th1' (v,th2') 1844 end 1845 end 1846handle HOL_ERR _ => failwith "PCHOOSE" ; 1847 1848fun P_PCHOOSE_THEN v ttac pth :tactic = 1849 let val (p,b) = dest_pexists (concl pth) 1850 handle HOL_ERR _ => failwith "P_PCHOOSE_THEN" 1851 in 1852 fn (asl,w) => 1853 let val th = itlist ADD_ASSUM (hyp pth) 1854 (ASSUME 1855 (rhs(concl(PBETA_CONV 1856 (mk_comb(mk_pabs(p,b),v)))))) 1857 val (gl,prf) = ttac th (asl,w) 1858 in 1859 (gl, (PCHOOSE (v, pth)) o prf) 1860 end 1861 end; 1862 1863fun PCHOOSE_THEN ttac pth :tactic = 1864 let val (p,b) = dest_pexists (concl pth) 1865 handle HOL_ERR _ => failwith "CHOOSE_THEN" 1866 in 1867 fn (asl,w) => 1868 let val q = pvariant ((thm_frees pth) @ (free_varsl (w::asl))) p 1869 val th = 1870 itlist 1871 ADD_ASSUM 1872 (hyp pth) 1873 (ASSUME 1874 (rhs (concl 1875 (PairedLambda.PAIRED_BETA_CONV 1876 (mk_comb(mk_pabs(p,b),q)))))) 1877 val (gl,prf) = ttac th (asl,w) 1878 in 1879 (gl, (PCHOOSE (q, pth)) o prf) 1880 end 1881 end; 1882 1883 1884fun P_PCHOOSE_TAC p = P_PCHOOSE_THEN p ASSUME_TAC ; 1885 1886val PCHOOSE_TAC = PCHOOSE_THEN ASSUME_TAC ; 1887 1888(* ------------------------------------------------------------------------- *) 1889(* A ?- ?p. t[p] *) 1890(* =============== PEXISTS_TAC "u" *) 1891(* A ?- t[u] *) 1892(* ------------------------------------------------------------------------- *) 1893 1894fun PEXISTS_TAC v (a,t) = let 1895 val (p,b) = dest_pexists t 1896 fun just ths = 1897 case ths of 1898 [th] => PEXISTS (t,v) th 1899 | _ => raise ERR "PEXISTS_TAC" "Justification Bind" 1900in 1901 ([(a, rhs (concl (PBETA_CONV (mk_comb(mk_pabs(p,b),v)))))], just) 1902end 1903handle HOL_ERR _ => failwith "PEXISTS_TAC" ; 1904 1905(* ------------------------------------------------------------------------- *) 1906(* |- ?!p. t[p] *) 1907(* -------------- PEXISTENCE *) 1908(* |- ?p. t[p] *) 1909(* ------------------------------------------------------------------------- *) 1910 1911fun PEXISTENCE th = 1912 let val (p,b) = dest_pabs (rand (concl th)) 1913 val th1 = 1914 AP_THM 1915 (INST_TYPE [alpha |-> type_of p] EXISTS_UNIQUE_DEF) (mk_pabs(p,b)) 1916 val th2 = EQ_MP th1 th 1917 val th3 = CONV_RULE BETA_CONV th2 1918 in 1919 CONJUNCT1 th3 1920 end 1921handle HOL_ERR _ => failwith "PEXISTENCE" ; 1922 1923(* ------------------------------------------------------------------------- *) 1924(* PEXISTS_UNIQUE_CONV "?!p. t[p]" = *) 1925(* (|- (?!p. t[p]) = (?p. t[p] /\ !p p'. t[p] /\ t[p'] ==> (p='p))) *) 1926(* ------------------------------------------------------------------------- *) 1927 1928fun PEXISTS_UNIQUE_CONV tm = 1929 let val (p,b) = dest_pabs (rand tm) 1930 val p' = pvariant (p::(free_vars tm)) p 1931 val th1 = 1932 AP_THM 1933 (INST_TYPE [alpha |-> type_of p] EXISTS_UNIQUE_DEF) (mk_pabs(p,b)) 1934 val th2 = CONV_RULE (RAND_CONV BETA_CONV) th1 1935 val th3 = CONV_RULE (RAND_CONV (RAND_CONV (RAND_CONV (ABS_CONV 1936 (GEN_PALPHA_CONV p'))))) th2 1937 val th4 = CONV_RULE (RAND_CONV (RAND_CONV (GEN_PALPHA_CONV p))) th3 1938 val th5 = CONV_RULE (RAND_CONV (RAND_CONV (RAND_CONV (PABS_CONV 1939 (RAND_CONV (PABS_CONV (RATOR_CONV (RAND_CONV 1940 (RATOR_CONV (RAND_CONV PBETA_CONV)))))))))) th4 1941 in 1942 CONV_RULE (RAND_CONV (RAND_CONV (RAND_CONV (PABS_CONV 1943 (RAND_CONV (PABS_CONV (RATOR_CONV (RAND_CONV 1944 (RAND_CONV PBETA_CONV))))))))) th5 1945 end 1946handle HOL_ERR _ => failwith "PEXISTS_UNIQUE_CONV" ; 1947 1948(* ------------------------------------------------------------------------- *) 1949(* P_PSKOLEM_CONV : introduce a skolem function. *) 1950(* *) 1951(* |- (!x1...xn. ?y. tm[x1,...,xn,y]) *) 1952(* = *) 1953(* (?f. !x1...xn. tm[x1,..,xn,f x1 ... xn] *) 1954(* *) 1955(* The first argument is the function f. *) 1956(* ------------------------------------------------------------------------- *) 1957 1958local fun BABY_P_PSKOLEM_CONV f = 1959 if not(is_vstruct f) then 1960 raise ERR "P_SKOLEM_CONV" "first argument not a varstruct" 1961 else 1962 fn tm => 1963 let val (xs,(y,P)) = (I ## dest_exists) (strip_pforall tm) 1964 val fx = with_exn list_mk_comb(f,xs) 1965 (ERR"P_SKOLEM_CONV" "function variable has the wrong type") 1966 in 1967 if free_in f tm then 1968 raise ERR "P_SKOLEM_CONV" 1969 "skolem function free in the input term" 1970 else 1971 let val pat = mk_exists(f,list_mk_pforall(xs,subst[y |-> fx]P)) 1972 val fnc = list_mk_pabs(xs,mk_select(y,P)) 1973 val bth = SYM(LIST_PBETA_CONV (list_mk_comb(fnc,xs))) 1974 val thm1 = 1975 SUBST[y |-> bth] P (SELECT_RULE(PSPECL xs (ASSUME tm))) 1976 val imp1 = DISCH tm (EXISTS (pat,fnc) (PGENL xs thm1)) 1977 val thm2 = PSPECL xs (ASSUME (snd(dest_exists pat))) 1978 val thm3 = PGENL xs (EXISTS (mk_exists(y,P),fx) thm2) 1979 val imp2 = DISCH pat (CHOOSE (f,ASSUME pat) thm3) 1980 in 1981 IMP_ANTISYM_RULE imp1 imp2 1982 end 1983 end 1984in 1985 fun P_PSKOLEM_CONV f = 1986 if not (is_vstruct f) then 1987 raise ERR"P_SKOLEM_CONV" "first argument not a variable pair" 1988 else 1989 fn tm => 1990 let val (xs,(y,P)) = (I##dest_pexists) (strip_pforall tm) 1991 handle HOL_ERR _ => raise ERR "P_SKOLEM_CONV" 1992 "expecting `!x1...xn. ?y.tm`" 1993 val FORALL_CONV = 1994 end_itlist 1995 (curry (op o)) 1996 (map (K (RAND_CONV o PABS_CONV)) xs) 1997 in 1998 if is_var f then 1999 if is_var y then 2000 BABY_P_PSKOLEM_CONV f tm 2001 else (* is_pair y *) 2002 let val y' = genvar (type_of y) 2003 val tha1 = 2004 (FORALL_CONV (RAND_CONV (PALPHA_CONV y'))) tm 2005 in 2006 CONV_RULE (RAND_CONV (BABY_P_PSKOLEM_CONV f)) tha1 2007 end 2008 else (* is_par f *) 2009 let val (f1,f2) = dest_pair f 2010 val thb1 = 2011 if is_var y then 2012 let val (y1',y2') = 2013 (genvar ## genvar) (dest_prod (type_of y)) 2014 handle HOL_ERR _ => raise 2015 ERR "P_PSKOLEM_CONV" 2016 "existential variable not of pair type" 2017 in 2018 (FORALL_CONV 2019 (RAND_CONV 2020 (PALPHA_CONV (mk_pair(y1',y2')))))tm 2021 end 2022 else 2023 REFL tm 2024 val thb2 = 2025 CONV_RULE 2026 (RAND_CONV (FORALL_CONV CURRY_EXISTS_CONV)) 2027 thb1 2028 val thb3 = CONV_RULE (RAND_CONV (P_PSKOLEM_CONV f1)) 2029 thb2 2030 val thb4 = CONV_RULE(RAND_CONV 2031 (RAND_CONV (PABS_CONV 2032 (P_PSKOLEM_CONV f2)))) 2033 thb3 2034 in 2035 CONV_RULE (RAND_CONV UNCURRY_EXISTS_CONV) thb4 2036 end 2037 end 2038end; 2039 2040(* ------------------------------------------------------------------------- *) 2041(* PSKOLEM_CONV : introduce a skolem function. *) 2042(* *) 2043(* |- (!x1...xn. ?y. tm[x1,...,xn,y]) *) 2044(* = *) 2045(* (?y'. !x1...xn. tm[x1,..,xn,f x1 ... xn] *) 2046(* *) 2047(* Where y' is a primed variant of y not free in the input term. *) 2048(* ------------------------------------------------------------------------- *) 2049 2050val PSKOLEM_CONV = 2051 let fun mkfn tm tyl = 2052 if is_var tm then 2053 let val (n,t) = dest_var tm 2054 in 2055 mk_var(n, itlist (curry (op -->)) tyl t) 2056 end 2057 else 2058 let val (p1,p2) = dest_pair tm 2059 in 2060 mk_pair(mkfn p1 tyl, mkfn p2 tyl) 2061 end 2062 in 2063 fn tm => 2064 let val (xs,(y,P)) = (I ## dest_pexists) (strip_pforall tm) 2065 val f = mkfn y (map type_of xs) 2066 val f' = pvariant (free_vars tm) f 2067 in 2068 P_PSKOLEM_CONV f' tm 2069 end 2070 end 2071handle HOL_ERR _ => failwith "PSKOLEM_CONV: expecting `!x1...xn. ?y.tm`"; 2072 2073(* end; Pair_exists *) 2074 2075(* ---------------------------------------------------------------------*) 2076(* CONTENTS: Functions which are common to both paired universal and *) 2077(* existential quantifications and which rely on more *) 2078(* primitive functions. *) 2079(* *) 2080(* Paired stripping tactics, same as basic ones, but they use PGEN_TAC *) 2081(* and PCHOOSE_THEN rather than GEN_TAC and CHOOSE_THEN *) 2082(* ---------------------------------------------------------------------*) 2083 2084(* structure Pair_both2 :> Pair_both2 = struct *) 2085 2086 2087val PSTRIP_THM_THEN = 2088 FIRST_TCL [CONJUNCTS_THEN, DISJ_CASES_THEN, PCHOOSE_THEN]; 2089 2090val PSTRIP_ASSUME_TAC = 2091 (REPEAT_TCL PSTRIP_THM_THEN) CHECK_ASSUME_TAC; 2092 2093val PSTRUCT_CASES_TAC = 2094 REPEAT_TCL PSTRIP_THM_THEN 2095 (fn th => SUBST1_TAC th ORELSE ASSUME_TAC th); 2096 2097fun PSTRIP_GOAL_THEN ttac = FIRST [PGEN_TAC, CONJ_TAC, DISCH_THEN ttac]; 2098 2099fun FILTER_PSTRIP_THEN ttac tm = 2100 FIRST [ 2101 FILTER_PGEN_TAC tm, 2102 FILTER_DISCH_THEN ttac tm, 2103 CONJ_TAC ]; 2104 2105val PSTRIP_TAC = PSTRIP_GOAL_THEN PSTRIP_ASSUME_TAC; 2106 2107val FILTER_PSTRIP_TAC = FILTER_PSTRIP_THEN PSTRIP_ASSUME_TAC; 2108 2109(* ------------------------------------------------------------------------- *) 2110(* A |- !p. (f p) = (g p) *) 2111(* ------------------------ PEXT *) 2112(* A |- f = g *) 2113(* ------------------------------------------------------------------------- *) 2114 2115fun PEXT th = 2116 let val (p,_) = dest_pforall (concl th) 2117 val p' = pvariant (thm_frees th) p 2118 val th1 = PSPEC p' th 2119 val th2 = PABS p' th1 2120 val th3 = (CONV_RULE (RATOR_CONV (RAND_CONV PETA_CONV))) th2 2121 in 2122 (CONV_RULE (RAND_CONV PETA_CONV)) th3 2123 end 2124handle HOL_ERR _ => failwith "PEXT"; 2125 2126(* ------------------------------------------------------------------------- *) 2127(* P_FUN_EQ_CONV "p" "f = g" = |- (f = g) = (!p. (f p) = (g p)) *) 2128(* ------------------------------------------------------------------------- *) 2129 2130val P_FUN_EQ_CONV = 2131 let val gpty = alpha 2132 val grange = beta 2133 val gfty = alpha --> beta 2134 val gf = genvar gfty 2135 val gg = genvar gfty 2136 val gp = genvar gpty 2137 val imp1 = DISCH_ALL (GEN gp (AP_THM (ASSUME (mk_eq(gf,gg))) gp)) 2138 val imp2 = DISCH_ALL (EXT (ASSUME 2139 (mk_forall(gp,mk_eq(mk_comb(gf,gp),mk_comb(gg,gp)))))) 2140 val ext_thm = IMP_ANTISYM_RULE imp1 imp2 2141 in 2142 fn p => 2143 fn tm => 2144 let val (f,g) = dest_eq tm 2145 val fty = type_of f 2146 and pty = type_of p 2147 val gfinst = mk_var((fst o dest_var)gf, fty) 2148 and gginst = mk_var((fst o dest_var)gg, fty) 2149 val rnge = hd (tl(snd(dest_type fty))) 2150 val th = 2151 INST_TY_TERM 2152 ([{residue=f,redex=gfinst},{residue=g,redex=gginst}], 2153 [{residue=pty,redex=gpty},{residue=rnge,redex=grange}]) 2154 ext_thm 2155 in 2156 (CONV_RULE (RAND_CONV (RAND_CONV (PALPHA_CONV p)))) th 2157 end 2158 end; 2159 2160 2161(* ------------------------------------------------------------------------- *) 2162(* A |- !p. t = u *) 2163(* ------------------------ MK_PABS *) 2164(* A |- (\p. t) = (\p. u) *) 2165(* ------------------------------------------------------------------------- *) 2166 2167fun MK_PABS th = 2168 let val (p,_) = dest_pforall (concl th) 2169 val th1 = (CONV_RULE (RAND_CONV (PABS_CONV (RATOR_CONV (RAND_CONV 2170 (UNPBETA_CONV p)))))) th 2171 val th2 = (CONV_RULE (RAND_CONV (PABS_CONV (RAND_CONV 2172 (UNPBETA_CONV p))))) th1 2173 val th3 = PEXT th2 2174 val th4 = (CONV_RULE (RATOR_CONV (RAND_CONV (PALPHA_CONV p)))) th3 2175 in 2176 (CONV_RULE (RAND_CONV (PALPHA_CONV p))) th4 2177 end 2178handle HOL_ERR _ => failwith "MK_PABS"; 2179 2180(* ------------------------------------------------------------------------- *) 2181(* A |- !p. t p = u *) 2182(* ------------------ HALF_MK_PABS *) 2183(* A |- t = (\p. u) *) 2184(* ------------------------------------------------------------------------- *) 2185 2186fun HALF_MK_PABS th = 2187 let val (p,_) = dest_pforall (concl th) 2188 val th1 = (CONV_RULE (RAND_CONV (PABS_CONV (RAND_CONV 2189 (UNPBETA_CONV p))))) th 2190 val th2 = PEXT th1 2191 in 2192 (CONV_RULE (RAND_CONV (PALPHA_CONV p))) th2 2193 end 2194handle HOL_ERR _ => failwith "HALF_MK_PABS" ; 2195 2196(* ------------------------------------------------------------------------- *) 2197(* A |- !p. t = u *) 2198(* ------------------------ MK_PFORALL *) 2199(* A |- (!p. t) = (!p. u) *) 2200(* ------------------------------------------------------------------------- *) 2201 2202fun MK_PFORALL th = 2203 let val (p,_) = dest_pforall (concl th) 2204 in 2205 AP_TERM 2206 (mk_const("!",(type_of p --> bool) --> bool)) 2207 (MK_PABS th) 2208 end 2209handle HOL_ERR _ => failwith "MK_PFORALL" ; 2210 2211 2212(* ------------------------------------------------------------------------- *) 2213(* A |- !p. t = u *) 2214(* ------------------------ MK_PEXISTS *) 2215(* A |- (?p. t) = (?p. u) *) 2216(* ------------------------------------------------------------------------- *) 2217 2218fun MK_PEXISTS th = 2219 let val (p,_) = dest_pforall (concl th) 2220 in 2221 AP_TERM 2222 (mk_const("?",(type_of p --> bool) --> bool)) 2223 (MK_PABS th) 2224 end 2225handle HOL_ERR _ => failwith "MK_PEXISTS" ; 2226 2227(* ------------------------------------------------------------------------- *) 2228(* A |- !p. t = u *) 2229(* ------------------------ MK_PSELECT *) 2230(* A |- (@p. t) = (@p. u) *) 2231(* ------------------------------------------------------------------------- *) 2232 2233fun MK_PSELECT th = 2234 let val (p,_) = dest_pforall (concl th) 2235 val pty = type_of p 2236 in 2237 AP_TERM 2238 (mk_const("@",(pty --> bool)--> pty)) 2239 (MK_PABS th) 2240 end 2241handle HOL_ERR _ => failwith "MK_PSELECT" ; 2242 2243(* ------------------------------------------------------------------------- *) 2244(* A |- t = u *) 2245(* ------------------------ PFORALL_EQ "p" *) 2246(* A |- (!p. t) = (!p. u) *) 2247(* ------------------------------------------------------------------------- *) 2248 2249fun PFORALL_EQ p th = 2250 let val pty = type_of p 2251 in 2252 AP_TERM 2253 (mk_const("!",(pty --> bool) --> bool)) 2254 (PABS p th) 2255 end 2256handle HOL_ERR _ => failwith "PFORALL_EQ" ; 2257 2258(* ------------------------------------------------------------------------- *) 2259(* A |- t = u *) 2260(* ------------------------ PEXISTS_EQ "p" *) 2261(* A |- (?p. t) = (?p. u) *) 2262(* ------------------------------------------------------------------------- *) 2263 2264fun PEXISTS_EQ p th = 2265 let val pty = type_of p 2266 in 2267 AP_TERM 2268 (mk_const("?",(pty --> bool) --> bool)) 2269 (PABS p th) 2270 end 2271handle HOL_ERR _ => failwith "PEXISTS_EQ" ; 2272 2273(* ------------------------------------------------------------------------- *) 2274(* A |- t = u *) 2275(* ------------------------ PSELECT_EQ "p" *) 2276(* A |- (@p. t) = (@p. u) *) 2277(* ------------------------------------------------------------------------- *) 2278 2279fun PSELECT_EQ p th = 2280 let val pty = type_of p 2281 in 2282 AP_TERM 2283 (mk_const("@",(pty --> bool) --> pty)) 2284 (PABS p th) 2285 end 2286handle HOL_ERR _ => failwith "PSELECT_EQ" ; 2287 2288(* ------------------------------------------------------------------------- *) 2289(* A |- t = u *) 2290(* ---------------------------------------- LIST_MK_PFORALL [p1;...pn] *) 2291(* A |- (!p1 ... pn. t) = (!p1 ... pn. u) *) 2292(* ------------------------------------------------------------------------- *) 2293 2294val LIST_MK_PFORALL = itlist PFORALL_EQ ; 2295 2296(* ------------------------------------------------------------------------- *) 2297(* A |- t = u *) 2298(* ---------------------------------------- LIST_MK_PEXISTS [p1;...pn] *) 2299(* A |- (?p1 ... pn. t) = (?p1 ... pn. u) *) 2300(* ------------------------------------------------------------------------- *) 2301 2302val LIST_MK_PEXISTS = itlist PEXISTS_EQ ; 2303 2304(* ------------------------------------------------------------------------- *) 2305(* A |- P ==> Q *) 2306(* -------------------------- EXISTS_IMP "p" *) 2307(* A |- (?p. P) ==> (?p. Q) *) 2308(* ------------------------------------------------------------------------- *) 2309 2310fun PEXISTS_IMP p th = 2311 let val (a,c) = dest_imp (concl th) 2312 val th1 = PEXISTS (mk_pexists(p,c),p) (UNDISCH th) 2313 val asm = mk_pexists(p,a) 2314 val th2 = DISCH asm (PCHOOSE (p, ASSUME asm) th1) 2315 in 2316 (CONV_RULE (RAND_CONV (GEN_PALPHA_CONV p))) th2 2317 end 2318handle HOL_ERR _ => failwith "PEXISTS_IMP"; 2319 2320(* ------------------------------------------------------------------------- *) 2321(* SWAP_PFORALL_CONV "!p q. t" = (|- (!p q. t) = (!q p. t)) *) 2322(* ------------------------------------------------------------------------- *) 2323 2324val genlike = genvarstruct o type_of; 2325 2326fun SWAP_PFORALL_CONV pqt = 2327 let val (p,qt) = dest_pforall pqt 2328 val (q,t) = dest_pforall qt 2329 val p' = genlike p 2330 val q' = genlike q 2331 val th1 = GEN_PALPHA_CONV p' pqt 2332 val th2 = CONV_RULE(RAND_CONV (RAND_CONV 2333 (PABS_CONV (GEN_PALPHA_CONV q')))) th1 2334 val t' = (snd o dest_pforall o snd o dest_pforall o rhs o concl)th2 2335 val pqt' = list_mk_pforall([p',q'],t') 2336 and qpt' = list_mk_pforall([q',p'],t') 2337 val th3 = IMP_ANTISYM_RULE 2338 ((DISCH pqt' o PGENL[q',p'] o PSPECL[p',q'] o ASSUME)pqt') 2339 ((DISCH qpt' o PGENL[p',q'] o PSPECL[q',p'] o ASSUME)qpt') 2340 val th4 = CONV_RULE(RAND_CONV(GEN_PALPHA_CONV q))th3 2341 val th5 = CONV_RULE(RAND_CONV (RAND_CONV 2342 (PABS_CONV (GEN_PALPHA_CONV p)))) th4 2343 in 2344 TRANS th2 th5 2345 end 2346handle HOL_ERR _ => failwith "SWAP_PFORALL_CONV"; 2347 2348 2349(* ------------------------------------------------------------------------- *) 2350(* SWAP_PEXISTS_CONV "?p q. t" = (|- (?p q. t) = (?q p. t)) *) 2351(* ------------------------------------------------------------------------- *) 2352 2353fun SWAP_PEXISTS_CONV xyt = 2354 let val (x,yt) = dest_pexists xyt 2355 val (y,t) = dest_pexists yt 2356 val xt = mk_pexists (x,t) 2357 val yxt = mk_pexists(y,xt) 2358 val t_thm = ASSUME t 2359 in 2360 IMP_ANTISYM_RULE 2361 (DISCH xyt (PCHOOSE (x,ASSUME xyt) (PCHOOSE (y, (ASSUME yt)) 2362 (PEXISTS (yxt,y) (PEXISTS (xt,x) t_thm))))) 2363 (DISCH yxt (PCHOOSE (y,ASSUME yxt) (PCHOOSE (x, (ASSUME xt)) 2364 (PEXISTS (xyt,x) (PEXISTS (yt,y) t_thm))))) 2365 end 2366handle HOL_ERR _ => failwith "SWAP_PEXISTS_CONV"; 2367 2368(* --------------------------------------------------------------------- *) 2369(* PART_PMATCH : just like PART_MATCH but doesn't mind leading paird q.s *) 2370(* --------------------------------------------------------------------- *) 2371 2372fun PART_PMATCH partfn th = 2373 let val pth = GPSPEC (GSPEC (GEN_ALL th)) 2374 val pat = partfn (concl pth) 2375 val matchfn = match_term pat 2376 in 2377 fn tm => INST_TY_TERM (matchfn tm) pth 2378 end; 2379 2380 2381(* --------------------------------------------------------------------- *) 2382(* A ?- !v1...vi. t' *) 2383(* ================== MATCH_MP_TAC (A' |- !x1...xn. s ==> !y1...tm. t) *) 2384(* A ?- ?z1...zp. s' *) 2385(* where z1, ..., zp are (type instances of) those variables among *) 2386(* x1, ..., xn that do not occur free in t. *) 2387(* --------------------------------------------------------------------- *) 2388 2389val PMATCH_MP_TAC : thm_tactic = 2390 let fun efn p (tm,th) = 2391 let val ntm = mk_pexists(p,tm) 2392 in 2393 (ntm, PCHOOSE (p, ASSUME ntm) th) 2394 end 2395 in 2396 fn thm => 2397 let val (tps,(ant,conseq)) = ((I ## dest_imp) o strip_pforall o concl) 2398 thm 2399 handle HOL_ERR _ => raise ERR "MATCH_MP_TAC" "not an implication" 2400 val (cps,con) = strip_forall conseq 2401 val th1 = PSPECL cps (UNDISCH (PSPECL tps thm)) 2402 val eps = filter (fn p => not (occs_in p con)) tps 2403 val th2 = uncurry DISCH (itlist efn eps (ant,th1)) 2404 in 2405 fn (A,g) => let 2406 val (gps,gl) = strip_pforall g 2407 val ins = match_term con gl 2408 handle HOL_ERR _ => 2409 raise ERR "PMATCH_MP_TAC" "no match" 2410 val ith = INST_TY_TERM ins th2 2411 val newg = fst(dest_imp(concl ith)) 2412 val gth = PGENL gps (UNDISCH ith) 2413 handle HOL_ERR _ => 2414 raise ERR "PMATCH_MP_TAC" "generalized pair(s)" 2415 fun just ths = 2416 case ths of 2417 [th] => PROVE_HYP th gth 2418 | _ => raise ERR "PMATCH_MP_TAC" "Justification Bind" 2419 in 2420 ([(A,newg)], just) 2421 end 2422 end 2423 end; 2424 2425 2426(* --------------------------------------------------------------------- *) 2427(* A1 |- !x1..xn. t1 ==> t2 A2 |- t1' *) 2428(* -------------------------------------- PMATCH_MP *) 2429(* A1 u A2 |- !xa..xk. t2' *) 2430(* --------------------------------------------------------------------- *) 2431 2432fun gen_assoc (keyf,resf)item = 2433 let fun assc (v::rst) = if (item = keyf v) then resf v else assc rst 2434 | assc [] = raise ERR "gen_assoc" "not found" 2435 in 2436 assc 2437 end; 2438 2439 2440val PMATCH_MP = 2441 let fun variants asl [] = [] 2442 | variants asl (h::t) = 2443 let val h' = variant (asl@(filter (fn e => not (e = h)) t)) h 2444 in {residue=h',redex=h}::(variants (h'::asl) t) 2445 end 2446 fun frev_assoc e2 (l:(''a,''a)subst) = gen_assoc(#redex,#residue)e2 l 2447 handle HOL_ERR _ => e2 2448 in 2449 fn ith => 2450 let val t = (fst o dest_imp o snd o strip_pforall o concl) ith 2451 handle HOL_ERR _ => raise ERR "PMATCH_MP" "not an implication" 2452 in 2453 fn th => 2454 let val (B,t') = dest_thm th 2455 val ty_inst = snd (match_term t t') 2456 val ith_ = INST_TYPE ty_inst ith 2457 val (A_, forall_ps_t_imp_u_) = dest_thm ith_ 2458 val (ps_,t_imp_u_) = strip_pforall forall_ps_t_imp_u_ 2459 val (t_,u_) = dest_imp (t_imp_u_) 2460 val pvs = free_varsl ps_ 2461 val A_vs = free_varsl A_ 2462 val B_vs = free_varsl B 2463 val tm_inst = fst (match_term t_ t') 2464 val (match_vs, unmatch_vs) = partition (C free_in t_) 2465 (free_vars u_) 2466 val rename = subtract unmatch_vs (subtract A_vs pvs) 2467 val new_vs = free_varsl (map (C frev_assoc tm_inst) match_vs) 2468 val renaming = variants (new_vs@A_vs@B_vs) rename 2469 val (specs,insts) = partition (C mem (free_varsl pvs) o #redex) 2470 (renaming@tm_inst) 2471 val spec_list = map (subst specs) ps_ 2472 val mp_th = MP (PSPECL spec_list (INST insts ith_)) th 2473 val gen_ps = (filter (fn p => null (subtract (strip_pair p) 2474 rename)) ps_) 2475 val qs = map (subst renaming) gen_ps 2476 in 2477 PGENL qs mp_th 2478 end 2479 end 2480 end 2481handle HOL_ERR _ => failwith "PMATCH_MP: can't instantiate theorem"; 2482 2483(* end; Pair_both2 *) 2484 2485end 2486