doc-src/IsarRef/generic.tex
author wenzelm
Wed Sep 08 18:10:39 1999 +0200 (1999-09-08)
changeset 7526 1ea137d3b5bf
parent 7466 7df66ce6508a
child 7897 7f18f5ffbb92
permissions -rw-r--r--
(un)fold: ignore facts;
wenzelm@7135
     1
wenzelm@7167
     2
\chapter{Generic Tools and Packages}\label{ch:gen-tools}
wenzelm@7167
     3
wenzelm@7315
     4
\section{Basic proof methods}\label{sec:pure-meth}
wenzelm@7167
     5
wenzelm@7167
     6
\indexisarmeth{fail}\indexisarmeth{succeed}\indexisarmeth{$-$}\indexisarmeth{assumption}
wenzelm@7458
     7
\indexisarmeth{fold}\indexisarmeth{unfold}
wenzelm@7167
     8
\indexisarmeth{rule}\indexisarmeth{erule}
wenzelm@7167
     9
\begin{matharray}{rcl}
wenzelm@7167
    10
  - & : & \isarmeth \\
wenzelm@7167
    11
  assumption & : & \isarmeth \\
wenzelm@7321
    12
  rule & : & \isarmeth \\
wenzelm@7321
    13
  erule^* & : & \isarmeth \\[0.5ex]
wenzelm@7167
    14
  fold & : & \isarmeth \\
wenzelm@7321
    15
  unfold & : & \isarmeth \\[0.5ex]
wenzelm@7335
    16
  succeed & : & \isarmeth \\
wenzelm@7321
    17
  fail & : & \isarmeth \\
wenzelm@7167
    18
\end{matharray}
wenzelm@7167
    19
wenzelm@7167
    20
\begin{rail}
wenzelm@7167
    21
  ('fold' | 'unfold' | 'rule' | 'erule') thmrefs
wenzelm@7167
    22
  ;
wenzelm@7167
    23
\end{rail}
wenzelm@7167
    24
wenzelm@7167
    25
\begin{descr}
wenzelm@7321
    26
\item [``$-$''] does nothing but insert the forward chaining facts as premises
wenzelm@7335
    27
  into the goal.  Note that command $\PROOFNAME$ without any method actually
wenzelm@7335
    28
  performs a single reduction step using the $rule$ method (see below); thus a
wenzelm@7335
    29
  plain \emph{do-nothing} proof step would be $\PROOF{-}$ rather than
wenzelm@7335
    30
  $\PROOFNAME$ alone.
wenzelm@7466
    31
\item [$assumption$] solves some goal by assumption.  Any facts given are
wenzelm@7466
    32
  guaranteed to participate in the refinement.
wenzelm@7321
    33
\item [$rule~thms$] applies some rule given as argument in backward manner;
wenzelm@7321
    34
  facts are used to reduce the rule before applying it to the goal.  Thus
wenzelm@7321
    35
  $rule$ without facts is plain \emph{introduction}, while with facts it
wenzelm@7321
    36
  becomes an \emph{elimination}.
wenzelm@7321
    37
  
wenzelm@7321
    38
  Note that the classical reasoner introduces another version of $rule$ that
wenzelm@7321
    39
  is able to pick appropriate rules automatically, whenever explicit $thms$
wenzelm@7335
    40
  are omitted (see \S\ref{sec:classical-basic}); that method is the default
wenzelm@7335
    41
  one for initial proof steps, such as $\PROOFNAME$ and ``$\DDOT$'' (two
wenzelm@7335
    42
  dots).
wenzelm@7321
    43
\item [$erule~thms$] is similar to $rule$, but applies rules by
wenzelm@7321
    44
  elim-resolution.  This is an improper method, mainly for experimentation and
wenzelm@7335
    45
  porting of old scripts.  Actual elimination proofs are usually done with
wenzelm@7335
    46
  $rule$ (single step, involving facts) or $elim$ (multiple steps, see
wenzelm@7321
    47
  \S\ref{sec:classical-basic}).
