src/HOL/Algebra/Lattice.thy
 author ballarin Sun Oct 31 11:38:09 2010 +0100 (2010-10-31) changeset 40293 cd932ab8cb59 parent 39990 9b4341366b63 child 44472 6f2943e34d60 permissions -rw-r--r--
Minor reformat.
 wenzelm@35849  1 (* Title: HOL/Algebra/Lattice.thy  wenzelm@35849  2  Author: Clemens Ballarin, started 7 November 2003  wenzelm@35849  3  Copyright: Clemens Ballarin  ballarin@27714  4 ballarin@27717  5 Most congruence rules by Stephan Hohe.  ballarin@14551  6 *)  ballarin@14551  7 wenzelm@35849  8 theory Lattice  wenzelm@35849  9 imports Congruence  wenzelm@35849  10 begin  ballarin@14551  11 ballarin@20318  12 section {* Orders and Lattices *}  ballarin@14751  13 ballarin@14551  14 subsection {* Partial Orders *}  ballarin@14551  15 ballarin@27713  16 record 'a gorder = "'a eq_object" +  ballarin@22063  17  le :: "['a, 'a] => bool" (infixl "\\" 50)  ballarin@21041  18 ballarin@29237  19 locale weak_partial_order = equivalence L for L (structure) +  ballarin@27713  20  assumes le_refl [intro, simp]:  ballarin@27713  21  "x \ carrier L ==> x \ x"  nipkow@33657  22  and weak_le_antisym [intro]:  ballarin@27713  23  "[| x \ y; y \ x; x \ carrier L; y \ carrier L |] ==> x .= y"  ballarin@27713  24  and le_trans [trans]:  ballarin@27713  25  "[| x \ y; y \ z; x \ carrier L; y \ carrier L; z \ carrier L |] ==> x \ z"  ballarin@27713  26  and le_cong:  ballarin@40293  27  "\ x .= y; z .= w; x \ carrier L; y \ carrier L; z \ carrier L; w \ carrier L \ \  ballarin@40293  28  x \ z \ y \ w"  ballarin@22063  29 wenzelm@35847  30 definition  ballarin@22063  31  lless :: "[_, 'a, 'a] => bool" (infixl "\\" 50)  wenzelm@35848  32  where "x \\<^bsub>L\<^esub> y \ x \\<^bsub>L\<^esub> y & x .\\<^bsub>L\<^esub> y"  ballarin@27713  33 ballarin@27713  34 ballarin@27713  35 subsubsection {* The order relation *}  ballarin@27713  36 ballarin@27713  37 context weak_partial_order begin  ballarin@27713  38 ballarin@27713  39 lemma le_cong_l [intro, trans]:  ballarin@27713  40  "\ x .= y; y \ z; x \ carrier L; y \ carrier L; z \ carrier L \ \ x \ z"  ballarin@27713  41  by (auto intro: le_cong [THEN iffD2])  ballarin@27713  42 ballarin@27713  43 lemma le_cong_r [intro, trans]:  ballarin@27713  44  "\ x \ y; y .= z; x \ carrier L; y \ carrier L; z \ carrier L \ \ x \ z"  ballarin@27713  45  by (auto intro: le_cong [THEN iffD1])  ballarin@27713  46 ballarin@27714  47 lemma weak_refl [intro, simp]: "\ x .= y; x \ carrier L; y \ carrier L \ \ x \ y"  ballarin@27713  48  by (simp add: le_cong_l)  ballarin@27713  49 ballarin@27713  50 end  ballarin@27713  51 ballarin@27713  52 lemma weak_llessI:  ballarin@27713  53  fixes R (structure)  ballarin@27713  54  assumes "x \ y" and "~(x .= y)"  ballarin@27713  55  shows "x \ y"  ballarin@27713  56  using assms unfolding lless_def by simp  ballarin@27713  57 ballarin@27713  58 lemma lless_imp_le:  ballarin@27713  59  fixes R (structure)  ballarin@27713  60  assumes "x \ y"  ballarin@27713  61  shows "x \ y"  ballarin@27713  62  using assms unfolding lless_def by simp  ballarin@27713  63 ballarin@27713  64 lemma weak_lless_imp_not_eq:  ballarin@27713  65  fixes R (structure)  ballarin@27713  66  assumes "x \ y"  ballarin@27713  67  shows "\ (x .= y)"  ballarin@27713  68  using assms unfolding lless_def by simp  ballarin@22063  69 ballarin@27713  70 lemma weak_llessE:  ballarin@27713  71  fixes R (structure)  ballarin@27713  72  assumes p: "x \ y" and e: "\x \ y; \ (x .= y)\ \ P"  ballarin@27713  73  shows "P"  ballarin@27713  74  using p by (blast dest: lless_imp_le weak_lless_imp_not_eq e)  ballarin@27713  75 ballarin@27713  76 lemma (in weak_partial_order) lless_cong_l [trans]:  ballarin@27713  77  assumes xx': "x .= x'"  ballarin@27713  78  and xy: "x' \ y"  ballarin@27713  79  and carr: "x \ carrier L" "x' \ carrier L" "y \ carrier L"  ballarin@27713  80  shows "x \ y"  ballarin@27713  81  using assms unfolding lless_def by (auto intro: trans sym)  ballarin@27713  82 ballarin@27713  83 lemma (in weak_partial_order) lless_cong_r [trans]:  ballarin@27713  84  assumes xy: "x \ y"  ballarin@27713  85  and yy': "y .= y'"  ballarin@27713  86  and carr: "x \ carrier L" "y \ carrier L" "y' \ carrier L"  ballarin@27713  87  shows "x \ y'"  ballarin@27713  88  using assms unfolding lless_def by (auto intro: trans sym)  ballarin@27713  89 ballarin@27713  90 ballarin@27713  91 lemma (in weak_partial_order) lless_antisym:  ballarin@27713  92  assumes "a \ carrier L" "b \ carrier L"  ballarin@27713  93  and "a \ b" "b \ a"  ballarin@27713  94  shows "P"  ballarin@27713  95  using assms  ballarin@27713  96  by (elim weak_llessE) auto  ballarin@27713  97 ballarin@27713  98 lemma (in weak_partial_order) lless_trans [trans]:  ballarin@27713  99  assumes "a \ b" "b \ c"  ballarin@27713  100  and carr[simp]: "a \ carrier L" "b \ carrier L" "c \ carrier L"  ballarin@27713  101  shows "a \ c"  ballarin@27713  102  using assms unfolding lless_def by (blast dest: le_trans intro: sym)  ballarin@27713  103 ballarin@27713  104 ballarin@27713  105 subsubsection {* Upper and lower bounds of a set *}  ballarin@27713  106 wenzelm@35847  107 definition  ballarin@22063  108  Upper :: "[_, 'a set] => 'a set"  wenzelm@35848  109  where "Upper L A = {u. (ALL x. x \ A \ carrier L --> x \\<^bsub>L\<^esub> u)} \ carrier L"  ballarin@22063  110 wenzelm@35847  111 definition  ballarin@22063  112  Lower :: "[_, 'a set] => 'a set"  wenzelm@35848  113  where "Lower L A = {l. (ALL x. x \ A \ carrier L --> l \\<^bsub>L\<^esub> x)} \ carrier L"  ballarin@22063  114 ballarin@27713  115 lemma Upper_closed [intro!, simp]:  ballarin@22063  116  "Upper L A \ carrier L"  ballarin@14551  117  by (unfold Upper_def) clarify  ballarin@14551  118 ballarin@27700  119 lemma Upper_memD [dest]:  ballarin@22063  120  fixes L (structure)  ballarin@27713  121  shows "[| u \ Upper L A; x \ A; A \ carrier L |] ==> x \ u \ u \ carrier L"  wenzelm@14693  122  by (unfold Upper_def) blast  ballarin@14551  123 ballarin@27713  124 lemma (in weak_partial_order) Upper_elemD [dest]:  ballarin@27713  125  "[| u .\ Upper L A; u \ carrier L; x \ A; A \ carrier L |] ==> x \ u"  ballarin@27713  126  unfolding Upper_def elem_def  ballarin@27713  127  by (blast dest: sym)  ballarin@27713  128 ballarin@22063  129 lemma Upper_memI:  ballarin@22063  130  fixes L (structure)  ballarin@22063  131  shows "[| !! y. y \ A ==> y \ x; x \ carrier L |] ==> x \ Upper L A"  wenzelm@14693  132  by (unfold Upper_def) blast  ballarin@14551  133 ballarin@27713  134 lemma (in weak_partial_order) Upper_elemI:  ballarin@27713  135  "[| !! y. y \ A ==> y \ x; x \ carrier L |] ==> x .\ Upper L A"  ballarin@27713  136  unfolding Upper_def by blast  ballarin@27713  137 ballarin@22063  138 lemma Upper_antimono:  ballarin@22063  139  "A \ B ==> Upper L B \ Upper L A"  ballarin@14551  140  by (unfold Upper_def) blast  ballarin@14551  141 ballarin@27713  142 lemma (in weak_partial_order) Upper_is_closed [simp]:  ballarin@27713  143  "A \ carrier L ==> is_closed (Upper L A)"  ballarin@27713  144  by (rule is_closedI) (blast intro: Upper_memI)+  wenzelm@14651  145 ballarin@27713  146 lemma (in weak_partial_order) Upper_mem_cong:  ballarin@27713  147  assumes a'carr: "a' \ carrier L" and Acarr: "A \ carrier L"  ballarin@27713  148  and aa': "a .= a'"  ballarin@27713  149  and aelem: "a \ Upper L A"  ballarin@27713  150  shows "a' \ Upper L A"  ballarin@27713  151 proof (rule Upper_memI[OF _ a'carr])  ballarin@27713  152  fix y  ballarin@27713  153  assume yA: "y \ A"  ballarin@27713  154  hence "y \ a" by (intro Upper_memD[OF aelem, THEN conjunct1] Acarr)  ballarin@27713  155  also note aa'  ballarin@27713  156  finally  ballarin@27713  157  show "y \ a'"  ballarin@27713  158  by (simp add: a'carr subsetD[OF Acarr yA] subsetD[OF Upper_closed aelem])  ballarin@27713  159 qed  ballarin@27713  160 ballarin@27713  161 lemma (in weak_partial_order) Upper_cong:  ballarin@27713  162  assumes Acarr: "A \ carrier L" and A'carr: "A' \ carrier L"  ballarin@27713  163  and AA': "A {.=} A'"  ballarin@27713  164  shows "Upper L A = Upper L A'"  ballarin@27713  165 unfolding Upper_def  ballarin@27713  166 apply rule  ballarin@27713  167  apply (rule, clarsimp) defer 1  ballarin@27713  168  apply (rule, clarsimp) defer 1  ballarin@27713  169 proof -  ballarin@27713  170  fix x a'  ballarin@27713  171  assume carr: "x \ carrier L" "a' \ carrier L"  ballarin@27713  172  and a'A': "a' \ A'"  ballarin@27713  173  assume aLxCond[rule_format]: "\a. a \ A \ a \ carrier L \ a \ x"  ballarin@14551  174 ballarin@27713  175  from AA' and a'A' have "\a\A. a' .= a" by (rule set_eqD2)  ballarin@27713  176  from this obtain a  ballarin@27713  177  where aA: "a \ A"  ballarin@27713  178  and a'a: "a' .= a"  ballarin@27713  179  by auto  ballarin@27713  180  note [simp] = subsetD[OF Acarr aA] carr  ballarin@27713  181 ballarin@27713  182  note a'a  ballarin@27713  183  also have "a \ x" by (simp add: aLxCond aA)  ballarin@27713  184  finally show "a' \ x" by simp  ballarin@27713  185 next  ballarin@27713  186  fix x a  ballarin@27713  187  assume carr: "x \ carrier L" "a \ carrier L"  ballarin@27713  188  and aA: "a \ A"  ballarin@27713  189  assume a'LxCond[rule_format]: "\a'. a' \ A' \ a' \ carrier L \ a' \ x"  ballarin@27713  190 ballarin@27713  191  from AA' and aA have "\a'\A'. a .= a'" by (rule set_eqD1)  ballarin@27713  192  from this obtain a'  ballarin@27713  193  where a'A': "a' \ A'"  ballarin@27713  194  and aa': "a .= a'"  ballarin@27713  195  by auto  ballarin@27713  196  note [simp] = subsetD[OF A'carr a'A'] carr  ballarin@27713  197 ballarin@27713  198  note aa'  ballarin@27713  199  also have "a' \ x" by (simp add: a'LxCond a'A')  ballarin@27713  200  finally show "a \ x" by simp  ballarin@27713  201 qed  ballarin@27713  202 ballarin@27713  203 lemma Lower_closed [intro!, simp]:  ballarin@22063  204  "Lower L A \ carrier L"  ballarin@14551  205  by (unfold Lower_def) clarify  ballarin@14551  206 ballarin@27700  207 lemma Lower_memD [dest]:  ballarin@22063  208  fixes L (structure)  ballarin@27713  209  shows "[| l \ Lower L A; x \ A; A \ carrier L |] ==> l \ x \ l \ carrier L"  wenzelm@14693  210  by (unfold Lower_def) blast  ballarin@14551  211 ballarin@22063  212 lemma Lower_memI:  ballarin@22063  213  fixes L (structure)  ballarin@22063  214  shows "[| !! y. y \ A ==> x \ y; x \ carrier L |] ==> x \ Lower L A"  wenzelm@14693  215  by (unfold Lower_def) blast  ballarin@14551  216 ballarin@22063  217 lemma Lower_antimono:  ballarin@22063  218  "A \ B ==> Lower L B \ Lower L A"  ballarin@14551  219  by (unfold Lower_def) blast  ballarin@14551  220 ballarin@27713  221 lemma (in weak_partial_order) Lower_is_closed [simp]:  ballarin@27713  222  "A \ carrier L \ is_closed (Lower L A)"  ballarin@27713  223  by (rule is_closedI) (blast intro: Lower_memI dest: sym)+  wenzelm@14651  224 ballarin@27713  225 lemma (in weak_partial_order) Lower_mem_cong:  ballarin@27713  226  assumes a'carr: "a' \ carrier L" and Acarr: "A \ carrier L"  ballarin@27713  227  and aa': "a .= a'"  ballarin@27713  228  and aelem: "a \ Lower L A"  ballarin@27713  229  shows "a' \ Lower L A"  ballarin@27713  230 using assms Lower_closed[of L A]  ballarin@27713  231 by (intro Lower_memI) (blast intro: le_cong_l[OF aa'[symmetric]])  ballarin@27713  232 ballarin@27713  233 lemma (in weak_partial_order) Lower_cong:  ballarin@27713  234  assumes Acarr: "A \ carrier L" and A'carr: "A' \ carrier L"  ballarin@27713  235  and AA': "A {.=} A'"  ballarin@27713  236  shows "Lower L A = Lower L A'"  ballarin@27713  237 unfolding Lower_def  krauss@39990  238 apply rule  ballarin@27713  239  apply clarsimp defer 1  ballarin@27713  240  apply clarsimp defer 1  ballarin@27713  241 proof -  ballarin@27713  242  fix x a'  ballarin@27713  243  assume carr: "x \ carrier L" "a' \ carrier L"  ballarin@27713  244  and a'A': "a' \ A'"  ballarin@27713  245  assume "\a. a \ A \ a \ carrier L \ x \ a"  ballarin@27713  246  hence aLxCond: "\a. \a \ A; a \ carrier L\ \ x \ a" by fast  ballarin@27713  247 ballarin@27713  248  from AA' and a'A' have "\a\A. a' .= a" by (rule set_eqD2)  ballarin@27713  249  from this obtain a  ballarin@27713  250  where aA: "a \ A"  ballarin@27713  251  and a'a: "a' .= a"  ballarin@27713  252  by auto  ballarin@27713  253 ballarin@27713  254  from aA and subsetD[OF Acarr aA]  ballarin@27713  255  have "x \ a" by (rule aLxCond)  ballarin@27713  256  also note a'a[symmetric]  ballarin@27713  257  finally  ballarin@27713  258  show "x \ a'" by (simp add: carr subsetD[OF Acarr aA])  ballarin@27713  259 next  ballarin@27713  260  fix x a  ballarin@27713  261  assume carr: "x \ carrier L" "a \ carrier L"  ballarin@27713  262  and aA: "a \ A"  ballarin@27713  263  assume "\a'. a' \ A' \ a' \ carrier L \ x \ a'"  ballarin@27713  264  hence a'LxCond: "\a'. \a' \ A'; a' \ carrier L\ \ x \ a'" by fast+  ballarin@27713  265 ballarin@27713  266  from AA' and aA have "\a'\A'. a .= a'" by (rule set_eqD1)  ballarin@27713  267  from this obtain a'  ballarin@27713  268  where a'A': "a' \ A'"  ballarin@27713  269  and aa': "a .= a'"  ballarin@27713  270  by auto  ballarin@27713  271  from a'A' and subsetD[OF A'carr a'A']  ballarin@27713  272  have "x \ a'" by (rule a'LxCond)  ballarin@27713  273  also note aa'[symmetric]  ballarin@27713  274  finally show "x \ a" by (simp add: carr subsetD[OF A'carr a'A'])  ballarin@27713  275 qed  ballarin@27713  276 ballarin@27713  277 ballarin@27713  278 subsubsection {* Least and greatest, as predicate *}  ballarin@27713  279 wenzelm@35847  280 definition  ballarin@27713  281  least :: "[_, 'a, 'a set] => bool"  wenzelm@35848  282  where "least L l A \ A \ carrier L & l \ A & (ALL x : A. l \\<^bsub>L\<^esub> x)"  ballarin@27713  283 wenzelm@35847  284 definition  ballarin@27713  285  greatest :: "[_, 'a, 'a set] => bool"  wenzelm@35848  286  where "greatest L g A \ A \ carrier L & g \ A & (ALL x : A. x \\<^bsub>L\<^esub> g)"  ballarin@27713  287 wenzelm@30363  288 text (in weak_partial_order) {* Could weaken these to @{term "l \ carrier L \ l  wenzelm@30363  289  .\ A"} and @{term "g \ carrier L \ g .\ A"}. *}  ballarin@14551  290 ballarin@27700  291 lemma least_closed [intro, simp]:  ballarin@27713  292  "least L l A ==> l \ carrier L"  ballarin@14551  293  by (unfold least_def) fast  ballarin@14551  294 ballarin@22063  295 lemma least_mem:  ballarin@22063  296  "least L l A ==> l \ A"  ballarin@14551  297  by (unfold least_def) fast  ballarin@14551  298 ballarin@27713  299 lemma (in weak_partial_order) weak_least_unique:  ballarin@27713  300  "[| least L x A; least L y A |] ==> x .= y"  ballarin@14551  301  by (unfold least_def) blast  ballarin@14551  302 ballarin@22063  303 lemma least_le:  ballarin@22063  304  fixes L (structure)  ballarin@22063  305  shows "[| least L x A; a \ A |] ==> x \ a"  ballarin@14551  306  by (unfold least_def) fast  ballarin@14551  307 ballarin@27713  308 lemma (in weak_partial_order) least_cong:  ballarin@27713  309  "[| x .= x'; x \ carrier L; x' \ carrier L; is_closed A |] ==> least L x A = least L x' A"  ballarin@27713  310  by (unfold least_def) (auto dest: sym)  ballarin@27713  311 wenzelm@30363  312 text (in weak_partial_order) {* @{const least} is not congruent in the second parameter for  wenzelm@30363  313  @{term "A {.=} A'"} *}  ballarin@27713  314 ballarin@27713  315 lemma (in weak_partial_order) least_Upper_cong_l:  ballarin@27713  316  assumes "x .= x'"  ballarin@27713  317  and "x \ carrier L" "x' \ carrier L"  ballarin@27713  318  and "A \ carrier L"  ballarin@27713  319  shows "least L x (Upper L A) = least L x' (Upper L A)"  ballarin@27713  320  apply (rule least_cong) using assms by auto  ballarin@27713  321 ballarin@27713  322 lemma (in weak_partial_order) least_Upper_cong_r:  ballarin@27713  323  assumes Acarrs: "A \ carrier L" "A' \ carrier L" (* unneccessary with current Upper? *)  ballarin@27713  324  and AA': "A {.=} A'"  ballarin@27713  325  shows "least L x (Upper L A) = least L x (Upper L A')"  ballarin@27713  326 apply (subgoal_tac "Upper L A = Upper L A'", simp)  ballarin@27713  327 by (rule Upper_cong) fact+  ballarin@27713  328 ballarin@22063  329 lemma least_UpperI:  ballarin@22063  330  fixes L (structure)  ballarin@14551  331  assumes above: "!! x. x \ A ==> x \ s"  ballarin@22063  332  and below: "!! y. y \ Upper L A ==> s \ y"  ballarin@22063  333  and L: "A \ carrier L" "s \ carrier L"  ballarin@22063  334  shows "least L s (Upper L A)"  wenzelm@14693  335 proof -  ballarin@22063  336  have "Upper L A \ carrier L" by simp  ballarin@22063  337  moreover from above L have "s \ Upper L A" by (simp add: Upper_def)  ballarin@22063  338  moreover from below have "ALL x : Upper L A. s \ x" by fast  wenzelm@14693  339  ultimately show ?thesis by (simp add: least_def)  ballarin@14551  340 qed  ballarin@14551  341 ballarin@27713  342 lemma least_Upper_above:  ballarin@27713  343  fixes L (structure)  ballarin@27713  344  shows "[| least L s (Upper L A); x \ A; A \ carrier L |] ==> x \ s"  ballarin@27713  345  by (unfold least_def) blast  ballarin@14551  346 ballarin@27700  347 lemma greatest_closed [intro, simp]:  ballarin@27713  348  "greatest L l A ==> l \ carrier L"  ballarin@14551  349  by (unfold greatest_def) fast  ballarin@14551  350 ballarin@22063  351 lemma greatest_mem:  ballarin@22063  352  "greatest L l A ==> l \ A"  ballarin@14551  353  by (unfold greatest_def) fast  ballarin@14551  354 ballarin@27713  355 lemma (in weak_partial_order) weak_greatest_unique:  ballarin@27713  356  "[| greatest L x A; greatest L y A |] ==> x .= y"  ballarin@14551  357  by (unfold greatest_def) blast  ballarin@14551  358 ballarin@22063  359 lemma greatest_le:  ballarin@22063  360  fixes L (structure)  ballarin@22063  361  shows "[| greatest L x A; a \ A |] ==> a \ x"  ballarin@14551  362  by (unfold greatest_def) fast  ballarin@14551  363 ballarin@27713  364 lemma (in weak_partial_order) greatest_cong:  ballarin@27713  365  "[| x .= x'; x \ carrier L; x' \ carrier L; is_closed A |] ==>  ballarin@27713  366  greatest L x A = greatest L x' A"  ballarin@27713  367  by (unfold greatest_def) (auto dest: sym)  ballarin@27713  368 wenzelm@30363  369 text (in weak_partial_order) {* @{const greatest} is not congruent in the second parameter for  wenzelm@30363  370  @{term "A {.=} A'"} *}  ballarin@27713  371 ballarin@27713  372 lemma (in weak_partial_order) greatest_Lower_cong_l:  ballarin@27713  373  assumes "x .= x'"  ballarin@27713  374  and "x \ carrier L" "x' \ carrier L"  ballarin@27713  375  and "A \ carrier L" (* unneccessary with current Lower *)  ballarin@27713  376  shows "greatest L x (Lower L A) = greatest L x' (Lower L A)"  ballarin@27713  377  apply (rule greatest_cong) using assms by auto  ballarin@27713  378 ballarin@27713  379 lemma (in weak_partial_order) greatest_Lower_cong_r:  ballarin@27713  380  assumes Acarrs: "A \ carrier L" "A' \ carrier L"  ballarin@27713  381  and AA': "A {.=} A'"  ballarin@27713  382  shows "greatest L x (Lower L A) = greatest L x (Lower L A')"  ballarin@27713  383 apply (subgoal_tac "Lower L A = Lower L A'", simp)  ballarin@27713  384 by (rule Lower_cong) fact+  ballarin@27713  385 ballarin@22063  386 lemma greatest_LowerI:  ballarin@22063  387  fixes L (structure)  ballarin@14551  388  assumes below: "!! x. x \ A ==> i \ x"  ballarin@22063  389  and above: "!! y. y \ Lower L A ==> y \ i"  ballarin@22063  390  and L: "A \ carrier L" "i \ carrier L"  ballarin@22063  391  shows "greatest L i (Lower L A)"  wenzelm@14693  392 proof -  ballarin@22063  393  have "Lower L A \ carrier L" by simp  ballarin@22063  394  moreover from below L have "i \ Lower L A" by (simp add: Lower_def)  ballarin@22063  395  moreover from above have "ALL x : Lower L A. x \ i" by fast  wenzelm@14693  396  ultimately show ?thesis by (simp add: greatest_def)  ballarin@14551  397 qed  ballarin@14551  398 ballarin@27700  399 lemma greatest_Lower_below:  ballarin@22063  400  fixes L (structure)  ballarin@22063  401  shows "[| greatest L i (Lower L A); x \ A; A \ carrier L |] ==> i \ x"  ballarin@14551  402  by (unfold greatest_def) blast  ballarin@14551  403 ballarin@27713  404 text {* Supremum and infimum *}  ballarin@27713  405 wenzelm@35847  406 definition  ballarin@27713  407  sup :: "[_, 'a set] => 'a" ("\\_" [90] 90)  wenzelm@35848  408  where "\\<^bsub>L\<^esub>A = (SOME x. least L x (Upper L A))"  ballarin@27713  409 wenzelm@35847  410 definition  ballarin@27713  411  inf :: "[_, 'a set] => 'a" ("\\_" [90] 90)  wenzelm@35848  412  where "\\<^bsub>L\<^esub>A = (SOME x. greatest L x (Lower L A))"  ballarin@27713  413 wenzelm@35847  414 definition  ballarin@27713  415  join :: "[_, 'a, 'a] => 'a" (infixl "\\" 65)  wenzelm@35848  416  where "x \\<^bsub>L\<^esub> y = \\<^bsub>L\<^esub>{x, y}"  ballarin@27713  417 wenzelm@35847  418 definition  ballarin@27713  419  meet :: "[_, 'a, 'a] => 'a" (infixl "\\" 70)  wenzelm@35848  420  where "x \\<^bsub>L\<^esub> y = \\<^bsub>L\<^esub>{x, y}"  ballarin@27713  421 ballarin@27713  422 ballarin@27713  423 subsection {* Lattices *}  ballarin@27713  424 ballarin@27713  425 locale weak_upper_semilattice = weak_partial_order +  ballarin@27713  426  assumes sup_of_two_exists:  ballarin@27713  427  "[| x \ carrier L; y \ carrier L |] ==> EX s. least L s (Upper L {x, y})"  ballarin@27713  428 ballarin@27713  429 locale weak_lower_semilattice = weak_partial_order +  ballarin@27713  430  assumes inf_of_two_exists:  ballarin@27713  431  "[| x \ carrier L; y \ carrier L |] ==> EX s. greatest L s (Lower L {x, y})"  ballarin@27713  432 ballarin@27713  433 locale weak_lattice = weak_upper_semilattice + weak_lower_semilattice  ballarin@27713  434 wenzelm@14666  435 ballarin@14551  436 subsubsection {* Supremum *}  ballarin@14551  437 ballarin@27713  438 lemma (in weak_upper_semilattice) joinI:  ballarin@22063  439  "[| !!l. least L l (Upper L {x, y}) ==> P l; x \ carrier L; y \ carrier L |]  ballarin@14551  440  ==> P (x \ y)"  ballarin@14551  441 proof (unfold join_def sup_def)  ballarin@22063  442  assume L: "x \ carrier L" "y \ carrier L"  ballarin@22063  443  and P: "!!l. least L l (Upper L {x, y}) ==> P l"  ballarin@22063  444  with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast  ballarin@27713  445  with L show "P (SOME l. least L l (Upper L {x, y}))"  ballarin@27713  446  by (fast intro: someI2 P)  ballarin@14551  447 qed  ballarin@14551  448 ballarin@27713  449 lemma (in weak_upper_semilattice) join_closed [simp]:  ballarin@22063  450  "[| x \ carrier L; y \ carrier L |] ==> x \ y \ carrier L"  ballarin@27700  451  by (rule joinI) (rule least_closed)  ballarin@14551  452 ballarin@27713  453 lemma (in weak_upper_semilattice) join_cong_l:  ballarin@27713  454  assumes carr: "x \ carrier L" "x' \ carrier L" "y \ carrier L"  ballarin@27713  455  and xx': "x .= x'"  ballarin@27713  456  shows "x \ y .= x' \ y"  ballarin@27713  457 proof (rule joinI, rule joinI)  ballarin@27713  458  fix a b  ballarin@27713  459  from xx' carr  ballarin@27713  460  have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)  ballarin@27713  461 ballarin@27713  462  assume leasta: "least L a (Upper L {x, y})"  ballarin@27713  463  assume "least L b (Upper L {x', y})"  ballarin@27713  464  with carr  ballarin@27713  465  have leastb: "least L b (Upper L {x, y})"  ballarin@27713  466  by (simp add: least_Upper_cong_r[OF _ _ seq])  ballarin@27713  467 ballarin@27713  468  from leasta leastb  ballarin@27713  469  show "a .= b" by (rule weak_least_unique)  ballarin@27713  470 qed (rule carr)+  ballarin@14551  471 ballarin@27713  472 lemma (in weak_upper_semilattice) join_cong_r:  ballarin@27713  473  assumes carr: "x \ carrier L" "y \ carrier L" "y' \ carrier L"  ballarin@27713  474  and yy': "y .= y'"  ballarin@27713  475  shows "x \ y .= x \ y'"  ballarin@27713  476 proof (rule joinI, rule joinI)  ballarin@27713  477  fix a b  ballarin@27713  478  have "{x, y} = {y, x}" by fast  ballarin@27713  479  also from carr yy'  ballarin@27713  480  have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)  ballarin@27713  481  also have "{y', x} = {x, y'}" by fast  ballarin@27713  482  finally  ballarin@27713  483  have seq: "{x, y} {.=} {x, y'}" .  ballarin@14551  484 ballarin@27713  485  assume leasta: "least L a (Upper L {x, y})"  ballarin@27713  486  assume "least L b (Upper L {x, y'})"  ballarin@27713  487  with carr  ballarin@27713  488  have leastb: "least L b (Upper L {x, y})"  ballarin@27713  489  by (simp add: least_Upper_cong_r[OF _ _ seq])  ballarin@27713  490 ballarin@27713  491  from leasta leastb  ballarin@27713  492  show "a .= b" by (rule weak_least_unique)  ballarin@27713  493 qed (rule carr)+  ballarin@27713  494 ballarin@27713  495 lemma (in weak_partial_order) sup_of_singletonI: (* only reflexivity needed ? *)  ballarin@27713  496  "x \ carrier L ==> least L x (Upper L {x})"  ballarin@27713  497  by (rule least_UpperI) auto  ballarin@27713  498 ballarin@27713  499 lemma (in weak_partial_order) weak_sup_of_singleton [simp]:  ballarin@27713  500  "x \ carrier L ==> \{x} .= x"  ballarin@27713  501  unfolding sup_def  ballarin@27713  502  by (rule someI2) (auto intro: weak_least_unique sup_of_singletonI)  ballarin@27713  503 ballarin@27713  504 lemma (in weak_partial_order) sup_of_singleton_closed [simp]:  ballarin@27713  505  "x \ carrier L \ \{x} \ carrier L"  ballarin@27713  506  unfolding sup_def  ballarin@27713  507  by (rule someI2) (auto intro: sup_of_singletonI)  wenzelm@14666  508 wenzelm@14666  509 text {* Condition on @{text A}: supremum exists. *}  ballarin@14551  510 ballarin@27713  511 lemma (in weak_upper_semilattice) sup_insertI:  ballarin@22063  512  "[| !!s. least L s (Upper L (insert x A)) ==> P s;  ballarin@22063  513  least L a (Upper L A); x \ carrier L; A \ carrier L |]  wenzelm@14693  514  ==> P (\(insert x A))"  ballarin@14551  515 proof (unfold sup_def)  ballarin@22063  516  assume L: "x \ carrier L" "A \ carrier L"  ballarin@22063  517  and P: "!!l. least L l (Upper L (insert x A)) ==> P l"  ballarin@22063  518  and least_a: "least L a (Upper L A)"  ballarin@22063  519  from L least_a have La: "a \ carrier L" by simp  ballarin@14551  520  from L sup_of_two_exists least_a  ballarin@22063  521  obtain s where least_s: "least L s (Upper L {a, x})" by blast  ballarin@27713  522  show "P (SOME l. least L l (Upper L (insert x A)))"  ballarin@27713  523  proof (rule someI2)  ballarin@22063  524  show "least L s (Upper L (insert x A))"  ballarin@14551  525  proof (rule least_UpperI)  ballarin@14551  526  fix z  wenzelm@14693  527  assume "z \ insert x A"  wenzelm@14693  528  then show "z \ s"  wenzelm@14693  529  proof  wenzelm@14693  530  assume "z = x" then show ?thesis  wenzelm@14693  531  by (simp add: least_Upper_above [OF least_s] L La)  wenzelm@14693  532  next  wenzelm@14693  533  assume "z \ A"  wenzelm@14693  534  with L least_s least_a show ?thesis  ballarin@27713  535  by (rule_tac le_trans [where y = a]) (auto dest: least_Upper_above)  wenzelm@14693  536  qed  wenzelm@14693  537  next  wenzelm@14693  538  fix y  ballarin@22063  539  assume y: "y \ Upper L (insert x A)"  wenzelm@14693  540  show "s \ y"  wenzelm@14693  541  proof (rule least_le [OF least_s], rule Upper_memI)  wenzelm@32960  542  fix z  wenzelm@32960  543  assume z: "z \ {a, x}"  wenzelm@32960  544  then show "z \ y"  wenzelm@32960  545  proof  ballarin@22063  546  have y': "y \ Upper L A"  ballarin@22063  547  apply (rule subsetD [where A = "Upper L (insert x A)"])  wenzelm@23463  548  apply (rule Upper_antimono)  wenzelm@32960  549  apply blast  wenzelm@32960  550  apply (rule y)  wenzelm@14693  551  done  wenzelm@14693  552  assume "z = a"  wenzelm@14693  553  with y' least_a show ?thesis by (fast dest: least_le)  wenzelm@32960  554  next  wenzelm@32960  555  assume "z \ {x}" (* FIXME "z = x"; declare specific elim rule for "insert x {}" (!?) *)  wenzelm@14693  556  with y L show ?thesis by blast  wenzelm@32960  557  qed  wenzelm@23350  558  qed (rule Upper_closed [THEN subsetD, OF y])  wenzelm@14693  559  next  ballarin@22063  560  from L show "insert x A \ carrier L" by simp  ballarin@22063  561  from least_s show "s \ carrier L" by simp  ballarin@14551  562  qed  wenzelm@23350  563  qed (rule P)  ballarin@14551  564 qed  ballarin@14551  565 ballarin@27713  566 lemma (in weak_upper_semilattice) finite_sup_least:  ballarin@22063  567  "[| finite A; A \ carrier L; A ~= {} |] ==> least L (\A) (Upper L A)"  berghofe@22265  568 proof (induct set: finite)  wenzelm@14693  569  case empty  wenzelm@14693  570  then show ?case by simp  ballarin@14551  571 next  nipkow@15328  572  case (insert x A)  ballarin@14551  573  show ?case  ballarin@14551  574  proof (cases "A = {}")  ballarin@14551  575  case True  ballarin@27713  576  with insert show ?thesis  ballarin@27713  577  by simp (simp add: least_cong [OF weak_sup_of_singleton]  wenzelm@32960  578  sup_of_singleton_closed sup_of_singletonI)  wenzelm@32960  579  (* The above step is hairy; least_cong can make simp loop.  wenzelm@32960  580  Would want special version of simp to apply least_cong. *)  ballarin@14551  581  next  ballarin@14551  582  case False  ballarin@22063  583  with insert have "least L (\A) (Upper L A)" by simp  wenzelm@14693  584  with _ show ?thesis  wenzelm@14693  585  by (rule sup_insertI) (simp_all add: insert [simplified])  ballarin@14551  586  qed  ballarin@14551  587 qed  ballarin@14551  588 ballarin@27713  589 lemma (in weak_upper_semilattice) finite_sup_insertI:  ballarin@22063  590  assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l"  ballarin@22063  591  and xA: "finite A" "x \ carrier L" "A \ carrier L"  ballarin@14551  592  shows "P (\ (insert x A))"  ballarin@14551  593 proof (cases "A = {}")  ballarin@14551  594  case True with P and xA show ?thesis  ballarin@27713  595  by (simp add: finite_sup_least)  ballarin@14551  596 next  ballarin@14551  597  case False with P and xA show ?thesis  ballarin@14551  598  by (simp add: sup_insertI finite_sup_least)  ballarin@14551  599 qed  ballarin@14551  600 ballarin@27713  601 lemma (in weak_upper_semilattice) finite_sup_closed [simp]:  ballarin@22063  602  "[| finite A; A \ carrier L; A ~= {} |] ==> \A \ carrier L"  berghofe@22265  603 proof (induct set: finite)  ballarin@14551  604  case empty then show ?case by simp  ballarin@14551  605 next  nipkow@15328  606  case insert then show ?case  wenzelm@14693  607  by - (rule finite_sup_insertI, simp_all)  ballarin@14551  608 qed  ballarin@14551  609 ballarin@27713  610 lemma (in weak_upper_semilattice) join_left:  ballarin@22063  611  "[| x \ carrier L; y \ carrier L |] ==> x \ x \ y"  wenzelm@14693  612  by (rule joinI [folded join_def]) (blast dest: least_mem)  ballarin@14551  613 ballarin@27713  614 lemma (in weak_upper_semilattice) join_right:  ballarin@22063  615  "[| x \ carrier L; y \ carrier L |] ==> y \ x \ y"  wenzelm@14693  616  by (rule joinI [folded join_def]) (blast dest: least_mem)  ballarin@14551  617 ballarin@27713  618 lemma (in weak_upper_semilattice) sup_of_two_least:  ballarin@22063  619  "[| x \ carrier L; y \ carrier L |] ==> least L (\{x, y}) (Upper L {x, y})"  ballarin@14551  620 proof (unfold sup_def)  ballarin@22063  621  assume L: "x \ carrier L" "y \ carrier L"  ballarin@22063  622  with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast  ballarin@27713  623  with L show "least L (SOME z. least L z (Upper L {x, y})) (Upper L {x, y})"  ballarin@27713  624  by (fast intro: someI2 weak_least_unique) (* blast fails *)  ballarin@14551  625 qed  ballarin@14551  626 ballarin@27713  627 lemma (in weak_upper_semilattice) join_le:  wenzelm@14693  628  assumes sub: "x \ z" "y \ z"  wenzelm@23350  629  and x: "x \ carrier L" and y: "y \ carrier L" and z: "z \ carrier L"  ballarin@14551  630  shows "x \ y \ z"  wenzelm@23350  631 proof (rule joinI [OF _ x y])  ballarin@14551  632  fix s  ballarin@22063  633  assume "least L s (Upper L {x, y})"  wenzelm@23350  634  with sub z show "s \ z" by (fast elim: least_le intro: Upper_memI)  ballarin@14551  635 qed  wenzelm@14693  636 ballarin@27713  637 lemma (in weak_upper_semilattice) weak_join_assoc_lemma:  ballarin@22063  638  assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L"  ballarin@27713  639  shows "x \ (y \ z) .= \{x, y, z}"  ballarin@14551  640 proof (rule finite_sup_insertI)  wenzelm@14651  641  -- {* The textbook argument in Jacobson I, p 457 *}  ballarin@14551  642  fix s  ballarin@22063  643  assume sup: "least L s (Upper L {x, y, z})"  ballarin@27713  644  show "x \ (y \ z) .= s"  nipkow@33657  645  proof (rule weak_le_antisym)  ballarin@14551  646  from sup L show "x \ (y \ z) \ s"  ballarin@14551  647  by (fastsimp intro!: join_le elim: least_Upper_above)  ballarin@14551  648  next  ballarin@14551  649  from sup L show "s \ x \ (y \ z)"  ballarin@14551  650  by (erule_tac least_le)  ballarin@27713  651  (blast intro!: Upper_memI intro: le_trans join_left join_right join_closed)  ballarin@27700  652  qed (simp_all add: L least_closed [OF sup])  ballarin@14551  653 qed (simp_all add: L)  ballarin@14551  654 ballarin@27713  655 text {* Commutativity holds for @{text "="}. *}  ballarin@27713  656 ballarin@22063  657 lemma join_comm:  ballarin@22063  658  fixes L (structure)  ballarin@22063  659  shows "x \ y = y \ x"  ballarin@14551  660  by (unfold join_def) (simp add: insert_commute)  ballarin@14551  661 ballarin@27713  662 lemma (in weak_upper_semilattice) weak_join_assoc:  ballarin@22063  663  assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L"  ballarin@27713  664  shows "(x \ y) \ z .= x \ (y \ z)"  ballarin@14551  665 proof -  ballarin@27713  666  (* FIXME: could be simplified by improved simp: uniform use of .=,  ballarin@27713  667  omit [symmetric] in last step. *)  ballarin@14551  668  have "(x \ y) \ z = z \ (x \ y)" by (simp only: join_comm)  ballarin@27713  669  also from L have "... .= \{z, x, y}" by (simp add: weak_join_assoc_lemma)  wenzelm@14693  670  also from L have "... = \{x, y, z}" by (simp add: insert_commute)  ballarin@27713  671  also from L have "... .= x \ (y \ z)" by (simp add: weak_join_assoc_lemma [symmetric])  ballarin@27713  672  finally show ?thesis by (simp add: L)  ballarin@14551  673 qed  ballarin@14551  674 wenzelm@14693  675 ballarin@14551  676 subsubsection {* Infimum *}  ballarin@14551  677 ballarin@27713  678 lemma (in weak_lower_semilattice) meetI:  ballarin@22063  679  "[| !!i. greatest L i (Lower L {x, y}) ==> P i;  ballarin@22063  680  x \ carrier L; y \ carrier L |]  ballarin@14551  681  ==> P (x \ y)"  ballarin@14551  682 proof (unfold meet_def inf_def)  ballarin@22063  683  assume L: "x \ carrier L" "y \ carrier L"  ballarin@22063  684  and P: "!!g. greatest L g (Lower L {x, y}) ==> P g"  ballarin@22063  685  with inf_of_two_exists obtain i where "greatest L i (Lower L {x, y})" by fast  ballarin@27713  686  with L show "P (SOME g. greatest L g (Lower L {x, y}))"  ballarin@27713  687  by (fast intro: someI2 weak_greatest_unique P)  ballarin@14551  688 qed  ballarin@14551  689 ballarin@27713  690 lemma (in weak_lower_semilattice) meet_closed [simp]:  ballarin@22063  691  "[| x \ carrier L; y \ carrier L |] ==> x \ y \ carrier L"  ballarin@27700  692  by (rule meetI) (rule greatest_closed)  ballarin@14551  693 ballarin@27713  694 lemma (in weak_lower_semilattice) meet_cong_l:  ballarin@27713  695  assumes carr: "x \ carrier L" "x' \ carrier L" "y \ carrier L"  ballarin@27713  696  and xx': "x .= x'"  ballarin@27713  697  shows "x \ y .= x' \ y"  ballarin@27713  698 proof (rule meetI, rule meetI)  ballarin@27713  699  fix a b  ballarin@27713  700  from xx' carr  ballarin@27713  701  have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)  ballarin@27713  702 ballarin@27713  703  assume greatesta: "greatest L a (Lower L {x, y})"  ballarin@27713  704  assume "greatest L b (Lower L {x', y})"  ballarin@27713  705  with carr  ballarin@27713  706  have greatestb: "greatest L b (Lower L {x, y})"  ballarin@27713  707  by (simp add: greatest_Lower_cong_r[OF _ _ seq])  ballarin@27713  708 ballarin@27713  709  from greatesta greatestb  ballarin@27713  710  show "a .= b" by (rule weak_greatest_unique)  ballarin@27713  711 qed (rule carr)+  ballarin@14551  712 ballarin@27713  713 lemma (in weak_lower_semilattice) meet_cong_r:  ballarin@27713  714  assumes carr: "x \ carrier L" "y \ carrier L" "y' \ carrier L"  ballarin@27713  715  and yy': "y .= y'"  ballarin@27713  716  shows "x \ y .= x \ y'"  ballarin@27713  717 proof (rule meetI, rule meetI)  ballarin@27713  718  fix a b  ballarin@27713  719  have "{x, y} = {y, x}" by fast  ballarin@27713  720  also from carr yy'  ballarin@27713  721  have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)  ballarin@27713  722  also have "{y', x} = {x, y'}" by fast  ballarin@27713  723  finally  ballarin@27713  724  have seq: "{x, y} {.=} {x, y'}" .  ballarin@27713  725 ballarin@27713  726  assume greatesta: "greatest L a (Lower L {x, y})"  ballarin@27713  727  assume "greatest L b (Lower L {x, y'})"  ballarin@27713  728  with carr  ballarin@27713  729  have greatestb: "greatest L b (Lower L {x, y})"  ballarin@27713  730  by (simp add: greatest_Lower_cong_r[OF _ _ seq])  ballarin@14551  731 ballarin@27713  732  from greatesta greatestb  ballarin@27713  733  show "a .= b" by (rule weak_greatest_unique)  ballarin@27713  734 qed (rule carr)+  ballarin@27713  735 ballarin@27713  736 lemma (in weak_partial_order) inf_of_singletonI: (* only reflexivity needed ? *)  ballarin@27713  737  "x \ carrier L ==> greatest L x (Lower L {x})"  ballarin@27713  738  by (rule greatest_LowerI) auto  ballarin@14551  739 ballarin@27713  740 lemma (in weak_partial_order) weak_inf_of_singleton [simp]:  ballarin@27713  741  "x \ carrier L ==> \{x} .= x"  ballarin@27713  742  unfolding inf_def  ballarin@27713  743  by (rule someI2) (auto intro: weak_greatest_unique inf_of_singletonI)  ballarin@27713  744 ballarin@27713  745 lemma (in weak_partial_order) inf_of_singleton_closed:  ballarin@27713  746  "x \ carrier L ==> \{x} \ carrier L"  ballarin@27713  747  unfolding inf_def  ballarin@27713  748  by (rule someI2) (auto intro: inf_of_singletonI)  ballarin@27713  749 ballarin@27713  750 text {* Condition on @{text A}: infimum exists. *}  ballarin@27713  751 ballarin@27713  752 lemma (in weak_lower_semilattice) inf_insertI:  ballarin@22063  753  "[| !!i. greatest L i (Lower L (insert x A)) ==> P i;  ballarin@22063  754  greatest L a (Lower L A); x \ carrier L; A \ carrier L |]  wenzelm@14693  755  ==> P (\(insert x A))"  ballarin@14551  756 proof (unfold inf_def)  ballarin@22063  757  assume L: "x \ carrier L" "A \ carrier L"  ballarin@22063  758  and P: "!!g. greatest L g (Lower L (insert x A)) ==> P g"  ballarin@22063  759  and greatest_a: "greatest L a (Lower L A)"  ballarin@22063  760  from L greatest_a have La: "a \ carrier L" by simp  ballarin@14551  761  from L inf_of_two_exists greatest_a  ballarin@22063  762  obtain i where greatest_i: "greatest L i (Lower L {a, x})" by blast  ballarin@27713  763  show "P (SOME g. greatest L g (Lower L (insert x A)))"  ballarin@27713  764  proof (rule someI2)  ballarin@22063  765  show "greatest L i (Lower L (insert x A))"  ballarin@14551  766  proof (rule greatest_LowerI)  ballarin@14551  767  fix z  wenzelm@14693  768  assume "z \ insert x A"  wenzelm@14693  769  then show "i \ z"  wenzelm@14693  770  proof  wenzelm@14693  771  assume "z = x" then show ?thesis  ballarin@27700  772  by (simp add: greatest_Lower_below [OF greatest_i] L La)  wenzelm@14693  773  next  wenzelm@14693  774  assume "z \ A"  wenzelm@14693  775  with L greatest_i greatest_a show ?thesis  ballarin@27713  776  by (rule_tac le_trans [where y = a]) (auto dest: greatest_Lower_below)  wenzelm@14693  777  qed  wenzelm@14693  778  next  wenzelm@14693  779  fix y  ballarin@22063  780  assume y: "y \ Lower L (insert x A)"  wenzelm@14693  781  show "y \ i"  wenzelm@14693  782  proof (rule greatest_le [OF greatest_i], rule Lower_memI)  wenzelm@32960  783  fix z  wenzelm@32960  784  assume z: "z \ {a, x}"  wenzelm@32960  785  then show "y \ z"  wenzelm@32960  786  proof  ballarin@22063  787  have y': "y \ Lower L A"  ballarin@22063  788  apply (rule subsetD [where A = "Lower L (insert x A)"])  wenzelm@23463  789  apply (rule Lower_antimono)  wenzelm@32960  790  apply blast  wenzelm@32960  791  apply (rule y)  wenzelm@14693  792  done  wenzelm@14693  793  assume "z = a"  wenzelm@14693  794  with y' greatest_a show ?thesis by (fast dest: greatest_le)  wenzelm@32960  795  next  wenzelm@14693  796  assume "z \ {x}"  wenzelm@14693  797  with y L show ?thesis by blast  wenzelm@32960  798  qed  wenzelm@23350  799  qed (rule Lower_closed [THEN subsetD, OF y])  wenzelm@14693  800  next  ballarin@22063  801  from L show "insert x A \ carrier L" by simp  ballarin@22063  802  from greatest_i show "i \ carrier L" by simp  ballarin@14551  803  qed  wenzelm@23350  804  qed (rule P)  ballarin@14551  805 qed  ballarin@14551  806 ballarin@27713  807 lemma (in weak_lower_semilattice) finite_inf_greatest:  ballarin@22063  808  "[| finite A; A \ carrier L; A ~= {} |] ==> greatest L (\A) (Lower L A)"  berghofe@22265  809 proof (induct set: finite)  ballarin@14551  810  case empty then show ?case by simp  ballarin@14551  811 next  nipkow@15328  812  case (insert x A)  ballarin@14551  813  show ?case  ballarin@14551  814  proof (cases "A = {}")  ballarin@14551  815  case True  ballarin@27713  816  with insert show ?thesis  ballarin@27713  817  by simp (simp add: greatest_cong [OF weak_inf_of_singleton]  wenzelm@32960  818  inf_of_singleton_closed inf_of_singletonI)  ballarin@14551  819  next  ballarin@14551  820  case False  ballarin@14551  821  from insert show ?thesis  ballarin@14551  822  proof (rule_tac inf_insertI)  ballarin@22063  823  from False insert show "greatest L (\A) (Lower L A)" by simp  ballarin@14551  824  qed simp_all  ballarin@14551  825  qed  ballarin@14551  826 qed  ballarin@14551  827 ballarin@27713  828 lemma (in weak_lower_semilattice) finite_inf_insertI:  ballarin@22063  829  assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i"  ballarin@22063  830  and xA: "finite A" "x \ carrier L" "A \ carrier L"  ballarin@14551  831  shows "P (\ (insert x A))"  ballarin@14551  832 proof (cases "A = {}")  ballarin@14551  833  case True with P and xA show ?thesis  ballarin@27713  834  by (simp add: finite_inf_greatest)  ballarin@14551  835 next  ballarin@14551  836  case False with P and xA show ?thesis  ballarin@14551  837  by (simp add: inf_insertI finite_inf_greatest)  ballarin@14551  838 qed  ballarin@14551  839 ballarin@27713  840 lemma (in weak_lower_semilattice) finite_inf_closed [simp]:  ballarin@22063  841  "[| finite A; A \ carrier L; A ~= {} |] ==> \A \ carrier L"  berghofe@22265  842 proof (induct set: finite)  ballarin@14551  843  case empty then show ?case by simp  ballarin@14551  844 next  nipkow@15328  845  case insert then show ?case  ballarin@14551  846  by (rule_tac finite_inf_insertI) (simp_all)  ballarin@14551  847 qed  ballarin@14551  848 ballarin@27713  849 lemma (in weak_lower_semilattice) meet_left:  ballarin@22063  850  "[| x \ carrier L; y \ carrier L |] ==> x \ y \ x"  wenzelm@14693  851  by (rule meetI [folded meet_def]) (blast dest: greatest_mem)  ballarin@14551  852 ballarin@27713  853 lemma (in weak_lower_semilattice) meet_right:  ballarin@22063  854  "[| x \ carrier L; y \ carrier L |] ==> x \ y \ y"  wenzelm@14693  855  by (rule meetI [folded meet_def]) (blast dest: greatest_mem)  ballarin@14551  856 ballarin@27713  857 lemma (in weak_lower_semilattice) inf_of_two_greatest:  ballarin@22063  858  "[| x \ carrier L; y \ carrier L |] ==>  ballarin@22063  859  greatest L (\ {x, y}) (Lower L {x, y})"  ballarin@14551  860 proof (unfold inf_def)  ballarin@22063  861  assume L: "x \ carrier L" "y \ carrier L"  ballarin@22063  862  with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast  ballarin@14551  863  with L  ballarin@27713  864  show "greatest L (SOME z. greatest L z (Lower L {x, y})) (Lower L {x, y})"  ballarin@27713  865  by (fast intro: someI2 weak_greatest_unique) (* blast fails *)  ballarin@14551  866 qed  ballarin@14551  867 ballarin@27713  868 lemma (in weak_lower_semilattice) meet_le:  wenzelm@14693  869  assumes sub: "z \ x" "z \ y"  wenzelm@23350  870  and x: "x \ carrier L" and y: "y \ carrier L" and z: "z \ carrier L"  ballarin@14551  871  shows "z \ x \ y"  wenzelm@23350  872 proof (rule meetI [OF _ x y])  ballarin@14551  873  fix i  ballarin@22063  874  assume "greatest L i (Lower L {x, y})"  wenzelm@23350  875  with sub z show "z \ i" by (fast elim: greatest_le intro: Lower_memI)  ballarin@14551  876 qed  wenzelm@14693  877 ballarin@27713  878 lemma (in weak_lower_semilattice) weak_meet_assoc_lemma:  ballarin@22063  879  assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L"  ballarin@27713  880  shows "x \ (y \ z) .= \{x, y, z}"  ballarin@14551  881 proof (rule finite_inf_insertI)  ballarin@14551  882  txt {* The textbook argument in Jacobson I, p 457 *}  ballarin@14551  883  fix i  ballarin@22063  884  assume inf: "greatest L i (Lower L {x, y, z})"  ballarin@27713  885  show "x \ (y \ z) .= i"  nipkow@33657  886  proof (rule weak_le_antisym)  ballarin@14551  887  from inf L show "i \ x \ (y \ z)"  ballarin@27700  888  by (fastsimp intro!: meet_le elim: greatest_Lower_below)  ballarin@14551  889  next  ballarin@14551  890  from inf L show "x \ (y \ z) \ i"  ballarin@14551  891  by (erule_tac greatest_le)  ballarin@27713  892  (blast intro!: Lower_memI intro: le_trans meet_left meet_right meet_closed)  ballarin@27700  893  qed (simp_all add: L greatest_closed [OF inf])  ballarin@14551  894 qed (simp_all add: L)  ballarin@14551  895 ballarin@22063  896 lemma meet_comm:  ballarin@22063  897  fixes L (structure)  ballarin@22063  898  shows "x \ y = y \ x"  ballarin@14551  899  by (unfold meet_def) (simp add: insert_commute)  ballarin@14551  900 ballarin@27713  901 lemma (in weak_lower_semilattice) weak_meet_assoc:  ballarin@22063  902  assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L"  ballarin@27713  903  shows "(x \ y) \ z .= x \ (y \ z)"  ballarin@14551  904 proof -  ballarin@27713  905  (* FIXME: improved simp, see weak_join_assoc above *)  ballarin@14551  906  have "(x \ y) \ z = z \ (x \ y)" by (simp only: meet_comm)  ballarin@27713  907  also from L have "... .= \ {z, x, y}" by (simp add: weak_meet_assoc_lemma)  ballarin@14551  908  also from L have "... = \ {x, y, z}" by (simp add: insert_commute)  ballarin@27713  909  also from L have "... .= x \ (y \ z)" by (simp add: weak_meet_assoc_lemma [symmetric])  ballarin@27713  910  finally show ?thesis by (simp add: L)  ballarin@14551  911 qed  ballarin@14551  912 wenzelm@14693  913 ballarin@14551  914 subsection {* Total Orders *}  ballarin@14551  915 ballarin@27713  916 locale weak_total_order = weak_partial_order +  ballarin@22063  917  assumes total: "[| x \ carrier L; y \ carrier L |] ==> x \ y | y \ x"  ballarin@14551  918 ballarin@14551  919 text {* Introduction rule: the usual definition of total order *}  ballarin@14551  920 ballarin@27713  921 lemma (in weak_partial_order) weak_total_orderI:  ballarin@22063  922  assumes total: "!!x y. [| x \ carrier L; y \ carrier L |] ==> x \ y | y \ x"  ballarin@27713  923  shows "weak_total_order L"  haftmann@28823  924  proof qed (rule total)  ballarin@24087  925 ballarin@24087  926 text {* Total orders are lattices. *}  ballarin@24087  927 ballarin@29242  928 sublocale weak_total_order < weak: weak_lattice  haftmann@28823  929 proof  ballarin@24087  930  fix x y  ballarin@24087  931  assume L: "x \ carrier L" "y \ carrier L"  ballarin@24087  932  show "EX s. least L s (Upper L {x, y})"  ballarin@24087  933  proof -  ballarin@24087  934  note total L  ballarin@24087  935  moreover  ballarin@24087  936  {  ballarin@24087  937  assume "x \ y"  ballarin@24087  938  with L have "least L y (Upper L {x, y})"  ballarin@24087  939  by (rule_tac least_UpperI) auto  ballarin@24087  940  }  ballarin@24087  941  moreover  ballarin@24087  942  {  ballarin@24087  943  assume "y \ x"  ballarin@24087  944  with L have "least L x (Upper L {x, y})"  ballarin@24087  945  by (rule_tac least_UpperI) auto  ballarin@24087  946  }  ballarin@24087  947  ultimately show ?thesis by blast  ballarin@14551  948  qed  ballarin@24087  949 next  ballarin@24087  950  fix x y  ballarin@24087  951  assume L: "x \ carrier L" "y \ carrier L"  ballarin@24087  952  show "EX i. greatest L i (Lower L {x, y})"  ballarin@24087  953  proof -  ballarin@24087  954  note total L  ballarin@24087  955  moreover  ballarin@24087  956  {  ballarin@24087  957  assume "y \ x"  ballarin@24087  958  with L have "greatest L y (Lower L {x, y})"  ballarin@24087  959  by (rule_tac greatest_LowerI) auto  ballarin@24087  960  }  ballarin@24087  961  moreover  ballarin@24087  962  {  ballarin@24087  963  assume "x \ y"  ballarin@24087  964  with L have "greatest L x (Lower L {x, y})"  ballarin@24087  965  by (rule_tac greatest_LowerI) auto  ballarin@24087  966  }  ballarin@24087  967  ultimately show ?thesis by blast  ballarin@24087  968  qed  ballarin@24087  969 qed  ballarin@14551  970 wenzelm@14693  971 ballarin@27717  972 subsection {* Complete Lattices *}  ballarin@14551  973 ballarin@27713  974 locale weak_complete_lattice = weak_lattice +  ballarin@14551  975  assumes sup_exists:  ballarin@22063  976  "[| A \ carrier L |] ==> EX s. least L s (Upper L A)"  ballarin@14551  977  and inf_exists:  ballarin@22063  978  "[| A \ carrier L |] ==> EX i. greatest L i (Lower L A)"  ballarin@21041  979 ballarin@14551  980 text {* Introduction rule: the usual definition of complete lattice *}  ballarin@14551  981 ballarin@27713  982 lemma (in weak_partial_order) weak_complete_latticeI:  ballarin@14551  983  assumes sup_exists:  ballarin@22063  984  "!!A. [| A \ carrier L |] ==> EX s. least L s (Upper L A)"  ballarin@14551  985  and inf_exists:  ballarin@22063  986  "!!A. [| A \ carrier L |] ==> EX i. greatest L i (Lower L A)"  ballarin@27713  987  shows "weak_complete_lattice L"  haftmann@28823  988  proof qed (auto intro: sup_exists inf_exists)  ballarin@14551  989 wenzelm@35847  990 definition  ballarin@22063  991  top :: "_ => 'a" ("\\")  wenzelm@35848  992  where "\\<^bsub>L\<^esub> = sup L (carrier L)"  ballarin@21041  993 wenzelm@35847  994 definition  ballarin@22063  995  bottom :: "_ => 'a" ("\\")  wenzelm@35848  996  where "\\<^bsub>L\<^esub> = inf L (carrier L)"  ballarin@14551  997 ballarin@14551  998 ballarin@27713  999 lemma (in weak_complete_lattice) supI:  ballarin@22063  1000  "[| !!l. least L l (Upper L A) ==> P l; A \ carrier L |]  wenzelm@14651  1001  ==> P (\A)"  ballarin@14551  1002 proof (unfold sup_def)  ballarin@22063  1003  assume L: "A \ carrier L"  ballarin@22063  1004  and P: "!!l. least L l (Upper L A) ==> P l"  ballarin@22063  1005  with sup_exists obtain s where "least L s (Upper L A)" by blast  ballarin@27713  1006  with L show "P (SOME l. least L l (Upper L A))"  ballarin@27713  1007  by (fast intro: someI2 weak_least_unique P)  ballarin@14551  1008 qed  ballarin@14551  1009 ballarin@27713  1010 lemma (in weak_complete_lattice) sup_closed [simp]:  ballarin@22063  1011  "A \ carrier L ==> \A \ carrier L"  ballarin@14551  1012  by (rule supI) simp_all  ballarin@14551  1013 ballarin@27713  1014 lemma (in weak_complete_lattice) top_closed [simp, intro]:  ballarin@22063  1015  "\ \ carrier L"  ballarin@14551  1016  by (unfold top_def) simp  ballarin@14551  1017 ballarin@27713  1018 lemma (in weak_complete_lattice) infI:  ballarin@22063  1019  "[| !!i. greatest L i (Lower L A) ==> P i; A \ carrier L |]  wenzelm@14693  1020  ==> P (\A)"  ballarin@14551  1021 proof (unfold inf_def)  ballarin@22063  1022  assume L: "A \ carrier L"  ballarin@22063  1023  and P: "!!l. greatest L l (Lower L A) ==> P l"  ballarin@22063  1024  with inf_exists obtain s where "greatest L s (Lower L A)" by blast  ballarin@27713  1025  with L show "P (SOME l. greatest L l (Lower L A))"  ballarin@27713  1026  by (fast intro: someI2 weak_greatest_unique P)  ballarin@14551  1027 qed  ballarin@14551  1028 ballarin@27713  1029 lemma (in weak_complete_lattice) inf_closed [simp]:  ballarin@22063  1030  "A \ carrier L ==> \A \ carrier L"  ballarin@14551  1031  by (rule infI) simp_all  ballarin@14551  1032 ballarin@27713  1033 lemma (in weak_complete_lattice) bottom_closed [simp, intro]:  ballarin@22063  1034  "\ \ carrier L"  ballarin@14551  1035  by (unfold bottom_def) simp  ballarin@14551  1036 ballarin@14551  1037 text {* Jacobson: Theorem 8.1 *}  ballarin@14551  1038 ballarin@22063  1039 lemma Lower_empty [simp]:  ballarin@22063  1040  "Lower L {} = carrier L"  ballarin@14551  1041  by (unfold Lower_def) simp  ballarin@14551  1042 ballarin@22063  1043 lemma Upper_empty [simp]:  ballarin@22063  1044  "Upper L {} = carrier L"  ballarin@14551  1045  by (unfold Upper_def) simp  ballarin@14551  1046 ballarin@27713  1047 theorem (in weak_partial_order) weak_complete_lattice_criterion1:  ballarin@27713  1048  assumes top_exists: "EX g. greatest L g (carrier L)"  ballarin@27713  1049  and inf_exists:  ballarin@27713  1050  "!!A. [| A \ carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)"  ballarin@27713  1051  shows "weak_complete_lattice L"  ballarin@27713  1052 proof (rule weak_complete_latticeI)  ballarin@27713  1053  from top_exists obtain top where top: "greatest L top (carrier L)" ..  ballarin@27713  1054  fix A  ballarin@27713  1055  assume L: "A \ carrier L"  ballarin@27713  1056  let ?B = "Upper L A"  ballarin@27713  1057  from L top have "top \ ?B" by (fast intro!: Upper_memI intro: greatest_le)  ballarin@27713  1058  then have B_non_empty: "?B ~= {}" by fast  ballarin@27713  1059  have B_L: "?B \ carrier L" by simp  ballarin@27713  1060  from inf_exists [OF B_L B_non_empty]  ballarin@27713  1061  obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..  ballarin@27713  1062  have "least L b (Upper L A)"  ballarin@27713  1063 apply (rule least_UpperI)  ballarin@27713  1064  apply (rule greatest_le [where A = "Lower L ?B"])  ballarin@27713  1065  apply (rule b_inf_B)  ballarin@27713  1066  apply (rule Lower_memI)  ballarin@27713  1067  apply (erule Upper_memD [THEN conjunct1])  ballarin@27713  1068  apply assumption  ballarin@27713  1069  apply (rule L)  ballarin@27713  1070  apply (fast intro: L [THEN subsetD])  ballarin@27713  1071  apply (erule greatest_Lower_below [OF b_inf_B])  ballarin@27713  1072  apply simp  ballarin@27713  1073  apply (rule L)  ballarin@27713  1074 apply (rule greatest_closed [OF b_inf_B])  ballarin@27713  1075 done  ballarin@27713  1076  then show "EX s. least L s (Upper L A)" ..  ballarin@27713  1077 next  ballarin@27713  1078  fix A  ballarin@27713  1079  assume L: "A \ carrier L"  ballarin@27713  1080  show "EX i. greatest L i (Lower L A)"  ballarin@27713  1081  proof (cases "A = {}")  ballarin@27713  1082  case True then show ?thesis  ballarin@27713  1083  by (simp add: top_exists)  ballarin@27713  1084  next  ballarin@27713  1085  case False with L show ?thesis  ballarin@27713  1086  by (rule inf_exists)  ballarin@27713  1087  qed  ballarin@27713  1088 qed  ballarin@27713  1089 ballarin@27713  1090 (* TODO: prove dual version *)  ballarin@27713  1091 ballarin@27713  1092 ballarin@27713  1093 subsection {* Orders and Lattices where @{text eq} is the Equality *}  ballarin@27713  1094 ballarin@27713  1095 locale partial_order = weak_partial_order +  ballarin@27713  1096  assumes eq_is_equal: "op .= = op ="  ballarin@27713  1097 begin  ballarin@27713  1098 nipkow@33657  1099 declare weak_le_antisym [rule del]  ballarin@27713  1100 nipkow@33657  1101 lemma le_antisym [intro]:  ballarin@27713  1102  "[| x \ y; y \ x; x \ carrier L; y \ carrier L |] ==> x = y"  nipkow@33657  1103  using weak_le_antisym unfolding eq_is_equal .  ballarin@27713  1104 ballarin@27713  1105 lemma lless_eq:  ballarin@27713  1106  "x \ y \ x \ y & x \ y"  ballarin@27713  1107  unfolding lless_def by (simp add: eq_is_equal)  ballarin@27713  1108 ballarin@27713  1109 lemma lless_asym:  ballarin@27713  1110  assumes "a \ carrier L" "b \ carrier L"  ballarin@27713  1111  and "a \ b" "b \ a"  ballarin@27713  1112  shows "P"  ballarin@27713  1113  using assms unfolding lless_eq by auto  ballarin@27713  1114 ballarin@27713  1115 end  ballarin@27713  1116 ballarin@27713  1117 ballarin@27717  1118 text {* Least and greatest, as predicate *}  ballarin@27713  1119 ballarin@27713  1120 lemma (in partial_order) least_unique:  ballarin@27713  1121  "[| least L x A; least L y A |] ==> x = y"  ballarin@27713  1122  using weak_least_unique unfolding eq_is_equal .  ballarin@27713  1123 ballarin@27713  1124 lemma (in partial_order) greatest_unique:  ballarin@27713  1125  "[| greatest L x A; greatest L y A |] ==> x = y"  ballarin@27713  1126  using weak_greatest_unique unfolding eq_is_equal .  ballarin@27713  1127 ballarin@27713  1128 ballarin@27717  1129 text {* Lattices *}  ballarin@27713  1130 ballarin@27713  1131 locale upper_semilattice = partial_order +  ballarin@27713  1132  assumes sup_of_two_exists:  ballarin@27713  1133  "[| x \ carrier L; y \ carrier L |] ==> EX s. least L s (Upper L {x, y})"  ballarin@27713  1134 ballarin@29242  1135 sublocale upper_semilattice < weak: weak_upper_semilattice  haftmann@28823  1136  proof qed (rule sup_of_two_exists)  ballarin@27713  1137 ballarin@27713  1138 locale lower_semilattice = partial_order +  ballarin@27713  1139  assumes inf_of_two_exists:  ballarin@27713  1140  "[| x \ carrier L; y \ carrier L |] ==> EX s. greatest L s (Lower L {x, y})"  ballarin@27713  1141 ballarin@29242  1142 sublocale lower_semilattice < weak: weak_lower_semilattice  haftmann@28823  1143  proof qed (rule inf_of_two_exists)  ballarin@27713  1144 ballarin@27713  1145 locale lattice = upper_semilattice + lower_semilattice  ballarin@27713  1146 ballarin@27713  1147 ballarin@27717  1148 text {* Supremum *}  ballarin@27713  1149 ballarin@27714  1150 declare (in partial_order) weak_sup_of_singleton [simp del]  ballarin@27713  1151 ballarin@27714  1152 lemma (in partial_order) sup_of_singleton [simp]:  ballarin@27713  1153  "x \ carrier L ==> \{x} = x"  ballarin@27713  1154  using weak_sup_of_singleton unfolding eq_is_equal .  ballarin@27713  1155 ballarin@27714  1156 lemma (in upper_semilattice) join_assoc_lemma:  ballarin@27713  1157  assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L"  ballarin@27713  1158  shows "x \ (y \ z) = \{x, y, z}"  ballarin@27714  1159  using weak_join_assoc_lemma L unfolding eq_is_equal .  ballarin@27713  1160 ballarin@27713  1161 lemma (in upper_semilattice) join_assoc:  ballarin@27713  1162  assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L"  ballarin@27713  1163  shows "(x \ y) \ z = x \ (y \ z)"  ballarin@27714  1164  using weak_join_assoc L unfolding eq_is_equal .  ballarin@27713  1165 ballarin@27713  1166 ballarin@27717  1167 text {* Infimum *}  ballarin@27713  1168 ballarin@27714  1169 declare (in partial_order) weak_inf_of_singleton [simp del]  ballarin@27713  1170 ballarin@27714  1171 lemma (in partial_order) inf_of_singleton [simp]:  ballarin@27713  1172  "x \ carrier L ==> \{x} = x"  ballarin@27713  1173  using weak_inf_of_singleton unfolding eq_is_equal .  ballarin@27713  1174 ballarin@27713  1175 text {* Condition on @{text A}: infimum exists. *}  ballarin@27713  1176 ballarin@27714  1177 lemma (in lower_semilattice) meet_assoc_lemma:  ballarin@27713  1178  assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L"  ballarin@27713  1179  shows "x \ (y \ z) = \{x, y, z}"  ballarin@27714  1180  using weak_meet_assoc_lemma L unfolding eq_is_equal .  ballarin@27713  1181 ballarin@27713  1182 lemma (in lower_semilattice) meet_assoc:  ballarin@27713  1183  assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L"  ballarin@27713  1184  shows "(x \ y) \ z = x \ (y \ z)"  ballarin@27714  1185  using weak_meet_assoc L unfolding eq_is_equal .  ballarin@27713  1186 ballarin@27713  1187 ballarin@27717  1188 text {* Total Orders *}  ballarin@27713  1189 ballarin@27713  1190 locale total_order = partial_order +  haftmann@28823  1191  assumes total_order_total: "[| x \ carrier L; y \ carrier L |] ==> x \ y | y \ x"  ballarin@27713  1192 ballarin@29242  1193 sublocale total_order < weak: weak_total_order  haftmann@28823  1194  proof qed (rule total_order_total)  ballarin@27713  1195 ballarin@27713  1196 text {* Introduction rule: the usual definition of total order *}  ballarin@27713  1197 ballarin@27713  1198 lemma (in partial_order) total_orderI:  ballarin@27713  1199  assumes total: "!!x y. [| x \ carrier L; y \ carrier L |] ==> x \ y | y \ x"  ballarin@27713  1200  shows "total_order L"  haftmann@28823  1201  proof qed (rule total)  ballarin@27713  1202 ballarin@27713  1203 text {* Total orders are lattices. *}  ballarin@27713  1204 ballarin@29242  1205 sublocale total_order < weak: lattice  haftmann@28823  1206  proof qed (auto intro: sup_of_two_exists inf_of_two_exists)  ballarin@27713  1207 ballarin@27713  1208 ballarin@27717  1209 text {* Complete lattices *}  ballarin@27713  1210 ballarin@27713  1211 locale complete_lattice = lattice +  ballarin@27713  1212  assumes sup_exists:  ballarin@27713  1213  "[| A \ carrier L |] ==> EX s. least L s (Upper L A)"  ballarin@27713  1214  and inf_exists:  ballarin@27713  1215  "[| A \ carrier L |] ==> EX i. greatest L i (Lower L A)"  ballarin@27713  1216 ballarin@29242  1217 sublocale complete_lattice < weak: weak_complete_lattice  haftmann@28823  1218  proof qed (auto intro: sup_exists inf_exists)  ballarin@27713  1219 ballarin@27713  1220 text {* Introduction rule: the usual definition of complete lattice *}  ballarin@27713  1221 ballarin@27713  1222 lemma (in partial_order) complete_latticeI:  ballarin@27713  1223  assumes sup_exists:  ballarin@27713  1224  "!!A. [| A \ carrier L |] ==> EX s. least L s (Upper L A)"  ballarin@27713  1225  and inf_exists:  ballarin@27713  1226  "!!A. [| A \ carrier L |] ==> EX i. greatest L i (Lower L A)"  ballarin@27713  1227  shows "complete_lattice L"  haftmann@28823  1228  proof qed (auto intro: sup_exists inf_exists)  ballarin@27713  1229 ballarin@14551  1230 theorem (in partial_order) complete_lattice_criterion1:  ballarin@22063  1231  assumes top_exists: "EX g. greatest L g (carrier L)"  ballarin@14551  1232  and inf_exists:  ballarin@22063  1233  "!!A. [| A \ carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)"  ballarin@22063  1234  shows "complete_lattice L"  ballarin@14551  1235 proof (rule complete_latticeI)  ballarin@22063  1236  from top_exists obtain top where top: "greatest L top (carrier L)" ..  ballarin@14551  1237  fix A  ballarin@22063  1238  assume L: "A \ carrier L"  ballarin@22063  1239  let ?B = "Upper L A"  ballarin@14551  1240  from L top have "top \ ?B" by (fast intro!: Upper_memI intro: greatest_le)  ballarin@14551  1241  then have B_non_empty: "?B ~= {}" by fast  ballarin@22063  1242  have B_L: "?B \ carrier L" by simp  ballarin@14551  1243  from inf_exists [OF B_L B_non_empty]  ballarin@22063  1244  obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..  ballarin@22063  1245  have "least L b (Upper L A)"  ballarin@14551  1246 apply (rule least_UpperI)  ballarin@22063  1247  apply (rule greatest_le [where A = "Lower L ?B"])  ballarin@14551  1248  apply (rule b_inf_B)  ballarin@14551  1249  apply (rule Lower_memI)  ballarin@27713  1250  apply (erule Upper_memD [THEN conjunct1])  ballarin@14551  1251  apply assumption  ballarin@14551  1252  apply (rule L)  ballarin@14551  1253  apply (fast intro: L [THEN subsetD])  ballarin@27700  1254  apply (erule greatest_Lower_below [OF b_inf_B])  ballarin@14551  1255  apply simp  ballarin@14551  1256  apply (rule L)  ballarin@27700  1257 apply (rule greatest_closed [OF b_inf_B])  ballarin@14551  1258 done  ballarin@22063  1259  then show "EX s. least L s (Upper L A)" ..  ballarin@14551  1260 next  ballarin@14551  1261  fix A  ballarin@22063  1262  assume L: "A \ carrier L"  ballarin@22063  1263  show "EX i. greatest L i (Lower L A)"  ballarin@14551  1264  proof (cases "A = {}")  ballarin@14551  1265  case True then show ?thesis  ballarin@14551  1266  by (simp add: top_exists)  ballarin@14551  1267  next  ballarin@14551  1268  case False with L show ?thesis  ballarin@14551  1269  by (rule inf_exists)  ballarin@14551  1270  qed  ballarin@14551  1271 qed  ballarin@14551  1272 ballarin@14551  1273 (* TODO: prove dual version *)  ballarin@14551  1274 ballarin@20318  1275 ballarin@14551  1276 subsection {* Examples *}  ballarin@14551  1277 ballarin@27717  1278 subsubsection {* The Powerset of a Set is a Complete Lattice *}  ballarin@14551  1279 ballarin@14551  1280 theorem powerset_is_complete_lattice:  ballarin@27713  1281  "complete_lattice (| carrier = Pow A, eq = op =, le = op \ |)"  ballarin@22063  1282  (is "complete_lattice ?L")  ballarin@14551  1283 proof (rule partial_order.complete_latticeI)  ballarin@22063  1284  show "partial_order ?L"  haftmann@28823  1285  proof qed auto  ballarin@14551  1286 next  ballarin@14551  1287  fix B  berghofe@26805  1288  assume B: "B \ carrier ?L"  berghofe@26805  1289  show "EX s. least ?L s (Upper ?L B)"  berghofe@26805  1290  proof  berghofe@26805  1291  from B show "least ?L (\ B) (Upper ?L B)"  berghofe@26805  1292  by (fastsimp intro!: least_UpperI simp: Upper_def)  berghofe@26805  1293  qed  ballarin@14551  1294 next  ballarin@14551  1295  fix B  berghofe@26805  1296  assume B: "B \ carrier ?L"  berghofe@26805  1297  show "EX i. greatest ?L i (Lower ?L B)"  berghofe@26805  1298  proof  berghofe@26805  1299  from B show "greatest ?L (\ B \ A) (Lower ?L B)"  berghofe@26805  1300  txt {* @{term "\ B"} is not the infimum of @{term B}:  wenzelm@32960  1301  @{term "\ {} = UNIV"} which is in general bigger than @{term "A"}! *}  berghofe@26805  1302  by (fastsimp intro!: greatest_LowerI simp: Lower_def)  berghofe@26805  1303  qed  ballarin@14551  1304 qed  ballarin@14551  1305 ballarin@14751  1306 text {* An other example, that of the lattice of subgroups of a group,  ballarin@14751  1307  can be found in Group theory (Section~\ref{sec:subgroup-lattice}). *}  ballarin@14551  1308 wenzelm@14693  1309 end