# HG changeset patch # User wenzelm # Date 1571596702 -7200 # Node ID bd4d37edfee41e630bb06f33603f2dca1d905c4a # Parent 05c4c6a99b3f7ebae16f4d373b1a92ef4429ae4e clarified expand_proof/expand_name: allow more detailed control via thm_header; export_standard_proofs: authentic theorem names in "print" format; diff -r 05c4c6a99b3f -r bd4d37edfee4 src/Doc/Implementation/Logic.thy --- a/src/Doc/Implementation/Logic.thy Sun Oct 20 16:16:23 2019 +0200 +++ b/src/Doc/Implementation/Logic.thy Sun Oct 20 20:38:22 2019 +0200 @@ -1189,7 +1189,7 @@ @{index_ML Proofterm.reconstruct_proof: "theory -> term -> proof -> proof"} \\ @{index_ML Proofterm.expand_proof: "theory -> - (string * term option) list -> proof -> proof"} \\ + (Proofterm.thm_header -> string option) -> proof -> proof"} \\ @{index_ML Proof_Checker.thm_of_proof: "theory -> proof -> thm"} \\ @{index_ML Proof_Syntax.read_proof: "theory -> bool -> bool -> string -> proof"} \\ @{index_ML Proof_Syntax.pretty_proof: "Proof.context -> proof -> Pretty.T"} \\ @@ -1228,10 +1228,11 @@ for proofs that are constructed manually, but not for those produced automatically by the inference kernel. - \<^descr> \<^ML>\Proofterm.expand_proof\~\thy [thm\<^sub>1, \, thm\<^sub>n] prf\ expands and - reconstructs the proofs of all specified theorems, with the given (full) - proof. Theorems that are not unique specified via their name may be - disambiguated by giving their proposition. + \<^descr> \<^ML>\Proofterm.expand_proof\~\thy expand prf\ reconstructs and expands + the proofs of nested theorems according to the given \expand\ function: a + result of @{ML \SOME ""\} means full expansion, @{ML \SOME\}~\name\ means to + keep the theorem node but replace its internal name, @{ML NONE} means no + change. \<^descr> \<^ML>\Proof_Checker.thm_of_proof\~\thy prf\ turns the given (full) proof into a theorem, by replaying it using only primitive rules of the inference diff -r 05c4c6a99b3f -r bd4d37edfee4 src/HOL/Proofs/ex/XML_Data.thy --- a/src/HOL/Proofs/ex/XML_Data.thy Sun Oct 20 16:16:23 2019 +0200 +++ b/src/HOL/Proofs/ex/XML_Data.thy Sun Oct 20 20:38:22 2019 +0200 @@ -15,7 +15,7 @@ fun export_proof thy thm = Proofterm.encode (Sign.consts_of thy) (Proofterm.reconstruct_proof thy (Thm.prop_of thm) - (Thm.standard_proof_of {full = true, expand = [Thm.raw_derivation_name thm]} thm)); + (Thm.standard_proof_of {full = true, expand_name = Thm.expand_name thm} thm)); fun import_proof thy xml = let diff -r 05c4c6a99b3f -r bd4d37edfee4 src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Sun Oct 20 16:16:23 2019 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Sun Oct 20 20:38:22 2019 +0200 @@ -19,11 +19,10 @@ [name] => name | _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm])); -fun prf_of thy raw_thm = - let val thm = Thm.transfer thy raw_thm in - Thm.reconstruct_proof_of thm - |> Proofterm.expand_proof (Thm.theory_of_thm thm) [("", NONE)] - end; +fun prf_of thy = + Thm.transfer thy #> + Thm.reconstruct_proof_of #> + Proofterm.expand_proof thy Proofterm.expand_name_empty; fun subsets [] = [[]] | subsets (x::xs) = diff -r 05c4c6a99b3f -r bd4d37edfee4 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Sun Oct 20 16:16:23 2019 +0200 +++ b/src/Pure/Proof/extraction.ML Sun Oct 20 20:38:22 2019 +0200 @@ -504,9 +504,11 @@ val procs = maps (rev o fst o snd) types; val rtypes = map fst types; val typroc = typeof_proc []; + fun expand_name ({name, ...}: Proofterm.thm_header) = + if name = "" orelse member (op =) expand name then SOME "" 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' (map (rpair NONE) ("" :: expand)); + Proofterm.expand_proof thy' expand_name; val rrews = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns); fun find_inst prop Ts ts vs = diff -r 05c4c6a99b3f -r bd4d37edfee4 src/Pure/Proof/proof_rewrite_rules.ML --- a/src/Pure/Proof/proof_rewrite_rules.ML Sun Oct 20 16:16:23 2019 +0200 +++ b/src/Pure/Proof/proof_rewrite_rules.ML Sun Oct 20 20:38:22 2019 +0200 @@ -261,14 +261,14 @@ if r then let val cnames = map (fst o dest_Const o fst) defs'; - val thms = Proofterm.fold_proof_atoms true - (fn PThm ({name, prop, ...}, _) => + val expand = Proofterm.fold_proof_atoms true + (fn PThm ({serial, name, prop, ...}, _) => if member (op =) defnames name orelse not (exists_Const (member (op =) cnames o #1) prop) then I - else cons (name, SOME prop) - | _ => I) [prf] []; - in Proofterm.expand_proof thy thms prf end + else Inttab.update (serial, "") + | _ => I) [prf] Inttab.empty; + in Proofterm.expand_proof thy (Inttab.lookup expand o #serial) prf end else prf; in rewrite_terms (Pattern.rewrite_term thy defs' []) @@ -360,7 +360,7 @@ fun reconstruct prop = Proofterm.reconstruct_proof thy prop #> - Proofterm.expand_proof thy [("", NONE)] #> + Proofterm.expand_proof thy Proofterm.expand_name_empty #> Same.commit (Proofterm.map_proof_same Same.same Same.same of_class_index); in map2 reconstruct (Logic.mk_of_sort (T, S)) diff -r 05c4c6a99b3f -r bd4d37edfee4 src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Sun Oct 20 16:16:23 2019 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Sun Oct 20 20:38:22 2019 +0200 @@ -196,7 +196,6 @@ (Proofterm.term_of_proof prf); fun pretty_standard_proof_of ctxt full thm = - pretty_proof ctxt - (Thm.standard_proof_of {full = full, expand = [Thm.raw_derivation_name thm]} thm); + pretty_proof ctxt (Thm.standard_proof_of {full = full, expand_name = Thm.expand_name thm} thm); end; diff -r 05c4c6a99b3f -r bd4d37edfee4 src/Pure/Thy/export_theory.ML --- a/src/Pure/Thy/export_theory.ML Sun Oct 20 16:16:23 2019 +0200 +++ b/src/Pure/Thy/export_theory.ML Sun Oct 20 20:38:22 2019 +0200 @@ -263,6 +263,13 @@ if #serial thm_id = #serial thm_id' then false else is_some (lookup_thm_id thm_id')); in dep_boxes @ [thm_id] end; + fun expand_name thm_id (header: Proofterm.thm_header) = + if #serial header = #serial thm_id then "" + else + (case lookup_thm_id (Proofterm.thm_header_id header) of + NONE => "" + | SOME thm_name => Thm_Name.print thm_name); + fun entity_markup_thm (serial, (name, i)) = let val space = Facts.space_of (Global_Theory.facts_of thy); @@ -270,15 +277,15 @@ val {pos, ...} = Name_Space.the_entry space name; in make_entity_markup (Thm_Name.print (name, i)) (Thm_Name.print (xname, i)) pos serial end; - fun encode_thm (thm_id, thm_name) raw_thm = + fun encode_thm thm_id raw_thm = let val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy [raw_thm]); val thm = Thm.unconstrainT (clean_thm raw_thm); val boxes = proof_boxes_of thm thm_id; val proof0 = - if export_standard_proofs - then Thm.standard_proof_of {full = true, expand = [Thm_Name.flatten thm_name]} thm + if export_standard_proofs then + Thm.standard_proof_of {full = true, expand_name = SOME o expand_name thm_id} thm else if Proofterm.export_enabled () then Thm.reconstruct_proof_of thm else MinProof; val (prop, SOME proof) = @@ -297,7 +304,7 @@ let val markup = entity_markup_thm (#serial thm_id, thm_name); val thm = Global_Theory.get_thm_name thy (thm_name, Position.none); - val body = encode_thm (thm_id, thm_name) thm; + val body = encode_thm thm_id thm; in YXML.buffer (XML.Elem (markup, body)) end; val _ = diff -r 05c4c6a99b3f -r bd4d37edfee4 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Sun Oct 20 16:16:23 2019 +0200 +++ b/src/Pure/more_thm.ML Sun Oct 20 20:38:22 2019 +0200 @@ -114,7 +114,8 @@ val untag: string -> attribute val kind: string -> attribute val reconstruct_proof_of: thm -> Proofterm.proof - val standard_proof_of: {full: bool, expand: string list} -> thm -> Proofterm.proof + val standard_proof_of: {full: bool, expand_name: Proofterm.thm_header -> string option} -> + thm -> Proofterm.proof val register_proofs: thm list lazy -> theory -> theory val consolidate_theory: theory -> unit val show_consts: bool Config.T @@ -656,10 +657,10 @@ fun reconstruct_proof_of thm = Proofterm.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm); -fun standard_proof_of {full, expand} thm = +fun standard_proof_of {full, expand_name} thm = let val thy = Thm.theory_of_thm thm in reconstruct_proof_of thm - |> Proofterm.expand_proof thy (map (rpair NONE) ("" :: expand)) + |> Proofterm.expand_proof thy expand_name |> Proofterm.rew_proof thy |> Proofterm.no_thm_proofs |> not full ? Proofterm.shrink_proof diff -r 05c4c6a99b3f -r bd4d37edfee4 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Sun Oct 20 16:16:23 2019 +0200 +++ b/src/Pure/proofterm.ML Sun Oct 20 20:38:22 2019 +0200 @@ -162,7 +162,8 @@ val reconstruct_proof: theory -> term -> proof -> proof val prop_of': term list -> proof -> term val prop_of: proof -> term - val expand_proof: theory -> (string * term option) list -> proof -> proof + val expand_name_empty: thm_header -> string option + val expand_proof: theory -> (thm_header -> string option) -> proof -> proof val standard_vars: Name.context -> term * proof option -> term * proof option val standard_vars_term: Name.context -> term -> term @@ -178,9 +179,12 @@ val unconstrain_thm_proof: theory -> (class * class -> proof) -> (string * class list list * class -> proof) -> sort list -> term -> (serial * proof_body future) list -> proof_body -> thm * proof + val get_identity: sort list -> term list -> term -> proof -> + {serial: serial, theory_name: string, name: string} option val get_approximative_name: sort list -> term list -> term -> proof -> string type thm_id = {serial: serial, theory_name: string} val make_thm_id: serial * string -> thm_id + val thm_header_id: thm_header -> thm_id val thm_id: thm -> thm_id val get_id: sort list -> term list -> term -> proof -> thm_id option end @@ -1935,11 +1939,10 @@ (* expand and reconstruct subproofs *) -fun expand_proof thy thms prf = +fun expand_name_empty (header: thm_header) = if #name header = "" then SOME "" else NONE; + +fun expand_proof thy expand_name prf = let - fun do_expand a prop = - exists (fn (b, NONE) => a = b | (b, SOME prop') => a = b andalso prop = prop') thms; - fun expand seen maxidx (AbsP (s, t, prf)) = let val (seen', maxidx', prf') = expand seen maxidx prf in (seen', maxidx', AbsP (s, t, prf')) end @@ -1954,28 +1957,36 @@ | expand seen maxidx (prf % t) = let val (seen', maxidx', prf') = expand seen maxidx prf in (seen', maxidx', prf' % t) end - | expand seen maxidx (prf as PThm ({name = a, prop, types = SOME Ts, ...}, thm_body)) = - if do_expand a prop then - let - val (seen', maxidx', prf') = - (case AList.lookup (op =) seen (a, prop) of - NONE => - let - val prf1 = - thm_body_proof_open thm_body - |> reconstruct_proof thy prop - |> forall_intr_vfs_prf prop; - val (seen1, maxidx1, prf2) = expand_init seen prf1 - val seen2 = ((a, prop), (maxidx1, prf2)) :: seen1; - in (seen2, maxidx1, prf2) end - | SOME (maxidx1, prf1) => (seen, maxidx1, prf1)); - val prf'' = prf' |> incr_indexes (maxidx + 1) |> app_types (maxidx + 1) prop Ts; - in (seen', maxidx' + maxidx + 1, prf'') end - else (seen, maxidx, prf) + | expand seen maxidx (prf as PThm (header, thm_body)) = + let val {serial, pos, theory_name, name, prop, types} = header in + (case expand_name header of + SOME name' => + if name' = "" andalso is_some types then + let + val (seen', maxidx', prf') = + (case Inttab.lookup seen serial of + NONE => + let + val prf1 = + thm_body_proof_open thm_body + |> reconstruct_proof thy prop + |> forall_intr_vfs_prf prop; + val (seen1, maxidx1, prf2) = expand_init seen prf1 + val seen2 = seen1 |> Inttab.update (serial, (maxidx1, prf2)); + in (seen2, maxidx1, prf2) end + | SOME (maxidx1, prf1) => (seen, maxidx1, prf1)); + val prf'' = prf' + |> incr_indexes (maxidx + 1) |> app_types (maxidx + 1) prop (the types); + in (seen', maxidx' + maxidx + 1, prf'') end + else if name' <> name then + (seen, maxidx, PThm (thm_header serial pos theory_name name' prop types, thm_body)) + else (seen, maxidx, prf) + | NONE => (seen, maxidx, prf)) + end | expand seen maxidx prf = (seen, maxidx, prf) and expand_init seen prf = expand seen (maxidx_proof prf ~1) prf; - in #3 (expand_init [] prf) end; + in #3 (expand_init Inttab.empty prf) end; end; @@ -2289,6 +2300,9 @@ fun make_thm_id (serial, theory_name) : thm_id = {serial = serial, theory_name = theory_name}; +fun thm_header_id ({serial, theory_name, ...}: thm_header) = + make_thm_id (serial, theory_name); + fun thm_id (serial, thm_node) : thm_id = make_thm_id (serial, thm_node_theory_name thm_node); diff -r 05c4c6a99b3f -r bd4d37edfee4 src/Pure/thm.ML --- a/src/Pure/thm.ML Sun Oct 20 16:16:23 2019 +0200 +++ b/src/Pure/thm.ML Sun Oct 20 20:38:22 2019 +0200 @@ -108,6 +108,7 @@ val derivation_name: thm -> string val derivation_id: thm -> Proofterm.thm_id option val raw_derivation_name: thm -> string + val expand_name: thm -> Proofterm.thm_header -> string option val name_derivation: string * Position.T -> thm -> thm val close_derivation: Position.T -> thm -> thm val trim_context: thm -> thm @@ -993,6 +994,15 @@ fun raw_derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) = Proofterm.get_approximative_name shyps hyps prop (Proofterm.proof_of body); +fun expand_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) = + let + val self_id = + (case Proofterm.get_identity shyps hyps prop (Proofterm.proof_of body) of + NONE => K false + | SOME {serial, ...} => fn (header: Proofterm.thm_header) => serial = #serial header); + fun expand header = if self_id header orelse #name header = "" then SOME "" 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);