equal
deleted
inserted
replaced
1 |
1 |
2 \chapter{Theorems and Forward Proof} |
2 \chapter{Theorems and Forward Proof} |
3 |
3 |
4 \section{Proof terms}\label{sec:proofObjects} |
4 \section{Proof terms}\label{sec:proofObjects} |
5 \index{proof terms|(} Isabelle can record the full meta-level proof of each |
|
6 theorem. The proof term contains all logical inferences in detail. |
|
7 %while |
|
8 %omitting bookkeeping steps that have no logical meaning to an outside |
|
9 %observer. Rewriting steps are recorded in similar detail as the output of |
|
10 %simplifier tracing. |
|
11 Resolution and rewriting steps are broken down to primitive rules of the |
|
12 meta-logic. The proof term can be inspected by a separate proof-checker, |
|
13 for example. |
|
14 |
|
15 According to the well-known {\em Curry-Howard isomorphism}, a proof can |
|
16 be viewed as a $\lambda$-term. Following this idea, proofs |
|
17 in Isabelle are internally represented by a datatype similar to the one for |
|
18 terms described in \S\ref{sec:terms}. |
|
19 \begin{ttbox} |
5 \begin{ttbox} |
20 infix 8 % %%; |
6 infix 8 % %%; |
21 |
7 |
22 datatype proof = |
8 datatype proof = |
23 PBound of int |
9 PBound of int |