author | wenzelm |
Wed, 02 Jan 2002 21:53:50 +0100 | |
changeset 12618 | 43a97a2155d0 |
parent 11691 | fc9bd420162c |
child 12621 | 48cafea0684b |
permissions | -rw-r--r-- |
7135 | 1 |
|
7167 | 2 |
\chapter{Generic Tools and Packages}\label{ch:gen-tools} |
3 |
||
12618 | 4 |
\section{Theory commands} |
5 |
||
6 |
\subsection{Axiomatic type classes}\label{sec:axclass} |
|
7167 | 7 |
|
8904 | 8 |
%FIXME |
9 |
% - qualified names |
|
10 |
% - class intro rules; |
|
11 |
% - class axioms; |
|
12 |
||
8517 | 13 |
\indexisarcmd{axclass}\indexisarcmd{instance}\indexisarmeth{intro-classes} |
7167 | 14 |
\begin{matharray}{rcl} |
8517 | 15 |
\isarcmd{axclass} & : & \isartrans{theory}{theory} \\ |
16 |
\isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\ |
|
17 |
intro_classes & : & \isarmeth \\ |
|
7167 | 18 |
\end{matharray} |
19 |
||
8517 | 20 |
Axiomatic type classes are provided by Isabelle/Pure as a \emph{definitional} |
21 |
interface to type classes (cf.~\S\ref{sec:classes}). Thus any object logic |
|
8547 | 22 |
may make use of this light-weight mechanism of abstract theories |
8901 | 23 |
\cite{Wenzel:1997:TPHOL}. There is also a tutorial on using axiomatic type |
24 |
classes in isabelle \cite{isabelle-axclass} that is part of the standard |
|
25 |
Isabelle documentation. |
|
8517 | 26 |
|
7167 | 27 |
\begin{rail} |
8517 | 28 |
'axclass' classdecl (axmdecl prop comment? +) |
29 |
; |
|
11100
34d58b1818f4
\<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents:
11095
diff
changeset
|
30 |
'instance' (nameref ('<' | subseteq) nameref | nameref '::' simplearity) comment? |
7167 | 31 |
; |
32 |
\end{rail} |
|
33 |
||
34 |
\begin{descr} |
|
11100
34d58b1818f4
\<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents:
11095
diff
changeset
|
35 |
\item [$\AXCLASS~c \subseteq \vec c~axms$] defines an axiomatic type class as |
34d58b1818f4
\<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents:
11095
diff
changeset
|
36 |
the intersection of existing classes, with additional axioms holding. Class |
10223 | 37 |
axioms may not contain more than one type variable. The class axioms (with |
38 |
implicit sort constraints added) are bound to the given names. Furthermore |
|
39 |
a class introduction rule is generated, which is employed by method |
|
40 |
$intro_classes$ to support instantiation proofs of this class. |
|
41 |
||
11100
34d58b1818f4
\<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents:
11095
diff
changeset
|
42 |
\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
|
43 |
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
|
44 |
proceed by $intro_classes$, and then establish the characteristic theorems |
34d58b1818f4
\<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents:
11095
diff
changeset
|
45 |
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
|
46 |
augmented by a type signature declaration corresponding to the resulting |
34d58b1818f4
\<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents:
11095
diff
changeset
|
47 |
theorem. |
8517 | 48 |
\item [$intro_classes$] repeatedly expands all class introduction rules of |
10858 | 49 |
this theory. Note that this method usually needs not be named explicitly, |
50 |
as it is already included in the default proof step (of $\PROOFNAME$, |
|
51 |
$\BYNAME$, etc.). In particular, instantiation of trivial (syntactic) |
|
52 |
classes may be performed by a single ``$\DDOT$'' proof step. |
|
7167 | 53 |
\end{descr} |
54 |
||
7315 | 55 |
|
12618 | 56 |
\subsection{Locales and local contexts}\label{sec:locale} |
57 |
||
58 |
FIXME |
|
59 |
||
60 |
||
61 |
\section{Proof commands} |
|
62 |
||
63 |
\subsection{Calculational Reasoning}\label{sec:calculation} |
|
7315 | 64 |
|
8619 | 65 |
\indexisarcmd{also}\indexisarcmd{finally} |
66 |
\indexisarcmd{moreover}\indexisarcmd{ultimately} |
|
9606 | 67 |
\indexisarcmd{print-trans-rules}\indexisaratt{trans} |
7315 | 68 |
\begin{matharray}{rcl} |
69 |
\isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\ |
|
70 |
\isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\ |
|
8619 | 71 |
\isarcmd{moreover} & : & \isartrans{proof(state)}{proof(state)} \\ |
72 |
\isarcmd{ultimately} & : & \isartrans{proof(state)}{proof(chain)} \\ |
|
10154 | 73 |
\isarcmd{print_trans_rules}^* & : & \isarkeep{theory~|~proof} \\ |
7315 | 74 |
trans & : & \isaratt \\ |
75 |
\end{matharray} |
|
76 |
||
77 |
Calculational proof is forward reasoning with implicit application of |
|
11332 | 78 |
transitivity rules (such those of $=$, $\leq$, $<$). Isabelle/Isar maintains |
7391 | 79 |
an auxiliary register $calculation$\indexisarthm{calculation} for accumulating |
7897 | 80 |
results obtained by transitivity composed with the current result. Command |
81 |
$\ALSO$ updates $calculation$ involving $this$, while $\FINALLY$ exhibits the |
|
82 |
final $calculation$ by forward chaining towards the next goal statement. Both |
|
83 |
commands require valid current facts, i.e.\ may occur only after commands that |
|
84 |
produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or some finished proof of |
|
8619 | 85 |
$\HAVENAME$, $\SHOWNAME$ etc. The $\MOREOVER$ and $\ULTIMATELY$ commands are |
86 |
similar to $\ALSO$ and $\FINALLY$, but only collect further results in |
|
87 |
$calculation$ without applying any rules yet. |
|
7315 | 88 |
|
89 |
Also note that the automatic term abbreviation ``$\dots$'' has its canonical |
|
8619 | 90 |
application with calculational proofs. It refers to the argument\footnote{The |
91 |
argument of a curried infix expression is its right-hand side.} of the |
|
92 |
preceding statement. |
|
7315 | 93 |
|
94 |
Isabelle/Isar calculations are implicitly subject to block structure in the |
|
95 |
sense that new threads of calculational reasoning are commenced for any new |
|
96 |
block (as opened by a local goal, for example). This means that, apart from |
|
97 |
being able to nest calculations, there is no separate \emph{begin-calculation} |
|
98 |
command required. |
|
99 |
||
8619 | 100 |
\medskip |
101 |
||
102 |
The Isar calculation proof commands may be defined as |
|
103 |
follows:\footnote{Internal bookkeeping such as proper handling of |
|
104 |
block-structure has been suppressed.} |
|
105 |
\begin{matharray}{rcl} |
|
106 |
\ALSO@0 & \equiv & \NOTE{calculation}{this} \\ |
|
9606 | 107 |
\ALSO@{n+1} & \equiv & \NOTE{calculation}{trans~[OF~calculation~this]} \\[0.5ex] |
8619 | 108 |
\FINALLY & \equiv & \ALSO~\FROM{calculation} \\ |
109 |
\MOREOVER & \equiv & \NOTE{calculation}{calculation~this} \\ |
|
110 |
\ULTIMATELY & \equiv & \MOREOVER~\FROM{calculation} \\ |
|
111 |
\end{matharray} |
|
112 |
||
7315 | 113 |
\begin{rail} |
114 |
('also' | 'finally') transrules? comment? |
|
115 |
; |
|
8619 | 116 |
('moreover' | 'ultimately') comment? |
117 |
; |
|
8507 | 118 |
'trans' (() | 'add' | 'del') |
7315 | 119 |
; |
120 |
||
121 |
transrules: '(' thmrefs ')' interest? |
|
122 |
; |
|
123 |
\end{rail} |
|
124 |
||
125 |
\begin{descr} |
|
8547 | 126 |
\item [$\ALSO~(\vec a)$] maintains the auxiliary $calculation$ register as |
7315 | 127 |
follows. The first occurrence of $\ALSO$ in some calculational thread |
7905 | 128 |
initializes $calculation$ by $this$. Any subsequent $\ALSO$ on the same |
7335 | 129 |
level of block-structure updates $calculation$ by some transitivity rule |
7458 | 130 |
applied to $calculation$ and $this$ (in that order). Transitivity rules are |
11095 | 131 |
picked from the current context, unless alternative rules are given as |
132 |
explicit arguments. |
|
9614 | 133 |
|
8547 | 134 |
\item [$\FINALLY~(\vec a)$] maintaining $calculation$ in the same way as |
7315 | 135 |
$\ALSO$, and concludes the current calculational thread. The final result |
136 |
is exhibited as fact for forward chaining towards the next goal. Basically, |
|
7987 | 137 |
$\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$. Note that |
138 |
``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and |
|
139 |
``$\FINALLY~\HAVE{}{\phi}~\DOT$'' are typical idioms for concluding |
|
140 |
calculational proofs. |
|
9614 | 141 |
|
8619 | 142 |
\item [$\MOREOVER$ and $\ULTIMATELY$] are analogous to $\ALSO$ and $\FINALLY$, |
143 |
but collect results only, without applying rules. |
|
9614 | 144 |
|
9606 | 145 |
\item [$\isarkeyword{print_trans_rules}$] prints the list of transitivity |
146 |
rules declared in the current context. |
|
9614 | 147 |
|
8547 | 148 |
\item [$trans$] declares theorems as transitivity rules. |
9614 | 149 |
|
7315 | 150 |
\end{descr} |
151 |
||
152 |
||
12618 | 153 |
\subsection{Generalized elimination}\label{sec:obtain} |
7135 | 154 |
|
8517 | 155 |
\indexisarcmd{obtain} |
7135 | 156 |
\begin{matharray}{rcl} |
9480 | 157 |
\isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\ |
8517 | 158 |
\end{matharray} |
159 |
||
12618 | 160 |
Generalized elimination means that additional elements with certain properties |
161 |
may introduced in the current context, by virtue of a locally proven |
|
162 |
``soundness statement''. Technically speaking, the $\OBTAINNAME$ language |
|
163 |
element is like a declaration of $\FIXNAME$ and $\ASSUMENAME$ (see also see |
|
164 |
\S\ref{sec:proof-context}), together with a soundness proof of its additional |
|
165 |
claim. According to the nature of existential reasoning, assumptions get |
|
166 |
eliminated from any result exported from the context later, provided that the |
|
167 |
corresponding parameters do \emph{not} occur in the conclusion. |
|
8517 | 168 |
|
169 |
\begin{rail} |
|
12618 | 170 |
'obtain' (vars + 'and') comment? \\ 'where' (props comment? + 'and') |
8517 | 171 |
; |
172 |
\end{rail} |
|
173 |
||
9480 | 174 |
$\OBTAINNAME$ is defined as a derived Isar command as follows, where $\vec b$ |
175 |
shall refer to (optional) facts indicated for forward chaining. |
|
8517 | 176 |
\begin{matharray}{l} |
9480 | 177 |
\langle facts~\vec b\rangle \\ |
178 |
\OBTAIN{\vec x}{a}{\vec \phi}~~\langle proof\rangle \equiv {} \\[1ex] |
|
179 |
\quad \BG \\ |
|
180 |
\qquad \FIX{thesis} \\ |
|
10160 | 181 |
\qquad \ASSUME{that~[simp, intro]}{\All{\vec x} \vec\phi \Imp thesis} \\ |
9480 | 182 |
\qquad \FROM{\vec b}~\HAVE{}{thesis}~~\langle proof\rangle \\ |
183 |
\quad \EN \\ |
|
10154 | 184 |
\quad \FIX{\vec x}~\ASSUMENAME^\ast~a\colon~\vec\phi \\ |
7135 | 185 |
\end{matharray} |
186 |
||
8517 | 187 |
Typically, the soundness proof is relatively straight-forward, often just by |
188 |
canonical automated tools such as $\BY{simp}$ (see \S\ref{sec:simp}) or |
|
9480 | 189 |
$\BY{blast}$ (see \S\ref{sec:classical-auto}). Accordingly, the ``$that$'' |
190 |
reduction above is declared as simplification and introduction rule. |
|
8517 | 191 |
|
192 |
\medskip |
|
193 |
||
194 |
In a sense, $\OBTAINNAME$ represents at the level of Isar proofs what would be |
|
195 |
meta-logical existential quantifiers and conjunctions. This concept has a |
|
196 |
broad range of useful applications, ranging from plain elimination (or even |
|
197 |
introduction) of object-level existentials and conjunctions, to elimination |
|
198 |
over results of symbolic evaluation of recursive definitions, for example. |
|
9480 | 199 |
Also note that $\OBTAINNAME$ without parameters acts much like $\HAVENAME$, |
200 |
where the result is treated as an assumption. |
|
8517 | 201 |
|
202 |
||
12618 | 203 |
\subsection{Miscellaneous methods and attributes}\label{sec:misc-meth-att} |
8517 | 204 |
|
9606 | 205 |
\indexisarmeth{unfold}\indexisarmeth{fold}\indexisarmeth{insert} |
8517 | 206 |
\indexisarmeth{erule}\indexisarmeth{drule}\indexisarmeth{frule} |
207 |
\indexisarmeth{fail}\indexisarmeth{succeed} |
|
208 |
\begin{matharray}{rcl} |
|
209 |
unfold & : & \isarmeth \\ |
|
10741 | 210 |
fold & : & \isarmeth \\ |
211 |
insert & : & \isarmeth \\[0.5ex] |
|
8517 | 212 |
erule^* & : & \isarmeth \\ |
213 |
drule^* & : & \isarmeth \\ |
|
214 |
frule^* & : & \isarmeth \\[0.5ex] |
|
215 |
succeed & : & \isarmeth \\ |
|
216 |
fail & : & \isarmeth \\ |
|
217 |
\end{matharray} |
|
7135 | 218 |
|
219 |
\begin{rail} |
|
10741 | 220 |
('fold' | 'unfold' | 'insert') thmrefs |
221 |
; |
|
222 |
('erule' | 'drule' | 'frule') ('('nat')')? thmrefs |
|
7135 | 223 |
; |
224 |
\end{rail} |
|
225 |
||
7167 | 226 |
\begin{descr} |
8547 | 227 |
\item [$unfold~\vec a$ and $fold~\vec a$] expand and fold back again the given |
8517 | 228 |
meta-level definitions throughout all goals; any facts provided are inserted |
229 |
into the goal and subject to rewriting as well. |
|
10741 | 230 |
\item [$insert~\vec a$] inserts theorems as facts into all goals of the proof |
231 |
state. Note that current facts indicated for forward chaining are ignored. |
|
8547 | 232 |
\item [$erule~\vec a$, $drule~\vec a$, and $frule~\vec a$] are similar to the |
233 |
basic $rule$ method (see \S\ref{sec:pure-meth-att}), but apply rules by |
|
8517 | 234 |
elim-resolution, destruct-resolution, and forward-resolution, respectively |
10741 | 235 |
\cite{isabelle-ref}. The optional natural number argument (default $0$) |
236 |
specifies additional assumption steps to be performed. |
|
237 |
||
238 |
Note that these methods are improper ones, mainly serving for |
|
239 |
experimentation and tactic script emulation. Different modes of basic rule |
|
240 |
application are usually expressed in Isar at the proof language level, |
|
241 |
rather than via implicit proof state manipulations. For example, a proper |
|
242 |
single-step elimination would be done using the basic $rule$ method, with |
|
243 |
forward chaining of current facts. |
|
8517 | 244 |
\item [$succeed$] yields a single (unchanged) result; it is the identity of |
245 |
the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}). |
|
246 |
\item [$fail$] yields an empty result sequence; it is the identity of the |
|
247 |
``\texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}). |
|
7167 | 248 |
\end{descr} |
7135 | 249 |
|
10318 | 250 |
\indexisaratt{tagged}\indexisaratt{untagged} |
9614 | 251 |
\indexisaratt{THEN}\indexisaratt{COMP} |
10318 | 252 |
\indexisaratt{where}\indexisaratt{unfolded}\indexisaratt{folded} |
253 |
\indexisaratt{standard}\indexisaratt{elim-format} |
|
254 |
\indexisaratt{no-vars}\indexisaratt{exported} |
|
8517 | 255 |
\begin{matharray}{rcl} |
9905 | 256 |
tagged & : & \isaratt \\ |
257 |
untagged & : & \isaratt \\[0.5ex] |
|
9614 | 258 |
THEN & : & \isaratt \\ |
8517 | 259 |
COMP & : & \isaratt \\[0.5ex] |
260 |
where & : & \isaratt \\[0.5ex] |
|
9905 | 261 |
unfolded & : & \isaratt \\ |
262 |
folded & : & \isaratt \\[0.5ex] |
|
8517 | 263 |
standard & : & \isaratt \\ |
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9936
diff
changeset
|
264 |
elim_format & : & \isaratt \\ |
9936 | 265 |
no_vars^* & : & \isaratt \\ |
9905 | 266 |
exported^* & : & \isaratt \\ |
8517 | 267 |
\end{matharray} |
268 |
||
269 |
\begin{rail} |
|
9905 | 270 |
'tagged' (nameref+) |
8517 | 271 |
; |
9905 | 272 |
'untagged' name |
8517 | 273 |
; |
10154 | 274 |
('THEN' | 'COMP') ('[' nat ']')? thmref |
8517 | 275 |
; |
276 |
'where' (name '=' term * 'and') |
|
277 |
; |
|
9905 | 278 |
('unfolded' | 'folded') thmrefs |
8517 | 279 |
; |
280 |
\end{rail} |
|
281 |
||
282 |
\begin{descr} |
|
9905 | 283 |
\item [$tagged~name~args$ and $untagged~name$] add and remove $tags$ of some |
8517 | 284 |
theorem. Tags may be any list of strings that serve as comment for some |
285 |
tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the |
|
286 |
result). The first string is considered the tag name, the rest its |
|
287 |
arguments. Note that untag removes any tags of the same name. |
|
9614 | 288 |
\item [$THEN~n~a$ and $COMP~n~a$] compose rules. $THEN$ resolves with the |
289 |
$n$-th premise of $a$; the $COMP$ version skips the automatic lifting |
|
8547 | 290 |
process that is normally intended (cf.\ \texttt{RS} and \texttt{COMP} in |
291 |
\cite[\S5]{isabelle-ref}). |
|
8517 | 292 |
\item [$where~\vec x = \vec t$] perform named instantiation of schematic |
9606 | 293 |
variables occurring in a theorem. Unlike instantiation tactics such as |
294 |
$rule_tac$ (see \S\ref{sec:tactic-commands}), actual schematic variables |
|
8517 | 295 |
have to be specified (e.g.\ $\Var{x@3}$). |
9905 | 296 |
\item [$unfolded~\vec a$ and $folded~\vec a$] expand and fold back again the |
297 |
given meta-level definitions throughout a rule. |
|
8517 | 298 |
\item [$standard$] puts a theorem into the standard form of object-rules, just |
299 |
as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}). |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9936
diff
changeset
|
300 |
\item [$elim_format$] turns a destruction rule into elimination rule format; |
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9936
diff
changeset
|
301 |
see also the ML function \texttt{make\_elim} (see \cite{isabelle-ref}). |
9232 | 302 |
\item [$no_vars$] replaces schematic variables by free ones; this is mainly |
303 |
for tuning output of pretty printed theorems. |
|
9905 | 304 |
\item [$exported$] lifts a local result out of the current proof context, |
8517 | 305 |
generalizing all fixed variables and discharging all assumptions. Note that |
8547 | 306 |
proper incremental export is already done as part of the basic Isar |
307 |
machinery. This attribute is mainly for experimentation. |
|
8517 | 308 |
\end{descr} |
7135 | 309 |
|
310 |
||
12618 | 311 |
\subsection{Tactic emulations}\label{sec:tactics} |
9606 | 312 |
|
313 |
The following improper proof methods emulate traditional tactics. These admit |
|
314 |
direct access to the goal state, which is normally considered harmful! In |
|
315 |
particular, this may involve both numbered goal addressing (default 1), and |
|
316 |
dynamic instantiation within the scope of some subgoal. |
|
317 |
||
318 |
\begin{warn} |
|
319 |
Dynamic instantiations are read and type-checked according to a subgoal of |
|
320 |
the current dynamic goal state, rather than the static proof context! In |
|
321 |
particular, locally fixed variables and term abbreviations may not be |
|
322 |
included in the term specifications. Thus schematic variables are left to |
|
323 |
be solved by unification with certain parts of the subgoal involved. |
|
324 |
\end{warn} |
|
325 |
||
326 |
Note that the tactic emulation proof methods in Isabelle/Isar are consistently |
|
327 |
named $foo_tac$. |
|
328 |
||
329 |
\indexisarmeth{rule-tac}\indexisarmeth{erule-tac} |
|
330 |
\indexisarmeth{drule-tac}\indexisarmeth{frule-tac} |
|
331 |
\indexisarmeth{cut-tac}\indexisarmeth{thin-tac} |
|
9642 | 332 |
\indexisarmeth{subgoal-tac}\indexisarmeth{rename-tac} |
9614 | 333 |
\indexisarmeth{rotate-tac}\indexisarmeth{tactic} |
9606 | 334 |
\begin{matharray}{rcl} |
335 |
rule_tac^* & : & \isarmeth \\ |
|
336 |
erule_tac^* & : & \isarmeth \\ |
|
337 |
drule_tac^* & : & \isarmeth \\ |
|
338 |
frule_tac^* & : & \isarmeth \\ |
|
339 |
cut_tac^* & : & \isarmeth \\ |
|
340 |
thin_tac^* & : & \isarmeth \\ |
|
341 |
subgoal_tac^* & : & \isarmeth \\ |
|
9614 | 342 |
rename_tac^* & : & \isarmeth \\ |
343 |
rotate_tac^* & : & \isarmeth \\ |
|
9606 | 344 |
tactic^* & : & \isarmeth \\ |
345 |
\end{matharray} |
|
346 |
||
347 |
\railalias{ruletac}{rule\_tac} |
|
348 |
\railterm{ruletac} |
|
349 |
||
350 |
\railalias{eruletac}{erule\_tac} |
|
351 |
\railterm{eruletac} |
|
352 |
||
353 |
\railalias{druletac}{drule\_tac} |
|
354 |
\railterm{druletac} |
|
355 |
||
356 |
\railalias{fruletac}{frule\_tac} |
|
357 |
\railterm{fruletac} |
|
358 |
||
359 |
\railalias{cuttac}{cut\_tac} |
|
360 |
\railterm{cuttac} |
|
361 |
||
362 |
\railalias{thintac}{thin\_tac} |
|
363 |
\railterm{thintac} |
|
364 |
||
365 |
\railalias{subgoaltac}{subgoal\_tac} |
|
366 |
\railterm{subgoaltac} |
|
367 |
||
9614 | 368 |
\railalias{renametac}{rename\_tac} |
369 |
\railterm{renametac} |
|
370 |
||
371 |
\railalias{rotatetac}{rotate\_tac} |
|
372 |
\railterm{rotatetac} |
|
373 |
||
9606 | 374 |
\begin{rail} |
375 |
( ruletac | eruletac | druletac | fruletac | cuttac | thintac ) goalspec? |
|
376 |
( insts thmref | thmrefs ) |
|
377 |
; |
|
378 |
subgoaltac goalspec? (prop +) |
|
379 |
; |
|
9614 | 380 |
renametac goalspec? (name +) |
381 |
; |
|
382 |
rotatetac goalspec? int? |
|
383 |
; |
|
9606 | 384 |
'tactic' text |
385 |
; |
|
386 |
||
387 |
insts: ((name '=' term) + 'and') 'in' |
|
388 |
; |
|
389 |
\end{rail} |
|
390 |
||
391 |
\begin{descr} |
|
392 |
\item [$rule_tac$ etc.] do resolution of rules with explicit instantiation. |
|
393 |
This works the same way as the ML tactics \texttt{res_inst_tac} etc. (see |
|
394 |
\cite[\S3]{isabelle-ref}). |
|
9614 | 395 |
|
9606 | 396 |
Note that multiple rules may be only given there is no instantiation. Then |
397 |
$rule_tac$ is the same as \texttt{resolve_tac} in ML (see |
|
398 |
\cite[\S3]{isabelle-ref}). |
|
399 |
\item [$cut_tac$] inserts facts into the proof state as assumption of a |
|
400 |
subgoal, see also \texttt{cut_facts_tac} in \cite[\S3]{isabelle-ref}. Note |
|
401 |
that the scope of schmatic variables is spread over the main goal statement. |
|
402 |
Instantiations may be given as well, see also ML tactic |
|
403 |
\texttt{cut_inst_tac} in \cite[\S3]{isabelle-ref}. |
|
404 |
\item [$thin_tac~\phi$] deletes the specified assumption from a subgoal; note |
|
405 |
that $\phi$ may contain schematic variables. See also \texttt{thin_tac} in |
|
406 |
\cite[\S3]{isabelle-ref}. |
|
407 |
\item [$subgoal_tac~\phi$] adds $\phi$ as an assumption to a subgoal. See |
|
408 |
also \texttt{subgoal_tac} and \texttt{subgoals_tac} in |
|
409 |
\cite[\S3]{isabelle-ref}. |
|
9614 | 410 |
\item [$rename_tac~\vec x$] renames parameters of a goal according to the list |
411 |
$\vec x$, which refers to the \emph{suffix} of variables. |
|
412 |
\item [$rotate_tac~n$] rotates the assumptions of a goal by $n$ positions: |
|
413 |
from right to left if $n$ is positive, and from left to right if $n$ is |
|
414 |
negative; the default value is $1$. See also \texttt{rotate_tac} in |
|
415 |
\cite[\S3]{isabelle-ref}. |
|
9606 | 416 |
\item [$tactic~text$] produces a proof method from any ML text of type |
417 |
\texttt{tactic}. Apart from the usual ML environment and the current |
|
418 |
implicit theory context, the ML code may refer to the following locally |
|
419 |
bound values: |
|
420 |
||
421 |
%%FIXME ttbox produces too much trailing space (why?) |
|
422 |
{\footnotesize\begin{verbatim} |
|
423 |
val ctxt : Proof.context |
|
424 |
val facts : thm list |
|
425 |
val thm : string -> thm |
|
426 |
val thms : string -> thm list |
|
427 |
\end{verbatim}} |
|
428 |
Here \texttt{ctxt} refers to the current proof context, \texttt{facts} |
|
429 |
indicates any current facts for forward-chaining, and |
|
430 |
\texttt{thm}~/~\texttt{thms} retrieve named facts (including global |
|
431 |
theorems) from the context. |
|
432 |
\end{descr} |
|
433 |
||
434 |
||
9614 | 435 |
\section{The Simplifier}\label{sec:simplifier} |
7135 | 436 |
|
7321 | 437 |
\subsection{Simplification methods}\label{sec:simp} |
7315 | 438 |
|
12618 | 439 |
\subsubsection{FIXME} |
440 |
||
8483 | 441 |
\indexisarmeth{simp}\indexisarmeth{simp-all} |
7315 | 442 |
\begin{matharray}{rcl} |
443 |
simp & : & \isarmeth \\ |
|
8483 | 444 |
simp_all & : & \isarmeth \\ |
7315 | 445 |
\end{matharray} |
446 |
||
8483 | 447 |
\railalias{simpall}{simp\_all} |
448 |
\railterm{simpall} |
|
449 |
||
8704 | 450 |
\railalias{noasm}{no\_asm} |
451 |
\railterm{noasm} |
|
452 |
||
453 |
\railalias{noasmsimp}{no\_asm\_simp} |
|
454 |
\railterm{noasmsimp} |
|
455 |
||
456 |
\railalias{noasmuse}{no\_asm\_use} |
|
457 |
\railterm{noasmuse} |
|
458 |
||
11128 | 459 |
\indexouternonterm{simpmod} |
7315 | 460 |
\begin{rail} |
8706 | 461 |
('simp' | simpall) ('!' ?) opt? (simpmod * ) |
7315 | 462 |
; |
463 |
||
8811 | 464 |
opt: '(' (noasm | noasmsimp | noasmuse) ')' |
8704 | 465 |
; |
9711 | 466 |
simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') | |
9847 | 467 |
'split' (() | 'add' | 'del')) ':' thmrefs |
7315 | 468 |
; |
469 |
\end{rail} |
|
470 |
||
7321 | 471 |
\begin{descr} |
8547 | 472 |
\item [$simp$] invokes Isabelle's simplifier, after declaring additional rules |
8594 | 473 |
according to the arguments given. Note that the \railtterm{only} modifier |
8547 | 474 |
first removes all other rewrite rules, congruences, and looper tactics |
8594 | 475 |
(including splits), and then behaves like \railtterm{add}. |
9711 | 476 |
|
477 |
\medskip The \railtterm{cong} modifiers add or delete Simplifier congruence |
|
478 |
rules (see also \cite{isabelle-ref}), the default is to add. |
|
479 |
||
480 |
\medskip The \railtterm{split} modifiers add or delete rules for the |
|
481 |
Splitter (see also \cite{isabelle-ref}), the default is to add. This works |
|
482 |
only if the Simplifier method has been properly setup to include the |
|
483 |
Splitter (all major object logics such HOL, HOLCF, FOL, ZF do this already). |
|
8483 | 484 |
\item [$simp_all$] is similar to $simp$, but acts on all goals. |
7321 | 485 |
\end{descr} |
486 |
||
8704 | 487 |
By default, the Simplifier methods are based on \texttt{asm_full_simp_tac} |
8706 | 488 |
internally \cite[\S10]{isabelle-ref}, which means that assumptions are both |
489 |
simplified as well as used in simplifying the conclusion. In structured |
|
490 |
proofs this is usually quite well behaved in practice: just the local premises |
|
491 |
of the actual goal are involved, additional facts may inserted via explicit |
|
492 |
forward-chaining (using $\THEN$, $\FROMNAME$ etc.). The full context of |
|
493 |
assumptions is only included if the ``$!$'' (bang) argument is given, which |
|
494 |
should be used with some care, though. |
|
7321 | 495 |
|
8704 | 496 |
Additional Simplifier options may be specified to tune the behavior even |
9614 | 497 |
further: $(no_asm)$ means assumptions are ignored completely (cf.\ |
8811 | 498 |
\texttt{simp_tac}), $(no_asm_simp)$ means assumptions are used in the |
9614 | 499 |
simplification of the conclusion but are not themselves simplified (cf.\ |
8811 | 500 |
\texttt{asm_simp_tac}), and $(no_asm_use)$ means assumptions are simplified |
501 |
but are not used in the simplification of each other or the conclusion (cf. |
|
8704 | 502 |
\texttt{full_simp_tac}). |
503 |
||
504 |
\medskip |
|
505 |
||
506 |
The Splitter package is usually configured to work as part of the Simplifier. |
|
9711 | 507 |
The effect of repeatedly applying \texttt{split_tac} can be simulated by |
508 |
$(simp~only\colon~split\colon~\vec a)$. There is also a separate $split$ |
|
509 |
method available for single-step case splitting, see \S\ref{sec:basic-eq}. |
|
8483 | 510 |
|
511 |
||
512 |
\subsection{Declaring rules} |
|
513 |
||
8667 | 514 |
\indexisarcmd{print-simpset} |
8638 | 515 |
\indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong} |
7321 | 516 |
\begin{matharray}{rcl} |
10154 | 517 |
print_simpset^* & : & \isarkeep{theory~|~proof} \\ |
7321 | 518 |
simp & : & \isaratt \\ |
9711 | 519 |
cong & : & \isaratt \\ |
8483 | 520 |
split & : & \isaratt \\ |
7321 | 521 |
\end{matharray} |
522 |
||
523 |
\begin{rail} |
|
9711 | 524 |
('simp' | 'cong' | 'split') (() | 'add' | 'del') |
7321 | 525 |
; |
526 |
\end{rail} |
|
527 |
||
528 |
\begin{descr} |
|
8667 | 529 |
\item [$print_simpset$] prints the collection of rules declared to the |
530 |
Simplifier, which is also known as ``simpset'' internally |
|
531 |
\cite{isabelle-ref}. This is a diagnostic command; $undo$ does not apply. |
|
8547 | 532 |
\item [$simp$] declares simplification rules. |
8638 | 533 |
\item [$cong$] declares congruence rules. |
9711 | 534 |
\item [$split$] declares case split rules. |
7321 | 535 |
\end{descr} |
7319 | 536 |
|
7315 | 537 |
|
538 |
\subsection{Forward simplification} |
|
539 |
||
9905 | 540 |
\indexisaratt{simplified} |
7315 | 541 |
\begin{matharray}{rcl} |
9905 | 542 |
simplified & : & \isaratt \\ |
7315 | 543 |
\end{matharray} |
544 |
||
9905 | 545 |
\begin{rail} |
546 |
'simplified' opt? |
|
547 |
; |
|
548 |
||
549 |
opt: '(' (noasm | noasmsimp | noasmuse) ')' |
|
550 |
; |
|
551 |
\end{rail} |
|
7905 | 552 |
|
9905 | 553 |
\begin{descr} |
554 |
\item [$simplified$] causes a theorem to be simplified according to the |
|
555 |
current Simplifier context (there are no separate arguments for declaring |
|
556 |
additional rules). By default the result is fully simplified, including |
|
557 |
assumptions and conclusion. The options $no_asm$ etc.\ restrict the |
|
558 |
Simplifier in the same way as the for the $simp$ method (see |
|
12618 | 559 |
\S\ref{sec:simp}). FIXME args |
9905 | 560 |
|
561 |
The $simplified$ operation should be used only very rarely, usually for |
|
562 |
experimentation only. |
|
563 |
\end{descr} |
|
7315 | 564 |
|
565 |
||
9711 | 566 |
\section{Basic equational reasoning}\label{sec:basic-eq} |
9614 | 567 |
|
9703 | 568 |
\indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisarmeth{split}\indexisaratt{symmetric} |
9614 | 569 |
\begin{matharray}{rcl} |
570 |
subst & : & \isarmeth \\ |
|
571 |
hypsubst^* & : & \isarmeth \\ |
|
9703 | 572 |
split & : & \isarmeth \\ |
9614 | 573 |
symmetric & : & \isaratt \\ |
574 |
\end{matharray} |
|
575 |
||
576 |
\begin{rail} |
|
577 |
'subst' thmref |
|
578 |
; |
|
9799 | 579 |
'split' ('(' 'asm' ')')? thmrefs |
9703 | 580 |
; |
9614 | 581 |
\end{rail} |
582 |
||
583 |
These methods and attributes provide basic facilities for equational reasoning |
|
584 |
that are intended for specialized applications only. Normally, single step |
|
585 |
reasoning would be performed by calculation (see \S\ref{sec:calculation}), |
|
586 |
while the Simplifier is the canonical tool for automated normalization (see |
|
587 |
\S\ref{sec:simplifier}). |
|
588 |
||
589 |
\begin{descr} |
|
590 |
\item [$subst~thm$] performs a single substitution step using rule $thm$, |
|
591 |
which may be either a meta or object equality. |
|
592 |
\item [$hypsubst$] performs substitution using some assumption. |
|
9703 | 593 |
\item [$split~thms$] performs single-step case splitting using rules $thms$. |
9799 | 594 |
By default, splitting is performed in the conclusion of a goal; the $asm$ |
595 |
option indicates to operate on assumptions instead. |
|
596 |
||
9703 | 597 |
Note that the $simp$ method already involves repeated application of split |
598 |
rules as declared in the current context (see \S\ref{sec:simp}). |
|
9614 | 599 |
\item [$symmetric$] applies the symmetry rule of meta or object equality. |
12618 | 600 |
FIXME sym decl |
9614 | 601 |
\end{descr} |
602 |
||
603 |
||
9847 | 604 |
\section{The Classical Reasoner}\label{sec:classical} |
7135 | 605 |
|
7335 | 606 |
\subsection{Basic methods}\label{sec:classical-basic} |
7321 | 607 |
|
7974 | 608 |
\indexisarmeth{rule}\indexisarmeth{intro} |
609 |
\indexisarmeth{elim}\indexisarmeth{default}\indexisarmeth{contradiction} |
|
7321 | 610 |
\begin{matharray}{rcl} |
611 |
rule & : & \isarmeth \\ |
|
612 |
intro & : & \isarmeth \\ |
|
613 |
elim & : & \isarmeth \\ |
|
614 |
contradiction & : & \isarmeth \\ |
|
615 |
\end{matharray} |
|
616 |
||
617 |
\begin{rail} |
|
8547 | 618 |
('rule' | 'intro' | 'elim') thmrefs? |
7321 | 619 |
; |
620 |
\end{rail} |
|
621 |
||
622 |
\begin{descr} |
|
7466 | 623 |
\item [$rule$] as offered by the classical reasoner is a refinement over the |
8517 | 624 |
primitive one (see \S\ref{sec:pure-meth-att}). In case that no rules are |
7466 | 625 |
provided as arguments, it automatically determines elimination and |
7321 | 626 |
introduction rules from the context (see also \S\ref{sec:classical-mod}). |
8517 | 627 |
This is made the default method for basic proof steps, such as $\PROOFNAME$ |
628 |
and ``$\DDOT$'' (two dots), see also \S\ref{sec:proof-steps} and |
|
629 |
\S\ref{sec:pure-meth-att}. |
|
9614 | 630 |
|
7466 | 631 |
\item [$intro$ and $elim$] repeatedly refine some goal by intro- or |
7905 | 632 |
elim-resolution, after having inserted any facts. Omitting the arguments |
8547 | 633 |
refers to any suitable rules declared in the context, otherwise only the |
634 |
explicitly given ones may be applied. The latter form admits better control |
|
635 |
of what actually happens, thus it is very appropriate as an initial method |
|
636 |
for $\PROOFNAME$ that splits up certain connectives of the goal, before |
|
637 |
entering the actual sub-proof. |
|
9614 | 638 |
|
7466 | 639 |
\item [$contradiction$] solves some goal by contradiction, deriving any result |
640 |
from both $\neg A$ and $A$. Facts, which are guaranteed to participate, may |
|
641 |
appear in either order. |
|
7321 | 642 |
\end{descr} |
643 |
||
644 |
||
7981 | 645 |
\subsection{Automated methods}\label{sec:classical-auto} |
7315 | 646 |
|
9799 | 647 |
\indexisarmeth{blast}\indexisarmeth{fast}\indexisarmeth{slow} |
648 |
\indexisarmeth{best}\indexisarmeth{safe}\indexisarmeth{clarify} |
|
7321 | 649 |
\begin{matharray}{rcl} |
9780 | 650 |
blast & : & \isarmeth \\ |
651 |
fast & : & \isarmeth \\ |
|
9799 | 652 |
slow & : & \isarmeth \\ |
9780 | 653 |
best & : & \isarmeth \\ |
654 |
safe & : & \isarmeth \\ |
|
655 |
clarify & : & \isarmeth \\ |
|
7321 | 656 |
\end{matharray} |
657 |
||
11128 | 658 |
\indexouternonterm{clamod} |
7321 | 659 |
\begin{rail} |
7905 | 660 |
'blast' ('!' ?) nat? (clamod * ) |
7321 | 661 |
; |
9799 | 662 |
('fast' | 'slow' | 'best' | 'safe' | 'clarify') ('!' ?) (clamod * ) |
7321 | 663 |
; |
664 |
||
9408 | 665 |
clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs |
7321 | 666 |
; |
667 |
\end{rail} |
|
668 |
||
669 |
\begin{descr} |
|
670 |
\item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac} |
|
7335 | 671 |
in \cite[\S11]{isabelle-ref}). The optional argument specifies a |
10858 | 672 |
user-supplied search bound (default 20). |
9799 | 673 |
\item [$fast$, $slow$, $best$, $safe$, and $clarify$] refer to the generic |
674 |
classical reasoner. See \texttt{fast_tac}, \texttt{slow_tac}, |
|
675 |
\texttt{best_tac}, \texttt{safe_tac}, and \texttt{clarify_tac} in |
|
676 |
\cite[\S11]{isabelle-ref} for more information. |
|
7321 | 677 |
\end{descr} |
678 |
||
679 |
Any of above methods support additional modifiers of the context of classical |
|
8517 | 680 |
rules. Their semantics is analogous to the attributes given in |
8547 | 681 |
\S\ref{sec:classical-mod}. Facts provided by forward chaining are |
682 |
inserted\footnote{These methods usually cannot make proper use of actual rules |
|
683 |
inserted that way, though.} into the goal before doing the search. The |
|
684 |
``!''~argument causes the full context of assumptions to be included as well. |
|
685 |
This is slightly less hazardous than for the Simplifier (see |
|
686 |
\S\ref{sec:simp}). |
|
7321 | 687 |
|
7315 | 688 |
|
9847 | 689 |
\subsection{Combined automated methods}\label{sec:clasimp} |
7315 | 690 |
|
9799 | 691 |
\indexisarmeth{auto}\indexisarmeth{force}\indexisarmeth{clarsimp} |
692 |
\indexisarmeth{fastsimp}\indexisarmeth{slowsimp}\indexisarmeth{bestsimp} |
|
7321 | 693 |
\begin{matharray}{rcl} |
9606 | 694 |
auto & : & \isarmeth \\ |
7321 | 695 |
force & : & \isarmeth \\ |
9438 | 696 |
clarsimp & : & \isarmeth \\ |
9606 | 697 |
fastsimp & : & \isarmeth \\ |
9799 | 698 |
slowsimp & : & \isarmeth \\ |
699 |
bestsimp & : & \isarmeth \\ |
|
7321 | 700 |
\end{matharray} |
701 |
||
11128 | 702 |
\indexouternonterm{clasimpmod} |
7321 | 703 |
\begin{rail} |
9780 | 704 |
'auto' '!'? (nat nat)? (clasimpmod * ) |
705 |
; |
|
9799 | 706 |
('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') '!'? (clasimpmod * ) |
7321 | 707 |
; |
7315 | 708 |
|
9711 | 709 |
clasimpmod: ('simp' (() | 'add' | 'del' | 'only') | |
10031 | 710 |
('cong' | 'split') (() | 'add' | 'del') | |
711 |
'iff' (((() | 'add') '?'?) | 'del') | |
|
9408 | 712 |
(('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' thmrefs |
7321 | 713 |
\end{rail} |
7315 | 714 |
|
7321 | 715 |
\begin{descr} |
9799 | 716 |
\item [$auto$, $force$, $clarsimp$, $fastsimp$, $slowsimp$, and $bestsimp$] |
717 |
provide access to Isabelle's combined simplification and classical reasoning |
|
718 |
tactics. These correspond to \texttt{auto_tac}, \texttt{force_tac}, |
|
719 |
\texttt{clarsimp_tac}, and Classical Reasoner tactics with the Simplifier |
|
720 |
added as wrapper, see \cite[\S11]{isabelle-ref} for more information. The |
|
721 |
modifier arguments correspond to those given in \S\ref{sec:simp} and |
|
9606 | 722 |
\S\ref{sec:classical-auto}. Just note that the ones related to the |
723 |
Simplifier are prefixed by \railtterm{simp} here. |
|
9614 | 724 |
|
7987 | 725 |
Facts provided by forward chaining are inserted into the goal before doing |
726 |
the search. The ``!''~argument causes the full context of assumptions to be |
|
727 |
included as well. |
|
7321 | 728 |
\end{descr} |
729 |
||
7987 | 730 |
|
8483 | 731 |
\subsection{Declaring rules}\label{sec:classical-mod} |
7135 | 732 |
|
8667 | 733 |
\indexisarcmd{print-claset} |
7391 | 734 |
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest} |
9936 | 735 |
\indexisaratt{iff}\indexisaratt{rule} |
7321 | 736 |
\begin{matharray}{rcl} |
10154 | 737 |
print_claset^* & : & \isarkeep{theory~|~proof} \\ |
7321 | 738 |
intro & : & \isaratt \\ |
739 |
elim & : & \isaratt \\ |
|
740 |
dest & : & \isaratt \\ |
|
9936 | 741 |
rule & : & \isaratt \\ |
7391 | 742 |
iff & : & \isaratt \\ |
7321 | 743 |
\end{matharray} |
7135 | 744 |
|
7321 | 745 |
\begin{rail} |
9408 | 746 |
('intro' | 'elim' | 'dest') ('!' | () | '?') |
7321 | 747 |
; |
9936 | 748 |
'rule' 'del' |
749 |
; |
|
10031 | 750 |
'iff' (((() | 'add') '?'?) | 'del') |
9936 | 751 |
; |
7321 | 752 |
\end{rail} |
7135 | 753 |
|
7321 | 754 |
\begin{descr} |
8667 | 755 |
\item [$print_claset$] prints the collection of rules declared to the |
756 |
Classical Reasoner, which is also known as ``simpset'' internally |
|
757 |
\cite{isabelle-ref}. This is a diagnostic command; $undo$ does not apply. |
|
8517 | 758 |
\item [$intro$, $elim$, and $dest$] declare introduction, elimination, and |
11332 | 759 |
destruction rules, respectively. By default, rules are considered as |
9408 | 760 |
\emph{unsafe} (i.e.\ not applied blindly without backtracking), while a |
761 |
single ``!'' classifies as \emph{safe}, and ``?'' as \emph{extra} (i.e.\ not |
|
762 |
applied in the search-oriented automated methods, but only in single-step |
|
763 |
methods such as $rule$). |
|
11332 | 764 |
\item [$rule~del$] deletes introduction, elimination, or destruction rules from |
9936 | 765 |
the context. |
11442 | 766 |
\item [$iff$] declares a (possibly conditional) ``safe'' rule to the context in |
767 |
several ways. The rule is declared as a rewrite rule to the Simplifier. |
|
768 |
Furthermore, it is |
|
11332 | 769 |
declared in several ways (depending on its structure) to the Classical |
770 |
Reasoner for aggressive use, which would normally be indicated by ``!''). |
|
771 |
If the rule is an equivalence, the two corresponding implications are |
|
11469 | 772 |
declared as introduction and destruction rules. Otherwise, |
773 |
if the rule is an inequality, the corresponding negation elimination rule |
|
11442 | 774 |
is declared, else the rule itself is declared as an introduction rule. |
10031 | 775 |
|
776 |
The ``?'' version of $iff$ declares ``extra'' Classical Reasoner rules only, |
|
777 |
and omits the Simplifier declaration. Thus the declaration does not have |
|
778 |
any effect on automated proof tools, but only on simple methods such as |
|
12618 | 779 |
$rule$ (see \S\ref{sec:misc-meth-att}). |
7321 | 780 |
\end{descr} |
7135 | 781 |
|
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8195
diff
changeset
|
782 |
|
12618 | 783 |
\section{Proof by cases and induction}\label{sec:cases-induct} |
784 |
||
785 |
\subsection{Rule contexts}\label{sec:rule-cases} |
|
786 |
||
787 |
\indexisarcmd{case}\indexisarcmd{print-cases} |
|
788 |
\indexisaratt{case-names}\indexisaratt{params}\indexisaratt{consumes} |
|
789 |
\begin{matharray}{rcl} |
|
790 |
\isarcmd{case} & : & \isartrans{proof(state)}{proof(state)} \\ |
|
791 |
\isarcmd{print_cases}^* & : & \isarkeep{proof} \\ |
|
792 |
case_names & : & \isaratt \\ |
|
793 |
params & : & \isaratt \\ |
|
794 |
consumes & : & \isaratt \\ |
|
795 |
\end{matharray} |
|
796 |
||
797 |
Basically, Isar proof contexts are built up explicitly using commands like |
|
798 |
$\FIXNAME$, $\ASSUMENAME$ etc.\ (see \S\ref{sec:proof-context}). In typical |
|
799 |
verification tasks this can become hard to manage, though. In particular, a |
|
800 |
large number of local contexts may emerge from case analysis or induction over |
|
801 |
inductive sets and types. |
|
802 |
||
803 |
\medskip |
|
804 |
||
805 |
The $\CASENAME$ command provides a shorthand to refer to certain parts of |
|
806 |
logical context symbolically. Proof methods may provide an environment of |
|
807 |
named ``cases'' of the form $c\colon \vec x, \vec \phi$. Then the effect of |
|
808 |
$\CASE{c}$ is exactly the same as $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$. |
|
809 |
||
810 |
FIXME |
|
811 |
||
812 |
It is important to note that $\CASENAME$ does \emph{not} provide any means to |
|
813 |
peek at the current goal state, which is treated as strictly non-observable in |
|
814 |
Isar! Instead, the cases considered here usually emerge in a canonical way |
|
815 |
from certain pieces of specification that appear in the theory somewhere else |
|
816 |
(e.g.\ in an inductive definition, or recursive function). |
|
817 |
||
818 |
FIXME |
|
819 |
||
820 |
\medskip |
|
821 |
||
822 |
Named cases may be exhibited in the current proof context only if both the |
|
823 |
proof method and the rules involved support this. Case names and parameters |
|
824 |
of basic rules may be declared by hand as well, by using appropriate |
|
825 |
attributes. Thus variant versions of rules that have been derived manually |
|
826 |
may be used in advanced case analysis later. |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
827 |
|
12618 | 828 |
\railalias{casenames}{case\_names} |
829 |
\railterm{casenames} |
|
830 |
||
831 |
\begin{rail} |
|
832 |
'case' nameref attributes? |
|
833 |
; |
|
834 |
casenames (name + ) |
|
835 |
; |
|
836 |
'params' ((name * ) + 'and') |
|
837 |
; |
|
838 |
'consumes' nat? |
|
839 |
; |
|
840 |
\end{rail} |
|
841 |
%FIXME bug in rail |
|
842 |
||
843 |
\begin{descr} |
|
844 |
\item [$\CASE{c}$] invokes a named local context $c\colon \vec x, \vec \phi$, |
|
845 |
as provided by an appropriate proof method (such as $cases$ and $induct$, |
|
846 |
see \S\ref{sec:cases-induct-meth}). The command $\CASE{c}$ abbreviates |
|
847 |
$\FIX{\vec x}~\ASSUME{c}{\vec\phi}$. |
|
848 |
\item [$\isarkeyword{print_cases}$] prints all local contexts of the current |
|
849 |
state, using Isar proof language notation. This is a diagnostic command; |
|
850 |
$undo$ does not apply. |
|
851 |
\item [$case_names~\vec c$] declares names for the local contexts of premises |
|
852 |
of some theorem; $\vec c$ refers to the \emph{suffix} of the list of |
|
853 |
premises. |
|
854 |
\item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of |
|
855 |
premises $1, \dots, n$ of some theorem. An empty list of names may be given |
|
856 |
to skip positions, leaving the present parameters unchanged. |
|
857 |
||
858 |
Note that the default usage of case rules does \emph{not} directly expose |
|
859 |
parameters to the proof context (see also \S\ref{sec:cases-induct-meth}). |
|
860 |
\item [$consumes~n$] declares the number of ``major premises'' of a rule, |
|
861 |
i.e.\ the number of facts to be consumed when it is applied by an |
|
862 |
appropriate proof method (cf.\ \S\ref{sec:cases-induct-meth}). The default |
|
863 |
value of $consumes$ is $n = 1$, which is appropriate for the usual kind of |
|
864 |
cases and induction rules for inductive sets (cf.\ |
|
865 |
\S\ref{sec:hol-inductive}). Rules without any $consumes$ declaration given |
|
866 |
are treated as if $consumes~0$ had been specified. |
|
867 |
||
868 |
Note that explicit $consumes$ declarations are only rarely needed; this is |
|
869 |
already taken care of automatically by the higher-level $cases$ and $induct$ |
|
870 |
declarations, see also \S\ref{sec:cases-induct-att}. |
|
871 |
\end{descr} |
|
872 |
||
873 |
||
874 |
\subsection{Proof methods}\label{sec:cases-induct-meth} |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
875 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
876 |
\indexisarmeth{cases}\indexisarmeth{induct} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
877 |
\begin{matharray}{rcl} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
878 |
cases & : & \isarmeth \\ |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
879 |
induct & : & \isarmeth \\ |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
880 |
\end{matharray} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
881 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
882 |
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
|
883 |
and induction over datatypes, inductive sets, and recursive functions. The |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
884 |
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
|
885 |
Furthermore, these methods provide named local contexts that may be invoked |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
886 |
via the $\CASENAME$ proof command within the subsequent proof text (cf.\ |
12618 | 887 |
\S\ref{sec:rule-cases}). This accommodates compact proof texts even when |
888 |
reasoning about large specifications. |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
889 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
890 |
Note that the full spectrum of this generic functionality is currently only |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
891 |
supported by Isabelle/HOL, when used in conjunction with advanced definitional |
12618 | 892 |
packages (see especially \S\ref{sec:hol-datatype} and |
893 |
\S\ref{sec:hol-inductive}). |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
894 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
895 |
\begin{rail} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
896 |
'cases' spec |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
897 |
; |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
898 |
'induct' spec |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
899 |
; |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
900 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
901 |
spec: open? args rule? params? |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
902 |
; |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
903 |
open: '(' 'open' ')' |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
904 |
; |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
905 |
args: (insts * 'and') |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
906 |
; |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
907 |
rule: ('type' | 'set') ':' nameref | 'rule' ':' thmref |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
908 |
; |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
909 |
params: 'of' ':' insts |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
910 |
; |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
911 |
\end{rail} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
912 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
913 |
\begin{descr} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
914 |
\item [$cases~insts~R~ps$] applies method $rule$ with an appropriate case |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
915 |
distinction theorem, instantiated to the subjects $insts$. Symbolic case |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
916 |
names are bound according to the rule's local contexts. |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
917 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
918 |
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
|
919 |
passed to the $cases$ method: |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
920 |
\begin{matharray}{llll} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
921 |
\Text{facts} & & \Text{arguments} & \Text{rule} \\\hline |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
922 |
& cases & & \Text{classical case split} \\ |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
923 |
& cases & t & \Text{datatype exhaustion (type of $t$)} \\ |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
924 |
\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
|
925 |
\dots & cases & \dots ~ R & \Text{explicit rule $R$} \\ |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
926 |
\end{matharray} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
927 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
928 |
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
|
929 |
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
|
930 |
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
|
931 |
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
|
932 |
usually the same for all cases). |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
933 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
934 |
Additional parameters may be specified as $ps$; these are applied after the |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
935 |
primary instantiation in the same manner as by the $of$ attribute (cf.\ |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
936 |
\S\ref{sec:pure-meth-att}). This feature is rarely needed in practice; a |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
937 |
typical application would be to specify additional arguments for rules |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
938 |
stemming from parameterized inductive definitions (see also |
12618 | 939 |
\S\ref{sec:hol-inductive}). |
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
940 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
941 |
The $open$ option causes the parameters of the new local contexts to be |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
942 |
exposed to the current proof context. Thus local variables stemming from |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
943 |
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
|
944 |
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
|
945 |
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
|
946 |
less robust proof texts. |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
947 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
948 |
\item [$induct~insts~R~ps$] is analogous to the $cases$ method, but refers to |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
949 |
induction rules, which are determined as follows: |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
950 |
\begin{matharray}{llll} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
951 |
\Text{facts} & & \Text{arguments} & \Text{rule} \\\hline |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
952 |
& induct & P ~ x ~ \dots & \Text{datatype induction (type of $x$)} \\ |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
953 |
\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
|
954 |
\dots & induct & \dots ~ R & \Text{explicit rule $R$} \\ |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
955 |
\end{matharray} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
956 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
957 |
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
|
958 |
inductive definition or datatype --- only related partial induction rules |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
959 |
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
|
960 |
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
|
961 |
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
|
962 |
predicates and variables, for example. |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
963 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
964 |
Additional parameters (including the $open$ option) may be given in the same |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
965 |
way as for $cases$, see above. |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
966 |
\end{descr} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
967 |
|
12618 | 968 |
Above methods produce named local contexts (cf.\ \S\ref{sec:rule-cases}), as |
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
969 |
determined by the instantiated rule \emph{before} it has been applied to the |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
970 |
internal proof state.\footnote{As a general principle, Isar proof text may |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
971 |
never refer to parts of proof states directly.} Thus proper use of symbolic |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
972 |
cases usually require the rule to be instantiated fully, as far as the |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
973 |
emerging local contexts and subgoals are concerned. In particular, for |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
974 |
induction both the predicates and variables have to be specified. Otherwise |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
975 |
the $\CASENAME$ command would refuse to invoke cases containing schematic |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
976 |
variables. Furthermore the resulting local goal statement is bound to the |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
977 |
term variable $\Var{case}$\indexisarvar{case} --- for each case where it is |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
978 |
fully specified. |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
979 |
|
12618 | 980 |
The $\isarkeyword{print_cases}$ command (\S\ref{sec:rule-cases}) prints all |
981 |
named cases present in the current proof state. |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
982 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
983 |
\medskip |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
984 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
985 |
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
|
986 |
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
|
987 |
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
|
988 |
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
|
989 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
990 |
In contrast, $induct$ passes the full goal statement through the ``recursive'' |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
991 |
course involved in the induction. Thus the original statement is basically |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
992 |
replaced by separate copies, corresponding to the induction hypotheses and |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
993 |
conclusion; the original goal context is no longer available. This behavior |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
994 |
allows \emph{strengthened induction predicates} to be expressed concisely as |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
995 |
meta-level rule statements, i.e.\ $\All{\vec x} \vec\phi \Imp \psi$ to |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
996 |
indicate ``variable'' parameters $\vec x$ and ``recursive'' assumptions |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
997 |
$\vec\phi$. Also note that local definitions may be expressed as $\All{\vec |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
998 |
x} n \equiv t[\vec x] \Imp \phi[n]$, with induction over $n$. |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
999 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1000 |
\medskip |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1001 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1002 |
Facts presented to either method are consumed according to the number of |
12618 | 1003 |
``major premises'' of the rule involved (see also \S\ref{sec:cases-induct}), |
1004 |
which is usually $0$ for plain cases and induction rules of datatypes etc.\ |
|
1005 |
and $1$ for rules of inductive sets and the like. The remaining facts are |
|
1006 |
inserted into the goal verbatim before the actual $cases$ or $induct$ rule is |
|
1007 |
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
|
1008 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1009 |
Note that whenever facts are present, the default rule selection scheme would |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1010 |
provide a ``set'' rule only, with the first fact consumed and the rest |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1011 |
inserted into the goal. In order to pass all facts into a ``type'' rule |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1012 |
instead, one would have to specify this explicitly, e.g.\ by appending |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1013 |
``$type: name$'' to the method argument. |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1014 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1015 |
|
12618 | 1016 |
\subsection{Declaring rules}\label{sec:cases-induct-att} |
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1017 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1018 |
\indexisarcmd{print-induct-rules}\indexisaratt{cases}\indexisaratt{induct} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1019 |
\begin{matharray}{rcl} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1020 |
\isarcmd{print_induct_rules}^* & : & \isarkeep{theory~|~proof} \\ |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1021 |
cases & : & \isaratt \\ |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1022 |
induct & : & \isaratt \\ |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1023 |
\end{matharray} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1024 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1025 |
\begin{rail} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1026 |
'cases' spec |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1027 |
; |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1028 |
'induct' spec |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1029 |
; |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1030 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1031 |
spec: ('type' | 'set') ':' nameref |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1032 |
; |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1033 |
\end{rail} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1034 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1035 |
The $cases$ and $induct$ attributes augment the corresponding context of rules |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1036 |
for reasoning about inductive sets and types. The standard rules are already |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1037 |
declared by advanced definitional packages. For special applications, these |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1038 |
may be replaced manually by variant versions. |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1039 |
|
12618 | 1040 |
Refer to the $case_names$ and $ps$ attributes (see \S\ref{sec:rule-cases}) to |
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1041 |
adjust names of cases and parameters of a rule. |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1042 |
|
12618 | 1043 |
The $consumes$ declaration (cf.\ \S\ref{sec:rule-cases}) is taken care of |
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1044 |
automatically (if none had been given already): $consumes~0$ is specified for |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1045 |
``type'' rules and $consumes~1$ for ``set'' rules. |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1046 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1047 |
|
12618 | 1048 |
\section{Object-logic setup}\label{sec:object-logic} |
1049 |
||
1050 |
The very starting point for any Isabelle object-logic is a ``truth judgment'' |
|
1051 |
that links object-level statements to the meta-logic (with its minimal |
|
1052 |
language of $prop$ that covers universal quantification $\Forall$ and |
|
1053 |
implication $\Imp$). Common object-logics are sufficiently expressive to |
|
1054 |
\emph{internalize} rule statements over $\Forall$ and $\Imp$ within their own |
|
1055 |
language. This is useful in certain situations where a rule needs to be |
|
1056 |
viewed as an atomic statement from the meta-level perspective (e.g.\ $\All x x |
|
1057 |
\in A \Imp P(x)$ versus $\forall x \in A. P(x)$). |
|
1058 |
||
1059 |
From the following language elements, only the $atomize$ method and |
|
1060 |
$rule_format$ attribute are occasionally required by end-users, the rest is |
|
1061 |
mainly for those who need to setup their own object-logic. In the latter case |
|
1062 |
existing formulations of Isabelle/FOL or Isabelle/HOL may be taken as |
|
1063 |
realistic examples. |
|
1064 |
||
1065 |
Further generic tools may refer to the information provided by object-logic |
|
1066 |
declarations internally (such as locales \S\ref{sec:locale}, or the Classical |
|
1067 |
Reasoner \S\ref{sec:classical}). |
|
1068 |
||
1069 |
\indexisarcmd{judgment} |
|
1070 |
\indexisarmeth{atomize}\indexisaratt{atomize} |
|
1071 |
\indexisaratt{rule-format}\indexisaratt{rulify} |
|
1072 |
||
1073 |
\begin{matharray}{rcl} |
|
1074 |
\isarcmd{judgment} & : & \isartrans{theory}{theory} \\ |
|
1075 |
atomize & : & \isarmeth \\ |
|
1076 |
atomize & : & \isaratt \\ |
|
1077 |
rule_format & : & \isaratt \\ |
|
1078 |
rulify & : & \isaratt \\ |
|
1079 |
\end{matharray} |
|
1080 |
||
1081 |
\railalias{ruleformat}{rule\_format} |
|
1082 |
\railterm{ruleformat} |
|
1083 |
||
1084 |
\begin{rail} |
|
1085 |
'judgment' constdecl |
|
1086 |
; |
|
1087 |
ruleformat ('(' noasm ')')? |
|
1088 |
; |
|
1089 |
\end{rail} |
|
1090 |
||
1091 |
\begin{descr} |
|
1092 |
||
1093 |
\item [$\isarkeyword{judgment}~c::\sigma~~syn$] declares constant $c$ as the |
|
1094 |
truth judgment of the current object-logic. Its type $\sigma$ should |
|
1095 |
specify a coercion of the category of object-level propositions to $prop$ of |
|
1096 |
the Pure meta-logic; the mixfix annotation $syn$ would typically just link |
|
1097 |
the object language (internally of syntactic category $logic$) with that of |
|
1098 |
$prop$. Only one $\isarkeyword{judgment}$ declaration may be given in any |
|
1099 |
theory development. |
|
1100 |
||
1101 |
\item [$atomize$] (as a method) rewrites any non-atomic premises of a |
|
1102 |
sub-goal, using the meta-level equations that have been declared via |
|
1103 |
$atomize$ (as an attribute) beforehand. As a result, heavily nested goals |
|
1104 |
become amenable to fundamental operations such as resolution (cf.\ the |
|
1105 |
$rule$ method) and proof-by-assumption (cf.\ $assumption$). |
|
1106 |
||
1107 |
A typical collection of $atomize$ rules for a particular object-logic would |
|
1108 |
provide an internalization for each of the connectives of $\Forall$, $\Imp$, |
|
1109 |
$\equiv$; meta-level conjunction expressed as $\All{\PROP\,C} (A \Imp B \Imp |
|
1110 |
\PROP\,C) \Imp PROP\,C$ should be covered as well. |
|
1111 |
||
1112 |
\item [$rule_format$] rewrites a theorem by the equalities declared as |
|
1113 |
$rulify$ rules in the current object-logic. By default, the result is fully |
|
1114 |
normalized, including assumptions and conclusions at any depth. The |
|
1115 |
$no_asm$ option restricts the transformation to the conclusion of a rule. |
|
1116 |
||
1117 |
In common object logics (HOL, FOL, ZF), the effect of $rule_format$ is to |
|
1118 |
replace (bounded) universal quantification ($\forall$) and implication |
|
1119 |
($\imp$) by the corresponding rule statements over $\Forall$ and $\Imp$. |
|
1120 |
||
1121 |
\end{descr} |
|
1122 |
||
1123 |
||
9614 | 1124 |
%%% Local Variables: |
7135 | 1125 |
%%% mode: latex |
1126 |
%%% TeX-master: "isar-ref" |
|
9614 | 1127 |
%%% End: |