doc-src/IsarRef/generic.tex
author wenzelm
Thu Oct 21 18:04:07 1999 +0200 (1999-10-21)
changeset 7897 7f18f5ffbb92
parent 7526 1ea137d3b5bf
child 7905 c5f735f7428c
permissions -rw-r--r--
*** empty log message ***
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@7458
   174
  initialises $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@7897
   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@7466
   267
  nevertheless there may be side-effects on the context via attributes.  This
wenzelm@7466
   268
  provides a back door for arbitrary context manipulation.
wenzelm@7321
   269
  
wenzelm@7897
   270
  The $simp$ method is based on \texttt{asm_full_simp_tac} (see also
wenzelm@7897
   271
  \cite[\S10]{isabelle-ref}), but is much better behaved in practice.  Only
wenzelm@7897
   272
  the local premises of the actual goal are involved by default.  Additional
wenzelm@7897
   273
  facts may be insert via forward-chaining (using $\THEN$, $\FROMNAME$ etc.).
wenzelm@7897
   274
  The full context of assumptions is
wenzelm@7897
   275
wenzelm@7897
   276
; $simp$ removes any premises of the goal, before
wenzelm@7466
   277
  inserting the goal facts; $asm_simp$ leaves the premises.  Thus $asm_simp$
wenzelm@7466
   278
  may refer to premises that are not explicitly spelled out, potentially
wenzelm@7466
   279
  obscuring the reasoning.  The plain $simp$ method is more faithful in the
wenzelm@7466
   280
  sense that, apart from the rewrite rules of the current context, \emph{at
wenzelm@7466
   281
    most} the explicitly provided facts may participate in the simplification.
wenzelm@7321
   282
\end{descr}
wenzelm@7321
   283
wenzelm@7321
   284
\subsection{Modifying the context}
wenzelm@7321
   285
wenzelm@7321
   286
\indexisaratt{simp}
wenzelm@7321
   287
\begin{matharray}{rcl}
wenzelm@7321
   288
  simp & : & \isaratt \\
wenzelm@7321
   289
\end{matharray}
wenzelm@7321
   290
wenzelm@7321
   291
\begin{rail}
wenzelm@7321
   292
  'simp' (() | 'add' | 'del')
wenzelm@7321
   293
  ;
wenzelm@7321
   294
\end{rail}
wenzelm@7321
   295
wenzelm@7321
   296
\begin{descr}
wenzelm@7466
   297
\item [$simp$] adds or deletes rules from the theory or proof context (the
wenzelm@7466
   298
  default is to add).
wenzelm@7321
   299
\end{descr}
wenzelm@7319
   300
wenzelm@7315
   301
wenzelm@7315
   302
\subsection{Forward simplification}
wenzelm@7315
   303
wenzelm@7391
   304
\indexisaratt{simplify}\indexisaratt{asm-simplify}
wenzelm@7391
   305
\indexisaratt{full-simplify}\indexisaratt{asm-full-simplify}
wenzelm@7315
   306
\begin{matharray}{rcl}
wenzelm@7315
   307
  simplify & : & \isaratt \\
wenzelm@7315
   308
  asm_simplify & : & \isaratt \\
wenzelm@7315
   309
  full_simplify & : & \isaratt \\
wenzelm@7315
   310
  asm_full_simplify & : & \isaratt \\
wenzelm@7315
   311
\end{matharray}
wenzelm@7315
   312
wenzelm@7321
   313
These attributes provide forward rules for simplification, which should be
wenzelm@7335
   314
used only very rarely.  See the ML functions of the same name in
wenzelm@7321
   315
\cite[\S10]{isabelle-ref} for more information.
wenzelm@7315
   316
wenzelm@7315
   317
wenzelm@7135
   318
\section{The Classical Reasoner}
wenzelm@7135
   319
wenzelm@7335
   320
\subsection{Basic methods}\label{sec:classical-basic}
wenzelm@7321
   321
wenzelm@7321
   322
\indexisarmeth{rule}\indexisarmeth{default}\indexisarmeth{contradiction}
wenzelm@7321
   323
\begin{matharray}{rcl}
wenzelm@7321
   324
  rule & : & \isarmeth \\
wenzelm@7321
   325
  intro & : & \isarmeth \\
wenzelm@7321
   326
  elim & : & \isarmeth \\
wenzelm@7321
   327
  contradiction & : & \isarmeth \\
wenzelm@7321
   328
\end{matharray}
wenzelm@7321
   329
wenzelm@7321
   330
\begin{rail}
wenzelm@7321
   331
  ('rule' | 'intro' | 'elim') thmrefs
wenzelm@7321
   332
  ;
wenzelm@7321
   333
\end{rail}
wenzelm@7321
   334
wenzelm@7321
   335
\begin{descr}
wenzelm@7466
   336
\item [$rule$] as offered by the classical reasoner is a refinement over the
wenzelm@7466
   337
  primitive one (see \S\ref{sec:pure-meth}).  In the case that no rules are
wenzelm@7466
   338
  provided as arguments, it automatically determines elimination and
wenzelm@7321
   339
  introduction rules from the context (see also \S\ref{sec:classical-mod}).
wenzelm@7335
   340
  In that form it is the default method for basic proof steps, such as
wenzelm@7335
   341
  $\PROOFNAME$ and ``$\DDOT$'' (two dots).
wenzelm@7321
   342
  
wenzelm@7466
   343
\item [$intro$ and $elim$] repeatedly refine some goal by intro- or
wenzelm@7321
   344
  elim-resolution, after having inserted the facts.  Omitting the arguments
wenzelm@7321
   345
  refers to any suitable rules from the context, otherwise only the explicitly
wenzelm@7335
   346
  given ones may be applied.  The latter form admits better control of what
wenzelm@7335
   347
  actually happens, thus it is very appropriate as an initial method for
wenzelm@7335
   348
  $\PROOFNAME$ that splits up certain connectives of the goal, before entering
wenzelm@7335
   349
  the sub-proof.
wenzelm@7458
   350
  
wenzelm@7466
   351
\item [$contradiction$] solves some goal by contradiction, deriving any result
wenzelm@7466
   352
  from both $\neg A$ and $A$.  Facts, which are guaranteed to participate, may
wenzelm@7466
   353
  appear in either order.
wenzelm@7321
   354
\end{descr}
wenzelm@7321
   355
wenzelm@7321
   356
wenzelm@7321
   357
\subsection{Automatic methods}\label{sec:classical-auto}
wenzelm@7315
   358
wenzelm@7321
   359
\indexisarmeth{blast}
wenzelm@7391
   360
\indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{slow}\indexisarmeth{slow-best}
wenzelm@7321
   361
\begin{matharray}{rcl}
wenzelm@7321
   362
 blast & : & \isarmeth \\
wenzelm@7321
   363
 fast & : & \isarmeth \\
wenzelm@7321
   364
 best & : & \isarmeth \\
wenzelm@7321
   365
 slow & : & \isarmeth \\
wenzelm@7321
   366
 slow_best & : & \isarmeth \\
wenzelm@7321
   367
\end{matharray}
wenzelm@7321
   368
wenzelm@7321
   369
\railalias{slowbest}{slow\_best}
wenzelm@7321
   370
\railterm{slowbest}
wenzelm@7321
   371
wenzelm@7321
   372
\begin{rail}
wenzelm@7321
   373
  'blast' nat? (clamod * )
wenzelm@7321
   374
  ;
wenzelm@7321
   375
  ('fast' | 'best' | 'slow' | slowbest) (clamod * )
wenzelm@7321
   376
  ;
wenzelm@7321
   377
wenzelm@7321
   378
  clamod: (('intro' | 'elim' | 'dest') (() | '!' | '!!') | 'del') ':' thmrefs
wenzelm@7321
   379
  ;
wenzelm@7321
   380
\end{rail}
wenzelm@7321
   381
wenzelm@7321
   382
\begin{descr}
wenzelm@7321
   383
\item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac}
wenzelm@7335
   384
  in \cite[\S11]{isabelle-ref}).  The optional argument specifies a
wenzelm@7321
   385
  user-supplied search bound (default 20).
wenzelm@7321
   386
\item [$fast$, $best$, $slow$, $slow_best$] refer to the generic classical
wenzelm@7335
   387
  reasoner (see \cite[\S11]{isabelle-ref}, tactic \texttt{fast_tac} etc).
wenzelm@7321
   388
\end{descr}
wenzelm@7321
   389
wenzelm@7321
   390
