src/HOL/Algebra/Lattice.thy
 author ballarin Tue Jul 31 14:18:24 2007 +0200 (2007-07-31) changeset 24087 eb025d149a34 parent 23463 9953ff53cc64 child 26805 27941d7d9a11 permissions -rw-r--r--
Proper interpretation of total orders in lattices.
 ballarin@14551  1 (*  wenzelm@14706  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@14551  6 *)  ballarin@14551  7 ballarin@20318  8 theory Lattice imports Main begin  ballarin@14551  9 ballarin@20318  10 ballarin@20318  11 section {* Orders and Lattices *}  ballarin@14751  12 ballarin@14751  13 text {* Object with a carrier set. *}  ballarin@14751  14 ballarin@14751  15 record 'a partial_object =  ballarin@14751  16  carrier :: "'a set"  ballarin@14551  17 ballarin@20318  18 ballarin@14551  19 subsection {* Partial Orders *}  ballarin@14551  20 ballarin@22063  21 record 'a order = "'a partial_object" +  ballarin@22063  22  le :: "['a, 'a] => bool" (infixl "\\" 50)  ballarin@21041  23 ballarin@22063  24 locale partial_order =  ballarin@22063  25  fixes L (structure)  ballarin@14551  26  assumes refl [intro, simp]:  ballarin@22063  27  "x \ carrier L ==> x \ x"  ballarin@14551  28  and anti_sym [intro]:  ballarin@22063  29  "[| x \ y; y \ x; x \ carrier L; y \ carrier L |] ==> x = y"  ballarin@14551  30  and trans [trans]:  ballarin@14551  31  "[| x \ y; y \ z;  ballarin@22063  32  x \ carrier L; y \ carrier L; z \ carrier L |] ==> x \ z"  ballarin@22063  33 ballarin@22063  34 constdefs (structure L)  ballarin@22063  35  lless :: "[_, 'a, 'a] => bool" (infixl "\\" 50)  ballarin@22063  36  "x \ y == x \ y & x ~= y"  ballarin@22063  37 ballarin@22063  38  -- {* Upper and lower bounds of a set. *}  ballarin@22063  39  Upper :: "[_, 'a set] => 'a set"  ballarin@22063  40  "Upper L A == {u. (ALL x. x \ A \ carrier L --> x \ u)} \  ballarin@22063  41  carrier L"  ballarin@22063  42 ballarin@22063  43  Lower :: "[_, 'a set] => 'a set"  ballarin@22063  44  "Lower L A == {l. (ALL x. x \ A \ carrier L --> l \ x)} \  ballarin@22063  45  carrier L"  ballarin@22063  46 ballarin@22063  47  -- {* Least and greatest, as predicate. *}  ballarin@22063  48  least :: "[_, 'a, 'a set] => bool"  ballarin@22063  49  "least L l A == A \ carrier L & l \ A & (ALL x : A. l \ x)"  ballarin@22063  50 ballarin@22063  51  greatest :: "[_, 'a, 'a set] => bool"  ballarin@22063  52  "greatest L g A == A \ carrier L & g \ A & (ALL x : A. x \ g)"  ballarin@22063  53 ballarin@22063  54  -- {* Supremum and infimum *}  ballarin@22063  55  sup :: "[_, 'a set] => 'a" ("\\_" [90] 90)  ballarin@22063  56  "\A == THE x. least L x (Upper L A)"  ballarin@22063  57 ballarin@22063  58  inf :: "[_, 'a set] => 'a" ("\\_" [90] 90)  ballarin@22063  59  "\A == THE x. greatest L x (Lower L A)"  ballarin@22063  60 ballarin@22063  61  join :: "[_, 'a, 'a] => 'a" (infixl "\\" 65)  ballarin@22063  62  "x \ y == sup L {x, y}"  ballarin@22063  63 ballarin@22063  64  meet :: "[_, 'a, 'a] => 'a" (infixl "\\" 70)  ballarin@22063  65  "x \ y == inf L {x, y}"  ballarin@14551  66 wenzelm@14651  67 wenzelm@14651  68 subsubsection {* Upper *}  ballarin@14551  69 ballarin@22063  70 lemma Upper_closed [intro, simp]:  ballarin@22063  71  "Upper L A \ carrier L"  ballarin@14551  72  by (unfold Upper_def) clarify  ballarin@14551  73 ballarin@22063  74 lemma UpperD [dest]:  ballarin@22063  75  fixes L (structure)  ballarin@22063  76  shows "[| u \ Upper L A; x \ A; A \ carrier L |] ==> x \ u"  wenzelm@14693  77  by (unfold Upper_def) blast  ballarin@14551  78 ballarin@22063  79 lemma Upper_memI:  ballarin@22063  80  fixes L (structure)  ballarin@22063  81  shows "[| !! y. y \ A ==> y \ x; x \ carrier L |] ==> x \ Upper L A"  wenzelm@14693  82  by (unfold Upper_def) blast  ballarin@14551  83 ballarin@22063  84 lemma Upper_antimono:  ballarin@22063  85  "A \ B ==> Upper L B \ Upper L A"  ballarin@14551  86  by (unfold Upper_def) blast  ballarin@14551  87 wenzelm@14651  88 wenzelm@14651  89 subsubsection {* Lower *}  ballarin@14551  90 ballarin@22063  91 lemma Lower_closed [intro, simp]:  ballarin@22063  92  "Lower L A \ carrier L"  ballarin@14551  93  by (unfold Lower_def) clarify  ballarin@14551  94 ballarin@22063  95 lemma LowerD [dest]:  ballarin@22063  96  fixes L (structure)  ballarin@22063  97  shows "[| l \ Lower L A; x \ A; A \ carrier L |] ==> l \ x"  wenzelm@14693  98  by (unfold Lower_def) blast  ballarin@14551  99 ballarin@22063  100 lemma Lower_memI:  ballarin@22063  101  fixes L (structure)  ballarin@22063  102  shows "[| !! y. y \ A ==> x \ y; x \ carrier L |] ==> x \ Lower L A"  wenzelm@14693  103  by (unfold Lower_def) blast  ballarin@14551  104 ballarin@22063  105 lemma Lower_antimono:  ballarin@22063  106  "A \ B ==> Lower L B \ Lower L A"  ballarin@14551  107  by (unfold Lower_def) blast  ballarin@14551  108 wenzelm@14651  109 wenzelm@14651  110 subsubsection {* least *}  ballarin@14551  111 ballarin@22063  112 lemma least_carrier [intro, simp]:  ballarin@22063  113  shows "least L l A ==> l \ carrier L"  ballarin@14551  114  by (unfold least_def) fast  ballarin@14551  115 ballarin@22063  116 lemma least_mem:  ballarin@22063  117  "least L l A ==> l \ A"  ballarin@14551  118  by (unfold least_def) fast  ballarin@14551  119 ballarin@14551  120 lemma (in partial_order) least_unique:  ballarin@22063  121  "[| least L x A; least L y A |] ==> x = y"  ballarin@14551  122  by (unfold least_def) blast  ballarin@14551  123 ballarin@22063  124 lemma least_le:  ballarin@22063  125  fixes L (structure)  ballarin@22063  126  shows "[| least L x A; a \ A |] ==> x \ a"  ballarin@14551  127  by (unfold least_def) fast  ballarin@14551  128 ballarin@22063  129 lemma least_UpperI:  ballarin@22063  130  fixes L (structure)  ballarin@14551  131  assumes above: "!! x. x \ A ==> x \ s"  ballarin@22063  132  and below: "!! y. y \ Upper L A ==> s \ y"  ballarin@22063  133  and L: "A \ carrier L" "s \ carrier L"  ballarin@22063  134  shows "least L s (Upper L A)"  wenzelm@14693  135 proof -  ballarin@22063  136  have "Upper L A \ carrier L" by simp  ballarin@22063  137  moreover from above L have "s \ Upper L A" by (simp add: Upper_def)  ballarin@22063  138  moreover from below have "ALL x : Upper L A. s \ x" by fast  wenzelm@14693  139  ultimately show ?thesis by (simp add: least_def)  ballarin@14551  140 qed  ballarin@14551  141 wenzelm@14651  142 wenzelm@14651  143 subsubsection {* greatest *}  ballarin@14551  144 ballarin@22063  145 lemma greatest_carrier [intro, simp]:  ballarin@22063  146  shows "greatest L l A ==> l \ carrier L"  ballarin@14551  147  by (unfold greatest_def) fast  ballarin@14551  148 ballarin@22063  149 lemma greatest_mem:  ballarin@22063  150  "greatest L l A ==> l \ A"  ballarin@14551  151  by (unfold greatest_def) fast  ballarin@14551  152 ballarin@14551  153 lemma (in partial_order) greatest_unique:  ballarin@22063  154  "[| greatest L x A; greatest L y A |] ==> x = y"  ballarin@14551  155  by (unfold greatest_def) blast  ballarin@14551  156 ballarin@22063  157 lemma greatest_le:  ballarin@22063  158  fixes L (structure)  ballarin@22063  159  shows "[| greatest L x A; a \ A |] ==> a \ x"  ballarin@14551  160  by (unfold greatest_def) fast  ballarin@14551  161 ballarin@22063  162 lemma greatest_LowerI:  ballarin@22063  163  fixes L (structure)  ballarin@14551  164  assumes below: "!! x. x \ A ==> i \ x"  ballarin@22063  165  and above: "!! y. y \ Lower L A ==> y \ i"  ballarin@22063  166  and L: "A \ carrier L" "i \ carrier L"  ballarin@22063  167  shows "greatest L i (Lower L A)"  wenzelm@14693  168 proof -  ballarin@22063  169  have "Lower L A \ carrier L" by simp  ballarin@22063  170  moreover from below L have "i \ Lower L A" by (simp add: Lower_def)  ballarin@22063  171  moreover from above have "ALL x : Lower L A. x \ i" by fast  wenzelm@14693  172  ultimately show ?thesis by (simp add: greatest_def)  ballarin@14551  173 qed  ballarin@14551  174 wenzelm@14693  175 ballarin@14551  176 subsection {* Lattices *}  ballarin@14551  177 ballarin@14551  178 locale lattice = partial_order +  ballarin@14551  179  assumes sup_of_two_exists:  ballarin@22063  180  "[| x \ carrier L; y \ carrier L |] ==> EX s. least L s (Upper L {x, y})"  ballarin@14551  181  and inf_of_two_exists:  ballarin@22063  182  "[| x \ carrier L; y \ carrier L |] ==> EX s. greatest L s (Lower L {x, y})"  ballarin@14551  183 ballarin@22063  184 lemma least_Upper_above:  ballarin@22063  185  fixes L (structure)  ballarin@22063  186  shows "[| least L s (Upper L A); x \ A; A \ carrier L |] ==> x \ s"  ballarin@14551  187  by (unfold least_def) blast  ballarin@14551  188 ballarin@22063  189 lemma greatest_Lower_above:  ballarin@22063  190  fixes L (structure)  ballarin@22063  191  shows "[| greatest L i (Lower L A); x \ A; A \ carrier L |] ==> i \ x"  ballarin@14551  192  by (unfold greatest_def) blast  ballarin@14551  193 wenzelm@14666  194 ballarin@14551  195 subsubsection {* Supremum *}  ballarin@14551  196 ballarin@14551  197 lemma (in lattice) joinI:  ballarin@22063  198  "[| !!l. least L l (Upper L {x, y}) ==> P l; x \ carrier L; y \ carrier L |]  ballarin@14551  199  ==> P (x \ y)"  ballarin@14551  200 proof (unfold join_def sup_def)  ballarin@22063  201  assume L: "x \ carrier L" "y \ carrier L"  ballarin@22063  202  and P: "!!l. least L l (Upper L {x, y}) ==> P l"  ballarin@22063  203  with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast  ballarin@22063  204  with L show "P (THE l. least L l (Upper L {x, y}))"  wenzelm@14693  205  by (fast intro: theI2 least_unique P)  ballarin@14551  206 qed  ballarin@14551  207 ballarin@14551  208 lemma (in lattice) join_closed [simp]:  ballarin@22063  209  "[| x \ carrier L; y \ carrier L |] ==> x \ y \ carrier L"  ballarin@22063  210  by (rule joinI) (rule least_carrier)  ballarin@14551  211 ballarin@22063  212 lemma (in partial_order) sup_of_singletonI: (* only reflexivity needed ? *)  ballarin@22063  213  "x \ carrier L ==> least L x (Upper L {x})"  ballarin@14551  214  by (rule least_UpperI) fast+  ballarin@14551  215 ballarin@14551  216 lemma (in partial_order) sup_of_singleton [simp]:  ballarin@22063  217  "x \ carrier L ==> \{x} = x"  ballarin@14551  218  by (unfold sup_def) (blast intro: least_unique least_UpperI sup_of_singletonI)  ballarin@14551  219 wenzelm@14666  220 wenzelm@14666  221 text {* Condition on @{text A}: supremum exists. *}  ballarin@14551  222 ballarin@14551  223 lemma (in lattice) sup_insertI:  ballarin@22063  224  "[| !!s. least L s (Upper L (insert x A)) ==> P s;  ballarin@22063  225  least L a (Upper L A); x \ carrier L; A \ carrier L |]  wenzelm@14693  226  ==> P (\(insert x A))"  ballarin@14551  227 proof (unfold sup_def)  ballarin@22063  228  assume L: "x \ carrier L" "A \ carrier L"  ballarin@22063  229  and P: "!!l. least L l (Upper L (insert x A)) ==> P l"  ballarin@22063  230  and least_a: "least L a (Upper L A)"  ballarin@22063  231  from L least_a have La: "a \ carrier L" by simp  ballarin@14551  232  from L sup_of_two_exists least_a  ballarin@22063  233  obtain s where least_s: "least L s (Upper L {a, x})" by blast  ballarin@22063  234  show "P (THE l. least L l (Upper L (insert x A)))"  wenzelm@14693  235  proof (rule theI2)  ballarin@22063  236  show "least L s (Upper L (insert x A))"  ballarin@14551  237  proof (rule least_UpperI)  ballarin@14551  238  fix z  wenzelm@14693  239  assume "z \ insert x A"  wenzelm@14693  240  then show "z \ s"  wenzelm@14693  241  proof  wenzelm@14693  242  assume "z = x" then show ?thesis  wenzelm@14693  243  by (simp add: least_Upper_above [OF least_s] L La)  wenzelm@14693  244  next  wenzelm@14693  245  assume "z \ A"  wenzelm@14693  246  with L least_s least_a show ?thesis  wenzelm@14693  247  by (rule_tac trans [where y = a]) (auto dest: least_Upper_above)  wenzelm@14693  248  qed  wenzelm@14693  249  next  wenzelm@14693  250  fix y  ballarin@22063  251  assume y: "y \ Upper L (insert x A)"  wenzelm@14693  252  show "s \ y"  wenzelm@14693  253  proof (rule least_le [OF least_s], rule Upper_memI)  wenzelm@14693  254  fix z  wenzelm@14693  255  assume z: "z \ {a, x}"  wenzelm@14693  256  then show "z \ y"  wenzelm@14693  257  proof  ballarin@22063  258  have y': "y \ Upper L A"  ballarin@22063  259  apply (rule subsetD [where A = "Upper L (insert x A)"])  wenzelm@23463  260  apply (rule Upper_antimono)  wenzelm@23463  261  apply blast  wenzelm@23463  262  apply (rule y)  wenzelm@14693  263  done  wenzelm@14693  264  assume "z = a"  wenzelm@14693  265  with y' least_a show ?thesis by (fast dest: least_le)  wenzelm@14693  266  next  wenzelm@14693  267  assume "z \ {x}" (* FIXME "z = x"; declare specific elim rule for "insert x {}" (!?) *)  wenzelm@14693  268  with y L show ?thesis by blast  wenzelm@14693  269  qed  wenzelm@23350  270  qed (rule Upper_closed [THEN subsetD, OF y])  wenzelm@14693  271  next  ballarin@22063  272  from L show "insert x A \ carrier L" by simp  ballarin@22063  273  from least_s show "s \ carrier L" by simp  ballarin@14551  274  qed  ballarin@14551  275  next  ballarin@14551  276  fix l  ballarin@22063  277  assume least_l: "least L l (Upper L (insert x A))"  ballarin@14551  278  show "l = s"  ballarin@14551  279  proof (rule least_unique)  ballarin@22063  280  show "least L s (Upper L (insert x A))"  ballarin@14551  281  proof (rule least_UpperI)  wenzelm@14693  282  fix z  wenzelm@14693  283  assume "z \ insert x A"  wenzelm@14693  284  then show "z \ s"  wenzelm@14693  285  proof  wenzelm@14693  286  assume "z = x" then show ?thesis  wenzelm@14693  287  by (simp add: least_Upper_above [OF least_s] L La)  wenzelm@14693  288  next  wenzelm@14693  289  assume "z \ A"  wenzelm@14693  290  with L least_s least_a show ?thesis  wenzelm@14693  291  by (rule_tac trans [where y = a]) (auto dest: least_Upper_above)  ballarin@14551  292  qed  ballarin@14551  293  next  wenzelm@14693  294  fix y  ballarin@22063  295  assume y: "y \ Upper L (insert x A)"  wenzelm@14693  296  show "s \ y"  wenzelm@14693  297  proof (rule least_le [OF least_s], rule Upper_memI)  wenzelm@14693  298  fix z  wenzelm@14693  299  assume z: "z \ {a, x}"  wenzelm@14693  300  then show "z \ y"  wenzelm@14693  301  proof  ballarin@22063  302  have y': "y \ Upper L A"  ballarin@22063  303  apply (rule subsetD [where A = "Upper L (insert x A)"])  wenzelm@23463  304  apply (rule Upper_antimono)  wenzelm@23463  305  apply blast  wenzelm@23463  306  apply (rule y)  wenzelm@14693  307  done  wenzelm@14693  308  assume "z = a"  wenzelm@14693  309  with y' least_a show ?thesis by (fast dest: least_le)  wenzelm@14693  310  next  wenzelm@14693  311  assume "z \ {x}"  wenzelm@14693  312  with y L show ?thesis by blast  wenzelm@14693  313  qed  wenzelm@23350  314  qed (rule Upper_closed [THEN subsetD, OF y])  ballarin@14551  315  next  ballarin@22063  316  from L show "insert x A \ carrier L" by simp  ballarin@22063  317  from least_s show "s \ carrier L" by simp  ballarin@14551  318  qed  wenzelm@23350  319  qed (rule least_l)  wenzelm@23350  320  qed (rule P)  ballarin@14551  321 qed  ballarin@14551  322 ballarin@14551  323 lemma (in lattice) finite_sup_least:  ballarin@22063  324  "[| finite A; A \ carrier L; A ~= {} |] ==> least L (\A) (Upper L A)"  berghofe@22265  325 proof (induct set: finite)  wenzelm@14693  326  case empty  wenzelm@14693  327  then show ?case by simp  ballarin@14551  328 next  nipkow@15328  329  case (insert x A)  ballarin@14551  330  show ?case  ballarin@14551  331  proof (cases "A = {}")  ballarin@14551  332  case True  ballarin@14551  333  with insert show ?thesis by (simp add: sup_of_singletonI)  ballarin@14551  334  next  ballarin@14551  335  case False  ballarin@22063  336  with insert have "least L (\A) (Upper L A)" by simp  wenzelm@14693  337  with _ show ?thesis  wenzelm@14693  338  by (rule sup_insertI) (simp_all add: insert [simplified])  ballarin@14551  339  qed  ballarin@14551  340 qed  ballarin@14551  341 ballarin@14551  342 lemma (in lattice) finite_sup_insertI:  ballarin@22063  343  assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l"  ballarin@22063  344  and xA: "finite A" "x \ carrier L" "A \ carrier L"  ballarin@14551  345  shows "P (\ (insert x A))"  ballarin@14551  346 proof (cases "A = {}")  ballarin@14551  347  case True with P and xA show ?thesis  ballarin@14551  348  by (simp add: sup_of_singletonI)  ballarin@14551  349 next  ballarin@14551  350  case False with P and xA show ?thesis  ballarin@14551  351  by (simp add: sup_insertI finite_sup_least)  ballarin@14551  352 qed  ballarin@14551  353 ballarin@14551  354 lemma (in lattice) finite_sup_closed:  ballarin@22063  355  "[| finite A; A \ carrier L; A ~= {} |] ==> \A \ carrier L"  berghofe@22265  356 proof (induct set: finite)  ballarin@14551  357  case empty then show ?case by simp  ballarin@14551  358 next  nipkow@15328  359  case insert then show ?case  wenzelm@14693  360  by - (rule finite_sup_insertI, simp_all)  ballarin@14551  361 qed  ballarin@14551  362 ballarin@14551  363 lemma (in lattice) join_left:  ballarin@22063  364  "[| x \ carrier L; y \ carrier L |] ==> x \ x \ y"  wenzelm@14693  365  by (rule joinI [folded join_def]) (blast dest: least_mem)  ballarin@14551  366 ballarin@14551  367 lemma (in lattice) join_right:  ballarin@22063  368  "[| x \ carrier L; y \ carrier L |] ==> y \ x \ y"  wenzelm@14693  369  by (rule joinI [folded join_def]) (blast dest: least_mem)  ballarin@14551  370 ballarin@14551  371 lemma (in lattice) sup_of_two_least:  ballarin@22063  372  "[| x \ carrier L; y \ carrier L |] ==> least L (\{x, y}) (Upper L {x, y})"  ballarin@14551  373 proof (unfold sup_def)  ballarin@22063  374  assume L: "x \ carrier L" "y \ carrier L"  ballarin@22063  375  with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast  ballarin@22063  376  with L show "least L (THE xa. least L xa (Upper L {x, y})) (Upper L {x, y})"  ballarin@14551  377  by (fast intro: theI2 least_unique) (* blast fails *)  ballarin@14551  378 qed  ballarin@14551  379 ballarin@14551  380 lemma (in lattice) join_le:  wenzelm@14693  381  assumes sub: "x \ z" "y \ z"  wenzelm@23350  382  and x: "x \ carrier L" and y: "y \ carrier L" and z: "z \ carrier L"  ballarin@14551  383  shows "x \ y \ z"  wenzelm@23350  384 proof (rule joinI [OF _ x y])  ballarin@14551  385  fix s  ballarin@22063  386  assume "least L s (Upper L {x, y})"  wenzelm@23350  387  with sub z show "s \ z" by (fast elim: least_le intro: Upper_memI)  ballarin@14551  388 qed  wenzelm@14693  389 ballarin@14551  390 lemma (in lattice) join_assoc_lemma:  ballarin@22063  391  assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L"  wenzelm@14693  392  shows "x \ (y \ z) = \{x, y, z}"  ballarin@14551  393 proof (rule finite_sup_insertI)  wenzelm@14651  394  -- {* The textbook argument in Jacobson I, p 457 *}  ballarin@14551  395  fix s  ballarin@22063  396  assume sup: "least L s (Upper L {x, y, z})"  ballarin@14551  397  show "x \ (y \ z) = s"  ballarin@14551  398  proof (rule anti_sym)  ballarin@14551  399  from sup L show "x \ (y \ z) \ s"  ballarin@14551  400  by (fastsimp intro!: join_le elim: least_Upper_above)  ballarin@14551  401  next  ballarin@14551  402  from sup L show "s \ x \ (y \ z)"  ballarin@14551  403  by (erule_tac least_le)  ballarin@14551  404  (blast intro!: Upper_memI intro: trans join_left join_right join_closed)  ballarin@22063  405  qed (simp_all add: L least_carrier [OF sup])  ballarin@14551  406 qed (simp_all add: L)  ballarin@14551  407 ballarin@22063  408 lemma join_comm:  ballarin@22063  409  fixes L (structure)  ballarin@22063  410  shows "x \ y = y \ x"  ballarin@14551  411  by (unfold join_def) (simp add: insert_commute)  ballarin@14551  412 ballarin@14551  413 lemma (in lattice) join_assoc:  ballarin@22063  414  assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L"  ballarin@14551  415  shows "(x \ y) \ z = x \ (y \ z)"  ballarin@14551  416 proof -  ballarin@14551  417  have "(x \ y) \ z = z \ (x \ y)" by (simp only: join_comm)  wenzelm@14693  418  also from L have "... = \{z, x, y}" by (simp add: join_assoc_lemma)  wenzelm@14693  419  also from L have "... = \{x, y, z}" by (simp add: insert_commute)  ballarin@14551  420  also from L have "... = x \ (y \ z)" by (simp add: join_assoc_lemma)  ballarin@14551  421  finally show ?thesis .  ballarin@14551  422 qed  ballarin@14551  423 wenzelm@14693  424 ballarin@14551  425 subsubsection {* Infimum *}  ballarin@14551  426 ballarin@14551  427 lemma (in lattice) meetI:  ballarin@22063  428  "[| !!i. greatest L i (Lower L {x, y}) ==> P i;  ballarin@22063  429  x \ carrier L; y \ carrier L |]  ballarin@14551  430  ==> P (x \ y)"  ballarin@14551  431 proof (unfold meet_def inf_def)  ballarin@22063  432  assume L: "x \ carrier L" "y \ carrier L"  ballarin@22063  433  and P: "!!g. greatest L g (Lower L {x, y}) ==> P g"  ballarin@22063  434  with inf_of_two_exists obtain i where "greatest L i (Lower L {x, y})" by fast  ballarin@22063  435  with L show "P (THE g. greatest L g (Lower L {x, y}))"  ballarin@14551  436  by (fast intro: theI2 greatest_unique P)  ballarin@14551  437 qed  ballarin@14551  438 ballarin@14551  439 lemma (in lattice) meet_closed [simp]:  ballarin@22063  440  "[| x \ carrier L; y \ carrier L |] ==> x \ y \ carrier L"  ballarin@22063  441  by (rule meetI) (rule greatest_carrier)  ballarin@14551  442 wenzelm@14651  443 lemma (in partial_order) inf_of_singletonI: (* only reflexivity needed ? *)  ballarin@22063  444  "x \ carrier L ==> greatest L x (Lower L {x})"  ballarin@14551  445  by (rule greatest_LowerI) fast+  ballarin@14551  446 ballarin@14551  447 lemma (in partial_order) inf_of_singleton [simp]:  ballarin@22063  448  "x \ carrier L ==> \ {x} = x"  ballarin@14551  449  by (unfold inf_def) (blast intro: greatest_unique greatest_LowerI inf_of_singletonI)  ballarin@14551  450 ballarin@14551  451 text {* Condition on A: infimum exists. *}  ballarin@14551  452 ballarin@14551  453 lemma (in lattice) inf_insertI:  ballarin@22063  454  "[| !!i. greatest L i (Lower L (insert x A)) ==> P i;  ballarin@22063  455  greatest L a (Lower L A); x \ carrier L; A \ carrier L |]  wenzelm@14693  456  ==> P (\(insert x A))"  ballarin@14551  457 proof (unfold inf_def)  ballarin@22063  458  assume L: "x \ carrier L" "A \ carrier L"  ballarin@22063  459  and P: "!!g. greatest L g (Lower L (insert x A)) ==> P g"  ballarin@22063  460  and greatest_a: "greatest L a (Lower L A)"  ballarin@22063  461  from L greatest_a have La: "a \ carrier L" by simp  ballarin@14551  462  from L inf_of_two_exists greatest_a  ballarin@22063  463  obtain i where greatest_i: "greatest L i (Lower L {a, x})" by blast  ballarin@22063  464  show "P (THE g. greatest L g (Lower L (insert x A)))"  wenzelm@14693  465  proof (rule theI2)  ballarin@22063  466  show "greatest L i (Lower L (insert x A))"  ballarin@14551  467  proof (rule greatest_LowerI)  ballarin@14551  468  fix z  wenzelm@14693  469  assume "z \ insert x A"  wenzelm@14693  470  then show "i \ z"  wenzelm@14693  471  proof  wenzelm@14693  472  assume "z = x" then show ?thesis  wenzelm@14693  473  by (simp add: greatest_Lower_above [OF greatest_i] L La)  wenzelm@14693  474  next  wenzelm@14693  475  assume "z \ A"  wenzelm@14693  476  with L greatest_i greatest_a show ?thesis  wenzelm@14693  477  by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_above)  wenzelm@14693  478  qed  wenzelm@14693  479  next  wenzelm@14693  480  fix y  ballarin@22063  481  assume y: "y \ Lower L (insert x A)"  wenzelm@14693  482  show "y \ i"  wenzelm@14693  483  proof (rule greatest_le [OF greatest_i], rule Lower_memI)  wenzelm@14693  484  fix z  wenzelm@14693  485  assume z: "z \ {a, x}"  wenzelm@14693  486  then show "y \ z"  wenzelm@14693  487  proof  ballarin@22063  488  have y': "y \ Lower L A"  ballarin@22063  489  apply (rule subsetD [where A = "Lower L (insert x A)"])  wenzelm@23463  490  apply (rule Lower_antimono)  wenzelm@23463  491  apply blast  wenzelm@23463  492  apply (rule y)  wenzelm@14693  493  done  wenzelm@14693  494  assume "z = a"  wenzelm@14693  495  with y' greatest_a show ?thesis by (fast dest: greatest_le)  wenzelm@14693  496  next  wenzelm@14693  497  assume "z \ {x}"  wenzelm@14693  498  with y L show ?thesis by blast  wenzelm@14693  499  qed  wenzelm@23350  500  qed (rule Lower_closed [THEN subsetD, OF y])  wenzelm@14693  501  next  ballarin@22063  502  from L show "insert x A \ carrier L" by simp  ballarin@22063  503  from greatest_i show "i \ carrier L" by simp  ballarin@14551  504  qed  ballarin@14551  505  next  ballarin@14551  506  fix g  ballarin@22063  507  assume greatest_g: "greatest L g (Lower L (insert x A))"  ballarin@14551  508  show "g = i"  ballarin@14551  509  proof (rule greatest_unique)  ballarin@22063  510  show "greatest L i (Lower L (insert x A))"  ballarin@14551  511  proof (rule greatest_LowerI)  wenzelm@14693  512  fix z  wenzelm@14693  513  assume "z \ insert x A"  wenzelm@14693  514  then show "i \ z"  wenzelm@14693  515  proof  wenzelm@14693  516  assume "z = x" then show ?thesis  wenzelm@14693  517  by (simp add: greatest_Lower_above [OF greatest_i] L La)  wenzelm@14693  518  next  wenzelm@14693  519  assume "z \ A"  wenzelm@14693  520  with L greatest_i greatest_a show ?thesis  wenzelm@14693  521  by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_above)  wenzelm@14693  522  qed  ballarin@14551  523  next  wenzelm@14693  524  fix y  ballarin@22063  525  assume y: "y \ Lower L (insert x A)"  wenzelm@14693  526  show "y \ i"  wenzelm@14693  527  proof (rule greatest_le [OF greatest_i], rule Lower_memI)  wenzelm@14693  528  fix z  wenzelm@14693  529  assume z: "z \ {a, x}"  wenzelm@14693  530  then show "y \ z"  wenzelm@14693  531  proof  ballarin@22063  532  have y': "y \ Lower L A"  ballarin@22063  533  apply (rule subsetD [where A = "Lower L (insert x A)"])  wenzelm@23463  534  apply (rule Lower_antimono)  wenzelm@23463  535  apply blast  wenzelm@23463  536  apply (rule y)  wenzelm@14693  537  done  wenzelm@14693  538  assume "z = a"  wenzelm@14693  539  with y' greatest_a show ?thesis by (fast dest: greatest_le)  wenzelm@14693  540  next  wenzelm@14693  541  assume "z \ {x}"  wenzelm@14693  542  with y L show ?thesis by blast  ballarin@14551  543  qed  wenzelm@23350  544  qed (rule Lower_closed [THEN subsetD, OF y])  ballarin@14551  545  next  ballarin@22063  546  from L show "insert x A \ carrier L" by simp  ballarin@22063  547  from greatest_i show "i \ carrier L" by simp  ballarin@14551  548  qed  wenzelm@23350  549  qed (rule greatest_g)  wenzelm@23350  550  qed (rule P)  ballarin@14551  551 qed  ballarin@14551  552 ballarin@14551  553 lemma (in lattice) finite_inf_greatest:  ballarin@22063  554  "[| finite A; A \ carrier L; A ~= {} |] ==> greatest L (\A) (Lower L A)"  berghofe@22265  555 proof (induct set: finite)  ballarin@14551  556  case empty then show ?case by simp  ballarin@14551  557 next  nipkow@15328  558  case (insert x A)  ballarin@14551  559  show ?case  ballarin@14551  560  proof (cases "A = {}")  ballarin@14551  561  case True  ballarin@14551  562  with insert show ?thesis by (simp add: inf_of_singletonI)  ballarin@14551  563  next  ballarin@14551  564  case False  ballarin@14551  565  from insert show ?thesis  ballarin@14551  566  proof (rule_tac inf_insertI)  ballarin@22063  567  from False insert show "greatest L (\A) (Lower L A)" by simp  ballarin@14551  568  qed simp_all  ballarin@14551  569  qed  ballarin@14551  570 qed  ballarin@14551  571 ballarin@14551  572 lemma (in lattice) finite_inf_insertI:  ballarin@22063  573  assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i"  ballarin@22063  574  and xA: "finite A" "x \ carrier L" "A \ carrier L"  ballarin@14551  575  shows "P (\ (insert x A))"  ballarin@14551  576 proof (cases "A = {}")  ballarin@14551  577  case True with P and xA show ?thesis  ballarin@14551  578  by (simp add: inf_of_singletonI)  ballarin@14551  579 next  ballarin@14551  580  case False with P and xA show ?thesis  ballarin@14551  581  by (simp add: inf_insertI finite_inf_greatest)  ballarin@14551  582 qed  ballarin@14551  583 ballarin@14551  584 lemma (in lattice) finite_inf_closed:  ballarin@22063  585  "[| finite A; A \ carrier L; A ~= {} |] ==> \A \ carrier L"  berghofe@22265  586 proof (induct set: finite)  ballarin@14551  587  case empty then show ?case by simp  ballarin@14551  588 next  nipkow@15328  589  case insert then show ?case  ballarin@14551  590  by (rule_tac finite_inf_insertI) (simp_all)  ballarin@14551  591 qed  ballarin@14551  592 ballarin@14551  593 lemma (in lattice) meet_left:  ballarin@22063  594  "[| x \ carrier L; y \ carrier L |] ==> x \ y \ x"  wenzelm@14693  595  by (rule meetI [folded meet_def]) (blast dest: greatest_mem)  ballarin@14551  596 ballarin@14551  597 lemma (in lattice) meet_right:  ballarin@22063  598  "[| x \ carrier L; y \ carrier L |] ==> x \ y \ y"  wenzelm@14693  599  by (rule meetI [folded meet_def]) (blast dest: greatest_mem)  ballarin@14551  600 ballarin@14551  601 lemma (in lattice) inf_of_two_greatest:  ballarin@22063  602  "[| x \ carrier L; y \ carrier L |] ==>  ballarin@22063  603  greatest L (\ {x, y}) (Lower L {x, y})"  ballarin@14551  604 proof (unfold inf_def)  ballarin@22063  605  assume L: "x \ carrier L" "y \ carrier L"  ballarin@22063  606  with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast  ballarin@14551  607  with L  ballarin@22063  608  show "greatest L (THE xa. greatest L xa (Lower L {x, y})) (Lower L {x, y})"  ballarin@14551  609  by (fast intro: theI2 greatest_unique) (* blast fails *)  ballarin@14551  610 qed  ballarin@14551  611 ballarin@14551  612 lemma (in lattice) meet_le:  wenzelm@14693  613  assumes sub: "z \ x" "z \ y"  wenzelm@23350  614  and x: "x \ carrier L" and y: "y \ carrier L" and z: "z \ carrier L"  ballarin@14551  615  shows "z \ x \ y"  wenzelm@23350  616 proof (rule meetI [OF _ x y])  ballarin@14551  617  fix i  ballarin@22063  618  assume "greatest L i (Lower L {x, y})"  wenzelm@23350  619  with sub z show "z \ i" by (fast elim: greatest_le intro: Lower_memI)  ballarin@14551  620 qed  wenzelm@14693  621 ballarin@14551  622 lemma (in lattice) meet_assoc_lemma:  ballarin@22063  623  assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L"  wenzelm@14693  624  shows "x \ (y \ z) = \{x, y, z}"  ballarin@14551  625 proof (rule finite_inf_insertI)  ballarin@14551  626  txt {* The textbook argument in Jacobson I, p 457 *}  ballarin@14551  627  fix i  ballarin@22063  628  assume inf: "greatest L i (Lower L {x, y, z})"  ballarin@14551  629  show "x \ (y \ z) = i"  ballarin@14551  630  proof (rule anti_sym)  ballarin@14551  631  from inf L show "i \ x \ (y \ z)"  ballarin@14551  632  by (fastsimp intro!: meet_le elim: greatest_Lower_above)  ballarin@14551  633  next  ballarin@14551  634  from inf L show "x \ (y \ z) \ i"  ballarin@14551  635  by (erule_tac greatest_le)  ballarin@14551  636  (blast intro!: Lower_memI intro: trans meet_left meet_right meet_closed)  ballarin@22063  637  qed (simp_all add: L greatest_carrier [OF inf])  ballarin@14551  638 qed (simp_all add: L)  ballarin@14551  639 ballarin@22063  640 lemma meet_comm:  ballarin@22063  641  fixes L (structure)  ballarin@22063  642  shows "x \ y = y \ x"  ballarin@14551  643  by (unfold meet_def) (simp add: insert_commute)  ballarin@14551  644 ballarin@14551  645 lemma (in lattice) meet_assoc:  ballarin@22063  646  assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L"  ballarin@14551  647  shows "(x \ y) \ z = x \ (y \ z)"  ballarin@14551  648 proof -  ballarin@14551  649  have "(x \ y) \ z = z \ (x \ y)" by (simp only: meet_comm)  ballarin@14551  650  also from L have "... = \ {z, x, y}" by (simp add: meet_assoc_lemma)  ballarin@14551  651  also from L have "... = \ {x, y, z}" by (simp add: insert_commute)  ballarin@14551  652  also from L have "... = x \ (y \ z)" by (simp add: meet_assoc_lemma)  ballarin@14551  653  finally show ?thesis .  ballarin@14551  654 qed  ballarin@14551  655 wenzelm@14693  656 ballarin@14551  657 subsection {* Total Orders *}  ballarin@14551  658 ballarin@24087  659 locale total_order = partial_order +  ballarin@22063  660  assumes total: "[| x \ carrier L; y \ carrier L |] ==> x \ y | y \ x"  ballarin@14551  661 ballarin@14551  662 text {* Introduction rule: the usual definition of total order *}  ballarin@14551  663 ballarin@14551  664 lemma (in partial_order) total_orderI:  ballarin@22063  665  assumes total: "!!x y. [| x \ carrier L; y \ carrier L |] ==> x \ y | y \ x"  ballarin@22063  666  shows "total_order L"  ballarin@24087  667  by unfold_locales (rule total)  ballarin@24087  668 ballarin@24087  669 text {* Total orders are lattices. *}  ballarin@24087  670 ballarin@24087  671 interpretation total_order < lattice  ballarin@24087  672 proof unfold_locales  ballarin@24087  673  fix x y  ballarin@24087  674  assume L: "x \ carrier L" "y \ carrier L"  ballarin@24087  675  show "EX s. least L s (Upper L {x, y})"  ballarin@24087  676  proof -  ballarin@24087  677  note total L  ballarin@24087  678  moreover  ballarin@24087  679  {  ballarin@24087  680  assume "x \ y"  ballarin@24087  681  with L have "least L y (Upper L {x, y})"  ballarin@24087  682  by (rule_tac least_UpperI) auto  ballarin@24087  683  }  ballarin@24087  684  moreover  ballarin@24087  685  {  ballarin@24087  686  assume "y \ x"  ballarin@24087  687  with L have "least L x (Upper L {x, y})"  ballarin@24087  688  by (rule_tac least_UpperI) auto  ballarin@24087  689  }  ballarin@24087  690  ultimately show ?thesis by blast  ballarin@14551  691  qed  ballarin@24087  692 next  ballarin@24087  693  fix x y  ballarin@24087  694  assume L: "x \ carrier L" "y \ carrier L"  ballarin@24087  695  show "EX i. greatest L i (Lower L {x, y})"  ballarin@24087  696  proof -  ballarin@24087  697  note total L  ballarin@24087  698  moreover  ballarin@24087  699  {  ballarin@24087  700  assume "y \ x"  ballarin@24087  701  with L have "greatest L y (Lower L {x, y})"  ballarin@24087  702  by (rule_tac greatest_LowerI) auto  ballarin@24087  703  }  ballarin@24087  704  moreover  ballarin@24087  705  {  ballarin@24087  706  assume "x \ y"  ballarin@24087  707  with L have "greatest L x (Lower L {x, y})"  ballarin@24087  708  by (rule_tac greatest_LowerI) auto  ballarin@24087  709  }  ballarin@24087  710  ultimately show ?thesis by blast  ballarin@24087  711  qed  ballarin@24087  712 qed  ballarin@14551  713 wenzelm@14693  714 ballarin@14551  715 subsection {* Complete lattices *}  ballarin@14551  716 ballarin@14551  717 locale complete_lattice = lattice +  ballarin@14551  718  assumes sup_exists:  ballarin@22063  719  "[| A \ carrier L |] ==> EX s. least L s (Upper L A)"  ballarin@14551  720  and inf_exists:  ballarin@22063  721  "[| A \ carrier L |] ==> EX i. greatest L i (Lower L A)"  ballarin@21041  722 ballarin@14551  723 text {* Introduction rule: the usual definition of complete lattice *}  ballarin@14551  724 ballarin@14551  725 lemma (in partial_order) complete_latticeI:  ballarin@14551  726  assumes sup_exists:  ballarin@22063  727  "!!A. [| A \ carrier L |] ==> EX s. least L s (Upper L A)"  ballarin@14551  728  and inf_exists:  ballarin@22063  729  "!!A. [| A \ carrier L |] ==> EX i. greatest L i (Lower L A)"  ballarin@22063  730  shows "complete_lattice L"  ballarin@19984  731 proof intro_locales  ballarin@22063  732  show "lattice_axioms L"  wenzelm@14693  733  by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+  wenzelm@23463  734 qed (rule complete_lattice_axioms.intro sup_exists inf_exists | assumption)+  ballarin@14551  735 ballarin@22063  736 constdefs (structure L)  ballarin@22063  737  top :: "_ => 'a" ("\\")  ballarin@22063  738  "\ == sup L (carrier L)"  ballarin@21041  739 ballarin@22063  740  bottom :: "_ => 'a" ("\\")  ballarin@22063  741  "\ == inf L (carrier L)"  ballarin@14551  742 ballarin@14551  743 ballarin@14551  744 lemma (in complete_lattice) supI:  ballarin@22063  745  "[| !!l. least L l (Upper L A) ==> P l; A \ carrier L |]  wenzelm@14651  746  ==> P (\A)"  ballarin@14551  747 proof (unfold sup_def)  ballarin@22063  748  assume L: "A \ carrier L"  ballarin@22063  749  and P: "!!l. least L l (Upper L A) ==> P l"  ballarin@22063  750  with sup_exists obtain s where "least L s (Upper L A)" by blast  ballarin@22063  751  with L show "P (THE l. least L l (Upper L A))"  ballarin@14551  752  by (fast intro: theI2 least_unique P)  ballarin@14551  753 qed  ballarin@14551  754 ballarin@14551  755 lemma (in complete_lattice) sup_closed [simp]:  ballarin@22063  756  "A \ carrier L ==> \A \ carrier L"  ballarin@14551  757  by (rule supI) simp_all  ballarin@14551  758 ballarin@14551  759 lemma (in complete_lattice) top_closed [simp, intro]:  ballarin@22063  760  "\ \ carrier L"  ballarin@14551  761  by (unfold top_def) simp  ballarin@14551  762 ballarin@14551  763 lemma (in complete_lattice) infI:  ballarin@22063  764  "[| !!i. greatest L i (Lower L A) ==> P i; A \ carrier L |]  wenzelm@14693  765  ==> P (\A)"  ballarin@14551  766 proof (unfold inf_def)  ballarin@22063  767  assume L: "A \ carrier L"  ballarin@22063  768  and P: "!!l. greatest L l (Lower L A) ==> P l"  ballarin@22063  769  with inf_exists obtain s where "greatest L s (Lower L A)" by blast  ballarin@22063  770  with L show "P (THE l. greatest L l (Lower L A))"  ballarin@14551  771  by (fast intro: theI2 greatest_unique P)  ballarin@14551  772 qed  ballarin@14551  773 ballarin@14551  774 lemma (in complete_lattice) inf_closed [simp]:  ballarin@22063  775  "A \ carrier L ==> \A \ carrier L"  ballarin@14551  776  by (rule infI) simp_all  ballarin@14551  777 ballarin@14551  778 lemma (in complete_lattice) bottom_closed [simp, intro]:  ballarin@22063  779  "\ \ carrier L"  ballarin@14551  780  by (unfold bottom_def) simp  ballarin@14551  781 ballarin@14551  782 text {* Jacobson: Theorem 8.1 *}  ballarin@14551  783 ballarin@22063  784 lemma Lower_empty [simp]:  ballarin@22063  785  "Lower L {} = carrier L"  ballarin@14551  786  by (unfold Lower_def) simp  ballarin@14551  787 ballarin@22063  788 lemma Upper_empty [simp]:  ballarin@22063  789  "Upper L {} = carrier L"  ballarin@14551  790  by (unfold Upper_def) simp  ballarin@14551  791 ballarin@14551  792 theorem (in partial_order) complete_lattice_criterion1:  ballarin@22063  793  assumes top_exists: "EX g. greatest L g (carrier L)"  ballarin@14551  794  and inf_exists:  ballarin@22063  795  "!!A. [| A \ carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)"  ballarin@22063  796  shows "complete_lattice L"  ballarin@14551  797 proof (rule complete_latticeI)  ballarin@22063  798  from top_exists obtain top where top: "greatest L top (carrier L)" ..  ballarin@14551  799  fix A  ballarin@22063  800  assume L: "A \ carrier L"  ballarin@22063  801  let ?B = "Upper L A"  ballarin@14551  802  from L top have "top \ ?B" by (fast intro!: Upper_memI intro: greatest_le)  ballarin@14551  803  then have B_non_empty: "?B ~= {}" by fast  ballarin@22063  804  have B_L: "?B \ carrier L" by simp  ballarin@14551  805  from inf_exists [OF B_L B_non_empty]  ballarin@22063  806  obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..  ballarin@22063  807  have "least L b (Upper L A)"  ballarin@14551  808 apply (rule least_UpperI)  ballarin@22063  809  apply (rule greatest_le [where A = "Lower L ?B"])  ballarin@14551  810  apply (rule b_inf_B)  ballarin@14551  811  apply (rule Lower_memI)  ballarin@14551  812  apply (erule UpperD)  ballarin@14551  813  apply assumption  ballarin@14551  814  apply (rule L)  ballarin@14551  815  apply (fast intro: L [THEN subsetD])  ballarin@14551  816  apply (erule greatest_Lower_above [OF b_inf_B])  ballarin@14551  817  apply simp  ballarin@14551  818  apply (rule L)  ballarin@22063  819 apply (rule greatest_carrier [OF b_inf_B]) (* rename rule: _closed *)  ballarin@14551  820 done  ballarin@22063  821  then show "EX s. least L s (Upper L A)" ..  ballarin@14551  822 next  ballarin@14551  823  fix A  ballarin@22063  824  assume L: "A \ carrier L"  ballarin@22063  825  show "EX i. greatest L i (Lower L A)"  ballarin@14551  826  proof (cases "A = {}")  ballarin@14551  827  case True then show ?thesis  ballarin@14551  828  by (simp add: top_exists)  ballarin@14551  829  next  ballarin@14551  830  case False with L show ?thesis  ballarin@14551  831  by (rule inf_exists)  ballarin@14551  832  qed  ballarin@14551  833 qed  ballarin@14551  834 ballarin@14551  835 (* TODO: prove dual version *)  ballarin@14551  836 ballarin@20318  837 ballarin@14551  838 subsection {* Examples *}  ballarin@14551  839 ballarin@20318  840 subsubsection {* Powerset of a Set is a Complete Lattice *}  ballarin@14551  841 ballarin@14551  842 theorem powerset_is_complete_lattice:  ballarin@22063  843  "complete_lattice (| carrier = Pow A, le = op \ |)"  ballarin@22063  844  (is "complete_lattice ?L")  ballarin@14551  845 proof (rule partial_order.complete_latticeI)  ballarin@22063  846  show "partial_order ?L"  ballarin@14551  847  by (rule partial_order.intro) auto  ballarin@14551  848 next  ballarin@14551  849  fix B  ballarin@22063  850  assume "B \ carrier ?L"  ballarin@22063  851  then have "least ?L (\ B) (Upper ?L B)"  ballarin@22063  852  by (fastsimp intro!: least_UpperI simp: Upper_def)  ballarin@22063  853  then show "EX s. least ?L s (Upper ?L B)" ..  ballarin@14551  854 next  ballarin@14551  855  fix B  ballarin@22063  856  assume "B \ carrier ?L"  ballarin@22063  857  then have "greatest ?L (\ B \ A) (Lower ?L B)"  ballarin@14551  858  txt {* @{term "\ B"} is not the infimum of @{term B}:  ballarin@14551  859  @{term "\ {} = UNIV"} which is in general bigger than @{term "A"}! *}  ballarin@22063  860  by (fastsimp intro!: greatest_LowerI simp: Lower_def)  ballarin@22063  861  then show "EX i. greatest ?L i (Lower ?L B)" ..  ballarin@14551  862 qed  ballarin@14551  863 ballarin@14751  864 text {* An other example, that of the lattice of subgroups of a group,  ballarin@14751  865  can be found in Group theory (Section~\ref{sec:subgroup-lattice}). *}  ballarin@14551  866 wenzelm@14693  867 end