doc-src/IsarRef/generic.tex
author wenzelm
Thu Sep 07 21:06:55 2000 +0200 (2000-09-07)
changeset 9905 14a71104a498
parent 9847 32ce11c3f6b1
child 9936 f080397656d8
permissions -rw-r--r--
improved att names;
wenzelm@7135
     1
wenzelm@7167
     2
\chapter{Generic Tools and Packages}\label{ch:gen-tools}
wenzelm@7167
     3
wenzelm@8517
     4
\section{Axiomatic Type Classes}\label{sec:axclass}
wenzelm@7167
     5
wenzelm@8904
     6
%FIXME
wenzelm@8904
     7
% - qualified names
wenzelm@8904
     8
% - class intro rules;
wenzelm@8904
     9
% - class axioms;
wenzelm@8904
    10
wenzelm@8517
    11
\indexisarcmd{axclass}\indexisarcmd{instance}\indexisarmeth{intro-classes}
wenzelm@7167
    12
\begin{matharray}{rcl}
wenzelm@8517
    13
  \isarcmd{axclass} & : & \isartrans{theory}{theory} \\
wenzelm@8517
    14
  \isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
wenzelm@8517
    15
  intro_classes & : & \isarmeth \\
wenzelm@7167
    16
\end{matharray}
wenzelm@7167
    17
wenzelm@8517
    18
Axiomatic type classes are provided by Isabelle/Pure as a \emph{definitional}
wenzelm@8517
    19
interface to type classes (cf.~\S\ref{sec:classes}).  Thus any object logic
wenzelm@8547
    20
may make use of this light-weight mechanism of abstract theories
wenzelm@8901
    21
\cite{Wenzel:1997:TPHOL}.  There is also a tutorial on using axiomatic type
wenzelm@8901
    22
classes in isabelle \cite{isabelle-axclass} that is part of the standard
wenzelm@8901
    23
Isabelle documentation.
wenzelm@8517
    24
wenzelm@7167
    25
\begin{rail}
wenzelm@8517
    26
  'axclass' classdecl (axmdecl prop comment? +)
wenzelm@8517
    27
  ;
wenzelm@8517
    28
  'instance' (nameref '<' nameref | nameref '::' simplearity) comment?
wenzelm@7167
    29
  ;
wenzelm@7167
    30
\end{rail}
wenzelm@7167
    31
wenzelm@7167
    32
\begin{descr}
wenzelm@8517
    33
\item [$\isarkeyword{axclass}~c < \vec c~axms$] defines an axiomatic type
wenzelm@8517
    34
  class as the intersection of existing classes, with additional axioms
wenzelm@8517
    35
  holding.  Class axioms may not contain more than one type variable.  The
wenzelm@8517
    36
  class axioms (with implicit sort constraints added) are bound to the given
wenzelm@8517
    37
  names.  Furthermore a class introduction rule is generated, which is
wenzelm@8517
    38
  employed by method $intro_classes$ to support instantiation proofs of this
wenzelm@8517
    39
  class.
wenzelm@9614
    40
wenzelm@8517
    41
\item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~t ::
wenzelm@8547
    42
  (\vec s)c$] setup a goal stating a class relation or type arity.  The proof
wenzelm@8547
    43
  would usually proceed by $intro_classes$, and then establish the
wenzelm@8517
    44
  characteristic theorems of the type classes involved.  After finishing the
wenzelm@8517
    45
  proof, the theory will be augmented by a type signature declaration
wenzelm@8517
    46
  corresponding to the resulting theorem.
wenzelm@8517
    47
\item [$intro_classes$] repeatedly expands all class introduction rules of
wenzelm@8517
    48
  this theory.
wenzelm@7167
    49
\end{descr}
wenzelm@7167
    50
wenzelm@7315
    51
wenzelm@7315
    52
\section{Calculational proof}\label{sec:calculation}
wenzelm@7315
    53
wenzelm@8619
    54
\indexisarcmd{also}\indexisarcmd{finally}
wenzelm@8619
    55
\indexisarcmd{moreover}\indexisarcmd{ultimately}
wenzelm@9606
    56
\indexisarcmd{print-trans-rules}\indexisaratt{trans}
wenzelm@7315
    57
\begin{matharray}{rcl}
wenzelm@7315
    58
  \isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7315
    59
  \isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\
wenzelm@8619
    60
  \isarcmd{moreover} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@8619
    61
  \isarcmd{ultimately} & : & \isartrans{proof(state)}{proof(chain)} \\
wenzelm@9606
    62
  \isarcmd{print_trans_rules} & : & \isarkeep{theory~|~proof} \\
wenzelm@7315
    63
  trans & : & \isaratt \\
wenzelm@7315
    64
\end{matharray}
wenzelm@7315
    65
wenzelm@7315
    66
Calculational proof is forward reasoning with implicit application of
wenzelm@7315
    67
transitivity rules (such those of $=$, $\le$, $<$).  Isabelle/Isar maintains
wenzelm@7391
    68
an auxiliary register $calculation$\indexisarthm{calculation} for accumulating
wenzelm@7897
    69
results obtained by transitivity composed with the current result.  Command
wenzelm@7897
    70
$\ALSO$ updates $calculation$ involving $this$, while $\FINALLY$ exhibits the
wenzelm@7897
    71
final $calculation$ by forward chaining towards the next goal statement.  Both
wenzelm@7897
    72
commands require valid current facts, i.e.\ may occur only after commands that
wenzelm@7897
    73
produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or some finished proof of
wenzelm@8619
    74
$\HAVENAME$, $\SHOWNAME$ etc.  The $\MOREOVER$ and $\ULTIMATELY$ commands are
wenzelm@8619
    75
similar to $\ALSO$ and $\FINALLY$, but only collect further results in
wenzelm@8619
    76
$calculation$ without applying any rules yet.
wenzelm@7315
    77
wenzelm@7315
    78
Also note that the automatic term abbreviation ``$\dots$'' has its canonical
wenzelm@8619
    79
application with calculational proofs.  It refers to the argument\footnote{The
wenzelm@8619
    80
  argument of a curried infix expression is its right-hand side.} of the
wenzelm@8619
    81
preceding statement.
wenzelm@7315
    82
wenzelm@7315
    83
Isabelle/Isar calculations are implicitly subject to block structure in the
wenzelm@7315
    84
sense that new threads of calculational reasoning are commenced for any new
wenzelm@7315
    85
block (as opened by a local goal, for example).  This means that, apart from
wenzelm@7315
    86
being able to nest calculations, there is no separate \emph{begin-calculation}
wenzelm@7315
    87
command required.
wenzelm@7315
    88
wenzelm@8619
    89
\medskip
wenzelm@8619
    90
wenzelm@8619
    91
The Isar calculation proof commands may be defined as
wenzelm@8619
    92
follows:\footnote{Internal bookkeeping such as proper handling of
wenzelm@8619
    93
  block-structure has been suppressed.}
wenzelm@8619
    94
\begin{matharray}{rcl}
wenzelm@8619
    95
  \ALSO@0 & \equiv & \NOTE{calculation}{this} \\
wenzelm@9606
    96
  \ALSO@{n+1} & \equiv & \NOTE{calculation}{trans~[OF~calculation~this]} \\[0.5ex]
wenzelm@8619
    97
  \FINALLY & \equiv & \ALSO~\FROM{calculation} \\
wenzelm@8619
    98
  \MOREOVER & \equiv & \NOTE{calculation}{calculation~this} \\
wenzelm@8619
    99
  \ULTIMATELY & \equiv & \MOREOVER~\FROM{calculation} \\
wenzelm@8619
   100
\end{matharray}
wenzelm@8619
   101
wenzelm@7315
   102
\begin{rail}
wenzelm@7315
   103
  ('also' | 'finally') transrules? comment?
wenzelm@7315
   104
  ;
wenzelm@8619
   105
  ('moreover' | 'ultimately') comment?
wenzelm@8619
   106
  ;
wenzelm@8507
   107
  'trans' (() | 'add' | 'del')
wenzelm@7315
   108
  ;
wenzelm@7315
   109
wenzelm@7315
   110
  transrules: '(' thmrefs ')' interest?
wenzelm@7315
   111
  ;
wenzelm@7315
   112
\end{rail}
wenzelm@7315
   113
wenzelm@7315
   114
\begin{descr}
wenzelm@8547
   115
\item [$\ALSO~(\vec a)$] maintains the auxiliary $calculation$ register as
wenzelm@7315
   116
  follows.  The first occurrence of $\ALSO$ in some calculational thread
wenzelm@7905
   117
  initializes $calculation$ by $this$. Any subsequent $\ALSO$ on the same
wenzelm@7335
   118
  level of block-structure updates $calculation$ by some transitivity rule
wenzelm@7458
   119
  applied to $calculation$ and $this$ (in that order).  Transitivity rules are
wenzelm@8547
   120
  picked from the current context plus those given as explicit arguments (the
wenzelm@8547
   121
  latter have precedence).
wenzelm@9614
   122
wenzelm@8547
   123
\item [$\FINALLY~(\vec a)$] maintaining $calculation$ in the same way as
wenzelm@7315
   124
  $\ALSO$, and concludes the current calculational thread.  The final result
wenzelm@7315
   125
  is exhibited as fact for forward chaining towards the next goal. Basically,
wenzelm@7987
   126
  $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$.  Note that
wenzelm@7987
   127
  ``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and
wenzelm@7987
   128
  ``$\FINALLY~\HAVE{}{\phi}~\DOT$'' are typical idioms for concluding
wenzelm@7987
   129
  calculational proofs.
wenzelm@9614
   130
wenzelm@8619
   131
\item [$\MOREOVER$ and $\ULTIMATELY$] are analogous to $\ALSO$ and $\FINALLY$,
wenzelm@8619
   132
  but collect results only, without applying rules.
wenzelm@9614
   133
wenzelm@9606
   134
\item [$\isarkeyword{print_trans_rules}$] prints the list of transitivity
wenzelm@9606
   135
  rules declared in the current context.
wenzelm@9614
   136
wenzelm@8547
   137
\item [$trans$] declares theorems as transitivity rules.
wenzelm@9614
   138
wenzelm@7315
   139
\end{descr}
wenzelm@7315
   140
wenzelm@7315
   141
wenzelm@8483
   142
\section{Named local contexts (cases)}\label{sec:cases}
wenzelm@8483
   143
wenzelm@8483
   144
\indexisarcmd{case}\indexisarcmd{print-cases}
wenzelm@8483
   145
\indexisaratt{case-names}\indexisaratt{params}
wenzelm@8483
   146
\begin{matharray}{rcl}
wenzelm@8483
   147
  \isarcmd{case} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@8517
   148
  \isarcmd{print_cases}^* & : & \isarkeep{proof} \\
wenzelm@8483
   149
  case_names & : & \isaratt \\
wenzelm@8483
   150
  params & : & \isaratt \\
wenzelm@8483
   151
\end{matharray}
wenzelm@8483
   152
wenzelm@8483
   153
Basically, Isar proof contexts are built up explicitly using commands like
wenzelm@8483
   154
$\FIXNAME$, $\ASSUMENAME$ etc.\ (see \S\ref{sec:proof-context}).  In typical
wenzelm@8483
   155
verification tasks this can become hard to manage, though.  In particular, a
wenzelm@8483
   156
large number of local contexts may emerge from case analysis or induction over
wenzelm@8483
   157
inductive sets and types.
wenzelm@8483
   158
wenzelm@8483
   159
\medskip
wenzelm@8483
   160
wenzelm@8483
   161
The $\CASENAME$ command provides a shorthand to refer to certain parts of
wenzelm@8483
   162
logical context symbolically.  Proof methods may provide an environment of
wenzelm@8507
   163
named ``cases'' of the form $c\colon \vec x, \vec \phi$.  Then the effect of
wenzelm@8507
   164
$\CASE{c}$ is exactly the same as $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$.
wenzelm@8483
   165
wenzelm@8483
   166
It is important to note that $\CASENAME$ does \emph{not} provide any means to
wenzelm@8483
   167
peek at the current goal state, which is treated as strictly non-observable in
wenzelm@8483
   168
Isar!  Instead, the cases considered here usually emerge in a canonical way
wenzelm@8483
   169
from certain pieces of specification that appear in the theory somewhere else
wenzelm@8483
   170
(e.g.\ in an inductive definition, or recursive function).  See also
wenzelm@8483
   171
\S\ref{sec:induct-method} for more details of how this works in HOL.
wenzelm@8483
   172
wenzelm@8483
   173
\medskip
wenzelm@8483
   174
wenzelm@8483
   175
Named cases may be exhibited in the current proof context only if both the
wenzelm@8547
   176
proof method and the rules involved support this.  Case names and parameters
wenzelm@8547
   177
of basic rules may be declared by hand as well, by using appropriate
wenzelm@8547
   178
attributes.  Thus variant versions of rules that have been derived manually
wenzelm@8547
   179
may be used in advanced case analysis later.
wenzelm@8483
   180
wenzelm@8483
   181
\railalias{casenames}{case\_names}
wenzelm@8483
   182
\railterm{casenames}
wenzelm@8483
   183
wenzelm@8483
   184
\begin{rail}
wenzelm@8483
   185
  'case' nameref attributes?
wenzelm@8483
   186
  ;
wenzelm@8483
   187
  casenames (name + )
wenzelm@8483
   188
  ;
wenzelm@8483
   189
  'params' ((name * ) + 'and')
wenzelm@8483
   190
  ;
wenzelm@8483
   191
\end{rail}
wenzelm@8547
   192
%FIXME bug in rail
wenzelm@8483
   193
wenzelm@8483
   194
\begin{descr}
wenzelm@8507
   195
\item [$\CASE{c}$] invokes a named local context $c\colon \vec x, \vec \phi$,
wenzelm@8547
   196
  as provided by an appropriate proof method (such as $cases$ and $induct$ in
wenzelm@8547
   197
  Isabelle/HOL, see \S\ref{sec:induct-method}).  The command $\CASE{c}$
wenzelm@8547
   198
  abbreviates $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$.
wenzelm@8483
   199
\item [$\isarkeyword{print_cases}$] prints all local contexts of the current
wenzelm@8547
   200
  state, using Isar proof language notation.  This is a diagnostic command;
wenzelm@8547
   201
  $undo$ does not apply.
wenzelm@8483
   202
\item [$case_names~\vec c$] declares names for the local contexts of premises
wenzelm@8547
   203
  of some theorem; $\vec c$ refers to the \emph{suffix} of the list premises.
wenzelm@8483
   204
\item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of
wenzelm@8547
   205
  premises $1, \dots, n$ of some theorem.  An empty list of names may be given
wenzelm@8547
   206
  to skip positions, leaving the present parameters unchanged.
wenzelm@9614
   207
wenzelm@9614
   208
  Note that the default usage of case rules does \emph{not} directly expose
wenzelm@9614
   209
  parameters to the proof context (see also \S\ref{sec:induct-method-proper}).
wenzelm@8483
   210
\end{descr}
wenzelm@8483
   211
wenzelm@8483
   212
wenzelm@9614
   213
\section{Generalized existence}\label{sec:obtain}
wenzelm@7135
   214
wenzelm@8517
   215
\indexisarcmd{obtain}
wenzelm@7135
   216
\begin{matharray}{rcl}
wenzelm@9480
   217
  \isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\
wenzelm@8517
   218
\end{matharray}
wenzelm@8517
   219
wenzelm@9480
   220
Generalized existence means that additional elements with certain properties
wenzelm@9480
   221
may introduced in the current context.  Technically, the $\OBTAINNAME$
wenzelm@9480
   222
language element is like a declaration of $\FIXNAME$ and $\ASSUMENAME$ (see
wenzelm@9480
   223
also see \S\ref{sec:proof-context}), together with a soundness proof of its
wenzelm@9480
   224
additional claim.  According to the nature of existential reasoning,
wenzelm@9480
   225
assumptions get eliminated from any result exported from the context later,
wenzelm@9480
   226
provided that the corresponding parameters do \emph{not} occur in the
wenzelm@9480
   227
conclusion.
wenzelm@8517
   228
wenzelm@8517
   229
\begin{rail}
wenzelm@8517
   230
  'obtain' (vars + 'and') comment? \\ 'where' (assm comment? + 'and')
wenzelm@8517
   231
  ;
wenzelm@8517
   232
\end{rail}
wenzelm@8517
   233
wenzelm@9480
   234
$\OBTAINNAME$ is defined as a derived Isar command as follows, where $\vec b$
wenzelm@9480
   235
shall refer to (optional) facts indicated for forward chaining.
wenzelm@8517
   236
\begin{matharray}{l}
wenzelm@9480
   237
  \langle facts~\vec b\rangle \\
wenzelm@9480
   238
  \OBTAIN{\vec x}{a}{\vec \phi}~~\langle proof\rangle \equiv {} \\[1ex]
wenzelm@9480
   239
  \quad \BG \\
wenzelm@9480
   240
  \qquad \FIX{thesis} \\
wenzelm@9480
   241
  \qquad \ASSUME{that [simp, intro]}{\All{\vec x} \vec\phi \Imp thesis} \\
wenzelm@9480
   242
  \qquad \FROM{\vec b}~\HAVE{}{thesis}~~\langle proof\rangle \\
wenzelm@9480
   243
  \quad \EN \\
wenzelm@9606
   244
  \quad \FIX{\vec x}~\ASSUMENAME^{\ast}~{a}~{\vec\phi} \\
wenzelm@7135
   245
\end{matharray}
wenzelm@7135
   246
wenzelm@8517
   247
Typically, the soundness proof is relatively straight-forward, often just by
wenzelm@8517
   248
canonical automated tools such as $\BY{simp}$ (see \S\ref{sec:simp}) or
wenzelm@9480
   249
$\BY{blast}$ (see \S\ref{sec:classical-auto}).  Accordingly, the ``$that$''
wenzelm@9480
   250
reduction above is declared as simplification and introduction rule.
wenzelm@8517
   251
wenzelm@8517
   252
\medskip
wenzelm@8517
   253
wenzelm@8517
   254
In a sense, $\OBTAINNAME$ represents at the level of Isar proofs what would be
wenzelm@8517
   255
meta-logical existential quantifiers and conjunctions.  This concept has a
wenzelm@8517
   256
broad range of useful applications, ranging from plain elimination (or even
wenzelm@8517
   257
introduction) of object-level existentials and conjunctions, to elimination
wenzelm@8517
   258
over results of symbolic evaluation of recursive definitions, for example.
wenzelm@9480
   259
Also note that $\OBTAINNAME$ without parameters acts much like $\HAVENAME$,
wenzelm@9480
   260
where the result is treated as an assumption.
wenzelm@8517
   261
wenzelm@8517
   262
wenzelm@8517
   263
\section{Miscellaneous methods and attributes}
wenzelm@8517
   264
wenzelm@9606
   265
\indexisarmeth{unfold}\indexisarmeth{fold}\indexisarmeth{insert}
wenzelm@8517
   266
\indexisarmeth{erule}\indexisarmeth{drule}\indexisarmeth{frule}
wenzelm@8517
   267
\indexisarmeth{fail}\indexisarmeth{succeed}
wenzelm@8517
   268
\begin{matharray}{rcl}
wenzelm@8517
   269
  unfold & : & \isarmeth \\
wenzelm@8517
   270
  fold & : & \isarmeth \\[0.5ex]
wenzelm@9606
   271
  insert^* & : & \isarmeth \\[0.5ex]
wenzelm@8517
   272
  erule^* & : & \isarmeth \\
wenzelm@8517
   273
  drule^* & : & \isarmeth \\
wenzelm@8517
   274
  frule^* & : & \isarmeth \\[0.5ex]
wenzelm@8517
   275
  succeed & : & \isarmeth \\
wenzelm@8517
   276
  fail & : & \isarmeth \\
wenzelm@8517
   277
\end{matharray}
wenzelm@7135
   278
wenzelm@7135
   279
\begin{rail}
wenzelm@9606
   280
  ('fold' | 'unfold' | 'insert' | 'erule' | 'drule' | 'frule') thmrefs
wenzelm@7135
   281
  ;
wenzelm@7135
   282
\end{rail}
wenzelm@7135
   283
wenzelm@7167
   284
\begin{descr}
wenzelm@8547
   285
\item [$unfold~\vec a$ and $fold~\vec a$] expand and fold back again the given
wenzelm@8517
   286
  meta-level definitions throughout all goals; any facts provided are inserted
wenzelm@8517
   287
  into the goal and subject to rewriting as well.
wenzelm@8547
   288
\item [$erule~\vec a$, $drule~\vec a$, and $frule~\vec a$] are similar to the
wenzelm@8547
   289
  basic $rule$ method (see \S\ref{sec:pure-meth-att}), but apply rules by
wenzelm@8517
   290
  elim-resolution, destruct-resolution, and forward-resolution, respectively
wenzelm@8517
   291
  \cite{isabelle-ref}.  These are improper method, mainly for experimentation
wenzelm@8517
   292
  and emulating tactic scripts.
wenzelm@9614
   293
wenzelm@8517
   294
  Different modes of basic rule application are usually expressed in Isar at
wenzelm@8517
   295
  the proof language level, rather than via implicit proof state
wenzelm@8547
   296
  manipulations.  For example, a proper single-step elimination would be done
wenzelm@8517
   297
  using the basic $rule$ method, with forward chaining of current facts.
wenzelm@9606
   298
\item [$insert~\vec a$] inserts theorems as facts into all goals of the proof
wenzelm@9606
   299
  state.  Note that current facts indicated for forward chaining are ignored.
wenzelm@8517
   300
\item [$succeed$] yields a single (unchanged) result; it is the identity of
wenzelm@8517
   301
  the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
wenzelm@8517
   302
\item [$fail$] yields an empty result sequence; it is the identity of the
wenzelm@8517
   303
  ``\texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
wenzelm@7167
   304
\end{descr}
wenzelm@7135
   305
wenzelm@8517
   306
wenzelm@8517
   307
\indexisaratt{standard}
wenzelm@9905
   308
\indexisaratt{elimified}
wenzelm@9232
   309
\indexisaratt{no-vars}
wenzelm@8517
   310
wenzelm@9614
   311
\indexisaratt{THEN}\indexisaratt{COMP}
wenzelm@9905
   312
\indexisaratt{where}\indexisaratt{tagged}\indexisaratt{untagged}
wenzelm@9905
   313
\indexisaratt{unfolded}\indexisaratt{folded}\indexisaratt{exported}
wenzelm@8517
   314
\begin{matharray}{rcl}
wenzelm@9905
   315
  tagged & : & \isaratt \\
wenzelm@9905
   316
  untagged & : & \isaratt \\[0.5ex]
wenzelm@9614
   317
  THEN & : & \isaratt \\
wenzelm@8517
   318
  COMP & : & \isaratt \\[0.5ex]
wenzelm@8517
   319
  where & : & \isaratt \\[0.5ex]
wenzelm@9905
   320
  unfolded & : & \isaratt \\
wenzelm@9905
   321
  folded & : & \isaratt \\[0.5ex]
wenzelm@8517
   322
  standard & : & \isaratt \\
wenzelm@9905
   323
  elimified & : & \isaratt \\
wenzelm@9232
   324
  no_vars & : & \isaratt \\
wenzelm@9905
   325
  exported^* & : & \isaratt \\
wenzelm@8517
   326
\end{matharray}
wenzelm@8517
   327
wenzelm@8517
   328
\begin{rail}
wenzelm@9905
   329
  'tagged' (nameref+)
wenzelm@8517
   330
  ;
wenzelm@9905
   331
  'untagged' name
wenzelm@8517
   332
  ;
wenzelm@9614
   333
  ('THEN' | 'COMP') nat? thmref
wenzelm@8517
   334
  ;
wenzelm@8517
   335
  'where' (name '=' term * 'and')
wenzelm@8517
   336
  ;
wenzelm@9905
   337
  ('unfolded' | 'folded') thmrefs
wenzelm@8517
   338
  ;
wenzelm@8517
   339
\end{rail}
wenzelm@8517
   340
wenzelm@8517
   341
\begin{descr}
wenzelm@9905
   342
\item [$tagged~name~args$ and $untagged~name$] add and remove $tags$ of some
wenzelm@8517
   343
  theorem.  Tags may be any list of strings that serve as comment for some
wenzelm@8517
   344
  tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the
wenzelm@8517
   345
  result).  The first string is considered the tag name, the rest its
wenzelm@8517
   346
  arguments.  Note that untag removes any tags of the same name.
wenzelm@9614
   347
\item [$THEN~n~a$ and $COMP~n~a$] compose rules.  $THEN$ resolves with the
wenzelm@9614
   348
  $n$-th premise of $a$; the $COMP$ version skips the automatic lifting
wenzelm@8547
   349
  process that is normally intended (cf.\ \texttt{RS} and \texttt{COMP} in
wenzelm@8547
   350
  \cite[\S5]{isabelle-ref}).
wenzelm@8517
   351
\item [$where~\vec x = \vec t$] perform named instantiation of schematic
wenzelm@9606
   352
  variables occurring in a theorem.  Unlike instantiation tactics such as
wenzelm@9606
   353
  $rule_tac$ (see \S\ref{sec:tactic-commands}), actual schematic variables
wenzelm@8517
   354
  have to be specified (e.g.\ $\Var{x@3}$).
wenzelm@9905
   355
\item [$unfolded~\vec a$ and $folded~\vec a$] expand and fold back again the
wenzelm@9905
   356
  given meta-level definitions throughout a rule.
wenzelm@8517
   357
\item [$standard$] puts a theorem into the standard form of object-rules, just
wenzelm@8517
   358
  as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).
wenzelm@9905
   359
\item [$elimified$] turns an destruction rule into an elimination, just as the
wenzelm@8517
   360
  ML function \texttt{make\_elim} (see \cite{isabelle-ref}).
wenzelm@9232
   361
\item [$no_vars$] replaces schematic variables by free ones; this is mainly
wenzelm@9232
   362
  for tuning output of pretty printed theorems.
wenzelm@9905
   363
\item [$exported$] lifts a local result out of the current proof context,
wenzelm@8517
   364
  generalizing all fixed variables and discharging all assumptions.  Note that
wenzelm@8547
   365
  proper incremental export is already done as part of the basic Isar
wenzelm@8547
   366
  machinery.  This attribute is mainly for experimentation.
wenzelm@8517
   367
\end{descr}
wenzelm@7135
   368
wenzelm@7135
   369
wenzelm@9606
   370
\section{Tactic emulations}\label{sec:tactics}
wenzelm@9606
   371
wenzelm@9606
   372
The following improper proof methods emulate traditional tactics.  These admit
wenzelm@9606
   373
direct access to the goal state, which is normally considered harmful!  In
wenzelm@9606
   374
particular, this may involve both numbered goal addressing (default 1), and
wenzelm@9606
   375
dynamic instantiation within the scope of some subgoal.
wenzelm@9606
   376
wenzelm@9606
   377
\begin{warn}
wenzelm@9606
   378
  Dynamic instantiations are read and type-checked according to a subgoal of
wenzelm@9606
   379
  the current dynamic goal state, rather than the static proof context!  In
wenzelm@9606
   380
  particular, locally fixed variables and term abbreviations may not be
wenzelm@9606
   381
  included in the term specifications.  Thus schematic variables are left to
wenzelm@9606
   382
  be solved by unification with certain parts of the subgoal involved.
wenzelm@9606
   383
\end{warn}
wenzelm@9606
   384
wenzelm@9606
   385
Note that the tactic emulation proof methods in Isabelle/Isar are consistently
wenzelm@9606
   386
named $foo_tac$.
wenzelm@9606
   387
wenzelm@9606
   388
\indexisarmeth{rule-tac}\indexisarmeth{erule-tac}
wenzelm@9606
   389
\indexisarmeth{drule-tac}\indexisarmeth{frule-tac}
wenzelm@9606
   390
\indexisarmeth{cut-tac}\indexisarmeth{thin-tac}
wenzelm@9642
   391
\indexisarmeth{subgoal-tac}\indexisarmeth{rename-tac}
wenzelm@9614
   392
\indexisarmeth{rotate-tac}\indexisarmeth{tactic}
wenzelm@9606
   393
\begin{matharray}{rcl}
wenzelm@9606
   394
  rule_tac^* & : & \isarmeth \\
wenzelm@9606
   395
  erule_tac^* & : & \isarmeth \\
wenzelm@9606
   396
  drule_tac^* & : & \isarmeth \\
wenzelm@9606
   397
  frule_tac^* & : & \isarmeth \\
wenzelm@9606
   398
  cut_tac^* & : & \isarmeth \\
wenzelm@9606
   399
  thin_tac^* & : & \isarmeth \\
wenzelm@9606
   400
  subgoal_tac^* & : & \isarmeth \\
wenzelm@9614
   401
  rename_tac^* & : & \isarmeth \\
wenzelm@9614
   402
  rotate_tac^* & : & \isarmeth \\
wenzelm@9606
   403
  tactic^* & : & \isarmeth \\
wenzelm@9606
   404
\end{matharray}
wenzelm@9606
   405
wenzelm@9606
   406
\railalias{ruletac}{rule\_tac}
wenzelm@9606
   407
\railterm{ruletac}
wenzelm@9606
   408
wenzelm@9606
   409
\railalias{eruletac}{erule\_tac}
wenzelm@9606
   410
\railterm{eruletac}
wenzelm@9606
   411
wenzelm@9606
   412
\railalias{druletac}{drule\_tac}
wenzelm@9606
   413
\railterm{druletac}
wenzelm@9606
   414
wenzelm@9606
   415
\railalias{fruletac}{frule\_tac}
wenzelm@9606
   416
\railterm{fruletac}
wenzelm@9606
   417
wenzelm@9606
   418
\railalias{cuttac}{cut\_tac}
wenzelm@9606
   419
\railterm{cuttac}
wenzelm@9606
   420
wenzelm@9606
   421
\railalias{thintac}{thin\_tac}
wenzelm@9606
   422
\railterm{thintac}
wenzelm@9606
   423
wenzelm@9606
   424
\railalias{subgoaltac}{subgoal\_tac}
wenzelm@9606
   425
\railterm{subgoaltac}
wenzelm@9606
   426
wenzelm@9614
   427
\railalias{renametac}{rename\_tac}
wenzelm@9614
   428
\railterm{renametac}
wenzelm@9614
   429
wenzelm@9614
   430
\railalias{rotatetac}{rotate\_tac}
wenzelm@9614
   431
\railterm{rotatetac}
wenzelm@9614
   432
wenzelm@9606
   433
\begin{rail}
wenzelm@9606
   434
  ( ruletac | eruletac | druletac | fruletac | cuttac | thintac ) goalspec?
wenzelm@9606
   435
  ( insts thmref | thmrefs )
wenzelm@9606
   436
  ;
wenzelm@9606
   437
  subgoaltac goalspec? (prop +)
wenzelm@9606
   438
  ;
wenzelm@9614
   439
  renametac goalspec? (name +)
wenzelm@9614
   440
  ;
wenzelm@9614
   441
  rotatetac goalspec? int?
wenzelm@9614
   442
  ;
wenzelm@9606
   443
  'tactic' text
wenzelm@9606
   444
  ;
wenzelm@9606
   445
wenzelm@9606
   446
  insts: ((name '=' term) + 'and') 'in'
wenzelm@9606
   447
  ;
wenzelm@9606
   448
\end{rail}
wenzelm@9606
   449
wenzelm@9606
   450
\begin{descr}
wenzelm@9606
   451
\item [$rule_tac$ etc.] do resolution of rules with explicit instantiation.
wenzelm@9606
   452
  This works the same way as the ML tactics \texttt{res_inst_tac} etc. (see
wenzelm@9606
   453
  \cite[\S3]{isabelle-ref}).
wenzelm@9614
   454
wenzelm@9606
   455
  Note that multiple rules may be only given there is no instantiation.  Then
wenzelm@9606
   456
  $rule_tac$ is the same as \texttt{resolve_tac} in ML (see
wenzelm@9606
   457
  \cite[\S3]{isabelle-ref}).
wenzelm@9606
   458
\item [$cut_tac$] inserts facts into the proof state as assumption of a
wenzelm@9606
   459
  subgoal, see also \texttt{cut_facts_tac} in \cite[\S3]{isabelle-ref}.  Note
wenzelm@9606
   460
  that the scope of schmatic variables is spread over the main goal statement.
wenzelm@9606
   461
  Instantiations may be given as well, see also ML tactic
wenzelm@9606
   462
  \texttt{cut_inst_tac} in \cite[\S3]{isabelle-ref}.
wenzelm@9606
   463
\item [$thin_tac~\phi$] deletes the specified assumption from a subgoal; note
wenzelm@9606
   464
  that $\phi$ may contain schematic variables.  See also \texttt{thin_tac} in
wenzelm@9606
   465
  \cite[\S3]{isabelle-ref}.
wenzelm@9606
   466
\item [$subgoal_tac~\phi$] adds $\phi$ as an assumption to a subgoal.  See
wenzelm@9606
   467
  also \texttt{subgoal_tac} and \texttt{subgoals_tac} in
wenzelm@9606
   468
  \cite[\S3]{isabelle-ref}.
wenzelm@9614
   469
\item [$rename_tac~\vec x$] renames parameters of a goal according to the list
wenzelm@9614
   470
  $\vec x$, which refers to the \emph{suffix} of variables.
wenzelm@9614
   471
\item [$rotate_tac~n$] rotates the assumptions of a goal by $n$ positions:
wenzelm@9614
   472
  from right to left if $n$ is positive, and from left to right if $n$ is
wenzelm@9614
   473
  negative; the default value is $1$.  See also \texttt{rotate_tac} in
wenzelm@9614
   474
  \cite[\S3]{isabelle-ref}.
wenzelm@9606
   475
\item [$tactic~text$] produces a proof method from any ML text of type
wenzelm@9606
   476
  \texttt{tactic}.  Apart from the usual ML environment and the current
wenzelm@9606
   477
  implicit theory context, the ML code may refer to the following locally
wenzelm@9606
   478
  bound values:
wenzelm@9606
   479
wenzelm@9606
   480
%%FIXME ttbox produces too much trailing space (why?)
wenzelm@9606
   481
{\footnotesize\begin{verbatim}
wenzelm@9606
   482
val ctxt  : Proof.context
wenzelm@9606
   483
val facts : thm list
wenzelm@9606
   484
val thm   : string -> thm
wenzelm@9606
   485
val thms  : string -> thm list
wenzelm@9606
   486
\end{verbatim}}
wenzelm@9606
   487
  Here \texttt{ctxt} refers to the current proof context, \texttt{facts}
wenzelm@9606
   488
  indicates any current facts for forward-chaining, and
wenzelm@9606
   489
  \texttt{thm}~/~\texttt{thms} retrieve named facts (including global
wenzelm@9606
   490
  theorems) from the context.
wenzelm@9606
   491
\end{descr}
wenzelm@9606
   492
wenzelm@9606
   493
wenzelm@9614
   494
\section{The Simplifier}\label{sec:simplifier}
wenzelm@7135
   495
wenzelm@7321
   496
\subsection{Simplification methods}\label{sec:simp}
wenzelm@7315
   497
wenzelm@8483
   498
\indexisarmeth{simp}\indexisarmeth{simp-all}
wenzelm@7315
   499
\begin{matharray}{rcl}
wenzelm@7315
   500
  simp & : & \isarmeth \\
wenzelm@8483
   501
  simp_all & : & \isarmeth \\
wenzelm@7315
   502
\end{matharray}
wenzelm@7315
   503
wenzelm@8483
   504
\railalias{simpall}{simp\_all}
wenzelm@8483
   505
\railterm{simpall}
wenzelm@8483
   506
wenzelm@8704
   507
\railalias{noasm}{no\_asm}
wenzelm@8704
   508
\railterm{noasm}
wenzelm@8704
   509
wenzelm@8704
   510
\railalias{noasmsimp}{no\_asm\_simp}
wenzelm@8704
   511
\railterm{noasmsimp}
wenzelm@8704
   512
wenzelm@8704
   513
\railalias{noasmuse}{no\_asm\_use}
wenzelm@8704
   514
\railterm{noasmuse}
wenzelm@8704
   515
wenzelm@7315
   516
\begin{rail}
wenzelm@8706
   517
  ('simp' | simpall) ('!' ?) opt? (simpmod * )
wenzelm@7315
   518
  ;
wenzelm@7315
   519
wenzelm@8811
   520
  opt: '(' (noasm | noasmsimp | noasmuse) ')'
wenzelm@8704
   521
  ;
wenzelm@9711
   522
  simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
wenzelm@9847
   523
    'split' (() | 'add' | 'del')) ':' thmrefs
wenzelm@7315
   524
  ;
wenzelm@7315
   525
\end{rail}
wenzelm@7315
   526
wenzelm@7321
   527
\begin{descr}
wenzelm@8547
   528
\item [$simp$] invokes Isabelle's simplifier, after declaring additional rules
wenzelm@8594
   529
  according to the arguments given.  Note that the \railtterm{only} modifier
wenzelm@8547
   530
  first removes all other rewrite rules, congruences, and looper tactics
wenzelm@8594
   531
  (including splits), and then behaves like \railtterm{add}.
wenzelm@9711
   532
  
wenzelm@9711
   533
  \medskip The \railtterm{cong} modifiers add or delete Simplifier congruence
wenzelm@9711
   534
  rules (see also \cite{isabelle-ref}), the default is to add.
wenzelm@9711
   535
  
wenzelm@9711
   536
  \medskip The \railtterm{split} modifiers add or delete rules for the
wenzelm@9711
   537
  Splitter (see also \cite{isabelle-ref}), the default is to add.  This works
wenzelm@9711
   538
  only if the Simplifier method has been properly setup to include the
wenzelm@9711
   539
  Splitter (all major object logics such HOL, HOLCF, FOL, ZF do this already).
wenzelm@8483
   540
\item [$simp_all$] is similar to $simp$, but acts on all goals.
wenzelm@7321
   541
\end{descr}
wenzelm@7321
   542
wenzelm@8704
   543
By default, the Simplifier methods are based on \texttt{asm_full_simp_tac}
wenzelm@8706
   544
internally \cite[\S10]{isabelle-ref}, which means that assumptions are both
wenzelm@8706
   545
simplified as well as used in simplifying the conclusion.  In structured
wenzelm@8706
   546
proofs this is usually quite well behaved in practice: just the local premises
wenzelm@8706
   547
of the actual goal are involved, additional facts may inserted via explicit
wenzelm@8706
   548
forward-chaining (using $\THEN$, $\FROMNAME$ etc.).  The full context of
wenzelm@8706
   549
assumptions is only included if the ``$!$'' (bang) argument is given, which
wenzelm@8706
   550
should be used with some care, though.
wenzelm@7321
   551
wenzelm@8704
   552
Additional Simplifier options may be specified to tune the behavior even
wenzelm@9614
   553
further: $(no_asm)$ means assumptions are ignored completely (cf.\
wenzelm@8811
   554
\texttt{simp_tac}), $(no_asm_simp)$ means assumptions are used in the
wenzelm@9614
   555
simplification of the conclusion but are not themselves simplified (cf.\
wenzelm@8811
   556
\texttt{asm_simp_tac}), and $(no_asm_use)$ means assumptions are simplified
wenzelm@8811
   557
but are not used in the simplification of each other or the conclusion (cf.
wenzelm@8704
   558
\texttt{full_simp_tac}).
wenzelm@8704
   559
wenzelm@8704
   560
\medskip
wenzelm@8704
   561
wenzelm@8704
   562
The Splitter package is usually configured to work as part of the Simplifier.
wenzelm@9711
   563
The effect of repeatedly applying \texttt{split_tac} can be simulated by
wenzelm@9711
   564
$(simp~only\colon~split\colon~\vec a)$.  There is also a separate $split$
wenzelm@9711
   565
method available for single-step case splitting, see \S\ref{sec:basic-eq}.
wenzelm@8483
   566
wenzelm@8483
   567
wenzelm@8483
   568
\subsection{Declaring rules}
wenzelm@8483
   569
wenzelm@8667
   570
\indexisarcmd{print-simpset}
wenzelm@8638
   571
\indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong}
wenzelm@7321
   572
\begin{matharray}{rcl}
wenzelm@8667
   573
  print_simpset & : & \isarkeep{theory~|~proof} \\
wenzelm@7321
   574
  simp & : & \isaratt \\
wenzelm@9711
   575
  cong & : & \isaratt \\
wenzelm@8483
   576
  split & : & \isaratt \\
wenzelm@7321
   577
\end{matharray}
wenzelm@7321
   578
wenzelm@7321
   579
\begin{rail}
wenzelm@9711
   580
  ('simp' | 'cong' | 'split') (() | 'add' | 'del')
wenzelm@7321
   581
  ;
wenzelm@7321
   582
\end{rail}
wenzelm@7321
   583
wenzelm@7321
   584
\begin{descr}
wenzelm@8667
   585
\item [$print_simpset$] prints the collection of rules declared to the
wenzelm@8667
   586
  Simplifier, which is also known as ``simpset'' internally
wenzelm@8667
   587
  \cite{isabelle-ref}.  This is a diagnostic command; $undo$ does not apply.
wenzelm@8547
   588
\item [$simp$] declares simplification rules.
wenzelm@8638
   589
\item [$cong$] declares congruence rules.
wenzelm@9711
   590
\item [$split$] declares case split rules.
wenzelm@7321
   591
\end{descr}
wenzelm@7319
   592
wenzelm@7315
   593
wenzelm@7315
   594
\subsection{Forward simplification}
wenzelm@7315
   595
wenzelm@9905
   596
\indexisaratt{simplified}
wenzelm@7315
   597
\begin{matharray}{rcl}
wenzelm@9905
   598
  simplified & : & \isaratt \\
wenzelm@7315
   599
\end{matharray}
wenzelm@7315
   600
wenzelm@9905
   601
\begin{rail}
wenzelm@9905
   602
  'simplified' opt?
wenzelm@9905
   603
  ;
wenzelm@9905
   604
wenzelm@9905
   605
  opt: '(' (noasm | noasmsimp | noasmuse) ')'
wenzelm@9905
   606
  ;
wenzelm@9905
   607
\end{rail}
wenzelm@7905
   608
wenzelm@9905
   609
\begin{descr}
wenzelm@9905
   610
\item [$simplified$] causes a theorem to be simplified according to the
wenzelm@9905
   611
  current Simplifier context (there are no separate arguments for declaring
wenzelm@9905
   612
  additional rules).  By default the result is fully simplified, including
wenzelm@9905
   613
  assumptions and conclusion.  The options $no_asm$ etc.\ restrict the
wenzelm@9905
   614
  Simplifier in the same way as the for the $simp$ method (see
wenzelm@9905
   615
  \S\ref{sec:simp}).
wenzelm@9905
   616
  
wenzelm@9905
   617
  The $simplified$ operation should be used only very rarely, usually for
wenzelm@9905
   618
  experimentation only.
wenzelm@9905
   619
\end{descr}
wenzelm@7315
   620
wenzelm@7315
   621
wenzelm@9711
   622
\section{Basic equational reasoning}\label{sec:basic-eq}
wenzelm@9614
   623
wenzelm@9703
   624
\indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisarmeth{split}\indexisaratt{symmetric}
wenzelm@9614
   625
\begin{matharray}{rcl}
wenzelm@9614
   626
  subst & : & \isarmeth \\
wenzelm@9614
   627
  hypsubst^* & : & \isarmeth \\
wenzelm@9703
   628
  split & : & \isarmeth \\
wenzelm@9614
   629
  symmetric & : & \isaratt \\
wenzelm@9614
   630
\end{matharray}
wenzelm@9614
   631
wenzelm@9614
   632
\begin{rail}
wenzelm@9614
   633
  'subst' thmref
wenzelm@9614
   634
  ;
wenzelm@9799
   635
  'split' ('(' 'asm' ')')? thmrefs
wenzelm@9703
   636
  ;
wenzelm@9614
   637
\end{rail}
wenzelm@9614
   638
wenzelm@9614
   639
These methods and attributes provide basic facilities for equational reasoning
wenzelm@9614
   640
that are intended for specialized applications only.  Normally, single step
wenzelm@9614
   641
reasoning would be performed by calculation (see \S\ref{sec:calculation}),
wenzelm@9614
   642
while the Simplifier is the canonical tool for automated normalization (see
wenzelm@9614
   643
\S\ref{sec:simplifier}).
wenzelm@9614
   644
wenzelm@9614
   645
\begin{descr}
wenzelm@9614
   646
\item [$subst~thm$] performs a single substitution step using rule $thm$,
wenzelm@9614
   647
  which may be either a meta or object equality.
wenzelm@9614
   648
\item [$hypsubst$] performs substitution using some assumption.
wenzelm@9703
   649
\item [$split~thms$] performs single-step case splitting using rules $thms$.
wenzelm@9799
   650
  By default, splitting is performed in the conclusion of a goal; the $asm$
wenzelm@9799
   651
  option indicates to operate on assumptions instead.
wenzelm@9799
   652
  
wenzelm@9703
   653
  Note that the $simp$ method already involves repeated application of split
wenzelm@9703
   654
  rules as declared in the current context (see \S\ref{sec:simp}).
wenzelm@9614
   655
\item [$symmetric$] applies the symmetry rule of meta or object equality.
wenzelm@9614
   656
\end{descr}
wenzelm@9614
   657
wenzelm@9614
   658
wenzelm@9847
   659
\section{The Classical Reasoner}\label{sec:classical}
wenzelm@7135
   660
wenzelm@7335
   661
\subsection{Basic methods}\label{sec:classical-basic}
wenzelm@7321
   662
wenzelm@7974
   663
\indexisarmeth{rule}\indexisarmeth{intro}
wenzelm@7974
   664
\indexisarmeth{elim}\indexisarmeth{default}\indexisarmeth{contradiction}
wenzelm@7321
   665
\begin{matharray}{rcl}
wenzelm@7321
   666
  rule & : & \isarmeth \\
wenzelm@7321
   667
  intro & : & \isarmeth \\
wenzelm@7321
   668
  elim & : & \isarmeth \\
wenzelm@7321
   669
  contradiction & : & \isarmeth \\
wenzelm@7321
   670
\end{matharray}
wenzelm@7321
   671
wenzelm@7321
   672
\begin{rail}
wenzelm@8547
   673
  ('rule' | 'intro' | 'elim') thmrefs?
wenzelm@7321
   674
  ;
wenzelm@7321
   675
\end{rail}
wenzelm@7321
   676
wenzelm@7321
   677
\begin{descr}
wenzelm@7466
   678
\item [$rule$] as offered by the classical reasoner is a refinement over the
wenzelm@8517
   679
  primitive one (see \S\ref{sec:pure-meth-att}).  In case that no rules are
wenzelm@7466
   680
  provided as arguments, it automatically determines elimination and
wenzelm@7321
   681
  introduction rules from the context (see also \S\ref{sec:classical-mod}).
wenzelm@8517
   682
  This is made the default method for basic proof steps, such as $\PROOFNAME$
wenzelm@8517
   683
  and ``$\DDOT$'' (two dots), see also \S\ref{sec:proof-steps} and
wenzelm@8517
   684
  \S\ref{sec:pure-meth-att}.
wenzelm@9614
   685
wenzelm@7466
   686
\item [$intro$ and $elim$] repeatedly refine some goal by intro- or
wenzelm@7905
   687
  elim-resolution, after having inserted any facts.  Omitting the arguments
wenzelm@8547
   688
  refers to any suitable rules declared in the context, otherwise only the
wenzelm@8547
   689
  explicitly given ones may be applied.  The latter form admits better control
wenzelm@8547
   690
  of what actually happens, thus it is very appropriate as an initial method
wenzelm@8547
   691
  for $\PROOFNAME$ that splits up certain connectives of the goal, before
wenzelm@8547
   692
  entering the actual sub-proof.
wenzelm@9614
   693
wenzelm@7466
   694
\item [$contradiction$] solves some goal by contradiction, deriving any result
wenzelm@7466
   695
  from both $\neg A$ and $A$.  Facts, which are guaranteed to participate, may
wenzelm@7466
   696
  appear in either order.
wenzelm@7321
   697
\end{descr}
wenzelm@7321
   698
wenzelm@7321
   699
wenzelm@7981
   700
\subsection{Automated methods}\label{sec:classical-auto}
wenzelm@7315
   701
wenzelm@9799
   702
\indexisarmeth{blast}\indexisarmeth{fast}\indexisarmeth{slow}
wenzelm@9799
   703
\indexisarmeth{best}\indexisarmeth{safe}\indexisarmeth{clarify}
wenzelm@7321
   704
\begin{matharray}{rcl}
wenzelm@9780
   705
  blast & : & \isarmeth \\
wenzelm@9780
   706
  fast & : & \isarmeth \\
wenzelm@9799
   707
  slow & : & \isarmeth \\
wenzelm@9780
   708
  best & : & \isarmeth \\
wenzelm@9780
   709
  safe & : & \isarmeth \\
wenzelm@9780
   710
  clarify & : & \isarmeth \\
wenzelm@7321
   711
\end{matharray}
wenzelm@7321
   712
wenzelm@7321
   713
\begin{rail}
wenzelm@7905
   714
  'blast' ('!' ?) nat? (clamod * )
wenzelm@7321
   715
  ;
wenzelm@9799
   716
  ('fast' | 'slow' | 'best' | 'safe' | 'clarify') ('!' ?) (clamod * )
wenzelm@7321
   717
  ;
wenzelm@7321
   718
wenzelm@9408
   719
  clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs
wenzelm@7321
   720
  ;
wenzelm@7321
   721
\end{rail}
wenzelm@7321
   722
wenzelm@7321
   723
\begin{descr}
wenzelm@7321
   724
\item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac}
wenzelm@7335
   725
  in \cite[\S11]{isabelle-ref}).  The optional argument specifies a
wenzelm@9606
   726
  user-supplied search bound (default 20).  Note that $blast$ is the only
wenzelm@9606
   727
  classical proof procedure in Isabelle that can handle actual object-logic
wenzelm@9606
   728
  rules as local assumptions ($fast$ etc.\ would just ignore non-atomic
wenzelm@9606
   729
  facts).
wenzelm@9799
   730
\item [$fast$, $slow$, $best$, $safe$, and $clarify$] refer to the generic
wenzelm@9799
   731
  classical reasoner.  See \texttt{fast_tac}, \texttt{slow_tac},
wenzelm@9799
   732
  \texttt{best_tac}, \texttt{safe_tac}, and \texttt{clarify_tac} in
wenzelm@9799
   733
  \cite[\S11]{isabelle-ref} for more information.
wenzelm@7321
   734
\end{descr}
wenzelm@7321
   735
wenzelm@7321
   736
Any of above methods support additional modifiers of the context of classical
wenzelm@8517
   737
rules.  Their semantics is analogous to the attributes given in
wenzelm@8547
   738
\S\ref{sec:classical-mod}.  Facts provided by forward chaining are
wenzelm@8547
   739
inserted\footnote{These methods usually cannot make proper use of actual rules
wenzelm@8547
   740
  inserted that way, though.} into the goal before doing the search.  The
wenzelm@8547
   741
``!''~argument causes the full context of assumptions to be included as well.
wenzelm@8547
   742
This is slightly less hazardous than for the Simplifier (see
wenzelm@8547
   743
\S\ref{sec:simp}).
wenzelm@7321
   744
wenzelm@7315
   745
wenzelm@9847
   746
\subsection{Combined automated methods}\label{sec:clasimp}
wenzelm@7315
   747
wenzelm@9799
   748
\indexisarmeth{auto}\indexisarmeth{force}\indexisarmeth{clarsimp}
wenzelm@9799
   749
\indexisarmeth{fastsimp}\indexisarmeth{slowsimp}\indexisarmeth{bestsimp}
wenzelm@7321
   750
\begin{matharray}{rcl}
wenzelm@9606
   751
  auto & : & \isarmeth \\
wenzelm@7321
   752
  force & : & \isarmeth \\
wenzelm@9438
   753
  clarsimp & : & \isarmeth \\
wenzelm@9606
   754
  fastsimp & : & \isarmeth \\
wenzelm@9799
   755
  slowsimp & : & \isarmeth \\
wenzelm@9799
   756
  bestsimp & : & \isarmeth \\
wenzelm@7321
   757
\end{matharray}
wenzelm@7321
   758
wenzelm@7321
   759
\begin{rail}
wenzelm@9780
   760
  'auto' '!'? (nat nat)? (clasimpmod * )
wenzelm@9780
   761
  ;
wenzelm@9799
   762
  ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') '!'? (clasimpmod * )
wenzelm@7321
   763
  ;
wenzelm@7315
   764
wenzelm@9711
   765
  clasimpmod: ('simp' (() | 'add' | 'del' | 'only') |
wenzelm@9847
   766
    ('cong' | 'split' | 'iff') (() | 'add' | 'del') |
wenzelm@9408
   767
    (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' thmrefs
wenzelm@7321
   768
\end{rail}
wenzelm@7315
   769
wenzelm@7321
   770
\begin{descr}
wenzelm@9799
   771
\item [$auto$, $force$, $clarsimp$, $fastsimp$, $slowsimp$, and $bestsimp$]
wenzelm@9799
   772
  provide access to Isabelle's combined simplification and classical reasoning
wenzelm@9799
   773
  tactics.  These correspond to \texttt{auto_tac}, \texttt{force_tac},
wenzelm@9799
   774
  \texttt{clarsimp_tac}, and Classical Reasoner tactics with the Simplifier
wenzelm@9799
   775
  added as wrapper, see \cite[\S11]{isabelle-ref} for more information.  The
wenzelm@9799
   776
  modifier arguments correspond to those given in \S\ref{sec:simp} and
wenzelm@9606
   777
  \S\ref{sec:classical-auto}.  Just note that the ones related to the
wenzelm@9606
   778
  Simplifier are prefixed by \railtterm{simp} here.
wenzelm@9614
   779
wenzelm@7987
   780
  Facts provided by forward chaining are inserted into the goal before doing
wenzelm@7987
   781
  the search.  The ``!''~argument causes the full context of assumptions to be
wenzelm@7987
   782
  included as well.
wenzelm@7321
   783
\end{descr}
wenzelm@7321
   784
wenzelm@7987
   785
wenzelm@8483
   786
\subsection{Declaring rules}\label{sec:classical-mod}
wenzelm@7135
   787
wenzelm@8667
   788
\indexisarcmd{print-claset}
wenzelm@7391
   789
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
wenzelm@7391
   790
\indexisaratt{iff}\indexisaratt{delrule}
wenzelm@7321
   791
\begin{matharray}{rcl}
wenzelm@8667
   792
  print_claset & : & \isarkeep{theory~|~proof} \\
wenzelm@7321
   793
  intro & : & \isaratt \\
wenzelm@7321
   794
  elim & : & \isaratt \\
wenzelm@7321
   795
  dest & : & \isaratt \\
wenzelm@7391
   796
  iff & : & \isaratt \\
wenzelm@7321
   797
  delrule & : & \isaratt \\
wenzelm@7321
   798
\end{matharray}
wenzelm@7135
   799
wenzelm@7321
   800
\begin{rail}
wenzelm@9408
   801
  ('intro' | 'elim' | 'dest') ('!' | () | '?')
wenzelm@7321
   802
  ;
wenzelm@8638
   803
  'iff' (() | 'add' | 'del')
wenzelm@7321
   804
\end{rail}
wenzelm@7135
   805
wenzelm@7321
   806
\begin{descr}
wenzelm@8667
   807
\item [$print_claset$] prints the collection of rules declared to the
wenzelm@8667
   808
  Classical Reasoner, which is also known as ``simpset'' internally
wenzelm@8667
   809
  \cite{isabelle-ref}.  This is a diagnostic command; $undo$ does not apply.
wenzelm@8517
   810
\item [$intro$, $elim$, and $dest$] declare introduction, elimination, and
wenzelm@8517
   811
  destruct rules, respectively.  By default, rules are considered as
wenzelm@9408
   812
  \emph{unsafe} (i.e.\ not applied blindly without backtracking), while a
wenzelm@9408
   813
  single ``!'' classifies as \emph{safe}, and ``?'' as \emph{extra} (i.e.\ not
wenzelm@9408
   814
  applied in the search-oriented automated methods, but only in single-step
wenzelm@9408
   815
  methods such as $rule$).
wenzelm@9614
   816
wenzelm@8547
   817
\item [$iff$] declares equations both as rules for the Simplifier and
wenzelm@8547
   818
  Classical Reasoner.
wenzelm@7391
   819
wenzelm@7335
   820
\item [$delrule$] deletes introduction or elimination rules from the context.
wenzelm@7335
   821
  Note that destruction rules would have to be turned into elimination rules
wenzelm@9905
   822
  first, e.g.\ by using the $elimified$ attribute.
wenzelm@7321
   823
\end{descr}
wenzelm@7135
   824
wenzelm@8203
   825
wenzelm@9614
   826
%%% Local Variables:
wenzelm@7135
   827
%%% mode: latex
wenzelm@7135
   828
%%% TeX-master: "isar-ref"
wenzelm@9614
   829
%%% End: