--- a/src/HOL/HOL.thy Sat Jul 25 23:15:37 2015 +0200
+++ b/src/HOL/HOL.thy Sat Jul 25 23:41:53 2015 +0200
@@ -1190,15 +1190,6 @@
simproc_setup let_simp ("Let x f") = \<open>
let
- val (f_Let_unfold, x_Let_unfold) =
- let val [(_ $ (f $ x) $ _)] = Thm.prems_of @{thm Let_unfold}
- in apply2 (Thm.cterm_of @{context}) (f, x) end
- val (f_Let_folded, x_Let_folded) =
- let val [(_ $ (f $ x) $ _)] = Thm.prems_of @{thm Let_folded}
- in apply2 (Thm.cterm_of @{context}) (f, x) end;
- val g_Let_folded =
- let val [(_ $ _ $ (g $ _))] = Thm.prems_of @{thm Let_folded}
- in Thm.cterm_of @{context} g end;
fun count_loose (Bound i) k = if i >= k then 1 else 0
| count_loose (s $ t) k = count_loose s k + count_loose t k
| count_loose (Abs (_, _, t)) k = count_loose t (k + 1)
@@ -1234,7 +1225,7 @@
if g aconv g' then
let
val rl =
- cterm_instantiate [(f_Let_unfold, cf), (x_Let_unfold, cx)] @{thm Let_unfold};
+ infer_instantiate ctxt [(("f", 0), cf), (("x", 0), cx)] @{thm Let_unfold};
in SOME (rl OF [fx_g]) end
else if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract abs_g')
then NONE (*avoid identity conversion*)
@@ -1243,10 +1234,10 @@
val g'x = abs_g' $ x;
val g_g'x = Thm.symmetric (Thm.beta_conversion false (Thm.cterm_of ctxt g'x));
val rl =
- @{thm Let_folded} |> cterm_instantiate
- [(f_Let_folded, Thm.cterm_of ctxt f),
- (x_Let_folded, cx),
- (g_Let_folded, Thm.cterm_of ctxt abs_g')];
+ @{thm Let_folded} |> infer_instantiate ctxt
+ [(("f", 0), Thm.cterm_of ctxt f),
+ (("x", 0), cx),
+ (("g", 0), Thm.cterm_of ctxt abs_g')];
in SOME (rl OF [Thm.transitive fx_g g_g'x]) end
end
| _ => NONE)
--- a/src/HOL/Library/old_recdef.ML Sat Jul 25 23:15:37 2015 +0200
+++ b/src/HOL/Library/old_recdef.ML Sat Jul 25 23:41:53 2015 +0200
@@ -175,8 +175,7 @@
val PROVE_HYP: thm -> thm -> thm
val CHOOSE: Proof.context -> cterm * thm -> thm -> thm
- val EXISTS: cterm * cterm -> thm -> thm
- val EXISTL: cterm list -> thm -> thm
+ val EXISTS: Proof.context -> cterm * cterm -> thm -> thm
val IT_EXISTS: Proof.context -> (cterm * cterm) list -> thm -> thm
val EVEN_ORS: thm list -> thm list
@@ -1199,29 +1198,11 @@
handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg
end;
-local
- val prop = Thm.prop_of exI
- val [P, x] = map (Thm.cterm_of @{context}) (Misc_Legacy.term_vars prop)
-in
-fun EXISTS (template,witness) thm =
+fun EXISTS ctxt (template,witness) thm =
let val abstr = #2 (Dcterm.dest_comb template) in
- thm RS (cterm_instantiate [(P, abstr), (x, witness)] exI)
+ thm RS (infer_instantiate ctxt [(("P", 0), abstr), (("x", 0), witness)] exI)
handle THM (msg, _, _) => raise RULES_ERR "EXISTS" msg
- end
-end;
-
-(*----------------------------------------------------------------------------
- *
- * A |- M
- * ------------------- [v_1,...,v_n]
- * A |- ?v1...v_n. M
- *
- *---------------------------------------------------------------------------*)
-
-fun EXISTL vlist th =
- fold_rev (fn v => fn thm => EXISTS(Dcterm.mk_exists(v,cconcl thm), v) thm)
- vlist th;
-
+ end;
(*----------------------------------------------------------------------------
*
@@ -1238,7 +1219,7 @@
fun ex v M = Thm.cterm_of ctxt (USyntax.mk_exists{Bvar=v,Body = M})
in
fold_rev (fn (b as (r1,r2)) => fn thm =>
- EXISTS(ex r2 (subst_free [b]
+ EXISTS ctxt (ex r2 (subst_free [b]
(HOLogic.dest_Trueprop(Thm.prop_of thm))), Thm.cterm_of ctxt r1)
thm)
blist' th
@@ -1453,13 +1434,7 @@
fun PGEN ctxt tych a vstr th =
let val a1 = tych a
- val vstr1 = tych vstr
- in
- Thm.forall_intr a1
- (if (is_Free vstr)
- then cterm_instantiate [(vstr1,a1)] th
- else VSTRUCT_ELIM ctxt tych a vstr th)
- end;
+ in Thm.forall_intr a1 (VSTRUCT_ELIM ctxt tych a vstr th) end;
(*---------------------------------------------------------------------------
@@ -2243,7 +2218,7 @@
val a = Free (aname, T)
val v = Free (vname, T)
val a_eq_v = HOLogic.mk_eq(a,v)
- val ex_th0 = Rules.EXISTS (tych (USyntax.mk_exists{Bvar=v,Body=a_eq_v}), tych a)
+ val ex_th0 = Rules.EXISTS ctxt (tych (USyntax.mk_exists{Bvar=v,Body=a_eq_v}), tych a)
(Rules.REFL (tych a))
val th0 = Rules.ASSUME (tych a_eq_v)
val rows = map (fn x => ([x], (th0,[]))) pats
--- a/src/HOL/Nominal/nominal_datatype.ML Sat Jul 25 23:15:37 2015 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Sat Jul 25 23:41:53 2015 +0200
@@ -788,8 +788,8 @@
(Const (Sign.intern_const thy ("Rep_" ^ tname), T --> T'));
val dist =
Drule.export_without_context
- (cterm_instantiate
- [(Thm.global_cterm_of thy distinct_f, rep_const)] Old_Datatype.distinct_lemma);
+ (infer_instantiate (Proof_Context.init_global thy)
+ [(#1 (dest_Var distinct_f), rep_const)] Old_Datatype.distinct_lemma);
val (thy', defs', eqns') = fold (make_constr_def tname T T')
(constrs ~~ constrs' ~~ constr_syntax) (Sign.add_path tname thy, defs, [])
in
@@ -1058,24 +1058,27 @@
val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of indrule_lemma)));
val frees = if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] else
map (Free o apfst fst o dest_Var) Ps;
- val indrule_lemma' = cterm_instantiate
- (map (Thm.global_cterm_of thy8) Ps ~~ map (Thm.global_cterm_of thy8) frees) indrule_lemma;
val Abs_inverse_thms' = map (fn r => r RS subst) Abs_inverse_thms;
val dt_induct_prop = Old_Datatype_Prop.make_ind descr';
val dt_induct = Goal.prove_global_future thy8 []
(Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
- (fn {prems, context = ctxt} => EVERY
- [resolve_tac ctxt [indrule_lemma'] 1,
- (Old_Datatype_Aux.ind_tac ctxt rep_induct [] THEN_ALL_NEW
- Object_Logic.atomize_prems_tac ctxt) 1,
- EVERY (map (fn (prem, r) => (EVERY
- [REPEAT (eresolve_tac ctxt Abs_inverse_thms' 1),
- simp_tac (put_simpset HOL_basic_ss ctxt addsimps [Thm.symmetric r]) 1,
- DEPTH_SOLVE_1
- (assume_tac ctxt 1 ORELSE resolve_tac ctxt [prem] 1 ORELSE eresolve_tac ctxt [allE] 1)]))
- (prems ~~ constr_defs))]);
+ (fn {prems, context = ctxt} =>
+ let
+ val indrule_lemma' = infer_instantiate ctxt
+ (map (#1 o dest_Var) Ps ~~ map (Thm.cterm_of ctxt) frees) indrule_lemma;
+ in
+ EVERY [resolve_tac ctxt [indrule_lemma'] 1,
+ (Old_Datatype_Aux.ind_tac ctxt rep_induct [] THEN_ALL_NEW
+ Object_Logic.atomize_prems_tac ctxt) 1,
+ EVERY (map (fn (prem, r) => (EVERY
+ [REPEAT (eresolve_tac ctxt Abs_inverse_thms' 1),
+ simp_tac (put_simpset HOL_basic_ss ctxt addsimps [Thm.symmetric r]) 1,
+ DEPTH_SOLVE_1
+ (assume_tac ctxt 1 ORELSE resolve_tac ctxt [prem] 1 ORELSE eresolve_tac ctxt [allE] 1)]))
+ (prems ~~ constr_defs))]
+ end);
val case_names_induct = Old_Datatype_Data.mk_case_names_induct descr'';
--- a/src/HOL/Tools/Function/function_context_tree.ML Sat Jul 25 23:15:37 2015 +0200
+++ b/src/HOL/Tools/Function/function_context_tree.ML Sat Jul 25 23:41:53 2015 +0200
@@ -119,10 +119,10 @@
val subst = Pattern.match thy (c, tt') (Vartab.empty, Vartab.empty)
val branches = map (mk_branch ctxt o Envir.beta_norm o Envir.subst_term subst) subs
val inst =
- map (fn v => apply2 (Thm.cterm_of ctxt) (Var v, Envir.subst_term subst (Var v)))
+ map (fn v => (#1 v, Thm.cterm_of ctxt (Envir.subst_term subst (Var v))))
(Term.add_vars c [])
in
- (cterm_instantiate inst r, dep, branches)
+ (infer_instantiate ctxt inst r, dep, branches)
end handle Pattern.MATCH => find_cong_rule ctxt fvar h rs t)
| find_cong_rule _ _ _ [] _ = raise General.Fail "No cong rule found!"
--- a/src/HOL/Tools/Function/lexicographic_order.ML Sat Jul 25 23:15:37 2015 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Sat Jul 25 23:41:53 2015 +0200
@@ -201,7 +201,7 @@
in (* 4: proof reconstruction *)
st |>
- (PRIMITIVE (cterm_instantiate [apply2 (Thm.cterm_of ctxt) (rel, relation)])
+ (PRIMITIVE (infer_instantiate ctxt [(#1 (dest_Var rel), Thm.cterm_of ctxt relation)])
THEN (REPEAT (resolve_tac ctxt @{thms wf_mlex} 1))
THEN (resolve_tac ctxt @{thms wf_empty} 1)
THEN EVERY (map (prove_row_tac ctxt) clean_table))
--- a/src/HOL/Tools/Function/pat_completeness.ML Sat Jul 25 23:15:37 2015 +0200
+++ b/src/HOL/Tools/Function/pat_completeness.ML Sat Jul 25 23:41:53 2015 +0200
@@ -24,9 +24,9 @@
fun inst_free var inst = Thm.forall_elim inst o Thm.forall_intr var
fun inst_case_thm ctxt x P thm =
- let val [Pv, xv] = Term.add_vars (Thm.prop_of thm) []
+ let val [P_name, x_name] = Term.add_var_names (Thm.prop_of thm) []
in
- thm |> cterm_instantiate (map (apply2 (Thm.cterm_of ctxt)) [(Var xv, x), (Var Pv, P)])
+ thm |> infer_instantiate ctxt [(x_name, Thm.cterm_of ctxt x), (P_name, Thm.cterm_of ctxt P)]
end
fun invent_vars constr i =
--- a/src/HOL/Tools/Meson/meson.ML Sat Jul 25 23:15:37 2015 +0200
+++ b/src/HOL/Tools/Meson/meson.ML Sat Jul 25 23:41:53 2015 +0200
@@ -10,7 +10,6 @@
sig
val trace : bool Config.T
val max_clauses : int Config.T
- val term_pair_of: indexname * (typ * 'a) -> term * 'a
val first_order_resolve : Proof.context -> thm -> thm -> thm
val size_of_subgoals: thm -> int
val has_too_many_clauses: Proof.context -> term -> bool
@@ -95,8 +94,6 @@
(** First-order Resolution **)
-fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t);
-
(*FIXME: currently does not "rename variables apart"*)
fun first_order_resolve ctxt thA thB =
(case
@@ -107,8 +104,8 @@
val tenv =
Pattern.first_order_match thy (tmB, tmA)
(Vartab.empty, Vartab.empty) |> snd
- val ct_pairs = map (apply2 (Thm.cterm_of ctxt) o term_pair_of) (Vartab.dest tenv)
- in thA RS (cterm_instantiate ct_pairs thB) end) () of
+ val insts = Vartab.fold (fn (xi, (_, t)) => cons (xi, Thm.cterm_of ctxt t)) tenv [];
+ in thA RS (infer_instantiate ctxt insts thB) end) () of
SOME th => th
| NONE => raise THM ("first_order_resolve", 0, [thA, thB]))
@@ -616,10 +613,6 @@
handle NO_F_PATTERN () => NONE
val ext_cong_neq = @{thm ext_cong_neq}
-val F_ext_cong_neq =
- Term.add_vars (Thm.prop_of @{thm ext_cong_neq}) []
- |> filter (fn ((s, _), _) => s = "F")
- |> the_single |> Var
(* Strengthens "f g ~= f h" to "f g ~= f h & (EX x. g x ~= h x)". *)
fun cong_extensionalize_thm ctxt th =
@@ -628,11 +621,8 @@
$ (Const (@{const_name HOL.eq}, Type (_, [T, _]))
$ (t as _ $ _) $ (u as _ $ _))) =>
(case get_F_pattern T t u of
- SOME p =>
- let val inst = [apply2 (Thm.cterm_of ctxt) (F_ext_cong_neq, p)] in
- th RS cterm_instantiate inst ext_cong_neq
- end
- | NONE => th)
+ SOME p => th RS infer_instantiate ctxt [(("F", 0), Thm.cterm_of ctxt p)] ext_cong_neq
+ | NONE => th)
| _ => th)
(* Removes the lambdas from an equation of the form "t = (%x1 ... xn. u)". It
--- a/src/HOL/Tools/Meson/meson_clausify.ML Sat Jul 25 23:15:37 2015 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Sat Jul 25 23:41:53 2015 +0200
@@ -94,10 +94,6 @@
| is_quasi_lambda_free (Abs _) = false
| is_quasi_lambda_free _ = true
-val [f_B,g_B] = map (Thm.cterm_of @{context}) (Misc_Legacy.term_vars (Thm.prop_of @{thm abs_B}));
-val [g_C,f_C] = map (Thm.cterm_of @{context}) (Misc_Legacy.term_vars (Thm.prop_of @{thm abs_C}));
-val [f_S,g_S] = map (Thm.cterm_of @{context}) (Misc_Legacy.term_vars (Thm.prop_of @{thm abs_S}));
-
(* FIXME: Requires more use of cterm constructors. *)
fun abstract ctxt ct =
let
@@ -118,7 +114,8 @@
if Term.is_dependent rand then (*S*)
let val crator = Thm.cterm_of ctxt (Abs (x, xT, rator))
val crand = Thm.cterm_of ctxt (Abs (x, xT, rand))
- val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S}
+ val abs_S' =
+ infer_instantiate ctxt [(("f", 0), crator), (("g", 0), crand)] @{thm abs_S}
val (_,rhs) = Thm.dest_equals (Thm.cprop_of abs_S')
in
Thm.transitive abs_S' (Conv.binop_conv (abstract ctxt) rhs)
@@ -126,7 +123,8 @@
else (*C*)
let val crator = Thm.cterm_of ctxt (Abs (x, xT, rator))
val abs_C' =
- cterm_instantiate [(f_C, crator), (g_C, Thm.cterm_of ctxt rand)] @{thm abs_C}
+ infer_instantiate ctxt [(("f", 0), crator), (("b", 0), Thm.cterm_of ctxt rand)]
+ @{thm abs_C}
val (_,rhs) = Thm.dest_equals (Thm.cprop_of abs_C')
in
Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv (abstract ctxt)) rhs)
@@ -136,7 +134,8 @@
else (*B*)
let val crand = Thm.cterm_of ctxt (Abs (x, xT, rand))
val crator = Thm.cterm_of ctxt rator
- val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B}
+ val abs_B' =
+ infer_instantiate ctxt [(("a", 0), crator), (("g", 0), crand)] @{thm abs_B}
val (_,rhs) = Thm.dest_equals (Thm.cprop_of abs_B')
in Thm.transitive abs_B' (Conv.arg_conv (abstract ctxt) rhs) end
else makeK ()
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Sat Jul 25 23:15:37 2015 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Sat Jul 25 23:41:53 2015 +0200
@@ -650,7 +650,7 @@
|> sort (cluster_ord
o apply2 (Meson_Clausify.cluster_of_zapped_var_name
o fst o fst))
- |> map (Meson.term_pair_of #> apply2 (Envir.subst_term_types tyenv))
+ |> map (fn (xi, (T, t)) => apply2 (Envir.subst_term_types tyenv) (Var (xi, T), t))
val tysubst = tyenv |> Vartab.dest
in (tysubst, tsubst) end
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML Sat Jul 25 23:15:37 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML Sat Jul 25 23:41:53 2015 +0200
@@ -248,10 +248,11 @@
fun dt_constr_defs (((((_, (_, _, constrs)), tname), typedef: Typedef.info), T), constr_syntax)
(thy, defs, eqns, rep_congs, dist_lemmas) =
let
+ val ctxt = Proof_Context.init_global thy;
val _ $ (_ $ (cong_f $ _) $ _) = Thm.concl_of arg_cong;
- val rep_const = Thm.global_cterm_of thy (Const (#Rep_name (#1 typedef), T --> Univ_elT));
- val cong' = cterm_instantiate [(Thm.global_cterm_of thy cong_f, rep_const)] arg_cong;
- val dist = cterm_instantiate [(Thm.global_cterm_of thy distinct_f, rep_const)] distinct_lemma;
+ val rep_const = Thm.cterm_of ctxt (Const (#Rep_name (#1 typedef), T --> Univ_elT));
+ val cong' = infer_instantiate ctxt [(#1 (dest_Var cong_f), rep_const)] arg_cong;
+ val dist = infer_instantiate ctxt [(#1 (dest_Var distinct_f), rep_const)] distinct_lemma;
val (thy', defs', eqns', _) =
fold (make_constr_def typedef T (length constrs))
(constrs ~~ constr_syntax) (Sign.add_path tname thy, defs, [], 1);
@@ -635,8 +636,6 @@
val frees =
if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))]
else map (Free o apfst fst o dest_Var) Ps;
- val indrule_lemma' =
- cterm_instantiate (map (Thm.global_cterm_of thy6) Ps ~~ map (Thm.global_cterm_of thy6) frees) indrule_lemma;
val dt_induct_prop = Old_Datatype_Prop.make_ind descr;
val dt_induct =
@@ -644,16 +643,22 @@
(Logic.strip_imp_prems dt_induct_prop)
(Logic.strip_imp_concl dt_induct_prop)
(fn {context = ctxt, prems, ...} =>
- EVERY
- [resolve_tac ctxt [indrule_lemma'] 1,
- (Old_Datatype_Aux.ind_tac ctxt rep_induct [] THEN_ALL_NEW
- Object_Logic.atomize_prems_tac ctxt) 1,
- EVERY (map (fn (prem, r) => (EVERY
- [REPEAT (eresolve_tac ctxt Abs_inverse_thms 1),
- simp_tac (put_simpset HOL_basic_ss ctxt
- addsimps (Thm.symmetric r :: Rep_inverse_thms')) 1,
- DEPTH_SOLVE_1 (ares_tac ctxt [prem] 1 ORELSE eresolve_tac ctxt [allE] 1)]))
- (prems ~~ (constr_defs @ map mk_meta_eq iso_char_thms)))]);
+ let
+ val indrule_lemma' =
+ infer_instantiate ctxt
+ (map (#1 o dest_Var) Ps ~~ map (Thm.cterm_of ctxt) frees) indrule_lemma;
+ in
+ EVERY
+ [resolve_tac ctxt [indrule_lemma'] 1,
+ (Old_Datatype_Aux.ind_tac ctxt rep_induct [] THEN_ALL_NEW
+ Object_Logic.atomize_prems_tac ctxt) 1,
+ EVERY (map (fn (prem, r) => (EVERY
+ [REPEAT (eresolve_tac ctxt Abs_inverse_thms 1),
+ simp_tac (put_simpset HOL_basic_ss ctxt
+ addsimps (Thm.symmetric r :: Rep_inverse_thms')) 1,
+ DEPTH_SOLVE_1 (ares_tac ctxt [prem] 1 ORELSE eresolve_tac ctxt [allE] 1)]))
+ (prems ~~ (constr_defs @ map mk_meta_eq iso_char_thms)))]
+ end);
val ([(_, [dt_induct'])], thy7) =
thy6
--- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML Sat Jul 25 23:15:37 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML Sat Jul 25 23:41:53 2015 +0200
@@ -147,8 +147,8 @@
(ts ~~ ts') |> map_filter (fn (t, u) =>
(case abstr (getP u) of
NONE => NONE
- | SOME u' => SOME (apply2 (Thm.cterm_of ctxt) (t |> getP |> snd |> head_of, u'))));
- val indrule' = cterm_instantiate insts indrule;
+ | SOME u' => SOME (t |> getP |> snd |> head_of |> dest_Var |> #1, Thm.cterm_of ctxt u')));
+ val indrule' = infer_instantiate ctxt insts indrule;
in resolve_tac ctxt [indrule'] i end);
@@ -163,9 +163,9 @@
val prem' = hd (Thm.prems_of exhaustion);
val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
val exhaustion' =
- cterm_instantiate
- [apply2 (Thm.cterm_of ctxt)
- (head_of lhs, fold_rev (fn (_, T) => fn t => Abs ("z", T, t)) params (Bound 0))]
+ infer_instantiate ctxt
+ [(#1 (dest_Var (head_of lhs)),
+ Thm.cterm_of ctxt (fold_rev (fn (_, T) => fn t => Abs ("z", T, t)) params (Bound 0)))]
exhaustion;
in compose_tac ctxt (false, exhaustion', Thm.nprems_of exhaustion) i end);
--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Sat Jul 25 23:15:37 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Sat Jul 25 23:41:53 2015 +0200
@@ -46,21 +46,24 @@
Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", maxidx + 1), T), Bound 0) $
Var (("P", 0), HOLogic.boolT));
val insts = take i dummyPs @ (P :: drop (i + 1) dummyPs);
- val insts' = map (Thm.global_cterm_of thy) induct_Ps ~~ map (Thm.global_cterm_of thy) insts;
- val induct' =
- refl RS
- (nth (Old_Datatype_Aux.split_conj_thm (cterm_instantiate insts' induct)) i
- RSN (2, rev_mp));
in
Goal.prove_sorry_global thy []
(Logic.strip_imp_prems t)
(Logic.strip_imp_concl t)
(fn {context = ctxt, prems, ...} =>
- EVERY
- [resolve_tac ctxt [induct'] 1,
- REPEAT (resolve_tac ctxt [TrueI] 1),
- REPEAT ((resolve_tac ctxt [impI] 1) THEN (eresolve_tac ctxt prems 1)),
- REPEAT (resolve_tac ctxt [TrueI] 1)])
+ let
+ val insts' = map (#1 o dest_Var) induct_Ps ~~ map (Thm.cterm_of ctxt) insts;
+ val induct' =
+ refl RS
+ (nth (Old_Datatype_Aux.split_conj_thm (infer_instantiate ctxt insts' induct)) i
+ RSN (2, rev_mp));
+ in
+ EVERY
+ [resolve_tac ctxt [induct'] 1,
+ REPEAT (resolve_tac ctxt [TrueI] 1),
+ REPEAT ((resolve_tac ctxt [impI] 1) THEN (eresolve_tac ctxt prems 1)),
+ REPEAT (resolve_tac ctxt [TrueI] 1)]
+ end)
end;
val casedist_thms =
@@ -206,16 +209,19 @@
val insts =
map (fn ((i, T), t) => absfree ("x" ^ string_of_int i, T) t)
((1 upto length recTs) ~~ recTs ~~ rec_unique_ts);
- val induct' = induct
- |> cterm_instantiate
- (map (Thm.global_cterm_of thy1) induct_Ps ~~ map (Thm.global_cterm_of thy1) insts);
in
Old_Datatype_Aux.split_conj_thm (Goal.prove_sorry_global thy1 [] []
(HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj rec_unique_ts))
(fn {context = ctxt, ...} =>
- #1 (fold (mk_unique_tac ctxt) (descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts)
- (((resolve_tac ctxt [induct'] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1 THEN
- rewrite_goals_tac ctxt [mk_meta_eq @{thm choice_eq}], rec_intrs)))))
+ let
+ val induct' =
+ infer_instantiate ctxt
+ (map (#1 o dest_Var) induct_Ps ~~ map (Thm.cterm_of ctxt) insts) induct;
+ in
+ #1 (fold (mk_unique_tac ctxt) (descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts)
+ (((resolve_tac ctxt [induct'] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1 THEN
+ rewrite_goals_tac ctxt [mk_meta_eq @{thm choice_eq}], rec_intrs)))
+ end))
end;
val rec_total_thms = map (fn r => r RS @{thm theI'}) rec_unique_thms;
@@ -380,15 +386,16 @@
fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'), exhaustion), case_thms'), T) =
let
val _ $ (_ $ lhs $ _) = hd (Logic.strip_assums_hyp (hd (Thm.prems_of exhaustion)));
+ val ctxt = Proof_Context.init_global thy;
val exhaustion' = exhaustion
- |> cterm_instantiate [apply2 (Thm.global_cterm_of thy) (lhs, Free ("x", T))];
- fun tac ctxt =
+ |> infer_instantiate ctxt [(#1 (dest_Var lhs), Thm.cterm_of ctxt (Free ("x", T)))];
+ val tac =
EVERY [resolve_tac ctxt [exhaustion'] 1,
ALLGOALS (asm_simp_tac
(put_simpset HOL_ss ctxt addsimps (dist_rewrites' @ inject @ case_thms')))];
in
- (Goal.prove_sorry_global thy [] [] t1 (tac o #context),
- Goal.prove_sorry_global thy [] [] t2 (tac o #context))
+ (Goal.prove_sorry_global thy [] [] t1 (K tac),
+ Goal.prove_sorry_global thy [] [] t2 (K tac))
end;
val split_thm_pairs =
@@ -451,13 +458,13 @@
val Const (@{const_name Pure.imp}, _) $ tm $ _ = t;
val Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ Ma) = tm;
val nchotomy' = nchotomy RS spec;
- val [v] = Term.add_vars (Thm.concl_of nchotomy') [];
- val nchotomy'' =
- cterm_instantiate [apply2 (Thm.global_cterm_of thy) (Var v, Ma)] nchotomy';
+ val [v] = Term.add_var_names (Thm.concl_of nchotomy') [];
in
Goal.prove_sorry_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
(fn {context = ctxt, prems, ...} =>
let
+ val nchotomy'' =
+ infer_instantiate ctxt [(v, Thm.cterm_of ctxt Ma)] nchotomy';
val simplify = asm_simp_tac (put_simpset HOL_ss ctxt addsimps (prems @ case_rewrites))
in
EVERY [
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Sat Jul 25 23:15:37 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Sat Jul 25 23:41:53 2015 +0200
@@ -141,9 +141,8 @@
(intros'', (local_defs, thy'))
end
-fun introrulify thy ths =
+fun introrulify ctxt ths =
let
- val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *)
val ((_, ths'), ctxt') = Variable.import true ths ctxt
fun introrulify' th =
let
@@ -158,8 +157,8 @@
in
(ps, Logic.list_implies (prems, HOLogic.mk_Trueprop lhs))
end
- val x =
- (Thm.cterm_of ctxt' o the_single o snd o strip_comb o HOLogic.dest_Trueprop o fst o
+ val Var (x, _) =
+ (the_single o snd o strip_comb o HOLogic.dest_Trueprop o fst o
Logic.dest_implies o Thm.prop_of) @{thm exI}
fun prove_introrule (index, (ps, introrule)) =
let
@@ -167,7 +166,7 @@
THEN Inductive.select_disj_tac ctxt' (length disjuncts) (index + 1) 1
THEN (EVERY (map (fn y =>
resolve_tac ctxt'
- [Drule.cterm_instantiate [(x, Thm.cterm_of ctxt' (Free y))] @{thm exI}] 1) ps))
+ [infer_instantiate ctxt' [(x, Thm.cterm_of ctxt' (Free y))] @{thm exI}] 1) ps))
THEN REPEAT_DETERM (resolve_tac ctxt' @{thms conjI} 1 THEN assume_tac ctxt' 1)
THEN TRY (assume_tac ctxt' 1)
in
@@ -205,7 +204,7 @@
val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *)
val intros =
if forall is_pred_equation specs then
- map (split_conjuncts_in_assms ctxt) (introrulify thy (map (rewrite ctxt) specs))
+ map (split_conjuncts_in_assms ctxt) (introrulify ctxt (map (rewrite ctxt) specs))
else if forall (is_intro constname) specs then
map (rewrite_intros ctxt) specs
else
--- a/src/HOL/Tools/datatype_realizer.ML Sat Jul 25 23:15:37 2015 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML Sat Jul 25 23:41:53 2015 +0200
@@ -105,15 +105,17 @@
(map (fn ((((i, _), T), U), tname) =>
make_pred i U T (mk_proj i is r) (Free (tname, T)))
(descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
- val inst = map (apply2 (Thm.cterm_of ctxt)) (map head_of (HOLogic.dest_conj
- (HOLogic.dest_Trueprop (Thm.concl_of induct))) ~~ ps);
+ val inst =
+ map (#1 o dest_Var o head_of)
+ (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of induct))) ~~
+ map (Thm.cterm_of ctxt) ps;
val thm =
Goal.prove_internal ctxt (map (Thm.cterm_of ctxt) prems) (Thm.cterm_of ctxt concl)
(fn prems =>
EVERY [
rewrite_goals_tac ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
- resolve_tac ctxt [cterm_instantiate inst induct] 1,
+ resolve_tac ctxt [infer_instantiate ctxt inst induct] 1,
ALLGOALS (Object_Logic.atomize_prems_tac ctxt),
rewrite_goals_tac ctxt (@{thm o_def} :: map mk_meta_eq rec_rewrites),
REPEAT ((resolve_tac ctxt prems THEN_ALL_NEW (fn i =>
@@ -190,7 +192,7 @@
(HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y']))))
(fn prems =>
EVERY [
- resolve_tac ctxt [cterm_instantiate [apply2 (Thm.cterm_of ctxt) (y, y')] exhaust] 1,
+ resolve_tac ctxt [infer_instantiate ctxt [(#1 (dest_Var y), Thm.cterm_of ctxt y')] exhaust] 1,
ALLGOALS (EVERY'
[asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps case_rewrites),
resolve_tac ctxt prems, asm_simp_tac (put_simpset HOL_basic_ss ctxt)])])
--- a/src/HOL/Tools/inductive_set.ML Sat Jul 25 23:15:37 2015 +0200
+++ b/src/HOL/Tools/inductive_set.ML Sat Jul 25 23:41:53 2015 +0200
@@ -223,12 +223,11 @@
let
val U = HOLogic.dest_setT (body_type T);
val Ts = HOLogic.strip_ptupleT fs' U;
- (* FIXME: should cterm_instantiate increment indexes? *)
val arg_cong' = Thm.incr_indexes (Thm.maxidx_of thm + 1) arg_cong;
- val (arg_cong_f, _) = arg_cong' |> Thm.cprop_of |> Drule.strip_imp_concl |>
- Thm.dest_comb |> snd |> Drule.strip_comb |> snd |> hd |> Thm.dest_comb
+ val (Var (arg_cong_f, _), _) = arg_cong' |> Thm.concl_of |>
+ dest_comb |> snd |> strip_comb |> snd |> hd |> dest_comb;
in
- thm' RS (Drule.cterm_instantiate [(arg_cong_f,
+ thm' RS (infer_instantiate ctxt [(arg_cong_f,
Thm.cterm_of ctxt (Abs ("P", Ts ---> HOLogic.boolT,
HOLogic.Collect_const U $ HOLogic.mk_psplits fs' U
HOLogic.boolT (Bound 0))))] arg_cong' RS sym)
--- a/src/HOL/Tools/set_comprehension_pointfree.ML Sat Jul 25 23:15:37 2015 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML Sat Jul 25 23:41:53 2015 +0200
@@ -495,9 +495,9 @@
fun instantiate_arg_cong ctxt pred =
let
val arg_cong = Thm.incr_indexes (maxidx_of_term pred + 1) @{thm arg_cong}
- val f $ _ = fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.concl_of arg_cong)))
+ val (Var (f, _) $ _, _) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.concl_of arg_cong))
in
- cterm_instantiate [(Thm.cterm_of ctxt f, Thm.cterm_of ctxt pred)] arg_cong
+ infer_instantiate ctxt [(f, Thm.cterm_of ctxt pred)] arg_cong
end;
fun simproc ctxt redex =
--- a/src/Provers/splitter.ML Sat Jul 25 23:15:37 2015 +0200
+++ b/src/Provers/splitter.ML Sat Jul 25 23:41:53 2015 +0200
@@ -317,9 +317,10 @@
val (cntxt, u) = mk_cntxt t pos (T --> U);
val trlift' = Thm.lift_rule (Thm.cprem_of state i)
(Thm.rename_boundvars abs_lift u trlift);
- val (P, _) = strip_comb (fst (Logic.dest_equals
- (Logic.strip_assums_concl (Thm.prop_of trlift'))));
- in cterm_instantiate [apply2 (Thm.cterm_of ctxt) (P, abss Ts cntxt)] trlift' end;
+ val (Var (P, _), _) =
+ strip_comb (fst (Logic.dest_equals
+ (Logic.strip_assums_concl (Thm.prop_of trlift'))));
+ in infer_instantiate ctxt [(P, Thm.cterm_of ctxt (abss Ts cntxt))] trlift' end;
(*************************************************************
@@ -338,10 +339,11 @@
fun inst_split ctxt Ts t tt thm TB state i =
let
val thm' = Thm.lift_rule (Thm.cprem_of state i) thm;
- val (P, _) = strip_comb (fst (Logic.dest_equals
- (Logic.strip_assums_concl (Thm.prop_of thm'))));
+ val (Var (P, _), _) =
+ strip_comb (fst (Logic.dest_equals
+ (Logic.strip_assums_concl (Thm.prop_of thm'))));
val cntxt = mk_cntxt_splitthm t tt TB;
- in cterm_instantiate [apply2 (Thm.cterm_of ctxt) (P, abss Ts cntxt)] thm' end;
+ in infer_instantiate ctxt [(P, Thm.cterm_of ctxt (abss Ts cntxt))] thm' end;
(*****************************************************************************