bool.ml

   1 (* ========================================================================= *)
   2 (* Boolean theory including (intuitionistic) defs of logical connectives.    *)
   3 (*                                                                           *)
   4 (*       John Harrison, University of Cambridge Computer Laboratory          *)
   5 (*                                                                           *)
   6 (*            (c) Copyright, University of Cambridge 1998                    *)
   7 (*              (c) Copyright, John Harrison 1998-2007                       *)
   8 (* ========================================================================= *)
   9
  10 needs "equal.ml";;
  11
  12 (* ------------------------------------------------------------------------- *)
  13 (* Set up parse status of basic and derived logical constants.               *)
  14 (* ------------------------------------------------------------------------- *)
  15
  16 parse_as_prefix "~";;
  17
  18 parse_as_binder "\\";;
  19 parse_as_binder "!";;
  20 parse_as_binder "?";;
  21 parse_as_binder "?!";;
  22
  23 parse_as_infix ("==>",(4,"right"));;
  24 parse_as_infix ("\\/",(6,"right"));;
  25 parse_as_infix ("/\\",(8,"right"));;
  26
  27 (* ------------------------------------------------------------------------- *)
  28 (* Set up more orthodox notation for equations and equivalence.              *)
  29 (* ------------------------------------------------------------------------- *)
  30
  31 parse_as_infix("<=>",(2,"right"));;
  32 override_interface ("<=>",`(=):bool->bool->bool`);;
  33 parse_as_infix("=",(12,"right"));;
  34
  35 (* ------------------------------------------------------------------------- *)
  36 (* Special syntax for Boolean equations (IFF).                               *)
  37 (* ------------------------------------------------------------------------- *)
  38
  39 let is_iff tm =
  40   match tm with
  41     Comb(Comb(Const("=",Tyapp("fun",[Tyapp("bool",[]);_])),l),r) -> true
  42   | _ -> false;;
  43
  44 let dest_iff tm =
  45   match tm with
  46     Comb(Comb(Const("=",Tyapp("fun",[Tyapp("bool",[]);_])),l),r) -> (l,r)
  47   | _ -> failwith "dest_iff";;
  48
  49 let mk_iff =
  50   let eq_tm = `(<=>)` in
  51   fun (l,r) -> mk_comb(mk_comb(eq_tm,l),r);;
  52
  53 (* ------------------------------------------------------------------------- *)
  54 (* Rule allowing easy instantiation of polymorphic proformas.                *)
  55 (* ------------------------------------------------------------------------- *)
  56
  57 let PINST tyin tmin =
  58   let iterm_fn = INST (map (I F_F (inst tyin)) tmin)
  59   and itype_fn = INST_TYPE tyin in
  60   fun th -> try iterm_fn (itype_fn th)
  61             with Failure _ -> failwith "PINST";;
  62
  63 (* ------------------------------------------------------------------------- *)
  64 (* Useful derived deductive rule.                                            *)
  65 (* ------------------------------------------------------------------------- *)
  66
  67 let PROVE_HYP ath bth =
  68   if exists (aconv (concl ath)) (hyp bth)
  69   then EQ_MP (DEDUCT_ANTISYM_RULE ath bth) ath
  70   else bth;;
  71
  72 (* ------------------------------------------------------------------------- *)
  73 (* Rules for T                                                               *)
  74 (* ------------------------------------------------------------------------- *)
  75
  76 let T_DEF = new_basic_definition
  77  `T = ((\p:bool. p) = (\p:bool. p))`;;
  78
  79 let TRUTH = EQ_MP (SYM T_DEF) (REFL `\p:bool. p`);;
  80
  81 let EQT_ELIM th =
  82   try EQ_MP (SYM th) TRUTH
  83   with Failure _ -> failwith "EQT_ELIM";;
  84
  85 let EQT_INTRO =
  86   let t = `t:bool` in
  87   let pth =
  88     let th1 = DEDUCT_ANTISYM_RULE (ASSUME t) TRUTH in
  89     let th2 = EQT_ELIM(ASSUME(concl th1)) in
  90     DEDUCT_ANTISYM_RULE th2 th1 in
  91   fun th -> EQ_MP (INST[concl th,t] pth) th;;
  92
  93 (* ------------------------------------------------------------------------- *)
  94 (* Rules for /\                                                              *)
  95 (* ------------------------------------------------------------------------- *)
  96
  97 let AND_DEF = new_basic_definition
  98  `(/\) = \p q. (\f:bool->bool->bool. f p q) = (\f. f T T)`;;
  99
 100 let mk_conj = mk_binary "/\\";;
 101 let list_mk_conj = end_itlist (curry mk_conj);;
 102
 103 let CONJ =
 104   let f = `f:bool->bool->bool`
 105   and p = `p:bool`
 106   and q = `q:bool` in
 107   let pth1 =
 108     let th1 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM AND_DEF p) in
 109     let th2 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM th1 q) in
 110     let th3 = EQ_MP th2 (ASSUME(mk_conj(p,q))) in
 111     EQT_ELIM(BETA_RULE (AP_THM th3 `\(p:bool) (q:bool). q`))
 112   and pth2 =
 113     let pth = ASSUME p
 114     and qth = ASSUME q in
 115     let th1 = MK_COMB(AP_TERM f (EQT_INTRO pth),EQT_INTRO qth) in
 116     let th2 = ABS f th1 in
 117     let th3 = BETA_RULE (AP_THM (AP_THM AND_DEF p) q) in
 118     EQ_MP (SYM th3) th2 in
 119   let pth = DEDUCT_ANTISYM_RULE pth1 pth2 in
 120   fun th1 th2 ->
 121     let th = INST [concl th1,p; concl th2,q] pth in
 122     EQ_MP (PROVE_HYP th1 th) th2;;
 123
 124 let CONJUNCT1 =
 125   let P = `P:bool` and Q = `Q:bool` in
 126   let pth =
 127     let th1 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM AND_DEF P) in
 128     let th2 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM th1 Q) in
 129     let th3 = EQ_MP th2 (ASSUME(mk_conj(P,Q))) in
 130     EQT_ELIM(BETA_RULE (AP_THM th3 `\(p:bool) (q:bool). p`)) in
 131   fun th ->
 132     try let l,r = dest_conj(concl th) in
 133         PROVE_HYP th (INST [l,P; r,Q] pth)
 134     with Failure _ -> failwith "CONJUNCT1";;
 135
 136 let CONJUNCT2 =
 137   let P = `P:bool` and Q = `Q:bool` in
 138   let pth =
 139     let th1 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM AND_DEF P) in
 140     let th2 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM th1 Q) in
 141     let th3 = EQ_MP th2 (ASSUME(mk_conj(P,Q))) in
 142     EQT_ELIM(BETA_RULE (AP_THM th3 `\(p:bool) (q:bool). q`)) in
 143   fun th ->
 144     try let l,r = dest_conj(concl th) in
 145         PROVE_HYP th (INST [l,P; r,Q] pth)
 146     with Failure _ -> failwith "CONJUNCT2";;
 147
 148 let CONJ_PAIR th =
 149   try CONJUNCT1 th,CONJUNCT2 th
 150   with Failure _ -> failwith "CONJ_PAIR: Not a conjunction";;
 151
 152 let CONJUNCTS = striplist CONJ_PAIR;;
 153
 154 (* ------------------------------------------------------------------------- *)
 155 (* Rules for ==>                                                             *)
 156 (* ------------------------------------------------------------------------- *)
 157
 158 let IMP_DEF = new_basic_definition
 159   `(==>) = \p q. p /\ q <=> p`;;
 160
 161 let mk_imp = mk_binary "==>";;
 162
 163 let MP =
 164   let p = `p:bool` and q = `q:bool` in
 165   let pth =
 166     let th1 = BETA_RULE (AP_THM (AP_THM IMP_DEF p) q)
 167     and th2 = CONJ (ASSUME p) (ASSUME q)
 168     and th3 = CONJUNCT1(ASSUME(mk_conj(p,q))) in
 169     EQ_MP (SYM th1) (DEDUCT_ANTISYM_RULE th2 th3)
 170   and qth =
 171     let th1 = BETA_RULE (AP_THM (AP_THM IMP_DEF p) q) in
 172     let th2 = EQ_MP th1 (ASSUME(mk_imp(p,q))) in
 173     CONJUNCT2 (EQ_MP (SYM th2) (ASSUME p)) in
 174   let rth = DEDUCT_ANTISYM_RULE pth qth in
 175   fun ith th ->
 176     let ant,con = dest_imp (concl ith) in
 177     if aconv ant (concl th) then
 178       EQ_MP (PROVE_HYP th (INST [ant,p; con,q] rth)) ith
 179     else failwith "MP: theorems do not agree";;
 180
 181 let DISCH =
 182   let p = `p:bool`
 183   and q = `q:bool` in
 184   let pth = SYM(BETA_RULE (AP_THM (AP_THM IMP_DEF p) q)) in
 185   fun a th ->
 186     let th1 = CONJ (ASSUME a) th in
 187     let th2 = CONJUNCT1 (ASSUME (concl th1)) in
 188     let th3 = DEDUCT_ANTISYM_RULE th1 th2 in
 189     let th4 = INST [a,p; concl th,q] pth in
 190     EQ_MP th4 th3;;
 191
 192 let rec DISCH_ALL th =
 193   try DISCH_ALL (DISCH (hd (hyp th)) th)
 194   with Failure _ -> th;;
 195
 196 let UNDISCH th =
 197   try MP th (ASSUME(rand(rator(concl th))))
 198   with Failure _ -> failwith "UNDISCH";;
 199
 200 let rec UNDISCH_ALL th =
 201   if is_imp (concl th) then UNDISCH_ALL (UNDISCH th)
 202   else th;;
 203
 204 let IMP_ANTISYM_RULE =
 205   let p = `p:bool` and q = `q:bool` and imp_tm = `(==>)` in
 206   let pq = mk_imp(p,q) and qp = mk_imp(q,p) in
 207   let pth1,pth2 = CONJ_PAIR(ASSUME(mk_conj(pq,qp))) in
 208   let pth3 = DEDUCT_ANTISYM_RULE (UNDISCH pth2) (UNDISCH pth1) in
 209   let pth4 = DISCH_ALL(ASSUME q) and pth5 = ASSUME(mk_eq(p,q)) in
 210   let pth6 = CONJ (EQ_MP (SYM(AP_THM (AP_TERM imp_tm pth5) q)) pth4)
 211                   (EQ_MP (SYM(AP_TERM (mk_comb(imp_tm,q)) pth5)) pth4) in
 212   let pth = DEDUCT_ANTISYM_RULE pth6 pth3 in
 213   fun th1 th2 ->
 214     let p1,q1 = dest_imp(concl th1) and p2,q2 = dest_imp(concl th2) in
 215     EQ_MP (INST [p1,p; q1,q] pth) (CONJ th1 th2);;
 216
 217 let ADD_ASSUM tm th = MP (DISCH tm th) (ASSUME tm);;
 218
 219 let EQ_IMP_RULE =
 220   let peq = `p <=> q` in
 221   let p,q = dest_iff peq in
 222   let pth1 = DISCH peq (DISCH p (EQ_MP (ASSUME peq) (ASSUME p)))
 223   and pth2 = DISCH peq (DISCH q (EQ_MP (SYM(ASSUME peq)) (ASSUME q))) in
 224   fun th -> let l,r = dest_iff(concl th) in
 225             MP (INST [l,p; r,q] pth1) th,MP (INST [l,p; r,q] pth2) th;;
 226
 227 let IMP_TRANS =
 228   let pq = `p ==> q`
 229   and qr = `q ==> r` in
 230   let p,q = dest_imp pq and r = rand qr in
 231   let pth =
 232     itlist DISCH [pq; qr; p] (MP (ASSUME qr) (MP (ASSUME pq) (ASSUME p))) in
 233   fun th1 th2 ->
 234         let x,y = dest_imp(concl th1)
 235         and y',z = dest_imp(concl th2) in
 236         if y <> y' then failwith "IMP_TRANS" else
 237         MP (MP (INST [x,p; y,q; z,r] pth) th1) th2;;
 238
 239 (* ------------------------------------------------------------------------- *)
 240 (* Rules for !                                                               *)
 241 (* ------------------------------------------------------------------------- *)
 242
 243 let FORALL_DEF = new_basic_definition
 244  `(!) = \P:A->bool. P = \x. T`;;
 245
 246 let mk_forall = mk_binder "!";;
 247 let list_mk_forall(vs,bod) = itlist (curry mk_forall) vs bod;;
 248
 249 let SPEC =
 250   let P = `P:A->bool`
 251   and x = `x:A` in
 252   let pth =
 253     let th1 = EQ_MP(AP_THM FORALL_DEF `P:A->bool`) (ASSUME `(!)(P:A->bool)`) in
 254     let th2 = AP_THM (CONV_RULE BETA_CONV th1) `x:A` in
 255     let th3 = CONV_RULE (RAND_CONV BETA_CONV) th2 in
 256     DISCH_ALL (EQT_ELIM th3) in
 257   fun tm th ->
 258     try let abs = rand(concl th) in
 259         CONV_RULE BETA_CONV
 260          (MP (PINST [snd(dest_var(bndvar abs)),aty] [abs,P; tm,x] pth) th)
 261     with Failure _ -> failwith "SPEC";;
 262
 263 let SPECL tms th =
 264   try rev_itlist SPEC tms th
 265   with Failure _ -> failwith "SPECL";;
 266
 267 let SPEC_VAR th =
 268   let bv = variant (thm_frees th) (bndvar(rand(concl th))) in
 269   bv,SPEC bv th;;
 270
 271 let rec SPEC_ALL th =
 272   if is_forall(concl th) then SPEC_ALL(snd(SPEC_VAR th)) else th;;
 273
 274 let ISPEC t th =
 275   let x,_ = try dest_forall(concl th) with Failure _ ->
 276     failwith "ISPEC: input theorem not universally quantified" in
 277   let tyins = try type_match (snd(dest_var x)) (type_of t) [] with Failure _ ->
 278     failwith "ISPEC can't type-instantiate input theorem" in
 279   try SPEC t (INST_TYPE tyins th)
 280   with Failure _ -> failwith "ISPEC: type variable(s) free in assumptions";;
 281
 282 let ISPECL tms th =
 283   try if tms = [] then th else
 284       let avs = fst (chop_list (length tms) (fst(strip_forall(concl th)))) in
 285       let tyins = itlist2 type_match (map (snd o dest_var) avs)
 286                           (map type_of tms) [] in
 287       SPECL tms (INST_TYPE tyins th)
 288   with Failure _ -> failwith "ISPECL";;
 289
 290 let GEN =
 291   let pth = SYM(CONV_RULE (RAND_CONV BETA_CONV)
 292                           (AP_THM FORALL_DEF `P:A->bool`)) in
 293   fun x ->
 294     let qth = INST_TYPE[snd(dest_var x),aty] pth in
 295     let ptm = rand(rand(concl qth)) in
 296     fun th ->
 297         let th' = ABS x (EQT_INTRO th) in
 298         let phi = lhand(concl th') in
 299         let rth = INST[phi,ptm] qth in
 300         EQ_MP rth th';;
 301
 302 let GENL = itlist GEN;;
 303
 304 let GEN_ALL th =
 305   let asl,c = dest_thm th in
 306   let vars = subtract (frees c) (freesl asl) in
 307   GENL vars th;;
 308
 309 (* ------------------------------------------------------------------------- *)
 310 (* Rules for ?                                                               *)
 311 (* ------------------------------------------------------------------------- *)
 312
 313 let EXISTS_DEF = new_basic_definition
 314  `(?) = \P:A->bool. !q. (!x. P x ==> q) ==> q`;;
 315
 316 let mk_exists =  mk_binder "?";;
 317 let list_mk_exists(vs,bod) =  itlist (curry mk_exists) vs bod;;
 318
 319 let EXISTS =
 320   let P = `P:A->bool` and x = `x:A` in
 321   let pth =
 322     let th1 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM EXISTS_DEF P) in
 323     let th2 = SPEC `x:A` (ASSUME `!x:A. P x ==> Q`) in
 324     let th3 = DISCH `!x:A. P x ==> Q` (MP th2 (ASSUME `(P:A->bool) x`)) in
 325     EQ_MP (SYM th1) (GEN `Q:bool` th3) in
 326   fun (etm,stm) th ->
 327     try let qf,abs = dest_comb etm in
 328         let bth = BETA_CONV(mk_comb(abs,stm)) in
 329         let cth = PINST [type_of stm,aty] [abs,P; stm,x] pth in
 330         PROVE_HYP (EQ_MP (SYM bth) th) cth
 331     with Failure _ -> failwith "EXISTS";;
 332
 333 let SIMPLE_EXISTS v th =
 334   EXISTS (mk_exists(v,concl th),v) th;;
 335
 336 let CHOOSE =
 337   let P = `P:A->bool` and Q = `Q:bool` in
 338   let pth =
 339     let th1 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM EXISTS_DEF P) in
 340     let th2 = SPEC `Q:bool` (UNDISCH(fst(EQ_IMP_RULE th1))) in
 341     DISCH_ALL (DISCH `(?) (P:A->bool)` (UNDISCH th2)) in
 342   fun (v,th1) th2 ->
 343     try let abs = rand(concl th1) in
 344         let bv,bod = dest_abs abs in
 345         let cmb = mk_comb(abs,v) in
 346         let pat = vsubst[v,bv] bod in
 347         let th3 = CONV_RULE BETA_CONV (ASSUME cmb) in
 348         let th4 = GEN v (DISCH cmb (MP (DISCH pat th2) th3)) in
 349         let th5 = PINST [snd(dest_var v),aty] [abs,P; concl th2,Q] pth in
 350         MP (MP th5 th4) th1
 351     with Failure _ -> failwith "CHOOSE";;
 352
 353 let SIMPLE_CHOOSE v th =
 354   CHOOSE(v,ASSUME (mk_exists(v,hd(hyp th)))) th;;
 355
 356 (* ------------------------------------------------------------------------- *)
 357 (* Rules for \/                                                              *)
 358 (* ------------------------------------------------------------------------- *)
 359
 360 let OR_DEF = new_basic_definition
 361  `(\/) = \p q. !r. (p ==> r) ==> (q ==> r) ==> r`;;
 362
 363 let mk_disj = mk_binary "\\/";;
 364 let list_mk_disj = end_itlist (curry mk_disj);;
 365
 366 let DISJ1 =
 367   let P = `P:bool` and Q = `Q:bool` in
 368   let pth =
 369     let th1 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM OR_DEF `P:bool`) in
 370     let th2 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM th1 `Q:bool`) in
 371     let th3 = MP (ASSUME `P ==> t`) (ASSUME `P:bool`) in
 372     let th4 = GEN `t:bool` (DISCH `P ==> t` (DISCH `Q ==> t` th3)) in
 373     EQ_MP (SYM th2) th4 in
 374   fun th tm ->
 375     try PROVE_HYP th (INST [concl th,P; tm,Q] pth)
 376     with Failure _ -> failwith "DISJ1";;
 377
 378 let DISJ2 =
 379   let P = `P:bool` and Q = `Q:bool` in
 380   let pth =
 381     let th1 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM OR_DEF `P:bool`) in
 382     let th2 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM th1 `Q:bool`) in
 383     let th3 = MP (ASSUME `Q ==> t`) (ASSUME `Q:bool`) in
 384     let th4 = GEN `t:bool` (DISCH `P ==> t` (DISCH `Q ==> t` th3)) in
 385     EQ_MP (SYM th2) th4 in
 386   fun tm th ->
 387     try PROVE_HYP th (INST [tm,P; concl th,Q] pth)
 388     with Failure _ -> failwith "DISJ2";;
 389
 390 let DISJ_CASES =
 391   let P = `P:bool` and Q = `Q:bool` and R = `R:bool` in
 392   let pth =
 393     let th1 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM OR_DEF `P:bool`) in
 394     let th2 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM th1 `Q:bool`) in
 395     let th3 = SPEC `R:bool` (EQ_MP th2 (ASSUME `P \/ Q`)) in
 396     UNDISCH (UNDISCH th3) in
 397   fun th0 th1 th2 ->
 398     try let c1 = concl th1 and c2 = concl th2 in
 399         if not (aconv c1 c2) then failwith "DISJ_CASES" else
 400         let l,r = dest_disj (concl th0) in
 401         let th = INST [l,P; r,Q; c1,R] pth in
 402         PROVE_HYP (DISCH r th2) (PROVE_HYP (DISCH l th1) (PROVE_HYP th0 th))
 403     with Failure _ -> failwith "DISJ_CASES";;
 404
 405 let SIMPLE_DISJ_CASES th1 th2 =
 406   DISJ_CASES (ASSUME(mk_disj(hd(hyp th1),hd(hyp th2)))) th1 th2;;
 407
 408 (* ------------------------------------------------------------------------- *)
 409 (* Rules for negation and falsity.                                           *)
 410 (* ------------------------------------------------------------------------- *)
 411
 412 let F_DEF = new_basic_definition
 413  `F = !p:bool. p`;;
 414
 415 let NOT_DEF = new_basic_definition
 416  `(~) = \p. p ==> F`;;
 417
 418 let mk_neg =
 419   let neg_tm = `(~)` in
 420   fun tm -> try mk_comb(neg_tm,tm)
 421             with Failure _ -> failwith "mk_neg";;
 422
 423 let NOT_ELIM =
 424   let P = `P:bool` in
 425   let pth = CONV_RULE(RAND_CONV BETA_CONV) (AP_THM NOT_DEF P) in
 426   fun th ->
 427     try EQ_MP (INST [rand(concl th),P] pth) th
 428     with Failure _ -> failwith "NOT_ELIM";;
 429
 430 let NOT_INTRO =
 431   let P = `P:bool` in
 432   let pth = SYM(CONV_RULE(RAND_CONV BETA_CONV) (AP_THM NOT_DEF P)) in
 433   fun th ->
 434     try EQ_MP (INST [rand(rator(concl th)),P] pth) th
 435     with Failure _ -> failwith "NOT_INTRO";;
 436
 437 let EQF_INTRO =
 438   let P = `P:bool` in
 439   let pth =
 440     let th1 = NOT_ELIM (ASSUME `~ P`)
 441     and th2 = DISCH `F` (SPEC P (EQ_MP F_DEF (ASSUME `F`))) in
 442     DISCH_ALL (IMP_ANTISYM_RULE th1 th2) in
 443   fun th ->
 444     try MP (INST [rand(concl th),P] pth) th
 445     with Failure _ -> failwith "EQF_INTRO";;
 446
 447 let EQF_ELIM =
 448   let P = `P:bool` in
 449   let pth =
 450     let th1 = EQ_MP (ASSUME `P = F`) (ASSUME `P:bool`) in
 451     let th2 = DISCH P (SPEC `F` (EQ_MP F_DEF th1)) in
 452     DISCH_ALL (NOT_INTRO th2) in
 453   fun th ->
 454     try MP (INST [rand(rator(concl th)),P] pth) th
 455     with Failure _ -> failwith "EQF_ELIM";;
 456
 457 let CONTR =
 458   let P = `P:bool` and f_tm = `F` in
 459   let pth = SPEC P (EQ_MP F_DEF (ASSUME `F`)) in
 460   fun tm th ->
 461     if concl th <> f_tm then failwith "CONTR"
 462     else PROVE_HYP th (INST [tm,P] pth);;
 463
 464 (* ------------------------------------------------------------------------- *)
 465 (* Rules for unique existence.                                               *)
 466 (* ------------------------------------------------------------------------- *)
 467
 468 let EXISTS_UNIQUE_DEF = new_basic_definition
 469  `(?!) = \P:A->bool. ((?) P) /\ (!x y. P x /\ P y ==> x = y)`;;
 470
 471 let mk_uexists = mk_binder "?!";;
 472
 473 let EXISTENCE =
 474   let P = `P:A->bool` in
 475   let pth =
 476     let th1 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM EXISTS_UNIQUE_DEF P) in
 477     let th2 = UNDISCH (fst(EQ_IMP_RULE th1)) in
 478     DISCH_ALL (CONJUNCT1 th2) in
 479   fun th ->
 480     try let abs = rand(concl th) in
 481         let ty = snd(dest_var(bndvar abs)) in
 482         MP (PINST [ty,aty] [abs,P] pth) th
 483     with Failure _ -> failwith "EXISTENCE";;