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 aconv 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 (aconv 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 (aconv 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 (aconv 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 (aconv 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 aconv 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 (aconv 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 1764 fun right t = 1765 is_pselect t andalso 1766 aconv (rhs (concl (PBETA_CONV (mk_comb(rand t,t))))) tm 1767 val epi = find_first right tm 1768 val (p,b) = dest_pselect epi 1769 in 1770 SYM (PEXISTS_CONV (mk_pexists(p,b))) 1771 end 1772 end 1773handle HOL_ERR _ => failwith "PSELECT_CONV" ; 1774 1775 1776(* ------------------------------------------------------------------------- *) 1777(* A |- t[@p .t[p]] *) 1778(* ------------------ PEXISTS_RULE *) 1779(* A |- ?p. t[p] *) 1780(* ------------------------------------------------------------------------- *) 1781 1782val PEXISTS_RULE = CONV_RULE PSELECT_CONV ; 1783 1784(* ------------------------------------------------------------------------- *) 1785(* A |- P t *) 1786(* -------------- PSELECT_INTRO *) 1787(* A |- P($@ P) *) 1788(* ------------------------------------------------------------------------- *) 1789 1790val PSELECT_INTRO = SELECT_INTRO ; 1791 1792(* ------------------------------------------------------------------------- *) 1793(* A1 |- f($@ f) , A2, f p |- t *) 1794(* -------------------------------- PSELECT_ELIM th1 ("p", th2) [p not free] *) 1795(* A1 u A2 |- t *) 1796(* ------------------------------------------------------------------------- *) 1797 1798fun PSELECT_ELIM th1 (v,th2) = 1799 let val (f,sf) = dest_comb (concl th1) 1800 val t1 = MP (PSPEC sf (PGEN v (DISCH (mk_comb(f,v)) th2))) th1 1801 val t2 = ALPHA (concl t1) (concl th2) 1802 in 1803 EQ_MP t2 t1 1804 end 1805handle HOL_ERR _ => failwith "PSELECT_ELIM" ; 1806 1807(* ------------------------------------------------------------------------- *) 1808(* A |- t[q] *) 1809(* ----------------- PEXISTS ("?p. t[p]", "q") *) 1810(* A |- ?p. t[p] *) 1811(* ------------------------------------------------------------------------- *) 1812 1813fun PEXISTS (fm,tm) th = 1814 let val (p,b) = dest_pexists fm 1815 val th1 = PBETA_CONV (mk_comb(mk_pabs(p,b),tm)) 1816 val th2 = EQ_MP (SYM th1) th 1817 val th3 = PSELECT_INTRO th2 1818 val th4 = AP_THM(INST_TYPE [alpha |-> type_of p] EXISTS_DEF) 1819 (mk_pabs(p, b)) 1820 val th5 = TRANS th4 (BETA_CONV(rhs(concl th4))) 1821 in 1822 EQ_MP (SYM th5) th3 1823 end 1824handle HOL_ERR _ => failwith "PEXISTS" ; 1825 1826(* ------------------------------------------------------------------------- *) 1827(* A1 |- ?p. t[p] , A2, t[v] |- u *) 1828(* ---------------------------------- PCHOOSE (v,th1) th2 [v not free] *) 1829(* A1 u A2 |- u *) 1830(* ------------------------------------------------------------------------- *) 1831 1832val PCHOOSE = 1833 let val f = mk_var("f", alpha --> bool) 1834 val t1 = AP_THM EXISTS_DEF f 1835 val t2 = GEN f ((CONV_RULE (RAND_CONV BETA_CONV)) t1) 1836 in 1837 fn (v,th1) => 1838 fn th2 => 1839 let val p = rand (concl th1) 1840 val th1' = EQ_MP (ISPEC p t2) th1 1841 val u1 = UNDISCH (fst 1842 (EQ_IMP_RULE (PBETA_CONV (mk_comb(p,v))))) 1843 val th2' = PROVE_HYP u1 th2 1844 in 1845 PSELECT_ELIM th1' (v,th2') 1846 end 1847 end 1848handle HOL_ERR _ => failwith "PCHOOSE" ; 1849 1850fun P_PCHOOSE_THEN v ttac pth :tactic = 1851 let val (p,b) = dest_pexists (concl pth) 1852 handle HOL_ERR _ => failwith "P_PCHOOSE_THEN" 1853 in 1854 fn (asl,w) => 1855 let val th = itlist ADD_ASSUM (hyp pth) 1856 (ASSUME 1857 (rhs(concl(PBETA_CONV 1858 (mk_comb(mk_pabs(p,b),v)))))) 1859 val (gl,prf) = ttac th (asl,w) 1860 in 1861 (gl, (PCHOOSE (v, pth)) o prf) 1862 end 1863 end; 1864 1865fun PCHOOSE_THEN ttac pth :tactic = 1866 let val (p,b) = dest_pexists (concl pth) 1867 handle HOL_ERR _ => failwith "CHOOSE_THEN" 1868 in 1869 fn (asl,w) => 1870 let val q = pvariant ((thm_frees pth) @ (free_varsl (w::asl))) p 1871 val th = 1872 itlist 1873 ADD_ASSUM 1874 (hyp pth) 1875 (ASSUME 1876 (rhs (concl 1877 (PairedLambda.PAIRED_BETA_CONV 1878 (mk_comb(mk_pabs(p,b),q)))))) 1879 val (gl,prf) = ttac th (asl,w) 1880 in 1881 (gl, (PCHOOSE (q, pth)) o prf) 1882 end 1883 end; 1884 1885 1886fun P_PCHOOSE_TAC p = P_PCHOOSE_THEN p ASSUME_TAC ; 1887 1888val PCHOOSE_TAC = PCHOOSE_THEN ASSUME_TAC ; 1889 1890(* ------------------------------------------------------------------------- *) 1891(* A ?- ?p. t[p] *) 1892(* =============== PEXISTS_TAC "u" *) 1893(* A ?- t[u] *) 1894(* ------------------------------------------------------------------------- *) 1895 1896fun PEXISTS_TAC v (a,t) = let 1897 val (p,b) = dest_pexists t 1898 fun just ths = 1899 case ths of 1900 [th] => PEXISTS (t,v) th 1901 | _ => raise ERR "PEXISTS_TAC" "Justification Bind" 1902in 1903 ([(a, rhs (concl (PBETA_CONV (mk_comb(mk_pabs(p,b),v)))))], just) 1904end 1905handle HOL_ERR _ => failwith "PEXISTS_TAC" ; 1906 1907(* ------------------------------------------------------------------------- *) 1908(* |- ?!p. t[p] *) 1909(* -------------- PEXISTENCE *) 1910(* |- ?p. t[p] *) 1911(* ------------------------------------------------------------------------- *) 1912 1913fun PEXISTENCE th = 1914 let val (p,b) = dest_pabs (rand (concl th)) 1915 val th1 = 1916 AP_THM 1917 (INST_TYPE [alpha |-> type_of p] EXISTS_UNIQUE_DEF) (mk_pabs(p,b)) 1918 val th2 = EQ_MP th1 th 1919 val th3 = CONV_RULE BETA_CONV th2 1920 in 1921 CONJUNCT1 th3 1922 end 1923handle HOL_ERR _ => failwith "PEXISTENCE" ; 1924 1925(* ------------------------------------------------------------------------- *) 1926(* PEXISTS_UNIQUE_CONV "?!p. t[p]" = *) 1927(* (|- (?!p. t[p]) = (?p. t[p] /\ !p p'. t[p] /\ t[p'] ==> (p='p))) *) 1928(* ------------------------------------------------------------------------- *) 1929 1930fun PEXISTS_UNIQUE_CONV tm = 1931 let val (p,b) = dest_pabs (rand tm) 1932 val p' = pvariant (p::(free_vars tm)) p 1933 val th1 = 1934 AP_THM 1935 (INST_TYPE [alpha |-> type_of p] EXISTS_UNIQUE_DEF) (mk_pabs(p,b)) 1936 val th2 = CONV_RULE (RAND_CONV BETA_CONV) th1 1937 val th3 = CONV_RULE (RAND_CONV (RAND_CONV (RAND_CONV (ABS_CONV 1938 (GEN_PALPHA_CONV p'))))) th2 1939 val th4 = CONV_RULE (RAND_CONV (RAND_CONV (GEN_PALPHA_CONV p))) th3 1940 val th5 = CONV_RULE (RAND_CONV (RAND_CONV (RAND_CONV (PABS_CONV 1941 (RAND_CONV (PABS_CONV (RATOR_CONV (RAND_CONV 1942 (RATOR_CONV (RAND_CONV PBETA_CONV)))))))))) th4 1943 in 1944 CONV_RULE (RAND_CONV (RAND_CONV (RAND_CONV (PABS_CONV 1945 (RAND_CONV (PABS_CONV (RATOR_CONV (RAND_CONV 1946 (RAND_CONV PBETA_CONV))))))))) th5 1947 end 1948handle HOL_ERR _ => failwith "PEXISTS_UNIQUE_CONV" ; 1949 1950(* ------------------------------------------------------------------------- *) 1951(* P_PSKOLEM_CONV : introduce a skolem function. *) 1952(* *) 1953(* |- (!x1...xn. ?y. tm[x1,...,xn,y]) *) 1954(* = *) 1955(* (?f. !x1...xn. tm[x1,..,xn,f x1 ... xn] *) 1956(* *) 1957(* The first argument is the function f. *) 1958(* ------------------------------------------------------------------------- *) 1959 1960local fun BABY_P_PSKOLEM_CONV f = 1961 if not(is_vstruct f) then 1962 raise ERR "P_SKOLEM_CONV" "first argument not a varstruct" 1963 else 1964 fn tm => 1965 let val (xs,(y,P)) = (I ## dest_exists) (strip_pforall tm) 1966 val fx = with_exn list_mk_comb(f,xs) 1967 (ERR"P_SKOLEM_CONV" "function variable has the wrong type") 1968 in 1969 if free_in f tm then 1970 raise ERR "P_SKOLEM_CONV" 1971 "skolem function free in the input term" 1972 else 1973 let val pat = mk_exists(f,list_mk_pforall(xs,subst[y |-> fx]P)) 1974 val fnc = list_mk_pabs(xs,mk_select(y,P)) 1975 val bth = SYM(LIST_PBETA_CONV (list_mk_comb(fnc,xs))) 1976 val thm1 = 1977 SUBST[y |-> bth] P (SELECT_RULE(PSPECL xs (ASSUME tm))) 1978 val imp1 = DISCH tm (EXISTS (pat,fnc) (PGENL xs thm1)) 1979 val thm2 = PSPECL xs (ASSUME (snd(dest_exists pat))) 1980 val thm3 = PGENL xs (EXISTS (mk_exists(y,P),fx) thm2) 1981 val imp2 = DISCH pat (CHOOSE (f,ASSUME pat) thm3) 1982 in 1983 IMP_ANTISYM_RULE imp1 imp2 1984 end 1985 end 1986in 1987 fun P_PSKOLEM_CONV f = 1988 if not (is_vstruct f) then 1989 raise ERR"P_SKOLEM_CONV" "first argument not a variable pair" 1990 else 1991 fn tm => 1992 let val (xs,(y,P)) = (I##dest_pexists) (strip_pforall tm) 1993 handle HOL_ERR _ => raise ERR "P_SKOLEM_CONV" 1994 "expecting `!x1...xn. ?y.tm`" 1995 val FORALL_CONV = 1996 end_itlist 1997 (curry (op o)) 1998 (map (K (RAND_CONV o PABS_CONV)) xs) 1999 in 2000 if is_var f then 2001 if is_var y then 2002 BABY_P_PSKOLEM_CONV f tm 2003 else (* is_pair y *) 2004 let val y' = genvar (type_of y) 2005 val tha1 = 2006 (FORALL_CONV (RAND_CONV (PALPHA_CONV y'))) tm 2007 in 2008 CONV_RULE (RAND_CONV (BABY_P_PSKOLEM_CONV f)) tha1 2009 end 2010 else (* is_par f *) 2011 let val (f1,f2) = dest_pair f 2012 val thb1 = 2013 if is_var y then 2014 let val (y1',y2') = 2015 (genvar ## genvar) (dest_prod (type_of y)) 2016 handle HOL_ERR _ => raise 2017 ERR "P_PSKOLEM_CONV" 2018 "existential variable not of pair type" 2019 in 2020 (FORALL_CONV 2021 (RAND_CONV 2022 (PALPHA_CONV (mk_pair(y1',y2')))))tm 2023 end 2024 else 2025 REFL tm 2026 val thb2 = 2027 CONV_RULE 2028 (RAND_CONV (FORALL_CONV CURRY_EXISTS_CONV)) 2029 thb1 2030 val thb3 = CONV_RULE (RAND_CONV (P_PSKOLEM_CONV f1)) 2031 thb2 2032 val thb4 = CONV_RULE(RAND_CONV 2033 (RAND_CONV (PABS_CONV 2034 (P_PSKOLEM_CONV f2)))) 2035 thb3 2036 in 2037 CONV_RULE (RAND_CONV UNCURRY_EXISTS_CONV) thb4 2038 end 2039 end 2040end; 2041 2042(* ------------------------------------------------------------------------- *) 2043(* PSKOLEM_CONV : introduce a skolem function. *) 2044(* *) 2045(* |- (!x1...xn. ?y. tm[x1,...,xn,y]) *) 2046(* = *) 2047(* (?y'. !x1...xn. tm[x1,..,xn,f x1 ... xn] *) 2048(* *) 2049(* Where y' is a primed variant of y not free in the input term. *) 2050(* ------------------------------------------------------------------------- *) 2051 2052val PSKOLEM_CONV = 2053 let fun mkfn tm tyl = 2054 if is_var tm then 2055 let val (n,t) = dest_var tm 2056 in 2057 mk_var(n, itlist (curry (op -->)) tyl t) 2058 end 2059 else 2060 let val (p1,p2) = dest_pair tm 2061 in 2062 mk_pair(mkfn p1 tyl, mkfn p2 tyl) 2063 end 2064 in 2065 fn tm => 2066 let val (xs,(y,P)) = (I ## dest_pexists) (strip_pforall tm) 2067 val f = mkfn y (map type_of xs) 2068 val f' = pvariant (free_vars tm) f 2069 in 2070 P_PSKOLEM_CONV f' tm 2071 end 2072 end 2073handle HOL_ERR _ => failwith "PSKOLEM_CONV: expecting `!x1...xn. ?y.tm`"; 2074 2075(* end; Pair_exists *) 2076 2077(* ---------------------------------------------------------------------*) 2078(* CONTENTS: Functions which are common to both paired universal and *) 2079(* existential quantifications and which rely on more *) 2080(* primitive functions. *) 2081(* *) 2082(* Paired stripping tactics, same as basic ones, but they use PGEN_TAC *) 2083(* and PCHOOSE_THEN rather than GEN_TAC and CHOOSE_THEN *) 2084(* ---------------------------------------------------------------------*) 2085 2086(* structure Pair_both2 :> Pair_both2 = struct *) 2087 2088 2089val PSTRIP_THM_THEN = 2090 FIRST_TCL [CONJUNCTS_THEN, DISJ_CASES_THEN, PCHOOSE_THEN]; 2091 2092val PSTRIP_ASSUME_TAC = 2093 (REPEAT_TCL PSTRIP_THM_THEN) CHECK_ASSUME_TAC; 2094 2095val PSTRUCT_CASES_TAC = 2096 REPEAT_TCL PSTRIP_THM_THEN 2097 (fn th => SUBST1_TAC th ORELSE ASSUME_TAC th); 2098 2099fun PSTRIP_GOAL_THEN ttac = FIRST [PGEN_TAC, CONJ_TAC, DISCH_THEN ttac]; 2100 2101fun FILTER_PSTRIP_THEN ttac tm = 2102 FIRST [ 2103 FILTER_PGEN_TAC tm, 2104 FILTER_DISCH_THEN ttac tm, 2105 CONJ_TAC ]; 2106 2107val PSTRIP_TAC = PSTRIP_GOAL_THEN PSTRIP_ASSUME_TAC; 2108 2109val FILTER_PSTRIP_TAC = FILTER_PSTRIP_THEN PSTRIP_ASSUME_TAC; 2110 2111(* ------------------------------------------------------------------------- *) 2112(* A |- !p. (f p) = (g p) *) 2113(* ------------------------ PEXT *) 2114(* A |- f = g *) 2115(* ------------------------------------------------------------------------- *) 2116 2117fun PEXT th = 2118 let val (p,_) = dest_pforall (concl th) 2119 val p' = pvariant (thm_frees th) p 2120 val th1 = PSPEC p' th 2121 val th2 = PABS p' th1 2122 val th3 = (CONV_RULE (RATOR_CONV (RAND_CONV PETA_CONV))) th2 2123 in 2124 (CONV_RULE (RAND_CONV PETA_CONV)) th3 2125 end 2126handle HOL_ERR _ => failwith "PEXT"; 2127 2128(* ------------------------------------------------------------------------- *) 2129(* P_FUN_EQ_CONV "p" "f = g" = |- (f = g) = (!p. (f p) = (g p)) *) 2130(* ------------------------------------------------------------------------- *) 2131 2132val P_FUN_EQ_CONV = 2133 let val gpty = alpha 2134 val grange = beta 2135 val gfty = alpha --> beta 2136 val gf = genvar gfty 2137 val gg = genvar gfty 2138 val gp = genvar gpty 2139 val imp1 = DISCH_ALL (GEN gp (AP_THM (ASSUME (mk_eq(gf,gg))) gp)) 2140 val imp2 = DISCH_ALL (EXT (ASSUME 2141 (mk_forall(gp,mk_eq(mk_comb(gf,gp),mk_comb(gg,gp)))))) 2142 val ext_thm = IMP_ANTISYM_RULE imp1 imp2 2143 in 2144 fn p => 2145 fn tm => 2146 let val (f,g) = dest_eq tm 2147 val fty = type_of f 2148 and pty = type_of p 2149 val gfinst = mk_var((fst o dest_var)gf, fty) 2150 and gginst = mk_var((fst o dest_var)gg, fty) 2151 val rnge = hd (tl(snd(dest_type fty))) 2152 val th = 2153 INST_TY_TERM 2154 ([{residue=f,redex=gfinst},{residue=g,redex=gginst}], 2155 [{residue=pty,redex=gpty},{residue=rnge,redex=grange}]) 2156 ext_thm 2157 in 2158 (CONV_RULE (RAND_CONV (RAND_CONV (PALPHA_CONV p)))) th 2159 end 2160 end; 2161 2162 2163(* ------------------------------------------------------------------------- *) 2164(* A |- !p. t = u *) 2165(* ------------------------ MK_PABS *) 2166(* A |- (\p. t) = (\p. u) *) 2167(* ------------------------------------------------------------------------- *) 2168 2169fun MK_PABS th = 2170 let val (p,_) = dest_pforall (concl th) 2171 val th1 = (CONV_RULE (RAND_CONV (PABS_CONV (RATOR_CONV (RAND_CONV 2172 (UNPBETA_CONV p)))))) th 2173 val th2 = (CONV_RULE (RAND_CONV (PABS_CONV (RAND_CONV 2174 (UNPBETA_CONV p))))) th1 2175 val th3 = PEXT th2 2176 val th4 = (CONV_RULE (RATOR_CONV (RAND_CONV (PALPHA_CONV p)))) th3 2177 in 2178 (CONV_RULE (RAND_CONV (PALPHA_CONV p))) th4 2179 end 2180handle HOL_ERR _ => failwith "MK_PABS"; 2181 2182(* ------------------------------------------------------------------------- *) 2183(* A |- !p. t p = u *) 2184(* ------------------ HALF_MK_PABS *) 2185(* A |- t = (\p. u) *) 2186(* ------------------------------------------------------------------------- *) 2187 2188fun HALF_MK_PABS th = 2189 let val (p,_) = dest_pforall (concl th) 2190 val th1 = (CONV_RULE (RAND_CONV (PABS_CONV (RAND_CONV 2191 (UNPBETA_CONV p))))) th 2192 val th2 = PEXT th1 2193 in 2194 (CONV_RULE (RAND_CONV (PALPHA_CONV p))) th2 2195 end 2196handle HOL_ERR _ => failwith "HALF_MK_PABS" ; 2197 2198(* ------------------------------------------------------------------------- *) 2199(* A |- !p. t = u *) 2200(* ------------------------ MK_PFORALL *) 2201(* A |- (!p. t) = (!p. u) *) 2202(* ------------------------------------------------------------------------- *) 2203 2204fun MK_PFORALL th = 2205 let val (p,_) = dest_pforall (concl th) 2206 in 2207 AP_TERM 2208 (mk_const("!",(type_of p --> bool) --> bool)) 2209 (MK_PABS th) 2210 end 2211handle HOL_ERR _ => failwith "MK_PFORALL" ; 2212 2213 2214(* ------------------------------------------------------------------------- *) 2215(* A |- !p. t = u *) 2216(* ------------------------ MK_PEXISTS *) 2217(* A |- (?p. t) = (?p. u) *) 2218(* ------------------------------------------------------------------------- *) 2219 2220fun MK_PEXISTS th = 2221 let val (p,_) = dest_pforall (concl th) 2222 in 2223 AP_TERM 2224 (mk_const("?",(type_of p --> bool) --> bool)) 2225 (MK_PABS th) 2226 end 2227handle HOL_ERR _ => failwith "MK_PEXISTS" ; 2228 2229(* ------------------------------------------------------------------------- *) 2230(* A |- !p. t = u *) 2231(* ------------------------ MK_PSELECT *) 2232(* A |- (@p. t) = (@p. u) *) 2233(* ------------------------------------------------------------------------- *) 2234 2235fun MK_PSELECT th = 2236 let val (p,_) = dest_pforall (concl th) 2237 val pty = type_of p 2238 in 2239 AP_TERM 2240 (mk_const("@",(pty --> bool)--> pty)) 2241 (MK_PABS th) 2242 end 2243handle HOL_ERR _ => failwith "MK_PSELECT" ; 2244 2245(* ------------------------------------------------------------------------- *) 2246(* A |- t = u *) 2247(* ------------------------ PFORALL_EQ "p" *) 2248(* A |- (!p. t) = (!p. u) *) 2249(* ------------------------------------------------------------------------- *) 2250 2251fun PFORALL_EQ p th = 2252 let val pty = type_of p 2253 in 2254 AP_TERM 2255 (mk_const("!",(pty --> bool) --> bool)) 2256 (PABS p th) 2257 end 2258handle HOL_ERR _ => failwith "PFORALL_EQ" ; 2259 2260(* ------------------------------------------------------------------------- *) 2261(* A |- t = u *) 2262(* ------------------------ PEXISTS_EQ "p" *) 2263(* A |- (?p. t) = (?p. u) *) 2264(* ------------------------------------------------------------------------- *) 2265 2266fun PEXISTS_EQ p th = 2267 let val pty = type_of p 2268 in 2269 AP_TERM 2270 (mk_const("?",(pty --> bool) --> bool)) 2271 (PABS p th) 2272 end 2273handle HOL_ERR _ => failwith "PEXISTS_EQ" ; 2274 2275(* ------------------------------------------------------------------------- *) 2276(* A |- t = u *) 2277(* ------------------------ PSELECT_EQ "p" *) 2278(* A |- (@p. t) = (@p. u) *) 2279(* ------------------------------------------------------------------------- *) 2280 2281fun PSELECT_EQ p th = 2282 let val pty = type_of p 2283 in 2284 AP_TERM 2285 (mk_const("@",(pty --> bool) --> pty)) 2286 (PABS p th) 2287 end 2288handle HOL_ERR _ => failwith "PSELECT_EQ" ; 2289 2290(* ------------------------------------------------------------------------- *) 2291(* A |- t = u *) 2292(* ---------------------------------------- LIST_MK_PFORALL [p1;...pn] *) 2293(* A |- (!p1 ... pn. t) = (!p1 ... pn. u) *) 2294(* ------------------------------------------------------------------------- *) 2295 2296val LIST_MK_PFORALL = itlist PFORALL_EQ ; 2297 2298(* ------------------------------------------------------------------------- *) 2299(* A |- t = u *) 2300(* ---------------------------------------- LIST_MK_PEXISTS [p1;...pn] *) 2301(* A |- (?p1 ... pn. t) = (?p1 ... pn. u) *) 2302(* ------------------------------------------------------------------------- *) 2303 2304val LIST_MK_PEXISTS = itlist PEXISTS_EQ ; 2305 2306(* ------------------------------------------------------------------------- *) 2307(* A |- P ==> Q *) 2308(* -------------------------- EXISTS_IMP "p" *) 2309(* A |- (?p. P) ==> (?p. Q) *) 2310(* ------------------------------------------------------------------------- *) 2311 2312fun PEXISTS_IMP p th = 2313 let val (a,c) = dest_imp (concl th) 2314 val th1 = PEXISTS (mk_pexists(p,c),p) (UNDISCH th) 2315 val asm = mk_pexists(p,a) 2316 val th2 = DISCH asm (PCHOOSE (p, ASSUME asm) th1) 2317 in 2318 (CONV_RULE (RAND_CONV (GEN_PALPHA_CONV p))) th2 2319 end 2320handle HOL_ERR _ => failwith "PEXISTS_IMP"; 2321 2322(* ------------------------------------------------------------------------- *) 2323(* SWAP_PFORALL_CONV "!p q. t" = (|- (!p q. t) = (!q p. t)) *) 2324(* ------------------------------------------------------------------------- *) 2325 2326val genlike = genvarstruct o type_of; 2327 2328fun SWAP_PFORALL_CONV pqt = 2329 let val (p,qt) = dest_pforall pqt 2330 val (q,t) = dest_pforall qt 2331 val p' = genlike p 2332 val q' = genlike q 2333 val th1 = GEN_PALPHA_CONV p' pqt 2334 val th2 = CONV_RULE(RAND_CONV (RAND_CONV 2335 (PABS_CONV (GEN_PALPHA_CONV q')))) th1 2336 val t' = (snd o dest_pforall o snd o dest_pforall o rhs o concl)th2 2337 val pqt' = list_mk_pforall([p',q'],t') 2338 and qpt' = list_mk_pforall([q',p'],t') 2339 val th3 = IMP_ANTISYM_RULE 2340 ((DISCH pqt' o PGENL[q',p'] o PSPECL[p',q'] o ASSUME)pqt') 2341 ((DISCH qpt' o PGENL[p',q'] o PSPECL[q',p'] o ASSUME)qpt') 2342 val th4 = CONV_RULE(RAND_CONV(GEN_PALPHA_CONV q))th3 2343 val th5 = CONV_RULE(RAND_CONV (RAND_CONV 2344 (PABS_CONV (GEN_PALPHA_CONV p)))) th4 2345 in 2346 TRANS th2 th5 2347 end 2348handle HOL_ERR _ => failwith "SWAP_PFORALL_CONV"; 2349 2350 2351(* ------------------------------------------------------------------------- *) 2352(* SWAP_PEXISTS_CONV "?p q. t" = (|- (?p q. t) = (?q p. t)) *) 2353(* ------------------------------------------------------------------------- *) 2354 2355fun SWAP_PEXISTS_CONV xyt = 2356 let val (x,yt) = dest_pexists xyt 2357 val (y,t) = dest_pexists yt 2358 val xt = mk_pexists (x,t) 2359 val yxt = mk_pexists(y,xt) 2360 val t_thm = ASSUME t 2361 in 2362 IMP_ANTISYM_RULE 2363 (DISCH xyt (PCHOOSE (x,ASSUME xyt) (PCHOOSE (y, (ASSUME yt)) 2364 (PEXISTS (yxt,y) (PEXISTS (xt,x) t_thm))))) 2365 (DISCH yxt (PCHOOSE (y,ASSUME yxt) (PCHOOSE (x, (ASSUME xt)) 2366 (PEXISTS (xyt,x) (PEXISTS (yt,y) t_thm))))) 2367 end 2368handle HOL_ERR _ => failwith "SWAP_PEXISTS_CONV"; 2369 2370(* --------------------------------------------------------------------- *) 2371(* PART_PMATCH : just like PART_MATCH but doesn't mind leading paird q.s *) 2372(* --------------------------------------------------------------------- *) 2373 2374fun PART_PMATCH partfn th = 2375 let val pth = GPSPEC (GSPEC (GEN_ALL th)) 2376 val pat = partfn (concl pth) 2377 val matchfn = match_term pat 2378 in 2379 fn tm => INST_TY_TERM (matchfn tm) pth 2380 end; 2381 2382 2383(* --------------------------------------------------------------------- *) 2384(* A ?- !v1...vi. t' *) 2385(* ================== MATCH_MP_TAC (A' |- !x1...xn. s ==> !y1...tm. t) *) 2386(* A ?- ?z1...zp. s' *) 2387(* where z1, ..., zp are (type instances of) those variables among *) 2388(* x1, ..., xn that do not occur free in t. *) 2389(* --------------------------------------------------------------------- *) 2390 2391val PMATCH_MP_TAC : thm_tactic = 2392 let fun efn p (tm,th) = 2393 let val ntm = mk_pexists(p,tm) 2394 in 2395 (ntm, PCHOOSE (p, ASSUME ntm) th) 2396 end 2397 in 2398 fn thm => 2399 let val (tps,(ant,conseq)) = ((I ## dest_imp) o strip_pforall o concl) 2400 thm 2401 handle HOL_ERR _ => raise ERR "MATCH_MP_TAC" "not an implication" 2402 val (cps,con) = strip_forall conseq 2403 val th1 = PSPECL cps (UNDISCH (PSPECL tps thm)) 2404 val eps = filter (fn p => not (occs_in p con)) tps 2405 val th2 = uncurry DISCH (itlist efn eps (ant,th1)) 2406 in 2407 fn (A,g) => let 2408 val (gps,gl) = strip_pforall g 2409 val ins = match_term con gl 2410 handle HOL_ERR _ => 2411 raise ERR "PMATCH_MP_TAC" "no match" 2412 val ith = INST_TY_TERM ins th2 2413 val newg = fst(dest_imp(concl ith)) 2414 val gth = PGENL gps (UNDISCH ith) 2415 handle HOL_ERR _ => 2416 raise ERR "PMATCH_MP_TAC" "generalized pair(s)" 2417 fun just ths = 2418 case ths of 2419 [th] => PROVE_HYP th gth 2420 | _ => raise ERR "PMATCH_MP_TAC" "Justification Bind" 2421 in 2422 ([(A,newg)], just) 2423 end 2424 end 2425 end; 2426 2427 2428(* --------------------------------------------------------------------- *) 2429(* A1 |- !x1..xn. t1 ==> t2 A2 |- t1' *) 2430(* -------------------------------------- PMATCH_MP *) 2431(* A1 u A2 |- !xa..xk. t2' *) 2432(* --------------------------------------------------------------------- *) 2433 2434fun gen_assoc (keyf,resf)item = 2435 let fun assc (v::rst) = if aconv item (keyf v) then resf v else assc rst 2436 | assc [] = raise ERR "gen_assoc" "not found" 2437 in 2438 assc 2439 end; 2440 2441 2442val PMATCH_MP = 2443 let fun variants asl [] = [] 2444 | variants asl (h::t) = 2445 let val h' = variant (asl@(filter (fn e => not (aconv e h)) t)) h 2446 in {residue=h',redex=h}::(variants (h'::asl) t) 2447 end 2448 fun frev_assoc e2 (l:(term,term)subst) = gen_assoc(#redex,#residue)e2 l 2449 handle HOL_ERR _ => e2 2450 in 2451 fn ith => 2452 let val t = (fst o dest_imp o snd o strip_pforall o concl) ith 2453 handle HOL_ERR _ => raise ERR "PMATCH_MP" "not an implication" 2454 in 2455 fn th => 2456 let val (B,t') = dest_thm th 2457 val ty_inst = snd (match_term t t') 2458 val ith_ = INST_TYPE ty_inst ith 2459 val (A_, forall_ps_t_imp_u_) = dest_thm ith_ 2460 val (ps_,t_imp_u_) = strip_pforall forall_ps_t_imp_u_ 2461 val (t_,u_) = dest_imp (t_imp_u_) 2462 val pvs = free_varsl ps_ 2463 val A_vs = free_varsl A_ 2464 val B_vs = free_varsl B 2465 val tm_inst = fst (match_term t_ t') 2466 val (match_vs, unmatch_vs) = partition (C free_in t_) 2467 (free_vars u_) 2468 val rename = 2469 op_set_diff aconv unmatch_vs (op_set_diff aconv A_vs pvs) 2470 val new_vs = free_varsl (map (C frev_assoc tm_inst) match_vs) 2471 val renaming = variants (new_vs@A_vs@B_vs) rename 2472 val (specs,insts) = 2473 partition (C (op_mem aconv) (free_varsl pvs) o #redex) 2474 (renaming@tm_inst) 2475 val spec_list = map (subst specs) ps_ 2476 val mp_th = MP (PSPECL spec_list (INST insts ith_)) th 2477 val gen_ps = 2478 filter (fn p => null (op_set_diff aconv 2479 (strip_pair p) 2480 rename)) 2481 ps_ 2482 val qs = map (subst renaming) gen_ps 2483 in 2484 PGENL qs mp_th 2485 end 2486 end 2487 end 2488handle HOL_ERR _ => failwith "PMATCH_MP: can't instantiate theorem"; 2489 2490(* end; Pair_both2 *) 2491 2492end 2493