src/HOL/Library/old_recdef.ML
changeset 60781 2da59cdf531c
parent 60774 6c28d8ed2488
child 60825 bacfb7c45d81
     1.1 --- a/src/HOL/Library/old_recdef.ML	Sat Jul 25 23:15:37 2015 +0200
     1.2 +++ b/src/HOL/Library/old_recdef.ML	Sat Jul 25 23:41:53 2015 +0200
     1.3 @@ -175,8 +175,7 @@
     1.4    val PROVE_HYP: thm -> thm -> thm
     1.5  
     1.6    val CHOOSE: Proof.context -> cterm * thm -> thm -> thm
     1.7 -  val EXISTS: cterm * cterm -> thm -> thm
     1.8 -  val EXISTL: cterm list -> thm -> thm
     1.9 +  val EXISTS: Proof.context -> cterm * cterm -> thm -> thm
    1.10    val IT_EXISTS: Proof.context -> (cterm * cterm) list -> thm -> thm
    1.11  
    1.12    val EVEN_ORS: thm list -> thm list
    1.13 @@ -1199,29 +1198,11 @@
    1.14        handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg
    1.15    end;
    1.16  
    1.17 -local
    1.18 -  val prop = Thm.prop_of exI
    1.19 -  val [P, x] = map (Thm.cterm_of @{context}) (Misc_Legacy.term_vars prop)
    1.20 -in
    1.21 -fun EXISTS (template,witness) thm =
    1.22 +fun EXISTS ctxt (template,witness) thm =
    1.23    let val abstr = #2 (Dcterm.dest_comb template) in
    1.24 -    thm RS (cterm_instantiate [(P, abstr), (x, witness)] exI)
    1.25 +    thm RS (infer_instantiate ctxt [(("P", 0), abstr), (("x", 0), witness)] exI)
    1.26        handle THM (msg, _, _) => raise RULES_ERR "EXISTS" msg
    1.27 -  end
    1.28 -end;
    1.29 -
    1.30 -(*----------------------------------------------------------------------------
    1.31 - *
    1.32 - *         A |- M
    1.33 - *   -------------------   [v_1,...,v_n]
    1.34 - *    A |- ?v1...v_n. M
    1.35 - *
    1.36 - *---------------------------------------------------------------------------*)
    1.37 -
    1.38 -fun EXISTL vlist th =
    1.39 -  fold_rev (fn v => fn thm => EXISTS(Dcterm.mk_exists(v,cconcl thm), v) thm)
    1.40 -           vlist th;
    1.41 -
    1.42 +  end;
    1.43  
    1.44  (*----------------------------------------------------------------------------
    1.45   *
    1.46 @@ -1238,7 +1219,7 @@
    1.47      fun ex v M = Thm.cterm_of ctxt (USyntax.mk_exists{Bvar=v,Body = M})
    1.48    in
    1.49      fold_rev (fn (b as (r1,r2)) => fn thm =>
    1.50 -        EXISTS(ex r2 (subst_free [b]
    1.51 +        EXISTS ctxt (ex r2 (subst_free [b]
    1.52                     (HOLogic.dest_Trueprop(Thm.prop_of thm))), Thm.cterm_of ctxt r1)
    1.53                thm)
    1.54         blist' th
    1.55 @@ -1453,13 +1434,7 @@
    1.56  
    1.57  fun PGEN ctxt tych a vstr th =
    1.58    let val a1 = tych a
    1.59 -      val vstr1 = tych vstr
    1.60 -  in
    1.61 -  Thm.forall_intr a1
    1.62 -     (if (is_Free vstr)
    1.63 -      then cterm_instantiate [(vstr1,a1)] th
    1.64 -      else VSTRUCT_ELIM ctxt tych a vstr th)
    1.65 -  end;
    1.66 +  in Thm.forall_intr a1 (VSTRUCT_ELIM ctxt tych a vstr th) end;
    1.67  
    1.68  
    1.69  (*---------------------------------------------------------------------------
    1.70 @@ -2243,7 +2218,7 @@
    1.71       val a = Free (aname, T)
    1.72       val v = Free (vname, T)
    1.73       val a_eq_v = HOLogic.mk_eq(a,v)
    1.74 -     val ex_th0 = Rules.EXISTS (tych (USyntax.mk_exists{Bvar=v,Body=a_eq_v}), tych a)
    1.75 +     val ex_th0 = Rules.EXISTS ctxt (tych (USyntax.mk_exists{Bvar=v,Body=a_eq_v}), tych a)
    1.76                             (Rules.REFL (tych a))
    1.77       val th0 = Rules.ASSUME (tych a_eq_v)
    1.78       val rows = map (fn x => ([x], (th0,[]))) pats