author | ballarin |
Sat, 28 Mar 2009 22:14:21 +0100 | |
changeset 30780 | c3f1e8a9e0b5 |
parent 30580 | cc5a55d7a5be |
child 30826 | a53f4872400e |
permissions | -rw-r--r-- |
27063 | 1 |
theory Examples |
27375 | 2 |
imports Main GCD |
27063 | 3 |
begin |
4 |
||
27081 | 5 |
hide %invisible const Lattices.lattice |
6 |
pretty_setmargin %invisible 65 |
|
27063 | 7 |
|
8 |
(* |
|
9 |
text {* The following presentation will use notation of |
|
10 |
Isabelle's meta logic, hence a few sentences to explain this. |
|
11 |
The logical |
|
12 |
primitives are universal quantification (@{text "\<And>"}), entailment |
|
13 |
(@{text "\<Longrightarrow>"}) and equality (@{text "\<equiv>"}). Variables (not bound |
|
14 |
variables) are sometimes preceded by a question mark. The logic is |
|
15 |
typed. Type variables are denoted by @{text "'a"}, @{text "'b"} |
|
16 |
etc., and @{text "\<Rightarrow>"} is the function type. Double brackets @{text |
|
17 |
"\<lbrakk>"} and @{text "\<rbrakk>"} are used to abbreviate nested entailment. |
|
18 |
*} |
|
19 |
*) |
|
20 |
||
21 |
section {* Introduction *} |
|
22 |
||
23 |
text {* |
|
24 |
Locales are based on contexts. A \emph{context} can be seen as a |
|
25 |
formula schema |
|
26 |
\[ |
|
27 |
@{text "\<And>x\<^sub>1\<dots>x\<^sub>n. \<lbrakk> A\<^sub>1; \<dots> ;A\<^sub>m \<rbrakk> \<Longrightarrow> \<dots>"} |
|
28 |
\] |
|
29 |
where variables @{text "x\<^sub>1"}, \ldots, @{text "x\<^sub>n"} are called |
|
30 |
\emph{parameters} and the premises $@{text "A\<^sub>1"}, \ldots, |
|
31 |
@{text "A\<^sub>m"}$ \emph{assumptions}. A formula @{text "C"} |
|
32 |
is a \emph{theorem} in the context if it is a conclusion |
|
33 |
\[ |
|
34 |
%\label{eq-fact-in-context} |
|
35 |
@{text "\<And>x\<^sub>1\<dots>x\<^sub>n. \<lbrakk> A\<^sub>1; \<dots> ;A\<^sub>m \<rbrakk> \<Longrightarrow> C"}. |
|
36 |
\] |
|
37 |
Isabelle/Isar's notion of context goes beyond this logical view. |
|
38 |
Its contexts record, in a consecutive order, proved |
|
39 |
conclusions along with attributes, which |
|
40 |
may control proof procedures. Contexts also contain syntax information |
|
41 |
for parameters and for terms depending on them. |
|
42 |
*} |
|
43 |
||
44 |
section {* Simple Locales *} |
|
45 |
||
46 |
text {* |
|
47 |
Locales can be seen as persistent contexts. In its simplest form, a |
|
48 |
\emph{locale declaration} consists of a sequence of context elements |
|
49 |
declaring parameters (keyword \isakeyword{fixes}) and assumptions |
|
50 |
(keyword \isakeyword{assumes}). The following is the specification of |
|
51 |
partial orders, as locale @{text partial_order}. |
|
52 |
*} |
|
53 |
||
54 |
locale partial_order = |
|
55 |
fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubseteq>" 50) |
|
56 |
assumes refl [intro, simp]: "x \<sqsubseteq> x" |
|
57 |
and anti_sym [intro]: "\<lbrakk> x \<sqsubseteq> y; y \<sqsubseteq> x \<rbrakk> \<Longrightarrow> x = y" |
|
58 |
and trans [trans]: "\<lbrakk> x \<sqsubseteq> y; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z" |
|
59 |
||
60 |
text {* The parameter of this locale is @{term le}, with infix syntax |
|
61 |
@{text \<sqsubseteq>}. There is an implicit type parameter @{typ "'a"}. It |
|
62 |
is not necessary to declare parameter types: most general types will |
|
63 |
be inferred from the context elements for all parameters. |
|
64 |
||
65 |
The above declaration not only introduces the locale, it also |
|
66 |
defines the \emph{locale predicate} @{term partial_order} with |
|
67 |
definition @{thm [source] partial_order_def}: |
|
68 |
@{thm [display, indent=2] partial_order_def} |
|
69 |
||
70 |
The specification of a locale is fixed, but its list of conclusions |
|
71 |
may be extended through Isar commands that take a \emph{target} argument. |
|
72 |
In the following, \isakeyword{definition} and |
|
73 |
\isakeyword{theorem} are illustrated. |
|
74 |
Table~\ref{tab:commands-with-target} lists Isar commands that accept |
|
75 |
a target. There are various ways of specifying the target. A |
|
76 |
target for a single command may be indicated with keyword |
|
77 |
\isakeyword{in} in the following way: |
|
78 |
||
79 |
\begin{table} |
|
80 |
\hrule |
|
81 |
\vspace{2ex} |
|
82 |
\begin{center} |
|
83 |
\begin{tabular}{ll} |
|
84 |
\isakeyword{definition} & definition through an equation \\ |
|
85 |
\isakeyword{inductive} & inductive definition \\ |
|
86 |
\isakeyword{fun}, \isakeyword{function} & recursive function \\ |
|
87 |
\isakeyword{abbreviation} & syntactic abbreviation \\ |
|
88 |
\isakeyword{theorem}, etc.\ & theorem statement with proof \\ |
|
89 |
\isakeyword{theorems}, etc.\ & redeclaration of theorems |
|
90 |
\end{tabular} |
|
91 |
\end{center} |
|
92 |
\hrule |
|
93 |
\caption{Isar commands that accept a target.} |
|
94 |
\label{tab:commands-with-target} |
|
95 |
\end{table} |
|
96 |
*} |
|
97 |
||
98 |
definition (in partial_order) |
|
99 |
less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubset>" 50) |
|
100 |
where "(x \<sqsubset> y) = (x \<sqsubseteq> y \<and> x \<noteq> y)" |
|
101 |
||
102 |
text {* A definition in a locale depends on the locale parameters. |
|
103 |
Here, a global constant @{term partial_order.less} is declared, which is lifted over the |
|
104 |
locale parameter @{term le}. Its definition is the global theorem |
|
105 |
@{thm [source] partial_order.less_def}: |
|
106 |
@{thm [display, indent=2] partial_order.less_def} |
|
107 |
At the same time, the locale is extended by syntax information |
|
108 |
hiding this construction in the context of the locale. That is, |
|
109 |
@{term "partial_order.less le"} is printed and parsed as infix |
|
30393
aa6f42252bf6
replaced old locale option by proper "text (in locale)";
wenzelm
parents:
29567
diff
changeset
|
110 |
@{text \<sqsubset>}. *} |
aa6f42252bf6
replaced old locale option by proper "text (in locale)";
wenzelm
parents:
29567
diff
changeset
|
111 |
|
aa6f42252bf6
replaced old locale option by proper "text (in locale)";
wenzelm
parents:
29567
diff
changeset
|
112 |
text (in partial_order) {* Finally, the conclusion of the definition |
aa6f42252bf6
replaced old locale option by proper "text (in locale)";
wenzelm
parents:
29567
diff
changeset
|
113 |
is added to the locale, @{thm [source] less_def}: |
aa6f42252bf6
replaced old locale option by proper "text (in locale)";
wenzelm
parents:
29567
diff
changeset
|
114 |
@{thm [display, indent=2] less_def} |
27063 | 115 |
*} |
116 |
||
117 |
text {* As an example of a theorem statement in the locale, here is the |
|
118 |
derivation of a transitivity law. *} |
|
119 |
||
120 |
lemma (in partial_order) less_le_trans [trans]: |
|
121 |
"\<lbrakk> x \<sqsubset> y; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<sqsubset> z" |
|
122 |
unfolding %visible less_def by %visible (blast intro: trans) |
|
123 |
||
124 |
text {* In the context of the proof, assumptions and theorems of the |
|
125 |
locale may be used. Attributes are effective: @{text anti_sym} was |
|
126 |
declared as introduction rule, hence it is in the context's set of |
|
127 |
rules used by the classical reasoner by default. *} |
|
128 |
||
129 |
text {* When working with locales, sequences of commands with the same |
|
130 |
target are frequent. A block of commands, delimited by |
|
131 |
\isakeyword{begin} and \isakeyword{end}, makes a theory-like style |
|
132 |
of working possible. All commands inside the block refer to the |
|
133 |
same target. A block may immediately follow a locale |
|
134 |
declaration, which makes that locale the target. Alternatively the |
|
135 |
target for a block may be given with the \isakeyword{context} |
|
136 |
command. |
|
137 |
||
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
138 |
This style of working is illustrated in the block below, where |
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
139 |
notions of infimum and supremum for partial orders are introduced, |
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
140 |
together with theorems. *} |
27063 | 141 |
|
142 |
context partial_order begin |
|
143 |
||
144 |
definition |
|
145 |
is_inf where "is_inf x y i = |
|
146 |
(i \<sqsubseteq> x \<and> i \<sqsubseteq> y \<and> (\<forall>z. z \<sqsubseteq> x \<and> z \<sqsubseteq> y \<longrightarrow> z \<sqsubseteq> i))" |
|
147 |
||
148 |
definition |
|
149 |
is_sup where "is_sup x y s = |
|
150 |
(x \<sqsubseteq> s \<and> y \<sqsubseteq> s \<and> (\<forall>z. x \<sqsubseteq> z \<and> y \<sqsubseteq> z \<longrightarrow> s \<sqsubseteq> z))" |
|
151 |
||
152 |
lemma %invisible is_infI [intro?]: "i \<sqsubseteq> x \<Longrightarrow> i \<sqsubseteq> y \<Longrightarrow> |
|
153 |
(\<And>z. z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> i) \<Longrightarrow> is_inf x y i" |
|
154 |
by (unfold is_inf_def) blast |
|
155 |
||
156 |
lemma %invisible is_inf_lower [elim?]: |
|
157 |
"is_inf x y i \<Longrightarrow> (i \<sqsubseteq> x \<Longrightarrow> i \<sqsubseteq> y \<Longrightarrow> C) \<Longrightarrow> C" |
|
158 |
by (unfold is_inf_def) blast |
|
159 |
||
160 |
lemma %invisible is_inf_greatest [elim?]: |
|
161 |
"is_inf x y i \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> i" |
|
162 |
by (unfold is_inf_def) blast |
|
163 |
||
164 |
theorem is_inf_uniq: "\<lbrakk>is_inf x y i; is_inf x y i'\<rbrakk> \<Longrightarrow> i = i'" |
|
165 |
proof - |
|
166 |
assume inf: "is_inf x y i" |
|
167 |
assume inf': "is_inf x y i'" |
|
168 |
show ?thesis |
|
169 |
proof (rule anti_sym) |
|
170 |
from inf' show "i \<sqsubseteq> i'" |
|
171 |
proof (rule is_inf_greatest) |
|
172 |
from inf show "i \<sqsubseteq> x" .. |
|
173 |
from inf show "i \<sqsubseteq> y" .. |
|
174 |
qed |
|
175 |
from inf show "i' \<sqsubseteq> i" |
|
176 |
proof (rule is_inf_greatest) |
|
177 |
from inf' show "i' \<sqsubseteq> x" .. |
|
178 |
from inf' show "i' \<sqsubseteq> y" .. |
|
179 |
qed |
|
180 |
qed |
|
181 |
qed |
|
182 |
||
183 |
theorem %invisible is_inf_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> is_inf x y x" |
|
184 |
proof - |
|
185 |
assume "x \<sqsubseteq> y" |
|
186 |
show ?thesis |
|
187 |
proof |
|
188 |
show "x \<sqsubseteq> x" .. |
|
189 |
show "x \<sqsubseteq> y" by fact |
|
190 |
fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" show "z \<sqsubseteq> x" by fact |
|
191 |
qed |
|
192 |
qed |
|
193 |
||
194 |
lemma %invisible is_supI [intro?]: "x \<sqsubseteq> s \<Longrightarrow> y \<sqsubseteq> s \<Longrightarrow> |
|
195 |
(\<And>z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> s \<sqsubseteq> z) \<Longrightarrow> is_sup x y s" |
|
196 |
by (unfold is_sup_def) blast |
|
197 |
||
198 |
lemma %invisible is_sup_least [elim?]: |
|
199 |
"is_sup x y s \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> s \<sqsubseteq> z" |
|
200 |
by (unfold is_sup_def) blast |
|
201 |
||
202 |
lemma %invisible is_sup_upper [elim?]: |
|
203 |
"is_sup x y s \<Longrightarrow> (x \<sqsubseteq> s \<Longrightarrow> y \<sqsubseteq> s \<Longrightarrow> C) \<Longrightarrow> C" |
|
204 |
by (unfold is_sup_def) blast |
|
205 |
||
206 |
theorem is_sup_uniq: "\<lbrakk>is_sup x y s; is_sup x y s'\<rbrakk> \<Longrightarrow> s = s'" |
|
207 |
proof - |
|
208 |
assume sup: "is_sup x y s" |
|
209 |
assume sup': "is_sup x y s'" |
|
210 |
show ?thesis |
|
211 |
proof (rule anti_sym) |
|
212 |
from sup show "s \<sqsubseteq> s'" |
|
213 |
proof (rule is_sup_least) |
|
214 |
from sup' show "x \<sqsubseteq> s'" .. |
|
215 |
from sup' show "y \<sqsubseteq> s'" .. |
|
216 |
qed |
|
217 |
from sup' show "s' \<sqsubseteq> s" |
|
218 |
proof (rule is_sup_least) |
|
219 |
from sup show "x \<sqsubseteq> s" .. |
|
220 |
from sup show "y \<sqsubseteq> s" .. |
|
221 |
qed |
|
222 |
qed |
|
223 |
qed |
|
224 |
||
225 |
theorem %invisible is_sup_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> is_sup x y y" |
|
226 |
proof - |
|
227 |
assume "x \<sqsubseteq> y" |
|
228 |
show ?thesis |
|
229 |
proof |
|
230 |
show "x \<sqsubseteq> y" by fact |
|
231 |
show "y \<sqsubseteq> y" .. |
|
232 |
fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z" |
|
233 |
show "y \<sqsubseteq> z" by fact |
|
234 |
qed |
|
235 |
qed |
|
236 |
||
237 |
end |
|
238 |
||
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
239 |
text {* The definitions of @{text is_inf} and @{text is_sup} look |
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
240 |
like ordinary definitions in theories. Despite, what is going on |
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
241 |
behind the scenes is more complex. The definition of @{text |
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
242 |
is_inf}, say, creates a constant @{const partial_order.is_inf} where |
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
243 |
the locale parameters that occur in the definition of @{text is_inf} |
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
244 |
are additional arguments. Writing @{text "is_inf x y inf"} is just |
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
245 |
a notational convenience for @{text "partial_order.is_inf op \<sqsubseteq> x y |
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
246 |
inf"}. *} |
27063 | 247 |
|
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
248 |
text {* Two commands are provided to inspect locales: |
27063 | 249 |
\isakeyword{print\_locales} lists the names of all locales of the |
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
250 |
current theory; \isakeyword{print\_locale}~$n$ prints the parameters |
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
251 |
and assumptions of locale $n$; \isakeyword{print\_locale!}~$n$ |
27063 | 252 |
additionally outputs the conclusions. |
253 |
||
254 |
The syntax of the locale commands discussed in this tutorial is |
|
30780 | 255 |
shown in Table~\ref{tab:commands}. The grammer is complete with the |
256 |
exception of additional context elements not discussed here. See the |
|
27063 | 257 |
Isabelle/Isar Reference Manual~\cite{IsarRef} |
258 |
for full documentation. *} |
|
259 |
||
260 |
||
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
261 |
section {* Import \label{sec:import} *} |
27063 | 262 |
|
263 |
text {* |
|
264 |
Algebraic structures are commonly defined by adding operations and |
|
265 |
properties to existing structures. For example, partial orders |
|
266 |
are extended to lattices and total orders. Lattices are extended to |
|
267 |
distributive lattices. |
|
268 |
||
269 |
With locales, this inheritance is achieved through \emph{import} of a |
|
270 |
locale. The import comes before the context elements. |
|
271 |
*} |
|
272 |
||
273 |
locale lattice = partial_order + |
|
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
274 |
assumes ex_inf: "\<exists>inf. is_inf x y inf" |
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
275 |
and ex_sup: "\<exists>sup. is_sup x y sup" |
27063 | 276 |
begin |
277 |
||
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
278 |
text {* These assumptions refer to the predicates for infimum |
27063 | 279 |
and supremum defined in @{text partial_order}. In the current |
280 |
implementation of locales, syntax from definitions of the imported |
|
281 |
locale is unavailable in the locale declaration, neither are their |
|
282 |
names. Hence we refer to the constants of the theory. The names |
|
283 |
and syntax is available below, in the context of the locale. *} |
|
284 |
||
285 |
definition |
|
286 |
meet (infixl "\<sqinter>" 70) where "x \<sqinter> y = (THE inf. is_inf x y inf)" |
|
287 |
||
288 |
definition |
|
289 |
join (infixl "\<squnion>" 65) where "x \<squnion> y = (THE sup. is_sup x y sup)" |
|
290 |
||
291 |
lemma %invisible meet_equality [elim?]: "is_inf x y i \<Longrightarrow> x \<sqinter> y = i" |
|
292 |
proof (unfold meet_def) |
|
293 |
assume "is_inf x y i" |
|
294 |
then show "(THE i. is_inf x y i) = i" |
|
295 |
by (rule the_equality) (rule is_inf_uniq [OF _ `is_inf x y i`]) |
|
296 |
qed |
|
297 |
||
298 |
lemma %invisible meetI [intro?]: |
|
299 |
"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" |
|
300 |
by (rule meet_equality, rule is_infI) blast+ |
|
301 |
||
302 |
lemma %invisible is_inf_meet [intro?]: "is_inf x y (x \<sqinter> y)" |
|
303 |
proof (unfold meet_def) |
|
304 |
from ex_inf obtain i where "is_inf x y i" .. |
|
305 |
then show "is_inf x y (THE i. is_inf x y i)" |
|
306 |
by (rule theI) (rule is_inf_uniq [OF _ `is_inf x y i`]) |
|
307 |
qed |
|
308 |
||
309 |
lemma %invisible meet_left [intro?]: |
|
310 |
"x \<sqinter> y \<sqsubseteq> x" |
|
311 |
by (rule is_inf_lower) (rule is_inf_meet) |
|
312 |
||
313 |
lemma %invisible meet_right [intro?]: |
|
314 |
"x \<sqinter> y \<sqsubseteq> y" |
|
315 |
by (rule is_inf_lower) (rule is_inf_meet) |
|
316 |
||
317 |
lemma %invisible meet_le [intro?]: |
|
318 |
"\<lbrakk> z \<sqsubseteq> x; z \<sqsubseteq> y \<rbrakk> \<Longrightarrow> z \<sqsubseteq> x \<sqinter> y" |
|
319 |
by (rule is_inf_greatest) (rule is_inf_meet) |
|
320 |
||
321 |
lemma %invisible join_equality [elim?]: "is_sup x y s \<Longrightarrow> x \<squnion> y = s" |
|
322 |
proof (unfold join_def) |
|
323 |
assume "is_sup x y s" |
|
324 |
then show "(THE s. is_sup x y s) = s" |
|
325 |
by (rule the_equality) (rule is_sup_uniq [OF _ `is_sup x y s`]) |
|
326 |
qed |
|
327 |
||
328 |
lemma %invisible joinI [intro?]: "x \<sqsubseteq> s \<Longrightarrow> y \<sqsubseteq> s \<Longrightarrow> |
|
329 |
(\<And>z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> s \<sqsubseteq> z) \<Longrightarrow> x \<squnion> y = s" |
|
330 |
by (rule join_equality, rule is_supI) blast+ |
|
331 |
||
332 |
lemma %invisible is_sup_join [intro?]: "is_sup x y (x \<squnion> y)" |
|
333 |
proof (unfold join_def) |
|
334 |
from ex_sup obtain s where "is_sup x y s" .. |
|
335 |
then show "is_sup x y (THE s. is_sup x y s)" |
|
336 |
by (rule theI) (rule is_sup_uniq [OF _ `is_sup x y s`]) |
|
337 |
qed |
|
338 |
||
339 |
lemma %invisible join_left [intro?]: |
|
340 |
"x \<sqsubseteq> x \<squnion> y" |
|
341 |
by (rule is_sup_upper) (rule is_sup_join) |
|
342 |
||
343 |
lemma %invisible join_right [intro?]: |
|
344 |
"y \<sqsubseteq> x \<squnion> y" |
|
345 |
by (rule is_sup_upper) (rule is_sup_join) |
|
346 |
||
347 |
lemma %invisible join_le [intro?]: |
|
348 |
"\<lbrakk> x \<sqsubseteq> z; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<squnion> y \<sqsubseteq> z" |
|
349 |
by (rule is_sup_least) (rule is_sup_join) |
|
350 |
||
351 |
theorem %invisible meet_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)" |
|
352 |
proof (rule meetI) |
|
353 |
show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x \<sqinter> y" |
|
354 |
proof |
|
355 |
show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> x" .. |
|
356 |
show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y" |
|
357 |
proof - |
|
358 |
have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" .. |
|
359 |
also have "\<dots> \<sqsubseteq> y" .. |
|
360 |
finally show ?thesis . |
|
361 |
qed |
|
362 |
qed |
|
363 |
show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> z" |
|
364 |
proof - |
|
365 |
have "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> y \<sqinter> z" .. |
|
366 |
also have "\<dots> \<sqsubseteq> z" .. |
|
367 |
finally show ?thesis . |
|
368 |
qed |
|
369 |
fix w assume "w \<sqsubseteq> x \<sqinter> y" and "w \<sqsubseteq> z" |
|
370 |
show "w \<sqsubseteq> x \<sqinter> (y \<sqinter> z)" |
|
371 |
proof |
|
372 |
show "w \<sqsubseteq> x" |
|
373 |
proof - |
|
374 |
have "w \<sqsubseteq> x \<sqinter> y" by fact |
|
375 |
also have "\<dots> \<sqsubseteq> x" .. |
|
376 |
finally show ?thesis . |
|
377 |
qed |
|
378 |
show "w \<sqsubseteq> y \<sqinter> z" |
|
379 |
proof |
|
380 |
show "w \<sqsubseteq> y" |
|
381 |
proof - |
|
382 |
have "w \<sqsubseteq> x \<sqinter> y" by fact |
|
383 |
also have "\<dots> \<sqsubseteq> y" .. |
|
384 |
finally show ?thesis . |
|
385 |
qed |
|
386 |
show "w \<sqsubseteq> z" by fact |
|
387 |
qed |
|
388 |
qed |
|
389 |
qed |
|
390 |
||
391 |
theorem %invisible meet_commute: "x \<sqinter> y = y \<sqinter> x" |
|
392 |
proof (rule meetI) |
|
393 |
show "y \<sqinter> x \<sqsubseteq> x" .. |
|
394 |
show "y \<sqinter> x \<sqsubseteq> y" .. |
|
395 |
fix z assume "z \<sqsubseteq> y" and "z \<sqsubseteq> x" |
|
396 |
then show "z \<sqsubseteq> y \<sqinter> x" .. |
|
397 |
qed |
|
398 |
||
399 |
theorem %invisible meet_join_absorb: "x \<sqinter> (x \<squnion> y) = x" |
|
400 |
proof (rule meetI) |
|
401 |
show "x \<sqsubseteq> x" .. |
|
402 |
show "x \<sqsubseteq> x \<squnion> y" .. |
|
403 |
fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> x \<squnion> y" |
|
404 |
show "z \<sqsubseteq> x" by fact |
|
405 |
qed |
|
406 |
||
407 |
theorem %invisible join_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)" |
|
408 |
proof (rule joinI) |
|
409 |
show "x \<squnion> y \<sqsubseteq> x \<squnion> (y \<squnion> z)" |
|
410 |
proof |
|
411 |
show "x \<sqsubseteq> x \<squnion> (y \<squnion> z)" .. |
|
412 |
show "y \<sqsubseteq> x \<squnion> (y \<squnion> z)" |
|
413 |
proof - |
|
414 |
have "y \<sqsubseteq> y \<squnion> z" .. |
|
415 |
also have "... \<sqsubseteq> x \<squnion> (y \<squnion> z)" .. |
|
416 |
finally show ?thesis . |
|
417 |
qed |
|
418 |
qed |
|
419 |
show "z \<sqsubseteq> x \<squnion> (y \<squnion> z)" |
|
420 |
proof - |
|
421 |
have "z \<sqsubseteq> y \<squnion> z" .. |
|
422 |
also have "... \<sqsubseteq> x \<squnion> (y \<squnion> z)" .. |
|
423 |
finally show ?thesis . |
|
424 |
qed |
|
425 |
fix w assume "x \<squnion> y \<sqsubseteq> w" and "z \<sqsubseteq> w" |
|
426 |
show "x \<squnion> (y \<squnion> z) \<sqsubseteq> w" |
|
427 |
proof |
|
428 |
show "x \<sqsubseteq> w" |
|
429 |
proof - |
|
430 |
have "x \<sqsubseteq> x \<squnion> y" .. |
|
431 |
also have "\<dots> \<sqsubseteq> w" by fact |
|
432 |
finally show ?thesis . |
|
433 |
qed |
|
434 |
show "y \<squnion> z \<sqsubseteq> w" |
|
435 |
proof |
|
436 |
show "y \<sqsubseteq> w" |
|
437 |
proof - |
|
438 |
have "y \<sqsubseteq> x \<squnion> y" .. |
|
439 |
also have "... \<sqsubseteq> w" by fact |
|
440 |
finally show ?thesis . |
|
441 |
qed |
|
442 |
show "z \<sqsubseteq> w" by fact |
|
443 |
qed |
|
444 |
qed |
|
445 |
qed |
|
446 |
||
447 |
theorem %invisible join_commute: "x \<squnion> y = y \<squnion> x" |
|
448 |
proof (rule joinI) |
|
449 |
show "x \<sqsubseteq> y \<squnion> x" .. |
|
450 |
show "y \<sqsubseteq> y \<squnion> x" .. |
|
451 |
fix z assume "y \<sqsubseteq> z" and "x \<sqsubseteq> z" |
|
452 |
then show "y \<squnion> x \<sqsubseteq> z" .. |
|
453 |
qed |
|
454 |
||
455 |
theorem %invisible join_meet_absorb: "x \<squnion> (x \<sqinter> y) = x" |
|
456 |
proof (rule joinI) |
|
457 |
show "x \<sqsubseteq> x" .. |
|
458 |
show "x \<sqinter> y \<sqsubseteq> x" .. |
|
459 |
fix z assume "x \<sqsubseteq> z" and "x \<sqinter> y \<sqsubseteq> z" |
|
460 |
show "x \<sqsubseteq> z" by fact |
|
461 |
qed |
|
462 |
||
463 |
theorem %invisible meet_idem: "x \<sqinter> x = x" |
|
464 |
proof - |
|
465 |
have "x \<sqinter> (x \<squnion> (x \<sqinter> x)) = x" by (rule meet_join_absorb) |
|
466 |
also have "x \<squnion> (x \<sqinter> x) = x" by (rule join_meet_absorb) |
|
467 |
finally show ?thesis . |
|
468 |
qed |
|
469 |
||
470 |
theorem %invisible meet_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x" |
|
471 |
proof (rule meetI) |
|
472 |
assume "x \<sqsubseteq> y" |
|
473 |
show "x \<sqsubseteq> x" .. |
|
474 |
show "x \<sqsubseteq> y" by fact |
|
475 |
fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" |
|
476 |
show "z \<sqsubseteq> x" by fact |
|
477 |
qed |
|
478 |
||
479 |
theorem %invisible meet_related2 [elim?]: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y" |
|
480 |
by (drule meet_related) (simp add: meet_commute) |
|
481 |
||
482 |
theorem %invisible join_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y" |
|
483 |
proof (rule joinI) |
|
484 |
assume "x \<sqsubseteq> y" |
|
485 |
show "y \<sqsubseteq> y" .. |
|
486 |
show "x \<sqsubseteq> y" by fact |
|
487 |
fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z" |
|
488 |
show "y \<sqsubseteq> z" by fact |
|
489 |
qed |
|
490 |
||
491 |
theorem %invisible join_related2 [elim?]: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x" |
|
492 |
by (drule join_related) (simp add: join_commute) |
|
493 |
||
494 |
theorem %invisible meet_connection: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)" |
|
495 |
proof |
|
496 |
assume "x \<sqsubseteq> y" |
|
497 |
then have "is_inf x y x" .. |
|
498 |
then show "x \<sqinter> y = x" .. |
|
499 |
next |
|
500 |
have "x \<sqinter> y \<sqsubseteq> y" .. |
|
501 |
also assume "x \<sqinter> y = x" |
|
502 |
finally show "x \<sqsubseteq> y" . |
|
503 |
qed |
|
504 |
||
505 |
theorem %invisible join_connection: "(x \<sqsubseteq> y) = (x \<squnion> y = y)" |
|
506 |
proof |
|
507 |
assume "x \<sqsubseteq> y" |
|
508 |
then have "is_sup x y y" .. |
|
509 |
then show "x \<squnion> y = y" .. |
|
510 |
next |
|
511 |
have "x \<sqsubseteq> x \<squnion> y" .. |
|
512 |
also assume "x \<squnion> y = y" |
|
513 |
finally show "x \<sqsubseteq> y" . |
|
514 |
qed |
|
515 |
||
516 |
theorem %invisible meet_connection2: "(x \<sqsubseteq> y) = (y \<sqinter> x = x)" |
|
517 |
using meet_commute meet_connection by simp |
|
518 |
||
519 |
theorem %invisible join_connection2: "(x \<sqsubseteq> y) = (x \<squnion> y = y)" |
|
520 |
using join_commute join_connection by simp |
|
521 |
||
522 |
text %invisible {* Naming according to Jacobson I, p.\ 459. *} |
|
523 |
lemmas %invisible L1 = join_commute meet_commute |
|
524 |
lemmas %invisible L2 = join_assoc meet_assoc |
|
525 |
(* lemmas L3 = join_idem meet_idem *) |
|
526 |
lemmas %invisible L4 = join_meet_absorb meet_join_absorb |
|
527 |
||
528 |
end |
|
529 |
||
530 |
text {* Locales for total orders and distributive lattices follow. |
|
531 |
Each comes with an example theorem. *} |
|
532 |
||
533 |
locale total_order = partial_order + |
|
534 |
assumes total: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x" |
|
535 |
||
536 |
lemma (in total_order) less_total: "x \<sqsubset> y \<or> x = y \<or> y \<sqsubset> x" |
|
537 |
using total |
|
538 |
by (unfold less_def) blast |
|
539 |
||
540 |
locale distrib_lattice = lattice + |
|
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
541 |
assumes meet_distr: "x \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> z" |
27063 | 542 |
|
543 |
lemma (in distrib_lattice) join_distr: |
|
544 |
"x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" (* txt {* Jacobson I, p.\ 462 *} *) |
|
545 |
proof - |
|
546 |
have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by (simp add: L4) |
|
547 |
also have "... = x \<squnion> ((x \<sqinter> z) \<squnion> (y \<sqinter> z))" by (simp add: L2) |
|
548 |
also have "... = x \<squnion> ((x \<squnion> y) \<sqinter> z)" by (simp add: L1 meet_distr) |
|
549 |
also have "... = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)" by (simp add: L1 L4) |
|
550 |
also have "... = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by (simp add: meet_distr) |
|
551 |
finally show ?thesis . |
|
552 |
qed |
|
553 |
||
554 |
text {* |
|
555 |
The locale hierachy obtained through these declarations is shown in Figure~\ref{fig:lattices}(a). |
|
556 |
||
557 |
\begin{figure} |
|
558 |
\hrule \vspace{2ex} |
|
559 |
\begin{center} |
|
560 |
\subfigure[Declared hierachy]{ |
|
561 |
\begin{tikzpicture} |
|
562 |
\node (po) at (0,0) {@{text partial_order}}; |
|
563 |
\node (lat) at (-1.5,-1) {@{text lattice}}; |
|
564 |
\node (dlat) at (-1.5,-2) {@{text distrib_lattice}}; |
|
565 |
\node (to) at (1.5,-1) {@{text total_order}}; |
|
566 |
\draw (po) -- (lat); |
|
567 |
\draw (lat) -- (dlat); |
|
568 |
\draw (po) -- (to); |
|
569 |
% \draw[->, dashed] (lat) -- (to); |
|
570 |
\end{tikzpicture} |
|
571 |
} \\ |
|
572 |
\subfigure[Total orders are lattices]{ |
|
573 |
\begin{tikzpicture} |
|
574 |
\node (po) at (0,0) {@{text partial_order}}; |
|
575 |
\node (lat) at (0,-1) {@{text lattice}}; |
|
576 |
\node (dlat) at (-1.5,-2) {@{text distrib_lattice}}; |
|
577 |
\node (to) at (1.5,-2) {@{text total_order}}; |
|
578 |
\draw (po) -- (lat); |
|
579 |
\draw (lat) -- (dlat); |
|
580 |
\draw (lat) -- (to); |
|
581 |
% \draw[->, dashed] (dlat) -- (to); |
|
582 |
\end{tikzpicture} |
|
583 |
} \quad |
|
584 |
\subfigure[Total orders are distributive lattices]{ |
|
585 |
\begin{tikzpicture} |
|
586 |
\node (po) at (0,0) {@{text partial_order}}; |
|
587 |
\node (lat) at (0,-1) {@{text lattice}}; |
|
588 |
\node (dlat) at (0,-2) {@{text distrib_lattice}}; |
|
589 |
\node (to) at (0,-3) {@{text total_order}}; |
|
590 |
\draw (po) -- (lat); |
|
591 |
\draw (lat) -- (dlat); |
|
592 |
\draw (dlat) -- (to); |
|
593 |
\end{tikzpicture} |
|
594 |
} |
|
595 |
\end{center} |
|
596 |
\hrule |
|
597 |
\caption{Hierarchy of Lattice Locales.} |
|
598 |
\label{fig:lattices} |
|
599 |
\end{figure} |
|
600 |
*} |
|
601 |
||
30580
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
602 |
section {* Changing the Locale Hierarchy |
cc5a55d7a5be
Updated chapters 1-5 to locale reimplementation.
ballarin
parents:
30393
diff
changeset
|
603 |
\label{sec:changing-the-hierarchy} *} |
27063 | 604 |
|
605 |
text {* |
|
606 |
Total orders are lattices. Hence, by deriving the lattice |
|
607 |
axioms for total orders, the hierarchy may be changed |
|
608 |
and @{text lattice} be placed between @{text partial_order} |
|
609 |
and @{text total_order}, as shown in Figure~\ref{fig:lattices}(b). |
|
610 |
Changes to the locale hierarchy may be declared |
|
29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27375
diff
changeset
|
611 |
with the \isakeyword{sublocale} command. *} |
27063 | 612 |
|
29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27375
diff
changeset
|
613 |
sublocale %visible total_order \<subseteq> lattice |
27063 | 614 |
|
615 |
txt {* This enters the context of locale @{text total_order}, in |
|
616 |
which the goal @{subgoals [display]} must be shown. First, the |
|
617 |
locale predicate needs to be unfolded --- for example using its |
|
618 |
definition or by introduction rules |
|
619 |
provided by the locale package. The methods @{text intro_locales} |
|
620 |
and @{text unfold_locales} automate this. They are aware of the |
|
621 |
current context and dependencies between locales and automatically |
|
622 |
discharge goals implied by these. While @{text unfold_locales} |
|
623 |
always unfolds locale predicates to assumptions, @{text |
|
624 |
intro_locales} only unfolds definitions along the locale |
|
625 |
hierarchy, leaving a goal consisting of predicates defined by the |
|
626 |
locale package. Occasionally the latter is of advantage since the goal |
|
627 |
is smaller. |
|
628 |
||
629 |
For the current goal, we would like to get hold of |
|
630 |
the assumptions of @{text lattice}, hence @{text unfold_locales} |
|
631 |
is appropriate. *} |
|
632 |
||
633 |
proof unfold_locales |
|
634 |
||
635 |
txt {* Since both @{text lattice} and @{text total_order} |
|
636 |
inherit @{text partial_order}, the assumptions of the latter are |
|
637 |
discharged, and the only subgoals that remain are the assumptions |
|
638 |
introduced in @{text lattice} @{subgoals [display]} |
|
639 |
The proof for the first subgoal is *} |
|
640 |
||
641 |
fix x y |
|
642 |
from total have "is_inf x y (if x \<sqsubseteq> y then x else y)" |
|
643 |
by (auto simp: is_inf_def) |
|
644 |
then show "\<exists>inf. is_inf x y inf" .. |
|
645 |
txt {* The proof for the second subgoal is analogous and not |
|
646 |
reproduced here. *} |
|
647 |
next %invisible |
|
648 |
fix x y |
|
649 |
from total have "is_sup x y (if x \<sqsubseteq> y then y else x)" |
|
650 |
by (auto simp: is_sup_def) |
|
651 |
then show "\<exists>sup. is_sup x y sup" .. qed %visible |
|
652 |
||
653 |
text {* Similarly, total orders are distributive lattices. *} |
|
654 |
||
29566
937baa077df2
Fixed tutorial to compile with new locales; grammar of new locale commands.
ballarin
parents:
27375
diff
changeset
|
655 |
sublocale total_order \<subseteq> distrib_lattice |
27063 | 656 |
proof unfold_locales |
657 |
fix %"proof" x y z |
|
658 |
show "x \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> z" (is "?l = ?r") |
|
659 |
txt {* Jacobson I, p.\ 462 *} |
|
660 |
proof - |
|
661 |
{ assume c: "y \<sqsubseteq> x" "z \<sqsubseteq> x" |
|
662 |
from c have "?l = y \<squnion> z" |
|
663 |
by (metis c join_connection2 join_related2 meet_related2 total) |
|
664 |
also from c have "... = ?r" by (metis meet_related2) |
|
665 |
finally have "?l = ?r" . } |
|
666 |
moreover |
|
667 |
{ assume c: "x \<sqsubseteq> y \<or> x \<sqsubseteq> z" |
|
668 |
from c have "?l = x" |
|
669 |
by (metis join_connection2 join_related2 meet_connection total trans) |
|
670 |
also from c have "... = ?r" |
|
671 |
by (metis join_commute join_related2 meet_connection meet_related2 total) |
|
672 |
finally have "?l = ?r" . } |
|
673 |
moreover note total |
|
674 |
ultimately show ?thesis by blast |
|
675 |
qed |
|
676 |
qed |
|
677 |
||
678 |
text {* The locale hierarchy is now as shown in Figure~\ref{fig:lattices}(c). *} |
|
679 |
||
680 |
end |