doc-src/IsarRef/generic.tex
 author wenzelm Mon Aug 14 18:49:23 2000 +0200 (2000-08-14) changeset 9606 1bf495402ae9 parent 9480 7afb808b6b3e child 9614 8ca1fc75230e permissions -rw-r--r--
moved tactic emulation methods here;
renamed "res_inst_tac' etc. to 'rule_tac' etc.;
     1

     2 \chapter{Generic Tools and Packages}\label{ch:gen-tools}

     3

     4 \section{Axiomatic Type Classes}\label{sec:axclass}

     5

     6 %FIXME

     7 % - qualified names

     8 % - class intro rules;

     9 % - class axioms;

    10

    11 \indexisarcmd{axclass}\indexisarcmd{instance}\indexisarmeth{intro-classes}

    12 \begin{matharray}{rcl}

    13   \isarcmd{axclass} & : & \isartrans{theory}{theory} \\

    14   \isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\

    15   intro_classes & : & \isarmeth \\

    16 \end{matharray}

    17

    18 Axiomatic type classes are provided by Isabelle/Pure as a \emph{definitional}

    19 interface to type classes (cf.~\S\ref{sec:classes}).  Thus any object logic

    20 may make use of this light-weight mechanism of abstract theories

    21 \cite{Wenzel:1997:TPHOL}.  There is also a tutorial on using axiomatic type

    22 classes in isabelle \cite{isabelle-axclass} that is part of the standard

    23 Isabelle documentation.

    24

    25 \begin{rail}

    26   'axclass' classdecl (axmdecl prop comment? +)

    27   ;

    28   'instance' (nameref '<' nameref | nameref '::' simplearity) comment?

    29   ;

    30 \end{rail}

    31

    32 \begin{descr}

    33 \item [$\isarkeyword{axclass}~c < \vec c~axms$] defines an axiomatic type

    34   class as the intersection of existing classes, with additional axioms

    35   holding.  Class axioms may not contain more than one type variable.  The

    36   class axioms (with implicit sort constraints added) are bound to the given

    37   names.  Furthermore a class introduction rule is generated, which is

    38   employed by method $intro_classes$ to support instantiation proofs of this

    39   class.

    40

    41 \item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~t ::   42 (\vec s)c$] setup a goal stating a class relation or type arity.  The proof

    43   would usually proceed by $intro_classes$, and then establish the

    44   characteristic theorems of the type classes involved.  After finishing the

    45   proof, the theory will be augmented by a type signature declaration

    46   corresponding to the resulting theorem.

    47 \item [$intro_classes$] repeatedly expands all class introduction rules of

    48   this theory.

    49 \end{descr}

    50

    51

    52 \section{Calculational proof}\label{sec:calculation}

    53

    54 \indexisarcmd{also}\indexisarcmd{finally}

    55 \indexisarcmd{moreover}\indexisarcmd{ultimately}

    56 \indexisarcmd{print-trans-rules}\indexisaratt{trans}

    57 \begin{matharray}{rcl}

    58   \isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\

    59   \isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\

    60   \isarcmd{moreover} & : & \isartrans{proof(state)}{proof(state)} \\

    61   \isarcmd{ultimately} & : & \isartrans{proof(state)}{proof(chain)} \\

    62   \isarcmd{print_trans_rules} & : & \isarkeep{theory~|~proof} \\

    63   trans & : & \isaratt \\

    64 \end{matharray}

    65

    66 Calculational proof is forward reasoning with implicit application of

    67 transitivity rules (such those of $=$, $\le$, $<$).  Isabelle/Isar maintains

    68 an auxiliary register $calculation$\indexisarthm{calculation} for accumulating

    69 results obtained by transitivity composed with the current result.  Command

    70 $\ALSO$ updates $calculation$ involving $this$, while $\FINALLY$ exhibits the

    71 final $calculation$ by forward chaining towards the next goal statement.  Both

    72 commands require valid current facts, i.e.\ may occur only after commands that

    73 produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or some finished proof of

    74 $\HAVENAME$, $\SHOWNAME$ etc.  The $\MOREOVER$ and $\ULTIMATELY$ commands are

    75 similar to $\ALSO$ and $\FINALLY$, but only collect further results in

    76 $calculation$ without applying any rules yet.

    77

    78 Also note that the automatic term abbreviation $\dots$'' has its canonical

    79 application with calculational proofs.  It refers to the argument\footnote{The

    80   argument of a curried infix expression is its right-hand side.} of the

    81 preceding statement.

    82

    83 Isabelle/Isar calculations are implicitly subject to block structure in the

    84 sense that new threads of calculational reasoning are commenced for any new

    85 block (as opened by a local goal, for example).  This means that, apart from

    86 being able to nest calculations, there is no separate \emph{begin-calculation}

    87 command required.

    88

    89 \medskip

    90

    91 The Isar calculation proof commands may be defined as

    92 follows:\footnote{Internal bookkeeping such as proper handling of

    93   block-structure has been suppressed.}

    94 \begin{matharray}{rcl}

    95   \ALSO@0 & \equiv & \NOTE{calculation}{this} \\

    96   \ALSO@{n+1} & \equiv & \NOTE{calculation}{trans~[OF~calculation~this]} \\[0.5ex]

    97   \FINALLY & \equiv & \ALSO~\FROM{calculation} \\

    98   \MOREOVER & \equiv & \NOTE{calculation}{calculation~this} \\

    99   \ULTIMATELY & \equiv & \MOREOVER~\FROM{calculation} \\

   100 \end{matharray}

   101

   102 \begin{rail}

   103   ('also' | 'finally') transrules? comment?

   104   ;

   105   ('moreover' | 'ultimately') comment?

   106   ;

   107   'trans' (() | 'add' | 'del')

   108   ;

   109

   110   transrules: '(' thmrefs ')' interest?

   111   ;

   112 \end{rail}

   113

   114 \begin{descr}

   115 \item [$\ALSO~(\vec a)$] maintains the auxiliary $calculation$ register as

   116   follows.  The first occurrence of $\ALSO$ in some calculational thread

   117   initializes $calculation$ by $this$. Any subsequent $\ALSO$ on the same

   118   level of block-structure updates $calculation$ by some transitivity rule

   119   applied to $calculation$ and $this$ (in that order).  Transitivity rules are

   120   picked from the current context plus those given as explicit arguments (the

   121   latter have precedence).

   122

   123 \item [$\FINALLY~(\vec a)$] maintaining $calculation$ in the same way as

   124   $\ALSO$, and concludes the current calculational thread.  The final result

   125   is exhibited as fact for forward chaining towards the next goal. Basically,

   126   $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$.  Note that

   127   $\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and

   128   $\FINALLY~\HAVE{}{\phi}~\DOT$'' are typical idioms for concluding

   129   calculational proofs.

   130

   131 \item [$\MOREOVER$ and $\ULTIMATELY$] are analogous to $\ALSO$ and $\FINALLY$,

   132   but collect results only, without applying rules.

   133

   134 \item [$\isarkeyword{print_trans_rules}$] prints the list of transitivity

   135   rules declared in the current context.

   136

   137 \item [$trans$] declares theorems as transitivity rules.

   138

   139 \end{descr}

   140

   141

   142 \section{Named local contexts (cases)}\label{sec:cases}

   143

   144 \indexisarcmd{case}\indexisarcmd{print-cases}

   145 \indexisaratt{case-names}\indexisaratt{params}

   146 \begin{matharray}{rcl}

   147   \isarcmd{case} & : & \isartrans{proof(state)}{proof(state)} \\

   148   \isarcmd{print_cases}^* & : & \isarkeep{proof} \\

   149   case_names & : & \isaratt \\

   150   params & : & \isaratt \\

   151 \end{matharray}

   152

   153 Basically, Isar proof contexts are built up explicitly using commands like

   154 $\FIXNAME$, $\ASSUMENAME$ etc.\ (see \S\ref{sec:proof-context}).  In typical

   155 verification tasks this can become hard to manage, though.  In particular, a

   156 large number of local contexts may emerge from case analysis or induction over

   157 inductive sets and types.

   158

   159 \medskip

   160

   161 The $\CASENAME$ command provides a shorthand to refer to certain parts of

   162 logical context symbolically.  Proof methods may provide an environment of

   163 named cases'' of the form $c\colon \vec x, \vec \phi$.  Then the effect of

   164 $\CASE{c}$ is exactly the same as $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$.

   165

   166 It is important to note that $\CASENAME$ does \emph{not} provide any means to

   167 peek at the current goal state, which is treated as strictly non-observable in

   168 Isar!  Instead, the cases considered here usually emerge in a canonical way

   169 from certain pieces of specification that appear in the theory somewhere else

   170 (e.g.\ in an inductive definition, or recursive function).  See also

   171 \S\ref{sec:induct-method} for more details of how this works in HOL.

   172

   173 \medskip

   174

   175 Named cases may be exhibited in the current proof context only if both the

   176 proof method and the rules involved support this.  Case names and parameters

   177 of basic rules may be declared by hand as well, by using appropriate

   178 attributes.  Thus variant versions of rules that have been derived manually

   179 may be used in advanced case analysis later.

   180

   181 \railalias{casenames}{case\_names}

   182 \railterm{casenames}

   183

   184 \begin{rail}

   185   'case' nameref attributes?

   186   ;

   187   casenames (name + )

   188   ;

   189   'params' ((name * ) + 'and')

   190   ;

   191 \end{rail}

   192 %FIXME bug in rail

   193

   194 \begin{descr}

   195 \item [$\CASE{c}$] invokes a named local context $c\colon \vec x, \vec \phi$,

   196   as provided by an appropriate proof method (such as $cases$ and $induct$ in

   197   Isabelle/HOL, see \S\ref{sec:induct-method}).  The command $\CASE{c}$

   198   abbreviates $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$.

   199 \item [$\isarkeyword{print_cases}$] prints all local contexts of the current

   200   state, using Isar proof language notation.  This is a diagnostic command;

   201   $undo$ does not apply.

   202 \item [$case_names~\vec c$] declares names for the local contexts of premises

   203   of some theorem; $\vec c$ refers to the \emph{suffix} of the list premises.

   204 \item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of

   205   premises $1, \dots, n$ of some theorem.  An empty list of names may be given

   206   to skip positions, leaving the present parameters unchanged.

   207 \end{descr}

   208

   209

   210 \section{Generalized existence}

   211

   212 \indexisarcmd{obtain}

   213 \begin{matharray}{rcl}

   214   \isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\

   215 \end{matharray}

   216

   217 Generalized existence means that additional elements with certain properties

   218 may introduced in the current context.  Technically, the $\OBTAINNAME$

   219 language element is like a declaration of $\FIXNAME$ and $\ASSUMENAME$ (see

   220 also see \S\ref{sec:proof-context}), together with a soundness proof of its

   221 additional claim.  According to the nature of existential reasoning,

   222 assumptions get eliminated from any result exported from the context later,

   223 provided that the corresponding parameters do \emph{not} occur in the

   224 conclusion.

   225

   226 \begin{rail}

   227   'obtain' (vars + 'and') comment? \\ 'where' (assm comment? + 'and')

   228   ;

   229 \end{rail}

   230

   231 $\OBTAINNAME$ is defined as a derived Isar command as follows, where $\vec b$

   232 shall refer to (optional) facts indicated for forward chaining.

   233 \begin{matharray}{l}

   234   \langle facts~\vec b\rangle \\

   235   \OBTAIN{\vec x}{a}{\vec \phi}~~\langle proof\rangle \equiv {} \\[1ex]

   236   \quad \BG \\

   237   \qquad \FIX{thesis} \\

   238   \qquad \ASSUME{that [simp, intro]}{\All{\vec x} \vec\phi \Imp thesis} \\

   239   \qquad \FROM{\vec b}~\HAVE{}{thesis}~~\langle proof\rangle \\

   240   \quad \EN \\

   241   \quad \FIX{\vec x}~\ASSUMENAME^{\ast}~{a}~{\vec\phi} \\

   242 \end{matharray}

   243

   244 Typically, the soundness proof is relatively straight-forward, often just by

   245 canonical automated tools such as $\BY{simp}$ (see \S\ref{sec:simp}) or

   246 $\BY{blast}$ (see \S\ref{sec:classical-auto}).  Accordingly, the $that$''

   247 reduction above is declared as simplification and introduction rule.

   248

   249 \medskip

   250

   251 In a sense, $\OBTAINNAME$ represents at the level of Isar proofs what would be

   252 meta-logical existential quantifiers and conjunctions.  This concept has a

   253 broad range of useful applications, ranging from plain elimination (or even

   254 introduction) of object-level existentials and conjunctions, to elimination

   255 over results of symbolic evaluation of recursive definitions, for example.

   256 Also note that $\OBTAINNAME$ without parameters acts much like $\HAVENAME$,

   257 where the result is treated as an assumption.

   258

   259

   260 \section{Miscellaneous methods and attributes}

   261

   262 \indexisarmeth{unfold}\indexisarmeth{fold}\indexisarmeth{insert}

   263 \indexisarmeth{erule}\indexisarmeth{drule}\indexisarmeth{frule}

   264 \indexisarmeth{fail}\indexisarmeth{succeed}

   265 \begin{matharray}{rcl}

   266   unfold & : & \isarmeth \\

   267   fold & : & \isarmeth \\[0.5ex]

   268   insert^* & : & \isarmeth \\[0.5ex]

   269   erule^* & : & \isarmeth \\

   270   drule^* & : & \isarmeth \\

   271   frule^* & : & \isarmeth \\[0.5ex]

   272   succeed & : & \isarmeth \\

   273   fail & : & \isarmeth \\

   274 \end{matharray}

   275

   276 \begin{rail}

   277   ('fold' | 'unfold' | 'insert' | 'erule' | 'drule' | 'frule') thmrefs

   278   ;

   279 \end{rail}

   280

   281 \begin{descr}

   282 \item [$unfold~\vec a$ and $fold~\vec a$] expand and fold back again the given

   283   meta-level definitions throughout all goals; any facts provided are inserted

   284   into the goal and subject to rewriting as well.

   285 \item [$erule~\vec a$, $drule~\vec a$, and $frule~\vec a$] are similar to the

   286   basic $rule$ method (see \S\ref{sec:pure-meth-att}), but apply rules by

   287   elim-resolution, destruct-resolution, and forward-resolution, respectively

   288   \cite{isabelle-ref}.  These are improper method, mainly for experimentation

   289   and emulating tactic scripts.

   290

   291   Different modes of basic rule application are usually expressed in Isar at

   292   the proof language level, rather than via implicit proof state

   293   manipulations.  For example, a proper single-step elimination would be done

   294   using the basic $rule$ method, with forward chaining of current facts.

   295 \item [$insert~\vec a$] inserts theorems as facts into all goals of the proof

   296   state.  Note that current facts indicated for forward chaining are ignored.

   297 \item [$succeed$] yields a single (unchanged) result; it is the identity of

   298   the \texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}).

   299 \item [$fail$] yields an empty result sequence; it is the identity of the

   300   \texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}).

   301 \end{descr}

   302

   303

   304 \indexisaratt{standard}

   305 \indexisaratt{elimify}

   306 \indexisaratt{no-vars}

   307

   308 \indexisaratt{RS}\indexisaratt{COMP}

   309 \indexisaratt{where}

   310 \indexisaratt{tag}\indexisaratt{untag}

   311 \indexisaratt{export}

   312 \indexisaratt{unfold}\indexisaratt{fold}

   313 \begin{matharray}{rcl}

   314   tag & : & \isaratt \\

   315   untag & : & \isaratt \\[0.5ex]

   316   RS & : & \isaratt \\

   317   COMP & : & \isaratt \\[0.5ex]

   318   where & : & \isaratt \\[0.5ex]

   319   unfold & : & \isaratt \\

   320   fold & : & \isaratt \\[0.5ex]

   321   standard & : & \isaratt \\

   322   elimify & : & \isaratt \\

   323   no_vars & : & \isaratt \\

   324   export^* & : & \isaratt \\

   325 \end{matharray}

   326

   327 \begin{rail}

   328   'tag' (nameref+)

   329   ;

   330   'untag' name

   331   ;

   332   ('RS' | 'COMP') nat? thmref

   333   ;

   334   'where' (name '=' term * 'and')

   335   ;

   336   ('unfold' | 'fold') thmrefs

   337   ;

   338 \end{rail}

   339

   340 \begin{descr}

   341 \item [$tag~name~args$ and $untag~name$] add and remove $tags$ of some

   342   theorem.  Tags may be any list of strings that serve as comment for some

   343   tools (e.g.\ $\LEMMANAME$ causes the tag $lemma$'' to be added to the

   344   result).  The first string is considered the tag name, the rest its

   345   arguments.  Note that untag removes any tags of the same name.

   346 \item [$RS~n~a$ and $COMP~n~a$] compose rules.  $RS$ resolves with the $n$-th

   347   premise of $a$; $COMP$ is a version of $RS$ that skips the automatic lifting

   348   process that is normally intended (cf.\ \texttt{RS} and \texttt{COMP} in

   349   \cite[\S5]{isabelle-ref}).

   350 \item [$where~\vec x = \vec t$] perform named instantiation of schematic

   351   variables occurring in a theorem.  Unlike instantiation tactics such as

   352   $rule_tac$ (see \S\ref{sec:tactic-commands}), actual schematic variables

   353   have to be specified (e.g.\ $\Var{x@3}$).

   354

   355 \item [$unfold~\vec a$ and $fold~\vec a$] expand and fold back again the given

   356   meta-level definitions throughout a rule.

   357

   358 \item [$standard$] puts a theorem into the standard form of object-rules, just

   359   as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).

   360

   361 \item [$elimify$] turns an destruction rule into an elimination, just as the

   362   ML function \texttt{make\_elim} (see \cite{isabelle-ref}).

   363

   364 \item [$no_vars$] replaces schematic variables by free ones; this is mainly

   365   for tuning output of pretty printed theorems.

   366

   367 \item [$export$] lifts a local result out of the current proof context,

   368   generalizing all fixed variables and discharging all assumptions.  Note that

   369   proper incremental export is already done as part of the basic Isar

   370   machinery.  This attribute is mainly for experimentation.

   371

   372 \end{descr}

   373

   374

   375 \section{Tactic emulations}\label{sec:tactics}

   376

   377 The following improper proof methods emulate traditional tactics.  These admit

   378 direct access to the goal state, which is normally considered harmful!  In

   379 particular, this may involve both numbered goal addressing (default 1), and

   380 dynamic instantiation within the scope of some subgoal.

   381

   382 \begin{warn}

   383   Dynamic instantiations are read and type-checked according to a subgoal of

   384   the current dynamic goal state, rather than the static proof context!  In

   385   particular, locally fixed variables and term abbreviations may not be

   386   included in the term specifications.  Thus schematic variables are left to

   387   be solved by unification with certain parts of the subgoal involved.

   388 \end{warn}

   389

   390 Note that the tactic emulation proof methods in Isabelle/Isar are consistently

   391 named $foo_tac$.

   392

   393 \indexisarmeth{rule-tac}\indexisarmeth{erule-tac}

   394 \indexisarmeth{drule-tac}\indexisarmeth{frule-tac}

   395 \indexisarmeth{cut-tac}\indexisarmeth{thin-tac}

   396 \indexisarmeth{subgoal-tac}\indexisarmeth{tactic}

   397 \begin{matharray}{rcl}

   398   rule_tac^* & : & \isarmeth \\

   399   erule_tac^* & : & \isarmeth \\

   400   drule_tac^* & : & \isarmeth \\

   401   frule_tac^* & : & \isarmeth \\

   402   cut_tac^* & : & \isarmeth \\

   403   thin_tac^* & : & \isarmeth \\

   404   subgoal_tac^* & : & \isarmeth \\

   405   tactic^* & : & \isarmeth \\

   406 \end{matharray}

   407

   408 \railalias{ruletac}{rule\_tac}

   409 \railterm{ruletac}

   410

   411 \railalias{eruletac}{erule\_tac}

   412 \railterm{eruletac}

   413

   414 \railalias{druletac}{drule\_tac}

   415 \railterm{druletac}

   416

   417 \railalias{fruletac}{frule\_tac}

   418 \railterm{fruletac}

   419

   420 \railalias{cuttac}{cut\_tac}

   421 \railterm{cuttac}

   422

   423 \railalias{thintac}{thin\_tac}

   424 \railterm{thintac}

   425

   426 \railalias{subgoaltac}{subgoal\_tac}

   427 \railterm{subgoaltac}

   428

   429 \begin{rail}

   430   ( ruletac | eruletac | druletac | fruletac | cuttac | thintac ) goalspec?

   431   ( insts thmref | thmrefs )

   432   ;

   433   subgoaltac goalspec? (prop +)

   434   ;

   435   'tactic' text

   436   ;

   437

   438   insts: ((name '=' term) + 'and') 'in'

   439   ;

   440 \end{rail}

   441

   442 \begin{descr}

   443 \item [$rule_tac$ etc.] do resolution of rules with explicit instantiation.

   444   This works the same way as the ML tactics \texttt{res_inst_tac} etc. (see

   445   \cite[\S3]{isabelle-ref}).

   446

   447   Note that multiple rules may be only given there is no instantiation.  Then

   448   $rule_tac$ is the same as \texttt{resolve_tac} in ML (see

   449   \cite[\S3]{isabelle-ref}).

   450 \item [$cut_tac$] inserts facts into the proof state as assumption of a

   451   subgoal, see also \texttt{cut_facts_tac} in \cite[\S3]{isabelle-ref}.  Note

   452   that the scope of schmatic variables is spread over the main goal statement.

   453   Instantiations may be given as well, see also ML tactic

   454   \texttt{cut_inst_tac} in \cite[\S3]{isabelle-ref}.

   455 \item [$thin_tac~\phi$] deletes the specified assumption from a subgoal; note

   456   that $\phi$ may contain schematic variables.  See also \texttt{thin_tac} in

   457   \cite[\S3]{isabelle-ref}.

   458 \item [$subgoal_tac~\phi$] adds $\phi$ as an assumption to a subgoal.  See

   459   also \texttt{subgoal_tac} and \texttt{subgoals_tac} in

   460   \cite[\S3]{isabelle-ref}.

   461 \item [$tactic~text$] produces a proof method from any ML text of type

   462   \texttt{tactic}.  Apart from the usual ML environment and the current

   463   implicit theory context, the ML code may refer to the following locally

   464   bound values:

   465

   466 %%FIXME ttbox produces too much trailing space (why?)

   467 {\footnotesize\begin{verbatim}

   468 val ctxt  : Proof.context

   469 val facts : thm list

   470 val thm   : string -> thm

   471 val thms  : string -> thm list

   472 \end{verbatim}}

   473   Here \texttt{ctxt} refers to the current proof context, \texttt{facts}

   474   indicates any current facts for forward-chaining, and

   475   \texttt{thm}~/~\texttt{thms} retrieve named facts (including global

   476   theorems) from the context.

   477 \end{descr}

   478

   479

   480 \section{The Simplifier}

   481

   482 \subsection{Simplification methods}\label{sec:simp}

   483

   484 \indexisarmeth{simp}\indexisarmeth{simp-all}

   485 \begin{matharray}{rcl}

   486   simp & : & \isarmeth \\

   487   simp_all & : & \isarmeth \\

   488 \end{matharray}

   489

   490 \railalias{simpall}{simp\_all}

   491 \railterm{simpall}

   492

   493 \railalias{noasm}{no\_asm}

   494 \railterm{noasm}

   495

   496 \railalias{noasmsimp}{no\_asm\_simp}

   497 \railterm{noasmsimp}

   498

   499 \railalias{noasmuse}{no\_asm\_use}

   500 \railterm{noasmuse}

   501

   502 \begin{rail}

   503   ('simp' | simpall) ('!' ?) opt? (simpmod * )

   504   ;

   505

   506   opt: '(' (noasm | noasmsimp | noasmuse) ')'

   507   ;

   508   simpmod: ('add' | 'del' | 'only' | 'split' (() | 'add' | 'del') | 'other') ':' thmrefs

   509   ;

   510 \end{rail}

   511

   512 \begin{descr}

   513 \item [$simp$] invokes Isabelle's simplifier, after declaring additional rules

   514   according to the arguments given.  Note that the \railtterm{only} modifier

   515   first removes all other rewrite rules, congruences, and looper tactics

   516   (including splits), and then behaves like \railtterm{add}.

   517

   518   The \railtterm{split} modifiers add or delete rules for the Splitter (see

   519   also \cite{isabelle-ref}), the default is to add.  This works only if the

   520   Simplifier method has been properly setup to include the Splitter (all major

   521   object logics such HOL, HOLCF, FOL, ZF do this already).

   522

   523   The \railtterm{other} modifier ignores its arguments.  Nevertheless,

   524   additional kinds of rules may be declared by including appropriate

   525   attributes in the specification.

   526 \item [$simp_all$] is similar to $simp$, but acts on all goals.

   527 \end{descr}

   528

   529 By default, the Simplifier methods are based on \texttt{asm_full_simp_tac}

   530 internally \cite[\S10]{isabelle-ref}, which means that assumptions are both

   531 simplified as well as used in simplifying the conclusion.  In structured

   532 proofs this is usually quite well behaved in practice: just the local premises

   533 of the actual goal are involved, additional facts may inserted via explicit

   534 forward-chaining (using $\THEN$, $\FROMNAME$ etc.).  The full context of

   535 assumptions is only included if the $!$'' (bang) argument is given, which

   536 should be used with some care, though.

   537

   538 Additional Simplifier options may be specified to tune the behavior even

   539 further: $(no_asm)$ means assumptions are ignored completely (cf.\

   540 \texttt{simp_tac}), $(no_asm_simp)$ means assumptions are used in the

   541 simplification of the conclusion but are not themselves simplified (cf.\

   542 \texttt{asm_simp_tac}), and $(no_asm_use)$ means assumptions are simplified

   543 but are not used in the simplification of each other or the conclusion (cf.

   544 \texttt{full_simp_tac}).

   545

   546 \medskip

   547

   548 The Splitter package is usually configured to work as part of the Simplifier.

   549 There is no separate $split$ method available.  The effect of repeatedly

   550 applying \texttt{split_tac} can be simulated by

   551 $(simp~only\colon~split\colon~\vec a)$.

   552

   553

   554 \subsection{Declaring rules}

   555

   556 \indexisarcmd{print-simpset}

   557 \indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong}

   558 \begin{matharray}{rcl}

   559   print_simpset & : & \isarkeep{theory~|~proof} \\

   560   simp & : & \isaratt \\

   561   split & : & \isaratt \\

   562   cong & : & \isaratt \\

   563 \end{matharray}

   564

   565 \begin{rail}

   566   ('simp' | 'split' | 'cong') (() | 'add' | 'del')

   567   ;

   568 \end{rail}

   569

   570 \begin{descr}

   571 \item [$print_simpset$] prints the collection of rules declared to the

   572   Simplifier, which is also known as simpset'' internally

   573   \cite{isabelle-ref}.  This is a diagnostic command; $undo$ does not apply.

   574 \item [$simp$] declares simplification rules.

   575 \item [$split$] declares split rules.

   576 \item [$cong$] declares congruence rules.

   577 \end{descr}

   578

   579

   580 \subsection{Forward simplification}

   581

   582 \indexisaratt{simplify}\indexisaratt{asm-simplify}

   583 \indexisaratt{full-simplify}\indexisaratt{asm-full-simplify}

   584 \begin{matharray}{rcl}

   585   simplify & : & \isaratt \\

   586   asm_simplify & : & \isaratt \\

   587   full_simplify & : & \isaratt \\

   588   asm_full_simplify & : & \isaratt \\

   589 \end{matharray}

   590

   591 These attributes provide forward rules for simplification, which should be

   592 used only very rarely.  There are no separate options for declaring

   593 simplification rules locally.

   594

   595 See the ML functions of the same name in \cite[\S10]{isabelle-ref} for more

   596 information.

   597

   598

   599 \section{The Classical Reasoner}

   600

   601 \subsection{Basic methods}\label{sec:classical-basic}

   602

   603 \indexisarmeth{rule}\indexisarmeth{intro}

   604 \indexisarmeth{elim}\indexisarmeth{default}\indexisarmeth{contradiction}

   605 \begin{matharray}{rcl}

   606   rule & : & \isarmeth \\

   607   intro & : & \isarmeth \\

   608   elim & : & \isarmeth \\

   609   contradiction & : & \isarmeth \\

   610 \end{matharray}

   611

   612 \begin{rail}

   613   ('rule' | 'intro' | 'elim') thmrefs?

   614   ;

   615 \end{rail}

   616

   617 \begin{descr}

   618 \item [$rule$] as offered by the classical reasoner is a refinement over the

   619   primitive one (see \S\ref{sec:pure-meth-att}).  In case that no rules are

   620   provided as arguments, it automatically determines elimination and

   621   introduction rules from the context (see also \S\ref{sec:classical-mod}).

   622   This is made the default method for basic proof steps, such as $\PROOFNAME$

   623   and $\DDOT$'' (two dots), see also \S\ref{sec:proof-steps} and

   624   \S\ref{sec:pure-meth-att}.

   625

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

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

   628   refers to any suitable rules declared in the context, otherwise only the

   629   explicitly given ones may be applied.  The latter form admits better control

   630   of what actually happens, thus it is very appropriate as an initial method

   631   for $\PROOFNAME$ that splits up certain connectives of the goal, before

   632   entering the actual sub-proof.

   633

   634 \item [$contradiction$] solves some goal by contradiction, deriving any result

   635   from both $\neg A$ and $A$.  Facts, which are guaranteed to participate, may

   636   appear in either order.

   637 \end{descr}

   638

   639

   640 \subsection{Automated methods}\label{sec:classical-auto}

   641

   642 \indexisarmeth{blast}\indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{clarify}

   643 \begin{matharray}{rcl}

   644  blast & : & \isarmeth \\

   645  fast & : & \isarmeth \\

   646  best & : & \isarmeth \\

   647  clarify & : & \isarmeth \\

   648 \end{matharray}

   649

   650 \begin{rail}

   651   'blast' ('!' ?) nat? (clamod * )

   652   ;

   653   ('fast' | 'best' | 'clarify') ('!' ?) (clamod * )

   654   ;

   655

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

   657   ;

   658 \end{rail}

   659

   660 \begin{descr}

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

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

   663   user-supplied search bound (default 20).  Note that $blast$ is the only

   664   classical proof procedure in Isabelle that can handle actual object-logic

   665   rules as local assumptions ($fast$ etc.\ would just ignore non-atomic

   666   facts).

   667 \item [$fast$, $best$, and $clarify$] refer to the generic classical reasoner.

   668   See \texttt{fast_tac}, \texttt{best_tac}, and \texttt{clarify_tac} in

   669   \cite[\S11]{isabelle-ref} for more information.

   670 \end{descr}

   671

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

   673 rules.  Their semantics is analogous to the attributes given in

   674 \S\ref{sec:classical-mod}.  Facts provided by forward chaining are

   675 inserted\footnote{These methods usually cannot make proper use of actual rules

   676   inserted that way, though.} into the goal before doing the search.  The

   677 !''~argument causes the full context of assumptions to be included as well.

   678 This is slightly less hazardous than for the Simplifier (see

   679 \S\ref{sec:simp}).

   680

   681

   682 \subsection{Combined automated methods}

   683

   684 \indexisarmeth{auto}\indexisarmeth{force}

   685 \indexisarmeth{clarsimp}\indexisarmeth{fastsimp}

   686 \begin{matharray}{rcl}

   687   auto & : & \isarmeth \\

   688   force & : & \isarmeth \\

   689   clarsimp & : & \isarmeth \\

   690   fastsimp & : & \isarmeth \\

   691 \end{matharray}

   692

   693 \begin{rail}

   694   ('auto' | 'force' | 'clarsimp' | 'fastsimp') ('!' ?) (clasimpmod * )

   695   ;

   696

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

   698     ('split' (() | 'add' | 'del')) |

   699     (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' thmrefs

   700 \end{rail}

   701

   702 \begin{descr}

   703 \item [$auto$, $force$, $clarsimp$, $fastsimp$] provide access to Isabelle's

   704   combined simplification and classical reasoning tactics.  These correspond

   705   to \texttt{auto_tac}, \texttt{force_tac}, \texttt{clarsimp_tac}, and

   706   \texttt{fast_tac} (with the Simplifier added as wrapper), see

   707   \cite[\S11]{isabelle-ref} for more information.  The modifier arguments

   708   correspond to those given in \S\ref{sec:simp} and

   709   \S\ref{sec:classical-auto}.  Just note that the ones related to the

   710   Simplifier are prefixed by \railtterm{simp} here.

   711

   712   Facts provided by forward chaining are inserted into the goal before doing

   713   the search.  The !''~argument causes the full context of assumptions to be

   714   included as well.

   715 \end{descr}

   716

   717

   718 \subsection{Declaring rules}\label{sec:classical-mod}

   719

   720 \indexisarcmd{print-claset}

   721 \indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}

   722 \indexisaratt{iff}\indexisaratt{delrule}

   723 \begin{matharray}{rcl}

   724   print_claset & : & \isarkeep{theory~|~proof} \\

   725   intro & : & \isaratt \\

   726   elim & : & \isaratt \\

   727   dest & : & \isaratt \\

   728   iff & : & \isaratt \\

   729   delrule & : & \isaratt \\

   730 \end{matharray}

   731

   732 \begin{rail}

   733   ('intro' | 'elim' | 'dest') ('!' | () | '?')

   734   ;

   735   'iff' (() | 'add' | 'del')

   736 \end{rail}

   737

   738 \begin{descr}

   739 \item [$print_claset$] prints the collection of rules declared to the

   740   Classical Reasoner, which is also known as simpset'' internally

   741   \cite{isabelle-ref}.  This is a diagnostic command; $undo$ does not apply.

   742 \item [$intro$, $elim$, and $dest$] declare introduction, elimination, and

   743   destruct rules, respectively.  By default, rules are considered as

   744   \emph{unsafe} (i.e.\ not applied blindly without backtracking), while a

   745   single !'' classifies as \emph{safe}, and ?'' as \emph{extra} (i.e.\ not

   746   applied in the search-oriented automated methods, but only in single-step

   747   methods such as $rule$).

   748

   749 \item [$iff$] declares equations both as rules for the Simplifier and

   750   Classical Reasoner.

   751

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

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

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

   755 \end{descr}

   756

   757

   758 %%% Local Variables:

   759 %%% mode: latex

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

   761 %%% End: