--- a/src/Doc/IsarImplementation/Logic.thy Thu Jun 13 17:40:58 2013 +0200
+++ b/src/Doc/IsarImplementation/Logic.thy Sat Jun 15 16:55:49 2013 +0200
@@ -523,9 +523,9 @@
\infer[@{text "(assume)"}]{@{text "A \<turnstile> A"}}{}
\]
\[
- \infer[@{text "(\<And>\<hyphen>intro)"}]{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}{@{text "\<Gamma> \<turnstile> b[x]"} & @{text "x \<notin> \<Gamma>"}}
+ \infer[@{text "(\<And>\<hyphen>intro)"}]{@{text "\<Gamma> \<turnstile> \<And>x. B[x]"}}{@{text "\<Gamma> \<turnstile> B[x]"} & @{text "x \<notin> \<Gamma>"}}
\qquad
- \infer[@{text "(\<And>\<hyphen>elim)"}]{@{text "\<Gamma> \<turnstile> b[a]"}}{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}
+ \infer[@{text "(\<And>\<hyphen>elim)"}]{@{text "\<Gamma> \<turnstile> B[a]"}}{@{text "\<Gamma> \<turnstile> \<And>x. B[x]"}}
\]
\[
\infer[@{text "(\<Longrightarrow>\<hyphen>intro)"}]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
@@ -1210,4 +1210,73 @@
\end{description}
*}
+
+section {* Proof terms \label{sec:proof-terms} *}
+
+text {* The Isabelle/Pure inference kernel can record the proof of
+ each theorem as a proof term that contains all logical inferences in
+ detail. Rule composition by resolution (\secref{sec:obj-rules}) and
+ type-class reasoning is broken down to primitive rules of the
+ logical framework. The proof term can be inspected by a separate
+ proof-checker, for example.
+
+ According to the well-known \emph{Curry-Howard isomorphism}, a proof
+ can be viewed as a @{text "\<lambda>"}-term. Following this idea, proofs in
+ Isabelle are internally represented by a datatype similar to the one
+ for terms described in \secref{sec:terms}. On top of these
+ syntactic terms, two more layers of @{text "\<lambda>"}-calculus are added,
+ which correspond to @{text "\<And>x :: \<alpha>. B x"} and @{text "A \<Longrightarrow> B"}
+ according to the propositions-as-types principle. The resulting
+ 3-level @{text "\<lambda>"}-calculus resembles ``@{text "\<lambda>HOL"}'' in the
+ more abstract setting of Pure Type Systems (PTS)
+ \cite{Barendregt-Geuvers:2001}, if some fine points like schematic
+ polymorphism and type classes are ignored.
+
+ \medskip\emph{Proof abstractions} of the form @{text "\<^bold>\<lambda>x :: \<alpha>. prf"}
+ or @{text "\<^bold>\<lambda>p : A. prf"} correspond to introduction of @{text
+ "\<And>"}/@{text "\<Longrightarrow>"}, and \emph{proof applications} of the form @{text
+ "p \<cdot> t"} or @{text "p \<bullet> q"} correspond to elimination of @{text
+ "\<And>"}/@{text "\<Longrightarrow>"}. Actual types @{text "\<alpha>"}, propositions @{text
+ "A"}, and terms @{text "t"} might be suppressed and reconstructed
+ from the overall proof term.
+
+ \medskip Various atomic proofs indicate special situations within
+ the proof construction as follows.
+
+ A \emph{bound proof variable} is a natural number @{text "b"} that
+ acts as de-Bruijn index for proof term abstractions.
+
+ A \emph{minimal proof} ``@{text "?"}'' is a dummy proof term. This
+ indicates some unrecorded part of the proof.
+
+ @{text "Hyp A"} refers to some pending hypothesis by giving its
+ proposition. This indicates an open context of implicit hypotheses,
+ similar to loose bound variables or free variables within a term
+ (\secref{sec:terms}).
+
+ An \emph{axiom} or \emph{oracle} @{text "a : A[\<^vec>\<tau>]"} refers
+ some postulated @{text "proof constant"}, which is subject to
+ schematic polymorphism of theory content, and the particular type
+ instantiation may be given explicitly. The vector of types @{text
+ "\<^vec>\<tau>"} refers to the schematic type variables in the generic
+ proposition @{text "A"} in canonical order.
+
+ A \emph{proof promise} @{text "a : A[\<^vec>\<tau>]"} is a placeholder
+ for some proof of polymorphic proposition @{text "A"}, with explicit
+ type instantiation as given by the vector @{text "\<^vec>\<tau>"}, as
+ above. Unlike axioms or oracles, proof promises may be
+ \emph{fulfilled} eventually, by substituting @{text "a"} by some
+ particular proof @{text "q"} at the corresponding type instance.
+ This acts like Hindley-Milner @{text "let"}-polymorphism: a generic
+ local proof definition may get used at different type instances, and
+ is replaced by the concrete instance eventually.
+
+ A \emph{named theorem} wraps up some concrete proof as a closed
+ formal entity, in the manner of constant definitions for proof
+ terms. The \emph{proof body} of such boxed theorems involves some
+ digest about oracles and promises occurring in the original proof.
+ This allows the inference kernel to manage this critical information
+ without the full overhead of explicit proof terms.
+*}
+
end
--- a/src/Doc/Ref/document/thm.tex Thu Jun 13 17:40:58 2013 +0200
+++ b/src/Doc/Ref/document/thm.tex Sat Jun 15 16:55:49 2013 +0200
@@ -2,20 +2,6 @@
\chapter{Theorems and Forward Proof}
\section{Proof terms}\label{sec:proofObjects}
-\index{proof terms|(} Isabelle can record the full meta-level proof of each
-theorem. The proof term contains all logical inferences in detail.
-%while
-%omitting bookkeeping steps that have no logical meaning to an outside
-%observer. Rewriting steps are recorded in similar detail as the output of
-%simplifier tracing.
-Resolution and rewriting steps are broken down to primitive rules of the
-meta-logic. The proof term can be inspected by a separate proof-checker,
-for example.
-
-According to the well-known {\em Curry-Howard isomorphism}, a proof can
-be viewed as a $\lambda$-term. Following this idea, proofs
-in Isabelle are internally represented by a datatype similar to the one for
-terms described in \S\ref{sec:terms}.
\begin{ttbox}
infix 8 % %%;