Any of above methods support additional modifiers of the context of classical
wenzelm@7321
   391
rules.  There semantics is analogous to the attributes given in
wenzelm@7321
   392
\S\ref{sec:classical-mod}.
wenzelm@7321
   393
wenzelm@7315
   394
wenzelm@7315
   395
\subsection{Combined automatic methods}
wenzelm@7315
   396
wenzelm@7321
   397
\indexisarmeth{auto}\indexisarmeth{force}
wenzelm@7321
   398
\begin{matharray}{rcl}
wenzelm@7321
   399
  force & : & \isarmeth \\
wenzelm@7321
   400
  auto & : & \isarmeth \\
wenzelm@7321
   401
\end{matharray}
wenzelm@7321
   402
wenzelm@7321
   403
\begin{rail}
wenzelm@7321
   404
  ('force' | 'auto') (clasimpmod * )
wenzelm@7321
   405
  ;
wenzelm@7315
   406
wenzelm@7321
   407
  clasimpmod: ('simp' ('add' | 'del' | 'only') | other |
wenzelm@7321
   408
    (('intro' | 'elim' | 'dest') (() | '!' | '!!') | 'del')) ':' thmrefs
wenzelm@7321
   409
\end{rail}
wenzelm@7315
   410
wenzelm@7321
   411
\begin{descr}
wenzelm@7321
   412
\item [$force$ and $auto$] provide access to Isabelle's combined
wenzelm@7321
   413
  simplification and classical reasoning tactics.  See \texttt{force_tac} and
wenzelm@7321
   414
  \texttt{auto_tac} in \cite[\S11]{isabelle-ref} for more information.  The
wenzelm@7321
   415
  modifier arguments correspond to those given in \S\ref{sec:simp} and
wenzelm@7335
   416
  \S\ref{sec:classical-auto}.  Note that the ones related to the Simplifier
wenzelm@7335
   417
  are prefixed by \railtoken{simp} here.
wenzelm@7321
   418
\end{descr}
wenzelm@7321
   419
wenzelm@7321
   420
\subsection{Modifying the context}\label{sec:classical-mod}
wenzelm@7135
   421
wenzelm@7391
   422
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
wenzelm@7391
   423
\indexisaratt{iff}\indexisaratt{delrule}
wenzelm@7321
   424
\begin{matharray}{rcl}
wenzelm@7321
   425
  intro & : & \isaratt \\
wenzelm@7321
   426
  elim & : & \isaratt \\
wenzelm@7321
   427
  dest & : & \isaratt \\
wenzelm@7391
   428
  iff & : & \isaratt \\
wenzelm@7321
   429
  delrule & : & \isaratt \\
wenzelm@7321
   430
\end{matharray}
wenzelm@7135
   431
wenzelm@7321
   432
\begin{rail}
wenzelm@7321
   433
  ('intro' | 'elim' | 'dest') (() | '!' | '!!')
wenzelm@7321
   434
  ;
wenzelm@7321
   435
\end{rail}
wenzelm@7135
   436
wenzelm@7321
   437
\begin{descr}
wenzelm@7335
   438
\item [$intro$, $elim$, $dest$] add introduction, elimination, destruct rules,
wenzelm@7335
   439
  respectively.  By default, rules are considered as \emph{safe}, while a
wenzelm@7335
   440
  single ``!'' classifies as \emph{unsafe}, and ``!!'' as \emph{extra} (i.e.\ 
wenzelm@7466
   441
  not applied in the search-oriented automatic methods, but only $rule$).
wenzelm@7335
   442
  
wenzelm@7391
   443
\item [$iff$] declares equations both as rewrite rules for the simplifier and
wenzelm@7391
   444
  classical reasoning rules.
wenzelm@7391
   445
wenzelm@7335
   446
\item [$delrule$] deletes introduction or elimination rules from the context.
wenzelm@7335
   447
  Note that destruction rules would have to be turned into elimination rules
wenzelm@7321
   448
  first, e.g.\ by using the $elimify$ attribute.
wenzelm@7321
   449
\end{descr}
wenzelm@7135
   450
wenzelm@7135
   451
wenzelm@7135
   452
%%% Local Variables: 
wenzelm@7135
   453
%%% mode: latex
wenzelm@7135
   454
%%% TeX-master: "isar-ref"
wenzelm@7135
   455
%%% End: