14738

1 
(* Title: HOL/LOrder.thy


2 
ID: $Id$


3 
Author: Steven Obua, TU Muenchen


4 
*)


5 


6 
header {* Lattice Orders *}


7 

15131

8 
theory LOrder

15140

9 
imports HOL

15131

10 
begin

14738

11 


12 
text {*


13 
The theory of lattices developed here is taken from the book:


14 
\begin{itemize}


15 
\item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979.


16 
\end{itemize}


17 
*}


18 


19 
constdefs


20 
is_meet :: "(('a::order) \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"


21 
"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)"


22 
is_join :: "(('a::order) \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"


23 
"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)"


24 


25 
lemma is_meet_unique:


26 
assumes "is_meet u" "is_meet v" shows "u = v"


27 
proof 


28 
{


29 
fix a b :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"


30 
assume a: "is_meet a"


31 
assume b: "is_meet b"


32 
{


33 
fix x y


34 
let ?za = "a x y"


35 
let ?zb = "b x y"


36 
from a have za_le: "?za <= x & ?za <= y" by (auto simp add: is_meet_def)


37 
with b have "?za <= ?zb" by (auto simp add: is_meet_def)


38 
}


39 
}


40 
note f_le = this


41 
show "u = v" by ((rule ext)+, simp_all add: order_antisym prems f_le)


42 
qed


43 


44 
lemma is_join_unique:


45 
assumes "is_join u" "is_join v" shows "u = v"


46 
proof 


47 
{


48 
fix a b :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"


49 
assume a: "is_join a"


50 
assume b: "is_join b"


51 
{


52 
fix x y


53 
let ?za = "a x y"


54 
let ?zb = "b x y"


55 
from a have za_le: "x <= ?za & y <= ?za" by (auto simp add: is_join_def)


56 
with b have "?zb <= ?za" by (auto simp add: is_join_def)


57 
}


58 
}


59 
note f_le = this


60 
show "u = v" by ((rule ext)+, simp_all add: order_antisym prems f_le)


61 
qed


62 


63 
axclass join_semilorder < order


64 
join_exists: "? j. is_join j"


65 


66 
axclass meet_semilorder < order


67 
meet_exists: "? m. is_meet m"


68 


69 
axclass lorder < join_semilorder, meet_semilorder


70 


71 
constdefs


72 
meet :: "('a::meet_semilorder) \<Rightarrow> 'a \<Rightarrow> 'a"


73 
"meet == THE m. is_meet m"


74 
join :: "('a::join_semilorder) \<Rightarrow> 'a \<Rightarrow> 'a"


75 
"join == THE j. is_join j"


76 


77 
lemma is_meet_meet: "is_meet (meet::'a \<Rightarrow> 'a \<Rightarrow> ('a::meet_semilorder))"


78 
proof 


79 
from meet_exists obtain k::"'a \<Rightarrow> 'a \<Rightarrow> 'a" where "is_meet k" ..


80 
with is_meet_unique[of _ k] show ?thesis


81 
by (simp add: meet_def theI[of is_meet])


82 
qed


83 


84 
lemma meet_unique: "(is_meet m) = (m = meet)"


85 
by (insert is_meet_meet, auto simp add: is_meet_unique)


86 


87 
lemma is_join_join: "is_join (join::'a \<Rightarrow> 'a \<Rightarrow> ('a::join_semilorder))"


88 
proof 


89 
from join_exists obtain k::"'a \<Rightarrow> 'a \<Rightarrow> 'a" where "is_join k" ..


90 
with is_join_unique[of _ k] show ?thesis


91 
by (simp add: join_def theI[of is_join])


92 
qed


93 


94 
lemma join_unique: "(is_join j) = (j = join)"


95 
by (insert is_join_join, auto simp add: is_join_unique)


96 


97 
lemma meet_left_le: "meet a b \<le> (a::'a::meet_semilorder)"


98 
by (insert is_meet_meet, auto simp add: is_meet_def)


99 


100 
lemma meet_right_le: "meet a b \<le> (b::'a::meet_semilorder)"


101 
by (insert is_meet_meet, auto simp add: is_meet_def)


102 


103 
lemma meet_imp_le: "x \<le> a \<Longrightarrow> x \<le> b \<Longrightarrow> x \<le> meet a (b::'a::meet_semilorder)"


104 
by (insert is_meet_meet, auto simp add: is_meet_def)


105 


106 
lemma join_left_le: "a \<le> join a (b::'a::join_semilorder)"


107 
by (insert is_join_join, auto simp add: is_join_def)


108 


109 
lemma join_right_le: "b \<le> join a (b::'a::join_semilorder)"


110 
by (insert is_join_join, auto simp add: is_join_def)


111 


112 
lemma join_imp_le: "a \<le> x \<Longrightarrow> b \<le> x \<Longrightarrow> join a b \<le> (x::'a::join_semilorder)"


113 
by (insert is_join_join, auto simp add: is_join_def)


114 


115 
lemmas meet_join_le = meet_left_le meet_right_le join_left_le join_right_le


116 


117 
lemma is_meet_min: "is_meet (min::'a \<Rightarrow> 'a \<Rightarrow> ('a::linorder))"


118 
by (auto simp add: is_meet_def min_def)


119 


120 
lemma is_join_max: "is_join (max::'a \<Rightarrow> 'a \<Rightarrow> ('a::linorder))"


121 
by (auto simp add: is_join_def max_def)


122 


123 
instance linorder \<subseteq> meet_semilorder


124 
proof


125 
from is_meet_min show "? (m::'a\<Rightarrow>'a\<Rightarrow>('a::linorder)). is_meet m" by auto


126 
qed


127 


128 
instance linorder \<subseteq> join_semilorder


129 
proof


130 
from is_join_max show "? (j::'a\<Rightarrow>'a\<Rightarrow>('a::linorder)). is_join j" by auto


131 
qed


132 


133 
instance linorder \<subseteq> lorder ..


134 


135 
lemma meet_min: "meet = (min :: 'a\<Rightarrow>'a\<Rightarrow>('a::linorder))"


136 
by (simp add: is_meet_meet is_meet_min is_meet_unique)


137 


138 
lemma join_max: "join = (max :: 'a\<Rightarrow>'a\<Rightarrow>('a::linorder))"


139 
by (simp add: is_join_join is_join_max is_join_unique)


140 


141 
lemma meet_idempotent[simp]: "meet x x = x"


142 
by (rule order_antisym, simp_all add: meet_left_le meet_imp_le)


143 


144 
lemma join_idempotent[simp]: "join x x = x"


145 
by (rule order_antisym, simp_all add: join_left_le join_imp_le)


146 


147 
lemma meet_comm: "meet x y = meet y x"


148 
by (rule order_antisym, (simp add: meet_left_le meet_right_le meet_imp_le)+)


149 


150 
lemma join_comm: "join x y = join y x"


151 
by (rule order_antisym, (simp add: join_right_le join_left_le join_imp_le)+)


152 


153 
lemma meet_assoc: "meet (meet x y) z = meet x (meet y z)" (is "?l=?r")


154 
proof 


155 
have "?l <= meet x y & meet x y <= x & ?l <= z & meet x y <= y" by (simp add: meet_left_le meet_right_le)


156 
hence "?l <= x & ?l <= y & ?l <= z" by auto


157 
hence "?l <= ?r" by (simp add: meet_imp_le)


158 
hence a:"?l <= meet x (meet y z)" by (simp add: meet_imp_le)


159 
have "?r <= meet y z & meet y z <= y & meet y z <= z & ?r <= x" by (simp add: meet_left_le meet_right_le)


160 
hence "?r <= x & ?r <= y & ?r <= z" by (auto)


161 
hence "?r <= meet x y & ?r <= z" by (simp add: meet_imp_le)


162 
hence b:"?r <= ?l" by (simp add: meet_imp_le)


163 
from a b show "?l = ?r" by auto


164 
qed


165 


166 
lemma join_assoc: "join (join x y) z = join x (join y z)" (is "?l=?r")


167 
proof 


168 
have "join x y <= ?l & x <= join x y & z <= ?l & y <= join x y" by (simp add: join_left_le join_right_le)


169 
hence "x <= ?l & y <= ?l & z <= ?l" by auto


170 
hence "join y z <= ?l & x <= ?l" by (simp add: join_imp_le)


171 
hence a:"?r <= ?l" by (simp add: join_imp_le)


172 
have "join y z <= ?r & y <= join y z & z <= join y z & x <= ?r" by (simp add: join_left_le join_right_le)


173 
hence "y <= ?r & z <= ?r & x <= ?r" by auto


174 
hence "join x y <= ?r & z <= ?r" by (simp add: join_imp_le)


175 
hence b:"?l <= ?r" by (simp add: join_imp_le)


176 
from a b show "?l = ?r" by auto


177 
qed


178 


179 
lemma meet_left_comm: "meet a (meet b c) = meet b (meet a c)"


180 
by (simp add: meet_assoc[symmetric, of a b c], simp add: meet_comm[of a b], simp add: meet_assoc)


181 


182 
lemma meet_left_idempotent: "meet y (meet y x) = meet y x"


183 
by (simp add: meet_assoc meet_comm meet_left_comm)


184 


185 
lemma join_left_comm: "join a (join b c) = join b (join a c)"


186 
by (simp add: join_assoc[symmetric, of a b c], simp add: join_comm[of a b], simp add: join_assoc)


187 


188 
lemma join_left_idempotent: "join y (join y x) = join y x"


189 
by (simp add: join_assoc join_comm join_left_comm)


190 


191 
lemmas meet_aci = meet_assoc meet_comm meet_left_comm meet_left_idempotent


192 


193 
lemmas join_aci = join_assoc join_comm join_left_comm join_left_idempotent


194 


195 
lemma le_def_meet: "(x <= y) = (meet x y = x)"


196 
proof 


197 
have u: "x <= y \<longrightarrow> meet x y = x"


198 
proof


199 
assume "x <= y"


200 
hence "x <= meet x y & meet x y <= x" by (simp add: meet_imp_le meet_left_le)


201 
thus "meet x y = x" by auto


202 
qed


203 
have v:"meet x y = x \<longrightarrow> x <= y"


204 
proof


205 
have a:"meet x y <= y" by (simp add: meet_right_le)


206 
assume "meet x y = x"


207 
hence "x = meet x y" by auto


208 
with a show "x <= y" by (auto)


209 
qed


210 
from u v show ?thesis by blast


211 
qed


212 


213 
lemma le_def_join: "(x <= y) = (join x y = y)"


214 
proof 


215 
have u: "x <= y \<longrightarrow> join x y = y"


216 
proof


217 
assume "x <= y"


218 
hence "join x y <= y & y <= join x y" by (simp add: join_imp_le join_right_le)


219 
thus "join x y = y" by auto


220 
qed


221 
have v:"join x y = y \<longrightarrow> x <= y"


222 
proof


223 
have a:"x <= join x y" by (simp add: join_left_le)


224 
assume "join x y = y"


225 
hence "y = join x y" by auto


226 
with a show "x <= y" by (auto)


227 
qed


228 
from u v show ?thesis by blast


229 
qed


230 


231 
lemma meet_join_absorp: "meet x (join x y) = x"


232 
proof 


233 
have a:"meet x (join x y) <= x" by (simp add: meet_left_le)


234 
have b:"x <= meet x (join x y)" by (rule meet_imp_le, simp_all add: join_left_le)


235 
from a b show ?thesis by auto


236 
qed


237 


238 
lemma join_meet_absorp: "join x (meet x y) = x"


239 
proof 


240 
have a:"x <= join x (meet x y)" by (simp add: join_left_le)


241 
have b:"join x (meet x y) <= x" by (rule join_imp_le, simp_all add: meet_left_le)


242 
from a b show ?thesis by auto


243 
qed


244 


245 
lemma meet_mono: "y \<le> z \<Longrightarrow> meet x y \<le> meet x z"


246 
proof 


247 
assume a: "y <= z"


248 
have "meet x y <= x & meet x y <= y" by (simp add: meet_left_le meet_right_le)


249 
with a have "meet x y <= x & meet x y <= z" by auto


250 
thus "meet x y <= meet x z" by (simp add: meet_imp_le)


251 
qed


252 


253 
lemma join_mono: "y \<le> z \<Longrightarrow> join x y \<le> join x z"


254 
proof 


255 
assume a: "y \<le> z"


256 
have "x <= join x z & z <= join x z" by (simp add: join_left_le join_right_le)


257 
with a have "x <= join x z & y <= join x z" by auto


258 
thus "join x y <= join x z" by (simp add: join_imp_le)


259 
qed


260 


261 
lemma distrib_join_le: "join x (meet y z) \<le> meet (join x y) (join x z)" (is "_ <= ?r")


262 
proof 


263 
have a: "x <= ?r" by (rule meet_imp_le, simp_all add: join_left_le)


264 
from meet_join_le have b: "meet y z <= ?r"


265 
by (rule_tac meet_imp_le, (blast intro: order_trans)+)


266 
from a b show ?thesis by (simp add: join_imp_le)


267 
qed


268 


269 
lemma distrib_meet_le: "join (meet x y) (meet x z) \<le> meet x (join y z)" (is "?l <= _")


270 
proof 


271 
have a: "?l <= x" by (rule join_imp_le, simp_all add: meet_left_le)


272 
from meet_join_le have b: "?l <= join y z"


273 
by (rule_tac join_imp_le, (blast intro: order_trans)+)


274 
from a b show ?thesis by (simp add: meet_imp_le)


275 
qed


276 


277 
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"


278 
by (insert meet_join_le, blast intro: order_trans)


279 


280 
lemma modular_le: "x \<le> z \<Longrightarrow> join x (meet y z) \<le> meet (join x y) z" (is "_ \<Longrightarrow> ?t <= _")


281 
proof 


282 
assume a: "x <= z"


283 
have b: "?t <= join x y" by (rule join_imp_le, simp_all add: meet_join_le meet_join_eq_imp_le)


284 
have c: "?t <= z" by (rule join_imp_le, simp_all add: meet_join_le a)


285 
from b c show ?thesis by (simp add: meet_imp_le)


286 
qed


287 


288 
ML {*


289 
val is_meet_unique = thm "is_meet_unique";


290 
val is_join_unique = thm "is_join_unique";


291 
val join_exists = thm "join_exists";


292 
val meet_exists = thm "meet_exists";


293 
val is_meet_meet = thm "is_meet_meet";


294 
val meet_unique = thm "meet_unique";


295 
val is_join_join = thm "is_join_join";


296 
val join_unique = thm "join_unique";


297 
val meet_left_le = thm "meet_left_le";


298 
val meet_right_le = thm "meet_right_le";


299 
val meet_imp_le = thm "meet_imp_le";


300 
val join_left_le = thm "join_left_le";


301 
val join_right_le = thm "join_right_le";


302 
val join_imp_le = thm "join_imp_le";


303 
val meet_join_le = thms "meet_join_le";


304 
val is_meet_min = thm "is_meet_min";


305 
val is_join_max = thm "is_join_max";


306 
val meet_min = thm "meet_min";


307 
val join_max = thm "join_max";


308 
val meet_idempotent = thm "meet_idempotent";


309 
val join_idempotent = thm "join_idempotent";


310 
val meet_comm = thm "meet_comm";


311 
val join_comm = thm "join_comm";


312 
val meet_assoc = thm "meet_assoc";


313 
val join_assoc = thm "join_assoc";


314 
val meet_left_comm = thm "meet_left_comm";


315 
val meet_left_idempotent = thm "meet_left_idempotent";


316 
val join_left_comm = thm "join_left_comm";


317 
val join_left_idempotent = thm "join_left_idempotent";


318 
val meet_aci = thms "meet_aci";


319 
val join_aci = thms "join_aci";


320 
val le_def_meet = thm "le_def_meet";


321 
val le_def_join = thm "le_def_join";


322 
val meet_join_absorp = thm "meet_join_absorp";


323 
val join_meet_absorp = thm "join_meet_absorp";


324 
val meet_mono = thm "meet_mono";


325 
val join_mono = thm "join_mono";


326 
val distrib_join_le = thm "distrib_join_le";


327 
val distrib_meet_le = thm "distrib_meet_le";


328 
val meet_join_eq_imp_le = thm "meet_join_eq_imp_le";


329 
val modular_le = thm "modular_le";


330 
*}


331 

15131

332 
end
