src/HOL/Algebra/Lattice.thy
 author haftmann Sat Mar 18 09:58:49 2006 +0100 (2006-03-18) changeset 19286 83404ccd270a parent 16417 9bc16273c2d4 child 19783 82f365a14960 permissions -rw-r--r--
renamed constant less in lattice
 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 wenzelm@14693  22 locale partial_order = struct L +  ballarin@14551  23  assumes refl [intro, simp]:  ballarin@14551  24  "x \ carrier L ==> x \ x"  ballarin@14551  25  and anti_sym [intro]:  ballarin@14551  26  "[| x \ y; y \ x; x \ carrier L; y \ carrier L |] ==> x = y"  ballarin@14551  27  and trans [trans]:  ballarin@14551  28  "[| x \ y; y \ z;  ballarin@14551  29  x \ carrier L; y \ carrier L; z \ carrier L |] ==> x \ z"  ballarin@14551  30 wenzelm@14651  31 constdefs (structure L)  haftmann@19286  32  lless :: "[_, 'a, 'a] => bool" (infixl "\\" 50)  wenzelm@14651  33  "x \ y == x \ y & x ~= y"  ballarin@14551  34 wenzelm@14651  35  -- {* Upper and lower bounds of a set. *}  wenzelm@14651  36  Upper :: "[_, 'a set] => 'a set"  wenzelm@14693  37  "Upper L A == {u. (ALL x. x \ A \ carrier L --> x \ u)} \  ballarin@14551  38  carrier L"  ballarin@14551  39 wenzelm@14651  40  Lower :: "[_, 'a set] => 'a set"  wenzelm@14693  41  "Lower L A == {l. (ALL x. x \ A \ carrier L --> l \ x)} \  ballarin@14551  42  carrier L"  ballarin@14551  43 wenzelm@14651  44  -- {* Least and greatest, as predicate. *}  wenzelm@14651  45  least :: "[_, 'a, 'a set] => bool"  wenzelm@14693  46  "least L l A == A \ carrier L & l \ A & (ALL x : A. l \ x)"  ballarin@14551  47 wenzelm@14651  48  greatest :: "[_, 'a, 'a set] => bool"  wenzelm@14693  49  "greatest L g A == A \ carrier L & g \ A & (ALL x : A. x \ g)"  ballarin@14551  50 wenzelm@14651  51  -- {* Supremum and infimum *}  wenzelm@14651  52  sup :: "[_, 'a set] => 'a" ("\\_" [90] 90)  wenzelm@14651  53  "\A == THE x. least L x (Upper L A)"  ballarin@14551  54 wenzelm@14651  55  inf :: "[_, 'a set] => 'a" ("\\_" [90] 90)  wenzelm@14651  56  "\A == THE x. greatest L x (Lower L A)"  ballarin@14551  57 wenzelm@14651  58  join :: "[_, 'a, 'a] => 'a" (infixl "\\" 65)  wenzelm@14651  59  "x \ y == sup L {x, y}"  ballarin@14551  60 ballarin@16325  61  meet :: "[_, 'a, 'a] => 'a" (infixl "\\" 70)  wenzelm@14651  62  "x \ y == inf L {x, y}"  ballarin@14551  63 wenzelm@14651  64 wenzelm@14651  65 subsubsection {* Upper *}  ballarin@14551  66 ballarin@14551  67 lemma Upper_closed [intro, simp]:  ballarin@14551  68  "Upper L A \ carrier L"  ballarin@14551  69  by (unfold Upper_def) clarify  ballarin@14551  70 ballarin@14551  71 lemma UpperD [dest]:  wenzelm@14693  72  includes struct L  ballarin@14551  73  shows "[| u \ Upper L A; x \ A; A \ carrier L |] ==> x \ u"  wenzelm@14693  74  by (unfold Upper_def) blast  ballarin@14551  75 ballarin@14551  76 lemma Upper_memI:  wenzelm@14693  77  includes struct L  ballarin@14551  78  shows "[| !! y. y \ A ==> y \ x; x \ carrier L |] ==> x \ Upper L A"  wenzelm@14693  79  by (unfold Upper_def) blast  ballarin@14551  80 ballarin@14551  81 lemma Upper_antimono:  ballarin@14551  82  "A \ B ==> Upper L B \ Upper L A"  ballarin@14551  83  by (unfold Upper_def) blast  ballarin@14551  84 wenzelm@14651  85 wenzelm@14651  86 subsubsection {* Lower *}  ballarin@14551  87 ballarin@14551  88 lemma Lower_closed [intro, simp]:  ballarin@14551  89  "Lower L A \ carrier L"  ballarin@14551  90  by (unfold Lower_def) clarify  ballarin@14551  91 ballarin@14551  92 lemma LowerD [dest]:  wenzelm@14693  93  includes struct L  ballarin@14551  94  shows "[| l \ Lower L A; x \ A; A \ carrier L |] ==> l \ x"  wenzelm@14693  95  by (unfold Lower_def) blast  ballarin@14551  96 ballarin@14551  97 lemma Lower_memI:  wenzelm@14693  98  includes struct L  ballarin@14551  99  shows "[| !! y. y \ A ==> x \ y; x \ carrier L |] ==> x \ Lower L A"  wenzelm@14693  100  by (unfold Lower_def) blast  ballarin@14551  101 ballarin@14551  102 lemma Lower_antimono:  ballarin@14551  103  "A \ B ==> Lower L B \ Lower L A"  ballarin@14551  104  by (unfold Lower_def) blast  ballarin@14551  105 wenzelm@14651  106 wenzelm@14651  107 subsubsection {* least *}  ballarin@14551  108 ballarin@14551  109 lemma least_carrier [intro, simp]:  ballarin@14551  110  shows "least L l A ==> l \ carrier L"  ballarin@14551  111  by (unfold least_def) fast  ballarin@14551  112 ballarin@14551  113 lemma least_mem:  ballarin@14551  114  "least L l A ==> l \ A"  ballarin@14551  115  by (unfold least_def) fast  ballarin@14551  116 ballarin@14551  117 lemma (in partial_order) least_unique:  ballarin@14551  118  "[| least L x A; least L y A |] ==> x = y"  ballarin@14551  119  by (unfold least_def) blast  ballarin@14551  120 ballarin@14551  121 lemma least_le:  wenzelm@14693  122  includes struct L  ballarin@14551  123  shows "[| least L x A; a \ A |] ==> x \ a"  ballarin@14551  124  by (unfold least_def) fast  ballarin@14551  125 ballarin@14551  126 lemma least_UpperI:  wenzelm@14693  127  includes struct L  ballarin@14551  128  assumes above: "!! x. x \ A ==> x \ s"  ballarin@14551  129  and below: "!! y. y \ Upper L A ==> s \ y"  wenzelm@14693  130  and L: "A \ carrier L" "s \ carrier L"  ballarin@14551  131  shows "least L s (Upper L A)"  wenzelm@14693  132 proof -  wenzelm@14693  133  have "Upper L A \ carrier L" by simp  wenzelm@14693  134  moreover from above L have "s \ Upper L A" by (simp add: Upper_def)  wenzelm@14693  135  moreover from below have "ALL x : Upper L A. s \ x" by fast  wenzelm@14693  136  ultimately show ?thesis by (simp add: least_def)  ballarin@14551  137 qed  ballarin@14551  138 wenzelm@14651  139 wenzelm@14651  140 subsubsection {* greatest *}  ballarin@14551  141 ballarin@14551  142 lemma greatest_carrier [intro, simp]:  ballarin@14551  143  shows "greatest L l A ==> l \ carrier L"  ballarin@14551  144  by (unfold greatest_def) fast  ballarin@14551  145 ballarin@14551  146 lemma greatest_mem:  ballarin@14551  147  "greatest L l A ==> l \ A"  ballarin@14551  148  by (unfold greatest_def) fast  ballarin@14551  149 ballarin@14551  150 lemma (in partial_order) greatest_unique:  ballarin@14551  151  "[| greatest L x A; greatest L y A |] ==> x = y"  ballarin@14551  152  by (unfold greatest_def) blast  ballarin@14551  153 ballarin@14551  154 lemma greatest_le:  wenzelm@14693  155  includes struct L  ballarin@14551  156  shows "[| greatest L x A; a \ A |] ==> a \ x"  ballarin@14551  157  by (unfold greatest_def) fast  ballarin@14551  158 ballarin@14551  159 lemma greatest_LowerI:  wenzelm@14693  160  includes struct L  ballarin@14551  161  assumes below: "!! x. x \ A ==> i \ x"  ballarin@14551  162  and above: "!! y. y \ Lower L A ==> y \ i"  wenzelm@14693  163  and L: "A \ carrier L" "i \ carrier L"  ballarin@14551  164  shows "greatest L i (Lower L A)"  wenzelm@14693  165 proof -  wenzelm@14693  166  have "Lower L A \ carrier L" by simp  wenzelm@14693  167  moreover from below L have "i \ Lower L A" by (simp add: Lower_def)  wenzelm@14693  168  moreover from above have "ALL x : Lower L A. x \ i" by fast  wenzelm@14693  169  ultimately show ?thesis by (simp add: greatest_def)  ballarin@14551  170 qed  ballarin@14551  171 wenzelm@14693  172 ballarin@14551  173 subsection {* Lattices *}  ballarin@14551  174 ballarin@14551  175 locale lattice = partial_order +  ballarin@14551  176  assumes sup_of_two_exists:  ballarin@14551  177  "[| x \ carrier L; y \ carrier L |] ==> EX s. least L s (Upper L {x, y})"  ballarin@14551  178  and inf_of_two_exists:  ballarin@14551  179  "[| x \ carrier L; y \ carrier L |] ==> EX s. greatest L s (Lower L {x, y})"  ballarin@14551  180 ballarin@14551  181 lemma least_Upper_above:  wenzelm@14693  182  includes struct L  ballarin@14551  183  shows "[| least L s (Upper L A); x \ A; A \ carrier L |] ==> x \ s"  ballarin@14551  184  by (unfold least_def) blast  ballarin@14551  185 ballarin@14551  186 lemma greatest_Lower_above:  wenzelm@14693  187  includes struct L  ballarin@14551  188  shows "[| greatest L i (Lower L A); x \ A; A \ carrier L |] ==> i \ x"  ballarin@14551  189  by (unfold greatest_def) blast  ballarin@14551  190 wenzelm@14666  191 ballarin@14551  192 subsubsection {* Supremum *}  ballarin@14551  193 ballarin@14551  194 lemma (in lattice) joinI:  ballarin@14551  195  "[| !!l. least L l (Upper L {x, y}) ==> P l; x \ carrier L; y \ carrier L |]  ballarin@14551  196  ==> P (x \ y)"  ballarin@14551  197 proof (unfold join_def sup_def)  wenzelm@14693  198  assume L: "x \ carrier L" "y \ carrier L"  ballarin@14551  199  and P: "!!l. least L l (Upper L {x, y}) ==> P l"  ballarin@14551  200  with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast  ballarin@14551  201  with L show "P (THE l. least L l (Upper L {x, y}))"  wenzelm@14693  202  by (fast intro: theI2 least_unique P)  ballarin@14551  203 qed  ballarin@14551  204 ballarin@14551  205 lemma (in lattice) join_closed [simp]:  ballarin@14551  206  "[| x \ carrier L; y \ carrier L |] ==> x \ y \ carrier L"  ballarin@14551  207  by (rule joinI) (rule least_carrier)  ballarin@14551  208 wenzelm@14651  209 lemma (in partial_order) sup_of_singletonI: (* only reflexivity needed ? *)  ballarin@14551  210  "x \ carrier L ==> least L x (Upper L {x})"  ballarin@14551  211  by (rule least_UpperI) fast+  ballarin@14551  212 ballarin@14551  213 lemma (in partial_order) sup_of_singleton [simp]:  wenzelm@14693  214  includes struct L  wenzelm@14693  215  shows "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:  wenzelm@14693  403  includes struct L  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]:  wenzelm@14693  442  includes struct L  ballarin@14551  443  shows "x \ carrier L ==> \ {x} = x"  ballarin@14551  444  by (unfold inf_def) (blast intro: greatest_unique greatest_LowerI inf_of_singletonI)  ballarin@14551  445 ballarin@14551  446 text {* Condition on A: infimum exists. *}  ballarin@14551  447 ballarin@14551  448 lemma (in lattice) inf_insertI:  ballarin@14551  449  "[| !!i. greatest L i (Lower L (insert x A)) ==> P i;  ballarin@14551  450  greatest L a (Lower L A); x \ carrier L; A \ carrier L |]  wenzelm@14693  451  ==> P (\(insert x A))"  ballarin@14551  452 proof (unfold inf_def)  wenzelm@14693  453  assume L: "x \ carrier L" "A \ carrier L"  ballarin@14551  454  and P: "!!g. greatest L g (Lower L (insert x A)) ==> P g"  ballarin@14551  455  and greatest_a: "greatest L a (Lower L A)"  ballarin@14551  456  from L greatest_a have La: "a \ carrier L" by simp  ballarin@14551  457  from L inf_of_two_exists greatest_a  ballarin@14551  458  obtain i where greatest_i: "greatest L i (Lower L {a, x})" by blast  ballarin@14551  459  show "P (THE g. greatest L g (Lower L (insert x A)))"  wenzelm@14693  460  proof (rule theI2)  ballarin@14551  461  show "greatest L i (Lower L (insert x A))"  ballarin@14551  462  proof (rule greatest_LowerI)  ballarin@14551  463  fix z  wenzelm@14693  464  assume "z \ insert x A"  wenzelm@14693  465  then show "i \ z"  wenzelm@14693  466  proof  wenzelm@14693  467  assume "z = x" then show ?thesis  wenzelm@14693  468  by (simp add: greatest_Lower_above [OF greatest_i] L La)  wenzelm@14693  469  next  wenzelm@14693  470  assume "z \ A"  wenzelm@14693  471  with L greatest_i greatest_a show ?thesis  wenzelm@14693  472  by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_above)  wenzelm@14693  473  qed  wenzelm@14693  474  next  wenzelm@14693  475  fix y  wenzelm@14693  476  assume y: "y \ Lower L (insert x A)"  wenzelm@14693  477  show "y \ i"  wenzelm@14693  478  proof (rule greatest_le [OF greatest_i], rule Lower_memI)  wenzelm@14693  479  fix z  wenzelm@14693  480  assume z: "z \ {a, x}"  wenzelm@14693  481  then show "y \ z"  wenzelm@14693  482  proof  wenzelm@14693  483  have y': "y \ Lower L A"  wenzelm@14693  484  apply (rule subsetD [where A = "Lower L (insert x A)"])  wenzelm@14693  485  apply (rule Lower_antimono) apply clarify apply assumption  wenzelm@14693  486  done  wenzelm@14693  487  assume "z = a"  wenzelm@14693  488  with y' greatest_a show ?thesis by (fast dest: greatest_le)  wenzelm@14693  489  next  wenzelm@14693  490  assume "z \ {x}"  wenzelm@14693  491  with y L show ?thesis by blast  wenzelm@14693  492  qed  wenzelm@14693  493  qed (rule Lower_closed [THEN subsetD])  wenzelm@14693  494  next  wenzelm@14693  495  from L show "insert x A \ carrier L" by simp  wenzelm@14693  496  from greatest_i show "i \ carrier L" by simp  ballarin@14551  497  qed  ballarin@14551  498  next  ballarin@14551  499  fix g  ballarin@14551  500  assume greatest_g: "greatest L g (Lower L (insert x A))"  ballarin@14551  501  show "g = i"  ballarin@14551  502  proof (rule greatest_unique)  ballarin@14551  503  show "greatest L i (Lower L (insert x A))"  ballarin@14551  504  proof (rule greatest_LowerI)  wenzelm@14693  505  fix z  wenzelm@14693  506  assume "z \ insert x A"  wenzelm@14693  507  then show "i \ z"  wenzelm@14693  508  proof  wenzelm@14693  509  assume "z = x" then show ?thesis  wenzelm@14693  510  by (simp add: greatest_Lower_above [OF greatest_i] L La)  wenzelm@14693  511  next  wenzelm@14693  512  assume "z \ A"  wenzelm@14693  513  with L greatest_i greatest_a show ?thesis  wenzelm@14693  514  by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_above)  wenzelm@14693  515  qed  ballarin@14551  516  next  wenzelm@14693  517  fix y  wenzelm@14693  518  assume y: "y \ Lower L (insert x A)"  wenzelm@14693  519  show "y \ i"  wenzelm@14693  520  proof (rule greatest_le [OF greatest_i], rule Lower_memI)  wenzelm@14693  521  fix z  wenzelm@14693  522  assume z: "z \ {a, x}"  wenzelm@14693  523  then show "y \ z"  wenzelm@14693  524  proof  wenzelm@14693  525  have y': "y \ Lower L A"  wenzelm@14693  526  apply (rule subsetD [where A = "Lower L (insert x A)"])  wenzelm@14693  527  apply (rule Lower_antimono) apply clarify apply assumption  wenzelm@14693  528  done  wenzelm@14693  529  assume "z = a"  wenzelm@14693  530  with y' greatest_a show ?thesis by (fast dest: greatest_le)  wenzelm@14693  531  next  wenzelm@14693  532  assume "z \ {x}"  wenzelm@14693  533  with y L show ?thesis by blast  ballarin@14551  534  qed  wenzelm@14693  535  qed (rule Lower_closed [THEN subsetD])  ballarin@14551  536  next  wenzelm@14693  537  from L show "insert x A \ carrier L" by simp  wenzelm@14693  538  from greatest_i show "i \ carrier L" by simp  ballarin@14551  539  qed  ballarin@14551  540  qed  ballarin@14551  541  qed  ballarin@14551  542 qed  ballarin@14551  543 ballarin@14551  544 lemma (in lattice) finite_inf_greatest:  wenzelm@14693  545  "[| finite A; A \ carrier L; A ~= {} |] ==> greatest L (\A) (Lower L A)"  ballarin@14551  546 proof (induct set: Finites)  ballarin@14551  547  case empty then show ?case by simp  ballarin@14551  548 next  nipkow@15328  549  case (insert x A)  ballarin@14551  550  show ?case  ballarin@14551  551  proof (cases "A = {}")  ballarin@14551  552  case True  ballarin@14551  553  with insert show ?thesis by (simp add: inf_of_singletonI)  ballarin@14551  554  next  ballarin@14551  555  case False  ballarin@14551  556  from insert show ?thesis  ballarin@14551  557  proof (rule_tac inf_insertI)  wenzelm@14693  558  from False insert show "greatest L (\A) (Lower L A)" by simp  ballarin@14551  559  qed simp_all  ballarin@14551  560  qed  ballarin@14551  561 qed  ballarin@14551  562 ballarin@14551  563 lemma (in lattice) finite_inf_insertI:  ballarin@14551  564  assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i"  wenzelm@14693  565  and xA: "finite A" "x \ carrier L" "A \ carrier L"  ballarin@14551  566  shows "P (\ (insert x A))"  ballarin@14551  567 proof (cases "A = {}")  ballarin@14551  568  case True with P and xA show ?thesis  ballarin@14551  569  by (simp add: inf_of_singletonI)  ballarin@14551  570 next  ballarin@14551  571  case False with P and xA show ?thesis  ballarin@14551  572  by (simp add: inf_insertI finite_inf_greatest)  ballarin@14551  573 qed  ballarin@14551  574 ballarin@14551  575 lemma (in lattice) finite_inf_closed:  wenzelm@14693  576  "[| finite A; A \ carrier L; A ~= {} |] ==> \A \ carrier L"  ballarin@14551  577 proof (induct set: Finites)  ballarin@14551  578  case empty then show ?case by simp  ballarin@14551  579 next  nipkow@15328  580  case insert then show ?case  ballarin@14551  581  by (rule_tac finite_inf_insertI) (simp_all)  ballarin@14551  582 qed  ballarin@14551  583 ballarin@14551  584 lemma (in lattice) meet_left:  ballarin@14551  585  "[| x \ carrier L; y \ carrier L |] ==> x \ y \ x"  wenzelm@14693  586  by (rule meetI [folded meet_def]) (blast dest: greatest_mem)  ballarin@14551  587 ballarin@14551  588 lemma (in lattice) meet_right:  ballarin@14551  589  "[| x \ carrier L; y \ carrier L |] ==> x \ y \ y"  wenzelm@14693  590  by (rule meetI [folded meet_def]) (blast dest: greatest_mem)  ballarin@14551  591 ballarin@14551  592 lemma (in lattice) inf_of_two_greatest:  ballarin@14551  593  "[| x \ carrier L; y \ carrier L |] ==>  ballarin@14551  594  greatest L (\ {x, y}) (Lower L {x, y})"  ballarin@14551  595 proof (unfold inf_def)  wenzelm@14693  596  assume L: "x \ carrier L" "y \ carrier L"  ballarin@14551  597  with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast  ballarin@14551  598  with L  ballarin@14551  599  show "greatest L (THE xa. greatest L xa (Lower L {x, y})) (Lower L {x, y})"  ballarin@14551  600  by (fast intro: theI2 greatest_unique) (* blast fails *)  ballarin@14551  601 qed  ballarin@14551  602 ballarin@14551  603 lemma (in lattice) meet_le:  wenzelm@14693  604  assumes sub: "z \ x" "z \ y"  wenzelm@14693  605  and L: "x \ carrier L" "y \ carrier L" "z \ carrier L"  ballarin@14551  606  shows "z \ x \ y"  ballarin@14551  607 proof (rule meetI)  ballarin@14551  608  fix i  ballarin@14551  609  assume "greatest L i (Lower L {x, y})"  ballarin@14551  610  with sub L show "z \ i" by (fast elim: greatest_le intro: Lower_memI)  ballarin@14551  611 qed  wenzelm@14693  612 ballarin@14551  613 lemma (in lattice) meet_assoc_lemma:  wenzelm@14693  614  assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L"  wenzelm@14693  615  shows "x \ (y \ z) = \{x, y, z}"  ballarin@14551  616 proof (rule finite_inf_insertI)  ballarin@14551  617  txt {* The textbook argument in Jacobson I, p 457 *}  ballarin@14551  618  fix i  ballarin@14551  619  assume inf: "greatest L i (Lower L {x, y, z})"  ballarin@14551  620  show "x \ (y \ z) = i"  ballarin@14551  621  proof (rule anti_sym)  ballarin@14551  622  from inf L show "i \ x \ (y \ z)"  ballarin@14551  623  by (fastsimp intro!: meet_le elim: greatest_Lower_above)  ballarin@14551  624  next  ballarin@14551  625  from inf L show "x \ (y \ z) \ i"  ballarin@14551  626  by (erule_tac greatest_le)  ballarin@14551  627  (blast intro!: Lower_memI intro: trans meet_left meet_right meet_closed)  ballarin@14551  628  qed (simp_all add: L greatest_carrier [OF inf])  ballarin@14551  629 qed (simp_all add: L)  ballarin@14551  630 ballarin@14551  631 lemma meet_comm:  wenzelm@14693  632  includes struct L  ballarin@14551  633  shows "x \ y = y \ x"  ballarin@14551  634  by (unfold meet_def) (simp add: insert_commute)  ballarin@14551  635 ballarin@14551  636 lemma (in lattice) meet_assoc:  wenzelm@14693  637  assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L"  ballarin@14551  638  shows "(x \ y) \ z = x \ (y \ z)"  ballarin@14551  639 proof -  ballarin@14551  640  have "(x \ y) \ z = z \ (x \ y)" by (simp only: meet_comm)  ballarin@14551  641  also from L have "... = \ {z, x, y}" by (simp add: meet_assoc_lemma)  ballarin@14551  642  also from L have "... = \ {x, y, z}" by (simp add: insert_commute)  ballarin@14551  643  also from L have "... = x \ (y \ z)" by (simp add: meet_assoc_lemma)  ballarin@14551  644  finally show ?thesis .  ballarin@14551  645 qed  ballarin@14551  646 wenzelm@14693  647 ballarin@14551  648 subsection {* Total Orders *}  ballarin@14551  649 ballarin@14551  650 locale total_order = lattice +  ballarin@14551  651  assumes total: "[| x \ carrier L; y \ carrier L |] ==> x \ y | y \ x"  ballarin@14551  652 ballarin@14551  653 text {* Introduction rule: the usual definition of total order *}  ballarin@14551  654 ballarin@14551  655 lemma (in partial_order) total_orderI:  ballarin@14551  656  assumes total: "!!x y. [| x \ carrier L; y \ carrier L |] ==> x \ y | y \ x"  ballarin@14551  657  shows "total_order L"  ballarin@14551  658 proof (rule total_order.intro)  ballarin@14551  659  show "lattice_axioms L"  ballarin@14551  660  proof (rule lattice_axioms.intro)  ballarin@14551  661  fix x y  wenzelm@14693  662  assume L: "x \ carrier L" "y \ carrier L"  ballarin@14551  663  show "EX s. least L s (Upper L {x, y})"  ballarin@14551  664  proof -  ballarin@14551  665  note total L  ballarin@14551  666  moreover  ballarin@14551  667  {  wenzelm@14693  668  assume "x \ y"  ballarin@14551  669  with L have "least L y (Upper L {x, y})"  wenzelm@14693  670  by (rule_tac least_UpperI) auto  ballarin@14551  671  }  ballarin@14551  672  moreover  ballarin@14551  673  {  wenzelm@14693  674  assume "y \ x"  ballarin@14551  675  with L have "least L x (Upper L {x, y})"  wenzelm@14693  676  by (rule_tac least_UpperI) auto  ballarin@14551  677  }  ballarin@14551  678  ultimately show ?thesis by blast  ballarin@14551  679  qed  ballarin@14551  680  next  ballarin@14551  681  fix x y  wenzelm@14693  682  assume L: "x \ carrier L" "y \ carrier L"  ballarin@14551  683  show "EX i. greatest L i (Lower L {x, y})"  ballarin@14551  684  proof -  ballarin@14551  685  note total L  ballarin@14551  686  moreover  ballarin@14551  687  {  wenzelm@14693  688  assume "y \ x"  ballarin@14551  689  with L have "greatest L y (Lower L {x, y})"  wenzelm@14693  690  by (rule_tac greatest_LowerI) auto  ballarin@14551  691  }  ballarin@14551  692  moreover  ballarin@14551  693  {  wenzelm@14693  694  assume "x \ y"  ballarin@14551  695  with L have "greatest L x (Lower L {x, y})"  wenzelm@14693  696  by (rule_tac greatest_LowerI) auto  ballarin@14551  697  }  ballarin@14551  698  ultimately show ?thesis by blast  ballarin@14551  699  qed  ballarin@14551  700  qed  ballarin@14551  701 qed (assumption | rule total_order_axioms.intro)+  ballarin@14551  702 wenzelm@14693  703 ballarin@14551  704 subsection {* Complete lattices *}  ballarin@14551  705 ballarin@14551  706 locale complete_lattice = lattice +  ballarin@14551  707  assumes sup_exists:  ballarin@14551  708  "[| A \ carrier L |] ==> EX s. least L s (Upper L A)"  ballarin@14551  709  and inf_exists:  ballarin@14551  710  "[| A \ carrier L |] ==> EX i. greatest L i (Lower L A)"  ballarin@14551  711 ballarin@14551  712 text {* Introduction rule: the usual definition of complete lattice *}  ballarin@14551  713 ballarin@14551  714 lemma (in partial_order) complete_latticeI:  ballarin@14551  715  assumes sup_exists:  ballarin@14551  716  "!!A. [| A \ carrier L |] ==> EX s. least L s (Upper L A)"  ballarin@14551  717  and inf_exists:  ballarin@14551  718  "!!A. [| A \ carrier L |] ==> EX i. greatest L i (Lower L A)"  ballarin@14551  719  shows "complete_lattice L"  ballarin@14551  720 proof (rule complete_lattice.intro)  ballarin@14551  721  show "lattice_axioms L"  wenzelm@14693  722  by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+  ballarin@14551  723 qed (assumption | rule complete_lattice_axioms.intro)+  ballarin@14551  724 wenzelm@14651  725 constdefs (structure L)  wenzelm@14651  726  top :: "_ => 'a" ("\\")  wenzelm@14651  727  "\ == sup L (carrier L)"  ballarin@14551  728 wenzelm@14651  729  bottom :: "_ => 'a" ("\\")  wenzelm@14651  730  "\ == inf L (carrier L)"  ballarin@14551  731 ballarin@14551  732 ballarin@14551  733 lemma (in complete_lattice) supI:  ballarin@14551  734  "[| !!l. least L l (Upper L A) ==> P l; A \ carrier L |]  wenzelm@14651  735  ==> P (\A)"  ballarin@14551  736 proof (unfold sup_def)  ballarin@14551  737  assume L: "A \ carrier L"  ballarin@14551  738  and P: "!!l. least L l (Upper L A) ==> P l"  ballarin@14551  739  with sup_exists obtain s where "least L s (Upper L A)" by blast  ballarin@14551  740  with L show "P (THE l. least L l (Upper L A))"  ballarin@14551  741  by (fast intro: theI2 least_unique P)  ballarin@14551  742 qed  ballarin@14551  743 ballarin@14551  744 lemma (in complete_lattice) sup_closed [simp]:  wenzelm@14693  745  "A \ carrier L ==> \A \ carrier L"  ballarin@14551  746  by (rule supI) simp_all  ballarin@14551  747 ballarin@14551  748 lemma (in complete_lattice) top_closed [simp, intro]:  ballarin@14551  749  "\ \ carrier L"  ballarin@14551  750  by (unfold top_def) simp  ballarin@14551  751 ballarin@14551  752 lemma (in complete_lattice) infI:  ballarin@14551  753  "[| !!i. greatest L i (Lower L A) ==> P i; A \ carrier L |]  wenzelm@14693  754  ==> P (\A)"  ballarin@14551  755 proof (unfold inf_def)  ballarin@14551  756  assume L: "A \ carrier L"  ballarin@14551  757  and P: "!!l. greatest L l (Lower L A) ==> P l"  ballarin@14551  758  with inf_exists obtain s where "greatest L s (Lower L A)" by blast  ballarin@14551  759  with L show "P (THE l. greatest L l (Lower L A))"  ballarin@14551  760  by (fast intro: theI2 greatest_unique P)  ballarin@14551  761 qed  ballarin@14551  762 ballarin@14551  763 lemma (in complete_lattice) inf_closed [simp]:  wenzelm@14693  764  "A \ carrier L ==> \A \ carrier L"  ballarin@14551  765  by (rule infI) simp_all  ballarin@14551  766 ballarin@14551  767 lemma (in complete_lattice) bottom_closed [simp, intro]:  ballarin@14551  768  "\ \ carrier L"  ballarin@14551  769  by (unfold bottom_def) simp  ballarin@14551  770 ballarin@14551  771 text {* Jacobson: Theorem 8.1 *}  ballarin@14551  772 ballarin@14551  773 lemma Lower_empty [simp]:  ballarin@14551  774  "Lower L {} = carrier L"  ballarin@14551  775  by (unfold Lower_def) simp  ballarin@14551  776 ballarin@14551  777 lemma Upper_empty [simp]:  ballarin@14551  778  "Upper L {} = carrier L"  ballarin@14551  779  by (unfold Upper_def) simp  ballarin@14551  780 ballarin@14551  781 theorem (in partial_order) complete_lattice_criterion1:  ballarin@14551  782  assumes top_exists: "EX g. greatest L g (carrier L)"  ballarin@14551  783  and inf_exists:  ballarin@14551  784  "!!A. [| A \ carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)"  ballarin@14551  785  shows "complete_lattice L"  ballarin@14551  786 proof (rule complete_latticeI)  ballarin@14551  787  from top_exists obtain top where top: "greatest L top (carrier L)" ..  ballarin@14551  788  fix A  ballarin@14551  789  assume L: "A \ carrier L"  ballarin@14551  790  let ?B = "Upper L A"  ballarin@14551  791  from L top have "top \ ?B" by (fast intro!: Upper_memI intro: greatest_le)  ballarin@14551  792  then have B_non_empty: "?B ~= {}" by fast  ballarin@14551  793  have B_L: "?B \ carrier L" by simp  ballarin@14551  794  from inf_exists [OF B_L B_non_empty]  ballarin@14551  795  obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..  ballarin@14551  796  have "least L b (Upper L A)"  ballarin@14551  797 apply (rule least_UpperI)  wenzelm@14693  798  apply (rule greatest_le [where A = "Lower L ?B"])  ballarin@14551  799  apply (rule b_inf_B)  ballarin@14551  800  apply (rule Lower_memI)  ballarin@14551  801  apply (erule UpperD)  ballarin@14551  802  apply assumption  ballarin@14551  803  apply (rule L)  ballarin@14551  804  apply (fast intro: L [THEN subsetD])  ballarin@14551  805  apply (erule greatest_Lower_above [OF b_inf_B])  ballarin@14551  806  apply simp  ballarin@14551  807  apply (rule L)  ballarin@14551  808 apply (rule greatest_carrier [OF b_inf_B]) (* rename rule: _closed *)  ballarin@14551  809 done  ballarin@14551  810  then show "EX s. least L s (Upper L A)" ..  ballarin@14551  811 next  ballarin@14551  812  fix A  ballarin@14551  813  assume L: "A \ carrier L"  ballarin@14551  814  show "EX i. greatest L i (Lower L A)"  ballarin@14551  815  proof (cases "A = {}")  ballarin@14551  816  case True then show ?thesis  ballarin@14551  817  by (simp add: top_exists)  ballarin@14551  818  next  ballarin@14551  819  case False with L show ?thesis  ballarin@14551  820  by (rule inf_exists)  ballarin@14551  821  qed  ballarin@14551  822 qed  ballarin@14551  823 ballarin@14551  824 (* TODO: prove dual version *)  ballarin@14551  825 ballarin@14551  826 subsection {* Examples *}  ballarin@14551  827 ballarin@14551  828 subsubsection {* Powerset of a set is a complete lattice *}  ballarin@14551  829 ballarin@14551  830 theorem powerset_is_complete_lattice:  ballarin@14551  831  "complete_lattice (| carrier = Pow A, le = op \ |)"  ballarin@14551  832  (is "complete_lattice ?L")  ballarin@14551  833 proof (rule partial_order.complete_latticeI)  ballarin@14551  834  show "partial_order ?L"  ballarin@14551  835  by (rule partial_order.intro) auto  ballarin@14551  836 next  ballarin@14551  837  fix B  ballarin@14551  838  assume "B \ carrier ?L"  ballarin@14551  839  then have "least ?L (\ B) (Upper ?L B)"  ballarin@14551  840  by (fastsimp intro!: least_UpperI simp: Upper_def)  ballarin@14551  841  then show "EX s. least ?L s (Upper ?L B)" ..  ballarin@14551  842 next  ballarin@14551  843  fix B  ballarin@14551  844  assume "B \ carrier ?L"  ballarin@14551  845  then have "greatest ?L (\ B \ A) (Lower ?L B)"  ballarin@14551  846  txt {* @{term "\ B"} is not the infimum of @{term B}:  ballarin@14551  847  @{term "\ {} = UNIV"} which is in general bigger than @{term "A"}! *}  ballarin@14551  848  by (fastsimp intro!: greatest_LowerI simp: Lower_def)  ballarin@14551  849  then show "EX i. greatest ?L i (Lower ?L B)" ..  ballarin@14551  850 qed  ballarin@14551  851 ballarin@14751  852 text {* An other example, that of the lattice of subgroups of a group,  ballarin@14751  853  can be found in Group theory (Section~\ref{sec:subgroup-lattice}). *}  ballarin@14551  854 wenzelm@14693  855 end