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