# HG changeset patch # User wenzelm # Date 1733002401 -3600 # Node ID cdc43c0fdbfc299d7333304d9d79c619a9798c7b # Parent f012cbfd96d05bdf7d57bb8919df95817db08757 clarified signature; diff -r f012cbfd96d0 -r cdc43c0fdbfc src/HOL/Data_Structures/Define_Time_Function.ML --- a/src/HOL/Data_Structures/Define_Time_Function.ML Sat Nov 30 22:02:36 2024 +0100 +++ b/src/HOL/Data_Structures/Define_Time_Function.ML Sat Nov 30 22:33:21 2024 +0100 @@ -883,7 +883,7 @@ | args _ = [] val dom_vars = terms |> hd |> get_l |> map_types (map_atyps freeTypes) - |> args |> Variable.variant_frees lthy [] + |> args |> Variable.variant_names lthy val dom_args = List.foldl (fn (t,p) => HOLogic.mk_prod ((Free t),p)) (Free (hd dom_vars)) (tl dom_vars) diff -r f012cbfd96d0 -r cdc43c0fdbfc src/HOL/Hoare/hoare_tac.ML --- a/src/HOL/Hoare/hoare_tac.ML Sat Nov 30 22:02:36 2024 +0100 +++ b/src/HOL/Hoare/hoare_tac.ML Sat Nov 30 22:33:21 2024 +0100 @@ -87,7 +87,7 @@ fun Mset ctxt prop = let - val [(Mset, _), (P, _)] = Variable.variant_frees ctxt [] [("Mset", ()), ("P", ())]; + val [(Mset, _), (P, _)] = Variable.variant_names ctxt [("Mset", ()), ("P", ())]; val vars = get_vars prop; val varsT = fastype_of (mk_bodyC vars); diff -r f012cbfd96d0 -r cdc43c0fdbfc src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sat Nov 30 22:02:36 2024 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sat Nov 30 22:33:21 2024 +0100 @@ -274,11 +274,11 @@ in t |> map_aterms norm_var_types |> fold_rev quant_of (map Var normTs) end (* This assumes that distinct names are mapped to distinct names by - "Variable.variant_frees". This does not hold in general but should hold for + "Variable.variant_names". This does not hold in general but should hold for ATP-generated Skolem function names, since these end with a digit and "variant_frees" appends letters. *) fun desymbolize_and_fresh_up ctxt s = - fst (hd (Variable.variant_frees ctxt [] [(Name.desymbolize (SOME false) s, ())])) + fst (singleton (Variable.variant_names ctxt) (Name.desymbolize (SOME false) s, ())) (* Higher-order translation. Variables are typed (although we don't use that information). Lambdas are typed. The code is similar to "term_of_atp_fo". *) diff -r f012cbfd96d0 -r cdc43c0fdbfc src/HOL/Tools/ATP/atp_util.ML --- a/src/HOL/Tools/ATP/atp_util.ML Sat Nov 30 22:02:36 2024 +0100 +++ b/src/HOL/Tools/ATP/atp_util.ML Sat Nov 30 22:33:21 2024 +0100 @@ -410,7 +410,7 @@ let val (t, (frees, params)) = Logic.goal_params (Thm.prop_of goal) i - ||> (map dest_Free #> Variable.variant_frees ctxt [] #> `(map Free)) + ||> (map dest_Free #> Variable.variant_names ctxt #> `(map Free)) val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees) val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees in (rev params, hyp_ts, concl_t) end diff -r f012cbfd96d0 -r cdc43c0fdbfc src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Sat Nov 30 22:02:36 2024 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Sat Nov 30 22:33:21 2024 +0100 @@ -262,7 +262,7 @@ |> mk_TFrees' (map Type.sort_of_atyp As0); val fpT = Type (fpT_name, As); - val (var_name, ()) = singleton (Variable.variant_frees ctxt []) ("x", ()); + val (var_name, ()) = singleton (Variable.variant_names ctxt) ("x", ()); val var = Free (var_name, fpT); val goal = mk_Trueprop_eq (expand_to_ctr_term ctxt fpT var, var); @@ -394,7 +394,7 @@ val fun_T = fastype_of fun_t; val num_args = num_binder_types fun_T; - val f = Free (singleton (Variable.variant_frees ctxt []) ("f", fun_T)); + val f = Free (singleton (Variable.variant_names ctxt) ("f", fun_T)); val is_self_call = curry (op aconv) fun_t; val has_self_call = exists_subterm is_self_call; @@ -777,7 +777,8 @@ val (arg_Ts, _) = strip_type (fastype_of fun_t); val added_Ts = drop (length arg_ts) arg_Ts; val free_names = mk_names (length added_Ts) "x" ~~ added_Ts; - val free_args = Variable.variant_frees ctxt [rhs, lhs] free_names |> map Free; + val free_args = + Variable.variant_names (fold Variable.declare_names [rhs, lhs] ctxt) free_names |> map Free; in (arg_ts @ free_args, list_comb (rhs, free_args)) end; diff -r f012cbfd96d0 -r cdc43c0fdbfc src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Sat Nov 30 22:02:36 2024 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Sat Nov 30 22:33:21 2024 +0100 @@ -1212,7 +1212,9 @@ (map2 append (take actual_nn thmss'') nchotomy_taut_thmss, drop actual_nn thmss''); val ps = - Variable.variant_frees lthy (maps (maps #fun_args) disc_eqnss) [("P", HOLogic.boolT)]; + Variable.variant_names + (fold Variable.declare_names (maps (maps #fun_args) disc_eqnss) lthy) + [("P", HOLogic.boolT)]; val exhaust_thmss = map2 (fn false => K [] diff -r f012cbfd96d0 -r cdc43c0fdbfc src/HOL/Tools/Function/function_elims.ML --- a/src/HOL/Tools/Function/function_elims.ML Sat Nov 30 22:02:36 2024 +0100 +++ b/src/HOL/Tools/Function/function_elims.ML Sat Nov 30 22:33:21 2024 +0100 @@ -79,7 +79,7 @@ val n_fs = length fs; fun variant_free used_term v = - Free (singleton (Variable.variant_frees ctxt [used_term]) v); + Free (singleton (Variable.variant_names (Variable.declare_names used_term ctxt)) v); fun mk_partial_elim_rule (idx, f) = let diff -r f012cbfd96d0 -r cdc43c0fdbfc src/HOL/Tools/Function/induction_schema.ML --- a/src/HOL/Tools/Function/induction_schema.ML Sat Nov 30 22:02:36 2024 +0100 +++ b/src/HOL/Tools/Function/induction_schema.ML Sat Nov 30 22:33:21 2024 +0100 @@ -121,7 +121,8 @@ val relevant_cases = filter (fn SchemeCase {bidx=bidx', ...} => bidx' = bidx) cases val allqnames = fold (fn SchemeCase {qs, ...} => fold (insert (op =) o Free) qs) relevant_cases [] - val (Pbool :: xs') = map Free (Variable.variant_frees ctxt allqnames (("P", HOLogic.boolT) :: xs)) + val (Pbool :: xs') = + map Free (Variable.variant_names (fold Variable.declare_names allqnames ctxt) (("P", HOLogic.boolT) :: xs)) val Cs' = map (Pattern.rewrite_term (Proof_Context.theory_of ctxt) (filter_out (op aconv) (map Free xs ~~ xs')) []) Cs fun mk_case (SchemeCase {qs, oqnames, gs, lhs, ...}) = diff -r f012cbfd96d0 -r cdc43c0fdbfc src/HOL/Tools/Function/mutual.ML --- a/src/HOL/Tools/Function/mutual.ML Sat Nov 30 22:02:36 2024 +0100 +++ b/src/HOL/Tools/Function/mutual.ML Sat Nov 30 22:33:21 2024 +0100 @@ -247,7 +247,7 @@ fun mutual_cases_rule ctxt cases_rule n ST (MutualPart {i, cargTs = Ts, ...}) = let val [P, x] = - Variable.variant_frees ctxt [] [("P", \<^typ>\bool\), ("x", HOLogic.mk_tupleT Ts)] + Variable.variant_names ctxt [("P", \<^typ>\bool\), ("x", HOLogic.mk_tupleT Ts)] |> map (Thm.cterm_of ctxt o Free); val sumtree_inj = Thm.cterm_of ctxt (Sum_Tree.mk_inj ST n i (Thm.term_of x)); diff -r f012cbfd96d0 -r cdc43c0fdbfc src/HOL/Tools/Function/pattern_split.ML --- a/src/HOL/Tools/Function/pattern_split.ML Sat Nov 30 22:02:36 2024 +0100 +++ b/src/HOL/Tools/Function/pattern_split.ML Sat Nov 30 22:33:21 2024 +0100 @@ -20,7 +20,7 @@ fun new_var ctxt vs T = let - val [v] = Variable.variant_frees ctxt vs [("v", T)] + val v = singleton (Variable.variant_names (fold Variable.declare_names vs ctxt)) ("v", T) in (Free v :: vs, Free v) end diff -r f012cbfd96d0 -r cdc43c0fdbfc src/HOL/Tools/Predicate_Compile/code_prolog.ML --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sat Nov 30 22:02:36 2024 +0100 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sat Nov 30 22:33:21 2024 +0100 @@ -991,8 +991,9 @@ mk_set_compr (t :: in_insert) ts xs else let - val uu as (uuN, uuT) = - singleton (Variable.variant_frees ctxt' [t]) ("uu", fastype_of t) + val uuT = fastype_of t + val uu as (uuN, _) = + singleton (Variable.variant_names (Variable.declare_names t ctxt')) ("uu", uuT) val set_compr = HOLogic.mk_Collect (uuN, uuT, fold (fn (s, T) => fn t => HOLogic.mk_exists (s, T, t)) diff -r f012cbfd96d0 -r cdc43c0fdbfc src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sat Nov 30 22:02:36 2024 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sat Nov 30 22:33:21 2024 +0100 @@ -1204,7 +1204,7 @@ fun define_quickcheck_predicate t thy = let val (vs, t') = strip_abs t - val vs' = Variable.variant_frees (Proof_Context.init_global thy) [] vs (* FIXME proper context!? *) + val vs' = Variable.variant_names (Proof_Context.init_global thy) vs (* FIXME proper context!? *) val t'' = subst_bounds (map Free (rev vs'), t') val (prems, concl) = strip_horn t'' val constname = "quickcheck" diff -r f012cbfd96d0 -r cdc43c0fdbfc src/HOL/Tools/Quickcheck/exhaustive_generators.ML --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Sat Nov 30 22:02:36 2024 +0100 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Sat Nov 30 22:33:21 2024 +0100 @@ -279,14 +279,12 @@ let val (constr, args) = strip_comb t val T = fastype_of t + val ctxt1 = fold Variable.declare_names (concl :: assms) ctxt val vars = - map Free - (Variable.variant_frees ctxt (concl :: assms) - (map (fn t => ("x", fastype_of t)) args)) + map Free (Variable.variant_names ctxt1 (map (fn t => ("x", fastype_of t)) args)) val varnames = map (fst o dest_Free) vars - val dummy_var = - Free (singleton - (Variable.variant_frees ctxt (concl :: assms @ vars)) ("dummy", T)) + val ctxt2 = fold Variable.declare_names vars ctxt1 + val dummy_var = Free (singleton (Variable.variant_names ctxt2) ("dummy", T)) val new_assms = map HOLogic.mk_eq (vars ~~ args) val bound_vars' = union (op =) (vars_of lhs) (union (op =) varnames bound_vars) val cont_t = mk_smart_test_term' concl bound_vars' (new_assms @ assms) genuine diff -r f012cbfd96d0 -r cdc43c0fdbfc src/HOL/Tools/Quickcheck/quickcheck_common.ML --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Sat Nov 30 22:02:36 2024 +0100 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Sat Nov 30 22:33:21 2024 +0100 @@ -248,7 +248,7 @@ @{thm bot_fun_def}, @{thm less_bool_def}]) val t' = Pattern.rewrite_term thy rewrs [] (Object_Logic.atomize_term ctxt t) val (vs, body) = strip_all t' - val vs' = Variable.variant_frees ctxt [t'] vs + val vs' = Variable.variant_names (Variable.declare_names t' ctxt) vs in subst_bounds (map Free (rev vs'), body) end diff -r f012cbfd96d0 -r cdc43c0fdbfc src/HOL/Tools/Quotient/quotient_type.ML --- a/src/HOL/Tools/Quotient/quotient_type.ML Sat Nov 30 22:02:36 2024 +0100 +++ b/src/HOL/Tools/Quotient/quotient_type.ML Sat Nov 30 22:33:21 2024 +0100 @@ -33,7 +33,7 @@ let val [x, c] = [("x", rty), ("c", HOLogic.mk_setT rty)] - |> Variable.variant_frees lthy [rel] + |> Variable.variant_names (Variable.declare_names rel lthy) |> map Free in HOLogic.Collect_const (HOLogic.mk_setT rty) $ (lambda c (HOLogic.exists_const rty $ diff -r f012cbfd96d0 -r cdc43c0fdbfc src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Sat Nov 30 22:02:36 2024 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Sat Nov 30 22:33:21 2024 +0100 @@ -139,8 +139,8 @@ (cf. "~~/src/Pure/Isar/obtain.ML") *) let val frees = map Free xs - val thesis = - Free (singleton (Variable.variant_frees ctxt frees) ("thesis", HOLogic.boolT)) + val ctxt' = fold Variable.declare_names frees ctxt + val thesis = Free (singleton (Variable.variant_names ctxt') ("thesis", HOLogic.boolT)) val thesis_prop = HOLogic.mk_Trueprop thesis (* !!x1...xn. t ==> thesis *) diff -r f012cbfd96d0 -r cdc43c0fdbfc src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Sat Nov 30 22:02:36 2024 +0100 +++ b/src/HOL/Tools/inductive.ML Sat Nov 30 22:33:21 2024 +0100 @@ -925,12 +925,12 @@ val predT = replicate k HOLogic.boolT ---> argTs ---> HOLogic.boolT; val fp_const = if coind then \<^Const>\gfp predT\ else \<^Const>\lfp predT\; + val ctxt1 = fold Variable.declare_names intr_ts lthy val p :: xs = - map Free (Variable.variant_frees lthy intr_ts + map Free (Variable.variant_names ctxt1 (("p", predT) :: (mk_names "x" (length argTs) ~~ argTs))); - val bs = - map Free (Variable.variant_frees lthy (p :: xs @ intr_ts) - (map (rpair HOLogic.boolT) (mk_names "b" k))); + val ctxt2 = fold Variable.declare_names (p :: xs) ctxt1 + val bs = map Free (Variable.variant_names ctxt2 (map (rpair HOLogic.boolT) (mk_names "b" k))); fun subst t = (case dest_predicate cs params t of @@ -1001,8 +1001,8 @@ map_index (fn (i, ((b, mx), c)) => let val Ts = arg_types_of (length params) c; - val xs = - map Free (Variable.variant_frees lthy' intr_ts (mk_names "x" (length Ts) ~~ Ts)); + val ctxt = fold Variable.declare_names intr_ts lthy'; + val xs = map Free (Variable.variant_names ctxt (mk_names "x" (length Ts) ~~ Ts)); in ((b, mx), ((Thm.make_def_binding internals b, []), fold_rev lambda (params @ xs) diff -r f012cbfd96d0 -r cdc43c0fdbfc src/Pure/Isar/object_logic.ML --- a/src/Pure/Isar/object_logic.ML Sat Nov 30 22:02:36 2024 +0100 +++ b/src/Pure/Isar/object_logic.ML Sat Nov 30 22:33:21 2024 +0100 @@ -159,7 +159,7 @@ fun is_propositional ctxt T = T = propT orelse - let val x = Free (singleton (Variable.variant_frees ctxt []) ("x", T)) + let val x = Free (singleton (Variable.variant_names ctxt) ("x", T)) in can (fn () => Syntax.check_term ctxt (ensure_propT ctxt x)) () end; diff -r f012cbfd96d0 -r cdc43c0fdbfc src/Pure/variable.ML --- a/src/Pure/variable.ML Sat Nov 30 22:02:36 2024 +0100 +++ b/src/Pure/variable.ML Sat Nov 30 22:33:21 2024 +0100 @@ -17,13 +17,13 @@ val def_sort: Proof.context -> indexname -> sort option val declare_maxidx: int -> Proof.context -> Proof.context val declare_names: term -> Proof.context -> Proof.context + val variant_names: Proof.context -> (string * 'a) list -> (string * 'a) list val declare_constraints: term -> Proof.context -> Proof.context val declare_internal: term -> Proof.context -> Proof.context val declare_term: term -> Proof.context -> Proof.context val declare_typ: typ -> Proof.context -> Proof.context val declare_prf: Proofterm.proof -> Proof.context -> Proof.context val declare_thm: thm -> Proof.context -> Proof.context - val variant_frees: Proof.context -> term list -> (string * 'a) list -> (string * 'a) list val bind_term: indexname * term -> Proof.context -> Proof.context val unbind_term: indexname -> Proof.context -> Proof.context val maybe_bind_term: indexname * term option -> Proof.context -> Proof.context @@ -211,7 +211,7 @@ val declare_maxidx = map_maxidx o Integer.max; -(* names *) +(* type/term names *) fun declare_type_names t = map_names (Term.declare_tfree_names t) #> @@ -222,6 +222,8 @@ map_names (Term.declare_free_names t) #> map_maxidx (Term.maxidx_term t); +fun variant_names ctxt xs = Name.variant_names (names_of ctxt) xs; + (* type occurrences *) @@ -275,12 +277,6 @@ val declare_thm = Thm.fold_terms {hyps = true} declare_internal; -(* renaming term/type frees *) - -fun variant_frees ctxt ts frees = - Name.variant_names (names_of (fold declare_names ts ctxt)) frees; - - (** term bindings **)