--- a/src/Doc/Implementation/Logic.thy Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Doc/Implementation/Logic.thy Thu Sep 09 12:33:14 2021 +0200
@@ -585,7 +585,7 @@
@{define_ML Thm.forall_elim: "cterm -> thm -> thm"} \\
@{define_ML Thm.implies_intr: "cterm -> thm -> thm"} \\
@{define_ML Thm.implies_elim: "thm -> thm -> thm"} \\
- @{define_ML Thm.generalize: "Symtab.set * Symtab.set -> int -> 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.add_axiom: "Proof.context ->
--- a/src/Doc/Implementation/Proof.thy Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Doc/Implementation/Proof.thy Thu Sep 09 12:33:14 2021 +0200
@@ -101,7 +101,7 @@
@{define_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\
@{define_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
@{define_ML Variable.import: "bool -> thm list -> Proof.context ->
- ((ctyp Term_Subst.TVars.table * cterm Term_Subst.Vars.table) * thm list)
+ ((ctyp TVars.table * cterm Vars.table) * thm list)
* Proof.context"} \\
@{define_ML Variable.focus: "binding list option -> term -> Proof.context ->
((string * (string * typ)) list * term) * Proof.context"} \\
--- a/src/HOL/Eisbach/match_method.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/HOL/Eisbach/match_method.ML Thu Sep 09 12:33:14 2021 +0200
@@ -173,7 +173,7 @@
val param_thm = map (Drule.mk_term o Thm.cterm_of ctxt' o Free) abs_nms
|> Conjunction.intr_balanced
- |> Drule.generalize (Symtab.empty, Symtab.make_set (map fst abs_nms))
+ |> Drule.generalize (Names.empty, Names.make_set (map fst abs_nms))
|> Thm.tag_free_dummy;
val atts = map (Attrib.attribute ctxt') att;
@@ -453,7 +453,7 @@
val ((_, inst), ctxt'') = Variable.import_inst true [Thm.term_of concl] ctxt';
val schematic_terms =
- Term_Subst.Vars.fold (fn (v, t) => cons (v, Thm.cterm_of ctxt'' t)) inst [];
+ 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;
--- a/src/HOL/Library/cconv.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/HOL/Library/cconv.ML Thu Sep 09 12:33:14 2021 +0200
@@ -147,7 +147,7 @@
val inst = Thm.match (Drule.cprems_of rule |> hd, mk_concl (Thm.term_of v) eq)
in
(Drule.instantiate_normalize inst rule OF
- [Drule.generalize (Symtab.empty, Symtab.make_set [u]) eq])
+ [Drule.generalize (Names.empty, Names.make_set [u]) eq])
|> Drule.zero_var_indexes
end
--- a/src/HOL/Library/code_lazy.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/HOL/Library/code_lazy.ML Thu Sep 09 12:33:14 2021 +0200
@@ -122,7 +122,7 @@
|> Conjunction.intr_balanced
|> rewrite_rule ctxt [Thm.symmetric (Thm.assume assum)]
|> Thm.implies_intr assum
- |> Thm.generalize (Symtab.empty, Symtab.make_set params) 0
+ |> Thm.generalize (Names.empty, Names.make_set params) 0
|> Axclass.unoverload ctxt
|> Thm.varifyT_global
end
@@ -495,7 +495,7 @@
|> Drule.infer_instantiate' lthy10
[SOME (Thm.cterm_of lthy10 (Const (\<^const_name>\<open>Pure.dummy_pattern\<close>, HOLogic.unitT --> lazy_type)))]
|> Thm.generalize
- (Symtab.make_set (map (fst o dest_TFree) type_args), Symtab.empty)
+ (Names.make_set (map (fst o dest_TFree) type_args), Names.empty)
(Variable.maxidx_of lthy10 + 1);
val ctr_post = delay_dummy_thm :: map (fn thm => thm RS @{thm sym}) ctrs_lazy_thms
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Thu Sep 09 12:33:14 2021 +0200
@@ -45,7 +45,7 @@
('a -> thm -> 'b Seq.seq) -> 'a -> thm -> 'b Seq.seq
val try_dest_Trueprop : term -> term
- val type_devar : typ Term_Subst.TVars.table -> term -> term
+ val type_devar : typ TVars.table -> term -> term
val diff_and_instantiate : Proof.context -> thm -> term -> term -> thm
val batter_tac : Proof.context -> int -> tactic
@@ -573,7 +573,7 @@
val typeval = map (fn (v, T) => (dest_TVar v, Thm.ctyp_of ctxt T)) type_pairing
val typeval_env =
- Term_Subst.TVars.table (map (apfst dest_TVar) type_pairing)
+ TVars.make (map (apfst dest_TVar) type_pairing)
(*valuation of term variables*)
val termval =
map (apfst (dest_Var o type_devar typeval_env)) term_pairing
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Sep 09 12:33:14 2021 +0200
@@ -852,7 +852,7 @@
|> unfold_thms lthy [dtor_ctor];
in
(fp_map_thm' RS ctor_cong RS (ctor_dtor RS sym RS trans))
- |> Drule.generalize (Symtab.empty, Symtab.make_set [y_s])
+ |> Drule.generalize (Names.empty, Names.make_set [y_s])
end;
val map_thms =
@@ -931,7 +931,7 @@
|> infer_instantiate' lthy (replicate live NONE @
[SOME (Thm.cterm_of lthy (ctorA $ y)), SOME (Thm.cterm_of lthy (ctorB $ z))])
|> unfold_thms lthy [dtor_ctor]
- |> Drule.generalize (Symtab.empty, Symtab.make_set [y_s, z_s])
+ |> Drule.generalize (Names.empty, Names.make_set [y_s, z_s])
end;
val rel_inject_thms =
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Thu Sep 09 12:33:14 2021 +0200
@@ -160,7 +160,7 @@
val eq = Abs (Name.uu, T, HOLogic.mk_eq (Free (s, T), Bound 0));
in
Thm.instantiate' [] [SOME (Thm.cterm_of ctxt eq)] split
- |> Drule.generalize (Symtab.empty, Symtab.make_set [s])
+ |> Drule.generalize (Names.empty, Names.make_set [s])
end
| _ => split);
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Thu Sep 09 12:33:14 2021 +0200
@@ -42,7 +42,7 @@
|> Conjunction.intr_balanced
|> rewrite_rule ctxt [Thm.symmetric (Thm.assume assum)]
|> Thm.implies_intr assum
- |> Thm.generalize (Symtab.empty, Symtab.make_set params) 0
+ |> Thm.generalize (Names.empty, Names.make_set params) 0
|> Axclass.unoverload ctxt
|> Thm.varifyT_global
end;
--- a/src/HOL/Tools/Function/induction_schema.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/HOL/Tools/Function/induction_schema.ML Thu Sep 09 12:33:14 2021 +0200
@@ -381,7 +381,7 @@
val res = Conjunction.intr_balanced (map_index project branches)
|> fold_rev Thm.implies_intr (map Thm.cprop_of newgoals @ steps)
- |> Drule.generalize (Symtab.empty, Symtab.make_set [Rn])
+ |> Drule.generalize (Names.empty, Names.make_set [Rn])
val nbranches = length branches
val npres = length pres
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Thu Sep 09 12:33:14 2021 +0200
@@ -78,8 +78,8 @@
val (instT, lthy2) = lthy1
|> Variable.declare_names fixed_crel
|> Variable.importT_inst (param_rel_subst :: args_subst)
- val args_fixed = (map (Term_Subst.instantiate (instT, Term_Subst.Vars.empty))) args_subst
- val param_rel_fixed = Term_Subst.instantiate (instT, Term_Subst.Vars.empty) param_rel_subst
+ val args_fixed = (map (Term_Subst.instantiate (instT, Vars.empty))) args_subst
+ val param_rel_fixed = Term_Subst.instantiate (instT, Vars.empty) param_rel_subst
val rty = (domain_type o fastype_of) param_rel_fixed
val relcomp_op = Const (\<^const_name>\<open>relcompp\<close>,
(rty --> rty' --> HOLogic.boolT) -->
@@ -295,7 +295,7 @@
let
val tvars = rev (subtract op= exclude (fold Term.add_tvars ts []))
val (tfrees, ctxt') = Variable.invent_types (map #2 tvars) ctxt
- in (Term_Subst.TVars.table (tvars ~~ map TFree tfrees), ctxt') end
+ in (TVars.make (tvars ~~ map TFree tfrees), ctxt') end
fun import_inst_exclude exclude ts ctxt =
let
@@ -304,7 +304,7 @@
val vars = map (apsnd (Term_Subst.instantiateT instT))
(rev (subtract op= exclude (fold Term.add_vars ts [])))
val (xs, ctxt'') = Variable.variant_fixes (map (#1 o #1) vars) ctxt'
- val inst = Term_Subst.Vars.table (vars ~~ map Free (xs ~~ map #2 vars))
+ val inst = Vars.make (vars ~~ map Free (xs ~~ map #2 vars))
in ((instT, inst), ctxt'') end
fun import_terms_exclude exclude ts ctxt =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Sep 09 12:33:14 2021 +0200
@@ -870,8 +870,8 @@
val (pats', _, ctxt3) = fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2)
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 (Term_Subst.Vars.dest t_insts)
- val intro'' = Thm.instantiate (Term_Subst.TVars.dest T_insts, t_insts') intro
+ val t_insts' = map rewrite_pat (Vars.dest t_insts)
+ val intro'' = Thm.instantiate (TVars.dest T_insts, t_insts') intro
val [intro'''] = Variable.export ctxt3 ctxt [intro'']
val intro'''' =
Simplifier.full_simplify
@@ -1072,10 +1072,7 @@
" (trying to match " ^ Syntax.string_of_typ ctxt' (fastype_of pred') ^
" and " ^ Syntax.string_of_typ ctxt' (fastype_of pred) ^ ")" ^
" in " ^ Thm.string_of_thm ctxt' th)
- in
- Vartab.fold (fn (xi, (S, T)) => Term_Subst.TVars.add ((xi, S), T))
- subst Term_Subst.TVars.empty
- end
+ in TVars.build (Vartab.fold (fn (xi, (S, T)) => TVars.add ((xi, S), T)) subst) end
fun instantiate_typ th =
let
val (pred', _) = strip_intro_concl th
@@ -1084,7 +1081,7 @@
raise Fail "Trying to instantiate another predicate"
else ()
val instT =
- Term_Subst.TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt' T))
+ TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt' T))
(subst_of (pred', pred)) [];
in Thm.instantiate (instT, []) th end
fun instantiate_ho_args th =
@@ -1094,7 +1091,7 @@
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
val outp_pred =
- Term_Subst.instantiate (subst_of (inp_pred, pred), Term_Subst.Vars.empty) inp_pred
+ Term_Subst.instantiate (subst_of (inp_pred, pred), Vars.empty) inp_pred
val ((_, ths'), ctxt1) =
Variable.import false (map (instantiate_typ #> instantiate_ho_args) ths) ctxt'
in
@@ -1163,8 +1160,7 @@
val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
fun varify (t, (i, ts)) =
let
- val t' = map_types (Logic.incr_tvar (i + 1))
- (#2 (Type.varify_global Term_Subst.TFrees.empty t))
+ val t' = map_types (Logic.incr_tvar (i + 1)) (#2 (Type.varify_global TFrees.empty t))
in (maxidx_of_term t', t' :: ts) end
val (i, cs') = List.foldr varify (~1, []) cs
val (i', intr_ts') = List.foldr varify (i, []) intr_ts
--- a/src/HOL/Tools/SMT/smt_replay_methods.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_replay_methods.ML Thu Sep 09 12:33:14 2021 +0200
@@ -171,7 +171,7 @@
fun by_tac ctxt thms ns ts t tac =
Goal.prove ctxt [] (map as_prop ts) (as_prop t)
(fn {context, prems} => HEADGOAL (tac context prems))
- |> Drule.generalize (Symtab.empty, Symtab.make_set ns)
+ |> Drule.generalize (Names.empty, Names.make_set ns)
|> discharge 1 thms
fun prove ctxt t tac = by_tac ctxt [] [] [] t (K o tac)
--- a/src/HOL/Tools/Transfer/transfer.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML Thu Sep 09 12:33:14 2021 +0200
@@ -575,7 +575,7 @@
((Name.clean_index (prep a, idx), \<^typ>\<open>bool \<Rightarrow> bool \<Rightarrow> bool\<close>), Thm.cterm_of ctxt' t)
in
thm
- |> Thm.generalize (Symtab.make_set tfrees, Symtab.make_set (rnames @ frees)) idx
+ |> Thm.generalize (Names.make_set tfrees, Names.make_set (rnames @ frees)) idx
|> Thm.instantiate (map tinst binsts, map inst binsts)
end
@@ -596,7 +596,7 @@
((Name.clean_index (prep a, idx), \<^typ>\<open>bool \<Rightarrow> bool \<Rightarrow> bool\<close>), Thm.cterm_of ctxt' t)
in
thm
- |> Thm.generalize (Symtab.make_set tfrees, Symtab.make_set (rnames @ frees)) idx
+ |> Thm.generalize (Names.make_set tfrees, Names.make_set (rnames @ frees)) idx
|> Thm.instantiate (map tinst binsts, map inst binsts)
end
@@ -719,7 +719,7 @@
|> Raw_Simplifier.rewrite_rule ctxt' post_simps
|> Simplifier.norm_hhf ctxt'
|> Drule.generalize
- (Symtab.make_set (map (fst o dest_TFree o Thm.typ_of o snd) instT), Symtab.empty)
+ (Names.make_set (map (fst o dest_TFree o Thm.typ_of o snd) instT), Names.empty)
|> Drule.zero_var_indexes
end
(*
@@ -755,7 +755,7 @@
|> Raw_Simplifier.rewrite_rule ctxt' post_simps
|> Simplifier.norm_hhf ctxt'
|> Drule.generalize
- (Symtab.make_set (map (fst o dest_TFree o Thm.typ_of o snd) instT), Symtab.empty)
+ (Names.make_set (map (fst o dest_TFree o Thm.typ_of o snd) instT), Names.empty)
|> Drule.zero_var_indexes
end
--- a/src/HOL/Tools/choice_specification.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/HOL/Tools/choice_specification.ML Thu Sep 09 12:33:14 2021 +0200
@@ -99,7 +99,7 @@
val frees = map snd props''
val prop = myfoldr HOLogic.mk_conj (map fst props'')
- val (vmap, prop_thawed) = Type.varify_global Term_Subst.TFrees.empty prop
+ val (vmap, prop_thawed) = Type.varify_global TFrees.empty prop
val thawed_prop_consts = collect_consts (prop_thawed, [])
val (altcos, overloaded) = split_list cos
val (names, sconsts) = split_list altcos
@@ -109,7 +109,7 @@
fun proc_const c =
let
- val (_, c') = Type.varify_global Term_Subst.TFrees.empty c
+ val (_, c') = Type.varify_global TFrees.empty c
val (cname,ctyp) = dest_Const c'
in
(case filter (fn t =>
--- a/src/Pure/General/table.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/General/table.ML Thu Sep 09 12:33:14 2021 +0200
@@ -406,7 +406,7 @@
(* simultaneous modifications *)
-fun make entries = fold update_new entries empty;
+fun make entries = build (fold update_new entries);
fun join f (table1, table2) =
let
@@ -437,7 +437,7 @@
modify key (fn NONE => [x] | SOME [] => [x] | SOME (xs as y :: _) =>
if eq (x, y) then raise SAME else Library.update eq x xs);
-fun make_list args = fold_rev cons_list args empty;
+fun make_list args = build (fold_rev cons_list args);
fun dest_list tab = maps (fn (key, xs) => map (pair key) xs) (dest tab);
fun merge_list eq = join (fn _ => Library.merge eq);
@@ -448,7 +448,7 @@
fun insert_set x = default (x, ());
fun remove_set x : set -> set = delete_safe x;
-fun make_set entries = fold insert_set entries empty;
+fun make_set xs = build (fold insert_set xs);
fun subset (A: set, B: set) = forall (defined B o #1) A;
fun eq_set (A: set, B: set) = size A = size B andalso subset (A, B);
--- a/src/Pure/Isar/expression.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/Isar/expression.ML Thu Sep 09 12:33:14 2021 +0200
@@ -191,7 +191,7 @@
|> map_filter (fn (v, T) => if TFree v = T then NONE else SOME (v, T));
val cert_inst =
((map #1 params ~~
- map (Term_Subst.instantiateT_frees (Term_Subst.TFrees.table instT)) parm_types) ~~ insts'')
+ 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));
in
(Element.instantiate_normalize_morphism (map (apsnd certT) instT, cert_inst) $>
--- a/src/Pure/Isar/generic_target.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/Isar/generic_target.ML Thu Sep 09 12:33:14 2021 +0200
@@ -95,10 +95,10 @@
val u = fold_rev lambda term_params rhs';
val global_rhs = singleton (Variable.polymorphic thy_ctxt) u;
- val type_tfrees = Term_Subst.TFrees.build (Term_Subst.add_tfreesT (Term.fastype_of u));
+ val type_tfrees = TFrees.build (TFrees.add_tfreesT (Term.fastype_of u));
val extra_tfrees =
build_rev (u |> (Term.fold_types o Term.fold_atyps)
- (fn TFree v => not (Term_Subst.TFrees.defined type_tfrees v) ? insert (op =) v | _ => I));
+ (fn TFree v => not (TFrees.defined type_tfrees v) ? insert (op =) v | _ => I));
val type_params = map (Logic.mk_type o TFree) extra_tfrees;
in (global_rhs, (extra_tfrees, (type_params, term_params))) end;
@@ -261,11 +261,10 @@
val xs = Variable.add_fixed lthy rhs' [];
val T = Term.fastype_of rhs;
- val type_tfrees =
- Term_Subst.TFrees.build (Term_Subst.add_tfreesT T #> fold (Term_Subst.add_tfreesT o #2) xs);
+ val type_tfrees = TFrees.build (TFrees.add_tfreesT T #> fold (TFrees.add_tfreesT o #2) xs);
val extra_tfrees =
build_rev (rhs |> (Term.fold_types o Term.fold_atyps)
- (fn TFree v => not (Term_Subst.TFrees.defined type_tfrees v) ? insert (op =) v | _ => I));
+ (fn TFree v => not (TFrees.defined type_tfrees v) ? insert (op =) v | _ => I));
val mx' = check_mixfix lthy (b, extra_tfrees) mx;
val type_params = map (Logic.mk_type o TFree) extra_tfrees;
@@ -323,9 +322,9 @@
|>> map Logic.dest_type;
val instT =
- Term_Subst.TVars.build (fold2 (fn a => fn b =>
- (case a of TVar v => Term_Subst.TVars.add (v, b) | _ => I)) tvars tfrees);
- val cinstT = Term_Subst.TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt T)) 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 cinst =
map_filter
(fn (Var (xi, T), t) =>
--- a/src/Pure/Isar/local_defs.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/Isar/local_defs.ML Thu Sep 09 12:33:14 2021 +0200
@@ -90,7 +90,7 @@
fun expand defs =
Drule.implies_intr_list defs
#> Drule.generalize
- (Symtab.empty, fold (Symtab.insert_set o #1 o head_of_def o Thm.term_of) defs Symtab.empty)
+ (Names.empty, Names.build (fold (Names.add_set o #1 o head_of_def o Thm.term_of) defs))
#> funpow (length defs) (fn th => Drule.reflexive_thm RS th);
val expand_term = Envir.expand_term_frees o map (abs_def o Thm.term_of);
--- a/src/Pure/Isar/obtain.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/Isar/obtain.ML Thu Sep 09 12:33:14 2021 +0200
@@ -103,11 +103,9 @@
fun mk_all_internal ctxt (y, z) t =
let
- val frees =
- Term_Subst.Frees.build (t |> Term.fold_aterms
- (fn Free v => Term_Subst.Frees.add (v, ()) | _ => I));
+ val frees = Frees.build (t |> Term.fold_aterms (fn Free v => Frees.add_set v | _ => I));
val T =
- (case Term_Subst.Frees.get_first (fn ((x, T), ()) => if x = z then SOME T else NONE) frees of
+ (case Frees.get_first (fn ((x, T), ()) => if x = z then SOME T else NONE) frees of
SOME T => T
| NONE => the_default dummyT (Variable.default_type ctxt z));
in Logic.all_const T $ Term.lambda_name (y, Free (z, T)) t end;
@@ -328,16 +326,16 @@
val terms = map (Drule.mk_term o Thm.cterm_of ctxt o Free) (xs @ ys');
val instT =
- Term_Subst.TVars.build
+ TVars.build
(params |> fold (#2 #> Term.fold_atyps (fn T => fn instT =>
(case T of
TVar v =>
- if Term_Subst.TVars.defined instT v then instT
- else Term_Subst.TVars.update (v, Thm.ctyp_of ctxt (norm_type T)) instT
+ if TVars.defined instT v then instT
+ else TVars.add (v, Thm.ctyp_of ctxt (norm_type T)) instT
| _ => instT))));
val closed_rule = rule
|> Thm.forall_intr (Thm.cterm_of ctxt (Free thesis_var))
- |> Thm.instantiate (Term_Subst.TVars.dest instT, []);
+ |> Thm.instantiate (TVars.dest instT, []);
val ((_, rule' :: terms'), ctxt') = Variable.import false (closed_rule :: terms) ctxt;
val vars' =
--- a/src/Pure/Isar/specification.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/Isar/specification.ML Thu Sep 09 12:33:14 2021 +0200
@@ -281,7 +281,7 @@
val _ =
Proof_Display.print_consts int (Position.thread_data ()) lthy5
- (Term_Subst.Frees.defined (Term_Subst.Frees.build (Term_Subst.add_frees lhs'))) [(x, T)];
+ (Frees.defined (Frees.build (Frees.add_frees lhs'))) [(x, T)];
in ((lhs, (def_name, th')), lthy5) end;
val definition' = gen_def check_spec_open (K I);
--- a/src/Pure/Isar/subgoal.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/Isar/subgoal.ML Thu Sep 09 12:33:14 2021 +0200
@@ -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 = Term_Subst.Vars.fold (fn (v, t) => cons (v, Thm.cterm_of ctxt3 t)) inst [];
+ val schematic_terms = Vars.fold (fn (v, t) => cons (v, Thm.cterm_of ctxt3 t)) inst [];
- val schematics = (Term_Subst.TVars.dest schematic_types, schematic_terms);
+ val schematics = (TVars.dest 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;
@@ -88,7 +88,7 @@
val ts = map Thm.term_of params;
val prop = Thm.full_prop_of th';
- val concl_vars = Term_Subst.Vars.build (Term_Subst.add_vars (Logic.strip_imp_concl prop));
+ val concl_vars = Vars.build (Vars.add_vars (Logic.strip_imp_concl prop));
val vars = build_rev (Term.add_vars prop);
val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt';
@@ -96,7 +96,7 @@
let
val ((x, i), T) = v;
val (U, args) =
- if Term_Subst.Vars.defined concl_vars v then (T, [])
+ if Vars.defined concl_vars v then (T, [])
else (Ts ---> T, ts);
val u = Free (y, U);
in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end;
--- a/src/Pure/Proof/proof_checker.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/Proof/proof_checker.ML Thu Sep 09 12:33:14 2021 +0200
@@ -77,7 +77,7 @@
fun thm_of_atom thm Ts =
let
val tvars = build_rev (Term.add_tvars (Thm.full_prop_of thm));
- val (fmap, thm') = Thm.varifyT_global' Term_Subst.TFrees.empty thm;
+ val (fmap, thm') = Thm.varifyT_global' TFrees.empty thm;
val ctye =
(tvars @ map (fn ((_, S), ixn) => (ixn, S)) fmap ~~ map (Thm.global_ctyp_of thy) Ts);
in
--- a/src/Pure/Proof/proof_rewrite_rules.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Thu Sep 09 12:33:14 2021 +0200
@@ -291,11 +291,11 @@
fun elim_vars mk_default prf =
let
val prop = Proofterm.prop_of prf;
- val tv = Term_Subst.Vars.build (Term_Subst.add_vars prop);
- val tf = Term_Subst.Frees.build (Term_Subst.add_frees prop);
+ val tv = Vars.build (Vars.add_vars prop);
+ val tf = Frees.build (Frees.add_frees prop);
- fun hidden_variable (Var v) = not (Term_Subst.Vars.defined tv v)
- | hidden_variable (Free f) = not (Term_Subst.Frees.defined tf f)
+ fun hidden_variable (Var v) = not (Vars.defined tv v)
+ | hidden_variable (Free f) = not (Frees.defined tf f)
| hidden_variable _ = false;
fun mk_default' T =
@@ -303,8 +303,8 @@
fun elim_varst (t $ u) = elim_varst t $ elim_varst u
| elim_varst (Abs (s, T, t)) = Abs (s, T, elim_varst t)
- | elim_varst (t as Free (x, T)) = if Term_Subst.Frees.defined tf (x, T) then t else mk_default' T
- | elim_varst (t as Var (xi, T)) = if Term_Subst.Vars.defined tv (xi, T) then t else mk_default' T
+ | elim_varst (t as Free (x, T)) = if Frees.defined tf (x, T) then t else mk_default' T
+ | elim_varst (t as Var (xi, T)) = if Vars.defined tv (xi, T) then t else mk_default' T
| elim_varst t = t;
in
Proofterm.map_proof_terms (fn t =>
--- a/src/Pure/Tools/rule_insts.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/Tools/rule_insts.ML Thu Sep 09 12:33:14 2021 +0200
@@ -53,7 +53,7 @@
error (msg ^ quote (Term.string_of_vname xi) ^ Position.here pos);
fun the_sort tvars (ai, pos) : sort =
- (case Term_Subst.TVars.get_first (fn ((bi, S), ()) => if ai = bi then SOME S else NONE) tvars of
+ (case TVars.get_first (fn ((bi, S), ()) => if ai = bi then SOME S else NONE) tvars of
SOME S => S
| NONE => error_var "No such type variable in theorem: " (ai, pos));
@@ -71,14 +71,14 @@
else error_var "Bad sort for instantiation of type variable: " (xi, pos)
end;
-fun make_instT f (tvars: Term_Subst.TVars.set) =
+fun make_instT f (tvars: TVars.set) =
let
fun add v =
let
val T = TVar v;
val T' = f T;
in if T = T' then I else cons (v, T') end;
- in Term_Subst.TVars.fold (add o #1) tvars [] end;
+ in TVars.fold (add o #1) tvars [] end;
fun make_inst f vars =
let
@@ -115,20 +115,20 @@
val (type_insts, term_insts) =
List.partition (fn (((x, _), _), _) => String.isPrefix "'" x) raw_insts;
- val tvars = Term_Subst.TVars.build (Thm.fold_terms {hyps = false} Term_Subst.add_tvars thm);
- val vars = Term_Subst.Vars.build (Thm.fold_terms {hyps = false} Term_Subst.add_vars thm);
+ val tvars = TVars.build (Thm.fold_terms {hyps = false} TVars.add_tvars thm);
+ val vars = Vars.build (Thm.fold_terms {hyps = false} Vars.add_vars thm);
(*eigen-context*)
val (_, ctxt1) = ctxt
- |> Term_Subst.TVars.fold (Variable.declare_internal o Logic.mk_type o TVar o #1) tvars
- |> Term_Subst.Vars.fold (Variable.declare_internal o Var o #1) vars
+ |> TVars.fold (Variable.declare_internal o Logic.mk_type o TVar o #1) tvars
+ |> Vars.fold (Variable.declare_internal o Var o #1) vars
|> Proof_Context.add_fixes_cmd raw_fixes;
(*explicit type instantiations*)
val instT1 =
- Term_Subst.instantiateT (Term_Subst.TVars.table (map (read_type ctxt1 tvars) type_insts));
+ Term_Subst.instantiateT (TVars.make (map (read_type ctxt1 tvars) type_insts));
val vars1 =
- Vartab.build (vars |> Term_Subst.Vars.fold (fn ((v, T), ()) =>
+ Vartab.build (vars |> Vars.fold (fn ((v, T), ()) =>
Vartab.insert (K true) (v, instT1 T)));
(*term instantiations*)
@@ -137,12 +137,11 @@
val ((ts, inferred), ctxt2) = read_terms ss Ts ctxt1;
(*implicit type instantiations*)
- val instT2 = Term_Subst.instantiateT (Term_Subst.TVars.table inferred);
+ val instT2 = Term_Subst.instantiateT (TVars.make inferred);
val vars2 = Vartab.fold (fn (v, T) => cons (v, instT2 T)) vars1 [];
val inst2 =
- Term_Subst.instantiate (Term_Subst.TVars.empty,
- Term_Subst.Vars.build
- (fold2 (fn (xi, _) => fn t => Term_Subst.Vars.add ((xi, Term.fastype_of t), t)) xs ts))
+ Term_Subst.instantiate (TVars.empty,
+ Vars.build (fold2 (fn (xi, _) => fn t => Vars.add ((xi, Term.fastype_of t), t)) xs ts))
#> Envir.beta_norm;
val inst_tvars = make_instT (instT2 o instT1) tvars;
--- a/src/Pure/consts.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/consts.ML Thu Sep 09 12:33:14 2021 +0200
@@ -227,9 +227,8 @@
val declT = type_scheme consts c;
val args = typargs consts (c, declT);
val inst =
- Term_Subst.TVars.build
- (fold2 (fn a => fn T => Term_Subst.TVars.add (Term.dest_TVar a, T)) args Ts)
- handle ListPair.UnequalLengths => raise TYPE ("Consts.instance", Ts, [Const (c, dummyT)]);
+ TVars.build (fold2 (fn a => fn T => TVars.add (Term.dest_TVar a, T)) args Ts)
+ handle ListPair.UnequalLengths => raise TYPE ("Consts.instance", Ts, [Const (c, dummyT)]);
in declT |> Term_Subst.instantiateT inst end;
fun dummy_types consts =
--- a/src/Pure/drule.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/drule.ML Thu Sep 09 12:33:14 2021 +0200
@@ -51,7 +51,7 @@
sig
include BASIC_DRULE
val outer_params: term -> (string * typ) list
- val generalize: Symtab.set * Symtab.set -> thm -> thm
+ val generalize: Names.set * Names.set -> thm -> thm
val list_comb: cterm * cterm list -> cterm
val strip_comb: cterm -> cterm * cterm list
val beta_conv: cterm -> cterm -> cterm
@@ -179,18 +179,18 @@
|> map (fn (x, T) => Var ((x, maxidx + 1), Logic.incr_tvar (maxidx + 1) T));
val Ts = map Term.fastype_of ps;
val inst =
- Term_Subst.Vars.build (th |> (Thm.fold_terms {hyps = false} o Term.fold_aterms)
+ Vars.build (th |> (Thm.fold_terms {hyps = false} o Term.fold_aterms)
(fn t => fn inst =>
(case t of
Var (xi, T) =>
- if Term_Subst.Vars.defined inst (xi, T) then inst
+ if Vars.defined inst (xi, T) then inst
else
let val ct = Thm.cterm_of ctxt (Term.list_comb (Var (xi, Ts ---> T), ps))
- in Term_Subst.Vars.update ((xi, T), ct) inst end
+ in Vars.add ((xi, T), ct) inst end
| _ => inst)));
in
th
- |> Thm.instantiate ([], Term_Subst.Vars.dest inst)
+ |> Thm.instantiate ([], Vars.dest inst)
|> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt) ps
end;
@@ -213,16 +213,16 @@
val (instT, inst) =
Term_Subst.zero_var_indexes_inst Name.context (map Thm.full_prop_of ths);
- val tvars = fold Thm.add_tvars ths Term_Subst.TVars.empty;
- val the_tvar = the o Term_Subst.TVars.lookup tvars;
+ val tvars = TVars.build (fold Thm.add_tvars ths);
+ val the_tvar = the o TVars.lookup tvars;
val instT' =
- build (instT |> Term_Subst.TVars.fold (fn (v, TVar (b, _)) =>
+ build (instT |> TVars.fold (fn (v, TVar (b, _)) =>
cons (v, Thm.rename_tvar b (the_tvar v))));
- val vars = fold (Thm.add_vars o Thm.instantiate (instT', [])) ths Term_Subst.Vars.empty;
- val the_var = the o Term_Subst.Vars.lookup vars;
+ val vars = Vars.build (fold (Thm.add_vars o Thm.instantiate (instT', [])) ths);
+ val the_var = the o Vars.lookup vars;
val inst' =
- build (inst |> Term_Subst.Vars.fold (fn (v, Var (b, _)) =>
+ build (inst |> Vars.fold (fn (v, Var (b, _)) =>
cons (v, Thm.var (b, Thm.ctyp_of_cterm (the_var v)))));
in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate (instT', inst')) ths end;
--- a/src/Pure/goal.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/goal.ML Thu Sep 09 12:33:14 2021 +0200
@@ -116,18 +116,18 @@
val assms = Assumption.all_assms_of ctxt;
val As = map Thm.term_of assms;
- val frees = Term_Subst.Frees.build (fold Term_Subst.add_frees (prop :: As));
- val xs = Term_Subst.Frees.fold_rev (cons o Thm.cterm_of ctxt o Free o #1) frees [];
+ val frees = Frees.build (fold Frees.add_frees (prop :: As));
+ val xs = Frees.fold_rev (cons o Thm.cterm_of ctxt o Free o #1) frees [];
- val tfrees = Term_Subst.TFrees.build (fold Term_Subst.add_tfrees (prop :: As));
- val Ts = Symtab.build (Term_Subst.TFrees.fold (Symtab.insert_set o #1 o #1) tfrees);
+ 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 |> Term_Subst.TFrees.fold (fn ((a, S), ()) =>
+ build (tfrees |> TFrees.fold (fn ((a, S), ()) =>
cons (((a, 0), S), Thm.ctyp_of ctxt (TFree (a, S)))));
val global_prop =
Logic.list_implies (As, prop)
- |> Term_Subst.Frees.fold_rev (Logic.all o Free o #1) frees
+ |> Frees.fold_rev (Logic.all o Free o #1) frees
|> Logic.varify_types_global
|> Thm.cterm_of ctxt
|> Thm.weaken_sorts' ctxt;
@@ -136,7 +136,7 @@
Drule.implies_intr_list assms #>
Drule.forall_intr_list xs #>
Thm.adjust_maxidx_thm ~1 #>
- Thm.generalize (Ts, Symtab.empty) 0 #>
+ Thm.generalize (Ts, Names.empty) 0 #>
Thm.strip_shyps #>
Thm.solve_constraints);
val local_result =
--- a/src/Pure/more_thm.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/more_thm.ML Thu Sep 09 12:33:14 2021 +0200
@@ -25,8 +25,8 @@
structure Thmtab: TABLE
val eq_ctyp: ctyp * ctyp -> bool
val aconvc: cterm * cterm -> bool
- val add_tvars: thm -> ctyp Term_Subst.TVars.table -> ctyp Term_Subst.TVars.table
- val add_vars: thm -> cterm Term_Subst.Vars.table -> cterm Term_Subst.Vars.table
+ val add_tvars: thm -> ctyp TVars.table -> ctyp TVars.table
+ val add_vars: thm -> cterm Vars.table -> cterm Vars.table
val dest_funT: ctyp -> ctyp * ctyp
val strip_type: ctyp -> ctyp list * ctyp
val all_name: Proof.context -> string * cterm -> cterm -> cterm
@@ -140,12 +140,12 @@
val add_tvars =
Thm.fold_atomic_ctyps {hyps = false} Term.is_TVar (fn cT => fn tab =>
let val v = Term.dest_TVar (Thm.typ_of cT)
- in tab |> not (Term_Subst.TVars.defined tab v) ? Term_Subst.TVars.update (v, cT) end);
+ in tab |> not (TVars.defined tab v) ? TVars.add (v, cT) end);
val add_vars =
Thm.fold_atomic_cterms {hyps = false} Term.is_Var (fn ct => fn tab =>
let val v = Term.dest_Var (Thm.term_of ct)
- in tab |> not (Term_Subst.Vars.defined tab v) ? Term_Subst.Vars.update (v, ct) end);
+ in tab |> not (Vars.defined tab v) ? Vars.add (v, ct) end);
(* ctyp operations *)
@@ -414,8 +414,8 @@
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 = Symtab.build (fold (Symtab.insert_set o #1 o #1) instT);
- val frees = Symtab.build (fold (Symtab.insert_set o #1 o #1) 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);
val hyps = Thm.chyps_of th;
val inst_cterm =
@@ -454,11 +454,11 @@
fun forall_intr_vars th =
let
val (_, vars) =
- (th, (Term_Subst.Vars.empty, [])) |-> Thm.fold_atomic_cterms {hyps = false} Term.is_Var
+ (th, (Vars.empty, [])) |-> Thm.fold_atomic_cterms {hyps = false} Term.is_Var
(fn ct => fn (seen, vars) =>
let val v = Term.dest_Var (Thm.term_of ct) in
- if not (Term_Subst.Vars.defined seen v)
- then (Term_Subst.Vars.add (v, ()) seen, ct :: vars)
+ if not (Vars.defined seen v)
+ then (Vars.add_set v seen, ct :: vars)
else (seen, vars)
end);
in fold Thm.forall_intr vars th end;
@@ -466,15 +466,15 @@
fun forall_intr_frees th =
let
val fixed =
- Term_Subst.Frees.build
- (fold Term_Subst.add_frees (Thm.terms_of_tpairs (Thm.tpairs_of th)) #>
- fold Term_Subst.add_frees (Thm.hyps_of th));
+ Frees.build
+ (fold Frees.add_frees (Thm.terms_of_tpairs (Thm.tpairs_of th)) #>
+ fold Frees.add_frees (Thm.hyps_of th));
val (_, frees) =
(th, (fixed, [])) |-> Thm.fold_atomic_cterms {hyps = false} Term.is_Free
(fn ct => fn (seen, frees) =>
let val v = Term.dest_Free (Thm.term_of ct) in
- if not (Term_Subst.Frees.defined seen v)
- then (Term_Subst.Frees.add (v, ()) seen, ct :: frees)
+ if not (Frees.defined seen v)
+ then (Frees.add_set v seen, ct :: frees)
else (seen, frees)
end);
in fold Thm.forall_intr frees th end;
@@ -492,23 +492,23 @@
val certT = Thm.global_ctyp_of thy;
val instT =
- Term_Subst.TVars.build (prop |> (Term.fold_types o Term.fold_atyps)
+ TVars.build (prop |> (Term.fold_types o Term.fold_atyps)
(fn T => fn instT =>
(case T of
TVar (v as ((a, _), S)) =>
- if Term_Subst.TVars.defined instT v then instT
- else Term_Subst.TVars.update (v, TFree (a, S)) instT
+ if TVars.defined instT v then instT
+ else TVars.add (v, TFree (a, S)) instT
| _ => instT)));
- val cinstT = Term_Subst.TVars.map (K certT) instT;
+ val cinstT = TVars.map (K certT) instT;
val cinst =
- Term_Subst.Vars.build (prop |> Term.fold_aterms
+ Vars.build (prop |> Term.fold_aterms
(fn t => fn inst =>
(case t of
Var ((x, i), T) =>
let val T' = Term_Subst.instantiateT instT T
- in Term_Subst.Vars.update (((x, i), T'), cert (Free ((x, T')))) inst end
+ in Vars.add (((x, i), T'), cert (Free ((x, T')))) inst end
| _ => inst)));
- in Thm.instantiate (Term_Subst.TVars.dest cinstT, Term_Subst.Vars.dest cinst) th end;
+ in Thm.instantiate (TVars.dest cinstT, Vars.dest cinst) th end;
fun unvarify_axiom thy = unvarify_global thy o Thm.axiom thy;
--- a/src/Pure/morphism.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/morphism.ML Thu Sep 09 12:33:14 2021 +0200
@@ -137,17 +137,13 @@
fun instantiate_frees_morphism ([], []) = identity
| instantiate_frees_morphism (cinstT, cinst) =
let
- val instT =
- Term_Subst.TFrees.build
- (cinstT |> fold (fn (v, cT) => Term_Subst.TFrees.add (v, Thm.typ_of cT)));
- val inst =
- Term_Subst.Frees.build
- (cinst |> fold (fn (v, ct) => Term_Subst.Frees.add (v, Thm.term_of ct)));
+ 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 Term_Subst.TFrees.is_empty instT then []
+ 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))]}
@@ -156,17 +152,13 @@
fun instantiate_morphism ([], []) = identity
| instantiate_morphism (cinstT, cinst) =
let
- val instT =
- Term_Subst.TVars.build (cinstT |> fold (fn (v, cT) =>
- Term_Subst.TVars.add (v, Thm.typ_of cT)));
- val inst =
- Term_Subst.Vars.build (cinst |> fold (fn (v, ct) =>
- Term_Subst.Vars.add (v, Thm.term_of ct)));
+ 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 Term_Subst.TVars.is_empty instT then []
+ if TVars.is_empty instT then []
else [Term_Subst.instantiateT instT],
term = [Term_Subst.instantiate (instT, inst)],
fact = [map (Thm.instantiate (cinstT, cinst))]}
--- a/src/Pure/primitive_defs.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/primitive_defs.ML Thu Sep 09 12:33:14 2021 +0200
@@ -37,7 +37,7 @@
val (raw_lhs, rhs) = Logic.dest_equals eq_body handle TERM _ => err "Not a meta-equality (\<equiv>)";
val lhs = Envir.beta_eta_contract raw_lhs;
val (head, args) = Term.strip_comb lhs;
- val head_tfrees = Term_Subst.TFrees.build (Term_Subst.add_tfrees head);
+ val head_tfrees = TFrees.build (TFrees.add_tfrees head);
fun check_arg (Bound _) = true
| check_arg (Free (x, _)) = check_free_lhs x
@@ -52,7 +52,7 @@
if check_free_rhs x orelse member (op aconv) args v then I
else insert (op aconv) v | _ => I) rhs [];
val rhs_extrasT = Term.fold_aterms (Term.fold_types (fn v as TFree (a, S) =>
- if check_tfree a orelse Term_Subst.TFrees.defined head_tfrees (a, S) then I
+ if check_tfree a orelse TFrees.defined head_tfrees (a, S) then I
else insert (op =) v | _ => I)) rhs [];
in
if not (check_head head) then
--- a/src/Pure/proofterm.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/proofterm.ML Thu Sep 09 12:33:14 2021 +0200
@@ -109,12 +109,12 @@
val implies_intr_proof': term -> proof -> proof
val forall_intr_proof: string * term -> typ option -> proof -> proof
val forall_intr_proof': term -> proof -> proof
- val varify_proof: term -> Term_Subst.TFrees.set -> proof -> proof
+ val varify_proof: term -> TFrees.set -> proof -> proof
val legacy_freezeT: term -> proof -> proof
val rotate_proof: term list -> term -> (string * typ) list -> term list -> int -> proof -> proof
val permute_prems_proof: term list -> int -> int -> proof -> proof
- val generalize_proof: Symtab.set * Symtab.set -> int -> term -> proof -> proof
- val instantiate: typ Term_Subst.TVars.table * term Term_Subst.Vars.table -> proof -> proof
+ val generalize_proof: Names.set * Names.set -> int -> term -> proof -> proof
+ val instantiate: typ TVars.table * term Vars.table -> proof -> proof
val lift_proof: term -> int -> term -> proof -> proof
val incr_indexes: int -> proof -> proof
val assumption_proof: term list -> term -> int -> proof -> proof
@@ -678,8 +678,8 @@
(fn T => fn instT =>
(case T of
TVar (v as (_, S)) =>
- if Term_Subst.TVars.defined instT v orelse can (Type.lookup envT) v then instT
- else Term_Subst.TVars.update (v, Logic.dummy_tfree S) instT
+ if TVars.defined instT v orelse can (Type.lookup envT) v then instT
+ else TVars.add (v, Logic.dummy_tfree S) instT
| _ => instT));
fun conflicting_tvars env =
@@ -687,18 +687,18 @@
(fn t => fn inst =>
(case t of
Var (v as (_, T)) =>
- if Term_Subst.Vars.defined inst v orelse can (Envir.lookup env) v then inst
- else Term_Subst.Vars.update (v, Free ("dummy", T)) inst
+ if Vars.defined inst v orelse can (Envir.lookup env) v then inst
+ else Vars.add (v, Free ("dummy", T)) inst
| _ => inst));
fun del_conflicting_tvars envT ty =
- Term_Subst.instantiateT (Term_Subst.TVars.build (conflicting_tvarsT envT ty)) ty;
+ Term_Subst.instantiateT (TVars.build (conflicting_tvarsT envT ty)) ty;
fun del_conflicting_vars env tm =
let
val instT =
- Term_Subst.TVars.build (tm |> Term.fold_types (conflicting_tvarsT (Envir.type_env env)));
- val inst = Term_Subst.Vars.build (tm |> conflicting_tvars env);
+ TVars.build (tm |> Term.fold_types (conflicting_tvarsT (Envir.type_env env)));
+ val inst = Vars.build (tm |> conflicting_tvars env);
in Term_Subst.instantiate (instT, inst) tm end;
in
@@ -903,7 +903,7 @@
let
val fs =
build (t |> (Term.fold_types o Term.fold_atyps)
- (fn TFree v => if Term_Subst.TFrees.defined fixed v then I else insert (op =) v | _ => I));
+ (fn TFree v => if TFrees.defined fixed v then I else insert (op =) v | _ => I));
val used = Name.context
|> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t;
val fmap = fs ~~ #1 (fold_map Name.variant (map fst fs) used);
@@ -970,14 +970,14 @@
fun generalize_proof (tfrees, frees) idx prop prf =
let
val gen =
- if Symtab.is_empty frees then []
+ if Names.is_empty frees then []
else
- fold_aterms (fn Free (x, T) => Symtab.defined frees x ? insert (op =) (x, T) | _ => I)
- (Term_Subst.generalize (tfrees, Symtab.empty) idx prop) [];
+ fold_aterms (fn Free (x, T) => Names.defined frees x ? insert (op =) (x, T) | _ => I)
+ (Term_Subst.generalize (tfrees, Names.empty) idx prop) [];
in
prf
|> Same.commit (map_proof_terms_same
- (Term_Subst.generalize_same (tfrees, Symtab.empty) idx)
+ (Term_Subst.generalize_same (tfrees, Names.empty) idx)
(Term_Subst.generalizeT_same tfrees idx))
|> fold (fn (x, T) => forall_intr_proof (x, Free (x, T)) NONE) gen
|> fold_rev (fn (x, T) => fn prf' => prf' %> Var (Name.clean_index (x, idx), T)) gen
@@ -988,7 +988,7 @@
fun instantiate (instT, inst) =
Same.commit (map_proof_terms_same
- (Term_Subst.instantiate_same (instT, Term_Subst.Vars.map (K remove_types) inst))
+ (Term_Subst.instantiate_same (instT, Vars.map (K remove_types) inst))
(Term_Subst.instantiateT_same instT));
--- a/src/Pure/raw_simplifier.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/raw_simplifier.ML Thu Sep 09 12:33:14 2021 +0200
@@ -161,13 +161,13 @@
fun rewrite_rule_extra_vars prems elhs erhs =
let
val elhss = elhs :: prems;
- val tvars = Term_Subst.TVars.build (fold Term_Subst.add_tvars elhss);
- val vars = Term_Subst.Vars.build (fold Term_Subst.add_vars elhss);
+ val tvars = TVars.build (fold TVars.add_tvars elhss);
+ val vars = Vars.build (fold Vars.add_vars elhss);
in
erhs |> Term.exists_type (Term.exists_subtype
- (fn TVar v => not (Term_Subst.TVars.defined tvars v) | _ => false)) orelse
+ (fn TVar v => not (TVars.defined tvars v) | _ => false)) orelse
erhs |> Term.exists_subterm
- (fn Var v => not (Term_Subst.Vars.defined vars v) | _ => false)
+ (fn Var v => not (Vars.defined vars v) | _ => false)
end;
fun rrule_extra_vars elhs thm =
@@ -474,7 +474,7 @@
(cond_warning ctxt (fn () => print_thm ctxt "Ignoring duplicate rewrite rule:" ("", thm));
ctxt));
-val vars_set = Term_Subst.Vars.build o Term_Subst.add_vars;
+val vars_set = Vars.build o Vars.add_vars;
local
@@ -483,7 +483,7 @@
| vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
| vperm (t, u) = (t = u);
-fun var_perm (t, u) = vperm (t, u) andalso Term_Subst.Vars.eq_set (apply2 vars_set (t, u));
+fun var_perm (t, u) = vperm (t, u) andalso Vars.eq_set (apply2 vars_set (t, u));
in
@@ -946,7 +946,7 @@
while the premises are solved.*)
fun cond_skel (args as (_, (lhs, rhs))) =
- if Term_Subst.Vars.subset (vars_set rhs, vars_set lhs) then uncond_skel args
+ if Vars.subset (vars_set rhs, vars_set lhs) then uncond_skel args
else skel0;
(*
--- a/src/Pure/term_ord.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/term_ord.ML Thu Sep 09 12:33:14 2021 +0200
@@ -5,6 +5,70 @@
Term orderings and scalable collections.
*)
+signature ITEMS =
+sig
+ type key
+ type 'a table
+ val empty: 'a table
+ val build: ('a table -> 'a table) -> 'a table
+ val is_empty: 'a table -> bool
+ val map: (key -> 'a -> 'b) -> 'a table -> 'b table
+ val fold: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
+ val fold_rev: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
+ val size: 'a table -> int
+ val dest: 'a table -> (key * 'a) list
+ val keys: 'a table -> key list
+ val exists: (key * 'a -> bool) -> 'a table -> bool
+ val forall: (key * 'a -> bool) -> 'a table -> bool
+ val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option
+ val lookup: 'a table -> key -> 'a option
+ val defined: 'a table -> key -> bool
+ val add: key * 'a -> 'a table -> 'a table
+ val make: (key * 'a) list -> 'a table
+ type set = unit table
+ val add_set: key -> set -> set
+ val make_set: key list -> set
+ val subset: set * set -> bool
+ val eq_set: set * set -> bool
+end;
+
+functor Items(Key: KEY): ITEMS =
+struct
+
+structure Table = Table(Key);
+
+type key = Table.key;
+type 'a table = 'a Table.table;
+
+val empty = Table.empty;
+val build = Table.build;
+val is_empty = Table.is_empty;
+val size = Table.size;
+val dest = Table.dest;
+val keys = Table.keys;
+val exists = Table.exists;
+val forall = Table.forall;
+val get_first = Table.get_first;
+val lookup = Table.lookup;
+val defined = Table.defined;
+
+fun add entry = Table.insert (K true) entry;
+fun make entries = Table.build (fold add entries);
+
+type set = unit table;
+
+fun add_set x = add (x, ());
+fun make_set xs = build (fold add_set xs);
+
+fun subset (A: set, B: set) = forall (defined B o #1) A;
+fun eq_set (A: set, B: set) = size A = size B andalso subset (A, B);
+
+val map = Table.map;
+val fold = Table.fold;
+val fold_rev = Table.fold_rev;
+
+end;
+
signature BASIC_TERM_ORD =
sig
structure Vartab: TABLE
@@ -15,6 +79,35 @@
structure Sort_Graph: GRAPH
structure Typ_Graph: GRAPH
structure Term_Graph: GRAPH
+ structure TFrees:
+ sig
+ include ITEMS
+ val add_tfreesT: typ -> set -> set
+ val add_tfrees: term -> set -> set
+ end
+ structure TVars:
+ sig
+ include ITEMS
+ val add_tvarsT: typ -> set -> set
+ val add_tvars: term -> set -> set
+ end
+ structure Frees:
+ sig
+ include ITEMS
+ val add_frees: term -> set -> set
+ end
+ structure Vars:
+ sig
+ include ITEMS
+ val add_vars: term -> set -> set
+ end
+ structure Names:
+ sig
+ include ITEMS
+ val add_tfree_namesT: typ -> set -> set
+ val add_tfree_names: term -> set -> set
+ val add_free_names: term -> set -> set
+ end
end;
signature TERM_ORD =
@@ -221,12 +314,55 @@
structure Typtab = Table(type key = typ val ord = typ_ord);
structure Termtab = Table(type key = term val ord = fast_term_ord);
+fun term_cache f = Cache.create Termtab.empty Termtab.lookup Termtab.update f;
+
structure Var_Graph = Graph(type key = indexname val ord = fast_indexname_ord);
structure Sort_Graph = Graph(type key = sort val ord = sort_ord);
structure Typ_Graph = Graph(type key = typ val ord = typ_ord);
structure Term_Graph = Graph(type key = term val ord = fast_term_ord);
-fun term_cache f = Cache.create Termtab.empty Termtab.lookup Termtab.update f;
+structure TFrees =
+struct
+ structure Items =
+ Items(type key = string * sort val ord = pointer_eq_ord (prod_ord fast_string_ord sort_ord));
+ open Items;
+ val add_tfreesT = fold_atyps (fn TFree v => add_set v | _ => I);
+ val add_tfrees = fold_types add_tfreesT;
+end;
+
+structure TVars =
+struct
+ structure Items =
+ Items(type key = indexname * sort val ord = pointer_eq_ord (prod_ord fast_indexname_ord sort_ord));
+ open Items;
+ val add_tvarsT = fold_atyps (fn TVar v => add_set v | _ => I);
+ val add_tvars = fold_types add_tvarsT;
+end;
+
+structure Frees =
+struct
+ structure Items =
+ Items(type key = string * typ val ord = pointer_eq_ord (prod_ord fast_string_ord typ_ord));
+ open Items;
+ val add_frees = fold_aterms (fn Free v => add_set v | _ => I);
+end;
+
+structure Vars =
+struct
+ structure Items =
+ Items(type key = indexname * typ val ord = pointer_eq_ord (prod_ord fast_indexname_ord typ_ord));
+ open Items;
+ val add_vars = fold_aterms (fn Var v => add_set v | _ => I);
+end;
+
+structure Names =
+struct
+ structure Items = Items(type key = string val ord = fast_string_ord);
+ open Items;
+ val add_tfree_namesT = fold_atyps (fn TFree (a, _) => add_set a | _ => I);
+ val add_tfree_names = fold_types add_tfree_namesT;
+ val add_free_names = fold_aterms (fn Free (x, _) => add_set x | _ => I);
+end;
end;
--- a/src/Pure/term_subst.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/term_subst.ML Thu Sep 09 12:33:14 2021 +0200
@@ -4,47 +4,15 @@
Efficient type/term substitution.
*)
-signature INST_TABLE =
-sig
- include TABLE
- val add: key * 'a -> 'a table -> 'a table
- val table: (key * 'a) list -> 'a table
-end;
-
-functor Inst_Table(Key: KEY): INST_TABLE =
-struct
-
-structure Tab = Table(Key);
-
-fun add entry = Tab.insert (K true) entry;
-fun table entries = Tab.build (fold add entries);
-
-open Tab;
-
-end;
-
signature TERM_SUBST =
sig
- structure TFrees: INST_TABLE
- structure TVars: INST_TABLE
- structure Frees: INST_TABLE
- structure Vars: INST_TABLE
- val add_tfreesT: typ -> TFrees.set -> TFrees.set
- val add_tfrees: term -> TFrees.set -> TFrees.set
- val add_tvarsT: typ -> TVars.set -> TVars.set
- val add_tvars: term -> TVars.set -> TVars.set
- val add_frees: term -> Frees.set -> Frees.set
- val add_vars: term -> Vars.set -> Vars.set
- val add_tfree_namesT: typ -> Symtab.set -> Symtab.set
- val add_tfree_names: term -> Symtab.set -> Symtab.set
- val add_free_names: term -> Symtab.set -> Symtab.set
val map_atypsT_same: typ Same.operation -> typ Same.operation
val map_types_same: typ Same.operation -> term Same.operation
val map_aterms_same: term Same.operation -> term Same.operation
- val generalizeT_same: Symtab.set -> int -> typ Same.operation
- val generalize_same: Symtab.set * Symtab.set -> int -> term Same.operation
- val generalizeT: Symtab.set -> int -> typ -> typ
- val generalize: Symtab.set * Symtab.set -> int -> term -> term
+ val generalizeT_same: Names.set -> int -> typ Same.operation
+ val generalize_same: Names.set * Names.set -> int -> term Same.operation
+ val generalizeT: Names.set -> int -> typ -> typ
+ val generalize: Names.set * Names.set -> int -> term -> term
val instantiateT_maxidx: (typ * int) TVars.table -> typ -> int -> typ * int
val instantiate_maxidx: (typ * int) TVars.table * (term * int) Vars.table ->
term -> int -> term * int
@@ -64,39 +32,6 @@
structure Term_Subst: TERM_SUBST =
struct
-(* instantiation as table *)
-
-structure TFrees = Inst_Table(
- type key = string * sort
- val ord = pointer_eq_ord (prod_ord fast_string_ord Term_Ord.sort_ord)
-);
-
-structure TVars = Inst_Table(
- type key = indexname * sort
- val ord = pointer_eq_ord (prod_ord Term_Ord.fast_indexname_ord Term_Ord.sort_ord)
-);
-
-structure Frees = Inst_Table(
- type key = string * typ
- val ord = pointer_eq_ord (prod_ord fast_string_ord Term_Ord.typ_ord)
-);
-
-structure Vars = Inst_Table(
- type key = indexname * typ
- val ord = pointer_eq_ord (prod_ord Term_Ord.fast_indexname_ord Term_Ord.typ_ord)
-);
-
-val add_tfreesT = fold_atyps (fn TFree v => TFrees.add (v, ()) | _ => I);
-val add_tfrees = fold_types add_tfreesT;
-val add_tvarsT = fold_atyps (fn TVar v => TVars.add (v, ()) | _ => I);
-val add_tvars = fold_types add_tvarsT;
-val add_frees = fold_aterms (fn Free v => Frees.add (v, ()) | _ => I);
-val add_vars = fold_aterms (fn Var v => Vars.add (v, ()) | _ => I);
-val add_tfree_namesT = fold_atyps (fn TFree (a, _) => Symtab.insert_set a | _ => I);
-val add_tfree_names = fold_types add_tfree_namesT;
-val add_free_names = fold_aterms (fn Free (x, _) => Symtab.insert_set x | _ => I);
-
-
(* generic mapping *)
fun map_atypsT_same f =
@@ -128,23 +63,23 @@
(* generalization of fixed variables *)
fun generalizeT_same tfrees idx ty =
- if Symtab.is_empty tfrees then raise Same.SAME
+ if Names.is_empty tfrees then raise Same.SAME
else
let
fun gen (Type (a, Ts)) = Type (a, Same.map gen Ts)
| gen (TFree (a, S)) =
- if Symtab.defined tfrees a then TVar ((a, idx), S)
+ if Names.defined tfrees a then TVar ((a, idx), S)
else raise Same.SAME
| gen _ = raise Same.SAME;
in gen ty end;
fun generalize_same (tfrees, frees) idx tm =
- if Symtab.is_empty tfrees andalso Symtab.is_empty frees then raise Same.SAME
+ if Names.is_empty tfrees andalso Names.is_empty frees then raise Same.SAME
else
let
val genT = generalizeT_same tfrees idx;
fun gen (Free (x, T)) =
- if Symtab.defined frees x then
+ if Names.defined frees x then
Var (Name.clean_index (x, idx), Same.commit genT T)
else Free (x, genT T)
| gen (Var (xi, T)) = Var (xi, genT T)
--- a/src/Pure/theory.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/theory.ML Thu Sep 09 12:33:14 2021 +0200
@@ -244,10 +244,10 @@
[] => (item, map Logic.varifyT_global args)
| vs => raise TYPE ("Illegal schematic type variable(s)", map TVar vs, []));
- val lhs_vars = Term_Subst.TFrees.build (snd lhs |> fold Term_Subst.add_tfreesT);
+ val lhs_vars = TFrees.build (snd lhs |> fold TFrees.add_tfreesT);
val rhs_extras =
build (rhs |> fold (#2 #> (fold o Term.fold_atyps)
- (fn TFree v => not (Term_Subst.TFrees.defined lhs_vars v) ? insert (op =) v | _ => I)));
+ (fn TFree v => not (TFrees.defined lhs_vars v) ? insert (op =) v | _ => I)));
val _ =
if null rhs_extras then ()
else error ("Specification depends on extra type variables: " ^
--- a/src/Pure/thm.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/thm.ML Thu Sep 09 12:33:14 2021 +0200
@@ -151,9 +151,9 @@
val equal_elim: thm -> thm -> thm
val solve_constraints: thm -> thm
val flexflex_rule: Proof.context option -> thm -> thm Seq.seq
- val generalize: Symtab.set * Symtab.set -> int -> thm -> thm
- val generalize_cterm: Symtab.set * Symtab.set -> int -> cterm -> cterm
- val generalize_ctyp: Symtab.set -> int -> ctyp -> ctyp
+ 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 ->
@@ -161,7 +161,7 @@
val trivial: cterm -> thm
val of_class: ctyp * class -> thm
val unconstrainT: thm -> thm
- val varifyT_global': Term_Subst.TFrees.set -> thm -> ((string * sort) * indexname) list * thm
+ val varifyT_global': TFrees.set -> thm -> ((string * sort) * indexname) list * thm
val varifyT_global: thm -> thm
val legacy_freezeT: thm -> thm
val plain_prop_of: thm -> term
@@ -1547,16 +1547,16 @@
*)
fun generalize (tfrees, frees) idx th =
- if Symtab.is_empty tfrees andalso Symtab.is_empty frees then th
+ if Names.is_empty tfrees andalso Names.is_empty frees then th
else
let
val Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = th;
val _ = idx <= maxidx andalso raise THM ("generalize: bad index", idx, [th]);
val bad_type =
- if Symtab.is_empty tfrees then K false
- else Term.exists_subtype (fn TFree (a, _) => Symtab.defined tfrees a | _ => false);
- fun bad_term (Free (x, T)) = bad_type T orelse Symtab.defined frees x
+ if Names.is_empty tfrees then K false
+ else Term.exists_subtype (fn TFree (a, _) => Names.defined tfrees a | _ => false);
+ fun bad_term (Free (x, T)) = bad_type T orelse Names.defined frees x
| bad_term (Var (_, T)) = bad_type T
| bad_term (Const (_, T)) = bad_type T
| bad_term (Abs (_, T, t)) = bad_type T orelse bad_term t
@@ -1582,7 +1582,7 @@
end;
fun generalize_cterm (tfrees, frees) idx (ct as Cterm {cert, t, T, maxidx, sorts}) =
- if Symtab.is_empty tfrees andalso Symtab.is_empty frees then ct
+ if Names.is_empty tfrees andalso Names.is_empty frees then ct
else if idx <= maxidx then raise CTERM ("generalize_cterm: bad index", [ct])
else
Cterm {cert = cert, sorts = sorts,
@@ -1591,7 +1591,7 @@
maxidx = Int.max (maxidx, idx)};
fun generalize_ctyp tfrees idx (cT as Ctyp {cert, T, maxidx, sorts}) =
- if Symtab.is_empty tfrees then cT
+ if Names.is_empty tfrees then cT
else if idx <= maxidx then raise CTERM ("generalize_ctyp: bad index", [])
else
Ctyp {cert = cert, sorts = sorts,
@@ -1616,11 +1616,11 @@
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 Term_Subst.TVars.add (v, (U, maxidx))
+ if Sign.of_sort thy (U, S) then TVars.add (v, (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 Term_Subst.Vars.add (v, (u, maxidx))
+ if T = U then Vars.add (v, (u, maxidx))
else
let
fun pretty_typing t ty =
@@ -1645,8 +1645,8 @@
|> fold add_instT_sorts instT
|> fold add_inst_sorts inst;
- val instT' = Term_Subst.TVars.build (fold (add_instT thy') instT);
- val inst' = Term_Subst.Vars.build (fold (add_inst thy') inst);
+ val instT' = TVars.build (fold (add_instT thy') instT);
+ val inst' = Vars.build (fold (add_inst thy') inst);
in ((instT', inst'), (cert', sorts')) end;
in
@@ -1669,13 +1669,11 @@
val thy' = Context.certificate_theory cert';
val constraints' =
- Term_Subst.TVars.fold (fn ((_, S), (T, _)) => insert_constraints thy' (T, S))
+ TVars.fold (fn ((_, S), (T, _)) => insert_constraints thy' (T, S))
instT' constraints;
in
Thm (deriv_rule1
- (fn d =>
- Proofterm.instantiate
- (Term_Subst.TVars.map (K #1) instT', Term_Subst.Vars.map (K #1) inst') d) der,
+ (fn d => Proofterm.instantiate (TVars.map (K #1) instT', Vars.map (K #1) inst') d) der,
{cert = cert',
tags = [],
maxidx = maxidx',
@@ -1780,7 +1778,7 @@
(*Replace all TFrees not fixed or in the hyps by new TVars*)
fun varifyT_global' fixed (Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...})) =
let
- val tfrees = fold Term_Subst.add_tfrees hyps fixed;
+ val tfrees = fold TFrees.add_tfrees hyps fixed;
val prop1 = attach_tpairs tpairs prop;
val (al, prop2) = Type.varify_global tfrees prop1;
val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
@@ -1796,7 +1794,7 @@
prop = prop3}))
end;
-val varifyT_global = #2 o varifyT_global' Term_Subst.TFrees.empty;
+val varifyT_global = #2 o varifyT_global' TFrees.empty;
(*Replace all TVars by TFrees that are often new*)
fun legacy_freezeT (Thm (der, {cert, constraints, shyps, hyps, tpairs, prop, ...})) =
--- a/src/Pure/type.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/type.ML Thu Sep 09 12:33:14 2021 +0200
@@ -61,7 +61,7 @@
val strip_sorts: typ -> typ
val strip_sorts_dummy: typ -> typ
val no_tvars: typ -> typ
- val varify_global: Term_Subst.TFrees.set -> term -> ((string * sort) * indexname) list * term
+ val varify_global: TFrees.set -> term -> ((string * sort) * indexname) list * term
val legacy_freeze_thaw_type: typ -> typ * (typ -> typ)
val legacy_freeze_type: typ -> typ
val legacy_freeze_thaw: term -> term * (term -> term)
@@ -357,7 +357,7 @@
let
val fs =
build (t |> (Term.fold_types o Term.fold_atyps)
- (fn TFree v => if Term_Subst.TFrees.defined fixed v then I else insert (op =) v | _ => I));
+ (fn TFree v => if TFrees.defined fixed v then I else insert (op =) v | _ => I));
val used = Name.context
|> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t;
val fmap = fs ~~ map (rpair 0) (#1 (fold_map Name.variant (map fst fs) used));
--- a/src/Pure/type_infer.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/type_infer.ML Thu Sep 09 12:33:14 2021 +0200
@@ -114,10 +114,10 @@
let
val [a] = Name.invent used Name.aT 1;
val used' = Name.declare a used;
- in (Term_Subst.TVars.add ((xi, S), TFree (a, improve_sort S)) inst, used') end
+ in (TVars.add ((xi, S), TFree (a, improve_sort S)) inst, used') end
else (inst, used);
val used = (fold o fold_types) Term.declare_typ_names ts (Variable.names_of ctxt);
- val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) (Term_Subst.TVars.empty, used);
+ val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) (TVars.empty, used);
in (map o map_types) (Term_Subst.instantiateT inst) ts end;
end;
--- a/src/Pure/variable.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Pure/variable.ML Thu Sep 09 12:33:14 2021 +0200
@@ -69,15 +69,15 @@
val export: Proof.context -> Proof.context -> thm list -> thm list
val export_morphism: Proof.context -> Proof.context -> morphism
val invent_types: sort list -> Proof.context -> (string * sort) list * Proof.context
- val importT_inst: term list -> Proof.context -> typ Term_Subst.TVars.table * Proof.context
+ val importT_inst: term list -> Proof.context -> typ TVars.table * Proof.context
val import_inst: bool -> term list -> Proof.context ->
- (typ Term_Subst.TVars.table * term Term_Subst.Vars.table) * Proof.context
+ (typ TVars.table * term Vars.table) * Proof.context
val importT_terms: term list -> Proof.context -> term list * Proof.context
val import_terms: bool -> term list -> Proof.context -> term list * Proof.context
- val importT: thm list -> Proof.context -> (ctyp Term_Subst.TVars.table * thm list) * Proof.context
+ val importT: thm list -> Proof.context -> (ctyp TVars.table * thm list) * Proof.context
val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context
val import: bool -> thm list -> Proof.context ->
- ((ctyp Term_Subst.TVars.table * cterm Term_Subst.Vars.table) * thm list) * Proof.context
+ ((ctyp TVars.table * cterm Vars.table) * thm list) * Proof.context
val import_vars: Proof.context -> thm -> thm
val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
@@ -515,14 +515,14 @@
val still_fixed = not o is_newly_fixed inner outer;
val gen_fixes =
- Symtab.build (fixes_of inner |> Name_Space.fold_table (fn (y, _) =>
- not (is_fixed outer y) ? Symtab.insert_set y));
+ Names.build (fixes_of inner |> Name_Space.fold_table (fn (y, _) =>
+ not (is_fixed outer y) ? Names.add_set y));
val type_occs_inner = type_occs_of inner;
fun gen_fixesT ts =
- Symtab.build (fold decl_type_occs ts type_occs_inner |> Symtab.fold (fn (a, xs) =>
+ Names.build (fold decl_type_occs ts type_occs_inner |> Symtab.fold (fn (a, xs) =>
if declared_outer a orelse exists still_fixed xs
- then I else Symtab.insert_set a));
+ then I else Names.add_set a));
in (gen_fixesT, gen_fixes) end;
fun exportT_inst inner outer = #1 (export_inst inner outer);
@@ -533,7 +533,7 @@
val maxidx = maxidx_of outer;
in
fn ts => ts |> map
- (Term_Subst.generalize (mk_tfrees ts, Symtab.empty)
+ (Term_Subst.generalize (mk_tfrees ts, Names.empty)
(fold (Term.fold_types Term.maxidx_typ) ts maxidx + 1))
end;
@@ -564,7 +564,7 @@
val idx = fold Thm.maxidx_thm ths maxidx + 1;
in map (Thm.generalize (tfrees, frees) idx) ths end;
-fun exportT inner outer = gen_export (exportT_inst inner outer, Symtab.empty) (maxidx_of outer);
+fun exportT inner outer = gen_export (exportT_inst inner outer, Names.empty) (maxidx_of outer);
fun export inner outer = gen_export (export_inst inner outer) (maxidx_of outer);
fun export_morphism inner outer =
@@ -592,9 +592,7 @@
let
val tvars = build_rev (fold Term.add_tvars ts);
val (tfrees, ctxt') = invent_types (map #2 tvars) ctxt;
- val instT =
- Term_Subst.TVars.build (fold2 (fn a => fn b =>
- Term_Subst.TVars.add (a, TFree b)) tvars tfrees);
+ val instT = TVars.build (fold2 (fn a => fn b => TVars.add (a, TFree b)) tvars tfrees);
in (instT, ctxt') end;
fun import_inst is_open ts ctxt =
@@ -603,14 +601,12 @@
val (instT, ctxt') = importT_inst ts ctxt;
val vars = map (apsnd (Term_Subst.instantiateT instT)) (build_rev (fold Term.add_vars ts));
val (ys, ctxt'') = variant_fixes (map (ren o #1 o #1) vars) ctxt';
- val inst =
- Term_Subst.Vars.build (fold2 (fn (x, T) => fn y =>
- Term_Subst.Vars.add ((x, T), Free (y, T))) vars ys);
+ val inst = Vars.build (fold2 (fn (x, T) => fn y => Vars.add ((x, T), Free (y, T))) vars ys);
in ((instT, inst), ctxt'') end;
fun importT_terms ts ctxt =
let val (instT, ctxt') = importT_inst ts ctxt
- in (map (Term_Subst.instantiate (instT, Term_Subst.Vars.empty)) ts, ctxt') end;
+ in (map (Term_Subst.instantiate (instT, Vars.empty)) ts, ctxt') end;
fun import_terms is_open ts ctxt =
let val (inst, ctxt') = import_inst is_open ts ctxt
@@ -619,8 +615,8 @@
fun importT ths ctxt =
let
val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt;
- val instT' = Term_Subst.TVars.map (K (Thm.ctyp_of ctxt')) instT;
- val ths' = map (Thm.instantiate (Term_Subst.TVars.dest instT', [])) ths;
+ val instT' = TVars.map (K (Thm.ctyp_of ctxt')) instT;
+ val ths' = map (Thm.instantiate (TVars.dest instT', [])) ths;
in ((instT', ths'), ctxt') end;
fun import_prf is_open prf ctxt =
@@ -632,9 +628,9 @@
fun import is_open ths ctxt =
let
val ((instT, inst), ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt;
- val instT' = Term_Subst.TVars.map (K (Thm.ctyp_of ctxt')) instT;
- val inst' = Term_Subst.Vars.map (K (Thm.cterm_of ctxt')) inst;
- val ths' = map (Thm.instantiate (Term_Subst.TVars.dest instT', Term_Subst.Vars.dest inst')) ths;
+ 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;
in (((instT', inst'), ths'), ctxt') end;
fun import_vars ctxt th =
@@ -690,10 +686,10 @@
fun focus_subgoal bindings i st =
let
- val all_vars = Term_Subst.Vars.build (Thm.fold_terms {hyps = false} Term_Subst.add_vars st);
+ val all_vars = Vars.build (Thm.fold_terms {hyps = false} Vars.add_vars st);
in
- Term_Subst.Vars.fold (unbind_term o #1 o #1) all_vars #>
- Term_Subst.Vars.fold (declare_constraints o Var o #1) all_vars #>
+ Vars.fold (unbind_term o #1 o #1) all_vars #>
+ Vars.fold (declare_constraints o Var o #1) all_vars #>
focus_cterm bindings (Thm.cprem_of st i)
end;
@@ -732,14 +728,14 @@
val occs = type_occs_of ctxt;
val occs' = type_occs_of ctxt';
val types =
- Symtab.build (occs' |> Symtab.fold (fn (a, _) =>
- if Symtab.defined occs a then I else Symtab.insert_set a));
+ Names.build (occs' |> Symtab.fold (fn (a, _) =>
+ if Symtab.defined occs a then I else Names.add_set a));
val idx = maxidx_of ctxt' + 1;
val Ts' = (fold o fold_types o fold_atyps)
(fn T as TFree _ =>
(case Term_Subst.generalizeT types idx T of TVar v => insert (op =) v | _ => I)
| _ => I) ts [];
- val ts' = map (Term_Subst.generalize (types, Symtab.empty) idx) ts;
+ val ts' = map (Term_Subst.generalize (types, Names.empty) idx) ts;
in (rev Ts', ts') end;
fun polymorphic ctxt ts = snd (polymorphic_types ctxt ts);
--- a/src/Tools/IsaPlanner/rw_inst.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Tools/IsaPlanner/rw_inst.ML Thu Sep 09 12:33:14 2021 +0200
@@ -236,7 +236,7 @@
|> Drule.implies_intr_list cprems
|> Drule.forall_intr_list frees_of_fixed_vars
|> Drule.forall_elim_list vars
- |> Thm.varifyT_global' (Term_Subst.TFrees.make_set othertfrees)
+ |> Thm.varifyT_global' (TFrees.make_set othertfrees)
|-> K Drule.zero_var_indexes
end;
--- a/src/Tools/misc_legacy.ML Thu Sep 09 10:40:57 2021 +0200
+++ b/src/Tools/misc_legacy.ML Thu Sep 09 12:33:14 2021 +0200
@@ -27,11 +27,11 @@
struct
fun thm_frees th =
- (th, (Term_Subst.Frees.empty, [])) |-> Thm.fold_atomic_cterms {hyps = true} Term.is_Free
+ (th, (Frees.empty, [])) |-> Thm.fold_atomic_cterms {hyps = true} Term.is_Free
(fn ct => fn (set, list) =>
let val v = Term.dest_Free (Thm.term_of ct) in
- if not (Term_Subst.Frees.defined set v)
- then (Term_Subst.Frees.add (v, ()) set, ct :: list)
+ if not (Frees.defined set v)
+ then (Frees.add_set v set, ct :: list)
else (set, list)
end)
|> #2;