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