wenzelm@7335
    48
\item [$unfold~thms$ and $fold~thms$] expand and fold back again the given
wenzelm@7526
    49
  meta-level definitions throughout all goals; any facts provided are
wenzelm@7526
    50
  \emph{ignored}.
wenzelm@7335
    51
\item [$succeed$] yields a single (unchanged) result; it is the identify of
wenzelm@7335
    52
  the ``\texttt{,}'' method combinator.
wenzelm@7321
    53
\item [$fail$] yields an empty result sequence; it is the identify of the
wenzelm@7321
    54
  ``\texttt{|}'' method combinator.
wenzelm@7321
    55
\end{descr}
wenzelm@7167
    56
wenzelm@7315
    57
wenzelm@7315
    58
\section{Miscellaneous attributes}
wenzelm@7315
    59
wenzelm@7167
    60
\indexisaratt{tag}\indexisaratt{untag}\indexisaratt{COMP}\indexisaratt{RS}
wenzelm@7167
    61
\indexisaratt{OF}\indexisaratt{where}\indexisaratt{of}\indexisaratt{standard}
wenzelm@7167
    62
\indexisaratt{elimify}\indexisaratt{transfer}\indexisaratt{export}
wenzelm@7167
    63
\begin{matharray}{rcl}
wenzelm@7167
    64
  tag & : & \isaratt \\
wenzelm@7321
    65
  untag & : & \isaratt \\[0.5ex]
wenzelm@7321
    66
  OF & : & \isaratt \\
wenzelm@7167
    67
  RS & : & \isaratt \\
wenzelm@7321
    68
  COMP & : & \isaratt \\[0.5ex]
wenzelm@7335
    69
  of & : & \isaratt \\
wenzelm@7335
    70
  where & : & \isaratt \\[0.5ex]
wenzelm@7167
    71
  standard & : & \isaratt \\
wenzelm@7167
    72
  elimify & : & \isaratt \\
wenzelm@7335
    73
  export^* & : & \isaratt \\
wenzelm@7167
    74
  transfer & : & \isaratt \\
wenzelm@7167
    75
\end{matharray}
wenzelm@7167
    76
wenzelm@7167
    77
\begin{rail}
wenzelm@7167
    78
  ('tag' | 'untag') (nameref+)
wenzelm@7167
    79
  ;
wenzelm@7167
    80
  'OF' thmrefs
wenzelm@7167
    81
  ;
wenzelm@7321
    82
  ('RS' | 'COMP') nat? thmref
wenzelm@7167
    83
  ;
wenzelm@7175
    84
  'of' (inst * ) ('concl' ':' (inst * ))?
wenzelm@7167
    85
  ;
wenzelm@7321
    86
  'where' (name '=' term * 'and')
wenzelm@7321
    87
  ;
wenzelm@7167
    88
wenzelm@7167
    89
  inst: underscore | term
wenzelm@7167
    90
  ;
wenzelm@7167
    91
\end{rail}
wenzelm@7167
    92
wenzelm@7167
    93
\begin{descr}
wenzelm@7321
    94
\item [$tag~tags$ and $untag~tags$] add and remove $tags$ to the theorem,
wenzelm@7321
    95
  respectively.  Tags may be any list of strings that serve as comment for
wenzelm@7321
    96
  some tools (e.g.\ $\LEMMANAME$ causes tag ``$lemma$'' to be added to the
wenzelm@7321
    97
  result).
wenzelm@7321
    98
\item [$OF~thms$, $RS~n~thm$, and $COMP~n~thm$] compose rules.  $OF$ applies
wenzelm@7321
    99
  $thms$ in parallel (cf.\ \texttt{MRS} in \cite[\S5]{isabelle-ref}, but note
wenzelm@7396
   100
  the reversed order).  Note that premises may be skipped by including $\_$
wenzelm@7396
   101
  (underscore) as argument.
wenzelm@7396
   102
  
