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