summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sat, 15 Jun 2013 21:01:07 +0200 | |

changeset 52408 | fa2dc6c6c94f |

parent 52407 | e4662afb3483 |

child 52409 | 47c62377be78 |

updated operations on proof terms;

--- 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}.