--- a/src/Doc/IsarImplementation/Logic.thy Sat Jun 15 21:07:32 2013 +0200
+++ b/src/Doc/IsarImplementation/Logic.thy Mon Jun 17 19:30:41 2013 +0200
@@ -1314,4 +1314,107 @@
\end{description}
*}
+text %mlex {* Detailed proof information of a theorem may be retrieved
+ as follows: *}
+
+lemma ex: "A \<and> B \<longrightarrow> B \<and> A"
+proof
+ assume "A \<and> B"
+ then obtain B and A ..
+ then show "B \<and> A" ..
+qed
+
+ML_val {*
+ (*proof body with digest*)
+ val body = Proofterm.strip_thm (Thm.proof_body_of @{thm ex});
+
+ (*proof term only*)
+ val prf = Proofterm.proof_of body;
+ Pretty.writeln (Proof_Syntax.pretty_proof @{context} prf);
+
+ (*all theorems used in the graph of nested proofs*)
+ val all_thms =
+ Proofterm.fold_body_thms
+ (fn (name, _, _) => insert (op =) name) [body] [];
+*}
+
+text {* The result refers to various basic facts of Isabelle/HOL:
+ @{thm [source] HOL.impI}, @{thm [source] HOL.conjE}, @{thm [source]
+ HOL.conjI} etc. The combinator @{ML Proofterm.fold_body_thms}
+ recursively explores the graph of the proofs of all theorems being
+ used here.
+
+ \medskip Alternatively, we may produce a proof term manually, and
+ turn it into a theorem as follows: *}
+
+ML_val {*
+ val thy = @{theory};
+ val prf =
+ Proof_Syntax.read_proof thy true false
+ "impI \<cdot> _ \<cdot> _ \<bullet> \
+ \ (Lam H: _. \
+ \ conjE \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> H \<bullet> \
+ \ (Lam (H: _) Ha: _. conjI \<cdot> _ \<cdot> _ \<bullet> Ha \<bullet> H))";
+ val thm =
+ prf
+ |> Reconstruct.reconstruct_proof thy @{prop "A \<and> B \<longrightarrow> B \<and> A"}
+ |> Proof_Checker.thm_of_proof thy
+ |> Drule.export_without_context;
+*}
+
+text {* \medskip The subsequent example illustrates the use of various
+ key operations on proof terms: the proof term of an existing theorem
+ is reconstructed and turned again into a theorem using the proof
+ checker; some informative output is printed as well. *}
+
+ML {*
+ fun recheck ctxt0 thm0 =
+ let
+ (*formal transfer and import -- avoid schematic variables*)
+ val thy = Proof_Context.theory_of ctxt0;
+ val ((_, [thm]), ctxt) =
+ Variable.import true [Thm.transfer thy thm0] ctxt0;
+
+ (*main proof information*)
+ val prop = Thm.prop_of thm;
+ val prf =
+ Proofterm.proof_of
+ (Proofterm.strip_thm (Thm.proof_body_of thm));
+ val full_prf = Reconstruct.reconstruct_proof thy prop prf;
+
+ (*informative output*)
+ fun pretty_item name prt =
+ Pretty.block [Pretty.str name, Pretty.brk 1, prt];
+ val _ =
+ [pretty_item "proposition:" (Syntax.pretty_term ctxt prop),
+ pretty_item "proof:" (Proof_Syntax.pretty_proof ctxt prf),
+ pretty_item "full proof:"
+ (Proof_Syntax.pretty_proof ctxt full_prf)]
+ |> Pretty.chunks |> Pretty.writeln;
+
+ (*rechecked theorem*)
+ val thm' =
+ Proof_Checker.thm_of_proof thy full_prf
+ |> singleton (Proof_Context.export ctxt ctxt0);
+ in thm' end;
+*}
+
+text {* As anticipated, the rechecked theorem establishes the same
+ proposition: *}
+
+ML_val {*
+ val thm = @{thm ex};
+ val thm' = recheck @{context} thm;
+ @{assert} (Thm.eq_thm_prop (thm, thm'));
+*}
+
+text {* More precise theorem equality is achieved by adjusting a few
+ accidental details of the theorems involved here: *}
+
+ML_val {*
+ val thm = Thm.map_tags (K []) @{thm ex};
+ val thm' = Thm.strip_shyps (recheck @{context} thm);
+ @{assert} (Thm.eq_thm (thm, thm'));
+*}
+
end
--- a/src/Doc/ROOT Sat Jun 15 21:07:32 2013 +0200
+++ b/src/Doc/ROOT Mon Jun 17 19:30:41 2013 +0200
@@ -69,19 +69,20 @@
"document/build"
"document/root.tex"
-session IsarImplementation (doc) in "IsarImplementation" = HOL +
+session IsarImplementation (doc) in "IsarImplementation" = "HOL-Proofs" +
options [document_variants = "implementation"]
theories
Eq
Integration
Isar
Local_Theory
- Logic
ML
Prelim
Proof
Syntax
Tactic
+ theories [proofs = 2, parallel_proofs = 0]
+ Logic
files
"../prepare_document"
"../pdfsetup.sty"
--- a/src/Doc/Ref/document/thm.tex Sat Jun 15 21:07:32 2013 +0200
+++ b/src/Doc/Ref/document/thm.tex Mon Jun 17 19:30:41 2013 +0200
@@ -3,26 +3,6 @@
\section{Proof terms}\label{sec:proofObjects}
-Each theorem's derivation is stored as the {\tt der} field of its internal
-record:
-\begin{ttbox}
-#2 (#der (rep_thm conjI));
-{\out PThm (("HOL.conjI", []),}
-{\out AbsP ("H", None, AbsP ("H", None, \dots)), \dots, None) %}
-{\out None % None : Proofterm.proof}
-\end{ttbox}
-This proof term identifies a labelled theorem, {\tt conjI} of theory
-\texttt{HOL}, whose underlying proof is
-{\tt AbsP ("H", None, AbsP ("H", None, $\dots$))}.
-The theorem is applied to two (implicit) term arguments, which correspond
-to the two variables occurring in its proposition.
-
-Reconstruction and checking of proofs as described in \S\ref{sec:reconstruct_proofs}
-will not work for proofs constructed with {\tt proofs} set to
-{\tt 0} or {\tt 1}.
-Theorems involving oracles will be printed with a
-suffixed \verb|[!]| to point out the different quality of confidence achieved.
-
\subsection{Reconstructing and checking proof terms}\label{sec:reconstruct_proofs}
\index{proof terms!reconstructing}
\index{proof terms!checking}
@@ -115,45 +95,6 @@
argument which indicates whether the proof term should
be reconstructed before printing.
-The following example (based on Isabelle/HOL) illustrates how
-to parse and check proof terms. We start by parsing a partial
-proof term
-\begin{ttbox}
-val prf = ProofSyntax.read_proof Main.thy false
- "impI % _ % _ %% (Lam H : _. conjE % _ % _ % _ %% H %%
- (Lam (H1 : _) H2 : _. conjI % _ % _ %% H2 %% H1))";
-{\out val prf = PThm (("HOL.impI", []), \dots, \dots, None) % None % None %%}
-{\out AbsP ("H", None, PThm (("HOL.conjE", []), \dots, \dots, None) %}
-{\out None % None % None %% PBound 0 %%}
-{\out AbsP ("H1", None, AbsP ("H2", None, \dots))) : Proofterm.proof}
-\end{ttbox}
-The statement to be established by this proof is
-\begin{ttbox}
-val t = term_of
- (read_cterm (sign_of Main.thy) ("A & B --> B & A", propT));
-{\out val t = Const ("Trueprop", "bool => prop") $}
-{\out (Const ("op -->", "[bool, bool] => bool") $}
-{\out \dots $ \dots : Term.term}
-\end{ttbox}
-Using {\tt t} we can reconstruct the full proof
-\begin{ttbox}
-val prf' = Reconstruct.reconstruct_proof (sign_of Main.thy) t prf;
-{\out val prf' = PThm (("HOL.impI", []), \dots, \dots, Some []) %}
-{\out Some (Const ("op &", \dots) $ Free ("A", \dots) $ Free ("B", \dots)) %}
-{\out Some (Const ("op &", \dots) $ Free ("B", \dots) $ Free ("A", \dots)) %%}
-{\out AbsP ("H", Some (Const ("Trueprop", \dots) $ \dots), \dots)}
-{\out : Proofterm.proof}
-\end{ttbox}
-This proof can finally be turned into a theorem
-\begin{ttbox}
-val thm = ProofChecker.thm_of_proof Main.thy prf';
-{\out val thm = "A & B --> B & A" : Thm.thm}
-\end{ttbox}
-
-\index{proof terms|)}
-\index{theorems|)}
-
-
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "ref"