1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/LOrder.thy Tue May 11 20:11:08 2004 +0200
1.3 @@ -0,0 +1,331 @@
1.4 +(* Title: HOL/LOrder.thy
1.5 + ID: $Id$
1.6 + Author: Steven Obua, TU Muenchen
1.7 + License: GPL (GNU GENERAL PUBLIC LICENSE)
1.8 +*)
1.9 +
1.10 +header {* Lattice Orders *}
1.11 +
1.12 +theory LOrder = HOL:
1.13 +
1.14 +text {*
1.15 + The theory of lattices developed here is taken from the book:
1.16 + \begin{itemize}
1.17 + \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979.
1.18 + \end{itemize}
1.19 +*}
1.20 +
1.21 +constdefs
1.22 + is_meet :: "(('a::order) \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
1.23 + "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)"
1.24 + is_join :: "(('a::order) \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
1.25 + "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)"
1.26 +
1.27 +lemma is_meet_unique:
1.28 + assumes "is_meet u" "is_meet v" shows "u = v"
1.29 +proof -
1.30 + {
1.31 + fix a b :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
1.32 + assume a: "is_meet a"
1.33 + assume b: "is_meet b"
1.34 + {
1.35 + fix x y
1.36 + let ?za = "a x y"
1.37 + let ?zb = "b x y"
1.38 + from a have za_le: "?za <= x & ?za <= y" by (auto simp add: is_meet_def)
1.39 + with b have "?za <= ?zb" by (auto simp add: is_meet_def)
1.40 + }
1.41 + }
1.42 + note f_le = this
1.43 + show "u = v" by ((rule ext)+, simp_all add: order_antisym prems f_le)
1.44 +qed
1.45 +
1.46 +lemma is_join_unique:
1.47 + assumes "is_join u" "is_join v" shows "u = v"
1.48 +proof -
1.49 + {
1.50 + fix a b :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
1.51 + assume a: "is_join a"
1.52 + assume b: "is_join b"
1.53 + {
1.54 + fix x y
1.55 + let ?za = "a x y"
1.56 + let ?zb = "b x y"
1.57 + from a have za_le: "x <= ?za & y <= ?za" by (auto simp add: is_join_def)
1.58 + with b have "?zb <= ?za" by (auto simp add: is_join_def)
1.59 + }
1.60 + }
1.61 + note f_le = this
1.62 + show "u = v" by ((rule ext)+, simp_all add: order_antisym prems f_le)
1.63 +qed
1.64 +
1.65 +axclass join_semilorder < order
1.66 + join_exists: "? j. is_join j"
1.67 +
1.68 +axclass meet_semilorder < order
1.69 + meet_exists: "? m. is_meet m"
1.70 +
1.71 +axclass lorder < join_semilorder, meet_semilorder
1.72 +
1.73 +constdefs
1.74 + meet :: "('a::meet_semilorder) \<Rightarrow> 'a \<Rightarrow> 'a"
1.75 + "meet == THE m. is_meet m"
1.76 + join :: "('a::join_semilorder) \<Rightarrow> 'a \<Rightarrow> 'a"
1.77 + "join == THE j. is_join j"
1.78 +
1.79 +lemma is_meet_meet: "is_meet (meet::'a \<Rightarrow> 'a \<Rightarrow> ('a::meet_semilorder))"
1.80 +proof -
1.81 + from meet_exists obtain k::"'a \<Rightarrow> 'a \<Rightarrow> 'a" where "is_meet k" ..
1.82 + with is_meet_unique[of _ k] show ?thesis
1.83 + by (simp add: meet_def theI[of is_meet])
1.84 +qed
1.85 +
1.86 +lemma meet_unique: "(is_meet m) = (m = meet)"
1.87 +by (insert is_meet_meet, auto simp add: is_meet_unique)
1.88 +
1.89 +lemma is_join_join: "is_join (join::'a \<Rightarrow> 'a \<Rightarrow> ('a::join_semilorder))"
1.90 +proof -
1.91 + from join_exists obtain k::"'a \<Rightarrow> 'a \<Rightarrow> 'a" where "is_join k" ..
1.92 + with is_join_unique[of _ k] show ?thesis
1.93 + by (simp add: join_def theI[of is_join])
1.94 +qed
1.95 +
1.96 +lemma join_unique: "(is_join j) = (j = join)"
1.97 +by (insert is_join_join, auto simp add: is_join_unique)
1.98 +
1.99 +lemma meet_left_le: "meet a b \<le> (a::'a::meet_semilorder)"
1.100 +by (insert is_meet_meet, auto simp add: is_meet_def)
1.101 +
1.102 +lemma meet_right_le: "meet a b \<le> (b::'a::meet_semilorder)"
1.103 +by (insert is_meet_meet, auto simp add: is_meet_def)
1.104 +
1.105 +lemma meet_imp_le: "x \<le> a \<Longrightarrow> x \<le> b \<Longrightarrow> x \<le> meet a (b::'a::meet_semilorder)"
1.106 +by (insert is_meet_meet, auto simp add: is_meet_def)
1.107 +
1.108 +lemma join_left_le: "a \<le> join a (b::'a::join_semilorder)"
1.109 +by (insert is_join_join, auto simp add: is_join_def)
1.110 +
1.111 +lemma join_right_le: "b \<le> join a (b::'a::join_semilorder)"
1.112 +by (insert is_join_join, auto simp add: is_join_def)
1.113 +
1.114 +lemma join_imp_le: "a \<le> x \<Longrightarrow> b \<le> x \<Longrightarrow> join a b \<le> (x::'a::join_semilorder)"
1.115 +by (insert is_join_join, auto simp add: is_join_def)
1.116 +
1.117 +lemmas meet_join_le = meet_left_le meet_right_le join_left_le join_right_le
1.118 +
1.119 +lemma is_meet_min: "is_meet (min::'a \<Rightarrow> 'a \<Rightarrow> ('a::linorder))"
1.120 +by (auto simp add: is_meet_def min_def)
1.121 +
1.122 +lemma is_join_max: "is_join (max::'a \<Rightarrow> 'a \<Rightarrow> ('a::linorder))"
1.123 +by (auto simp add: is_join_def max_def)
1.124 +
1.125 +instance linorder \<subseteq> meet_semilorder
1.126 +proof
1.127 + from is_meet_min show "? (m::'a\<Rightarrow>'a\<Rightarrow>('a::linorder)). is_meet m" by auto
1.128 +qed
1.129 +
1.130 +instance linorder \<subseteq> join_semilorder
1.131 +proof
1.132 + from is_join_max show "? (j::'a\<Rightarrow>'a\<Rightarrow>('a::linorder)). is_join j" by auto
1.133 +qed
1.134 +
1.135 +instance linorder \<subseteq> lorder ..
1.136 +
1.137 +lemma meet_min: "meet = (min :: 'a\<Rightarrow>'a\<Rightarrow>('a::linorder))"
1.138 +by (simp add: is_meet_meet is_meet_min is_meet_unique)
1.139 +
1.140 +lemma join_max: "join = (max :: 'a\<Rightarrow>'a\<Rightarrow>('a::linorder))"
1.141 +by (simp add: is_join_join is_join_max is_join_unique)
1.142 +
1.143 +lemma meet_idempotent[simp]: "meet x x = x"
1.144 +by (rule order_antisym, simp_all add: meet_left_le meet_imp_le)
1.145 +
1.146 +lemma join_idempotent[simp]: "join x x = x"
1.147 +by (rule order_antisym, simp_all add: join_left_le join_imp_le)
1.148 +
1.149 +lemma meet_comm: "meet x y = meet y x"
1.150 +by (rule order_antisym, (simp add: meet_left_le meet_right_le meet_imp_le)+)
1.151 +
1.152 +lemma join_comm: "join x y = join y x"
1.153 +by (rule order_antisym, (simp add: join_right_le join_left_le join_imp_le)+)
1.154 +
1.155 +lemma meet_assoc: "meet (meet x y) z = meet x (meet y z)" (is "?l=?r")
1.156 +proof -
1.157 + have "?l <= meet x y & meet x y <= x & ?l <= z & meet x y <= y" by (simp add: meet_left_le meet_right_le)
1.158 + hence "?l <= x & ?l <= y & ?l <= z" by auto
1.159 + hence "?l <= ?r" by (simp add: meet_imp_le)
1.160 + hence a:"?l <= meet x (meet y z)" by (simp add: meet_imp_le)
1.161 + have "?r <= meet y z & meet y z <= y & meet y z <= z & ?r <= x" by (simp add: meet_left_le meet_right_le)
1.162 + hence "?r <= x & ?r <= y & ?r <= z" by (auto)
1.163 + hence "?r <= meet x y & ?r <= z" by (simp add: meet_imp_le)
1.164 + hence b:"?r <= ?l" by (simp add: meet_imp_le)
1.165 + from a b show "?l = ?r" by auto
1.166 +qed
1.167 +
1.168 +lemma join_assoc: "join (join x y) z = join x (join y z)" (is "?l=?r")
1.169 +proof -
1.170 + have "join x y <= ?l & x <= join x y & z <= ?l & y <= join x y" by (simp add: join_left_le join_right_le)
1.171 + hence "x <= ?l & y <= ?l & z <= ?l" by auto
1.172 + hence "join y z <= ?l & x <= ?l" by (simp add: join_imp_le)
1.173 + hence a:"?r <= ?l" by (simp add: join_imp_le)
1.174 + have "join y z <= ?r & y <= join y z & z <= join y z & x <= ?r" by (simp add: join_left_le join_right_le)
1.175 + hence "y <= ?r & z <= ?r & x <= ?r" by auto
1.176 + hence "join x y <= ?r & z <= ?r" by (simp add: join_imp_le)
1.177 + hence b:"?l <= ?r" by (simp add: join_imp_le)
1.178 + from a b show "?l = ?r" by auto
1.179 +qed
1.180 +
1.181 +lemma meet_left_comm: "meet a (meet b c) = meet b (meet a c)"
1.182 +by (simp add: meet_assoc[symmetric, of a b c], simp add: meet_comm[of a b], simp add: meet_assoc)
1.183 +
1.184 +lemma meet_left_idempotent: "meet y (meet y x) = meet y x"
1.185 +by (simp add: meet_assoc meet_comm meet_left_comm)
1.186 +
1.187 +lemma join_left_comm: "join a (join b c) = join b (join a c)"
1.188 +by (simp add: join_assoc[symmetric, of a b c], simp add: join_comm[of a b], simp add: join_assoc)
1.189 +
1.190 +lemma join_left_idempotent: "join y (join y x) = join y x"
1.191 +by (simp add: join_assoc join_comm join_left_comm)
1.192 +
1.193 +lemmas meet_aci = meet_assoc meet_comm meet_left_comm meet_left_idempotent
1.194 +
1.195 +lemmas join_aci = join_assoc join_comm join_left_comm join_left_idempotent
1.196 +
1.197 +lemma le_def_meet: "(x <= y) = (meet x y = x)"
1.198 +proof -
1.199 + have u: "x <= y \<longrightarrow> meet x y = x"
1.200 + proof
1.201 + assume "x <= y"
1.202 + hence "x <= meet x y & meet x y <= x" by (simp add: meet_imp_le meet_left_le)
1.203 + thus "meet x y = x" by auto
1.204 + qed
1.205 + have v:"meet x y = x \<longrightarrow> x <= y"
1.206 + proof
1.207 + have a:"meet x y <= y" by (simp add: meet_right_le)
1.208 + assume "meet x y = x"
1.209 + hence "x = meet x y" by auto
1.210 + with a show "x <= y" by (auto)
1.211 + qed
1.212 + from u v show ?thesis by blast
1.213 +qed
1.214 +
1.215 +lemma le_def_join: "(x <= y) = (join x y = y)"
1.216 +proof -
1.217 + have u: "x <= y \<longrightarrow> join x y = y"
1.218 + proof
1.219 + assume "x <= y"
1.220 + hence "join x y <= y & y <= join x y" by (simp add: join_imp_le join_right_le)
1.221 + thus "join x y = y" by auto
1.222 + qed
1.223 + have v:"join x y = y \<longrightarrow> x <= y"
1.224 + proof
1.225 + have a:"x <= join x y" by (simp add: join_left_le)
1.226 + assume "join x y = y"
1.227 + hence "y = join x y" by auto
1.228 + with a show "x <= y" by (auto)
1.229 + qed
1.230 + from u v show ?thesis by blast
1.231 +qed
1.232 +
1.233 +lemma meet_join_absorp: "meet x (join x y) = x"
1.234 +proof -
1.235 + have a:"meet x (join x y) <= x" by (simp add: meet_left_le)
1.236 + have b:"x <= meet x (join x y)" by (rule meet_imp_le, simp_all add: join_left_le)
1.237 + from a b show ?thesis by auto
1.238 +qed
1.239 +
1.240 +lemma join_meet_absorp: "join x (meet x y) = x"
1.241 +proof -
1.242 + have a:"x <= join x (meet x y)" by (simp add: join_left_le)
1.243 + have b:"join x (meet x y) <= x" by (rule join_imp_le, simp_all add: meet_left_le)
1.244 + from a b show ?thesis by auto
1.245 +qed
1.246 +
1.247 +lemma meet_mono: "y \<le> z \<Longrightarrow> meet x y \<le> meet x z"
1.248 +proof -
1.249 + assume a: "y <= z"
1.250 + have "meet x y <= x & meet x y <= y" by (simp add: meet_left_le meet_right_le)
1.251 + with a have "meet x y <= x & meet x y <= z" by auto
1.252 + thus "meet x y <= meet x z" by (simp add: meet_imp_le)
1.253 +qed
1.254 +
1.255 +lemma join_mono: "y \<le> z \<Longrightarrow> join x y \<le> join x z"
1.256 +proof -
1.257 + assume a: "y \<le> z"
1.258 + have "x <= join x z & z <= join x z" by (simp add: join_left_le join_right_le)
1.259 + with a have "x <= join x z & y <= join x z" by auto
1.260 + thus "join x y <= join x z" by (simp add: join_imp_le)
1.261 +qed
1.262 +
1.263 +lemma distrib_join_le: "join x (meet y z) \<le> meet (join x y) (join x z)" (is "_ <= ?r")
1.264 +proof -
1.265 + have a: "x <= ?r" by (rule meet_imp_le, simp_all add: join_left_le)
1.266 + from meet_join_le have b: "meet y z <= ?r"
1.267 + by (rule_tac meet_imp_le, (blast intro: order_trans)+)
1.268 + from a b show ?thesis by (simp add: join_imp_le)
1.269 +qed
1.270 +
1.271 +lemma distrib_meet_le: "join (meet x y) (meet x z) \<le> meet x (join y z)" (is "?l <= _")
1.272 +proof -
1.273 + have a: "?l <= x" by (rule join_imp_le, simp_all add: meet_left_le)
1.274 + from meet_join_le have b: "?l <= join y z"
1.275 + by (rule_tac join_imp_le, (blast intro: order_trans)+)
1.276 + from a b show ?thesis by (simp add: meet_imp_le)
1.277 +qed
1.278 +
1.279 +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"
1.280 +by (insert meet_join_le, blast intro: order_trans)
1.281 +
1.282 +lemma modular_le: "x \<le> z \<Longrightarrow> join x (meet y z) \<le> meet (join x y) z" (is "_ \<Longrightarrow> ?t <= _")
1.283 +proof -
1.284 + assume a: "x <= z"
1.285 + have b: "?t <= join x y" by (rule join_imp_le, simp_all add: meet_join_le meet_join_eq_imp_le)
1.286 + have c: "?t <= z" by (rule join_imp_le, simp_all add: meet_join_le a)
1.287 + from b c show ?thesis by (simp add: meet_imp_le)
1.288 +qed
1.289 +
1.290 +ML {*
1.291 +val is_meet_unique = thm "is_meet_unique";
1.292 +val is_join_unique = thm "is_join_unique";
1.293 +val join_exists = thm "join_exists";
1.294 +val meet_exists = thm "meet_exists";
1.295 +val is_meet_meet = thm "is_meet_meet";
1.296 +val meet_unique = thm "meet_unique";
1.297 +val is_join_join = thm "is_join_join";
1.298 +val join_unique = thm "join_unique";
1.299 +val meet_left_le = thm "meet_left_le";
1.300 +val meet_right_le = thm "meet_right_le";
1.301 +val meet_imp_le = thm "meet_imp_le";
1.302 +val join_left_le = thm "join_left_le";
1.303 +val join_right_le = thm "join_right_le";
1.304 +val join_imp_le = thm "join_imp_le";
1.305 +val meet_join_le = thms "meet_join_le";
1.306 +val is_meet_min = thm "is_meet_min";
1.307 +val is_join_max = thm "is_join_max";
1.308 +val meet_min = thm "meet_min";
1.309 +val join_max = thm "join_max";
1.310 +val meet_idempotent = thm "meet_idempotent";
1.311 +val join_idempotent = thm "join_idempotent";
1.312 +val meet_comm = thm "meet_comm";
1.313 +val join_comm = thm "join_comm";
1.314 +val meet_assoc = thm "meet_assoc";
1.315 +val join_assoc = thm "join_assoc";
1.316 +val meet_left_comm = thm "meet_left_comm";
1.317 +val meet_left_idempotent = thm "meet_left_idempotent";
1.318 +val join_left_comm = thm "join_left_comm";
1.319 +val join_left_idempotent = thm "join_left_idempotent";
1.320 +val meet_aci = thms "meet_aci";
1.321 +val join_aci = thms "join_aci";
1.322 +val le_def_meet = thm "le_def_meet";
1.323 +val le_def_join = thm "le_def_join";
1.324 +val meet_join_absorp = thm "meet_join_absorp";
1.325 +val join_meet_absorp = thm "join_meet_absorp";
1.326 +val meet_mono = thm "meet_mono";
1.327 +val join_mono = thm "join_mono";
1.328 +val distrib_join_le = thm "distrib_join_le";
1.329 +val distrib_meet_le = thm "distrib_meet_le";
1.330 +val meet_join_eq_imp_le = thm "meet_join_eq_imp_le";
1.331 +val modular_le = thm "modular_le";
1.332 +*}
1.333 +
1.334 +end
1.335 \ No newline at end of file