2 \chapter{Generic tools and packages}\label{ch:gen-tools}
4 \section{Theory specification commands}
6 \subsection{Axiomatic type classes}\label{sec:axclass}
8 \indexisarcmd{axclass}\indexisarcmd{instance}\indexisarmeth{intro-classes}
10 \isarcmd{axclass} & : & \isartrans{theory}{theory} \\
11 \isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\
12 intro_classes & : & \isarmeth \\
15 Axiomatic type classes are provided by Isabelle/Pure as a \emph{definitional}
16 interface to type classes (cf.~\S\ref{sec:classes}). Thus any object logic
17 may make use of this light-weight mechanism of abstract theories
18 \cite{Wenzel:1997:TPHOL}. There is also a tutorial on using axiomatic type
19 classes in Isabelle \cite{isabelle-axclass} that is part of the standard
20 Isabelle documentation.
23 'axclass' classdecl (axmdecl prop +)
25 'instance' (nameref ('<' | subseteq) nameref | nameref '::' simplearity)
31 \item [$\AXCLASS~c \subseteq \vec c~~axms$] defines an axiomatic type class as
32 the intersection of existing classes, with additional axioms holding. Class
33 axioms may not contain more than one type variable. The class axioms (with
34 implicit sort constraints added) are bound to the given names. Furthermore
35 a class introduction rule is generated (being bound as $c{.}intro$); this
36 rule is employed by method $intro_classes$ to support instantiation proofs
39 The ``axioms'' are stored as theorems according to the given name
40 specifications, adding the class name $c$ as name space prefix; the same
41 facts are also stored collectively as $c{\dtt}axioms$.
43 \item [$\INSTANCE~c@1 \subseteq c@2$ and $\INSTANCE~t :: (\vec s)c$] setup a
44 goal stating a class relation or type arity. The proof would usually
45 proceed by $intro_classes$, and then establish the characteristic theorems
46 of the type classes involved. After finishing the proof, the theory will be
47 augmented by a type signature declaration corresponding to the resulting
50 \item [$intro_classes$] repeatedly expands all class introduction rules of
51 this theory. Note that this method usually needs not be named explicitly,
52 as it is already included in the default proof step (of $\PROOFNAME$ etc.).
53 In particular, instantiation of trivial (syntactic) classes may be performed
54 by a single ``$\DDOT$'' proof step.
59 \subsection{Locales and local contexts}\label{sec:locale}
61 Locales are named local contexts, consisting of a list of declaration elements
62 that are modeled after the Isar proof context commands (cf.\
63 \S\ref{sec:proof-context}).
66 \subsubsection{Localized commands}
68 Existing locales may be augmented later on by adding new facts. Note that the
69 actual context definition may not be changed! Several theory commands that
70 produce facts in some way are available in ``localized'' versions, referring
71 to a named locale instead of the global theory context.
73 \indexouternonterm{locale}
75 locale: '(' 'in' name ')'
79 Emerging facts of localized commands are stored in two versions, both in the
80 target locale and the theory (after export). The latter view produces a
81 qualified binding, using the locale name as a name space prefix.
83 For example, ``$\LEMMAS~(\IN~loc)~a = \vec b$'' retrieves facts $\vec b$ from
84 the locale context of $loc$ and augments its body by an appropriate
85 ``$\isarkeyword{notes}$'' element (see below). The exported view of $a$,
86 after discharging the locale context, is stored as $loc{.}a$ within the global
87 theory. A localized goal ``$\LEMMANAME~(\IN~loc)~a:~\phi$'' works similarly,
88 only that the fact emerges through the subsequent proof, which may refer to
89 the full infrastructure of the locale context (covering local parameters with
90 typing and concrete syntax, assumptions, definitions etc.). Most notably,
91 fact declarations of the locale are active during the proof as well (e.g.\
95 \subsubsection{Locale specifications}
97 \indexisarcmd{locale}\indexisarcmd{print-locale}\indexisarcmd{print-locales}
98 \begin{matharray}{rcl}
99 \isarcmd{locale} & : & \isarkeep{theory} \\
100 \isarcmd{print_locale}^* & : & \isarkeep{theory~|~proof} \\
101 \isarcmd{print_locales}^* & : & \isarkeep{theory~|~proof} \\
104 \indexouternonterm{contextexpr}\indexouternonterm{contextelem}
106 \railalias{printlocale}{print\_locale}
107 \railterm{printlocale}
110 'locale' name ('=' localeexpr)?
112 printlocale localeexpr
114 localeexpr: ((contextexpr '+' (contextelem+)) | contextexpr | (contextelem+))
117 contextexpr: nameref | '(' contextexpr ')' |
118 (contextexpr (name+)) | (contextexpr + '+')
120 contextelem: fixes | assumes | defines | notes | includes
122 fixes: 'fixes' (name ('::' type)? structmixfix? + 'and')
124 assumes: 'assumes' (thmdecl? props + 'and')
126 defines: 'defines' (thmdecl? prop proppat? + 'and')
128 notes: 'notes' (thmdef? thmrefs + 'and')
130 includes: 'includes' contextexpr
136 \item [$\LOCALE~loc~=~import~+~body$] defines new locale $loc$ as a context
137 consisting of a certain view of existing locales ($import$) plus some
138 additional elements ($body$). Both $import$ and $body$ are optional; the
139 degenerate form $\LOCALE~loc$ defines an empty locale, which may still be
140 useful to collect declarations of facts later on. Type-inference on locale
141 expressions automatically takes care of the most general typing that the
142 combined context elements may acquire.
144 The $import$ consists of a structured context expression, consisting of
145 references to existing locales, renamed contexts, or merged contexts.
146 Renaming uses positional notation: $c~\vec x$ means that (a prefix) the
147 fixed parameters of context $c$ are named according to $\vec x$; a
148 ``\texttt{_}'' (underscore).\indexisarthm{_@\texttt{_}} means to skip that
149 position. Also note that concrete syntax only works with the original name.
150 Merging proceeds from left-to-right, suppressing any duplicates stemming
151 from different paths through the import hierarchy.
153 The $body$ consists of basic context elements, further context expressions
154 may be included as well.
158 \item [$\FIXES{~x::\tau~(mx)}$] declares a local parameter of type $\tau$
159 and mixfix annotation $mx$ (both are optional). The special syntax
160 declaration ``$(structure)$'' means that $x$ may be referenced
161 implicitly in this context.
163 \item [$\ASSUMES{a}{\vec\phi}$] introduces local premises, similar to
164 $\ASSUMENAME$ within a proof (cf.\ \S\ref{sec:proof-context}).
166 \item [$\DEFINES{a}{x \equiv t}$] defines a previously declared parameter.
167 This is close to $\DEFNAME$ within a proof (cf.\
168 \S\ref{sec:proof-context}), but $\DEFINESNAME$ takes an equational
169 proposition instead of variable-term pair. The left-hand side of the
170 equation may have additional arguments, e.g.\ ``$\DEFINES{}{f~\vec x
173 \item [$\NOTES{a}{\vec b}$] reconsiders facts within a local context. Most
174 notably, this may include arbitrary declarations in any attribute
175 specifications included here, e.g.\ a local $simp$ rule.
177 \item [$\INCLUDES{c}$] copies the specified context in a statically scoped
180 In contrast, the initial $import$ specification of a locale expression
181 maintains a dynamic relation to the locales being referenced (benefiting
182 from any later fact declarations in the obvious manner).
185 Note that ``$\IS{p}$'' patterns given in the syntax of $\ASSUMESNAME$ and
186 $\DEFINESNAME$ above are actually illegal in locale definitions. In the
187 long goal format of \S\ref{sec:goals}, term bindings may be included as
190 \item [$\isarkeyword{print_locale}~import~+~body$] prints the specified locale
191 expression in a flattened form. The notable special case
192 $\isarkeyword{print_locale}~loc$ just prints the contents of the named
193 locale, but keep in mind that type-inference will normalize type variables
194 according to the usual alphabetical order.
196 \item [$\isarkeyword{print_locales}$] prints the names of all locales of the
202 \section{Derived proof schemes}
204 \subsection{Generalized elimination}\label{sec:obtain}
206 \indexisarcmd{obtain}
207 \begin{matharray}{rcl}
208 \isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\
211 Generalized elimination means that additional elements with certain properties
212 may be introduced in the current context, by virtue of a locally proven
213 ``soundness statement''. Technically speaking, the $\OBTAINNAME$ language
214 element is like a declaration of $\FIXNAME$ and $\ASSUMENAME$ (see also see
215 \S\ref{sec:proof-context}), together with a soundness proof of its additional
216 claim. According to the nature of existential reasoning, assumptions get
217 eliminated from any result exported from the context later, provided that the
218 corresponding parameters do \emph{not} occur in the conclusion.
221 'obtain' (vars + 'and') 'where' (props + 'and')
225 $\OBTAINNAME$ is defined as a derived Isar command as follows, where $\vec b$
226 shall refer to (optional) facts indicated for forward chaining.
228 \langle facts~\vec b\rangle \\
229 \OBTAIN{\vec x}{a}{\vec \phi}~~\langle proof\rangle \equiv {} \\[1ex]
230 \quad \HAVE{}{\All{thesis} (\All{\vec x} \vec\phi \Imp thesis) \Imp thesis} \\
231 \quad \PROOF{succeed} \\
232 \qquad \FIX{thesis} \\
233 \qquad \ASSUME{that~[intro?]}{\All{\vec x} \vec\phi \Imp thesis} \\
234 \qquad \THUS{}{thesis} \\
235 \quad\qquad \APPLY{-} \\
236 \quad\qquad \USING{\vec b}~~\langle proof\rangle \\
238 \quad \FIX{\vec x}~\ASSUMENAME^\ast~a\colon~\vec\phi \\
241 Typically, the soundness proof is relatively straight-forward, often just by
242 canonical automated tools such as ``$\BY{simp}$'' or ``$\BY{blast}$''.
243 Accordingly, the ``$that$'' reduction above is declared as simplification and
248 In a sense, $\OBTAINNAME$ represents at the level of Isar proofs what would be
249 meta-logical existential quantifiers and conjunctions. This concept has a
250 broad range of useful applications, ranging from plain elimination (or
251 introduction) of object-level existentials and conjunctions, to elimination
252 over results of symbolic evaluation of recursive definitions, for example.
253 Also note that $\OBTAINNAME$ without parameters acts much like $\HAVENAME$,
254 where the result is treated as a genuine assumption.
257 \subsection{Calculational reasoning}\label{sec:calculation}
259 \indexisarcmd{also}\indexisarcmd{finally}
260 \indexisarcmd{moreover}\indexisarcmd{ultimately}
261 \indexisarcmd{print-trans-rules}
262 \indexisaratt{trans}\indexisaratt{sym}\indexisaratt{symmetric}
263 \begin{matharray}{rcl}
264 \isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\
265 \isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\
266 \isarcmd{moreover} & : & \isartrans{proof(state)}{proof(state)} \\
267 \isarcmd{ultimately} & : & \isartrans{proof(state)}{proof(chain)} \\
268 \isarcmd{print_trans_rules}^* & : & \isarkeep{theory~|~proof} \\
269 trans & : & \isaratt \\
270 sym & : & \isaratt \\
271 symmetric & : & \isaratt \\
274 Calculational proof is forward reasoning with implicit application of
275 transitivity rules (such those of $=$, $\leq$, $<$). Isabelle/Isar maintains
276 an auxiliary register $calculation$\indexisarthm{calculation} for accumulating
277 results obtained by transitivity composed with the current result. Command
278 $\ALSO$ updates $calculation$ involving $this$, while $\FINALLY$ exhibits the
279 final $calculation$ by forward chaining towards the next goal statement. Both
280 commands require valid current facts, i.e.\ may occur only after commands that
281 produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or some finished proof of
282 $\HAVENAME$, $\SHOWNAME$ etc. The $\MOREOVER$ and $\ULTIMATELY$ commands are
283 similar to $\ALSO$ and $\FINALLY$, but only collect further results in
284 $calculation$ without applying any rules yet.
286 Also note that the implicit term abbreviation ``$\dots$'' has its canonical
287 application with calculational proofs. It refers to the argument of the
288 preceding statement. (The argument of a curried infix expression happens to be
289 its right-hand side.)
291 Isabelle/Isar calculations are implicitly subject to block structure in the
292 sense that new threads of calculational reasoning are commenced for any new
293 block (as opened by a local goal, for example). This means that, apart from
294 being able to nest calculations, there is no separate \emph{begin-calculation}
299 The Isar calculation proof commands may be defined as follows:\footnote{We
300 suppress internal bookkeeping such as proper handling of block-structure.}
301 \begin{matharray}{rcl}
302 \ALSO@0 & \equiv & \NOTE{calculation}{this} \\
303 \ALSO@{n+1} & \equiv & \NOTE{calculation}{trans~[OF~calculation~this]} \\[0.5ex]
304 \FINALLY & \equiv & \ALSO~\FROM{calculation} \\
305 \MOREOVER & \equiv & \NOTE{calculation}{calculation~this} \\
306 \ULTIMATELY & \equiv & \MOREOVER~\FROM{calculation} \\
310 ('also' | 'finally') ('(' thmrefs ')')?
312 'trans' (() | 'add' | 'del')
318 \item [$\ALSO~(\vec a)$] maintains the auxiliary $calculation$ register as
319 follows. The first occurrence of $\ALSO$ in some calculational thread
320 initializes $calculation$ by $this$. Any subsequent $\ALSO$ on the same
321 level of block-structure updates $calculation$ by some transitivity rule
322 applied to $calculation$ and $this$ (in that order). Transitivity rules are
323 picked from the current context, unless alternative rules are given as
326 \item [$\FINALLY~(\vec a)$] maintaining $calculation$ in the same way as
327 $\ALSO$, and concludes the current calculational thread. The final result
328 is exhibited as fact for forward chaining towards the next goal. Basically,
329 $\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$. Note that
330 ``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and
331 ``$\FINALLY~\HAVE{}{\phi}~\DOT$'' are typical idioms for concluding
332 calculational proofs.
334 \item [$\MOREOVER$ and $\ULTIMATELY$] are analogous to $\ALSO$ and $\FINALLY$,
335 but collect results only, without applying rules.
337 \item [$\isarkeyword{print_trans_rules}$] prints the list of transitivity
338 rules (for calculational commands $\ALSO$ and $\FINALLY$) and symmetry rules
339 (for the $symmetric$ operation and single step elimination patters) of the
342 \item [$trans$] declares theorems as transitivity rules.
344 \item [$sym$] declares symmetry rules.
346 \item [$symmetric$] resolves a theorem with some rule declared as $sym$ in the
347 current context. For example, ``$\ASSUME{[symmetric]}{x = y}$'' produces a
348 swapped fact derived from that assumption.
350 In structured proof texts it is often more appropriate to use an explicit
351 single-step elimination proof, such as ``$\ASSUME{}{x = y}~\HENCE{}{y =
352 x}~\DDOT$''. The very same rules known to $symmetric$ are declared as
358 \section{Proof tools}
360 \subsection{Miscellaneous methods and attributes}\label{sec:misc-meth-att}
362 \indexisarmeth{unfold}\indexisarmeth{fold}\indexisarmeth{insert}
363 \indexisarmeth{erule}\indexisarmeth{drule}\indexisarmeth{frule}
364 \indexisarmeth{fail}\indexisarmeth{succeed}
365 \begin{matharray}{rcl}
366 unfold & : & \isarmeth \\
367 fold & : & \isarmeth \\
368 insert & : & \isarmeth \\[0.5ex]
369 erule^* & : & \isarmeth \\
370 drule^* & : & \isarmeth \\
371 frule^* & : & \isarmeth \\
372 succeed & : & \isarmeth \\
373 fail & : & \isarmeth \\
377 ('fold' | 'unfold' | 'insert') thmrefs
379 ('erule' | 'drule' | 'frule') ('('nat')')? thmrefs
385 \item [$unfold~\vec a$ and $fold~\vec a$] expand (or fold back again) the
386 given meta-level definitions throughout all goals; any chained facts
387 provided are inserted into the goal and subject to rewriting as well.
389 \item [$insert~\vec a$] inserts theorems as facts into all goals of the proof
390 state. Note that current facts indicated for forward chaining are ignored.
392 \item [$erule~\vec a$, $drule~\vec a$, and $frule~\vec a$] are similar to the
393 basic $rule$ method (see \S\ref{sec:pure-meth-att}), but apply rules by
394 elim-resolution, destruct-resolution, and forward-resolution, respectively
395 \cite{isabelle-ref}. The optional natural number argument (default $0$)
396 specifies additional assumption steps to be performed here.
398 Note that these methods are improper ones, mainly serving for
399 experimentation and tactic script emulation. Different modes of basic rule
400 application are usually expressed in Isar at the proof language level,
401 rather than via implicit proof state manipulations. For example, a proper
402 single-step elimination would be done using the plain $rule$ method, with
403 forward chaining of current facts.
405 \item [$succeed$] yields a single (unchanged) result; it is the identity of
406 the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
408 \item [$fail$] yields an empty result sequence; it is the identity of the
409 ``\texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
413 \indexisaratt{tagged}\indexisaratt{untagged}
414 \indexisaratt{THEN}\indexisaratt{COMP}
415 \indexisaratt{where}\indexisaratt{unfolded}\indexisaratt{folded}
416 \indexisaratt{standard}\indexisarattof{Pure}{elim-format}
417 \indexisaratt{no-vars}
418 \begin{matharray}{rcl}
419 tagged & : & \isaratt \\
420 untagged & : & \isaratt \\[0.5ex]
421 THEN & : & \isaratt \\
422 COMP & : & \isaratt \\[0.5ex]
423 where & : & \isaratt \\[0.5ex]
424 unfolded & : & \isaratt \\
425 folded & : & \isaratt \\[0.5ex]
426 elim_format & : & \isaratt \\
427 standard^* & : & \isaratt \\
428 no_vars^* & : & \isaratt \\
436 ('THEN' | 'COMP') ('[' nat ']')? thmref
438 'where' (name '=' term * 'and')
440 ('unfolded' | 'folded') thmrefs
446 \item [$tagged~name~args$ and $untagged~name$] add and remove $tags$ of some
447 theorem. Tags may be any list of strings that serve as comment for some
448 tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the
449 result). The first string is considered the tag name, the rest its
450 arguments. Note that untag removes any tags of the same name.
452 \item [$THEN~a$ and $COMP~a$] compose rules by resolution. $THEN$ resolves
453 with the first premise of $a$ (an alternative position may be also
454 specified); the $COMP$ version skips the automatic lifting process that is
455 normally intended (cf.\ \texttt{RS} and \texttt{COMP} in
456 \cite[\S5]{isabelle-ref}).
458 \item [$where~\vec x = \vec t$] perform named instantiation of schematic
459 variables occurring in a theorem. Unlike instantiation tactics such as
460 $rule_tac$ (see \S\ref{sec:tactic-commands}), actual schematic variables
461 have to be specified on the left-hand side (e.g.\ $\Var{x@3}$).
463 \item [$unfolded~\vec a$ and $folded~\vec a$] expand and fold back again the
464 given meta-level definitions throughout a rule.
466 \item [$elim_format$] turns a destruction rule into elimination rule format,
467 by resolving with the rule $\PROP A \Imp (\PROP A \Imp \PROP B) \Imp \PROP
470 Note that the Classical Reasoner (\S\ref{sec:classical}) provides its own
471 version of this operation.
473 \item [$standard$] puts a theorem into the standard form of object-rules at
474 the outermost theory level. Note that this operation violates the local
475 proof context (including active locales).
477 \item [$no_vars$] replaces schematic variables by free ones; this is mainly
478 for tuning output of pretty printed theorems.
483 \subsection{Further tactic emulations}\label{sec:tactics}
485 The following improper proof methods emulate traditional tactics. These admit
486 direct access to the goal state, which is normally considered harmful! In
487 particular, this may involve both numbered goal addressing (default 1), and
488 dynamic instantiation within the scope of some subgoal.
491 Dynamic instantiations are read and type-checked according to a subgoal of
492 the current dynamic goal state, rather than the static proof context! In
493 particular, locally fixed variables and term abbreviations may not be
494 included in the term specifications. Thus schematic variables are left to
495 be solved by unification with certain parts of the subgoal involved.
498 Note that the tactic emulation proof methods in Isabelle/Isar are consistently
501 \indexisarmeth{rule-tac}\indexisarmeth{erule-tac}
502 \indexisarmeth{drule-tac}\indexisarmeth{frule-tac}
503 \indexisarmeth{cut-tac}\indexisarmeth{thin-tac}
504 \indexisarmeth{subgoal-tac}\indexisarmeth{rename-tac}
505 \indexisarmeth{rotate-tac}\indexisarmeth{tactic}
506 \begin{matharray}{rcl}
507 rule_tac^* & : & \isarmeth \\
508 erule_tac^* & : & \isarmeth \\
509 drule_tac^* & : & \isarmeth \\
510 frule_tac^* & : & \isarmeth \\
511 cut_tac^* & : & \isarmeth \\
512 thin_tac^* & : & \isarmeth \\
513 subgoal_tac^* & : & \isarmeth \\
514 rename_tac^* & : & \isarmeth \\
515 rotate_tac^* & : & \isarmeth \\
516 tactic^* & : & \isarmeth \\
519 \railalias{ruletac}{rule\_tac}
522 \railalias{eruletac}{erule\_tac}
525 \railalias{druletac}{drule\_tac}
528 \railalias{fruletac}{frule\_tac}
531 \railalias{cuttac}{cut\_tac}
534 \railalias{thintac}{thin\_tac}
537 \railalias{subgoaltac}{subgoal\_tac}
538 \railterm{subgoaltac}
540 \railalias{renametac}{rename\_tac}
543 \railalias{rotatetac}{rotate\_tac}
547 ( ruletac | eruletac | druletac | fruletac | cuttac | thintac ) goalspec?
548 ( insts thmref | thmrefs )
550 subgoaltac goalspec? (prop +)
552 renametac goalspec? (name +)
554 rotatetac goalspec? int?
559 insts: ((name '=' term) + 'and') 'in'
565 \item [$rule_tac$ etc.] do resolution of rules with explicit instantiation.
566 This works the same way as the ML tactics \texttt{res_inst_tac} etc. (see
567 \cite[\S3]{isabelle-ref}).
569 Multiple rules may be only given if there is no instantiation; then
570 $rule_tac$ is the same as \texttt{resolve_tac} in ML (see
571 \cite[\S3]{isabelle-ref}).
573 \item [$cut_tac$] inserts facts into the proof state as assumption of a
574 subgoal, see also \texttt{cut_facts_tac} in \cite[\S3]{isabelle-ref}. Note
575 that the scope of schematic variables is spread over the main goal
576 statement. Instantiations may be given as well, see also ML tactic
577 \texttt{cut_inst_tac} in \cite[\S3]{isabelle-ref}.
579 \item [$thin_tac~\phi$] deletes the specified assumption from a subgoal; note
580 that $\phi$ may contain schematic variables. See also \texttt{thin_tac} in
581 \cite[\S3]{isabelle-ref}.
583 \item [$subgoal_tac~\phi$] adds $\phi$ as an assumption to a subgoal. See
584 also \texttt{subgoal_tac} and \texttt{subgoals_tac} in
585 \cite[\S3]{isabelle-ref}.
587 \item [$rename_tac~\vec x$] renames parameters of a goal according to the list
588 $\vec x$, which refers to the \emph{suffix} of variables.
590 \item [$rotate_tac~n$] rotates the assumptions of a goal by $n$ positions:
591 from right to left if $n$ is positive, and from left to right if $n$ is
592 negative; the default value is $1$. See also \texttt{rotate_tac} in
593 \cite[\S3]{isabelle-ref}.
595 \item [$tactic~text$] produces a proof method from any ML text of type
596 \texttt{tactic}. Apart from the usual ML environment and the current
597 implicit theory context, the ML code may refer to the following locally
600 {\footnotesize\begin{verbatim}
601 val ctxt : Proof.context
603 val thm : string -> thm
604 val thms : string -> thm list
606 Here \texttt{ctxt} refers to the current proof context, \texttt{facts}
607 indicates any current facts for forward-chaining, and
608 \texttt{thm}~/~\texttt{thms} retrieve named facts (including global
609 theorems) from the context.
613 \subsection{The Simplifier}\label{sec:simplifier}
615 \subsubsection{Simplification methods}
617 \indexisarmeth{simp}\indexisarmeth{simp-all}
618 \begin{matharray}{rcl}
619 simp & : & \isarmeth \\
620 simp_all & : & \isarmeth \\
623 \railalias{simpall}{simp\_all}
626 \railalias{noasm}{no\_asm}
629 \railalias{noasmsimp}{no\_asm\_simp}
632 \railalias{noasmuse}{no\_asm\_use}
635 \indexouternonterm{simpmod}
637 ('simp' | simpall) ('!' ?) opt? (simpmod *)
640 opt: '(' (noasm | noasmsimp | noasmuse) ')'
642 simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
643 'split' (() | 'add' | 'del')) ':' thmrefs
649 \item [$simp$] invokes Isabelle's simplifier, after declaring additional rules
650 according to the arguments given. Note that the \railtterm{only} modifier
651 first removes all other rewrite rules, congruences, and looper tactics
652 (including splits), and then behaves like \railtterm{add}.
654 \medskip The \railtterm{cong} modifiers add or delete Simplifier congruence
655 rules (see also \cite{isabelle-ref}), the default is to add.
657 \medskip The \railtterm{split} modifiers add or delete rules for the
658 Splitter (see also \cite{isabelle-ref}), the default is to add. This works
659 only if the Simplifier method has been properly setup to include the
660 Splitter (all major object logics such HOL, HOLCF, FOL, ZF do this already).
662 \item [$simp_all$] is similar to $simp$, but acts on all goals (backwards from
663 the last to the first one).
667 By default the Simplifier methods take local assumptions fully into account,
668 using equational assumptions in the subsequent normalization process, or
669 simplifying assumptions themselves (cf.\ \texttt{asm_full_simp_tac} in
670 \cite[\S10]{isabelle-ref}). In structured proofs this is usually quite well
671 behaved in practice: just the local premises of the actual goal are involved,
672 additional facts may be inserted via explicit forward-chaining (using $\THEN$,
673 $\FROMNAME$ etc.). The full context of assumptions is only included if the
674 ``$!$'' (bang) argument is given, which should be used with some care, though.
676 Additional Simplifier options may be specified to tune the behavior further
677 (mostly for unstructured scripts with many accidental local facts):
678 ``$(no_asm)$'' means assumptions are ignored completely (cf.\
679 \texttt{simp_tac}), ``$(no_asm_simp)$'' means assumptions are used in the
680 simplification of the conclusion but are not themselves simplified (cf.\
681 \texttt{asm_simp_tac}), and ``$(no_asm_use)$'' means assumptions are
682 simplified but are not used in the simplification of each other or the
683 conclusion (cf.\ \texttt{full_simp_tac}).
687 The Splitter package is usually configured to work as part of the Simplifier.
688 The effect of repeatedly applying \texttt{split_tac} can be simulated by
689 ``$(simp~only\colon~split\colon~\vec a)$''. There is also a separate $split$
690 method available for single-step case splitting.
693 \subsubsection{Declaring rules}
695 \indexisarcmd{print-simpset}
696 \indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong}
697 \begin{matharray}{rcl}
698 \isarcmd{print_simpset}^* & : & \isarkeep{theory~|~proof} \\
699 simp & : & \isaratt \\
700 cong & : & \isaratt \\
701 split & : & \isaratt \\
705 ('simp' | 'cong' | 'split') (() | 'add' | 'del')
711 \item [$\isarcmd{print_simpset}$] prints the collection of rules declared to
712 the Simplifier, which is also known as ``simpset'' internally
713 \cite{isabelle-ref}. This is a diagnostic command; $undo$ does not apply.
715 \item [$simp$] declares simplification rules.
717 \item [$cong$] declares congruence rules.
719 \item [$split$] declares case split rules.
724 \subsubsection{Forward simplification}
726 \indexisaratt{simplified}
727 \begin{matharray}{rcl}
728 simplified & : & \isaratt \\
732 'simplified' opt? thmrefs?
735 opt: '(' (noasm | noasmsimp | noasmuse) ')'
741 \item [$simplified~\vec a$] causes a theorem to be simplified, either by
742 exactly the specified rules $\vec a$, or the implicit Simplifier context if
743 no arguments are given. The result is fully simplified by default,
744 including assumptions and conclusion; the options $no_asm$ etc.\ tune the
745 Simplifier in the same way as the for the $simp$ method.
747 Note that forward simplification restricts the simplifier to its most basic
748 operation of term rewriting; solver and looper tactics \cite{isabelle-ref}
749 are \emph{not} involved here. The $simplified$ attribute should be only
750 rarely required under normal circumstances.
755 \subsubsection{Low-level equational reasoning}
757 \indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisarmeth{split}
758 \begin{matharray}{rcl}
759 subst^* & : & \isarmeth \\
760 hypsubst^* & : & \isarmeth \\
761 split^* & : & \isarmeth \\
767 'split' ('(' 'asm' ')')? thmrefs
771 These methods provide low-level facilities for equational reasoning that are
772 intended for specialized applications only. Normally, single step
773 calculations would be performed in a structured text (see also
774 \S\ref{sec:calculation}), while the Simplifier methods provide the canonical
775 way for automated normalization (see \S\ref{sec:simplifier}).
779 \item [$subst~a$] performs a single substitution step using rule $a$, which
780 may be either a meta or object equality.
782 \item [$hypsubst$] performs substitution using some assumption; this only
783 works for equations of the form $x = t$ where $x$ is a free or bound
786 \item [$split~\vec a$] performs single-step case splitting using rules $thms$.
787 By default, splitting is performed in the conclusion of a goal; the $asm$
788 option indicates to operate on assumptions instead.
790 Note that the $simp$ method already involves repeated application of split
791 rules as declared in the current context.
795 \subsection{The Classical Reasoner}\label{sec:classical}
797 \subsubsection{Basic methods}
799 \indexisarmeth{rule}\indexisarmeth{default}\indexisarmeth{contradiction}
800 \indexisarmeth{intro}\indexisarmeth{elim}
801 \begin{matharray}{rcl}
802 rule & : & \isarmeth \\
803 contradiction & : & \isarmeth \\
804 intro & : & \isarmeth \\
805 elim & : & \isarmeth \\
809 ('rule' | 'intro' | 'elim') thmrefs?
815 \item [$rule$] as offered by the classical reasoner is a refinement over the
816 primitive one (see \S\ref{sec:pure-meth-att}). Both versions essentially
817 work the same, but the classical version observes the classical rule context
818 in addition to that of Isabelle/Pure.
820 Common object logics (HOL, ZF, etc.) declare a rich collection of classical
821 rules (even if these would qualify as intuitionistic ones), but only few
822 declarations to the rule context of Isabelle/Pure
823 (\S\ref{sec:pure-meth-att}).
825 \item [$contradiction$] solves some goal by contradiction, deriving any result
826 from both $\neg A$ and $A$. Chained facts, which are guaranteed to
827 participate, may appear in either order.
829 \item [$intro$ and $elim$] repeatedly refine some goal by intro- or
830 elim-resolution, after having inserted any chained facts. Exactly the rules
831 given as arguments are taken into account; this allows fine-tuned
832 decomposition of a proof problem, in contrast to common automated tools.
837 \subsubsection{Automated methods}
839 \indexisarmeth{blast}\indexisarmeth{fast}\indexisarmeth{slow}
840 \indexisarmeth{best}\indexisarmeth{safe}\indexisarmeth{clarify}
841 \begin{matharray}{rcl}
842 blast & : & \isarmeth \\
843 fast & : & \isarmeth \\
844 slow & : & \isarmeth \\
845 best & : & \isarmeth \\
846 safe & : & \isarmeth \\
847 clarify & : & \isarmeth \\
850 \indexouternonterm{clamod}
852 'blast' ('!' ?) nat? (clamod *)
854 ('fast' | 'slow' | 'best' | 'safe' | 'clarify') ('!' ?) (clamod *)
857 clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs
862 \item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac}
863 in \cite[\S11]{isabelle-ref}). The optional argument specifies a
864 user-supplied search bound (default 20).
865 \item [$fast$, $slow$, $best$, $safe$, and $clarify$] refer to the generic
866 classical reasoner. See \texttt{fast_tac}, \texttt{slow_tac},
867 \texttt{best_tac}, \texttt{safe_tac}, and \texttt{clarify_tac} in
868 \cite[\S11]{isabelle-ref} for more information.
871 Any of the above methods support additional modifiers of the context of
872 classical rules. Their semantics is analogous to the attributes given before.
873 Facts provided by forward chaining are inserted into the goal before
874 commencing proof search. The ``!''~argument causes the full context of
875 assumptions to be included as well.
878 \subsubsection{Combined automated methods}\label{sec:clasimp}
880 \indexisarmeth{auto}\indexisarmeth{force}\indexisarmeth{clarsimp}
881 \indexisarmeth{fastsimp}\indexisarmeth{slowsimp}\indexisarmeth{bestsimp}
882 \begin{matharray}{rcl}
883 auto & : & \isarmeth \\
884 force & : & \isarmeth \\
885 clarsimp & : & \isarmeth \\
886 fastsimp & : & \isarmeth \\
887 slowsimp & : & \isarmeth \\
888 bestsimp & : & \isarmeth \\
891 \indexouternonterm{clasimpmod}
893 'auto' '!'? (nat nat)? (clasimpmod *)
895 ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') '!'? (clasimpmod *)
898 clasimpmod: ('simp' (() | 'add' | 'del' | 'only') |
899 ('cong' | 'split') (() | 'add' | 'del') |
900 'iff' (((() | 'add') '?'?) | 'del') |
901 (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' thmrefs
905 \item [$auto$, $force$, $clarsimp$, $fastsimp$, $slowsimp$, and $bestsimp$]
906 provide access to Isabelle's combined simplification and classical reasoning
907 tactics. These correspond to \texttt{auto_tac}, \texttt{force_tac},
908 \texttt{clarsimp_tac}, and Classical Reasoner tactics with the Simplifier
909 added as wrapper, see \cite[\S11]{isabelle-ref} for more information. The
910 modifier arguments correspond to those given in \S\ref{sec:simplifier} and
911 \S\ref{sec:classical}. Just note that the ones related to the Simplifier
912 are prefixed by \railtterm{simp} here.
914 Facts provided by forward chaining are inserted into the goal before doing
915 the search. The ``!''~argument causes the full context of assumptions to be
920 \subsubsection{Declaring rules}
922 \indexisarcmd{print-claset}
923 \indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
924 \indexisaratt{iff}\indexisaratt{rule}
925 \begin{matharray}{rcl}
926 \isarcmd{print_claset}^* & : & \isarkeep{theory~|~proof} \\
927 intro & : & \isaratt \\
928 elim & : & \isaratt \\
929 dest & : & \isaratt \\
930 rule & : & \isaratt \\
931 iff & : & \isaratt \\
935 ('intro' | 'elim' | 'dest') ('!' | () | '?')
939 'iff' (((() | 'add') '?'?) | 'del')
945 \item [$\isarcmd{print_claset}$] prints the collection of rules declared to
946 the Classical Reasoner, which is also known as ``simpset'' internally
947 \cite{isabelle-ref}. This is a diagnostic command; $undo$ does not apply.
949 \item [$intro$, $elim$, and $dest$] declare introduction, elimination, and
950 destruction rules, respectively. By default, rules are considered as
951 \emph{unsafe} (i.e.\ not applied blindly without backtracking), while a
952 single ``!'' classifies as \emph{safe}. Rule declarations marked by ``?''
953 coincide with those of Isabelle/Pure, cf.\ \S\ref{sec:pure-meth-att} (i.e.\
954 are only applied in single steps of the $rule$ method).
956 \item [$rule~del$] deletes introduction, elimination, or destruction rules from
959 \item [$iff$] declares logical equivalences to the Simplifier and the
960 Classical reasoner at the same time. Non-conditional rules result in a
961 ``safe'' introduction and elimination pair; conditional ones are considered
962 ``unsafe''. Rules with negative conclusion are automatically inverted
963 (using $\neg$ elimination internally).
965 The ``?'' version of $iff$ declares rules to the Isabelle/Pure context only,
966 and omits the Simplifier declaration.
971 \subsubsection{Classical operations}
973 \indexisaratt{elim-format}\indexisaratt{swapped}
975 \begin{matharray}{rcl}
976 elim_format & : & \isaratt \\
977 swapped & : & \isaratt \\
982 \item [$elim_format$] turns a destruction rule into elimination rule format;
983 this operation is similar to the the intuitionistic version
984 (\S\ref{sec:misc-meth-att}), but each premise of the resulting rule acquires
985 an additional local fact of the negated main thesis; according to the
986 classical principle $(\neg A \Imp A) \Imp A$.
988 \item [$swapped$] turns an introduction rule into an elimination, by resolving
989 with the classical swap principle $(\neg B \Imp A) \Imp (\neg A \Imp B)$.
994 \subsection{Proof by cases and induction}\label{sec:cases-induct}
996 \subsubsection{Rule contexts}
998 \indexisarcmd{case}\indexisarcmd{print-cases}
999 \indexisaratt{case-names}\indexisaratt{params}\indexisaratt{consumes}
1000 \begin{matharray}{rcl}
1001 \isarcmd{case} & : & \isartrans{proof(state)}{proof(state)} \\
1002 \isarcmd{print_cases}^* & : & \isarkeep{proof} \\
1003 case_names & : & \isaratt \\
1004 params & : & \isaratt \\
1005 consumes & : & \isaratt \\
1008 Basically, Isar proof contexts are built up explicitly using commands like
1009 $\FIXNAME$, $\ASSUMENAME$ etc.\ (see \S\ref{sec:proof-context}). In typical
1010 verification tasks this can become hard to manage, though. In particular, a
1011 large number of local contexts may emerge from case analysis or induction over
1012 inductive sets and types.
1016 The $\CASENAME$ command provides a shorthand to refer to certain parts of
1017 logical context symbolically. Proof methods may provide an environment of
1018 named ``cases'' of the form $c\colon \vec x, \vec \phi$. Then the effect of
1019 ``$\CASE{c}$'' is that of ``$\FIX{\vec x}~\ASSUME{c}{\vec\phi}$''. Term
1020 bindings may be covered as well, such as $\Var{case}$ for the intended
1023 Normally the ``terminology'' of a case value (i.e.\ the parameters $\vec x$)
1024 are marked as hidden. Using the explicit form ``$\CASE{(c~\vec x)}$'' enables
1025 proof writers to choose their own names for the subsequent proof text.
1029 It is important to note that $\CASENAME$ does \emph{not} provide direct means
1030 to peek at the current goal state, which is generally considered
1031 non-observable in Isar. The text of the cases basically emerge from standard
1032 elimination or induction rules, which in turn are derived from previous theory
1033 specifications in a canonical way (say from $\isarkeyword{inductive}$
1036 Named cases may be exhibited in the current proof context only if both the
1037 proof method and the rules involved support this. Case names and parameters
1038 of basic rules may be declared by hand as well, by using appropriate
1039 attributes. Thus variant versions of rules that have been derived manually
1040 may be used in advanced case analysis later.
1042 \railalias{casenames}{case\_names}
1043 \railterm{casenames}
1046 'case' (caseref | '(' caseref ((name | underscore) +) ')')
1048 caseref: nameref attributes?
1053 'params' ((name *) + 'and')
1061 \item [$\CASE{(c~\vec x)}$] invokes a named local context $c\colon \vec x,
1062 \vec \phi$, as provided by an appropriate proof method (such as $cases$ and
1063 $induct$, see \S\ref{sec:cases-induct-meth}). The command ``$\CASE{(c~\vec
1064 x)}$'' abbreviates ``$\FIX{\vec x}~\ASSUME{c}{\vec\phi}$''.
1066 \item [$\isarkeyword{print_cases}$] prints all local contexts of the current
1067 state, using Isar proof language notation. This is a diagnostic command;
1068 $undo$ does not apply.
1070 \item [$case_names~\vec c$] declares names for the local contexts of premises
1071 of some theorem; $\vec c$ refers to the \emph{suffix} of the list of
1074 \item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of
1075 premises $1, \dots, n$ of some theorem. An empty list of names may be given
1076 to skip positions, leaving the present parameters unchanged.
1078 Note that the default usage of case rules does \emph{not} directly expose
1079 parameters to the proof context (see also \S\ref{sec:cases-induct-meth}).
1081 \item [$consumes~n$] declares the number of ``major premises'' of a rule,
1082 i.e.\ the number of facts to be consumed when it is applied by an
1083 appropriate proof method (cf.\ \S\ref{sec:cases-induct-meth}). The default
1084 value of $consumes$ is $n = 1$, which is appropriate for the usual kind of
1085 cases and induction rules for inductive sets (cf.\
1086 \S\ref{sec:hol-inductive}). Rules without any $consumes$ declaration given
1087 are treated as if $consumes~0$ had been specified.
1089 Note that explicit $consumes$ declarations are only rarely needed; this is
1090 already taken care of automatically by the higher-level $cases$ and $induct$
1091 declarations, see also \S\ref{sec:cases-induct-att}.
1096 \subsubsection{Proof methods}\label{sec:cases-induct-meth}
1098 \indexisarmeth{cases}\indexisarmeth{induct}
1099 \begin{matharray}{rcl}
1100 cases & : & \isarmeth \\
1101 induct & : & \isarmeth \\
1104 The $cases$ and $induct$ methods provide a uniform interface to case analysis
1105 and induction over datatypes, inductive sets, and recursive functions. The
1106 corresponding rules may be specified and instantiated in a casual manner.
1107 Furthermore, these methods provide named local contexts that may be invoked
1108 via the $\CASENAME$ proof command within the subsequent proof text. This
1109 accommodates compact proof texts even when reasoning about large
1118 spec: open? args rule?
1120 open: '(' 'open' ')'
1122 args: (insts * 'and')
1124 rule: ('type' | 'set') ':' nameref | 'rule' ':' thmref
1130 \item [$cases~insts~R$] applies method $rule$ with an appropriate case
1131 distinction theorem, instantiated to the subjects $insts$. Symbolic case
1132 names are bound according to the rule's local contexts.
1134 The rule is determined as follows, according to the facts and arguments
1135 passed to the $cases$ method:
1136 \begin{matharray}{llll}
1137 \Text{facts} & & \Text{arguments} & \Text{rule} \\\hline
1138 & cases & & \Text{classical case split} \\
1139 & cases & t & \Text{datatype exhaustion (type of $t$)} \\
1140 \edrv a \in A & cases & \dots & \Text{inductive set elimination (of $A$)} \\
1141 \dots & cases & \dots ~ R & \Text{explicit rule $R$} \\
1144 Several instantiations may be given, referring to the \emph{suffix} of
1145 premises of the case rule; within each premise, the \emph{prefix} of
1146 variables is instantiated. In most situations, only a single term needs to
1147 be specified; this refers to the first variable of the last premise (it is
1148 usually the same for all cases).
1150 The ``$(open)$'' option causes the parameters of the new local contexts to
1151 be exposed to the current proof context. Thus local variables stemming from
1152 distant parts of the theory development may be introduced in an implicit
1153 manner, which can be quite confusing to the reader. Furthermore, this
1154 option may cause unwanted hiding of existing local variables, resulting in
1155 less robust proof texts.
1157 \item [$induct~insts~R$] is analogous to the $cases$ method, but refers to
1158 induction rules, which are determined as follows:
1159 \begin{matharray}{llll}
1160 \Text{facts} & & \Text{arguments} & \Text{rule} \\\hline
1161 & induct & P ~ x ~ \dots & \Text{datatype induction (type of $x$)} \\
1162 \edrv x \in A & induct & \dots & \Text{set induction (of $A$)} \\
1163 \dots & induct & \dots ~ R & \Text{explicit rule $R$} \\
1166 Several instantiations may be given, each referring to some part of a mutual
1167 inductive definition or datatype --- only related partial induction rules
1168 may be used together, though. Any of the lists of terms $P, x, \dots$
1169 refers to the \emph{suffix} of variables present in the induction rule.
1170 This enables the writer to specify only induction variables, or both
1171 predicates and variables, for example.
1173 The ``$(open)$'' option works the same way as for $cases$.
1177 Above methods produce named local contexts, as determined by the instantiated
1178 rule as specified in the text. Beyond that, the $induct$ method guesses
1179 further instantiations from the goal specification itself. Any persisting
1180 unresolved schematic variables of the resulting rule will render the the
1181 corresponding case invalid. The term binding $\Var{case}$\indexisarvar{case}
1182 for the conclusion will be provided with each case, provided that term is
1185 The $\isarkeyword{print_cases}$ command prints all named cases present in the
1186 current proof state.
1190 It is important to note that there is a fundamental difference of the $cases$
1191 and $induct$ methods in handling of non-atomic goal statements: $cases$ just
1192 applies a certain rule in backward fashion, splitting the result into new
1193 goals with the local contexts being augmented in a purely monotonic manner.
1195 In contrast, $induct$ passes the full goal statement through the ``recursive''
1196 course involved in the induction. Thus the original statement is basically
1197 replaced by separate copies, corresponding to the induction hypotheses and
1198 conclusion; the original goal context is no longer available. This behavior
1199 allows \emph{strengthened induction predicates} to be expressed concisely as
1200 meta-level rule statements, i.e.\ $\All{\vec x} \vec\phi \Imp \psi$ to
1201 indicate ``variable'' parameters $\vec x$ and ``recursive'' assumptions
1202 $\vec\phi$. Also note that local definitions may be expressed as $\All{\vec
1203 x} n \equiv t[\vec x] \Imp \phi[n]$, with induction over $n$.
1207 Facts presented to either method are consumed according to the number of
1208 ``major premises'' of the rule involved (see also \S\ref{sec:cases-induct}),
1209 which is usually $0$ for plain cases and induction rules of datatypes etc.\
1210 and $1$ for rules of inductive sets and the like. The remaining facts are
1211 inserted into the goal verbatim before the actual $cases$ or $induct$ rule is
1212 applied (thus facts may be even passed through an induction).
1215 \subsubsection{Declaring rules}\label{sec:cases-induct-att}
1217 \indexisarcmd{print-induct-rules}\indexisaratt{cases}\indexisaratt{induct}
1218 \begin{matharray}{rcl}
1219 \isarcmd{print_induct_rules}^* & : & \isarkeep{theory~|~proof} \\
1220 cases & : & \isaratt \\
1221 induct & : & \isaratt \\
1230 spec: ('type' | 'set') ':' nameref
1236 \item [$\isarkeyword{print_induct_rules}$] prints cases and induct rules for
1237 sets and types of the current context.
1239 \item [$cases$ and $induct$] (as attributes) augment the corresponding context
1240 of rules for reasoning about inductive sets and types, using the
1241 corresponding methods of the same name. Certain definitional packages of
1242 object-logics usually declare emerging cases and induction rules as
1243 expected, so users rarely need to intervene.
1245 Manual rule declarations usually include the the $case_names$ and $ps$
1246 attributes to adjust names of cases and parameters of a rule (see
1247 \S\ref{sec:cases-induct}); the $consumes$ declaration is taken care of
1248 automatically: $consumes~0$ is specified for ``type'' rules and $consumes~1$
1253 %%% Local Variables:
1255 %%% TeX-master: "isar-ref"