author | wenzelm |
Mon, 17 Jun 2013 20:15:34 +0200 | |
changeset 52411 | f192c4ea5b17 |
parent 52410 | fb1fb867c146 |
permissions | -rw-r--r-- |
30184
37969710e61f
removed parts of the manual that are clearly obsolete, or covered by
wenzelm
parents:
11625
diff
changeset
|
1 |
|
104 | 2 |
\chapter{Theorems and Forward Proof} |
2040
6db93e6f1b11
Documented sort hypotheses and improved discussion of derivations
paulson
parents:
1876
diff
changeset
|
3 |
|
11622 | 4 |
\section{Proof terms}\label{sec:proofObjects} |
5 |
||
6 |
||
7 |
\subsection{Parsing and printing proof terms} |
|
8 |
\index{proof terms!parsing} |
|
9 |
\index{proof terms!printing} |
|
10 |
||
11 |
Isabelle offers several functions for parsing and printing |
|
12 |
proof terms. The concrete syntax for proof terms is described |
|
13 |
in Fig.\ts\ref{fig:proof_gram}. |
|
14 |
Implicit term arguments in partial proofs are indicated |
|
15 |
by ``{\tt _}''. |
|
16 |
Type arguments for theorems and axioms may be specified using |
|
17 |
\verb!%! or ``$\cdot$'' with an argument of the form {\tt TYPE($type$)} |
|
18 |
(see \S\ref{sec:basic_syntax}). |
|
19 |
They must appear before any other term argument of a theorem |
|
20 |
or axiom. In contrast to term arguments, type arguments may |
|
21 |
be completely omitted. |
|
7871 | 22 |
\begin{ttbox} |
11625
74cdf24724ea
Tuned section about parsing and printing proof terms.
berghofe
parents:
11622
diff
changeset
|
23 |
ProofSyntax.read_proof : theory -> bool -> string -> Proofterm.proof |
74cdf24724ea
Tuned section about parsing and printing proof terms.
berghofe
parents:
11622
diff
changeset
|
24 |
ProofSyntax.pretty_proof : Sign.sg -> Proofterm.proof -> Pretty.T |
74cdf24724ea
Tuned section about parsing and printing proof terms.
berghofe
parents:
11622
diff
changeset
|
25 |
ProofSyntax.pretty_proof_of : bool -> thm -> Pretty.T |
74cdf24724ea
Tuned section about parsing and printing proof terms.
berghofe
parents:
11622
diff
changeset
|
26 |
ProofSyntax.print_proof_of : bool -> thm -> unit |
7871 | 27 |
\end{ttbox} |
11622 | 28 |
\begin{figure} |
29 |
\begin{center} |
|
30 |
\begin{tabular}{rcl} |
|
31 |
$proof$ & $=$ & {\tt Lam} $params${\tt .} $proof$ ~~$|$~~ |
|
32 |
$\Lambda params${\tt .} $proof$ \\ |
|
33 |
& $|$ & $proof$ \verb!%! $any$ ~~$|$~~ |
|
34 |
$proof$ $\cdot$ $any$ \\ |
|
35 |
& $|$ & $proof$ \verb!%%! $proof$ ~~$|$~~ |
|
36 |
$proof$ {\boldmath$\cdot$} $proof$ \\ |
|
37 |
& $|$ & $id$ ~~$|$~~ $longid$ \\\\ |
|
38 |
$param$ & $=$ & $idt$ ~~$|$~~ $idt$ {\tt :} $prop$ ~~$|$~~ |
|
39 |
{\tt (} $param$ {\tt )} \\\\ |
|
40 |
$params$ & $=$ & $param$ ~~$|$~~ $param$ $params$ |
|
41 |
\end{tabular} |
|
42 |
\end{center} |
|
43 |
\caption{Proof term syntax}\label{fig:proof_gram} |
|
44 |
\end{figure} |
|
45 |
The function {\tt read_proof} reads in a proof term with |
|
46 |
respect to a given theory. The boolean flag indicates whether |
|
47 |
the proof term to be parsed contains explicit typing information |
|
48 |
to be taken into account. |
|
49 |
Usually, typing information is left implicit and |
|
50 |
is inferred during proof reconstruction. The pretty printing |
|
51 |
functions operating on theorems take a boolean flag as an |
|
52 |
argument which indicates whether the proof term should |
|
53 |
be reconstructed before printing. |
|
54 |
||
5371 | 55 |
%%% Local Variables: |
56 |
%%% mode: latex |
|
57 |
%%% TeX-master: "ref" |
|
58 |
%%% End: |