summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/IsarRef/generic.tex

changeset 7987 | d9aef93c0e32 |

parent 7981 | 5120a2a15d06 |

child 7990 | 0a604b2fc2b1 |

1.1 --- a/doc-src/IsarRef/generic.tex Sat Oct 30 20:41:30 1999 +0200 1.2 +++ b/doc-src/IsarRef/generic.tex Sun Oct 31 15:20:35 1999 +0100 1.3 @@ -37,9 +37,9 @@ 1.4 becomes a (generalized) \emph{elimination}. 1.5 1.6 Note that the classical reasoner introduces another version of $rule$ that 1.7 - is able to pick appropriate rules automatically, whenever explicit $thms$ 1.8 - are omitted (see \S\ref{sec:classical-basic}); that method is the default 1.9 - for $\PROOFNAME$ steps. Note that ``$\DDOT$'' (double-dot) abbreviates 1.10 + is able to pick appropriate rules automatically, whenever $thms$ are omitted 1.11 + (see \S\ref{sec:classical-basic}); that method is the default for 1.12 + $\PROOFNAME$ steps. Note that ``$\DDOT$'' (double-dot) abbreviates 1.13 $\BY{default}$. 1.14 \item [$erule~thms$] is similar to $rule$, but applies rules by 1.15 elim-resolution. This is an improper method, mainly for experimentation and 1.16 @@ -47,11 +47,11 @@ 1.17 $rule$ (single step, involving facts) or $elim$ (repeated steps, see 1.18 \S\ref{sec:classical-basic}). 1.19 \item [$unfold~thms$ and $fold~thms$] expand and fold back again the given 1.20 - meta-level definitions throughout all goals; any facts provided are 1.21 - \emph{ignored}. 1.22 -\item [$succeed$] yields a single (unchanged) result; it is the identify of 1.23 + meta-level definitions throughout all goals; any facts provided are inserted 1.24 + into the goal and subject to rewriting as well. 1.25 +\item [$succeed$] yields a single (unchanged) result; it is the identity of 1.26 the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}). 1.27 -\item [$fail$] yields an empty result sequence; it is the identify of the 1.28 +\item [$fail$] yields an empty result sequence; it is the identity of the 1.29 ``\texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}). 1.30 \end{descr} 1.31 1.32 @@ -98,12 +98,12 @@ 1.33 result). 1.34 \item [$OF~thms$, $RS~n~thm$, and $COMP~n~thm$] compose rules. $OF$ applies 1.35 $thms$ in parallel (cf.\ \texttt{MRS} in \cite[\S5]{isabelle-ref}, but note 1.36 - the reversed order). Note that premises may be skipped by including $\_$ 1.37 - (underscore) as argument. 1.38 + the reversed order). Note that premises may be skipped by including 1.39 + ``$\_$'' (underscore) as argument. 1.40 1.41 $RS$ resolves with the $n$-th premise of $thm$; $COMP$ is a version of $RS$ 1.42 - that does not include the automatic lifting process that is normally 1.43 - intended (cf.\ \texttt{RS} and \texttt{COMP} in \cite[\S5]{isabelle-ref}). 1.44 + that skips the automatic lifting process that is normally intended (cf.\ 1.45 + \texttt{RS} and \texttt{COMP} in \cite[\S5]{isabelle-ref}). 1.46 1.47 \item [$of~\vec t$ and $where~\vec x = \vec t$] perform positional and named 1.48 instantiation, respectively. The terms given in $of$ are substituted for 1.49 @@ -180,9 +180,10 @@ 1.50 \item [$\FINALLY~(thms)$] maintaining $calculation$ in the same way as 1.51 $\ALSO$, and concludes the current calculational thread. The final result 1.52 is exhibited as fact for forward chaining towards the next goal. Basically, 1.53 - $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$. Typical proof 1.54 - idioms are``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and 1.55 - ``$\FINALLY~\HAVE{}{\phi}~\DOT$''. 1.56 + $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$. Note that 1.57 + ``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and 1.58 + ``$\FINALLY~\HAVE{}{\phi}~\DOT$'' are typical idioms for concluding 1.59 + calculational proofs. 1.60 1.61 \item [$trans$] maintains the set of transitivity rules of the theory or proof 1.62 context, by adding or deleting theorems (the default is to add). 1.63 @@ -204,12 +205,12 @@ 1.64 intro_classes & : & \isarmeth \\ 1.65 \end{matharray} 1.66 1.67 -Axiomatic type classes are provided by Isabelle/Pure as a purely 1.68 -\emph{definitional} interface to type classes (cf.~\S\ref{sec:classes}). Thus 1.69 -any object logic may make use of this light-weight mechanism for abstract 1.70 -theories. See \cite{Wenzel:1997:TPHOL} for more information. There is also a 1.71 -tutorial on \emph{Using Axiomatic Type Classes in Isabelle} that is part of 1.72 -the standard Isabelle documentation. 1.73 +Axiomatic type classes are provided by Isabelle/Pure as a \emph{definitional} 1.74 +interface to type classes (cf.~\S\ref{sec:classes}). Thus any object logic 1.75 +may make use of this light-weight mechanism of abstract theories. See 1.76 +\cite{Wenzel:1997:TPHOL} for more information. There is also a tutorial on 1.77 +\emph{Using Axiomatic Type Classes in Isabelle} that is part of the standard 1.78 +Isabelle documentation. 1.79 %FIXME cite 1.80 1.81 \begin{rail} 1.82 @@ -225,21 +226,22 @@ 1.83 holding. Class axioms may not contain more than one type variable. The 1.84 class axioms (with implicit sort constraints added) are bound to the given 1.85 names. Furthermore a class introduction rule is generated, which is 1.86 - employed by method $intro_classes$ in support instantiation proofs of this 1.87 + employed by method $intro_classes$ to support instantiation proofs of this 1.88 class. 1.89 1.90 \item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~t :: 1.91 (\vec s)c$] setup up a goal stating the class relation or type arity. The 1.92 - proof would usually proceed by the $intro_classes$ method, and then 1.93 - establish the characteristic theorems of the type classes involved. After 1.94 - finishing the proof the theory will be augmented by a type signature 1.95 - declaration corresponding to the resulting theorem. 1.96 -\item [$intro_classes$] repeatedly expands the class introduction rules of 1.97 + proof would usually proceed by $intro_classes$, and then establish the 1.98 + characteristic theorems of the type classes involved. After finishing the 1.99 + proof, the theory will be augmented by a type signature declaration 1.100 + corresponding to the resulting theorem. 1.101 +\item [$intro_classes$] repeatedly expands all class introduction rules of 1.102 this theory. 1.103 \end{descr} 1.104 1.105 -See theory \texttt{HOL/Isar_examples/Group} for a simple example of using 1.106 -axiomatic type classes, including instantiation proofs. 1.107 +%FIXME 1.108 +%See theory \texttt{HOL/Isar_examples/Group} for a simple example of using 1.109 +%axiomatic type classes, including instantiation proofs. 1.110 1.111 1.112 \section{The Simplifier} 1.113 @@ -345,7 +347,7 @@ 1.114 given ones may be applied. The latter form admits better control of what 1.115 actually happens, thus it is very appropriate as an initial method for 1.116 $\PROOFNAME$ that splits up certain connectives of the goal, before entering 1.117 - the actual proof. 1.118 + the actual sub-proof. 1.119 1.120 \item [$contradiction$] solves some goal by contradiction, deriving any result 1.121 from both $\neg A$ and $A$. Facts, which are guaranteed to participate, may 1.122 @@ -388,7 +390,10 @@ 1.123 1.124 Any of above methods support additional modifiers of the context of classical 1.125 rules. There semantics is analogous to the attributes given in 1.126 -\S\ref{sec:classical-mod}. 1.127 +\S\ref{sec:classical-mod}. Facts provided by forward chaining are inserted 1.128 +into the goal before doing the search. The ``!''~argument causes the full 1.129 +context of assumptions to be included as well.\footnote{This is slightly less 1.130 + hazardous than for the Simplifier (see \S\ref{sec:simp}).} 1.131 1.132 1.133 \subsection{Combined automated methods} 1.134 @@ -403,7 +408,7 @@ 1.135 ('force' | 'auto') ('!' ?) (clasimpmod * ) 1.136 ; 1.137 1.138 - clasimpmod: ('simp' ('add' | 'del' | 'only') | other | 1.139 + clasimpmod: ('simp' ('add' | 'del' | 'only') | 'other' | 1.140 (('intro' | 'elim' | 'dest') (() | '!' | '!!') | 'del')) ':' thmrefs 1.141 \end{rail} 1.142 1.143 @@ -414,8 +419,13 @@ 1.144 modifier arguments correspond to those given in \S\ref{sec:simp} and 1.145 \S\ref{sec:classical-auto}. Just note that the ones related to the 1.146 Simplifier are prefixed by \railtoken{simp} here. 1.147 + 1.148 + Facts provided by forward chaining are inserted into the goal before doing 1.149 + the search. The ``!''~argument causes the full context of assumptions to be 1.150 + included as well. 1.151 \end{descr} 1.152 1.153 + 1.154 \subsection{Modifying the context}\label{sec:classical-mod} 1.155 1.156 \indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}