# HG changeset patch # User wenzelm # Date 1571600533 -7200 # Node ID d36f600c6500c63448228ba12ac3f2c77f047887 # Parent 8c2bef3df48885f0cf3e2ba73579f1337690b84d# Parent 693e811b91bb6bdeece45876ab894cddca661987 merged diff -r 8c2bef3df488 -r d36f600c6500 etc/options --- a/etc/options Sat Oct 19 20:41:09 2019 +0200 +++ b/etc/options Sun Oct 20 21:42:13 2019 +0200 @@ -291,6 +291,9 @@ option export_theory : bool = false -- "export theory content to Isabelle/Scala" +option export_standard_proofs : bool = false + -- "export standardized proof terms to Isabelle/Scala (not scalable)" + option export_proofs : bool = false -- "export proof terms to Isabelle/Scala" diff -r 8c2bef3df488 -r d36f600c6500 src/Doc/Implementation/Logic.thy --- a/src/Doc/Implementation/Logic.thy Sat Oct 19 20:41:09 2019 +0200 +++ b/src/Doc/Implementation/Logic.thy Sun Oct 20 21:42:13 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 8c2bef3df488 -r d36f600c6500 src/HOL/Proofs/ex/XML_Data.thy --- a/src/HOL/Proofs/ex/XML_Data.thy Sat Oct 19 20:41:09 2019 +0200 +++ b/src/HOL/Proofs/ex/XML_Data.thy Sun Oct 20 21:42:13 2019 +0200 @@ -14,7 +14,8 @@ ML \ fun export_proof thy thm = Proofterm.encode (Sign.consts_of thy) - (Proofterm.reconstruct_proof thy (Thm.prop_of thm) (Thm.standard_proof_of true thm)); + (Proofterm.reconstruct_proof thy (Thm.prop_of thm) + (Thm.standard_proof_of {full = true, expand_name = Thm.expand_name thm} thm)); fun import_proof thy xml = let diff -r 8c2bef3df488 -r d36f600c6500 src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Sat Oct 19 20:41:09 2019 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Sun Oct 20 21:42:13 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 8c2bef3df488 -r d36f600c6500 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Sat Oct 19 20:41:09 2019 +0200 +++ b/src/Pure/Proof/extraction.ML Sun Oct 20 21:42:13 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 8c2bef3df488 -r d36f600c6500 src/Pure/Proof/proof_rewrite_rules.ML --- a/src/Pure/Proof/proof_rewrite_rules.ML Sat Oct 19 20:41:09 2019 +0200 +++ b/src/Pure/Proof/proof_rewrite_rules.ML Sun Oct 20 21:42:13 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 8c2bef3df488 -r d36f600c6500 src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Sat Oct 19 20:41:09 2019 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Sun Oct 20 21:42:13 2019 +0200 @@ -196,6 +196,6 @@ (Proofterm.term_of_proof prf); fun pretty_standard_proof_of ctxt full thm = - pretty_proof ctxt (Thm.standard_proof_of full thm); + pretty_proof ctxt (Thm.standard_proof_of {full = full, expand_name = Thm.expand_name thm} thm); end; diff -r 8c2bef3df488 -r d36f600c6500 src/Pure/ROOT --- a/src/Pure/ROOT Sat Oct 19 20:41:09 2019 +0200 +++ b/src/Pure/ROOT Sun Oct 20 21:42:13 2019 +0200 @@ -4,7 +4,7 @@ description " The Pure logical framework. " - options [threads = 1, export_proofs] + options [threads = 1, export_proofs, export_standard_proofs, prune_proofs = false] theories [export_theory] Pure (global) theories diff -r 8c2bef3df488 -r d36f600c6500 src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Sat Oct 19 20:41:09 2019 +0200 +++ b/src/Pure/System/isabelle_process.ML Sun Oct 20 21:42:13 2019 +0200 @@ -203,6 +203,7 @@ Multithreading.trace := Options.default_int "threads_trace"; Multithreading.max_threads_update (Options.default_int "threads"); Multithreading.parallel_proofs := Options.default_int "parallel_proofs"; + if Options.default_bool "export_standard_proofs" then Proofterm.proofs := 2 else (); let val proofs = Options.default_int "record_proofs" in if proofs < 0 then () else Proofterm.proofs := proofs end; Printer.show_markup_default := false); diff -r 8c2bef3df488 -r d36f600c6500 src/Pure/Thy/export_theory.ML --- a/src/Pure/Thy/export_theory.ML Sat Oct 19 20:41:09 2019 +0200 +++ b/src/Pure/Thy/export_theory.ML Sun Oct 20 21:42:13 2019 +0200 @@ -246,12 +246,28 @@ Theory.axiom_space (Theory.axioms_of thy); - (* theorems *) + (* theorems and proof terms *) + + val export_standard_proofs = Options.default_bool @{system_option export_standard_proofs}; val clean_thm = Thm.check_hyps (Context.Theory thy) #> Thm.strip_shyps; val lookup_thm_id = Global_Theory.lookup_thm_id thy; + fun proof_boxes_of thm thm_id = + let + val dep_boxes = + thm |> Thm_Deps.proof_boxes (fn thm_id' => + 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); @@ -263,13 +279,15 @@ 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 dep_boxes = - thm |> Thm_Deps.proof_boxes (fn thm_id' => - if #serial thm_id = #serial thm_id' then false else is_some (lookup_thm_id thm_id')); - val boxes = dep_boxes @ [thm_id]; + val boxes = proof_boxes_of thm thm_id; + + val proof0 = + 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) = - SOME (if Proofterm.export_enabled () then Thm.reconstruct_proof_of thm else MinProof) - |> standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm); + standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm) (SOME proof0); val _ = Proofterm.commit_proof proof; in (prop, (deps, (boxes, proof))) |> @@ -283,7 +301,8 @@ fun buffer_export_thm (thm_id, thm_name) = let val markup = entity_markup_thm (#serial thm_id, thm_name); - val body = encode_thm thm_id (Global_Theory.get_thm_name thy (thm_name, Position.none)); + val thm = Global_Theory.get_thm_name thy (thm_name, Position.none); + val body = encode_thm thm_id thm; in YXML.buffer (XML.Elem (markup, body)) end; val _ = diff -r 8c2bef3df488 -r d36f600c6500 src/Pure/Thy/export_theory.scala --- a/src/Pure/Thy/export_theory.scala Sat Oct 19 20:41:09 2019 +0200 +++ b/src/Pure/Thy/export_theory.scala Sun Oct 20 21:42:13 2019 +0200 @@ -184,6 +184,9 @@ val CLASS = Value("class") val LOCALE = Value("locale") val LOCALE_DEPENDENCY = Value("locale_dependency") + val DOCUMENT_HEADING = Value("document_heading") + val DOCUMENT_TEXT = Value("document_text") + val PROOF_TEXT = Value("proof_text") } sealed case class Entity( diff -r 8c2bef3df488 -r d36f600c6500 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Sat Oct 19 20:41:09 2019 +0200 +++ b/src/Pure/more_thm.ML Sun Oct 20 21:42:13 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: bool -> 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 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 [("", NONE), (Thm.raw_derivation_name thm, NONE)] + |> Proofterm.expand_proof thy expand_name |> Proofterm.rew_proof thy |> Proofterm.no_thm_proofs |> not full ? Proofterm.shrink_proof diff -r 8c2bef3df488 -r d36f600c6500 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Sat Oct 19 20:41:09 2019 +0200 +++ b/src/Pure/proofterm.ML Sun Oct 20 21:42:13 2019 +0200 @@ -56,6 +56,7 @@ val unions_oracles: oracle Ord_List.T list -> oracle Ord_List.T val unions_thms: thm Ord_List.T list -> thm Ord_List.T val no_proof_body: proof -> proof_body + val no_thm_names: proof -> proof val no_thm_proofs: proof -> proof val no_body_proofs: proof -> proof @@ -162,7 +163,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 +180,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 @@ -306,6 +311,14 @@ fun no_proof_body proof = PBody {oracles = [], thms = [], proof = proof}; val no_thm_body = thm_body (no_proof_body MinProof); +fun no_thm_names (Abst (x, T, prf)) = Abst (x, T, no_thm_names prf) + | 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, name = _, prop, types}, thm_body)) = + PThm (thm_header serial pos theory_name "" prop types, thm_body) + | no_thm_names a = a; + fun no_thm_proofs (Abst (x, T, prf)) = Abst (x, T, no_thm_proofs prf) | no_thm_proofs (AbsP (x, t, prf)) = AbsP (x, t, no_thm_proofs prf) | no_thm_proofs (prf % t) = no_thm_proofs prf % t @@ -1935,11 +1948,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 +1966,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; @@ -2164,7 +2184,7 @@ val typargs = [] |> Term.add_tfrees prop' |> fold_proof_terms Term.add_tfrees prf' |> rev; val consts = Sign.consts_of thy; - val xml = (typargs, (args, (prop', prf'))) |> + val xml = (typargs, (args, (prop', no_thm_names prf'))) |> let open XML.Encode Term_XML.Encode; val encode_vars = list (pair string typ); @@ -2289,6 +2309,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 8c2bef3df488 -r d36f600c6500 src/Pure/term.scala --- a/src/Pure/term.scala Sat Oct 19 20:41:09 2019 +0200 +++ b/src/Pure/term.scala Sun Oct 20 21:42:13 2019 +0200 @@ -94,8 +94,7 @@ case class PAxm(name: String, types: List[Typ]) extends Proof case class OfClass(typ: Typ, cls: Class) extends Proof case class Oracle(name: String, prop: Term, types: List[Typ]) extends Proof - case class PThm(serial: Long, theory_name: String, approximative_name: String, types: List[Typ]) - extends Proof + case class PThm(serial: Long, theory_name: String, name: String, types: List[Typ]) extends Proof /* type classes within the logic */ diff -r 8c2bef3df488 -r d36f600c6500 src/Pure/thm.ML --- a/src/Pure/thm.ML Sat Oct 19 20:41:09 2019 +0200 +++ b/src/Pure/thm.ML Sun Oct 20 21:42:13 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);