doc-src/IsarRef/generic.tex
 author wenzelm Wed Aug 25 20:46:40 1999 +0200 (1999-08-25) changeset 7356 1714c91b8729 parent 7335 abba35b98892 child 7391 b7ca64c8fa64 permissions -rw-r--r--
expand_classes renamed to intro_classes;
     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$\indexisarreg{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}\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 only very rarely.  See the ML functions of the same name in

   307 \cite[\S10]{isabelle-ref} for more information.

   308

   309

   310 \section{The Classical Reasoner}

   311

   312 \subsection{Basic 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, such as

   333   $\PROOFNAME$ and $\DDOT$'' (two dots).

   334

   335 \item [Methods $intro$ and $elim$] repeatedly refine some goal by intro- or

   336   elim-resolution, after having inserted the facts.  Omitting the arguments

   337   refers to any suitable rules from the context, otherwise only the explicitly

   338   given ones may be applied.  The latter form admits better control of what

   339   actually happens, thus it is very appropriate as an initial method for

   340   $\PROOFNAME$ that splits up certain connectives of the goal, before entering

   341   the sub-proof.

   342

   343 \item [Method $contradiction$] solves some goal by contradiction: both $A$ and

   344   $\neg A$ have to be present in the assumptions.

   345 \end{descr}

   346

   347

   348 \subsection{Automatic methods}\label{sec:classical-auto}

   349

   350 \indexisarmeth{blast}

   351 \indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{slow}\indexisarmeth{slow_best}

   352 \begin{matharray}{rcl}

   353  blast & : & \isarmeth \\

   354  fast & : & \isarmeth \\

   355  best & : & \isarmeth \\

   356  slow & : & \isarmeth \\

   357  slow_best & : & \isarmeth \\

   358 \end{matharray}

   359

   360 \railalias{slowbest}{slow\_best}

   361 \railterm{slowbest}

   362

   363 \begin{rail}

   364   'blast' nat? (clamod * )

   365   ;

   366   ('fast' | 'best' | 'slow' | slowbest) (clamod * )

   367   ;

   368

   369   clamod: (('intro' | 'elim' | 'dest') (() | '!' | '!!') | 'del') ':' thmrefs

   370   ;

   371 \end{rail}

   372

   373 \begin{descr}

   374 \item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac}

   375   in \cite[\S11]{isabelle-ref}).  The optional argument specifies a

   376   user-supplied search bound (default 20).

   377 \item [$fast$, $best$, $slow$, $slow_best$] refer to the generic classical

   378   reasoner (see \cite[\S11]{isabelle-ref}, tactic \texttt{fast_tac} etc).

   379 \end{descr}

   380

   381 Any of above methods support additional modifiers of the context of classical

   382 rules.  There semantics is analogous to the attributes given in

   383 \S\ref{sec:classical-mod}.

   384

   385

   386 \subsection{Combined automatic methods}

   387

   388 \indexisarmeth{auto}\indexisarmeth{force}

   389 \begin{matharray}{rcl}

   390   force & : & \isarmeth \\

   391   auto & : & \isarmeth \\

   392 \end{matharray}

   393

   394 \begin{rail}

   395   ('force' | 'auto') (clasimpmod * )

   396   ;

   397

   398   clasimpmod: ('simp' ('add' | 'del' | 'only') | other |

   399     (('intro' | 'elim' | 'dest') (() | '!' | '!!') | 'del')) ':' thmrefs

   400 \end{rail}

   401

   402 \begin{descr}

   403 \item [$force$ and $auto$] provide access to Isabelle's combined

   404   simplification and classical reasoning tactics.  See \texttt{force_tac} and

   405   \texttt{auto_tac} in \cite[\S11]{isabelle-ref} for more information.  The

   406   modifier arguments correspond to those given in \S\ref{sec:simp} and

   407   \S\ref{sec:classical-auto}.  Note that the ones related to the Simplifier

   408   are prefixed by \railtoken{simp} here.

   409 \end{descr}

   410

   411 \subsection{Modifying the context}\label{sec:classical-mod}

   412

   413 \indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}\indexisaratt{delrule}

   414 \begin{matharray}{rcl}

   415   intro & : & \isaratt \\

   416   elim & : & \isaratt \\

   417   dest & : & \isaratt \\

   418   delrule & : & \isaratt \\

   419 \end{matharray}

   420

   421 \begin{rail}

   422   ('intro' | 'elim' | 'dest') (() | '!' | '!!')

   423   ;

   424 \end{rail}

   425

   426 \begin{descr}

   427 \item [$intro$, $elim$, $dest$] add introduction, elimination, destruct rules,

   428   respectively.  By default, rules are considered as \emph{safe}, while a

   429   single !'' classifies as \emph{unsafe}, and !!'' as \emph{extra} (i.e.\

   430   not applied in the search-oriented automatic methods).

   431

   432 \item [$delrule$] deletes introduction or elimination rules from the context.

   433   Note that destruction rules would have to be turned into elimination rules

   434   first, e.g.\ by using the $elimify$ attribute.

   435 \end{descr}

   436

   437

   438 %%% Local Variables:

   439 %%% mode: latex

   440 %%% TeX-master: "isar-ref"

   441 %%% End: