14738
|
1 |
(* Title: HOL/LOrder.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Steven Obua, TU Muenchen
|
|
4 |
*)
|
|
5 |
|
21312
|
6 |
header "Lattice Orders"
|
14738
|
7 |
|
15131
|
8 |
theory LOrder
|
21249
|
9 |
imports Lattices
|
15131
|
10 |
begin
|
14738
|
11 |
|
21312
|
12 |
text {* The theory of lattices developed here is taken from
|
|
13 |
\cite{Birkhoff79}. *}
|
14738
|
14 |
|
|
15 |
constdefs
|
|
16 |
is_meet :: "(('a::order) \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
|
|
17 |
"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)"
|
|
18 |
is_join :: "(('a::order) \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
|
|
19 |
"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)"
|
|
20 |
|
|
21 |
lemma is_meet_unique:
|
|
22 |
assumes "is_meet u" "is_meet v" shows "u = v"
|
|
23 |
proof -
|
|
24 |
{
|
|
25 |
fix a b :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
|
|
26 |
assume a: "is_meet a"
|
|
27 |
assume b: "is_meet b"
|
|
28 |
{
|
|
29 |
fix x y
|
|
30 |
let ?za = "a x y"
|
|
31 |
let ?zb = "b x y"
|
|
32 |
from a have za_le: "?za <= x & ?za <= y" by (auto simp add: is_meet_def)
|
|
33 |
with b have "?za <= ?zb" by (auto simp add: is_meet_def)
|
|
34 |
}
|
|
35 |
}
|
|
36 |
note f_le = this
|
|
37 |
show "u = v" by ((rule ext)+, simp_all add: order_antisym prems f_le)
|
|
38 |
qed
|
|
39 |
|
|
40 |
lemma is_join_unique:
|
|
41 |
assumes "is_join u" "is_join v" shows "u = v"
|
|
42 |
proof -
|
|
43 |
{
|
|
44 |
fix a b :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
|
|
45 |
assume a: "is_join a"
|
|
46 |
assume b: "is_join b"
|
|
47 |
{
|
|
48 |
fix x y
|
|
49 |
let ?za = "a x y"
|
|
50 |
let ?zb = "b x y"
|
|
51 |
from a have za_le: "x <= ?za & y <= ?za" by (auto simp add: is_join_def)
|
|
52 |
with b have "?zb <= ?za" by (auto simp add: is_join_def)
|
|
53 |
}
|
|
54 |
}
|
|
55 |
note f_le = this
|
|
56 |
show "u = v" by ((rule ext)+, simp_all add: order_antisym prems f_le)
|
|
57 |
qed
|
|
58 |
|
|
59 |
axclass join_semilorder < order
|
|
60 |
join_exists: "? j. is_join j"
|
|
61 |
|
|
62 |
axclass meet_semilorder < order
|
|
63 |
meet_exists: "? m. is_meet m"
|
|
64 |
|
|
65 |
axclass lorder < join_semilorder, meet_semilorder
|
|
66 |
|
|
67 |
constdefs
|
|
68 |
meet :: "('a::meet_semilorder) \<Rightarrow> 'a \<Rightarrow> 'a"
|
|
69 |
"meet == THE m. is_meet m"
|
|
70 |
join :: "('a::join_semilorder) \<Rightarrow> 'a \<Rightarrow> 'a"
|
|
71 |
"join == THE j. is_join j"
|
|
72 |
|
|
73 |
lemma is_meet_meet: "is_meet (meet::'a \<Rightarrow> 'a \<Rightarrow> ('a::meet_semilorder))"
|
|
74 |
proof -
|
|
75 |
from meet_exists obtain k::"'a \<Rightarrow> 'a \<Rightarrow> 'a" where "is_meet k" ..
|
|
76 |
with is_meet_unique[of _ k] show ?thesis
|
|
77 |
by (simp add: meet_def theI[of is_meet])
|
|
78 |
qed
|
|
79 |
|
|
80 |
lemma meet_unique: "(is_meet m) = (m = meet)"
|
|
81 |
by (insert is_meet_meet, auto simp add: is_meet_unique)
|
|
82 |
|
|
83 |
lemma is_join_join: "is_join (join::'a \<Rightarrow> 'a \<Rightarrow> ('a::join_semilorder))"
|
|
84 |
proof -
|
|
85 |
from join_exists obtain k::"'a \<Rightarrow> 'a \<Rightarrow> 'a" where "is_join k" ..
|
|
86 |
with is_join_unique[of _ k] show ?thesis
|
|
87 |
by (simp add: join_def theI[of is_join])
|
|
88 |
qed
|
|
89 |
|
|
90 |
lemma join_unique: "(is_join j) = (j = join)"
|
|
91 |
by (insert is_join_join, auto simp add: is_join_unique)
|
|
92 |
|
21380
|
93 |
interpretation lattice:
|
|
94 |
lattice ["op \<le> \<Colon> 'a\<Colon>lorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" meet join]
|
|
95 |
proof unfold_locales
|
|
96 |
fix x y z :: "'a\<Colon>lorder"
|
|
97 |
from is_meet_meet have "is_meet meet" by blast
|
|
98 |
note meet = this is_meet_def
|
|
99 |
from meet show "meet x y \<le> x" by blast
|
|
100 |
from meet show "meet x y \<le> y" by blast
|
|
101 |
from meet show "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> meet y z" by blast
|
|
102 |
from is_join_join have "is_join join" by blast
|
|
103 |
note join = this is_join_def
|
|
104 |
from join show "x \<le> join x y" by blast
|
|
105 |
from join show "y \<le> join x y" by blast
|
|
106 |
from join show "y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> join y z \<le> x" by blast
|
|
107 |
qed
|
|
108 |
|
14738
|
109 |
lemma meet_left_le: "meet a b \<le> (a::'a::meet_semilorder)"
|
|
110 |
by (insert is_meet_meet, auto simp add: is_meet_def)
|
|
111 |
|
|
112 |
lemma meet_right_le: "meet a b \<le> (b::'a::meet_semilorder)"
|
|
113 |
by (insert is_meet_meet, auto simp add: is_meet_def)
|
|
114 |
|
21312
|
115 |
(* intro! breaks a proof in Hyperreal/SEQ and NumberTheory/IntPrimes *)
|
|
116 |
lemma le_meetI:
|
|
117 |
"x \<le> a \<Longrightarrow> x \<le> b \<Longrightarrow> x \<le> meet a (b::'a::meet_semilorder)"
|
14738
|
118 |
by (insert is_meet_meet, auto simp add: is_meet_def)
|
|
119 |
|
|
120 |
lemma join_left_le: "a \<le> join a (b::'a::join_semilorder)"
|
|
121 |
by (insert is_join_join, auto simp add: is_join_def)
|
|
122 |
|
|
123 |
lemma join_right_le: "b \<le> join a (b::'a::join_semilorder)"
|
|
124 |
by (insert is_join_join, auto simp add: is_join_def)
|
|
125 |
|
21312
|
126 |
lemma join_leI:
|
|
127 |
"a \<le> x \<Longrightarrow> b \<le> x \<Longrightarrow> join a b \<le> (x::'a::join_semilorder)"
|
14738
|
128 |
by (insert is_join_join, auto simp add: is_join_def)
|
|
129 |
|
21312
|
130 |
lemmas meet_join_le[simp] = meet_left_le meet_right_le join_left_le join_right_le
|
|
131 |
|
|
132 |
lemma le_meet[simp]: "(x <= meet y z) = (x <= y & x <= z)" (is "?L = ?R")
|
|
133 |
proof
|
|
134 |
assume ?L
|
|
135 |
moreover have "meet y z \<le> y" "meet y z <= z" by(simp_all)
|
|
136 |
ultimately show ?R by(blast intro:order_trans)
|
|
137 |
next
|
|
138 |
assume ?R thus ?L by (blast intro!:le_meetI)
|
|
139 |
qed
|
|
140 |
|
|
141 |
lemma join_le[simp]: "(join x y <= z) = (x <= z & y <= z)" (is "?L = ?R")
|
|
142 |
proof
|
|
143 |
assume ?L
|
|
144 |
moreover have "x \<le> join x y" "y \<le> join x y" by(simp_all)
|
|
145 |
ultimately show ?R by(blast intro:order_trans)
|
|
146 |
next
|
|
147 |
assume ?R thus ?L by (blast intro:join_leI)
|
|
148 |
qed
|
|
149 |
|
14738
|
150 |
|
|
151 |
lemma is_meet_min: "is_meet (min::'a \<Rightarrow> 'a \<Rightarrow> ('a::linorder))"
|
|
152 |
by (auto simp add: is_meet_def min_def)
|
|
153 |
|
|
154 |
lemma is_join_max: "is_join (max::'a \<Rightarrow> 'a \<Rightarrow> ('a::linorder))"
|
|
155 |
by (auto simp add: is_join_def max_def)
|
|
156 |
|
|
157 |
instance linorder \<subseteq> meet_semilorder
|
|
158 |
proof
|
|
159 |
from is_meet_min show "? (m::'a\<Rightarrow>'a\<Rightarrow>('a::linorder)). is_meet m" by auto
|
|
160 |
qed
|
|
161 |
|
|
162 |
instance linorder \<subseteq> join_semilorder
|
|
163 |
proof
|
|
164 |
from is_join_max show "? (j::'a\<Rightarrow>'a\<Rightarrow>('a::linorder)). is_join j" by auto
|
|
165 |
qed
|
|
166 |
|
|
167 |
instance linorder \<subseteq> lorder ..
|
|
168 |
|
|
169 |
lemma meet_min: "meet = (min :: 'a\<Rightarrow>'a\<Rightarrow>('a::linorder))"
|
|
170 |
by (simp add: is_meet_meet is_meet_min is_meet_unique)
|
|
171 |
|
|
172 |
lemma join_max: "join = (max :: 'a\<Rightarrow>'a\<Rightarrow>('a::linorder))"
|
|
173 |
by (simp add: is_join_join is_join_max is_join_unique)
|
|
174 |
|
|
175 |
lemma meet_idempotent[simp]: "meet x x = x"
|
21312
|
176 |
by (rule order_antisym, simp_all add: le_meetI)
|
14738
|
177 |
|
|
178 |
lemma join_idempotent[simp]: "join x x = x"
|
21312
|
179 |
by (rule order_antisym, simp_all add: join_leI)
|
14738
|
180 |
|
|
181 |
lemma meet_comm: "meet x y = meet y x"
|
21312
|
182 |
by (rule order_antisym, (simp add: le_meetI)+)
|
14738
|
183 |
|
|
184 |
lemma join_comm: "join x y = join y x"
|
21312
|
185 |
by (rule order_antisym, (simp add: join_leI)+)
|
|
186 |
|
|
187 |
lemma meet_leI1: "x \<le> z \<Longrightarrow> meet x y \<le> z"
|
|
188 |
apply(subgoal_tac "meet x y <= x")
|
|
189 |
apply(blast intro:order_trans)
|
|
190 |
apply simp
|
|
191 |
done
|
|
192 |
|
|
193 |
lemma meet_leI2: "y \<le> z \<Longrightarrow> meet x y \<le> z"
|
|
194 |
apply(subgoal_tac "meet x y <= y")
|
|
195 |
apply(blast intro:order_trans)
|
|
196 |
apply simp
|
|
197 |
done
|
14738
|
198 |
|
21312
|
199 |
lemma le_joinI1: "x \<le> y \<Longrightarrow> x \<le> join y z"
|
|
200 |
apply(subgoal_tac "y <= join y z")
|
|
201 |
apply(blast intro:order_trans)
|
|
202 |
apply simp
|
|
203 |
done
|
|
204 |
|
|
205 |
lemma le_joinI2: "x \<le> z \<Longrightarrow> x \<le> join y z"
|
|
206 |
apply(subgoal_tac "z <= join y z")
|
|
207 |
apply(blast intro:order_trans)
|
|
208 |
apply simp
|
|
209 |
done
|
14738
|
210 |
|
21312
|
211 |
lemma meet_assoc: "meet (meet x y) z = meet x (meet y z)"
|
|
212 |
apply(rule order_antisym)
|
|
213 |
apply (simp add:meet_leI1 meet_leI2)
|
|
214 |
apply (simp add:meet_leI1 meet_leI2)
|
|
215 |
done
|
|
216 |
|
|
217 |
lemma join_assoc: "join (join x y) z = join x (join y z)"
|
|
218 |
apply(rule order_antisym)
|
|
219 |
apply (simp add:le_joinI1 le_joinI2)
|
|
220 |
apply (simp add:le_joinI1 le_joinI2)
|
|
221 |
done
|
14738
|
222 |
|
|
223 |
lemma meet_left_comm: "meet a (meet b c) = meet b (meet a c)"
|
|
224 |
by (simp add: meet_assoc[symmetric, of a b c], simp add: meet_comm[of a b], simp add: meet_assoc)
|
|
225 |
|
|
226 |
lemma meet_left_idempotent: "meet y (meet y x) = meet y x"
|
|
227 |
by (simp add: meet_assoc meet_comm meet_left_comm)
|
|
228 |
|
|
229 |
lemma join_left_comm: "join a (join b c) = join b (join a c)"
|
|
230 |
by (simp add: join_assoc[symmetric, of a b c], simp add: join_comm[of a b], simp add: join_assoc)
|
|
231 |
|
|
232 |
lemma join_left_idempotent: "join y (join y x) = join y x"
|
|
233 |
by (simp add: join_assoc join_comm join_left_comm)
|
|
234 |
|
|
235 |
lemmas meet_aci = meet_assoc meet_comm meet_left_comm meet_left_idempotent
|
|
236 |
|
|
237 |
lemmas join_aci = join_assoc join_comm join_left_comm join_left_idempotent
|
|
238 |
|
21312
|
239 |
lemma le_def_meet: "(x <= y) = (meet x y = x)"
|
|
240 |
apply rule
|
|
241 |
apply(simp add: order_antisym)
|
|
242 |
apply(subgoal_tac "meet x y <= y")
|
|
243 |
apply(simp)
|
|
244 |
apply(simp (no_asm))
|
|
245 |
done
|
14738
|
246 |
|
21312
|
247 |
lemma le_def_join: "(x <= y) = (join x y = y)"
|
|
248 |
apply rule
|
|
249 |
apply(simp add: order_antisym)
|
|
250 |
apply(subgoal_tac "x <= join x y")
|
|
251 |
apply(simp)
|
|
252 |
apply(simp (no_asm))
|
|
253 |
done
|
|
254 |
|
|
255 |
lemma join_absorp2: "a \<le> b \<Longrightarrow> join a b = b"
|
|
256 |
by (simp add: le_def_join)
|
|
257 |
|
|
258 |
lemma join_absorp1: "b \<le> a \<Longrightarrow> join a b = a"
|
|
259 |
by (simp add: le_def_join join_aci)
|
|
260 |
|
|
261 |
lemma meet_absorp1: "a \<le> b \<Longrightarrow> meet a b = a"
|
|
262 |
by (simp add: le_def_meet)
|
|
263 |
|
|
264 |
lemma meet_absorp2: "b \<le> a \<Longrightarrow> meet a b = b"
|
|
265 |
by (simp add: le_def_meet meet_aci)
|
14738
|
266 |
|
|
267 |
lemma meet_join_absorp: "meet x (join x y) = x"
|
21312
|
268 |
by(simp add:meet_absorp1)
|
14738
|
269 |
|
|
270 |
lemma join_meet_absorp: "join x (meet x y) = x"
|
21312
|
271 |
by(simp add:join_absorp1)
|
14738
|
272 |
|
|
273 |
lemma meet_mono: "y \<le> z \<Longrightarrow> meet x y \<le> meet x z"
|
21312
|
274 |
by(simp add:meet_leI2)
|
14738
|
275 |
|
|
276 |
lemma join_mono: "y \<le> z \<Longrightarrow> join x y \<le> join x z"
|
21312
|
277 |
by(simp add:le_joinI2)
|
14738
|
278 |
|
|
279 |
lemma distrib_join_le: "join x (meet y z) \<le> meet (join x y) (join x z)" (is "_ <= ?r")
|
|
280 |
proof -
|
21312
|
281 |
have a: "x <= ?r" by (simp_all add:le_meetI)
|
|
282 |
have b: "meet y z <= ?r" by (simp add:le_joinI2)
|
|
283 |
from a b show ?thesis by (simp add: join_leI)
|
14738
|
284 |
qed
|
|
285 |
|
21312
|
286 |
lemma distrib_meet_le: "join (meet x y) (meet x z) \<le> meet x (join y z)" (is "?l <= _")
|
14738
|
287 |
proof -
|
21312
|
288 |
have a: "?l <= x" by (simp_all add: join_leI)
|
|
289 |
have b: "?l <= join y z" by (simp add:meet_leI2)
|
|
290 |
from a b show ?thesis by (simp add: le_meetI)
|
14738
|
291 |
qed
|
|
292 |
|
|
293 |
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"
|
21312
|
294 |
by (auto simp:meet_leI2 meet_leI1)
|
14738
|
295 |
|
|
296 |
lemma modular_le: "x \<le> z \<Longrightarrow> join x (meet y z) \<le> meet (join x y) z" (is "_ \<Longrightarrow> ?t <= _")
|
|
297 |
proof -
|
|
298 |
assume a: "x <= z"
|
21312
|
299 |
have b: "?t <= join x y" by (simp_all add: join_leI meet_join_eq_imp_le )
|
|
300 |
have c: "?t <= z" by (simp_all add: a join_leI)
|
|
301 |
from b c show ?thesis by (simp add: le_meetI)
|
14738
|
302 |
qed
|
|
303 |
|
15131
|
304 |
end
|