--- a/doc-src/Ref/thm.tex Mon Aug 27 17:11:55 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,636 +0,0 @@
-
-\chapter{Theorems and Forward Proof}
-\index{theorems|(}
-
-Theorems, which represent the axioms, theorems and rules of
-object-logics, have type \mltydx{thm}. This chapter describes
-operations that join theorems in forward proof. Most theorem
-operations are intended for advanced applications, such as programming
-new proof procedures.
-
-
-\subsection{Instantiating unknowns in a theorem} \label{sec:instantiate}
-\index{instantiation}
-\begin{alltt}\footnotesize
-read_instantiate : (string*string) list -> thm -> thm
-read_instantiate_sg : Sign.sg -> (string*string) list -> thm -> thm
-cterm_instantiate : (cterm*cterm) list -> thm -> thm
-instantiate' : ctyp option list -> cterm option list -> thm -> thm
-\end{alltt}
-These meta-rules instantiate type and term unknowns in a theorem. They are
-occasionally useful. They can prevent difficulties with higher-order
-unification, and define specialized versions of rules.
-\begin{ttdescription}
-\item[\ttindexbold{read_instantiate} {\it insts} {\it thm}]
-processes the instantiations {\it insts} and instantiates the rule~{\it
-thm}. The processing of instantiations is described
-in \S\ref{res_inst_tac}, under {\tt res_inst_tac}.
-
-Use {\tt res_inst_tac}, not {\tt read_instantiate}, to instantiate a rule
-and refine a particular subgoal. The tactic allows instantiation by the
-subgoal's parameters, and reads the instantiations using the signature
-associated with the proof state.
-
-Use {\tt read_instantiate_sg} below if {\it insts\/} appears to be treated
-incorrectly.
-
-\item[\ttindexbold{read_instantiate_sg} {\it sg} {\it insts} {\it thm}]
- is like \texttt{read_instantiate {\it insts}~{\it thm}}, but it reads
- the instantiations under signature~{\it sg}. This is necessary to
- instantiate a rule from a general theory, such as first-order logic,
- using the notation of some specialized theory. Use the function {\tt
- sign_of} to get a theory's signature.
-
-\item[\ttindexbold{cterm_instantiate} {\it ctpairs} {\it thm}]
-is similar to {\tt read_instantiate}, but the instantiations are provided
-as pairs of certified terms, not as strings to be read.
-
-\item[\ttindexbold{instantiate'} {\it ctyps} {\it cterms} {\it thm}]
- instantiates {\it thm} according to the positional arguments {\it
- ctyps} and {\it cterms}. Counting from left to right, schematic
- variables $?x$ are either replaced by $t$ for any argument
- \texttt{Some\(\;t\)}, or left unchanged in case of \texttt{None} or
- if the end of the argument list is encountered. Types are
- instantiated before terms.
-
-\end{ttdescription}
-
-
-\subsection{Miscellaneous forward rules}\label{MiscellaneousForwardRules}
-\index{theorems!standardizing}
-\begin{ttbox}
-standard : thm -> thm
-zero_var_indexes : thm -> thm
-make_elim : thm -> thm
-rule_by_tactic : tactic -> thm -> thm
-rotate_prems : int -> thm -> thm
-permute_prems : int -> int -> thm -> thm
-rearrange_prems : int list -> thm -> thm
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{standard} $thm$] puts $thm$ into the standard form
- of object-rules. It discharges all meta-assumptions, replaces free
- variables by schematic variables, renames schematic variables to
- have subscript zero, also strips outer (meta) quantifiers and
- removes dangling sort hypotheses.
-
-\item[\ttindexbold{zero_var_indexes} $thm$]
-makes all schematic variables have subscript zero, renaming them to avoid
-clashes.
-
-\item[\ttindexbold{make_elim} $thm$]
-\index{rules!converting destruction to elimination}
-converts $thm$, which should be a destruction rule of the form
-$\List{P@1;\ldots;P@m}\Imp
-Q$, to the elimination rule $\List{P@1; \ldots; P@m; Q\Imp R}\Imp R$. This
-is the basis for destruct-resolution: {\tt dresolve_tac}, etc.
-
-\item[\ttindexbold{rule_by_tactic} {\it tac} {\it thm}]
- applies {\it tac\/} to the {\it thm}, freezing its variables first, then
- yields the proof state returned by the tactic. In typical usage, the
- {\it thm\/} represents an instance of a rule with several premises, some
- with contradictory assumptions (because of the instantiation). The
- tactic proves those subgoals and does whatever else it can, and returns
- whatever is left.
-
-\item[\ttindexbold{rotate_prems} $k$ $thm$] rotates the premises of $thm$ to
- the left by~$k$ positions (to the right if $k<0$). It simply calls
- \texttt{permute_prems}, below, with $j=0$. Used with
- \texttt{eresolve_tac}\index{*eresolve_tac!on other than first premise}, it
- gives the effect of applying the tactic to some other premise of $thm$ than
- the first.
-
-\item[\ttindexbold{permute_prems} $j$ $k$ $thm$] rotates the premises of $thm$
- leaving the first $j$ premises unchanged. It
- requires $0\leq j\leq n$, where $n$ is the number of premises. If $k$ is
- positive then it rotates the remaining $n-j$ premises to the left; if $k$ is
- negative then it rotates the premises to the right.
-
-\item[\ttindexbold{rearrange_prems} $ps$ $thm$] permutes the premises of $thm$
- where the value at the $i$-th position (counting from $0$) in the list $ps$
- gives the position within the original thm to be transferred to position $i$.
- Any remaining trailing positions are left unchanged.
-\end{ttdescription}
-
-
-\subsection{Taking a theorem apart}
-\index{theorems!taking apart}
-\index{flex-flex constraints}
-\begin{ttbox}
-cprop_of : thm -> cterm
-concl_of : thm -> term
-prems_of : thm -> term list
-cprems_of : thm -> cterm list
-nprems_of : thm -> int
-tpairs_of : thm -> (term*term) list
-theory_of_thm : thm -> theory
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{cprop_of} $thm$] returns the statement of $thm$ as
- a certified term.
-
-\item[\ttindexbold{concl_of} $thm$] returns the conclusion of $thm$ as
- a term.
-
-\item[\ttindexbold{prems_of} $thm$] returns the premises of $thm$ as a
- list of terms.
-
-\item[\ttindexbold{cprems_of} $thm$] returns the premises of $thm$ as
- a list of certified terms.
-
-\item[\ttindexbold{nprems_of} $thm$]
-returns the number of premises in $thm$, and is equivalent to {\tt
- length~(prems_of~$thm$)}.
-
-\item[\ttindexbold{tpairs_of} $thm$] returns the flex-flex constraints
- of $thm$.
-
-\item[\ttindexbold{theory_of_thm} $thm$] returns the theory associated
- with $thm$. Note that this does a lookup in Isabelle's global
- database of loaded theories.
-
-\end{ttdescription}
-
-
-\subsection{*Sort hypotheses} \label{sec:sort-hyps}
-\index{sort hypotheses}
-\begin{ttbox}
-strip_shyps : thm -> thm
-strip_shyps_warning : thm -> thm
-\end{ttbox}
-
-Isabelle's type variables are decorated with sorts, constraining them to
-certain ranges of types. This has little impact when sorts only serve for
-syntactic classification of types --- for example, FOL distinguishes between
-terms and other types. But when type classes are introduced through axioms,
-this may result in some sorts becoming {\em empty\/}: where one cannot exhibit
-a type belonging to it because certain sets of axioms are unsatisfiable.
-
-If a theorem contains a type variable that is constrained by an empty
-sort, then that theorem has no instances. It is basically an instance
-of {\em ex falso quodlibet}. But what if it is used to prove another
-theorem that no longer involves that sort? The latter theorem holds
-only if under an additional non-emptiness assumption.
-
-Therefore, Isabelle's theorems carry around sort hypotheses. The {\tt
-shyps} field is a list of sorts occurring in type variables in the current
-{\tt prop} and {\tt hyps} fields. It may also includes sorts used in the
-theorem's proof that no longer appear in the {\tt prop} or {\tt hyps}
-fields --- so-called {\em dangling\/} sort constraints. These are the
-critical ones, asserting non-emptiness of the corresponding sorts.
-
-Isabelle automatically removes extraneous sorts from the {\tt shyps} field at
-the end of a proof, provided that non-emptiness can be established by looking
-at the theorem's signature: from the {\tt classes} and {\tt arities}
-information. This operation is performed by \texttt{strip_shyps} and
-\texttt{strip_shyps_warning}.
-
-\begin{ttdescription}
-
-\item[\ttindexbold{strip_shyps} $thm$] removes any extraneous sort hypotheses
- that can be witnessed from the type signature.
-
-\item[\ttindexbold{strip_shyps_warning}] is like \texttt{strip_shyps}, but
- issues a warning message of any pending sort hypotheses that do not have a
- (syntactic) witness.
-
-\end{ttdescription}
-
-
-\subsection{Tracing flags for unification}
-\index{tracing!of unification}
-\begin{ttbox}
-Unify.trace_simp : bool ref \hfill\textbf{initially false}
-Unify.trace_types : bool ref \hfill\textbf{initially false}
-Unify.trace_bound : int ref \hfill\textbf{initially 10}
-Unify.search_bound : int ref \hfill\textbf{initially 20}
-\end{ttbox}
-Tracing the search may be useful when higher-order unification behaves
-unexpectedly. Letting {\tt res_inst_tac} circumvent the problem is easier,
-though.
-\begin{ttdescription}
-\item[set Unify.trace_simp;]
-causes tracing of the simplification phase.
-
-\item[set Unify.trace_types;]
-generates warnings of incompleteness, when unification is not considering
-all possible instantiations of type unknowns.
-
-\item[Unify.trace_bound := $n$;]
-causes unification to print tracing information once it reaches depth~$n$.
-Use $n=0$ for full tracing. At the default value of~10, tracing
-information is almost never printed.
-
-\item[Unify.search_bound := $n$;] prevents unification from
- searching past the depth~$n$. Because of this bound, higher-order
- unification cannot return an infinite sequence, though it can return
- an exponentially long one. The search rarely approaches the default value
- of~20. If the search is cut off, unification prints a warning
- \texttt{Unification bound exceeded}.
-\end{ttdescription}
-
-
-\section{*Primitive meta-level inference rules}
-\index{meta-rules|(}
-
-\subsection{Logical equivalence rules}
-\index{meta-equality}
-\begin{ttbox}
-equal_intr : thm -> thm -> thm
-equal_elim : thm -> thm -> thm
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{equal_intr} $thm@1$ $thm@2$]
-applies $({\equiv}I)$ to $thm@1$ and~$thm@2$. It maps the premises~$\psi$
-and~$\phi$ to the conclusion~$\phi\equiv\psi$; the assumptions are those of
-the first premise with~$\phi$ removed, plus those of
-the second premise with~$\psi$ removed.
-
-\item[\ttindexbold{equal_elim} $thm@1$ $thm@2$]
-applies $({\equiv}E)$ to $thm@1$ and~$thm@2$. It maps the premises
-$\phi\equiv\psi$ and $\phi$ to the conclusion~$\psi$.
-\end{ttdescription}
-
-
-\subsection{Equality rules}
-\index{meta-equality}
-\begin{ttbox}
-reflexive : cterm -> thm
-symmetric : thm -> thm
-transitive : thm -> thm -> thm
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{reflexive} $ct$]
-makes the theorem \(ct\equiv ct\).
-
-\item[\ttindexbold{symmetric} $thm$]
-maps the premise $a\equiv b$ to the conclusion $b\equiv a$.
-
-\item[\ttindexbold{transitive} $thm@1$ $thm@2$]
-maps the premises $a\equiv b$ and $b\equiv c$ to the conclusion~${a\equiv c}$.
-\end{ttdescription}
-
-
-\subsection{The $\lambda$-conversion rules}
-\index{lambda calc@$\lambda$-calculus}
-\begin{ttbox}
-beta_conversion : cterm -> thm
-extensional : thm -> thm
-abstract_rule : string -> cterm -> thm -> thm
-combination : thm -> thm -> thm
-\end{ttbox}
-There is no rule for $\alpha$-conversion because Isabelle regards
-$\alpha$-convertible theorems as equal.
-\begin{ttdescription}
-\item[\ttindexbold{beta_conversion} $ct$]
-makes the theorem $((\lambda x.a)(b)) \equiv a[b/x]$, where $ct$ is the
-term $(\lambda x.a)(b)$.
-
-\item[\ttindexbold{extensional} $thm$]
-maps the premise $f(x) \equiv g(x)$ to the conclusion $f\equiv g$.
-Parameter~$x$ is taken from the premise. It may be an unknown or a free
-variable (provided it does not occur in the assumptions); it must not occur
-in $f$ or~$g$.
-
-\item[\ttindexbold{abstract_rule} $v$ $x$ $thm$]
-maps the premise $a\equiv b$ to the conclusion $(\lambda x.a) \equiv
-(\lambda x.b)$, abstracting over all occurrences (if any!) of~$x$.
-Parameter~$x$ is supplied as a cterm. It may be an unknown or a free
-variable (provided it does not occur in the assumptions). In the
-conclusion, the bound variable is named~$v$.
-
-\item[\ttindexbold{combination} $thm@1$ $thm@2$]
-maps the premises $f\equiv g$ and $a\equiv b$ to the conclusion~$f(a)\equiv
-g(b)$.
-\end{ttdescription}
-
-
-\section{Derived rules for goal-directed proof}
-Most of these rules have the sole purpose of implementing particular
-tactics. There are few occasions for applying them directly to a theorem.
-
-\subsection{Resolution}
-\index{resolution}
-\begin{ttbox}
-biresolution : bool -> (bool*thm)list -> int -> thm
- -> thm Seq.seq
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{biresolution} $match$ $rules$ $i$ $state$]
-performs bi-resolution on subgoal~$i$ of $state$, using the list of $\it
-(flag,rule)$ pairs. For each pair, it applies resolution if the flag
-is~{\tt false} and elim-resolution if the flag is~{\tt true}. If $match$
-is~{\tt true}, the $state$ is not instantiated.
-\end{ttdescription}
-
-
-\subsection{Composition: resolution without lifting}
-\index{resolution!without lifting}
-\begin{ttbox}
-compose : thm * int * thm -> thm list
-COMP : thm * thm -> thm
-bicompose : bool -> bool * thm * int -> int -> thm
- -> thm Seq.seq
-\end{ttbox}
-In forward proof, a typical use of composition is to regard an assertion of
-the form $\phi\Imp\psi$ as atomic. Schematic variables are not renamed, so
-beware of clashes!
-\begin{ttdescription}
-\item[\ttindexbold{compose} ($thm@1$, $i$, $thm@2$)]
-uses $thm@1$, regarded as an atomic formula, to solve premise~$i$
-of~$thm@2$. Let $thm@1$ and $thm@2$ be $\psi$ and $\List{\phi@1; \ldots;
-\phi@n} \Imp \phi$. For each $s$ that unifies~$\psi$ and $\phi@i$, the
-result list contains the theorem
-\[ (\List{\phi@1; \ldots; \phi@{i-1}; \phi@{i+1}; \ldots; \phi@n} \Imp \phi)s.
-\]
-
-\item[$thm@1$ \ttindexbold{COMP} $thm@2$]
-calls \hbox{\tt compose ($thm@1$, 1, $thm@2$)} and returns the result, if
-unique; otherwise, it raises exception~\xdx{THM}\@. It is
-analogous to {\tt RS}\@.
-
-For example, suppose that $thm@1$ is $a=b\Imp b=a$, a symmetry rule, and
-that $thm@2$ is $\List{P\Imp Q; \neg Q} \Imp\neg P$, which is the
-principle of contrapositives. Then the result would be the
-derived rule $\neg(b=a)\Imp\neg(a=b)$.
-
-\item[\ttindexbold{bicompose} $match$ ($flag$, $rule$, $m$) $i$ $state$]
-refines subgoal~$i$ of $state$ using $rule$, without lifting. The $rule$
-is taken to have the form $\List{\psi@1; \ldots; \psi@m} \Imp \psi$, where
-$\psi$ need not be atomic; thus $m$ determines the number of new
-subgoals. If $flag$ is {\tt true} then it performs elim-resolution --- it
-solves the first premise of~$rule$ by assumption and deletes that
-assumption. If $match$ is~{\tt true}, the $state$ is not instantiated.
-\end{ttdescription}
-
-
-\subsection{Other meta-rules}
-\begin{ttbox}
-rename_params_rule : string list * int -> thm -> thm
-\end{ttbox}
-\begin{ttdescription}
-
-\item[\ttindexbold{rename_params_rule} ({\it names}, {\it i}) $thm$]
-uses the $names$ to rename the parameters of premise~$i$ of $thm$. The
-names must be distinct. If there are fewer names than parameters, then the
-rule renames the innermost parameters and may modify the remaining ones to
-ensure that all the parameters are distinct.
-\index{parameters!renaming}
-
-\end{ttdescription}
-\index{meta-rules|)}
-
-
-\section{Proof terms}\label{sec:proofObjects}
-\index{proof terms|(} Isabelle can record the full meta-level proof of each
-theorem. The proof term contains all logical inferences in detail.
-%while
-%omitting bookkeeping steps that have no logical meaning to an outside
-%observer. Rewriting steps are recorded in similar detail as the output of
-%simplifier tracing.
-Resolution and rewriting steps are broken down to primitive rules of the
-meta-logic. The proof term can be inspected by a separate proof-checker,
-for example.
-
-According to the well-known {\em Curry-Howard isomorphism}, a proof can
-be viewed as a $\lambda$-term. Following this idea, proofs
-in Isabelle are internally represented by a datatype similar to the one for
-terms described in \S\ref{sec:terms}.
-\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
-attached to {\tt Thm}, {\tt Axm} and {\tt Oracle}.
-
-Each theorem's derivation is stored as the {\tt der} field of its internal
-record:
-\begin{ttbox}
-#2 (#der (rep_thm conjI));
-{\out PThm (("HOL.conjI", []),}
-{\out AbsP ("H", None, AbsP ("H", None, \dots)), \dots, None) %}
-{\out None % None : Proofterm.proof}
-\end{ttbox}
-This proof term identifies a labelled theorem, {\tt conjI} of theory
-\texttt{HOL}, whose underlying proof is
-{\tt AbsP ("H", None, AbsP ("H", None, $\dots$))}.
-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}.
-Theorems involving oracles will be printed with a
-suffixed \verb|[!]| to point out the different quality of confidence achieved.
-
-\medskip
-
-The dependencies of theorems can be viewed using the function
-\ttindexbold{thm_deps}\index{theorems!dependencies}:
-\begin{ttbox}
-thm_deps [\(thm@1\), \(\ldots\), \(thm@n\)];
-\end{ttbox}
-generates the dependency graph of the theorems $thm@1$, $\ldots$, $thm@n$ and
-displays it using Isabelle's graph browser. For this to work properly,
-the theorems in question have to be proved with {\tt proofs} set to a value
-greater than {\tt 0}. You can use
-\begin{ttbox}
-ThmDeps.enable : unit -> unit
-ThmDeps.disable : unit -> unit
-\end{ttbox}
-to set \texttt{proofs} appropriately.
-
-\subsection{Reconstructing and checking proof terms}\label{sec:reconstruct_proofs}
-\index{proof terms!reconstructing}
-\index{proof terms!checking}
-
-When looking at the above datatype of proofs more closely, one notices that
-some arguments of constructors are {\it optional}. The reason for this is that
-keeping a full proof term for each theorem would result in enormous memory
-requirements. Fortunately, typical proof terms usually contain quite a lot of
-redundant information that can be reconstructed from the context. Therefore,
-Isabelle's inference kernel creates only {\em partial} (or {\em implicit})
-\index{proof terms!partial} proof terms, in which
-all typing information in terms, all term and type labels of abstractions
-{\tt AbsP} and {\tt Abst}, and (if possible) some argument terms of
-\verb!%! are omitted. The following functions are available for
-reconstructing and checking proof terms:
-\begin{ttbox}
-Reconstruct.reconstruct_proof :
- Sign.sg -> term -> Proofterm.proof -> Proofterm.proof
-Reconstruct.expand_proof :
- Sign.sg -> string list -> Proofterm.proof -> Proofterm.proof
-ProofChecker.thm_of_proof : theory -> Proofterm.proof -> thm
-\end{ttbox}
-
-\begin{ttdescription}
-\item[Reconstruct.reconstruct_proof $sg$ $t$ $prf$]
-turns the partial proof $prf$ into a full proof of the
-proposition denoted by $t$, with respect to signature $sg$.
-Reconstruction will fail with an error message if $prf$
-is not a proof of $t$, is ill-formed, or does not contain
-sufficient information for reconstruction by
-{\em higher order pattern unification}
-\cite{nipkow-patterns, Berghofer-Nipkow:2000:TPHOL}.
-The latter may only happen for proofs
-built up ``by hand'' but not for those produced automatically
-by Isabelle's inference kernel.
-\item[Reconstruct.expand_proof $sg$
- \ttlbrack$name@1$, $\ldots$, $name@n${\ttrbrack} $prf$]
-expands and reconstructs the proofs of all theorems with names
-$name@1$, $\ldots$, $name@n$ in the (full) proof $prf$.
-\item[ProofChecker.thm_of_proof $thy$ $prf$] turns the (full) proof
-$prf$ into a theorem with respect to theory $thy$ by replaying
-it using only primitive rules from Isabelle's inference kernel.
-\end{ttdescription}
-
-\subsection{Parsing and printing proof terms}
-\index{proof terms!parsing}
-\index{proof terms!printing}
-
-Isabelle offers several functions for parsing and printing
-proof terms. The concrete syntax for proof terms is described
-in Fig.\ts\ref{fig:proof_gram}.
-Implicit term arguments in partial proofs are indicated
-by ``{\tt _}''.
-Type arguments for theorems and axioms may be specified using
-\verb!%! or ``$\cdot$'' with an argument of the form {\tt TYPE($type$)}
-(see \S\ref{sec:basic_syntax}).
-They must appear before any other term argument of a theorem
-or axiom. In contrast to term arguments, type arguments may
-be completely omitted.
-\begin{ttbox}
-ProofSyntax.read_proof : theory -> bool -> string -> Proofterm.proof
-ProofSyntax.pretty_proof : Sign.sg -> Proofterm.proof -> Pretty.T
-ProofSyntax.pretty_proof_of : bool -> thm -> Pretty.T
-ProofSyntax.print_proof_of : bool -> thm -> unit
-\end{ttbox}
-\begin{figure}
-\begin{center}
-\begin{tabular}{rcl}
-$proof$ & $=$ & {\tt Lam} $params${\tt .} $proof$ ~~$|$~~
- $\Lambda params${\tt .} $proof$ \\
- & $|$ & $proof$ \verb!%! $any$ ~~$|$~~
- $proof$ $\cdot$ $any$ \\
- & $|$ & $proof$ \verb!%%! $proof$ ~~$|$~~
- $proof$ {\boldmath$\cdot$} $proof$ \\
- & $|$ & $id$ ~~$|$~~ $longid$ \\\\
-$param$ & $=$ & $idt$ ~~$|$~~ $idt$ {\tt :} $prop$ ~~$|$~~
- {\tt (} $param$ {\tt )} \\\\
-$params$ & $=$ & $param$ ~~$|$~~ $param$ $params$
-\end{tabular}
-\end{center}
-\caption{Proof term syntax}\label{fig:proof_gram}
-\end{figure}
-The function {\tt read_proof} reads in a proof term with
-respect to a given theory. The boolean flag indicates whether
-the proof term to be parsed contains explicit typing information
-to be taken into account.
-Usually, typing information is left implicit and
-is inferred during proof reconstruction. The pretty printing
-functions operating on theorems take a boolean flag as an
-argument which indicates whether the proof term should
-be reconstructed before printing.
-
-The following example (based on Isabelle/HOL) illustrates how
-to parse and check proof terms. We start by parsing a partial
-proof term
-\begin{ttbox}
-val prf = ProofSyntax.read_proof Main.thy false
- "impI % _ % _ %% (Lam H : _. conjE % _ % _ % _ %% H %%
- (Lam (H1 : _) H2 : _. conjI % _ % _ %% H2 %% H1))";
-{\out val prf = PThm (("HOL.impI", []), \dots, \dots, None) % None % None %%}
-{\out AbsP ("H", None, PThm (("HOL.conjE", []), \dots, \dots, None) %}
-{\out None % None % None %% PBound 0 %%}
-{\out AbsP ("H1", None, AbsP ("H2", None, \dots))) : Proofterm.proof}
-\end{ttbox}
-The statement to be established by this proof is
-\begin{ttbox}
-val t = term_of
- (read_cterm (sign_of Main.thy) ("A & B --> B & A", propT));
-{\out val t = Const ("Trueprop", "bool => prop") $}
-{\out (Const ("op -->", "[bool, bool] => bool") $}
-{\out \dots $ \dots : Term.term}
-\end{ttbox}
-Using {\tt t} we can reconstruct the full proof
-\begin{ttbox}
-val prf' = Reconstruct.reconstruct_proof (sign_of Main.thy) t prf;
-{\out val prf' = PThm (("HOL.impI", []), \dots, \dots, Some []) %}
-{\out Some (Const ("op &", \dots) $ Free ("A", \dots) $ Free ("B", \dots)) %}
-{\out Some (Const ("op &", \dots) $ Free ("B", \dots) $ Free ("A", \dots)) %%}
-{\out AbsP ("H", Some (Const ("Trueprop", \dots) $ \dots), \dots)}
-{\out : Proofterm.proof}
-\end{ttbox}
-This proof can finally be turned into a theorem
-\begin{ttbox}
-val thm = ProofChecker.thm_of_proof Main.thy prf';
-{\out val thm = "A & B --> B & A" : Thm.thm}
-\end{ttbox}
-
-\index{proof terms|)}
-\index{theorems|)}
-
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "ref"
-%%% End: