doc-src/IsarRef/generic.tex
author wenzelm
Sat Mar 18 19:11:34 2000 +0100 (2000-03-18)
changeset 8517 062e6cd78534
parent 8507 d22fcea34cb7
child 8547 93b8685d004b
permissions -rw-r--r--
obtain;
moved pure methods / atts to pure.tex;
tuned;
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@8517
     6
\indexisarcmd{axclass}\indexisarcmd{instance}\indexisarmeth{intro-classes}
wenzelm@7167
     7
\begin{matharray}{rcl}
wenzelm@8517
     8
  \isarcmd{axclass} & : & \isartrans{theory}{theory} \\
wenzelm@8517
     9
  \isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
wenzelm@8517
    10
  intro_classes & : & \isarmeth \\
wenzelm@7167
    11
\end{matharray}
wenzelm@7167
    12
wenzelm@8517
    13
Axiomatic type classes are provided by Isabelle/Pure as a \emph{definitional}
wenzelm@8517
    14
interface to type classes (cf.~\S\ref{sec:classes}).  Thus any object logic
wenzelm@8517
    15
may make use of this light-weight mechanism of abstract theories.  See
wenzelm@8517
    16
\cite{Wenzel:1997:TPHOL} for more information.  There is also a tutorial on
wenzelm@8517
    17
\emph{Using Axiomatic Type Classes in Isabelle} that is part of the standard
wenzelm@8517
    18
Isabelle documentation.
wenzelm@8517
    19
%FIXME cite
wenzelm@8517
    20
wenzelm@7167
    21
\begin{rail}
wenzelm@8517
    22
  'axclass' classdecl (axmdecl prop comment? +)
wenzelm@8517
    23
  ;
wenzelm@8517
    24
  'instance' (nameref '<' nameref | nameref '::' simplearity) comment?
wenzelm@7167
    25
  ;
wenzelm@7167
    26
\end{rail}
wenzelm@7167
    27
wenzelm@7167
    28
\begin{descr}
wenzelm@8517
    29
\item [$\isarkeyword{axclass}~c < \vec c~axms$] defines an axiomatic type
wenzelm@8517
    30
  class as the intersection of existing classes, with additional axioms
wenzelm@8517
    31
  holding.  Class axioms may not contain more than one type variable.  The
wenzelm@8517
    32
  class axioms (with implicit sort constraints added) are bound to the given
wenzelm@8517
    33
  names.  Furthermore a class introduction rule is generated, which is
wenzelm@8517
    34
  employed by method $intro_classes$ to support instantiation proofs of this
wenzelm@8517
    35
  class.
wenzelm@7321
    36
  
wenzelm@8517
    37
\item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~t ::
wenzelm@8517
    38
  (\vec s)c$] setup up a goal stating the class relation or type arity.  The
wenzelm@8517
    39
  proof would usually proceed by $intro_classes$, and then establish the
wenzelm@8517
    40
  characteristic theorems of the type classes involved.  After finishing the
wenzelm@8517
    41
  proof, the theory will be augmented by a type signature declaration
wenzelm@8517
    42
  corresponding to the resulting theorem.
wenzelm@8517
    43
\item [$intro_classes$] repeatedly expands all class introduction rules of
wenzelm@8517
    44
  this theory.
wenzelm@7167
    45
\end{descr}
wenzelm@7167
    46
wenzelm@7315
    47
wenzelm@7315
    48
\section{Calculational proof}\label{sec:calculation}
wenzelm@7315
    49
wenzelm@7315
    50
\indexisarcmd{also}\indexisarcmd{finally}\indexisaratt{trans}
wenzelm@7315
    51
\begin{matharray}{rcl}
wenzelm@7315
    52
  \isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7315
    53
  \isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\
wenzelm@7315
    54
  trans & : & \isaratt \\
wenzelm@7315
    55
\end{matharray}
wenzelm@7315
    56
wenzelm@7315
    57
Calculational proof is forward reasoning with implicit application of
wenzelm@7315
    58
transitivity rules (such those of $=$, $\le$, $<$).  Isabelle/Isar maintains
wenzelm@7391
    59
an auxiliary register $calculation$\indexisarthm{calculation} for accumulating
wenzelm@7897
    60
results obtained by transitivity composed with the current result.  Command
wenzelm@7897
    61
$\ALSO$ updates $calculation$ involving $this$, while $\FINALLY$ exhibits the
wenzelm@7897
    62
final $calculation$ by forward chaining towards the next goal statement.  Both
wenzelm@7897
    63
commands require valid current facts, i.e.\ may occur only after commands that
wenzelm@7897
    64
produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or some finished proof of
wenzelm@7897
    65
$\HAVENAME$, $\SHOWNAME$ etc.
wenzelm@7315
    66
wenzelm@7315
    67
Also note that the automatic term abbreviation ``$\dots$'' has its canonical
wenzelm@7315
    68
application with calculational proofs.  It automatically refers to the
wenzelm@7315
    69
argument\footnote{The argument of a curried infix expression is its right-hand
wenzelm@7315
    70
  side.} of the preceding statement.
wenzelm@7315
    71
wenzelm@7315
    72
Isabelle/Isar calculations are implicitly subject to block structure in the
wenzelm@7315
    73
sense that new threads of calculational reasoning are commenced for any new
wenzelm@7315
    74
block (as opened by a local goal, for example).  This means that, apart from
wenzelm@7315
    75
being able to nest calculations, there is no separate \emph{begin-calculation}
wenzelm@7315
    76
command required.
wenzelm@7315
    77
wenzelm@7315
    78
\begin{rail}
wenzelm@7315
    79
  ('also' | 'finally') transrules? comment?
wenzelm@7315
    80
  ;
wenzelm@8507
    81
  'trans' (() | 'add' | 'del')
wenzelm@7315
    82
  ;
wenzelm@7315
    83
wenzelm@7315
    84
  transrules: '(' thmrefs ')' interest?
wenzelm@7315
    85
  ;
wenzelm@7315
    86
\end{rail}
wenzelm@7315
    87
wenzelm@7315
    88
\begin{descr}
wenzelm@7315
    89
\item [$\ALSO~(thms)$] maintains the auxiliary $calculation$ register as
wenzelm@7315
    90
  follows.  The first occurrence of $\ALSO$ in some calculational thread
wenzelm@7905
    91
  initializes $calculation$ by $this$. Any subsequent $\ALSO$ on the same
wenzelm@7335
    92
  level of block-structure updates $calculation$ by some transitivity rule
wenzelm@7458
    93
  applied to $calculation$ and $this$ (in that order).  Transitivity rules are
wenzelm@7458
    94
  picked from the current context plus those given as $thms$ (the latter have
wenzelm@7458
    95
  precedence).
wenzelm@7315
    96
  
wenzelm@7315
    97
\item [$\FINALLY~(thms)$] maintaining $calculation$ in the same way as
wenzelm@7315
    98
  $\ALSO$, and concludes the current calculational thread.  The final result
wenzelm@7315
    99
  is exhibited as fact for forward chaining towards the next goal. Basically,
wenzelm@7987
   100
  $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$.  Note that
wenzelm@7987
   101
  ``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and
wenzelm@7987
   102
  ``$\FINALLY~\HAVE{}{\phi}~\DOT$'' are typical idioms for concluding
wenzelm@7987
   103
  calculational proofs.
wenzelm@7315
   104
  
wenzelm@7335
   105
\item [$trans$] maintains the set of transitivity rules of the theory or proof
wenzelm@7335
   106
  context, by adding or deleting theorems (the default is to add).
wenzelm@7315
   107
\end{descr}
wenzelm@7315
   108
wenzelm@7315
   109
wenzelm@8483
   110
\section{Named local contexts (cases)}\label{sec:cases}
wenzelm@8483
   111
wenzelm@8483
   112
\indexisarcmd{case}\indexisarcmd{print-cases}
wenzelm@8483
   113
\indexisaratt{case-names}\indexisaratt{params}
wenzelm@8483
   114
\begin{matharray}{rcl}
wenzelm@8483
   115
  \isarcmd{case} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@8517
   116
  \isarcmd{print_cases}^* & : & \isarkeep{proof} \\
wenzelm@8483
   117
  case_names & : & \isaratt \\
wenzelm@8483
   118
  params & : & \isaratt \\
wenzelm@8483
   119
\end{matharray}
wenzelm@8483
   120
wenzelm@8483
   121
Basically, Isar proof contexts are built up explicitly using commands like
wenzelm@8483
   122
$\FIXNAME$, $\ASSUMENAME$ etc.\ (see \S\ref{sec:proof-context}).  In typical
wenzelm@8483
   123
verification tasks this can become hard to manage, though.  In particular, a
wenzelm@8483
   124
large number of local contexts may emerge from case analysis or induction over
wenzelm@8483
   125
inductive sets and types.
wenzelm@8483
   126
wenzelm@8483
   127
\medskip
wenzelm@8483
   128
wenzelm@8483
   129
The $\CASENAME$ command provides a shorthand to refer to certain parts of
wenzelm@8483
   130
logical context symbolically.  Proof methods may provide an environment of
wenzelm@8507
   131
named ``cases'' of the form $c\colon \vec x, \vec \phi$.  Then the effect of
wenzelm@8507
   132
$\CASE{c}$ is exactly the same as $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$.
wenzelm@8483
   133
wenzelm@8483
   134
It is important to note that $\CASENAME$ does \emph{not} provide any means to
wenzelm@8483
   135
peek at the current goal state, which is treated as strictly non-observable in
wenzelm@8483
   136
Isar!  Instead, the cases considered here usually emerge in a canonical way
wenzelm@8483
   137
from certain pieces of specification that appear in the theory somewhere else
wenzelm@8483
   138
(e.g.\ in an inductive definition, or recursive function).  See also
wenzelm@8483
   139
\S\ref{sec:induct-method} for more details of how this works in HOL.
wenzelm@8483
   140
wenzelm@8483
   141
\medskip
wenzelm@8483
   142
wenzelm@8483
   143
Named cases may be exhibited in the current proof context only if both the
wenzelm@8483
   144
proof method and the corresponding rule support this.  Case names and
wenzelm@8483
   145
parameters of basic rules may be declared by hand as well, by using
wenzelm@8483
   146
appropriate attributes.  Thus variant versions of rules that have been derived
wenzelm@8483
   147
manually may be used in advanced case analysis later.
wenzelm@8483
   148
wenzelm@8483
   149
\railalias{casenames}{case\_names}
wenzelm@8483
   150
\railterm{casenames}
wenzelm@8483
   151
wenzelm@8483
   152
\begin{rail}
wenzelm@8483
   153
  'case' nameref attributes?
wenzelm@8483
   154
  ;
wenzelm@8483
   155
  casenames (name + )
wenzelm@8483
   156
  ;
wenzelm@8483
   157
  'params' ((name * ) + 'and')
wenzelm@8483
   158
  ;
wenzelm@8483
   159
\end{rail}
wenzelm@8483
   160
wenzelm@8483
   161
\begin{descr}
wenzelm@8507
   162
\item [$\CASE{c}$] invokes a named local context $c\colon \vec x, \vec \phi$,
wenzelm@8483
   163
  as provided by an appropriate proof method (such as $cases$ and $induct$,
wenzelm@8483
   164
  see \S\ref{sec:induct-method}).  The command $\CASE{c}$ abbreviates
wenzelm@8507
   165
  $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$.
wenzelm@8483
   166
\item [$\isarkeyword{print_cases}$] prints all local contexts of the current
wenzelm@8483
   167
  goal context, using Isar proof language notation.  This is a diagnostic
wenzelm@8483
   168
  command; $undo$ does not apply.
wenzelm@8483
   169
\item [$case_names~\vec c$] declares names for the local contexts of premises
wenzelm@8483
   170
  of some theorem ($\vec c$ refers to the \emph{suffix} of the list premises).
wenzelm@8483
   171
\item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of
wenzelm@8483
   172
  premises $1, \dots, n$ of some theorem.  An empty list of names be be given
wenzelm@8483
   173
  to skip positions, leaving the corresponding parameters unchanged.
wenzelm@8483
   174
\end{descr}
wenzelm@8483
   175
wenzelm@8483
   176
wenzelm@8517
   177
\section{Generalized existence}
wenzelm@7135
   178
wenzelm@8517
   179
\indexisarcmd{obtain}
wenzelm@7135
   180
\begin{matharray}{rcl}
wenzelm@8517
   181
  \isarcmd{obtain} & : & \isartrans{proof(prove)}{proof(state)} \\
wenzelm@8517
   182
\end{matharray}
wenzelm@8517
   183
wenzelm@8517
   184
Generalized existence reasoning means that additional elements with certain
wenzelm@8517
   185
properties are introduced, together with a soundness proof of that context
wenzelm@8517
   186
change (the rest of the main goal is left unchanged).
wenzelm@8517
   187
wenzelm@8517
   188
Syntactically, the $\OBTAINNAME$ language element is like a proof method to
wenzelm@8517
   189
the present goal, followed by a proof of its additional claim, followed by the
wenzelm@8517
   190
actual context commands (cf.\ $\FIXNAME$ and $\ASSUMENAME$,
wenzelm@8517
   191
\S\ref{sec:proof-context}).
wenzelm@8517
   192
wenzelm@8517
   193
\begin{rail}
wenzelm@8517
   194
  'obtain' (vars + 'and') comment? \\ 'where' (assm comment? + 'and')
wenzelm@8517
   195
  ;
wenzelm@8517
   196
\end{rail}
wenzelm@8517
   197
wenzelm@8517
   198
$\OBTAINNAME$ is defined as a derived Isar command as follows, where the
wenzelm@8517
   199
preceding goal shall be $\psi$, with (optional) facts $\vec b$ indicated for
wenzelm@8517
   200
forward chaining.
wenzelm@8517
   201
\begin{matharray}{l}
wenzelm@8517
   202
  \OBTAIN{\vec x}{a}{\vec \phi}~~\langle proof\rangle \equiv {} \\[0.5ex]
wenzelm@8517
   203
  \quad \PROOF{succeed} \\
wenzelm@8517
   204
  \qquad \DEF{}{thesis \equiv \psi} \\
wenzelm@8517
   205
  \qquad \PRESUME{that}{\All{\vec x} \vec\phi \Imp thesis} \\
wenzelm@8517
   206
  \qquad \FROM{\vec b}~\SHOW{}{thesis}~~\langle proof\rangle \\
wenzelm@8517
   207
  \quad \NEXT \\
wenzelm@8517
   208
  \qquad \FIX{\vec x}~\ASSUME{a}{\vec\phi} \\
wenzelm@7135
   209
\end{matharray}
wenzelm@7135
   210
wenzelm@8517
   211
Typically, the soundness proof is relatively straight-forward, often just by
wenzelm@8517
   212
canonical automated tools such as $\BY{simp}$ (see \S\ref{sec:simp}) or
wenzelm@8517
   213
$\BY{blast}$ (see \S\ref{sec:classical-auto}).  Note that the ``$that$''
wenzelm@8517
   214
presumption above is usually declared as simplification and (unsafe)
wenzelm@8517
   215
introduction rule, somewhat depending on the object-logic's policy,
wenzelm@8517
   216
though.\footnote{Major object-logics such as HOL and HOLCF do this already.}
wenzelm@8517
   217
wenzelm@8517
   218
The original goal statement is wrapped into a local definition in order to
wenzelm@8517
   219
avoid any automated tools descending into it.  Usually, any statement would
wenzelm@8517
   220
admit the intended reduction; only in very rare cases $thesis_def$ has to be
wenzelm@8517
   221
expanded to complete the soundness proof.
wenzelm@8517
   222
wenzelm@8517
   223
\medskip
wenzelm@8517
   224
wenzelm@8517
   225
In a sense, $\OBTAINNAME$ represents at the level of Isar proofs what would be
wenzelm@8517
   226
meta-logical existential quantifiers and conjunctions.  This concept has a
wenzelm@8517
   227
broad range of useful applications, ranging from plain elimination (or even
wenzelm@8517
   228
introduction) of object-level existentials and conjunctions, to elimination
wenzelm@8517
   229
over results of symbolic evaluation of recursive definitions, for example.
wenzelm@8517
   230
wenzelm@8517
   231
wenzelm@8517
   232
\section{Miscellaneous methods and attributes}
wenzelm@8517
   233
wenzelm@8517
   234
\indexisarmeth{unfold}\indexisarmeth{fold}
wenzelm@8517
   235
\indexisarmeth{erule}\indexisarmeth{drule}\indexisarmeth{frule}
wenzelm@8517
   236
\indexisarmeth{fail}\indexisarmeth{succeed}
wenzelm@8517
   237
\begin{matharray}{rcl}
wenzelm@8517
   238
  unfold & : & \isarmeth \\
wenzelm@8517
   239
  fold & : & \isarmeth \\[0.5ex]
wenzelm@8517
   240
  erule^* & : & \isarmeth \\
wenzelm@8517
   241
  drule^* & : & \isarmeth \\
wenzelm@8517
   242
  frule^* & : & \isarmeth \\[0.5ex]
wenzelm@8517
   243
  succeed & : & \isarmeth \\
wenzelm@8517
   244
  fail & : & \isarmeth \\
wenzelm@8517
   245
\end{matharray}
wenzelm@7135
   246
wenzelm@7135
   247
\begin{rail}
wenzelm@8517
   248
  ('fold' | 'unfold' | 'erule' | 'drule' | 'frule') thmrefs
wenzelm@7135
   249
  ;
wenzelm@7135
   250
\end{rail}
wenzelm@7135
   251
wenzelm@7167
   252
\begin{descr}
wenzelm@8517
   253
\item [$unfold~thms$ and $fold~thms$] expand and fold back again the given
wenzelm@8517
   254
  meta-level definitions throughout all goals; any facts provided are inserted
wenzelm@8517
   255
  into the goal and subject to rewriting as well.
wenzelm@8517
   256
\item [$erule~thms$, $drule~thms$, and $frule~thms$] are similar to the basic
wenzelm@8517
   257
  $rule$ method (see \S\ref{sec:pure-meth-att}), but apply rules by
wenzelm@8517
   258
  elim-resolution, destruct-resolution, and forward-resolution, respectively
wenzelm@8517
   259
  \cite{isabelle-ref}.  These are improper method, mainly for experimentation
wenzelm@8517
   260
  and emulating tactic scripts.
wenzelm@7335
   261
  
wenzelm@8517
   262
  Different modes of basic rule application are usually expressed in Isar at
wenzelm@8517
   263
  the proof language level, rather than via implicit proof state
wenzelm@8517
   264
  modifications.  For example, a proper single-step elimination would be done
wenzelm@8517
   265
  using the basic $rule$ method, with forward chaining of current facts.
wenzelm@8517
   266
\item [$succeed$] yields a single (unchanged) result; it is the identity of
wenzelm@8517
   267
  the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
wenzelm@8517
   268
\item [$fail$] yields an empty result sequence; it is the identity of the
wenzelm@8517
   269
  ``\texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
wenzelm@7167
   270
\end{descr}
wenzelm@7135
   271
wenzelm@8517
   272
wenzelm@8517
   273
\indexisaratt{standard}
wenzelm@8517
   274
\indexisaratt{elimify}
wenzelm@8517
   275
wenzelm@8517
   276
\indexisaratt{RS}\indexisaratt{COMP}
wenzelm@8517
   277
\indexisaratt{where}
wenzelm@8517
   278
\indexisaratt{tag}\indexisaratt{untag}
wenzelm@8517
   279
\indexisaratt{transfer}
wenzelm@8517
   280
\indexisaratt{export}
wenzelm@8517
   281
\indexisaratt{unfold}\indexisaratt{fold}
wenzelm@8517
   282
\begin{matharray}{rcl}
wenzelm@8517
   283
  tag & : & \isaratt \\
wenzelm@8517
   284
  untag & : & \isaratt \\[0.5ex]
wenzelm@8517
   285
  RS & : & \isaratt \\
wenzelm@8517
   286
  COMP & : & \isaratt \\[0.5ex]
wenzelm@8517
   287
  where & : & \isaratt \\[0.5ex]
wenzelm@8517
   288
  unfold & : & \isaratt \\
wenzelm@8517
   289
  fold & : & \isaratt \\[0.5ex]
wenzelm@8517
   290
  standard & : & \isaratt \\
wenzelm@8517
   291
  elimify & : & \isaratt \\
wenzelm@8517
   292
  export^* & : & \isaratt \\
wenzelm@8517
   293
  transfer & : & \isaratt \\[0.5ex]
wenzelm@8517
   294
\end{matharray}
wenzelm@8517
   295
wenzelm@8517
   296
\begin{rail}
wenzelm@8517
   297
  'tag' (nameref+)
wenzelm@8517
   298
  ;
wenzelm@8517
   299
  'untag' name
wenzelm@8517
   300
  ;
wenzelm@8517
   301
  ('RS' | 'COMP') nat? thmref
wenzelm@8517
   302
  ;
wenzelm@8517
   303
  'where' (name '=' term * 'and')
wenzelm@8517
   304
  ;
wenzelm@8517
   305
  ('unfold' | 'fold') thmrefs
wenzelm@8517
   306
  ;
wenzelm@8517
   307
\end{rail}
wenzelm@8517
   308
wenzelm@8517
   309
\begin{descr}
wenzelm@8517
   310
\item [$tag~name~args$ and $untag~name$] add and remove $tags$ of some
wenzelm@8517
   311
  theorem.  Tags may be any list of strings that serve as comment for some
wenzelm@8517
   312
  tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the
wenzelm@8517
   313
  result).  The first string is considered the tag name, the rest its
wenzelm@8517
   314
  arguments.  Note that untag removes any tags of the same name.
wenzelm@8517
   315
\item [$RS~n~thm$ and $COMP~n~thm$] compose rules.  $RS$ resolves with the
wenzelm@8517
   316
  $n$-th premise of $thm$; $COMP$ is a version of $RS$ that skips the
wenzelm@8517
   317
  automatic lifting process that is normally intended (cf.\ \texttt{RS} and
wenzelm@8517
   318
  \texttt{COMP} in \cite[\S5]{isabelle-ref}).
wenzelm@8517
   319
\item [$where~\vec x = \vec t$] perform named instantiation of schematic
wenzelm@8517
   320
  variables occurring in a theorem.  Unlike instantiation tactics (such as
wenzelm@8517
   321
  \texttt{res_inst_tac}, see \cite{isabelle-ref}), actual schematic variables
wenzelm@8517
   322
  have to be specified (e.g.\ $\Var{x@3}$).
wenzelm@8517
   323
  
wenzelm@8517
   324
\item [$unfold~thms$ and $fold~thms$] expand and fold back again the given
wenzelm@8517
   325
  meta-level definitions throughout a rule.
wenzelm@8517
   326
 
wenzelm@8517
   327
\item [$standard$] puts a theorem into the standard form of object-rules, just
wenzelm@8517
   328
  as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).
wenzelm@8517
   329
  
wenzelm@8517
   330
\item [$elimify$] turns an destruction rule into an elimination, just as the
wenzelm@8517
   331
  ML function \texttt{make\_elim} (see \cite{isabelle-ref}).
wenzelm@8517
   332
  
wenzelm@8517
   333
\item [$export$] lifts a local result out of the current proof context,
wenzelm@8517
   334
  generalizing all fixed variables and discharging all assumptions.  Note that
wenzelm@8517
   335
  (partial) export is usually done automatically behind the scenes.  This
wenzelm@8517
   336
  attribute is mainly for experimentation.
wenzelm@8517
   337
  
wenzelm@8517
   338
\item [$transfer$] promotes a theorem to the current theory context, which has
wenzelm@8517
   339
  to enclose the former one.  Normally, this is done automatically when rules
wenzelm@8517
   340
  are joined by inference.
wenzelm@8517
   341
wenzelm@8517
   342
\end{descr}
wenzelm@7135
   343
wenzelm@7135
   344
wenzelm@7135
   345
\section{The Simplifier}
wenzelm@7135
   346
wenzelm@7321
   347
\subsection{Simplification methods}\label{sec:simp}
wenzelm@7315
   348
wenzelm@8483
   349
\indexisarmeth{simp}\indexisarmeth{simp-all}
wenzelm@7315
   350
\begin{matharray}{rcl}
wenzelm@7315
   351
  simp & : & \isarmeth \\
wenzelm@8483
   352
  simp_all & : & \isarmeth \\
wenzelm@7315
   353
\end{matharray}
wenzelm@7315
   354
wenzelm@8483
   355
\railalias{simpall}{simp\_all}
wenzelm@8483
   356
\railterm{simpall}
wenzelm@8483
   357
wenzelm@7315
   358
\begin{rail}
wenzelm@8483
   359
  ('simp' | simpall) ('!' ?) (simpmod * )
wenzelm@7315
   360
  ;
wenzelm@7315
   361
wenzelm@8483
   362
  simpmod: ('add' | 'del' | 'only' | 'split' (() | 'add' | 'del') | 'other') ':' thmrefs
wenzelm@7315
   363
  ;
wenzelm@7315
   364
\end{rail}
wenzelm@7315
   365
wenzelm@7321
   366
\begin{descr}
wenzelm@7897
   367
\item [$simp$] invokes Isabelle's simplifier, after modifying the context by
wenzelm@7897
   368
  adding or deleting rules as specified.  The \railtoken{only} modifier first
wenzelm@8483
   369
  removes all other rewrite rules, congruences, and looper tactics (including
wenzelm@8483
   370
  splits), and then behaves like \railtoken{add}.
wenzelm@7321
   371
  
wenzelm@8483
   372
  The \railtoken{split} modifiers add or delete rules for the Splitter (see
wenzelm@8483
   373
  also \cite{isabelle-ref}), the default is to add.  This works only if the
wenzelm@8483
   374
  Simplifier method has been properly setup to include the Splitter (all major
wenzelm@8483
   375
  object logics such HOL, HOLCF, FOL, ZF do this already).
wenzelm@8483
   376
  
wenzelm@8483
   377
  The \railtoken{other} modifier ignores its arguments.  Nevertheless there
wenzelm@8483
   378
  may be side-effects on the context via attributes.\footnote{This provides a
wenzelm@8483
   379
    back door for arbitrary context manipulation.}
wenzelm@8483
   380
  
wenzelm@8483
   381
\item [$simp_all$] is similar to $simp$, but acts on all goals.
wenzelm@7321
   382
\end{descr}
wenzelm@7321
   383
wenzelm@8483
   384
The $simp$ methods are based on \texttt{asm_full_simp_tac}
wenzelm@8483
   385
\cite[\S10]{isabelle-ref}, but is much better behaved in practice.  Just the
wenzelm@8483
   386
local premises of the actual goal are involved by default.  Additional facts
wenzelm@8483
   387
may be inserted via forward-chaining (using $\THEN$, $\FROMNAME$ etc.).  The
wenzelm@8483
   388
full context of assumptions is only included in the $simp!$ versions, which
wenzelm@8483
   389
should be used with some care, though.
wenzelm@7321
   390
wenzelm@8483
   391
Note that there is no separate $split$ method.  The effect of
wenzelm@8517
   392
\texttt{split_tac} can be simulated by $(simp~only\colon~split\colon~thms)$.
wenzelm@8483
   393
wenzelm@8483
   394
wenzelm@8483
   395
\subsection{Declaring rules}
wenzelm@8483
   396
wenzelm@8483
   397
\indexisaratt{simp}\indexisaratt{split}
wenzelm@7321
   398
\begin{matharray}{rcl}
wenzelm@7321
   399
  simp & : & \isaratt \\
wenzelm@8483
   400
  split & : & \isaratt \\
wenzelm@7321
   401
\end{matharray}
wenzelm@7321
   402
wenzelm@7321
   403
\begin{rail}
wenzelm@8483
   404
  ('simp' | 'split') (() | 'add' | 'del')
wenzelm@7321
   405
  ;
wenzelm@7321
   406
\end{rail}
wenzelm@7321
   407
wenzelm@7321
   408
\begin{descr}
wenzelm@7466
   409
\item [$simp$] adds or deletes rules from the theory or proof context (the
wenzelm@7466
   410
  default is to add).
wenzelm@8483
   411
\item [$split$] is similar to $simp$, but refers to split rules.
wenzelm@7321
   412
\end{descr}
wenzelm@7319
   413
wenzelm@7315
   414
wenzelm@7315
   415
\subsection{Forward simplification}
wenzelm@7315
   416
wenzelm@7391
   417
\indexisaratt{simplify}\indexisaratt{asm-simplify}
wenzelm@7391
   418
\indexisaratt{full-simplify}\indexisaratt{asm-full-simplify}
wenzelm@7315
   419
\begin{matharray}{rcl}
wenzelm@7315
   420
  simplify & : & \isaratt \\
wenzelm@7315
   421
  asm_simplify & : & \isaratt \\
wenzelm@7315
   422
  full_simplify & : & \isaratt \\
wenzelm@7315
   423
  asm_full_simplify & : & \isaratt \\
wenzelm@7315
   424
\end{matharray}
wenzelm@7315
   425
wenzelm@7321
   426
These attributes provide forward rules for simplification, which should be
wenzelm@7905
   427
used only very rarely.  There are no separate options for adding or deleting
wenzelm@7905
   428
simplification rules locally.
wenzelm@7905
   429
wenzelm@7905
   430
See the ML functions of the same name in \cite[\S10]{isabelle-ref} for more
wenzelm@7905
   431
information.
wenzelm@7315
   432
wenzelm@7315
   433
wenzelm@7135
   434
\section{The Classical Reasoner}
wenzelm@7135
   435
wenzelm@7335
   436
\subsection{Basic methods}\label{sec:classical-basic}
wenzelm@7321
   437
wenzelm@7974
   438
\indexisarmeth{rule}\indexisarmeth{intro}
wenzelm@7974
   439
\indexisarmeth{elim}\indexisarmeth{default}\indexisarmeth{contradiction}
wenzelm@7321
   440
\begin{matharray}{rcl}
wenzelm@7321
   441
  rule & : & \isarmeth \\
wenzelm@7321
   442
  intro & : & \isarmeth \\
wenzelm@7321
   443
  elim & : & \isarmeth \\
wenzelm@7321
   444
  contradiction & : & \isarmeth \\
wenzelm@7321
   445
\end{matharray}
wenzelm@7321
   446
wenzelm@7321
   447
\begin{rail}
wenzelm@7321
   448
  ('rule' | 'intro' | 'elim') thmrefs
wenzelm@7321
   449
  ;
wenzelm@7321
   450
\end{rail}
wenzelm@7321
   451
wenzelm@7321
   452
\begin{descr}
wenzelm@7466
   453
\item [$rule$] as offered by the classical reasoner is a refinement over the
wenzelm@8517
   454
  primitive one (see \S\ref{sec:pure-meth-att}).  In case that no rules are
wenzelm@7466
   455
  provided as arguments, it automatically determines elimination and
wenzelm@7321
   456
  introduction rules from the context (see also \S\ref{sec:classical-mod}).
wenzelm@8517
   457
  This is made the default method for basic proof steps, such as $\PROOFNAME$
wenzelm@8517
   458
  and ``$\DDOT$'' (two dots), see also \S\ref{sec:proof-steps} and
wenzelm@8517
   459
  \S\ref{sec:pure-meth-att}.
wenzelm@7321
   460
  
wenzelm@7466
   461
\item [$intro$ and $elim$] repeatedly refine some goal by intro- or
wenzelm@7905
   462
  elim-resolution, after having inserted any facts.  Omitting the arguments
wenzelm@7321
   463
  refers to any suitable rules from the context, otherwise only the explicitly
wenzelm@7335
   464
  given ones may be applied.  The latter form admits better control of what
wenzelm@7335
   465
  actually happens, thus it is very appropriate as an initial method for
wenzelm@7335
   466
  $\PROOFNAME$ that splits up certain connectives of the goal, before entering
wenzelm@7987
   467
  the actual sub-proof.
wenzelm@7458
   468
  
wenzelm@7466
   469
\item [$contradiction$] solves some goal by contradiction, deriving any result
wenzelm@7466
   470
  from both $\neg A$ and $A$.  Facts, which are guaranteed to participate, may
wenzelm@7466
   471
  appear in either order.
wenzelm@7321
   472
\end{descr}
wenzelm@7321
   473
wenzelm@7321
   474
wenzelm@7981
   475
\subsection{Automated methods}\label{sec:classical-auto}
wenzelm@7315
   476
wenzelm@7321
   477
\indexisarmeth{blast}
wenzelm@7391
   478
\indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{slow}\indexisarmeth{slow-best}
wenzelm@7321
   479
\begin{matharray}{rcl}
wenzelm@7321
   480
 blast & : & \isarmeth \\
wenzelm@7321
   481
 fast & : & \isarmeth \\
wenzelm@7321
   482
 best & : & \isarmeth \\
wenzelm@7321
   483
 slow & : & \isarmeth \\
wenzelm@7321
   484
 slow_best & : & \isarmeth \\
wenzelm@7321
   485
\end{matharray}
wenzelm@7321
   486
wenzelm@7321
   487
\railalias{slowbest}{slow\_best}
wenzelm@7321
   488
\railterm{slowbest}
wenzelm@7321
   489
wenzelm@7321
   490
\begin{rail}
wenzelm@7905
   491
  'blast' ('!' ?) nat? (clamod * )
wenzelm@7321
   492
  ;
wenzelm@7905
   493
  ('fast' | 'best' | 'slow' | slowbest) ('!' ?) (clamod * )
wenzelm@7321
   494
  ;
wenzelm@7321
   495
wenzelm@8203
   496
  clamod: (('intro' | 'elim' | 'dest') (() | '?' | '??') | 'del') ':' thmrefs
wenzelm@7321
   497
  ;
wenzelm@7321
   498
\end{rail}
wenzelm@7321
   499
wenzelm@7321
   500
\begin{descr}
wenzelm@7321
   501
\item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac}
wenzelm@7335
   502
  in \cite[\S11]{isabelle-ref}).  The optional argument specifies a
wenzelm@7321
   503
  user-supplied search bound (default 20).
wenzelm@7321
   504
\item [$fast$, $best$, $slow$, $slow_best$] refer to the generic classical
wenzelm@7335
   505
  reasoner (see \cite[\S11]{isabelle-ref}, tactic \texttt{fast_tac} etc).
wenzelm@7321
   506
\end{descr}
wenzelm@7321
   507
wenzelm@7321
   508
Any of above methods support additional modifiers of the context of classical
wenzelm@8517
   509
rules.  Their semantics is analogous to the attributes given in
wenzelm@7987
   510
\S\ref{sec:classical-mod}.  Facts provided by forward chaining are inserted
wenzelm@7987
   511
into the goal before doing the search.  The ``!''~argument causes the full
wenzelm@7987
   512
context of assumptions to be included as well.\footnote{This is slightly less
wenzelm@7987
   513
  hazardous than for the Simplifier (see \S\ref{sec:simp}).}
wenzelm@7321
   514
wenzelm@7315
   515
wenzelm@7981
   516
\subsection{Combined automated methods}
wenzelm@7315
   517
wenzelm@7321
   518
\indexisarmeth{auto}\indexisarmeth{force}
wenzelm@7321
   519
\begin{matharray}{rcl}
wenzelm@7321
   520
  force & : & \isarmeth \\
wenzelm@7321
   521
  auto & : & \isarmeth \\
wenzelm@7321
   522
\end{matharray}
wenzelm@7321
   523
wenzelm@7321
   524
\begin{rail}
wenzelm@7905
   525
  ('force' | 'auto') ('!' ?) (clasimpmod * )
wenzelm@7321
   526
  ;
wenzelm@7315
   527
wenzelm@8483
   528
  clasimpmod: ('simp' (() | 'add' | 'del' | 'only') | 'other' |
wenzelm@8483
   529
    ('split' (() | 'add' | 'del')) |
wenzelm@8203
   530
    (('intro' | 'elim' | 'dest') (() | '?' | '??') | 'del')) ':' thmrefs
wenzelm@7321
   531
\end{rail}
wenzelm@7315
   532
wenzelm@7321
   533
\begin{descr}
wenzelm@7321
   534
\item [$force$ and $auto$] provide access to Isabelle's combined
wenzelm@7321
   535
  simplification and classical reasoning tactics.  See \texttt{force_tac} and
wenzelm@7321
   536
  \texttt{auto_tac} in \cite[\S11]{isabelle-ref} for more information.  The
wenzelm@7321
   537
  modifier arguments correspond to those given in \S\ref{sec:simp} and
wenzelm@7905
   538
  \S\ref{sec:classical-auto}.  Just note that the ones related to the
wenzelm@7905
   539
  Simplifier are prefixed by \railtoken{simp} here.
wenzelm@7987
   540
  
wenzelm@7987
   541
  Facts provided by forward chaining are inserted into the goal before doing
wenzelm@7987
   542
  the search.  The ``!''~argument causes the full context of assumptions to be
wenzelm@7987
   543
  included as well.
wenzelm@7321
   544
\end{descr}
wenzelm@7321
   545
wenzelm@7987
   546
wenzelm@8483
   547
\subsection{Declaring rules}\label{sec:classical-mod}
wenzelm@7135
   548
wenzelm@7391
   549
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
wenzelm@7391
   550
\indexisaratt{iff}\indexisaratt{delrule}
wenzelm@7321
   551
\begin{matharray}{rcl}
wenzelm@7321
   552
  intro & : & \isaratt \\
wenzelm@7321
   553
  elim & : & \isaratt \\
wenzelm@7321
   554
  dest & : & \isaratt \\
wenzelm@7391
   555
  iff & : & \isaratt \\
wenzelm@7321
   556
  delrule & : & \isaratt \\
wenzelm@7321
   557
\end{matharray}
wenzelm@7135
   558
wenzelm@7321
   559
\begin{rail}
wenzelm@8203
   560
  ('intro' | 'elim' | 'dest') (() | '?' | '??')
wenzelm@7321
   561
  ;
wenzelm@7321
   562
\end{rail}
wenzelm@7135
   563
wenzelm@7321
   564
\begin{descr}
wenzelm@8517
   565
\item [$intro$, $elim$, and $dest$] declare introduction, elimination, and
wenzelm@8517
   566
  destruct rules, respectively.  By default, rules are considered as
wenzelm@8517
   567
  \emph{safe}, while a single ``?'' classifies as \emph{unsafe}, and ``??'' as
wenzelm@8517
   568
  \emph{extra} (i.e.\ not applied in the search-oriented automated methods,
wenzelm@8517
   569
  but only in single-step methods such as $rule$).
wenzelm@7335
   570
  
wenzelm@7391
   571
\item [$iff$] declares equations both as rewrite rules for the simplifier and
wenzelm@7391
   572
  classical reasoning rules.
wenzelm@7391
   573
wenzelm@7335
   574
\item [$delrule$] deletes introduction or elimination rules from the context.
wenzelm@7335
   575
  Note that destruction rules would have to be turned into elimination rules
wenzelm@7321
   576
  first, e.g.\ by using the $elimify$ attribute.
wenzelm@7321
   577
\end{descr}
wenzelm@7135
   578
wenzelm@8203
   579
wenzelm@7135
   580
%%% Local Variables: 
wenzelm@7135
   581
%%% mode: latex
wenzelm@7135
   582
%%% TeX-master: "isar-ref"
wenzelm@7135
   583
%%% End: