1 (* Title: HOL/LOrder.thy
3 Author: Steven Obua, TU Muenchen
4 License: GPL (GNU GENERAL PUBLIC LICENSE)
7 header {* Lattice Orders *}
12 The theory of lattices developed here is taken from the book:
14 \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979.
19 is_meet :: "(('a::order) \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
20 "is_meet m == ! a b x. m a b \<le> a \<and> m a b \<le> b \<and> (x \<le> a \<and> x \<le> b \<longrightarrow> x \<le> m a b)"
21 is_join :: "(('a::order) \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
22 "is_join j == ! a b x. a \<le> j a b \<and> b \<le> j a b \<and> (a \<le> x \<and> b \<le> x \<longrightarrow> j a b \<le> x)"
25 assumes "is_meet u" "is_meet v" shows "u = v"
28 fix a b :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
35 from a have za_le: "?za <= x & ?za <= y" by (auto simp add: is_meet_def)
36 with b have "?za <= ?zb" by (auto simp add: is_meet_def)
40 show "u = v" by ((rule ext)+, simp_all add: order_antisym prems f_le)
44 assumes "is_join u" "is_join v" shows "u = v"
47 fix a b :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
54 from a have za_le: "x <= ?za & y <= ?za" by (auto simp add: is_join_def)
55 with b have "?zb <= ?za" by (auto simp add: is_join_def)
59 show "u = v" by ((rule ext)+, simp_all add: order_antisym prems f_le)
62 axclass join_semilorder < order
63 join_exists: "? j. is_join j"
65 axclass meet_semilorder < order
66 meet_exists: "? m. is_meet m"
68 axclass lorder < join_semilorder, meet_semilorder
71 meet :: "('a::meet_semilorder) \<Rightarrow> 'a \<Rightarrow> 'a"
72 "meet == THE m. is_meet m"
73 join :: "('a::join_semilorder) \<Rightarrow> 'a \<Rightarrow> 'a"
74 "join == THE j. is_join j"
76 lemma is_meet_meet: "is_meet (meet::'a \<Rightarrow> 'a \<Rightarrow> ('a::meet_semilorder))"
78 from meet_exists obtain k::"'a \<Rightarrow> 'a \<Rightarrow> 'a" where "is_meet k" ..
79 with is_meet_unique[of _ k] show ?thesis
80 by (simp add: meet_def theI[of is_meet])
83 lemma meet_unique: "(is_meet m) = (m = meet)"
84 by (insert is_meet_meet, auto simp add: is_meet_unique)
86 lemma is_join_join: "is_join (join::'a \<Rightarrow> 'a \<Rightarrow> ('a::join_semilorder))"
88 from join_exists obtain k::"'a \<Rightarrow> 'a \<Rightarrow> 'a" where "is_join k" ..
89 with is_join_unique[of _ k] show ?thesis
90 by (simp add: join_def theI[of is_join])
93 lemma join_unique: "(is_join j) = (j = join)"
94 by (insert is_join_join, auto simp add: is_join_unique)
96 lemma meet_left_le: "meet a b \<le> (a::'a::meet_semilorder)"
97 by (insert is_meet_meet, auto simp add: is_meet_def)
99 lemma meet_right_le: "meet a b \<le> (b::'a::meet_semilorder)"
100 by (insert is_meet_meet, auto simp add: is_meet_def)
102 lemma meet_imp_le: "x \<le> a \<Longrightarrow> x \<le> b \<Longrightarrow> x \<le> meet a (b::'a::meet_semilorder)"
103 by (insert is_meet_meet, auto simp add: is_meet_def)
105 lemma join_left_le: "a \<le> join a (b::'a::join_semilorder)"
106 by (insert is_join_join, auto simp add: is_join_def)
108 lemma join_right_le: "b \<le> join a (b::'a::join_semilorder)"
109 by (insert is_join_join, auto simp add: is_join_def)
111 lemma join_imp_le: "a \<le> x \<Longrightarrow> b \<le> x \<Longrightarrow> join a b \<le> (x::'a::join_semilorder)"
112 by (insert is_join_join, auto simp add: is_join_def)
114 lemmas meet_join_le = meet_left_le meet_right_le join_left_le join_right_le
116 lemma is_meet_min: "is_meet (min::'a \<Rightarrow> 'a \<Rightarrow> ('a::linorder))"
117 by (auto simp add: is_meet_def min_def)
119 lemma is_join_max: "is_join (max::'a \<Rightarrow> 'a \<Rightarrow> ('a::linorder))"
120 by (auto simp add: is_join_def max_def)
122 instance linorder \<subseteq> meet_semilorder
124 from is_meet_min show "? (m::'a\<Rightarrow>'a\<Rightarrow>('a::linorder)). is_meet m" by auto
127 instance linorder \<subseteq> join_semilorder
129 from is_join_max show "? (j::'a\<Rightarrow>'a\<Rightarrow>('a::linorder)). is_join j" by auto
132 instance linorder \<subseteq> lorder ..
134 lemma meet_min: "meet = (min :: 'a\<Rightarrow>'a\<Rightarrow>('a::linorder))"
135 by (simp add: is_meet_meet is_meet_min is_meet_unique)
137 lemma join_max: "join = (max :: 'a\<Rightarrow>'a\<Rightarrow>('a::linorder))"
138 by (simp add: is_join_join is_join_max is_join_unique)
140 lemma meet_idempotent[simp]: "meet x x = x"
141 by (rule order_antisym, simp_all add: meet_left_le meet_imp_le)
143 lemma join_idempotent[simp]: "join x x = x"
144 by (rule order_antisym, simp_all add: join_left_le join_imp_le)
146 lemma meet_comm: "meet x y = meet y x"
147 by (rule order_antisym, (simp add: meet_left_le meet_right_le meet_imp_le)+)
149 lemma join_comm: "join x y = join y x"
150 by (rule order_antisym, (simp add: join_right_le join_left_le join_imp_le)+)
152 lemma meet_assoc: "meet (meet x y) z = meet x (meet y z)" (is "?l=?r")
154 have "?l <= meet x y & meet x y <= x & ?l <= z & meet x y <= y" by (simp add: meet_left_le meet_right_le)
155 hence "?l <= x & ?l <= y & ?l <= z" by auto
156 hence "?l <= ?r" by (simp add: meet_imp_le)
157 hence a:"?l <= meet x (meet y z)" by (simp add: meet_imp_le)
158 have "?r <= meet y z & meet y z <= y & meet y z <= z & ?r <= x" by (simp add: meet_left_le meet_right_le)
159 hence "?r <= x & ?r <= y & ?r <= z" by (auto)
160 hence "?r <= meet x y & ?r <= z" by (simp add: meet_imp_le)
161 hence b:"?r <= ?l" by (simp add: meet_imp_le)
162 from a b show "?l = ?r" by auto
165 lemma join_assoc: "join (join x y) z = join x (join y z)" (is "?l=?r")
167 have "join x y <= ?l & x <= join x y & z <= ?l & y <= join x y" by (simp add: join_left_le join_right_le)
168 hence "x <= ?l & y <= ?l & z <= ?l" by auto
169 hence "join y z <= ?l & x <= ?l" by (simp add: join_imp_le)
170 hence a:"?r <= ?l" by (simp add: join_imp_le)
171 have "join y z <= ?r & y <= join y z & z <= join y z & x <= ?r" by (simp add: join_left_le join_right_le)
172 hence "y <= ?r & z <= ?r & x <= ?r" by auto
173 hence "join x y <= ?r & z <= ?r" by (simp add: join_imp_le)
174 hence b:"?l <= ?r" by (simp add: join_imp_le)
175 from a b show "?l = ?r" by auto
178 lemma meet_left_comm: "meet a (meet b c) = meet b (meet a c)"
179 by (simp add: meet_assoc[symmetric, of a b c], simp add: meet_comm[of a b], simp add: meet_assoc)
181 lemma meet_left_idempotent: "meet y (meet y x) = meet y x"
182 by (simp add: meet_assoc meet_comm meet_left_comm)
184 lemma join_left_comm: "join a (join b c) = join b (join a c)"
185 by (simp add: join_assoc[symmetric, of a b c], simp add: join_comm[of a b], simp add: join_assoc)
187 lemma join_left_idempotent: "join y (join y x) = join y x"
188 by (simp add: join_assoc join_comm join_left_comm)
190 lemmas meet_aci = meet_assoc meet_comm meet_left_comm meet_left_idempotent
192 lemmas join_aci = join_assoc join_comm join_left_comm join_left_idempotent
194 lemma le_def_meet: "(x <= y) = (meet x y = x)"
196 have u: "x <= y \<longrightarrow> meet x y = x"
199 hence "x <= meet x y & meet x y <= x" by (simp add: meet_imp_le meet_left_le)
200 thus "meet x y = x" by auto
202 have v:"meet x y = x \<longrightarrow> x <= y"
204 have a:"meet x y <= y" by (simp add: meet_right_le)
205 assume "meet x y = x"
206 hence "x = meet x y" by auto
207 with a show "x <= y" by (auto)
209 from u v show ?thesis by blast
212 lemma le_def_join: "(x <= y) = (join x y = y)"
214 have u: "x <= y \<longrightarrow> join x y = y"
217 hence "join x y <= y & y <= join x y" by (simp add: join_imp_le join_right_le)
218 thus "join x y = y" by auto
220 have v:"join x y = y \<longrightarrow> x <= y"
222 have a:"x <= join x y" by (simp add: join_left_le)
223 assume "join x y = y"
224 hence "y = join x y" by auto
225 with a show "x <= y" by (auto)
227 from u v show ?thesis by blast
230 lemma meet_join_absorp: "meet x (join x y) = x"
232 have a:"meet x (join x y) <= x" by (simp add: meet_left_le)
233 have b:"x <= meet x (join x y)" by (rule meet_imp_le, simp_all add: join_left_le)
234 from a b show ?thesis by auto
237 lemma join_meet_absorp: "join x (meet x y) = x"
239 have a:"x <= join x (meet x y)" by (simp add: join_left_le)
240 have b:"join x (meet x y) <= x" by (rule join_imp_le, simp_all add: meet_left_le)
241 from a b show ?thesis by auto
244 lemma meet_mono: "y \<le> z \<Longrightarrow> meet x y \<le> meet x z"
247 have "meet x y <= x & meet x y <= y" by (simp add: meet_left_le meet_right_le)
248 with a have "meet x y <= x & meet x y <= z" by auto
249 thus "meet x y <= meet x z" by (simp add: meet_imp_le)
252 lemma join_mono: "y \<le> z \<Longrightarrow> join x y \<le> join x z"
254 assume a: "y \<le> z"
255 have "x <= join x z & z <= join x z" by (simp add: join_left_le join_right_le)
256 with a have "x <= join x z & y <= join x z" by auto
257 thus "join x y <= join x z" by (simp add: join_imp_le)
260 lemma distrib_join_le: "join x (meet y z) \<le> meet (join x y) (join x z)" (is "_ <= ?r")
262 have a: "x <= ?r" by (rule meet_imp_le, simp_all add: join_left_le)
263 from meet_join_le have b: "meet y z <= ?r"
264 by (rule_tac meet_imp_le, (blast intro: order_trans)+)
265 from a b show ?thesis by (simp add: join_imp_le)
268 lemma distrib_meet_le: "join (meet x y) (meet x z) \<le> meet x (join y z)" (is "?l <= _")
270 have a: "?l <= x" by (rule join_imp_le, simp_all add: meet_left_le)
271 from meet_join_le have b: "?l <= join y z"
272 by (rule_tac join_imp_le, (blast intro: order_trans)+)
273 from a b show ?thesis by (simp add: meet_imp_le)
276 lemma meet_join_eq_imp_le: "a = c \<or> a = d \<or> b = c \<or> b = d \<Longrightarrow> meet a b \<le> join c d"
277 by (insert meet_join_le, blast intro: order_trans)
279 lemma modular_le: "x \<le> z \<Longrightarrow> join x (meet y z) \<le> meet (join x y) z" (is "_ \<Longrightarrow> ?t <= _")
282 have b: "?t <= join x y" by (rule join_imp_le, simp_all add: meet_join_le meet_join_eq_imp_le)
283 have c: "?t <= z" by (rule join_imp_le, simp_all add: meet_join_le a)
284 from b c show ?thesis by (simp add: meet_imp_le)
288 val is_meet_unique = thm "is_meet_unique";
289 val is_join_unique = thm "is_join_unique";
290 val join_exists = thm "join_exists";
291 val meet_exists = thm "meet_exists";
292 val is_meet_meet = thm "is_meet_meet";
293 val meet_unique = thm "meet_unique";
294 val is_join_join = thm "is_join_join";
295 val join_unique = thm "join_unique";
296 val meet_left_le = thm "meet_left_le";
297 val meet_right_le = thm "meet_right_le";
298 val meet_imp_le = thm "meet_imp_le";
299 val join_left_le = thm "join_left_le";
300 val join_right_le = thm "join_right_le";
301 val join_imp_le = thm "join_imp_le";
302 val meet_join_le = thms "meet_join_le";
303 val is_meet_min = thm "is_meet_min";
304 val is_join_max = thm "is_join_max";
305 val meet_min = thm "meet_min";
306 val join_max = thm "join_max";
307 val meet_idempotent = thm "meet_idempotent";
308 val join_idempotent = thm "join_idempotent";
309 val meet_comm = thm "meet_comm";
310 val join_comm = thm "join_comm";
311 val meet_assoc = thm "meet_assoc";
312 val join_assoc = thm "join_assoc";
313 val meet_left_comm = thm "meet_left_comm";
314 val meet_left_idempotent = thm "meet_left_idempotent";
315 val join_left_comm = thm "join_left_comm";
316 val join_left_idempotent = thm "join_left_idempotent";
317 val meet_aci = thms "meet_aci";
318 val join_aci = thms "join_aci";
319 val le_def_meet = thm "le_def_meet";
320 val le_def_join = thm "le_def_join";
321 val meet_join_absorp = thm "meet_join_absorp";
322 val join_meet_absorp = thm "join_meet_absorp";
323 val meet_mono = thm "meet_mono";
324 val join_mono = thm "join_mono";
325 val distrib_join_le = thm "distrib_join_le";
326 val distrib_meet_le = thm "distrib_meet_le";
327 val meet_join_eq_imp_le = thm "meet_join_eq_imp_le";
328 val modular_le = thm "modular_le";