--- 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"
--- 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>\<open>Proofterm.expand_proof\<close>~\<open>thy [thm\<^sub>1, \<dots>, thm\<^sub>n] prf\<close> 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>\<open>Proofterm.expand_proof\<close>~\<open>thy expand prf\<close> reconstructs and expands
+ the proofs of nested theorems according to the given \<open>expand\<close> function: a
+ result of @{ML \<open>SOME ""\<close>} means full expansion, @{ML \<open>SOME\<close>}~\<open>name\<close> means to
+ keep the theorem node but replace its internal name, @{ML NONE} means no
+ change.
\<^descr> \<^ML>\<open>Proof_Checker.thm_of_proof\<close>~\<open>thy prf\<close> turns the given (full) proof
into a theorem, by replaying it using only primitive rules of the inference
--- 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 \<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_name = Thm.expand_name thm} thm));
fun import_proof thy xml =
let
--- 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) =
--- 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 =
--- 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))
--- 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;
--- 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
--- 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);
--- 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 _ =
--- 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(
--- 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
--- 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);
--- 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 */
--- 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);