diff -r a90fc1e5fb19 -r abba35b98892 doc-src/IsarRef/generic.tex --- 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}