1.1 --- a/src/Doc/IsarImplementation/Logic.thy Sat Jun 15 16:55:49 2013 +0200
1.2 +++ b/src/Doc/IsarImplementation/Logic.thy Sat Jun 15 21:01:07 2013 +0200
1.3 @@ -378,8 +378,9 @@
1.4
1.5 \item Type @{ML_type term} represents de-Bruijn terms, with comments
1.6 in abstractions, and explicitly named free variables and constants;
1.7 - this is a datatype with constructors @{ML Bound}, @{ML Free}, @{ML
1.8 - Var}, @{ML Const}, @{ML Abs}, @{ML_op "$"}.
1.9 + this is a datatype with constructors @{index_ML Bound}, @{index_ML
1.10 + Free}, @{index_ML Var}, @{index_ML Const}, @{index_ML Abs},
1.11 + @{index_ML_op "$"}.
1.12
1.13 \item @{text "t"}~@{ML_text aconv}~@{text "u"} checks @{text
1.14 "\<alpha>"}-equivalence of two terms. This is the basic equality relation
1.15 @@ -554,10 +555,10 @@
1.16 "\<lambda>"}-terms representing the underlying proof objects. Proof terms
1.17 are irrelevant in the Pure logic, though; they cannot occur within
1.18 propositions. The system provides a runtime option to record
1.19 - explicit proof terms for primitive inferences. Thus all three
1.20 - levels of @{text "\<lambda>"}-calculus become explicit: @{text "\<Rightarrow>"} for
1.21 - terms, and @{text "\<And>/\<Longrightarrow>"} for proofs (cf.\
1.22 - \cite{Berghofer-Nipkow:2000:TPHOL}).
1.23 + explicit proof terms for primitive inferences, see also
1.24 + \secref{sec:proof-terms}. Thus all three levels of @{text
1.25 + "\<lambda>"}-calculus become explicit: @{text "\<Rightarrow>"} for terms, and @{text
1.26 + "\<And>/\<Longrightarrow>"} for proofs (cf.\ \cite{Berghofer-Nipkow:2000:TPHOL}).
1.27
1.28 Observe that locally fixed parameters (as in @{text
1.29 "\<And>\<hyphen>intro"}) need not be recorded in the hypotheses, because
1.30 @@ -647,7 +648,6 @@
1.31 \end{mldecls}
1.32 \begin{mldecls}
1.33 @{index_ML_type thm} \\
1.34 - @{index_ML proofs: "int Unsynchronized.ref"} \\
1.35 @{index_ML Thm.peek_status: "thm -> {oracle: bool, unfinished: bool, failed: bool}"} \\
1.36 @{index_ML Thm.transfer: "theory -> thm -> thm"} \\
1.37 @{index_ML Thm.assume: "cterm -> thm"} \\
1.38 @@ -721,12 +721,6 @@
1.39 Every @{ML_type thm} value contains a sliding back-reference to the
1.40 enclosing theory, cf.\ \secref{sec:context-theory}.
1.41
1.42 - \item @{ML proofs} specifies the detail of proof recording within
1.43 - @{ML_type thm} values: @{ML 0} records only the names of oracles,
1.44 - @{ML 1} records oracle names and propositions, @{ML 2} additionally
1.45 - records full proof terms. Officially named theorems that contribute
1.46 - to a result are recorded in any case.
1.47 -
1.48 \item @{ML Thm.transfer}~@{text "thy thm"} transfers the given
1.49 theorem to a \emph{larger} theory, see also \secref{sec:context}.
1.50 This formal adjustment of the background context has no logical
1.51 @@ -1279,4 +1273,45 @@
1.52 without the full overhead of explicit proof terms.
1.53 *}
1.54
1.55 +text %mlref {*
1.56 + \begin{mldecls}
1.57 + @{index_ML_type proof} \\
1.58 + @{index_ML_type proof_body} \\
1.59 + @{index_ML proofs: "int Unsynchronized.ref"} \\
1.60 + \end{mldecls}
1.61 +
1.62 + \begin{description}
1.63 +
1.64 + \item Type @{ML_type proof} represents proof terms; this is a
1.65 + datatype with constructors @{index_ML Abst}, @{index_ML AbsP},
1.66 + @{index_ML_op "%"}, @{index_ML_op "%%"}, @{index_ML PBound},
1.67 + @{index_ML MinProof}, @{index_ML Hyp}, @{index_ML PAxm}, @{index_ML
1.68 + Oracle}, @{index_ML Promise}, @{index_ML PThm} as explained above.
1.69 +
1.70 + \item Type @{ML_type proof_body} represents the nested proof
1.71 + information of a named theorem, consisting of a digest of oracles
1.72 + and named theorem over some proof term. The digest only covers the
1.73 + directly visible part of the proof: in order to get the full
1.74 + information, the implicit graph of nested theorems needs to be
1.75 + traversed (e.g.\ using @{ML Proofterm.fold_body_thms}).
1.76 +
1.77 + \item @{ML Thm.proof_of}~@{text "thm"} and @{ML
1.78 + Thm.proof_body_of}~@{text "thm"} produce the proof term or proof
1.79 + body (with digest of oracles and theorems) from a given theorem.
1.80 + Note that this involves a full join of internal futures that fulfill
1.81 + pending proof promises, and thus disrupts the natural bottom-up
1.82 + construction of proofs by introducing dynamic ad-hoc dependencies.
1.83 + Parallel performance may suffer by inspecting proof terms at
1.84 + run-time.
1.85 +
1.86 + \item @{ML proofs} specifies the detail of proof recording within
1.87 + @{ML_type thm} values produced by the inference kernel: @{ML 0}
1.88 + records only the names of oracles, @{ML 1} records oracle names and
1.89 + propositions, @{ML 2} additionally records full proof terms.
1.90 + Officially named theorems that contribute to a result are recorded
1.91 + in any case.
1.92 +
1.93 + \end{description}
1.94 +*}
1.95 +
1.96 end
2.1 --- a/src/Doc/Ref/document/thm.tex Sat Jun 15 16:55:49 2013 +0200
2.2 +++ b/src/Doc/Ref/document/thm.tex Sat Jun 15 21:01:07 2013 +0200
2.3 @@ -2,58 +2,7 @@
2.4 \chapter{Theorems and Forward Proof}
2.5
2.6 \section{Proof terms}\label{sec:proofObjects}
2.7 -\begin{ttbox}
2.8 -infix 8 % %%;
2.9
2.10 -datatype proof =
2.11 - PBound of int
2.12 - | Abst of string * typ option * proof
2.13 - | AbsP of string * term option * proof
2.14 - | op % of proof * term option
2.15 - | op %% of proof * proof
2.16 - | Hyp of term
2.17 - | PThm of (string * (string * string list) list) *
2.18 - proof * term * typ list option
2.19 - | PAxm of string * term * typ list option
2.20 - | Oracle of string * term * typ list option
2.21 - | MinProof of proof list;
2.22 -\end{ttbox}
2.23 -
2.24 -\begin{ttdescription}
2.25 -\item[\ttindexbold{Abst} ($a$, $\tau$, $prf$)] is the abstraction over
2.26 -a {\it term variable} of type $\tau$ in the body $prf$. Logically, this
2.27 -corresponds to $\bigwedge$ introduction. The name $a$ is used only for
2.28 -parsing and printing.
2.29 -\item[\ttindexbold{AbsP} ($a$, $\varphi$, $prf$)] is the abstraction
2.30 -over a {\it proof variable} standing for a proof of proposition $\varphi$
2.31 -in the body $prf$. This corresponds to $\Longrightarrow$ introduction.
2.32 -\item[$prf$ \% $t$] \index{\%@{\tt\%}|bold}
2.33 -is the application of proof $prf$ to term $t$
2.34 -which corresponds to $\bigwedge$ elimination.
2.35 -\item[$prf@1$ \%\% $prf@2$] \index{\%\%@{\tt\%\%}|bold}
2.36 -is the application of proof $prf@1$ to
2.37 -proof $prf@2$ which corresponds to $\Longrightarrow$ elimination.
2.38 -\item[\ttindexbold{PBound} $i$] is a {\em proof variable} with de Bruijn
2.39 -\cite{debruijn72} index $i$.
2.40 -\item[\ttindexbold{Hyp} $\varphi$] corresponds to the use of a meta level
2.41 -hypothesis $\varphi$.
2.42 -\item[\ttindexbold{PThm} (($name$, $tags$), $prf$, $\varphi$, $\overline{\tau}$)]
2.43 -stands for a pre-proved theorem, where $name$ is the name of the theorem,
2.44 -$prf$ is its actual proof, $\varphi$ is the proven proposition,
2.45 -and $\overline{\tau}$ is
2.46 -a type assignment for the type variables occurring in the proposition.
2.47 -\item[\ttindexbold{PAxm} ($name$, $\varphi$, $\overline{\tau}$)]
2.48 -corresponds to the use of an axiom with name $name$ and proposition
2.49 -$\varphi$, where $\overline{\tau}$ is a type assignment for the type
2.50 -variables occurring in the proposition.
2.51 -\item[\ttindexbold{Oracle} ($name$, $\varphi$, $\overline{\tau}$)]
2.52 -denotes the invocation of an oracle with name $name$ which produced
2.53 -a proposition $\varphi$, where $\overline{\tau}$ is a type assignment
2.54 -for the type variables occurring in the proposition.
2.55 -\item[\ttindexbold{MinProof} $prfs$]
2.56 -represents a {\em minimal proof} where $prfs$ is a list of theorems,
2.57 -axioms or oracles.
2.58 -\end{ttdescription}
2.59 Note that there are no separate constructors
2.60 for abstraction and application on the level of {\em types}, since
2.61 instantiation of type variables is accomplished via the type assignments
2.62 @@ -73,15 +22,6 @@
2.63 The theorem is applied to two (implicit) term arguments, which correspond
2.64 to the two variables occurring in its proposition.
2.65
2.66 -Isabelle's inference kernel can produce proof objects with different
2.67 -levels of detail. This is controlled via the global reference variable
2.68 -\ttindexbold{proofs}:
2.69 -\begin{ttdescription}
2.70 -\item[proofs := 0;] only record uses of oracles
2.71 -\item[proofs := 1;] record uses of oracles as well as dependencies
2.72 - on other theorems and axioms
2.73 -\item[proofs := 2;] record inferences in full detail
2.74 -\end{ttdescription}
2.75 Reconstruction and checking of proofs as described in \S\ref{sec:reconstruct_proofs}
2.76 will not work for proofs constructed with {\tt proofs} set to
2.77 {\tt 0} or {\tt 1}.
3.1 --- a/src/Doc/antiquote_setup.ML Sat Jun 15 16:55:49 2013 +0200
3.2 +++ b/src/Doc/antiquote_setup.ML Sat Jun 15 21:01:07 2013 +0200
3.3 @@ -19,6 +19,8 @@
3.4 val clean_string = translate
3.5 (fn "_" => "\\_"
3.6 | "#" => "\\#"
3.7 + | "$" => "\\$"
3.8 + | "%" => "\\%"
3.9 | "<" => "$<$"
3.10 | ">" => "$>$"
3.11 | "{" => "\\{"