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