src/Doc/Ref/document/thm.tex

updated operations on proof terms;

\chapter{Theorems and Forward Proof}

\section{Proof terms}\label{sec:proofObjects}

Note that there are no separate constructors
for abstraction and application on the level of {\em types}, since
instantiation of type variables is accomplished via the type assignments
attached to {\tt Thm}, {\tt Axm} and {\tt Oracle}.

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.

\medskip

The dependencies of theorems can be viewed using the function
\ttindexbold{thm_deps}\index{theorems!dependencies}:
\begin{ttbox}
thm_deps [\(thm@1\), \(\ldots\), \(thm@n\)];
\end{ttbox}
generates the dependency graph of the theorems $thm@1$, $\ldots$, $thm@n$ and
displays it using Isabelle's graph browser. For this to work properly,
the theorems in question have to be proved with {\tt proofs} set to a value
greater than {\tt 0}. You can use
\begin{ttbox}
ThmDeps.enable : unit -> unit
ThmDeps.disable : unit -> unit
\end{ttbox}
to set \texttt{proofs} appropriately.

\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}
\index{proof terms!printing}

Isabelle offers several functions for parsing and printing
proof terms. The concrete syntax for proof terms is described
in Fig.\ts\ref{fig:proof_gram}.
Implicit term arguments in partial proofs are indicated
by ``{\tt _}''.
Type arguments for theorems and axioms may be specified using
\verb!%! or ``$\cdot$'' with an argument of the form {\tt TYPE($type$)}
(see \S\ref{sec:basic_syntax}).
They must appear before any other term argument of a theorem
or axiom. In contrast to term arguments, type arguments may
be completely omitted.
\begin{ttbox}
ProofSyntax.read_proof : theory -> bool -> string -> Proofterm.proof
ProofSyntax.pretty_proof : Sign.sg -> Proofterm.proof -> Pretty.T
ProofSyntax.pretty_proof_of : bool -> thm -> Pretty.T
ProofSyntax.print_proof_of : bool -> thm -> unit
\end{ttbox}
\begin{figure}
\begin{center}
\begin{tabular}{rcl}
$proof$  & $=$ & {\tt Lam} $params${\tt .} $proof$ ~~$|$~~
                 $\Lambda params${\tt .} $proof$ \\
         & $|$ & $proof$ \verb!%! $any$ ~~$|$~~
                 $proof$ $\cdot$ $any$ \\
         & $|$ & $proof$ \verb!%%! $proof$ ~~$|$~~
                 $proof$ {\boldmath$\cdot$} $proof$ \\
         & $|$ & $id$ ~~$|$~~ $longid$ \\\\
$param$  & $=$ & $idt$ ~~$|$~~ $idt$ {\tt :} $prop$ ~~$|$~~
                 {\tt (} $param$ {\tt )} \\\\
$params$ & $=$ & $param$ ~~$|$~~ $param$ $params$
\end{tabular}
\end{center}
\caption{Proof term syntax}\label{fig:proof_gram}
\end{figure}
The function {\tt read_proof} reads in a proof term with
respect to a given theory. The boolean flag indicates whether
the proof term to be parsed contains explicit typing information
to be taken into account.
Usually, typing information is left implicit and
is inferred during proof reconstruction. The pretty printing
functions operating on theorems take a boolean flag as an
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"
%%% End: