# HG changeset patch
# User wenzelm
# Date 1371492934 -7200
# Node ID f192c4ea5b17bec17c4dedc6918e695122dda787
# Parent  fb1fb867c1461ab4539a8bf24ff82ecb75159449
more on reconstructing and checking proof terms;

diff -r fb1fb867c146 -r f192c4ea5b17 src/Doc/IsarImplementation/Logic.thy
--- 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}
 *}
 
diff -r fb1fb867c146 -r f192c4ea5b17 src/Doc/Ref/document/root.tex
--- 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
diff -r fb1fb867c146 -r f192c4ea5b17 src/Doc/Ref/document/thm.tex
--- 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}