author | wenzelm |

Sat Jun 15 16:55:49 2013 +0200 (2013-06-15) | |

changeset 52407 | e4662afb3483 |

parent 52406 | 1e57c3c4e05c |

child 52408 | fa2dc6c6c94f |

more on proof terms;

src/Doc/IsarImplementation/Logic.thy | file | annotate | diff | revisions | |

src/Doc/Ref/document/thm.tex | file | annotate | diff | revisions | |

src/HOL/Tools/reflection.ML | file | annotate | diff | revisions |

1.1 --- a/src/Doc/IsarImplementation/Logic.thy Thu Jun 13 17:40:58 2013 +0200 1.2 +++ b/src/Doc/IsarImplementation/Logic.thy Sat Jun 15 16:55:49 2013 +0200 1.3 @@ -523,9 +523,9 @@ 1.4 \infer[@{text "(assume)"}]{@{text "A \<turnstile> A"}}{} 1.5 \] 1.6 \[ 1.7 - \infer[@{text "(\<And>\<hyphen>intro)"}]{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}{@{text "\<Gamma> \<turnstile> b[x]"} & @{text "x \<notin> \<Gamma>"}} 1.8 + \infer[@{text "(\<And>\<hyphen>intro)"}]{@{text "\<Gamma> \<turnstile> \<And>x. B[x]"}}{@{text "\<Gamma> \<turnstile> B[x]"} & @{text "x \<notin> \<Gamma>"}} 1.9 \qquad 1.10 - \infer[@{text "(\<And>\<hyphen>elim)"}]{@{text "\<Gamma> \<turnstile> b[a]"}}{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}} 1.11 + \infer[@{text "(\<And>\<hyphen>elim)"}]{@{text "\<Gamma> \<turnstile> B[a]"}}{@{text "\<Gamma> \<turnstile> \<And>x. B[x]"}} 1.12 \] 1.13 \[ 1.14 \infer[@{text "(\<Longrightarrow>\<hyphen>intro)"}]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}} 1.15 @@ -1210,4 +1210,73 @@ 1.16 \end{description} 1.17 *} 1.18 1.19 + 1.20 +section {* Proof terms \label{sec:proof-terms} *} 1.21 + 1.22 +text {* The Isabelle/Pure inference kernel can record the proof of 1.23 + each theorem as a proof term that contains all logical inferences in 1.24 + detail. Rule composition by resolution (\secref{sec:obj-rules}) and 1.25 + type-class reasoning is broken down to primitive rules of the 1.26 + logical framework. The proof term can be inspected by a separate 1.27 + proof-checker, for example. 1.28 + 1.29 + According to the well-known \emph{Curry-Howard isomorphism}, a proof 1.30 + can be viewed as a @{text "\<lambda>"}-term. Following this idea, proofs in 1.31 + Isabelle are internally represented by a datatype similar to the one 1.32 + for terms described in \secref{sec:terms}. On top of these 1.33 + syntactic terms, two more layers of @{text "\<lambda>"}-calculus are added, 1.34 + which correspond to @{text "\<And>x :: \<alpha>. B x"} and @{text "A \<Longrightarrow> B"} 1.35 + according to the propositions-as-types principle. The resulting 1.36 + 3-level @{text "\<lambda>"}-calculus resembles ``@{text "\<lambda>HOL"}'' in the 1.37 + more abstract setting of Pure Type Systems (PTS) 1.38 + \cite{Barendregt-Geuvers:2001}, if some fine points like schematic 1.39 + polymorphism and type classes are ignored. 1.40 + 1.41 + \medskip\emph{Proof abstractions} of the form @{text "\<^bold>\<lambda>x :: \<alpha>. prf"} 1.42 + or @{text "\<^bold>\<lambda>p : A. prf"} correspond to introduction of @{text 1.43 + "\<And>"}/@{text "\<Longrightarrow>"}, and \emph{proof applications} of the form @{text 1.44 + "p \<cdot> t"} or @{text "p \<bullet> q"} correspond to elimination of @{text 1.45 + "\<And>"}/@{text "\<Longrightarrow>"}. Actual types @{text "\<alpha>"}, propositions @{text 1.46 + "A"}, and terms @{text "t"} might be suppressed and reconstructed 1.47 + from the overall proof term. 1.48 + 1.49 + \medskip Various atomic proofs indicate special situations within 1.50 + the proof construction as follows. 1.51 + 1.52 + A \emph{bound proof variable} is a natural number @{text "b"} that 1.53 + acts as de-Bruijn index for proof term abstractions. 1.54 + 1.55 + A \emph{minimal proof} ``@{text "?"}'' is a dummy proof term. This 1.56 + indicates some unrecorded part of the proof. 1.57 + 1.58 + @{text "Hyp A"} refers to some pending hypothesis by giving its 1.59 + proposition. This indicates an open context of implicit hypotheses, 1.60 + similar to loose bound variables or free variables within a term 1.61 + (\secref{sec:terms}). 1.62 + 1.63 + An \emph{axiom} or \emph{oracle} @{text "a : A[\<^vec>\<tau>]"} refers 1.64 + some postulated @{text "proof constant"}, which is subject to 1.65 + schematic polymorphism of theory content, and the particular type 1.66 + instantiation may be given explicitly. The vector of types @{text 1.67 + "\<^vec>\<tau>"} refers to the schematic type variables in the generic 1.68 + proposition @{text "A"} in canonical order. 1.69 + 1.70 + A \emph{proof promise} @{text "a : A[\<^vec>\<tau>]"} is a placeholder 1.71 + for some proof of polymorphic proposition @{text "A"}, with explicit 1.72 + type instantiation as given by the vector @{text "\<^vec>\<tau>"}, as 1.73 + above. Unlike axioms or oracles, proof promises may be 1.74 + \emph{fulfilled} eventually, by substituting @{text "a"} by some 1.75 + particular proof @{text "q"} at the corresponding type instance. 1.76 + This acts like Hindley-Milner @{text "let"}-polymorphism: a generic 1.77 + local proof definition may get used at different type instances, and 1.78 + is replaced by the concrete instance eventually. 1.79 + 1.80 + A \emph{named theorem} wraps up some concrete proof as a closed 1.81 + formal entity, in the manner of constant definitions for proof 1.82 + terms. The \emph{proof body} of such boxed theorems involves some 1.83 + digest about oracles and promises occurring in the original proof. 1.84 + This allows the inference kernel to manage this critical information 1.85 + without the full overhead of explicit proof terms. 1.86 +*} 1.87 + 1.88 end

