# HG changeset patch # User wenzelm # Date 1486239311 -3600 # Node ID b81a048960a31fdd66c6a7b68d9ca0b3b63c591e # Parent 69592ac048368e97d62d8e3f2f9a99eb1f24af77 more uniform use of Reconstruct.clean_proof_of; diff -r 69592ac04836 -r b81a048960a3 NEWS --- a/NEWS Sat Feb 04 20:12:27 2017 +0100 +++ b/NEWS Sat Feb 04 21:15:11 2017 +0100 @@ -7,6 +7,12 @@ New in this Isabelle version ---------------------------- +*** General *** + +* Document antiquotations @{prf} and @{full_prf} output proof terms +(again) in the same way as commands 'prf' and 'full_prf'. + + *** Prover IDE -- Isabelle/Scala/jEdit *** * Command-line invocation "isabelle jedit -R -l LOGIC" opens the ROOT diff -r 69592ac04836 -r b81a048960a3 src/HOL/Proofs/ex/Proof_Terms.thy --- a/src/HOL/Proofs/ex/Proof_Terms.thy Sat Feb 04 20:12:27 2017 +0100 +++ b/src/HOL/Proofs/ex/Proof_Terms.thy Sat Feb 04 21:15:11 2017 +0100 @@ -20,12 +20,17 @@ qed ML_val \ + val thm = @{thm ex}; + (*proof body with digest*) - val body = Proofterm.strip_thm (Thm.proof_body_of @{thm ex}); + val body = Proofterm.strip_thm (Thm.proof_body_of thm); (*proof term only*) val prf = Proofterm.proof_of body; - Pretty.writeln (Proof_Syntax.pretty_proof @{context} prf); + + (*clean output*) + Pretty.writeln (Proof_Syntax.pretty_clean_proof_of @{context} false thm); + Pretty.writeln (Proof_Syntax.pretty_clean_proof_of @{context} true thm); (*all theorems used in the graph of nested proofs*) val all_thms = diff -r 69592ac04836 -r b81a048960a3 src/HOL/Proofs/ex/XML_Data.thy --- a/src/HOL/Proofs/ex/XML_Data.thy Sat Feb 04 20:12:27 2017 +0100 +++ b/src/HOL/Proofs/ex/XML_Data.thy Sat Feb 04 21:15:11 2017 +0100 @@ -6,25 +6,14 @@ *) theory XML_Data -imports "~~/src/HOL/Isar_Examples/Drinker" + imports "~~/src/HOL/Isar_Examples/Drinker" begin subsection \Export and re-import of global proof terms\ ML \ fun export_proof ctxt thm = - let - val thy = Proof_Context.theory_of ctxt; - val (_, prop) = - Logic.unconstrainT (Thm.shyps_of thm) - (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm)); - val prf = - Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm)) |> - Reconstruct.reconstruct_proof ctxt prop |> - Reconstruct.expand_proof ctxt [("", NONE)] |> - Proofterm.rew_proof thy |> - Proofterm.no_thm_proofs; - in Proofterm.encode prf end; + Proofterm.encode (Reconstruct.clean_proof_of ctxt true thm); fun import_proof thy xml = let diff -r 69592ac04836 -r b81a048960a3 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Sat Feb 04 20:12:27 2017 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Sat Feb 04 21:15:11 2017 +0100 @@ -260,21 +260,7 @@ | SOME srcs => let val ctxt = Toplevel.context_of state; - val thy = Proof_Context.theory_of ctxt; - fun pretty_proof thm = - let - val (_, prop) = - Logic.unconstrainT (Thm.shyps_of thm) - (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm)); - in - Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm)) - |> Reconstruct.reconstruct_proof ctxt prop - |> Reconstruct.expand_proof ctxt [("", NONE)] - |> Proofterm.rew_proof thy - |> Proofterm.no_thm_proofs - |> not full ? Proofterm.shrink_proof - |> Proof_Syntax.pretty_proof ctxt - end; + val pretty_proof = Proof_Syntax.pretty_clean_proof_of ctxt full; in Pretty.chunks (map pretty_proof (Attrib.eval_thms ctxt srcs)) end); fun string_of_prop ctxt s = diff -r 69592ac04836 -r b81a048960a3 src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Sat Feb 04 20:12:27 2017 +0100 +++ b/src/Pure/Proof/proof_syntax.ML Sat Feb 04 21:15:11 2017 +0100 @@ -16,7 +16,7 @@ val proof_syntax: Proofterm.proof -> theory -> theory val proof_of: Proof.context -> bool -> thm -> Proofterm.proof val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T - val pretty_proof_of: Proof.context -> bool -> thm -> Pretty.T + val pretty_clean_proof_of: Proof.context -> bool -> thm -> Pretty.T end; structure Proof_Syntax : PROOF_SYNTAX = @@ -259,7 +259,7 @@ (Proof_Context.transfer (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt) (term_of_proof prf); -fun pretty_proof_of ctxt full th = - pretty_proof ctxt (proof_of ctxt full th); +fun pretty_clean_proof_of ctxt full thm = + pretty_proof ctxt (Reconstruct.clean_proof_of ctxt full thm); end; diff -r 69592ac04836 -r b81a048960a3 src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Sat Feb 04 20:12:27 2017 +0100 +++ b/src/Pure/Proof/reconstruct.ML Sat Feb 04 21:15:11 2017 +0100 @@ -13,6 +13,7 @@ val proof_of : Proof.context -> thm -> Proofterm.proof val expand_proof : Proof.context -> (string * term option) list -> Proofterm.proof -> Proofterm.proof + val clean_proof_of : Proof.context -> bool -> thm -> Proofterm.proof end; structure Reconstruct : RECONSTRUCT = @@ -388,4 +389,21 @@ in #3 (expand (Proofterm.maxidx_proof prf ~1) [] prf) end; + +(* cleanup for output etc. *) + +fun clean_proof_of ctxt full thm = + let + val (_, prop) = + Logic.unconstrainT (Thm.shyps_of thm) + (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm)); + in + Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm)) + |> reconstruct_proof ctxt prop + |> expand_proof ctxt [("", NONE)] + |> Proofterm.rew_proof (Proof_Context.theory_of ctxt) + |> Proofterm.no_thm_proofs + |> not full ? Proofterm.shrink_proof + end; + end; diff -r 69592ac04836 -r b81a048960a3 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Sat Feb 04 20:12:27 2017 +0100 +++ b/src/Pure/Thy/thy_output.ML Sat Feb 04 21:15:11 2017 +0100 @@ -584,7 +584,7 @@ let val Type (name, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s in Pretty.str (Proof_Context.extern_type ctxt name) end; -fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full; +fun pretty_prf full ctxt = Proof_Syntax.pretty_clean_proof_of ctxt full; fun pretty_theory ctxt (name, pos) = (Theory.check ctxt (name, pos); Pretty.str name);