wenzelm@7396
   103
  $RS$ resolves with the $n$-th premise of $thm$; $COMP$ is a version of $RS$
wenzelm@7396
   104
  that does not include the automatic lifting process that is normally
wenzelm@7396
   105
  intended (see also \texttt{RS} and \texttt{COMP} in
wenzelm@7321
   106
  \cite[\S5]{isabelle-ref}).
wenzelm@7321
   107
  
wenzelm@7466
   108
\item [$of~\vec t$ and $where~\vec x = \vec t$] perform positional and named
wenzelm@7335
   109
  instantiation, respectively.  The terms given in $of$ are substituted for
wenzelm@7335
   110
  any schematic variables occurring in a theorem from left to right;
wenzelm@7335
   111
  ``\texttt{_}'' (underscore) indicates to skip a position.
wenzelm@7321
   112
 
wenzelm@7321
   113
\item [$standard$] puts a theorem into the standard form of object-rules, just
wenzelm@7321
   114
  as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).
wenzelm@7321
   115
  
wenzelm@7335
   116
\item [$elimify$] turns an destruction rule into an elimination.
wenzelm@7321
   117
  
wenzelm@7321
   118
\item [$export$] lifts a local result out of the current proof context,
wenzelm@7335
   119
  generalizing all fixed variables and discharging all assumptions.  Note that
wenzelm@7335
   120
  (partial) export is usually done automatically behind the scenes.  This
wenzelm@7335
   121
  attribute is mainly for experimentation.
wenzelm@7321
   122
  
wenzelm@7321
   123
\item [$transfer$] promotes a theorem to the current theory context, which has
wenzelm@7321
   124
  to enclose the former one.  Normally, this is done automatically when rules
wenzelm@7321
   125
  are joined by inference.
wenzelm@7321
   126
wenzelm@7167
   127
\end{descr}
wenzelm@7167
   128
wenzelm@7315
   129
wenzelm@7315
   130
\section{Calculational proof}\label{sec:calculation}
wenzelm@7315
   131
wenzelm@7315
   132
\indexisarcmd{also}\indexisarcmd{finally}\indexisaratt{trans}
wenzelm@7315
   133
\begin{matharray}{rcl}
wenzelm@7315
   134
  \isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7315
   135
  \isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\
wenzelm@7315
   136
  trans & : & \isaratt \\
wenzelm@7315
   137
\end{matharray}
wenzelm@7315
   138
wenzelm@7315
   139
Calculational proof is forward reasoning with implicit application of
wenzelm@7315
   140
transitivity rules (such those of $=$, $\le$, $<$).  Isabelle/Isar maintains
wenzelm@7391
   141
an auxiliary register $calculation$\indexisarthm{calculation} for accumulating
wenzelm@7458
   142
results obtained by transitivity obtained together with the current result.
wenzelm@7315
   143
Command $\ALSO$ updates $calculation$ from the most recent result, while
wenzelm@7315
   144
$\FINALLY$ exhibits the final result by forward chaining towards the next goal
wenzelm@7315
   145
statement.  Both commands require valid current facts, i.e.\ may occur only
wenzelm@7315
   146
after commands that produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or
wenzelm@7315
   147
some finished $\HAVENAME$ or $\SHOWNAME$.
wenzelm@7315
   148
wenzelm@7315
   149
Also note that the automatic term abbreviation ``$\dots$'' has its canonical
wenzelm@7315
   150
application with calculational proofs.  It automatically refers to the
wenzelm@7315
   151
argument\footnote{The argument of a curried infix expression is its right-hand
wenzelm@7315
   152
  side.} of the preceding statement.
wenzelm@7315
   153
wenzelm@7315
   154
Isabelle/Isar calculations are implicitly subject to block structure in the
wenzelm@7315
   155
sense that new threads of calculational reasoning are commenced for any new
wenzelm@7315
   156
block (as opened by a local goal, for example).  This means that, apart from
wenzelm@7315
   157
being able to nest calculations, there is no separate \emph{begin-calculation}
wenzelm@7315
   158
command required.
wenzelm@7315
   159
wenzelm@7315
   160
\begin{rail}
wenzelm@7315
   161
  ('also' | 'finally') transrules? comment?
wenzelm@7315
   162
  ;
wenzelm@7315
   163
  'trans' (() | 'add' ':' | 'del' ':') thmrefs
wenzelm@7315
   164
  ;
wenzelm@7315
   165
wenzelm@7315
   166
  transrules: '(' thmrefs ')' interest?
wenzelm@7315
   167
  ;
wenzelm@7315
   168
\end{rail}
wenzelm@7315
   169
wenzelm@7315
   170
\begin{descr}
wenzelm@7315
   171
\item [$\ALSO~(thms)$] maintains the auxiliary $calculation$ register as
wenzelm@7315
   172
  follows.  The first occurrence of $\ALSO$ in some calculational thread
wenzelm@7458
   173
  initialises $calculation$ by $this$. Any subsequent $\ALSO$ on the same
wenzelm@7335
   174
  level of block-structure updates $calculation$ by some transitivity rule
wenzelm@7458
   175
  applied to $calculation$ and $this$ (in that order).  Transitivity rules are
wenzelm@7458
   176
  picked from the current context plus those given as $thms$ (the latter have
wenzelm@7458
   177
  precedence).
wenzelm@7315
   178
  
wenzelm@7315
   179
\item [$\FINALLY~(thms)$] maintaining $calculation$ in the same way as
wenzelm@7315
   180
  $\ALSO$, and concludes the current calculational thread.  The final result
wenzelm@7315
   181
  is exhibited as fact for forward chaining towards the next goal. Basically,
wenzelm@7315
   182
  $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$.  A typical proof
wenzelm@7466
   183
  idiom is ``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$''.
wenzelm@7315
   184
  
wenzelm@7335
   185
\item [$trans$] maintains the set of transitivity rules of the theory or proof
wenzelm@7335
   186
  context, by adding or deleting theorems (the default is to add).
wenzelm@7315
   187
\end{descr}
wenzelm@7315
   188
wenzelm@7335
   189
See theory \texttt{HOL/Isar_examples/Group} for a simple application of
wenzelm@7315
   190
calculations for basic equational reasoning.
wenzelm@7315
   191
\texttt{HOL/Isar_examples/KnasterTarski} involves a few more advanced
wenzelm@7315
   192
calculational steps in combination with natural deduction.
wenzelm@7315
   193
wenzelm@7315
   194
wenzelm@7135
   195
\section{Axiomatic Type Classes}\label{sec:axclass}
wenzelm@7135
   196
wenzelm@7356
   197
\indexisarcmd{axclass}\indexisarcmd{instance}\indexisarmeth{intro-classes}
wenzelm@7135
   198
\begin{matharray}{rcl}
wenzelm@7135
   199
  \isarcmd{axclass} & : & \isartrans{theory}{theory} \\
wenzelm@7135
   200
  \isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
wenzelm@7356
   201
  intro_classes & : & \isarmeth \\
wenzelm@7135
   202
\end{matharray}
wenzelm@7135
   203
wenzelm@7135
   204
Axiomatic type classes are provided by Isabelle/Pure as a purely
wenzelm@7135
   205
\emph{definitional} interface to type classes (cf.~\S\ref{sec:classes}).  Thus
wenzelm@7135
   206
any object logic may make use of this light-weight mechanism for abstract
wenzelm@7135
   207
theories.  See \cite{Wenzel:1997:TPHOL} for more information.  There is also a
wenzelm@7135
   208
tutorial on \emph{Using Axiomatic Type Classes in Isabelle} that is part of
wenzelm@7135
   209
the standard Isabelle documentation.
wenzelm@7335
   210
%FIXME cite
wenzelm@7135
   211
wenzelm@7135
   212
\begin{rail}
wenzelm@7135
   213
  'axclass' classdecl (axmdecl prop comment? +)
wenzelm@7135
   214
  ;
wenzelm@7135
   215
  'instance' (nameref '<' nameref | nameref '::' simplearity) comment?
wenzelm@7135
   216
  ;
wenzelm@7135
   217
\end{rail}
wenzelm@7135
   218
wenzelm@7167
   219
\begin{descr}
wenzelm@7335
   220
\item [$\isarkeyword{axclass}~c < \vec c~axms$] defines an axiomatic type
wenzelm@7335
   221
  class as the intersection of existing classes, with additional axioms
wenzelm@7335
   222
  holding.  Class axioms may not contain more than one type variable.  The
wenzelm@7335
   223
  class axioms (with implicit sort constraints added) are bound to the given
wenzelm@7335
   224
  names.  Furthermore a class introduction rule is generated, which is
wenzelm@7356
   225
  employed by method $intro_classes$ in support instantiation proofs of this
wenzelm@7335
   226
  class.
wenzelm@7335
   227
  
wenzelm@7335
   228
\item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~t ::
wenzelm@7335
   229
  (\vec s)c$] setup up a goal stating the class relation or type arity.  The
wenzelm@7356
   230
  proof would usually proceed by the $intro_classes$ method, and then
wenzelm@7335
   231
  establish the characteristic theorems of the type classes involved.  After
wenzelm@7335
   232
  finishing the proof the theory will be augmented by a type signature
wenzelm@7335
   233
  declaration corresponding to the resulting theorem.
wenzelm@7466
   234
\item [$intro_classes$] iteratively expands the class introduction rules of
wenzelm@7466
   235
  this theory.
wenzelm@7167
   236
\end{descr}
wenzelm@7135
   237
wenzelm@7319
   238
See theory \texttt{HOL/Isar_examples/Group} for a simple example of using
wenzelm@7319
   239
axiomatic type classes, including instantiation proofs.
wenzelm@7135
   240
wenzelm@7135
   241
wenzelm@7135
   242
\section{The Simplifier}
wenzelm@7135
   243
wenzelm@7321
   244
\subsection{Simplification methods}\label{sec:simp}
wenzelm@7315
   245
wenzelm@7391
   246
\indexisarmeth{simp}\indexisarmeth{asm-simp}
wenzelm@7315
   247
\begin{matharray}{rcl}
wenzelm@7315
   248
  simp & : & \isarmeth \\
wenzelm@7315
   249
  asm_simp & : & \isarmeth \\
wenzelm@7315
   250
\end{matharray}
wenzelm@7315
   251
wenzelm@7335
   252
\railalias{asmsimp}{asm\_simp}
wenzelm@7335
   253
\railterm{asmsimp}
wenzelm@7335
   254
wenzelm@7315
   255
\begin{rail}
wenzelm@7335
   256
  ('simp' | asmsimp) (simpmod * )
wenzelm@7315
   257
  ;
wenzelm@7315
   258
wenzelm@7315
   259
  simpmod: ('add' | 'del' | 'only' | 'other') ':' thmrefs
wenzelm@7315
   260
  ;
wenzelm@7315
   261
\end{rail}
wenzelm@7315
   262
wenzelm@7321
   263
\begin{descr}
wenzelm@7466
   264
\item [$simp$ and $asm_simp$] invoke Isabelle's simplifier, after modifying
wenzelm@7466
   265
  the context by adding or deleting given rules.  The \railtoken{only}
wenzelm@7466
   266
  modifier first removes all other rewrite rules and congruences, and then is
wenzelm@7466
   267
  like \railtoken{add}.  In contrast, \railtoken{other} ignores its arguments;
wenzelm@7466
   268
  nevertheless there may be side-effects on the context via attributes.  This
wenzelm@7466
   269
  provides a back door for arbitrary context manipulation.
wenzelm@7321
   270
  
wenzelm@7321
   271
  Both of these methods are based on \texttt{asm_full_simp_tac}, see
wenzelm@7466
   272
  \cite[\S10]{isabelle-ref}; $simp$ removes any premises of the goal, before
wenzelm@7466
   273
  inserting the goal facts; $asm_simp$ leaves the premises.  Thus $asm_simp$
wenzelm@7466
   274
  may refer to premises that are not explicitly spelled out, potentially
wenzelm@7466
   275
  obscuring the reasoning.  The plain $simp$ method is more faithful in the
wenzelm@7466
   276
  sense that, apart from the rewrite rules of the current context, \emph{at
wenzelm@7466
   277
    most} the explicitly provided facts may participate in the simplification.
wenzelm@7321
   278
\end{descr}
wenzelm@7321
   279
wenzelm@7321
   280
\subsection{Modifying the context}
wenzelm@7321
   281
wenzelm@7321
   282
\indexisaratt{simp}
wenzelm@7321
   283
\begin{matharray}{rcl}
wenzelm@7321
   284
  simp & : & \isaratt \\
wenzelm@7321
   285
\end{matharray}
wenzelm@7321
   286
wenzelm@7321
   287
\begin{rail}
wenzelm@7321
   288
  'simp' (() | 'add' | 'del')
wenzelm@7321
   289
  ;
wenzelm@7321
   290
\end{rail}
wenzelm@7321
   291
wenzelm@7321
   292
\begin{descr}
wenzelm@7466
   293
\item [$simp$] adds or deletes rules from the theory or proof context (the
wenzelm@7466
   294
  default is to add).
wenzelm@7321
   295
\end{descr}
wenzelm@7319
   296
wenzelm@7315
   297
wenzelm@7315
   298
\subsection{Forward simplification}
wenzelm@7315
   299
wenzelm@7391
   300
\indexisaratt{simplify}\indexisaratt{asm-simplify}
wenzelm@7391
   301
\indexisaratt{full-simplify}\indexisaratt{asm-full-simplify}
wenzelm@7315
   302
\begin{matharray}{rcl}
wenzelm@7315
   303
  simplify & : & \isaratt \\
wenzelm@7315
   304
  asm_simplify & : & \isaratt \\
wenzelm@7315
   305
  full_simplify & : & \isaratt \\
wenzelm@7315
   306
  asm_full_simplify & : & \isaratt \\
wenzelm@7315
   307
\end{matharray}
wenzelm@7315
   308
wenzelm@7321
   309
These attributes provide forward rules for simplification, which should be
wenzelm@7335
   310
used only very rarely.  See the ML functions of the same name in
wenzelm@7321
   311
\cite[\S10]{isabelle-ref} for more information.
wenzelm@7315
   312
wenzelm@7315
   313
wenzelm@7135
   314
\section{The Classical Reasoner}
wenzelm@7135
   315
wenzelm@7335
   316
\subsection{Basic methods}\label{sec:classical-basic}
wenzelm@7321
   317
wenzelm@7321
   318
\indexisarmeth{rule}\indexisarmeth{default}\indexisarmeth{contradiction}
wenzelm@7321
   319
\begin{matharray}{rcl}
wenzelm@7321
   320
  rule & : & \isarmeth \\
wenzelm@7321
   321
  intro & : & \isarmeth \\
wenzelm@7321
   322
  elim & : & \isarmeth \\
wenzelm@7321
   323
  contradiction & : & \isarmeth \\
wenzelm@7321
   324
\end{matharray}
wenzelm@7321
   325
wenzelm@7321
   326
\begin{rail}
wenzelm@7321
   327
  ('rule' | 'intro' | 'elim') thmrefs
wenzelm@7321
   328
  ;
wenzelm@7321
   329
\end{rail}
wenzelm@7321
   330
wenzelm@7321
   331
\begin{descr}
wenzelm@7466
   332
\item [$rule$] as offered by the classical reasoner is a refinement over the
wenzelm@7466
   333
  primitive one (see \S\ref{sec:pure-meth}).  In the case that no rules are
