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