doc-src/IsarRef/generic.tex
author wenzelm
Mon Aug 14 18:49:23 2000 +0200 (2000-08-14)
changeset 9606 1bf495402ae9
parent 9480 7afb808b6b3e
child 9614 8ca1fc75230e
permissions -rw-r--r--
moved tactic emulation methods here;
added print_trans_rules;
renamed "res_inst_tac' etc. to 'rule_tac' etc.;
added 'fastsimp';
     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 \indexisarcmd{print-trans-rules}\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   \isarcmd{print_trans_rules} & : & \isarkeep{theory~|~proof} \\
    63   trans & : & \isaratt \\
    64 \end{matharray}
    65 
    66 Calculational proof is forward reasoning with implicit application of
    67 transitivity rules (such those of $=$, $\le$, $<$).  Isabelle/Isar maintains
    68 an auxiliary register $calculation$\indexisarthm{calculation} for accumulating
    69 results obtained by transitivity composed with the current result.  Command
    70 $\ALSO$ updates $calculation$ involving $this$, while $\FINALLY$ exhibits the
    71 final $calculation$ by forward chaining towards the next goal statement.  Both
    72 commands require valid current facts, i.e.\ may occur only after commands that
    73 produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or some finished proof of
    74 $\HAVENAME$, $\SHOWNAME$ etc.  The $\MOREOVER$ and $\ULTIMATELY$ commands are
    75 similar to $\ALSO$ and $\FINALLY$, but only collect further results in
    76 $calculation$ without applying any rules yet.
    77 
    78 Also note that the automatic term abbreviation ``$\dots$'' has its canonical
    79 application with calculational proofs.  It refers to the argument\footnote{The
    80   argument of a curried infix expression is its right-hand side.} of the
    81 preceding statement.
    82 
    83 Isabelle/Isar calculations are implicitly subject to block structure in the
    84 sense that new threads of calculational reasoning are commenced for any new
    85 block (as opened by a local goal, for example).  This means that, apart from
    86 being able to nest calculations, there is no separate \emph{begin-calculation}
    87 command required.
    88 
    89 \medskip
    90 
    91 The Isar calculation proof commands may be defined as
    92 follows:\footnote{Internal bookkeeping such as proper handling of
    93   block-structure has been suppressed.}
    94 \begin{matharray}{rcl}
    95   \ALSO@0 & \equiv & \NOTE{calculation}{this} \\
    96   \ALSO@{n+1} & \equiv & \NOTE{calculation}{trans~[OF~calculation~this]} \\[0.5ex]
    97   \FINALLY & \equiv & \ALSO~\FROM{calculation} \\
    98   \MOREOVER & \equiv & \NOTE{calculation}{calculation~this} \\
    99   \ULTIMATELY & \equiv & \MOREOVER~\FROM{calculation} \\
   100 \end{matharray}
   101 
   102 \begin{rail}
   103   ('also' | 'finally') transrules? comment?
   104   ;
   105   ('moreover' | 'ultimately') comment?
   106   ;
   107   'trans' (() | 'add' | 'del')
   108   ;
   109 
   110   transrules: '(' thmrefs ')' interest?
   111   ;
   112 \end{rail}
   113 
   114 \begin{descr}
   115 \item [$\ALSO~(\vec a)$] maintains the auxiliary $calculation$ register as
   116   follows.  The first occurrence of $\ALSO$ in some calculational thread
   117   initializes $calculation$ by $this$. Any subsequent $\ALSO$ on the same
   118   level of block-structure updates $calculation$ by some transitivity rule
   119   applied to $calculation$ and $this$ (in that order).  Transitivity rules are
   120   picked from the current context plus those given as explicit arguments (the
   121   latter have precedence).
   122   
   123 \item [$\FINALLY~(\vec a)$] maintaining $calculation$ in the same way as
   124   $\ALSO$, and concludes the current calculational thread.  The final result
   125   is exhibited as fact for forward chaining towards the next goal. Basically,
   126   $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$.  Note that
   127   ``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and
   128   ``$\FINALLY~\HAVE{}{\phi}~\DOT$'' are typical idioms for concluding
   129   calculational proofs.
   130   
   131 \item [$\MOREOVER$ and $\ULTIMATELY$] are analogous to $\ALSO$ and $\FINALLY$,
   132   but collect results only, without applying rules.
   133   
   134 \item [$\isarkeyword{print_trans_rules}$] prints the list of transitivity
   135   rules declared in the current context.
   136   
   137 \item [$trans$] declares theorems as transitivity rules.
   138  
   139 \end{descr}
   140 
   141 
   142 \section{Named local contexts (cases)}\label{sec:cases}
   143 
   144 \indexisarcmd{case}\indexisarcmd{print-cases}
   145 \indexisaratt{case-names}\indexisaratt{params}
   146 \begin{matharray}{rcl}
   147   \isarcmd{case} & : & \isartrans{proof(state)}{proof(state)} \\
   148   \isarcmd{print_cases}^* & : & \isarkeep{proof} \\
   149   case_names & : & \isaratt \\
   150   params & : & \isaratt \\
   151 \end{matharray}
   152 
   153 Basically, Isar proof contexts are built up explicitly using commands like
   154 $\FIXNAME$, $\ASSUMENAME$ etc.\ (see \S\ref{sec:proof-context}).  In typical
   155 verification tasks this can become hard to manage, though.  In particular, a
   156 large number of local contexts may emerge from case analysis or induction over
   157 inductive sets and types.
   158 
   159 \medskip
   160 
   161 The $\CASENAME$ command provides a shorthand to refer to certain parts of
   162 logical context symbolically.  Proof methods may provide an environment of
   163 named ``cases'' of the form $c\colon \vec x, \vec \phi$.  Then the effect of
   164 $\CASE{c}$ is exactly the same as $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$.
   165 
   166 It is important to note that $\CASENAME$ does \emph{not} provide any means to
   167 peek at the current goal state, which is treated as strictly non-observable in
   168 Isar!  Instead, the cases considered here usually emerge in a canonical way
   169 from certain pieces of specification that appear in the theory somewhere else
   170 (e.g.\ in an inductive definition, or recursive function).  See also
   171 \S\ref{sec:induct-method} for more details of how this works in HOL.
   172 
   173 \medskip
   174 
   175 Named cases may be exhibited in the current proof context only if both the
   176 proof method and the rules involved support this.  Case names and parameters
   177 of basic rules may be declared by hand as well, by using appropriate
   178 attributes.  Thus variant versions of rules that have been derived manually
   179 may be used in advanced case analysis later.
   180 
   181 \railalias{casenames}{case\_names}
   182 \railterm{casenames}
   183 
   184 \begin{rail}
   185   'case' nameref attributes?
   186   ;
   187   casenames (name + )
   188   ;
   189   'params' ((name * ) + 'and')
   190   ;
   191 \end{rail}
   192 %FIXME bug in rail
   193 
   194 \begin{descr}
   195 \item [$\CASE{c}$] invokes a named local context $c\colon \vec x, \vec \phi$,
   196   as provided by an appropriate proof method (such as $cases$ and $induct$ in
   197   Isabelle/HOL, see \S\ref{sec:induct-method}).  The command $\CASE{c}$
   198   abbreviates $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$.
   199 \item [$\isarkeyword{print_cases}$] prints all local contexts of the current
   200   state, using Isar proof language notation.  This is a diagnostic command;
   201   $undo$ does not apply.
   202 \item [$case_names~\vec c$] declares names for the local contexts of premises
   203   of some theorem; $\vec c$ refers to the \emph{suffix} of the list premises.
   204 \item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of
   205   premises $1, \dots, n$ of some theorem.  An empty list of names may be given
   206   to skip positions, leaving the present parameters unchanged.
   207 \end{descr}
   208 
   209 
   210 \section{Generalized existence}
   211 
   212 \indexisarcmd{obtain}
   213 \begin{matharray}{rcl}
   214   \isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\
   215 \end{matharray}
   216 
   217 Generalized existence means that additional elements with certain properties
   218 may introduced in the current context.  Technically, the $\OBTAINNAME$
   219 language element is like a declaration of $\FIXNAME$ and $\ASSUMENAME$ (see
   220 also see \S\ref{sec:proof-context}), together with a soundness proof of its
   221 additional claim.  According to the nature of existential reasoning,
   222 assumptions get eliminated from any result exported from the context later,
   223 provided that the corresponding parameters do \emph{not} occur in the
   224 conclusion.
   225 
   226 \begin{rail}
   227   'obtain' (vars + 'and') comment? \\ 'where' (assm comment? + 'and')
   228   ;
   229 \end{rail}
   230 
   231 $\OBTAINNAME$ is defined as a derived Isar command as follows, where $\vec b$
   232 shall refer to (optional) facts indicated for forward chaining.
   233 \begin{matharray}{l}
   234   \langle facts~\vec b\rangle \\
   235   \OBTAIN{\vec x}{a}{\vec \phi}~~\langle proof\rangle \equiv {} \\[1ex]
   236   \quad \BG \\
   237   \qquad \FIX{thesis} \\
   238   \qquad \ASSUME{that [simp, intro]}{\All{\vec x} \vec\phi \Imp thesis} \\
   239   \qquad \FROM{\vec b}~\HAVE{}{thesis}~~\langle proof\rangle \\
   240   \quad \EN \\
   241   \quad \FIX{\vec x}~\ASSUMENAME^{\ast}~{a}~{\vec\phi} \\
   242 \end{matharray}
   243 
   244 Typically, the soundness proof is relatively straight-forward, often just by
   245 canonical automated tools such as $\BY{simp}$ (see \S\ref{sec:simp}) or
   246 $\BY{blast}$ (see \S\ref{sec:classical-auto}).  Accordingly, the ``$that$''
   247 reduction above is declared as simplification and introduction rule.
   248 
   249 \medskip
   250 
   251 In a sense, $\OBTAINNAME$ represents at the level of Isar proofs what would be
   252 meta-logical existential quantifiers and conjunctions.  This concept has a
   253 broad range of useful applications, ranging from plain elimination (or even
   254 introduction) of object-level existentials and conjunctions, to elimination
   255 over results of symbolic evaluation of recursive definitions, for example.
   256 Also note that $\OBTAINNAME$ without parameters acts much like $\HAVENAME$,
   257 where the result is treated as an assumption.
   258 
   259 
   260 \section{Miscellaneous methods and attributes}
   261 
   262 \indexisarmeth{unfold}\indexisarmeth{fold}\indexisarmeth{insert}
   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   insert^* & : & \isarmeth \\[0.5ex]
   269   erule^* & : & \isarmeth \\
   270   drule^* & : & \isarmeth \\
   271   frule^* & : & \isarmeth \\[0.5ex]
   272   succeed & : & \isarmeth \\
   273   fail & : & \isarmeth \\
   274 \end{matharray}
   275 
   276 \begin{rail}
   277   ('fold' | 'unfold' | 'insert' | 'erule' | 'drule' | 'frule') thmrefs
   278   ;
   279 \end{rail}
   280 
   281 \begin{descr}
   282 \item [$unfold~\vec a$ and $fold~\vec a$] expand and fold back again the given
   283   meta-level definitions throughout all goals; any facts provided are inserted
   284   into the goal and subject to rewriting as well.
   285 \item [$erule~\vec a$, $drule~\vec a$, and $frule~\vec a$] are similar to the
   286   basic $rule$ method (see \S\ref{sec:pure-meth-att}), but apply rules by
   287   elim-resolution, destruct-resolution, and forward-resolution, respectively
   288   \cite{isabelle-ref}.  These are improper method, mainly for experimentation
   289   and emulating tactic scripts.
   290   
   291   Different modes of basic rule application are usually expressed in Isar at
   292   the proof language level, rather than via implicit proof state
   293   manipulations.  For example, a proper single-step elimination would be done
   294   using the basic $rule$ method, with forward chaining of current facts.
   295 \item [$insert~\vec a$] inserts theorems as facts into all goals of the proof
   296   state.  Note that current facts indicated for forward chaining are ignored.
   297 \item [$succeed$] yields a single (unchanged) result; it is the identity of
   298   the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
   299 \item [$fail$] yields an empty result sequence; it is the identity of the
   300   ``\texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
   301 \end{descr}
   302 
   303 
   304 \indexisaratt{standard}
   305 \indexisaratt{elimify}
   306 \indexisaratt{no-vars}
   307 
   308 \indexisaratt{RS}\indexisaratt{COMP}
   309 \indexisaratt{where}
   310 \indexisaratt{tag}\indexisaratt{untag}
   311 \indexisaratt{export}
   312 \indexisaratt{unfold}\indexisaratt{fold}
   313 \begin{matharray}{rcl}
   314   tag & : & \isaratt \\
   315   untag & : & \isaratt \\[0.5ex]
   316   RS & : & \isaratt \\
   317   COMP & : & \isaratt \\[0.5ex]
   318   where & : & \isaratt \\[0.5ex]
   319   unfold & : & \isaratt \\
   320   fold & : & \isaratt \\[0.5ex]
   321   standard & : & \isaratt \\
   322   elimify & : & \isaratt \\
   323   no_vars & : & \isaratt \\
   324   export^* & : & \isaratt \\
   325 \end{matharray}
   326 
   327 \begin{rail}
   328   'tag' (nameref+)
   329   ;
   330   'untag' name
   331   ;
   332   ('RS' | 'COMP') nat? thmref
   333   ;
   334   'where' (name '=' term * 'and')
   335   ;
   336   ('unfold' | 'fold') thmrefs
   337   ;
   338 \end{rail}
   339 
   340 \begin{descr}
   341 \item [$tag~name~args$ and $untag~name$] add and remove $tags$ of some
   342   theorem.  Tags may be any list of strings that serve as comment for some
   343   tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the
   344   result).  The first string is considered the tag name, the rest its
   345   arguments.  Note that untag removes any tags of the same name.
   346 \item [$RS~n~a$ and $COMP~n~a$] compose rules.  $RS$ resolves with the $n$-th
   347   premise of $a$; $COMP$ is a version of $RS$ that skips the automatic lifting
   348   process that is normally intended (cf.\ \texttt{RS} and \texttt{COMP} in
   349   \cite[\S5]{isabelle-ref}).
   350 \item [$where~\vec x = \vec t$] perform named instantiation of schematic
   351   variables occurring in a theorem.  Unlike instantiation tactics such as
   352   $rule_tac$ (see \S\ref{sec:tactic-commands}), actual schematic variables
   353   have to be specified (e.g.\ $\Var{x@3}$).
   354   
   355 \item [$unfold~\vec a$ and $fold~\vec a$] expand and fold back again the given
   356   meta-level definitions throughout a rule.
   357  
   358 \item [$standard$] puts a theorem into the standard form of object-rules, just
   359   as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).
   360   
   361 \item [$elimify$] turns an destruction rule into an elimination, just as the
   362   ML function \texttt{make\_elim} (see \cite{isabelle-ref}).
   363   
   364 \item [$no_vars$] replaces schematic variables by free ones; this is mainly
   365   for tuning output of pretty printed theorems.
   366   
   367 \item [$export$] lifts a local result out of the current proof context,
   368   generalizing all fixed variables and discharging all assumptions.  Note that
   369   proper incremental export is already done as part of the basic Isar
   370   machinery.  This attribute is mainly for experimentation.
   371   
   372 \end{descr}
   373 
   374 
   375 \section{Tactic emulations}\label{sec:tactics}
   376 
   377 The following improper proof methods emulate traditional tactics.  These admit
   378 direct access to the goal state, which is normally considered harmful!  In
   379 particular, this may involve both numbered goal addressing (default 1), and
   380 dynamic instantiation within the scope of some subgoal.
   381 
   382 \begin{warn}
   383   Dynamic instantiations are read and type-checked according to a subgoal of
   384   the current dynamic goal state, rather than the static proof context!  In
   385   particular, locally fixed variables and term abbreviations may not be
   386   included in the term specifications.  Thus schematic variables are left to
   387   be solved by unification with certain parts of the subgoal involved.
   388 \end{warn}
   389 
   390 Note that the tactic emulation proof methods in Isabelle/Isar are consistently
   391 named $foo_tac$.
   392 
   393 \indexisarmeth{rule-tac}\indexisarmeth{erule-tac}
   394 \indexisarmeth{drule-tac}\indexisarmeth{frule-tac}
   395 \indexisarmeth{cut-tac}\indexisarmeth{thin-tac}
   396 \indexisarmeth{subgoal-tac}\indexisarmeth{tactic}
   397 \begin{matharray}{rcl}
   398   rule_tac^* & : & \isarmeth \\
   399   erule_tac^* & : & \isarmeth \\
   400   drule_tac^* & : & \isarmeth \\
   401   frule_tac^* & : & \isarmeth \\
   402   cut_tac^* & : & \isarmeth \\
   403   thin_tac^* & : & \isarmeth \\
   404   subgoal_tac^* & : & \isarmeth \\
   405   tactic^* & : & \isarmeth \\
   406 \end{matharray}
   407 
   408 \railalias{ruletac}{rule\_tac}
   409 \railterm{ruletac}
   410 
   411 \railalias{eruletac}{erule\_tac}
   412 \railterm{eruletac}
   413 
   414 \railalias{druletac}{drule\_tac}
   415 \railterm{druletac}
   416 
   417 \railalias{fruletac}{frule\_tac}
   418 \railterm{fruletac}
   419 
   420 \railalias{cuttac}{cut\_tac}
   421 \railterm{cuttac}
   422 
   423 \railalias{thintac}{thin\_tac}
   424 \railterm{thintac}
   425 
   426 \railalias{subgoaltac}{subgoal\_tac}
   427 \railterm{subgoaltac}
   428 
   429 \begin{rail}
   430   ( ruletac | eruletac | druletac | fruletac | cuttac | thintac ) goalspec?
   431   ( insts thmref | thmrefs )
   432   ;
   433   subgoaltac goalspec? (prop +)
   434   ;
   435   'tactic' text
   436   ;
   437 
   438   insts: ((name '=' term) + 'and') 'in'
   439   ;
   440 \end{rail}
   441 
   442 \begin{descr}
   443 \item [$rule_tac$ etc.] do resolution of rules with explicit instantiation.
   444   This works the same way as the ML tactics \texttt{res_inst_tac} etc. (see
   445   \cite[\S3]{isabelle-ref}).
   446   
   447   Note that multiple rules may be only given there is no instantiation.  Then
   448   $rule_tac$ is the same as \texttt{resolve_tac} in ML (see
   449   \cite[\S3]{isabelle-ref}).
   450 \item [$cut_tac$] inserts facts into the proof state as assumption of a
   451   subgoal, see also \texttt{cut_facts_tac} in \cite[\S3]{isabelle-ref}.  Note
   452   that the scope of schmatic variables is spread over the main goal statement.
   453   Instantiations may be given as well, see also ML tactic
   454   \texttt{cut_inst_tac} in \cite[\S3]{isabelle-ref}.
   455 \item [$thin_tac~\phi$] deletes the specified assumption from a subgoal; note
   456   that $\phi$ may contain schematic variables.  See also \texttt{thin_tac} in
   457   \cite[\S3]{isabelle-ref}.
   458 \item [$subgoal_tac~\phi$] adds $\phi$ as an assumption to a subgoal.  See
   459   also \texttt{subgoal_tac} and \texttt{subgoals_tac} in
   460   \cite[\S3]{isabelle-ref}.
   461 \item [$tactic~text$] produces a proof method from any ML text of type
   462   \texttt{tactic}.  Apart from the usual ML environment and the current
   463   implicit theory context, the ML code may refer to the following locally
   464   bound values:
   465 
   466 %%FIXME ttbox produces too much trailing space (why?)
   467 {\footnotesize\begin{verbatim}
   468 val ctxt  : Proof.context
   469 val facts : thm list
   470 val thm   : string -> thm
   471 val thms  : string -> thm list
   472 \end{verbatim}}
   473   Here \texttt{ctxt} refers to the current proof context, \texttt{facts}
   474   indicates any current facts for forward-chaining, and
   475   \texttt{thm}~/~\texttt{thms} retrieve named facts (including global
   476   theorems) from the context.
   477 \end{descr}
   478 
   479 
   480 \section{The Simplifier}
   481 
   482 \subsection{Simplification methods}\label{sec:simp}
   483 
   484 \indexisarmeth{simp}\indexisarmeth{simp-all}
   485 \begin{matharray}{rcl}
   486   simp & : & \isarmeth \\
   487   simp_all & : & \isarmeth \\
   488 \end{matharray}
   489 
   490 \railalias{simpall}{simp\_all}
   491 \railterm{simpall}
   492 
   493 \railalias{noasm}{no\_asm}
   494 \railterm{noasm}
   495 
   496 \railalias{noasmsimp}{no\_asm\_simp}
   497 \railterm{noasmsimp}
   498 
   499 \railalias{noasmuse}{no\_asm\_use}
   500 \railterm{noasmuse}
   501 
   502 \begin{rail}
   503   ('simp' | simpall) ('!' ?) opt? (simpmod * )
   504   ;
   505 
   506   opt: '(' (noasm | noasmsimp | noasmuse) ')'
   507   ;
   508   simpmod: ('add' | 'del' | 'only' | 'split' (() | 'add' | 'del') | 'other') ':' thmrefs
   509   ;
   510 \end{rail}
   511 
   512 \begin{descr}
   513 \item [$simp$] invokes Isabelle's simplifier, after declaring additional rules
   514   according to the arguments given.  Note that the \railtterm{only} modifier
   515   first removes all other rewrite rules, congruences, and looper tactics
   516   (including splits), and then behaves like \railtterm{add}.
   517   
   518   The \railtterm{split} modifiers add or delete rules for the Splitter (see
   519   also \cite{isabelle-ref}), the default is to add.  This works only if the
   520   Simplifier method has been properly setup to include the Splitter (all major
   521   object logics such HOL, HOLCF, FOL, ZF do this already).
   522   
   523   The \railtterm{other} modifier ignores its arguments.  Nevertheless,
   524   additional kinds of rules may be declared by including appropriate
   525   attributes in the specification.
   526 \item [$simp_all$] is similar to $simp$, but acts on all goals.
   527 \end{descr}
   528 
   529 By default, the Simplifier methods are based on \texttt{asm_full_simp_tac}
   530 internally \cite[\S10]{isabelle-ref}, which means that assumptions are both
   531 simplified as well as used in simplifying the conclusion.  In structured
   532 proofs this is usually quite well behaved in practice: just the local premises
   533 of the actual goal are involved, additional facts may inserted via explicit
   534 forward-chaining (using $\THEN$, $\FROMNAME$ etc.).  The full context of
   535 assumptions is only included if the ``$!$'' (bang) argument is given, which
   536 should be used with some care, though.
   537 
   538 Additional Simplifier options may be specified to tune the behavior even
   539 further: $(no_asm)$ means assumptions are ignored completely (cf.\ 
   540 \texttt{simp_tac}), $(no_asm_simp)$ means assumptions are used in the
   541 simplification of the conclusion but are not themselves simplified (cf.\ 
   542 \texttt{asm_simp_tac}), and $(no_asm_use)$ means assumptions are simplified
   543 but are not used in the simplification of each other or the conclusion (cf.
   544 \texttt{full_simp_tac}).
   545 
   546 \medskip
   547 
   548 The Splitter package is usually configured to work as part of the Simplifier.
   549 There is no separate $split$ method available.  The effect of repeatedly
   550 applying \texttt{split_tac} can be simulated by
   551 $(simp~only\colon~split\colon~\vec a)$.
   552 
   553 
   554 \subsection{Declaring rules}
   555 
   556 \indexisarcmd{print-simpset}
   557 \indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong}
   558 \begin{matharray}{rcl}
   559   print_simpset & : & \isarkeep{theory~|~proof} \\
   560   simp & : & \isaratt \\
   561   split & : & \isaratt \\
   562   cong & : & \isaratt \\
   563 \end{matharray}
   564 
   565 \begin{rail}
   566   ('simp' | 'split' | 'cong') (() | 'add' | 'del')
   567   ;
   568 \end{rail}
   569 
   570 \begin{descr}
   571 \item [$print_simpset$] prints the collection of rules declared to the
   572   Simplifier, which is also known as ``simpset'' internally
   573   \cite{isabelle-ref}.  This is a diagnostic command; $undo$ does not apply.
   574 \item [$simp$] declares simplification rules.
   575 \item [$split$] declares split rules.
   576 \item [$cong$] declares congruence rules.
   577 \end{descr}
   578 
   579 
   580 \subsection{Forward simplification}
   581 
   582 \indexisaratt{simplify}\indexisaratt{asm-simplify}
   583 \indexisaratt{full-simplify}\indexisaratt{asm-full-simplify}
   584 \begin{matharray}{rcl}
   585   simplify & : & \isaratt \\
   586   asm_simplify & : & \isaratt \\
   587   full_simplify & : & \isaratt \\
   588   asm_full_simplify & : & \isaratt \\
   589 \end{matharray}
   590 
   591 These attributes provide forward rules for simplification, which should be
   592 used only very rarely.  There are no separate options for declaring
   593 simplification rules locally.
   594 
   595 See the ML functions of the same name in \cite[\S10]{isabelle-ref} for more
   596 information.
   597 
   598 
   599 \section{The Classical Reasoner}
   600 
   601 \subsection{Basic methods}\label{sec:classical-basic}
   602 
   603 \indexisarmeth{rule}\indexisarmeth{intro}
   604 \indexisarmeth{elim}\indexisarmeth{default}\indexisarmeth{contradiction}
   605 \begin{matharray}{rcl}
   606   rule & : & \isarmeth \\
   607   intro & : & \isarmeth \\
   608   elim & : & \isarmeth \\
   609   contradiction & : & \isarmeth \\
   610 \end{matharray}
   611 
   612 \begin{rail}
   613   ('rule' | 'intro' | 'elim') thmrefs?
   614   ;
   615 \end{rail}
   616 
   617 \begin{descr}
   618 \item [$rule$] as offered by the classical reasoner is a refinement over the
   619   primitive one (see \S\ref{sec:pure-meth-att}).  In case that no rules are
   620   provided as arguments, it automatically determines elimination and
   621   introduction rules from the context (see also \S\ref{sec:classical-mod}).
   622   This is made the default method for basic proof steps, such as $\PROOFNAME$
   623   and ``$\DDOT$'' (two dots), see also \S\ref{sec:proof-steps} and
   624   \S\ref{sec:pure-meth-att}.
   625   
   626 \item [$intro$ and $elim$] repeatedly refine some goal by intro- or
   627   elim-resolution, after having inserted any facts.  Omitting the arguments
   628   refers to any suitable rules declared in the context, otherwise only the
   629   explicitly given ones may be applied.  The latter form admits better control
   630   of what actually happens, thus it is very appropriate as an initial method
   631   for $\PROOFNAME$ that splits up certain connectives of the goal, before
   632   entering the actual sub-proof.
   633   
   634 \item [$contradiction$] solves some goal by contradiction, deriving any result
   635   from both $\neg A$ and $A$.  Facts, which are guaranteed to participate, may
   636   appear in either order.
   637 \end{descr}
   638 
   639 
   640 \subsection{Automated methods}\label{sec:classical-auto}
   641 
   642 \indexisarmeth{blast}\indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{clarify}
   643 \begin{matharray}{rcl}
   644  blast & : & \isarmeth \\
   645  fast & : & \isarmeth \\
   646  best & : & \isarmeth \\
   647  clarify & : & \isarmeth \\
   648 \end{matharray}
   649 
   650 \begin{rail}
   651   'blast' ('!' ?) nat? (clamod * )
   652   ;
   653   ('fast' | 'best' | 'clarify') ('!' ?) (clamod * )
   654   ;
   655 
   656   clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs
   657   ;
   658 \end{rail}
   659 
   660 \begin{descr}
   661 \item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac}
   662   in \cite[\S11]{isabelle-ref}).  The optional argument specifies a
   663   user-supplied search bound (default 20).  Note that $blast$ is the only
   664   classical proof procedure in Isabelle that can handle actual object-logic
   665   rules as local assumptions ($fast$ etc.\ would just ignore non-atomic
   666   facts).
   667 \item [$fast$, $best$, and $clarify$] refer to the generic classical reasoner.
   668   See \texttt{fast_tac}, \texttt{best_tac}, and \texttt{clarify_tac} in
   669   \cite[\S11]{isabelle-ref} for more information.
   670 \end{descr}
   671 
   672 Any of above methods support additional modifiers of the context of classical
   673 rules.  Their semantics is analogous to the attributes given in
   674 \S\ref{sec:classical-mod}.  Facts provided by forward chaining are
   675 inserted\footnote{These methods usually cannot make proper use of actual rules
   676   inserted that way, though.} into the goal before doing the search.  The
   677 ``!''~argument causes the full context of assumptions to be included as well.
   678 This is slightly less hazardous than for the Simplifier (see
   679 \S\ref{sec:simp}).
   680 
   681 
   682 \subsection{Combined automated methods}
   683 
   684 \indexisarmeth{auto}\indexisarmeth{force}
   685 \indexisarmeth{clarsimp}\indexisarmeth{fastsimp}
   686 \begin{matharray}{rcl}
   687   auto & : & \isarmeth \\
   688   force & : & \isarmeth \\
   689   clarsimp & : & \isarmeth \\
   690   fastsimp & : & \isarmeth \\
   691 \end{matharray}
   692 
   693 \begin{rail}
   694   ('auto' | 'force' | 'clarsimp' | 'fastsimp') ('!' ?) (clasimpmod * )
   695   ;
   696 
   697   clasimpmod: ('simp' (() | 'add' | 'del' | 'only') | 'other' |
   698     ('split' (() | 'add' | 'del')) |
   699     (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' thmrefs
   700 \end{rail}
   701 
   702 \begin{descr}
   703 \item [$auto$, $force$, $clarsimp$, $fastsimp$] provide access to Isabelle's
   704   combined simplification and classical reasoning tactics.  These correspond
   705   to \texttt{auto_tac}, \texttt{force_tac}, \texttt{clarsimp_tac}, and
   706   \texttt{fast_tac} (with the Simplifier added as wrapper), see
   707   \cite[\S11]{isabelle-ref} for more information.  The modifier arguments
   708   correspond to those given in \S\ref{sec:simp} and
   709   \S\ref{sec:classical-auto}.  Just note that the ones related to the
   710   Simplifier are prefixed by \railtterm{simp} here.
   711   
   712   Facts provided by forward chaining are inserted into the goal before doing
   713   the search.  The ``!''~argument causes the full context of assumptions to be
   714   included as well.
   715 \end{descr}
   716 
   717 
   718 \subsection{Declaring rules}\label{sec:classical-mod}
   719 
   720 \indexisarcmd{print-claset}
   721 \indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
   722 \indexisaratt{iff}\indexisaratt{delrule}
   723 \begin{matharray}{rcl}
   724   print_claset & : & \isarkeep{theory~|~proof} \\
   725   intro & : & \isaratt \\
   726   elim & : & \isaratt \\
   727   dest & : & \isaratt \\
   728   iff & : & \isaratt \\
   729   delrule & : & \isaratt \\
   730 \end{matharray}
   731 
   732 \begin{rail}
   733   ('intro' | 'elim' | 'dest') ('!' | () | '?')
   734   ;
   735   'iff' (() | 'add' | 'del')
   736 \end{rail}
   737 
   738 \begin{descr}
   739 \item [$print_claset$] prints the collection of rules declared to the
   740   Classical Reasoner, which is also known as ``simpset'' internally
   741   \cite{isabelle-ref}.  This is a diagnostic command; $undo$ does not apply.
   742 \item [$intro$, $elim$, and $dest$] declare introduction, elimination, and
   743   destruct rules, respectively.  By default, rules are considered as
   744   \emph{unsafe} (i.e.\ not applied blindly without backtracking), while a
   745   single ``!'' classifies as \emph{safe}, and ``?'' as \emph{extra} (i.e.\ not
   746   applied in the search-oriented automated methods, but only in single-step
   747   methods such as $rule$).
   748   
   749 \item [$iff$] declares equations both as rules for the Simplifier and
   750   Classical Reasoner.
   751 
   752 \item [$delrule$] deletes introduction or elimination rules from the context.
   753   Note that destruction rules would have to be turned into elimination rules
   754   first, e.g.\ by using the $elimify$ attribute.
   755 \end{descr}
   756 
   757 
   758 %%% Local Variables: 
   759 %%% mode: latex
   760 %%% TeX-master: "isar-ref"
   761 %%% End: