# HG changeset patch # User wenzelm # Date 1571580983 -7200 # Node ID 05c4c6a99b3f7ebae16f4d373b1a92ef4429ae4e # Parent 935c78a90ee021acc20407b2d5fa3e04793f717e option to export standardized proof terms (not scalable); diff -r 935c78a90ee0 -r 05c4c6a99b3f etc/options --- a/etc/options Sun Oct 20 12:56:36 2019 +0200 +++ b/etc/options Sun Oct 20 16:16:23 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 935c78a90ee0 -r 05c4c6a99b3f src/HOL/Proofs/ex/XML_Data.thy --- a/src/HOL/Proofs/ex/XML_Data.thy Sun Oct 20 12:56:36 2019 +0200 +++ b/src/HOL/Proofs/ex/XML_Data.thy Sun Oct 20 16:16:23 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 = [Thm.raw_derivation_name thm]} thm)); fun import_proof thy xml = let diff -r 935c78a90ee0 -r 05c4c6a99b3f src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Sun Oct 20 12:56:36 2019 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Sun Oct 20 16:16:23 2019 +0200 @@ -196,6 +196,7 @@ (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 = [Thm.raw_derivation_name thm]} thm); end; diff -r 935c78a90ee0 -r 05c4c6a99b3f src/Pure/ROOT --- a/src/Pure/ROOT Sun Oct 20 12:56:36 2019 +0200 +++ b/src/Pure/ROOT Sun Oct 20 16:16:23 2019 +0200 @@ -4,7 +4,7 @@ description " The Pure logical framework. " - options [threads = 1, export_proofs] + options [threads = 1, export_proofs, export_standard_proofs] theories [export_theory] Pure (global) theories diff -r 935c78a90ee0 -r 05c4c6a99b3f src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Sun Oct 20 12:56:36 2019 +0200 +++ b/src/Pure/System/isabelle_process.ML Sun Oct 20 16:16:23 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 935c78a90ee0 -r 05c4c6a99b3f src/Pure/Thy/export_theory.ML --- a/src/Pure/Thy/export_theory.ML Sun Oct 20 12:56:36 2019 +0200 +++ b/src/Pure/Thy/export_theory.ML Sun Oct 20 16:16:23 2019 +0200 @@ -246,12 +246,23 @@ 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 = + if export_standard_proofs then [] + else + 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 entity_markup_thm (serial, (name, i)) = let val space = Facts.space_of (Global_Theory.facts_of thy); @@ -259,17 +270,19 @@ 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 raw_thm = + fun encode_thm (thm_id, thm_name) 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 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 = [Thm_Name.flatten thm_name]} 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 +296,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_name) thm; in YXML.buffer (XML.Elem (markup, body)) end; val _ = diff -r 935c78a90ee0 -r 05c4c6a99b3f src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Sun Oct 20 12:56:36 2019 +0200 +++ b/src/Pure/more_thm.ML Sun Oct 20 16:16:23 2019 +0200 @@ -114,7 +114,7 @@ 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: string list} -> thm -> Proofterm.proof val register_proofs: thm list lazy -> theory -> theory val consolidate_theory: theory -> unit val show_consts: bool Config.T @@ -656,10 +656,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} 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 (map (rpair NONE) ("" :: expand)) |> Proofterm.rew_proof thy |> Proofterm.no_thm_proofs |> not full ? Proofterm.shrink_proof