--- a/src/Doc/IsarImplementation/Logic.thy Sat Jun 15 16:55:49 2013 +0200
+++ b/src/Doc/IsarImplementation/Logic.thy Sat Jun 15 21:01:07 2013 +0200
@@ -378,8 +378,9 @@
\item Type @{ML_type term} represents de-Bruijn terms, with comments
in abstractions, and explicitly named free variables and constants;
- this is a datatype with constructors @{ML Bound}, @{ML Free}, @{ML
- Var}, @{ML Const}, @{ML Abs}, @{ML_op "$"}.
+ this is a datatype with constructors @{index_ML Bound}, @{index_ML
+ Free}, @{index_ML Var}, @{index_ML Const}, @{index_ML Abs},
+ @{index_ML_op "$"}.
\item @{text "t"}~@{ML_text aconv}~@{text "u"} checks @{text
"\<alpha>"}-equivalence of two terms. This is the basic equality relation
@@ -554,10 +555,10 @@
"\<lambda>"}-terms representing the underlying proof objects. Proof terms
are irrelevant in the Pure logic, though; they cannot occur within
propositions. The system provides a runtime option to record
- explicit proof terms for primitive inferences. Thus all three
- levels of @{text "\<lambda>"}-calculus become explicit: @{text "\<Rightarrow>"} for
- terms, and @{text "\<And>/\<Longrightarrow>"} for proofs (cf.\
- \cite{Berghofer-Nipkow:2000:TPHOL}).
+ explicit proof terms for primitive inferences, see also
+ \secref{sec:proof-terms}. Thus all three levels of @{text
+ "\<lambda>"}-calculus become explicit: @{text "\<Rightarrow>"} for terms, and @{text
+ "\<And>/\<Longrightarrow>"} for proofs (cf.\ \cite{Berghofer-Nipkow:2000:TPHOL}).
Observe that locally fixed parameters (as in @{text
"\<And>\<hyphen>intro"}) need not be recorded in the hypotheses, because
@@ -647,7 +648,6 @@
\end{mldecls}
\begin{mldecls}
@{index_ML_type thm} \\
- @{index_ML proofs: "int Unsynchronized.ref"} \\
@{index_ML Thm.peek_status: "thm -> {oracle: bool, unfinished: bool, failed: bool}"} \\
@{index_ML Thm.transfer: "theory -> thm -> thm"} \\
@{index_ML Thm.assume: "cterm -> thm"} \\
@@ -721,12 +721,6 @@
Every @{ML_type thm} value contains a sliding back-reference to the
enclosing theory, cf.\ \secref{sec:context-theory}.
- \item @{ML proofs} specifies the detail of proof recording within
- @{ML_type thm} values: @{ML 0} records only the names of oracles,
- @{ML 1} records oracle names and propositions, @{ML 2} additionally
- records full proof terms. Officially named theorems that contribute
- to a result are recorded in any case.
-
\item @{ML Thm.transfer}~@{text "thy thm"} transfers the given
theorem to a \emph{larger} theory, see also \secref{sec:context}.
This formal adjustment of the background context has no logical
@@ -1279,4 +1273,45 @@
without the full overhead of explicit proof terms.
*}
+text %mlref {*
+ \begin{mldecls}
+ @{index_ML_type proof} \\
+ @{index_ML_type proof_body} \\
+ @{index_ML proofs: "int Unsynchronized.ref"} \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item Type @{ML_type proof} represents proof terms; this is a
+ datatype with constructors @{index_ML Abst}, @{index_ML AbsP},
+ @{index_ML_op "%"}, @{index_ML_op "%%"}, @{index_ML PBound},
+ @{index_ML MinProof}, @{index_ML Hyp}, @{index_ML PAxm}, @{index_ML
+ Oracle}, @{index_ML Promise}, @{index_ML PThm} as explained above.
+
+ \item Type @{ML_type proof_body} represents the nested proof
+ information of a named theorem, consisting of a digest of oracles
+ and named theorem over some proof term. The digest only covers the
+ directly visible part of the proof: in order to get the full
+ information, the implicit graph of nested theorems needs to be
+ traversed (e.g.\ using @{ML Proofterm.fold_body_thms}).
+
+ \item @{ML Thm.proof_of}~@{text "thm"} and @{ML
+ Thm.proof_body_of}~@{text "thm"} produce the proof term or proof
+ body (with digest of oracles and theorems) from a given theorem.
+ Note that this involves a full join of internal futures that fulfill
+ pending proof promises, and thus disrupts the natural bottom-up
+ construction of proofs by introducing dynamic ad-hoc dependencies.
+ Parallel performance may suffer by inspecting proof terms at
+ run-time.
+
+ \item @{ML proofs} specifies the detail of proof recording within
+ @{ML_type thm} values produced by the inference kernel: @{ML 0}
+ records only the names of oracles, @{ML 1} records oracle names and
+ propositions, @{ML 2} additionally records full proof terms.
+ Officially named theorems that contribute to a result are recorded
+ in any case.
+
+ \end{description}
+*}
+
end
--- a/src/Doc/Ref/document/thm.tex Sat Jun 15 16:55:49 2013 +0200
+++ b/src/Doc/Ref/document/thm.tex Sat Jun 15 21:01:07 2013 +0200
@@ -2,58 +2,7 @@
\chapter{Theorems and Forward Proof}
\section{Proof terms}\label{sec:proofObjects}
-\begin{ttbox}
-infix 8 % %%;
-datatype proof =
- PBound of int
- | Abst of string * typ option * proof
- | AbsP of string * term option * proof
- | op % of proof * term option
- | op %% of proof * proof
- | Hyp of term
- | PThm of (string * (string * string list) list) *
- proof * term * typ list option
- | PAxm of string * term * typ list option
- | Oracle of string * term * typ list option
- | MinProof of proof list;
-\end{ttbox}
-
-\begin{ttdescription}
-\item[\ttindexbold{Abst} ($a$, $\tau$, $prf$)] is the abstraction over
-a {\it term variable} of type $\tau$ in the body $prf$. Logically, this
-corresponds to $\bigwedge$ introduction. The name $a$ is used only for
-parsing and printing.
-\item[\ttindexbold{AbsP} ($a$, $\varphi$, $prf$)] is the abstraction
-over a {\it proof variable} standing for a proof of proposition $\varphi$
-in the body $prf$. This corresponds to $\Longrightarrow$ introduction.
-\item[$prf$ \% $t$] \index{\%@{\tt\%}|bold}
-is the application of proof $prf$ to term $t$
-which corresponds to $\bigwedge$ elimination.
-\item[$prf@1$ \%\% $prf@2$] \index{\%\%@{\tt\%\%}|bold}
-is the application of proof $prf@1$ to
-proof $prf@2$ which corresponds to $\Longrightarrow$ elimination.
-\item[\ttindexbold{PBound} $i$] is a {\em proof variable} with de Bruijn
-\cite{debruijn72} index $i$.
-\item[\ttindexbold{Hyp} $\varphi$] corresponds to the use of a meta level
-hypothesis $\varphi$.
-\item[\ttindexbold{PThm} (($name$, $tags$), $prf$, $\varphi$, $\overline{\tau}$)]
-stands for a pre-proved theorem, where $name$ is the name of the theorem,
-$prf$ is its actual proof, $\varphi$ is the proven proposition,
-and $\overline{\tau}$ is
-a type assignment for the type variables occurring in the proposition.
-\item[\ttindexbold{PAxm} ($name$, $\varphi$, $\overline{\tau}$)]
-corresponds to the use of an axiom with name $name$ and proposition
-$\varphi$, where $\overline{\tau}$ is a type assignment for the type
-variables occurring in the proposition.
-\item[\ttindexbold{Oracle} ($name$, $\varphi$, $\overline{\tau}$)]
-denotes the invocation of an oracle with name $name$ which produced
-a proposition $\varphi$, where $\overline{\tau}$ is a type assignment
-for the type variables occurring in the proposition.
-\item[\ttindexbold{MinProof} $prfs$]
-represents a {\em minimal proof} where $prfs$ is a list of theorems,
-axioms or oracles.
-\end{ttdescription}
Note that there are no separate constructors
for abstraction and application on the level of {\em types}, since
instantiation of type variables is accomplished via the type assignments
@@ -73,15 +22,6 @@
The theorem is applied to two (implicit) term arguments, which correspond
to the two variables occurring in its proposition.
-Isabelle's inference kernel can produce proof objects with different
-levels of detail. This is controlled via the global reference variable
-\ttindexbold{proofs}:
-\begin{ttdescription}
-\item[proofs := 0;] only record uses of oracles
-\item[proofs := 1;] record uses of oracles as well as dependencies
- on other theorems and axioms
-\item[proofs := 2;] record inferences in full detail
-\end{ttdescription}
Reconstruction and checking of proofs as described in \S\ref{sec:reconstruct_proofs}
will not work for proofs constructed with {\tt proofs} set to
{\tt 0} or {\tt 1}.
--- a/src/Doc/antiquote_setup.ML Sat Jun 15 16:55:49 2013 +0200
+++ b/src/Doc/antiquote_setup.ML Sat Jun 15 21:01:07 2013 +0200
@@ -19,6 +19,8 @@
val clean_string = translate
(fn "_" => "\\_"
| "#" => "\\#"
+ | "$" => "\\$"
+ | "%" => "\\%"
| "<" => "$<$"
| ">" => "$>$"
| "{" => "\\{"