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