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: