doc-src/IsarRef/generic.tex
 author wenzelm Sun Oct 31 15:20:35 1999 +0100 (1999-10-31) changeset 7987 d9aef93c0e32 parent 7981 5120a2a15d06 child 7990 0a604b2fc2b1 permissions -rw-r--r--
tuned;
     1

     2 \chapter{Generic Tools and Packages}\label{ch:gen-tools}

     3

     4 \section{Basic proof methods}\label{sec:pure-meth}

     5

     6 \indexisarmeth{fail}\indexisarmeth{succeed}\indexisarmeth{$-$}\indexisarmeth{assumption}

     7 \indexisarmeth{fold}\indexisarmeth{unfold}

     8 \indexisarmeth{rule}\indexisarmeth{erule}

     9 \begin{matharray}{rcl}

    10   - & : & \isarmeth \\

    11   assumption & : & \isarmeth \\

    12   rule & : & \isarmeth \\

    13   erule^* & : & \isarmeth \\[0.5ex]

    14   fold & : & \isarmeth \\

    15   unfold & : & \isarmeth \\[0.5ex]

    16   succeed & : & \isarmeth \\

    17   fail & : & \isarmeth \\

    18 \end{matharray}

    19

    20 \begin{rail}

    21   ('fold' | 'unfold' | 'rule' | 'erule') thmrefs

    22   ;

    23 \end{rail}

    24

    25 \begin{descr}

    26 \item [$-$''] does nothing but insert the forward chaining facts as premises

    27   into the goal.  Note that command $\PROOFNAME$ without any method actually

    28   performs a single reduction step using the $rule$ method (see below); thus a

    29   plain \emph{do-nothing} proof step would be $\PROOF{-}$ rather than

    30   $\PROOFNAME$ alone.

    31 \item [$assumption$] solves some goal by assumption.  Any facts given are

    32   guaranteed to participate in the refinement.  Note that $\DOT$'' (dot)

    33   abbreviates $\BY{assumption}$.

    34 \item [$rule~thms$] applies some rule given as argument in backward manner;

    35   facts are used to reduce the rule before applying it to the goal.  Thus

    36   $rule$ without facts is plain \emph{introduction}, while with facts it

    37   becomes a (generalized) \emph{elimination}.

    38

    39   Note that the classical reasoner introduces another version of $rule$ that

    40   is able to pick appropriate rules automatically, whenever $thms$ are omitted

    41   (see \S\ref{sec:classical-basic}); that method is the default for

    42   $\PROOFNAME$ steps.  Note that $\DDOT$'' (double-dot) abbreviates

    43   $\BY{default}$.

    44 \item [$erule~thms$] is similar to $rule$, but applies rules by

    45   elim-resolution.  This is an improper method, mainly for experimentation and

    46   porting of old scripts.  Actual elimination proofs are usually done with

    47   $rule$ (single step, involving facts) or $elim$ (repeated steps, see

    48   \S\ref{sec:classical-basic}).

    49 \item [$unfold~thms$ and $fold~thms$] expand and fold back again the given

    50   meta-level definitions throughout all goals; any facts provided are inserted

    51   into the goal and subject to rewriting as well.

    52 \item [$succeed$] yields a single (unchanged) result; it is the identity of

    53   the \texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}).

    54 \item [$fail$] yields an empty result sequence; it is the identity of the

    55   \texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}).

    56 \end{descr}

    57

    58

    59 \section{Miscellaneous attributes}

    60

    61 \indexisaratt{tag}\indexisaratt{untag}\indexisaratt{COMP}\indexisaratt{RS}

    62 \indexisaratt{OF}\indexisaratt{where}\indexisaratt{of}\indexisaratt{standard}

    63 \indexisaratt{elimify}\indexisaratt{transfer}\indexisaratt{export}

    64 \begin{matharray}{rcl}

    65   tag & : & \isaratt \\

    66   untag & : & \isaratt \\[0.5ex]

    67   OF & : & \isaratt \\

    68   RS & : & \isaratt \\

    69   COMP & : & \isaratt \\[0.5ex]

    70   of & : & \isaratt \\

    71   where & : & \isaratt \\[0.5ex]

    72   standard & : & \isaratt \\

    73   elimify & : & \isaratt \\

    74   export^* & : & \isaratt \\

    75   transfer & : & \isaratt \\

    76 \end{matharray}

    77

    78 \begin{rail}

    79   ('tag' | 'untag') (nameref+)

    80   ;

    81   'OF' thmrefs

    82   ;

    83   ('RS' | 'COMP') nat? thmref

    84   ;

    85   'of' (inst * ) ('concl' ':' (inst * ))?

    86   ;

    87   'where' (name '=' term * 'and')

    88   ;

    89

    90   inst: underscore | term

    91   ;

    92 \end{rail}

    93

    94 \begin{descr}

    95 \item [$tag~tags$ and $untag~tags$] add and remove $tags$ of the theorem,

    96   respectively.  Tags may be any list of strings that serve as comment for

    97   some tools (e.g.\ $\LEMMANAME$ causes the tag $lemma$'' to be added to the

    98   result).

    99 \item [$OF~thms$, $RS~n~thm$, and $COMP~n~thm$] compose rules.  $OF$ applies

   100   $thms$ in parallel (cf.\ \texttt{MRS} in \cite[\S5]{isabelle-ref}, but note

   101   the reversed order).  Note that premises may be skipped by including

   102   $\_$'' (underscore) as argument.

   103

   104   $RS$ resolves with the $n$-th premise of $thm$; $COMP$ is a version of $RS$

   105   that skips the automatic lifting process that is normally intended (cf.\

   106   \texttt{RS} and \texttt{COMP} in \cite[\S5]{isabelle-ref}).

   107

   108 \item [$of~\vec t$ and $where~\vec x = \vec t$] perform positional and named

   109   instantiation, respectively.  The terms given in $of$ are substituted for

   110   any schematic variables occurring in a theorem from left to right;

   111   \texttt{_}'' (underscore) indicates to skip a position.

   112

   113 \item [$standard$] puts a theorem into the standard form of object-rules, just

   114   as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).

   115

   116 \item [$elimify$] turns an destruction rule into an elimination, just as the

   117   ML function \texttt{make\_elim} (see \cite{isabelle-ref}).

   118

   119 \item [$export$] lifts a local result out of the current proof context,

   120   generalizing all fixed variables and discharging all assumptions.  Note that

   121   (partial) export is usually done automatically behind the scenes.  This

   122   attribute is mainly for experimentation.

   123

   124 \item [$transfer$] promotes a theorem to the current theory context, which has

   125   to enclose the former one.  Normally, this is done automatically when rules

   126   are joined by inference.

   127

   128 \end{descr}

   129

   130

   131 \section{Calculational proof}\label{sec:calculation}

   132

   133 \indexisarcmd{also}\indexisarcmd{finally}\indexisaratt{trans}

   134 \begin{matharray}{rcl}

   135   \isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\

   136   \isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\

   137   trans & : & \isaratt \\

   138 \end{matharray}

   139

   140 Calculational proof is forward reasoning with implicit application of

   141 transitivity rules (such those of $=$, $\le$, $<$).  Isabelle/Isar maintains

   142 an auxiliary register $calculation$\indexisarthm{calculation} for accumulating

   143 results obtained by transitivity composed with the current result.  Command

   144 $\ALSO$ updates $calculation$ involving $this$, while $\FINALLY$ exhibits the

   145 final $calculation$ by forward chaining towards the next goal statement.  Both

   146 commands require valid current facts, i.e.\ may occur only after commands that

   147 produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or some finished proof of

   148 $\HAVENAME$, $\SHOWNAME$ etc.

   149

   150 Also note that the automatic term abbreviation $\dots$'' has its canonical

   151 application with calculational proofs.  It automatically refers to the

   152 argument\footnote{The argument of a curried infix expression is its right-hand

   153   side.} of the preceding statement.

   154

   155 Isabelle/Isar calculations are implicitly subject to block structure in the

   156 sense that new threads of calculational reasoning are commenced for any new

   157 block (as opened by a local goal, for example).  This means that, apart from

   158 being able to nest calculations, there is no separate \emph{begin-calculation}

   159 command required.

   160

   161 \begin{rail}

   162   ('also' | 'finally') transrules? comment?

   163   ;

   164   'trans' (() | 'add' ':' | 'del' ':') thmrefs

   165   ;

   166

   167   transrules: '(' thmrefs ')' interest?

   168   ;

   169 \end{rail}

   170

   171 \begin{descr}

   172 \item [$\ALSO~(thms)$] maintains the auxiliary $calculation$ register as

   173   follows.  The first occurrence of $\ALSO$ in some calculational thread

   174   initializes $calculation$ by $this$. Any subsequent $\ALSO$ on the same

   175   level of block-structure updates $calculation$ by some transitivity rule

   176   applied to $calculation$ and $this$ (in that order).  Transitivity rules are

   177   picked from the current context plus those given as $thms$ (the latter have

   178   precedence).

   179

   180 \item [$\FINALLY~(thms)$] maintaining $calculation$ in the same way as

   181   $\ALSO$, and concludes the current calculational thread.  The final result

   182   is exhibited as fact for forward chaining towards the next goal. Basically,

   183   $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$.  Note that

   184   $\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and

   185   $\FINALLY~\HAVE{}{\phi}~\DOT$'' are typical idioms for concluding

   186   calculational proofs.

   187

   188 \item [$trans$] maintains the set of transitivity rules of the theory or proof

   189   context, by adding or deleting theorems (the default is to add).

   190 \end{descr}

   191

   192 %FIXME

   193 %See theory \texttt{HOL/Isar_examples/Group} for a simple application of

   194 %calculations for basic equational reasoning.

   195 %\texttt{HOL/Isar_examples/KnasterTarski} involves a few more advanced

   196 %calculational steps in combination with natural deduction.

   197

   198

   199 \section{Axiomatic Type Classes}\label{sec:axclass}

   200

   201 \indexisarcmd{axclass}\indexisarcmd{instance}\indexisarmeth{intro-classes}

   202 \begin{matharray}{rcl}

   203   \isarcmd{axclass} & : & \isartrans{theory}{theory} \\

   204   \isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\

   205   intro_classes & : & \isarmeth \\

   206 \end{matharray}

   207

   208 Axiomatic type classes are provided by Isabelle/Pure as a \emph{definitional}

   209 interface to type classes (cf.~\S\ref{sec:classes}).  Thus any object logic

   210 may make use of this light-weight mechanism of abstract theories.  See

   211 \cite{Wenzel:1997:TPHOL} for more information.  There is also a tutorial on

   212 \emph{Using Axiomatic Type Classes in Isabelle} that is part of the standard

   213 Isabelle documentation.

   214 %FIXME cite

   215

   216 \begin{rail}

   217   'axclass' classdecl (axmdecl prop comment? +)

   218   ;

   219   'instance' (nameref '<' nameref | nameref '::' simplearity) comment?

   220   ;

   221 \end{rail}

   222

   223 \begin{descr}

   224 \item [$\isarkeyword{axclass}~c < \vec c~axms$] defines an axiomatic type

   225   class as the intersection of existing classes, with additional axioms

   226   holding.  Class axioms may not contain more than one type variable.  The

   227   class axioms (with implicit sort constraints added) are bound to the given

   228   names.  Furthermore a class introduction rule is generated, which is

   229   employed by method $intro_classes$ to support instantiation proofs of this

   230   class.

   231

   232 \item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~t ::   233 (\vec s)c$] setup up a goal stating the class relation or type arity.  The

   234   proof would usually proceed by $intro_classes$, and then establish the

   235   characteristic theorems of the type classes involved.  After finishing the

   236   proof, the theory will be augmented by a type signature declaration

   237   corresponding to the resulting theorem.

   238 \item [$intro_classes$] repeatedly expands all class introduction rules of

   239   this theory.

   240 \end{descr}

   241

   242 %FIXME

   243 %See theory \texttt{HOL/Isar_examples/Group} for a simple example of using

   244 %axiomatic type classes, including instantiation proofs.

   245

   246

   247 \section{The Simplifier}

   248

   249 \subsection{Simplification methods}\label{sec:simp}

   250

   251 \indexisarmeth{simp}

   252 \begin{matharray}{rcl}

   253   simp & : & \isarmeth \\

   254 \end{matharray}

   255

   256 \begin{rail}

   257   'simp' ('!' ?) (simpmod * )

   258   ;

   259

   260   simpmod: ('add' | 'del' | 'only' | 'other') ':' thmrefs

   261   ;

   262 \end{rail}

   263

   264 \begin{descr}

   265 \item [$simp$] invokes Isabelle's simplifier, after modifying the context by

   266   adding or deleting rules as specified.  The \railtoken{only} modifier first

   267   removes all other rewrite rules and congruences, and then is like

   268   \railtoken{add}.  In contrast, \railtoken{other} ignores its arguments;

   269   nevertheless there may be side-effects on the context via

   270   attributes.\footnote{This provides a back door for arbitrary context

   271     manipulation.}

   272

   273   The $simp$ method is based on \texttt{asm_full_simp_tac}

   274   \cite[\S10]{isabelle-ref}, but is much better behaved in practice.  Just the

   275   local premises of the actual goal are involved by default.  Additional facts

   276   may be inserted via forward-chaining (using $\THEN$, $\FROMNAME$ etc.).  The

   277   full context of assumptions is only included in the $simp!$ version, which

   278   should be used with care.

   279 \end{descr}

   280

   281 \subsection{Modifying the context}

   282

   283 \indexisaratt{simp}

   284 \begin{matharray}{rcl}

   285   simp & : & \isaratt \\

   286 \end{matharray}

   287

   288 \begin{rail}

   289   'simp' (() | 'add' | 'del')

   290   ;

   291 \end{rail}

   292

   293 \begin{descr}

   294 \item [$simp$] adds or deletes rules from the theory or proof context (the

   295   default is to add).

   296 \end{descr}

   297

   298

   299 \subsection{Forward simplification}

   300

   301 \indexisaratt{simplify}\indexisaratt{asm-simplify}

   302 \indexisaratt{full-simplify}\indexisaratt{asm-full-simplify}

   303 \begin{matharray}{rcl}

   304   simplify & : & \isaratt \\

   305   asm_simplify & : & \isaratt \\

   306   full_simplify & : & \isaratt \\

   307   asm_full_simplify & : & \isaratt \\

   308 \end{matharray}

   309

   310 These attributes provide forward rules for simplification, which should be

   311 used only very rarely.  There are no separate options for adding or deleting

   312 simplification rules locally.

   313

   314 See the ML functions of the same name in \cite[\S10]{isabelle-ref} for more

   315 information.

   316

   317

   318 \section{The Classical Reasoner}

   319

   320 \subsection{Basic methods}\label{sec:classical-basic}

   321

   322 \indexisarmeth{rule}\indexisarmeth{intro}

   323 \indexisarmeth{elim}\indexisarmeth{default}\indexisarmeth{contradiction}

   324 \begin{matharray}{rcl}

   325   rule & : & \isarmeth \\

   326   intro & : & \isarmeth \\

   327   elim & : & \isarmeth \\

   328   contradiction & : & \isarmeth \\

   329 \end{matharray}

   330

   331 \begin{rail}

   332   ('rule' | 'intro' | 'elim') thmrefs

   333   ;

   334 \end{rail}

   335

   336 \begin{descr}

   337 \item [$rule$] as offered by the classical reasoner is a refinement over the

   338   primitive one (see \S\ref{sec:pure-meth}).  In case that no rules are

   339   provided as arguments, it automatically determines elimination and

   340   introduction rules from the context (see also \S\ref{sec:classical-mod}).

   341   In that form it is the default method for basic proof steps, such as

   342   $\PROOFNAME$ and $\DDOT$'' (two dots).

   343

   344 \item [$intro$ and $elim$] repeatedly refine some goal by intro- or

   345   elim-resolution, after having inserted any facts.  Omitting the arguments

   346   refers to any suitable rules from the context, otherwise only the explicitly

   347   given ones may be applied.  The latter form admits better control of what

   348   actually happens, thus it is very appropriate as an initial method for

   349   $\PROOFNAME$ that splits up certain connectives of the goal, before entering

   350   the actual sub-proof.

   351

   352 \item [$contradiction$] solves some goal by contradiction, deriving any result

   353   from both $\neg A$ and $A$.  Facts, which are guaranteed to participate, may

   354   appear in either order.

   355 \end{descr}

   356

   357

   358 \subsection{Automated methods}\label{sec:classical-auto}

   359

   360 \indexisarmeth{blast}

   361 \indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{slow}\indexisarmeth{slow-best}

   362 \begin{matharray}{rcl}

   363  blast & : & \isarmeth \\

   364  fast & : & \isarmeth \\

   365  best & : & \isarmeth \\

   366  slow & : & \isarmeth \\

   367  slow_best & : & \isarmeth \\

   368 \end{matharray}

   369

   370 \railalias{slowbest}{slow\_best}

   371 \railterm{slowbest}

   372

   373 \begin{rail}

   374   'blast' ('!' ?) nat? (clamod * )

   375   ;

   376   ('fast' | 'best' | 'slow' | slowbest) ('!' ?) (clamod * )

   377   ;

   378

   379   clamod: (('intro' | 'elim' | 'dest') (() | '!' | '!!') | 'del') ':' thmrefs

   380   ;

   381 \end{rail}

   382

   383 \begin{descr}

   384 \item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac}

   385   in \cite[\S11]{isabelle-ref}).  The optional argument specifies a

   386   user-supplied search bound (default 20).

   387 \item [$fast$, $best$, $slow$, $slow_best$] refer to the generic classical

   388   reasoner (see \cite[\S11]{isabelle-ref}, tactic \texttt{fast_tac} etc).

   389 \end{descr}

   390

   391 Any of above methods support additional modifiers of the context of classical

   392 rules.  There semantics is analogous to the attributes given in

   393 \S\ref{sec:classical-mod}.  Facts provided by forward chaining are inserted

   394 into the goal before doing the search.  The !''~argument causes the full

   395 context of assumptions to be included as well.\footnote{This is slightly less

   396   hazardous than for the Simplifier (see \S\ref{sec:simp}).}

   397

   398

   399 \subsection{Combined automated methods}

   400

   401 \indexisarmeth{auto}\indexisarmeth{force}

   402 \begin{matharray}{rcl}

   403   force & : & \isarmeth \\

   404   auto & : & \isarmeth \\

   405 \end{matharray}

   406

   407 \begin{rail}

   408   ('force' | 'auto') ('!' ?) (clasimpmod * )

   409   ;

   410

   411   clasimpmod: ('simp' ('add' | 'del' | 'only') | 'other' |

   412     (('intro' | 'elim' | 'dest') (() | '!' | '!!') | 'del')) ':' thmrefs

   413 \end{rail}

   414

   415 \begin{descr}

   416 \item [$force$ and $auto$] provide access to Isabelle's combined

   417   simplification and classical reasoning tactics.  See \texttt{force_tac} and

   418   \texttt{auto_tac} in \cite[\S11]{isabelle-ref} for more information.  The

   419   modifier arguments correspond to those given in \S\ref{sec:simp} and

   420   \S\ref{sec:classical-auto}.  Just note that the ones related to the

   421   Simplifier are prefixed by \railtoken{simp} here.

   422

   423   Facts provided by forward chaining are inserted into the goal before doing

   424   the search.  The !''~argument causes the full context of assumptions to be

   425   included as well.

   426 \end{descr}

   427

   428

   429 \subsection{Modifying the context}\label{sec:classical-mod}

   430

   431 \indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}

   432 \indexisaratt{iff}\indexisaratt{delrule}

   433 \begin{matharray}{rcl}

   434   intro & : & \isaratt \\

   435   elim & : & \isaratt \\

   436   dest & : & \isaratt \\

   437   iff & : & \isaratt \\

   438   delrule & : & \isaratt \\

   439 \end{matharray}

   440

   441 \begin{rail}

   442   ('intro' | 'elim' | 'dest') (() | '!' | '!!')

   443   ;

   444 \end{rail}

   445

   446 \begin{descr}

   447 \item [$intro$, $elim$, $dest$] add introduction, elimination, destruct rules,

   448   respectively.  By default, rules are considered as \emph{safe}, while a

   449   single !'' classifies as \emph{unsafe}, and !!'' as \emph{extra} (i.e.\

   450   not applied in the search-oriented automated methods, but only $rule$).

   451

   452 \item [$iff$] declares equations both as rewrite rules for the simplifier and

   453   classical reasoning rules.

   454

   455 \item [$delrule$] deletes introduction or elimination rules from the context.

   456   Note that destruction rules would have to be turned into elimination rules

   457   first, e.g.\ by using the $elimify$ attribute.

   458 \end{descr}

   459

   460 %%% Local Variables:

   461 %%% mode: latex

   462 %%% TeX-master: "isar-ref"

   463 %%% End: