|
1 theory Examples |
|
2 imports Main |
|
3 begin |
|
4 |
|
5 pretty_setmargin %invisible 65 |
|
6 |
|
7 (* |
|
8 text {* The following presentation will use notation of |
|
9 Isabelle's meta logic, hence a few sentences to explain this. |
|
10 The logical |
|
11 primitives are universal quantification (@{text "\<And>"}), entailment |
|
12 (@{text "\<Longrightarrow>"}) and equality (@{text "\<equiv>"}). Variables (not bound |
|
13 variables) are sometimes preceded by a question mark. The logic is |
|
14 typed. Type variables are denoted by~@{text "'a"},~@{text "'b"} |
|
15 etc., and~@{text "\<Rightarrow>"} is the function type. Double brackets~@{text |
|
16 "\<lbrakk>"} and~@{text "\<rbrakk>"} are used to abbreviate nested entailment. |
|
17 *} |
|
18 *) |
|
19 |
|
20 section {* Introduction *} |
|
21 |
|
22 text {* |
|
23 Locales are based on contexts. A \emph{context} can be seen as a |
|
24 formula schema |
|
25 \[ |
|
26 @{text "\<And>x\<^sub>1\<dots>x\<^sub>n. \<lbrakk> A\<^sub>1; \<dots> ;A\<^sub>m \<rbrakk> \<Longrightarrow> \<dots>"} |
|
27 \] |
|
28 where the variables~@{text "x\<^sub>1"}, \ldots,~@{text "x\<^sub>n"} are called |
|
29 \emph{parameters} and the premises $@{text "A\<^sub>1"}, \ldots,~@{text |
|
30 "A\<^sub>m"}$ \emph{assumptions}. A formula~@{text "C"} |
|
31 is a \emph{theorem} in the context if it is a conclusion |
|
32 \[ |
|
33 @{text "\<And>x\<^sub>1\<dots>x\<^sub>n. \<lbrakk> A\<^sub>1; \<dots> ;A\<^sub>m \<rbrakk> \<Longrightarrow> C"}. |
|
34 \] |
|
35 Isabelle/Isar's notion of context goes beyond this logical view. |
|
36 Its contexts record, in a consecutive order, proved |
|
37 conclusions along with \emph{attributes}, which can provide context |
|
38 specific configuration information for proof procedures and concrete |
|
39 syntax. From a logical perspective, locales are just contexts that |
|
40 have been made persistent. To the user, though, they provide |
|
41 powerful means for declaring and combining contexts, and for the |
|
42 reuse of theorems proved in these contexts. |
|
43 *} |
|
44 |
|
45 section {* Simple Locales *} |
|
46 |
|
47 text {* |
|
48 In its simplest form, a |
|
49 \emph{locale declaration} consists of a sequence of context elements |
|
50 declaring parameters (keyword \isakeyword{fixes}) and assumptions |
|
51 (keyword \isakeyword{assumes}). The following is the specification of |
|
52 partial orders, as locale @{text partial_order}. |
|
53 *} |
|
54 |
|
55 locale partial_order = |
|
56 fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubseteq>" 50) |
|
57 assumes refl [intro, simp]: "x \<sqsubseteq> x" |
|
58 and anti_sym [intro]: "\<lbrakk> x \<sqsubseteq> y; y \<sqsubseteq> x \<rbrakk> \<Longrightarrow> x = y" |
|
59 and trans [trans]: "\<lbrakk> x \<sqsubseteq> y; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z" |
|
60 |
|
61 text (in partial_order) {* The parameter of this locale is~@{text le}, |
|
62 which is a binary predicate with infix syntax~@{text \<sqsubseteq>}. The |
|
63 parameter syntax is available in the subsequent |
|
64 assumptions, which are the familiar partial order axioms. |
|
65 |
|
66 Isabelle recognises unbound names as free variables. In locale |
|
67 assumptions, these are implicitly universally quantified. That is, |
|
68 @{term "\<lbrakk> x \<sqsubseteq> y; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"} in fact means |
|
69 @{term "\<And>x y z. \<lbrakk> x \<sqsubseteq> y; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"}. |
|
70 |
|
71 Two commands are provided to inspect locales: |
|
72 \isakeyword{print\_locales} lists the names of all locales of the |
|
73 current theory; \isakeyword{print\_locale}~$n$ prints the parameters |
|
74 and assumptions of locale $n$; the variation \isakeyword{print\_locale!}~$n$ |
|
75 additionally outputs the conclusions that are stored in the locale. |
|
76 We may inspect the new locale |
|
77 by issuing \isakeyword{print\_locale!} @{term partial_order}. The output |
|
78 is the following list of context elements. |
|
79 \begin{small} |
|
80 \begin{alltt} |
|
81 \isakeyword{fixes} le :: "'a \(\Rightarrow\) 'a \(\Rightarrow\) bool" (\isakeyword{infixl} "\(\sqsubseteq\)" 50) |
|
82 \isakeyword{assumes} "partial_order op \(\sqsubseteq\)" |
|
83 \isakeyword{notes} assumption |
|
84 refl [intro, simp] = `?x \(\sqsubseteq\) ?x` |
|
85 \isakeyword{and} |
|
86 anti_sym [intro] = `\(\isasymlbrakk\)?x \(\sqsubseteq\) ?y; ?y \(\sqsubseteq\) ?x\(\isasymrbrakk\) \(\Longrightarrow\) ?x = ?y` |
|
87 \isakeyword{and} |
|
88 trans [trans] = `\(\isasymlbrakk\)?x \(\sqsubseteq\) ?y; ?y \(\sqsubseteq\) ?z\(\isasymrbrakk\) \(\Longrightarrow\) ?x \(\sqsubseteq\) ?z` |
|
89 \end{alltt} |
|
90 \end{small} |
|
91 The keyword \isakeyword{notes} denotes a conclusion element. There |
|
92 is one conclusion, which was added automatically. Instead, there is |
|
93 only one assumption, namely @{term "partial_order le"}. The locale |
|
94 declaration has introduced the predicate @{term |
|
95 partial_order} to the theory. This predicate is the |
|
96 \emph{locale predicate}. Its definition may be inspected by |
|
97 issuing \isakeyword{thm} @{thm [source] partial_order_def}. |
|
98 @{thm [display, indent=2] partial_order_def} |
|
99 In our example, this is a unary predicate over the parameter of the |
|
100 locale. It is equivalent to the original assumptions, which have |
|
101 been turned into conclusions and are |
|
102 available as theorems in the context of the locale. The names and |
|
103 attributes from the locale declaration are associated to these |
|
104 theorems and are effective in the context of the locale. |
|
105 |
|
106 Each conclusion has a \emph{foundational theorem} as counterpart |
|
107 in the theory. Technically, this is simply the theorem composed |
|
108 of context and conclusion. For the transitivity theorem, this is |
|
109 @{thm [source] partial_order.trans}: |
|
110 @{thm [display, indent=2] partial_order.trans} |
|
111 *} |
|
112 |
|
113 subsection {* Targets: Extending Locales *} |
|
114 |
|
115 text {* |
|
116 The specification of a locale is fixed, but its list of conclusions |
|
117 may be extended through Isar commands that take a \emph{target} argument. |
|
118 In the following, \isakeyword{definition} and |
|
119 \isakeyword{theorem} are illustrated. |
|
120 Table~\ref{tab:commands-with-target} lists Isar commands that accept |
|
121 a target. Isar provides various ways of specifying the target. A |
|
122 target for a single command may be indicated with keyword |
|
123 \isakeyword{in} in the following way: |
|
124 |
|
125 \begin{table} |
|
126 \hrule |
|
127 \vspace{2ex} |
|
128 \begin{center} |
|
129 \begin{tabular}{ll} |
|
130 \isakeyword{definition} & definition through an equation \\ |
|
131 \isakeyword{inductive} & inductive definition \\ |
|
132 \isakeyword{primrec} & primitive recursion \\ |
|
133 \isakeyword{fun}, \isakeyword{function} & general recursion \\ |
|
134 \isakeyword{abbreviation} & syntactic abbreviation \\ |
|
135 \isakeyword{theorem}, etc.\ & theorem statement with proof \\ |
|
136 \isakeyword{theorems}, etc.\ & redeclaration of theorems \\ |
|
137 \isakeyword{text}, etc.\ & document markup |
|
138 \end{tabular} |
|
139 \end{center} |
|
140 \hrule |
|
141 \caption{Isar commands that accept a target.} |
|
142 \label{tab:commands-with-target} |
|
143 \end{table} |
|
144 *} |
|
145 |
|
146 definition (in partial_order) |
|
147 less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubset>" 50) |
|
148 where "(x \<sqsubset> y) = (x \<sqsubseteq> y \<and> x \<noteq> y)" |
|
149 |
|
150 text (in partial_order) {* The strict order @{text less} with infix |
|
151 syntax~@{text \<sqsubset>} is |
|
152 defined in terms of the locale parameter~@{text le} and the general |
|
153 equality of the object logic we work in. The definition generates a |
|
154 \emph{foundational constant} |
|
155 @{term partial_order.less} with definition @{thm [source] |
|
156 partial_order.less_def}: |
|
157 @{thm [display, indent=2] partial_order.less_def} |
|
158 At the same time, the locale is extended by syntax transformations |
|
159 hiding this construction in the context of the locale. Here, the |
|
160 abbreviation @{text less} is available for |
|
161 @{text "partial_order.less le"}, and it is printed |
|
162 and parsed as infix~@{text \<sqsubset>}. Finally, the conclusion @{thm [source] |
|
163 less_def} is added to the locale: |
|
164 @{thm [display, indent=2] less_def} |
|
165 *} |
|
166 |
|
167 text {* The treatment of theorem statements is more straightforward. |
|
168 As an example, here is the derivation of a transitivity law for the |
|
169 strict order relation. *} |
|
170 |
|
171 lemma (in partial_order) less_le_trans [trans]: |
|
172 "\<lbrakk> x \<sqsubset> y; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<sqsubset> z" |
|
173 unfolding %visible less_def by %visible (blast intro: trans) |
|
174 |
|
175 text {* In the context of the proof, conclusions of the |
|
176 locale may be used like theorems. Attributes are effective: @{text |
|
177 anti_sym} was |
|
178 declared as introduction rule, hence it is in the context's set of |
|
179 rules used by the classical reasoner by default. *} |
|
180 |
|
181 subsection {* Context Blocks *} |
|
182 |
|
183 text {* When working with locales, sequences of commands with the same |
|
184 target are frequent. A block of commands, delimited by |
|
185 \isakeyword{begin} and \isakeyword{end}, makes a theory-like style |
|
186 of working possible. All commands inside the block refer to the |
|
187 same target. A block may immediately follow a locale |
|
188 declaration, which makes that locale the target. Alternatively the |
|
189 target for a block may be given with the \isakeyword{context} |
|
190 command. |
|
191 |
|
192 This style of working is illustrated in the block below, where |
|
193 notions of infimum and supremum for partial orders are introduced, |
|
194 together with theorems about their uniqueness. *} |
|
195 |
|
196 context partial_order |
|
197 begin |
|
198 |
|
199 definition |
|
200 is_inf where "is_inf x y i = |
|
201 (i \<sqsubseteq> x \<and> i \<sqsubseteq> y \<and> (\<forall>z. z \<sqsubseteq> x \<and> z \<sqsubseteq> y \<longrightarrow> z \<sqsubseteq> i))" |
|
202 |
|
203 definition |
|
204 is_sup where "is_sup x y s = |
|
205 (x \<sqsubseteq> s \<and> y \<sqsubseteq> s \<and> (\<forall>z. x \<sqsubseteq> z \<and> y \<sqsubseteq> z \<longrightarrow> s \<sqsubseteq> z))" |
|
206 |
|
207 lemma %invisible is_infI [intro?]: "i \<sqsubseteq> x \<Longrightarrow> i \<sqsubseteq> y \<Longrightarrow> |
|
208 (\<And>z. z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> i) \<Longrightarrow> is_inf x y i" |
|
209 by (unfold is_inf_def) blast |
|
210 |
|
211 lemma %invisible is_inf_lower [elim?]: |
|
212 "is_inf x y i \<Longrightarrow> (i \<sqsubseteq> x \<Longrightarrow> i \<sqsubseteq> y \<Longrightarrow> C) \<Longrightarrow> C" |
|
213 by (unfold is_inf_def) blast |
|
214 |
|
215 lemma %invisible is_inf_greatest [elim?]: |
|
216 "is_inf x y i \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> i" |
|
217 by (unfold is_inf_def) blast |
|
218 |
|
219 theorem is_inf_uniq: "\<lbrakk>is_inf x y i; is_inf x y i'\<rbrakk> \<Longrightarrow> i = i'" |
|
220 proof - |
|
221 assume inf: "is_inf x y i" |
|
222 assume inf': "is_inf x y i'" |
|
223 show ?thesis |
|
224 proof (rule anti_sym) |
|
225 from inf' show "i \<sqsubseteq> i'" |
|
226 proof (rule is_inf_greatest) |
|
227 from inf show "i \<sqsubseteq> x" .. |
|
228 from inf show "i \<sqsubseteq> y" .. |
|
229 qed |
|
230 from inf show "i' \<sqsubseteq> i" |
|
231 proof (rule is_inf_greatest) |
|
232 from inf' show "i' \<sqsubseteq> x" .. |
|
233 from inf' show "i' \<sqsubseteq> y" .. |
|
234 qed |
|
235 qed |
|
236 qed |
|
237 |
|
238 theorem %invisible is_inf_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> is_inf x y x" |
|
239 proof - |
|
240 assume "x \<sqsubseteq> y" |
|
241 show ?thesis |
|
242 proof |
|
243 show "x \<sqsubseteq> x" .. |
|
244 show "x \<sqsubseteq> y" by fact |
|
245 fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" show "z \<sqsubseteq> x" by fact |
|
246 qed |
|
247 qed |
|
248 |
|
249 lemma %invisible is_supI [intro?]: "x \<sqsubseteq> s \<Longrightarrow> y \<sqsubseteq> s \<Longrightarrow> |
|
250 (\<And>z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> s \<sqsubseteq> z) \<Longrightarrow> is_sup x y s" |
|
251 by (unfold is_sup_def) blast |
|
252 |
|
253 lemma %invisible is_sup_least [elim?]: |
|
254 "is_sup x y s \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> s \<sqsubseteq> z" |
|
255 by (unfold is_sup_def) blast |
|
256 |
|
257 lemma %invisible is_sup_upper [elim?]: |
|
258 "is_sup x y s \<Longrightarrow> (x \<sqsubseteq> s \<Longrightarrow> y \<sqsubseteq> s \<Longrightarrow> C) \<Longrightarrow> C" |
|
259 by (unfold is_sup_def) blast |
|
260 |
|
261 theorem is_sup_uniq: "\<lbrakk>is_sup x y s; is_sup x y s'\<rbrakk> \<Longrightarrow> s = s'" |
|
262 proof - |
|
263 assume sup: "is_sup x y s" |
|
264 assume sup': "is_sup x y s'" |
|
265 show ?thesis |
|
266 proof (rule anti_sym) |
|
267 from sup show "s \<sqsubseteq> s'" |
|
268 proof (rule is_sup_least) |
|
269 from sup' show "x \<sqsubseteq> s'" .. |
|
270 from sup' show "y \<sqsubseteq> s'" .. |
|
271 qed |
|
272 from sup' show "s' \<sqsubseteq> s" |
|
273 proof (rule is_sup_least) |
|
274 from sup show "x \<sqsubseteq> s" .. |
|
275 from sup show "y \<sqsubseteq> s" .. |
|
276 qed |
|
277 qed |
|
278 qed |
|
279 |
|
280 theorem %invisible is_sup_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> is_sup x y y" |
|
281 proof - |
|
282 assume "x \<sqsubseteq> y" |
|
283 show ?thesis |
|
284 proof |
|
285 show "x \<sqsubseteq> y" by fact |
|
286 show "y \<sqsubseteq> y" .. |
|
287 fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z" |
|
288 show "y \<sqsubseteq> z" by fact |
|
289 qed |
|
290 qed |
|
291 |
|
292 end |
|
293 |
|
294 text {* The syntax of the locale commands discussed in this tutorial is |
|
295 shown in Table~\ref{tab:commands}. The grammar is complete with the |
|
296 exception of the context elements \isakeyword{constrains} and |
|
297 \isakeyword{defines}, which are provided for backward |
|
298 compatibility. See the Isabelle/Isar Reference |
|
299 Manual~\cite{IsarRef} for full documentation. *} |
|
300 |
|
301 |
|
302 section {* Import \label{sec:import} *} |
|
303 |
|
304 text {* |
|
305 Algebraic structures are commonly defined by adding operations and |
|
306 properties to existing structures. For example, partial orders |
|
307 are extended to lattices and total orders. Lattices are extended to |
|
308 distributive lattices. *} |
|
309 |
|
310 text {* |
|
311 With locales, this kind of inheritance is achieved through |
|
312 \emph{import} of locales. The import part of a locale declaration, |
|
313 if present, precedes the context elements. Here is an example, |
|
314 where partial orders are extended to lattices. |
|
315 *} |
|
316 |
|
317 locale lattice = partial_order + |
|
318 assumes ex_inf: "\<exists>inf. is_inf x y inf" |
|
319 and ex_sup: "\<exists>sup. is_sup x y sup" |
|
320 begin |
|
321 |
|
322 text {* These assumptions refer to the predicates for infimum |
|
323 and supremum defined for @{text partial_order} in the previous |
|
324 section. We now introduce the notions of meet and join. *} |
|
325 |
|
326 definition |
|
327 meet (infixl "\<sqinter>" 70) where "x \<sqinter> y = (THE inf. is_inf x y inf)" |
|
328 definition |
|
329 join (infixl "\<squnion>" 65) where "x \<squnion> y = (THE sup. is_sup x y sup)" |
|
330 |
|
331 lemma %invisible meet_equality [elim?]: "is_inf x y i \<Longrightarrow> x \<sqinter> y = i" |
|
332 proof (unfold meet_def) |
|
333 assume "is_inf x y i" |
|
334 then show "(THE i. is_inf x y i) = i" |
|
335 by (rule the_equality) (rule is_inf_uniq [OF _ `is_inf x y i`]) |
|
336 qed |
|
337 |
|
338 lemma %invisible meetI [intro?]: |
|
339 "i \<sqsubseteq> x \<Longrightarrow> i \<sqsubseteq> y \<Longrightarrow> (\<And>z. z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> i) \<Longrightarrow> x \<sqinter> y = i" |
|
340 by (rule meet_equality, rule is_infI) blast+ |
|
341 |
|
342 lemma %invisible is_inf_meet [intro?]: "is_inf x y (x \<sqinter> y)" |
|
343 proof (unfold meet_def) |
|
344 from ex_inf obtain i where "is_inf x y i" .. |
|
345 then show "is_inf x y (THE i. is_inf x y i)" |
|
346 by (rule theI) (rule is_inf_uniq [OF _ `is_inf x y i`]) |
|
347 qed |
|
348 |
|
349 lemma %invisible meet_left [intro?]: |
|
350 "x \<sqinter> y \<sqsubseteq> x" |
|
351 by (rule is_inf_lower) (rule is_inf_meet) |
|
352 |
|
353 lemma %invisible meet_right [intro?]: |
|
354 "x \<sqinter> y \<sqsubseteq> y" |
|
355 by (rule is_inf_lower) (rule is_inf_meet) |
|
356 |
|
357 lemma %invisible meet_le [intro?]: |
|
358 "\<lbrakk> z \<sqsubseteq> x; z \<sqsubseteq> y \<rbrakk> \<Longrightarrow> z \<sqsubseteq> x \<sqinter> y" |
|
359 by (rule is_inf_greatest) (rule is_inf_meet) |
|
360 |
|
361 lemma %invisible join_equality [elim?]: "is_sup x y s \<Longrightarrow> x \<squnion> y = s" |
|
362 proof (unfold join_def) |
|
363 assume "is_sup x y s" |
|
364 then show "(THE s. is_sup x y s) = s" |
|
365 by (rule the_equality) (rule is_sup_uniq [OF _ `is_sup x y s`]) |
|
366 qed |
|
367 |
|
368 lemma %invisible joinI [intro?]: "x \<sqsubseteq> s \<Longrightarrow> y \<sqsubseteq> s \<Longrightarrow> |
|
369 (\<And>z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> s \<sqsubseteq> z) \<Longrightarrow> x \<squnion> y = s" |
|
370 by (rule join_equality, rule is_supI) blast+ |
|
371 |
|
372 lemma %invisible is_sup_join [intro?]: "is_sup x y (x \<squnion> y)" |
|
373 proof (unfold join_def) |
|
374 from ex_sup obtain s where "is_sup x y s" .. |
|
375 then show "is_sup x y (THE s. is_sup x y s)" |
|
376 by (rule theI) (rule is_sup_uniq [OF _ `is_sup x y s`]) |
|
377 qed |
|
378 |
|
379 lemma %invisible join_left [intro?]: |
|
380 "x \<sqsubseteq> x \<squnion> y" |
|
381 by (rule is_sup_upper) (rule is_sup_join) |
|
382 |
|
383 lemma %invisible join_right [intro?]: |
|
384 "y \<sqsubseteq> x \<squnion> y" |
|
385 by (rule is_sup_upper) (rule is_sup_join) |
|
386 |
|
387 lemma %invisible join_le [intro?]: |
|
388 "\<lbrakk> x \<sqsubseteq> z; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<squnion> y \<sqsubseteq> z" |
|
389 by (rule is_sup_least) (rule is_sup_join) |
|
390 |
|
391 theorem %invisible meet_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)" |
|
392 proof (rule meetI) |
|
393 show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x \<sqinter> y" |
|
394 proof |
|
395 show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x" .. |
|
396 show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y" |
|
397 proof - |
|
398 have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" .. |
|
399 also have "\<dots> \<sqsubseteq> y" .. |
|
400 finally show ?thesis . |
|
401 qed |
|
402 qed |
|
403 show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> z" |
|
404 proof - |
|
405 have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" .. |
|
406 also have "\<dots> \<sqsubseteq> z" .. |
|
407 finally show ?thesis . |
|
408 qed |
|
409 fix w assume "w \<sqsubseteq> x \<sqinter> y" and "w \<sqsubseteq> z" |
|
410 show "w \<sqsubseteq> x \<sqinter> (y \<sqinter> z)" |
|
411 proof |
|
412 show "w \<sqsubseteq> x" |
|
413 proof - |
|
414 have "w \<sqsubseteq> x \<sqinter> y" by fact |
|
415 also have "\<dots> \<sqsubseteq> x" .. |
|
416 finally show ?thesis . |
|
417 qed |
|
418 show "w \<sqsubseteq> y \<sqinter> z" |
|
419 proof |
|
420 show "w \<sqsubseteq> y" |
|
421 proof - |
|
422 have "w \<sqsubseteq> x \<sqinter> y" by fact |
|
423 also have "\<dots> \<sqsubseteq> y" .. |
|
424 finally show ?thesis . |
|
425 qed |
|
426 show "w \<sqsubseteq> z" by fact |
|
427 qed |
|
428 qed |
|
429 qed |
|
430 |
|
431 theorem %invisible meet_commute: "x \<sqinter> y = y \<sqinter> x" |
|
432 proof (rule meetI) |
|
433 show "y \<sqinter> x \<sqsubseteq> x" .. |
|
434 show "y \<sqinter> x \<sqsubseteq> y" .. |
|
435 fix z assume "z \<sqsubseteq> y" and "z \<sqsubseteq> x" |
|
436 then show "z \<sqsubseteq> y \<sqinter> x" .. |
|
437 qed |
|
438 |
|
439 theorem %invisible meet_join_absorb: "x \<sqinter> (x \<squnion> y) = x" |
|
440 proof (rule meetI) |
|
441 show "x \<sqsubseteq> x" .. |
|
442 show "x \<sqsubseteq> x \<squnion> y" .. |
|
443 fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> x \<squnion> y" |
|
444 show "z \<sqsubseteq> x" by fact |
|
445 qed |
|
446 |
|
447 theorem %invisible join_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)" |
|
448 proof (rule joinI) |
|
449 show "x \<squnion> y \<sqsubseteq> x \<squnion> (y \<squnion> z)" |
|
450 proof |
|
451 show "x \<sqsubseteq> x \<squnion> (y \<squnion> z)" .. |
|
452 show "y \<sqsubseteq> x \<squnion> (y \<squnion> z)" |
|
453 proof - |
|
454 have "y \<sqsubseteq> y \<squnion> z" .. |
|
455 also have "... \<sqsubseteq> x \<squnion> (y \<squnion> z)" .. |
|
456 finally show ?thesis . |
|
457 qed |
|
458 qed |
|
459 show "z \<sqsubseteq> x \<squnion> (y \<squnion> z)" |
|
460 proof - |
|
461 have "z \<sqsubseteq> y \<squnion> z" .. |
|
462 also have "... \<sqsubseteq> x \<squnion> (y \<squnion> z)" .. |
|
463 finally show ?thesis . |
|
464 qed |
|
465 fix w assume "x \<squnion> y \<sqsubseteq> w" and "z \<sqsubseteq> w" |
|
466 show "x \<squnion> (y \<squnion> z) \<sqsubseteq> w" |
|
467 proof |
|
468 show "x \<sqsubseteq> w" |
|
469 proof - |
|
470 have "x \<sqsubseteq> x \<squnion> y" .. |
|
471 also have "\<dots> \<sqsubseteq> w" by fact |
|
472 finally show ?thesis . |
|
473 qed |
|
474 show "y \<squnion> z \<sqsubseteq> w" |
|
475 proof |
|
476 show "y \<sqsubseteq> w" |
|
477 proof - |
|
478 have "y \<sqsubseteq> x \<squnion> y" .. |
|
479 also have "... \<sqsubseteq> w" by fact |
|
480 finally show ?thesis . |
|
481 qed |
|
482 show "z \<sqsubseteq> w" by fact |
|
483 qed |
|
484 qed |
|
485 qed |
|
486 |
|
487 theorem %invisible join_commute: "x \<squnion> y = y \<squnion> x" |
|
488 proof (rule joinI) |
|
489 show "x \<sqsubseteq> y \<squnion> x" .. |
|
490 show "y \<sqsubseteq> y \<squnion> x" .. |
|
491 fix z assume "y \<sqsubseteq> z" and "x \<sqsubseteq> z" |
|
492 then show "y \<squnion> x \<sqsubseteq> z" .. |
|
493 qed |
|
494 |
|
495 theorem %invisible join_meet_absorb: "x \<squnion> (x \<sqinter> y) = x" |
|
496 proof (rule joinI) |
|
497 show "x \<sqsubseteq> x" .. |
|
498 show "x \<sqinter> y \<sqsubseteq> x" .. |
|
499 fix z assume "x \<sqsubseteq> z" and "x \<sqinter> y \<sqsubseteq> z" |
|
500 show "x \<sqsubseteq> z" by fact |
|
501 qed |
|
502 |
|
503 theorem %invisible meet_idem: "x \<sqinter> x = x" |
|
504 proof - |
|
505 have "x \<sqinter> (x \<squnion> (x \<sqinter> x)) = x" by (rule meet_join_absorb) |
|
506 also have "x \<squnion> (x \<sqinter> x) = x" by (rule join_meet_absorb) |
|
507 finally show ?thesis . |
|
508 qed |
|
509 |
|
510 theorem %invisible meet_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x" |
|
511 proof (rule meetI) |
|
512 assume "x \<sqsubseteq> y" |
|
513 show "x \<sqsubseteq> x" .. |
|
514 show "x \<sqsubseteq> y" by fact |
|
515 fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" |
|
516 show "z \<sqsubseteq> x" by fact |
|
517 qed |
|
518 |
|
519 theorem %invisible meet_related2 [elim?]: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y" |
|
520 by (drule meet_related) (simp add: meet_commute) |
|
521 |
|
522 theorem %invisible join_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y" |
|
523 proof (rule joinI) |
|
524 assume "x \<sqsubseteq> y" |
|
525 show "y \<sqsubseteq> y" .. |
|
526 show "x \<sqsubseteq> y" by fact |
|
527 fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z" |
|
528 show "y \<sqsubseteq> z" by fact |
|
529 qed |
|
530 |
|
531 theorem %invisible join_related2 [elim?]: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x" |
|
532 by (drule join_related) (simp add: join_commute) |
|
533 |
|
534 theorem %invisible meet_connection: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)" |
|
535 proof |
|
536 assume "x \<sqsubseteq> y" |
|
537 then have "is_inf x y x" .. |
|
538 then show "x \<sqinter> y = x" .. |
|
539 next |
|
540 have "x \<sqinter> y \<sqsubseteq> y" .. |
|
541 also assume "x \<sqinter> y = x" |
|
542 finally show "x \<sqsubseteq> y" . |
|
543 qed |
|
544 |
|
545 theorem %invisible join_connection: "(x \<sqsubseteq> y) = (x \<squnion> y = y)" |
|
546 proof |
|
547 assume "x \<sqsubseteq> y" |
|
548 then have "is_sup x y y" .. |
|
549 then show "x \<squnion> y = y" .. |
|
550 next |
|
551 have "x \<sqsubseteq> x \<squnion> y" .. |
|
552 also assume "x \<squnion> y = y" |
|
553 finally show "x \<sqsubseteq> y" . |
|
554 qed |
|
555 |
|
556 theorem %invisible meet_connection2: "(x \<sqsubseteq> y) = (y \<sqinter> x = x)" |
|
557 using meet_commute meet_connection by simp |
|
558 |
|
559 theorem %invisible join_connection2: "(x \<sqsubseteq> y) = (x \<squnion> y = y)" |
|
560 using join_commute join_connection by simp |
|
561 |
|
562 text %invisible {* Naming according to Jacobson I, p.\ 459. *} |
|
563 lemmas %invisible L1 = join_commute meet_commute |
|
564 lemmas %invisible L2 = join_assoc meet_assoc |
|
565 (* lemmas L3 = join_idem meet_idem *) |
|
566 lemmas %invisible L4 = join_meet_absorb meet_join_absorb |
|
567 |
|
568 end |
|
569 |
|
570 text {* Locales for total orders and distributive lattices follow to |
|
571 establish a sufficiently rich landscape of locales for |
|
572 further examples in this tutorial. Each comes with an example |
|
573 theorem. *} |
|
574 |
|
575 locale total_order = partial_order + |
|
576 assumes total: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x" |
|
577 |
|
578 lemma (in total_order) less_total: "x \<sqsubset> y \<or> x = y \<or> y \<sqsubset> x" |
|
579 using total |
|
580 by (unfold less_def) blast |
|
581 |
|
582 locale distrib_lattice = lattice + |
|
583 assumes meet_distr: "x \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> z" |
|
584 |
|
585 lemma (in distrib_lattice) join_distr: |
|
586 "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" (* txt {* Jacobson I, p.\ 462 *} *) |
|
587 proof - |
|
588 have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by (simp add: L4) |
|
589 also have "... = x \<squnion> ((x \<sqinter> z) \<squnion> (y \<sqinter> z))" by (simp add: L2) |
|
590 also have "... = x \<squnion> ((x \<squnion> y) \<sqinter> z)" by (simp add: L1 meet_distr) |
|
591 also have "... = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)" by (simp add: L1 L4) |
|
592 also have "... = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by (simp add: meet_distr) |
|
593 finally show ?thesis . |
|
594 qed |
|
595 |
|
596 text {* |
|
597 The locale hierarchy obtained through these declarations is shown in |
|
598 Figure~\ref{fig:lattices}(a). |
|
599 |
|
600 \begin{figure} |
|
601 \hrule \vspace{2ex} |
|
602 \begin{center} |
|
603 \subfigure[Declared hierarchy]{ |
|
604 \begin{tikzpicture} |
|
605 \node (po) at (0,0) {@{text partial_order}}; |
|
606 \node (lat) at (-1.5,-1) {@{text lattice}}; |
|
607 \node (dlat) at (-1.5,-2) {@{text distrib_lattice}}; |
|
608 \node (to) at (1.5,-1) {@{text total_order}}; |
|
609 \draw (po) -- (lat); |
|
610 \draw (lat) -- (dlat); |
|
611 \draw (po) -- (to); |
|
612 % \draw[->, dashed] (lat) -- (to); |
|
613 \end{tikzpicture} |
|
614 } \\ |
|
615 \subfigure[Total orders are lattices]{ |
|
616 \begin{tikzpicture} |
|
617 \node (po) at (0,0) {@{text partial_order}}; |
|
618 \node (lat) at (0,-1) {@{text lattice}}; |
|
619 \node (dlat) at (-1.5,-2) {@{text distrib_lattice}}; |
|
620 \node (to) at (1.5,-2) {@{text total_order}}; |
|
621 \draw (po) -- (lat); |
|
622 \draw (lat) -- (dlat); |
|
623 \draw (lat) -- (to); |
|
624 % \draw[->, dashed] (dlat) -- (to); |
|
625 \end{tikzpicture} |
|
626 } \quad |
|
627 \subfigure[Total orders are distributive lattices]{ |
|
628 \begin{tikzpicture} |
|
629 \node (po) at (0,0) {@{text partial_order}}; |
|
630 \node (lat) at (0,-1) {@{text lattice}}; |
|
631 \node (dlat) at (0,-2) {@{text distrib_lattice}}; |
|
632 \node (to) at (0,-3) {@{text total_order}}; |
|
633 \draw (po) -- (lat); |
|
634 \draw (lat) -- (dlat); |
|
635 \draw (dlat) -- (to); |
|
636 \end{tikzpicture} |
|
637 } |
|
638 \end{center} |
|
639 \hrule |
|
640 \caption{Hierarchy of Lattice Locales.} |
|
641 \label{fig:lattices} |
|
642 \end{figure} |
|
643 *} |
|
644 |
|
645 section {* Changing the Locale Hierarchy |
|
646 \label{sec:changing-the-hierarchy} *} |
|
647 |
|
648 text {* |
|
649 Locales enable to prove theorems abstractly, relative to |
|
650 sets of assumptions. These theorems can then be used in other |
|
651 contexts where the assumptions themselves, or |
|
652 instances of the assumptions, are theorems. This form of theorem |
|
653 reuse is called \emph{interpretation}. Locales generalise |
|
654 interpretation from theorems to conclusions, enabling the reuse of |
|
655 definitions and other constructs that are not part of the |
|
656 specifications of the locales. |
|
657 |
|
658 The first form of interpretation we will consider in this tutorial |
|
659 is provided by the \isakeyword{sublocale} command. It enables to |
|
660 modify the import hierarchy to reflect the \emph{logical} relation |
|
661 between locales. |
|
662 |
|
663 Consider the locale hierarchy from Figure~\ref{fig:lattices}(a). |
|
664 Total orders are lattices, although this is not reflected here, and |
|
665 definitions, theorems and other conclusions |
|
666 from @{term lattice} are not available in @{term total_order}. To |
|
667 obtain the situation in Figure~\ref{fig:lattices}(b), it is |
|
668 sufficient to add the conclusions of the latter locale to the former. |
|
669 The \isakeyword{sublocale} command does exactly this. |
|
670 The declaration \isakeyword{sublocale} $l_1 |
|
671 \subseteq l_2$ causes locale $l_2$ to be \emph{interpreted} in the |
|
672 context of $l_1$. This means that all conclusions of $l_2$ are made |
|
673 available in $l_1$. |
|
674 |
|
675 Of course, the change of hierarchy must be supported by a theorem |
|
676 that reflects, in our example, that total orders are indeed |
|
677 lattices. Therefore the \isakeyword{sublocale} command generates a |
|
678 goal, which must be discharged by the user. This is illustrated in |
|
679 the following paragraphs. First the sublocale relation is stated. |
|
680 *} |
|
681 |
|
682 sublocale %visible total_order \<subseteq> lattice |
|
683 |
|
684 txt {* \normalsize |
|
685 This enters the context of locale @{text total_order}, in |
|
686 which the goal @{subgoals [display]} must be shown. |
|
687 Now the |
|
688 locale predicate needs to be unfolded --- for example, using its |
|
689 definition or by introduction rules |
|
690 provided by the locale package. For automation, the locale package |
|
691 provides the methods @{text intro_locales} and @{text |
|
692 unfold_locales}. They are aware of the |
|
693 current context and dependencies between locales and automatically |
|
694 discharge goals implied by these. While @{text unfold_locales} |
|
695 always unfolds locale predicates to assumptions, @{text |
|
696 intro_locales} only unfolds definitions along the locale |
|
697 hierarchy, leaving a goal consisting of predicates defined by the |
|
698 locale package. Occasionally the latter is of advantage since the goal |
|
699 is smaller. |
|
700 |
|
701 For the current goal, we would like to get hold of |
|
702 the assumptions of @{text lattice}, which need to be shown, hence |
|
703 @{text unfold_locales} is appropriate. *} |
|
704 |
|
705 proof unfold_locales |
|
706 |
|
707 txt {* \normalsize |
|
708 Since the fact that both lattices and total orders are partial |
|
709 orders is already reflected in the locale hierarchy, the assumptions |
|
710 of @{text partial_order} are discharged automatically, and only the |
|
711 assumptions introduced in @{text lattice} remain as subgoals |
|
712 @{subgoals [display]} |
|
713 The proof for the first subgoal is obtained by constructing an |
|
714 infimum, whose existence is implied by totality. *} |
|
715 |
|
716 fix x y |
|
717 from total have "is_inf x y (if x \<sqsubseteq> y then x else y)" |
|
718 by (auto simp: is_inf_def) |
|
719 then show "\<exists>inf. is_inf x y inf" .. |
|
720 txt {* \normalsize |
|
721 The proof for the second subgoal is analogous and not |
|
722 reproduced here. *} |
|
723 next %invisible |
|
724 fix x y |
|
725 from total have "is_sup x y (if x \<sqsubseteq> y then y else x)" |
|
726 by (auto simp: is_sup_def) |
|
727 then show "\<exists>sup. is_sup x y sup" .. qed %visible |
|
728 |
|
729 text {* Similarly, we may establish that total orders are distributive |
|
730 lattices with a second \isakeyword{sublocale} statement. *} |
|
731 |
|
732 sublocale total_order \<subseteq> distrib_lattice |
|
733 proof unfold_locales |
|
734 fix %"proof" x y z |
|
735 show "x \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> z" (is "?l = ?r") |
|
736 txt {* Jacobson I, p.\ 462 *} |
|
737 proof - |
|
738 { assume c: "y \<sqsubseteq> x" "z \<sqsubseteq> x" |
|
739 from c have "?l = y \<squnion> z" |
|
740 by (metis c join_connection2 join_related2 meet_related2 total) |
|
741 also from c have "... = ?r" by (metis meet_related2) |
|
742 finally have "?l = ?r" . } |
|
743 moreover |
|
744 { assume c: "x \<sqsubseteq> y \<or> x \<sqsubseteq> z" |
|
745 from c have "?l = x" |
|
746 by (metis join_connection2 join_related2 meet_connection total trans) |
|
747 also from c have "... = ?r" |
|
748 by (metis join_commute join_related2 meet_connection meet_related2 total) |
|
749 finally have "?l = ?r" . } |
|
750 moreover note total |
|
751 ultimately show ?thesis by blast |
|
752 qed |
|
753 qed |
|
754 |
|
755 text {* The locale hierarchy is now as shown in |
|
756 Figure~\ref{fig:lattices}(c). *} |
|
757 |
|
758 text {* |
|
759 Locale interpretation is \emph{dynamic}. The statement |
|
760 \isakeyword{sublocale} $l_1 \subseteq l_2$ will not just add the |
|
761 current conclusions of $l_2$ to $l_1$. Rather the dependency is |
|
762 stored, and conclusions that will be |
|
763 added to $l_2$ in future are automatically propagated to $l_1$. |
|
764 The sublocale relation is transitive --- that is, propagation takes |
|
765 effect along chains of sublocales. Even cycles in the sublocale relation are |
|
766 supported, as long as these cycles do not lead to infinite chains. |
|
767 Details are discussed in the technical report \cite{Ballarin2006a}. |
|
768 See also Section~\ref{sec:infinite-chains} of this tutorial. *} |
|
769 |
|
770 end |