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