wenzelm@7466
   334
  provided as arguments, it automatically determines elimination and
wenzelm@7321
   335
  introduction rules from the context (see also \S\ref{sec:classical-mod}).
wenzelm@7335
   336
  In that form it is the default method for basic proof steps, such as
wenzelm@7335
   337
  $\PROOFNAME$ and ``$\DDOT$'' (two dots).
wenzelm@7321
   338
  
wenzelm@7466
   339
\item [$intro$ and $elim$] repeatedly refine some goal by intro- or
wenzelm@7321
   340
  elim-resolution, after having inserted the facts.  Omitting the arguments
wenzelm@7321
   341
  refers to any suitable rules from the context, otherwise only the explicitly
wenzelm@7335
   342
  given ones may be applied.  The latter form admits better control of what
wenzelm@7335
   343
  actually happens, thus it is very appropriate as an initial method for
wenzelm@7335
   344
  $\PROOFNAME$ that splits up certain connectives of the goal, before entering
wenzelm@7335
   345
  the sub-proof.
wenzelm@7458
   346
  
wenzelm@7466
   347
\item [$contradiction$] solves some goal by contradiction, deriving any result
wenzelm@7466
   348
  from both $\neg A$ and $A$.  Facts, which are guaranteed to participate, may
wenzelm@7466
   349
  appear in either order.
wenzelm@7321
   350
\end{descr}
wenzelm@7321
   351
wenzelm@7321
   352
wenzelm@7321
   353
\subsection{Automatic methods}\label{sec:classical-auto}
wenzelm@7315
   354
wenzelm@7321
   355
\indexisarmeth{blast}
wenzelm@7391
   356
\indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{slow}\indexisarmeth{slow-best}
wenzelm@7321
   357
\begin{matharray}{rcl}
wenzelm@7321
   358
 blast & : & \isarmeth \\
wenzelm@7321
   359
 fast & : & \isarmeth \\
wenzelm@7321
   360
 best & : & \isarmeth \\
wenzelm@7321
   361
 slow & : & \isarmeth \\
wenzelm@7321
   362
 slow_best & : & \isarmeth \\
wenzelm@7321
   363
\end{matharray}
wenzelm@7321
   364
wenzelm@7321
   365
\railalias{slowbest}{slow\_best}
wenzelm@7321
   366
\railterm{slowbest}
wenzelm@7321
   367
wenzelm@7321
   368
\begin{rail}
wenzelm@7321
   369
  'blast' nat? (clamod * )
wenzelm@7321
   370
  ;
wenzelm@7321
   371
  ('fast' | 'best' | 'slow' | slowbest) (clamod * )
wenzelm@7321
   372
  ;
wenzelm@7321
   373
wenzelm@7321
   374
  clamod: (('intro' | 'elim' | 'dest') (() | '!' | '!!') | 'del') ':' thmrefs
wenzelm@7321
   375
  ;
wenzelm@7321
   376
\end{rail}
wenzelm@7321
   377
wenzelm@7321
   378
\begin{descr}
wenzelm@7321
   379
\item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac}
wenzelm@7335
   380
  in \cite[\S11]{isabelle-ref}).  The optional argument specifies a
wenzelm@7321
   381
  user-supplied search bound (default 20).
wenzelm@7321
   382
\item [$fast$, $best$, $slow$, $slow_best$] refer to the generic classical
wenzelm@7335
   383
  reasoner (see \cite[\S11]{isabelle-ref}, tactic \texttt{fast_tac} etc).
wenzelm@7321
   384
\end{descr}
wenzelm@7321
   385
wenzelm@7321
   386
Any of above methods support additional modifiers of the context of classical
wenzelm@7321
   387
rules.  There semantics is analogous to the attributes given in
wenzelm@7321
   388
\S\ref{sec:classical-mod}.
wenzelm@7321
   389
wenzelm@7315
   390
wenzelm@7315
   391
\subsection{Combined automatic methods}
wenzelm@7315
   392
wenzelm@7321
   393
\indexisarmeth{auto}\indexisarmeth{force}
wenzelm@7321
   394
\begin{matharray}{rcl}
wenzelm@7321
   395
  force & : & \isarmeth \\
wenzelm@7321
   396
  auto & : & \isarmeth \\
wenzelm@7321
   397
\end{matharray}
wenzelm@7321
   398
wenzelm@7321
   399
\begin{rail}
wenzelm@7321
   400
  ('force' | 'auto') (clasimpmod * )
wenzelm@7321
   401
  ;
wenzelm@7315
   402
wenzelm@7321
   403
  clasimpmod: ('simp' ('add' | 'del' | 'only') | other |
wenzelm@7321
   404
    (('intro' | 'elim' | 'dest') (() | '!' | '!!') | 'del')) ':' thmrefs
wenzelm@7321
   405
\end{rail}
wenzelm@7315
   406
wenzelm@7321
   407
\begin{descr}
wenzelm@7321
   408
\item [$force$ and $auto$] provide access to Isabelle's combined
wenzelm@7321
   409
  simplification and classical reasoning tactics.  See \texttt{force_tac} and
wenzelm@7321
   410
  \texttt{auto_tac} in \cite[\S11]{isabelle-ref} for more information.  The
wenzelm@7321
   411
  modifier arguments correspond to those given in \S\ref{sec:simp} and
wenzelm@7335
   412
  \S\ref{sec:classical-auto}.  Note that the ones related to the Simplifier
wenzelm@7335
   413
  are prefixed by \railtoken{simp} here.
wenzelm@7321
   414
\end{descr}
wenzelm@7321
   415
wenzelm@7321
   416
\subsection{Modifying the context}\label{sec:classical-mod}
wenzelm@7135
   417
wenzelm@7391
   418
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
wenzelm@7391
   419
\indexisaratt{iff}\indexisaratt{delrule}
wenzelm@7321
   420
\begin{matharray}{rcl}
wenzelm@7321
   421
  intro & : & \isaratt \\
wenzelm@7321
   422
  elim & : & \isaratt \\
wenzelm@7321
   423
  dest & : & \isaratt \\
wenzelm@7391
   424
  iff & : & \isaratt \\
wenzelm@7321
   425
  delrule & : & \isaratt \\
wenzelm@7321
   426
\end{matharray}
wenzelm@7135
   427
wenzelm@7321
   428
\begin{rail}
wenzelm@7321
   429
  ('intro' | 'elim' | 'dest') (() | '!' | '!!')
wenzelm@7321
   430
  ;
wenzelm@7321
   431
\end{rail}
wenzelm@7135
   432
wenzelm@7321
   433
\begin{descr}
wenzelm@7335
   434
\item [$intro$, $elim$, $dest$] add introduction, elimination, destruct rules,
wenzelm@7335
   435
  respectively.  By default, rules are considered as \emph{safe}, while a
wenzelm@7335
   436
  single ``!'' classifies as \emph{unsafe}, and ``!!'' as \emph{extra} (i.e.\ 
wenzelm@7466
   437
  not applied in the search-oriented automatic methods, but only $rule$).
wenzelm@7335
   438
  
wenzelm@7391
   439
\item [$iff$] declares equations both as rewrite rules for the simplifier and
wenzelm@7391
   440
  classical reasoning rules.
wenzelm@7391
   441
wenzelm@7335
   442
\item [$delrule$] deletes introduction or elimination rules from the context.
wenzelm@7335
   443
  Note that destruction rules would have to be turned into elimination rules
wenzelm@7321
   444
  first, e.g.\ by using the $elimify$ attribute.
wenzelm@7321
   445
\end{descr}
wenzelm@7135
   446
wenzelm@7135
   447
wenzelm@7135
   448
%%% Local Variables: 
wenzelm@7135
   449
%%% mode: latex
wenzelm@7135
   450
%%% TeX-master: "isar-ref"
wenzelm@7135
   451
%%% End: