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