equal
deleted
inserted
replaced
479 |
479 |
480 fun choose v th th' = case Thm.concl_of th of |
480 fun choose v th th' = case Thm.concl_of th of |
481 \<^term>\<open>Trueprop\<close> $ (Const(\<^const_name>\<open>Ex\<close>,_)$_) => |
481 \<^term>\<open>Trueprop\<close> $ (Const(\<^const_name>\<open>Ex\<close>,_)$_) => |
482 let |
482 let |
483 val p = (funpow 2 Thm.dest_arg o Thm.cprop_of) th |
483 val p = (funpow 2 Thm.dest_arg o Thm.cprop_of) th |
484 val T = (hd o Thm.dest_ctyp o Thm.ctyp_of_cterm) p |
484 val T = Thm.dest_ctyp_nth 0 (Thm.ctyp_of_cterm p) |
485 val th0 = Conv.fconv_rule (Thm.beta_conversion true) |
485 val th0 = Conv.fconv_rule (Thm.beta_conversion true) |
486 (Thm.instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o Thm.cprop_of) th'] exE) |
486 (Thm.instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o Thm.cprop_of) th'] exE) |
487 val pv = (Thm.rhs_of o Thm.beta_conversion true) |
487 val pv = (Thm.rhs_of o Thm.beta_conversion true) |
488 (Thm.apply \<^cterm>\<open>Trueprop\<close> (Thm.apply p v)) |
488 (Thm.apply \<^cterm>\<open>Trueprop\<close> (Thm.apply p v)) |
489 val th1 = Thm.forall_intr v (Thm.implies_intr pv th') |
489 val th1 = Thm.forall_intr v (Thm.implies_intr pv th') |