--- 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"
--- 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 \<open>
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
--- 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;
--- 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
--- 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);
--- 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 _ =
--- 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