src/HOL/LOrder.thy
 author nipkow Thu Feb 10 18:51:12 2005 +0100 (2005-02-10) changeset 15524 2ef571f80a55 parent 15140 322485b816ac child 17508 c84af7f39a6b permissions -rw-r--r--
Moved oderings from HOL into the new Orderings.thy
 obua@14738  1 (* Title: HOL/LOrder.thy  obua@14738  2  ID: $Id$  obua@14738  3  Author: Steven Obua, TU Muenchen  obua@14738  4 *)  obua@14738  5 obua@14738  6 header {* Lattice Orders *}  obua@14738  7 nipkow@15131  8 theory LOrder  nipkow@15524  9 imports Orderings  nipkow@15131  10 begin  obua@14738  11 obua@14738  12 text {*  obua@14738  13  The theory of lattices developed here is taken from the book:  obua@14738  14  \begin{itemize}  obua@14738  15  \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979.  obua@14738  16  \end{itemize}  obua@14738  17 *}  obua@14738  18 obua@14738  19 constdefs  obua@14738  20  is_meet :: "(('a::order) \ 'a \ 'a) \ bool"  obua@14738  21  "is_meet m == ! a b x. m a b \ a \ m a b \ b \ (x \ a \ x \ b \ x \ m a b)"  obua@14738  22  is_join :: "(('a::order) \ 'a \ 'a) \ bool"  obua@14738  23  "is_join j == ! a b x. a \ j a b \ b \ j a b \ (a \ x \ b \ x \ j a b \ x)"  obua@14738  24 obua@14738  25 lemma is_meet_unique:  obua@14738  26  assumes "is_meet u" "is_meet v" shows "u = v"  obua@14738  27 proof -  obua@14738  28  {  obua@14738  29  fix a b :: "'a \ 'a \ 'a"  obua@14738  30  assume a: "is_meet a"  obua@14738  31  assume b: "is_meet b"  obua@14738  32  {  obua@14738  33  fix x y  obua@14738  34  let ?za = "a x y"  obua@14738  35  let ?zb = "b x y"  obua@14738  36  from a have za_le: "?za <= x & ?za <= y" by (auto simp add: is_meet_def)  obua@14738  37  with b have "?za <= ?zb" by (auto simp add: is_meet_def)  obua@14738  38  }  obua@14738  39  }  obua@14738  40  note f_le = this  obua@14738  41  show "u = v" by ((rule ext)+, simp_all add: order_antisym prems f_le)  obua@14738  42 qed  obua@14738  43 obua@14738  44 lemma is_join_unique:  obua@14738  45  assumes "is_join u" "is_join v" shows "u = v"  obua@14738  46 proof -  obua@14738  47  {  obua@14738  48  fix a b :: "'a \ 'a \ 'a"  obua@14738  49  assume a: "is_join a"  obua@14738  50  assume b: "is_join b"  obua@14738  51  {  obua@14738  52  fix x y  obua@14738  53  let ?za = "a x y"  obua@14738  54  let ?zb = "b x y"  obua@14738  55  from a have za_le: "x <= ?za & y <= ?za" by (auto simp add: is_join_def)  obua@14738  56  with b have "?zb <= ?za" by (auto simp add: is_join_def)  obua@14738  57  }  obua@14738  58  }  obua@14738  59  note f_le = this  obua@14738  60  show "u = v" by ((rule ext)+, simp_all add: order_antisym prems f_le)  obua@14738  61 qed  obua@14738  62 obua@14738  63 axclass join_semilorder < order  obua@14738  64  join_exists: "? j. is_join j"  obua@14738  65 obua@14738  66 axclass meet_semilorder < order  obua@14738  67  meet_exists: "? m. is_meet m"  obua@14738  68 obua@14738  69 axclass lorder < join_semilorder, meet_semilorder  obua@14738  70 obua@14738  71 constdefs  obua@14738  72  meet :: "('a::meet_semilorder) \ 'a \ 'a"  obua@14738  73  "meet == THE m. is_meet m"  obua@14738  74  join :: "('a::join_semilorder) \ 'a \ 'a"  obua@14738  75  "join == THE j. is_join j"  obua@14738  76 obua@14738  77 lemma is_meet_meet: "is_meet (meet::'a \ 'a \ ('a::meet_semilorder))"  obua@14738  78 proof -  obua@14738  79  from meet_exists obtain k::"'a \ 'a \ 'a" where "is_meet k" ..  obua@14738  80  with is_meet_unique[of _ k] show ?thesis  obua@14738  81  by (simp add: meet_def theI[of is_meet])  obua@14738  82 qed  obua@14738  83 obua@14738  84 lemma meet_unique: "(is_meet m) = (m = meet)"  obua@14738  85 by (insert is_meet_meet, auto simp add: is_meet_unique)  obua@14738  86 obua@14738  87 lemma is_join_join: "is_join (join::'a \ 'a \ ('a::join_semilorder))"  obua@14738  88 proof -  obua@14738  89  from join_exists obtain k::"'a \ 'a \ 'a" where "is_join k" ..  obua@14738  90  with is_join_unique[of _ k] show ?thesis  obua@14738  91  by (simp add: join_def theI[of is_join])  obua@14738  92 qed  obua@14738  93 obua@14738  94 lemma join_unique: "(is_join j) = (j = join)"  obua@14738  95 by (insert is_join_join, auto simp add: is_join_unique)  obua@14738  96 obua@14738  97 lemma meet_left_le: "meet a b \ (a::'a::meet_semilorder)"  obua@14738  98 by (insert is_meet_meet, auto simp add: is_meet_def)  obua@14738  99 obua@14738  100 lemma meet_right_le: "meet a b \ (b::'a::meet_semilorder)"  obua@14738  101 by (insert is_meet_meet, auto simp add: is_meet_def)  obua@14738  102 obua@14738  103 lemma meet_imp_le: "x \ a \ x \ b \ x \ meet a (b::'a::meet_semilorder)"  obua@14738  104 by (insert is_meet_meet, auto simp add: is_meet_def)  obua@14738  105 obua@14738  106 lemma join_left_le: "a \ join a (b::'a::join_semilorder)"  obua@14738  107 by (insert is_join_join, auto simp add: is_join_def)  obua@14738  108 obua@14738  109 lemma join_right_le: "b \ join a (b::'a::join_semilorder)"  obua@14738  110 by (insert is_join_join, auto simp add: is_join_def)  obua@14738  111 obua@14738  112 lemma join_imp_le: "a \ x \ b \ x \ join a b \ (x::'a::join_semilorder)"  obua@14738  113 by (insert is_join_join, auto simp add: is_join_def)  obua@14738  114 obua@14738  115 lemmas meet_join_le = meet_left_le meet_right_le join_left_le join_right_le  obua@14738  116 obua@14738  117 lemma is_meet_min: "is_meet (min::'a \ 'a \ ('a::linorder))"  obua@14738  118 by (auto simp add: is_meet_def min_def)  obua@14738  119 obua@14738  120 lemma is_join_max: "is_join (max::'a \ 'a \ ('a::linorder))"  obua@14738  121 by (auto simp add: is_join_def max_def)  obua@14738  122 obua@14738  123 instance linorder \ meet_semilorder  obua@14738  124 proof  obua@14738  125  from is_meet_min show "? (m::'a\'a\('a::linorder)). is_meet m" by auto  obua@14738  126 qed  obua@14738  127 obua@14738  128 instance linorder \ join_semilorder  obua@14738  129 proof  obua@14738  130  from is_join_max show "? (j::'a\'a\('a::linorder)). is_join j" by auto  obua@14738  131 qed  obua@14738  132   obua@14738  133 instance linorder \ lorder ..  obua@14738  134 obua@14738  135 lemma meet_min: "meet = (min :: 'a\'a\('a::linorder))"  obua@14738  136 by (simp add: is_meet_meet is_meet_min is_meet_unique)  obua@14738  137 obua@14738  138 lemma join_max: "join = (max :: 'a\'a\('a::linorder))"  obua@14738  139 by (simp add: is_join_join is_join_max is_join_unique)  obua@14738  140 obua@14738  141 lemma meet_idempotent[simp]: "meet x x = x"  obua@14738  142 by (rule order_antisym, simp_all add: meet_left_le meet_imp_le)  obua@14738  143 obua@14738  144 lemma join_idempotent[simp]: "join x x = x"  obua@14738  145 by (rule order_antisym, simp_all add: join_left_le join_imp_le)  obua@14738  146 obua@14738  147 lemma meet_comm: "meet x y = meet y x"  obua@14738  148 by (rule order_antisym, (simp add: meet_left_le meet_right_le meet_imp_le)+)  obua@14738  149 obua@14738  150 lemma join_comm: "join x y = join y x"  obua@14738  151 by (rule order_antisym, (simp add: join_right_le join_left_le join_imp_le)+)  obua@14738  152 obua@14738  153 lemma meet_assoc: "meet (meet x y) z = meet x (meet y z)" (is "?l=?r")  obua@14738  154 proof -  obua@14738  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)  obua@14738  156  hence "?l <= x & ?l <= y & ?l <= z" by auto  obua@14738  157  hence "?l <= ?r" by (simp add: meet_imp_le)  obua@14738  158  hence a:"?l <= meet x (meet y z)" by (simp add: meet_imp_le)  obua@14738  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)  obua@14738  160  hence "?r <= x & ?r <= y & ?r <= z" by (auto)  obua@14738  161  hence "?r <= meet x y & ?r <= z" by (simp add: meet_imp_le)  obua@14738  162  hence b:"?r <= ?l" by (simp add: meet_imp_le)  obua@14738  163  from a b show "?l = ?r" by auto  obua@14738  164 qed  obua@14738  165 obua@14738  166 lemma join_assoc: "join (join x y) z = join x (join y z)" (is "?l=?r")  obua@14738  167 proof -  obua@14738  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)  obua@14738  169  hence "x <= ?l & y <= ?l & z <= ?l" by auto  obua@14738  170  hence "join y z <= ?l & x <= ?l" by (simp add: join_imp_le)  obua@14738  171  hence a:"?r <= ?l" by (simp add: join_imp_le)  obua@14738  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)  obua@14738  173  hence "y <= ?r & z <= ?r & x <= ?r" by auto  obua@14738  174  hence "join x y <= ?r & z <= ?r" by (simp add: join_imp_le)  obua@14738  175  hence b:"?l <= ?r" by (simp add: join_imp_le)  obua@14738  176  from a b show "?l = ?r" by auto  obua@14738  177 qed  obua@14738  178 obua@14738  179 lemma meet_left_comm: "meet a (meet b c) = meet b (meet a c)"  obua@14738  180 by (simp add: meet_assoc[symmetric, of a b c], simp add: meet_comm[of a b], simp add: meet_assoc)  obua@14738  181 obua@14738  182 lemma meet_left_idempotent: "meet y (meet y x) = meet y x"  obua@14738  183 by (simp add: meet_assoc meet_comm meet_left_comm)  obua@14738  184 obua@14738  185 lemma join_left_comm: "join a (join b c) = join b (join a c)"  obua@14738  186 by (simp add: join_assoc[symmetric, of a b c], simp add: join_comm[of a b], simp add: join_assoc)  obua@14738  187 obua@14738  188 lemma join_left_idempotent: "join y (join y x) = join y x"  obua@14738  189 by (simp add: join_assoc join_comm join_left_comm)  obua@14738  190   obua@14738  191 lemmas meet_aci = meet_assoc meet_comm meet_left_comm meet_left_idempotent  obua@14738  192 obua@14738  193 lemmas join_aci = join_assoc join_comm join_left_comm join_left_idempotent  obua@14738  194 obua@14738  195 lemma le_def_meet: "(x <= y) = (meet x y = x)"  obua@14738  196 proof -  obua@14738  197  have u: "x <= y \ meet x y = x"  obua@14738  198  proof  obua@14738  199  assume "x <= y"  obua@14738  200  hence "x <= meet x y & meet x y <= x" by (simp add: meet_imp_le meet_left_le)  obua@14738  201  thus "meet x y = x" by auto  obua@14738  202  qed  obua@14738  203  have v:"meet x y = x \ x <= y"  obua@14738  204  proof  obua@14738  205  have a:"meet x y <= y" by (simp add: meet_right_le)  obua@14738  206  assume "meet x y = x"  obua@14738  207  hence "x = meet x y" by auto  obua@14738  208  with a show "x <= y" by (auto)  obua@14738  209  qed  obua@14738  210  from u v show ?thesis by blast  obua@14738  211 qed  obua@14738  212 obua@14738  213 lemma le_def_join: "(x <= y) = (join x y = y)"  obua@14738  214 proof -  obua@14738  215  have u: "x <= y \ join x y = y"  obua@14738  216  proof  obua@14738  217  assume "x <= y"  obua@14738  218  hence "join x y <= y & y <= join x y" by (simp add: join_imp_le join_right_le)  obua@14738  219  thus "join x y = y" by auto  obua@14738  220  qed  obua@14738  221  have v:"join x y = y \ x <= y"  obua@14738  222  proof  obua@14738  223  have a:"x <= join x y" by (simp add: join_left_le)  obua@14738  224  assume "join x y = y"  obua@14738  225  hence "y = join x y" by auto  obua@14738  226  with a show "x <= y" by (auto)  obua@14738  227  qed  obua@14738  228  from u v show ?thesis by blast  obua@14738  229 qed  obua@14738  230 obua@14738  231 lemma meet_join_absorp: "meet x (join x y) = x"  obua@14738  232 proof -  obua@14738  233  have a:"meet x (join x y) <= x" by (simp add: meet_left_le)  obua@14738  234  have b:"x <= meet x (join x y)" by (rule meet_imp_le, simp_all add: join_left_le)  obua@14738  235  from a b show ?thesis by auto  obua@14738  236 qed  obua@14738  237 obua@14738  238 lemma join_meet_absorp: "join x (meet x y) = x"  obua@14738  239 proof -  obua@14738  240  have a:"x <= join x (meet x y)" by (simp add: join_left_le)  obua@14738  241  have b:"join x (meet x y) <= x" by (rule join_imp_le, simp_all add: meet_left_le)  obua@14738  242  from a b show ?thesis by auto  obua@14738  243 qed  obua@14738  244 obua@14738  245 lemma meet_mono: "y \ z \ meet x y \ meet x z"  obua@14738  246 proof -  obua@14738  247  assume a: "y <= z"  obua@14738  248  have "meet x y <= x & meet x y <= y" by (simp add: meet_left_le meet_right_le)  obua@14738  249  with a have "meet x y <= x & meet x y <= z" by auto  obua@14738  250  thus "meet x y <= meet x z" by (simp add: meet_imp_le)  obua@14738  251 qed  obua@14738  252 obua@14738  253 lemma join_mono: "y \ z \ join x y \ join x z"  obua@14738  254 proof -  obua@14738  255  assume a: "y \ z"  obua@14738  256  have "x <= join x z & z <= join x z" by (simp add: join_left_le join_right_le)  obua@14738  257  with a have "x <= join x z & y <= join x z" by auto  obua@14738  258  thus "join x y <= join x z" by (simp add: join_imp_le)  obua@14738  259 qed  obua@14738  260 obua@14738  261 lemma distrib_join_le: "join x (meet y z) \ meet (join x y) (join x z)" (is "_ <= ?r")  obua@14738  262 proof -  obua@14738  263  have a: "x <= ?r" by (rule meet_imp_le, simp_all add: join_left_le)  obua@14738  264  from meet_join_le have b: "meet y z <= ?r"  obua@14738  265  by (rule_tac meet_imp_le, (blast intro: order_trans)+)  obua@14738  266  from a b show ?thesis by (simp add: join_imp_le)  obua@14738  267 qed  obua@14738  268   obua@14738  269 lemma distrib_meet_le: "join (meet x y) (meet x z) \ meet x (join y z)" (is "?l <= _")  obua@14738  270 proof -  obua@14738  271  have a: "?l <= x" by (rule join_imp_le, simp_all add: meet_left_le)  obua@14738  272  from meet_join_le have b: "?l <= join y z"  obua@14738  273  by (rule_tac join_imp_le, (blast intro: order_trans)+)  obua@14738  274  from a b show ?thesis by (simp add: meet_imp_le)  obua@14738  275 qed  obua@14738  276 obua@14738  277 lemma meet_join_eq_imp_le: "a = c \ a = d \ b = c \ b = d \ meet a b \ join c d"  obua@14738  278 by (insert meet_join_le, blast intro: order_trans)  obua@14738  279 obua@14738  280 lemma modular_le: "x \ z \ join x (meet y z) \ meet (join x y) z" (is "_ \ ?t <= _")  obua@14738  281 proof -  obua@14738  282  assume a: "x <= z"  obua@14738  283  have b: "?t <= join x y" by (rule join_imp_le, simp_all add: meet_join_le meet_join_eq_imp_le)  obua@14738  284  have c: "?t <= z" by (rule join_imp_le, simp_all add: meet_join_le a)  obua@14738  285  from b c show ?thesis by (simp add: meet_imp_le)  obua@14738  286 qed  obua@14738  287 obua@14738  288 ML {*  obua@14738  289 val is_meet_unique = thm "is_meet_unique";  obua@14738  290 val is_join_unique = thm "is_join_unique";  obua@14738  291 val join_exists = thm "join_exists";  obua@14738  292 val meet_exists = thm "meet_exists";  obua@14738  293 val is_meet_meet = thm "is_meet_meet";  obua@14738  294 val meet_unique = thm "meet_unique";  obua@14738  295 val is_join_join = thm "is_join_join";  obua@14738  296 val join_unique = thm "join_unique";  obua@14738  297 val meet_left_le = thm "meet_left_le";  obua@14738  298 val meet_right_le = thm "meet_right_le";  obua@14738  299 val meet_imp_le = thm "meet_imp_le";  obua@14738  300 val join_left_le = thm "join_left_le";  obua@14738  301 val join_right_le = thm "join_right_le";  obua@14738  302 val join_imp_le = thm "join_imp_le";  obua@14738  303 val meet_join_le = thms "meet_join_le";  obua@14738  304 val is_meet_min = thm "is_meet_min";  obua@14738  305 val is_join_max = thm "is_join_max";  obua@14738  306 val meet_min = thm "meet_min";  obua@14738  307 val join_max = thm "join_max";  obua@14738  308 val meet_idempotent = thm "meet_idempotent";  obua@14738  309 val join_idempotent = thm "join_idempotent";  obua@14738  310 val meet_comm = thm "meet_comm";  obua@14738  311 val join_comm = thm "join_comm";  obua@14738  312 val meet_assoc = thm "meet_assoc";  obua@14738  313 val join_assoc = thm "join_assoc";  obua@14738  314 val meet_left_comm = thm "meet_left_comm";  obua@14738  315 val meet_left_idempotent = thm "meet_left_idempotent";  obua@14738  316 val join_left_comm = thm "join_left_comm";  obua@14738  317 val join_left_idempotent = thm "join_left_idempotent";  obua@14738  318 val meet_aci = thms "meet_aci";  obua@14738  319 val join_aci = thms "join_aci";  obua@14738  320 val le_def_meet = thm "le_def_meet";  obua@14738  321 val le_def_join = thm "le_def_join";  obua@14738  322 val meet_join_absorp = thm "meet_join_absorp";  obua@14738  323 val join_meet_absorp = thm "join_meet_absorp";  obua@14738  324 val meet_mono = thm "meet_mono";  obua@14738  325 val join_mono = thm "join_mono";  obua@14738  326 val distrib_join_le = thm "distrib_join_le";  obua@14738  327 val distrib_meet_le = thm "distrib_meet_le";  obua@14738  328 val meet_join_eq_imp_le = thm "meet_join_eq_imp_le";  obua@14738  329 val modular_le = thm "modular_le";  obua@14738  330 *}  obua@14738  331 nipkow@15131  332 end