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