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