# HG changeset patch # User wenzelm # Date 1701806211 -3600 # Node ID 5f0bbed1c606b1acf9ba3436ad6467109e0be320 # Parent cfe9953696558886fce3bd27c17de3a70bb341da misc tuning and clarification; eliminate clones (see also 3ae09d27ee7a); diff -r cfe995369655 -r 5f0bbed1c606 src/HOL/Tools/choice_specification.ML --- a/src/HOL/Tools/choice_specification.ML Tue Dec 05 20:07:52 2023 +0100 +++ b/src/HOL/Tools/choice_specification.ML Tue Dec 05 20:56:51 2023 +0100 @@ -57,10 +57,10 @@ fun unvarify_global t fmap = let val fmap' = map Library.swap fmap - fun unthaw (f as (a, S)) = - (case AList.lookup (op =) fmap' a of - NONE => TVar f - | SOME (b, _) => TFree (b, S)) + fun unthaw v = + (case AList.lookup (op =) fmap' v of + NONE => TVar v + | SOME w => TFree w) in map_types (map_type_tvar unthaw) t end diff -r cfe995369655 -r 5f0bbed1c606 src/Pure/Proof/proof_checker.ML --- a/src/Pure/Proof/proof_checker.ML Tue Dec 05 20:07:52 2023 +0100 +++ b/src/Pure/Proof/proof_checker.ML Tue Dec 05 20:56:51 2023 +0100 @@ -78,9 +78,8 @@ 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' TFrees.empty thm; - val ctye = - (tvars @ map (fn ((_, S), ixn) => (ixn, S)) fmap ~~ map (Thm.global_ctyp_of thy) Ts); + val (names, thm') = Thm.varifyT_global' TFrees.empty thm; + val ctye = tvars @ map #2 names ~~ map (Thm.global_ctyp_of thy) Ts; in Thm.instantiate (TVars.make ctye, Vars.empty) (Thm.forall_intr_vars (Thm.forall_intr_frees thm')) diff -r cfe995369655 -r 5f0bbed1c606 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Tue Dec 05 20:07:52 2023 +0100 +++ b/src/Pure/proofterm.ML Tue Dec 05 20:56:51 2023 +0100 @@ -121,7 +121,7 @@ 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 -> TFrees.set -> proof -> proof + val varify_proof: ((string * sort) * (indexname * sort)) list -> 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 @@ -932,25 +932,13 @@ (* varify *) -fun varify_names t fixed = +fun varify_proof names prf = let - val xs = - build (t |> (Term.fold_types o Term.fold_atyps) - (fn TFree v => if TFrees.defined fixed v then I else insert (op =) v | _ => I)); - val used = - Name.build_context (t |> - (fold_types o fold_atyps) (fn TVar ((a, _), _) => Name.declare a | _ => I)); - val (ys, _) = fold_map Name.variant (map #1 xs) used; - val zs = map2 (fn (_, S) => fn y => ((y, 0), S)) xs ys; - in xs ~~ zs end; - -fun varify_proof t fixed prf = - let - val table = TFrees.make (varify_names t fixed); - fun varify (a, S) = - (case TFrees.lookup table (a, S) of - NONE => TFree (a, S) - | SOME b => TVar b); + val tab = TFrees.make names; + fun varify v = + (case TFrees.lookup tab v of + NONE => TFree v + | SOME w => TVar w); in map_proof_terms (map_types (map_type_tfree varify)) (map_type_tfree varify) prf end; diff -r cfe995369655 -r 5f0bbed1c606 src/Pure/thm.ML --- a/src/Pure/thm.ML Tue Dec 05 20:07:52 2023 +0100 +++ b/src/Pure/thm.ML Tue Dec 05 20:56:51 2023 +0100 @@ -169,7 +169,7 @@ val trivial: cterm -> thm val of_class: ctyp * class -> thm val unconstrainT: thm -> thm - val varifyT_global': TFrees.set -> thm -> ((string * sort) * indexname) list * thm + val varifyT_global': TFrees.set -> thm -> ((string * sort) * (indexname * sort)) list * thm val varifyT_global: thm -> thm val legacy_freezeT: thm -> thm val plain_prop_of: thm -> term @@ -1934,7 +1934,7 @@ val (al, prop2) = Type.varify_global tfrees prop1; val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2); in - (al, Thm (deriv_rule1 (Proofterm.varify_proof prop tfrees, ZTerm.todo_proof) der, + (al, Thm (deriv_rule1 (Proofterm.varify_proof al, ZTerm.todo_proof) der, {cert = cert, tags = [], maxidx = Int.max (0, maxidx), diff -r cfe995369655 -r 5f0bbed1c606 src/Pure/type.ML --- a/src/Pure/type.ML Tue Dec 05 20:07:52 2023 +0100 +++ b/src/Pure/type.ML Tue Dec 05 20:56:51 2023 +0100 @@ -61,7 +61,8 @@ val strip_sorts: typ -> typ val strip_sorts_dummy: typ -> typ val no_tvars: typ -> typ - val varify_global: TFrees.set -> term -> ((string * sort) * indexname) list * term + val varify_global_names: TFrees.set -> term -> ((string * sort) * (indexname * sort)) list + val varify_global: TFrees.set -> term -> ((string * sort) * (indexname * sort)) 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) @@ -353,20 +354,26 @@ (* varify_global *) -fun varify_global fixed t = +fun varify_global_names fixed t = let - val fs = + val xs = build (t |> (Term.fold_types o Term.fold_atyps) (fn TFree v => if TFrees.defined fixed v then I else insert (op =) v | _ => I)); val used = Name.build_context (t |> (fold_types o fold_atyps) (fn TVar ((a, _), _) => Name.declare a | _ => I)); - val fmap = fs ~~ map (rpair 0) (#1 (fold_map Name.variant (map fst fs) used)); - fun thaw (f as (_, S)) = - (case AList.lookup (op =) fmap f of - NONE => TFree f - | SOME xi => TVar (xi, S)); - in (fmap, map_types (map_type_tfree thaw) t) end; + val ys = #1 (fold_map Name.variant (map #1 xs) used); + in map2 (fn (a, S) => fn b => ((a, S), ((b, 0), S))) xs ys end; + +fun varify_global fixed t = + let + val names = varify_global_names fixed t; + val tab = TFrees.make names; + fun get v = + (case TFrees.lookup tab v of + NONE => TFree v + | SOME w => TVar w); + in (names, (map_types o map_type_tfree) get t) end; (* freeze_thaw: freeze TVars in a term; return the "thaw" inverse *)