doc-src/IsarRef/generic.tex
author wenzelm
Mon Feb 07 18:38:51 2000 +0100 (2000-02-07)
changeset 8203 2fcc6017cb72
parent 8195 af2575a5c5ae
child 8483 b437907f9b26
permissions -rw-r--r--
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
     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{$-$}
     7 \indexisarmeth{assumption}\indexisarmeth{this}
     8 \indexisarmeth{fold}\indexisarmeth{unfold}
     9 \indexisarmeth{rule}\indexisarmeth{erule}
    10 \begin{matharray}{rcl}
    11   - & : & \isarmeth \\
    12   assumption & : & \isarmeth \\
    13   this & : & \isarmeth \\
    14   rule & : & \isarmeth \\
    15   erule^* & : & \isarmeth \\[0.5ex]
    16   fold & : & \isarmeth \\
    17   unfold & : & \isarmeth \\[0.5ex]
    18   succeed & : & \isarmeth \\
    19   fail & : & \isarmeth \\
    20 \end{matharray}
    21 
    22 \begin{rail}
    23   ('fold' | 'unfold' | 'rule' | 'erule') thmrefs
    24   ;
    25 \end{rail}
    26 
    27 \begin{descr}
    28 \item [``$-$''] does nothing but insert the forward chaining facts as premises
    29   into the goal.  Note that command $\PROOFNAME$ without any method actually
    30   performs a single reduction step using the $rule$ method (see below); thus a
    31   plain \emph{do-nothing} proof step would be $\PROOF{-}$ rather than
    32   $\PROOFNAME$ alone.
    33 \item [$assumption$] solves some goal by assumption.  Any facts given are
    34   guaranteed to participate in the refinement.
    35 \item [$this$] applies the current facts directly as rules.  Note that
    36   ``$\DOT$'' (dot) abbreviates $\BY{this}$.
    37 \item [$rule~thms$] applies some rule given as argument in backward manner;
    38   facts are used to reduce the rule before applying it to the goal.  Thus
    39   $rule$ without facts is plain \emph{introduction}, while with facts it
    40   becomes a (generalized) \emph{elimination}.
    41   
    42   Note that the classical reasoner introduces another version of $rule$ that
    43   is able to pick appropriate rules automatically, whenever $thms$ are omitted
    44   (see \S\ref{sec:classical-basic}); that method is the default for
    45   $\PROOFNAME$ steps.  Note that ``$\DDOT$'' (double-dot) abbreviates
    46   $\BY{default}$.
    47 \item [$erule~thms$] is similar to $rule$, but applies rules by
    48   elim-resolution.  This is an improper method, mainly for experimentation and
    49   porting of old scripts.  Actual elimination proofs are usually done with
    50   $rule$ (single step, involving facts) or $elim$ (repeated steps, see
    51   \S\ref{sec:classical-basic}).
    52 \item [$unfold~thms$ and $fold~thms$] expand and fold back again the given
    53   meta-level definitions throughout all goals; any facts provided are inserted
    54   into the goal and subject to rewriting as well.
    55 \item [$succeed$] yields a single (unchanged) result; it is the identity of
    56   the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
    57 \item [$fail$] yields an empty result sequence; it is the identity of the
    58   ``\texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
    59 \end{descr}
    60 
    61 
    62 \section{Miscellaneous attributes}
    63 
    64 \indexisaratt{tag}\indexisaratt{untag}\indexisaratt{COMP}\indexisaratt{RS}
    65 \indexisaratt{OF}\indexisaratt{where}\indexisaratt{of}\indexisaratt{standard}
    66 \indexisaratt{elimify}\indexisaratt{transfer}\indexisaratt{export}
    67 \indexisaratt{unfold}\indexisaratt{fold}
    68 \begin{matharray}{rcl}
    69   tag & : & \isaratt \\
    70   untag & : & \isaratt \\[0.5ex]
    71   OF & : & \isaratt \\
    72   RS & : & \isaratt \\
    73   COMP & : & \isaratt \\[0.5ex]
    74   of & : & \isaratt \\
    75   where & : & \isaratt \\[0.5ex]
    76   unfold & : & \isaratt \\
    77   fold & : & \isaratt \\[0.5ex]
    78   standard & : & \isaratt \\
    79   elimify & : & \isaratt \\
    80   export^* & : & \isaratt \\
    81   transfer & : & \isaratt \\[0.5ex]
    82 \end{matharray}
    83 
    84 \begin{rail}
    85   ('tag' | 'untag') (nameref+)
    86   ;
    87   'OF' thmrefs
    88   ;
    89   ('RS' | 'COMP') nat? thmref
    90   ;
    91   'of' (inst * ) ('concl' ':' (inst * ))?
    92   ;
    93   'where' (name '=' term * 'and')
    94   ;
    95   ('unfold' | 'fold') thmrefs
    96   ;
    97 
    98   inst: underscore | term
    99   ;
   100 \end{rail}
   101 
   102 \begin{descr}
   103 \item [$tag~tags$ and $untag~tags$] add and remove $tags$ of the theorem,
   104   respectively.  Tags may be any list of strings that serve as comment for
   105   some tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the
   106   result).
   107 \item [$OF~thms$, $RS~n~thm$, and $COMP~n~thm$] compose rules.  $OF$ applies
   108   $thms$ in parallel (cf.\ \texttt{MRS} in \cite[\S5]{isabelle-ref}, but note
   109   the reversed order).  Note that premises may be skipped by including
   110   ``$\_$'' (underscore) as argument.
   111   
   112   $RS$ resolves with the $n$-th premise of $thm$; $COMP$ is a version of $RS$
   113   that skips the automatic lifting process that is normally intended (cf.\ 
   114   \texttt{RS} and \texttt{COMP} in \cite[\S5]{isabelle-ref}).
   115   
   116 \item [$of~\vec t$ and $where~\vec x = \vec t$] perform positional and named
   117   instantiation, respectively.  The terms given in $of$ are substituted for
   118   any schematic variables occurring in a theorem from left to right;
   119   ``\texttt{_}'' (underscore) indicates to skip a position.  Arguments
   120   following a ``$concl\colon$'' specification refer to positions of the
   121   conclusion of a rule.
   122   
   123 \item [$unfold~thms$ and $fold~thms$] expand and fold back again the given
   124   meta-level definitions throughout a rule.
   125  
   126 \item [$standard$] puts a theorem into the standard form of object-rules, just
   127   as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).
   128   
   129 \item [$elimify$] turns an destruction rule into an elimination, just as the
   130   ML function \texttt{make\_elim} (see \cite{isabelle-ref}).
   131   
   132 \item [$export$] lifts a local result out of the current proof context,
   133   generalizing all fixed variables and discharging all assumptions.  Note that
   134   (partial) export is usually done automatically behind the scenes.  This
   135   attribute is mainly for experimentation.
   136   
   137 \item [$transfer$] promotes a theorem to the current theory context, which has
   138   to enclose the former one.  Normally, this is done automatically when rules
   139   are joined by inference.
   140 
   141 \end{descr}
   142 
   143 
   144 \section{Calculational proof}\label{sec:calculation}
   145 
   146 \indexisarcmd{also}\indexisarcmd{finally}\indexisaratt{trans}
   147 \begin{matharray}{rcl}
   148   \isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\
   149   \isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\
   150   trans & : & \isaratt \\
   151 \end{matharray}
   152 
   153 Calculational proof is forward reasoning with implicit application of
   154 transitivity rules (such those of $=$, $\le$, $<$).  Isabelle/Isar maintains
   155 an auxiliary register $calculation$\indexisarthm{calculation} for accumulating
   156 results obtained by transitivity composed with the current result.  Command
   157 $\ALSO$ updates $calculation$ involving $this$, while $\FINALLY$ exhibits the
   158 final $calculation$ by forward chaining towards the next goal statement.  Both
   159 commands require valid current facts, i.e.\ may occur only after commands that
   160 produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or some finished proof of
   161 $\HAVENAME$, $\SHOWNAME$ etc.
   162 
   163 Also note that the automatic term abbreviation ``$\dots$'' has its canonical
   164 application with calculational proofs.  It automatically refers to the
   165 argument\footnote{The argument of a curried infix expression is its right-hand
   166   side.} of the preceding statement.
   167 
   168 Isabelle/Isar calculations are implicitly subject to block structure in the
   169 sense that new threads of calculational reasoning are commenced for any new
   170 block (as opened by a local goal, for example).  This means that, apart from
   171 being able to nest calculations, there is no separate \emph{begin-calculation}
   172 command required.
   173 
   174 \begin{rail}
   175   ('also' | 'finally') transrules? comment?
   176   ;
   177   'trans' (() | 'add' ':' | 'del' ':') thmrefs
   178   ;
   179 
   180   transrules: '(' thmrefs ')' interest?
   181   ;
   182 \end{rail}
   183 
   184 \begin{descr}
   185 \item [$\ALSO~(thms)$] maintains the auxiliary $calculation$ register as
   186   follows.  The first occurrence of $\ALSO$ in some calculational thread
   187   initializes $calculation$ by $this$. Any subsequent $\ALSO$ on the same
   188   level of block-structure updates $calculation$ by some transitivity rule
   189   applied to $calculation$ and $this$ (in that order).  Transitivity rules are
   190   picked from the current context plus those given as $thms$ (the latter have
   191   precedence).
   192   
   193 \item [$\FINALLY~(thms)$] maintaining $calculation$ in the same way as
   194   $\ALSO$, and concludes the current calculational thread.  The final result
   195   is exhibited as fact for forward chaining towards the next goal. Basically,
   196   $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$.  Note that
   197   ``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and
   198   ``$\FINALLY~\HAVE{}{\phi}~\DOT$'' are typical idioms for concluding
   199   calculational proofs.
   200   
   201 \item [$trans$] maintains the set of transitivity rules of the theory or proof
   202   context, by adding or deleting theorems (the default is to add).
   203 \end{descr}
   204 
   205 %FIXME
   206 %See theory \texttt{HOL/Isar_examples/Group} for a simple application of
   207 %calculations for basic equational reasoning.
   208 %\texttt{HOL/Isar_examples/KnasterTarski} involves a few more advanced
   209 %calculational steps in combination with natural deduction.
   210 
   211 
   212 \section{Axiomatic Type Classes}\label{sec:axclass}
   213 
   214 \indexisarcmd{axclass}\indexisarcmd{instance}\indexisarmeth{intro-classes}
   215 \begin{matharray}{rcl}
   216   \isarcmd{axclass} & : & \isartrans{theory}{theory} \\
   217   \isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
   218   intro_classes & : & \isarmeth \\
   219 \end{matharray}
   220 
   221 Axiomatic type classes are provided by Isabelle/Pure as a \emph{definitional}
   222 interface to type classes (cf.~\S\ref{sec:classes}).  Thus any object logic
   223 may make use of this light-weight mechanism of abstract theories.  See
   224 \cite{Wenzel:1997:TPHOL} for more information.  There is also a tutorial on
   225 \emph{Using Axiomatic Type Classes in Isabelle} that is part of the standard
   226 Isabelle documentation.
   227 %FIXME cite
   228 
   229 \begin{rail}
   230   'axclass' classdecl (axmdecl prop comment? +)
   231   ;
   232   'instance' (nameref '<' nameref | nameref '::' simplearity) comment?
   233   ;
   234 \end{rail}
   235 
   236 \begin{descr}
   237 \item [$\isarkeyword{axclass}~c < \vec c~axms$] defines an axiomatic type
   238   class as the intersection of existing classes, with additional axioms
   239   holding.  Class axioms may not contain more than one type variable.  The
   240   class axioms (with implicit sort constraints added) are bound to the given
   241   names.  Furthermore a class introduction rule is generated, which is
   242   employed by method $intro_classes$ to support instantiation proofs of this
   243   class.
   244   
   245 \item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~t ::
   246   (\vec s)c$] setup up a goal stating the class relation or type arity.  The
   247   proof would usually proceed by $intro_classes$, and then establish the
   248   characteristic theorems of the type classes involved.  After finishing the
   249   proof, the theory will be augmented by a type signature declaration
   250   corresponding to the resulting theorem.
   251 \item [$intro_classes$] repeatedly expands all class introduction rules of
   252   this theory.
   253 \end{descr}
   254 
   255 %FIXME
   256 %See theory \texttt{HOL/Isar_examples/Group} for a simple example of using
   257 %axiomatic type classes, including instantiation proofs.
   258 
   259 
   260 \section{The Simplifier}
   261 
   262 \subsection{Simplification methods}\label{sec:simp}
   263 
   264 \indexisarmeth{simp}
   265 \begin{matharray}{rcl}
   266   simp & : & \isarmeth \\
   267 \end{matharray}
   268 
   269 \begin{rail}
   270   'simp' ('!' ?) (simpmod * )
   271   ;
   272 
   273   simpmod: ('add' | 'del' | 'only' | 'other') ':' thmrefs
   274   ;
   275 \end{rail}
   276 
   277 \begin{descr}
   278 \item [$simp$] invokes Isabelle's simplifier, after modifying the context by
   279   adding or deleting rules as specified.  The \railtoken{only} modifier first
   280   removes all other rewrite rules and congruences, and then is like
   281   \railtoken{add}.  In contrast, \railtoken{other} ignores its arguments;
   282   nevertheless there may be side-effects on the context via
   283   attributes.\footnote{This provides a back door for arbitrary context
   284     manipulation.}
   285   
   286   The $simp$ method is based on \texttt{asm_full_simp_tac}
   287   \cite[\S10]{isabelle-ref}, but is much better behaved in practice.  Just the
   288   local premises of the actual goal are involved by default.  Additional facts
   289   may be inserted via forward-chaining (using $\THEN$, $\FROMNAME$ etc.).  The
   290   full context of assumptions is only included in the $simp!$ version, which
   291   should be used with care.
   292 \end{descr}
   293 
   294 \subsection{Modifying the context}
   295 
   296 \indexisaratt{simp}
   297 \begin{matharray}{rcl}
   298   simp & : & \isaratt \\
   299 \end{matharray}
   300 
   301 \begin{rail}
   302   'simp' (() | 'add' | 'del')
   303   ;
   304 \end{rail}
   305 
   306 \begin{descr}
   307 \item [$simp$] adds or deletes rules from the theory or proof context (the
   308   default is to add).
   309 \end{descr}
   310 
   311 
   312 \subsection{Forward simplification}
   313 
   314 \indexisaratt{simplify}\indexisaratt{asm-simplify}
   315 \indexisaratt{full-simplify}\indexisaratt{asm-full-simplify}
   316 \begin{matharray}{rcl}
   317   simplify & : & \isaratt \\
   318   asm_simplify & : & \isaratt \\
   319   full_simplify & : & \isaratt \\
   320   asm_full_simplify & : & \isaratt \\
   321 \end{matharray}
   322 
   323 These attributes provide forward rules for simplification, which should be
   324 used only very rarely.  There are no separate options for adding or deleting
   325 simplification rules locally.
   326 
   327 See the ML functions of the same name in \cite[\S10]{isabelle-ref} for more
   328 information.
   329 
   330 
   331 \section{The Classical Reasoner}
   332 
   333 \subsection{Basic methods}\label{sec:classical-basic}
   334 
   335 \indexisarmeth{rule}\indexisarmeth{intro}
   336 \indexisarmeth{elim}\indexisarmeth{default}\indexisarmeth{contradiction}
   337 \begin{matharray}{rcl}
   338   rule & : & \isarmeth \\
   339   intro & : & \isarmeth \\
   340   elim & : & \isarmeth \\
   341   contradiction & : & \isarmeth \\
   342 \end{matharray}
   343 
   344 \begin{rail}
   345   ('rule' | 'intro' | 'elim') thmrefs
   346   ;
   347 \end{rail}
   348 
   349 \begin{descr}
   350 \item [$rule$] as offered by the classical reasoner is a refinement over the
   351   primitive one (see \S\ref{sec:pure-meth}).  In case that no rules are
   352   provided as arguments, it automatically determines elimination and
   353   introduction rules from the context (see also \S\ref{sec:classical-mod}).
   354   In that form it is the default method for basic proof steps, such as
   355   $\PROOFNAME$ and ``$\DDOT$'' (two dots).
   356   
   357 \item [$intro$ and $elim$] repeatedly refine some goal by intro- or
   358   elim-resolution, after having inserted any facts.  Omitting the arguments
   359   refers to any suitable rules from the context, otherwise only the explicitly
   360   given ones may be applied.  The latter form admits better control of what
   361   actually happens, thus it is very appropriate as an initial method for
   362   $\PROOFNAME$ that splits up certain connectives of the goal, before entering
   363   the actual sub-proof.
   364   
   365 \item [$contradiction$] solves some goal by contradiction, deriving any result
   366   from both $\neg A$ and $A$.  Facts, which are guaranteed to participate, may
   367   appear in either order.
   368 \end{descr}
   369 
   370 
   371 \subsection{Automated methods}\label{sec:classical-auto}
   372 
   373 \indexisarmeth{blast}
   374 \indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{slow}\indexisarmeth{slow-best}
   375 \begin{matharray}{rcl}
   376  blast & : & \isarmeth \\
   377  fast & : & \isarmeth \\
   378  best & : & \isarmeth \\
   379  slow & : & \isarmeth \\
   380  slow_best & : & \isarmeth \\
   381 \end{matharray}
   382 
   383 \railalias{slowbest}{slow\_best}
   384 \railterm{slowbest}
   385 
   386 \begin{rail}
   387   'blast' ('!' ?) nat? (clamod * )
   388   ;
   389   ('fast' | 'best' | 'slow' | slowbest) ('!' ?) (clamod * )
   390   ;
   391 
   392   clamod: (('intro' | 'elim' | 'dest') (() | '?' | '??') | 'del') ':' thmrefs
   393   ;
   394 \end{rail}
   395 
   396 \begin{descr}
   397 \item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac}
   398   in \cite[\S11]{isabelle-ref}).  The optional argument specifies a
   399   user-supplied search bound (default 20).
   400 \item [$fast$, $best$, $slow$, $slow_best$] refer to the generic classical
   401   reasoner (see \cite[\S11]{isabelle-ref}, tactic \texttt{fast_tac} etc).
   402 \end{descr}
   403 
   404 Any of above methods support additional modifiers of the context of classical
   405 rules.  There semantics is analogous to the attributes given in
   406 \S\ref{sec:classical-mod}.  Facts provided by forward chaining are inserted
   407 into the goal before doing the search.  The ``!''~argument causes the full
   408 context of assumptions to be included as well.\footnote{This is slightly less
   409   hazardous than for the Simplifier (see \S\ref{sec:simp}).}
   410 
   411 
   412 \subsection{Combined automated methods}
   413 
   414 \indexisarmeth{auto}\indexisarmeth{force}
   415 \begin{matharray}{rcl}
   416   force & : & \isarmeth \\
   417   auto & : & \isarmeth \\
   418 \end{matharray}
   419 
   420 \begin{rail}
   421   ('force' | 'auto') ('!' ?) (clasimpmod * )
   422   ;
   423 
   424   clasimpmod: ('simp' ('add' | 'del' | 'only') | 'other' |
   425     (('intro' | 'elim' | 'dest') (() | '?' | '??') | 'del')) ':' thmrefs
   426 \end{rail}
   427 
   428 \begin{descr}
   429 \item [$force$ and $auto$] provide access to Isabelle's combined
   430   simplification and classical reasoning tactics.  See \texttt{force_tac} and
   431   \texttt{auto_tac} in \cite[\S11]{isabelle-ref} for more information.  The
   432   modifier arguments correspond to those given in \S\ref{sec:simp} and
   433   \S\ref{sec:classical-auto}.  Just note that the ones related to the
   434   Simplifier are prefixed by \railtoken{simp} here.
   435   
   436   Facts provided by forward chaining are inserted into the goal before doing
   437   the search.  The ``!''~argument causes the full context of assumptions to be
   438   included as well.
   439 \end{descr}
   440 
   441 
   442 \subsection{Modifying the context}\label{sec:classical-mod}
   443 
   444 \indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
   445 \indexisaratt{iff}\indexisaratt{delrule}
   446 \begin{matharray}{rcl}
   447   intro & : & \isaratt \\
   448   elim & : & \isaratt \\
   449   dest & : & \isaratt \\
   450   iff & : & \isaratt \\
   451   delrule & : & \isaratt \\
   452 \end{matharray}
   453 
   454 \begin{rail}
   455   ('intro' | 'elim' | 'dest') (() | '?' | '??')
   456   ;
   457 \end{rail}
   458 
   459 \begin{descr}
   460 \item [$intro$, $elim$, $dest$] add introduction, elimination, destruct rules,
   461   respectively.  By default, rules are considered as \emph{safe}, while a
   462   single ``?'' classifies as \emph{unsafe}, and ``??'' as \emph{extra} (i.e.\ 
   463   not applied in the search-oriented automated methods, but only in
   464   single-step methods such as $rule$).
   465   
   466 \item [$iff$] declares equations both as rewrite rules for the simplifier and
   467   classical reasoning rules.
   468 
   469 \item [$delrule$] deletes introduction or elimination rules from the context.
   470   Note that destruction rules would have to be turned into elimination rules
   471   first, e.g.\ by using the $elimify$ attribute.
   472 \end{descr}
   473 
   474 
   475 %%% Local Variables: 
   476 %%% mode: latex
   477 %%% TeX-master: "isar-ref"
   478 %%% End: