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: