doc-src/IsarRef/generic.tex
author wenzelm
Tue Sep 12 22:13:23 2000 +0200 (2000-09-12)
changeset 9941 fe05af7ec816
parent 9936 f080397656d8
child 10031 12fd0fcf755a
permissions -rw-r--r--
renamed atts: rulify to rule_format, elimify to elim_format;
     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 
   208   Note that the default usage of case rules does \emph{not} directly expose
   209   parameters to the proof context (see also \S\ref{sec:induct-method-proper}).
   210 \end{descr}
   211 
   212 
   213 \section{Generalized existence}\label{sec:obtain}
   214 
   215 \indexisarcmd{obtain}
   216 \begin{matharray}{rcl}
   217   \isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\
   218 \end{matharray}
   219 
   220 Generalized existence means that additional elements with certain properties
   221 may introduced in the current context.  Technically, the $\OBTAINNAME$
   222 language element is like a declaration of $\FIXNAME$ and $\ASSUMENAME$ (see
   223 also see \S\ref{sec:proof-context}), together with a soundness proof of its
   224 additional claim.  According to the nature of existential reasoning,
   225 assumptions get eliminated from any result exported from the context later,
   226 provided that the corresponding parameters do \emph{not} occur in the
   227 conclusion.
   228 
   229 \begin{rail}
   230   'obtain' (vars + 'and') comment? \\ 'where' (assm comment? + 'and')
   231   ;
   232 \end{rail}
   233 
   234 $\OBTAINNAME$ is defined as a derived Isar command as follows, where $\vec b$
   235 shall refer to (optional) facts indicated for forward chaining.
   236 \begin{matharray}{l}
   237   \langle facts~\vec b\rangle \\
   238   \OBTAIN{\vec x}{a}{\vec \phi}~~\langle proof\rangle \equiv {} \\[1ex]
   239   \quad \BG \\
   240   \qquad \FIX{thesis} \\
   241   \qquad \ASSUME{that [simp, intro]}{\All{\vec x} \vec\phi \Imp thesis} \\
   242   \qquad \FROM{\vec b}~\HAVE{}{thesis}~~\langle proof\rangle \\
   243   \quad \EN \\
   244   \quad \FIX{\vec x}~\ASSUMENAME^{\ast}~{a}~{\vec\phi} \\
   245 \end{matharray}
   246 
   247 Typically, the soundness proof is relatively straight-forward, often just by
   248 canonical automated tools such as $\BY{simp}$ (see \S\ref{sec:simp}) or
   249 $\BY{blast}$ (see \S\ref{sec:classical-auto}).  Accordingly, the ``$that$''
   250 reduction above is declared as simplification and introduction rule.
   251 
   252 \medskip
   253 
   254 In a sense, $\OBTAINNAME$ represents at the level of Isar proofs what would be
   255 meta-logical existential quantifiers and conjunctions.  This concept has a
   256 broad range of useful applications, ranging from plain elimination (or even
   257 introduction) of object-level existentials and conjunctions, to elimination
   258 over results of symbolic evaluation of recursive definitions, for example.
   259 Also note that $\OBTAINNAME$ without parameters acts much like $\HAVENAME$,
   260 where the result is treated as an assumption.
   261 
   262 
   263 \section{Miscellaneous methods and attributes}
   264 
   265 \indexisarmeth{unfold}\indexisarmeth{fold}\indexisarmeth{insert}
   266 \indexisarmeth{erule}\indexisarmeth{drule}\indexisarmeth{frule}
   267 \indexisarmeth{fail}\indexisarmeth{succeed}
   268 \begin{matharray}{rcl}
   269   unfold & : & \isarmeth \\
   270   fold & : & \isarmeth \\[0.5ex]
   271   insert^* & : & \isarmeth \\[0.5ex]
   272   erule^* & : & \isarmeth \\
   273   drule^* & : & \isarmeth \\
   274   frule^* & : & \isarmeth \\[0.5ex]
   275   succeed & : & \isarmeth \\
   276   fail & : & \isarmeth \\
   277 \end{matharray}
   278 
   279 \begin{rail}
   280   ('fold' | 'unfold' | 'insert' | 'erule' | 'drule' | 'frule') thmrefs
   281   ;
   282 \end{rail}
   283 
   284 \begin{descr}
   285 \item [$unfold~\vec a$ and $fold~\vec a$] expand and fold back again the given
   286   meta-level definitions throughout all goals; any facts provided are inserted
   287   into the goal and subject to rewriting as well.
   288 \item [$erule~\vec a$, $drule~\vec a$, and $frule~\vec a$] are similar to the
   289   basic $rule$ method (see \S\ref{sec:pure-meth-att}), but apply rules by
   290   elim-resolution, destruct-resolution, and forward-resolution, respectively
   291   \cite{isabelle-ref}.  These are improper method, mainly for experimentation
   292   and emulating tactic scripts.
   293 
   294   Different modes of basic rule application are usually expressed in Isar at
   295   the proof language level, rather than via implicit proof state
   296   manipulations.  For example, a proper single-step elimination would be done
   297   using the basic $rule$ method, with forward chaining of current facts.
   298 \item [$insert~\vec a$] inserts theorems as facts into all goals of the proof
   299   state.  Note that current facts indicated for forward chaining are ignored.
   300 \item [$succeed$] yields a single (unchanged) result; it is the identity of
   301   the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
   302 \item [$fail$] yields an empty result sequence; it is the identity of the
   303   ``\texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
   304 \end{descr}
   305 
   306 
   307 \indexisaratt{standard}
   308 \indexisaratt{elim-format}
   309 \indexisaratt{no-vars}
   310 
   311 \indexisaratt{THEN}\indexisaratt{COMP}
   312 \indexisaratt{where}\indexisaratt{tagged}\indexisaratt{untagged}
   313 \indexisaratt{unfolded}\indexisaratt{folded}\indexisaratt{exported}
   314 \begin{matharray}{rcl}
   315   tagged & : & \isaratt \\
   316   untagged & : & \isaratt \\[0.5ex]
   317   THEN & : & \isaratt \\
   318   COMP & : & \isaratt \\[0.5ex]
   319   where & : & \isaratt \\[0.5ex]
   320   unfolded & : & \isaratt \\
   321   folded & : & \isaratt \\[0.5ex]
   322   standard & : & \isaratt \\
   323   elim_format & : & \isaratt \\
   324   no_vars^* & : & \isaratt \\
   325   exported^* & : & \isaratt \\
   326 \end{matharray}
   327 
   328 \begin{rail}
   329   'tagged' (nameref+)
   330   ;
   331   'untagged' name
   332   ;
   333   ('THEN' | 'COMP') nat? thmref
   334   ;
   335   'where' (name '=' term * 'and')
   336   ;
   337   ('unfolded' | 'folded') thmrefs
   338   ;
   339 \end{rail}
   340 
   341 \begin{descr}
   342 \item [$tagged~name~args$ and $untagged~name$] add and remove $tags$ of some
   343   theorem.  Tags may be any list of strings that serve as comment for some
   344   tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the
   345   result).  The first string is considered the tag name, the rest its
   346   arguments.  Note that untag removes any tags of the same name.
   347 \item [$THEN~n~a$ and $COMP~n~a$] compose rules.  $THEN$ resolves with the
   348   $n$-th premise of $a$; the $COMP$ version skips the automatic lifting
   349   process that is normally intended (cf.\ \texttt{RS} and \texttt{COMP} in
   350   \cite[\S5]{isabelle-ref}).
   351 \item [$where~\vec x = \vec t$] perform named instantiation of schematic
   352   variables occurring in a theorem.  Unlike instantiation tactics such as
   353   $rule_tac$ (see \S\ref{sec:tactic-commands}), actual schematic variables
   354   have to be specified (e.g.\ $\Var{x@3}$).
   355 \item [$unfolded~\vec a$ and $folded~\vec a$] expand and fold back again the
   356   given meta-level definitions throughout a rule.
   357 \item [$standard$] puts a theorem into the standard form of object-rules, just
   358   as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).
   359 \item [$elim_format$] turns a destruction rule into elimination rule format;
   360   see also the ML function \texttt{make\_elim} (see \cite{isabelle-ref}).
   361 \item [$no_vars$] replaces schematic variables by free ones; this is mainly
   362   for tuning output of pretty printed theorems.
   363 \item [$exported$] lifts a local result out of the current proof context,
   364   generalizing all fixed variables and discharging all assumptions.  Note that
   365   proper incremental export is already done as part of the basic Isar
   366   machinery.  This attribute is mainly for experimentation.
   367 \end{descr}
   368 
   369 
   370 \section{Tactic emulations}\label{sec:tactics}
   371 
   372 The following improper proof methods emulate traditional tactics.  These admit
   373 direct access to the goal state, which is normally considered harmful!  In
   374 particular, this may involve both numbered goal addressing (default 1), and
   375 dynamic instantiation within the scope of some subgoal.
   376 
   377 \begin{warn}
   378   Dynamic instantiations are read and type-checked according to a subgoal of
   379   the current dynamic goal state, rather than the static proof context!  In
   380   particular, locally fixed variables and term abbreviations may not be
   381   included in the term specifications.  Thus schematic variables are left to
   382   be solved by unification with certain parts of the subgoal involved.
   383 \end{warn}
   384 
   385 Note that the tactic emulation proof methods in Isabelle/Isar are consistently
   386 named $foo_tac$.
   387 
   388 \indexisarmeth{rule-tac}\indexisarmeth{erule-tac}
   389 \indexisarmeth{drule-tac}\indexisarmeth{frule-tac}
   390 \indexisarmeth{cut-tac}\indexisarmeth{thin-tac}
   391 \indexisarmeth{subgoal-tac}\indexisarmeth{rename-tac}
   392 \indexisarmeth{rotate-tac}\indexisarmeth{tactic}
   393 \begin{matharray}{rcl}
   394   rule_tac^* & : & \isarmeth \\
   395   erule_tac^* & : & \isarmeth \\
   396   drule_tac^* & : & \isarmeth \\
   397   frule_tac^* & : & \isarmeth \\
   398   cut_tac^* & : & \isarmeth \\
   399   thin_tac^* & : & \isarmeth \\
   400   subgoal_tac^* & : & \isarmeth \\
   401   rename_tac^* & : & \isarmeth \\
   402   rotate_tac^* & : & \isarmeth \\
   403   tactic^* & : & \isarmeth \\
   404 \end{matharray}
   405 
   406 \railalias{ruletac}{rule\_tac}
   407 \railterm{ruletac}
   408 
   409 \railalias{eruletac}{erule\_tac}
   410 \railterm{eruletac}
   411 
   412 \railalias{druletac}{drule\_tac}
   413 \railterm{druletac}
   414 
   415 \railalias{fruletac}{frule\_tac}
   416 \railterm{fruletac}
   417 
   418 \railalias{cuttac}{cut\_tac}
   419 \railterm{cuttac}
   420 
   421 \railalias{thintac}{thin\_tac}
   422 \railterm{thintac}
   423 
   424 \railalias{subgoaltac}{subgoal\_tac}
   425 \railterm{subgoaltac}
   426 
   427 \railalias{renametac}{rename\_tac}
   428 \railterm{renametac}
   429 
   430 \railalias{rotatetac}{rotate\_tac}
   431 \railterm{rotatetac}
   432 
   433 \begin{rail}
   434   ( ruletac | eruletac | druletac | fruletac | cuttac | thintac ) goalspec?
   435   ( insts thmref | thmrefs )
   436   ;
   437   subgoaltac goalspec? (prop +)
   438   ;
   439   renametac goalspec? (name +)
   440   ;
   441   rotatetac goalspec? int?
   442   ;
   443   'tactic' text
   444   ;
   445 
   446   insts: ((name '=' term) + 'and') 'in'
   447   ;
   448 \end{rail}
   449 
   450 \begin{descr}
   451 \item [$rule_tac$ etc.] do resolution of rules with explicit instantiation.
   452   This works the same way as the ML tactics \texttt{res_inst_tac} etc. (see
   453   \cite[\S3]{isabelle-ref}).
   454 
   455   Note that multiple rules may be only given there is no instantiation.  Then
   456   $rule_tac$ is the same as \texttt{resolve_tac} in ML (see
   457   \cite[\S3]{isabelle-ref}).
   458 \item [$cut_tac$] inserts facts into the proof state as assumption of a
   459   subgoal, see also \texttt{cut_facts_tac} in \cite[\S3]{isabelle-ref}.  Note
   460   that the scope of schmatic variables is spread over the main goal statement.
   461   Instantiations may be given as well, see also ML tactic
   462   \texttt{cut_inst_tac} in \cite[\S3]{isabelle-ref}.
   463 \item [$thin_tac~\phi$] deletes the specified assumption from a subgoal; note
   464   that $\phi$ may contain schematic variables.  See also \texttt{thin_tac} in
   465   \cite[\S3]{isabelle-ref}.
   466 \item [$subgoal_tac~\phi$] adds $\phi$ as an assumption to a subgoal.  See
   467   also \texttt{subgoal_tac} and \texttt{subgoals_tac} in
   468   \cite[\S3]{isabelle-ref}.
   469 \item [$rename_tac~\vec x$] renames parameters of a goal according to the list
   470   $\vec x$, which refers to the \emph{suffix} of variables.
   471 \item [$rotate_tac~n$] rotates the assumptions of a goal by $n$ positions:
   472   from right to left if $n$ is positive, and from left to right if $n$ is
   473   negative; the default value is $1$.  See also \texttt{rotate_tac} in
   474   \cite[\S3]{isabelle-ref}.
   475 \item [$tactic~text$] produces a proof method from any ML text of type
   476   \texttt{tactic}.  Apart from the usual ML environment and the current
   477   implicit theory context, the ML code may refer to the following locally
   478   bound values:
   479 
   480 %%FIXME ttbox produces too much trailing space (why?)
   481 {\footnotesize\begin{verbatim}
   482 val ctxt  : Proof.context
   483 val facts : thm list
   484 val thm   : string -> thm
   485 val thms  : string -> thm list
   486 \end{verbatim}}
   487   Here \texttt{ctxt} refers to the current proof context, \texttt{facts}
   488   indicates any current facts for forward-chaining, and
   489   \texttt{thm}~/~\texttt{thms} retrieve named facts (including global
   490   theorems) from the context.
   491 \end{descr}
   492 
   493 
   494 \section{The Simplifier}\label{sec:simplifier}
   495 
   496 \subsection{Simplification methods}\label{sec:simp}
   497 
   498 \indexisarmeth{simp}\indexisarmeth{simp-all}
   499 \begin{matharray}{rcl}
   500   simp & : & \isarmeth \\
   501   simp_all & : & \isarmeth \\
   502 \end{matharray}
   503 
   504 \railalias{simpall}{simp\_all}
   505 \railterm{simpall}
   506 
   507 \railalias{noasm}{no\_asm}
   508 \railterm{noasm}
   509 
   510 \railalias{noasmsimp}{no\_asm\_simp}
   511 \railterm{noasmsimp}
   512 
   513 \railalias{noasmuse}{no\_asm\_use}
   514 \railterm{noasmuse}
   515 
   516 \begin{rail}
   517   ('simp' | simpall) ('!' ?) opt? (simpmod * )
   518   ;
   519 
   520   opt: '(' (noasm | noasmsimp | noasmuse) ')'
   521   ;
   522   simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
   523     'split' (() | 'add' | 'del')) ':' thmrefs
   524   ;
   525 \end{rail}
   526 
   527 \begin{descr}
   528 \item [$simp$] invokes Isabelle's simplifier, after declaring additional rules
   529   according to the arguments given.  Note that the \railtterm{only} modifier
   530   first removes all other rewrite rules, congruences, and looper tactics
   531   (including splits), and then behaves like \railtterm{add}.
   532   
   533   \medskip The \railtterm{cong} modifiers add or delete Simplifier congruence
   534   rules (see also \cite{isabelle-ref}), the default is to add.
   535   
   536   \medskip The \railtterm{split} modifiers add or delete rules for the
   537   Splitter (see also \cite{isabelle-ref}), the default is to add.  This works
   538   only if the Simplifier method has been properly setup to include the
   539   Splitter (all major object logics such HOL, HOLCF, FOL, ZF do this already).
   540 \item [$simp_all$] is similar to $simp$, but acts on all goals.
   541 \end{descr}
   542 
   543 By default, the Simplifier methods are based on \texttt{asm_full_simp_tac}
   544 internally \cite[\S10]{isabelle-ref}, which means that assumptions are both
   545 simplified as well as used in simplifying the conclusion.  In structured
   546 proofs this is usually quite well behaved in practice: just the local premises
   547 of the actual goal are involved, additional facts may inserted via explicit
   548 forward-chaining (using $\THEN$, $\FROMNAME$ etc.).  The full context of
   549 assumptions is only included if the ``$!$'' (bang) argument is given, which
   550 should be used with some care, though.
   551 
   552 Additional Simplifier options may be specified to tune the behavior even
   553 further: $(no_asm)$ means assumptions are ignored completely (cf.\
   554 \texttt{simp_tac}), $(no_asm_simp)$ means assumptions are used in the
   555 simplification of the conclusion but are not themselves simplified (cf.\
   556 \texttt{asm_simp_tac}), and $(no_asm_use)$ means assumptions are simplified
   557 but are not used in the simplification of each other or the conclusion (cf.
   558 \texttt{full_simp_tac}).
   559 
   560 \medskip
   561 
   562 The Splitter package is usually configured to work as part of the Simplifier.
   563 The effect of repeatedly applying \texttt{split_tac} can be simulated by
   564 $(simp~only\colon~split\colon~\vec a)$.  There is also a separate $split$
   565 method available for single-step case splitting, see \S\ref{sec:basic-eq}.
   566 
   567 
   568 \subsection{Declaring rules}
   569 
   570 \indexisarcmd{print-simpset}
   571 \indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong}
   572 \begin{matharray}{rcl}
   573   print_simpset & : & \isarkeep{theory~|~proof} \\
   574   simp & : & \isaratt \\
   575   cong & : & \isaratt \\
   576   split & : & \isaratt \\
   577 \end{matharray}
   578 
   579 \begin{rail}
   580   ('simp' | 'cong' | 'split') (() | 'add' | 'del')
   581   ;
   582 \end{rail}
   583 
   584 \begin{descr}
   585 \item [$print_simpset$] prints the collection of rules declared to the
   586   Simplifier, which is also known as ``simpset'' internally
   587   \cite{isabelle-ref}.  This is a diagnostic command; $undo$ does not apply.
   588 \item [$simp$] declares simplification rules.
   589 \item [$cong$] declares congruence rules.
   590 \item [$split$] declares case split rules.
   591 \end{descr}
   592 
   593 
   594 \subsection{Forward simplification}
   595 
   596 \indexisaratt{simplified}
   597 \begin{matharray}{rcl}
   598   simplified & : & \isaratt \\
   599 \end{matharray}
   600 
   601 \begin{rail}
   602   'simplified' opt?
   603   ;
   604 
   605   opt: '(' (noasm | noasmsimp | noasmuse) ')'
   606   ;
   607 \end{rail}
   608 
   609 \begin{descr}
   610 \item [$simplified$] causes a theorem to be simplified according to the
   611   current Simplifier context (there are no separate arguments for declaring
   612   additional rules).  By default the result is fully simplified, including
   613   assumptions and conclusion.  The options $no_asm$ etc.\ restrict the
   614   Simplifier in the same way as the for the $simp$ method (see
   615   \S\ref{sec:simp}).
   616   
   617   The $simplified$ operation should be used only very rarely, usually for
   618   experimentation only.
   619 \end{descr}
   620 
   621 
   622 \section{Basic equational reasoning}\label{sec:basic-eq}
   623 
   624 \indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisarmeth{split}\indexisaratt{symmetric}
   625 \begin{matharray}{rcl}
   626   subst & : & \isarmeth \\
   627   hypsubst^* & : & \isarmeth \\
   628   split & : & \isarmeth \\
   629   symmetric & : & \isaratt \\
   630 \end{matharray}
   631 
   632 \begin{rail}
   633   'subst' thmref
   634   ;
   635   'split' ('(' 'asm' ')')? thmrefs
   636   ;
   637 \end{rail}
   638 
   639 These methods and attributes provide basic facilities for equational reasoning
   640 that are intended for specialized applications only.  Normally, single step
   641 reasoning would be performed by calculation (see \S\ref{sec:calculation}),
   642 while the Simplifier is the canonical tool for automated normalization (see
   643 \S\ref{sec:simplifier}).
   644 
   645 \begin{descr}
   646 \item [$subst~thm$] performs a single substitution step using rule $thm$,
   647   which may be either a meta or object equality.
   648 \item [$hypsubst$] performs substitution using some assumption.
   649 \item [$split~thms$] performs single-step case splitting using rules $thms$.
   650   By default, splitting is performed in the conclusion of a goal; the $asm$
   651   option indicates to operate on assumptions instead.
   652   
   653   Note that the $simp$ method already involves repeated application of split
   654   rules as declared in the current context (see \S\ref{sec:simp}).
   655 \item [$symmetric$] applies the symmetry rule of meta or object equality.
   656 \end{descr}
   657 
   658 
   659 \section{The Classical Reasoner}\label{sec:classical}
   660 
   661 \subsection{Basic methods}\label{sec:classical-basic}
   662 
   663 \indexisarmeth{rule}\indexisarmeth{intro}
   664 \indexisarmeth{elim}\indexisarmeth{default}\indexisarmeth{contradiction}
   665 \begin{matharray}{rcl}
   666   rule & : & \isarmeth \\
   667   intro & : & \isarmeth \\
   668   elim & : & \isarmeth \\
   669   contradiction & : & \isarmeth \\
   670 \end{matharray}
   671 
   672 \begin{rail}
   673   ('rule' | 'intro' | 'elim') thmrefs?
   674   ;
   675 \end{rail}
   676 
   677 \begin{descr}
   678 \item [$rule$] as offered by the classical reasoner is a refinement over the
   679   primitive one (see \S\ref{sec:pure-meth-att}).  In case that no rules are
   680   provided as arguments, it automatically determines elimination and
   681   introduction rules from the context (see also \S\ref{sec:classical-mod}).
   682   This is made the default method for basic proof steps, such as $\PROOFNAME$
   683   and ``$\DDOT$'' (two dots), see also \S\ref{sec:proof-steps} and
   684   \S\ref{sec:pure-meth-att}.
   685 
   686 \item [$intro$ and $elim$] repeatedly refine some goal by intro- or
   687   elim-resolution, after having inserted any facts.  Omitting the arguments
   688   refers to any suitable rules declared in the context, otherwise only the
   689   explicitly given ones may be applied.  The latter form admits better control
   690   of what actually happens, thus it is very appropriate as an initial method
   691   for $\PROOFNAME$ that splits up certain connectives of the goal, before
   692   entering the actual sub-proof.
   693 
   694 \item [$contradiction$] solves some goal by contradiction, deriving any result
   695   from both $\neg A$ and $A$.  Facts, which are guaranteed to participate, may
   696   appear in either order.
   697 \end{descr}
   698 
   699 
   700 \subsection{Automated methods}\label{sec:classical-auto}
   701 
   702 \indexisarmeth{blast}\indexisarmeth{fast}\indexisarmeth{slow}
   703 \indexisarmeth{best}\indexisarmeth{safe}\indexisarmeth{clarify}
   704 \begin{matharray}{rcl}
   705   blast & : & \isarmeth \\
   706   fast & : & \isarmeth \\
   707   slow & : & \isarmeth \\
   708   best & : & \isarmeth \\
   709   safe & : & \isarmeth \\
   710   clarify & : & \isarmeth \\
   711 \end{matharray}
   712 
   713 \begin{rail}
   714   'blast' ('!' ?) nat? (clamod * )
   715   ;
   716   ('fast' | 'slow' | 'best' | 'safe' | 'clarify') ('!' ?) (clamod * )
   717   ;
   718 
   719   clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs
   720   ;
   721 \end{rail}
   722 
   723 \begin{descr}
   724 \item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac}
   725   in \cite[\S11]{isabelle-ref}).  The optional argument specifies a
   726   user-supplied search bound (default 20).  Note that $blast$ is the only
   727   classical proof procedure in Isabelle that can handle actual object-logic
   728   rules as local assumptions ($fast$ etc.\ would just ignore non-atomic
   729   facts).
   730 \item [$fast$, $slow$, $best$, $safe$, and $clarify$] refer to the generic
   731   classical reasoner.  See \texttt{fast_tac}, \texttt{slow_tac},
   732   \texttt{best_tac}, \texttt{safe_tac}, and \texttt{clarify_tac} in
   733   \cite[\S11]{isabelle-ref} for more information.
   734 \end{descr}
   735 
   736 Any of above methods support additional modifiers of the context of classical
   737 rules.  Their semantics is analogous to the attributes given in
   738 \S\ref{sec:classical-mod}.  Facts provided by forward chaining are
   739 inserted\footnote{These methods usually cannot make proper use of actual rules
   740   inserted that way, though.} into the goal before doing the search.  The
   741 ``!''~argument causes the full context of assumptions to be included as well.
   742 This is slightly less hazardous than for the Simplifier (see
   743 \S\ref{sec:simp}).
   744 
   745 
   746 \subsection{Combined automated methods}\label{sec:clasimp}
   747 
   748 \indexisarmeth{auto}\indexisarmeth{force}\indexisarmeth{clarsimp}
   749 \indexisarmeth{fastsimp}\indexisarmeth{slowsimp}\indexisarmeth{bestsimp}
   750 \begin{matharray}{rcl}
   751   auto & : & \isarmeth \\
   752   force & : & \isarmeth \\
   753   clarsimp & : & \isarmeth \\
   754   fastsimp & : & \isarmeth \\
   755   slowsimp & : & \isarmeth \\
   756   bestsimp & : & \isarmeth \\
   757 \end{matharray}
   758 
   759 \begin{rail}
   760   'auto' '!'? (nat nat)? (clasimpmod * )
   761   ;
   762   ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') '!'? (clasimpmod * )
   763   ;
   764 
   765   clasimpmod: ('simp' (() | 'add' | 'del' | 'only') |
   766     ('cong' | 'split' | 'iff') (() | 'add' | 'del') |
   767     (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' thmrefs
   768 \end{rail}
   769 
   770 \begin{descr}
   771 \item [$auto$, $force$, $clarsimp$, $fastsimp$, $slowsimp$, and $bestsimp$]
   772   provide access to Isabelle's combined simplification and classical reasoning
   773   tactics.  These correspond to \texttt{auto_tac}, \texttt{force_tac},
   774   \texttt{clarsimp_tac}, and Classical Reasoner tactics with the Simplifier
   775   added as wrapper, see \cite[\S11]{isabelle-ref} for more information.  The
   776   modifier arguments correspond to those given in \S\ref{sec:simp} and
   777   \S\ref{sec:classical-auto}.  Just note that the ones related to the
   778   Simplifier are prefixed by \railtterm{simp} here.
   779 
   780   Facts provided by forward chaining are inserted into the goal before doing
   781   the search.  The ``!''~argument causes the full context of assumptions to be
   782   included as well.
   783 \end{descr}
   784 
   785 
   786 \subsection{Declaring rules}\label{sec:classical-mod}
   787 
   788 \indexisarcmd{print-claset}
   789 \indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
   790 \indexisaratt{iff}\indexisaratt{rule}
   791 \begin{matharray}{rcl}
   792   print_claset & : & \isarkeep{theory~|~proof} \\
   793   intro & : & \isaratt \\
   794   elim & : & \isaratt \\
   795   dest & : & \isaratt \\
   796   rule & : & \isaratt \\
   797   iff & : & \isaratt \\
   798 \end{matharray}
   799 
   800 \begin{rail}
   801   ('intro' | 'elim' | 'dest') ('!' | () | '?')
   802   ;
   803   'rule' 'del'
   804   ;
   805   'iff' (() | 'add' | 'del')
   806   ;
   807 \end{rail}
   808 
   809 \begin{descr}
   810 \item [$print_claset$] prints the collection of rules declared to the
   811   Classical Reasoner, which is also known as ``simpset'' internally
   812   \cite{isabelle-ref}.  This is a diagnostic command; $undo$ does not apply.
   813 \item [$intro$, $elim$, and $dest$] declare introduction, elimination, and
   814   destruct rules, respectively.  By default, rules are considered as
   815   \emph{unsafe} (i.e.\ not applied blindly without backtracking), while a
   816   single ``!'' classifies as \emph{safe}, and ``?'' as \emph{extra} (i.e.\ not
   817   applied in the search-oriented automated methods, but only in single-step
   818   methods such as $rule$).
   819 \item [$rule~del$] deletes introduction, elimination, or destruct rules from
   820   the context.
   821 \item [$iff$] declares equations both as rules for the Simplifier and
   822   Classical Reasoner.
   823 \end{descr}
   824 
   825 
   826 %%% Local Variables:
   827 %%% mode: latex
   828 %%% TeX-master: "isar-ref"
   829 %%% End: