--- a/src/Doc/IsarImplementation/Logic.thy Mon Jun 17 19:30:41 2013 +0200
+++ b/src/Doc/IsarImplementation/Logic.thy Mon Jun 17 20:15:34 2013 +0200
@@ -1273,11 +1273,35 @@
without the full overhead of explicit proof terms.
*}
+
+subsection {* Reconstructing and checking proof terms *}
+
+text {* Fully explicit proof terms can be large, but most of this
+ information is redundant and can be reconstructed from the context.
+ Therefore, the Isabelle/Pure inference kernel records only
+ \emph{implicit} proof terms, by omitting all typing information in
+ terms, all term and type labels of proof abstractions, and some
+ argument terms of applications @{text "p \<cdot> t"} (if possible).
+
+ There are separate operations to reconstruct the full proof term
+ later on, using \emph{higher-order pattern unification}
+ \cite{nipkow-patterns,Berghofer-Nipkow:2000:TPHOL}.
+
+ The \emph{proof checker} expects a fully reconstructed proof term,
+ and can turn it into a theorem by replaying its primitive inferences
+ within the kernel. *}
+
text %mlref {*
\begin{mldecls}
@{index_ML_type proof} \\
@{index_ML_type proof_body} \\
@{index_ML proofs: "int Unsynchronized.ref"} \\
+ @{index_ML Reconstruct.reconstruct_proof:
+ "theory -> term -> proof -> proof"} \\
+ @{index_ML Reconstruct.expand_proof: "theory ->
+ (string * term option) list -> proof -> proof"} \\
+ @{index_ML Proof_Checker.thm_of_proof:
+ "theory -> proof -> thm"} \\
\end{mldecls}
\begin{description}
@@ -1311,6 +1335,25 @@
Officially named theorems that contribute to a result are recorded
in any case.
+ \item @{ML Reconstruct.reconstruct_proof}~@{text "thy prop prf"}
+ turns the implicit proof term @{text "prf"} into a full proof of the
+ given proposition.
+
+ Reconstruction may fail if @{text "prf"} is not a proof of @{text
+ "prop"}, or if it does not contain sufficient information for
+ reconstruction. Failure may only happen for proofs that are
+ constructed manually, but not for those produced automatically by
+ the inference kernel.
+
+ \item @{ML Reconstruct.expand_proof}~@{text "thy [thm\<^sub>1, \<dots>, thm\<^sub>n]
+ prf"} 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.
+
+ \item @{ML Proof_Checker.thm_of_proof}~@{text "thy prf"} turns the
+ given (full) proof into a theorem, by replaying it using only
+ primitive rules of the inference kernel.
+
\end{description}
*}
--- a/src/Doc/Ref/document/root.tex Mon Jun 17 19:30:41 2013 +0200
+++ b/src/Doc/Ref/document/root.tex Mon Jun 17 20:15:34 2013 +0200
@@ -25,7 +25,8 @@
\emph{Note}: this document is part of the earlier Isabelle
documentation and is mostly outdated. Fully obsolete parts of the
original text have already been removed. The remaining material
-covers some aspects that did not make it into the newer manuals yet.
+covers some aspects that did not make it into the newer manuals yet
+\cite{isabelle-isar-ref,isabelle-implementation}.
\subsubsection*{Acknowledgements}
Tobias Nipkow, of T. U. Munich, wrote most of
--- a/src/Doc/Ref/document/thm.tex Mon Jun 17 19:30:41 2013 +0200
+++ b/src/Doc/Ref/document/thm.tex Mon Jun 17 20:15:34 2013 +0200
@@ -3,49 +3,6 @@
\section{Proof terms}\label{sec:proofObjects}
-\subsection{Reconstructing and checking proof terms}\label{sec:reconstruct_proofs}
-\index{proof terms!reconstructing}
-\index{proof terms!checking}
-
-When looking at the above datatype of proofs more closely, one notices that
-some arguments of constructors are {\it optional}. The reason for this is that
-keeping a full proof term for each theorem would result in enormous memory
-requirements. Fortunately, typical proof terms usually contain quite a lot of
-redundant information that can be reconstructed from the context. Therefore,
-Isabelle's inference kernel creates only {\em partial} (or {\em implicit})
-\index{proof terms!partial} proof terms, in which
-all typing information in terms, all term and type labels of abstractions
-{\tt AbsP} and {\tt Abst}, and (if possible) some argument terms of
-\verb!%! are omitted. The following functions are available for
-reconstructing and checking proof terms:
-\begin{ttbox}
-Reconstruct.reconstruct_proof :
- Sign.sg -> term -> Proofterm.proof -> Proofterm.proof
-Reconstruct.expand_proof :
- Sign.sg -> string list -> Proofterm.proof -> Proofterm.proof
-ProofChecker.thm_of_proof : theory -> Proofterm.proof -> thm
-\end{ttbox}
-
-\begin{ttdescription}
-\item[Reconstruct.reconstruct_proof $sg$ $t$ $prf$]
-turns the partial proof $prf$ into a full proof of the
-proposition denoted by $t$, with respect to signature $sg$.
-Reconstruction will fail with an error message if $prf$
-is not a proof of $t$, is ill-formed, or does not contain
-sufficient information for reconstruction by
-{\em higher order pattern unification}
-\cite{nipkow-patterns, Berghofer-Nipkow:2000:TPHOL}.
-The latter may only happen for proofs
-built up ``by hand'' but not for those produced automatically
-by Isabelle's inference kernel.
-\item[Reconstruct.expand_proof $sg$
- \ttlbrack$name@1$, $\ldots$, $name@n${\ttrbrack} $prf$]
-expands and reconstructs the proofs of all theorems with names
-$name@1$, $\ldots$, $name@n$ in the (full) proof $prf$.
-\item[ProofChecker.thm_of_proof $thy$ $prf$] turns the (full) proof
-$prf$ into a theorem with respect to theory $thy$ by replaying
-it using only primitive rules from Isabelle's inference kernel.
-\end{ttdescription}
\subsection{Parsing and printing proof terms}
\index{proof terms!parsing}