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