author | haftmann |
Tue, 23 Oct 2007 11:48:12 +0200 | |
changeset 25155 | 65612c9f7381 |
parent 25094 | ba43514068fd |
child 25544 | 437251bbc5ce |
permissions | -rw-r--r-- |
13048 | 1 |
\chapter{Generic tools and packages}\label{ch:gen-tools} |
7167 | 2 |
|
24085 | 3 |
\section{Specification commands} |
12618 | 4 |
|
19070
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
5 |
\subsection{Derived specifications} |
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
6 |
|
19666 | 7 |
\indexisarcmd{axiomatization} |
19070
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
8 |
\indexisarcmd{definition}\indexisaratt{defn} |
21716 | 9 |
\indexisarcmd{abbreviation}\indexisarcmd{print-abbrevs} |
24944 | 10 |
\indexisarcmd{notation}\indexisarcmd{no-notation} |
19070
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
11 |
\begin{matharray}{rcll} |
19666 | 12 |
\isarcmd{axiomatization} & : & \isarkeep{local{\dsh}theory} & (axiomatic!)\\ |
19070
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
13 |
\isarcmd{definition} & : & \isarkeep{local{\dsh}theory} \\ |
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
14 |
defn & : & \isaratt \\ |
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
15 |
\isarcmd{abbreviation} & : & \isarkeep{local{\dsh}theory} \\ |
21716 | 16 |
\isarcmd{print_abbrevs}^* & : & \isarkeep{theory~|~proof} \\ |
21209
dbb8decc36bc
'const_syntax' command: allow fixed variables, renamed to 'notation';
wenzelm
parents:
21076
diff
changeset
|
17 |
\isarcmd{notation} & : & \isarkeep{local{\dsh}theory} \\ |
24944 | 18 |
\isarcmd{no_notation} & : & \isarkeep{local{\dsh}theory} \\ |
19070
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
19 |
\end{matharray} |
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
20 |
|
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
21 |
These specification mechanisms provide a slightly more abstract view |
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
22 |
than the underlying primitives of $\CONSTS$, $\DEFS$ (see |
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
23 |
\S\ref{sec:consts}), and $\isarkeyword{axioms}$ (see |
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
24 |
\S\ref{sec:axms-thms}). In particular, type-inference is commonly |
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
25 |
available, and result names need not be given. |
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
26 |
|
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
27 |
\begin{rail} |
21601
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21403
diff
changeset
|
28 |
'axiomatization' target? fixes? ('where' specs)? |
19666 | 29 |
; |
21601
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21403
diff
changeset
|
30 |
'definition' target? (decl 'where')? thmdecl? prop |
19070
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
31 |
; |
21601
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21403
diff
changeset
|
32 |
'abbreviation' target? mode? (decl 'where')? prop |
19070
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
33 |
; |
24955 | 34 |
('notation' | 'no\_notation') target? mode? (nameref structmixfix + 'and') |
19070
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
35 |
; |
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
36 |
|
21601
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21403
diff
changeset
|
37 |
fixes: ((name ('::' type)? mixfix? | vars) + 'and') |
19070
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
38 |
; |
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
39 |
specs: (thmdecl? props + 'and') |
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
40 |
; |
21601
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21403
diff
changeset
|
41 |
decl: name ('::' type)? mixfix? |
6588b947d631
simplified syntax for 'definition', 'abbreviation';
wenzelm
parents:
21403
diff
changeset
|
42 |
; |
19070
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
43 |
\end{rail} |
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
44 |
|
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
45 |
\begin{descr} |
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
46 |
|
19666 | 47 |
\item $\isarkeyword{axiomatization} ~ c@1 \dots c@n ~ |
48 |
\isarkeyword{where} ~ A@1 \dots A@m$ introduces several constants |
|
49 |
simultaneously and states axiomatic properties for these. The |
|
50 |
constants are marked as being specified once and for all, which |
|
51 |
prevents additional specifications being issued later on. |
|
52 |
||
53 |
Note that axiomatic specifications are only appropriate when |
|
54 |
declaring a new logical system. Normal applications should only use |
|
55 |
definitional mechanisms! |
|
56 |
||
19070
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
57 |
\item $\isarkeyword{definition}~c~\isarkeyword{where}~eq$ produces an |
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
58 |
internal definition $c \equiv t$ according to the specification |
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
59 |
given as $eq$, which is then turned into a proven fact. The given |
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
60 |
proposition may deviate from internal meta-level equality according |
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
61 |
to the rewrite rules declared as $defn$ by the object-logic. This |
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
62 |
typically covers object-level equality $x = t$ and equivalence $A |
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
63 |
\leftrightarrow B$. Users normally need not change the $defn$ |
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
64 |
setup. |
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
65 |
|
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
66 |
Definitions may be presented with explicit arguments on the LHS, as |
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
67 |
well as additional conditions, e.g.\ $f\;x\;y = t$ instead of $f |
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
68 |
\equiv \lambda x\;y. t$ and $y \not= 0 \Imp g\;x\;y = u$ instead of |
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
69 |
an unguarded $g \equiv \lambda x\;y. u$. |
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
70 |
|
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
71 |
\item $\isarkeyword{abbreviation}~c~\isarkeyword{where}~eq$ introduces |
19363 | 72 |
a syntactic constant which is associated with a certain term |
73 |
according to the meta-level equality $eq$. |
|
19070
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
74 |
|
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
75 |
Abbreviations participate in the usual type-inference process, but |
19363 | 76 |
are expanded before the logic ever sees them. Pretty printing of |
77 |
terms involves higher-order rewriting with rules stemming from |
|
78 |
reverted abbreviations. This needs some care to avoid overlapping |
|
79 |
or looping syntactic replacements! |
|
80 |
||
81 |
The optional $mode$ specification restricts output to a particular |
|
82 |
print mode; using ``$input$'' here achieves the effect of one-way |
|
83 |
abbreviations. The mode may also include an ``$output$'' qualifier |
|
84 |
that affects the concrete syntax declared for abbreviations, cf.\ |
|
85 |
$\isarkeyword{syntax}$ in \S\ref{sec:syn-trans}. |
|
19070
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
86 |
|
21716 | 87 |
\item $\isarkeyword{print_abbrevs}$ prints all constant abbreviations |
88 |
of the current context. |
|
89 |
||
21209
dbb8decc36bc
'const_syntax' command: allow fixed variables, renamed to 'notation';
wenzelm
parents:
21076
diff
changeset
|
90 |
\item $\isarkeyword{notation}~c~mx$ associates mixfix syntax with an |
dbb8decc36bc
'const_syntax' command: allow fixed variables, renamed to 'notation';
wenzelm
parents:
21076
diff
changeset
|
91 |
existing constant or fixed variable. This is a robust interface to |
dbb8decc36bc
'const_syntax' command: allow fixed variables, renamed to 'notation';
wenzelm
parents:
21076
diff
changeset
|
92 |
the underlying $\isarkeyword{syntax}$ primitive |
dbb8decc36bc
'const_syntax' command: allow fixed variables, renamed to 'notation';
wenzelm
parents:
21076
diff
changeset
|
93 |
(\S\ref{sec:syn-trans}). Type declaration and internal syntactic |
dbb8decc36bc
'const_syntax' command: allow fixed variables, renamed to 'notation';
wenzelm
parents:
21076
diff
changeset
|
94 |
representation of the given entity is retrieved from the context. |
19070
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
95 |
|
24944 | 96 |
\item $\isarkeyword{no_notation}$ is similar to |
24955 | 97 |
$\isarkeyword{notation}$, but removes the specified syntax |
98 |
annotation from the present context. |
|
24944 | 99 |
|
19070
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
100 |
\end{descr} |
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
101 |
|
24944 | 102 |
All of these specifications support local theory targets (cf.\ |
21303 | 103 |
\S\ref{sec:target}). |
19070
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
104 |
|
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
105 |
|
24026 | 106 |
\subsection{Generic declarations} |
107 |
||
108 |
Arbitrary operations on the background context may be wrapped-up as |
|
109 |
generic declaration elements. Since the underlying concept of local |
|
110 |
theories may be subject to later re-interpretation, there is an |
|
111 |
additional dependency on a morphism that tells the difference of the |
|
112 |
original declaration context wrt.\ the application context encountered |
|
113 |
later on. A fact declaration is an important special case: it |
|
114 |
consists of a theorem which is applied to the context by means of an |
|
115 |
attribute. |
|
116 |
||
117 |
\indexisarcmd{declaration}\indexisarcmd{declare} |
|
118 |
\begin{matharray}{rcl} |
|
119 |
\isarcmd{declaration} & : & \isarkeep{local{\dsh}theory} \\ |
|
120 |
\isarcmd{declare} & : & \isarkeep{local{\dsh}theory} \\ |
|
121 |
\end{matharray} |
|
122 |
||
123 |
\begin{rail} |
|
124 |
'declaration' target? text |
|
125 |
; |
|
126 |
'declare' target? (thmrefs + 'and') |
|
127 |
; |
|
128 |
\end{rail} |
|
129 |
||
130 |
\begin{descr} |
|
131 |
||
132 |
\item [$\isarkeyword{declaration}~d$] adds the declaration function |
|
133 |
$d$ of ML type \verb,declaration, to the current local theory under |
|
134 |
construction. In later application contexts, the function is |
|
135 |
transformed according to the morphisms being involved in the |
|
136 |
interpretation hierarchy. |
|
137 |
||
138 |
\item [$\isarkeyword{declare}~thms$] declares theorems to the current |
|
139 |
local theory context. No theorem binding is involved here, unlike |
|
140 |
$\isarkeyword{theorems}$ or $\isarkeyword{lemmas}$ (cf.\ |
|
141 |
\S\ref{sec:axms-thms}), so $\isarkeyword{declare}$ only has the |
|
142 |
effect of applying attributes as included in the theorem |
|
143 |
specification. |
|
144 |
||
145 |
\end{descr} |
|
146 |
||
147 |
||
21303 | 148 |
\subsection{Local theory targets}\label{sec:target} |
149 |
||
150 |
A local theory target is a context managed separately within the |
|
151 |
enclosing theory. Contexts may introduce parameters (fixed variables) |
|
152 |
and assumptions (hypotheses). Definitions and theorems depending on |
|
153 |
the context may be added incrementally later on. Named contexts refer |
|
154 |
to locales (cf.\ \S\ref{sec:locale}) or type classes (cf.\ |
|
155 |
\S\ref{sec:class}); the name ``$-$'' signifies the global theory |
|
156 |
context. |
|
157 |
||
158 |
\indexisarcmd{context}\indexisarcmd{end} |
|
159 |
\begin{matharray}{rcll} |
|
160 |
\isarcmd{context} & : & \isartrans{theory}{local{\dsh}theory} \\ |
|
161 |
\isarcmd{end} & : & \isartrans{local{\dsh}theory}{theory} \\ |
|
162 |
\end{matharray} |
|
163 |
||
164 |
\indexouternonterm{target} |
|
165 |
\begin{rail} |
|
166 |
'context' name 'begin' |
|
167 |
; |
|
168 |
||
169 |
target: '(' 'in' name ')' |
|
170 |
; |
|
171 |
\end{rail} |
|
172 |
||
173 |
\begin{descr} |
|
174 |
||
175 |
\item $\isarkeyword{context}~c~\isarkeyword{begin}$ recommences an |
|
176 |
existing locale or class context $c$. Note that locale and class |
|
177 |
definitions allow to include the $\isarkeyword{begin}$ keyword as |
|
178 |
well, in order to continue the local theory immediately after the |
|
179 |
initial specification. |
|
180 |
||
181 |
\item $\END$ concludes the current local theory and continues the |
|
182 |
enclosing global theory. Note that a non-local $\END$ has a |
|
183 |
different meaning: it concludes the theory itself |
|
184 |
(\S\ref{sec:begin-thy}). |
|
185 |
||
186 |
\item $(\IN~loc)$ given after any local theory command specifies an |
|
187 |
immediate target, e.g.\ |
|
188 |
``$\isarkeyword{definition}~(\IN~loc)~\dots$'' or |
|
189 |
``$\THEOREMNAME~(\IN~loc)~\dots$''. This works both in a local or |
|
190 |
global theory context; the current target context will be suspended |
|
191 |
for this command only. Note that $(\IN~-)$ will always produce a |
|
192 |
global result independently of the current target context. |
|
193 |
||
194 |
\end{descr} |
|
195 |
||
196 |
The exact meaning of results produced within a local theory context |
|
197 |
depends on the underlying target infrastructure (locale, type class |
|
198 |
etc.). The general idea is as follows, considering a context named |
|
199 |
$c$ with parameter $x$ and assumption $A[x]$. |
|
200 |
||
201 |
Definitions are exported by introducing a global version with |
|
202 |
additional arguments; a syntactic abbreviation links the long form |
|
203 |
with the abstract version of the target context. For example, $a |
|
204 |
\equiv t[x]$ becomes $c\dtt a \; ?x \equiv t[?x]$ at the theory level |
|
205 |
(for arbitrary $?x$), together with a local abbreviation $c \equiv |
|
206 |
c\dtt a\; x$ in the target context (for fixed $x$). |
|
207 |
||
208 |
Theorems are exported by discharging the assumptions and generalizing |
|
209 |
the parameters of the context. For example, $a: B[x]$ becomes $c\dtt |
|
210 |
a: A[?x] \Imp B[?x]$ (for arbitrary $?x$). |
|
211 |
||
212 |
||
213 |
\subsection{Locales}\label{sec:locale} |
|
12618 | 214 |
|
13040 | 215 |
Locales are named local contexts, consisting of a list of declaration elements |
13041 | 216 |
that are modeled after the Isar proof context commands (cf.\ |
13040 | 217 |
\S\ref{sec:proof-context}). |
12976 | 218 |
|
13048 | 219 |
|
12976 | 220 |
\subsubsection{Locale specifications} |
221 |
||
222 |
\indexisarcmd{locale}\indexisarcmd{print-locale}\indexisarcmd{print-locales} |
|
223 |
\begin{matharray}{rcl} |
|
19070
99001616e0e2
derived specifications: definition, abbreviation, axiomatization;
wenzelm
parents:
18903
diff
changeset
|
224 |
\isarcmd{locale} & : & \isartrans{theory}{local{\dsh}theory} \\ |
12976 | 225 |
\isarcmd{print_locale}^* & : & \isarkeep{theory~|~proof} \\ |
226 |
\isarcmd{print_locales}^* & : & \isarkeep{theory~|~proof} \\ |
|
20468
0bda06d731ee
Documented methods intro_locales and unfold_locales.
ballarin
parents:
20467
diff
changeset
|
227 |
intro_locales & : & \isarmeth \\ |
0bda06d731ee
Documented methods intro_locales and unfold_locales.
ballarin
parents:
20467
diff
changeset
|
228 |
unfold_locales & : & \isarmeth \\ |
12976 | 229 |
\end{matharray} |
230 |
||
231 |
\indexouternonterm{contextexpr}\indexouternonterm{contextelem} |
|
18903 | 232 |
\indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes} |
233 |
\indexisarelem{defines}\indexisarelem{notes}\indexisarelem{includes} |
|
12976 | 234 |
|
235 |
\begin{rail} |
|
21303 | 236 |
'locale' ('(open)')? name ('=' localeexpr)? 'begin'? |
12976 | 237 |
; |
18903 | 238 |
'print\_locale' '!'? localeexpr |
12976 | 239 |
; |
240 |
localeexpr: ((contextexpr '+' (contextelem+)) | contextexpr | (contextelem+)) |
|
241 |
; |
|
242 |
||
243 |
contextexpr: nameref | '(' contextexpr ')' | |
|
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16010
diff
changeset
|
244 |
(contextexpr (name mixfix? +)) | (contextexpr + '+') |
12976 | 245 |
; |
16168
adb83939177f
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16102
diff
changeset
|
246 |
contextelem: fixes | constrains | assumes | defines | notes | includes |
12976 | 247 |
; |
18854 | 248 |
fixes: 'fixes' ((name ('::' type)? structmixfix? | vars) + 'and') |
12976 | 249 |
; |
16168
adb83939177f
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16102
diff
changeset
|
250 |
constrains: 'constrains' (name '::' type + 'and') |
adb83939177f
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16102
diff
changeset
|
251 |
; |
12976 | 252 |
assumes: 'assumes' (thmdecl? props + 'and') |
253 |
; |
|
254 |
defines: 'defines' (thmdecl? prop proppat? + 'and') |
|
255 |
; |
|
256 |
notes: 'notes' (thmdef? thmrefs + 'and') |
|
257 |
; |
|
258 |
includes: 'includes' contextexpr |
|
259 |
; |
|
12967 | 260 |
\end{rail} |
12618 | 261 |
|
12976 | 262 |
\begin{descr} |
13411 | 263 |
|
264 |
\item [$\LOCALE~loc~=~import~+~body$] defines a new locale $loc$ as a context |
|
12976 | 265 |
consisting of a certain view of existing locales ($import$) plus some |
266 |
additional elements ($body$). Both $import$ and $body$ are optional; the |
|
13024 | 267 |
degenerate form $\LOCALE~loc$ defines an empty locale, which may still be |
268 |
useful to collect declarations of facts later on. Type-inference on locale |
|
12976 | 269 |
expressions automatically takes care of the most general typing that the |
270 |
combined context elements may acquire. |
|
13041 | 271 |
|
12976 | 272 |
The $import$ consists of a structured context expression, consisting of |
273 |
references to existing locales, renamed contexts, or merged contexts. |
|
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16010
diff
changeset
|
274 |
Renaming uses positional notation: $c~\vec x$ means that (a prefix of) the |
12976 | 275 |
fixed parameters of context $c$ are named according to $\vec x$; a |
16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16010
diff
changeset
|
276 |
``\texttt{_}'' (underscore) \indexisarthm{_@\texttt{_}} means to skip that |
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16010
diff
changeset
|
277 |
position. Renaming by default deletes existing syntax. Optionally, |
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16010
diff
changeset
|
278 |
new syntax may by specified with a mixfix annotation. Note that the |
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16010
diff
changeset
|
279 |
special syntax declared with ``$(structure)$'' (see below) is |
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16010
diff
changeset
|
280 |
neither deleted nor can it be changed. |
13041 | 281 |
Merging proceeds from left-to-right, suppressing any duplicates stemming |
282 |
from different paths through the import hierarchy. |
|
283 |
||
12976 | 284 |
The $body$ consists of basic context elements, further context expressions |
285 |
may be included as well. |
|
286 |
||
287 |
\begin{descr} |
|
13041 | 288 |
|
12976 | 289 |
\item [$\FIXES{~x::\tau~(mx)}$] declares a local parameter of type $\tau$ |
290 |
and mixfix annotation $mx$ (both are optional). The special syntax |
|
13027 | 291 |
declaration ``$(structure)$'' means that $x$ may be referenced |
292 |
implicitly in this context. |
|
13041 | 293 |
|
16168
adb83939177f
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16102
diff
changeset
|
294 |
\item [$\CONSTRAINS{~x::\tau}$] introduces a type constraint $\tau$ |
adb83939177f
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16102
diff
changeset
|
295 |
on the local parameter $x$. |
adb83939177f
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16102
diff
changeset
|
296 |
|
12976 | 297 |
\item [$\ASSUMES{a}{\vec\phi}$] introduces local premises, similar to |
298 |
$\ASSUMENAME$ within a proof (cf.\ \S\ref{sec:proof-context}). |
|
13041 | 299 |
|
12976 | 300 |
\item [$\DEFINES{a}{x \equiv t}$] defines a previously declared parameter. |
13041 | 301 |
This is close to $\DEFNAME$ within a proof (cf.\ |
12976 | 302 |
\S\ref{sec:proof-context}), but $\DEFINESNAME$ takes an equational |
13041 | 303 |
proposition instead of variable-term pair. The left-hand side of the |
304 |
equation may have additional arguments, e.g.\ ``$\DEFINES{}{f~\vec x |
|
305 |
\equiv t}$''. |
|
306 |
||
12976 | 307 |
\item [$\NOTES{a}{\vec b}$] reconsiders facts within a local context. Most |
308 |
notably, this may include arbitrary declarations in any attribute |
|
309 |
specifications included here, e.g.\ a local $simp$ rule. |
|
13041 | 310 |
|
12976 | 311 |
\item [$\INCLUDES{c}$] copies the specified context in a statically scoped |
15763
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
312 |
manner. Only available in the long goal format of \S\ref{sec:goals}. |
13041 | 313 |
|
12976 | 314 |
In contrast, the initial $import$ specification of a locale expression |
315 |
maintains a dynamic relation to the locales being referenced (benefiting |
|
316 |
from any later fact declarations in the obvious manner). |
|
317 |
\end{descr} |
|
13411 | 318 |
|
13041 | 319 |
Note that ``$\IS{p}$'' patterns given in the syntax of $\ASSUMESNAME$ and |
13411 | 320 |
$\DEFINESNAME$ above are illegal in locale definitions. In the long goal |
321 |
format of \S\ref{sec:goals}, term bindings may be included as expected, |
|
322 |
though. |
|
323 |
||
324 |
\medskip By default, locale specifications are ``closed up'' by turning the |
|
325 |
given text into a predicate definition $loc_axioms$ and deriving the |
|
326 |
original assumptions as local lemmas (modulo local definitions). The |
|
327 |
predicate statement covers only the newly specified assumptions, omitting |
|
328 |
the content of included locale expressions. The full cumulative view is |
|
329 |
only provided on export, involving another predicate $loc$ that refers to |
|
330 |
the complete specification text. |
|
331 |
||
332 |
In any case, the predicate arguments are those locale parameters that |
|
333 |
actually occur in the respective piece of text. Also note that these |
|
334 |
predicates operate at the meta-level in theory, but the locale packages |
|
335 |
attempts to internalize statements according to the object-logic setup |
|
336 |
(e.g.\ replacing $\Forall$ by $\forall$, and $\Imp$ by $\imp$ in HOL; see |
|
337 |
also \S\ref{sec:object-logic}). Separate introduction rules |
|
338 |
$loc_axioms.intro$ and $loc.intro$ are declared as well. |
|
339 |
||
340 |
The $(open)$ option of a locale specification prevents both the current |
|
341 |
$loc_axioms$ and cumulative $loc$ predicate constructions. Predicates are |
|
342 |
also omitted for empty specification texts. |
|
12976 | 343 |
|
344 |
\item [$\isarkeyword{print_locale}~import~+~body$] prints the specified locale |
|
345 |
expression in a flattened form. The notable special case |
|
346 |
$\isarkeyword{print_locale}~loc$ just prints the contents of the named |
|
347 |
locale, but keep in mind that type-inference will normalize type variables |
|
17228 | 348 |
according to the usual alphabetical order. The command omits |
349 |
$\isarkeyword{notes}$ elements by default. Use |
|
350 |
$\isarkeyword{print_locale}!$ to get them included. |
|
13041 | 351 |
|
12976 | 352 |
\item [$\isarkeyword{print_locales}$] prints the names of all locales of the |
353 |
current theory. |
|
354 |
||
20468
0bda06d731ee
Documented methods intro_locales and unfold_locales.
ballarin
parents:
20467
diff
changeset
|
355 |
\item [$intro_locales$ and $unfold_locales$] repeatedly expand |
0bda06d731ee
Documented methods intro_locales and unfold_locales.
ballarin
parents:
20467
diff
changeset
|
356 |
all introduction rules of locale predicates of the theory. While |
0bda06d731ee
Documented methods intro_locales and unfold_locales.
ballarin
parents:
20467
diff
changeset
|
357 |
$intro_locales$ only applies the $loc.intro$ introduction rules and |
0bda06d731ee
Documented methods intro_locales and unfold_locales.
ballarin
parents:
20467
diff
changeset
|
358 |
therefore does not decend to assumptions, $unfold_locales$ is more |
0bda06d731ee
Documented methods intro_locales and unfold_locales.
ballarin
parents:
20467
diff
changeset
|
359 |
aggressive and applies $loc_axioms.intro$ as well. Both methods are |
0bda06d731ee
Documented methods intro_locales and unfold_locales.
ballarin
parents:
20467
diff
changeset
|
360 |
aware of locale specifications entailed by the context, both from |
0bda06d731ee
Documented methods intro_locales and unfold_locales.
ballarin
parents:
20467
diff
changeset
|
361 |
target and $\isarkeyword{includes}$ statements, and from |
0bda06d731ee
Documented methods intro_locales and unfold_locales.
ballarin
parents:
20467
diff
changeset
|
362 |
interpretations (see below). New goals that are entailed by the |
0bda06d731ee
Documented methods intro_locales and unfold_locales.
ballarin
parents:
20467
diff
changeset
|
363 |
current context are discharged automatically. |
0bda06d731ee
Documented methods intro_locales and unfold_locales.
ballarin
parents:
20467
diff
changeset
|
364 |
|
12976 | 365 |
\end{descr} |
366 |
||
12621 | 367 |
|
15763
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
368 |
\subsubsection{Interpretation of locales} |
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
369 |
|
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
370 |
Locale expressions (more precisely, \emph{context expressions}) may be |
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
371 |
instantiated, and the instantiated facts added to the current context. |
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
372 |
This requires a proof of the instantiated specification and is called |
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
373 |
\emph{locale interpretation}. Interpretation is possible in theories |
21303 | 374 |
and locales (command $\isarcmd{interpretation}$) and also in proof |
375 |
contexts ($\isarcmd{interpret}$). |
|
15763
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
376 |
|
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
377 |
\indexisarcmd{interpretation}\indexisarcmd{interpret} |
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
378 |
\indexisarcmd{print-interps} |
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
379 |
\begin{matharray}{rcl} |
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
380 |
\isarcmd{interpretation} & : & \isartrans{theory}{proof(prove)} \\ |
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
381 |
\isarcmd{interpret} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\ |
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
382 |
\isarcmd{print_interps}^* & : & \isarkeep{theory~|~proof} \\ |
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
383 |
\end{matharray} |
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
384 |
|
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
385 |
\indexouternonterm{interp} |
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
386 |
|
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
387 |
\railalias{printinterps}{print\_interps} |
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
388 |
\railterm{printinterps} |
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
389 |
|
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
390 |
\begin{rail} |
23920 | 391 |
'interpretation' (interp | name ('<' | subseteq) contextexpr) |
15763
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
392 |
; |
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
393 |
'interpret' interp |
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
394 |
; |
17139
165c97f9bb63
Printing of interpretations: option to show witness theorems;
ballarin
parents:
17043
diff
changeset
|
395 |
printinterps '!'? name |
15763
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
396 |
; |
25094
ba43514068fd
Interpretation equations may have name and/or attribute.
ballarin
parents:
24991
diff
changeset
|
397 |
instantiation: ('[' (inst+) ']')? |
ba43514068fd
Interpretation equations may have name and/or attribute.
ballarin
parents:
24991
diff
changeset
|
398 |
; |
ba43514068fd
Interpretation equations may have name and/or attribute.
ballarin
parents:
24991
diff
changeset
|
399 |
interp: thmdecl? \\ (contextexpr instantiation | |
ba43514068fd
Interpretation equations may have name and/or attribute.
ballarin
parents:
24991
diff
changeset
|
400 |
name instantiation 'where' (thmdecl? prop + 'and')) |
15763
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
401 |
; |
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
402 |
\end{rail} |
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
403 |
|
17043 | 404 |
|
15763
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
405 |
\begin{descr} |
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
406 |
|
23920 | 407 |
\item [$\isarcmd{interpretation}~expr~insts~\isarkeyword{where}~eqns$] |
17043 | 408 |
|
23920 | 409 |
The first form of $\isarcmd{interpretation}$ interprets $expr$ in |
410 |
the theory. The instantiation is given as a list of terms $insts$ |
|
411 |
and is positional. All parameters must receive an instantiation |
|
412 |
term --- with the exception of defined parameters. These are, if |
|
413 |
omitted, derived from the defining equation and other |
|
414 |
instantiations. Use ``\_'' to omit an instantiation term. Free |
|
415 |
variables are automatically generalized. |
|
15763
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
416 |
|
17043 | 417 |
The command generates proof obligations for the instantiated |
418 |
specifications (assumes and defines elements). Once these are |
|
419 |
discharged by the user, instantiated facts are added to the theory in |
|
420 |
a post-processing phase. |
|
15763
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
421 |
|
23920 | 422 |
Additional equations, which are unfolded in facts during |
423 |
post-processing, may be given after the keyword |
|
424 |
$\isarkeyword{where}$. This is useful for interpreting concepts |
|
425 |
introduced through definition specification elements. The equations |
|
426 |
must be proved. Note that if equations are present, the context |
|
427 |
expression is restricted to a locale name. |
|
428 |
||
15763
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
429 |
The command is aware of interpretations already active in the |
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
430 |
theory. No proof obligations are generated for those, neither is |
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
431 |
post-processing applied to their facts. This avoids duplication of |
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
432 |
interpreted facts, in particular. Note that, in the case of a |
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
433 |
locale with import, parts of the interpretation may already be |
23920 | 434 |
active. The command will only generate proof obligations and process |
15763
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
435 |
facts for new parts. |
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
436 |
|
17043 | 437 |
The context expression may be preceded by a name and/or attributes. |
438 |
These take effect in the post-processing of facts. The name is used |
|
439 |
to prefix fact names, for example to avoid accidental hiding of |
|
440 |
other facts. Attributes are applied after attributes of the |
|
441 |
interpreted facts. |
|
442 |
||
15763
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
443 |
Adding facts to locales has the |
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
444 |
effect of adding interpreted facts to the theory for all active |
17043 | 445 |
interpretations also. That is, interpretations dynamically |
446 |
participate in any facts added to locales. |
|
447 |
||
448 |
\item [$\isarcmd{interpretation}~name~\subseteq~expr$] |
|
449 |
||
450 |
This form of the command interprets $expr$ in the locale $name$. It |
|
451 |
requires a proof that the specification of $name$ implies the |
|
452 |
specification of $expr$. As in the localized version of the theorem |
|
453 |
command, the proof is in the context of $name$. After the proof |
|
454 |
obligation has been dischared, the facts of $expr$ |
|
455 |
become part of locale $name$ as \emph{derived} context elements and |
|
456 |
are available when the context $name$ is subsequently entered. |
|
457 |
Note that, like import, this is dynamic: facts added to a locale |
|
17139
165c97f9bb63
Printing of interpretations: option to show witness theorems;
ballarin
parents:
17043
diff
changeset
|
458 |
part of $expr$ after interpretation become also available in |
17043 | 459 |
$name$. Like facts |
460 |
of renamed context elements, facts obtained by interpretation may be |
|
461 |
accessed by prefixing with the parameter renaming (where the parameters |
|
462 |
are separated by `\_'). |
|
463 |
||
464 |
Unlike interpretation in theories, instantiation is confined to the |
|
465 |
renaming of parameters, which may be specified as part of the context |
|
466 |
expression $expr$. Using defined parameters in $name$ one may |
|
467 |
achieve an effect similar to instantiation, though. |
|
468 |
||
469 |
Only specification fragments of $expr$ that are not already part of |
|
470 |
$name$ (be it imported, derived or a derived fragment of the import) |
|
471 |
are considered by interpretation. This enables circular |
|
472 |
interpretations. |
|
473 |
||
17139
165c97f9bb63
Printing of interpretations: option to show witness theorems;
ballarin
parents:
17043
diff
changeset
|
474 |
If interpretations of $name$ exist in the current theory, the |
165c97f9bb63
Printing of interpretations: option to show witness theorems;
ballarin
parents:
17043
diff
changeset
|
475 |
command adds interpretations for $expr$ as well, with the same |
165c97f9bb63
Printing of interpretations: option to show witness theorems;
ballarin
parents:
17043
diff
changeset
|
476 |
prefix and attributes, although only for fragments of $expr$ that |
165c97f9bb63
Printing of interpretations: option to show witness theorems;
ballarin
parents:
17043
diff
changeset
|
477 |
are not interpreted in the theory already. |
165c97f9bb63
Printing of interpretations: option to show witness theorems;
ballarin
parents:
17043
diff
changeset
|
478 |
|
23920 | 479 |
\item [$\isarcmd{interpret}~expr~insts~\isarkeyword{where}~eqns$] |
15763
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
480 |
interprets $expr$ in the proof context and is otherwise similar to |
17043 | 481 |
interpretation in theories. Free variables in instantiations are not |
15763
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
482 |
generalized, however. |
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
483 |
|
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
484 |
\item [$\isarcmd{print_interps}~loc$] |
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
485 |
prints the interpretations of a particular locale $loc$ that are |
17139
165c97f9bb63
Printing of interpretations: option to show witness theorems;
ballarin
parents:
17043
diff
changeset
|
486 |
active in the current context, either theory or proof context. The |
19145 | 487 |
exclamation point argument triggers printing of |
17139
165c97f9bb63
Printing of interpretations: option to show witness theorems;
ballarin
parents:
17043
diff
changeset
|
488 |
\emph{witness} theorems justifying interpretations. These are |
165c97f9bb63
Printing of interpretations: option to show witness theorems;
ballarin
parents:
17043
diff
changeset
|
489 |
normally omitted from the output. |
165c97f9bb63
Printing of interpretations: option to show witness theorems;
ballarin
parents:
17043
diff
changeset
|
490 |
|
15763
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
491 |
|
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
492 |
\end{descr} |
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
493 |
|
15837 | 494 |
\begin{warn} |
495 |
Since attributes are applied to interpreted theorems, interpretation |
|
21303 | 496 |
may modify the context of common proof tools, e.g.\ the Simplifier |
497 |
or Classical Reasoner. Since the behavior of such automated |
|
498 |
reasoning tools is \emph{not} stable under interpretation morphisms, |
|
499 |
manual declarations might have to be issued. |
|
15837 | 500 |
\end{warn} |
501 |
||
16168
adb83939177f
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16102
diff
changeset
|
502 |
\begin{warn} |
17043 | 503 |
An interpretation in a theory may subsume previous interpretations. |
504 |
This happens if the same specification fragment is interpreted twice |
|
505 |
and the instantiation of the second interpretation is more general |
|
21303 | 506 |
than the interpretation of the first. A warning is issued, since it |
507 |
is likely that these could have been generalized in the first place. |
|
508 |
The locale package does not attempt to remove subsumed |
|
509 |
interpretations. |
|
16168
adb83939177f
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16102
diff
changeset
|
510 |
\end{warn} |
adb83939177f
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
16102
diff
changeset
|
511 |
|
15763
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
14605
diff
changeset
|
512 |
|
21303 | 513 |
\subsection{Type classes}\label{sec:class} |
20379 | 514 |
|
21303 | 515 |
A type class is a special case of a locale, with some additional |
516 |
infrastructure (notably a link to type-inference). Type classes |
|
517 |
consist of a locale with \emph{exactly one} type variable and an |
|
518 |
corresponding axclass. \cite{isabelle-classes} gives a substantial |
|
21076 | 519 |
introduction on type classes. |
20379 | 520 |
|
20467 | 521 |
\indexisarcmd{instance}\indexisarcmd{class}\indexisarcmd{print-classes} |
20379 | 522 |
\begin{matharray}{rcl} |
523 |
\isarcmd{class} & : & \isartrans{theory}{local{\dsh}theory} \\ |
|
24991 | 524 |
\isarcmd{subclass} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\ |
20379 | 525 |
\isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\ |
526 |
\isarcmd{print_classes}^* & : & \isarkeep{theory~|~proof} \\ |
|
527 |
\end{matharray} |
|
528 |
||
529 |
\begin{rail} |
|
24991 | 530 |
'class' name '=' ((superclassexpr '+' (contextelem+)) | superclassexpr | (contextelem+)) 'begin'? |
20379 | 531 |
; |
24991 | 532 |
'subclass' target? nameref |
533 |
; |
|
534 |
'instance' (nameref '::' arity + 'and') (axmdecl prop +)? |
|
20379 | 535 |
; |
536 |
'print\_classes' |
|
537 |
; |
|
538 |
||
539 |
superclassexpr: nameref | (nameref '+' superclassexpr) |
|
540 |
; |
|
541 |
\end{rail} |
|
542 |
||
543 |
\begin{descr} |
|
544 |
||
545 |
\item [$\CLASS~c = superclasses~+~body$] defines a new class $c$, |
|
546 |
inheriting from $superclasses$. Simultaneously, a locale |
|
20467 | 547 |
named $c$ is introduced, inheriting from the locales |
20379 | 548 |
corresponding to $superclasses$; also, an axclass |
549 |
named $c$, inheriting from the axclasses corresponding to |
|
550 |
$superclasses$. $\FIXESNAME$ in $body$ are lifted |
|
551 |
to the theory toplevel, constraining |
|
552 |
the free type variable to sort $c$ and stripping local syntax. |
|
553 |
$\ASSUMESNAME$ in $body$ are also lifted, |
|
554 |
constraining |
|
555 |
the free type variable to sort $c$. |
|
556 |
||
24991 | 557 |
\item [$\INSTANCE~~t :: (\vec s)s \vec{defs}$] |
20379 | 558 |
sets up a goal stating type arities. The proof would usually |
559 |
proceed by $intro_classes$, and then establish the characteristic theorems |
|
560 |
of the type classes involved. |
|
561 |
The $defs$, if given, must correspond to the class parameters |
|
24991 | 562 |
involved in the $arities$ and are introduced in the theory |
22294 | 563 |
before proof. |
20379 | 564 |
After finishing the proof, the theory will be |
565 |
augmented by a type signature declaration corresponding to the |
|
566 |
resulting theorems. |
|
22294 | 567 |
This $\isarcmd{instance}$ command is actually an extension |
568 |
of primitive axclass $\isarcmd{instance}$ (see \ref{sec:axclass}). |
|
20379 | 569 |
|
24991 | 570 |
\item [$\SUBCLASS~c$] in a class context for class $d$ |
571 |
sets up a goal stating that class $c$ is logically |
|
572 |
contained in class $d$. After finishing the proof, class $d$ is proven |
|
573 |
to be subclass $c$ and the locale $c$ is interpreted into $d$ simultaneously. |
|
20379 | 574 |
|
22294 | 575 |
\item [$\isarkeyword{print_classes}$] prints all classes |
20467 | 576 |
in the current theory. |
20379 | 577 |
|
578 |
\end{descr} |
|
579 |
||
580 |
||
20492 | 581 |
\subsection{Axiomatic type classes}\label{sec:axclass} |
582 |
||
583 |
\indexisarcmd{axclass}\indexisarmeth{intro-classes} |
|
584 |
\begin{matharray}{rcl} |
|
585 |
\isarcmd{axclass} & : & \isartrans{theory}{theory} \\ |
|
586 |
\isarcmd{instance} & : & \isartrans{theory}{proof(prove)} \\ |
|
587 |
intro_classes & : & \isarmeth \\ |
|
588 |
\end{matharray} |
|
589 |
||
590 |
Axiomatic type classes are provided by Isabelle/Pure as a \emph{definitional} |
|
591 |
interface to type classes (cf.~\S\ref{sec:classes}). Thus any object logic |
|
592 |
may make use of this light-weight mechanism of abstract theories |
|
593 |
\cite{Wenzel:1997:TPHOL}. There is also a tutorial on using axiomatic type |
|
594 |
classes in Isabelle \cite{isabelle-axclass} that is part of the standard |
|
595 |
Isabelle documentation. |
|
596 |
||
597 |
\begin{rail} |
|
598 |
'axclass' classdecl (axmdecl prop +) |
|
599 |
; |
|
600 |
'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity) |
|
601 |
; |
|
602 |
\end{rail} |
|
603 |
||
604 |
\begin{descr} |
|
605 |
||
606 |
\item [$\AXCLASS~c \subseteq \vec c~~axms$] defines an axiomatic type class as |
|
607 |
the intersection of existing classes, with additional axioms holding. Class |
|
608 |
axioms may not contain more than one type variable. The class axioms (with |
|
609 |
implicit sort constraints added) are bound to the given names. Furthermore |
|
610 |
a class introduction rule is generated (being bound as |
|
611 |
$c_class{\dtt}intro$); this rule is employed by method $intro_classes$ to |
|
612 |
support instantiation proofs of this class. |
|
613 |
||
614 |
The ``axioms'' are stored as theorems according to the given name |
|
615 |
specifications, adding the class name $c$ as name space prefix; the same |
|
616 |
facts are also stored collectively as $c_class{\dtt}axioms$. |
|
617 |
||
618 |
\item [$\INSTANCE~c@1 \subseteq c@2$ and $\INSTANCE~t :: (\vec s)s$] setup a |
|
619 |
goal stating a class relation or type arity. The proof would usually |
|
620 |
proceed by $intro_classes$, and then establish the characteristic theorems |
|
621 |
of the type classes involved. After finishing the proof, the theory will be |
|
622 |
augmented by a type signature declaration corresponding to the resulting |
|
623 |
theorem. |
|
624 |
||
625 |
\item [$intro_classes$] repeatedly expands all class introduction rules of |
|
626 |
this theory. Note that this method usually needs not be named explicitly, |
|
627 |
as it is already included in the default proof step (of $\PROOFNAME$ etc.). |
|
628 |
In particular, instantiation of trivial (syntactic) classes may be performed |
|
629 |
by a single ``$\DDOT$'' proof step. |
|
630 |
||
631 |
\end{descr} |
|
632 |
||
633 |
||
24085 | 634 |
\subsection{Configuration options} |
635 |
||
24110
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24085
diff
changeset
|
636 |
Isabelle/Pure maintains a record of named configuration options within the |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24085
diff
changeset
|
637 |
theory or proof context, with values of type $bool$, $int$, or $string$. |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24085
diff
changeset
|
638 |
Tools may declare options in ML, and then refer to these values (relative to |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24085
diff
changeset
|
639 |
the context). Thus global reference variables are easily avoided. The user |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24085
diff
changeset
|
640 |
may change the value of a configuration option by means of an associated |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24085
diff
changeset
|
641 |
attribute of the same name. This form of context declaration works |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24085
diff
changeset
|
642 |
particularly well with commands such as $\isarkeyword{declare}$ or |
24085 | 643 |
$\isarkeyword{using}$. |
644 |
||
645 |
For historical reasons, some tools cannot take the full proof context |
|
646 |
into account and merely refer to the background theory. This is |
|
647 |
accommodated by configuration options being declared as ``global'', |
|
648 |
which may not be changed within a local context. |
|
649 |
||
24110
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24085
diff
changeset
|
650 |
\indexisarcmd{print-configs} |
24085 | 651 |
\begin{matharray}{rcll} |
24110
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24085
diff
changeset
|
652 |
\isarcmd{print_configs} & : & \isarkeep{theory~|~proof} \\ |
24085 | 653 |
\end{matharray} |
654 |
||
655 |
\begin{rail} |
|
24110
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24085
diff
changeset
|
656 |
name ('=' ('true' | 'false' | int | name))? |
24085 | 657 |
\end{rail} |
658 |
||
659 |
\begin{descr} |
|
24110
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24085
diff
changeset
|
660 |
|
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24085
diff
changeset
|
661 |
\item [$\isarkeyword{print_configs}$] prints the available configuration |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24085
diff
changeset
|
662 |
options, with names, types, and current values. |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24085
diff
changeset
|
663 |
|
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24085
diff
changeset
|
664 |
\item [$name = value$] as an attribute expression modifies the named option, |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24085
diff
changeset
|
665 |
with the syntax of the value depending on the option's type. For $bool$ the |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24085
diff
changeset
|
666 |
default value is $true$. Any attempt to change a global option in a local |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24085
diff
changeset
|
667 |
context is ignored. |
24085 | 668 |
|
669 |
\end{descr} |
|
670 |
||
20492 | 671 |
|
12621 | 672 |
\section{Derived proof schemes} |
673 |
||
674 |
\subsection{Generalized elimination}\label{sec:obtain} |
|
675 |
||
17864 | 676 |
\indexisarcmd{obtain}\indexisarcmd{guess} |
12621 | 677 |
\begin{matharray}{rcl} |
678 |
\isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\ |
|
17864 | 679 |
\isarcmd{guess}^* & : & \isartrans{proof(state)}{proof(prove)} \\ |
12621 | 680 |
\end{matharray} |
681 |
||
682 |
Generalized elimination means that additional elements with certain properties |
|
13041 | 683 |
may be introduced in the current context, by virtue of a locally proven |
12621 | 684 |
``soundness statement''. Technically speaking, the $\OBTAINNAME$ language |
685 |
element is like a declaration of $\FIXNAME$ and $\ASSUMENAME$ (see also see |
|
686 |
\S\ref{sec:proof-context}), together with a soundness proof of its additional |
|
687 |
claim. According to the nature of existential reasoning, assumptions get |
|
688 |
eliminated from any result exported from the context later, provided that the |
|
689 |
corresponding parameters do \emph{not} occur in the conclusion. |
|
690 |
||
691 |
\begin{rail} |
|
18903 | 692 |
'obtain' parname? (vars + 'and') 'where' (props + 'and') |
12621 | 693 |
; |
17864 | 694 |
'guess' (vars + 'and') |
695 |
; |
|
12621 | 696 |
\end{rail} |
12618 | 697 |
|
12621 | 698 |
$\OBTAINNAME$ is defined as a derived Isar command as follows, where $\vec b$ |
699 |
shall refer to (optional) facts indicated for forward chaining. |
|
700 |
\begin{matharray}{l} |
|
701 |
\langle facts~\vec b\rangle \\ |
|
702 |
\OBTAIN{\vec x}{a}{\vec \phi}~~\langle proof\rangle \equiv {} \\[1ex] |
|
13041 | 703 |
\quad \HAVE{}{\All{thesis} (\All{\vec x} \vec\phi \Imp thesis) \Imp thesis} \\ |
704 |
\quad \PROOF{succeed} \\ |
|
12621 | 705 |
\qquad \FIX{thesis} \\ |
13041 | 706 |
\qquad \ASSUME{that~[intro?]}{\All{\vec x} \vec\phi \Imp thesis} \\ |
13042 | 707 |
\qquad \THUS{}{thesis} \\ |
708 |
\quad\qquad \APPLY{-} \\ |
|
13041 | 709 |
\quad\qquad \USING{\vec b}~~\langle proof\rangle \\ |
710 |
\quad \QED{} \\ |
|
12621 | 711 |
\quad \FIX{\vec x}~\ASSUMENAME^\ast~a\colon~\vec\phi \\ |
712 |
\end{matharray} |
|
713 |
||
714 |
Typically, the soundness proof is relatively straight-forward, often just by |
|
13048 | 715 |
canonical automated tools such as ``$\BY{simp}$'' or ``$\BY{blast}$''. |
716 |
Accordingly, the ``$that$'' reduction above is declared as simplification and |
|
717 |
introduction rule. |
|
12621 | 718 |
|
719 |
In a sense, $\OBTAINNAME$ represents at the level of Isar proofs what would be |
|
720 |
meta-logical existential quantifiers and conjunctions. This concept has a |
|
13041 | 721 |
broad range of useful applications, ranging from plain elimination (or |
17864 | 722 |
introduction) of object-level existential and conjunctions, to elimination |
12621 | 723 |
over results of symbolic evaluation of recursive definitions, for example. |
724 |
Also note that $\OBTAINNAME$ without parameters acts much like $\HAVENAME$, |
|
13041 | 725 |
where the result is treated as a genuine assumption. |
12621 | 726 |
|
18903 | 727 |
An alternative name to be used instead of ``$that$'' above may be |
728 |
given in parentheses. |
|
729 |
||
17864 | 730 |
\medskip |
731 |
||
732 |
The improper variant $\isarkeyword{guess}$ is similar to $\OBTAINNAME$, but |
|
733 |
derives the obtained statement from the course of reasoning! The proof starts |
|
734 |
with a fixed goal $thesis$. The subsequent proof may refine this to anything |
|
735 |
of the form like $\All{\vec x} \vec\phi \Imp thesis$, but must not introduce |
|
736 |
new subgoals. The final goal state is then used as reduction rule for the |
|
737 |
obtain scheme described above. Obtained parameters $\vec x$ are marked as |
|
738 |
internal by default, which prevents the proof context from being polluted by |
|
739 |
ad-hoc variables. The variable names and type constraints given as arguments |
|
740 |
for $\isarkeyword{guess}$ specify a prefix of obtained parameters explicitly |
|
741 |
in the text. |
|
742 |
||
743 |
It is important to note that the facts introduced by $\OBTAINNAME$ and |
|
744 |
$\isarkeyword{guess}$ may not be polymorphic: any type-variables occurring |
|
745 |
here are fixed in the present context! |
|
746 |
||
12621 | 747 |
|
748 |
\subsection{Calculational reasoning}\label{sec:calculation} |
|
7315 | 749 |
|
8619 | 750 |
\indexisarcmd{also}\indexisarcmd{finally} |
751 |
\indexisarcmd{moreover}\indexisarcmd{ultimately} |
|
12976 | 752 |
\indexisarcmd{print-trans-rules} |
753 |
\indexisaratt{trans}\indexisaratt{sym}\indexisaratt{symmetric} |
|
7315 | 754 |
\begin{matharray}{rcl} |
755 |
\isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\ |
|
756 |
\isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\ |
|
8619 | 757 |
\isarcmd{moreover} & : & \isartrans{proof(state)}{proof(state)} \\ |
758 |
\isarcmd{ultimately} & : & \isartrans{proof(state)}{proof(chain)} \\ |
|
10154 | 759 |
\isarcmd{print_trans_rules}^* & : & \isarkeep{theory~|~proof} \\ |
7315 | 760 |
trans & : & \isaratt \\ |
12976 | 761 |
sym & : & \isaratt \\ |
762 |
symmetric & : & \isaratt \\ |
|
7315 | 763 |
\end{matharray} |
764 |
||
765 |
Calculational proof is forward reasoning with implicit application of |
|
11332 | 766 |
transitivity rules (such those of $=$, $\leq$, $<$). Isabelle/Isar maintains |
7391 | 767 |
an auxiliary register $calculation$\indexisarthm{calculation} for accumulating |
7897 | 768 |
results obtained by transitivity composed with the current result. Command |
769 |
$\ALSO$ updates $calculation$ involving $this$, while $\FINALLY$ exhibits the |
|
770 |
final $calculation$ by forward chaining towards the next goal statement. Both |
|
771 |
commands require valid current facts, i.e.\ may occur only after commands that |
|
772 |
produce theorems such as $\ASSUMENAME$, $\NOTENAME$, or some finished proof of |
|
8619 | 773 |
$\HAVENAME$, $\SHOWNAME$ etc. The $\MOREOVER$ and $\ULTIMATELY$ commands are |
774 |
similar to $\ALSO$ and $\FINALLY$, but only collect further results in |
|
775 |
$calculation$ without applying any rules yet. |
|
7315 | 776 |
|
13041 | 777 |
Also note that the implicit term abbreviation ``$\dots$'' has its canonical |
778 |
application with calculational proofs. It refers to the argument of the |
|
779 |
preceding statement. (The argument of a curried infix expression happens to be |
|
780 |
its right-hand side.) |
|
7315 | 781 |
|
782 |
Isabelle/Isar calculations are implicitly subject to block structure in the |
|
783 |
sense that new threads of calculational reasoning are commenced for any new |
|
784 |
block (as opened by a local goal, for example). This means that, apart from |
|
785 |
being able to nest calculations, there is no separate \emph{begin-calculation} |
|
786 |
command required. |
|
787 |
||
8619 | 788 |
\medskip |
789 |
||
13041 | 790 |
The Isar calculation proof commands may be defined as follows:\footnote{We |
791 |
suppress internal bookkeeping such as proper handling of block-structure.} |
|
8619 | 792 |
\begin{matharray}{rcl} |
793 |
\ALSO@0 & \equiv & \NOTE{calculation}{this} \\ |
|
9606 | 794 |
\ALSO@{n+1} & \equiv & \NOTE{calculation}{trans~[OF~calculation~this]} \\[0.5ex] |
8619 | 795 |
\FINALLY & \equiv & \ALSO~\FROM{calculation} \\ |
796 |
\MOREOVER & \equiv & \NOTE{calculation}{calculation~this} \\ |
|
797 |
\ULTIMATELY & \equiv & \MOREOVER~\FROM{calculation} \\ |
|
798 |
\end{matharray} |
|
799 |
||
7315 | 800 |
\begin{rail} |
13024 | 801 |
('also' | 'finally') ('(' thmrefs ')')? |
8619 | 802 |
; |
8507 | 803 |
'trans' (() | 'add' | 'del') |
7315 | 804 |
; |
805 |
\end{rail} |
|
806 |
||
807 |
\begin{descr} |
|
13041 | 808 |
|
8547 | 809 |
\item [$\ALSO~(\vec a)$] maintains the auxiliary $calculation$ register as |
7315 | 810 |
follows. The first occurrence of $\ALSO$ in some calculational thread |
7905 | 811 |
initializes $calculation$ by $this$. Any subsequent $\ALSO$ on the same |
7335 | 812 |
level of block-structure updates $calculation$ by some transitivity rule |
7458 | 813 |
applied to $calculation$ and $this$ (in that order). Transitivity rules are |
11095 | 814 |
picked from the current context, unless alternative rules are given as |
815 |
explicit arguments. |
|
9614 | 816 |
|
8547 | 817 |
\item [$\FINALLY~(\vec a)$] maintaining $calculation$ in the same way as |
7315 | 818 |
$\ALSO$, and concludes the current calculational thread. The final result |
819 |
is exhibited as fact for forward chaining towards the next goal. Basically, |
|
7987 | 820 |
$\FINALLY$ just abbreviates $\ALSO~\FROM{calculation}$. Note that |
821 |
``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and |
|
822 |
``$\FINALLY~\HAVE{}{\phi}~\DOT$'' are typical idioms for concluding |
|
823 |
calculational proofs. |
|
9614 | 824 |
|
8619 | 825 |
\item [$\MOREOVER$ and $\ULTIMATELY$] are analogous to $\ALSO$ and $\FINALLY$, |
826 |
but collect results only, without applying rules. |
|
13041 | 827 |
|
13024 | 828 |
\item [$\isarkeyword{print_trans_rules}$] prints the list of transitivity |
829 |
rules (for calculational commands $\ALSO$ and $\FINALLY$) and symmetry rules |
|
830 |
(for the $symmetric$ operation and single step elimination patters) of the |
|
831 |
current context. |
|
13041 | 832 |
|
8547 | 833 |
\item [$trans$] declares theorems as transitivity rules. |
13041 | 834 |
|
13024 | 835 |
\item [$sym$] declares symmetry rules. |
13041 | 836 |
|
12976 | 837 |
\item [$symmetric$] resolves a theorem with some rule declared as $sym$ in the |
838 |
current context. For example, ``$\ASSUME{[symmetric]}{x = y}$'' produces a |
|
839 |
swapped fact derived from that assumption. |
|
13041 | 840 |
|
13024 | 841 |
In structured proof texts it is often more appropriate to use an explicit |
842 |
single-step elimination proof, such as ``$\ASSUME{}{x = y}~\HENCE{}{y = |
|
13041 | 843 |
x}~\DDOT$''. The very same rules known to $symmetric$ are declared as |
844 |
$elim?$ as well. |
|
13027 | 845 |
|
7315 | 846 |
\end{descr} |
847 |
||
848 |
||
13041 | 849 |
\section{Proof tools} |
8517 | 850 |
|
12618 | 851 |
\subsection{Miscellaneous methods and attributes}\label{sec:misc-meth-att} |
8517 | 852 |
|
9606 | 853 |
\indexisarmeth{unfold}\indexisarmeth{fold}\indexisarmeth{insert} |
8517 | 854 |
\indexisarmeth{erule}\indexisarmeth{drule}\indexisarmeth{frule} |
855 |
\indexisarmeth{fail}\indexisarmeth{succeed} |
|
856 |
\begin{matharray}{rcl} |
|
857 |
unfold & : & \isarmeth \\ |
|
10741 | 858 |
fold & : & \isarmeth \\ |
859 |
insert & : & \isarmeth \\[0.5ex] |
|
8517 | 860 |
erule^* & : & \isarmeth \\ |
861 |
drule^* & : & \isarmeth \\ |
|
13024 | 862 |
frule^* & : & \isarmeth \\ |
8517 | 863 |
succeed & : & \isarmeth \\ |
864 |
fail & : & \isarmeth \\ |
|
865 |
\end{matharray} |
|
7135 | 866 |
|
867 |
\begin{rail} |
|
10741 | 868 |
('fold' | 'unfold' | 'insert') thmrefs |
869 |
; |
|
870 |
('erule' | 'drule' | 'frule') ('('nat')')? thmrefs |
|
7135 | 871 |
; |
872 |
\end{rail} |
|
873 |
||
7167 | 874 |
\begin{descr} |
19379 | 875 |
|
876 |
\item [$unfold~\vec a$ and $fold~\vec a$] expand (or fold back again) |
|
877 |
the given definitions throughout all goals; any chained facts |
|
878 |
provided are inserted into the goal and subject to rewriting as |
|
879 |
well. |
|
13041 | 880 |
|
10741 | 881 |
\item [$insert~\vec a$] inserts theorems as facts into all goals of the proof |
882 |
state. Note that current facts indicated for forward chaining are ignored. |
|
13024 | 883 |
|
8547 | 884 |
\item [$erule~\vec a$, $drule~\vec a$, and $frule~\vec a$] are similar to the |
885 |
basic $rule$ method (see \S\ref{sec:pure-meth-att}), but apply rules by |
|
8517 | 886 |
elim-resolution, destruct-resolution, and forward-resolution, respectively |
10741 | 887 |
\cite{isabelle-ref}. The optional natural number argument (default $0$) |
13041 | 888 |
specifies additional assumption steps to be performed here. |
889 |
||
10741 | 890 |
Note that these methods are improper ones, mainly serving for |
891 |
experimentation and tactic script emulation. Different modes of basic rule |
|
892 |
application are usually expressed in Isar at the proof language level, |
|
893 |
rather than via implicit proof state manipulations. For example, a proper |
|
13041 | 894 |
single-step elimination would be done using the plain $rule$ method, with |
10741 | 895 |
forward chaining of current facts. |
13024 | 896 |
|
8517 | 897 |
\item [$succeed$] yields a single (unchanged) result; it is the identity of |
898 |
the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}). |
|
13024 | 899 |
|
8517 | 900 |
\item [$fail$] yields an empty result sequence; it is the identity of the |
901 |
``\texttt{|}'' method combinator (cf.\ \S\ref{sec:syn-meth}). |
|
13024 | 902 |
|
7167 | 903 |
\end{descr} |
7135 | 904 |
|
10318 | 905 |
\indexisaratt{tagged}\indexisaratt{untagged} |
9614 | 906 |
\indexisaratt{THEN}\indexisaratt{COMP} |
14175
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13622
diff
changeset
|
907 |
\indexisaratt{unfolded}\indexisaratt{folded} |
13027 | 908 |
\indexisaratt{standard}\indexisarattof{Pure}{elim-format} |
13024 | 909 |
\indexisaratt{no-vars} |
8517 | 910 |
\begin{matharray}{rcl} |
9905 | 911 |
tagged & : & \isaratt \\ |
912 |
untagged & : & \isaratt \\[0.5ex] |
|
9614 | 913 |
THEN & : & \isaratt \\ |
8517 | 914 |
COMP & : & \isaratt \\[0.5ex] |
9905 | 915 |
unfolded & : & \isaratt \\ |
916 |
folded & : & \isaratt \\[0.5ex] |
|
24429 | 917 |
rotated & : & \isaratt \\ |
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9936
diff
changeset
|
918 |
elim_format & : & \isaratt \\ |
13041 | 919 |
standard^* & : & \isaratt \\ |
9936 | 920 |
no_vars^* & : & \isaratt \\ |
8517 | 921 |
\end{matharray} |
922 |
||
923 |
\begin{rail} |
|
23654 | 924 |
'tagged' nameref |
8517 | 925 |
; |
9905 | 926 |
'untagged' name |
8517 | 927 |
; |
10154 | 928 |
('THEN' | 'COMP') ('[' nat ']')? thmref |
8517 | 929 |
; |
9905 | 930 |
('unfolded' | 'folded') thmrefs |
8517 | 931 |
; |
24429 | 932 |
'rotated' ( int )? |
8517 | 933 |
\end{rail} |
934 |
||
935 |
\begin{descr} |
|
13041 | 936 |
|
23654 | 937 |
\item [$tagged~name~arg$ and $untagged~name$] add and remove $tags$ of some |
8517 | 938 |
theorem. Tags may be any list of strings that serve as comment for some |
939 |
tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the |
|
23654 | 940 |
result). The first string is considered the tag name, the second its |
941 |
argument. Note that $untagged$ removes any tags of the same name. |
|
13041 | 942 |
|
943 |
\item [$THEN~a$ and $COMP~a$] compose rules by resolution. $THEN$ resolves |
|
944 |
with the first premise of $a$ (an alternative position may be also |
|
945 |
specified); the $COMP$ version skips the automatic lifting process that is |
|
946 |
normally intended (cf.\ \texttt{RS} and \texttt{COMP} in |
|
8547 | 947 |
\cite[\S5]{isabelle-ref}). |
19379 | 948 |
|
949 |
\item [$unfolded~\vec a$ and $folded~\vec a$] expand and fold back |
|
950 |
again the given definitions throughout a rule. |
|
13041 | 951 |
|
24429 | 952 |
\item [$rotated~n$] rotate the premises of a theorem by $n$ (default 1). |
953 |
||
13027 | 954 |
\item [$elim_format$] turns a destruction rule into elimination rule format, |
955 |
by resolving with the rule $\PROP A \Imp (\PROP A \Imp \PROP B) \Imp \PROP |
|
956 |
B$. |
|
13048 | 957 |
|
958 |
Note that the Classical Reasoner (\S\ref{sec:classical}) provides its own |
|
959 |
version of this operation. |
|
13041 | 960 |
|
961 |
\item [$standard$] puts a theorem into the standard form of object-rules at |
|
962 |
the outermost theory level. Note that this operation violates the local |
|
963 |
proof context (including active locales). |
|
964 |
||
9232 | 965 |
\item [$no_vars$] replaces schematic variables by free ones; this is mainly |
966 |
for tuning output of pretty printed theorems. |
|
13027 | 967 |
|
8517 | 968 |
\end{descr} |
7135 | 969 |
|
970 |
||
12621 | 971 |
\subsection{Further tactic emulations}\label{sec:tactics} |
9606 | 972 |
|
973 |
The following improper proof methods emulate traditional tactics. These admit |
|
974 |
direct access to the goal state, which is normally considered harmful! In |
|
975 |
particular, this may involve both numbered goal addressing (default 1), and |
|
976 |
dynamic instantiation within the scope of some subgoal. |
|
977 |
||
978 |
\begin{warn} |
|
14175
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13622
diff
changeset
|
979 |
Dynamic instantiations refer to universally quantified parameters of |
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13622
diff
changeset
|
980 |
a subgoal (the dynamic context) rather than fixed variables and term |
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13622
diff
changeset
|
981 |
abbreviations of a (static) Isar context. |
9606 | 982 |
\end{warn} |
983 |
||
14175
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13622
diff
changeset
|
984 |
Tactic emulation methods, unlike their ML counterparts, admit |
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13622
diff
changeset
|
985 |
simultaneous instantiation from both dynamic and static contexts. If |
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13622
diff
changeset
|
986 |
names occur in both contexts goal parameters hide locally fixed |
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13622
diff
changeset
|
987 |
variables. Likewise, schematic variables refer to term abbreviations, |
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13622
diff
changeset
|
988 |
if present in the static context. Otherwise the schematic variable is |
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13622
diff
changeset
|
989 |
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
|
990 |
with certain parts of the subgoal. |
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13622
diff
changeset
|
991 |
|
9606 | 992 |
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
|
993 |
named $foo_tac$. Note also that variable names occurring on left hand sides |
14212 | 994 |
of instantiations must be preceded by a question mark if they coincide with |
995 |
a keyword or contain dots. |
|
14175
dbd16ebaf907
Method rule_tac understands Isar contexts: documentation.
ballarin
parents:
13622
diff
changeset
|
996 |
This is consistent with the attribute $where$ (see \S\ref{sec:pure-meth-att}). |
9606 | 997 |
|
998 |
\indexisarmeth{rule-tac}\indexisarmeth{erule-tac} |
|
999 |
\indexisarmeth{drule-tac}\indexisarmeth{frule-tac} |
|
1000 |
\indexisarmeth{cut-tac}\indexisarmeth{thin-tac} |
|
9642 | 1001 |
\indexisarmeth{subgoal-tac}\indexisarmeth{rename-tac} |
9614 | 1002 |
\indexisarmeth{rotate-tac}\indexisarmeth{tactic} |
9606 | 1003 |
\begin{matharray}{rcl} |
1004 |
rule_tac^* & : & \isarmeth \\ |
|
1005 |
erule_tac^* & : & \isarmeth \\ |
|
1006 |
drule_tac^* & : & \isarmeth \\ |
|
1007 |
frule_tac^* & : & \isarmeth \\ |
|
1008 |
cut_tac^* & : & \isarmeth \\ |
|
1009 |
thin_tac^* & : & \isarmeth \\ |
|
1010 |
subgoal_tac^* & : & \isarmeth \\ |
|
9614 | 1011 |
rename_tac^* & : & \isarmeth \\ |
1012 |
rotate_tac^* & : & \isarmeth \\ |
|
9606 | 1013 |
tactic^* & : & \isarmeth \\ |
1014 |
\end{matharray} |
|
1015 |
||
1016 |
\railalias{ruletac}{rule\_tac} |
|
1017 |
\railterm{ruletac} |
|
1018 |
||
1019 |
\railalias{eruletac}{erule\_tac} |
|
1020 |
\railterm{eruletac} |
|
1021 |
||
1022 |
\railalias{druletac}{drule\_tac} |
|
1023 |
\railterm{druletac} |
|
1024 |
||
1025 |
\railalias{fruletac}{frule\_tac} |
|
1026 |
\railterm{fruletac} |
|
1027 |
||
1028 |
\railalias{cuttac}{cut\_tac} |
|
1029 |
\railterm{cuttac} |
|
1030 |
||
1031 |
\railalias{thintac}{thin\_tac} |
|
1032 |
\railterm{thintac} |
|
1033 |
||
1034 |
\railalias{subgoaltac}{subgoal\_tac} |
|
1035 |
\railterm{subgoaltac} |
|
1036 |
||
9614 | 1037 |
\railalias{renametac}{rename\_tac} |
1038 |
\railterm{renametac} |
|
1039 |
||
1040 |
\railalias{rotatetac}{rotate\_tac} |
|
1041 |
\railterm{rotatetac} |
|
1042 |
||
9606 | 1043 |
\begin{rail} |
1044 |
( ruletac | eruletac | druletac | fruletac | cuttac | thintac ) goalspec? |
|
1045 |
( insts thmref | thmrefs ) |
|
1046 |
; |
|
1047 |
subgoaltac goalspec? (prop +) |
|
1048 |
; |
|
9614 | 1049 |
renametac goalspec? (name +) |
1050 |
; |
|
1051 |
rotatetac goalspec? int? |
|
1052 |
; |
|
9606 | 1053 |
'tactic' text |
1054 |
; |
|
1055 |
||
1056 |
insts: ((name '=' term) + 'and') 'in' |
|
1057 |
; |
|
1058 |
\end{rail} |
|
1059 |
||
1060 |
\begin{descr} |
|
13041 | 1061 |
|
9606 | 1062 |
\item [$rule_tac$ etc.] do resolution of rules with explicit instantiation. |
1063 |
This works the same way as the ML tactics \texttt{res_inst_tac} etc. (see |
|
1064 |
\cite[\S3]{isabelle-ref}). |
|
13041 | 1065 |
|
1066 |
Multiple rules may be only given if there is no instantiation; then |
|
9606 | 1067 |
$rule_tac$ is the same as \texttt{resolve_tac} in ML (see |
1068 |
\cite[\S3]{isabelle-ref}). |
|
13041 | 1069 |
|
9606 | 1070 |
\item [$cut_tac$] inserts facts into the proof state as assumption of a |
1071 |
subgoal, see also \texttt{cut_facts_tac} in \cite[\S3]{isabelle-ref}. Note |
|
13027 | 1072 |
that the scope of schematic variables is spread over the main goal |
1073 |
statement. Instantiations may be given as well, see also ML tactic |
|
9606 | 1074 |
\texttt{cut_inst_tac} in \cite[\S3]{isabelle-ref}. |
13041 | 1075 |
|
9606 | 1076 |
\item [$thin_tac~\phi$] deletes the specified assumption from a subgoal; note |
1077 |
that $\phi$ may contain schematic variables. See also \texttt{thin_tac} in |
|
1078 |
\cite[\S3]{isabelle-ref}. |
|
13041 | 1079 |
|
9606 | 1080 |
\item [$subgoal_tac~\phi$] adds $\phi$ as an assumption to a subgoal. See |
1081 |
also \texttt{subgoal_tac} and \texttt{subgoals_tac} in |
|
1082 |
\cite[\S3]{isabelle-ref}. |
|
13041 | 1083 |
|
9614 | 1084 |
\item [$rename_tac~\vec x$] renames parameters of a goal according to the list |
1085 |
$\vec x$, which refers to the \emph{suffix} of variables. |
|
13041 | 1086 |
|
9614 | 1087 |
\item [$rotate_tac~n$] rotates the assumptions of a goal by $n$ positions: |
1088 |
from right to left if $n$ is positive, and from left to right if $n$ is |
|
1089 |
negative; the default value is $1$. See also \texttt{rotate_tac} in |
|
1090 |
\cite[\S3]{isabelle-ref}. |
|
13041 | 1091 |
|
9606 | 1092 |
\item [$tactic~text$] produces a proof method from any ML text of type |
1093 |
\texttt{tactic}. Apart from the usual ML environment and the current |
|
1094 |
implicit theory context, the ML code may refer to the following locally |
|
1095 |
bound values: |
|
1096 |
||
1097 |
{\footnotesize\begin{verbatim} |
|
1098 |
val ctxt : Proof.context |
|
1099 |
val facts : thm list |
|
1100 |
val thm : string -> thm |
|
1101 |
val thms : string -> thm list |
|
1102 |
\end{verbatim}} |
|
1103 |
Here \texttt{ctxt} refers to the current proof context, \texttt{facts} |
|
1104 |
indicates any current facts for forward-chaining, and |
|
1105 |
\texttt{thm}~/~\texttt{thms} retrieve named facts (including global |
|
1106 |
theorems) from the context. |
|
1107 |
\end{descr} |
|
1108 |
||
1109 |
||
12621 | 1110 |
\subsection{The Simplifier}\label{sec:simplifier} |
1111 |
||
13048 | 1112 |
\subsubsection{Simplification methods} |
12618 | 1113 |
|
8483 | 1114 |
\indexisarmeth{simp}\indexisarmeth{simp-all} |
7315 | 1115 |
\begin{matharray}{rcl} |
1116 |
simp & : & \isarmeth \\ |
|
8483 | 1117 |
simp_all & : & \isarmeth \\ |
7315 | 1118 |
\end{matharray} |
1119 |
||
11128 | 1120 |
\indexouternonterm{simpmod} |
7315 | 1121 |
\begin{rail} |
20126 | 1122 |
('simp' | 'simp\_all') ('!' ?) opt? (simpmod *) |
7315 | 1123 |
; |
1124 |
||
20126 | 1125 |
opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' | 'depth\_limit' ':' nat) ')' |
8704 | 1126 |
; |
9711 | 1127 |
simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') | |
9847 | 1128 |
'split' (() | 'add' | 'del')) ':' thmrefs |
7315 | 1129 |
; |
1130 |
\end{rail} |
|
1131 |
||
7321 | 1132 |
\begin{descr} |
13015 | 1133 |
|
8547 | 1134 |
\item [$simp$] invokes Isabelle's simplifier, after declaring additional rules |
8594 | 1135 |
according to the arguments given. Note that the \railtterm{only} modifier |
8547 | 1136 |
first removes all other rewrite rules, congruences, and looper tactics |
8594 | 1137 |
(including splits), and then behaves like \railtterm{add}. |
13041 | 1138 |
|
9711 | 1139 |
\medskip The \railtterm{cong} modifiers add or delete Simplifier congruence |
1140 |
rules (see also \cite{isabelle-ref}), the default is to add. |
|
13041 | 1141 |
|
9711 | 1142 |
\medskip The \railtterm{split} modifiers add or delete rules for the |
1143 |
Splitter (see also \cite{isabelle-ref}), the default is to add. This works |
|
1144 |
only if the Simplifier method has been properly setup to include the |
|
1145 |
Splitter (all major object logics such HOL, HOLCF, FOL, ZF do this already). |
|
13041 | 1146 |
|
13015 | 1147 |
\item [$simp_all$] is similar to $simp$, but acts on all goals (backwards from |
1148 |
the last to the first one). |
|
1149 |
||
7321 | 1150 |
\end{descr} |
1151 |
||
13015 | 1152 |
By default the Simplifier methods take local assumptions fully into account, |
1153 |
using equational assumptions in the subsequent normalization process, or |
|
13024 | 1154 |
simplifying assumptions themselves (cf.\ \texttt{asm_full_simp_tac} in |
13015 | 1155 |
\cite[\S10]{isabelle-ref}). In structured proofs this is usually quite well |
1156 |
behaved in practice: just the local premises of the actual goal are involved, |
|
13041 | 1157 |
additional facts may be inserted via explicit forward-chaining (using $\THEN$, |
13015 | 1158 |
$\FROMNAME$ etc.). The full context of assumptions is only included if the |
1159 |
``$!$'' (bang) argument is given, which should be used with some care, though. |
|
7321 | 1160 |
|
13015 | 1161 |
Additional Simplifier options may be specified to tune the behavior further |
13041 | 1162 |
(mostly for unstructured scripts with many accidental local facts): |
20126 | 1163 |
``$(no_asm)$'' means assumptions are ignored completely (cf.\ |
13041 | 1164 |
\texttt{simp_tac}), ``$(no_asm_simp)$'' means assumptions are used in the |
20126 | 1165 |
simplification of the conclusion but are not themselves simplified (cf.\ |
13041 | 1166 |
\texttt{asm_simp_tac}), and ``$(no_asm_use)$'' means assumptions are |
1167 |
simplified but are not used in the simplification of each other or the |
|
20126 | 1168 |
conclusion (cf.\ \texttt{full_simp_tac}). For compatibility reasons, there is |
1169 |
also an option ``$(asm_lr)$'', which means that an assumption is only used for |
|
1170 |
simplifying assumptions which are to the right of it (cf.\ |
|
1171 |
\texttt{asm_lr_simp_tac}). Giving an option ``$(depth_limit: n)$'' limits the |
|
1172 |
number of recursive invocations of the simplifier during conditional |
|
1173 |
rewriting. |
|
8704 | 1174 |
|
1175 |
\medskip |
|
1176 |
||
1177 |
The Splitter package is usually configured to work as part of the Simplifier. |
|
9711 | 1178 |
The effect of repeatedly applying \texttt{split_tac} can be simulated by |
13041 | 1179 |
``$(simp~only\colon~split\colon~\vec a)$''. There is also a separate $split$ |
1180 |
method available for single-step case splitting. |
|
8483 | 1181 |
|
1182 |
||
12621 | 1183 |
\subsubsection{Declaring rules} |
8483 | 1184 |
|
8667 | 1185 |
\indexisarcmd{print-simpset} |
8638 | 1186 |
\indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong} |
7321 | 1187 |
\begin{matharray}{rcl} |
13024 | 1188 |
\isarcmd{print_simpset}^* & : & \isarkeep{theory~|~proof} \\ |
7321 | 1189 |
simp & : & \isaratt \\ |
9711 | 1190 |
cong & : & \isaratt \\ |
8483 | 1191 |
split & : & \isaratt \\ |
7321 | 1192 |
\end{matharray} |
1193 |
||
1194 |
\begin{rail} |
|
9711 | 1195 |
('simp' | 'cong' | 'split') (() | 'add' | 'del') |
7321 | 1196 |
; |
1197 |
\end{rail} |
|
1198 |
||
1199 |
\begin{descr} |
|
13024 | 1200 |
|
1201 |
\item [$\isarcmd{print_simpset}$] prints the collection of rules declared to |
|
1202 |
the Simplifier, which is also known as ``simpset'' internally |
|
8667 | 1203 |
\cite{isabelle-ref}. This is a diagnostic command; $undo$ does not apply. |
13024 | 1204 |
|
8547 | 1205 |
\item [$simp$] declares simplification rules. |
13024 | 1206 |
|
8638 | 1207 |
\item [$cong$] declares congruence rules. |
13024 | 1208 |
|
9711 | 1209 |
\item [$split$] declares case split rules. |
13024 | 1210 |
|
7321 | 1211 |
\end{descr} |
7319 | 1212 |
|
7315 | 1213 |
|
24015
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1214 |
\subsubsection{Simplification procedures} |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1215 |
|
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1216 |
\indexisarcmd{simproc-setup} |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1217 |
\indexisaratt{simproc} |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1218 |
\begin{matharray}{rcl} |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1219 |
\isarcmd{simproc_setup} & : & \isarkeep{local{\dsh}theory} \\ |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1220 |
simproc & : & \isaratt \\ |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1221 |
\end{matharray} |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1222 |
|
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1223 |
\begin{rail} |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1224 |
'simproc\_setup' name '(' (term + '|') ')' '=' text \\ ('identifier' (nameref+))? |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1225 |
; |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1226 |
|
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1227 |
'simproc' (('add' ':')? | 'del' ':') (name+) |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1228 |
; |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1229 |
\end{rail} |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1230 |
|
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1231 |
\begin{descr} |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1232 |
|
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1233 |
\item [$\isarcmd{simproc_setup}$] defines a named simplification |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1234 |
procedure that is invoked by the Simplifier whenever any of the |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1235 |
given term patterns match the current redex. The implementation, |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1236 |
which is provided as ML source text, needs to be of type |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1237 |
\verb,morphism -> simpset -> cterm -> thm option,, where the |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1238 |
\verb,cterm, represents the current redex $r$ and the result is |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1239 |
supposed to be some proven rewrite rule $r \equiv r'$ (or a |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1240 |
generalized version), or \verb,NONE, to indicate failure. The |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1241 |
\verb,simpset, argument holds the full context of the current |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1242 |
Simplifier invocation, including the actual Isar proof context. The |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1243 |
\verb,morphism, informs about the difference of the original |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1244 |
compilation context wrt.\ the one of the actual application later |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1245 |
on. The optional $\isarkeyword{identifier}$ specifies theorems that |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1246 |
represent the logical content of the abstract theory of this |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1247 |
simproc. |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1248 |
|
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1249 |
Morphisms and identifiers are only relevant for simprocs that are |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1250 |
defined within a local target context, e.g.\ in a locale. |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1251 |
|
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1252 |
\item [$simproc\;add\colon\;name$ and $simproc\;del\colon\;name$] add |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1253 |
or delete named simprocs to the current Simplifier context. The |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1254 |
default is to add a simproc. Note that $\isarcmd{simproc_setup}$ |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1255 |
already adds the new simproc to the subsequent context. |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1256 |
|
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1257 |
\end{descr} |
253720dddcde
added command 'simproc_setup', attribute "simproc";
wenzelm
parents:
23920
diff
changeset
|
1258 |
|
12621 | 1259 |
\subsubsection{Forward simplification} |
1260 |
||
9905 | 1261 |
\indexisaratt{simplified} |
7315 | 1262 |
\begin{matharray}{rcl} |
9905 | 1263 |
simplified & : & \isaratt \\ |
7315 | 1264 |
\end{matharray} |
1265 |
||
9905 | 1266 |
\begin{rail} |
13015 | 1267 |
'simplified' opt? thmrefs? |
9905 | 1268 |
; |
1269 |
||
1270 |
opt: '(' (noasm | noasmsimp | noasmuse) ')' |
|
1271 |
; |
|
1272 |
\end{rail} |
|
7905 | 1273 |
|
9905 | 1274 |
\begin{descr} |
13048 | 1275 |
|
13015 | 1276 |
\item [$simplified~\vec a$] causes a theorem to be simplified, either by |
1277 |
exactly the specified rules $\vec a$, or the implicit Simplifier context if |
|
1278 |
no arguments are given. The result is fully simplified by default, |
|
1279 |
including assumptions and conclusion; the options $no_asm$ etc.\ tune the |
|
13048 | 1280 |
Simplifier in the same way as the for the $simp$ method. |
13041 | 1281 |
|
13015 | 1282 |
Note that forward simplification restricts the simplifier to its most basic |
1283 |
operation of term rewriting; solver and looper tactics \cite{isabelle-ref} |
|
1284 |
are \emph{not} involved here. The $simplified$ attribute should be only |
|
1285 |
rarely required under normal circumstances. |
|
1286 |
||
9905 | 1287 |
\end{descr} |
7315 | 1288 |
|
1289 |
||
13048 | 1290 |
\subsubsection{Low-level equational reasoning} |
9614 | 1291 |
|
12976 | 1292 |
\indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisarmeth{split} |
9614 | 1293 |
\begin{matharray}{rcl} |
13015 | 1294 |
subst^* & : & \isarmeth \\ |
9614 | 1295 |
hypsubst^* & : & \isarmeth \\ |
13015 | 1296 |
split^* & : & \isarmeth \\ |
9614 | 1297 |
\end{matharray} |
1298 |
||
1299 |
\begin{rail} |
|
15995 | 1300 |
'subst' ('(' 'asm' ')')? ('(' (nat+) ')')? thmref |
9614 | 1301 |
; |
9799 | 1302 |
'split' ('(' 'asm' ')')? thmrefs |
9703 | 1303 |
; |
9614 | 1304 |
\end{rail} |
1305 |
||
13015 | 1306 |
These methods provide low-level facilities for equational reasoning that are |
1307 |
intended for specialized applications only. Normally, single step |
|
1308 |
calculations would be performed in a structured text (see also |
|
1309 |
\S\ref{sec:calculation}), while the Simplifier methods provide the canonical |
|
1310 |
way for automated normalization (see \S\ref{sec:simplifier}). |
|
9614 | 1311 |
|
1312 |
\begin{descr} |
|
13041 | 1313 |
|
15995 | 1314 |
\item [$subst~eq$] performs a single substitution step using rule $eq$, which |
13041 | 1315 |
may be either a meta or object equality. |
1316 |
||
15995 | 1317 |
\item [$subst~(asm)~eq$] substitutes in an assumption. |
1318 |
||
1319 |
\item [$subst~(i \dots j)~eq$] performs several substitutions in the |
|
1320 |
conclusion. The numbers $i$ to $j$ indicate the positions to substitute at. |
|
1321 |
Positions are ordered from the top of the term tree moving down from left to |
|
1322 |
right. For example, in $(a+b)+(c+d)$ there are three positions where |
|
1323 |
commutativity of $+$ is applicable: 1 refers to the whole term, 2 to $a+b$ |
|
1324 |
and 3 to $c+d$. If the positions in the list $(i \dots j)$ are |
|
1325 |
non-overlapping (e.g. $(2~3)$ in $(a+b)+(c+d)$) you may assume all |
|
1326 |
substitutions are performed simultaneously. Otherwise the behaviour of |
|
1327 |
$subst$ is not specified. |
|
1328 |
||
1329 |
\item [$subst~(asm)~(i \dots j)~eq$] performs the substitutions in the |
|
16010 | 1330 |
assumptions. Positions $1 \dots i@1$ refer |
1331 |
to assumption 1, positions $i@1+1 \dots i@2$ to assumption 2, and so on. |
|
15995 | 1332 |
|
13041 | 1333 |
\item [$hypsubst$] performs substitution using some assumption; this only |
1334 |
works for equations of the form $x = t$ where $x$ is a free or bound |
|
1335 |
variable. |
|
1336 |
||
1337 |
\item [$split~\vec a$] performs single-step case splitting using rules $thms$. |
|
9799 | 1338 |
By default, splitting is performed in the conclusion of a goal; the $asm$ |
1339 |
option indicates to operate on assumptions instead. |
|
13048 | 1340 |
|
9703 | 1341 |
Note that the $simp$ method already involves repeated application of split |
13048 | 1342 |
rules as declared in the current context. |
9614 | 1343 |
\end{descr} |
1344 |
||
1345 |
||
12621 | 1346 |
\subsection{The Classical Reasoner}\label{sec:classical} |
7135 | 1347 |
|
13048 | 1348 |
\subsubsection{Basic methods} |
7321 | 1349 |
|
13024 | 1350 |
\indexisarmeth{rule}\indexisarmeth{default}\indexisarmeth{contradiction} |
1351 |
\indexisarmeth{intro}\indexisarmeth{elim} |
|
7321 | 1352 |
\begin{matharray}{rcl} |
1353 |
rule & : & \isarmeth \\ |
|
13024 | 1354 |
contradiction & : & \isarmeth \\ |
7321 | 1355 |
intro & : & \isarmeth \\ |
1356 |
elim & : & \isarmeth \\ |
|
1357 |
\end{matharray} |
|
1358 |
||
1359 |
\begin{rail} |
|
8547 | 1360 |
('rule' | 'intro' | 'elim') thmrefs? |
7321 | 1361 |
; |
1362 |
\end{rail} |
|
1363 |
||
1364 |
\begin{descr} |
|
13041 | 1365 |
|
7466 | 1366 |
\item [$rule$] as offered by the classical reasoner is a refinement over the |
13024 | 1367 |
primitive one (see \S\ref{sec:pure-meth-att}). Both versions essentially |
1368 |
work the same, but the classical version observes the classical rule context |
|
13041 | 1369 |
in addition to that of Isabelle/Pure. |
1370 |
||
1371 |
Common object logics (HOL, ZF, etc.) declare a rich collection of classical |
|
1372 |
rules (even if these would qualify as intuitionistic ones), but only few |
|
1373 |
declarations to the rule context of Isabelle/Pure |
|
1374 |
(\S\ref{sec:pure-meth-att}). |
|
1375 |
||
13024 | 1376 |
\item [$contradiction$] solves some goal by contradiction, deriving any result |
20379 | 1377 |
from both $\lnot A$ and $A$. Chained facts, which are guaranteed to |
13041 | 1378 |
participate, may appear in either order. |
9614 | 1379 |
|
7466 | 1380 |
\item [$intro$ and $elim$] repeatedly refine some goal by intro- or |
13041 | 1381 |
elim-resolution, after having inserted any chained facts. Exactly the rules |
1382 |
given as arguments are taken into account; this allows fine-tuned |
|
1383 |
decomposition of a proof problem, in contrast to common automated tools. |
|
1384 |
||
7321 | 1385 |
\end{descr} |
1386 |
||
1387 |
||
13048 | 1388 |
\subsubsection{Automated methods} |
7315 | 1389 |
|
9799 | 1390 |
\indexisarmeth{blast}\indexisarmeth{fast}\indexisarmeth{slow} |
1391 |
\indexisarmeth{best}\indexisarmeth{safe}\indexisarmeth{clarify} |
|
7321 | 1392 |
\begin{matharray}{rcl} |
9780 | 1393 |
blast & : & \isarmeth \\ |
1394 |
fast & : & \isarmeth \\ |
|
9799 | 1395 |
slow & : & \isarmeth \\ |
9780 | 1396 |
best & : & \isarmeth \\ |
1397 |
safe & : & \isarmeth \\ |
|
1398 |
clarify & : & \isarmeth \\ |
|
7321 | 1399 |
\end{matharray} |
1400 |
||
11128 | 1401 |
\indexouternonterm{clamod} |
7321 | 1402 |
\begin{rail} |
13027 | 1403 |
'blast' ('!' ?) nat? (clamod *) |
7321 | 1404 |
; |
13027 | 1405 |
('fast' | 'slow' | 'best' | 'safe' | 'clarify') ('!' ?) (clamod *) |
7321 | 1406 |
; |
1407 |
||
9408 | 1408 |
clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs |
7321 | 1409 |
; |
1410 |
\end{rail} |
|
1411 |
||
1412 |
\begin{descr} |
|
1413 |
\item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac} |
|
7335 | 1414 |
in \cite[\S11]{isabelle-ref}). The optional argument specifies a |
10858 | 1415 |
user-supplied search bound (default 20). |
9799 | 1416 |
\item [$fast$, $slow$, $best$, $safe$, and $clarify$] refer to the generic |
1417 |
classical reasoner. See \texttt{fast_tac}, \texttt{slow_tac}, |
|
1418 |
\texttt{best_tac}, \texttt{safe_tac}, and \texttt{clarify_tac} in |
|
1419 |
\cite[\S11]{isabelle-ref} for more information. |
|
7321 | 1420 |
\end{descr} |
1421 |
||
13041 | 1422 |
Any of the above methods support additional modifiers of the context of |
1423 |
classical rules. Their semantics is analogous to the attributes given before. |
|
1424 |
Facts provided by forward chaining are inserted into the goal before |
|
1425 |
commencing proof search. The ``!''~argument causes the full context of |
|
1426 |
assumptions to be included as well. |
|
7321 | 1427 |
|
7315 | 1428 |
|
12621 | 1429 |
\subsubsection{Combined automated methods}\label{sec:clasimp} |
7315 | 1430 |
|
9799 | 1431 |
\indexisarmeth{auto}\indexisarmeth{force}\indexisarmeth{clarsimp} |
1432 |
\indexisarmeth{fastsimp}\indexisarmeth{slowsimp}\indexisarmeth{bestsimp} |
|
7321 | 1433 |
\begin{matharray}{rcl} |
9606 | 1434 |
auto & : & \isarmeth \\ |
7321 | 1435 |
force & : & \isarmeth \\ |
9438 | 1436 |
clarsimp & : & \isarmeth \\ |
9606 | 1437 |
fastsimp & : & \isarmeth \\ |
9799 | 1438 |
slowsimp & : & \isarmeth \\ |
1439 |
bestsimp & : & \isarmeth \\ |
|
7321 | 1440 |
\end{matharray} |
1441 |
||
11128 | 1442 |
\indexouternonterm{clasimpmod} |
7321 | 1443 |
\begin{rail} |
13027 | 1444 |
'auto' '!'? (nat nat)? (clasimpmod *) |
9780 | 1445 |
; |
13027 | 1446 |
('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') '!'? (clasimpmod *) |
7321 | 1447 |
; |
7315 | 1448 |
|
9711 | 1449 |
clasimpmod: ('simp' (() | 'add' | 'del' | 'only') | |
10031 | 1450 |
('cong' | 'split') (() | 'add' | 'del') | |
1451 |
'iff' (((() | 'add') '?'?) | 'del') | |
|
9408 | 1452 |
(('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' thmrefs |
7321 | 1453 |
\end{rail} |
7315 | 1454 |
|
7321 | 1455 |
\begin{descr} |
9799 | 1456 |
\item [$auto$, $force$, $clarsimp$, $fastsimp$, $slowsimp$, and $bestsimp$] |
1457 |
provide access to Isabelle's combined simplification and classical reasoning |
|
1458 |
tactics. These correspond to \texttt{auto_tac}, \texttt{force_tac}, |
|
1459 |
\texttt{clarsimp_tac}, and Classical Reasoner tactics with the Simplifier |
|
1460 |
added as wrapper, see \cite[\S11]{isabelle-ref} for more information. The |
|
13048 | 1461 |
modifier arguments correspond to those given in \S\ref{sec:simplifier} and |
1462 |
\S\ref{sec:classical}. Just note that the ones related to the Simplifier |
|
1463 |
are prefixed by \railtterm{simp} here. |
|
9614 | 1464 |
|
7987 | 1465 |
Facts provided by forward chaining are inserted into the goal before doing |
1466 |
the search. The ``!''~argument causes the full context of assumptions to be |
|
1467 |
included as well. |
|
7321 | 1468 |
\end{descr} |
1469 |
||
7987 | 1470 |
|
13048 | 1471 |
\subsubsection{Declaring rules} |
7135 | 1472 |
|
8667 | 1473 |
\indexisarcmd{print-claset} |
7391 | 1474 |
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest} |
9936 | 1475 |
\indexisaratt{iff}\indexisaratt{rule} |
7321 | 1476 |
\begin{matharray}{rcl} |
13024 | 1477 |
\isarcmd{print_claset}^* & : & \isarkeep{theory~|~proof} \\ |
7321 | 1478 |
intro & : & \isaratt \\ |
1479 |
elim & : & \isaratt \\ |
|
1480 |
dest & : & \isaratt \\ |
|
9936 | 1481 |
rule & : & \isaratt \\ |
7391 | 1482 |
iff & : & \isaratt \\ |
7321 | 1483 |
\end{matharray} |
7135 | 1484 |
|
7321 | 1485 |
\begin{rail} |
18854 | 1486 |
('intro' | 'elim' | 'dest') ('!' | () | '?') nat? |
7321 | 1487 |
; |
9936 | 1488 |
'rule' 'del' |
1489 |
; |
|
10031 | 1490 |
'iff' (((() | 'add') '?'?) | 'del') |
9936 | 1491 |
; |
7321 | 1492 |
\end{rail} |
7135 | 1493 |
|
7321 | 1494 |
\begin{descr} |
13024 | 1495 |
|
1496 |
\item [$\isarcmd{print_claset}$] prints the collection of rules declared to |
|
21076 | 1497 |
the Classical Reasoner, which is also known as ``claset'' internally |
8667 | 1498 |
\cite{isabelle-ref}. This is a diagnostic command; $undo$ does not apply. |
18854 | 1499 |
|
8517 | 1500 |
\item [$intro$, $elim$, and $dest$] declare introduction, elimination, and |
11332 | 1501 |
destruction rules, respectively. By default, rules are considered as |
9408 | 1502 |
\emph{unsafe} (i.e.\ not applied blindly without backtracking), while a |
13041 | 1503 |
single ``!'' classifies as \emph{safe}. Rule declarations marked by ``?'' |
18854 | 1504 |
coincide with those of Isabelle/Pure, cf.\ \S\ref{sec:pure-meth-att} (i.e.\ |
1505 |
are only applied in single steps of the $rule$ method). The optional |
|
1506 |
natural number specifies an explicit weight argument, which is ignored by |
|
1507 |
automated tools, but determines the search order of single rule steps. |
|
13024 | 1508 |
|
11332 | 1509 |
\item [$rule~del$] deletes introduction, elimination, or destruction rules from |
9936 | 1510 |
the context. |
13041 | 1511 |
|
1512 |
\item [$iff$] declares logical equivalences to the Simplifier and the |
|
13024 | 1513 |
Classical reasoner at the same time. Non-conditional rules result in a |
1514 |
``safe'' introduction and elimination pair; conditional ones are considered |
|
1515 |
``unsafe''. Rules with negative conclusion are automatically inverted |
|
20379 | 1516 |
(using $\lnot$ elimination internally). |
13041 | 1517 |
|
1518 |
The ``?'' version of $iff$ declares rules to the Isabelle/Pure context only, |
|
1519 |
and omits the Simplifier declaration. |
|
1520 |
||
7321 | 1521 |
\end{descr} |
7135 | 1522 |
|
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8195
diff
changeset
|
1523 |
|
13048 | 1524 |
\subsubsection{Classical operations} |
13027 | 1525 |
|
18530 | 1526 |
\indexisaratt{swapped} |
13027 | 1527 |
|
1528 |
\begin{matharray}{rcl} |
|
1529 |
swapped & : & \isaratt \\ |
|
1530 |
\end{matharray} |
|
1531 |
||
1532 |
\begin{descr} |
|
13041 | 1533 |
|
13027 | 1534 |
\item [$swapped$] turns an introduction rule into an elimination, by resolving |
20379 | 1535 |
with the classical swap principle $(\lnot B \Imp A) \Imp (\lnot A \Imp B)$. |
13027 | 1536 |
|
1537 |
\end{descr} |
|
1538 |
||
1539 |
||
12621 | 1540 |
\subsection{Proof by cases and induction}\label{sec:cases-induct} |
12618 | 1541 |
|
13048 | 1542 |
\subsubsection{Rule contexts} |
12618 | 1543 |
|
1544 |
\indexisarcmd{case}\indexisarcmd{print-cases} |
|
18232 | 1545 |
\indexisaratt{case-names}\indexisaratt{case-conclusion} |
1546 |
\indexisaratt{params}\indexisaratt{consumes} |
|
12618 | 1547 |
\begin{matharray}{rcl} |
1548 |
\isarcmd{case} & : & \isartrans{proof(state)}{proof(state)} \\ |
|
1549 |
\isarcmd{print_cases}^* & : & \isarkeep{proof} \\ |
|
1550 |
case_names & : & \isaratt \\ |
|
18232 | 1551 |
case_conclusion & : & \isaratt \\ |
12618 | 1552 |
params & : & \isaratt \\ |
1553 |
consumes & : & \isaratt \\ |
|
1554 |
\end{matharray} |
|
1555 |
||
18232 | 1556 |
The puristic way to build up Isar proof contexts is by explicit language |
1557 |
elements like $\FIXNAME$, $\ASSUMENAME$, $\LET$ (see |
|
1558 |
\S\ref{sec:proof-context}). This is adequate for plain natural deduction, but |
|
1559 |
easily becomes unwieldy in concrete verification tasks, which typically |
|
1560 |
involve big induction rules with several cases. |
|
1561 |
||
1562 |
The $\CASENAME$ command provides a shorthand to refer to a local context |
|
1563 |
symbolically: certain proof methods provide an environment of named ``cases'' |
|
1564 |
of the form $c\colon \vec x, \vec \phi$; the effect of ``$\CASE{c}$'' is then |
|
1565 |
equivalent to ``$\FIX{\vec x}~\ASSUME{c}{\vec\phi}$''. Term bindings may be |
|
1566 |
covered as well, notably $\Var{case}$ for the main conclusion. |
|
1567 |
||
1568 |
By default, the ``terminology'' $\vec x$ of a case value is marked as hidden, |
|
1569 |
i.e.\ there is no way to refer to such parameters in the subsequent proof |
|
1570 |
text. After all, original rule parameters stem from somewhere outside of the |
|
1571 |
current proof text. By using the explicit form ``$\CASE{(c~\vec y)}$'' |
|
1572 |
instead, the proof author is able to chose local names that fit nicely into |
|
1573 |
the current context. |
|
12618 | 1574 |
|
1575 |
\medskip |
|
1576 |
||
18232 | 1577 |
It is important to note that proper use of $\CASENAME$ does not provide means |
1578 |
to peek at the current goal state, which is not directly observable in Isar! |
|
1579 |
Nonetheless, goal refinement commands do provide named cases $goal@i$ for each |
|
1580 |
subgoal $i = 1, \dots, n$ of the resulting goal state. Using this feature |
|
1581 |
requires great care, because some bits of the internal tactical machinery |
|
1582 |
intrude the proof text. In particular, parameter names stemming from the |
|
1583 |
left-over of automated reasoning tools are usually quite unpredictable. |
|
12618 | 1584 |
|
18232 | 1585 |
Under normal circumstances, the text of cases emerge from standard elimination |
1586 |
or induction rules, which in turn are derived from previous theory |
|
13041 | 1587 |
specifications in a canonical way (say from $\isarkeyword{inductive}$ |
1588 |
definitions). |
|
13027 | 1589 |
|
18232 | 1590 |
\medskip Proper cases are only available if both the proof method and the |
1591 |
rules involved support this. By using appropriate attributes, case names, |
|
1592 |
conclusions, and parameters may be also declared by hand. Thus variant |
|
19786 | 1593 |
versions of rules that have been derived manually become ready to use in |
18232 | 1594 |
advanced case analysis later. |
12618 | 1595 |
|
1596 |
\begin{rail} |
|
13041 | 1597 |
'case' (caseref | '(' caseref ((name | underscore) +) ')') |
12618 | 1598 |
; |
13024 | 1599 |
caseref: nameref attributes? |
1600 |
; |
|
1601 |
||
18232 | 1602 |
'case\_names' (name +) |
1603 |
; |
|
1604 |
'case\_conclusion' name (name *) |
|
12618 | 1605 |
; |
13027 | 1606 |
'params' ((name *) + 'and') |
12618 | 1607 |
; |
1608 |
'consumes' nat? |
|
1609 |
; |
|
1610 |
\end{rail} |
|
1611 |
||
1612 |
\begin{descr} |
|
18232 | 1613 |
|
13041 | 1614 |
\item [$\CASE{(c~\vec x)}$] invokes a named local context $c\colon \vec x, |
1615 |
\vec \phi$, as provided by an appropriate proof method (such as $cases$ and |
|
18232 | 1616 |
$induct$). The command ``$\CASE{(c~\vec x)}$'' abbreviates ``$\FIX{\vec |
1617 |
x}~\ASSUME{c}{\vec\phi}$''. |
|
13041 | 1618 |
|
12618 | 1619 |
\item [$\isarkeyword{print_cases}$] prints all local contexts of the current |
1620 |
state, using Isar proof language notation. This is a diagnostic command; |
|
1621 |
$undo$ does not apply. |
|
18232 | 1622 |
|
12618 | 1623 |
\item [$case_names~\vec c$] declares names for the local contexts of premises |
18232 | 1624 |
of a theorem; $\vec c$ refers to the \emph{suffix} of the list of premises. |
1625 |
||
1626 |
\item [$case_conclusion~c~\vec d$] declares names for the conclusions of a |
|
1627 |
named premise $c$; here $\vec d$ refers to the prefix of arguments of a |
|
1628 |
logical formula built by nesting a binary connective (e.g.\ $\lor$). |
|
1629 |
||
1630 |
Note that proof methods such as $induct$ and $coinduct$ already provide a |
|
1631 |
default name for the conclusion as a whole. The need to name subformulas |
|
1632 |
only arises with cases that split into several sub-cases, as in common |
|
1633 |
co-induction rules. |
|
13041 | 1634 |
|
12618 | 1635 |
\item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of |
1636 |
premises $1, \dots, n$ of some theorem. An empty list of names may be given |
|
1637 |
to skip positions, leaving the present parameters unchanged. |
|
18232 | 1638 |
|
12618 | 1639 |
Note that the default usage of case rules does \emph{not} directly expose |
18232 | 1640 |
parameters to the proof context. |
1641 |
||
12618 | 1642 |
\item [$consumes~n$] declares the number of ``major premises'' of a rule, |
1643 |
i.e.\ the number of facts to be consumed when it is applied by an |
|
18232 | 1644 |
appropriate proof method. The default value of $consumes$ is $n = 1$, which |
1645 |
is appropriate for the usual kind of cases and induction rules for inductive |
|
1646 |
sets (cf.\ \S\ref{sec:hol-inductive}). Rules without any $consumes$ |
|
1647 |
declaration given are treated as if $consumes~0$ had been specified. |
|
1648 |
||
12618 | 1649 |
Note that explicit $consumes$ declarations are only rarely needed; this is |
18232 | 1650 |
already taken care of automatically by the higher-level $cases$, $induct$, |
1651 |
and $coinduct$ declarations. |
|
13027 | 1652 |
|
12618 | 1653 |
\end{descr} |
1654 |
||
1655 |
||
18232 | 1656 |
\subsubsection{Proof methods} |
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1657 |
|
18232 | 1658 |
\indexisarmeth{cases}\indexisarmeth{induct}\indexisarmeth{coinduct} |
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1659 |
\begin{matharray}{rcl} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1660 |
cases & : & \isarmeth \\ |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1661 |
induct & : & \isarmeth \\ |
18232 | 1662 |
coinduct & : & \isarmeth \\ |
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1663 |
\end{matharray} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1664 |
|
24859 | 1665 |
The $cases$, $induct$, and $coinduct$ methods provide a uniform |
1666 |
interface to common proof techniques over datatypes, inductive |
|
1667 |
predicates (or sets), recursive functions etc. The corresponding |
|
1668 |
rules may be specified and instantiated in a casual manner. |
|
1669 |
Furthermore, these methods provide named local contexts that may be |
|
1670 |
invoked via the $\CASENAME$ proof command within the subsequent proof |
|
1671 |
text. This accommodates compact proof texts even when reasoning about |
|
1672 |
large specifications. |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1673 |
|
18232 | 1674 |
The $induct$ method also provides some additional infrastructure in order to |
1675 |
be applicable to structure statements (either using explicit meta-level |
|
1676 |
connectives, or including facts and parameters separately). This avoids |
|
1677 |
cumbersome encoding of ``strengthened'' inductive statements within the |
|
1678 |
object-logic. |
|
1679 |
||
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1680 |
\begin{rail} |
24859 | 1681 |
'cases' (insts * 'and') rule? |
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1682 |
; |
24859 | 1683 |
'induct' (definsts * 'and') \\ arbitrary? taking? rule? |
18232 | 1684 |
; |
24859 | 1685 |
'coinduct' insts taking rule? |
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1686 |
; |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1687 |
|
24859 | 1688 |
rule: ('type' | 'pred' | 'set') ':' (nameref +) | 'rule' ':' (thmref +) |
18232 | 1689 |
; |
1690 |
definst: name ('==' | equiv) term | inst |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1691 |
; |
18232 | 1692 |
definsts: ( definst *) |
1693 |
; |
|
20503 | 1694 |
arbitrary: 'arbitrary' ':' ((term *) 'and' +) |
18232 | 1695 |
; |
1696 |
taking: 'taking' ':' insts |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1697 |
; |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1698 |
\end{rail} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1699 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1700 |
\begin{descr} |
13041 | 1701 |
|
1702 |
\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
|
1703 |
distinction theorem, instantiated to the subjects $insts$. Symbolic case |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1704 |
names are bound according to the rule's local contexts. |
13041 | 1705 |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1706 |
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
|
1707 |
passed to the $cases$ method: |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1708 |
\begin{matharray}{llll} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1709 |
\Text{facts} & & \Text{arguments} & \Text{rule} \\\hline |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1710 |
& cases & & \Text{classical case split} \\ |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1711 |
& cases & t & \Text{datatype exhaustion (type of $t$)} \\ |
24859 | 1712 |
\edrv A\; t & cases & \dots & \Text{inductive predicate/set elimination (of $A$)} \\ |
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1713 |
\dots & cases & \dots ~ R & \Text{explicit rule $R$} \\ |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1714 |
\end{matharray} |
13041 | 1715 |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1716 |
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
|
1717 |
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
|
1718 |
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
|
1719 |
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
|
1720 |
usually the same for all cases). |
13041 | 1721 |
|
1722 |
\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
|
1723 |
induction rules, which are determined as follows: |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1724 |
\begin{matharray}{llll} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1725 |
\Text{facts} & & \Text{arguments} & \Text{rule} \\\hline |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1726 |
& induct & P ~ x ~ \dots & \Text{datatype induction (type of $x$)} \\ |
24859 | 1727 |
\edrv A\; x & induct & \dots & \Text{predicate/set induction (of $A$)} \\ |
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1728 |
\dots & induct & \dots ~ R & \Text{explicit rule $R$} \\ |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1729 |
\end{matharray} |
18505 | 1730 |
|
1731 |
Several instantiations may be given, each referring to some part of |
|
1732 |
a mutual inductive definition or datatype --- only related partial |
|
1733 |
induction rules may be used together, though. Any of the lists of |
|
1734 |
terms $P, x, \dots$ refers to the \emph{suffix} of variables present |
|
1735 |
in the induction rule. This enables the writer to specify only |
|
1736 |
induction variables, or both predicates and variables, for example. |
|
18232 | 1737 |
|
1738 |
Instantiations may be definitional: equations $x \equiv t$ introduce local |
|
1739 |
definitions, which are inserted into the claim and discharged after applying |
|
1740 |
the induction rule. Equalities reappear in the inductive cases, but have |
|
1741 |
been transformed according to the induction principle being involved here. |
|
1742 |
In order to achieve practically useful induction hypotheses, some variables |
|
1743 |
occurring in $t$ need to be fixed (see below). |
|
1744 |
||
20503 | 1745 |
The optional ``$arbitrary\colon \vec x$'' specification generalizes |
1746 |
variables $\vec x$ of the original goal before applying induction. Thus |
|
1747 |
induction hypotheses may become sufficiently general to get the proof |
|
1748 |
through. Together with definitional instantiations, one may effectively |
|
1749 |
perform induction over expressions of a certain structure. |
|
18232 | 1750 |
|
1751 |
The optional ``$taking\colon \vec t$'' specification provides additional |
|
1752 |
instantiations of a prefix of pending variables in the rule. Such schematic |
|
1753 |
induction rules rarely occur in practice, though. |
|
1754 |
||
1755 |
\item [$coinduct~inst~R$] is analogous to the $induct$ method, but refers to |
|
1756 |
coinduction rules, which are determined as follows: |
|
1757 |
\begin{matharray}{llll} |
|
1758 |
\Text{goal} & & \Text{arguments} & \Text{rule} \\\hline |
|
1759 |
& coinduct & x ~ \dots & \Text{type coinduction (type of $x$)} \\ |
|
24859 | 1760 |
A\; x & coinduct & \dots & \Text{predicate/set coinduction (of $A$)} \\ |
18232 | 1761 |
\dots & coinduct & \dots ~ R & \Text{explicit rule $R$} \\ |
1762 |
\end{matharray} |
|
1763 |
||
24859 | 1764 |
Coinduction is the dual of induction. Induction essentially |
1765 |
eliminates $A\; x$ towards a generic result $P\; x$, while |
|
1766 |
coinduction introduces $A\; x$ starting with $B\; x$, for a suitable |
|
1767 |
``bisimulation'' $B$. The cases of a coinduct rule are typically |
|
1768 |
named after the predicates or sets being covered, while the |
|
1769 |
conclusions consist of several alternatives being named after the |
|
18232 | 1770 |
individual destructor patterns. |
1771 |
||
24859 | 1772 |
The given instantiation refers to the \emph{suffix} of variables |
1773 |
occurring in the rule's major premise, or conclusion if unavailable. |
|
1774 |
An additional ``$taking: \vec t$'' specification may be required in |
|
1775 |
order to specify the bisimulation to be used in the coinduction |
|
1776 |
step. |
|
13027 | 1777 |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1778 |
\end{descr} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1779 |
|
13048 | 1780 |
Above methods produce named local contexts, as determined by the instantiated |
18232 | 1781 |
rule as given in the text. Beyond that, the $induct$ and $coinduct$ methods |
1782 |
guess further instantiations from the goal specification itself. Any |
|
1783 |
persisting unresolved schematic variables of the resulting rule will render |
|
1784 |
the the corresponding case invalid. The term binding |
|
1785 |
$\Var{case}$\indexisarvar{case} for the conclusion will be provided with each |
|
1786 |
case, provided that term is fully specified. |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1787 |
|
13048 | 1788 |
The $\isarkeyword{print_cases}$ command prints all named cases present in the |
1789 |
current proof state. |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1790 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1791 |
\medskip |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1792 |
|
18232 | 1793 |
Despite the additional infrastructure, both $cases$ and $coinduct$ merely |
1794 |
apply a certain rule, after instantiation, while conforming due to the usual |
|
1795 |
way of monotonic natural deduction: the context of a structured statement |
|
1796 |
$\All{\vec x} \vec\phi \Imp \dots$ reappears unchanged after the case split. |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1797 |
|
18232 | 1798 |
The $induct$ method is significantly different in this respect: the meta-level |
1799 |
structure is passed through the ``recursive'' course involved in the |
|
1800 |
induction. Thus the original statement is basically replaced by separate |
|
1801 |
copies, corresponding to the induction hypotheses and conclusion; the original |
|
1802 |
goal context is no longer available. Thus local assumptions, fixed parameters |
|
1803 |
and definitions effectively participate in the inductive rephrasing of the |
|
1804 |
original statement. |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1805 |
|
13425
119ae829ad9b
support for split assumptions in cases (hyps vs. prems);
wenzelm
parents:
13411
diff
changeset
|
1806 |
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
|
1807 |
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
|
1808 |
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
|
1809 |
``$\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
|
1810 |
$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
|
1811 |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1812 |
\medskip |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1813 |
|
24859 | 1814 |
Facts presented to either method are consumed according to the number |
1815 |
of ``major premises'' of the rule involved, which is usually $0$ for |
|
1816 |
plain cases and induction rules of datatypes etc.\ and $1$ for rules |
|
1817 |
of inductive predicates or sets and the like. The remaining facts are |
|
1818 |
inserted into the goal verbatim before the actual $cases$, $induct$, |
|
1819 |
or $coinduct$ rule is applied. |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1820 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1821 |
|
18232 | 1822 |
\subsubsection{Declaring rules} |
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1823 |
|
18232 | 1824 |
\indexisarcmd{print-induct-rules}\indexisaratt{cases}\indexisaratt{induct}\indexisaratt{coinduct} |
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1825 |
\begin{matharray}{rcl} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1826 |
\isarcmd{print_induct_rules}^* & : & \isarkeep{theory~|~proof} \\ |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1827 |
cases & : & \isaratt \\ |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1828 |
induct & : & \isaratt \\ |
18232 | 1829 |
coinduct & : & \isaratt \\ |
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1830 |
\end{matharray} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1831 |
|
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1832 |
\begin{rail} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1833 |
'cases' spec |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1834 |
; |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1835 |
'induct' spec |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1836 |
; |
18232 | 1837 |
'coinduct' spec |
1838 |
; |
|
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1839 |
|
24859 | 1840 |
spec: ('type' | 'pred' | 'set') ':' nameref |
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1841 |
; |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1842 |
\end{rail} |
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1843 |
|
13024 | 1844 |
\begin{descr} |
13041 | 1845 |
|
24859 | 1846 |
\item [$\isarkeyword{print_induct_rules}$] prints cases and induct |
1847 |
rules for predicates (or sets) and types of the current context. |
|
13048 | 1848 |
|
18232 | 1849 |
\item [$cases$, $induct$, and $coinduct$] (as attributes) augment the |
24859 | 1850 |
corresponding context of rules for reasoning about (co)inductive |
1851 |
predicates (or sets) and types, using the corresponding methods of |
|
1852 |
the same name. Certain definitional packages of object-logics |
|
1853 |
usually declare emerging cases and induction rules as expected, so |
|
1854 |
users rarely need to intervene. |
|
18232 | 1855 |
|
24859 | 1856 |
Manual rule declarations usually refer to the $case_names$ and |
1857 |
$params$ attributes to adjust names of cases and parameters of a |
|
1858 |
rule; the $consumes$ declaration is taken care of automatically: |
|
1859 |
$consumes~0$ is specified for ``type'' rules and $consumes~1$ for |
|
1860 |
``predicate'' / ``set'' rules. |
|
13041 | 1861 |
|
13024 | 1862 |
\end{descr} |
11691
fc9bd420162c
induct/cases made generic, removed simplified/stripped options;
wenzelm
parents:
11469
diff
changeset
|
1863 |
|
9614 | 1864 |
%%% Local Variables: |
7135 | 1865 |
%%% mode: latex |
1866 |
%%% TeX-master: "isar-ref" |
|
9614 | 1867 |
%%% End: |