# HG changeset patch # User wenzelm # Date 1721401132 -7200 # Node ID 505f97165f52c0ceff46c837cdacaa92b99dd974 # Parent 7849b6370425de5f330b09ea86f962908eb61cf6 clarified thm_header command_pos vs. thm_pos; diff -r 7849b6370425 -r 505f97165f52 src/Doc/Implementation/Logic.thy --- a/src/Doc/Implementation/Logic.thy Fri Jul 19 11:29:05 2024 +0200 +++ b/src/Doc/Implementation/Logic.thy Fri Jul 19 16:58:52 2024 +0200 @@ -1293,7 +1293,7 @@ @{define_ML Proofterm.reconstruct_proof: "theory -> term -> proof -> proof"} \\ @{define_ML Proofterm.expand_proof: "theory -> - (Proofterm.thm_header -> Thm_Name.T option) -> proof -> proof"} \\ + (Proofterm.thm_header -> Thm_Name.P option) -> proof -> proof"} \\ @{define_ML Proof_Checker.thm_of_proof: "theory -> proof -> thm"} \\ @{define_ML Proof_Syntax.read_proof: "theory -> bool -> bool -> string -> proof"} \\ @{define_ML Proof_Syntax.pretty_proof: "Proof.context -> proof -> Pretty.T"} \\ diff -r 7849b6370425 -r 505f97165f52 src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Fri Jul 19 11:29:05 2024 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Fri Jul 19 16:58:52 2024 +0200 @@ -16,7 +16,7 @@ fun thm_name_of thm = (case Proofterm.fold_proof_atoms false (fn PThm ({thm_name, ...}, _) => cons thm_name | _ => I) [Thm.proof_of thm] [] of - [thm_name] => thm_name + [(thm_name, _)] => thm_name | _ => raise THM ("thm_name_of: bad proof of theorem", 0, [thm])); val short_name_of = Thm_Name.short o thm_name_of; diff -r 7849b6370425 -r 505f97165f52 src/HOL/Tools/rewrite_hol_proof.ML --- a/src/HOL/Tools/rewrite_hol_proof.ML Fri Jul 19 11:29:05 2024 +0200 +++ b/src/HOL/Tools/rewrite_hol_proof.ML Fri Jul 19 16:58:52 2024 +0200 @@ -305,9 +305,9 @@ (** Replace congruence rules by substitution rules **) -fun strip_cong ps (PThm ({thm_name = ("HOL.cong", 0), ...}, _) % _ % _ % SOME x % SOME y %% +fun strip_cong ps (PThm ({thm_name = (("HOL.cong", 0), _), ...}, _) % _ % _ % SOME x % SOME y %% prfa %% prfT %% prf1 %% prf2) = strip_cong (((x, y), (prf2, prfa)) :: ps) prf1 - | strip_cong ps (PThm ({thm_name = ("HOL.refl", 0), ...}, _) % SOME f %% _) = SOME (f, ps) + | strip_cong ps (PThm ({thm_name = (("HOL.refl", 0), _), ...}, _) % SOME f %% _) = SOME (f, ps) | strip_cong _ _ = NONE; val subst_prf = Proofterm.any_head_of (Thm.proof_of @{thm subst}); @@ -330,15 +330,15 @@ fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t); -fun elim_cong_aux Ts (PThm ({thm_name = ("HOL.iffD1", 0), ...}, _) % _ % _ %% prf1 %% prf2) = +fun elim_cong_aux Ts (PThm ({thm_name = (("HOL.iffD1", 0), _), ...}, _) % _ % _ %% prf1 %% prf2) = Option.map (make_subst Ts prf2 []) (strip_cong [] prf1) - | elim_cong_aux Ts (PThm ({thm_name = ("HOL.iffD1", 0), ...}, _) % P % _ %% prf) = + | elim_cong_aux Ts (PThm ({thm_name = (("HOL.iffD1", 0), _), ...}, _) % P % _ %% prf) = Option.map (mk_AbsP P o make_subst Ts (PBound 0) []) (strip_cong [] (Proofterm.incr_boundvars 1 0 prf)) - | elim_cong_aux Ts (PThm ({thm_name = ("HOL.iffD2", 0), ...}, _) % _ % _ %% prf1 %% prf2) = + | elim_cong_aux Ts (PThm ({thm_name = (("HOL.iffD2", 0), _), ...}, _) % _ % _ %% prf1 %% prf2) = Option.map (make_subst Ts prf2 [] o apsnd (map (make_sym Ts))) (strip_cong [] prf1) - | elim_cong_aux Ts (PThm ({thm_name = ("HOL.iffD2", 0), ...}, _) % _ % P %% prf) = + | elim_cong_aux Ts (PThm ({thm_name = (("HOL.iffD2", 0), _), ...}, _) % _ % P %% prf) = Option.map (mk_AbsP P o make_subst Ts (PBound 0) [] o apsnd (map (make_sym Ts))) (strip_cong [] (Proofterm.incr_boundvars 1 0 prf)) | elim_cong_aux _ _ = NONE; diff -r 7849b6370425 -r 505f97165f52 src/Pure/Build/export_theory.ML --- a/src/Pure/Build/export_theory.ML Fri Jul 19 11:29:05 2024 +0200 +++ b/src/Pure/Build/export_theory.ML Fri Jul 19 16:58:52 2024 +0200 @@ -283,8 +283,8 @@ val lookup_thm_id = Global_Theory.lookup_thm_id thy; fun expand_name thm_id (header: Proofterm.thm_header) = - if #serial header = #serial thm_id then Thm_Name.empty - else the_default Thm_Name.empty (lookup_thm_id (Proofterm.thm_header_id header)); + if #serial header = #serial thm_id then Thm_Name.none + else the_default Thm_Name.none (lookup_thm_id (Proofterm.thm_header_id header)); fun entity_markup_thm (serial, (name, i)) = let @@ -314,7 +314,7 @@ in triple encode_prop (list Thm_Name.encode) encode_proof end end; - fun export_thm (thm_id, thm_name) = + fun export_thm (thm_id, (thm_name, _)) = let val markup = entity_markup_thm (#serial thm_id, thm_name); val body = diff -r 7849b6370425 -r 505f97165f52 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Fri Jul 19 11:29:05 2024 +0200 +++ b/src/Pure/Proof/extraction.ML Fri Jul 19 16:58:52 2024 +0200 @@ -511,9 +511,9 @@ val procs = maps (rev o fst o snd) types; val rtypes = map fst types; val typroc = typeof_proc []; - fun expand_name ({thm_name, ...}: Proofterm.thm_header) = + fun expand_name ({thm_name = (thm_name, _), ...}: Proofterm.thm_header) = if Thm_Name.is_empty thm_name orelse member (op =) expand thm_name - then SOME Thm_Name.empty else NONE; + then SOME Thm_Name.none else NONE; val prep = the_default (K I) prep thy' o Proof_Rewrite_Rules.elim_defs thy' false (map (Thm.transfer thy) defs) o Proofterm.expand_proof thy' expand_name; @@ -623,7 +623,7 @@ | corr d vs ts Ts hs cs _ (prf0 as PThm (thm_header as {types = SOME Ts', ...}, thm_body)) _ defs = let - val {pos, theory_name, thm_name, prop, ...} = thm_header; + val {command_pos, theory_name, thm_name = (thm_name, thm_pos), prop, ...} = thm_header; val prf = Proofterm.thm_body_proof_open thm_body; val (vs', tye) = find_inst prop Ts ts vs; val shyps = mk_shyps tye; @@ -650,8 +650,8 @@ val corr_prf = mkabsp shyps corr_prf0; val corr_prop = Proofterm.prop_of corr_prf; val corr_header = - Proofterm.thm_header (serial ()) pos theory_name - (corr_name thm_name vs', 0) corr_prop + Proofterm.thm_header (serial ()) command_pos theory_name + ((corr_name thm_name vs', 0), thm_pos) corr_prop (SOME (map TVar (Term.add_tvars corr_prop [] |> rev))); val corr_prf' = Proofterm.proof_combP @@ -727,7 +727,7 @@ | extr d vs ts Ts hs (prf0 as PThm (thm_header as {types = SOME Ts', ...}, thm_body)) defs = let - val {pos, theory_name, thm_name, prop, ...} = thm_header; + val {command_pos, theory_name, thm_name = (thm_name, thm_pos), prop, ...} = thm_header; val prf = Proofterm.thm_body_proof_open thm_body; val (vs', tye) = find_inst prop Ts ts vs; val shyps = mk_shyps tye; @@ -772,8 +772,8 @@ SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf); val corr_prop = Proofterm.prop_of corr_prf'; val corr_header = - Proofterm.thm_header (serial ()) pos theory_name - (corr_name thm_name vs', 0) corr_prop + Proofterm.thm_header (serial ()) command_pos theory_name + ((corr_name thm_name vs', 0), thm_pos) corr_prop (SOME (map TVar (Term.add_tvars corr_prop [] |> rev))); val corr_prf'' = Proofterm.proof_combP (Proofterm.proof_combt diff -r 7849b6370425 -r 505f97165f52 src/Pure/Proof/proof_checker.ML --- a/src/Pure/Proof/proof_checker.ML Fri Jul 19 11:29:05 2024 +0200 +++ b/src/Pure/Proof/proof_checker.ML Fri Jul 19 16:58:52 2024 +0200 @@ -88,7 +88,7 @@ (Thm.forall_intr_vars (Thm.forall_intr_frees thm')) end; - fun thm_of _ _ (PThm ({thm_name, prop = prop', types = SOME Ts, ...}, _)) = + fun thm_of _ _ (PThm ({thm_name = (thm_name, thm_pos), prop = prop', types = SOME Ts, ...}, _)) = let val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup thm_name)); val prop = Thm.prop_of thm; @@ -96,9 +96,9 @@ if is_equal prop prop' then () else error ("Duplicate use of theorem name " ^ - quote (Global_Theory.print_thm_name thy thm_name) ^ "\n" ^ - Syntax.string_of_term_global thy prop ^ "\n\n" ^ - Syntax.string_of_term_global thy prop'); + quote (Global_Theory.print_thm_name thy thm_name) ^ Position.here thm_pos + ^ "\n" ^ Syntax.string_of_term_global thy prop + ^ "\n\n" ^ Syntax.string_of_term_global thy prop'); in thm_of_atom thm Ts end | thm_of _ _ (PAxm (name, _, SOME Ts)) = diff -r 7849b6370425 -r 505f97165f52 src/Pure/Proof/proof_rewrite_rules.ML --- a/src/Pure/Proof/proof_rewrite_rules.ML Fri Jul 19 11:29:05 2024 +0200 +++ b/src/Pure/Proof/proof_rewrite_rules.ML Fri Jul 19 16:58:52 2024 +0200 @@ -39,12 +39,12 @@ val equal_elim_axm = ax Proofterm.equal_elim_axm []; val symmetric_axm = ax Proofterm.symmetric_axm [propT]; - fun rew' (PThm ({thm_name = ("Pure.protectD", 0), ...}, _) % _ %% - (PThm ({thm_name = ("Pure.protectI", 0), ...}, _) % _ %% prf)) = SOME prf - | rew' (PThm ({thm_name = ("Pure.conjunctionD1", 0), ...}, _) % _ % _ %% - (PThm ({thm_name = ("Pure.conjunctionI", 0), ...}, _) % _ % _ %% prf %% _)) = SOME prf - | rew' (PThm ({thm_name = ("Pure.conjunctionD2", 0), ...}, _) % _ % _ %% - (PThm ({thm_name = ("Pure.conjunctionI", 0), ...}, _) % _ % _ %% _ %% prf)) = SOME prf + fun rew' (PThm ({thm_name = (("Pure.protectD", 0), _), ...}, _) % _ %% + (PThm ({thm_name = (("Pure.protectI", 0), _), ...}, _) % _ %% prf)) = SOME prf + | rew' (PThm ({thm_name = (("Pure.conjunctionD1", 0), _), ...}, _) % _ % _ %% + (PThm ({thm_name = (("Pure.conjunctionI", 0), _), ...}, _) % _ % _ %% prf %% _)) = SOME prf + | rew' (PThm ({thm_name = (("Pure.conjunctionD2", 0), _), ...}, _) % _ % _ %% + (PThm ({thm_name = (("Pure.conjunctionI", 0), _), ...}, _) % _ % _ %% _ %% prf)) = SOME prf | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %% (PAxm ("Pure.equal_intr", _, _) % _ % _ %% prf %% _)) = SOME prf | rew' (PAxm ("Pure.symmetric", _, _) % _ % _ %% @@ -54,14 +54,14 @@ | rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %% (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.prop", _)) % _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% - ((tg as PThm ({thm_name = ("Pure.protectI", 0), ...}, _)) % _ %% prf2)) = + ((tg as PThm ({thm_name = (("Pure.protectI", 0), _), ...}, _)) % _ %% prf2)) = SOME (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2)) | rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %% (PAxm ("Pure.symmetric", _, _) % _ % _ %% (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.prop", _)) % _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1)) %% - ((tg as PThm ({thm_name = ("Pure.protectI", 0), ...}, _)) % _ %% prf2)) = + ((tg as PThm ({thm_name = (("Pure.protectI", 0), _), ...}, _)) % _ %% prf2)) = SOME (tg %> B %% (equal_elim_axm %> A %> B %% (symmetric_axm % ?? B % ?? A %% prf1) %% prf2)) @@ -245,7 +245,7 @@ (AbsP (s, t, fst (insert_refl defs Ts prf)), false) | insert_refl defs Ts prf = (case Proofterm.strip_combt prf of - (PThm ({thm_name, prop, types = SOME Ts, ...}, _), ts) => + (PThm ({thm_name = (thm_name, _), prop, types = SOME Ts, ...}, _), ts) => if member (op =) defs thm_name then let val vs = vars_of prop; @@ -271,11 +271,11 @@ let val cnames = map (fst o dest_Const o fst) defs'; val expand = Proofterm.fold_proof_atoms true - (fn PThm ({serial, thm_name, prop, ...}, _) => + (fn PThm ({serial, thm_name = (thm_name, _), prop, ...}, _) => if member (op =) defnames thm_name orelse not (exists_Const (member (op =) cnames o #1) prop) then I - else Inttab.update (serial, Thm_Name.empty) + else Inttab.update (serial, Thm_Name.none) | _ => I) [prf] Inttab.empty; in Proofterm.expand_proof thy (Inttab.lookup expand o #serial) prf end else prf; diff -r 7849b6370425 -r 505f97165f52 src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Fri Jul 19 11:29:05 2024 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Fri Jul 19 16:58:52 2024 +0200 @@ -16,7 +16,7 @@ val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T val pretty_proof_boxes_of: Proof.context -> {full: bool, preproc: theory -> proof -> proof} -> thm -> Pretty.T - val standard_proof_of: {full: bool, expand_name: Proofterm.thm_header -> Thm_Name.T option} -> + val standard_proof_of: {full: bool, expand_name: Proofterm.thm_header -> Thm_Name.P option} -> thm -> Proofterm.proof val pretty_standard_proof_of: Proof.context -> bool -> thm -> Pretty.T end; @@ -104,7 +104,7 @@ let val U = Term.itselfT T --> propT in Const ("Pure.PClass", U --> proofT) $ Const (Logic.const_of_class c, U) end; -fun term_of _ (PThm ({serial = i, thm_name = a, types = Ts, ...}, _)) = +fun term_of _ (PThm ({serial = i, thm_name = (a, _), types = Ts, ...}, _)) = fold AppT (these Ts) (Const (Long_Name.append "thm" @@ -227,7 +227,7 @@ fun proof_syntax prf = let val thm_names = Symset.dest (Proofterm.fold_proof_atoms true - (fn PThm ({thm_name, ...}, _) => + (fn PThm ({thm_name = (thm_name, _), ...}, _) => if Thm_Name.is_empty thm_name then I else Symset.insert (Thm_Name.short thm_name) | _ => I) [prf] Symset.empty); val axm_names = Symset.dest (Proofterm.fold_proof_atoms true @@ -264,7 +264,7 @@ excluded = is_some o Global_Theory.lookup_thm_id thy} in Proofterm.proof_boxes selection [Thm.proof_of thm] - |> map (fn ({serial = i, pos, prop, ...}, proof) => + |> map (fn ({serial = i, command_pos, prop, thm_name = (_, thm_pos), ...}, proof) => let val proof' = proof |> Proofterm.reconstruct_proof thy prop @@ -276,7 +276,7 @@ val name = Long_Name.append "thm" (string_of_int i); in Pretty.item - [Pretty.str (name ^ Position.here_list pos ^ ":"), Pretty.brk 1, + [Pretty.str (name ^ Position.here_list [command_pos, thm_pos] ^ ":"), Pretty.brk 1, Syntax.pretty_term ctxt prop', Pretty.fbrk, pretty_proof ctxt proof'] end) |> Pretty.chunks diff -r 7849b6370425 -r 505f97165f52 src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Fri Jul 19 11:29:05 2024 +0200 +++ b/src/Pure/global_theory.ML Fri Jul 19 16:58:52 2024 +0200 @@ -13,13 +13,13 @@ val defined_fact: theory -> string -> bool val alias_fact: binding -> string -> theory -> theory val hide_fact: bool -> string -> theory -> theory - val dest_thms: bool -> theory list -> theory -> (Thm_Name.T * thm) list + val dest_thms: bool -> theory list -> theory -> (Thm_Name.P * thm) list val pretty_thm_name: theory -> Thm_Name.T -> Pretty.T val print_thm_name: theory -> Thm_Name.T -> string - val get_thm_names: theory -> Thm_Name.T Inttab.table - val dest_thm_names: theory -> (Proofterm.thm_id * Thm_Name.T) list - val lookup_thm_id: theory -> Proofterm.thm_id -> Thm_Name.T option - val lookup_thm: theory -> thm -> (Proofterm.thm_id * Thm_Name.T) option + val get_thm_names: theory -> Thm_Name.P Inttab.table + val dest_thm_names: theory -> (Proofterm.thm_id * Thm_Name.P) list + val lookup_thm_id: theory -> Proofterm.thm_id -> Thm_Name.P option + val lookup_thm: theory -> thm -> (Proofterm.thm_id * Thm_Name.P) option val get_thms: theory -> xstring -> thm list val get_thm: theory -> xstring -> thm val transfer_theories: theory -> thm -> thm @@ -63,7 +63,7 @@ structure Data = Theory_Data ( - type T = Facts.T * Thm_Name.T Inttab.table lazy option; + type T = Facts.T * Thm_Name.P Inttab.table lazy option; val empty: T = (Facts.empty, NONE); fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), NONE); ); @@ -86,7 +86,7 @@ fun dest_thms verbose prev_thys thy = Facts.dest_static verbose (map facts_of prev_thys) (facts_of thy) - |> maps (fn (name, thms) => Thm_Name.list (name, Position.none) thms |> map (apfst fst)); + |> maps (fn (name, thms) => Thm_Name.list (name, Position.none) thms); fun pretty_thm_name thy = Facts.pretty_thm_name (Context.Theory thy) (facts_of thy); val print_thm_name = Pretty.string_of oo pretty_thm_name; @@ -99,7 +99,7 @@ fun make_thm_names thy = (dest_thms true (Theory.parents_of thy) thy, Inttab.empty) - |-> fold (fn (thm_name, thm) => fn thm_names => + |-> fold (fn ((thm_name, thm_pos), thm) => fn thm_names => (case Thm.derivation_id (Thm.transfer thy thm) of NONE => thm_names | SOME {serial, theory_name} => @@ -107,11 +107,11 @@ raise THM ("Bad theory name for derivation", 0, [thm]) else (case Inttab.lookup thm_names serial of - SOME thm_name' => + SOME (thm_name', thm_pos') => raise THM ("Duplicate use of derivation identity for " ^ - print_thm_name thy thm_name ^ " vs. " ^ - print_thm_name thy thm_name', 0, [thm]) - | NONE => Inttab.update (serial, thm_name) thm_names))); + print_thm_name thy thm_name ^ Position.here thm_pos ^ " vs. " ^ + print_thm_name thy thm_name' ^ Position.here thm_pos', 0, [thm]) + | NONE => Inttab.update (serial, (thm_name, thm_pos)) thm_names))); fun lazy_thm_names thy = (case thm_names_of thy of @@ -256,7 +256,7 @@ No_Name_Flags => thm | Name_Flags {post, official} => thm - |> (official andalso (post orelse Thm_Name.is_empty (Thm.raw_derivation_name thm))) ? + |> (official andalso (post orelse Thm_Name.is_empty (#1 (Thm.raw_derivation_name thm)))) ? Thm.name_derivation (name, pos) |> (not (Thm_Name.is_empty name) andalso (post orelse not (Thm.has_name_hint thm))) ? Thm.put_name_hint name)); diff -r 7849b6370425 -r 505f97165f52 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Fri Jul 19 11:29:05 2024 +0200 +++ b/src/Pure/proofterm.ML Fri Jul 19 16:58:52 2024 +0200 @@ -9,7 +9,7 @@ signature PROOFTERM = sig type thm_header = - {serial: serial, pos: Position.T list, theory_name: string, thm_name: Thm_Name.T, + {serial: serial, command_pos: Position.T, theory_name: string, thm_name: Thm_Name.P, prop: term, types: typ list option} type thm_body type thm_node @@ -38,7 +38,7 @@ val proof_of: proof_body -> proof val join_proof: proof_body future -> proof val map_proof_of: (proof -> proof) -> proof_body -> proof_body - val thm_header: serial -> Position.T list -> string -> Thm_Name.T -> term -> typ list option -> + val thm_header: serial -> Position.T -> string -> Thm_Name.P -> term -> typ list option -> thm_header val thm_body: proof_body -> thm_body val thm_body_proof_raw: thm_body -> proof @@ -171,8 +171,8 @@ val reconstruct_proof: theory -> term -> proof -> proof val prop_of': term list -> proof -> term val prop_of: proof -> term - val expand_name_empty: thm_header -> Thm_Name.T option - val expand_proof: theory -> (thm_header -> Thm_Name.T option) -> proof -> proof + val expand_name_empty: thm_header -> Thm_Name.P option + val expand_proof: theory -> (thm_header -> Thm_Name.P option) -> proof -> proof val standard_vars: Name.context -> term * proof option -> term * proof option val standard_vars_term: Name.context -> term -> term @@ -189,8 +189,8 @@ val unconstrain_thm_proof: theory -> sorts_proof -> sort list -> term -> (serial * proof_body future) list -> proof_body -> term * proof_body val get_identity: sort list -> term list -> term -> proof -> - {serial: serial, theory_name: string, thm_name: Thm_Name.T} option - val get_approximative_name: sort list -> term list -> term -> proof -> Thm_Name.T + {serial: serial, theory_name: string, thm_name: Thm_Name.P} option + val get_approximative_name: sort list -> term list -> term -> proof -> Thm_Name.P type thm_id = {serial: serial, theory_name: string} val make_thm_id: serial * string -> thm_id val thm_header_id: thm_header -> thm_id @@ -207,7 +207,7 @@ (** datatype proof **) type thm_header = - {serial: serial, pos: Position.T list, theory_name: string, thm_name: Thm_Name.T, + {serial: serial, command_pos: Position.T, theory_name: string, thm_name: Thm_Name.P, prop: term, types: typ list option}; datatype proof = @@ -254,8 +254,8 @@ fun no_proof (PBody {oracles, thms, zboxes, zproof, ...}) = PBody {oracles = oracles, thms = thms, zboxes = zboxes, zproof = zproof, proof = MinProof}; -fun thm_header serial pos theory_name thm_name prop types : thm_header = - {serial = serial, pos = pos, theory_name = theory_name, thm_name = thm_name, +fun thm_header serial command_pos theory_name thm_name prop types : thm_header = + {serial = serial, command_pos = command_pos, theory_name = theory_name, thm_name = thm_name, prop = prop, types = types}; fun thm_body body = Thm_Body {open_proof = I, body = Future.value body}; @@ -291,7 +291,9 @@ val no_export = Lazy.value (); -fun make_thm ({serial, theory_name, thm_name, prop, ...}: thm_header) (Thm_Body {body, ...}) = +fun make_thm + ({serial, theory_name, thm_name = (thm_name, _), prop, ...}: thm_header) + (Thm_Body {body, ...}) = (serial, make_thm_node theory_name thm_name prop body no_export); @@ -343,8 +345,8 @@ | no_thm_names (AbsP (x, t, prf)) = AbsP (x, t, no_thm_names prf) | no_thm_names (prf % t) = no_thm_names prf % t | no_thm_names (prf1 %% prf2) = no_thm_names prf1 %% no_thm_names prf2 - | no_thm_names (PThm ({serial, pos, theory_name, thm_name = _, prop, types}, thm_body)) = - PThm (thm_header serial pos theory_name Thm_Name.empty prop types, thm_body) + | no_thm_names (PThm ({serial, command_pos, theory_name, thm_name = _, prop, types}, thm_body)) = + PThm (thm_header serial command_pos theory_name Thm_Name.none prop types, thm_body) | no_thm_names a = a; fun no_thm_proofs (Abst (x, T, prf)) = Abst (x, T, no_thm_proofs prf) @@ -393,10 +395,9 @@ | zproof (PAxm (a, prop, SOME Ts)) = zproof_const (ZAxiom a) prop Ts | zproof (PClass (T, c)) = OFCLASSp (ztyp T, c) | zproof (Oracle (a, prop, SOME Ts)) = zproof_const (ZOracle a) prop Ts - | zproof (PThm ({serial, pos, theory_name, thm_name, prop, types = SOME Ts, ...}, _)) = - let - val name = (thm_name, try hd pos |> the_default Position.none); - val proof_name = ZThm {theory_name = theory_name, thm_name = name, serial = serial}; + | zproof (PThm ({serial, command_pos, theory_name, thm_name, prop, types = SOME Ts, ...}, _)) = + let val proof_name = + ZThm {theory_name = theory_name, thm_name = thm_name, serial = serial}; in zproof_const proof_name prop Ts end; in zproof end; @@ -421,11 +422,13 @@ fn PAxm (a, b, c) => ([a], pair (term consts) (option (list typ)) (b, c)), fn PClass (a, b) => ([b], typ a), fn Oracle (a, b, c) => ([a], pair (term consts) (option (list typ)) (b, c)), - fn PThm ({serial, pos, theory_name, thm_name, prop, types}, Thm_Body {open_proof, body, ...}) => - ([int_atom serial, theory_name, #1 thm_name, int_atom (#2 thm_name)], - pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts))) - (map Position.properties_of pos, - (prop, (types, map_proof_of open_proof (Future.join body)))))] + fn PThm ({serial, command_pos, theory_name, thm_name, prop, types}, Thm_Body {open_proof, body, ...}) => + ([int_atom serial, theory_name], + pair (properties o Position.properties_of) + (pair Thm_Name.encode_pos + (pair (term consts) + (pair (option (list typ)) (proof_body consts)))) + (command_pos, (thm_name, (prop, (types, map_proof_of open_proof (Future.join body))))))] and proof_body consts (PBody {oracles, thms, zboxes = _, zproof = _, proof = prf}) = triple (list (pair (pair string (properties o Position.properties_of)) (option (term consts)))) (list (thm consts)) (proof consts) (oracles, thms, prf) @@ -459,12 +462,14 @@ fn ([a], b) => let val (c, d) = pair (term consts) (option (list typ)) b in PAxm (a, c, d) end, fn ([b], a) => PClass (typ a, b), fn ([a], b) => let val (c, d) = pair (term consts) (option (list typ)) b in Oracle (a, c, d) end, - fn ([a, b, c, d], e) => + fn ([ser, theory_name], b) => let - val ((x, (y, (z, w)))) = - pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts))) e; - val header = thm_header (int_atom a) (map Position.of_properties x) b (c, int_atom d) y z; - in PThm (header, thm_body w) end] + val ((command_pos, (thm_name, (prop, (types, body))))) = + pair (Position.of_properties o properties) + (pair Thm_Name.decode_pos + (pair (term consts) (pair (option (list typ)) (proof_body consts)))) b; + val header = thm_header (int_atom ser) command_pos theory_name thm_name prop types; + in PThm (header, thm_body body) end] and proof_body consts x = let val (a, b, c) = @@ -568,8 +573,8 @@ | proof (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (typs Ts)) | proof (PClass C) = ofclass C | proof (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (typs Ts)) - | proof (PThm ({serial, pos, theory_name, thm_name, prop, types = SOME Ts}, thm_body)) = - PThm (thm_header serial pos theory_name thm_name prop (SOME (typs Ts)), thm_body) + | proof (PThm ({serial, command_pos, theory_name, thm_name, prop, types = SOME Ts}, thm_body)) = + PThm (thm_header serial command_pos theory_name thm_name prop (SOME (typs Ts)), thm_body) | proof _ = raise Same.SAME; in proof end; @@ -609,8 +614,8 @@ fun change_types types (PAxm (name, prop, _)) = PAxm (name, prop, types) | change_types (SOME [T]) (PClass (_, c)) = PClass (T, c) | change_types types (Oracle (name, prop, _)) = Oracle (name, prop, types) - | change_types types (PThm ({serial, pos, theory_name, thm_name, prop, types = _}, thm_body)) = - PThm (thm_header serial pos theory_name thm_name prop types, thm_body) + | change_types types (PThm ({serial, command_pos, theory_name, thm_name, prop, types = _}, thm_body)) = + PThm (thm_header serial command_pos theory_name thm_name prop types, thm_body) | change_types _ prf = prf; @@ -774,7 +779,7 @@ PClass (norm_type_same T, c) | norm (Oracle (a, prop, Ts)) = Oracle (a, prop, Same.map_option norm_types_same Ts) - | norm (PThm ({serial = i, pos = p, theory_name, thm_name, prop = t, types = Ts}, thm_body)) = + | norm (PThm ({serial = i, command_pos = p, theory_name, thm_name, prop = t, types = Ts}, thm_body)) = PThm (thm_header i p theory_name thm_name t (Same.map_option norm_types_same Ts), thm_body) | norm _ = raise Same.SAME; @@ -1035,8 +1040,8 @@ | proof _ _ (PAxm (a, prop, Ts)) = PAxm (a, prop, typs Ts) | proof _ _ (PClass (T, c)) = PClass (typ T, c) | proof _ _ (Oracle (a, prop, Ts)) = Oracle (a, prop, typs Ts) - | proof _ _ (PThm ({serial, pos, theory_name, thm_name, prop, types}, thm_body)) = - PThm (thm_header serial pos theory_name thm_name prop (typs types), thm_body) + | proof _ _ (PThm ({serial, command_pos, theory_name, thm_name, prop, types}, thm_body)) = + PThm (thm_header serial command_pos theory_name thm_name prop (typs types), thm_body) | proof _ _ _ = raise Same.SAME; val k = length prems; @@ -1458,7 +1463,7 @@ | subst _ _ (PAxm (id, prop, Ts)) = PAxm (id, prop, Same.map_option substTs Ts) | subst _ _ (PClass (T, c)) = PClass (substT T, c) | subst _ _ (Oracle (id, prop, Ts)) = Oracle (id, prop, Same.map_option substTs Ts) - | subst _ _ (PThm ({serial = i, pos = p, theory_name, thm_name, prop, types}, thm_body)) = + | subst _ _ (PThm ({serial = i, command_pos = p, theory_name, thm_name, prop, types}, thm_body)) = PThm (thm_header i p theory_name thm_name prop (Same.map_option substTs types), thm_body) | subst _ _ _ = raise Same.SAME; in fn t => subst 0 0 t handle Same.SAME => t end; @@ -1633,7 +1638,7 @@ | guess_name (prf %% PClass _) = guess_name prf | guess_name (prf % NONE) = guess_name prf | guess_name (prf % SOME (Var _)) = guess_name prf - | guess_name _ = Thm_Name.empty; + | guess_name _ = Thm_Name.none; (* generate constraints for proof term *) @@ -1745,7 +1750,8 @@ | SOME Ts => (Ts, env)); val prop' = subst_atomic_types (prop_types ~~ Ts) (forall_intr_variables_term prop) handle ListPair.UnequalLengths => - error ("Wrong number of type arguments for " ^ quote (Thm_Name.print (guess_name prf))) + error ("Wrong number of type arguments for " ^ + quote (Thm_Name.print_pos (guess_name prf))) in (prop', change_types (SOME Ts) prf, [], env', vTs) end; fun head_norm (prop, prf, cnstrts, env, vTs) = @@ -1933,7 +1939,7 @@ (* expand and reconstruct subproofs *) fun expand_name_empty (header: thm_header) = - if Thm_Name.is_empty (#thm_name header) then SOME Thm_Name.empty else NONE; + if Thm_Name.is_empty (#1 (#thm_name header)) then SOME Thm_Name.none else NONE; fun expand_proof thy expand_name prf = let @@ -1952,10 +1958,10 @@ let val (seen', maxidx', prf') = expand seen maxidx prf in (seen', maxidx', prf' % t) end | expand seen maxidx (prf as PThm (header, thm_body)) = - let val {serial, pos, theory_name, thm_name, prop, types} = header in + let val {serial, command_pos, theory_name, thm_name, prop, types} = header in (case expand_name header of SOME thm_name' => - if #1 thm_name' = "" andalso is_some types then + if #1 (#1 thm_name') = "" andalso is_some types then let val (seen', maxidx', prf') = (case Inttab.lookup seen serial of @@ -1974,7 +1980,7 @@ in (seen', maxidx' + maxidx + 1, prf'') end else if thm_name' <> thm_name then (seen, maxidx, - PThm (thm_header serial pos theory_name thm_name' prop types, thm_body)) + PThm (thm_header serial command_pos theory_name thm_name' prop types, thm_body)) else (seen, maxidx, prf) | NONE => (seen, maxidx, prf)) end @@ -2216,7 +2222,7 @@ if export_enabled () then new_prf () else (case strip_combt (proof_head_of proof0) of - (PThm ({serial = ser, thm_name = a, prop = prop', types = NONE, ...}, thm_body'), args') => + (PThm ({serial = ser, thm_name = (a, _), prop = prop', types = NONE, ...}, thm_body'), args') => if (#1 a = "" orelse a = name) andalso prop' = prop1 andalso args' = args then let val Thm_Body {body = body', ...} = thm_body'; @@ -2249,7 +2255,7 @@ val theory_name = Context.theory_long_name thy; val thm = (i, make_thm_node theory_name name prop1 thm_body export); - val header = thm_header i ([pos, Position.thread_data ()]) theory_name name prop1 NONE; + val header = thm_header i (Position.thread_data ()) theory_name (name, pos) prop1 NONE; val head = PThm (header, Thm_Body {open_proof = open_proof, body = thm_body}); val argst = if unconstrain then @@ -2288,7 +2294,7 @@ end; fun get_approximative_name shyps hyps prop prf = - Option.map #thm_name (get_identity shyps hyps prop prf) |> the_default Thm_Name.empty; + Option.map #thm_name (get_identity shyps hyps prop prf) |> the_default Thm_Name.none; (* thm_id *) @@ -2307,7 +2313,7 @@ fun get_id shyps hyps prop prf : thm_id option = (case get_identity shyps hyps prop prf of NONE => NONE - | SOME {serial, theory_name, thm_name, ...} => + | SOME {serial, theory_name, thm_name = (thm_name, _), ...} => if Thm_Name.is_empty thm_name then NONE else SOME (make_thm_id (serial, theory_name))); fun this_id NONE _ = false diff -r 7849b6370425 -r 505f97165f52 src/Pure/thm.ML --- a/src/Pure/thm.ML Fri Jul 19 11:29:05 2024 +0200 +++ b/src/Pure/thm.ML Fri Jul 19 16:58:52 2024 +0200 @@ -120,8 +120,8 @@ val derivation_closed: thm -> bool val derivation_name: thm -> Thm_Name.T val derivation_id: thm -> Proofterm.thm_id option - val raw_derivation_name: thm -> Thm_Name.T - val expand_name: thm -> Proofterm.thm_header -> Thm_Name.T option + val raw_derivation_name: thm -> Thm_Name.P + val expand_name: thm -> Proofterm.thm_header -> Thm_Name.P option val name_derivation: Thm_Name.P -> thm -> thm val close_derivation: Position.T -> thm -> thm val trim_context: thm -> thm @@ -1131,13 +1131,13 @@ NONE => K false | SOME {serial, ...} => fn (header: Proofterm.thm_header) => serial = #serial header); fun expand header = - if self_id header orelse Thm_Name.is_empty (#thm_name header) - then SOME Thm_Name.empty else NONE; + if self_id header orelse Thm_Name.is_empty (#1 (#thm_name header)) + then SOME Thm_Name.none else NONE; in expand end; (*deterministic name of finished proof*) fun derivation_name (thm as Thm (_, {shyps, hyps, prop, ...})) = - Proofterm.get_approximative_name shyps hyps prop (proof_of thm); + #1 (Proofterm.get_approximative_name shyps hyps prop (proof_of thm)); (*identified PThm node*) fun derivation_id (thm as Thm (_, {shyps, hyps, prop, ...})) = diff -r 7849b6370425 -r 505f97165f52 src/Pure/thm_deps.ML --- a/src/Pure/thm_deps.ML Fri Jul 19 11:29:05 2024 +0200 +++ b/src/Pure/thm_deps.ML Fri Jul 19 16:58:52 2024 +0200 @@ -59,7 +59,7 @@ else let val thm_id = Proofterm.thm_id (i, thm_node) in (case lookup thm_id of - SOME thm_name => + SOME (thm_name, _) => Inttab.update (i, SOME (thm_id, thm_name)) res | NONE => Inttab.update (i, NONE) res diff -r 7849b6370425 -r 505f97165f52 src/Pure/thm_name.ML --- a/src/Pure/thm_name.ML Fri Jul 19 11:29:05 2024 +0200 +++ b/src/Pure/thm_name.ML Fri Jul 19 16:58:52 2024 +0200 @@ -26,9 +26,12 @@ val print_prefix: Context.generic -> Name_Space.T -> T -> Markup.T * string val print_suffix: T -> string val print: T -> string + val print_pos: P -> string val short: T -> string val encode: T XML.Encode.T val decode: T XML.Decode.T + val encode_pos: P XML.Encode.T + val decode_pos: P XML.Decode.T end; structure Thm_Name: THM_NAME = @@ -106,6 +109,8 @@ fun print (name, index) = name ^ print_suffix (name, index); +fun print_pos (thm_name, pos) = print thm_name ^ Position.here pos; + fun short (name, index) = if name = "" orelse index = 0 then name else name ^ "_" ^ string_of_int index; @@ -116,4 +121,7 @@ val encode = let open XML.Encode in pair string int end; val decode = let open XML.Decode in pair string int end; +val encode_pos = let open XML.Encode in pair encode (properties o Position.properties_of) end; +val decode_pos = let open XML.Decode in pair decode (Position.of_properties o properties) end; + end;