author | ballarin |
Fri, 29 Aug 2003 15:40:11 +0200 | |
changeset 14175 | dbd16ebaf907 |
parent 13622 | 9768ba6ab5e7 |
child 14212 | cd05b503ca2d |
permissions | -rw-r--r-- |
7135 | 1 |
|
13048 | 2 |
\chapter{Generic tools and packages}\label{ch:gen-tools} |
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{intro-classes} |
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 light-weight 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{isabelle-axclass} that is part of the standard |
8901 | 20 |
Isabelle documentation. |
8517 | 21 |
|
7167 | 22 |
\begin{rail} |
12879 | 23 |
'axclass' classdecl (axmdecl prop +) |
8517 | 24 |
; |
12879 | 25 |
'instance' (nameref ('<' | subseteq) nameref | nameref '::' simplearity) |
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$. |
|
13041 | 42 |
|
11100
34d58b1818f4
\<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents:
11095
diff
changeset
|
43 |
\item [$\INSTANCE~c@1 \subseteq c@2$ and $\INSTANCE~t :: (\vec s)c$] setup a |
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:proof-context}). |
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{print-locale}\indexisarcmd{print-locales} |
|
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. Type-inference 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 left-to-right, 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:proof-context}). |
|
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:proof-context}), but $\DEFINESNAME$ takes an equational |
13041 | 174 |
proposition instead of variable-term pair. The left-hand 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 meta-level in theory, but the locale packages |
|
206 |
attempts to internalize statements according to the object-logic setup |
|
207 |
(e.g.\ replacing $\Forall$ by $\forall$, and $\Imp$ by $\imp$ in HOL; see |
|
208 |
also \S\ref{sec:object-logic}). 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 type-inference 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:proof-context}), 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 straight-forward, 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 |
meta-logical existential quantifiers and conjunctions. This concept has a |
|
13041 | 275 |
broad range of useful applications, ranging from plain elimination (or |
12621 | 276 |
introduction) of object-level 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{print-trans-rules} |
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 right-hand 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{begin-calculation} |
|
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 block-structure.} |
|
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 block-structure 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 |
single-step 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:misc-meth-att} |
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 meta-level 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:pure-meth-att}), but apply rules by |
|
8517 | 419 |
elim-resolution, destruct-resolution, and forward-resolution, respectively |
10741 | 420 |
\cite{isabelle-ref}. 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 |
single-step 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:syn-meth}). |
|
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:syn-meth}). |
|
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}{elim-format} |
13024 | 442 |
\indexisaratt{no-vars} |
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]{isabelle-ref}). |
13041 | 479 |
|
9905 | 480 |
\item [$unfolded~\vec a$ and $folded~\vec a$] expand and fold back again the |
481 |
given meta-level 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 object-rules 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 |
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13622
diff
changeset
|
523 |
of instantiations must be preceded by a question mark if they contain dots. |
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13622
diff
changeset
|
524 |
This is consistent with the attribute $where$ (see \S\ref{sec:pure-meth-att}). |
9606 | 525 |
|
526 |
\indexisarmeth{rule-tac}\indexisarmeth{erule-tac} |
|
527 |
\indexisarmeth{drule-tac}\indexisarmeth{frule-tac} |
|
528 |
\indexisarmeth{cut-tac}\indexisarmeth{thin-tac} |
|
9642 | 529 |
\indexisarmeth{subgoal-tac}\indexisarmeth{rename-tac} |
9614 | 530 |
\indexisarmeth{rotate-tac}\indexisarmeth{tactic} |
9606 | 531 |
\begin{matharray}{rcl} |
532 |
rule_tac^* & : & \isarmeth \\ |
|
533 |
erule_tac^* & : & \isarmeth \\ |
|
534 |
drule_tac^* & : & \isarmeth \\ |
|
535 |
frule_tac^* & : & \isarmeth \\ |
|
536 |
cut_tac^* & : & \isarmeth \\ |
|
537 |
thin_tac^* & : & \isarmeth \\ |
|
538 |
subgoal_tac^* & : & \isarmeth \\ |
|
9614 | 539 |
rename_tac^* & : & \isarmeth \\ |
540 |
rotate_tac^* & : & \isarmeth \\ |
|
9606 | 541 |
tactic^* & : & \isarmeth \\ |
542 |
\end{matharray} |
|
543 |
||
544 |
\railalias{ruletac}{rule\_tac} |
|
545 |
\railterm{ruletac} |
|
546 |
||
547 |
\railalias{eruletac}{erule\_tac} |
|
548 |
\railterm{eruletac} |
|
549 |
||
550 |
\railalias{druletac}{drule\_tac} |
|
551 |
\railterm{druletac} |
|
552 |
||
553 |
\railalias{fruletac}{frule\_tac} |
|
554 |
\railterm{fruletac} |
|
555 |
||
556 |
\railalias{cuttac}{cut\_tac} |
|
557 |
\railterm{cuttac} |
|
558 |
||
559 |
\railalias{thintac}{thin\_tac} |
|
560 |
\railterm{thintac} |
|
561 |
||
562 |
\railalias{subgoaltac}{subgoal\_tac} |
|
563 |
\railterm{subgoaltac} |
|
564 |
||
9614 | 565 |
\railalias{renametac}{rename\_tac} |
566 |
\railterm{renametac} |
|
567 |
||
568 |
\railalias{rotatetac}{rotate\_tac} |
|
569 |
\railterm{rotatetac} |
|
570 |
||
9606 | 571 |
\begin{rail} |
572 |
( ruletac | eruletac | druletac | fruletac | cuttac | thintac ) goalspec? |
|
573 |
( insts thmref | thmrefs ) |
|
574 |
; |
|
575 |
subgoaltac goalspec? (prop +) |
|
576 |
; |
|
9614 | 577 |
renametac goalspec? (name +) |
578 |
; |
|
579 |
rotatetac goalspec? int? |
|
580 |
; |
|
9606 | 581 |
'tactic' text |
582 |
; |
|
583 |
||
584 |
insts: ((name '=' term) + 'and') 'in' |
|
585 |
; |
|
586 |
\end{rail} |
|
587 |
||
588 |
\begin{descr} |
|
13041 | 589 |
|
9606 | 590 |
\item [$rule_tac$ etc.] do resolution of rules with explicit instantiation. |
591 |
This works the same way as the ML tactics \texttt{res_inst_tac} etc. (see |
|
592 |
\cite[\S3]{isabelle-ref}). |
|
13041 | 593 |
|
594 |
Multiple rules may be only given if there is no instantiation; then |
|
9606 | 595 |
$rule_tac$ is the same as \texttt{resolve_tac} in ML (see |
596 |
\cite[\S3]{isabelle-ref}). |
|
13041 | 597 |
|
9606 | 598 |
\item [$cut_tac$] inserts facts into the proof state as assumption of a |
599 |
subgoal, see also \texttt{cut_facts_tac} in \cite[\S3]{isabelle-ref}. Note |
|
13027 | 600 |
that the scope of schematic variables is spread over the main goal |
601 |
statement. Instantiations may be given as well, see also ML tactic |
|
9606 | 602 |
\texttt{cut_inst_tac} in \cite[\S3]{isabelle-ref}. |
13041 | 603 |
|
9606 | 604 |
\item [$thin_tac~\phi$] deletes the specified assumption from a subgoal; note |
605 |
that $\phi$ may contain schematic variables. See also \texttt{thin_tac} in |
|
606 |
\cite[\S3]{isabelle-ref}. |
|
13041 | 607 |
|
9606 | 608 |
\item [$subgoal_tac~\phi$] adds $\phi$ as an assumption to a subgoal. See |
609 |
also \texttt{subgoal_tac} and \texttt{subgoals_tac} in |
|
610 |
\cite[\S3]{isabelle-ref}. |
|
13041 | 611 |
|
9614 | 612 |
\item [$rename_tac~\vec x$] renames parameters of a goal according to the list |
613 |
$\vec x$, which refers to the \emph{suffix} of variables. |
|
13041 | 614 |
|
9614 | 615 |
\item [$rotate_tac~n$] rotates the assumptions of a goal by $n$ positions: |
616 |
from right to left if $n$ is positive, and from left to right if $n$ is |
|
617 |
negative; the default value is $1$. See also \texttt{rotate_tac} in |
|
618 |
\cite[\S3]{isabelle-ref}. |
|
13041 | 619 |
|
9606 | 620 |
\item [$tactic~text$] produces a proof method from any ML text of type |
621 |
\texttt{tactic}. Apart from the usual ML environment and the current |
|
622 |
implicit theory context, the ML code may refer to the following locally |
|
623 |
bound values: |
|
624 |
||
625 |
{\footnotesize\begin{verbatim} |
|
626 |
val ctxt : Proof.context |
|
627 |
val facts : thm list |
|
628 |
val thm : string -> thm |
|
629 |
val thms : string -> thm list |
|
630 |
\end{verbatim}} |
|
631 |
Here \texttt{ctxt} refers to the current proof context, \texttt{facts} |
|
632 |
indicates any current facts for forward-chaining, and |
|
633 |
\texttt{thm}~/~\texttt{thms} retrieve named facts (including global |
|
634 |
theorems) from the context. |
|
635 |
\end{descr} |
|
636 |
||
637 |
||
12621 | 638 |
\subsection{The Simplifier}\label{sec:simplifier} |
639 |
||
13048 | 640 |
\subsubsection{Simplification methods} |
12618 | 641 |
|
8483 | 642 |
\indexisarmeth{simp}\indexisarmeth{simp-all} |
7315 | 643 |
\begin{matharray}{rcl} |
644 |
simp & : & \isarmeth \\ |
|
8483 | 645 |
simp_all & : & \isarmeth \\ |
7315 | 646 |
\end{matharray} |
647 |
||
8483 | 648 |
\railalias{simpall}{simp\_all} |
649 |
\railterm{simpall} |
|
650 |
||
8704 | 651 |
\railalias{noasm}{no\_asm} |
652 |
\railterm{noasm} |
|
653 |
||
654 |
\railalias{noasmsimp}{no\_asm\_simp} |
|
655 |
\railterm{noasmsimp} |
|
656 |
||
657 |
\railalias{noasmuse}{no\_asm\_use} |
|
658 |
\railterm{noasmuse} |
|
659 |
||
13617 | 660 |
\railalias{asmlr}{asm\_lr} |
661 |
\railterm{asmlr} |
|
662 |
||
11128 | 663 |
\indexouternonterm{simpmod} |
7315 | 664 |
\begin{rail} |
13027 | 665 |
('simp' | simpall) ('!' ?) opt? (simpmod *) |
7315 | 666 |
; |
667 |
||
13617 | 668 |
opt: '(' (noasm | noasmsimp | noasmuse | asmlr) ')' |
8704 | 669 |
; |
9711 | 670 |
simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') | |
9847 | 671 |
'split' (() | 'add' | 'del')) ':' thmrefs |
7315 | 672 |
; |
673 |
\end{rail} |
|
674 |
||
7321 | 675 |
\begin{descr} |
13015 | 676 |
|
8547 | 677 |
\item [$simp$] invokes Isabelle's simplifier, after declaring additional rules |
8594 | 678 |
according to the arguments given. Note that the \railtterm{only} modifier |
8547 | 679 |
first removes all other rewrite rules, congruences, and looper tactics |
8594 | 680 |
(including splits), and then behaves like \railtterm{add}. |
13041 | 681 |
|
9711 | 682 |
\medskip The \railtterm{cong} modifiers add or delete Simplifier congruence |
683 |
rules (see also \cite{isabelle-ref}), the default is to add. |
|
13041 | 684 |
|
9711 | 685 |
\medskip The \railtterm{split} modifiers add or delete rules for the |
686 |
Splitter (see also \cite{isabelle-ref}), the default is to add. This works |
|
687 |
only if the Simplifier method has been properly setup to include the |
|
688 |
Splitter (all major object logics such HOL, HOLCF, FOL, ZF do this already). |
|
13041 | 689 |
|
13015 | 690 |
\item [$simp_all$] is similar to $simp$, but acts on all goals (backwards from |
691 |
the last to the first one). |
|
692 |
||
7321 | 693 |
\end{descr} |
694 |
||
13015 | 695 |
By default the Simplifier methods take local assumptions fully into account, |
696 |
using equational assumptions in the subsequent normalization process, or |
|
13024 | 697 |
simplifying assumptions themselves (cf.\ \texttt{asm_full_simp_tac} in |
13015 | 698 |
\cite[\S10]{isabelle-ref}). In structured proofs this is usually quite well |
699 |
behaved in practice: just the local premises of the actual goal are involved, |
|
13041 | 700 |
additional facts may be inserted via explicit forward-chaining (using $\THEN$, |
13015 | 701 |
$\FROMNAME$ etc.). The full context of assumptions is only included if the |
702 |
``$!$'' (bang) argument is given, which should be used with some care, though. |
|
7321 | 703 |
|
13015 | 704 |
Additional Simplifier options may be specified to tune the behavior further |
13041 | 705 |
(mostly for unstructured scripts with many accidental local facts): |
706 |
``$(no_asm)$'' means assumptions are ignored completely (cf.\ |
|
707 |
\texttt{simp_tac}), ``$(no_asm_simp)$'' means assumptions are used in the |
|
708 |
simplification of the conclusion but are not themselves simplified (cf.\ |
|
709 |
\texttt{asm_simp_tac}), and ``$(no_asm_use)$'' means assumptions are |
|
710 |
simplified but are not used in the simplification of each other or the |
|
711 |
conclusion (cf.\ \texttt{full_simp_tac}). |
|
13617 | 712 |
For compatibility reasons, there is also an option ``$(asm_lr)$'', |
713 |
which means that an assumption is only used for simplifying assumptions |
|
714 |
which are to the right of it (cf.\ \texttt{asm_lr_simp_tac}). |
|
8704 | 715 |
|
716 |
\medskip |
|
717 |
||
718 |
The Splitter package is usually configured to work as part of the Simplifier. |
|
9711 | 719 |
The effect of repeatedly applying \texttt{split_tac} can be simulated by |
13041 | 720 |
``$(simp~only\colon~split\colon~\vec a)$''. There is also a separate $split$ |
721 |
method available for single-step case splitting. |
|
8483 | 722 |
|
723 |
||
12621 | 724 |
\subsubsection{Declaring rules} |
8483 | 725 |
|
8667 | 726 |
\indexisarcmd{print-simpset} |
8638 | 727 |
\indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong} |
7321 | 728 |
\begin{matharray}{rcl} |
13024 | 729 |
\isarcmd{print_simpset}^* & : & \isarkeep{theory~|~proof} \\ |
7321 | 730 |
simp & : & \isaratt \\ |
9711 | 731 |
cong & : & \isaratt \\ |
8483 | 732 |
split & : & \isaratt \\ |
7321 | 733 |
\end{matharray} |
734 |
||
735 |
\begin{rail} |
|
9711 | 736 |
('simp' | 'cong' | 'split') (() | 'add' | 'del') |
7321 | 737 |
; |
738 |
\end{rail} |
|
739 |
||
740 |
\begin{descr} |
|
13024 | 741 |
|
742 |
\item [$\isarcmd{print_simpset}$] prints the collection of rules declared to |
|
743 |
the Simplifier, which is also known as ``simpset'' internally |
|
8667 | 744 |
\cite{isabelle-ref}. This is a diagnostic command; $undo$ does not apply. |
13024 | 745 |
|
8547 | 746 |
\item [$simp$] declares simplification rules. |
13024 | 747 |
|
8638 | 748 |
\item [$cong$] declares congruence rules. |
13024 | 749 |
|
9711 | 750 |
\item [$split$] declares case split rules. |
13024 | 751 |
|
7321 | 752 |
\end{descr} |
7319 | 753 |
|
7315 | 754 |
|
12621 | 755 |
\subsubsection{Forward simplification} |
756 |
||
9905 | 757 |
\indexisaratt{simplified} |
7315 | 758 |
\begin{matharray}{rcl} |
9905 | 759 |
simplified & : & \isaratt \\ |
7315 | 760 |
\end{matharray} |
761 |
||
9905 | 762 |
\begin{rail} |
13015 | 763 |
'simplified' opt? thmrefs? |
9905 | 764 |
; |
765 |
||
766 |
opt: '(' (noasm | noasmsimp | noasmuse) ')' |
|
767 |
; |
|
768 |
\end{rail} |
|
7905 | 769 |
|
9905 | 770 |
\begin{descr} |
13048 | 771 |
|
13015 | 772 |
\item [$simplified~\vec a$] causes a theorem to be simplified, either by |
773 |
exactly the specified rules $\vec a$, or the implicit Simplifier context if |
|
774 |
no arguments are given. The result is fully simplified by default, |
|
775 |
including assumptions and conclusion; the options $no_asm$ etc.\ tune the |
|
13048 | 776 |
Simplifier in the same way as the for the $simp$ method. |
13041 | 777 |
|
13015 | 778 |
Note that forward simplification restricts the simplifier to its most basic |
779 |
operation of term rewriting; solver and looper tactics \cite{isabelle-ref} |
|
780 |
are \emph{not} involved here. The $simplified$ attribute should be only |
|
781 |
rarely required under normal circumstances. |
|
782 |
||
9905 | 783 |
\end{descr} |
7315 | 784 |
|
785 |
||
13048 | 786 |
\subsubsection{Low-level equational reasoning} |
9614 | 787 |
|
12976 | 788 |
\indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisarmeth{split} |
9614 | 789 |
\begin{matharray}{rcl} |
13015 | 790 |
subst^* & : & \isarmeth \\ |
9614 | 791 |
hypsubst^* & : & \isarmeth \\ |
13015 | 792 |
split^* & : & \isarmeth \\ |
9614 | 793 |
\end{matharray} |
794 |
||
795 |
\begin{rail} |
|
796 |
'subst' thmref |
|
797 |
; |
|
9799 | 798 |
'split' ('(' 'asm' ')')? thmrefs |
9703 | 799 |
; |
9614 | 800 |
\end{rail} |
801 |
||
13015 | 802 |
These methods provide low-level facilities for equational reasoning that are |
803 |
intended for specialized applications only. Normally, single step |
|
804 |
calculations would be performed in a structured text (see also |
|
805 |
\S\ref{sec:calculation}), while the Simplifier methods provide the canonical |
|
806 |
way for automated normalization (see \S\ref{sec:simplifier}). |
|
9614 | 807 |
|
808 |
\begin{descr} |
|
13041 | 809 |
|
810 |
\item [$subst~a$] performs a single substitution step using rule $a$, which |
|
811 |
may be either a meta or object equality. |
|
812 |
||
813 |
\item [$hypsubst$] performs substitution using some assumption; this only |
|
814 |
works for equations of the form $x = t$ where $x$ is a free or bound |
|
815 |
variable. |
|
816 |
||
817 |
\item [$split~\vec a$] performs single-step case splitting using rules $thms$. |
|
9799 | 818 |
By default, splitting is performed in the conclusion of a goal; the $asm$ |
819 |
option indicates to operate on assumptions instead. |
|
13048 | 820 |
|
9703 | 821 |
Note that the $simp$ method already involves repeated application of split |
13048 | 822 |
rules as declared in the current context. |
9614 | 823 |
\end{descr} |
824 |
||
825 |
||
12621 | 826 |
\subsection{The Classical Reasoner}\label{sec:classical} |
7135 | 827 |
|
13048 | 828 |
\subsubsection{Basic methods} |
7321 | 829 |
|
13024 | 830 |
\indexisarmeth{rule}\indexisarmeth{default}\indexisarmeth{contradiction} |
831 |
\indexisarmeth{intro}\indexisarmeth{elim} |
|
7321 | 832 |
\begin{matharray}{rcl} |
833 |
rule & : & \isarmeth \\ |
|
13024 | 834 |
contradiction & : & \isarmeth \\ |
7321 | 835 |
intro & : & \isarmeth \\ |
836 |
elim & : & \isarmeth \\ |
|
837 |
\end{matharray} |
|
838 |
||
839 |
\begin{rail} |
|
8547 | 840 |
('rule' | 'intro' | 'elim') thmrefs? |
7321 | 841 |
; |
842 |
\end{rail} |
|
843 |
||
844 |
\begin{descr} |
|
13041 | 845 |
|
7466 | 846 |
\item [$rule$] as offered by the classical reasoner is a refinement over the |
13024 | 847 |
primitive one (see \S\ref{sec:pure-meth-att}). Both versions essentially |
848 |
work the same, but the classical version observes the classical rule context |
|
13041 | 849 |
in addition to that of Isabelle/Pure. |
850 |
||
851 |
Common object logics (HOL, ZF, etc.) declare a rich collection of classical |
|
852 |
rules (even if these would qualify as intuitionistic ones), but only few |
|
853 |
declarations to the rule context of Isabelle/Pure |
|
854 |
(\S\ref{sec:pure-meth-att}). |
|
855 |
||
13024 | 856 |
\item [$contradiction$] solves some goal by contradiction, deriving any result |
13041 | 857 |
from both $\neg A$ and $A$. Chained facts, which are guaranteed to |
858 |
participate, may appear in either order. |
|
9614 | 859 |
|
7466 | 860 |
\item [$intro$ and $elim$] repeatedly refine some goal by intro- or |
13041 | 861 |
elim-resolution, after having inserted any chained facts. Exactly the rules |
862 |
given as arguments are taken into account; this allows fine-tuned |
|
863 |
decomposition of a proof problem, in contrast to common automated tools. |
|
864 |
||
7321 | 865 |
\end{descr} |
866 |
||
867 |
||
13048 | 868 |
\subsubsection{Automated methods} |
7315 | 869 |
|
9799 | 870 |
\indexisarmeth{blast}\indexisarmeth{fast}\indexisarmeth{slow} |
871 |
\indexisarmeth{best}\indexisarmeth{safe}\indexisarmeth{clarify} |
|
7321 | 872 |
\begin{matharray}{rcl} |
9780 | 873 |
blast & : & \isarmeth \\ |
874 |
fast & : & \isarmeth \\ |
|
9799 | 875 |
slow & : & \isarmeth \\ |
9780 | 876 |
best & : & \isarmeth \\ |
877 |
safe & : & \isarmeth \\ |
|
878 |
clarify & : & \isarmeth \\ |
|
7321 | 879 |
\end{matharray} |
880 |
||
11128 | 881 |
\indexouternonterm{clamod} |
7321 | 882 |
\begin{rail} |
13027 | 883 |
'blast' ('!' ?) nat? (clamod *) |
7321 | 884 |
; |
13027 | 885 |
('fast' | 'slow' | 'best' | 'safe' | 'clarify') ('!' ?) (clamod *) |
7321 | 886 |
; |
887 |
||
9408 | 888 |
clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs |
7321 | 889 |
; |
890 |
\end{rail} |
|
891 |
||
892 |
\begin{descr} |
|
893 |
\item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac} |
|
7335 | 894 |
in \cite[\S11]{isabelle-ref}). The optional argument specifies a |
10858 | 895 |
user-supplied search bound (default 20). |
9799 | 896 |
\item [$fast$, $slow$, $best$, $safe$, and $clarify$] refer to the generic |
897 |
classical reasoner. See \texttt{fast_tac}, \texttt{slow_tac}, |
|
898 |
\texttt{best_tac}, \texttt{safe_tac}, and \texttt{clarify_tac} in |
|
899 |
\cite[\S11]{isabelle-ref} for more information. |
|
7321 | 900 |
\end{descr} |
901 |
||
13041 | 902 |
Any of the above methods support additional modifiers of the context of |
903 |
classical rules. Their semantics is analogous to the attributes given before. |
|
904 |
Facts provided by forward chaining are inserted into the goal before |
|
905 |
commencing proof search. The ``!''~argument causes the full context of |
|
906 |
assumptions to be included as well. |
|
7321 | 907 |
|
7315 | 908 |
|
12621 | 909 |
\subsubsection{Combined automated methods}\label{sec:clasimp} |
7315 | 910 |
|
9799 | 911 |
\indexisarmeth{auto}\indexisarmeth{force}\indexisarmeth{clarsimp} |
912 |
\indexisarmeth{fastsimp}\indexisarmeth{slowsimp}\indexisarmeth{bestsimp} |
|
7321 | 913 |
\begin{matharray}{rcl} |
9606 | 914 |
auto & : & \isarmeth \\ |
7321 | 915 |
force & : & \isarmeth \\ |
9438 | 916 |
clarsimp & : & \isarmeth \\ |
9606 | 917 |
fastsimp & : & \isarmeth \\ |
9799 | 918 |
slowsimp & : & \isarmeth \\ |
919 |
bestsimp & : & \isarmeth \\ |
|
7321 | 920 |
\end{matharray} |
921 |
||
11128 | 922 |
\indexouternonterm{clasimpmod} |
7321 | 923 |
\begin{rail} |
13027 | 924 |
'auto' '!'? (nat nat)? (clasimpmod *) |
9780 | 925 |
; |
13027 | 926 |
('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') '!'? (clasimpmod *) |
7321 | 927 |
; |
7315 | 928 |
|
9711 | 929 |
clasimpmod: ('simp' (() | 'add' | 'del' | 'only') | |
10031 | 930 |
('cong' | 'split') (() | 'add' | 'del') | |
931 |
'iff' (((() | 'add') '?'?) | 'del') | |
|
9408 | 932 |
(('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' thmrefs |
7321 | 933 |
\end{rail} |
7315 | 934 |
|
7321 | 935 |
\begin{descr} |
9799 | 936 |
\item [$auto$, $force$, $clarsimp$, $fastsimp$, $slowsimp$, and $bestsimp$] |
937 |
provide access to Isabelle's combined simplification and classical reasoning |
|
938 |
tactics. These correspond to \texttt{auto_tac}, \texttt{force_tac}, |
|
939 |
\texttt{clarsimp_tac}, and Classical Reasoner tactics with the Simplifier |
|
940 |
added as wrapper, see \cite[\S11]{isabelle-ref} for more information. The |
|
13048 | 941 |
modifier arguments correspond to those given in \S\ref{sec:simplifier} and |
942 |
\S\ref{sec:classical}. Just note that the ones related to the Simplifier |
|
943 |
are prefixed by \railtterm{simp} here. |
|
9614 | 944 |
|
7987 | 945 |
Facts provided by forward chaining are inserted into the goal before doing |
946 |
the search. The ``!''~argument causes the full context of assumptions to be |
|
947 |
included as well. |
|
7321 | 948 |
\end{descr} |
949 |
||
7987 | 950 |
|
13048 | 951 |
\subsubsection{Declaring rules} |
7135 | 952 |
|
8667 | 953 |
\indexisarcmd{print-claset} |
7391 | 954 |
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest} |
9936 | 955 |
\indexisaratt{iff}\indexisaratt{rule} |
7321 | 956 |
\begin{matharray}{rcl} |
13024 | 957 |
\isarcmd{print_claset}^* & : & \isarkeep{theory~|~proof} \\ |
7321 | 958 |
intro & : & \isaratt \\ |
959 |
elim & : & \isaratt \\ |
|
960 |
dest & : & \isaratt \\ |
|
9936 | 961 |
rule & : & \isaratt \\ |
7391 | 962 |
iff & : & \isaratt \\ |
7321 | 963 |
\end{matharray} |
7135 | 964 |
|
7321 | 965 |
\begin{rail} |
9408 | 966 |
('intro' | 'elim' | 'dest') ('!' | () | '?') |
7321 | 967 |
; |
9936 | 968 |
'rule' 'del' |
969 |
; |
|
10031 | 970 |
'iff' (((() | 'add') '?'?) | 'del') |
9936 | 971 |
; |
7321 | 972 |
\end{rail} |
7135 | 973 |
|
7321 | 974 |
\begin{descr} |
13024 | 975 |
|
976 |
\item [$\isarcmd{print_claset}$] prints the collection of rules declared to |
|
977 |
the Classical Reasoner, which is also known as ``simpset'' internally |
|
8667 | 978 |
\cite{isabelle-ref}. This is a diagnostic command; $undo$ does not apply. |
13024 | 979 |
|
8517 | 980 |
\item [$intro$, $elim$, and $dest$] declare introduction, elimination, and |
11332 | 981 |
destruction rules, respectively. By default, rules are considered as |
9408 | 982 |
\emph{unsafe} (i.e.\ not applied blindly without backtracking), while a |
13041 | 983 |
single ``!'' classifies as \emph{safe}. Rule declarations marked by ``?'' |
984 |
coincide with those of Isabelle/Pure, cf.\ \S\ref{sec:pure-meth-att} (i.e.\ |
|
985 |
are only applied in single steps of the $rule$ method). |
|
13024 | 986 |
|
11332 | 987 |
\item [$rule~del$] deletes introduction, elimination, or destruction rules from |
9936 | 988 |
the context. |
13041 | 989 |
|
990 |
\item [$iff$] declares logical equivalences to the Simplifier and the |
|
13024 | 991 |
Classical reasoner at the same time. Non-conditional rules result in a |
992 |
``safe'' introduction and elimination pair; conditional ones are considered |
|
993 |
``unsafe''. Rules with negative conclusion are automatically inverted |
|
13041 | 994 |
(using $\neg$ elimination internally). |
995 |
||
996 |
The ``?'' version of $iff$ declares rules to the Isabelle/Pure context only, |
|
997 |
and omits the Simplifier declaration. |
|
998 |
||
7321 | 999 |
\end{descr} |
7135 | 1000 |
|
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8195
diff
changeset
|
1001 |
|
13048 | 1002 |
\subsubsection{Classical operations} |
13027 | 1003 |
|
1004 |
\indexisaratt{elim-format}\indexisaratt{swapped} |
|
1005 |
||
1006 |
\begin{matharray}{rcl} |
|
1007 |
elim_format & : & \isaratt \\ |
|
1008 |
swapped & : & \isaratt \\ |
|
1009 |
\end{matharray} |
|
1010 |
||
1011 |
\begin{descr} |
|
13041 | 1012 |
|
13027 | 1013 |
\item [$elim_format$] turns a destruction rule into elimination rule format; |
1014 |
this operation is similar to the the intuitionistic version |
|
1015 |
(\S\ref{sec:misc-meth-att}), but each premise of the resulting rule acquires |
|
13041 | 1016 |
an additional local fact of the negated main thesis; according to the |
13027 | 1017 |
classical principle $(\neg A \Imp A) \Imp A$. |
13041 | 1018 |
|
13027 | 1019 |
\item [$swapped$] turns an introduction rule into an elimination, by resolving |
1020 |
with the classical swap principle $(\neg B \Imp A) \Imp (\neg A \Imp B)$. |
|
1021 |
||
1022 |
\end{descr} |
|
1023 |
||
1024 |
||
12621 | 1025 |
\subsection{Proof by cases and induction}\label{sec:cases-induct} |
12618 | 1026 |
|
13048 | 1027 |
\subsubsection{Rule contexts} |
12618 | 1028 |
|
1029 |
\indexisarcmd{case}\indexisarcmd{print-cases} |
|
1030 |
\indexisaratt{case-names}\indexisaratt{params}\indexisaratt{consumes} |
|
1031 |
\begin{matharray}{rcl} |
|
1032 |
\isarcmd{case} & : & \isartrans{proof(state)}{proof(state)} \\ |
|
1033 |
\isarcmd{print_cases}^* & : & \isarkeep{proof} \\ |
|
1034 |
case_names & : & \isaratt \\ |
|
1035 |
params & : & \isaratt \\ |
|
1036 |
consumes & : & \isaratt \\ |
|
1037 |
\end{matharray} |
|
1038 |
||
1039 |
Basically, Isar proof contexts are built up explicitly using commands like |
|
1040 |
$\FIXNAME$, $\ASSUMENAME$ etc.\ (see \S\ref{sec:proof-context}). In typical |
|
1041 |
verification tasks this can become hard to manage, though. In particular, a |
|
1042 |
large number of local contexts may emerge from case analysis or induction over |
|
1043 |
inductive sets and types. |
|
1044 |
||
1045 |
\medskip |
|
1046 |
||
1047 |
The $\CASENAME$ command provides a shorthand to refer to certain parts of |
|
1048 |
logical context symbolically. Proof methods may provide an environment of |
|
1049 |
named ``cases'' of the form $c\colon \vec x, \vec \phi$. Then the effect of |
|
13041 | 1050 |
``$\CASE{c}$'' is that of ``$\FIX{\vec x}~\ASSUME{c}{\vec\phi}$''. Term |
1051 |
bindings may be covered as well, such as $\Var{case}$ for the intended |
|
1052 |
conclusion. |
|
12618 | 1053 |
|
13027 | 1054 |
Normally the ``terminology'' of a case value (i.e.\ the parameters $\vec x$) |
13041 | 1055 |
are marked as hidden. Using the explicit form ``$\CASE{(c~\vec x)}$'' enables |
1056 |
proof writers to choose their own names for the subsequent proof text. |
|
12618 | 1057 |
|
1058 |
\medskip |
|
1059 |
||
13027 | 1060 |
It is important to note that $\CASENAME$ does \emph{not} provide direct means |
1061 |
to peek at the current goal state, which is generally considered |
|
1062 |
non-observable in Isar. The text of the cases basically emerge from standard |
|
1063 |
elimination or induction rules, which in turn are derived from previous theory |
|
13041 | 1064 |
specifications in a canonical way (say from $\isarkeyword{inductive}$ |
1065 |
definitions). |
|
13027 | 1066 |
|
12618 | 1067 |
Named cases may be exhibited in the current proof context only if both the |
1068 |
proof method and the rules involved support this. Case names and parameters |
|
1069 |
of basic rules may be declared by hand as well, by using appropriate |
|
1070 |
attributes. Thus variant versions of rules that have been derived manually |
|
1071 |
may be used in advanced case analysis later. |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1072 |
|
12618 | 1073 |
\railalias{casenames}{case\_names} |
1074 |
\railterm{casenames} |
|
1075 |
||
1076 |
\begin{rail} |
|
13041 | 1077 |
'case' (caseref | '(' caseref ((name | underscore) +) ')') |
12618 | 1078 |
; |
13024 | 1079 |
caseref: nameref attributes? |
1080 |
; |
|
1081 |
||
13027 | 1082 |
casenames (name +) |
12618 | 1083 |
; |
13027 | 1084 |
'params' ((name *) + 'and') |
12618 | 1085 |
; |
1086 |
'consumes' nat? |
|
1087 |
; |
|
1088 |
\end{rail} |
|
1089 |
||
1090 |
\begin{descr} |
|
13041 | 1091 |
|
1092 |
\item [$\CASE{(c~\vec x)}$] invokes a named local context $c\colon \vec x, |
|
1093 |
\vec \phi$, as provided by an appropriate proof method (such as $cases$ and |
|
1094 |
$induct$, see \S\ref{sec:cases-induct-meth}). The command ``$\CASE{(c~\vec |
|
1095 |
x)}$'' abbreviates ``$\FIX{\vec x}~\ASSUME{c}{\vec\phi}$''. |
|
1096 |
||
12618 | 1097 |
\item [$\isarkeyword{print_cases}$] prints all local contexts of the current |
1098 |
state, using Isar proof language notation. This is a diagnostic command; |
|
1099 |
$undo$ does not apply. |
|
13041 | 1100 |
|
12618 | 1101 |
\item [$case_names~\vec c$] declares names for the local contexts of premises |
1102 |
of some theorem; $\vec c$ refers to the \emph{suffix} of the list of |
|
1103 |
premises. |
|
13041 | 1104 |
|
12618 | 1105 |
\item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of |
1106 |
premises $1, \dots, n$ of some theorem. An empty list of names may be given |
|
1107 |
to skip positions, leaving the present parameters unchanged. |
|
13041 | 1108 |
|
12618 | 1109 |
Note that the default usage of case rules does \emph{not} directly expose |
1110 |
parameters to the proof context (see also \S\ref{sec:cases-induct-meth}). |
|
13041 | 1111 |
|
12618 | 1112 |
\item [$consumes~n$] declares the number of ``major premises'' of a rule, |
1113 |
i.e.\ the number of facts to be consumed when it is applied by an |
|
1114 |
appropriate proof method (cf.\ \S\ref{sec:cases-induct-meth}). The default |
|
1115 |
value of $consumes$ is $n = 1$, which is appropriate for the usual kind of |
|
13041 | 1116 |
cases and induction rules for inductive sets (cf.\ |
12618 | 1117 |
\S\ref{sec:hol-inductive}). Rules without any $consumes$ declaration given |
1118 |
are treated as if $consumes~0$ had been specified. |
|
13041 | 1119 |
|
12618 | 1120 |
Note that explicit $consumes$ declarations are only rarely needed; this is |
1121 |
already taken care of automatically by the higher-level $cases$ and $induct$ |
|
1122 |
declarations, see also \S\ref{sec:cases-induct-att}. |
|
13027 | 1123 |
|
12618 | 1124 |
\end{descr} |
1125 |
||
1126 |
||
12621 | 1127 |
\subsubsection{Proof methods}\label{sec:cases-induct-meth} |
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1128 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1129 |
\indexisarmeth{cases}\indexisarmeth{induct} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1130 |
\begin{matharray}{rcl} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1131 |
cases & : & \isarmeth \\ |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1132 |
induct & : & \isarmeth \\ |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1133 |
\end{matharray} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1134 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1135 |
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
|
1136 |
and induction over datatypes, inductive sets, and recursive functions. The |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1137 |
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
|
1138 |
Furthermore, these methods provide named local contexts that may be invoked |
13048 | 1139 |
via the $\CASENAME$ proof command within the subsequent proof text. This |
1140 |
accommodates compact proof texts even when reasoning about large |
|
1141 |
specifications. |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1142 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1143 |
\begin{rail} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1144 |
'cases' spec |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1145 |
; |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1146 |
'induct' spec |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1147 |
; |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1148 |
|
13041 | 1149 |
spec: open? args rule? |
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1150 |
; |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1151 |
open: '(' 'open' ')' |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1152 |
; |
13041 | 1153 |
args: (insts * 'and') |
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1154 |
; |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1155 |
rule: ('type' | 'set') ':' nameref | 'rule' ':' thmref |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1156 |
; |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1157 |
\end{rail} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1158 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1159 |
\begin{descr} |
13041 | 1160 |
|
1161 |
\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
|
1162 |
distinction theorem, instantiated to the subjects $insts$. Symbolic case |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1163 |
names are bound according to the rule's local contexts. |
13041 | 1164 |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1165 |
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
|
1166 |
passed to the $cases$ method: |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1167 |
\begin{matharray}{llll} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1168 |
\Text{facts} & & \Text{arguments} & \Text{rule} \\\hline |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1169 |
& cases & & \Text{classical case split} \\ |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1170 |
& cases & t & \Text{datatype exhaustion (type of $t$)} \\ |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1171 |
\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
|
1172 |
\dots & cases & \dots ~ R & \Text{explicit rule $R$} \\ |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1173 |
\end{matharray} |
13041 | 1174 |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1175 |
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
|
1176 |
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
|
1177 |
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
|
1178 |
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
|
1179 |
usually the same for all cases). |
13041 | 1180 |
|
1181 |
The ``$(open)$'' option causes the parameters of the new local contexts to |
|
1182 |
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
|
1183 |
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
|
1184 |
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
|
1185 |
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
|
1186 |
less robust proof texts. |
13041 | 1187 |
|
1188 |
\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
|
1189 |
induction rules, which are determined as follows: |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1190 |
\begin{matharray}{llll} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1191 |
\Text{facts} & & \Text{arguments} & \Text{rule} \\\hline |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1192 |
& induct & P ~ x ~ \dots & \Text{datatype induction (type of $x$)} \\ |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1193 |
\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
|
1194 |
\dots & induct & \dots ~ R & \Text{explicit rule $R$} \\ |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1195 |
\end{matharray} |
13041 | 1196 |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1197 |
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
|
1198 |
inductive definition or datatype --- only related partial induction rules |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1199 |
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
|
1200 |
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
|
1201 |
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
|
1202 |
predicates and variables, for example. |
13041 | 1203 |
|
1204 |
The ``$(open)$'' option works the same way as for $cases$. |
|
13027 | 1205 |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1206 |
\end{descr} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1207 |
|
13048 | 1208 |
Above methods produce named local contexts, as determined by the instantiated |
1209 |
rule as specified in the text. Beyond that, the $induct$ method guesses |
|
1210 |
further instantiations from the goal specification itself. Any persisting |
|
1211 |
unresolved schematic variables of the resulting rule will render the the |
|
1212 |
corresponding case invalid. The term binding $\Var{case}$\indexisarvar{case} |
|
1213 |
for the conclusion will be provided with each case, provided that term is |
|
1214 |
fully specified. |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1215 |
|
13048 | 1216 |
The $\isarkeyword{print_cases}$ command prints all named cases present in the |
1217 |
current proof state. |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1218 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1219 |
\medskip |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1220 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1221 |
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
|
1222 |
and $induct$ methods in handling of non-atomic goal statements: $cases$ just |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1223 |
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
|
1224 |
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
|
1225 |
|
13622 | 1226 |
In contrast, $induct$ passes the full goal statement through the |
1227 |
``recursive'' course involved in the induction. Thus the original statement |
|
1228 |
is basically replaced by separate copies, corresponding to the induction |
|
1229 |
hypotheses and conclusion; the original goal context is no longer available. |
|
1230 |
This behavior allows \emph{strengthened induction predicates} to be expressed |
|
1231 |
concisely as meta-level rule statements, i.e.\ $\All{\vec x} \vec\phi \Imp |
|
1232 |
\psi$ to indicate ``variable'' parameters $\vec x$ and ``recursive'' |
|
1233 |
assumptions $\vec\phi$. Note that ``$\isarcmd{case}~c$'' already performs |
|
1234 |
``$\FIX{\vec x}$''. Also note that local definitions may be expressed as |
|
1235 |
$\All{\vec x} n \equiv t[\vec x] \Imp \phi[n]$, with induction over $n$. |
|
1236 |
||
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1237 |
|
13425
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
13411
diff
changeset
|
1238 |
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
|
1239 |
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
|
1240 |
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
|
1241 |
``$\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
|
1242 |
$c\mathord.prems$, as well as fact $c$ to hold the all-inclusive list. |
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
13411
diff
changeset
|
1243 |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1244 |
\medskip |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1245 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1246 |
Facts presented to either method are consumed according to the number of |
12618 | 1247 |
``major premises'' of the rule involved (see also \S\ref{sec:cases-induct}), |
13041 | 1248 |
which is usually $0$ for plain cases and induction rules of datatypes etc.\ |
12618 | 1249 |
and $1$ for rules of inductive sets and the like. The remaining facts are |
1250 |
inserted into the goal verbatim before the actual $cases$ or $induct$ rule is |
|
1251 |
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
|
1252 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1253 |
|
12621 | 1254 |
\subsubsection{Declaring rules}\label{sec:cases-induct-att} |
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1255 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1256 |
\indexisarcmd{print-induct-rules}\indexisaratt{cases}\indexisaratt{induct} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1257 |
\begin{matharray}{rcl} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1258 |
\isarcmd{print_induct_rules}^* & : & \isarkeep{theory~|~proof} \\ |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1259 |
cases & : & \isaratt \\ |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1260 |
induct & : & \isaratt \\ |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1261 |
\end{matharray} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1262 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1263 |
\begin{rail} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1264 |
'cases' spec |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1265 |
; |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1266 |
'induct' spec |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1267 |
; |
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 |
spec: ('type' | 'set') ':' nameref |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1270 |
; |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1271 |
\end{rail} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1272 |
|
13024 | 1273 |
\begin{descr} |
13041 | 1274 |
|
13024 | 1275 |
\item [$\isarkeyword{print_induct_rules}$] prints cases and induct rules for |
1276 |
sets and types of the current context. |
|
13041 | 1277 |
|
13024 | 1278 |
\item [$cases$ and $induct$] (as attributes) augment the corresponding context |
1279 |
of rules for reasoning about inductive sets and types, using the |
|
1280 |
corresponding methods of the same name. Certain definitional packages of |
|
1281 |
object-logics usually declare emerging cases and induction rules as |
|
1282 |
expected, so users rarely need to intervene. |
|
13048 | 1283 |
|
13024 | 1284 |
Manual rule declarations usually include the the $case_names$ and $ps$ |
1285 |
attributes to adjust names of cases and parameters of a rule (see |
|
13048 | 1286 |
\S\ref{sec:cases-induct}); the $consumes$ declaration is taken care of |
13024 | 1287 |
automatically: $consumes~0$ is specified for ``type'' rules and $consumes~1$ |
1288 |
for ``set'' rules. |
|
13041 | 1289 |
|
13024 | 1290 |
\end{descr} |
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1291 |
|
9614 | 1292 |
%%% Local Variables: |
7135 | 1293 |
%%% mode: latex |
1294 |
%%% TeX-master: "isar-ref" |
|
9614 | 1295 |
%%% End: |