--- a/doc-src/IsarRef/generic.tex Tue Aug 24 11:54:13 1999 +0200
+++ b/doc-src/IsarRef/generic.tex Tue Aug 24 15:38:18 1999 +0200
@@ -14,8 +14,8 @@
erule^* & : & \isarmeth \\[0.5ex]
fold & : & \isarmeth \\
unfold & : & \isarmeth \\[0.5ex]
+ succeed & : & \isarmeth \\
fail & : & \isarmeth \\
- succeed & : & \isarmeth \\
\end{matharray}
\begin{rail}
@@ -25,12 +25,12 @@
\begin{descr}
\item [``$-$''] does nothing but insert the forward chaining facts as premises
- into the goal. Note that command $\PROOFNAME$ without any method given
- actually performs a single reduction step using the $rule$ method (see
- below); thus a plain \emph{do-nothing} proof step would be $\PROOF{-}$
- rather than $\PROOFNAME$ alone.
-\item [$assumption$] solves some goal by assumption (after inserting the
- goal's facts).
+ into the goal. Note that command $\PROOFNAME$ without any method actually
+ performs a single reduction step using the $rule$ method (see below); thus a
+ plain \emph{do-nothing} proof step would be $\PROOF{-}$ rather than
+ $\PROOFNAME$ alone.
+\item [$assumption$] solves some goal by assumption, after inserting the
+ goal's facts.
\item [$finish$] solves all remaining goals by assumption; this is the default
terminal proof method for $\QEDNAME$, i.e.\ it usually does not have to be
spelled out explicitly.
@@ -41,24 +41,20 @@
Note that the classical reasoner introduces another version of $rule$ that
is able to pick appropriate rules automatically, whenever explicit $thms$
- are omitted (see \S\ref{sec:classical-basic}) . That method is the default
- one for proof steps such as $\PROOFNAME$ and ``$\DDOT$'' (two dots).
-
+ are omitted (see \S\ref{sec:classical-basic}); that method is the default
+ one for initial proof steps, such as $\PROOFNAME$ and ``$\DDOT$'' (two
+ dots).
\item [$erule~thms$] is similar to $rule$, but applies rules by
elim-resolution. This is an improper method, mainly for experimentation and
- porting of old script. Actual elimination proofs are usually done with
- $rule$ (single step) or $elim$ (multiple steps, see
+ porting of old scripts. Actual elimination proofs are usually done with
+ $rule$ (single step, involving facts) or $elim$ (multiple steps, see
\S\ref{sec:classical-basic}).
-
-\item [$unfold~thms$ and $fold~thms$] expand and fold back again meta-level
- definitions $thms$ throughout all goals; facts may not be given.
-
+\item [$unfold~thms$ and $fold~thms$] expand and fold back again the given
+ meta-level definitions throughout all goals; facts may not be involved.
+\item [$succeed$] yields a single (unchanged) result; it is the identify of
+ the ``\texttt{,}'' method combinator.
\item [$fail$] yields an empty result sequence; it is the identify of the
``\texttt{|}'' method combinator.
-
-\item [$succeed$] yields a singleton result, which is unchanged except for the
- change from $prove$ mode back to $state$; it is the identify of the
- ``\texttt{,}'' method combinator.
\end{descr}
@@ -73,11 +69,11 @@
OF & : & \isaratt \\
RS & : & \isaratt \\
COMP & : & \isaratt \\[0.5ex]
- where & : & \isaratt \\
- of & : & \isaratt \\[0.5ex]
+ of & : & \isaratt \\
+ where & : & \isaratt \\[0.5ex]
standard & : & \isaratt \\
elimify & : & \isaratt \\
- export & : & \isaratt \\
+ export^* & : & \isaratt \\
transfer & : & \isaratt \\
\end{matharray}
@@ -106,24 +102,23 @@
$thms$ in parallel (cf.\ \texttt{MRS} in \cite[\S5]{isabelle-ref}, but note
the reversed order). $RS$ resolves with the $n$-th premise of $thm$; $COMP$
is a version of $RS$ that does not include the automatic lifting process
- that is normally desired (see \texttt{RS} and \texttt{COMP} in
+ that is normally intended (see also \texttt{RS} and \texttt{COMP} in
\cite[\S5]{isabelle-ref}).
-\item [$of~ts$ and $where~insts$] perform positional and named instantiation,
- respectively. The terms given in $of$ are substituted for any variables
- occurring in a theorem from left to right; ``\texttt{_}'' (underscore)
- indicates to skip a position.
+\item [$of~ts$ and $where~\vec x = \vec t$] perform positional and named
+ instantiation, respectively. The terms given in $of$ are substituted for
+ any schematic variables occurring in a theorem from left to right;
+ ``\texttt{_}'' (underscore) indicates to skip a position.
\item [$standard$] puts a theorem into the standard form of object-rules, just
as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).
-\item [$elimify$] turns an destruction rule (such as projection $conjunct@1$
- into an elimination.
+\item [$elimify$] turns an destruction rule into an elimination.
\item [$export$] lifts a local result out of the current proof context,
- generalizing all fixed variables and discharging all assumptions. Export is
- usually done automatically behind the scenes. This attribute is mainly for
- experimentation.
+ generalizing all fixed variables and discharging all assumptions. Note that
+ (partial) export is usually done automatically behind the scenes. This
+ attribute is mainly for experimentation.
\item [$transfer$] promotes a theorem to the current theory context, which has
to enclose the former one. Normally, this is done automatically when rules
@@ -175,24 +170,23 @@
\begin{descr}
\item [$\ALSO~(thms)$] maintains the auxiliary $calculation$ register as
follows. The first occurrence of $\ALSO$ in some calculational thread
- initialises $calculation$ by $facts$. Any subsequent $\ALSO$ on the
- \emph{same} level of block-structure updates $calculation$ by some
- transitivity rule applied to $calculation$ and $facts$ (in that order).
- Transitivity rules are picked from the current context plus those given as
- $thms$ (the latter have precedence).
+ initialises $calculation$ by $facts$. Any subsequent $\ALSO$ on the same
+ level of block-structure updates $calculation$ by some transitivity rule
+ applied to $calculation$ and $facts$ (in that order). Transitivity rules
+ are picked from the current context plus those given as $thms$ (the latter
+ have precedence).
\item [$\FINALLY~(thms)$] maintaining $calculation$ in the same way as
$\ALSO$, and concludes the current calculational thread. The final result
is exhibited as fact for forward chaining towards the next goal. Basically,
$\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$. A typical proof
- idiom is $\FINALLY~\SHOW~\VVar{thesis}~\DOT$.
+ idiom is ``$\FINALLY~\SHOW{}{\VVar{thesis}}~\DOT$''.
-\item [Attribute $trans$] maintains the set of transitivity rules of the
- theory or proof context, by adding or deleting the theorems provided as
- arguments. The default is adding of rules.
+\item [$trans$] maintains the set of transitivity rules of the theory or proof
+ context, by adding or deleting theorems (the default is to add).
\end{descr}
-See theory \texttt{HOL/Isar_examples/Group} for a simple applications of
+See theory \texttt{HOL/Isar_examples/Group} for a simple application of
calculations for basic equational reasoning.
\texttt{HOL/Isar_examples/KnasterTarski} involves a few more advanced
calculational steps in combination with natural deduction.
@@ -213,6 +207,7 @@
theories. See \cite{Wenzel:1997:TPHOL} for more information. There is also a
tutorial on \emph{Using Axiomatic Type Classes in Isabelle} that is part of
the standard Isabelle documentation.
+%FIXME cite
\begin{rail}
'axclass' classdecl (axmdecl prop comment? +)
@@ -222,21 +217,23 @@
\end{rail}
\begin{descr}
-\item [$\isarkeyword{axclass}~$] defines an axiomatic type class as the
- intersection of existing classes, with additional axioms holding. Class
- axioms may not contain more than one type variable. The class axioms (with
- implicit sort constraints added) are bound to the given names. Furthermore
- a class introduction rule is generated, which is employed by method
- $expand_classes$ in support instantiation proofs of this class.
-
-\item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~c@1 <
- c@2$] setup up a goal stating the class relation or type arity. The proof
- would usually proceed by the $expand_classes$ method, and then establish the
- characteristic theorems of the type classes involved. After finishing the
- proof the theory will be augmented by a type signature declaration
- corresponding to the resulting theorem.
+\item [$\isarkeyword{axclass}~c < \vec c~axms$] defines an axiomatic type
+ class as the intersection of existing classes, with additional axioms
+ holding. Class axioms may not contain more than one type variable. The
+ class axioms (with implicit sort constraints added) are bound to the given
+ names. Furthermore a class introduction rule is generated, which is
+ employed by method $expand_classes$ in support instantiation proofs of this
+ class.
+
+\item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~t ::
+ (\vec s)c$] setup up a goal stating the class relation or type arity. The
+ proof would usually proceed by the $expand_classes$ method, and then
+ establish the characteristic theorems of the type classes involved. After
+ finishing the proof the theory will be augmented by a type signature
+ declaration corresponding to the resulting theorem.
\item [Method $expand_classes$] iteratively expands the class introduction
rules
+%FIXME intro classIs etc;
\end{descr}
See theory \texttt{HOL/Isar_examples/Group} for a simple example of using
@@ -253,8 +250,11 @@
asm_simp & : & \isarmeth \\
\end{matharray}
+\railalias{asmsimp}{asm\_simp}
+\railterm{asmsimp}
+
\begin{rail}
- 'simp' (simpmod * )
+ ('simp' | asmsimp) (simpmod * )
;
simpmod: ('add' | 'del' | 'only' | 'other') ':' thmrefs
@@ -263,15 +263,16 @@
\begin{descr}
\item [Methods $simp$ and $asm_simp$] invoke Isabelle's simplifier, after
- modifying the context as follows adding or deleting given rules. The
+ modifying the context by adding or deleting given rules. The
\railtoken{only} modifier first removes all other rewrite rules and
congruences, and then is like \railtoken{add}. In contrast,
\railtoken{other} ignores its arguments; nevertheless there may be
side-effects on the context via attributes. This provides a back door for
- arbitrary manipulation of the context.
+ arbitrary context manipulation.
Both of these methods are based on \texttt{asm_full_simp_tac}, see
- \cite[\S10]{isabelle-ref}.
+ \cite[\S10]{isabelle-ref}; $simp$ removes any exisiting premises of the
+ goal, before inserting the goal facts; $asm_simp$ leaves the premises.
\end{descr}
\subsection{Modifying the context}
@@ -288,7 +289,7 @@
\begin{descr}
\item [Attribute $simp$] adds or deletes rules from the theory or proof
- context. The default is to add rules.
+ context (the default is to add).
\end{descr}
@@ -303,13 +304,13 @@
\end{matharray}
These attributes provide forward rules for simplification, which should be
-used very rarely. See the ML function of the same name in
+used only very rarely. See the ML functions of the same name in
\cite[\S10]{isabelle-ref} for more information.
\section{The Classical Reasoner}
-\subsection{Basic step methods}\label{sec:classical-basic}
+\subsection{Basic methods}\label{sec:classical-basic}
\indexisarmeth{rule}\indexisarmeth{default}\indexisarmeth{contradiction}
\begin{matharray}{rcl}
@@ -329,14 +330,16 @@
over the primitive one (see \S\ref{sec:pure-meth}). In the case that no
rules are provided as arguments, it automatically determines elimination and
introduction rules from the context (see also \S\ref{sec:classical-mod}).
- In that form it is the default method for basic proof steps.
+ In that form it is the default method for basic proof steps, such as
+ $\PROOFNAME$ and ``$\DDOT$'' (two dots).
\item [Methods $intro$ and $elim$] repeatedly refine some goal by intro- or
elim-resolution, after having inserted the facts. Omitting the arguments
refers to any suitable rules from the context, otherwise only the explicitly
- given ones may be applied. The latter form admits better control of what is
- actually happening, thus it is appropriate as an initial proof method that
- splits up certain connectives of the goal, before entering the sub-proof.
+ given ones may be applied. The latter form admits better control of what
+ actually happens, thus it is very appropriate as an initial method for
+ $\PROOFNAME$ that splits up certain connectives of the goal, before entering
+ the sub-proof.
\item [Method $contradiction$] solves some goal by contradiction: both $A$ and
$\neg A$ have to be present in the assumptions.
@@ -370,11 +373,10 @@
\begin{descr}
\item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac}
- in \cite[\S11]{isabelle-ref}). The optional argument specifies a applies a
+ in \cite[\S11]{isabelle-ref}). The optional argument specifies a
user-supplied search bound (default 20).
\item [$fast$, $best$, $slow$, $slow_best$] refer to the generic classical
- reasoner (see the corresponding tactics \texttt{fast_tac} etc.\ in
- \cite[\S11]{isabelle-ref}).
+ reasoner (see \cite[\S11]{isabelle-ref}, tactic \texttt{fast_tac} etc).
\end{descr}
Any of above methods support additional modifiers of the context of classical
@@ -403,7 +405,8 @@
simplification and classical reasoning tactics. See \texttt{force_tac} and
\texttt{auto_tac} in \cite[\S11]{isabelle-ref} for more information. The
modifier arguments correspond to those given in \S\ref{sec:simp} and
- \S\ref{sec:classical-auto}.
+ \S\ref{sec:classical-auto}. Note that the ones related to the Simplifier
+ are prefixed by \railtoken{simp} here.
\end{descr}
\subsection{Modifying the context}\label{sec:classical-mod}
@@ -422,13 +425,13 @@
\end{rail}
\begin{descr}
-\item [Attributes $intro$, $elim$, and $dest$] add introduction, elimination,
- and destruct rules, respectively. By default, rules are considered as
- \emph{safe}, while a single ``!'' classifies as \emph{unsafe}, and ``!!'' as
- \emph{extra} (i.e.\ not applied in the search-oriented automatic methods).
-
-\item [Attribute $delrule$] deletes introduction or elimination rules from the
- context. Destruction rules would have to be turned into elimination rules
+\item [$intro$, $elim$, $dest$] add introduction, elimination, destruct rules,
+ respectively. By default, rules are considered as \emph{safe}, while a
+ single ``!'' classifies as \emph{unsafe}, and ``!!'' as \emph{extra} (i.e.\
+ not applied in the search-oriented automatic methods).
+
+\item [$delrule$] deletes introduction or elimination rules from the context.
+ Note that destruction rules would have to be turned into elimination rules
first, e.g.\ by using the $elimify$ attribute.
\end{descr}