doc-src/IsarRef/generic.tex
author wenzelm
Tue Mar 21 17:32:43 2000 +0100 (2000-03-21)
changeset 8547 93b8685d004b
parent 8517 062e6cd78534
child 8594 d2e2a3df6871
permissions -rw-r--r--
tuned;
     1 
     2 \chapter{Generic Tools and Packages}\label{ch:gen-tools}
     3 
     4 \section{Axiomatic Type Classes}\label{sec:axclass}
     5 
     6 \indexisarcmd{axclass}\indexisarcmd{instance}\indexisarmeth{intro-classes}
     7 \begin{matharray}{rcl}
     8   \isarcmd{axclass} & : & \isartrans{theory}{theory} \\
     9   \isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
    10   intro_classes & : & \isarmeth \\
    11 \end{matharray}
    12 
    13 Axiomatic type classes are provided by Isabelle/Pure as a \emph{definitional}
    14 interface to type classes (cf.~\S\ref{sec:classes}).  Thus any object logic
    15 may make use of this light-weight mechanism of abstract theories
    16 \cite{Wenzel:1997:TPHOL}.  There is also a tutorial on \emph{Using Axiomatic
    17   Type Classes in Isabelle} that is part of the standard Isabelle
    18 documentation.
    19 %FIXME cite
    20 
    21 \begin{rail}
    22   'axclass' classdecl (axmdecl prop comment? +)
    23   ;
    24   'instance' (nameref '<' nameref | nameref '::' simplearity) comment?
    25   ;
    26 \end{rail}
    27 
    28 \begin{descr}
    29 \item [$\isarkeyword{axclass}~c < \vec c~axms$] defines an axiomatic type
    30   class as the intersection of existing classes, with additional axioms
    31   holding.  Class axioms may not contain more than one type variable.  The
    32   class axioms (with implicit sort constraints added) are bound to the given
    33   names.  Furthermore a class introduction rule is generated, which is
    34   employed by method $intro_classes$ to support instantiation proofs of this
    35   class.
    36   
    37 \item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~t ::
    38   (\vec s)c$] setup a goal stating a class relation or type arity.  The proof
    39   would usually proceed by $intro_classes$, and then establish the
    40   characteristic theorems of the type classes involved.  After finishing the
    41   proof, the theory will be augmented by a type signature declaration
    42   corresponding to the resulting theorem.
    43 \item [$intro_classes$] repeatedly expands all class introduction rules of
    44   this theory.
    45 \end{descr}
    46 
    47 
    48 \section{Calculational proof}\label{sec:calculation}
    49 
    50 \indexisarcmd{also}\indexisarcmd{finally}\indexisaratt{trans}
    51 \begin{matharray}{rcl}
    52   \isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\
    53   \isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\
    54   trans & : & \isaratt \\
    55 \end{matharray}
    56 
    57 Calculational proof is forward reasoning with implicit application of
    58 transitivity rules (such those of $=$, $\le$, $<$).  Isabelle/Isar maintains
    59 an auxiliary register $calculation$\indexisarthm{calculation} for accumulating
    60 results obtained by transitivity composed with the current result.  Command
    61 $\ALSO$ updates $calculation$ involving $this$, while $\FINALLY$ exhibits the
    62 final $calculation$ by forward chaining towards the next goal statement.  Both
    63 commands require valid current facts, i.e.\ may occur only after commands that
    64 produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or some finished proof of
    65 $\HAVENAME$, $\SHOWNAME$ etc.
    66 
    67 Also note that the automatic term abbreviation ``$\dots$'' has its canonical
    68 application with calculational proofs.  It automatically refers to the
    69 argument\footnote{The argument of a curried infix expression is its right-hand
    70   side.} of the preceding statement.
    71 
    72 Isabelle/Isar calculations are implicitly subject to block structure in the
    73 sense that new threads of calculational reasoning are commenced for any new
    74 block (as opened by a local goal, for example).  This means that, apart from
    75 being able to nest calculations, there is no separate \emph{begin-calculation}
    76 command required.
    77 
    78 \begin{rail}
    79   ('also' | 'finally') transrules? comment?
    80   ;
    81   'trans' (() | 'add' | 'del')
    82   ;
    83 
    84   transrules: '(' thmrefs ')' interest?
    85   ;
    86 \end{rail}
    87 
    88 \begin{descr}
    89 \item [$\ALSO~(\vec a)$] maintains the auxiliary $calculation$ register as
    90   follows.  The first occurrence of $\ALSO$ in some calculational thread
    91   initializes $calculation$ by $this$. Any subsequent $\ALSO$ on the same
    92   level of block-structure updates $calculation$ by some transitivity rule
    93   applied to $calculation$ and $this$ (in that order).  Transitivity rules are
    94   picked from the current context plus those given as explicit arguments (the
    95   latter have precedence).
    96   
    97 \item [$\FINALLY~(\vec a)$] maintaining $calculation$ in the same way as
    98   $\ALSO$, and concludes the current calculational thread.  The final result
    99   is exhibited as fact for forward chaining towards the next goal. Basically,
   100   $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$.  Note that
   101   ``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and
   102   ``$\FINALLY~\HAVE{}{\phi}~\DOT$'' are typical idioms for concluding
   103   calculational proofs.
   104   
   105 \item [$trans$] declares theorems as transitivity rules.
   106 \end{descr}
   107 
   108 
   109 \section{Named local contexts (cases)}\label{sec:cases}
   110 
   111 \indexisarcmd{case}\indexisarcmd{print-cases}
   112 \indexisaratt{case-names}\indexisaratt{params}
   113 \begin{matharray}{rcl}
   114   \isarcmd{case} & : & \isartrans{proof(state)}{proof(state)} \\
   115   \isarcmd{print_cases}^* & : & \isarkeep{proof} \\
   116   case_names & : & \isaratt \\
   117   params & : & \isaratt \\
   118 \end{matharray}
   119 
   120 Basically, Isar proof contexts are built up explicitly using commands like
   121 $\FIXNAME$, $\ASSUMENAME$ etc.\ (see \S\ref{sec:proof-context}).  In typical
   122 verification tasks this can become hard to manage, though.  In particular, a
   123 large number of local contexts may emerge from case analysis or induction over
   124 inductive sets and types.
   125 
   126 \medskip
   127 
   128 The $\CASENAME$ command provides a shorthand to refer to certain parts of
   129 logical context symbolically.  Proof methods may provide an environment of
   130 named ``cases'' of the form $c\colon \vec x, \vec \phi$.  Then the effect of
   131 $\CASE{c}$ is exactly the same as $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$.
   132 
   133 It is important to note that $\CASENAME$ does \emph{not} provide any means to
   134 peek at the current goal state, which is treated as strictly non-observable in
   135 Isar!  Instead, the cases considered here usually emerge in a canonical way
   136 from certain pieces of specification that appear in the theory somewhere else
   137 (e.g.\ in an inductive definition, or recursive function).  See also
   138 \S\ref{sec:induct-method} for more details of how this works in HOL.
   139 
   140 \medskip
   141 
   142 Named cases may be exhibited in the current proof context only if both the
   143 proof method and the rules involved support this.  Case names and parameters
   144 of basic rules may be declared by hand as well, by using appropriate
   145 attributes.  Thus variant versions of rules that have been derived manually
   146 may be used in advanced case analysis later.
   147 
   148 \railalias{casenames}{case\_names}
   149 \railterm{casenames}
   150 
   151 \begin{rail}
   152   'case' nameref attributes?
   153   ;
   154   casenames (name + )
   155   ;
   156   'params' ((name * ) + 'and')
   157   ;
   158 \end{rail}
   159 %FIXME bug in rail
   160 
   161 \begin{descr}
   162 \item [$\CASE{c}$] invokes a named local context $c\colon \vec x, \vec \phi$,
   163   as provided by an appropriate proof method (such as $cases$ and $induct$ in
   164   Isabelle/HOL, see \S\ref{sec:induct-method}).  The command $\CASE{c}$
   165   abbreviates $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$.
   166 \item [$\isarkeyword{print_cases}$] prints all local contexts of the current
   167   state, using Isar proof language notation.  This is a diagnostic command;
   168   $undo$ does not apply.
   169 \item [$case_names~\vec c$] declares names for the local contexts of premises
   170   of some theorem; $\vec c$ refers to the \emph{suffix} of the list premises.
   171 \item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of
   172   premises $1, \dots, n$ of some theorem.  An empty list of names may be given
   173   to skip positions, leaving the present parameters unchanged.
   174 \end{descr}
   175 
   176 
   177 \section{Generalized existence}
   178 
   179 \indexisarcmd{obtain}
   180 \begin{matharray}{rcl}
   181   \isarcmd{obtain} & : & \isartrans{proof(prove)}{proof(state)} \\
   182 \end{matharray}
   183 
   184 Generalized existence reasoning means that additional elements with certain
   185 properties are introduced, together with a soundness proof of that context
   186 change (the rest of the main goal is left unchanged).
   187 
   188 Syntactically, the $\OBTAINNAME$ language element is like an initial proof
   189 method to the present goal, followed by a proof of its additional claim,
   190 followed by the actual context commands (using the syntax of $\FIXNAME$ and
   191 $\ASSUMENAME$, see \S\ref{sec:proof-context}).
   192 
   193 \begin{rail}
   194   'obtain' (vars + 'and') comment? \\ 'where' (assm comment? + 'and')
   195   ;
   196 \end{rail}
   197 
   198 $\OBTAINNAME$ is defined as a derived Isar command as follows; here the
   199 preceding goal shall be $\psi$, with (optional) facts $\vec b$ indicated for
   200 forward chaining.
   201 \begin{matharray}{l}
   202   \OBTAIN{\vec x}{a}{\vec \phi}~~\langle proof\rangle \equiv {} \\[0.5ex]
   203   \quad \PROOF{succeed} \\
   204   \qquad \DEF{}{thesis \equiv \psi} \\
   205   \qquad \PRESUME{that}{\All{\vec x} \vec\phi \Imp thesis} \\
   206   \qquad \FROM{\vec b}~\SHOW{}{thesis}~~\langle proof\rangle \\
   207   \quad \NEXT \\
   208   \qquad \FIX{\vec x}~\ASSUME{a}{\vec\phi} \\
   209 \end{matharray}
   210 
   211 Typically, the soundness proof is relatively straight-forward, often just by
   212 canonical automated tools such as $\BY{simp}$ (see \S\ref{sec:simp}) or
   213 $\BY{blast}$ (see \S\ref{sec:classical-auto}).  Note that the ``$that$''
   214 presumption above is usually declared as simplification and (unsafe)
   215 introduction rule, depending on the object-logic's policy,
   216 though.\footnote{HOL and HOLCF do this already.}
   217 
   218 The original goal statement is wrapped into a local definition in order to
   219 avoid any automated tools descending into it.  Usually, any statement would
   220 admit the intended reduction anyway; only in very rare cases $thesis_def$ has
   221 to be expanded to complete the soundness proof.
   222 
   223 \medskip
   224 
   225 In a sense, $\OBTAINNAME$ represents at the level of Isar proofs what would be
   226 meta-logical existential quantifiers and conjunctions.  This concept has a
   227 broad range of useful applications, ranging from plain elimination (or even
   228 introduction) of object-level existentials and conjunctions, to elimination
   229 over results of symbolic evaluation of recursive definitions, for example.
   230 
   231 
   232 \section{Miscellaneous methods and attributes}
   233 
   234 \indexisarmeth{unfold}\indexisarmeth{fold}
   235 \indexisarmeth{erule}\indexisarmeth{drule}\indexisarmeth{frule}
   236 \indexisarmeth{fail}\indexisarmeth{succeed}
   237 \begin{matharray}{rcl}
   238   unfold & : & \isarmeth \\
   239   fold & : & \isarmeth \\[0.5ex]
   240   erule^* & : & \isarmeth \\
   241   drule^* & : & \isarmeth \\
   242   frule^* & : & \isarmeth \\[0.5ex]
   243   succeed & : & \isarmeth \\
   244   fail & : & \isarmeth \\
   245 \end{matharray}
   246 
   247 \begin{rail}
   248   ('fold' | 'unfold' | 'erule' | 'drule' | 'frule') thmrefs
   249   ;
   250 \end{rail}
   251 
   252 \begin{descr}
   253 \item [$unfold~\vec a$ and $fold~\vec a$] expand and fold back again the given
   254   meta-level definitions throughout all goals; any facts provided are inserted
   255   into the goal and subject to rewriting as well.
   256 \item [$erule~\vec a$, $drule~\vec a$, and $frule~\vec a$] are similar to the
   257   basic $rule$ method (see \S\ref{sec:pure-meth-att}), but apply rules by
   258   elim-resolution, destruct-resolution, and forward-resolution, respectively
   259   \cite{isabelle-ref}.  These are improper method, mainly for experimentation
   260   and emulating tactic scripts.
   261   
   262   Different modes of basic rule application are usually expressed in Isar at
   263   the proof language level, rather than via implicit proof state
   264   manipulations.  For example, a proper single-step elimination would be done
   265   using the basic $rule$ method, with forward chaining of current facts.
   266 \item [$succeed$] yields a single (unchanged) result; it is the identity of
   267   the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
   268 \item [$fail$] yields an empty result sequence; it is the identity of the
   269   ``\texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
   270 \end{descr}
   271 
   272 
   273 \indexisaratt{standard}
   274 \indexisaratt{elimify}
   275 
   276 \indexisaratt{RS}\indexisaratt{COMP}
   277 \indexisaratt{where}
   278 \indexisaratt{tag}\indexisaratt{untag}
   279 \indexisaratt{transfer}
   280 \indexisaratt{export}
   281 \indexisaratt{unfold}\indexisaratt{fold}
   282 \begin{matharray}{rcl}
   283   tag & : & \isaratt \\
   284   untag & : & \isaratt \\[0.5ex]
   285   RS & : & \isaratt \\
   286   COMP & : & \isaratt \\[0.5ex]
   287   where & : & \isaratt \\[0.5ex]
   288   unfold & : & \isaratt \\
   289   fold & : & \isaratt \\[0.5ex]
   290   standard & : & \isaratt \\
   291   elimify & : & \isaratt \\
   292   export^* & : & \isaratt \\
   293   transfer & : & \isaratt \\[0.5ex]
   294 \end{matharray}
   295 
   296 \begin{rail}
   297   'tag' (nameref+)
   298   ;
   299   'untag' name
   300   ;
   301   ('RS' | 'COMP') nat? thmref
   302   ;
   303   'where' (name '=' term * 'and')
   304   ;
   305   ('unfold' | 'fold') thmrefs
   306   ;
   307 \end{rail}
   308 
   309 \begin{descr}
   310 \item [$tag~name~args$ and $untag~name$] add and remove $tags$ of some
   311   theorem.  Tags may be any list of strings that serve as comment for some
   312   tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the
   313   result).  The first string is considered the tag name, the rest its
   314   arguments.  Note that untag removes any tags of the same name.
   315 \item [$RS~n~a$ and $COMP~n~a$] compose rules.  $RS$ resolves with the $n$-th
   316   premise of $a$; $COMP$ is a version of $RS$ that skips the automatic lifting
   317   process that is normally intended (cf.\ \texttt{RS} and \texttt{COMP} in
   318   \cite[\S5]{isabelle-ref}).
   319 \item [$where~\vec x = \vec t$] perform named instantiation of schematic
   320   variables occurring in a theorem.  Unlike instantiation tactics (such as
   321   \texttt{res_inst_tac}, see \cite{isabelle-ref}), actual schematic variables
   322   have to be specified (e.g.\ $\Var{x@3}$).
   323   
   324 \item [$unfold~\vec a$ and $fold~\vec a$] expand and fold back again the given
   325   meta-level definitions throughout a rule.
   326  
   327 \item [$standard$] puts a theorem into the standard form of object-rules, just
   328   as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).
   329   
   330 \item [$elimify$] turns an destruction rule into an elimination, just as the
   331   ML function \texttt{make\_elim} (see \cite{isabelle-ref}).
   332   
   333 \item [$export$] lifts a local result out of the current proof context,
   334   generalizing all fixed variables and discharging all assumptions.  Note that
   335   proper incremental export is already done as part of the basic Isar
   336   machinery.  This attribute is mainly for experimentation.
   337   
   338 \item [$transfer$] promotes a theorem to the current theory context, which has
   339   to enclose the former one.  This is done automatically whenever rules are
   340   joined by inference.
   341 
   342 \end{descr}
   343 
   344 
   345 \section{The Simplifier}
   346 
   347 \subsection{Simplification methods}\label{sec:simp}
   348 
   349 \indexisarmeth{simp}\indexisarmeth{simp-all}
   350 \begin{matharray}{rcl}
   351   simp & : & \isarmeth \\
   352   simp_all & : & \isarmeth \\
   353 \end{matharray}
   354 
   355 \railalias{simpall}{simp\_all}
   356 \railterm{simpall}
   357 
   358 \begin{rail}
   359   ('simp' | simpall) ('!' ?) (simpmod * )
   360   ;
   361 
   362   simpmod: ('add' | 'del' | 'only' | 'split' (() | 'add' | 'del') | 'other') ':' thmrefs
   363   ;
   364 \end{rail}
   365 
   366 \begin{descr}
   367 \item [$simp$] invokes Isabelle's simplifier, after declaring additional rules
   368   according to the arguments given.  Note that the \railtoken{only} modifier
   369   first removes all other rewrite rules, congruences, and looper tactics
   370   (including splits), and then behaves like \railtoken{add}.
   371   
   372   The \railtoken{split} modifiers add or delete rules for the Splitter (see
   373   also \cite{isabelle-ref}), the default is to add.  This works only if the
   374   Simplifier method has been properly setup to include the Splitter (all major
   375   object logics such HOL, HOLCF, FOL, ZF do this already).
   376   
   377   The \railtoken{other} modifier ignores its arguments.  Nevertheless,
   378   additional kinds of rules may be declared by including appropriate
   379   attributes in the specification.
   380 \item [$simp_all$] is similar to $simp$, but acts on all goals.
   381 \end{descr}
   382 
   383 Internally, the $simp$ method is based on \texttt{asm_full_simp_tac}
   384 \cite[\S10]{isabelle-ref}, but is much better behaved in practice.  Just the
   385 local premises of the actual goal are involved by default.  Additional facts
   386 may be inserted via forward-chaining (using $\THEN$, $\FROMNAME$ etc.).  The
   387 full context of assumptions is only included in the $simp!$ version, which
   388 should be used with some care, though.
   389 
   390 Note that there is no separate $split$ method.  The effect of
   391 \texttt{split_tac} can be simulated by $(simp~only\colon~split\colon~\vec a)$.
   392 
   393 
   394 \subsection{Declaring rules}
   395 
   396 \indexisaratt{simp}\indexisaratt{split}
   397 \begin{matharray}{rcl}
   398   simp & : & \isaratt \\
   399   split & : & \isaratt \\
   400 \end{matharray}
   401 
   402 \begin{rail}
   403   ('simp' | 'split') (() | 'add' | 'del')
   404   ;
   405 \end{rail}
   406 
   407 \begin{descr}
   408 \item [$simp$] declares simplification rules.
   409 \item [$split$] declares split rules.
   410 \end{descr}
   411 
   412 
   413 \subsection{Forward simplification}
   414 
   415 \indexisaratt{simplify}\indexisaratt{asm-simplify}
   416 \indexisaratt{full-simplify}\indexisaratt{asm-full-simplify}
   417 \begin{matharray}{rcl}
   418   simplify & : & \isaratt \\
   419   asm_simplify & : & \isaratt \\
   420   full_simplify & : & \isaratt \\
   421   asm_full_simplify & : & \isaratt \\
   422 \end{matharray}
   423 
   424 These attributes provide forward rules for simplification, which should be
   425 used only very rarely.  There are no separate options for declaring
   426 simplification rules locally.
   427 
   428 See the ML functions of the same name in \cite[\S10]{isabelle-ref} for more
   429 information.
   430 
   431 
   432 \section{The Classical Reasoner}
   433 
   434 \subsection{Basic methods}\label{sec:classical-basic}
   435 
   436 \indexisarmeth{rule}\indexisarmeth{intro}
   437 \indexisarmeth{elim}\indexisarmeth{default}\indexisarmeth{contradiction}
   438 \begin{matharray}{rcl}
   439   rule & : & \isarmeth \\
   440   intro & : & \isarmeth \\
   441   elim & : & \isarmeth \\
   442   contradiction & : & \isarmeth \\
   443 \end{matharray}
   444 
   445 \begin{rail}
   446   ('rule' | 'intro' | 'elim') thmrefs?
   447   ;
   448 \end{rail}
   449 
   450 \begin{descr}
   451 \item [$rule$] as offered by the classical reasoner is a refinement over the
   452   primitive one (see \S\ref{sec:pure-meth-att}).  In case that no rules are
   453   provided as arguments, it automatically determines elimination and
   454   introduction rules from the context (see also \S\ref{sec:classical-mod}).
   455   This is made the default method for basic proof steps, such as $\PROOFNAME$
   456   and ``$\DDOT$'' (two dots), see also \S\ref{sec:proof-steps} and
   457   \S\ref{sec:pure-meth-att}.
   458   
   459 \item [$intro$ and $elim$] repeatedly refine some goal by intro- or
   460   elim-resolution, after having inserted any facts.  Omitting the arguments
   461   refers to any suitable rules declared in the context, otherwise only the
   462   explicitly given ones may be applied.  The latter form admits better control
   463   of what actually happens, thus it is very appropriate as an initial method
   464   for $\PROOFNAME$ that splits up certain connectives of the goal, before
   465   entering the actual sub-proof.
   466   
   467 \item [$contradiction$] solves some goal by contradiction, deriving any result
   468   from both $\neg A$ and $A$.  Facts, which are guaranteed to participate, may
   469   appear in either order.
   470 \end{descr}
   471 
   472 
   473 \subsection{Automated methods}\label{sec:classical-auto}
   474 
   475 \indexisarmeth{blast}
   476 \indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{slow}\indexisarmeth{slow-best}
   477 \begin{matharray}{rcl}
   478  blast & : & \isarmeth \\
   479  fast & : & \isarmeth \\
   480  best & : & \isarmeth \\
   481  slow & : & \isarmeth \\
   482  slow_best & : & \isarmeth \\
   483 \end{matharray}
   484 
   485 \railalias{slowbest}{slow\_best}
   486 \railterm{slowbest}
   487 
   488 \begin{rail}
   489   'blast' ('!' ?) nat? (clamod * )
   490   ;
   491   ('fast' | 'best' | 'slow' | slowbest) ('!' ?) (clamod * )
   492   ;
   493 
   494   clamod: (('intro' | 'elim' | 'dest') (() | '?' | '??') | 'del') ':' thmrefs
   495   ;
   496 \end{rail}
   497 
   498 \begin{descr}
   499 \item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac}
   500   in \cite[\S11]{isabelle-ref}).  The optional argument specifies a
   501   user-supplied search bound (default 20).
   502 \item [$fast$, $best$, $slow$, $slow_best$] refer to the generic classical
   503   reasoner (see \cite[\S11]{isabelle-ref}, tactic \texttt{fast_tac} etc).
   504 \end{descr}
   505 
   506 Any of above methods support additional modifiers of the context of classical
   507 rules.  Their semantics is analogous to the attributes given in
   508 \S\ref{sec:classical-mod}.  Facts provided by forward chaining are
   509 inserted\footnote{These methods usually cannot make proper use of actual rules
   510   inserted that way, though.} into the goal before doing the search.  The
   511 ``!''~argument causes the full context of assumptions to be included as well.
   512 This is slightly less hazardous than for the Simplifier (see
   513 \S\ref{sec:simp}).
   514 
   515 
   516 \subsection{Combined automated methods}
   517 
   518 \indexisarmeth{auto}\indexisarmeth{force}
   519 \begin{matharray}{rcl}
   520   force & : & \isarmeth \\
   521   auto & : & \isarmeth \\
   522 \end{matharray}
   523 
   524 \begin{rail}
   525   ('force' | 'auto') ('!' ?) (clasimpmod * )
   526   ;
   527 
   528   clasimpmod: ('simp' (() | 'add' | 'del' | 'only') | 'other' |
   529     ('split' (() | 'add' | 'del')) |
   530     (('intro' | 'elim' | 'dest') (() | '?' | '??') | 'del')) ':' thmrefs
   531 \end{rail}
   532 
   533 \begin{descr}
   534 \item [$force$ and $auto$] provide access to Isabelle's combined
   535   simplification and classical reasoning tactics.  See \texttt{force_tac} and
   536   \texttt{auto_tac} in \cite[\S11]{isabelle-ref} for more information.  The
   537   modifier arguments correspond to those given in \S\ref{sec:simp} and
   538   \S\ref{sec:classical-auto}.  Just note that the ones related to the
   539   Simplifier are prefixed by \railtoken{simp} here.
   540   
   541   Facts provided by forward chaining are inserted into the goal before doing
   542   the search.  The ``!''~argument causes the full context of assumptions to be
   543   included as well.
   544 \end{descr}
   545 
   546 
   547 \subsection{Declaring rules}\label{sec:classical-mod}
   548 
   549 \indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
   550 \indexisaratt{iff}\indexisaratt{delrule}
   551 \begin{matharray}{rcl}
   552   intro & : & \isaratt \\
   553   elim & : & \isaratt \\
   554   dest & : & \isaratt \\
   555   iff & : & \isaratt \\
   556   delrule & : & \isaratt \\
   557 \end{matharray}
   558 
   559 \begin{rail}
   560   ('intro' | 'elim' | 'dest') (() | '?' | '??')
   561   ;
   562 \end{rail}
   563 
   564 \begin{descr}
   565 \item [$intro$, $elim$, and $dest$] declare introduction, elimination, and
   566   destruct rules, respectively.  By default, rules are considered as
   567   \emph{safe}, while a single ``?'' classifies as \emph{unsafe}, and ``??'' as
   568   \emph{extra} (i.e.\ not applied in the search-oriented automated methods,
   569   but only in single-step methods such as $rule$).
   570   
   571 \item [$iff$] declares equations both as rules for the Simplifier and
   572   Classical Reasoner.
   573 
   574 \item [$delrule$] deletes introduction or elimination rules from the context.
   575   Note that destruction rules would have to be turned into elimination rules
   576   first, e.g.\ by using the $elimify$ attribute.
   577 \end{descr}
   578 
   579 
   580 %%% Local Variables: 
   581 %%% mode: latex
   582 %%% TeX-master: "isar-ref"
   583 %%% End: