doc-src/IsarRef/generic.tex
 changeset 7321 b4dcc32310fb parent 7319 3907d597cae6 child 7335 abba35b98892
     1.1 --- a/doc-src/IsarRef/generic.tex	Mon Aug 23 15:24:00 1999 +0200
1.2 +++ b/doc-src/IsarRef/generic.tex	Mon Aug 23 15:27:27 1999 +0200
1.3 @@ -7,15 +7,15 @@
1.4  \indexisarmeth{finish}\indexisarmeth{fold}\indexisarmeth{unfold}
1.5  \indexisarmeth{rule}\indexisarmeth{erule}
1.6  \begin{matharray}{rcl}
1.7 -  fail & : & \isarmeth \\
1.8 -  succeed & : & \isarmeth \\
1.9    - & : & \isarmeth \\
1.10    assumption & : & \isarmeth \\
1.11 -  finish & : & \isarmeth \\
1.12 +  finish & : & \isarmeth \\[0.5ex]
1.13 +  rule & : & \isarmeth \\
1.14 +  erule^* & : & \isarmeth \\[0.5ex]
1.15    fold & : & \isarmeth \\
1.16 -  unfold & : & \isarmeth \\
1.17 -  rule & : & \isarmeth \\
1.18 -  erule^* & : & \isarmeth \\
1.19 +  unfold & : & \isarmeth \\[0.5ex]
1.20 +  fail & : & \isarmeth \\
1.21 +  succeed & : & \isarmeth \\
1.22  \end{matharray}
1.23
1.24  \begin{rail}
1.25 @@ -24,14 +24,42 @@
1.26  \end{rail}
1.27
1.28  \begin{descr}
1.29 -\item []
1.30 -\end{descr}
1.31 +\item [$-$''] does nothing but insert the forward chaining facts as premises
1.32 +  into the goal.  Note that command $\PROOFNAME$ without any method given
1.33 +  actually performs a single reduction step using the $rule$ method (see
1.34 +  below); thus a plain \emph{do-nothing} proof step would be $\PROOF{-}$
1.35 +  rather than $\PROOFNAME$ alone.
1.36 +\item [$assumption$] solves some goal by assumption (after inserting the
1.37 +  goal's facts).
1.38 +\item [$finish$] solves all remaining goals by assumption; this is the default
1.39 +  terminal proof method for $\QEDNAME$, i.e.\ it usually does not have to be
1.40 +  spelled out explicitly.
1.41 +\item [$rule~thms$] applies some rule given as argument in backward manner;
1.42 +  facts are used to reduce the rule before applying it to the goal.  Thus
1.43 +  $rule$ without facts is plain \emph{introduction}, while with facts it
1.44 +  becomes an \emph{elimination}.
1.45 +
1.46 +  Note that the classical reasoner introduces another version of $rule$ that
1.47 +  is able to pick appropriate rules automatically, whenever explicit $thms$
1.48 +  are omitted (see \S\ref{sec:classical-basic}) .  That method is the default
1.49 +  one for proof steps such as $\PROOFNAME$ and $\DDOT$'' (two dots).
1.50 +
1.51 +\item [$erule~thms$] is similar to $rule$, but applies rules by
1.52 +  elim-resolution.  This is an improper method, mainly for experimentation and
1.53 +  porting of old script.  Actual elimination proofs are usually done with
1.54 +  $rule$ (single step) or $elim$ (multiple steps, see
1.55 +  \S\ref{sec:classical-basic}).
1.56 +
1.57 +\item [$unfold~thms$ and $fold~thms$] expand and fold back again meta-level
1.58 +  definitions $thms$ throughout all goals; facts may not be given.
1.59
1.60 -FIXME
1.61 -
1.62 -%FIXME sort
1.63 -%FIXME thmref (single)
1.64 -%FIXME var vs. term
1.65 +\item [$fail$] yields an empty result sequence; it is the identify of the
1.66 +  \texttt{|}'' method combinator.
1.67 +
1.68 +\item [$succeed$] yields a singleton result, which is unchanged except for the
1.69 +  change from $prove$ mode back to $state$; it is the identify of the
1.70 +  \texttt{,}'' method combinator.
1.71 +\end{descr}
1.72
1.73
1.74  \section{Miscellaneous attributes}
1.75 @@ -41,46 +69,68 @@
1.76  \indexisaratt{elimify}\indexisaratt{transfer}\indexisaratt{export}
1.77  \begin{matharray}{rcl}
1.78    tag & : & \isaratt \\
1.79 -  untag & : & \isaratt \\
1.80 -  COMP & : & \isaratt \\
1.81 +  untag & : & \isaratt \\[0.5ex]
1.82 +  OF & : & \isaratt \\
1.83    RS & : & \isaratt \\
1.84 -  OF & : & \isaratt \\
1.85 +  COMP & : & \isaratt \\[0.5ex]
1.86    where & : & \isaratt \\
1.87 -  of & : & \isaratt \\
1.88 +  of & : & \isaratt \\[0.5ex]
1.89    standard & : & \isaratt \\
1.90    elimify & : & \isaratt \\
1.91 +  export & : & \isaratt \\
1.92    transfer & : & \isaratt \\
1.93 -  export & : & \isaratt \\
1.94  \end{matharray}
1.95
1.96  \begin{rail}
1.97    ('tag' | 'untag') (nameref+)
1.98    ;
1.99 -\end{rail}
1.100 -
1.101 -\begin{rail}
1.102 -  ('COMP' | 'RS') nat? thmref
1.103 -  ;
1.104    'OF' thmrefs
1.105    ;
1.106 -\end{rail}
1.107 -
1.108 -\begin{rail}
1.109 -  'where' (name '=' term * 'and')
1.110 +  ('RS' | 'COMP') nat? thmref
1.111    ;
1.112    'of' (inst * ) ('concl' ':' (inst * ))?
1.113    ;
1.114 +  'where' (name '=' term * 'and')
1.115 +  ;
1.116
1.117    inst: underscore | term
1.118    ;
1.119  \end{rail}
1.120
1.121  \begin{descr}
1.122 -\item []
1.123 +\item [$tag~tags$ and $untag~tags$] add and remove $tags$ to the theorem,
1.124 +  respectively.  Tags may be any list of strings that serve as comment for
1.125 +  some tools (e.g.\ $\LEMMANAME$ causes tag $lemma$'' to be added to the
1.126 +  result).
1.127 +\item [$OF~thms$, $RS~n~thm$, and $COMP~n~thm$] compose rules.  $OF$ applies
1.128 +  $thms$ in parallel (cf.\ \texttt{MRS} in \cite[\S5]{isabelle-ref}, but note
1.129 +  the reversed order).  $RS$ resolves with the $n$-th premise of $thm$; $COMP$
1.130 +  is a version of $RS$ that does not include the automatic lifting process
1.131 +  that is normally desired (see \texttt{RS} and \texttt{COMP} in
1.132 +  \cite[\S5]{isabelle-ref}).
1.133 +
1.134 +\item [$of~ts$ and $where~insts$] perform positional and named instantiation,
1.135 +  respectively.  The terms given in $of$ are substituted for any variables
1.136 +  occurring in a theorem from left to right; \texttt{_}'' (underscore)
1.137 +  indicates to skip a position.
1.138 +
1.139 +\item [$standard$] puts a theorem into the standard form of object-rules, just
1.140 +  as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).
1.141 +
1.142 +\item [$elimify$] turns an destruction rule (such as projection $conjunct@1$
1.143 +  into an elimination.
1.144 +
1.145 +\item [$export$] lifts a local result out of the current proof context,
1.146 +  generalizing all fixed variables and discharging all assumptions.  Export is
1.147 +  usually done automatically behind the scenes.  This attribute is mainly for
1.148 +  experimentation.
1.149 +
1.150 +\item [$transfer$] promotes a theorem to the current theory context, which has
1.151 +  to enclose the former one.  Normally, this is done automatically when rules
1.152 +  are joined by inference.
1.153 +
1.154  \end{descr}
1.155
1.156 -FIXME
1.157 -
1.158
1.159  \section{Calculational proof}\label{sec:calculation}
1.160
1.161 @@ -172,7 +222,13 @@
1.162  \end{rail}
1.163
1.164  \begin{descr}
1.165 -\item [$\isarkeyword{axclass}~$] FIXME
1.166 +\item [$\isarkeyword{axclass}~$] defines an axiomatic type class as the
1.167 +  intersection of existing classes, with additional axioms holding.  Class
1.168 +  axioms may not contain more than one type variable.  The class axioms (with
1.169 +  implicit sort constraints added) are bound to the given names.  Furthermore
1.170 +  a class introduction rule is generated, which is employed by method
1.171 +  $expand_classes$ in support instantiation proofs of this class.
1.172 +
1.173  \item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~c@1 < 1.174 c@2$] setup up a goal stating the class relation or type arity.  The proof
1.175    would usually proceed by the $expand_classes$ method, and then establish the
1.176 @@ -189,13 +245,12 @@
1.177
1.178  \section{The Simplifier}
1.179
1.180 -\subsection{Simplification methods}
1.181 +\subsection{Simplification methods}\label{sec:simp}
1.182
1.183 -\indexisarmeth{simp}\indexisarmeth{asm_simp}\indexisaratt{simp}
1.184 +\indexisarmeth{simp}\indexisarmeth{asm_simp}
1.185  \begin{matharray}{rcl}
1.186    simp & : & \isarmeth \\
1.187    asm_simp & : & \isarmeth \\
1.188 -  simp & : & \isaratt \\
1.189  \end{matharray}
1.190
1.191  \begin{rail}
1.192 @@ -206,7 +261,35 @@
1.193    ;
1.194  \end{rail}
1.195
1.196 -FIXME
1.197 +\begin{descr}
1.198 +\item [Methods $simp$ and $asm_simp$] invoke Isabelle's simplifier, after
1.199 +  modifying the context as follows adding or deleting given rules.  The
1.200 +  \railtoken{only} modifier first removes all other rewrite rules and
1.201 +  congruences, and then is like \railtoken{add}.  In contrast,
1.202 +  \railtoken{other} ignores its arguments; nevertheless there may be
1.203 +  side-effects on the context via attributes.  This provides a back door for
1.204 +  arbitrary manipulation of the context.
1.205 +
1.206 +  Both of these methods are based on \texttt{asm_full_simp_tac}, see
1.207 +  \cite[\S10]{isabelle-ref}.
1.208 +\end{descr}
1.209 +
1.210 +\subsection{Modifying the context}
1.211 +
1.212 +\indexisaratt{simp}
1.213 +\begin{matharray}{rcl}
1.214 +  simp & : & \isaratt \\
1.215 +\end{matharray}
1.216 +
1.217 +\begin{rail}
1.218 +  'simp' (() | 'add' | 'del')
1.219 +  ;
1.220 +\end{rail}
1.221 +
1.222 +\begin{descr}
1.223 +\item [Attribute $simp$] adds or deletes rules from the theory or proof
1.224 +  context.  The default is to add rules.
1.225 +\end{descr}
1.226
1.227
1.228  \subsection{Forward simplification}
1.229 @@ -219,33 +302,135 @@
1.230    asm_full_simplify & : & \isaratt \\
1.231  \end{matharray}
1.232
1.233 -FIXME
1.234 +These attributes provide forward rules for simplification, which should be
1.235 +used very rarely.  See the ML function of the same name in
1.237
1.238
1.239  \section{The Classical Reasoner}
1.240
1.241 -\subsection{Single step methods}
1.242 +\subsection{Basic step methods}\label{sec:classical-basic}
1.243 +
1.245 +\begin{matharray}{rcl}
1.246 +  rule & : & \isarmeth \\
1.247 +  intro & : & \isarmeth \\
1.248 +  elim & : & \isarmeth \\
1.249 +  contradiction & : & \isarmeth \\
1.250 +\end{matharray}
1.251 +
1.252 +\begin{rail}
1.253 +  ('rule' | 'intro' | 'elim') thmrefs
1.254 +  ;
1.255 +\end{rail}
1.256 +
1.257 +\begin{descr}
1.258 +\item [Method $rule$] as offered by the classical reasoner is a refinement
1.259 +  over the primitive one (see \S\ref{sec:pure-meth}).  In the case that no
1.260 +  rules are provided as arguments, it automatically determines elimination and
1.262 +  In that form it is the default method for basic proof steps.
1.263 +
1.264 +\item [Methods $intro$ and $elim$] repeatedly refine some goal by intro- or
1.265 +  elim-resolution, after having inserted the facts.  Omitting the arguments
1.266 +  refers to any suitable rules from the context, otherwise only the explicitly
1.267 +  given ones may be applied.  The latter form admits better control of what is
1.268 +  actually happening, thus it is appropriate as an initial proof method that
1.269 +  splits up certain connectives of the goal, before entering the sub-proof.
1.270 +
1.271 +\item [Method $contradiction$] solves some goal by contradiction: both $A$ and
1.272 +  $\neg A$ have to be present in the assumptions.
1.273 +\end{descr}
1.274 +
1.275 +
1.276 +\subsection{Automatic methods}\label{sec:classical-auto}
1.277
1.278 -\subsection{Automatic methods}
1.279 +\indexisarmeth{blast}
1.280 +\indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{slow}\indexisarmeth{slow_best}
1.281 +\begin{matharray}{rcl}
1.282 + blast & : & \isarmeth \\
1.283 + fast & : & \isarmeth \\
1.284 + best & : & \isarmeth \\
1.285 + slow & : & \isarmeth \\
1.286 + slow_best & : & \isarmeth \\
1.287 +\end{matharray}
1.288 +
1.289 +\railalias{slowbest}{slow\_best}
1.290 +\railterm{slowbest}
1.291 +
1.292 +\begin{rail}
1.293 +  'blast' nat? (clamod * )
1.294 +  ;
1.295 +  ('fast' | 'best' | 'slow' | slowbest) (clamod * )
1.296 +  ;
1.297 +
1.298 +  clamod: (('intro' | 'elim' | 'dest') (() | '!' | '!!') | 'del') ':' thmrefs
1.299 +  ;
1.300 +\end{rail}
1.301 +
1.302 +\begin{descr}
1.303 +\item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac}
1.304 +  in \cite[\S11]{isabelle-ref}).  The optional argument specifies a applies a
1.305 +  user-supplied search bound (default 20).
1.306 +\item [$fast$, $best$, $slow$, $slow_best$] refer to the generic classical
1.307 +  reasoner (see the corresponding tactics \texttt{fast_tac} etc.\ in
1.308 +  \cite[\S11]{isabelle-ref}).
1.309 +\end{descr}
1.310 +
1.311 +Any of above methods support additional modifiers of the context of classical
1.312 +rules.  There semantics is analogous to the attributes given in
1.313 +\S\ref{sec:classical-mod}.
1.314 +
1.315
1.316  \subsection{Combined automatic methods}
1.317
1.318 -\subsection{Modifying the context}
1.319 +\indexisarmeth{auto}\indexisarmeth{force}
1.320 +\begin{matharray}{rcl}
1.321 +  force & : & \isarmeth \\
1.322 +  auto & : & \isarmeth \\
1.323 +\end{matharray}
1.324 +
1.325 +\begin{rail}
1.326 +  ('force' | 'auto') (clasimpmod * )
1.327 +  ;
1.328
1.329 +  clasimpmod: ('simp' ('add' | 'del' | 'only') | other |
1.330 +    (('intro' | 'elim' | 'dest') (() | '!' | '!!') | 'del')) ':' thmrefs
1.331 +\end{rail}
1.332
1.333 +\begin{descr}
1.334 +\item [$force$ and $auto$] provide access to Isabelle's combined
1.335 +  simplification and classical reasoning tactics.  See \texttt{force_tac} and
1.337 +  modifier arguments correspond to those given in \S\ref{sec:simp} and
1.338 +  \S\ref{sec:classical-auto}.
1.339 +\end{descr}
1.340 +
1.341 +\subsection{Modifying the context}\label{sec:classical-mod}
1.342
1.343 -%\indexisarcmd{}
1.344 -%\begin{matharray}{rcl}
1.345 -%  \isarcmd{} & : & \isartrans{}{} \\
1.346 -%\end{matharray}
1.347 +\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}\indexisaratt{delrule}
1.348 +\begin{matharray}{rcl}
1.349 +  intro & : & \isaratt \\
1.350 +  elim & : & \isaratt \\
1.351 +  dest & : & \isaratt \\
1.352 +  delrule & : & \isaratt \\
1.353 +\end{matharray}
1.354
1.355 -%\begin{rail}
1.356 -
1.357 -%\end{rail}
1.358 +\begin{rail}
1.359 +  ('intro' | 'elim' | 'dest') (() | '!' | '!!')
1.360 +  ;
1.361 +\end{rail}
1.362
1.363 -%\begin{descr}
1.364 -%\item []
1.365 -%\end{descr}
1.366 +\begin{descr}
1.367 +\item [Attributes $intro$, $elim$, and $dest$] add introduction, elimination,
1.368 +  and destruct rules, respectively.  By default, rules are considered as
1.369 +  \emph{safe}, while a single !'' classifies as \emph{unsafe}, and !!'' as
1.370 +  \emph{extra} (i.e.\ not applied in the search-oriented automatic methods).
1.371 +
1.372 +\item [Attribute $delrule$] deletes introduction or elimination rules from the
1.373 +  context.  Destruction rules would have to be turned into elimination rules
1.374 +  first, e.g.\ by using the $elimify$ attribute.
1.375 +\end{descr}
1.376
1.377
1.378  %%% Local Variables: