--- a/src/Doc/Implementation/Logic.thy Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Doc/Implementation/Logic.thy Fri Sep 10 14:59:19 2021 +0200
@@ -586,8 +586,7 @@
@{define_ML Thm.implies_intr: "cterm -> thm -> thm"} \\
@{define_ML Thm.implies_elim: "thm -> thm -> thm"} \\
@{define_ML Thm.generalize: "Names.set * Names.set -> int -> thm -> thm"} \\
- @{define_ML Thm.instantiate: "((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
- -> thm -> thm"} \\
+ @{define_ML Thm.instantiate: "ctyp TVars.table * cterm Vars.table -> thm -> thm"} \\
@{define_ML Thm.add_axiom: "Proof.context ->
binding * term -> theory -> (string * thm) * theory"} \\
@{define_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory ->
--- a/src/HOL/Analysis/normarith.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Analysis/normarith.ML Fri Sep 10 14:59:19 2021 +0200
@@ -322,7 +322,8 @@
(fn t => null (FuncUtil.Ctermfunc.dom (vector_lincomb t))) (map snd rawdests)
in fst (RealArith.real_linear_prover translator
- (map (fn t => Drule.instantiate_normalize ([(tv_n, Thm.ctyp_of_cterm t)],[]) pth_zero)
+ (map (fn t =>
+ Drule.instantiate_normalize (TVars.make [(tv_n, Thm.ctyp_of_cterm t)], Vars.empty) pth_zero)
zerodests,
map (fconv_rule (try_conv (Conv.top_sweep_conv (K (norm_canon_conv ctxt)) ctxt) then_conv
arg_conv (arg_conv real_poly_conv))) ges',
@@ -365,7 +366,7 @@
val shs = filter (member (fn (t,th) => t aconvc Thm.cprop_of th) asl) (Thm.chyps_of th1)
val th11 = hd (Variable.export ctxt' ctxt [fold Thm.implies_intr shs th1])
val cps = map (swap o Thm.dest_equals) (cprems_of th11)
- val th12 = Drule.instantiate_normalize ([], map (apfst (dest_Var o Thm.term_of)) cps) th11
+ val th12 = Drule.instantiate_normalize (TVars.empty, Vars.make (map (apfst (dest_Var o Thm.term_of)) cps)) th11
val th13 = fold Thm.elim_implies (map (Thm.reflexive o snd) cps) th12;
in hd (Variable.export ctxt' ctxt [th13])
end
--- a/src/HOL/Decision_Procs/approximation.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Decision_Procs/approximation.ML Fri Sep 10 14:59:19 2021 +0200
@@ -75,9 +75,10 @@
|> HOLogic.mk_list \<^typ>\<open>nat\<close>
|> Thm.cterm_of ctxt
in
- (resolve_tac ctxt [Thm.instantiate ([], [((("n", 0), \<^typ>\<open>nat\<close>), n),
- ((("prec", 0), \<^typ>\<open>nat\<close>), p),
- ((("ss", 0), \<^typ>\<open>nat list\<close>), s)])
+ (resolve_tac ctxt [Thm.instantiate (TVars.empty,
+ Vars.make [((("n", 0), \<^typ>\<open>nat\<close>), n),
+ ((("prec", 0), \<^typ>\<open>nat\<close>), p),
+ ((("ss", 0), \<^typ>\<open>nat list\<close>), s)])
@{thm approx_form}] i
THEN simp_tac (put_simpset (simpset_of \<^context>) ctxt) i) st
end
@@ -92,9 +93,10 @@
val s = vs |> map lookup_splitting |> hd
|> Thm.cterm_of ctxt
in
- resolve_tac ctxt [Thm.instantiate ([], [((("s", 0), \<^typ>\<open>nat\<close>), s),
- ((("t", 0), \<^typ>\<open>nat\<close>), t),
- ((("prec", 0), \<^typ>\<open>nat\<close>), p)])
+ resolve_tac ctxt [Thm.instantiate (TVars.empty,
+ Vars.make [((("s", 0), \<^typ>\<open>nat\<close>), s),
+ ((("t", 0), \<^typ>\<open>nat\<close>), t),
+ ((("prec", 0), \<^typ>\<open>nat\<close>), p)])
@{thm approx_tse_form}] i st
end
end
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Fri Sep 10 14:59:19 2021 +0200
@@ -68,8 +68,8 @@
fun fw mi th th' th'' =
let
val th0 = if mi then
- Drule.instantiate_normalize ([],[(p1_v, p1),(p2_v, p2),(mp1_v, mp1), (mp2_v, mp2)]) th
- else Drule.instantiate_normalize ([],[(p1_v, p1),(p2_v, p2),(mp1_v, pp1), (mp2_v, pp2)]) th
+ Drule.instantiate_normalize (TVars.empty, Vars.make [(p1_v, p1),(p2_v, p2),(mp1_v, mp1), (mp2_v, mp2)]) th
+ else Drule.instantiate_normalize (TVars.empty, Vars.make [(p1_v, p1),(p2_v, p2),(mp1_v, pp1), (mp2_v, pp2)]) th
in Thm.implies_elim (Thm.implies_elim th0 th') th'' end
in (fw true th1 th_1 th_1', fw false th2 th_2 th_2',
fw true th3 th_3 th_3', fw false th4 th_4 th_4', fw true th5 th_5 th_5')
@@ -115,11 +115,11 @@
val [pinf_conj, pinf_disj, pinf_eq, pinf_neq, pinf_lt,
pinf_le, pinf_gt, pinf_ge, pinf_P] = pinf
val [nmi_conj, nmi_disj, nmi_eq, nmi_neq, nmi_lt,
- nmi_le, nmi_gt, nmi_ge, nmi_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) nmi
+ nmi_le, nmi_gt, nmi_ge, nmi_P] = map (Drule.instantiate_normalize (TVars.empty, Vars.make [(U_v,cU)])) nmi
val [npi_conj, npi_disj, npi_eq, npi_neq, npi_lt,
- npi_le, npi_gt, npi_ge, npi_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) npi
+ npi_le, npi_gt, npi_ge, npi_P] = map (Drule.instantiate_normalize (TVars.empty, Vars.make [(U_v,cU)])) npi
val [ld_conj, ld_disj, ld_eq, ld_neq, ld_lt,
- ld_le, ld_gt, ld_ge, ld_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) ld
+ ld_le, ld_gt, ld_ge, ld_P] = map (Drule.instantiate_normalize (TVars.empty, Vars.make [(U_v,cU)])) ld
fun decomp_mpinf fm =
case Thm.term_of fm of
--- a/src/HOL/Decision_Procs/ferrante_rackoff_data.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff_data.ML Fri Sep 10 14:59:19 2021 +0200
@@ -73,7 +73,7 @@
let
fun h instT =
let
- val substT = Thm.instantiate (instT, []);
+ val substT = Thm.instantiate (instT, Vars.empty);
val substT_cterm = Drule.cterm_rule substT;
val minf' = map substT minf
--- a/src/HOL/Decision_Procs/langford_data.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Decision_Procs/langford_data.ML Fri Sep 10 14:59:19 2021 +0200
@@ -50,7 +50,7 @@
let
fun h instT =
let
- val substT = Thm.instantiate (instT, []);
+ val substT = Thm.instantiate (instT, Vars.empty);
val substT_cterm = Drule.cterm_rule substT;
val qe_bnds' = substT qe_bnds;
--- a/src/HOL/Eisbach/eisbach_rule_insts.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Eisbach/eisbach_rule_insts.ML Fri Sep 10 14:59:19 2021 +0200
@@ -69,7 +69,7 @@
val (instT, inst) = fold add_inst insts ([], []);
in
- (Thm.instantiate (instT, []) thm
+ (Thm.instantiate (TVars.make instT, Vars.empty) thm
|> infer_instantiate ctxt inst
COMP_INCR asm_rl)
|> Thm.adjust_maxidx_thm ~1
--- a/src/HOL/Eisbach/match_method.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Eisbach/match_method.ML Fri Sep 10 14:59:19 2021 +0200
@@ -431,7 +431,7 @@
val (prem_ids, ctxt') = context
|> add_focus_params params
- |> add_focus_schematics (snd schematics)
+ |> add_focus_schematics (Vars.dest (snd schematics))
|> fold_map add_focus_prem (rev prems)
in
@@ -455,10 +455,10 @@
val schematic_terms =
Vars.fold (fn (v, t) => cons (v, Thm.cterm_of ctxt'' t)) inst [];
- val goal'' = Thm.instantiate ([], schematic_terms) goal';
- val concl' = Thm.instantiate_cterm ([], schematic_terms) concl;
+ val goal'' = Thm.instantiate (TVars.empty, Vars.make schematic_terms) goal';
+ val concl' = Thm.instantiate_cterm (TVars.empty, Vars.make schematic_terms) concl;
val (schematic_types, schematic_terms') = schematics;
- val schematics' = (schematic_types, schematic_terms @ schematic_terms');
+ val schematics' = (schematic_types, fold Vars.add schematic_terms schematic_terms');
in
({context = ctxt'', concl = concl', params = params, prems = prems,
schematics = schematics', asms = asms} : Subgoal.focus, goal'')
--- a/src/HOL/Import/import_rule.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Import/import_rule.ML Fri Sep 10 14:59:19 2021 +0200
@@ -162,7 +162,7 @@
val tvars = Term.add_tvars (Thm.prop_of thm) []
val tfrees = map (fn ((t, _), s) => TFree (t, s)) tvars
in
- Thm.instantiate ((tvars ~~ map (Thm.global_ctyp_of thy) tfrees), []) thm
+ Thm.instantiate (TVars.make (tvars ~~ map (Thm.global_ctyp_of thy) tfrees), Vars.empty) thm
end
fun def' constname rhs thy =
@@ -274,7 +274,7 @@
| NONE => (iS, Thm.global_ctyp_of thy (TFree bef))))
tys_before tys_after
in
- Thm.instantiate (tyinst,[]) th1
+ Thm.instantiate (TVars.make tyinst, Vars.empty) th1
end
fun inst sigma th =
@@ -338,7 +338,7 @@
val tns = map (fn (_, _) => "'") tvs
val nms = fst (fold_map Name.variant tns (Variable.names_of ctxt))
val vs = map TVar ((nms ~~ (map (snd o fst) tvs)) ~~ (map snd tvs))
- val thm' = Thm.instantiate ((tvs ~~ map (Thm.ctyp_of ctxt) vs), []) thm
+ val thm' = Thm.instantiate (TVars.make (tvs ~~ map (Thm.ctyp_of ctxt) vs), Vars.empty) thm
in
snd (Global_Theory.add_thm ((binding, thm'), []) thy)
end
--- a/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML Fri Sep 10 14:59:19 2021 +0200
@@ -476,7 +476,7 @@
fun real_not_eq_conv ct =
let
val (l,r) = dest_eq (Thm.dest_arg ct)
- val th = Thm.instantiate ([],[((("x", 0), \<^typ>\<open>real\<close>),l),((("y", 0), \<^typ>\<open>real\<close>),r)]) neq_th
+ val th = Thm.instantiate (TVars.empty, Vars.make [((("x", 0), \<^typ>\<open>real\<close>),l),((("y", 0), \<^typ>\<open>real\<close>),r)]) neq_th
val th_p = poly_conv(Thm.dest_arg(Thm.dest_arg1(Thm.rhs_of th)))
val th_x = Drule.arg_cong_rule \<^cterm>\<open>uminus :: real \<Rightarrow> _\<close> th_p
val th_n = fconv_rule (arg_conv poly_neg_conv) th_x
@@ -740,16 +740,16 @@
val elim_abs = eliminate_construct is_abs
(fn p => fn ax =>
- Thm.instantiate ([], [(p_v,p), (x_v, Thm.dest_arg ax)]) pth_abs)
+ Thm.instantiate (TVars.empty, Vars.make [(p_v,p), (x_v, Thm.dest_arg ax)]) pth_abs)
val elim_max = eliminate_construct is_max
(fn p => fn ax =>
let val (ax,y) = Thm.dest_comb ax
- in Thm.instantiate ([], [(p_v,p), (x_v, Thm.dest_arg ax), (y_v,y)])
+ in Thm.instantiate (TVars.empty, Vars.make [(p_v,p), (x_v, Thm.dest_arg ax), (y_v,y)])
pth_max end)
val elim_min = eliminate_construct is_min
(fn p => fn ax =>
let val (ax,y) = Thm.dest_comb ax
- in Thm.instantiate ([], [(p_v,p), (x_v, Thm.dest_arg ax), (y_v,y)])
+ in Thm.instantiate (TVars.empty, Vars.make [(p_v,p), (x_v, Thm.dest_arg ax), (y_v,y)])
pth_min end)
in first_conv [elim_abs, elim_max, elim_min, all_conv]
end;
--- a/src/HOL/Library/cconv.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Library/cconv.ML Fri Sep 10 14:59:19 2021 +0200
@@ -183,7 +183,8 @@
((if n = 1 then fun_cconv else I) o arg_cconv) (prems_cconv (n-1) cv) ct
| _ => cv ct)
-fun inst_imp_cong ct = Thm.instantiate ([], [((("A", 0), propT), ct)]) Drule.imp_cong
+fun inst_imp_cong ct =
+ Thm.instantiate (TVars.empty, Vars.make [((("A", 0), propT), ct)]) Drule.imp_cong
(*rewrite B in A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> B*)
fun concl_cconv 0 cv ct = cv ct
@@ -203,10 +204,12 @@
NONE => (As, B)
| SOME (A,B) => strip_prems (i - 1) (A::As) B
val (prem, (prems, concl)) = ct |> Thm.dest_implies ||> strip_prems n []
- val rewr_imp_concl = Thm.instantiate ([], [((("C", 0), propT), concl)]) @{thm rewr_imp}
+ val rewr_imp_concl =
+ Thm.instantiate (TVars.empty, Vars.make [((("C", 0), propT), concl)]) @{thm rewr_imp}
val th1 = cv prem RS rewr_imp_concl
val nprems = Thm.nprems_of th1
- fun inst_cut_rl ct = Thm.instantiate ([], [((("psi", 0), propT), ct)]) cut_rl
+ fun inst_cut_rl ct =
+ Thm.instantiate (TVars.empty, Vars.make [((("psi", 0), propT), ct)]) cut_rl
fun f p th = (th RS inst_cut_rl p)
|> Conv.fconv_rule (Conv.concl_conv nprems (Conv.rewr_conv @{thm imp_cong_eq}))
in fold f prems th1 end
--- a/src/HOL/Library/old_recdef.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Library/old_recdef.ML Fri Sep 10 14:59:19 2021 +0200
@@ -305,8 +305,8 @@
in
Conv.fconv_rule Drule.beta_eta_conversion
(case_thm
- |> Thm.instantiate (type_cinsts, [])
- |> Thm.instantiate ([], [(Pv, abs_ct), (Dv, free_ct)]))
+ |> Thm.instantiate (TVars.make type_cinsts, Vars.empty)
+ |> Thm.instantiate (TVars.empty, Vars.make [(Pv, abs_ct), (Dv, free_ct)]))
end;
@@ -1121,7 +1121,8 @@
val gspec = Thm.forall_intr (Thm.cterm_of \<^context> x) spec
in
fun SPEC tm thm =
- let val gspec' = Drule.instantiate_normalize ([(TV, Thm.ctyp_of_cterm tm)], []) gspec
+ let val gspec' =
+ Drule.instantiate_normalize (TVars.make [(TV, Thm.ctyp_of_cterm tm)], Vars.empty) gspec
in thm RS (Thm.forall_elim tm gspec') end
end;
@@ -1140,8 +1141,8 @@
let val ctm2 = Thm.cterm_of ctxt tm2
in ((i, Thm.typ_of_cterm ctm2), ctm2) end)
fun certify ctxt (ty_theta,tm_theta) =
- (cty_theta ctxt (Vartab.dest ty_theta),
- ctm_theta ctxt (Vartab.dest tm_theta))
+ (TVars.make (cty_theta ctxt (Vartab.dest ty_theta)),
+ Vars.make (ctm_theta ctxt (Vartab.dest tm_theta)))
in
fun GEN ctxt v th =
let val gth = Thm.forall_intr v th
--- a/src/HOL/Library/rewrite.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Library/rewrite.ML Fri Sep 10 14:59:19 2021 +0200
@@ -272,7 +272,7 @@
((s, norm_type env T), Thm.cterm_of ctxt (Envir.norm_term env (Var x))))
val tyinsts = Term.add_tvars prop []
|> map (fn x => (x, Thm.ctyp_of ctxt (norm_type env (TVar x))))
- in Drule.instantiate_normalize (tyinsts, insts) thm end
+ in Drule.instantiate_normalize (TVars.make tyinsts, Vars.make insts) thm end
fun unify_with_rhs context to env thm =
let
--- a/src/HOL/Matrix_LP/Compute_Oracle/linker.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/linker.ML Fri Sep 10 14:59:19 2021 +0200
@@ -326,7 +326,7 @@
let
val (newsubsts, instances) = Linker.add_instances thy instances monocs
val _ = if not (null newsubsts) then changed := true else ()
- val newths = map (fn subst => Thm.instantiate (conv_subst thy subst, []) th) newsubsts
+ val newths = map (fn subst => Thm.instantiate (TVars.make (conv_subst thy subst), Vars.empty) th) newsubsts
(* val _ = if not (null newths) then (print ("added new theorems: ", newths); ()) else ()*)
val newmonos = fold (fn th => fn monos => (snd (collect_consts_of_thm th))@monos) newths []
in
--- a/src/HOL/Nominal/nominal_datatype.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Fri Sep 10 14:59:19 2021 +0200
@@ -1397,8 +1397,8 @@
REPEAT (TRY (resolve_tac context [conjI] 1) THEN asm_full_simp_tac ind_ss5 1)]
end);
- val induct_aux' = Thm.instantiate ([],
- map (fn (s, Var (v as (_, T))) =>
+ val induct_aux' = Thm.instantiate (TVars.empty,
+ Vars.make (map (fn (s, Var (v as (_, T))) =>
(v, Thm.global_cterm_of thy9 (Free (s, T))))
(pnames ~~ map head_of (HOLogic.dest_conj
(HOLogic.dest_Trueprop (Thm.concl_of induct_aux)))) @
@@ -1406,7 +1406,7 @@
let val f' = Logic.varify_global f
in (dest_Var f',
Thm.global_cterm_of thy9 (Const (\<^const_name>\<open>Nominal.supp\<close>, fastype_of f')))
- end) fresh_fs) induct_aux;
+ end) fresh_fs)) induct_aux;
val induct = Goal.prove_global_future thy9 []
(map (augment_sort thy9 fs_cp_sort) ind_prems)
@@ -1571,8 +1571,8 @@
(augment_sort thy1 pt_cp_sort
(Logic.mk_implies (HOLogic.mk_Trueprop Q, HOLogic.mk_Trueprop P)))
(fn {context = ctxt, ...} =>
- dresolve_tac ctxt [Thm.instantiate ([],
- [((("pi", 0), permT),
+ dresolve_tac ctxt [Thm.instantiate (TVars.empty,
+ Vars.make [((("pi", 0), permT),
Thm.global_cterm_of thy11 (Const (\<^const_name>\<open>rev\<close>, permT --> permT) $ pi))]) th] 1 THEN
NominalPermeq.perm_simp_tac (put_simpset HOL_ss ctxt) 1)) (ps ~~ ths)
in (ths, ths') end) dt_atomTs);
@@ -1662,8 +1662,8 @@
resolve_tac ctxt [unique] 1,
SUBPROOF (fn {context = ctxt', prems = prems', params = [(_, a), (_, b)], ...} =>
EVERY [cut_facts_tac [rec_prem] 1,
- resolve_tac ctxt' [Thm.instantiate ([],
- [((("pi", 0), mk_permT aT),
+ resolve_tac ctxt' [Thm.instantiate (TVars.empty,
+ Vars.make [((("pi", 0), mk_permT aT),
Thm.cterm_of ctxt'
(perm_of_pair (Thm.term_of a, Thm.term_of b)))]) eqvt_th] 1,
asm_simp_tac (put_simpset HOL_ss ctxt' addsimps
@@ -1882,8 +1882,8 @@
val U as Type (_, [Type (_, [T, _])]) = fastype_of p;
val l = find_index (equal T) dt_atomTs;
val th = nth (nth rec_equiv_thms' l) k;
- val th' = Thm.instantiate ([],
- [((("pi", 0), U), Thm.global_cterm_of thy11 p)]) th;
+ val th' = Thm.instantiate (TVars.empty,
+ Vars.make [((("pi", 0), U), Thm.global_cterm_of thy11 p)]) th;
in resolve_tac ctxt [th'] 1 end;
val th' = Goal.prove context'' [] []
(HOLogic.mk_Trueprop (S $ mk_pi x $ mk_pi y))
--- a/src/HOL/Nominal/nominal_fresh_fun.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML Fri Sep 10 14:59:19 2021 +0200
@@ -33,8 +33,8 @@
fun res_inst_tac_term ctxt =
gen_res_inst_tac_term ctxt (fn instT => fn inst =>
Thm.instantiate
- (map (apfst dest_TVar) instT,
- map (apfst dest_Var) inst));
+ (TVars.make (map (apfst dest_TVar) instT),
+ Vars.make (map (apfst dest_Var) inst)));
fun res_inst_tac_term' ctxt =
gen_res_inst_tac_term ctxt
@@ -152,8 +152,8 @@
in case subtract (op =) vars vars' of
[Var v] =>
Seq.single
- (Thm.instantiate ([],
- [(v, Thm.cterm_of ctxt (fold_rev Term.abs params (Bound 0)))]) st)
+ (Thm.instantiate (TVars.empty,
+ Vars.make [(v, Thm.cterm_of ctxt (fold_rev Term.abs params (Bound 0)))]) st)
| _ => error "fresh_fun_simp: Too many variables, please report."
end
in
--- a/src/HOL/Nominal/nominal_inductive.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Fri Sep 10 14:59:19 2021 +0200
@@ -343,11 +343,11 @@
val pis'' = fold (concat_perm #> map) pis' pis;
val env = Pattern.first_order_match thy (ihypt, Thm.prop_of ihyp)
(Vartab.empty, Vartab.empty);
- val ihyp' = Thm.instantiate ([],
- map (fn (v, t) => (dest_Var v, Thm.global_cterm_of thy t))
+ val ihyp' = Thm.instantiate (TVars.empty,
+ Vars.make (map (fn (v, t) => (dest_Var v, Thm.global_cterm_of thy t))
(map (Envir.subst_term env) vs ~~
map (fold_rev (NominalDatatype.mk_perm [])
- (rev pis' @ pis)) params' @ [z])) ihyp;
+ (rev pis' @ pis)) params' @ [z]))) ihyp;
fun mk_pi th =
Simplifier.simplify (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}]
addsimprocs [NominalDatatype.perm_simproc])
--- a/src/HOL/Nominal/nominal_inductive2.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Fri Sep 10 14:59:19 2021 +0200
@@ -149,7 +149,9 @@
fun inst_params thy (vs, p) th cts =
let val env = Pattern.first_order_match thy (p, Thm.prop_of th)
(Vartab.empty, Vartab.empty)
- in Thm.instantiate ([], map (dest_Var o Envir.subst_term env) vs ~~ cts) th end;
+ in
+ Thm.instantiate (TVars.empty, Vars.make (map (dest_Var o Envir.subst_term env) vs ~~ cts)) th
+ end;
fun prove_strong_ind s alt_name avoids ctxt =
let
--- a/src/HOL/Real_Asymp/multiseries_expansion.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Real_Asymp/multiseries_expansion.ML Fri Sep 10 14:59:19 2021 +0200
@@ -219,10 +219,10 @@
case tvs of
[v] =>
let
- val thm' = Thm.instantiate ([(v, Thm.ctyp_of_cterm ct)], []) thm
+ val thm' = Thm.instantiate (TVars.make [(v, Thm.ctyp_of_cterm ct)], Vars.empty) thm
val vs = take (length cts) (rev (Term.add_vars (Thm.concl_of thm') []))
in
- Thm.instantiate ([], vs ~~ cts) thm'
+ Thm.instantiate (TVars.empty, Vars.make (vs ~~ cts)) thm'
end
| _ => raise THM ("get_parity", 0, [thm])
end
--- a/src/HOL/Statespace/distinct_tree_prover.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Statespace/distinct_tree_prover.ML Fri Sep 10 14:59:19 2021 +0200
@@ -97,8 +97,8 @@
val insts' = map (apfst mapT_and_recertify) insts;
in
Thm.instantiate
- (map (apfst (dest_TVar o Thm.typ_of)) instTs,
- map (apfst (dest_Var o Thm.term_of)) insts')
+ (TVars.make (map (apfst (dest_TVar o Thm.typ_of)) instTs),
+ Vars.make (map (apfst (dest_Var o Thm.term_of)) insts'))
end;
fun tvar_clash ixn S S' =
@@ -152,7 +152,7 @@
map (fn (v, (S, U)) => ((v, S), Thm.ctyp_of ctxt U)) tyinsts;
val insts' =
map (fn (idxn, ct) => ((idxn, Thm.typ_of_cterm ct), ct)) insts;
- val rule' = Thm.instantiate (tyinsts', insts') rule;
+ val rule' = Thm.instantiate (TVars.make tyinsts', Vars.make insts') rule;
in fold Thm.elim_implies prems rule' end;
local
@@ -299,8 +299,8 @@
val [alphaI] = #2 (dest_Type T);
in
Thm.instantiate
- ([(alpha, Thm.ctyp_of ctxt alphaI)],
- [((v, treeT alphaI), ct')]) @{thm subtract_Tip}
+ (TVars.make [(alpha, Thm.ctyp_of ctxt alphaI)],
+ Vars.make [((v, treeT alphaI), ct')]) @{thm subtract_Tip}
end
| subtractProver ctxt (Const (\<^const_name>\<open>Node\<close>, nT) $ l $ x $ d $ r) ct dist_thm =
let
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Fri Sep 10 14:59:19 2021 +0200
@@ -579,7 +579,7 @@
map (apfst (dest_Var o type_devar typeval_env)) term_pairing
|> map (apsnd (Thm.cterm_of ctxt))
in
- Thm.instantiate (typeval, termval) scheme_thm
+ Thm.instantiate (TVars.make typeval, Vars.make termval) scheme_thm
end
(*FIXME this is bad form?*)
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Fri Sep 10 14:59:19 2021 +0200
@@ -943,7 +943,7 @@
end
fun instantiate_tac from to =
- PRIMITIVE (Thm.instantiate ([], [(from, to)]))
+ PRIMITIVE (Thm.instantiate (TVars.empty, Vars.make [(from, to)]))
val tactic =
if is_none var_opt then no_tac
--- a/src/HOL/Tools/Argo/argo_real.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/Argo/argo_real.ML Fri Sep 10 14:59:19 2021 +0200
@@ -207,8 +207,10 @@
| var_of_add_cmp t = raise TERM ("var_of_add_cmp", [t])
fun add_cmp_conv ctxt n thm =
- let val v = var_of_add_cmp (Thm.prop_of thm)
- in Conv.rewr_conv (Thm.instantiate ([], [(v, Thm.cterm_of ctxt (mk_number n))]) thm) end
+ let val v = var_of_add_cmp (Thm.prop_of thm) in
+ Conv.rewr_conv
+ (Thm.instantiate (TVars.empty, Vars.make [(v, Thm.cterm_of ctxt (mk_number n))]) thm)
+ end
fun mul_cmp_conv ctxt n pos_thm neg_thm =
let val thm = if @0 < n then pos_thm else neg_thm
--- a/src/HOL/Tools/Argo/argo_tactic.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/Argo/argo_tactic.ML Fri Sep 10 14:59:19 2021 +0200
@@ -305,7 +305,8 @@
let val cprop = as_prop ct
in Thm.implies_intr cprop (f (Thm.assume cprop)) end
-fun instantiate cv ct = Thm.instantiate ([], [(Term.dest_Var (Thm.term_of cv), ct)])
+fun instantiate cv ct =
+ Thm.instantiate (TVars.empty, Vars.make [(Term.dest_Var (Thm.term_of cv), ct)])
(* proof replay for tautologies *)
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 10 14:59:19 2021 +0200
@@ -2060,7 +2060,7 @@
val unfolds = map2 mk_unfold rel_eqs rel_monos @ @{thms sup_fun_def sup_bool_def
imp_disjL all_conj_distrib subst_eq_imp simp_thms(18,21,35)};
in
- Thm.instantiate ([], insts) coind
+ Thm.instantiate (TVars.empty, Vars.make insts) coind
|> unfold_thms ctxt unfolds
end;
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Sep 10 14:59:19 2021 +0200
@@ -716,7 +716,7 @@
fun inst_thm t thm =
Thm.instantiate' [] [SOME (Thm.cterm_of lthy t)]
- (Thm.instantiate (rho_As, []) (Drule.zero_var_indexes thm));
+ (Thm.instantiate (TVars.make rho_As, Vars.empty) (Drule.zero_var_indexes thm));
val uexhaust_thm = inst_thm u exhaust_thm;
--- a/src/HOL/Tools/Function/partial_function.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML Fri Sep 10 14:59:19 2021 +0200
@@ -210,7 +210,7 @@
THEN Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 3
THEN CONVERSION (split_params_conv ctxt
then_conv (Conv.forall_conv (K split_paired_all_conv) ctxt)) 3)
- |> Thm.instantiate ([], [(P_var, P_inst), (x_var, x_inst)])
+ |> Thm.instantiate (TVars.empty, Vars.make [(P_var, P_inst), (x_var, x_inst)])
|> Simplifier.full_simplify (put_simpset split_conv_ss ctxt)
|> singleton (Variable.export ctxt' ctxt)
in
--- a/src/HOL/Tools/Function/relation.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/Function/relation.ML Fri Sep 10 14:59:19 2021 +0200
@@ -18,7 +18,8 @@
fun inst_state_tac ctxt inst =
SUBGOAL (fn (goal, _) =>
(case Term.add_vars goal [] of
- [v as (_, T)] => PRIMITIVE (Thm.instantiate ([], [(v, Thm.cterm_of ctxt (inst T))]))
+ [v as (_, T)] =>
+ PRIMITIVE (Thm.instantiate (TVars.empty, Vars.make [(v, Thm.cterm_of ctxt (inst T))]))
| _ => no_tac));
fun relation_tac ctxt rel i =
@@ -38,7 +39,7 @@
|> map_types Type_Infer.paramify_vars
|> Type.constraint T
|> Syntax.check_term ctxt;
- in PRIMITIVE (Thm.instantiate ([], [(v, Thm.cterm_of ctxt rel')])) end
+ in PRIMITIVE (Thm.instantiate (TVars.empty, Vars.make [(v, Thm.cterm_of ctxt rel')])) end
| _ => no_tac));
fun relation_infer_tac ctxt rel i =
--- a/src/HOL/Tools/Lifting/lifting_bnf.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/Lifting/lifting_bnf.ML Fri Sep 10 14:59:19 2021 +0200
@@ -24,7 +24,7 @@
val vars = get_lhs rel_Grp |> strip_comb |> snd |> map_filter (try (strip_comb #> snd #> hd))
val UNIVs = map (fn var => HOLogic.mk_UNIV (var |> dest_Var |> snd |> dest_Type |> snd |> hd)) vars
val inst = map dest_Var vars ~~ map (Thm.cterm_of ctxt) UNIVs
- val rel_Grp_UNIV_sym = rel_Grp |> Drule.instantiate_normalize ([], inst)
+ val rel_Grp_UNIV_sym = rel_Grp |> Drule.instantiate_normalize (TVars.empty, Vars.make inst)
|> Local_Defs.unfold0 ctxt @{thms subset_UNIV[THEN eqTrueI] UNIV_def[symmetric] simp_thms(21)}
|> (fn thm => thm RS sym)
val rel_mono = rel_mono_of_bnf bnf
--- a/src/HOL/Tools/Lifting/lifting_def.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Fri Sep 10 14:59:19 2021 +0200
@@ -119,7 +119,7 @@
val instT =
Vartab.fold (fn (a, (S, T)) => cons ((a, S), Thm.ctyp_of ctxt T))
(mk_inst_of_lift_def qty lift_def) []
- val phi = Morphism.instantiate_morphism (instT, [])
+ val phi = Morphism.instantiate_morphism (TVars.make instT, Vars.empty)
in morph_lift_def phi lift_def end
--- a/src/HOL/Tools/Lifting/lifting_term.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/Lifting/lifting_term.ML Fri Sep 10 14:59:19 2021 +0200
@@ -285,7 +285,7 @@
val match_env = Sign.typ_match (Proof_Context.theory_of ctxt) (qty_schematic, qty) Vartab.empty
fun prep_ty (x, (S, ty)) = ((x, S), Thm.ctyp_of ctxt ty)
val ty_inst = Vartab.fold (cons o prep_ty) match_env []
- in Thm.instantiate (ty_inst, []) quot_thm end
+ in Thm.instantiate (TVars.make ty_inst, Vars.empty) quot_thm end
fun check_rty_type ctxt rty quot_thm =
let
--- a/src/HOL/Tools/Meson/meson.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/Meson/meson.ML Fri Sep 10 14:59:19 2021 +0200
@@ -358,7 +358,8 @@
val ([x], ctxt') =
Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (Thm.concl_of th))] ctxt;
val spec' = spec
- |> Thm.instantiate ([], [(spec_var, Thm.cterm_of ctxt' (Free (x, snd spec_var)))]);
+ |> Thm.instantiate
+ (TVars.empty, Vars.make [(spec_var, Thm.cterm_of ctxt' (Free (x, snd spec_var)))]);
in (th RS spec', ctxt') end
end;
--- a/src/HOL/Tools/Meson/meson_clausify.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Fri Sep 10 14:59:19 2021 +0200
@@ -42,9 +42,9 @@
fun transform_elim_theorem th =
(case Thm.concl_of th of (*conclusion variable*)
\<^const>\<open>Trueprop\<close> $ (Var (v as (_, \<^typ>\<open>bool\<close>))) =>
- Thm.instantiate ([], [(v, cfalse)]) th
+ Thm.instantiate (TVars.empty, Vars.make [(v, cfalse)]) th
| Var (v as (_, \<^typ>\<open>prop\<close>)) =>
- Thm.instantiate ([], [(v, ctp_false)]) th
+ Thm.instantiate (TVars.empty, Vars.make [(v, ctp_false)]) th
| _ => th)
@@ -370,7 +370,8 @@
th ctxt1
val (cnf_ths, ctxt2) = clausify nnf_th
fun intr_imp ct th =
- Thm.instantiate ([], [((("i", 0), \<^typ>\<open>nat\<close>), Thm.cterm_of ctxt2 (HOLogic.mk_nat ax_no))])
+ Thm.instantiate (TVars.empty,
+ Vars.make [((("i", 0), \<^typ>\<open>nat\<close>), Thm.cterm_of ctxt2 (HOLogic.mk_nat ax_no))])
(zero_var_indexes @{thm skolem_COMBK_D})
RS Thm.implies_intr ct th
in
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Sep 10 14:59:19 2021 +0200
@@ -103,7 +103,7 @@
fun inst_excluded_middle i_atom =
@{lemma "P \<Longrightarrow> \<not> P \<Longrightarrow> False" by (rule notE)}
- |> instantiate_normalize ([], [((("P", 0), \<^typ>\<open>bool\<close>), i_atom)])
+ |> instantiate_normalize (TVars.empty, Vars.make [((("P", 0), \<^typ>\<open>bool\<close>), i_atom)])
fun assume_inference ctxt type_enc concealed sym_tab atom =
singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) (Metis_Term.Fn atom)
@@ -174,7 +174,7 @@
val tvs = Term.add_tvars (Thm.full_prop_of th) []
fun inc_tvar ((a, i), s) = (((a, i), s), Thm.ctyp_of ctxt (TVar ((a, i + inc), s)))
in
- Thm.instantiate (map inc_tvar tvs, []) th
+ Thm.instantiate (TVars.make (map inc_tvar tvs), Vars.empty) th
end
(*Like RSN, but we rename apart only the type variables. Vars here typically
@@ -217,7 +217,7 @@
again. We could do this the first time around but this error occurs seldom and we don't
want to break existing proofs in subtle ways or slow them down.*)
if null ps then raise TERM z
- else res (apply2 (Drule.instantiate_normalize (ps, [])) (th1', th2))
+ else res (apply2 (Drule.instantiate_normalize (TVars.make ps, Vars.empty)) (th1', th2))
end
end
@@ -407,7 +407,7 @@
val instsT = Vartab.fold (cons o mkT) tyenv []
val insts = Vartab.fold (cons o mk) tenv []
in
- Thm.instantiate (instsT, insts) th
+ Thm.instantiate (TVars.make instsT, Vars.make insts) th
end
handle THM _ => th)
@@ -574,7 +574,8 @@
tyenv []
val t_inst = [apply2 (Thm.cterm_of ctxt o Envir.norm_term env) (Var var, t')]
in
- Drule.instantiate_normalize (ty_inst, map (apfst (dest_Var o Thm.term_of)) t_inst) th
+ Drule.instantiate_normalize
+ (TVars.make ty_inst, Vars.make (map (apfst (dest_Var o Thm.term_of)) t_inst)) th
end
| _ => raise Fail "expected a single non-zapped, non-Metis Var")
in
--- a/src/HOL/Tools/Predicate_Compile/core_data.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Fri Sep 10 14:59:19 2021 +0200
@@ -240,10 +240,11 @@
map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop)
(take nargs (Thm.prems_of case_th))
val case_th' =
- Thm.instantiate ([], inst_of_matches pats) case_th
+ Thm.instantiate (TVars.empty, Vars.make (inst_of_matches pats)) case_th
OF replicate nargs @{thm refl}
val thesis =
- Thm.instantiate ([], inst_of_matches (Thm.prems_of case_th' ~~ map Thm.prop_of prems2))
+ Thm.instantiate (TVars.empty,
+ Vars.make (inst_of_matches (Thm.prems_of case_th' ~~ map Thm.prop_of prems2)))
case_th' OF prems2
in resolve_tac ctxt2 [thesis] 1 end
in
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Sep 10 14:59:19 2021 +0200
@@ -871,7 +871,7 @@
fun rewrite_pat (ct1, ct2) =
(ct1, Thm.cterm_of ctxt3 (Pattern.rewrite_term thy pats' [] (Thm.term_of ct2)))
val t_insts' = map rewrite_pat (Vars.dest t_insts)
- val intro'' = Thm.instantiate (TVars.dest T_insts, t_insts') intro
+ val intro'' = Thm.instantiate (T_insts, Vars.make t_insts') intro
val [intro'''] = Variable.export ctxt3 ctxt [intro'']
val intro'''' =
Simplifier.full_simplify
@@ -941,9 +941,9 @@
val f' = absdummy (U --> T') (Bound 0 $ y)
val th' =
Thm.instantiate
- ([(dest_TVar uninst_T, Thm.ctyp_of ctxt' (U --> T')),
+ (TVars.make [(dest_TVar uninst_T, Thm.ctyp_of ctxt' (U --> T')),
(dest_TVar uninst_T', Thm.ctyp_of ctxt' T')],
- [((fst (dest_Var f), (U --> T') --> T'), Thm.cterm_of ctxt' f')]) th
+ Vars.make [((fst (dest_Var f), (U --> T') --> T'), Thm.cterm_of ctxt' f')]) th
val [th'] = Variable.export (Variable.declare_thm th' ctxt') ctxt [th']
in
th'
@@ -1083,13 +1083,16 @@
val instT =
TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt' T))
(subst_of (pred', pred)) [];
- in Thm.instantiate (instT, []) th end
+ in Thm.instantiate (TVars.make instT, Vars.empty) th end
fun instantiate_ho_args th =
let
val (_, args') =
(strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o Thm.prop_of) th
val ho_args' = map dest_Var (ho_args_of_typ T args')
- in Thm.instantiate ([], ho_args' ~~ map (Thm.cterm_of ctxt') ho_args) th end
+ in
+ Thm.instantiate (TVars.empty, Vars.make (ho_args' ~~ map (Thm.cterm_of ctxt') ho_args))
+ th
+ end
val outp_pred =
Term_Subst.instantiate (subst_of (inp_pred, pred), Vars.empty) inp_pred
val ((_, ths'), ctxt1) =
--- a/src/HOL/Tools/Qelim/cooper.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Fri Sep 10 14:59:19 2021 +0200
@@ -160,10 +160,13 @@
[(th_1,th_2,th_3), (th_1',th_2',th_3')] =
let
val (mp', mq') = (get_pmi th_1, get_pmi th_1')
- val mi_th = FWD (Drule.instantiate_normalize ([],[(p_v,p),(q_v,q), (p_v',mp'),(q_v',mq')]) th1)
- [th_1, th_1']
- val infD_th = FWD (Drule.instantiate_normalize ([],[(p_v,mp'), (q_v, mq')]) th3) [th_3,th_3']
- val set_th = FWD (Drule.instantiate_normalize ([],[(p_v,p), (q_v,q)]) th2) [th_2, th_2']
+ val mi_th =
+ FWD (Drule.instantiate_normalize
+ (TVars.empty, Vars.make [(p_v,p),(q_v,q), (p_v',mp'),(q_v',mq')]) th1) [th_1, th_1']
+ val infD_th =
+ FWD (Drule.instantiate_normalize (TVars.empty, Vars.make [(p_v,mp'), (q_v, mq')]) th3) [th_3,th_3']
+ val set_th =
+ FWD (Drule.instantiate_normalize (TVars.empty, Vars.make [(p_v,p), (q_v,q)]) th2) [th_2, th_2']
in (mi_th, set_th, infD_th)
end;
@@ -504,16 +507,18 @@
if length (distinct (op aconv) bl) <= length (distinct (op aconv) al)
then
(bl,b0,decomp_minf,
- fn B => (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(B_v,B), (D_v,cd)]) th) dp)
+ fn B => (map (fn th =>
+ Thm.implies_elim (Thm.instantiate (TVars.empty, Vars.make [(B_v,B), (D_v,cd)]) th) dp)
[bseteq,bsetneq,bsetlt, bsetle, bsetgt,bsetge])@
- (map (Thm.instantiate ([],[(B_v,B), (D_v,cd)]))
+ (map (Thm.instantiate (TVars.empty, Vars.make [(B_v,B), (D_v,cd)]))
[bsetdvd,bsetndvd,bsetP,infDdvd, infDndvd,bsetconj,
bsetdisj,infDconj, infDdisj]),
cpmi)
else (al,a0,decomp_pinf,fn A =>
- (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(A_v,A), (D_v,cd)]) th) dp)
+ (map (fn th =>
+ Thm.implies_elim (Thm.instantiate (TVars.empty, Vars.make [(A_v,A), (D_v,cd)]) th) dp)
[aseteq,asetneq,asetlt, asetle, asetgt,asetge])@
- (map (Thm.instantiate ([],[(A_v,A), (D_v,cd)]))
+ (map (Thm.instantiate (TVars.empty, Vars.make [(A_v,A), (D_v,cd)]))
[asetdvd,asetndvd, asetP, infDdvd, infDndvd,asetconj,
asetdisj,infDconj, infDdisj]),cppi)
val cpth =
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Fri Sep 10 14:59:19 2021 +0200
@@ -92,7 +92,7 @@
(HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
val Type (_, [_, iT]) = T;
val icT = Thm.ctyp_of lthy iT;
- val inst = Thm.instantiate_cterm ([(a_v, icT)], []);
+ val inst = Thm.instantiate_cterm (TVars.make [(a_v, icT)], Vars.empty);
fun subst_v t' = map_aterms (fn t as Free (w, _) => if v = w then t' else t | t => t);
val t_rhs = lambda t_k proto_t_rhs;
val eqs0 = [subst_v \<^term>\<open>0::natural\<close> eq,
@@ -105,8 +105,8 @@
val cT_rhs = inst pt_rhs |> Thm.term_of |> dest_Var;
val rule = @{thm random_aux_rec}
|> Drule.instantiate_normalize
- ([(a_v, icT)],
- [(cT_random_aux, Thm.cterm_of lthy' t_random_aux),
+ (TVars.make [(a_v, icT)],
+ Vars.make [(cT_random_aux, Thm.cterm_of lthy' t_random_aux),
(cT_rhs, Thm.cterm_of lthy' t_rhs)]);
fun tac ctxt =
ALLGOALS (resolve_tac ctxt [rule])
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Fri Sep 10 14:59:19 2021 +0200
@@ -81,7 +81,7 @@
fun prep_ty (x, (S, ty)) = ((x, S), Thm.global_ctyp_of thy ty)
fun prep_trm (x, (T, t)) = ((x, T), Thm.global_cterm_of thy t)
in
- (map prep_ty tyenv, map prep_trm tenv)
+ (TVars.make (map prep_ty tyenv), Vars.make (map prep_trm tenv))
end
(* Calculates the instantiations for the lemmas:
@@ -476,7 +476,8 @@
then make_inst_id (Thm.term_of (Thm.lhs_of thm3)) (Thm.term_of ctrm)
else make_inst (Thm.term_of (Thm.lhs_of thm3)) (Thm.term_of ctrm)
val thm4 =
- Drule.instantiate_normalize ([], [(dest_Var insp, Thm.cterm_of ctxt inst)]) thm3
+ Drule.instantiate_normalize
+ (TVars.empty, Vars.make [(dest_Var insp, Thm.cterm_of ctxt inst)]) thm3
in
Conv.rewr_conv thm4 ctrm
end
--- a/src/HOL/Tools/SMT/smt_normalize.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Fri Sep 10 14:59:19 2021 +0200
@@ -35,7 +35,7 @@
fun inst f ct thm =
let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
- in Thm.instantiate ([], [(dest_Var (Thm.term_of cv), ct)]) thm end
+ in Thm.instantiate (TVars.empty, Vars.make [(dest_Var (Thm.term_of cv), ct)]) thm end
in
fun instantiate_elim thm =
@@ -203,7 +203,7 @@
let
val (ctr, cp) = Thm.dest_binop (Thm.rhs_of trigger_eq) ||> rpair ct
val inst = map (apfst (dest_Var o Thm.term_of)) [cp, (ctr, mk_trigger ctss)]
- in Thm.instantiate ([], inst) trigger_eq end
+ in Thm.instantiate (TVars.empty, Vars.make inst) trigger_eq end
fun infer_trigger_eq_conv outer_ctxt (ctxt, cvs) ct =
let
@@ -402,7 +402,7 @@
let val (q, cts) = fold (add_apps add_int_of_nat [] o Thm.cprop_of) thms (false, [])
in
if q then (thms, nat_int_thms)
- else (thms, map (fn ct => Thm.instantiate ([], [(var, ct)]) int_thm) cts)
+ else (thms, map (fn ct => Thm.instantiate (TVars.empty, Vars.make [(var, ct)]) int_thm) cts)
end
val setup_nat_as_int =
--- a/src/HOL/Tools/SMT/smt_replay.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_replay.ML Fri Sep 10 14:59:19 2021 +0200
@@ -96,7 +96,8 @@
fun compose (cvs, f, rule) thm =
discharge thm
- (Thm.instantiate ([], map (dest_Var o Thm.term_of) cvs ~~ f (Thm.cprop_of thm)) rule)
+ (Thm.instantiate
+ (TVars.empty, Vars.make (map (dest_Var o Thm.term_of) cvs ~~ f (Thm.cprop_of thm))) rule)
(* simpset *)
--- a/src/HOL/Tools/SMT/smt_replay_methods.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_replay_methods.ML Fri Sep 10 14:59:19 2021 +0200
@@ -157,12 +157,12 @@
fun match_instantiateT ctxt t thm =
if Term.exists_type (Term.exists_subtype Term.is_TVar) (dest_thm thm) then
- Thm.instantiate (gen_certify_inst fst (Thm.ctyp_of ctxt) ctxt thm t, []) thm
+ Thm.instantiate (TVars.make (gen_certify_inst fst (Thm.ctyp_of ctxt) ctxt thm t), Vars.empty) thm
else thm
fun match_instantiate ctxt t thm =
let val thm' = match_instantiateT ctxt t thm in
- Thm.instantiate ([], gen_certify_inst snd (Thm.cterm_of ctxt) ctxt thm' t) thm'
+ Thm.instantiate (TVars.empty, Vars.make (gen_certify_inst snd (Thm.cterm_of ctxt) ctxt thm' t)) thm'
end
fun discharge _ [] thm = thm
--- a/src/HOL/Tools/SMT/smt_util.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_util.ML Fri Sep 10 14:59:19 2021 +0200
@@ -173,7 +173,8 @@
let val cpat = Thm.global_cterm_of thy (Const (name, Sign.the_const_type thy name))
in (destT (Thm.ctyp_of_cterm cpat), cpat) end
-fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (map (dest_TVar o Thm.typ_of) cTs ~~ cUs, []) ct
+fun instTs cUs (cTs, ct) =
+ Thm.instantiate_cterm (TVars.make (map (dest_TVar o Thm.typ_of) cTs ~~ cUs), Vars.empty) ct
fun instT cU (cT, ct) = instTs [cU] ([cT], ct)
fun instT' ct = instT (Thm.ctyp_of_cterm ct)
--- a/src/HOL/Tools/Transfer/transfer.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML Fri Sep 10 14:59:19 2021 +0200
@@ -576,7 +576,7 @@
in
thm
|> Thm.generalize (Names.make_set tfrees, Names.make_set (rnames @ frees)) idx
- |> Thm.instantiate (map tinst binsts, map inst binsts)
+ |> Thm.instantiate (TVars.make (map tinst binsts), Vars.make (map inst binsts))
end
fun transfer_rule_of_lhs ctxt t =
@@ -597,7 +597,7 @@
in
thm
|> Thm.generalize (Names.make_set tfrees, Names.make_set (rnames @ frees)) idx
- |> Thm.instantiate (map tinst binsts, map inst binsts)
+ |> Thm.instantiate (TVars.make (map tinst binsts), Vars.make (map inst binsts))
end
fun eq_rules_tac ctxt eq_rules =
@@ -701,7 +701,7 @@
rev (Term.add_tvars (Thm.full_prop_of thm1) [])
|> map (fn v as ((a, _), S) => (v, Thm.ctyp_of ctxt (TFree (a, S))))
val thm2 = thm1
- |> Thm.instantiate (instT, [])
+ |> Thm.instantiate (TVars.make instT, Vars.empty)
|> Raw_Simplifier.rewrite_rule ctxt pre_simps
val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
val rule = transfer_rule_of_lhs ctxt' (HOLogic.dest_Trueprop (Thm.concl_of thm2))
@@ -736,7 +736,7 @@
rev (Term.add_tvars (Thm.full_prop_of thm1) [])
|> map (fn v as ((a, _), S) => (v, Thm.ctyp_of ctxt (TFree (a, S))))
val thm2 = thm1
- |> Thm.instantiate (instT, [])
+ |> Thm.instantiate (TVars.make instT, Vars.empty)
|> Raw_Simplifier.rewrite_rule ctxt pre_simps
val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
--- a/src/HOL/Tools/coinduction.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/coinduction.ML Fri Sep 10 14:59:19 2021 +0200
@@ -69,8 +69,8 @@
|> fold Variable.declare_thm (raw_thm :: prems);
val thm_concl = Thm.cprop_of raw_thm |> strip_imp_concl;
val (instT, inst) = Thm.match (thm_concl, concl);
- val rhoTs = map (fn (v, T) => (TVar v, Thm.typ_of T)) instT;
- val rhots = map (fn (v, t) => (Var v, Thm.term_of t)) inst;
+ val rhoTs = map (fn (v, T) => (TVar v, Thm.typ_of T)) (TVars.dest instT);
+ val rhots = map (fn (v, t) => (Var v, Thm.term_of t)) (Vars.dest inst);
val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd
|> map (subst_atomic_types rhoTs);
val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs;
--- a/src/HOL/Tools/hologic.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/hologic.ML Fri Sep 10 14:59:19 2021 +0200
@@ -205,16 +205,16 @@
let
val (P, Q) = apply2 (Object_Logic.dest_judgment ctxt o Thm.cprop_of) (thP, thQ)
handle CTERM (msg, _) => raise THM (msg, 0, [thP, thQ]);
- val inst = Thm.instantiate ([], [((("P", 0), boolT), P), ((("Q", 0), boolT), Q)]);
- in Drule.implies_elim_list (inst @{thm conjI}) [thP, thQ] end;
+ val inst = (TVars.empty, Vars.make [((("P", 0), boolT), P), ((("Q", 0), boolT), Q)]);
+ in Drule.implies_elim_list (Thm.instantiate inst @{thm conjI}) [thP, thQ] end;
fun conj_elim ctxt thPQ =
let
val (P, Q) = Thm.dest_binop (Object_Logic.dest_judgment ctxt (Thm.cprop_of thPQ))
handle CTERM (msg, _) => raise THM (msg, 0, [thPQ]);
- val inst = Thm.instantiate ([], [((("P", 0), boolT), P), ((("Q", 0), boolT), Q)]);
- val thP = Thm.implies_elim (inst @{thm conjunct1}) thPQ;
- val thQ = Thm.implies_elim (inst @{thm conjunct2}) thPQ;
+ val inst = (TVars.empty, Vars.make [((("P", 0), boolT), P), ((("Q", 0), boolT), Q)]);
+ val thP = Thm.implies_elim (Thm.instantiate inst @{thm conjunct1}) thPQ;
+ val thQ = Thm.implies_elim (Thm.instantiate inst @{thm conjunct2}) thPQ;
in (thP, thQ) end;
fun conj_elims ctxt th =
--- a/src/HOL/Tools/inductive_set.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/inductive_set.ML Fri Sep 10 14:59:19 2021 +0200
@@ -221,7 +221,7 @@
fun mk_to_pred_eq ctxt p fs optfs' T thm =
let
val insts = mk_to_pred_inst ctxt fs;
- val thm' = Thm.instantiate ([], insts) thm;
+ val thm' = Thm.instantiate (TVars.empty, Vars.make insts) thm;
val thm'' =
(case optfs' of
NONE => thm' RS sym
@@ -345,7 +345,7 @@
val insts = mk_to_pred_inst ctxt fs
in
thm |>
- Thm.instantiate ([], insts) |>
+ Thm.instantiate (TVars.empty, Vars.make insts) |>
Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimprocs
[to_pred_simproc
(@{thm mem_Collect_eq} :: @{thm case_prod_conv} :: map (Thm.transfer thy) to_pred_simps)]) |>
@@ -383,7 +383,7 @@
end) fs;
in
thm |>
- Thm.instantiate ([], insts) |>
+ Thm.instantiate (TVars.empty, Vars.make insts) |>
Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps to_set_simps
addsimprocs [strong_ind_simproc pred_arities, \<^simproc>\<open>Collect_mem\<close>]) |>
Rule_Cases.save thm
--- a/src/HOL/Tools/lin_arith.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/lin_arith.ML Fri Sep 10 14:59:19 2021 +0200
@@ -60,8 +60,9 @@
fun is_nat t = (fastype_of1 t = HOLogic.natT);
fun mk_nat_thm thy t =
- let val ct = Thm.global_cterm_of thy t
- in Drule.instantiate_normalize ([], [((("n", 0), HOLogic.natT), ct)]) @{thm le0} end;
+ let val ct = Thm.global_cterm_of thy t in
+ Drule.instantiate_normalize (TVars.empty, Vars.make [((("n", 0), HOLogic.natT), ct)]) @{thm le0}
+ end;
end;
--- a/src/HOL/Tools/monomorph.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/monomorph.ML Fri Sep 10 14:59:19 2021 +0200
@@ -165,7 +165,7 @@
let
fun cert (ix, (S, T)) = ((ix, S), Thm.ctyp_of ctxt T)
fun cert' subst = Vartab.fold (cons o cert) subst []
- in Thm.instantiate (cert' subst, []) end
+ in Thm.instantiate (TVars.make (cert' subst), Vars.empty) end
fun add_new_grounds used_grounds new_grounds thm =
let
--- a/src/HOL/Tools/numeral.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/numeral.ML Fri Sep 10 14:59:19 2021 +0200
@@ -64,7 +64,7 @@
val uminus_tvar = tvar \<^sort>\<open>uminus\<close>;
val uminus = cterm_of (Const (\<^const_name>\<open>uminus\<close>, TVar uminus_tvar --> TVar uminus_tvar));
-fun instT T v = Thm.instantiate_cterm ([(v, T)], []);
+fun instT T v = Thm.instantiate_cterm (TVars.make [(v, T)], Vars.empty);
in
--- a/src/HOL/Tools/numeral_simprocs.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML Fri Sep 10 14:59:19 2021 +0200
@@ -594,8 +594,8 @@
fun prove_nz ctxt T t =
let
- val z = Thm.instantiate_cterm ([(zero_tvar, T)], []) zero
- val eq = Thm.instantiate_cterm ([(type_tvar, T)], []) geq
+ val z = Thm.instantiate_cterm (TVars.make [(zero_tvar, T)], Vars.empty) zero
+ val eq = Thm.instantiate_cterm (TVars.make [(type_tvar, T)], Vars.empty) geq
val th =
Simplifier.rewrite (ctxt addsimps @{thms simp_thms})
(Thm.apply \<^cterm>\<open>Trueprop\<close> (Thm.apply \<^cterm>\<open>Not\<close>
--- a/src/HOL/Tools/record.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/record.ML Fri Sep 10 14:59:19 2021 +0200
@@ -1771,7 +1771,8 @@
fun mk_eq_refl ctxt =
@{thm equal_refl}
|> Thm.instantiate
- ([((("'a", 0), \<^sort>\<open>equal\<close>), Thm.ctyp_of ctxt (Logic.varifyT_global extT))], [])
+ (TVars.make [((("'a", 0), \<^sort>\<open>equal\<close>), Thm.ctyp_of ctxt (Logic.varifyT_global extT))],
+ Vars.empty)
|> Axclass.unoverload ctxt;
val ensure_random_record = ensure_sort_record (\<^sort>\<open>random\<close>, mk_random_eq);
val ensure_exhaustive_record =
--- a/src/HOL/Tools/reification.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/reification.ML Fri Sep 10 14:59:19 2021 +0200
@@ -176,7 +176,7 @@
(Vartab.dest tyenv);
in
((map (Thm.cterm_of ctxt) fts ~~ replicate (length fts) ctxt,
- apfst (FWD (Drule.instantiate_normalize (ctyenv, its) cong))), bds)
+ apfst (FWD (Drule.instantiate_normalize (TVars.make ctyenv, Vars.make its) cong))), bds)
end handle Pattern.MATCH => decomp_reify da congs (ct, ctxt) bds))
end;
@@ -229,10 +229,11 @@
(map (fn n => (n, 0)) xns) tml);
val substt =
let
- val ih = Drule.cterm_rule (Thm.instantiate (subst_ty, []));
+ val ih = Drule.cterm_rule (Thm.instantiate (TVars.make subst_ty, Vars.empty));
in map (apply2 ih) (subst_ns @ subst_vs @ cts) end;
val th =
- (Drule.instantiate_normalize (subst_ty, map (apfst (dest_Var o Thm.term_of)) substt) eq)
+ (Drule.instantiate_normalize
+ (TVars.make subst_ty, Vars.make (map (apfst (dest_Var o Thm.term_of)) substt)) eq)
RS sym;
in (hd (Variable.export ctxt'' ctxt [th]), bds) end)
handle Pattern.MATCH => tryeqs eqs (ct, ctxt) bds);
@@ -270,7 +271,7 @@
val (_, _ :: vs) = eq |> Thm.prop_of |> HOLogic.dest_Trueprop
|> HOLogic.dest_eq |> fst |> strip_comb;
val subst = map_filter (fn Var v => SOME (v, subst (#2 v)) | _ => NONE) vs;
- in Thm.instantiate ([], subst) eq end;
+ in Thm.instantiate (TVars.empty, Vars.make subst) eq end;
val (ps, congs) = map_split (mk_congeq ctxt' fs o prep_eq) eqs;
val bds = AList.make (K ([], [])) tys;
in (ps ~~ Variable.export ctxt' ctxt congs, bds) end
@@ -288,7 +289,7 @@
val vs = map (fn Var (v as (_, T)) =>
(v, the (AList.lookup Type.could_unify bds' T) |> snd |> HOLogic.mk_list (dest_listT T))) vars;
val th' =
- Drule.instantiate_normalize ([], map (apsnd (Thm.cterm_of ctxt)) vs) th;
+ Drule.instantiate_normalize (TVars.empty, Vars.make (map (apsnd (Thm.cterm_of ctxt)) vs)) th;
val th'' = Thm.symmetric (dereify ctxt [] (Thm.lhs_of th'));
in Thm.transitive th'' th' end;
--- a/src/HOL/Tools/sat.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/sat.ML Fri Sep 10 14:59:19 2021 +0200
@@ -171,7 +171,8 @@
val cLit =
snd (Thm.dest_comb (if hyp1_is_neg then hyp2 else hyp1)) (* strip Trueprop *)
in
- Thm.instantiate ([], [((("P", 0), HOLogic.boolT), cLit)]) resolution_thm
+ Thm.instantiate (TVars.empty, Vars.make [((("P", 0), HOLogic.boolT), cLit)])
+ resolution_thm
end
val _ =
--- a/src/HOL/Tools/semiring_normalizer.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/semiring_normalizer.ML Fri Sep 10 14:59:19 2021 +0200
@@ -81,7 +81,7 @@
let
fun h instT =
let
- val substT = Thm.instantiate (instT, []);
+ val substT = Thm.instantiate (instT, Vars.empty);
val substT_cterm = Drule.cterm_rule substT;
val vars' = map substT_cterm vars;
@@ -144,8 +144,9 @@
let val (a, b) = Rat.dest x
in if b = 1 then Numeral.mk_cnumber cT a
else Thm.apply
- (Thm.apply (Thm.instantiate_cterm ([(divide_tvar, cT)], []) divide_const)
- (Numeral.mk_cnumber cT a))
+ (Thm.apply
+ (Thm.instantiate_cterm (TVars.make [(divide_tvar, cT)], Vars.empty) divide_const)
+ (Numeral.mk_cnumber cT a))
(Numeral.mk_cnumber cT b)
end
in
@@ -249,7 +250,8 @@
if is_binop ct ct' then Thm.dest_binop ct'
else raise CTERM ("dest_binop: bad binop", [ct, ct'])
-fun inst_thm inst = Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) inst);
+fun inst_thm inst =
+ Thm.instantiate (TVars.empty, Vars.make (map (apfst (dest_Var o Thm.term_of)) inst));
val dest_number = Thm.term_of #> HOLogic.dest_number #> snd;
val is_number = can dest_number;
--- a/src/HOL/Tools/split_rule.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Tools/split_rule.ML Fri Sep 10 14:59:19 2021 +0200
@@ -42,7 +42,7 @@
fun split_rule_var' ctxt (t as Var (v, Type ("fun", [T1, T2]))) rl =
let val T' = HOLogic.flatten_tupleT T1 ---> T2;
val newt = ap_split T1 T2 (Var (v, T'));
- in Thm.instantiate ([], [(dest_Var t, Thm.cterm_of ctxt newt)]) rl end
+ in Thm.instantiate (TVars.empty, Vars.make [(dest_Var t, Thm.cterm_of ctxt newt)]) rl end
| split_rule_var' _ _ rl = rl;
@@ -73,7 +73,8 @@
val newt = ap_split' Us U (Var (v, T'));
val (vs', insts) = fold mk_tuple ts (vs, []);
in
- (Drule.instantiate_normalize ([], ((v, T), Thm.cterm_of ctxt newt) :: insts) rl, vs')
+ (Drule.instantiate_normalize
+ (TVars.empty, Vars.make (((v, T), Thm.cterm_of ctxt newt) :: insts)) rl, vs')
end
| complete_split_rule_var _ _ x = x;
--- a/src/HOL/Types_To_Sets/unoverload_type.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/HOL/Types_To_Sets/unoverload_type.ML Fri Sep 10 14:59:19 2021 +0200
@@ -40,7 +40,7 @@
val tyenv_list = tyenv |> Vartab.dest
|> map (fn (x, (s, TVar (x', _))) =>
((x, s), Thm.ctyp_of (Context.proof_of context) (TVar(x', s))))
- val thm'' = Drule.instantiate_normalize (tyenv_list, []) thm'
+ val thm'' = Drule.instantiate_normalize (TVars.make tyenv_list, Vars.empty) thm'
val varify_const =
apsnd (subst_TFree "'a" (TVar (tvar, @{sort type}))) #> Const #> Thm.global_cterm_of thy
val consts = params_of_sort thy sort
--- a/src/Provers/Arith/fast_lin_arith.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Fri Sep 10 14:59:19 2021 +0200
@@ -438,7 +438,7 @@
val T = Thm.typ_of_cterm cv
in
mth
- |> Thm.instantiate ([], [(dest_Var (Thm.term_of cv), number_of T n)])
+ |> Thm.instantiate (TVars.empty, Vars.make [(dest_Var (Thm.term_of cv), number_of T n)])
|> rewrite_concl
|> discharge_prem
handle CTERM _ => mult_by_add n thm
--- a/src/Provers/hypsubst.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Provers/hypsubst.ML Fri Sep 10 14:59:19 2021 +0200
@@ -179,10 +179,10 @@
val (instT, _) = Thm.match (apply2 (Thm.cterm_of ctxt o Logic.mk_type) (V, U));
in
compose_tac ctxt (true, Drule.instantiate_normalize (instT,
- map (apsnd (Thm.cterm_of ctxt))
+ Vars.make (map (apsnd (Thm.cterm_of ctxt))
[((ixn, Ts ---> U --> body_type T), u),
((fst (dest_Var (head_of v1)), Ts ---> U), fold_rev Term.abs ps t),
- ((fst (dest_Var (head_of v2)), Ts ---> U), fold_rev Term.abs ps t')]) rl',
+ ((fst (dest_Var (head_of v2)), Ts ---> U), fold_rev Term.abs ps t')])) rl',
Thm.nprems_of rl) i
end
| NONE => no_tac);
--- a/src/Pure/Isar/class_declaration.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Pure/Isar/class_declaration.ML Fri Sep 10 14:59:19 2021 +0200
@@ -36,12 +36,15 @@
val a_tfree = (Name.aT, base_sort);
val a_type = TFree a_tfree;
val param_map_const = (map o apsnd) Const param_map;
- val param_map_inst = param_map |> map (fn (x, (c, T)) =>
- let val T' = map_atyps (K a_type) T in ((x, T'), cert (Const (c, T'))) end);
+ val param_map_inst =
+ Frees.build (param_map |> fold (fn (x, (c, T)) =>
+ let val T' = map_atyps (K a_type) T
+ in Frees.add ((x, T'), cert (Const (c, T'))) end));
val const_morph =
- Element.instantiate_normalize_morphism ([], param_map_inst);
+ Element.instantiate_normalize_morphism (TFrees.empty, param_map_inst);
val typ_morph =
- Element.instantiate_normalize_morphism ([(a_tfree, certT (Term.aT [class]))], [])
+ Element.instantiate_normalize_morphism
+ (TFrees.make [(a_tfree, certT (Term.aT [class]))], Frees.empty)
val (([raw_props], _, [(_, raw_inst_morph)], _, export_morph), _) = thy_ctxt
|> Expression.cert_goal_expression ([(class, (("", false),
(Expression.Named param_map_const, [])))], []);
--- a/src/Pure/Isar/code.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Pure/Isar/code.ML Fri Sep 10 14:59:19 2021 +0200
@@ -799,13 +799,13 @@
val tvs = fold (Term.add_tvars o Thm.prop_of) thms [];
val instT =
mk_desymbolization (unprefix "'") (prefix "'") (Thm.global_ctyp_of thy o TVar) tvs;
- in map (Thm.instantiate (instT, [])) thms end;
+ in map (Thm.instantiate (TVars.make instT, Vars.empty)) thms end;
fun desymbolize_vars thy thm =
let
val vs = Term.add_vars (Thm.prop_of thm) [];
val inst = mk_desymbolization I I (Thm.global_cterm_of thy o Var) vs;
- in Thm.instantiate ([], inst) thm end;
+ in Thm.instantiate (TVars.empty, Vars.make inst) thm end;
fun canonize_thms thy = desymbolize_tvars thy #> same_arity thy #> map (desymbolize_vars thy);
@@ -895,14 +895,16 @@
let
val mapping = map2 (fn (v, sort) => fn sort' =>
(v, Sorts.inter_sort (Sign.classes_of thy) (sort, sort'))) vs sorts;
- val inst = map2 (fn (v, sort) => fn (_, sort') =>
- (((v, 0), sort), Thm.global_ctyp_of thy (TFree (v, sort')))) vs mapping;
+ val instT =
+ TVars.build
+ (fold2 (fn (v, sort) => fn (_, sort') =>
+ TVars.add (((v, 0), sort), Thm.global_ctyp_of thy (TFree (v, sort')))) vs mapping);
val subst = (Term.map_types o map_type_tfree)
(fn (v, _) => TFree (v, the (AList.lookup (op =) mapping v)));
in
thm
|> Thm.varifyT_global
- |> Thm.instantiate (inst, [])
+ |> Thm.instantiate (instT, Vars.empty)
|> pair subst
end;
@@ -966,8 +968,9 @@
fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs [];
val sorts = map_transpose inter_sorts vss;
val vts = Name.invent_names Name.context Name.aT sorts;
- val thms' =
- map2 (fn vs => Thm.instantiate (vs ~~ map (Thm.ctyp_of ctxt o TFree) vts, [])) vss thms;
+ fun instantiate vs =
+ Thm.instantiate (TVars.make (vs ~~ map (Thm.ctyp_of ctxt o TFree) vts), Vars.empty);
+ val thms' = map2 instantiate vss thms;
val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms'))));
fun head_conv ct = if can Thm.dest_comb ct
then Conv.fun_conv head_conv ct
--- a/src/Pure/Isar/element.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Pure/Isar/element.ML Fri Sep 10 14:59:19 2021 +0200
@@ -47,8 +47,7 @@
val transform_witness: morphism -> witness -> witness
val conclude_witness: Proof.context -> witness -> thm
val pretty_witness: Proof.context -> witness -> Pretty.T
- val instantiate_normalize_morphism:
- ((string * sort) * ctyp) list * ((string * typ) * cterm) list -> morphism
+ val instantiate_normalize_morphism: ctyp TFrees.table * cterm Frees.table -> morphism
val satisfy_morphism: witness list -> morphism
val eq_term_morphism: theory -> term list -> morphism option
val eq_morphism: theory -> thm list -> morphism option
@@ -208,7 +207,8 @@
SOME C =>
let
val thesis = Var ((Auto_Bind.thesisN, Thm.maxidx_of th + 1), fastype_of C);
- val th' = Thm.instantiate ([], [(Term.dest_Var C, Thm.cterm_of ctxt thesis)]) th;
+ val insts = (TVars.empty, Vars.make [(Term.dest_Var C, Thm.cterm_of ctxt thesis)]);
+ val th' = Thm.instantiate insts th;
in (th', true) end
| NONE => (th, false));
--- a/src/Pure/Isar/expression.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Pure/Isar/expression.ML Fri Sep 10 14:59:19 2021 +0200
@@ -187,14 +187,15 @@
(* instantiation *)
val instT =
- (type_parms ~~ map Logic.dest_type type_parms'')
- |> map_filter (fn (v, T) => if TFree v = T then NONE else SOME (v, T));
+ TFrees.build
+ (fold2 (fn v => fn T => not (TFree v = T) ? TFrees.add (v, T))
+ type_parms (map Logic.dest_type type_parms''));
val cert_inst =
- ((map #1 params ~~
- map (Term_Subst.instantiateT_frees (TFrees.make instT)) parm_types) ~~ insts'')
- |> map_filter (fn (v, t) => if Free v = t then NONE else SOME (v, cert t));
+ Frees.build
+ (fold2 (fn v => fn t => not (Free v = t) ? Frees.add (v, cert t))
+ (map #1 params ~~ map (Term_Subst.instantiateT_frees instT) parm_types) insts'');
in
- (Element.instantiate_normalize_morphism (map (apsnd certT) instT, cert_inst) $>
+ (Element.instantiate_normalize_morphism (TFrees.map (K certT) instT, cert_inst) $>
Morphism.binding_morphism "Expression.inst" (Binding.prefix mandatory prfx), ctxt')
end;
--- a/src/Pure/Isar/generic_target.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Pure/Isar/generic_target.ML Fri Sep 10 14:59:19 2021 +0200
@@ -328,13 +328,15 @@
val instT =
TVars.build (fold2 (fn a => fn b =>
(case a of TVar v => TVars.add (v, b) | _ => I)) tvars tfrees);
- val cinstT = TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt T)) instT [];
+ val cinstT = TVars.map (K (Thm.ctyp_of ctxt)) instT;
val cinst =
- map_filter
- (fn (Var (xi, T), t) =>
- SOME ((xi, Term_Subst.instantiateT instT T),
- Thm.cterm_of ctxt (Term.map_types (Term_Subst.instantiateT instT) t))
- | _ => NONE) (vars ~~ frees);
+ Vars.build
+ (fold2 (fn v => fn t =>
+ (case v of
+ Var (xi, T) =>
+ Vars.add ((xi, Term_Subst.instantiateT instT T),
+ Thm.cterm_of ctxt (Term.map_types (Term_Subst.instantiateT instT) t))
+ | _ => I)) vars frees);
val result' = Thm.instantiate (cinstT, cinst) result;
(*import assumes/defines*)
--- a/src/Pure/Isar/obtain.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Pure/Isar/obtain.ML Fri Sep 10 14:59:19 2021 +0200
@@ -335,7 +335,7 @@
| _ => instT))));
val closed_rule = rule
|> Thm.forall_intr (Thm.cterm_of ctxt (Free thesis_var))
- |> Thm.instantiate (TVars.dest instT, []);
+ |> Thm.instantiate (instT, Vars.empty);
val ((_, rule' :: terms'), ctxt') = Variable.import false (closed_rule :: terms) ctxt;
val vars' =
--- a/src/Pure/Isar/subgoal.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Pure/Isar/subgoal.ML Fri Sep 10 14:59:19 2021 +0200
@@ -14,7 +14,7 @@
sig
type focus =
{context: Proof.context, params: (string * cterm) list, prems: thm list, asms: cterm list,
- concl: cterm, schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list}
+ concl: cterm, schematics: ctyp TVars.table * cterm Vars.table}
val focus_params: Proof.context -> int -> binding list option -> thm -> focus * thm
val focus_params_fixed: Proof.context -> int -> binding list option -> thm -> focus * thm
val focus_prems: Proof.context -> int -> binding list option -> thm -> focus * thm
@@ -39,7 +39,7 @@
type focus =
{context: Proof.context, params: (string * cterm) list, prems: thm list, asms: cterm list,
- concl: cterm, schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list};
+ concl: cterm, schematics: ctyp TVars.table * cterm Vars.table};
fun gen_focus (do_prems, do_concl) ctxt i bindings raw_st =
let
@@ -56,9 +56,9 @@
val text = asms @ (if do_concl then [concl] else []);
val ((_, inst), ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2;
- val schematic_terms = Vars.fold (fn (v, t) => cons (v, Thm.cterm_of ctxt3 t)) inst [];
+ val schematic_terms = Vars.map (K (Thm.cterm_of ctxt3)) inst;
- val schematics = (TVars.dest schematic_types, schematic_terms);
+ val schematics = (schematic_types, schematic_terms);
val asms' = map (Thm.instantiate_cterm schematics) asms;
val concl' = Thm.instantiate_cterm schematics concl;
val (prems, context) = Assumption.add_assumes asms' ctxt3;
@@ -100,8 +100,8 @@
in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end;
val (inst1, inst2) =
split_list (map (apply2 (apply2 (Thm.cterm_of ctxt))) (map2 var_inst vars ys));
-
- val th'' = Thm.instantiate ([], map (apfst (Term.dest_Var o Thm.term_of)) inst1) th';
+ val inst = Vars.build (fold (Vars.add o apfst (Term.dest_Var o Thm.term_of)) inst1);
+ val th'' = Thm.instantiate (TVars.empty, inst) th';
in ((inst2, th''), ctxt'') end;
(*
--- a/src/Pure/Proof/proof_checker.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Pure/Proof/proof_checker.ML Fri Sep 10 14:59:19 2021 +0200
@@ -81,7 +81,8 @@
val ctye =
(tvars @ map (fn ((_, S), ixn) => (ixn, S)) fmap ~~ map (Thm.global_ctyp_of thy) Ts);
in
- Thm.instantiate (ctye, []) (Thm.forall_intr_vars (Thm.forall_intr_frees thm'))
+ Thm.instantiate (TVars.make ctye, Vars.empty)
+ (Thm.forall_intr_vars (Thm.forall_intr_frees thm'))
end;
fun thm_of _ _ (PThm ({name, prop = prop', types = SOME Ts, ...}, _)) =
--- a/src/Pure/Tools/rule_insts.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Pure/Tools/rule_insts.ML Fri Sep 10 14:59:19 2021 +0200
@@ -160,8 +160,8 @@
in
thm
|> Drule.instantiate_normalize
- (map (apsnd (Thm.ctyp_of ctxt')) inst_tvars,
- map (apsnd (Thm.cterm_of ctxt')) inst_vars)
+ (TVars.make (map (apsnd (Thm.ctyp_of ctxt')) inst_tvars),
+ Vars.make (map (apsnd (Thm.cterm_of ctxt')) inst_vars))
|> singleton (Variable.export ctxt' ctxt)
|> Rule_Cases.save thm
end;
@@ -255,10 +255,12 @@
fun lift_var ((a, j), T) = ((a, j + inc), paramTs ---> lift_type T);
fun lift_term t = fold_rev Term.absfree params (Logic.incr_indexes (fixed, paramTs, inc) t);
- val inst_tvars' = inst_tvars
- |> map (fn (((a, i), S), T) => (((a, i + inc), S), Thm.ctyp_of inst_ctxt (lift_type T)));
- val inst_vars' = inst_vars
- |> map (fn (v, t) => (lift_var v, Thm.cterm_of inst_ctxt (lift_term t)));
+ val inst_tvars' =
+ TVars.build (inst_tvars |> fold (fn (((a, i), S), T) =>
+ TVars.add (((a, i + inc), S), Thm.ctyp_of inst_ctxt (lift_type T))));
+ val inst_vars' =
+ Vars.build (inst_vars |> fold (fn (v, t) =>
+ Vars.add (lift_var v, Thm.cterm_of inst_ctxt (lift_term t))));
val thm' = Thm.lift_rule cgoal thm
|> Drule.instantiate_normalize (inst_tvars', inst_vars')
@@ -277,8 +279,8 @@
fun var x = ((x, 0), propT);
fun cvar xi = Thm.cterm_of ctxt (Var (xi, propT));
val revcut_rl' =
- Drule.instantiate_normalize ([], [(var "V", cvar ("V", maxidx + 1)),
- (var "W", cvar ("W", maxidx + 1))]) Drule.revcut_rl;
+ Drule.revcut_rl |> Drule.instantiate_normalize
+ (TVars.empty, Vars.make [(var "V", cvar ("V", maxidx + 1)), (var "W", cvar ("W", maxidx + 1))]);
in
(case Seq.list_of
(Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = false}
--- a/src/Pure/conjunction.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Pure/conjunction.ML Fri Sep 10 14:59:19 2021 +0200
@@ -102,7 +102,8 @@
fun intr tha thb =
Thm.implies_elim
(Thm.implies_elim
- (Thm.instantiate ([], [(vA, Thm.cprop_of tha), (vB, Thm.cprop_of thb)]) conjunctionI)
+ (Thm.instantiate (TVars.empty, Vars.make [(vA, Thm.cprop_of tha), (vB, Thm.cprop_of thb)])
+ conjunctionI)
tha)
thb;
@@ -110,7 +111,7 @@
let
val (A, B) = dest_conjunction (Thm.cprop_of th)
handle TERM (msg, _) => raise THM (msg, 0, [th]);
- val inst = Thm.instantiate ([], [(vA, A), (vB, B)]);
+ val inst = Thm.instantiate (TVars.empty, Vars.make [(vA, A), (vB, B)]);
in
(Thm.implies_elim (inst conjunctionD1) th,
Thm.implies_elim (inst conjunctionD2) th)
--- a/src/Pure/drule.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Pure/drule.ML Fri Sep 10 14:59:19 2021 +0200
@@ -18,8 +18,7 @@
val lift_all: Proof.context -> cterm -> thm -> thm
val implies_elim_list: thm -> thm list -> thm
val implies_intr_list: cterm list -> thm -> thm
- val instantiate_normalize: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list ->
- thm -> thm
+ val instantiate_normalize: ctyp TVars.table * cterm Vars.table -> thm -> thm
val instantiate'_normalize: ctyp option list -> cterm option list -> thm -> thm
val infer_instantiate_types: Proof.context -> ((indexname * typ) * cterm) list -> thm -> thm
val infer_instantiate: Proof.context -> (indexname * cterm) list -> thm -> thm
@@ -192,7 +191,7 @@
| _ => inst)));
in
th
- |> Thm.instantiate ([], Vars.dest inst)
+ |> Thm.instantiate (TVars.empty, inst)
|> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt) ps
end;
@@ -217,15 +216,12 @@
val tvars = TVars.build (fold Thm.add_tvars ths);
val the_tvar = the o TVars.lookup tvars;
- val instT' =
- build (instT |> TVars.fold (fn (v, TVar (b, _)) =>
- cons (v, Thm.rename_tvar b (the_tvar v))));
+ val instT' = instT |> TVars.map (fn v => fn TVar (b, _) => Thm.rename_tvar b (the_tvar v));
- val vars = Vars.build (fold (Thm.add_vars o Thm.instantiate (instT', [])) ths);
+ val vars = Vars.build (fold (Thm.add_vars o Thm.instantiate (instT', Vars.empty)) ths);
val the_var = the o Vars.lookup vars;
val inst' =
- build (inst |> Vars.fold (fn (v, Var (b, _)) =>
- cons (v, Thm.var (b, Thm.ctyp_of_cterm (the_var v)))));
+ inst |> Vars.map (fn v => fn Var (b, _) => Thm.var (b, Thm.ctyp_of_cterm (the_var v)));
in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate (instT', inst')) ths end;
val zero_var_indexes = singleton zero_var_indexes_list;
@@ -602,7 +598,9 @@
let
val cT = Thm.ctyp_of_cterm ct;
val T = Thm.typ_of cT;
- in Thm.instantiate ([((("'a", 0), []), cT)], [((("x", 0), T), ct)]) termI end;
+ in
+ Thm.instantiate (TVars.make [((("'a", 0), []), cT)], Vars.make [((("x", 0), T), ct)]) termI
+ end;
fun dest_term th =
let val cprop = strip_imp_concl (Thm.cprop_of th) in
@@ -766,11 +764,12 @@
val (tyenv, _) = fold infer args (Vartab.empty, 0);
val instT =
- Vartab.fold (fn (xi, (S, T)) =>
- cons ((xi, S), Thm.ctyp_of ctxt (Envir.norm_type tyenv T))) tyenv [];
- val inst = args |> map (fn ((xi, T), cu) =>
- ((xi, Envir.norm_type tyenv T),
- Thm.instantiate_cterm (instT, []) (Thm.transfer_cterm thy cu)));
+ TVars.build (tyenv |> Vartab.fold (fn (xi, (S, T)) =>
+ TVars.add ((xi, S), Thm.ctyp_of ctxt (Envir.norm_type tyenv T))));
+ val inst =
+ Vars.build (args |> fold (fn ((xi, T), cu) =>
+ Vars.add ((xi, Envir.norm_type tyenv T),
+ Thm.instantiate_cterm (instT, Vars.empty) (Thm.transfer_cterm thy cu))));
in instantiate_normalize (instT, inst) th end
handle CTERM (msg, _) => raise THM (msg, 0, [raw_th])
| TERM (msg, _) => raise THM (msg, 0, [raw_th])
--- a/src/Pure/goal.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Pure/goal.ML Fri Sep 10 14:59:19 2021 +0200
@@ -58,7 +58,7 @@
-------- (init)
C \<Longrightarrow> #C
*)
-fun init C = Thm.instantiate ([], [((("A", 0), propT), C)]) Drule.protectI;
+fun init C = Thm.instantiate (TVars.empty, Vars.make [((("A", 0), propT), C)]) Drule.protectI;
(*
A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> C
@@ -122,8 +122,8 @@
val tfrees = TFrees.build (fold TFrees.add_tfrees (prop :: As));
val Ts = Names.build (TFrees.fold (Names.add_set o #1 o #1) tfrees);
val instT =
- build (tfrees |> TFrees.fold (fn ((a, S), _) =>
- cons (((a, 0), S), Thm.ctyp_of ctxt (TFree (a, S)))));
+ TVars.build (tfrees |> TFrees.fold (fn ((a, S), _) =>
+ TVars.add (((a, 0), S), Thm.ctyp_of ctxt (TFree (a, S)))));
val global_prop =
Logic.list_implies (As, prop)
@@ -142,7 +142,7 @@
val local_result =
Thm.future global_result global_prop
|> Thm.close_derivation \<^here>
- |> Thm.instantiate (instT, [])
+ |> Thm.instantiate (instT, Vars.empty)
|> Drule.forall_elim_list xs
|> fold (Thm.elim_implies o Thm.assume) assms
|> Thm.solve_constraints;
--- a/src/Pure/more_thm.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Pure/more_thm.ML Fri Sep 10 14:59:19 2021 +0200
@@ -63,7 +63,7 @@
val forall_intr_name: string * cterm -> thm -> thm
val forall_elim_var: int -> thm -> thm
val forall_elim_vars: int -> thm -> thm
- val instantiate_frees: ((string * sort) * ctyp) list * ((string * typ) * cterm) list -> thm -> thm
+ val instantiate_frees: ctyp TFrees.table * cterm Frees.table -> thm -> thm
val instantiate': ctyp option list -> cterm option list -> thm -> thm
val forall_intr_frees: thm -> thm
val forall_intr_vars: thm -> thm
@@ -375,26 +375,29 @@
(* instantiate frees *)
-fun instantiate_frees ([], []) th = th
- | instantiate_frees (instT, inst) th =
- let
- val idx = Thm.maxidx_of th + 1;
- fun index ((a, A), b) = (((a, idx), A), b);
- val insts = (map index instT, map index inst);
- val tfrees = Names.build (fold (Names.add_set o #1 o #1) instT);
- val frees = Names.build (fold (Names.add_set o #1 o #1) inst);
+fun instantiate_frees (instT, inst) th =
+ if TFrees.is_empty instT andalso Frees.is_empty inst then th
+ else
+ let
+ val idx = Thm.maxidx_of th + 1;
+ fun index ((a, A), b) = (((a, idx), A), b);
+ val insts =
+ (TVars.build (TFrees.fold (TVars.add o index) instT),
+ Vars.build (Frees.fold (Vars.add o index) inst));
+ val tfrees = Names.build (TFrees.fold (Names.add_set o #1 o #1) instT);
+ val frees = Names.build (Frees.fold (Names.add_set o #1 o #1) inst);
- val hyps = Thm.chyps_of th;
- val inst_cterm =
- Thm.generalize_cterm (tfrees, frees) idx #>
- Thm.instantiate_cterm insts;
- in
- th
- |> fold_rev Thm.implies_intr hyps
- |> Thm.generalize (tfrees, frees) idx
- |> Thm.instantiate insts
- |> fold (elim_implies o Thm.assume o inst_cterm) hyps
- end;
+ val hyps = Thm.chyps_of th;
+ val inst_cterm =
+ Thm.generalize_cterm (tfrees, frees) idx #>
+ Thm.instantiate_cterm insts;
+ in
+ th
+ |> fold_rev Thm.implies_intr hyps
+ |> Thm.generalize (tfrees, frees) idx
+ |> Thm.instantiate insts
+ |> fold (elim_implies o Thm.assume o inst_cterm) hyps
+ end;
(* instantiate by left-to-right occurrence of variables *)
@@ -411,9 +414,9 @@
err "more instantiations than variables in thm";
val instT = zip_vars (build_rev (Thm.fold_terms {hyps = false} Term.add_tvars thm)) cTs;
- val thm' = Thm.instantiate (instT, []) thm;
+ val thm' = Thm.instantiate (TVars.make instT, Vars.empty) thm;
val inst = zip_vars (build_rev (Thm.fold_terms {hyps = false} Term.add_vars thm')) cts;
- in Thm.instantiate ([], inst) thm' end;
+ in Thm.instantiate (TVars.empty, Vars.make inst) thm' end;
(* implicit generalization over variables -- canonical order *)
@@ -463,7 +466,7 @@
let val T' = Term_Subst.instantiateT instT T
in Vars.add (((x, i), T'), cert (Free ((x, T')))) inst end
| _ => inst)));
- in Thm.instantiate (TVars.dest cinstT, Vars.dest cinst) th end;
+ in Thm.instantiate (cinstT, cinst) th end;
fun unvarify_axiom thy = unvarify_global thy o Thm.axiom thy;
@@ -528,7 +531,7 @@
val axm_name = Sign.full_name thy' b;
val axm' = Thm.axiom thy' axm_name;
val thm =
- Thm.instantiate (recover, []) axm'
+ Thm.instantiate (TVars.make recover, Vars.empty) axm'
|> unvarify_global thy'
|> fold elim_implies of_sorts;
in ((axm_name, thm), thy') end;
@@ -545,7 +548,7 @@
val axm_name = Sign.full_name thy' b;
val axm' = Thm.axiom thy' axm_name;
val thm =
- Thm.instantiate (recover, []) axm'
+ Thm.instantiate (TVars.make recover, Vars.empty) axm'
|> unvarify_global thy'
|> fold_rev Thm.implies_intr prems;
in ((axm_name, thm), thy') end;
--- a/src/Pure/morphism.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Pure/morphism.ML Fri Sep 10 14:59:19 2021 +0200
@@ -43,10 +43,8 @@
val transfer_morphism': Proof.context -> morphism
val transfer_morphism'': Context.generic -> morphism
val trim_context_morphism: morphism
- val instantiate_frees_morphism:
- ((string * sort) * ctyp) list * ((string * typ) * cterm) list -> morphism
- val instantiate_morphism:
- ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> morphism
+ val instantiate_frees_morphism: ctyp TFrees.table * cterm Frees.table -> morphism
+ val instantiate_morphism: ctyp TVars.table * cterm Vars.table -> morphism
end;
structure Morphism: MORPHISM =
@@ -134,35 +132,37 @@
(* instantiate *)
-fun instantiate_frees_morphism ([], []) = identity
- | instantiate_frees_morphism (cinstT, cinst) =
- let
- val instT = TFrees.build (cinstT |> fold (fn (v, cT) => TFrees.add (v, Thm.typ_of cT)));
- val inst = Frees.build (cinst |> fold (fn (v, ct) => Frees.add (v, Thm.term_of ct)));
- in
- morphism "instantiate_frees"
- {binding = [],
- typ =
- if TFrees.is_empty instT then []
- else [Term_Subst.instantiateT_frees instT],
- term = [Term_Subst.instantiate_frees (instT, inst)],
- fact = [map (Thm.instantiate_frees (cinstT, cinst))]}
- end;
+fun instantiate_frees_morphism (cinstT, cinst) =
+ if TFrees.is_empty cinstT andalso Frees.is_empty cinst then identity
+ else
+ let
+ val instT = TFrees.map (K Thm.typ_of) cinstT;
+ val inst = Frees.map (K Thm.term_of) cinst;
+ in
+ morphism "instantiate_frees"
+ {binding = [],
+ typ =
+ if TFrees.is_empty instT then []
+ else [Term_Subst.instantiateT_frees instT],
+ term = [Term_Subst.instantiate_frees (instT, inst)],
+ fact = [map (Thm.instantiate_frees (cinstT, cinst))]}
+ end;
-fun instantiate_morphism ([], []) = identity
- | instantiate_morphism (cinstT, cinst) =
- let
- val instT = TVars.build (cinstT |> fold (fn (v, cT) => TVars.add (v, Thm.typ_of cT)));
- val inst = Vars.build (cinst |> fold (fn (v, ct) => Vars.add (v, Thm.term_of ct)));
- in
- morphism "instantiate"
- {binding = [],
- typ =
- if TVars.is_empty instT then []
- else [Term_Subst.instantiateT instT],
- term = [Term_Subst.instantiate (instT, inst)],
- fact = [map (Thm.instantiate (cinstT, cinst))]}
- end;
+fun instantiate_morphism (cinstT, cinst) =
+ if TVars.is_empty cinstT andalso Vars.is_empty cinst then identity
+ else
+ let
+ val instT = TVars.map (K Thm.typ_of) cinstT;
+ val inst = Vars.map (K Thm.term_of) cinst;
+ in
+ morphism "instantiate"
+ {binding = [],
+ typ =
+ if TVars.is_empty instT then []
+ else [Term_Subst.instantiateT instT],
+ term = [Term_Subst.instantiate (instT, inst)],
+ fact = [map (Thm.instantiate (cinstT, cinst))]}
+ end;
end;
--- a/src/Pure/raw_simplifier.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Pure/raw_simplifier.ML Fri Sep 10 14:59:19 2021 +0200
@@ -1226,7 +1226,8 @@
val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of eq);
val eq' =
Thm.implies_elim
- (Thm.instantiate ([], [(vA, prem), (vB, lhs), (vC, rhs)]) Drule.imp_cong)
+ (Thm.instantiate (TVars.empty, Vars.make [(vA, prem), (vB, lhs), (vC, rhs)])
+ Drule.imp_cong)
(Thm.implies_intr prem eq);
in
if not r then eq'
@@ -1237,9 +1238,11 @@
in
Thm.transitive
(Thm.transitive
- (Thm.instantiate ([], [(vA, prem'), (vB, prem), (vC, concl)]) Drule.swap_prems_eq)
+ (Thm.instantiate (TVars.empty, Vars.make [(vA, prem'), (vB, prem), (vC, concl)])
+ Drule.swap_prems_eq)
eq')
- (Thm.instantiate ([], [(vA, prem), (vB, prem''), (vC, concl)]) Drule.swap_prems_eq)
+ (Thm.instantiate (TVars.empty, Vars.make [(vA, prem), (vB, prem''), (vC, concl)])
+ Drule.swap_prems_eq)
end
end
--- a/src/Pure/tactic.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Pure/tactic.ML Fri Sep 10 14:59:19 2021 +0200
@@ -164,14 +164,15 @@
val template = Drule.list_implies (As, C);
val inst =
- (dest_Free (Thm.term_of C), Thm.cconcl_of st) ::
- Ctermtab.fold (fn (ct, i) => cons ((Name.bound i, propT), ct)) tab [];
+ Frees.build
+ (Frees.add (dest_Free (Thm.term_of C), Thm.cconcl_of st) #>
+ Ctermtab.fold (fn (ct, i) => Frees.add ((Name.bound i, propT), ct)) tab);
in
Thm.assume template
|> fold (Thm.elim_implies o Thm.assume) As
|> fold_rev Thm.implies_intr As'
|> Thm.implies_intr template
- |> Thm.instantiate_frees ([], inst)
+ |> Thm.instantiate_frees (TFrees.empty, inst)
|> Thm.elim_implies st
end;
in Seq.single st' end;
--- a/src/Pure/thm.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Pure/thm.ML Fri Sep 10 14:59:19 2021 +0200
@@ -56,10 +56,8 @@
val lambda: cterm -> cterm -> cterm
val adjust_maxidx_cterm: int -> cterm -> cterm
val incr_indexes_cterm: int -> cterm -> cterm
- val match: cterm * cterm ->
- ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
- val first_order_match: cterm * cterm ->
- ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
+ val match: cterm * cterm -> ctyp TVars.table * cterm Vars.table
+ val first_order_match: cterm * cterm -> ctyp TVars.table * cterm Vars.table
(*theorems*)
val fold_terms: {hyps: bool} -> (term -> 'a -> 'a) -> thm -> 'a -> 'a
val fold_atomic_ctyps: {hyps: bool} -> (typ -> bool) -> (ctyp -> 'a -> 'a) -> thm -> 'a -> 'a
@@ -157,10 +155,8 @@
val generalize: Names.set * Names.set -> int -> thm -> thm
val generalize_cterm: Names.set * Names.set -> int -> cterm -> cterm
val generalize_ctyp: Names.set -> int -> ctyp -> ctyp
- val instantiate: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list ->
- thm -> thm
- val instantiate_cterm: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list ->
- cterm -> cterm
+ val instantiate: ctyp TVars.table * cterm Vars.table -> thm -> thm
+ val instantiate_cterm: ctyp TVars.table * cterm Vars.table -> cterm -> cterm
val trivial: cterm -> thm
val of_class: ctyp * class -> thm
val unconstrainT: thm -> thm
@@ -651,7 +647,10 @@
let val T = Envir.subst_type Tinsts U in
(((x, i), T), Cterm {t = t, T = T, cert = cert, maxidx = maxidx2, sorts = sorts})
end;
- in (Vartab.fold (cons o mk_cTinst) Tinsts [], Vartab.fold (cons o mk_ctinst) tinsts []) end;
+ in
+ (TVars.build (Vartab.fold (TVars.add o mk_cTinst) Tinsts),
+ Vars.build (Vartab.fold (Vars.add o mk_ctinst) tinsts))
+ end;
in
@@ -1630,12 +1629,12 @@
val add_instT_sorts = add_sorts (fn Ctyp {sorts, ...} => sorts);
val add_inst_sorts = add_sorts (fn Cterm {sorts, ...} => sorts);
-fun add_instT thy (v as (_, S), Ctyp {T = U, maxidx, ...}) =
- if Sign.of_sort thy (U, S) then TVars.add (v, (U, maxidx))
+fun make_instT thy (v as (_, S)) (Ctyp {T = U, maxidx, ...}) =
+ if Sign.of_sort thy (U, S) then (U, maxidx)
else raise TYPE ("Type not of sort " ^ Syntax.string_of_sort_global thy S, [U], []);
-fun add_inst thy (v as (_, T), Cterm {t = u, T = U, maxidx, ...}) =
- if T = U then Vars.add (v, (u, maxidx))
+fun make_inst thy (v as (_, T)) (Cterm {t = u, T = U, maxidx, ...}) =
+ if T = U then (u, maxidx)
else
let
fun pretty_typing t ty =
@@ -1651,17 +1650,18 @@
fun prep_insts (instT, inst) (cert, sorts) =
let
val cert' = cert
- |> fold add_instT_cert instT
- |> fold add_inst_cert inst;
- val thy' = Context.certificate_theory cert'
- handle ERROR msg => raise CONTEXT (msg, map #2 instT, map #2 inst, [], NONE);
+ |> TVars.fold add_instT_cert instT
+ |> Vars.fold add_inst_cert inst;
+ val thy' =
+ Context.certificate_theory cert' handle ERROR msg =>
+ raise CONTEXT (msg, TVars.dest instT |> map #2, Vars.dest inst |> map #2, [], NONE);
val sorts' = sorts
- |> fold add_instT_sorts instT
- |> fold add_inst_sorts inst;
+ |> TVars.fold add_instT_sorts instT
+ |> Vars.fold add_inst_sorts inst;
- val instT' = TVars.build (fold (add_instT thy') instT);
- val inst' = Vars.build (fold (add_inst thy') inst);
+ val instT' = TVars.map (make_instT thy') instT;
+ val inst' = Vars.map (make_inst thy') inst;
in ((instT', inst'), (cert', sorts')) end;
in
@@ -1669,49 +1669,51 @@
(*Left-to-right replacements: ctpairs = [..., (vi, ti), ...].
Instantiates distinct Vars by terms of same type.
Does NOT normalize the resulting theorem!*)
-fun instantiate ([], []) th = th
- | instantiate (instT, inst) th =
- let
- val Thm (der, {cert, hyps, constraints, shyps, tpairs, prop, ...}) = th;
- val ((instT', inst'), (cert', shyps')) = prep_insts (instT, inst) (cert, shyps)
- handle CONTEXT (msg, cTs, cts, ths, context) =>
- raise CONTEXT (msg, cTs, cts, th :: ths, context);
+fun instantiate (instT, inst) th =
+ if TVars.is_empty instT andalso Vars.is_empty inst then th
+ else
+ let
+ val Thm (der, {cert, hyps, constraints, shyps, tpairs, prop, ...}) = th;
+ val ((instT', inst'), (cert', shyps')) = prep_insts (instT, inst) (cert, shyps)
+ handle CONTEXT (msg, cTs, cts, ths, context) =>
+ raise CONTEXT (msg, cTs, cts, th :: ths, context);
- val subst = Term_Subst.instantiate_maxidx (instT', inst');
- val (prop', maxidx1) = subst prop ~1;
- val (tpairs', maxidx') =
- fold_map (fn (t, u) => fn i => subst t i ||>> subst u) tpairs maxidx1;
+ val subst = Term_Subst.instantiate_maxidx (instT', inst');
+ val (prop', maxidx1) = subst prop ~1;
+ val (tpairs', maxidx') =
+ fold_map (fn (t, u) => fn i => subst t i ||>> subst u) tpairs maxidx1;
- val thy' = Context.certificate_theory cert';
- val constraints' =
- TVars.fold (fn ((_, S), (T, _)) => insert_constraints thy' (T, S))
- instT' constraints;
- in
- Thm (deriv_rule1
- (fn d => Proofterm.instantiate (TVars.map (K #1) instT', Vars.map (K #1) inst') d) der,
- {cert = cert',
- tags = [],
- maxidx = maxidx',
- constraints = constraints',
- shyps = shyps',
- hyps = hyps,
- tpairs = tpairs',
- prop = prop'})
- |> solve_constraints
- end
- handle TYPE (msg, _, _) => raise THM (msg, 0, [th]);
+ val thy' = Context.certificate_theory cert';
+ val constraints' =
+ TVars.fold (fn ((_, S), (T, _)) => insert_constraints thy' (T, S))
+ instT' constraints;
+ in
+ Thm (deriv_rule1
+ (fn d => Proofterm.instantiate (TVars.map (K #1) instT', Vars.map (K #1) inst') d) der,
+ {cert = cert',
+ tags = [],
+ maxidx = maxidx',
+ constraints = constraints',
+ shyps = shyps',
+ hyps = hyps,
+ tpairs = tpairs',
+ prop = prop'})
+ |> solve_constraints
+ end
+ handle TYPE (msg, _, _) => raise THM (msg, 0, [th]);
-fun instantiate_cterm ([], []) ct = ct
- | instantiate_cterm (instT, inst) ct =
- let
- val Cterm {cert, t, T, sorts, ...} = ct;
- val ((instT', inst'), (cert', sorts')) = prep_insts (instT, inst) (cert, sorts);
- val subst = Term_Subst.instantiate_maxidx (instT', inst');
- val substT = Term_Subst.instantiateT_maxidx instT';
- val (t', maxidx1) = subst t ~1;
- val (T', maxidx') = substT T maxidx1;
- in Cterm {cert = cert', t = t', T = T', sorts = sorts', maxidx = maxidx'} end
- handle TYPE (msg, _, _) => raise CTERM (msg, [ct]);
+fun instantiate_cterm (instT, inst) ct =
+ if TVars.is_empty instT andalso Vars.is_empty inst then ct
+ else
+ let
+ val Cterm {cert, t, T, sorts, ...} = ct;
+ val ((instT', inst'), (cert', sorts')) = prep_insts (instT, inst) (cert, sorts);
+ val subst = Term_Subst.instantiate_maxidx (instT', inst');
+ val substT = Term_Subst.instantiateT_maxidx instT';
+ val (t', maxidx1) = subst t ~1;
+ val (T', maxidx') = substT T maxidx1;
+ in Cterm {cert = cert', t = t', T = T', sorts = sorts', maxidx = maxidx'} end
+ handle TYPE (msg, _, _) => raise CTERM (msg, [ct]);
end;
@@ -2278,7 +2280,7 @@
val names = Name.invent Name.context Name.aT (length tvars);
val tinst =
map2 (fn (ai, S) => fn b => ((ai, S), global_ctyp_of thy (TVar ((b, 0), S)))) tvars names;
- in instantiate (tinst, []) thm end
+ in instantiate (TVars.make tinst, Vars.empty) thm end
(* class relations *)
--- a/src/Pure/variable.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Pure/variable.ML Fri Sep 10 14:59:19 2021 +0200
@@ -618,7 +618,7 @@
let
val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt;
val instT' = TVars.map (K (Thm.ctyp_of ctxt')) instT;
- val ths' = map (Thm.instantiate (TVars.dest instT', [])) ths;
+ val ths' = map (Thm.instantiate (instT', Vars.empty)) ths;
in ((instT', ths'), ctxt') end;
fun import_prf is_open prf ctxt =
@@ -632,7 +632,7 @@
val ((instT, inst), ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt;
val instT' = TVars.map (K (Thm.ctyp_of ctxt')) instT;
val inst' = Vars.map (K (Thm.cterm_of ctxt')) inst;
- val ths' = map (Thm.instantiate (TVars.dest instT', Vars.dest inst')) ths;
+ val ths' = map (Thm.instantiate (instT', inst')) ths;
in (((instT', inst'), ths'), ctxt') end;
fun import_vars ctxt th =
--- a/src/Tools/Code/code_preproc.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Tools/Code/code_preproc.ML Fri Sep 10 14:59:19 2021 +0200
@@ -213,7 +213,7 @@
if eq_list (eq_fst (op =)) (vs_normalized, vs_original)
then (K I, ct)
else
- (K (Thm.instantiate (normalization, []) o Thm.varifyT_global),
+ (K (Thm.instantiate (TVars.make normalization, Vars.empty) o Thm.varifyT_global),
Thm.cterm_of ctxt (map_types normalize t))
end;
--- a/src/Tools/IsaPlanner/rw_inst.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Tools/IsaPlanner/rw_inst.ML Fri Sep 10 14:59:19 2021 +0200
@@ -174,11 +174,11 @@
val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts);
(* certified instantiations for types *)
- val ctyp_insts = map (fn (ix, (s, ty)) => ((ix, s), Thm.ctyp_of ctxt ty)) typinsts;
+ val ctyp_insts = TVars.make (map (fn (ix, (s, ty)) => ((ix, s), Thm.ctyp_of ctxt ty)) typinsts);
(* type instantiated versions *)
- val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm;
- val rule_tyinst = Thm.instantiate (ctyp_insts,[]) rule;
+ val tgt_th_tyinst = Thm.instantiate (ctyp_insts,Vars.empty) target_thm;
+ val rule_tyinst = Thm.instantiate (ctyp_insts,Vars.empty) rule;
val term_typ_inst = map (fn (ix,(_,ty)) => (ix,ty)) typinsts;
(* type instanitated outer term *)
@@ -198,10 +198,10 @@
(* create certms of instantiations *)
val cinsts_tyinst =
- map (fn (ix, (ty, t)) => ((ix, ty), Thm.cterm_of ctxt t)) insts_tyinst_inst;
+ Vars.make (map (fn (ix, (ty, t)) => ((ix, ty), Thm.cterm_of ctxt t)) insts_tyinst_inst);
(* The instantiated rule *)
- val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst);
+ val rule_inst = rule_tyinst |> Thm.instantiate (TVars.empty, cinsts_tyinst);
(* Create a table of vars to be renamed after instantiation - ie
other uninstantiated vars in the hyps the *instantiated* rule
@@ -217,7 +217,7 @@
val couter_inst = Thm.reflexive (Thm.cterm_of ctxt outerterm_inst);
val (cprems, abstract_rule_inst) =
rule_inst
- |> Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) cterm_renamings)
+ |> Thm.instantiate (TVars.empty, Vars.make (map (apfst (dest_Var o Thm.term_of)) cterm_renamings))
|> mk_abstractedrule ctxt FakeTs_tyinst Ts_tyinst;
val specific_tgt_rule =
Conv.fconv_rule Drule.beta_eta_conversion
@@ -226,8 +226,8 @@
(* create an instantiated version of the target thm *)
val tgt_th_inst =
tgt_th_tyinst
- |> Thm.instantiate ([], cinsts_tyinst)
- |> Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) cterm_renamings);
+ |> Thm.instantiate (TVars.empty, cinsts_tyinst)
+ |> Thm.instantiate (TVars.empty, Vars.make (map (apfst (dest_Var o Thm.term_of)) cterm_renamings));
val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings;
in
--- a/src/Tools/coherent.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Tools/coherent.ML Fri Sep 10 14:59:19 2021 +0200
@@ -175,13 +175,14 @@
val _ =
cond_trace ctxt (fn () =>
Pretty.string_of (Pretty.big_list "asms:" (map (Thm.pretty_thm ctxt) asms)));
+ val instT = map (fn (ixn, (S, T)) => ((ixn, S), Thm.ctyp_of ctxt T)) (Vartab.dest tye);
+ val inst =
+ map (fn (ixn, (T, t)) =>
+ ((ixn, Envir.subst_type tye T), Thm.cterm_of ctxt t)) (Vartab.dest env) @
+ map (fn (ixnT, t) => (ixnT, Thm.cterm_of ctxt t)) insts;
val th' =
Drule.implies_elim_list
- (Thm.instantiate
- (map (fn (ixn, (S, T)) => ((ixn, S), Thm.ctyp_of ctxt T)) (Vartab.dest tye),
- map (fn (ixn, (T, t)) =>
- ((ixn, Envir.subst_type tye T), Thm.cterm_of ctxt t)) (Vartab.dest env) @
- map (fn (ixnT, t) => (ixnT, Thm.cterm_of ctxt t)) insts) th)
+ (Thm.instantiate (TVars.make instT, Vars.make inst) th)
(map (nth asms) is);
val (_, cases) = dest_elim (Thm.prop_of th');
in
--- a/src/Tools/induct.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Tools/induct.ML Fri Sep 10 14:59:19 2021 +0200
@@ -593,13 +593,16 @@
local
-fun dest_env ctxt env =
+fun insts_env ctxt env =
let
val pairs = Vartab.dest (Envir.term_env env);
val types = Vartab.dest (Envir.type_env env);
val ts = map (Thm.cterm_of ctxt o Envir.norm_term env o #2 o #2) pairs;
val xs = map #1 pairs ~~ map Thm.typ_of_cterm ts;
- in (map (fn (ai, (S, T)) => ((ai, S), Thm.ctyp_of ctxt T)) types, xs ~~ ts) end;
+ val instT =
+ TVars.build (types |> fold (fn (ai, (S, T)) => TVars.add ((ai, S), Thm.ctyp_of ctxt T)));
+ val inst = Vars.build (fold2 (fn x => fn t => Vars.add (x, t)) xs ts);
+ in (instT, inst) end;
in
@@ -620,7 +623,7 @@
in
Unify.smash_unifiers (Context.Proof ctxt)
[(Thm.concl_of rule', concl)] (Envir.empty (Thm.maxidx_of rule'))
- |> Seq.map (fn env => Drule.instantiate_normalize (dest_env ctxt env) rule')
+ |> Seq.map (fn env => Drule.instantiate_normalize (insts_env ctxt env) rule')
end
end
handle General.Subscript => Seq.empty;
--- a/src/Tools/misc_legacy.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Tools/misc_legacy.ML Fri Sep 10 14:59:19 2021 +0200
@@ -185,7 +185,8 @@
fold Term.add_vars (Logic.strip_imp_prems prop) []
and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) []
val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
- val st' = Thm.instantiate ([], map mk_inst subgoal_insts) st
+ val st' =
+ Thm.instantiate (TVars.empty, Vars.build (fold (Vars.add o mk_inst) subgoal_insts)) st
val emBs = map (Thm.cterm_of ctxt o embed) (Thm.prems_of st')
val Cth = implies_elim_list st' (map (elim o Thm.assume) emBs)
in (*restore the unknowns to the hypotheses*)
@@ -247,7 +248,9 @@
fun thaw i th' = (*i is non-negative increment for Var indexes*)
th' |> forall_intr_list (map #2 insts)
|> forall_elim_list (map (Thm.incr_indexes_cterm i o #1) insts)
- in (Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) insts) fth, thaw) end
+ in
+ (Thm.instantiate (TVars.empty, Vars.build (fold (Vars.add o apfst (dest_Var o Thm.term_of)) insts)) fth, thaw)
+ end
end;
end;
--- a/src/Tools/nbe.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/Tools/nbe.ML Fri Sep 10 14:59:19 2021 +0200
@@ -109,7 +109,7 @@
val tvars =
Term.add_tvars (#1 (Logic.dest_equals (Logic.strip_imp_concl (Thm.prop_of thm)))) [];
val instT = map2 (fn v => fn (_, (_, (cT, _))) => (v, cT)) tvars vs_tab;
- in Thm.instantiate (instT, []) thm end;
+ in Thm.instantiate (TVars.make instT, Vars.empty) thm end;
fun of_class (TFree (v, _), class) =
the (AList.lookup (op =) ((snd o snd o the o AList.lookup (op =) vs_tab) v) class)
| of_class (T, _) = error ("Bad type " ^ Syntax.string_of_typ ctxt T);
--- a/src/ZF/Tools/cartprod.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/ZF/Tools/cartprod.ML Fri Sep 10 14:59:19 2021 +0200
@@ -108,8 +108,8 @@
val newt = ap_split T1 T2 (Var(v,T'))
in
remove_split ctxt
- (Drule.instantiate_normalize ([],
- [((v, Ind_Syntax.iT-->T2), Thm.cterm_of ctxt newt)]) rl)
+ (Drule.instantiate_normalize (TVars.empty,
+ Vars.make [((v, Ind_Syntax.iT-->T2), Thm.cterm_of ctxt newt)]) rl)
end
| split_rule_var _ (t,T,rl) = rl;
--- a/src/ZF/Tools/inductive_package.ML Thu Sep 09 23:07:02 2021 +0200
+++ b/src/ZF/Tools/inductive_package.ML Fri Sep 10 14:59:19 2021 +0200
@@ -508,7 +508,7 @@
The name "x.1" comes from the "RS spec" !*)
val inst =
case elem_frees of [_] => I
- | _ => Drule.instantiate_normalize ([], [(((("x",1), Ind_Syntax.iT)),
+ | _ => Drule.instantiate_normalize (TVars.empty, Vars.make [(((("x",1), Ind_Syntax.iT)),
Thm.global_cterm_of thy4 elem_tuple)]);
(*strip quantifier and the implication*)