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