doc-src/IsarRef/generic.tex
author wenzelm
Fri Sep 01 00:48:12 2000 +0200 (2000-09-01)
changeset 9780 d25d6a977ea6
parent 9711 75df6a20b0b3
child 9799 038b018f86f5
permissions -rw-r--r--
added 'safe' method;
'auto' method: optional parms;
     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{elimify}
   309 \indexisaratt{no-vars}
   310 
   311 \indexisaratt{THEN}\indexisaratt{COMP}
   312 \indexisaratt{where}
   313 \indexisaratt{tag}\indexisaratt{untag}
   314 \indexisaratt{export}
   315 \indexisaratt{unfold}\indexisaratt{fold}
   316 \begin{matharray}{rcl}
   317   tag & : & \isaratt \\
   318   untag & : & \isaratt \\[0.5ex]
   319   THEN & : & \isaratt \\
   320   COMP & : & \isaratt \\[0.5ex]
   321   where & : & \isaratt \\[0.5ex]
   322   unfold & : & \isaratt \\
   323   fold & : & \isaratt \\[0.5ex]
   324   standard & : & \isaratt \\
   325   elimify & : & \isaratt \\
   326   no_vars & : & \isaratt \\
   327   export^* & : & \isaratt \\
   328 \end{matharray}
   329 
   330 \begin{rail}
   331   'tag' (nameref+)
   332   ;
   333   'untag' name
   334   ;
   335   ('THEN' | 'COMP') nat? thmref
   336   ;
   337   'where' (name '=' term * 'and')
   338   ;
   339   ('unfold' | 'fold') thmrefs
   340   ;
   341 \end{rail}
   342 
   343 \begin{descr}
   344 \item [$tag~name~args$ and $untag~name$] add and remove $tags$ of some
   345   theorem.  Tags may be any list of strings that serve as comment for some
   346   tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the
   347   result).  The first string is considered the tag name, the rest its
   348   arguments.  Note that untag removes any tags of the same name.
   349 \item [$THEN~n~a$ and $COMP~n~a$] compose rules.  $THEN$ resolves with the
   350   $n$-th premise of $a$; the $COMP$ version skips the automatic lifting
   351   process that is normally intended (cf.\ \texttt{RS} and \texttt{COMP} in
   352   \cite[\S5]{isabelle-ref}).
   353 \item [$where~\vec x = \vec t$] perform named instantiation of schematic
   354   variables occurring in a theorem.  Unlike instantiation tactics such as
   355   $rule_tac$ (see \S\ref{sec:tactic-commands}), actual schematic variables
   356   have to be specified (e.g.\ $\Var{x@3}$).
   357 
   358 \item [$unfold~\vec a$ and $fold~\vec a$] expand and fold back again the given
   359   meta-level definitions throughout a rule.
   360 
   361 \item [$standard$] puts a theorem into the standard form of object-rules, just
   362   as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).
   363 
   364 \item [$elimify$] turns an destruction rule into an elimination, just as the
   365   ML function \texttt{make\_elim} (see \cite{isabelle-ref}).
   366 
   367 \item [$no_vars$] replaces schematic variables by free ones; this is mainly
   368   for tuning output of pretty printed theorems.
   369 
   370 \item [$export$] lifts a local result out of the current proof context,
   371   generalizing all fixed variables and discharging all assumptions.  Note that
   372   proper incremental export is already done as part of the basic Isar
   373   machinery.  This attribute is mainly for experimentation.
   374 
   375 \end{descr}
   376 
   377 
   378 \section{Tactic emulations}\label{sec:tactics}
   379 
   380 The following improper proof methods emulate traditional tactics.  These admit
   381 direct access to the goal state, which is normally considered harmful!  In
   382 particular, this may involve both numbered goal addressing (default 1), and
   383 dynamic instantiation within the scope of some subgoal.
   384 
   385 \begin{warn}
   386   Dynamic instantiations are read and type-checked according to a subgoal of
   387   the current dynamic goal state, rather than the static proof context!  In
   388   particular, locally fixed variables and term abbreviations may not be
   389   included in the term specifications.  Thus schematic variables are left to
   390   be solved by unification with certain parts of the subgoal involved.
   391 \end{warn}
   392 
   393 Note that the tactic emulation proof methods in Isabelle/Isar are consistently
   394 named $foo_tac$.
   395 
   396 \indexisarmeth{rule-tac}\indexisarmeth{erule-tac}
   397 \indexisarmeth{drule-tac}\indexisarmeth{frule-tac}
   398 \indexisarmeth{cut-tac}\indexisarmeth{thin-tac}
   399 \indexisarmeth{subgoal-tac}\indexisarmeth{rename-tac}
   400 \indexisarmeth{rotate-tac}\indexisarmeth{tactic}
   401 \begin{matharray}{rcl}
   402   rule_tac^* & : & \isarmeth \\
   403   erule_tac^* & : & \isarmeth \\
   404   drule_tac^* & : & \isarmeth \\
   405   frule_tac^* & : & \isarmeth \\
   406   cut_tac^* & : & \isarmeth \\
   407   thin_tac^* & : & \isarmeth \\
   408   subgoal_tac^* & : & \isarmeth \\
   409   rename_tac^* & : & \isarmeth \\
   410   rotate_tac^* & : & \isarmeth \\
   411   tactic^* & : & \isarmeth \\
   412 \end{matharray}
   413 
   414 \railalias{ruletac}{rule\_tac}
   415 \railterm{ruletac}
   416 
   417 \railalias{eruletac}{erule\_tac}
   418 \railterm{eruletac}
   419 
   420 \railalias{druletac}{drule\_tac}
   421 \railterm{druletac}
   422 
   423 \railalias{fruletac}{frule\_tac}
   424 \railterm{fruletac}
   425 
   426 \railalias{cuttac}{cut\_tac}
   427 \railterm{cuttac}
   428 
   429 \railalias{thintac}{thin\_tac}
   430 \railterm{thintac}
   431 
   432 \railalias{subgoaltac}{subgoal\_tac}
   433 \railterm{subgoaltac}
   434 
   435 \railalias{renametac}{rename\_tac}
   436 \railterm{renametac}
   437 
   438 \railalias{rotatetac}{rotate\_tac}
   439 \railterm{rotatetac}
   440 
   441 \begin{rail}
   442   ( ruletac | eruletac | druletac | fruletac | cuttac | thintac ) goalspec?
   443   ( insts thmref | thmrefs )
   444   ;
   445   subgoaltac goalspec? (prop +)
   446   ;
   447   renametac goalspec? (name +)
   448   ;
   449   rotatetac goalspec? int?
   450   ;
   451   'tactic' text
   452   ;
   453 
   454   insts: ((name '=' term) + 'and') 'in'
   455   ;
   456 \end{rail}
   457 
   458 \begin{descr}
   459 \item [$rule_tac$ etc.] do resolution of rules with explicit instantiation.
   460   This works the same way as the ML tactics \texttt{res_inst_tac} etc. (see
   461   \cite[\S3]{isabelle-ref}).
   462 
   463   Note that multiple rules may be only given there is no instantiation.  Then
   464   $rule_tac$ is the same as \texttt{resolve_tac} in ML (see
   465   \cite[\S3]{isabelle-ref}).
   466 \item [$cut_tac$] inserts facts into the proof state as assumption of a
   467   subgoal, see also \texttt{cut_facts_tac} in \cite[\S3]{isabelle-ref}.  Note
   468   that the scope of schmatic variables is spread over the main goal statement.
   469   Instantiations may be given as well, see also ML tactic
   470   \texttt{cut_inst_tac} in \cite[\S3]{isabelle-ref}.
   471 \item [$thin_tac~\phi$] deletes the specified assumption from a subgoal; note
   472   that $\phi$ may contain schematic variables.  See also \texttt{thin_tac} in
   473   \cite[\S3]{isabelle-ref}.
   474 \item [$subgoal_tac~\phi$] adds $\phi$ as an assumption to a subgoal.  See
   475   also \texttt{subgoal_tac} and \texttt{subgoals_tac} in
   476   \cite[\S3]{isabelle-ref}.
   477 \item [$rename_tac~\vec x$] renames parameters of a goal according to the list
   478   $\vec x$, which refers to the \emph{suffix} of variables.
   479 \item [$rotate_tac~n$] rotates the assumptions of a goal by $n$ positions:
   480   from right to left if $n$ is positive, and from left to right if $n$ is
   481   negative; the default value is $1$.  See also \texttt{rotate_tac} in
   482   \cite[\S3]{isabelle-ref}.
   483 \item [$tactic~text$] produces a proof method from any ML text of type
   484   \texttt{tactic}.  Apart from the usual ML environment and the current
   485   implicit theory context, the ML code may refer to the following locally
   486   bound values:
   487 
   488 %%FIXME ttbox produces too much trailing space (why?)
   489 {\footnotesize\begin{verbatim}
   490 val ctxt  : Proof.context
   491 val facts : thm list
   492 val thm   : string -> thm
   493 val thms  : string -> thm list
   494 \end{verbatim}}
   495   Here \texttt{ctxt} refers to the current proof context, \texttt{facts}
   496   indicates any current facts for forward-chaining, and
   497   \texttt{thm}~/~\texttt{thms} retrieve named facts (including global
   498   theorems) from the context.
   499 \end{descr}
   500 
   501 
   502 \section{The Simplifier}\label{sec:simplifier}
   503 
   504 \subsection{Simplification methods}\label{sec:simp}
   505 
   506 \indexisarmeth{simp}\indexisarmeth{simp-all}
   507 \begin{matharray}{rcl}
   508   simp & : & \isarmeth \\
   509   simp_all & : & \isarmeth \\
   510 \end{matharray}
   511 
   512 \railalias{simpall}{simp\_all}
   513 \railterm{simpall}
   514 
   515 \railalias{noasm}{no\_asm}
   516 \railterm{noasm}
   517 
   518 \railalias{noasmsimp}{no\_asm\_simp}
   519 \railterm{noasmsimp}
   520 
   521 \railalias{noasmuse}{no\_asm\_use}
   522 \railterm{noasmuse}
   523 
   524 \begin{rail}
   525   ('simp' | simpall) ('!' ?) opt? (simpmod * )
   526   ;
   527 
   528   opt: '(' (noasm | noasmsimp | noasmuse) ')'
   529   ;
   530   simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
   531     'split' (() | 'add' | 'del') | 'other') ':' thmrefs
   532   ;
   533 \end{rail}
   534 
   535 \begin{descr}
   536 \item [$simp$] invokes Isabelle's simplifier, after declaring additional rules
   537   according to the arguments given.  Note that the \railtterm{only} modifier
   538   first removes all other rewrite rules, congruences, and looper tactics
   539   (including splits), and then behaves like \railtterm{add}.
   540   
   541   \medskip The \railtterm{cong} modifiers add or delete Simplifier congruence
   542   rules (see also \cite{isabelle-ref}), the default is to add.
   543   
   544   \medskip The \railtterm{split} modifiers add or delete rules for the
   545   Splitter (see also \cite{isabelle-ref}), the default is to add.  This works
   546   only if the Simplifier method has been properly setup to include the
   547   Splitter (all major object logics such HOL, HOLCF, FOL, ZF do this already).
   548   
   549   \medskip The \railtterm{other} modifier ignores its arguments.
   550   Nevertheless, additional kinds of rules may be declared by including
   551   appropriate attributes in the specification.
   552 \item [$simp_all$] is similar to $simp$, but acts on all goals.
   553 \end{descr}
   554 
   555 By default, the Simplifier methods are based on \texttt{asm_full_simp_tac}
   556 internally \cite[\S10]{isabelle-ref}, which means that assumptions are both
   557 simplified as well as used in simplifying the conclusion.  In structured
   558 proofs this is usually quite well behaved in practice: just the local premises
   559 of the actual goal are involved, additional facts may inserted via explicit
   560 forward-chaining (using $\THEN$, $\FROMNAME$ etc.).  The full context of
   561 assumptions is only included if the ``$!$'' (bang) argument is given, which
   562 should be used with some care, though.
   563 
   564 Additional Simplifier options may be specified to tune the behavior even
   565 further: $(no_asm)$ means assumptions are ignored completely (cf.\
   566 \texttt{simp_tac}), $(no_asm_simp)$ means assumptions are used in the
   567 simplification of the conclusion but are not themselves simplified (cf.\
   568 \texttt{asm_simp_tac}), and $(no_asm_use)$ means assumptions are simplified
   569 but are not used in the simplification of each other or the conclusion (cf.
   570 \texttt{full_simp_tac}).
   571 
   572 \medskip
   573 
   574 The Splitter package is usually configured to work as part of the Simplifier.
   575 The effect of repeatedly applying \texttt{split_tac} can be simulated by
   576 $(simp~only\colon~split\colon~\vec a)$.  There is also a separate $split$
   577 method available for single-step case splitting, see \S\ref{sec:basic-eq}.
   578 
   579 
   580 \subsection{Declaring rules}
   581 
   582 \indexisarcmd{print-simpset}
   583 \indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong}
   584 \begin{matharray}{rcl}
   585   print_simpset & : & \isarkeep{theory~|~proof} \\
   586   simp & : & \isaratt \\
   587   cong & : & \isaratt \\
   588   split & : & \isaratt \\
   589 \end{matharray}
   590 
   591 \begin{rail}
   592   ('simp' | 'cong' | 'split') (() | 'add' | 'del')
   593   ;
   594 \end{rail}
   595 
   596 \begin{descr}
   597 \item [$print_simpset$] prints the collection of rules declared to the
   598   Simplifier, which is also known as ``simpset'' internally
   599   \cite{isabelle-ref}.  This is a diagnostic command; $undo$ does not apply.
   600 \item [$simp$] declares simplification rules.
   601 \item [$cong$] declares congruence rules.
   602 \item [$split$] declares case split rules.
   603 \end{descr}
   604 
   605 
   606 \subsection{Forward simplification}
   607 
   608 \indexisaratt{simplify}\indexisaratt{asm-simplify}
   609 \indexisaratt{full-simplify}\indexisaratt{asm-full-simplify}
   610 \begin{matharray}{rcl}
   611   simplify & : & \isaratt \\
   612   asm_simplify & : & \isaratt \\
   613   full_simplify & : & \isaratt \\
   614   asm_full_simplify & : & \isaratt \\
   615 \end{matharray}
   616 
   617 These attributes provide forward rules for simplification, which should be
   618 used only very rarely.  There are no separate options for declaring
   619 simplification rules locally.
   620 
   621 See the ML functions of the same name in \cite[\S10]{isabelle-ref} for more
   622 information.
   623 
   624 
   625 \section{Basic equational reasoning}\label{sec:basic-eq}
   626 
   627 \indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisarmeth{split}\indexisaratt{symmetric}
   628 \begin{matharray}{rcl}
   629   subst & : & \isarmeth \\
   630   hypsubst^* & : & \isarmeth \\
   631   split & : & \isarmeth \\
   632   symmetric & : & \isaratt \\
   633 \end{matharray}
   634 
   635 \begin{rail}
   636   'subst' thmref
   637   ;
   638   'split' thmrefs
   639   ;
   640 \end{rail}
   641 
   642 These methods and attributes provide basic facilities for equational reasoning
   643 that are intended for specialized applications only.  Normally, single step
   644 reasoning would be performed by calculation (see \S\ref{sec:calculation}),
   645 while the Simplifier is the canonical tool for automated normalization (see
   646 \S\ref{sec:simplifier}).
   647 
   648 \begin{descr}
   649 \item [$subst~thm$] performs a single substitution step using rule $thm$,
   650   which may be either a meta or object equality.
   651 \item [$hypsubst$] performs substitution using some assumption.
   652 \item [$split~thms$] performs single-step case splitting using rules $thms$.
   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}
   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{best}
   703 \indexisarmeth{safe}\indexisarmeth{clarify}
   704 \begin{matharray}{rcl}
   705   blast & : & \isarmeth \\
   706   fast & : & \isarmeth \\
   707   best & : & \isarmeth \\
   708   safe & : & \isarmeth \\
   709   clarify & : & \isarmeth \\
   710 \end{matharray}
   711 
   712 \begin{rail}
   713   'blast' ('!' ?) nat? (clamod * )
   714   ;
   715   ('fast' | 'best' | 'clarify' | 'safe') ('!' ?) (clamod * )
   716   ;
   717 
   718   clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs
   719   ;
   720 \end{rail}
   721 
   722 \begin{descr}
   723 \item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac}
   724   in \cite[\S11]{isabelle-ref}).  The optional argument specifies a
   725   user-supplied search bound (default 20).  Note that $blast$ is the only
   726   classical proof procedure in Isabelle that can handle actual object-logic
   727   rules as local assumptions ($fast$ etc.\ would just ignore non-atomic
   728   facts).
   729 \item [$fast$, $best$, $safe$, and $clarify$] refer to the generic classical
   730   reasoner.  See \texttt{fast_tac}, \texttt{best_tac}, \texttt{safe_tac}, and
   731   \texttt{clarify_tac} in \cite[\S11]{isabelle-ref} for more information.
   732 \end{descr}
   733 
   734 Any of above methods support additional modifiers of the context of classical
   735 rules.  Their semantics is analogous to the attributes given in
   736 \S\ref{sec:classical-mod}.  Facts provided by forward chaining are
   737 inserted\footnote{These methods usually cannot make proper use of actual rules
   738   inserted that way, though.} into the goal before doing the search.  The
   739 ``!''~argument causes the full context of assumptions to be included as well.
   740 This is slightly less hazardous than for the Simplifier (see
   741 \S\ref{sec:simp}).
   742 
   743 
   744 \subsection{Combined automated methods}
   745 
   746 \indexisarmeth{auto}\indexisarmeth{force}
   747 \indexisarmeth{clarsimp}\indexisarmeth{fastsimp}
   748 \begin{matharray}{rcl}
   749   auto & : & \isarmeth \\
   750   force & : & \isarmeth \\
   751   clarsimp & : & \isarmeth \\
   752   fastsimp & : & \isarmeth \\
   753 \end{matharray}
   754 
   755 \begin{rail}
   756   'auto' '!'? (nat nat)? (clasimpmod * )
   757   ;
   758   ('force' | 'clarsimp' | 'fastsimp') '!'? (clasimpmod * )
   759   ;
   760 
   761   clasimpmod: ('simp' (() | 'add' | 'del' | 'only') |
   762     'cong' (() | 'add' | 'del') | ('split' (() | 'add' | 'del')) | 'other' |
   763     (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' thmrefs
   764 \end{rail}
   765 
   766 \begin{descr}
   767 \item [$auto$, $force$, $clarsimp$, $fastsimp$] provide access to Isabelle's
   768   combined simplification and classical reasoning tactics.  These correspond
   769   to \texttt{auto_tac}, \texttt{force_tac}, \texttt{clarsimp_tac}, and
   770   \texttt{fast_tac} (with the Simplifier added as wrapper), see
   771   \cite[\S11]{isabelle-ref} for more information.  The modifier arguments
   772   correspond to those given in \S\ref{sec:simp} and
   773   \S\ref{sec:classical-auto}.  Just note that the ones related to the
   774   Simplifier are prefixed by \railtterm{simp} here.
   775 
   776   Facts provided by forward chaining are inserted into the goal before doing
   777   the search.  The ``!''~argument causes the full context of assumptions to be
   778   included as well.
   779 \end{descr}
   780 
   781 
   782 \subsection{Declaring rules}\label{sec:classical-mod}
   783 
   784 \indexisarcmd{print-claset}
   785 \indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
   786 \indexisaratt{iff}\indexisaratt{delrule}
   787 \begin{matharray}{rcl}
   788   print_claset & : & \isarkeep{theory~|~proof} \\
   789   intro & : & \isaratt \\
   790   elim & : & \isaratt \\
   791   dest & : & \isaratt \\
   792   iff & : & \isaratt \\
   793   delrule & : & \isaratt \\
   794 \end{matharray}
   795 
   796 \begin{rail}
   797   ('intro' | 'elim' | 'dest') ('!' | () | '?')
   798   ;
   799   'iff' (() | 'add' | 'del')
   800 \end{rail}
   801 
   802 \begin{descr}
   803 \item [$print_claset$] prints the collection of rules declared to the
   804   Classical Reasoner, which is also known as ``simpset'' internally
   805   \cite{isabelle-ref}.  This is a diagnostic command; $undo$ does not apply.
   806 \item [$intro$, $elim$, and $dest$] declare introduction, elimination, and
   807   destruct rules, respectively.  By default, rules are considered as
   808   \emph{unsafe} (i.e.\ not applied blindly without backtracking), while a
   809   single ``!'' classifies as \emph{safe}, and ``?'' as \emph{extra} (i.e.\ not
   810   applied in the search-oriented automated methods, but only in single-step
   811   methods such as $rule$).
   812 
   813 \item [$iff$] declares equations both as rules for the Simplifier and
   814   Classical Reasoner.
   815 
   816 \item [$delrule$] deletes introduction or elimination rules from the context.
   817   Note that destruction rules would have to be turned into elimination rules
   818   first, e.g.\ by using the $elimify$ attribute.
   819 \end{descr}
   820 
   821 
   822 %%% Local Variables:
   823 %%% mode: latex
   824 %%% TeX-master: "isar-ref"
   825 %%% End: