author  nipkow 
Wed, 04 Aug 2004 11:25:08 +0200  
changeset 15106  e8cef6993701 
parent 14605  9de4d64eee3b 
child 15763  b901a127ac73 
permissions  rwrr 
7135  1 

13048  2 
\chapter{Generic tools and packages}\label{ch:gentools} 
7167  3 

12621  4 
\section{Theory specification commands} 
12618  5 

6 
\subsection{Axiomatic type classes}\label{sec:axclass} 

7167  7 

8517  8 
\indexisarcmd{axclass}\indexisarcmd{instance}\indexisarmeth{introclasses} 
7167  9 
\begin{matharray}{rcl} 
8517  10 
\isarcmd{axclass} & : & \isartrans{theory}{theory} \\ 
11 
\isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\ 

12 
intro_classes & : & \isarmeth \\ 

7167  13 
\end{matharray} 
14 

8517  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 

8547  17 
may make use of this lightweight mechanism of abstract theories 
8901  18 
\cite{Wenzel:1997:TPHOL}. There is also a tutorial on using axiomatic type 
13024  19 
classes in Isabelle \cite{isabelleaxclass} that is part of the standard 
8901  20 
Isabelle documentation. 
8517  21 

7167  22 
\begin{rail} 
12879  23 
'axclass' classdecl (axmdecl prop +) 
8517  24 
; 
14605
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
14212
diff
changeset

25 
'instance' (nameref ('<'  subseteq) nameref  nameref '::' arity) 
7167  26 
; 
27 
\end{rail} 

28 

29 
\begin{descr} 

13041  30 

13024  31 
\item [$\AXCLASS~c \subseteq \vec c~~axms$] defines an axiomatic type class as 
11100
34d58b1818f4
\<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents:
11095
diff
changeset

32 
the intersection of existing classes, with additional axioms holding. Class 
10223  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 

12976  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 

37 
of this class. 

13041  38 

12976  39 
The ``axioms'' are stored as theorems according to the given name 
13039  40 
specifications, adding the class name $c$ as name space prefix; the same 
41 
facts are also stored collectively as $c{\dtt}axioms$. 

14605
9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
14212
diff
changeset

42 

9de4d64eee3b
'instance' and intro_classes now handle general sorts;
wenzelm
parents:
14212
diff
changeset

43 
\item [$\INSTANCE~c@1 \subseteq c@2$ and $\INSTANCE~t :: (\vec s)s$] setup a 
11100
34d58b1818f4
\<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents:
11095
diff
changeset

44 
goal stating a class relation or type arity. The proof would usually 
34d58b1818f4
\<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents:
11095
diff
changeset

45 
proceed by $intro_classes$, and then establish the characteristic theorems 
34d58b1818f4
\<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents:
11095
diff
changeset

46 
of the type classes involved. After finishing the proof, the theory will be 
34d58b1818f4
\<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents:
11095
diff
changeset

47 
augmented by a type signature declaration corresponding to the resulting 
34d58b1818f4
\<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents:
11095
diff
changeset

48 
theorem. 
13041  49 

8517  50 
\item [$intro_classes$] repeatedly expands all class introduction rules of 
10858  51 
this theory. Note that this method usually needs not be named explicitly, 
13040  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. 

13027  55 

7167  56 
\end{descr} 
57 

7315  58 

12618  59 
\subsection{Locales and local contexts}\label{sec:locale} 
60 

13040  61 
Locales are named local contexts, consisting of a list of declaration elements 
13041  62 
that are modeled after the Isar proof context commands (cf.\ 
13040  63 
\S\ref{sec:proofcontext}). 
12976  64 

13048  65 

12976  66 
\subsubsection{Localized commands} 
12618  67 

12976  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. 

12967  72 

12976  73 
\indexouternonterm{locale} 
12967  74 
\begin{rail} 
75 
locale: '(' 'in' name ')' 

76 
; 

12976  77 
\end{rail} 
12967  78 

12976  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. 

82 

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 

13041  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, 

13411  91 
fact declarations of the locale are active during the proof as well (e.g.\ 
13041  92 
local $simp$ rules). 
12976  93 

13411  94 
As a general principle, results exported from a locale context acquire 
95 
additional premises according to the specification. Usually this is only a 

96 
single predicate according to the standard ``closed'' view of locale 

97 
specifications. 

98 

12976  99 

100 
\subsubsection{Locale specifications} 

101 

102 
\indexisarcmd{locale}\indexisarcmd{printlocale}\indexisarcmd{printlocales} 

103 
\begin{matharray}{rcl} 

104 
\isarcmd{locale} & : & \isarkeep{theory} \\ 

105 
\isarcmd{print_locale}^* & : & \isarkeep{theory~~proof} \\ 

106 
\isarcmd{print_locales}^* & : & \isarkeep{theory~~proof} \\ 

107 
\end{matharray} 

108 

109 
\indexouternonterm{contextexpr}\indexouternonterm{contextelem} 

110 

111 
\railalias{printlocale}{print\_locale} 

112 
\railterm{printlocale} 

113 

114 
\begin{rail} 

13411  115 
'locale' ('(open)')? name ('=' localeexpr)? 
12976  116 
; 
117 
printlocale localeexpr 

118 
; 

119 
localeexpr: ((contextexpr '+' (contextelem+))  contextexpr  (contextelem+)) 

120 
; 

121 

122 
contextexpr: nameref  '(' contextexpr ')'  

123 
(contextexpr (name+))  (contextexpr + '+') 

124 
; 

125 
contextelem: fixes  assumes  defines  notes  includes 

126 
; 

127 
fixes: 'fixes' (name ('::' type)? structmixfix? + 'and') 

128 
; 

129 
assumes: 'assumes' (thmdecl? props + 'and') 

130 
; 

131 
defines: 'defines' (thmdecl? prop proppat? + 'and') 

132 
; 

133 
notes: 'notes' (thmdef? thmrefs + 'and') 

134 
; 

135 
includes: 'includes' contextexpr 

136 
; 

12967  137 
\end{rail} 
12618  138 

12976  139 
\begin{descr} 
13411  140 

141 
\item [$\LOCALE~loc~=~import~+~body$] defines a new locale $loc$ as a context 

12976  142 
consisting of a certain view of existing locales ($import$) plus some 
143 
additional elements ($body$). Both $import$ and $body$ are optional; the 

13024  144 
degenerate form $\LOCALE~loc$ defines an empty locale, which may still be 
145 
useful to collect declarations of facts later on. Typeinference on locale 

12976  146 
expressions automatically takes care of the most general typing that the 
147 
combined context elements may acquire. 

13041  148 

12976  149 
The $import$ consists of a structured context expression, consisting of 
150 
references to existing locales, renamed contexts, or merged contexts. 

151 
Renaming uses positional notation: $c~\vec x$ means that (a prefix) the 

152 
fixed parameters of context $c$ are named according to $\vec x$; a 

153 
``\texttt{_}'' (underscore).\indexisarthm{_@\texttt{_}} means to skip that 

154 
position. Also note that concrete syntax only works with the original name. 

13041  155 
Merging proceeds from lefttoright, suppressing any duplicates stemming 
156 
from different paths through the import hierarchy. 

157 

12976  158 
The $body$ consists of basic context elements, further context expressions 
159 
may be included as well. 

160 

161 
\begin{descr} 

13041  162 

12976  163 
\item [$\FIXES{~x::\tau~(mx)}$] declares a local parameter of type $\tau$ 
164 
and mixfix annotation $mx$ (both are optional). The special syntax 

13027  165 
declaration ``$(structure)$'' means that $x$ may be referenced 
166 
implicitly in this context. 

13041  167 

12976  168 
\item [$\ASSUMES{a}{\vec\phi}$] introduces local premises, similar to 
169 
$\ASSUMENAME$ within a proof (cf.\ \S\ref{sec:proofcontext}). 

13041  170 

12976  171 
\item [$\DEFINES{a}{x \equiv t}$] defines a previously declared parameter. 
13041  172 
This is close to $\DEFNAME$ within a proof (cf.\ 
12976  173 
\S\ref{sec:proofcontext}), but $\DEFINESNAME$ takes an equational 
13041  174 
proposition instead of variableterm pair. The lefthand side of the 
175 
equation may have additional arguments, e.g.\ ``$\DEFINES{}{f~\vec x 

176 
\equiv t}$''. 

177 

12976  178 
\item [$\NOTES{a}{\vec b}$] reconsiders facts within a local context. Most 
179 
notably, this may include arbitrary declarations in any attribute 

180 
specifications included here, e.g.\ a local $simp$ rule. 

13041  181 

12976  182 
\item [$\INCLUDES{c}$] copies the specified context in a statically scoped 
183 
manner. 

13041  184 

12976  185 
In contrast, the initial $import$ specification of a locale expression 
186 
maintains a dynamic relation to the locales being referenced (benefiting 

187 
from any later fact declarations in the obvious manner). 

188 
\end{descr} 

13411  189 

13041  190 
Note that ``$\IS{p}$'' patterns given in the syntax of $\ASSUMESNAME$ and 
13411  191 
$\DEFINESNAME$ above are illegal in locale definitions. In the long goal 
192 
format of \S\ref{sec:goals}, term bindings may be included as expected, 

193 
though. 

194 

195 
\medskip By default, locale specifications are ``closed up'' by turning the 

196 
given text into a predicate definition $loc_axioms$ and deriving the 

197 
original assumptions as local lemmas (modulo local definitions). The 

198 
predicate statement covers only the newly specified assumptions, omitting 

199 
the content of included locale expressions. The full cumulative view is 

200 
only provided on export, involving another predicate $loc$ that refers to 

201 
the complete specification text. 

202 

203 
In any case, the predicate arguments are those locale parameters that 

204 
actually occur in the respective piece of text. Also note that these 

205 
predicates operate at the metalevel in theory, but the locale packages 

206 
attempts to internalize statements according to the objectlogic setup 

207 
(e.g.\ replacing $\Forall$ by $\forall$, and $\Imp$ by $\imp$ in HOL; see 

208 
also \S\ref{sec:objectlogic}). Separate introduction rules 

209 
$loc_axioms.intro$ and $loc.intro$ are declared as well. 

210 

211 
The $(open)$ option of a locale specification prevents both the current 

212 
$loc_axioms$ and cumulative $loc$ predicate constructions. Predicates are 

213 
also omitted for empty specification texts. 

12976  214 

215 
\item [$\isarkeyword{print_locale}~import~+~body$] prints the specified locale 

216 
expression in a flattened form. The notable special case 

217 
$\isarkeyword{print_locale}~loc$ just prints the contents of the named 

218 
locale, but keep in mind that typeinference will normalize type variables 

219 
according to the usual alphabetical order. 

13041  220 

12976  221 
\item [$\isarkeyword{print_locales}$] prints the names of all locales of the 
222 
current theory. 

223 

224 
\end{descr} 

225 

12621  226 

227 
\section{Derived proof schemes} 

228 

229 
\subsection{Generalized elimination}\label{sec:obtain} 

230 

231 
\indexisarcmd{obtain} 

232 
\begin{matharray}{rcl} 

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

234 
\end{matharray} 

235 

236 
Generalized elimination means that additional elements with certain properties 

13041  237 
may be introduced in the current context, by virtue of a locally proven 
12621  238 
``soundness statement''. Technically speaking, the $\OBTAINNAME$ language 
239 
element is like a declaration of $\FIXNAME$ and $\ASSUMENAME$ (see also see 

240 
\S\ref{sec:proofcontext}), together with a soundness proof of its additional 

241 
claim. According to the nature of existential reasoning, assumptions get 

242 
eliminated from any result exported from the context later, provided that the 

243 
corresponding parameters do \emph{not} occur in the conclusion. 

244 

245 
\begin{rail} 

12879  246 
'obtain' (vars + 'and') 'where' (props + 'and') 
12621  247 
; 
248 
\end{rail} 

12618  249 

12621  250 
$\OBTAINNAME$ is defined as a derived Isar command as follows, where $\vec b$ 
251 
shall refer to (optional) facts indicated for forward chaining. 

252 
\begin{matharray}{l} 

253 
\langle facts~\vec b\rangle \\ 

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

13041  255 
\quad \HAVE{}{\All{thesis} (\All{\vec x} \vec\phi \Imp thesis) \Imp thesis} \\ 
256 
\quad \PROOF{succeed} \\ 

12621  257 
\qquad \FIX{thesis} \\ 
13041  258 
\qquad \ASSUME{that~[intro?]}{\All{\vec x} \vec\phi \Imp thesis} \\ 
13042  259 
\qquad \THUS{}{thesis} \\ 
260 
\quad\qquad \APPLY{} \\ 

13041  261 
\quad\qquad \USING{\vec b}~~\langle proof\rangle \\ 
262 
\quad \QED{} \\ 

12621  263 
\quad \FIX{\vec x}~\ASSUMENAME^\ast~a\colon~\vec\phi \\ 
264 
\end{matharray} 

265 

266 
Typically, the soundness proof is relatively straightforward, often just by 

13048  267 
canonical automated tools such as ``$\BY{simp}$'' or ``$\BY{blast}$''. 
268 
Accordingly, the ``$that$'' reduction above is declared as simplification and 

269 
introduction rule. 

12621  270 

271 
\medskip 

272 

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

274 
metalogical existential quantifiers and conjunctions. This concept has a 

13041  275 
broad range of useful applications, ranging from plain elimination (or 
12621  276 
introduction) of objectlevel existentials and conjunctions, to elimination 
277 
over results of symbolic evaluation of recursive definitions, for example. 

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

13041  279 
where the result is treated as a genuine assumption. 
12621  280 

281 

282 
\subsection{Calculational reasoning}\label{sec:calculation} 

7315  283 

8619  284 
\indexisarcmd{also}\indexisarcmd{finally} 
285 
\indexisarcmd{moreover}\indexisarcmd{ultimately} 

12976  286 
\indexisarcmd{printtransrules} 
287 
\indexisaratt{trans}\indexisaratt{sym}\indexisaratt{symmetric} 

7315  288 
\begin{matharray}{rcl} 
289 
\isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\ 

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

8619  291 
\isarcmd{moreover} & : & \isartrans{proof(state)}{proof(state)} \\ 
292 
\isarcmd{ultimately} & : & \isartrans{proof(state)}{proof(chain)} \\ 

10154  293 
\isarcmd{print_trans_rules}^* & : & \isarkeep{theory~~proof} \\ 
7315  294 
trans & : & \isaratt \\ 
12976  295 
sym & : & \isaratt \\ 
296 
symmetric & : & \isaratt \\ 

7315  297 
\end{matharray} 
298 

299 
Calculational proof is forward reasoning with implicit application of 

11332  300 
transitivity rules (such those of $=$, $\leq$, $<$). Isabelle/Isar maintains 
7391  301 
an auxiliary register $calculation$\indexisarthm{calculation} for accumulating 
7897  302 
results obtained by transitivity composed with the current result. Command 
303 
$\ALSO$ updates $calculation$ involving $this$, while $\FINALLY$ exhibits the 

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

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

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

8619  307 
$\HAVENAME$, $\SHOWNAME$ etc. The $\MOREOVER$ and $\ULTIMATELY$ commands are 
308 
similar to $\ALSO$ and $\FINALLY$, but only collect further results in 

309 
$calculation$ without applying any rules yet. 

7315  310 

13041  311 
Also note that the implicit term abbreviation ``$\dots$'' has its canonical 
312 
application with calculational proofs. It refers to the argument of the 

313 
preceding statement. (The argument of a curried infix expression happens to be 

314 
its righthand side.) 

7315  315 

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

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

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

319 
being able to nest calculations, there is no separate \emph{begincalculation} 

320 
command required. 

321 

8619  322 
\medskip 
323 

13041  324 
The Isar calculation proof commands may be defined as follows:\footnote{We 
325 
suppress internal bookkeeping such as proper handling of blockstructure.} 

8619  326 
\begin{matharray}{rcl} 
327 
\ALSO@0 & \equiv & \NOTE{calculation}{this} \\ 

9606  328 
\ALSO@{n+1} & \equiv & \NOTE{calculation}{trans~[OF~calculation~this]} \\[0.5ex] 
8619  329 
\FINALLY & \equiv & \ALSO~\FROM{calculation} \\ 
330 
\MOREOVER & \equiv & \NOTE{calculation}{calculation~this} \\ 

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

332 
\end{matharray} 

333 

7315  334 
\begin{rail} 
13024  335 
('also'  'finally') ('(' thmrefs ')')? 
8619  336 
; 
8507  337 
'trans' (()  'add'  'del') 
7315  338 
; 
339 
\end{rail} 

340 

341 
\begin{descr} 

13041  342 

8547  343 
\item [$\ALSO~(\vec a)$] maintains the auxiliary $calculation$ register as 
7315  344 
follows. The first occurrence of $\ALSO$ in some calculational thread 
7905  345 
initializes $calculation$ by $this$. Any subsequent $\ALSO$ on the same 
7335  346 
level of blockstructure updates $calculation$ by some transitivity rule 
7458  347 
applied to $calculation$ and $this$ (in that order). Transitivity rules are 
11095  348 
picked from the current context, unless alternative rules are given as 
349 
explicit arguments. 

9614  350 

8547  351 
\item [$\FINALLY~(\vec a)$] maintaining $calculation$ in the same way as 
7315  352 
$\ALSO$, and concludes the current calculational thread. The final result 
353 
is exhibited as fact for forward chaining towards the next goal. Basically, 

7987  354 
$\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$. Note that 
355 
``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and 

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

357 
calculational proofs. 

9614  358 

8619  359 
\item [$\MOREOVER$ and $\ULTIMATELY$] are analogous to $\ALSO$ and $\FINALLY$, 
360 
but collect results only, without applying rules. 

13041  361 

13024  362 
\item [$\isarkeyword{print_trans_rules}$] prints the list of transitivity 
363 
rules (for calculational commands $\ALSO$ and $\FINALLY$) and symmetry rules 

364 
(for the $symmetric$ operation and single step elimination patters) of the 

365 
current context. 

13041  366 

8547  367 
\item [$trans$] declares theorems as transitivity rules. 
13041  368 

13024  369 
\item [$sym$] declares symmetry rules. 
13041  370 

12976  371 
\item [$symmetric$] resolves a theorem with some rule declared as $sym$ in the 
372 
current context. For example, ``$\ASSUME{[symmetric]}{x = y}$'' produces a 

373 
swapped fact derived from that assumption. 

13041  374 

13024  375 
In structured proof texts it is often more appropriate to use an explicit 
376 
singlestep elimination proof, such as ``$\ASSUME{}{x = y}~\HENCE{}{y = 

13041  377 
x}~\DDOT$''. The very same rules known to $symmetric$ are declared as 
378 
$elim?$ as well. 

13027  379 

7315  380 
\end{descr} 
381 

382 

13041  383 
\section{Proof tools} 
8517  384 

12618  385 
\subsection{Miscellaneous methods and attributes}\label{sec:miscmethatt} 
8517  386 

9606  387 
\indexisarmeth{unfold}\indexisarmeth{fold}\indexisarmeth{insert} 
8517  388 
\indexisarmeth{erule}\indexisarmeth{drule}\indexisarmeth{frule} 
389 
\indexisarmeth{fail}\indexisarmeth{succeed} 

390 
\begin{matharray}{rcl} 

391 
unfold & : & \isarmeth \\ 

10741  392 
fold & : & \isarmeth \\ 
393 
insert & : & \isarmeth \\[0.5ex] 

8517  394 
erule^* & : & \isarmeth \\ 
395 
drule^* & : & \isarmeth \\ 

13024  396 
frule^* & : & \isarmeth \\ 
8517  397 
succeed & : & \isarmeth \\ 
398 
fail & : & \isarmeth \\ 

399 
\end{matharray} 

7135  400 

401 
\begin{rail} 

10741  402 
('fold'  'unfold'  'insert') thmrefs 
403 
; 

404 
('erule'  'drule'  'frule') ('('nat')')? thmrefs 

7135  405 
; 
406 
\end{rail} 

407 

7167  408 
\begin{descr} 
13041  409 

13024  410 
\item [$unfold~\vec a$ and $fold~\vec a$] expand (or fold back again) the 
411 
given metalevel definitions throughout all goals; any chained facts 

412 
provided are inserted into the goal and subject to rewriting as well. 

13041  413 

10741  414 
\item [$insert~\vec a$] inserts theorems as facts into all goals of the proof 
415 
state. Note that current facts indicated for forward chaining are ignored. 

13024  416 

8547  417 
\item [$erule~\vec a$, $drule~\vec a$, and $frule~\vec a$] are similar to the 
418 
basic $rule$ method (see \S\ref{sec:puremethatt}), but apply rules by 

8517  419 
elimresolution, destructresolution, and forwardresolution, respectively 
10741  420 
\cite{isabelleref}. The optional natural number argument (default $0$) 
13041  421 
specifies additional assumption steps to be performed here. 
422 

10741  423 
Note that these methods are improper ones, mainly serving for 
424 
experimentation and tactic script emulation. Different modes of basic rule 

425 
application are usually expressed in Isar at the proof language level, 

426 
rather than via implicit proof state manipulations. For example, a proper 

13041  427 
singlestep elimination would be done using the plain $rule$ method, with 
10741  428 
forward chaining of current facts. 
13024  429 

8517  430 
\item [$succeed$] yields a single (unchanged) result; it is the identity of 
431 
the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:synmeth}). 

13024  432 

8517  433 
\item [$fail$] yields an empty result sequence; it is the identity of the 
434 
``\texttt{}'' method combinator (cf.\ \S\ref{sec:synmeth}). 

13024  435 

7167  436 
\end{descr} 
7135  437 

10318  438 
\indexisaratt{tagged}\indexisaratt{untagged} 
9614  439 
\indexisaratt{THEN}\indexisaratt{COMP} 
14175
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13622
diff
changeset

440 
\indexisaratt{unfolded}\indexisaratt{folded} 
13027  441 
\indexisaratt{standard}\indexisarattof{Pure}{elimformat} 
13024  442 
\indexisaratt{novars} 
8517  443 
\begin{matharray}{rcl} 
9905  444 
tagged & : & \isaratt \\ 
445 
untagged & : & \isaratt \\[0.5ex] 

9614  446 
THEN & : & \isaratt \\ 
8517  447 
COMP & : & \isaratt \\[0.5ex] 
9905  448 
unfolded & : & \isaratt \\ 
449 
folded & : & \isaratt \\[0.5ex] 

9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9936
diff
changeset

450 
elim_format & : & \isaratt \\ 
13041  451 
standard^* & : & \isaratt \\ 
9936  452 
no_vars^* & : & \isaratt \\ 
8517  453 
\end{matharray} 
454 

455 
\begin{rail} 

9905  456 
'tagged' (nameref+) 
8517  457 
; 
9905  458 
'untagged' name 
8517  459 
; 
10154  460 
('THEN'  'COMP') ('[' nat ']')? thmref 
8517  461 
; 
9905  462 
('unfolded'  'folded') thmrefs 
8517  463 
; 
464 
\end{rail} 

465 

466 
\begin{descr} 

13041  467 

9905  468 
\item [$tagged~name~args$ and $untagged~name$] add and remove $tags$ of some 
8517  469 
theorem. Tags may be any list of strings that serve as comment for some 
470 
tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the 

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

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

13041  473 

474 
\item [$THEN~a$ and $COMP~a$] compose rules by resolution. $THEN$ resolves 

475 
with the first premise of $a$ (an alternative position may be also 

476 
specified); the $COMP$ version skips the automatic lifting process that is 

477 
normally intended (cf.\ \texttt{RS} and \texttt{COMP} in 

8547  478 
\cite[\S5]{isabelleref}). 
13041  479 

9905  480 
\item [$unfolded~\vec a$ and $folded~\vec a$] expand and fold back again the 
481 
given metalevel definitions throughout a rule. 

13041  482 

13027  483 
\item [$elim_format$] turns a destruction rule into elimination rule format, 
484 
by resolving with the rule $\PROP A \Imp (\PROP A \Imp \PROP B) \Imp \PROP 

485 
B$. 

13048  486 

487 
Note that the Classical Reasoner (\S\ref{sec:classical}) provides its own 

488 
version of this operation. 

13041  489 

490 
\item [$standard$] puts a theorem into the standard form of objectrules at 

491 
the outermost theory level. Note that this operation violates the local 

492 
proof context (including active locales). 

493 

9232  494 
\item [$no_vars$] replaces schematic variables by free ones; this is mainly 
495 
for tuning output of pretty printed theorems. 

13027  496 

8517  497 
\end{descr} 
7135  498 

499 

12621  500 
\subsection{Further tactic emulations}\label{sec:tactics} 
9606  501 

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

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

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

505 
dynamic instantiation within the scope of some subgoal. 

506 

507 
\begin{warn} 

14175
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13622
diff
changeset

508 
Dynamic instantiations refer to universally quantified parameters of 
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13622
diff
changeset

509 
a subgoal (the dynamic context) rather than fixed variables and term 
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13622
diff
changeset

510 
abbreviations of a (static) Isar context. 
9606  511 
\end{warn} 
512 

14175
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13622
diff
changeset

513 
Tactic emulation methods, unlike their ML counterparts, admit 
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13622
diff
changeset

514 
simultaneous instantiation from both dynamic and static contexts. If 
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13622
diff
changeset

515 
names occur in both contexts goal parameters hide locally fixed 
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13622
diff
changeset

516 
variables. Likewise, schematic variables refer to term abbreviations, 
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13622
diff
changeset

517 
if present in the static context. Otherwise the schematic variable is 
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13622
diff
changeset

518 
interpreted as a schematic variable and left to be solved by unification 
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13622
diff
changeset

519 
with certain parts of the subgoal. 
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13622
diff
changeset

520 

9606  521 
Note that the tactic emulation proof methods in Isabelle/Isar are consistently 
14175
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13622
diff
changeset

522 
named $foo_tac$. Note also that variable names occurring on left hand sides 
14212  523 
of instantiations must be preceded by a question mark if they coincide with 
524 
a keyword or contain dots. 

14175
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13622
diff
changeset

525 
This is consistent with the attribute $where$ (see \S\ref{sec:puremethatt}). 
9606  526 

527 
\indexisarmeth{ruletac}\indexisarmeth{eruletac} 

528 
\indexisarmeth{druletac}\indexisarmeth{fruletac} 

529 
\indexisarmeth{cuttac}\indexisarmeth{thintac} 

9642  530 
\indexisarmeth{subgoaltac}\indexisarmeth{renametac} 
9614  531 
\indexisarmeth{rotatetac}\indexisarmeth{tactic} 
9606  532 
\begin{matharray}{rcl} 
533 
rule_tac^* & : & \isarmeth \\ 

534 
erule_tac^* & : & \isarmeth \\ 

535 
drule_tac^* & : & \isarmeth \\ 

536 
frule_tac^* & : & \isarmeth \\ 

537 
cut_tac^* & : & \isarmeth \\ 

538 
thin_tac^* & : & \isarmeth \\ 

539 
subgoal_tac^* & : & \isarmeth \\ 

9614  540 
rename_tac^* & : & \isarmeth \\ 
541 
rotate_tac^* & : & \isarmeth \\ 

9606  542 
tactic^* & : & \isarmeth \\ 
543 
\end{matharray} 

544 

545 
\railalias{ruletac}{rule\_tac} 

546 
\railterm{ruletac} 

547 

548 
\railalias{eruletac}{erule\_tac} 

549 
\railterm{eruletac} 

550 

551 
\railalias{druletac}{drule\_tac} 

552 
\railterm{druletac} 

553 

554 
\railalias{fruletac}{frule\_tac} 

555 
\railterm{fruletac} 

556 

557 
\railalias{cuttac}{cut\_tac} 

558 
\railterm{cuttac} 

559 

560 
\railalias{thintac}{thin\_tac} 

561 
\railterm{thintac} 

562 

563 
\railalias{subgoaltac}{subgoal\_tac} 

564 
\railterm{subgoaltac} 

565 

9614  566 
\railalias{renametac}{rename\_tac} 
567 
\railterm{renametac} 

568 

569 
\railalias{rotatetac}{rotate\_tac} 

570 
\railterm{rotatetac} 

571 

9606  572 
\begin{rail} 
573 
( ruletac  eruletac  druletac  fruletac  cuttac  thintac ) goalspec? 

574 
( insts thmref  thmrefs ) 

575 
; 

576 
subgoaltac goalspec? (prop +) 

577 
; 

9614  578 
renametac goalspec? (name +) 
579 
; 

580 
rotatetac goalspec? int? 

581 
; 

9606  582 
'tactic' text 
583 
; 

584 

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

586 
; 

587 
\end{rail} 

588 

589 
\begin{descr} 

13041  590 

9606  591 
\item [$rule_tac$ etc.] do resolution of rules with explicit instantiation. 
592 
This works the same way as the ML tactics \texttt{res_inst_tac} etc. (see 

593 
\cite[\S3]{isabelleref}). 

13041  594 

595 
Multiple rules may be only given if there is no instantiation; then 

9606  596 
$rule_tac$ is the same as \texttt{resolve_tac} in ML (see 
597 
\cite[\S3]{isabelleref}). 

13041  598 

9606  599 
\item [$cut_tac$] inserts facts into the proof state as assumption of a 
600 
subgoal, see also \texttt{cut_facts_tac} in \cite[\S3]{isabelleref}. Note 

13027  601 
that the scope of schematic variables is spread over the main goal 
602 
statement. Instantiations may be given as well, see also ML tactic 

9606  603 
\texttt{cut_inst_tac} in \cite[\S3]{isabelleref}. 
13041  604 

9606  605 
\item [$thin_tac~\phi$] deletes the specified assumption from a subgoal; note 
606 
that $\phi$ may contain schematic variables. See also \texttt{thin_tac} in 

607 
\cite[\S3]{isabelleref}. 

13041  608 

9606  609 
\item [$subgoal_tac~\phi$] adds $\phi$ as an assumption to a subgoal. See 
610 
also \texttt{subgoal_tac} and \texttt{subgoals_tac} in 

611 
\cite[\S3]{isabelleref}. 

13041  612 

9614  613 
\item [$rename_tac~\vec x$] renames parameters of a goal according to the list 
614 
$\vec x$, which refers to the \emph{suffix} of variables. 

13041  615 

9614  616 
\item [$rotate_tac~n$] rotates the assumptions of a goal by $n$ positions: 
617 
from right to left if $n$ is positive, and from left to right if $n$ is 

618 
negative; the default value is $1$. See also \texttt{rotate_tac} in 

619 
\cite[\S3]{isabelleref}. 

13041  620 

9606  621 
\item [$tactic~text$] produces a proof method from any ML text of type 
622 
\texttt{tactic}. Apart from the usual ML environment and the current 

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

624 
bound values: 

625 

626 
{\footnotesize\begin{verbatim} 

627 
val ctxt : Proof.context 

628 
val facts : thm list 

629 
val thm : string > thm 

630 
val thms : string > thm list 

631 
\end{verbatim}} 

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

633 
indicates any current facts for forwardchaining, and 

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

635 
theorems) from the context. 

636 
\end{descr} 

637 

638 

12621  639 
\subsection{The Simplifier}\label{sec:simplifier} 
640 

13048  641 
\subsubsection{Simplification methods} 
12618  642 

8483  643 
\indexisarmeth{simp}\indexisarmeth{simpall} 
7315  644 
\begin{matharray}{rcl} 
645 
simp & : & \isarmeth \\ 

8483  646 
simp_all & : & \isarmeth \\ 
7315  647 
\end{matharray} 
648 

8483  649 
\railalias{simpall}{simp\_all} 
650 
\railterm{simpall} 

651 

8704  652 
\railalias{noasm}{no\_asm} 
653 
\railterm{noasm} 

654 

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

656 
\railterm{noasmsimp} 

657 

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

659 
\railterm{noasmuse} 

660 

13617  661 
\railalias{asmlr}{asm\_lr} 
662 
\railterm{asmlr} 

663 

11128  664 
\indexouternonterm{simpmod} 
7315  665 
\begin{rail} 
13027  666 
('simp'  simpall) ('!' ?) opt? (simpmod *) 
7315  667 
; 
668 

13617  669 
opt: '(' (noasm  noasmsimp  noasmuse  asmlr) ')' 
8704  670 
; 
9711  671 
simpmod: ('add'  'del'  'only'  'cong' (()  'add'  'del')  
9847  672 
'split' (()  'add'  'del')) ':' thmrefs 
7315  673 
; 
674 
\end{rail} 

675 

7321  676 
\begin{descr} 
13015  677 

8547  678 
\item [$simp$] invokes Isabelle's simplifier, after declaring additional rules 
8594  679 
according to the arguments given. Note that the \railtterm{only} modifier 
8547  680 
first removes all other rewrite rules, congruences, and looper tactics 
8594  681 
(including splits), and then behaves like \railtterm{add}. 
13041  682 

9711  683 
\medskip The \railtterm{cong} modifiers add or delete Simplifier congruence 
684 
rules (see also \cite{isabelleref}), the default is to add. 

13041  685 

9711  686 
\medskip The \railtterm{split} modifiers add or delete rules for the 
687 
Splitter (see also \cite{isabelleref}), the default is to add. This works 

688 
only if the Simplifier method has been properly setup to include the 

689 
Splitter (all major object logics such HOL, HOLCF, FOL, ZF do this already). 

13041  690 

13015  691 
\item [$simp_all$] is similar to $simp$, but acts on all goals (backwards from 
692 
the last to the first one). 

693 

7321  694 
\end{descr} 
695 

13015  696 
By default the Simplifier methods take local assumptions fully into account, 
697 
using equational assumptions in the subsequent normalization process, or 

13024  698 
simplifying assumptions themselves (cf.\ \texttt{asm_full_simp_tac} in 
13015  699 
\cite[\S10]{isabelleref}). In structured proofs this is usually quite well 
700 
behaved in practice: just the local premises of the actual goal are involved, 

13041  701 
additional facts may be inserted via explicit forwardchaining (using $\THEN$, 
13015  702 
$\FROMNAME$ etc.). The full context of assumptions is only included if the 
703 
``$!$'' (bang) argument is given, which should be used with some care, though. 

7321  704 

13015  705 
Additional Simplifier options may be specified to tune the behavior further 
13041  706 
(mostly for unstructured scripts with many accidental local facts): 
707 
``$(no_asm)$'' means assumptions are ignored completely (cf.\ 

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

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

710 
\texttt{asm_simp_tac}), and ``$(no_asm_use)$'' means assumptions are 

711 
simplified but are not used in the simplification of each other or the 

712 
conclusion (cf.\ \texttt{full_simp_tac}). 

13617  713 
For compatibility reasons, there is also an option ``$(asm_lr)$'', 
714 
which means that an assumption is only used for simplifying assumptions 

715 
which are to the right of it (cf.\ \texttt{asm_lr_simp_tac}). 

8704  716 

717 
\medskip 

718 

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

9711  720 
The effect of repeatedly applying \texttt{split_tac} can be simulated by 
13041  721 
``$(simp~only\colon~split\colon~\vec a)$''. There is also a separate $split$ 
722 
method available for singlestep case splitting. 

8483  723 

724 

12621  725 
\subsubsection{Declaring rules} 
8483  726 

8667  727 
\indexisarcmd{printsimpset} 
8638  728 
\indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong} 
7321  729 
\begin{matharray}{rcl} 
13024  730 
\isarcmd{print_simpset}^* & : & \isarkeep{theory~~proof} \\ 
7321  731 
simp & : & \isaratt \\ 
9711  732 
cong & : & \isaratt \\ 
8483  733 
split & : & \isaratt \\ 
7321  734 
\end{matharray} 
735 

736 
\begin{rail} 

9711  737 
('simp'  'cong'  'split') (()  'add'  'del') 
7321  738 
; 
739 
\end{rail} 

740 

741 
\begin{descr} 

13024  742 

743 
\item [$\isarcmd{print_simpset}$] prints the collection of rules declared to 

744 
the Simplifier, which is also known as ``simpset'' internally 

8667  745 
\cite{isabelleref}. This is a diagnostic command; $undo$ does not apply. 
13024  746 

8547  747 
\item [$simp$] declares simplification rules. 
13024  748 

8638  749 
\item [$cong$] declares congruence rules. 
13024  750 

9711  751 
\item [$split$] declares case split rules. 
13024  752 

7321  753 
\end{descr} 
7319  754 

7315  755 

12621  756 
\subsubsection{Forward simplification} 
757 

9905  758 
\indexisaratt{simplified} 
7315  759 
\begin{matharray}{rcl} 
9905  760 
simplified & : & \isaratt \\ 
7315  761 
\end{matharray} 
762 

9905  763 
\begin{rail} 
13015  764 
'simplified' opt? thmrefs? 
9905  765 
; 
766 

767 
opt: '(' (noasm  noasmsimp  noasmuse) ')' 

768 
; 

769 
\end{rail} 

7905  770 

9905  771 
\begin{descr} 
13048  772 

13015  773 
\item [$simplified~\vec a$] causes a theorem to be simplified, either by 
774 
exactly the specified rules $\vec a$, or the implicit Simplifier context if 

775 
no arguments are given. The result is fully simplified by default, 

776 
including assumptions and conclusion; the options $no_asm$ etc.\ tune the 

13048  777 
Simplifier in the same way as the for the $simp$ method. 
13041  778 

13015  779 
Note that forward simplification restricts the simplifier to its most basic 
780 
operation of term rewriting; solver and looper tactics \cite{isabelleref} 

781 
are \emph{not} involved here. The $simplified$ attribute should be only 

782 
rarely required under normal circumstances. 

783 

9905  784 
\end{descr} 
7315  785 

786 

13048  787 
\subsubsection{Lowlevel equational reasoning} 
9614  788 

12976  789 
\indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisarmeth{split} 
9614  790 
\begin{matharray}{rcl} 
13015  791 
subst^* & : & \isarmeth \\ 
9614  792 
hypsubst^* & : & \isarmeth \\ 
13015  793 
split^* & : & \isarmeth \\ 
9614  794 
\end{matharray} 
795 

796 
\begin{rail} 

797 
'subst' thmref 

798 
; 

9799  799 
'split' ('(' 'asm' ')')? thmrefs 
9703  800 
; 
9614  801 
\end{rail} 
802 

13015  803 
These methods provide lowlevel facilities for equational reasoning that are 
804 
intended for specialized applications only. Normally, single step 

805 
calculations would be performed in a structured text (see also 

806 
\S\ref{sec:calculation}), while the Simplifier methods provide the canonical 

807 
way for automated normalization (see \S\ref{sec:simplifier}). 

9614  808 

809 
\begin{descr} 

13041  810 

811 
\item [$subst~a$] performs a single substitution step using rule $a$, which 

812 
may be either a meta or object equality. 

813 

814 
\item [$hypsubst$] performs substitution using some assumption; this only 

815 
works for equations of the form $x = t$ where $x$ is a free or bound 

816 
variable. 

817 

818 
\item [$split~\vec a$] performs singlestep case splitting using rules $thms$. 

9799  819 
By default, splitting is performed in the conclusion of a goal; the $asm$ 
820 
option indicates to operate on assumptions instead. 

13048  821 

9703  822 
Note that the $simp$ method already involves repeated application of split 
13048  823 
rules as declared in the current context. 
9614  824 
\end{descr} 
825 

826 

12621  827 
\subsection{The Classical Reasoner}\label{sec:classical} 
7135  828 

13048  829 
\subsubsection{Basic methods} 
7321  830 

13024  831 
\indexisarmeth{rule}\indexisarmeth{default}\indexisarmeth{contradiction} 
832 
\indexisarmeth{intro}\indexisarmeth{elim} 

7321  833 
\begin{matharray}{rcl} 
834 
rule & : & \isarmeth \\ 

13024  835 
contradiction & : & \isarmeth \\ 
7321  836 
intro & : & \isarmeth \\ 
837 
elim & : & \isarmeth \\ 

838 
\end{matharray} 

839 

840 
\begin{rail} 

8547  841 
('rule'  'intro'  'elim') thmrefs? 
7321  842 
; 
843 
\end{rail} 

844 

845 
\begin{descr} 

13041  846 

7466  847 
\item [$rule$] as offered by the classical reasoner is a refinement over the 
13024  848 
primitive one (see \S\ref{sec:puremethatt}). Both versions essentially 
849 
work the same, but the classical version observes the classical rule context 

13041  850 
in addition to that of Isabelle/Pure. 
851 

852 
Common object logics (HOL, ZF, etc.) declare a rich collection of classical 

853 
rules (even if these would qualify as intuitionistic ones), but only few 

854 
declarations to the rule context of Isabelle/Pure 

855 
(\S\ref{sec:puremethatt}). 

856 

13024  857 
\item [$contradiction$] solves some goal by contradiction, deriving any result 
13041  858 
from both $\neg A$ and $A$. Chained facts, which are guaranteed to 
859 
participate, may appear in either order. 

9614  860 

7466  861 
\item [$intro$ and $elim$] repeatedly refine some goal by intro or 
13041  862 
elimresolution, after having inserted any chained facts. Exactly the rules 
863 
given as arguments are taken into account; this allows finetuned 

864 
decomposition of a proof problem, in contrast to common automated tools. 

865 

7321  866 
\end{descr} 
867 

868 

13048  869 
\subsubsection{Automated methods} 
7315  870 

9799  871 
\indexisarmeth{blast}\indexisarmeth{fast}\indexisarmeth{slow} 
872 
\indexisarmeth{best}\indexisarmeth{safe}\indexisarmeth{clarify} 

7321  873 
\begin{matharray}{rcl} 
9780  874 
blast & : & \isarmeth \\ 
875 
fast & : & \isarmeth \\ 

9799  876 
slow & : & \isarmeth \\ 
9780  877 
best & : & \isarmeth \\ 
878 
safe & : & \isarmeth \\ 

879 
clarify & : & \isarmeth \\ 

7321  880 
\end{matharray} 
881 

11128  882 
\indexouternonterm{clamod} 
7321  883 
\begin{rail} 
13027  884 
'blast' ('!' ?) nat? (clamod *) 
7321  885 
; 
13027  886 
('fast'  'slow'  'best'  'safe'  'clarify') ('!' ?) (clamod *) 
7321  887 
; 
888 

9408  889 
clamod: (('intro'  'elim'  'dest') ('!'  ()  '?')  'del') ':' thmrefs 
7321  890 
; 
891 
\end{rail} 

892 

893 
\begin{descr} 

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

7335  895 
in \cite[\S11]{isabelleref}). The optional argument specifies a 
10858  896 
usersupplied search bound (default 20). 
9799  897 
\item [$fast$, $slow$, $best$, $safe$, and $clarify$] refer to the generic 
898 
classical reasoner. See \texttt{fast_tac}, \texttt{slow_tac}, 

899 
\texttt{best_tac}, \texttt{safe_tac}, and \texttt{clarify_tac} in 

900 
\cite[\S11]{isabelleref} for more information. 

7321  901 
\end{descr} 
902 

13041  903 
Any of the above methods support additional modifiers of the context of 
904 
classical rules. Their semantics is analogous to the attributes given before. 

905 
Facts provided by forward chaining are inserted into the goal before 

906 
commencing proof search. The ``!''~argument causes the full context of 

907 
assumptions to be included as well. 

7321  908 

7315  909 

12621  910 
\subsubsection{Combined automated methods}\label{sec:clasimp} 
7315  911 

9799  912 
\indexisarmeth{auto}\indexisarmeth{force}\indexisarmeth{clarsimp} 
913 
\indexisarmeth{fastsimp}\indexisarmeth{slowsimp}\indexisarmeth{bestsimp} 

7321  914 
\begin{matharray}{rcl} 
9606  915 
auto & : & \isarmeth \\ 
7321  916 
force & : & \isarmeth \\ 
9438  917 
clarsimp & : & \isarmeth \\ 
9606  918 
fastsimp & : & \isarmeth \\ 
9799  919 
slowsimp & : & \isarmeth \\ 
920 
bestsimp & : & \isarmeth \\ 

7321  921 
\end{matharray} 
922 

11128  923 
\indexouternonterm{clasimpmod} 
7321  924 
\begin{rail} 
13027  925 
'auto' '!'? (nat nat)? (clasimpmod *) 
9780  926 
; 
13027  927 
('force'  'clarsimp'  'fastsimp'  'slowsimp'  'bestsimp') '!'? (clasimpmod *) 
7321  928 
; 
7315  929 

9711  930 
clasimpmod: ('simp' (()  'add'  'del'  'only')  
10031  931 
('cong'  'split') (()  'add'  'del')  
932 
'iff' (((()  'add') '?'?)  'del')  

9408  933 
(('intro'  'elim'  'dest') ('!'  ()  '?')  'del')) ':' thmrefs 
7321  934 
\end{rail} 
7315  935 

7321  936 
\begin{descr} 
9799  937 
\item [$auto$, $force$, $clarsimp$, $fastsimp$, $slowsimp$, and $bestsimp$] 
938 
provide access to Isabelle's combined simplification and classical reasoning 

939 
tactics. These correspond to \texttt{auto_tac}, \texttt{force_tac}, 

940 
\texttt{clarsimp_tac}, and Classical Reasoner tactics with the Simplifier 

941 
added as wrapper, see \cite[\S11]{isabelleref} for more information. The 

13048  942 
modifier arguments correspond to those given in \S\ref{sec:simplifier} and 
943 
\S\ref{sec:classical}. Just note that the ones related to the Simplifier 

944 
are prefixed by \railtterm{simp} here. 

9614  945 

7987  946 
Facts provided by forward chaining are inserted into the goal before doing 
947 
the search. The ``!''~argument causes the full context of assumptions to be 

948 
included as well. 

7321  949 
\end{descr} 
950 

7987  951 

13048  952 
\subsubsection{Declaring rules} 
7135  953 

8667  954 
\indexisarcmd{printclaset} 
7391  955 
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest} 
9936  956 
\indexisaratt{iff}\indexisaratt{rule} 
7321  957 
\begin{matharray}{rcl} 
13024  958 
\isarcmd{print_claset}^* & : & \isarkeep{theory~~proof} \\ 
7321  959 
intro & : & \isaratt \\ 
960 
elim & : & \isaratt \\ 

961 
dest & : & \isaratt \\ 

9936  962 
rule & : & \isaratt \\ 
7391  963 
iff & : & \isaratt \\ 
7321  964 
\end{matharray} 
7135  965 

7321  966 
\begin{rail} 
9408  967 
('intro'  'elim'  'dest') ('!'  ()  '?') 
7321  968 
; 
9936  969 
'rule' 'del' 
970 
; 

10031  971 
'iff' (((()  'add') '?'?)  'del') 
9936  972 
; 
7321  973 
\end{rail} 
7135  974 

7321  975 
\begin{descr} 
13024  976 

977 
\item [$\isarcmd{print_claset}$] prints the collection of rules declared to 

978 
the Classical Reasoner, which is also known as ``simpset'' internally 

8667  979 
\cite{isabelleref}. This is a diagnostic command; $undo$ does not apply. 
13024  980 

8517  981 
\item [$intro$, $elim$, and $dest$] declare introduction, elimination, and 
11332  982 
destruction rules, respectively. By default, rules are considered as 
9408  983 
\emph{unsafe} (i.e.\ not applied blindly without backtracking), while a 
13041  984 
single ``!'' classifies as \emph{safe}. Rule declarations marked by ``?'' 
985 
coincide with those of Isabelle/Pure, cf.\ \S\ref{sec:puremethatt} (i.e.\ 

986 
are only applied in single steps of the $rule$ method). 

13024  987 

11332  988 
\item [$rule~del$] deletes introduction, elimination, or destruction rules from 
9936  989 
the context. 
13041  990 

991 
\item [$iff$] declares logical equivalences to the Simplifier and the 

13024  992 
Classical reasoner at the same time. Nonconditional rules result in a 
993 
``safe'' introduction and elimination pair; conditional ones are considered 

994 
``unsafe''. Rules with negative conclusion are automatically inverted 

13041  995 
(using $\neg$ elimination internally). 
996 

997 
The ``?'' version of $iff$ declares rules to the Isabelle/Pure context only, 

998 
and omits the Simplifier declaration. 

999 

7321  1000 
\end{descr} 
7135  1001 

8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8195
diff
changeset

1002 

13048  1003 
\subsubsection{Classical operations} 
13027  1004 

1005 
\indexisaratt{elimformat}\indexisaratt{swapped} 

1006 

1007 
\begin{matharray}{rcl} 

1008 
elim_format & : & \isaratt \\ 

1009 
swapped & : & \isaratt \\ 

1010 
\end{matharray} 

1011 

1012 
\begin{descr} 

13041  1013 

13027  1014 
\item [$elim_format$] turns a destruction rule into elimination rule format; 
1015 
this operation is similar to the the intuitionistic version 

1016 
(\S\ref{sec:miscmethatt}), but each premise of the resulting rule acquires 

13041  1017 
an additional local fact of the negated main thesis; according to the 
13027  1018 
classical principle $(\neg A \Imp A) \Imp A$. 
13041  1019 

13027  1020 
\item [$swapped$] turns an introduction rule into an elimination, by resolving 
1021 
with the classical swap principle $(\neg B \Imp A) \Imp (\neg A \Imp B)$. 

1022 

1023 
\end{descr} 

1024 

1025 

12621  1026 
\subsection{Proof by cases and induction}\label{sec:casesinduct} 
12618  1027 

13048  1028 
\subsubsection{Rule contexts} 
12618  1029 

1030 
\indexisarcmd{case}\indexisarcmd{printcases} 

1031 
\indexisaratt{casenames}\indexisaratt{params}\indexisaratt{consumes} 

1032 
\begin{matharray}{rcl} 

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

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

1035 
case_names & : & \isaratt \\ 

1036 
params & : & \isaratt \\ 

1037 
consumes & : & \isaratt \\ 

1038 
\end{matharray} 

1039 

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

1041 
$\FIXNAME$, $\ASSUMENAME$ etc.\ (see \S\ref{sec:proofcontext}). In typical 

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

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

1044 
inductive sets and types. 

1045 

1046 
\medskip 

1047 

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

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

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

13041  1051 
``$\CASE{c}$'' is that of ``$\FIX{\vec x}~\ASSUME{c}{\vec\phi}$''. Term 
1052 
bindings may be covered as well, such as $\Var{case}$ for the intended 

1053 
conclusion. 

12618  1054 

13027  1055 
Normally the ``terminology'' of a case value (i.e.\ the parameters $\vec x$) 
13041  1056 
are marked as hidden. Using the explicit form ``$\CASE{(c~\vec x)}$'' enables 
1057 
proof writers to choose their own names for the subsequent proof text. 

12618  1058 

1059 
\medskip 

1060 

13027  1061 
It is important to note that $\CASENAME$ does \emph{not} provide direct means 
1062 
to peek at the current goal state, which is generally considered 

1063 
nonobservable in Isar. The text of the cases basically emerge from standard 

1064 
elimination or induction rules, which in turn are derived from previous theory 

13041  1065 
specifications in a canonical way (say from $\isarkeyword{inductive}$ 
1066 
definitions). 

13027  1067 

12618  1068 
Named cases may be exhibited in the current proof context only if both the 
1069 
proof method and the rules involved support this. Case names and parameters 

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

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

1072 
may be used in advanced case analysis later. 

11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1073 

12618  1074 
\railalias{casenames}{case\_names} 
1075 
\railterm{casenames} 

1076 

1077 
\begin{rail} 

13041  1078 
'case' (caseref  '(' caseref ((name  underscore) +) ')') 
12618  1079 
; 
13024  1080 
caseref: nameref attributes? 
1081 
; 

1082 

13027  1083 
casenames (name +) 
12618  1084 
; 
13027  1085 
'params' ((name *) + 'and') 
12618  1086 
; 
1087 
'consumes' nat? 

1088 
; 

1089 
\end{rail} 

1090 

1091 
\begin{descr} 

13041  1092 

1093 
\item [$\CASE{(c~\vec x)}$] invokes a named local context $c\colon \vec x, 

1094 
\vec \phi$, as provided by an appropriate proof method (such as $cases$ and 

1095 
$induct$, see \S\ref{sec:casesinductmeth}). The command ``$\CASE{(c~\vec 

1096 
x)}$'' abbreviates ``$\FIX{\vec x}~\ASSUME{c}{\vec\phi}$''. 

1097 

12618  1098 
\item [$\isarkeyword{print_cases}$] prints all local contexts of the current 
1099 
state, using Isar proof language notation. This is a diagnostic command; 

1100 
$undo$ does not apply. 

13041  1101 

12618  1102 
\item [$case_names~\vec c$] declares names for the local contexts of premises 
1103 
of some theorem; $\vec c$ refers to the \emph{suffix} of the list of 

1104 
premises. 

13041  1105 

12618  1106 
\item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of 
1107 
premises $1, \dots, n$ of some theorem. An empty list of names may be given 

1108 
to skip positions, leaving the present parameters unchanged. 

13041  1109 

12618  1110 
Note that the default usage of case rules does \emph{not} directly expose 
1111 
parameters to the proof context (see also \S\ref{sec:casesinductmeth}). 

13041  1112 

12618  1113 
\item [$consumes~n$] declares the number of ``major premises'' of a rule, 
1114 
i.e.\ the number of facts to be consumed when it is applied by an 

1115 
appropriate proof method (cf.\ \S\ref{sec:casesinductmeth}). The default 

1116 
value of $consumes$ is $n = 1$, which is appropriate for the usual kind of 

13041  1117 
cases and induction rules for inductive sets (cf.\ 
12618  1118 
\S\ref{sec:holinductive}). Rules without any $consumes$ declaration given 
1119 
are treated as if $consumes~0$ had been specified. 

13041  1120 

12618  1121 
Note that explicit $consumes$ declarations are only rarely needed; this is 
1122 
already taken care of automatically by the higherlevel $cases$ and $induct$ 

1123 
declarations, see also \S\ref{sec:casesinductatt}. 

13027  1124 

12618  1125 
\end{descr} 
1126 

1127 

12621  1128 
\subsubsection{Proof methods}\label{sec:casesinductmeth} 
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1129 

fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1130 
\indexisarmeth{cases}\indexisarmeth{induct} 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1131 
\begin{matharray}{rcl} 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1132 
cases & : & \isarmeth \\ 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1133 
induct & : & \isarmeth \\ 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1134 
\end{matharray} 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1135 

fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1136 
The $cases$ and $induct$ methods provide a uniform interface to case analysis 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1137 
and induction over datatypes, inductive sets, and recursive functions. The 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1138 
corresponding rules may be specified and instantiated in a casual manner. 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1139 
Furthermore, these methods provide named local contexts that may be invoked 
13048  1140 
via the $\CASENAME$ proof command within the subsequent proof text. This 
1141 
accommodates compact proof texts even when reasoning about large 

1142 
specifications. 

11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1143 

fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1144 
\begin{rail} 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1145 
'cases' spec 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1146 
; 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1147 
'induct' spec 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1148 
; 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1149 

13041  1150 
spec: open? args rule? 
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1151 
; 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1152 
open: '(' 'open' ')' 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1153 
; 
13041  1154 
args: (insts * 'and') 
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1155 
; 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1156 
rule: ('type'  'set') ':' nameref  'rule' ':' thmref 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1157 
; 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1158 
\end{rail} 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1159 

fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1160 
\begin{descr} 
13041  1161 

1162 
\item [$cases~insts~R$] applies method $rule$ with an appropriate case 

11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1163 
distinction theorem, instantiated to the subjects $insts$. Symbolic case 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1164 
names are bound according to the rule's local contexts. 
13041  1165 

11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1166 
The rule is determined as follows, according to the facts and arguments 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1167 
passed to the $cases$ method: 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1168 
\begin{matharray}{llll} 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1169 
\Text{facts} & & \Text{arguments} & \Text{rule} \\\hline 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1170 
& cases & & \Text{classical case split} \\ 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1171 
& cases & t & \Text{datatype exhaustion (type of $t$)} \\ 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1172 
\edrv a \in A & cases & \dots & \Text{inductive set elimination (of $A$)} \\ 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1173 
\dots & cases & \dots ~ R & \Text{explicit rule $R$} \\ 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1174 
\end{matharray} 
13041  1175 

11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1176 
Several instantiations may be given, referring to the \emph{suffix} of 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1177 
premises of the case rule; within each premise, the \emph{prefix} of 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1178 
variables is instantiated. In most situations, only a single term needs to 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1179 
be specified; this refers to the first variable of the last premise (it is 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1180 
usually the same for all cases). 
13041  1181 

1182 
The ``$(open)$'' option causes the parameters of the new local contexts to 

1183 
be exposed to the current proof context. Thus local variables stemming from 

11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1184 
distant parts of the theory development may be introduced in an implicit 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1185 
manner, which can be quite confusing to the reader. Furthermore, this 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1186 
option may cause unwanted hiding of existing local variables, resulting in 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1187 
less robust proof texts. 
13041  1188 

1189 
\item [$induct~insts~R$] is analogous to the $cases$ method, but refers to 

11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1190 
induction rules, which are determined as follows: 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1191 
\begin{matharray}{llll} 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1192 
\Text{facts} & & \Text{arguments} & \Text{rule} \\\hline 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1193 
& induct & P ~ x ~ \dots & \Text{datatype induction (type of $x$)} \\ 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1194 
\edrv x \in A & induct & \dots & \Text{set induction (of $A$)} \\ 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1195 
\dots & induct & \dots ~ R & \Text{explicit rule $R$} \\ 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1196 
\end{matharray} 
13041  1197 

11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1198 
Several instantiations may be given, each referring to some part of a mutual 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1199 
inductive definition or datatype  only related partial induction rules 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1200 
may be used together, though. Any of the lists of terms $P, x, \dots$ 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1201 
refers to the \emph{suffix} of variables present in the induction rule. 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1202 
This enables the writer to specify only induction variables, or both 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1203 
predicates and variables, for example. 
13041  1204 

1205 
The ``$(open)$'' option works the same way as for $cases$. 

13027  1206 

11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1207 
\end{descr} 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1208 

13048  1209 
Above methods produce named local contexts, as determined by the instantiated 
1210 
rule as specified in the text. Beyond that, the $induct$ method guesses 

1211 
further instantiations from the goal specification itself. Any persisting 

1212 
unresolved schematic variables of the resulting rule will render the the 

1213 
corresponding case invalid. The term binding $\Var{case}$\indexisarvar{case} 

1214 
for the conclusion will be provided with each case, provided that term is 

1215 
fully specified. 

11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1216 

13048  1217 
The $\isarkeyword{print_cases}$ command prints all named cases present in the 
1218 
current proof state. 

11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1219 

fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1220 
\medskip 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1221 

fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1222 
It is important to note that there is a fundamental difference of the $cases$ 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1223 
and $induct$ methods in handling of nonatomic goal statements: $cases$ just 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1224 
applies a certain rule in backward fashion, splitting the result into new 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1225 
goals with the local contexts being augmented in a purely monotonic manner. 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1226 

13622  1227 
In contrast, $induct$ passes the full goal statement through the 
1228 
``recursive'' course involved in the induction. Thus the original statement 

1229 
is basically replaced by separate copies, corresponding to the induction 

1230 
hypotheses and conclusion; the original goal context is no longer available. 

1231 
This behavior allows \emph{strengthened induction predicates} to be expressed 

1232 
concisely as metalevel rule statements, i.e.\ $\All{\vec x} \vec\phi \Imp 

1233 
\psi$ to indicate ``variable'' parameters $\vec x$ and ``recursive'' 

1234 
assumptions $\vec\phi$. Note that ``$\isarcmd{case}~c$'' already performs 

1235 
``$\FIX{\vec x}$''. Also note that local definitions may be expressed as 

1236 
$\All{\vec x} n \equiv t[\vec x] \Imp \phi[n]$, with induction over $n$. 

1237 

11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1238 

13425
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
13411
diff
changeset

1239 
In induction proofs, local assumptions introduced by cases are split into two 
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
13411
diff
changeset

1240 
different kinds: $hyps$ stemming from the rule and $prems$ from the goal 
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
13411
diff
changeset

1241 
statement. This is reflected in the extracted cases accordingly, so invoking 
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
13411
diff
changeset

1242 
``$\isarcmd{case}~c$'' will provide separate facts $c\mathord.hyps$ and 
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
13411
diff
changeset

1243 
$c\mathord.prems$, as well as fact $c$ to hold the allinclusive list. 
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
13411
diff
changeset

1244 

11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1245 
\medskip 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1246 

fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1247 
Facts presented to either method are consumed according to the number of 
12618  1248 
``major premises'' of the rule involved (see also \S\ref{sec:casesinduct}), 
13041  1249 
which is usually $0$ for plain cases and induction rules of datatypes etc.\ 
12618  1250 
and $1$ for rules of inductive sets and the like. The remaining facts are 
1251 
inserted into the goal verbatim before the actual $cases$ or $induct$ rule is 

1252 
applied (thus facts may be even passed through an induction). 

11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1253 

fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1254 

12621  1255 
\subsubsection{Declaring rules}\label{sec:casesinductatt} 
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1256 

fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1257 
\indexisarcmd{printinductrules}\indexisaratt{cases}\indexisaratt{induct} 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1258 
\begin{matharray}{rcl} 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1259 
\isarcmd{print_induct_rules}^* & : & \isarkeep{theory~~proof} \\ 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1260 
cases & : & \isaratt \\ 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1261 
induct & : & \isaratt \\ 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1262 
\end{matharray} 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1263 

fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1264 
\begin{rail} 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1265 
'cases' spec 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1266 
; 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1267 
'induct' spec 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1268 
; 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1269 

fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1270 
spec: ('type'  'set') ':' nameref 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1271 
; 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1272 
\end{rail} 
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset

1273 

13024  1274 
\begin{descr} 
13041  1275 

13024  1276 
\item [$\isarkeyword{print_induct_rules}$] prints cases and induct rules for 
1277 
sets and types of the current context. 

13041  1278 

13024  1279 
\item [$cases$ and $induct$] (as attributes) augment the corresponding context 
1280 
of rules for reasoning about inductive sets and types, using the 

1281 
corresponding methods of the same name. Certain definitional packages of 

1282 
objectlogics usually declare emerging cases and induction rules as 

1283 
expected, so users rarely need to intervene. 

13048  1284 

13024  1285 
Manual rule declarations usually include the the $case_names$ and $ps$ 
1286 
attributes to adjust na 