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: