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