--- a/src/HOL/Tools/BNF/bnf_def.ML Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Sun Jul 26 17:24:54 2015 +0200
@@ -1368,7 +1368,7 @@
let
val rel_conversep_thm = Lazy.force rel_conversep;
val cts = map (SOME o Thm.cterm_of lthy) Rs;
- val rel_conversep_thm' = cterm_instantiate_pos cts rel_conversep_thm;
+ val rel_conversep_thm' = infer_instantiate' lthy cts rel_conversep_thm;
in
unfold_thms lthy @{thms conversep_iff} (rel_conversep_thm' RS @{thm predicate2_eqD})
|> singleton (Proof_Context.export names_lthy pre_names_lthy)
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sun Jul 26 17:24:54 2015 +0200
@@ -473,13 +473,12 @@
fun mk_flip (x, Type (_, [T1, Type (_, [T2, T3])])) =
Abs ("x", T1, Abs ("y", T2, Var (x, T2 --> T1 --> T3) $ Bound 0 $ Bound 1));
-fun flip_rels lthy n thm =
+fun flip_rels ctxt n thm =
let
val Rs = Term.add_vars (Thm.prop_of thm) [];
val Rs' = rev (drop (length Rs - n) Rs);
- val cRs = map (fn f => (Thm.cterm_of lthy (Var f), Thm.cterm_of lthy (mk_flip f))) Rs';
in
- Drule.cterm_instantiate cRs thm
+ infer_instantiate ctxt (map (fn f => (fst f, Thm.cterm_of ctxt (mk_flip f))) Rs') thm
end;
fun mk_ctor_or_dtor get_T Ts t =
@@ -599,7 +598,7 @@
Drule.dummy_thm
else
let val ctor' = mk_ctor Bs ctor in
- cterm_instantiate_pos [NONE, NONE, SOME (Thm.cterm_of lthy ctor')] arg_cong
+ infer_instantiate' lthy [NONE, NONE, SOME (Thm.cterm_of lthy ctor')] arg_cong
end;
fun mk_cIn ctor k xs =
@@ -616,7 +615,7 @@
fold_thms lthy [ctr_def']
(unfold_thms lthy (o_apply :: pre_map_def ::
(if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_map @ abs_inverses)
- (cterm_instantiate_pos (map (SOME o Thm.cterm_of lthy) fs @ [SOME cxIn])
+ (infer_instantiate' lthy (map (SOME o Thm.cterm_of lthy) fs @ [SOME cxIn])
(if fp = Least_FP then fp_map_thm
else fp_map_thm RS ctor_cong RS (ctor_dtor RS sym RS trans))))
|> singleton (Proof_Context.export names_lthy lthy);
@@ -626,7 +625,7 @@
(unfold_thms lthy (pre_set_defs @ fp_nesting_set_maps @ live_nesting_set_maps @
(if fp = Least_FP then [] else [dtor_ctor]) @ basic_sumprod_thms_set @
@{thms UN_Un sup_assoc[THEN sym]} @ abs_inverses)
- (cterm_instantiate_pos [SOME cxIn] fp_set_thm))
+ (infer_instantiate' lthy [SOME cxIn] fp_set_thm))
|> singleton (Proof_Context.export names_lthy lthy);
fun mk_set0_thms fp_set_thm = map2 (mk_set0_thm fp_set_thm) ctr_defs' cxIns;
@@ -644,7 +643,7 @@
(unfold_thms lthy (pre_rel_def :: abs_inverses @
(if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_rel @
@{thms vimage2p_def sum.inject sum.distinct(1)[THEN eq_False[THEN iffD2]]})
- (cterm_instantiate_pos (map (SOME o Thm.cterm_of lthy) Rs @ [SOME cxIn, SOME cyIn])
+ (infer_instantiate' lthy (map (SOME o Thm.cterm_of lthy) Rs @ [SOME cxIn, SOME cyIn])
fp_rel_thm))
|> postproc
|> singleton (Proof_Context.export names_lthy lthy);
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Sun Jul 26 17:24:54 2015 +0200
@@ -96,11 +96,9 @@
let
val fs = Term.add_vars (Thm.prop_of thm) []
|> filter (fn (_, Type (@{type_name fun}, [_, T'])) => T' <> HOLogic.boolT | _ => false);
- fun mk_cfp (f as (_, T)) =
- (Thm.cterm_of ctxt (Var f), Thm.cterm_of ctxt (mk_proj T (num_binder_types T) k));
- val cfps = map mk_cfp fs;
+ fun mk_inst (xi, T) = (xi, Thm.cterm_of ctxt (mk_proj T (num_binder_types T) k));
in
- Drule.cterm_instantiate cfps thm
+ infer_instantiate ctxt (map mk_inst fs) thm
end;
val co_induct_inst_as_projs_tac = PRIMITIVE oo co_induct_inst_as_projs;
@@ -185,7 +183,7 @@
rel_eqs =
let
val ctor_rec_transfers' =
- map (cterm_instantiate_pos (map SOME (passives @ actives))) ctor_rec_transfers;
+ map (infer_instantiate' ctxt (map SOME (passives @ actives))) ctor_rec_transfers;
val total_n = Integer.sum ns;
val True = @{term True};
in
@@ -288,8 +286,9 @@
fun mk_unfold_corec_type_tac dtor_corec_transfer corec_def =
let
val active :: actives' = actives;
- val dtor_corec_transfer' = cterm_instantiate_pos
- (SOME active :: map SOME passives @ map SOME actives') dtor_corec_transfer;
+ val dtor_corec_transfer' =
+ infer_instantiate' ctxt
+ (SOME active :: map SOME passives @ map SOME actives') dtor_corec_transfer;
in
HEADGOAL Goal.conjunction_tac THEN REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI)) THEN
unfold_thms_tac ctxt [corec_def] THEN
@@ -389,7 +388,7 @@
fun mk_map_disc_iff_tac ctxt ct exhaust discs maps =
TRYALL Goal.conjunction_tac THEN
- ALLGOALS (rtac ctxt (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
+ ALLGOALS (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW
REPEAT_DETERM o hyp_subst_tac ctxt) THEN
unfold_thms_tac ctxt maps THEN
unfold_thms_tac ctxt (map (fn thm => thm RS eqFalseI
@@ -398,7 +397,7 @@
fun mk_map_sel_tac ctxt ct exhaust discs maps sels map_id0s =
TRYALL Goal.conjunction_tac THEN
- ALLGOALS (rtac ctxt (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
+ ALLGOALS (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW
REPEAT_DETERM o hyp_subst_tac ctxt) THEN
unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @
@{thms not_True_eq_False not_False_eq_True}) THEN
@@ -407,8 +406,8 @@
ALLGOALS (rtac ctxt refl);
fun mk_rel_cases_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts rel_eqs=
- HEADGOAL (rtac ctxt (cterm_instantiate_pos [SOME ct1] exhaust) THEN_ALL_NEW
- rtac ctxt (cterm_instantiate_pos [SOME ct2] exhaust) THEN_ALL_NEW
+ HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct1] exhaust) THEN_ALL_NEW
+ rtac ctxt (infer_instantiate' ctxt [SOME ct2] exhaust) THEN_ALL_NEW
hyp_subst_tac ctxt) THEN
unfold_thms_tac ctxt (rel_eqs @ injects @ rel_injects @ @{thms conj_imp_eq_imp_imp simp_thms(6)
True_implies_equals conj_imp_eq_imp_imp} @
@@ -426,7 +425,7 @@
EVERY (@{map 11} (fn ct => fn assm => fn exhaust => fn discs => fn sels => fn ctor_defs =>
fn dtor_ctor => fn ctor_inject => fn abs_inject => fn rel_pre_def => fn abs_inverse =>
(rtac ctxt exhaust THEN_ALL_NEW (rtac ctxt exhaust THEN_ALL_NEW
- (dtac ctxt (rotate_prems ~1 (cterm_instantiate_pos [NONE, NONE, NONE, NONE, SOME ct]
+ (dtac ctxt (rotate_prems ~1 (infer_instantiate' ctxt [NONE, NONE, NONE, NONE, SOME ct]
@{thm arg_cong2} RS iffD1)) THEN'
assume_tac ctxt THEN' assume_tac ctxt THEN' hyp_subst_tac ctxt THEN' dtac ctxt assm THEN'
REPEAT_DETERM o etac ctxt conjE))) 1 THEN
@@ -445,7 +444,7 @@
rtac ctxt ctor_rel_induct 1 THEN EVERY (@{map 6} (fn cterm => fn exhaust => fn ctor_defs =>
fn ctor_inject => fn rel_pre_list_def => fn Abs_inverse =>
HEADGOAL (rtac ctxt exhaust THEN_ALL_NEW (rtac ctxt exhaust THEN_ALL_NEW
- (rtac ctxt (cterm_instantiate_pos (replicate 4 NONE @ [SOME cterm]) @{thm arg_cong2} RS iffD2)
+ (rtac ctxt (infer_instantiate' ctxt (replicate 4 NONE @ [SOME cterm]) @{thm arg_cong2} RS iffD2)
THEN' assume_tac ctxt THEN' assume_tac ctxt THEN' TRY o resolve_tac ctxt assms))) THEN
unfold_thms_tac ctxt (ctor_inject :: rel_pre_list_def :: ctor_defs @ nesting_rel_eqs @
@{thms id_bnf_def vimage2p_def}) THEN
@@ -457,8 +456,8 @@
cterms exhausts ctor_defss ctor_injects rel_pre_list_defs Abs_inverses);
fun mk_rel_sel_tac ctxt ct1 ct2 exhaust discs sels rel_injects distincts rel_distincts rel_eqs =
- HEADGOAL (rtac ctxt (cterm_instantiate_pos [SOME ct1] exhaust) THEN_ALL_NEW
- rtac ctxt (cterm_instantiate_pos [SOME ct2] exhaust) THEN_ALL_NEW
+ HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct1] exhaust) THEN_ALL_NEW
+ rtac ctxt (infer_instantiate' ctxt [SOME ct2] exhaust) THEN_ALL_NEW
hyp_subst_tac ctxt) THEN
unfold_thms_tac ctxt (sels @ rel_injects @ rel_eqs @
@{thms simp_thms(6,7,8,11,12,15,16,21,22,24)} @ ((discs @ distincts) RL [eqTrueI, eqFalseI]) @
@@ -473,7 +472,7 @@
fun mk_set_sel_tac ctxt ct exhaust discs sels sets =
TRYALL Goal.conjunction_tac THEN
- ALLGOALS (rtac ctxt (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
+ ALLGOALS (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW
REPEAT_DETERM o hyp_subst_tac ctxt) THEN
unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @
@{thms not_True_eq_False not_False_eq_True}) THEN
@@ -485,7 +484,7 @@
(rtac ctxt @{thm singletonI} ORELSE' assume_tac ctxt));
fun mk_set_cases_tac ctxt ct assms exhaust sets =
- HEADGOAL (rtac ctxt (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW hyp_subst_tac ctxt) THEN
+ HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW hyp_subst_tac ctxt) THEN
unfold_thms_tac ctxt sets THEN
REPEAT_DETERM (HEADGOAL
(eresolve_tac ctxt @{thms FalseE emptyE singletonE UnE UN_E insertE} ORELSE'
@@ -509,12 +508,12 @@
(etac ctxt FalseE)
end;
val exhausts' = map (fn thm => thm RS @{thm asm_rl[of "P x y" for P x y]}) exhausts
- |> map2 (fn ct => cterm_instantiate_pos [NONE, SOME ct]) cts;
+ |> map2 (fn ct => infer_instantiate' ctxt [NONE, SOME ct]) cts;
in
ALLGOALS (resolve_tac ctxt dtor_set_inducts) THEN
TRYALL (resolve_tac ctxt exhausts' THEN_ALL_NEW
(resolve_tac ctxt (map (fn ct => refl RS
- cterm_instantiate_pos (replicate 4 NONE @ [SOME ct]) @{thm arg_cong2} RS iffD2) cts)
+ infer_instantiate' ctxt (replicate 4 NONE @ [SOME ct]) @{thm arg_cong2} RS iffD2) cts)
THEN' assume_tac ctxt THEN' hyp_subst_tac ctxt)) THEN
unfold_thms_tac ctxt (Abs_pre_inverses @ dtor_ctors @ set_pre_defs @ ctor_defs @
@{thms id_bnf_def o_apply sum_set_simps prod_set_simps UN_empty UN_insert Un_empty_left
--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML Sun Jul 26 17:24:54 2015 +0200
@@ -44,7 +44,7 @@
val else_branch = Var (("e", j), T);
val lam = Term.lambda cond (mk_If cond then_branch else_branch);
in
- cterm_instantiate_pos [SOME (Thm.cterm_of ctxt lam)] thm
+ infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt lam)] thm
end;
val transfer_rules =
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Sun Jul 26 17:24:54 2015 +0200
@@ -2223,9 +2223,10 @@
fun mk_helper_coind_thms fst concl cts =
Goal.prove_sorry lthy [] [] (Logic.list_implies (helper_prems, concl))
- (fn {context = ctxt, prems = _} => mk_rel_coinduct_coind_tac ctxt fst m
- (cterm_instantiate_pos cts dtor_coinduct_thm) ks map_comps map_cong0s
- map_arg_cong_thms set_mapss dtor_unfold_thms dtor_Jmap_thms in_rels)
+ (fn {context = ctxt, prems = _} =>
+ mk_rel_coinduct_coind_tac ctxt fst m
+ (infer_instantiate' ctxt cts dtor_coinduct_thm) ks map_comps map_cong0s
+ map_arg_cong_thms set_mapss dtor_unfold_thms dtor_Jmap_thms in_rels)
|> Thm.close_derivation
|> split_conj_thm
|> Proof_Context.export names_lthy lthy;
@@ -2261,8 +2262,9 @@
val helper_ind_thmss = if m = 0 then replicate n [] else
@{map 4} (fn concl => fn j => fn set_induct => fn cts =>
Goal.prove_sorry lthy [] [] (Logic.list_implies (helper_prems, concl))
- (fn {context = ctxt, prems = _} => mk_rel_coinduct_ind_tac ctxt m ks
- dtor_unfold_thms set_mapss j (cterm_instantiate_pos cts set_induct))
+ (fn {context = ctxt, prems = _} =>
+ mk_rel_coinduct_ind_tac ctxt m ks
+ dtor_unfold_thms set_mapss j (infer_instantiate' ctxt cts set_induct))
|> Thm.close_derivation
|> split_conj_thm
|> Proof_Context.export names_lthy lthy)
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Sun Jul 26 17:24:54 2015 +0200
@@ -43,13 +43,9 @@
let
val num_frees = length frees;
val fs = Term.add_vars (Thm.prop_of thm) [] |> filter (can dest_funT o snd);
- fun find s = find_index (curry (op =) s) frees;
- fun mk_cfp (f as ((s, _), T)) =
- (Thm.cterm_of ctxt (Var f), Thm.cterm_of ctxt (mk_proj T num_frees (find s)));
- val cfps = map mk_cfp fs;
- in
- Drule.cterm_instantiate cfps thm
- end;
+ fun find x = find_index (curry (op =) x) frees;
+ fun mk_inst ((x, i), T) = ((x, i), Thm.cterm_of ctxt (mk_proj T num_frees (find x)));
+ in infer_instantiate ctxt (map mk_inst fs) thm end;
val exhaust_inst_as_projs_tac = PRIMITIVE oo exhaust_inst_as_projs;
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Sun Jul 26 17:24:54 2015 +0200
@@ -783,7 +783,8 @@
val car_inits = map (mk_min_alg str_inits) ks;
- val alg_init_thm = cterm_instantiate_pos (map (SOME o Thm.cterm_of lthy) str_inits) alg_min_alg_thm;
+ val alg_init_thm =
+ infer_instantiate' lthy (map (SOME o Thm.cterm_of lthy) str_inits) alg_min_alg_thm;
val alg_select_thm = Goal.prove_sorry lthy [] []
(HOLogic.mk_Trueprop (mk_Ball II
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Sun Jul 26 17:24:54 2015 +0200
@@ -68,7 +68,7 @@
IF_UNSOLVED (unfold_thms_tac ctxt @{thms id_def o_def} THEN HEADGOAL (rtac ctxt refl));
fun mk_size_neq ctxt cts exhaust sizes =
- HEADGOAL (rtac ctxt (Ctr_Sugar_Util.cterm_instantiate_pos (map SOME cts) exhaust)) THEN
+ HEADGOAL (rtac ctxt (infer_instantiate' ctxt (map SOME cts) exhaust)) THEN
ALLGOALS (hyp_subst_tac ctxt) THEN
Ctr_Sugar_Tactics.unfold_thms_tac ctxt (@{thm neq0_conv} :: sizes) THEN
ALLGOALS (REPEAT_DETERM o (rtac ctxt @{thm zero_less_Suc} ORELSE' rtac ctxt @{thm trans_less_add2}));
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Sun Jul 26 17:24:54 2015 +0200
@@ -376,7 +376,7 @@
REPEAT_DETERM_N n o rtac ctxt @{thm Collect_restrict}, rtac ctxt CollectI,
REPEAT_DETERM_N (m + n) o (TRY o rtac ctxt conjI THEN' assume_tac ctxt)];
fun cong_tac ct map_cong0 = EVERY'
- [rtac ctxt (map_cong0 RS cterm_instantiate_pos [NONE, NONE, SOME ct] arg_cong),
+ [rtac ctxt (map_cong0 RS infer_instantiate' ctxt [NONE, NONE, SOME ct] arg_cong),
REPEAT_DETERM_N m o rtac ctxt refl,
REPEAT_DETERM_N n o (etac ctxt @{thm prop_restrict} THEN' assume_tac ctxt)];
@@ -434,7 +434,7 @@
CONJ_WRAP' (K (rtac ctxt ballI THEN' rtac ctxt UNIV_I)) Abs_inverses,
CONJ_WRAP' (fn (ct, thm) =>
EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE],
- rtac ctxt (thm RS (cterm_instantiate_pos [NONE, NONE, SOME ct] arg_cong) RS sym),
+ rtac ctxt (thm RS (infer_instantiate' ctxt [NONE, NONE, SOME ct] arg_cong) RS sym),
EVERY' (map (fn Abs_inverse =>
EVERY' [rtac ctxt (o_apply RS trans RS ballI), etac ctxt (set_mp RS Abs_inverse),
assume_tac ctxt])
@@ -559,7 +559,7 @@
fun mk_set_nat cset ctor_map ctor_set set_nats =
EVERY' [rtac ctxt trans, rtac ctxt @{thm image_cong}, rtac ctxt ctor_set, rtac ctxt refl, rtac ctxt sym,
- rtac ctxt (trans OF [ctor_map RS cterm_instantiate_pos [NONE, NONE, SOME cset] arg_cong,
+ rtac ctxt (trans OF [ctor_map RS infer_instantiate' ctxt [NONE, NONE, SOME cset] arg_cong,
ctor_set RS trans]),
rtac ctxt sym, EVERY' (map (rtac ctxt) [trans, @{thm image_Un}, Un_cong]),
rtac ctxt sym, rtac ctxt (nth set_nats (i - 1)),
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML Sun Jul 26 17:24:54 2015 +0200
@@ -99,7 +99,7 @@
fun mk_disc_eq_case_tac ctxt ct exhaust discs distincts cases =
HEADGOAL Goal.conjunction_tac THEN
- ALLGOALS (rtac ctxt (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
+ ALLGOALS (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW
(hyp_subst_tac ctxt THEN'
SELECT_GOAL (unfold_thms_tac ctxt (@{thms not_True_eq_False not_False_eq_True} @ cases @
((refl :: discs @ distincts) RL [eqTrueI, eqFalseI]))) THEN'
@@ -161,7 +161,7 @@
end;
fun mk_case_distrib_tac ctxt ct exhaust cases =
- HEADGOAL (rtac ctxt (cterm_instantiate_pos [SOME ct] exhaust)) THEN
+ HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust)) THEN
ALLGOALS (hyp_subst_tac ctxt THEN' SELECT_GOAL (unfold_thms_tac ctxt cases) THEN' rtac ctxt refl);
fun mk_case_cong_tac ctxt uexhaust cases =
--- a/src/HOL/Tools/Function/partial_function.ML Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML Sun Jul 26 17:24:54 2015 +0200
@@ -107,17 +107,6 @@
(*** Auxiliary functions ***)
-(*positional instantiation with computed type substitution.
- internal version of attribute "[of s t u]".*)
-fun cterm_instantiate' cts thm =
- let
- val thy = Thm.theory_of_thm thm;
- val vs = rev (Term.add_vars (Thm.prop_of thm) [])
- |> map (Thm.global_cterm_of thy o Var);
- in
- cterm_instantiate (zip_options vs cts) thm
- end;
-
(*Returns t $ u, but instantiates the type of t to make the
application type correct*)
fun apply_inst ctxt t u =
@@ -168,13 +157,13 @@
curry induction predicate *)
fun specialize_fixp_induct ctxt args fT fT_uc F curry uncurry mono_thm f_def rule =
let
- val cert = Thm.cterm_of ctxt
val ([P], ctxt') = Variable.variant_fixes ["P"] ctxt
val P_inst = Abs ("f", fT_uc, Free (P, fT --> HOLogic.boolT) $ (curry $ Bound 0))
in
(* FIXME ctxt vs. ctxt' (!?) *)
rule
- |> cterm_instantiate' [SOME (cert uncurry), NONE, SOME (cert curry), NONE, SOME (cert P_inst)]
+ |> infer_instantiate' ctxt
+ ((map o Option.map) (Thm.cterm_of ctxt) [SOME uncurry, NONE, SOME curry, NONE, SOME P_inst])
|> Tactic.rule_by_tactic ctxt
(Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 3 (* discharge U (C f) = f *)
THEN Simplifier.simp_tac (put_simpset curry_K_ss ctxt) 4 (* simplify bot case *)
@@ -235,7 +224,6 @@
val ((f_binding, fT), mixfix) = the_single fixes;
val fname = Binding.name_of f_binding;
- val cert = Thm.cterm_of lthy;
val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop plain_eqn);
val (head, args) = strip_comb lhs;
val argnames = map (fst o dest_Free) args;
@@ -258,9 +246,9 @@
|> HOLogic.mk_Trueprop
|> Logic.all x_uc;
- val mono_thm = Goal.prove_internal lthy [] (cert mono_goal)
+ val mono_thm = Goal.prove_internal lthy [] (Thm.cterm_of lthy mono_goal)
(K (mono_tac lthy 1))
- val inst_mono_thm = Thm.forall_elim (cert x_uc) mono_thm
+ val inst_mono_thm = Thm.forall_elim (Thm.cterm_of lthy x_uc) mono_thm
val f_def_rhs = curry_n arity (apply_inst lthy fixp F_uc);
val f_def_binding = Binding.concealed (Binding.name (Thm.def_name fname));
@@ -272,7 +260,7 @@
|> HOLogic.mk_Trueprop;
val unfold =
- (cterm_instantiate' (map (SOME o cert) [uncurry, F, curry]) fixp_eq
+ (infer_instantiate' lthy' (map (SOME o Thm.cterm_of lthy') [uncurry, F, curry]) fixp_eq
OF [inst_mono_thm, f_def])
|> Tactic.rule_by_tactic lthy' (Simplifier.simp_tac (put_simpset curry_uncurry_ss lthy') 1);
@@ -281,10 +269,12 @@
|> Drule.rename_bvars' (map SOME (fname :: fname :: argnames));
val mk_raw_induct =
- cterm_instantiate' [SOME (cert uncurry), NONE, SOME (cert curry)]
+ infer_instantiate' args_ctxt
+ ((map o Option.map) (Thm.cterm_of args_ctxt) [SOME uncurry, NONE, SOME curry])
#> mk_curried_induct args args_ctxt
#> singleton (Variable.export args_ctxt lthy')
- #> (fn thm => cterm_instantiate' [SOME (cert F)] thm OF [inst_mono_thm, f_def])
+ #> (fn thm => infer_instantiate' lthy'
+ [SOME (Thm.cterm_of lthy' F)] thm OF [inst_mono_thm, f_def])
#> Drule.rename_bvars' (map SOME (fname :: argnames @ argnames))
val raw_induct = Option.map mk_raw_induct fixp_induct_user
--- a/src/HOL/Tools/Function/termination.ML Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/Function/termination.ML Sun Jul 26 17:24:54 2015 +0200
@@ -299,9 +299,11 @@
THEN' (blast_tac ctxt))) (* Solve rest of context... not very elegant *)
) i
in
- (PRIMITIVE (Drule.cterm_instantiate [apply2 (Thm.cterm_of ctxt) (rel, relation)])
- THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i)
- THEN rewrite_goal_tac ctxt Un_aci_simps 1) (* eliminate duplicates *)
+ if is_Var rel then
+ PRIMITIVE (infer_instantiate ctxt [(#1 (dest_Var rel), Thm.cterm_of ctxt relation)])
+ THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i)
+ THEN rewrite_goal_tac ctxt Un_aci_simps 1 (* eliminate duplicates *)
+ else no_tac
end) 1 st
end
--- a/src/HOL/Tools/Lifting/lifting_def.ML Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Sun Jul 26 17:24:54 2015 +0200
@@ -183,19 +183,17 @@
val param_rel = (snd o dest_comb o fst o dest_comb) tm;
val free_vars = Term.add_vars param_rel [];
- fun make_subst (var as (_, typ)) subst =
+ fun make_subst (xi, typ) subst =
let
val [rty, rty'] = binder_types typ
in
- if (Term.is_TVar rty andalso is_Type rty') then
- (Var var, HOLogic.eq_const rty')::subst
+ if Term.is_TVar rty andalso is_Type rty' then
+ (xi, Thm.cterm_of ctxt (HOLogic.eq_const rty')) :: subst
else
subst
end;
-
- val subst = fold make_subst free_vars [];
- val csubst = map (apply2 (Thm.cterm_of ctxt)) subst;
- val inst_thm = Drule.cterm_instantiate csubst thm;
+
+ val inst_thm = infer_instantiate ctxt (fold make_subst free_vars []) thm;
in
Conv.fconv_rule
((Conv.concl_conv (Thm.nprems_of inst_thm) o
@@ -212,10 +210,9 @@
val fun2 = Thm.cterm_of ctxt (strip_args 2 t2)
val args2 = map (Thm.cterm_of ctxt) (get_args 1 t2)
val relcomppI = Drule.incr_indexes2 ant1 ant2 @{thm relcomppI}
- val vars = (rev (Term.add_vars (Thm.prop_of relcomppI) []))
- val subst = map (apfst (Thm.cterm_of ctxt o Var)) (vars ~~ ([fun1] @ args1 @ [fun2] @ args2))
+ val vars = map #1 (rev (Term.add_vars (Thm.prop_of relcomppI) []))
in
- Drule.cterm_instantiate subst relcomppI
+ infer_instantiate ctxt (vars ~~ ([fun1] @ args1 @ [fun2] @ args2)) relcomppI
end
fun zip_transfer_rules ctxt thm =
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Sun Jul 26 17:24:54 2015 +0200
@@ -217,9 +217,9 @@
(quot_thm, (lthy, rel_eq_onps))
end;
-fun case_tac rule ctxt i st =
- (Subgoal.FOCUS_PARAMS (fn {params, ...} => HEADGOAL(rtac ctxt
- (Ctr_Sugar_Util.cterm_instantiate_pos [SOME (params |> hd |> snd)] rule))) ctxt i st);
+fun case_tac rule =
+ Subgoal.FOCUS_PARAMS (fn {context = ctxt, params, ...} =>
+ HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME (snd (hd params))] rule)));
fun bundle_name_of_bundle_binding binding phi context =
Name_Space.full_name (Name_Space.naming_of context) (Morphism.binding phi binding);
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Sun Jul 26 17:24:54 2015 +0200
@@ -132,18 +132,17 @@
fun make_inst var ctxt =
let
- val typ = (snd o relation_types o snd o dest_Var) var
+ val typ = snd (relation_types (#2 (dest_Var var)))
val sort = Type.sort_of_atyp typ
val (fresh_var, ctxt') = yield_singleton Variable.invent_types sort ctxt
- in
- (apply2 (Thm.cterm_of ctxt') (var, HOLogic.eq_const (TFree fresh_var)), ctxt')
- end
+ val inst = (#1 (dest_Var var), Thm.cterm_of ctxt' (HOLogic.eq_const (TFree fresh_var)))
+ in (inst, ctxt') end
val orig_lthy = lthy
val (args_inst, lthy) = fold_map make_inst args lthy
val pcr_cr_eq =
pcr_rel_def
- |> Drule.cterm_instantiate args_inst
+ |> infer_instantiate lthy args_inst
|> Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv
(Transfer.bottom_rewr_conv (Transfer.get_relator_eq lthy))))
in
@@ -403,9 +402,9 @@
@{thm id_transfer}
|> Thm.incr_indexes (Term.maxidx_of_term parametrized_relator + 1)
|> Conv.fconv_rule(HOLogic.Trueprop_conv (Conv.arg_conv id_unfold then_conv Conv.arg1_conv id_unfold))
- val var = Var (hd (Term.add_vars (Thm.prop_of id_transfer) []))
- val inst = [(Thm.cterm_of lthy var, Thm.cterm_of lthy parametrized_relator)]
- val id_par_thm = Drule.cterm_instantiate inst id_transfer
+ val var = hd (Term.add_vars (Thm.prop_of id_transfer) [])
+ val inst = [(#1 var, Thm.cterm_of lthy parametrized_relator)]
+ val id_par_thm = infer_instantiate lthy inst id_transfer
in
Lifting_Def.generate_parametric_transfer_rule lthy id_transfer_rule id_par_thm
end
--- a/src/HOL/Tools/coinduction.ML Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/coinduction.ML Sun Jul 26 17:24:54 2015 +0200
@@ -80,15 +80,14 @@
|> Term.map_abs_vars (Variable.revert_fixed ctxt)
|> fold_rev Term.absfree (names ~~ Ts)
|> Thm.cterm_of ctxt;
- val thm = Ctr_Sugar_Util.cterm_instantiate_pos [SOME phi] raw_thm;
+ val thm = infer_instantiate' ctxt [SOME phi] raw_thm;
val e = length eqs;
val p = length prems;
in
HEADGOAL (EVERY' [resolve_tac ctxt [thm],
EVERY' (map (fn var =>
resolve_tac ctxt
- [Ctr_Sugar_Util.cterm_instantiate_pos
- [NONE, SOME (Thm.cterm_of ctxt var)] exI]) vars),
+ [infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt var)] exI]) vars),
if p = 0 then Ctr_Sugar_Util.CONJ_WRAP' (K (resolve_tac ctxt [refl])) eqs
else
REPEAT_DETERM_N e o (resolve_tac ctxt [conjI] THEN' resolve_tac ctxt [refl]) THEN'
--- a/src/HOL/Tools/inductive.ML Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/inductive.ML Sun Jul 26 17:24:54 2015 +0200
@@ -639,11 +639,11 @@
| _ => error
("equations matching pattern " ^ Syntax.string_of_term ctxt prop ^ " is not unique"));
val inst =
- map (fn v => apply2 (Thm.cterm_of ctxt') (Var v, Envir.subst_term subst (Var v)))
+ map (fn v => (fst v, Thm.cterm_of ctxt' (Envir.subst_term subst (Var v))))
(Term.add_vars (lhs_of eq) []);
in
- Drule.cterm_instantiate inst eq
- |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (Simplifier.full_rewrite ctxt)))
+ infer_instantiate ctxt' inst eq
+ |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (Simplifier.full_rewrite ctxt')))
|> singleton (Variable.export ctxt' ctxt)
end
--- a/src/HOL/Tools/legacy_transfer.ML Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/legacy_transfer.ML Sun Jul 26 17:24:54 2015 +0200
@@ -130,7 +130,7 @@
put_simpset HOL_ss ctxt5 addsimps (inj @ embed @ return)
|> fold Simplifier.add_cong cong;
val thm' = thm
- |> Drule.cterm_instantiate (c_vars ~~ c_exprs')
+ |> infer_instantiate ctxt5 (map (#1 o dest_Var o Thm.term_of) c_vars ~~ c_exprs')
|> fold_rev Thm.implies_intr (map Thm.cprop_of hyps)
|> Simplifier.asm_full_simplify simpset
in singleton (Variable.export ctxt5 ctxt1) thm' end;
--- a/src/Tools/cong_tac.ML Sun Jul 26 12:24:16 2015 +0200
+++ b/src/Tools/cong_tac.ML Sun Jul 26 17:24:54 2015 +0200
@@ -23,11 +23,11 @@
val _ $ (_ $ (f' $ x') $ (g' $ y')) = Logic.strip_assums_concl (Thm.prop_of cong');
val ps = Logic.strip_params (Thm.concl_of cong');
val insts =
- [(f', f), (g', g), (x', x), (y', y)]
- |> map (fn (t, u) => apply2 (Thm.cterm_of ctxt) (Term.head_of t, fold_rev Term.abs ps u));
+ [(f', f), (g', g), (x', x), (y', y)] |> map (fn (t, u) =>
+ (#1 (dest_Var (head_of t)), Thm.cterm_of ctxt (fold_rev Term.abs ps u)));
in
fn st =>
- compose_tac ctxt (false, Drule.cterm_instantiate insts cong', 2) i st
+ compose_tac ctxt (false, infer_instantiate ctxt insts cong', 2) i st
handle THM _ => no_tac st
end
| _ => no_tac)
--- a/src/Tools/induct.ML Sun Jul 26 12:24:16 2015 +0200
+++ b/src/Tools/induct.ML Sun Jul 26 17:24:54 2015 +0200
@@ -390,14 +390,12 @@
fun prep_inst ctxt align tune (tm, ts) =
let
- fun prep_var (x, SOME t) =
+ fun prep_var (Var (x, xT), SOME t) =
let
- val cx = Thm.cterm_of ctxt x;
- val xT = Thm.typ_of_cterm cx;
val ct = Thm.cterm_of ctxt (tune t);
val tT = Thm.typ_of_cterm ct;
in
- if Type.could_unify (tT, xT) then SOME (cx, ct)
+ if Type.could_unify (tT, xT) then SOME (x, ct)
else error (Pretty.string_of (Pretty.block
[Pretty.str "Ill-typed instantiation:", Pretty.fbrk,
Syntax.pretty_term ctxt (Thm.term_of ct), Pretty.str " ::", Pretty.brk 1,
@@ -478,7 +476,7 @@
else
(align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
|> maps (prep_inst ctxt align_left I)
- |> Drule.cterm_instantiate) r)
+ |> infer_instantiate ctxt) r)
|> simp ? mark_constraints (Rule_Cases.get_constraints r) ctxt
|> pair (Rule_Cases.get r);
@@ -557,7 +555,7 @@
(* prepare rule *)
fun rule_instance ctxt inst rule =
- Drule.cterm_instantiate (prep_inst ctxt align_left I (Thm.prop_of rule, inst)) rule;
+ infer_instantiate ctxt (prep_inst ctxt align_left I (Thm.prop_of rule, inst)) rule;
fun internalize ctxt k th =
th |> Thm.permute_prems 0 k
@@ -658,10 +656,9 @@
|> Thm.lift_rule (Thm.cterm_of ctxt prfx)
|> `(Thm.prop_of #> Logic.strip_assums_concl)
|-> (fn pred $ arg =>
- Drule.cterm_instantiate
- (map (apply2 (Thm.cterm_of ctxt))
- [(Term.head_of pred, Logic.rlist_abs (xs, body)),
- (Term.head_of arg, Logic.rlist_abs (xs, v))]));
+ infer_instantiate ctxt
+ [(#1 (dest_Var (head_of pred)), Thm.cterm_of ctxt (Logic.rlist_abs (xs, body))),
+ (#1 (dest_Var (head_of arg)), Thm.cterm_of ctxt (Logic.rlist_abs (xs, v)))]);
fun goal_concl k xs (Const (@{const_name Pure.all}, _) $ Abs (a, T, B)) =
goal_concl k ((a, T) :: xs) B
@@ -745,7 +742,7 @@
else (align_left "Rule has fewer conclusions than arguments given"
(map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
|> maps (prep_inst ctxt align_right (atomize_term ctxt))
- |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
+ |> infer_instantiate ctxt) r |> pair (Rule_Cases.get r))
|> mod_cases
|> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
@@ -828,7 +825,8 @@
let
fun inst_rule r =
if null inst then `Rule_Cases.get r
- else Drule.cterm_instantiate (prep_inst ctxt align_right I (main_prop_of r, inst)) r
+ else
+ infer_instantiate ctxt (prep_inst ctxt align_right I (main_prop_of r, inst)) r
|> pair (Rule_Cases.get r);
in
fn st =>