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: