more on proof terms;
authorwenzelm
Sat Jun 15 16:55:49 2013 +0200 (2013-06-15)
changeset 52407e4662afb3483
parent 52406 1e57c3c4e05c
child 52408 fa2dc6c6c94f
more on proof terms;
src/Doc/IsarImplementation/Logic.thy
src/Doc/Ref/document/thm.tex
src/HOL/Tools/reflection.ML
     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