2.1 --- a/src/Doc/Ref/document/thm.tex Thu Jun 13 17:40:58 2013 +0200 2.2 +++ b/src/Doc/Ref/document/thm.tex Sat Jun 15 16:55:49 2013 +0200 2.3 @@ -2,20 +2,6 @@ 2.4 \chapter{Theorems and Forward Proof} 2.5 2.6 \section{Proof terms}\label{sec:proofObjects} 2.7 -\index{proof terms|(} Isabelle can record the full meta-level proof of each 2.8 -theorem. The proof term contains all logical inferences in detail. 2.9 -%while 2.10 -%omitting bookkeeping steps that have no logical meaning to an outside 2.11 -%observer. Rewriting steps are recorded in similar detail as the output of 2.12 -%simplifier tracing. 2.13 -Resolution and rewriting steps are broken down to primitive rules of the 2.14 -meta-logic. The proof term can be inspected by a separate proof-checker, 2.15 -for example. 2.16 - 2.17 -According to the well-known {\em Curry-Howard isomorphism}, a proof can 2.18 -be viewed as a $\lambda$-term. Following this idea, proofs 2.19 -in Isabelle are internally represented by a datatype similar to the one for 2.20 -terms described in \S\ref{sec:terms}. 2.21 \begin{ttbox} 2.22 infix 8 % %%; 2.23