src/HOL/Algebra/Lattice.thy
 author ballarin Thu Aug 31 21:48:03 2017 +0200 (23 months ago) changeset 66580 e5b1d4d55bf6 parent 65099 30d0b2f1df76 child 67091 1393c2340eec permissions -rw-r--r--
Avoid \mu and \nu as constant syntax, use LFP and GFP instead.
 wenzelm@35849  1 (* Title: HOL/Algebra/Lattice.thy  wenzelm@35849  2  Author: Clemens Ballarin, started 7 November 2003  wenzelm@35849  3  Copyright: Clemens Ballarin  ballarin@27714  4 ballarin@27717  5 Most congruence rules by Stephan Hohe.  ballarin@65099  6 With additional contributions from Alasdair Armstrong and Simon Foster.  ballarin@14551  7 *)  ballarin@14551  8 wenzelm@35849  9 theory Lattice  ballarin@65099  10 imports Order  wenzelm@44472  11 begin  ballarin@27713  12 ballarin@65099  13 section \Lattices\  ballarin@65099  14   ballarin@65099  15 subsection \Supremum and infimum\  ballarin@27713  16 wenzelm@35847  17 definition  ballarin@27713  18  sup :: "[_, 'a set] => 'a" ("\\_" [90] 90)  wenzelm@35848  19  where "\\<^bsub>L\<^esub>A = (SOME x. least L x (Upper L A))"  ballarin@27713  20 wenzelm@35847  21 definition  ballarin@27713  22  inf :: "[_, 'a set] => 'a" ("\\_" [90] 90)  wenzelm@35848  23  where "\\<^bsub>L\<^esub>A = (SOME x. greatest L x (Lower L A))"  ballarin@27713  24 ballarin@65099  25 definition supr ::  ballarin@65099  26  "('a, 'b) gorder_scheme \ 'c set \ ('c \ 'a) \ 'a "  ballarin@65099  27  where "supr L A f = \\<^bsub>L\<^esub>(f  A)"  ballarin@65099  28 ballarin@65099  29 definition infi ::  ballarin@65099  30  "('a, 'b) gorder_scheme \ 'c set \ ('c \ 'a) \ 'a "  ballarin@65099  31  where "infi L A f = \\<^bsub>L\<^esub>(f  A)"  ballarin@65099  32 ballarin@65099  33 syntax  ballarin@65099  34  "_inf1" :: "('a, 'b) gorder_scheme \ pttrns \ 'a \ 'a" ("(3IINF\ _./ _)" [0, 10] 10)  ballarin@65099  35  "_inf" :: "('a, 'b) gorder_scheme \ pttrn \ 'c set \ 'a \ 'a" ("(3IINF\ _:_./ _)" [0, 0, 10] 10)  ballarin@65099  36  "_sup1" :: "('a, 'b) gorder_scheme \ pttrns \ 'a \ 'a" ("(3SSUP\ _./ _)" [0, 10] 10)  ballarin@65099  37  "_sup" :: "('a, 'b) gorder_scheme \ pttrn \ 'c set \ 'a \ 'a" ("(3SSUP\ _:_./ _)" [0, 0, 10] 10)  ballarin@65099  38 ballarin@65099  39 translations  ballarin@65099  40  "IINF\<^bsub>L\<^esub> x. B" == "CONST infi L CONST UNIV (%x. B)"  ballarin@65099  41  "IINF\<^bsub>L\<^esub> x:A. B" == "CONST infi L A (%x. B)"  ballarin@65099  42  "SSUP\<^bsub>L\<^esub> x. B" == "CONST supr L CONST UNIV (%x. B)"  ballarin@65099  43  "SSUP\<^bsub>L\<^esub> x:A. B" == "CONST supr L A (%x. B)"  ballarin@65099  44 wenzelm@35847  45 definition  ballarin@27713  46  join :: "[_, 'a, 'a] => 'a" (infixl "\\" 65)  wenzelm@35848  47  where "x \\<^bsub>L\<^esub> y = \\<^bsub>L\<^esub>{x, y}"  ballarin@27713  48 wenzelm@35847  49 definition  ballarin@27713  50  meet :: "[_, 'a, 'a] => 'a" (infixl "\\" 70)  wenzelm@35848  51  where "x \\<^bsub>L\<^esub> y = \\<^bsub>L\<^esub>{x, y}"  ballarin@27713  52 ballarin@65099  53 definition  ballarin@66580  54  LEAST_FP :: "('a, 'b) gorder_scheme \ ('a \ 'a) \ 'a" ("LFP\") where  ballarin@66580  55  "LEAST_FP L f = \\<^bsub>L\<^esub> {u \ carrier L. f u \\<^bsub>L\<^esub> u}" --\least fixed point\  ballarin@65099  56 ballarin@65099  57 definition  ballarin@66580  58  GREATEST_FP:: "('a, 'b) gorder_scheme \ ('a \ 'a) \ 'a" ("GFP\") where  ballarin@66580  59  "GREATEST_FP L f = \\<^bsub>L\<^esub> {u \ carrier L. u \\<^bsub>L\<^esub> f u}" --\greatest fixed point\  ballarin@65099  60 ballarin@65099  61 ballarin@65099  62 subsection \Dual operators\  ballarin@65099  63 ballarin@65099  64 lemma sup_dual [simp]:  ballarin@65099  65  "\\<^bsub>inv_gorder L\<^esub>A = \\<^bsub>L\<^esub>A"  ballarin@65099  66  by (simp add: sup_def inf_def)  ballarin@65099  67 ballarin@65099  68 lemma inf_dual [simp]:  ballarin@65099  69  "\\<^bsub>inv_gorder L\<^esub>A = \\<^bsub>L\<^esub>A"  ballarin@65099  70  by (simp add: sup_def inf_def)  ballarin@65099  71 ballarin@65099  72 lemma join_dual [simp]:  ballarin@65099  73  "p \\<^bsub>inv_gorder L\<^esub> q = p \\<^bsub>L\<^esub> q"  ballarin@65099  74  by (simp add:join_def meet_def)  ballarin@65099  75 ballarin@65099  76 lemma meet_dual [simp]:  ballarin@65099  77  "p \\<^bsub>inv_gorder L\<^esub> q = p \\<^bsub>L\<^esub> q"  ballarin@65099  78  by (simp add:join_def meet_def)  ballarin@65099  79 ballarin@65099  80 lemma top_dual [simp]:  ballarin@65099  81  "\\<^bsub>inv_gorder L\<^esub> = \\<^bsub>L\<^esub>"  ballarin@65099  82  by (simp add: top_def bottom_def)  ballarin@65099  83 ballarin@65099  84 lemma bottom_dual [simp]:  ballarin@65099  85  "\\<^bsub>inv_gorder L\<^esub> = \\<^bsub>L\<^esub>"  ballarin@65099  86  by (simp add: top_def bottom_def)  ballarin@65099  87 ballarin@65099  88 lemma LFP_dual [simp]:  ballarin@66580  89  "LEAST_FP (inv_gorder L) f = GREATEST_FP L f"  ballarin@66580  90  by (simp add:LEAST_FP_def GREATEST_FP_def)  ballarin@65099  91 ballarin@65099  92 lemma GFP_dual [simp]:  ballarin@66580  93  "GREATEST_FP (inv_gorder L) f = LEAST_FP L f"  ballarin@66580  94  by (simp add:LEAST_FP_def GREATEST_FP_def)  ballarin@65099  95 ballarin@27713  96 wenzelm@61382  97 subsection \Lattices\  ballarin@27713  98 ballarin@27713  99 locale weak_upper_semilattice = weak_partial_order +  ballarin@27713  100  assumes sup_of_two_exists:  ballarin@27713  101  "[| x \ carrier L; y \ carrier L |] ==> EX s. least L s (Upper L {x, y})"  ballarin@27713  102 ballarin@27713  103 locale weak_lower_semilattice = weak_partial_order +  ballarin@27713  104  assumes inf_of_two_exists:  ballarin@27713  105  "[| x \ carrier L; y \ carrier L |] ==> EX s. greatest L s (Lower L {x, y})"  ballarin@27713  106 ballarin@27713  107 locale weak_lattice = weak_upper_semilattice + weak_lower_semilattice  ballarin@27713  108 ballarin@65099  109 lemma (in weak_lattice) dual_weak_lattice:  ballarin@65099  110  "weak_lattice (inv_gorder L)"  ballarin@65099  111 proof -  ballarin@65099  112  interpret dual: weak_partial_order "inv_gorder L"  ballarin@65099  113  by (metis dual_weak_order)  ballarin@65099  114 ballarin@65099  115  show ?thesis  ballarin@65099  116  apply (unfold_locales)  ballarin@65099  117  apply (simp_all add: inf_of_two_exists sup_of_two_exists)  ballarin@65099  118  done  ballarin@65099  119 qed  ballarin@65099  120 wenzelm@14666  121 wenzelm@61382  122 subsubsection \Supremum\  ballarin@14551  123 ballarin@27713  124 lemma (in weak_upper_semilattice) joinI:  ballarin@22063  125  "[| !!l. least L l (Upper L {x, y}) ==> P l; x \ carrier L; y \ carrier L |]  ballarin@14551  126  ==> P (x \ y)"  ballarin@14551  127 proof (unfold join_def sup_def)  ballarin@22063  128  assume L: "x \ carrier L" "y \ carrier L"  ballarin@22063  129  and P: "!!l. least L l (Upper L {x, y}) ==> P l"  ballarin@22063  130  with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast  ballarin@27713  131  with L show "P (SOME l. least L l (Upper L {x, y}))"  ballarin@27713  132  by (fast intro: someI2 P)  ballarin@14551  133 qed  ballarin@14551  134 ballarin@27713  135 lemma (in weak_upper_semilattice) join_closed [simp]:  ballarin@22063  136  "[| x \ carrier L; y \ carrier L |] ==> x \ y \ carrier L"  ballarin@27700  137  by (rule joinI) (rule least_closed)  ballarin@14551  138 ballarin@27713  139 lemma (in weak_upper_semilattice) join_cong_l:  ballarin@27713  140  assumes carr: "x \ carrier L" "x' \ carrier L" "y \ carrier L"  ballarin@27713  141  and xx': "x .= x'"  ballarin@27713  142  shows "x \ y .= x' \ y"  ballarin@27713  143 proof (rule joinI, rule joinI)  ballarin@27713  144  fix a b  ballarin@27713  145  from xx' carr  ballarin@27713  146  have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)  ballarin@27713  147 ballarin@27713  148  assume leasta: "least L a (Upper L {x, y})"  ballarin@27713  149  assume "least L b (Upper L {x', y})"  ballarin@27713  150  with carr  ballarin@27713  151  have leastb: "least L b (Upper L {x, y})"  ballarin@27713  152  by (simp add: least_Upper_cong_r[OF _ _ seq])  ballarin@27713  153 ballarin@27713  154  from leasta leastb  ballarin@27713  155  show "a .= b" by (rule weak_least_unique)  ballarin@27713  156 qed (rule carr)+  ballarin@14551  157 ballarin@27713  158 lemma (in weak_upper_semilattice) join_cong_r:  ballarin@27713  159  assumes carr: "x \ carrier L" "y \ carrier L" "y' \ carrier L"  ballarin@27713  160  and yy': "y .= y'"  ballarin@27713  161  shows "x \ y .= x \ y'"  ballarin@27713  162 proof (rule joinI, rule joinI)  ballarin@27713  163  fix a b  ballarin@27713  164  have "{x, y} = {y, x}" by fast  ballarin@27713  165  also from carr yy'  ballarin@27713  166  have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)  ballarin@27713  167  also have "{y', x} = {x, y'}" by fast  ballarin@27713  168  finally  ballarin@27713  169  have seq: "{x, y} {.=} {x, y'}" .  ballarin@14551  170 ballarin@27713  171  assume leasta: "least L a (Upper L {x, y})"  ballarin@27713  172  assume "least L b (Upper L {x, y'})"  ballarin@27713  173  with carr  ballarin@27713  174  have leastb: "least L b (Upper L {x, y})"  ballarin@27713  175  by (simp add: least_Upper_cong_r[OF _ _ seq])  ballarin@27713  176 ballarin@27713  177  from leasta leastb  ballarin@27713  178  show "a .= b" by (rule weak_least_unique)  ballarin@27713  179 qed (rule carr)+  ballarin@27713  180 ballarin@27713  181 lemma (in weak_partial_order) sup_of_singletonI: (* only reflexivity needed ? *)  ballarin@27713  182  "x \ carrier L ==> least L x (Upper L {x})"  ballarin@27713  183  by (rule least_UpperI) auto  ballarin@27713  184 ballarin@27713  185 lemma (in weak_partial_order) weak_sup_of_singleton [simp]:  ballarin@27713  186  "x \ carrier L ==> \{x} .= x"  ballarin@27713  187  unfolding sup_def  ballarin@27713  188  by (rule someI2) (auto intro: weak_least_unique sup_of_singletonI)  ballarin@27713  189 ballarin@27713  190 lemma (in weak_partial_order) sup_of_singleton_closed [simp]:  ballarin@27713  191  "x \ carrier L \ \{x} \ carrier L"  ballarin@27713  192  unfolding sup_def  ballarin@27713  193  by (rule someI2) (auto intro: sup_of_singletonI)  wenzelm@14666  194 wenzelm@63167  195 text \Condition on \A\: supremum exists.\  ballarin@14551  196 ballarin@27713  197 lemma (in weak_upper_semilattice) sup_insertI:  ballarin@22063  198  "[| !!s. least L s (Upper L (insert x A)) ==> P s;  ballarin@22063  199  least L a (Upper L A); x \ carrier L; A \ carrier L |]  wenzelm@14693  200  ==> P (\(insert x A))"  ballarin@14551  201 proof (unfold sup_def)  ballarin@22063  202  assume L: "x \ carrier L" "A \ carrier L"  ballarin@22063  203  and P: "!!l. least L l (Upper L (insert x A)) ==> P l"  ballarin@22063  204  and least_a: "least L a (Upper L A)"  ballarin@22063  205  from L least_a have La: "a \ carrier L" by simp  ballarin@14551  206  from L sup_of_two_exists least_a  ballarin@22063  207  obtain s where least_s: "least L s (Upper L {a, x})" by blast  ballarin@27713  208  show "P (SOME l. least L l (Upper L (insert x A)))"  ballarin@27713  209  proof (rule someI2)  ballarin@22063  210  show "least L s (Upper L (insert x A))"  ballarin@14551  211  proof (rule least_UpperI)  ballarin@14551  212  fix z  wenzelm@14693  213  assume "z \ insert x A"  wenzelm@14693  214  then show "z \ s"  wenzelm@14693  215  proof  wenzelm@14693  216  assume "z = x" then show ?thesis  wenzelm@14693  217  by (simp add: least_Upper_above [OF least_s] L La)  wenzelm@14693  218  next  wenzelm@14693  219  assume "z \ A"  wenzelm@14693  220  with L least_s least_a show ?thesis  ballarin@27713  221  by (rule_tac le_trans [where y = a]) (auto dest: least_Upper_above)  wenzelm@14693  222  qed  wenzelm@14693  223  next  wenzelm@14693  224  fix y  ballarin@22063  225  assume y: "y \ Upper L (insert x A)"  wenzelm@14693  226  show "s \ y"  wenzelm@14693  227  proof (rule least_le [OF least_s], rule Upper_memI)  wenzelm@32960  228  fix z  wenzelm@32960  229  assume z: "z \ {a, x}"  wenzelm@32960  230  then show "z \ y"  wenzelm@32960  231  proof  ballarin@22063  232  have y': "y \ Upper L A"  ballarin@22063  233  apply (rule subsetD [where A = "Upper L (insert x A)"])  wenzelm@23463  234  apply (rule Upper_antimono)  wenzelm@32960  235  apply blast  wenzelm@32960  236  apply (rule y)  wenzelm@14693  237  done  wenzelm@14693  238  assume "z = a"  wenzelm@14693  239  with y' least_a show ?thesis by (fast dest: least_le)  wenzelm@32960  240  next  wenzelm@32960  241  assume "z \ {x}" (* FIXME "z = x"; declare specific elim rule for "insert x {}" (!?) *)  wenzelm@14693  242  with y L show ?thesis by blast  wenzelm@32960  243  qed  wenzelm@23350  244  qed (rule Upper_closed [THEN subsetD, OF y])  wenzelm@14693  245  next  ballarin@22063  246  from L show "insert x A \ carrier L" by simp  ballarin@22063  247  from least_s show "s \ carrier L" by simp  ballarin@14551  248  qed  wenzelm@23350  249  qed (rule P)  ballarin@14551  250 qed  ballarin@14551  251 ballarin@27713  252 lemma (in weak_upper_semilattice) finite_sup_least:  ballarin@22063  253  "[| finite A; A \ carrier L; A ~= {} |] ==> least L (\A) (Upper L A)"  berghofe@22265  254 proof (induct set: finite)  wenzelm@14693  255  case empty  wenzelm@14693  256  then show ?case by simp  ballarin@14551  257 next  nipkow@15328  258  case (insert x A)  ballarin@14551  259  show ?case  ballarin@14551  260  proof (cases "A = {}")  ballarin@14551  261  case True  ballarin@27713  262  with insert show ?thesis  wenzelm@44472  263  by simp (simp add: least_cong [OF weak_sup_of_singleton] sup_of_singletonI)  wenzelm@32960  264  (* The above step is hairy; least_cong can make simp loop.  wenzelm@32960  265  Would want special version of simp to apply least_cong. *)  ballarin@14551  266  next  ballarin@14551  267  case False  ballarin@22063  268  with insert have "least L (\A) (Upper L A)" by simp  wenzelm@14693  269  with _ show ?thesis  wenzelm@14693  270  by (rule sup_insertI) (simp_all add: insert [simplified])  ballarin@14551  271  qed  ballarin@14551  272 qed  ballarin@14551  273 ballarin@27713  274 lemma (in weak_upper_semilattice) finite_sup_insertI:  ballarin@22063  275  assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l"  ballarin@22063  276  and xA: "finite A" "x \ carrier L" "A \ carrier L"  ballarin@65099  277  shows "P (\ (insert x A))"  ballarin@14551  278 proof (cases "A = {}")  ballarin@14551  279  case True with P and xA show ?thesis  ballarin@27713  280  by (simp add: finite_sup_least)  ballarin@14551  281 next  ballarin@14551  282  case False with P and xA show ?thesis  ballarin@14551  283  by (simp add: sup_insertI finite_sup_least)  ballarin@14551  284 qed  ballarin@14551  285 ballarin@27713  286 lemma (in weak_upper_semilattice) finite_sup_closed [simp]:  ballarin@22063  287  "[| finite A; A \ carrier L; A ~= {} |] ==> \A \ carrier L"  berghofe@22265  288 proof (induct set: finite)  ballarin@14551  289  case empty then show ?case by simp  ballarin@14551  290 next  nipkow@15328  291  case insert then show ?case  wenzelm@14693  292  by - (rule finite_sup_insertI, simp_all)  ballarin@14551  293 qed  ballarin@14551  294 ballarin@27713  295 lemma (in weak_upper_semilattice) join_left:  ballarin@22063  296  "[| x \ carrier L; y \ carrier L |] ==> x \ x \ y"  wenzelm@14693  297  by (rule joinI [folded join_def]) (blast dest: least_mem)  ballarin@14551  298 ballarin@27713  299 lemma (in weak_upper_semilattice) join_right:  ballarin@22063  300  "[| x \ carrier L; y \ carrier L |] ==> y \ x \ y"  wenzelm@14693  301  by (rule joinI [folded join_def]) (blast dest: least_mem)  ballarin@14551  302 ballarin@27713  303 lemma (in weak_upper_semilattice) sup_of_two_least:  ballarin@22063  304  "[| x \ carrier L; y \ carrier L |] ==> least L (\{x, y}) (Upper L {x, y})"  ballarin@14551  305 proof (unfold sup_def)  ballarin@22063  306  assume L: "x \ carrier L" "y \ carrier L"  ballarin@22063  307  with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast  ballarin@27713  308  with L show "least L (SOME z. least L z (Upper L {x, y})) (Upper L {x, y})"  ballarin@27713  309  by (fast intro: someI2 weak_least_unique) (* blast fails *)  ballarin@14551  310 qed  ballarin@14551  311 ballarin@27713  312 lemma (in weak_upper_semilattice) join_le:  wenzelm@14693  313  assumes sub: "x \ z" "y \ z"  wenzelm@23350  314  and x: "x \ carrier L" and y: "y \ carrier L" and z: "z \ carrier L"  ballarin@14551  315  shows "x \ y \ z"  wenzelm@23350  316 proof (rule joinI [OF _ x y])  ballarin@14551  317  fix s  ballarin@22063  318  assume "least L s (Upper L {x, y})"  wenzelm@23350  319  with sub z show "s \ z" by (fast elim: least_le intro: Upper_memI)  ballarin@14551  320 qed  wenzelm@14693  321 ballarin@65099  322 lemma (in weak_lattice) weak_le_iff_meet:  ballarin@65099  323  assumes "x \ carrier L" "y \ carrier L"  ballarin@65099  324  shows "x \ y \ (x \ y) .= y"  ballarin@65099  325  by (meson assms(1) assms(2) join_closed join_le join_left join_right le_cong_r local.le_refl weak_le_antisym)  ballarin@65099  326   ballarin@27713  327 lemma (in weak_upper_semilattice) weak_join_assoc_lemma:  ballarin@22063  328  assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L"  ballarin@27713  329  shows "x \ (y \ z) .= \{x, y, z}"  ballarin@14551  330 proof (rule finite_sup_insertI)  wenzelm@63167  331  \ \The textbook argument in Jacobson I, p 457\  ballarin@14551  332  fix s  ballarin@22063  333  assume sup: "least L s (Upper L {x, y, z})"  ballarin@27713  334  show "x \ (y \ z) .= s"  nipkow@33657  335  proof (rule weak_le_antisym)  ballarin@14551  336  from sup L show "x \ (y \ z) \ s"  nipkow@44890  337  by (fastforce intro!: join_le elim: least_Upper_above)  ballarin@14551  338  next  ballarin@14551  339  from sup L show "s \ x \ (y \ z)"  ballarin@14551  340  by (erule_tac least_le)  ballarin@27713  341  (blast intro!: Upper_memI intro: le_trans join_left join_right join_closed)  ballarin@27700  342  qed (simp_all add: L least_closed [OF sup])  ballarin@14551  343 qed (simp_all add: L)  ballarin@14551  344 wenzelm@63167  345 text \Commutativity holds for \=\.\  ballarin@27713  346 ballarin@22063  347 lemma join_comm:  ballarin@22063  348  fixes L (structure)  ballarin@22063  349  shows "x \ y = y \ x"  ballarin@14551  350  by (unfold join_def) (simp add: insert_commute)  ballarin@14551  351 ballarin@27713  352 lemma (in weak_upper_semilattice) weak_join_assoc:  ballarin@22063  353  assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L"  ballarin@27713  354  shows "(x \ y) \ z .= x \ (y \ z)"  ballarin@14551  355 proof -  ballarin@27713  356  (* FIXME: could be simplified by improved simp: uniform use of .=,  ballarin@27713  357  omit [symmetric] in last step. *)  ballarin@14551  358  have "(x \ y) \ z = z \ (x \ y)" by (simp only: join_comm)  ballarin@27713  359  also from L have "... .= \{z, x, y}" by (simp add: weak_join_assoc_lemma)  wenzelm@14693  360  also from L have "... = \{x, y, z}" by (simp add: insert_commute)  ballarin@27713  361  also from L have "... .= x \ (y \ z)" by (simp add: weak_join_assoc_lemma [symmetric])  ballarin@27713  362  finally show ?thesis by (simp add: L)  ballarin@14551  363 qed  ballarin@14551  364 wenzelm@14693  365 wenzelm@61382  366 subsubsection \Infimum\  ballarin@14551  367 ballarin@27713  368 lemma (in weak_lower_semilattice) meetI:  ballarin@22063  369  "[| !!i. greatest L i (Lower L {x, y}) ==> P i;  ballarin@22063  370  x \ carrier L; y \ carrier L |]  ballarin@14551  371  ==> P (x \ y)"  ballarin@14551  372 proof (unfold meet_def inf_def)  ballarin@22063  373  assume L: "x \ carrier L" "y \ carrier L"  ballarin@22063  374  and P: "!!g. greatest L g (Lower L {x, y}) ==> P g"  ballarin@22063  375  with inf_of_two_exists obtain i where "greatest L i (Lower L {x, y})" by fast  ballarin@27713  376  with L show "P (SOME g. greatest L g (Lower L {x, y}))"  ballarin@27713  377  by (fast intro: someI2 weak_greatest_unique P)  ballarin@14551  378 qed  ballarin@14551  379 ballarin@27713  380 lemma (in weak_lower_semilattice) meet_closed [simp]:  ballarin@22063  381  "[| x \ carrier L; y \ carrier L |] ==> x \ y \ carrier L"  ballarin@27700  382  by (rule meetI) (rule greatest_closed)  ballarin@14551  383 ballarin@27713  384 lemma (in weak_lower_semilattice) meet_cong_l:  ballarin@27713  385  assumes carr: "x \ carrier L" "x' \ carrier L" "y \ carrier L"  ballarin@27713  386  and xx': "x .= x'"  ballarin@27713  387  shows "x \ y .= x' \ y"  ballarin@27713  388 proof (rule meetI, rule meetI)  ballarin@27713  389  fix a b  ballarin@27713  390  from xx' carr  ballarin@27713  391  have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)  ballarin@27713  392 ballarin@27713  393  assume greatesta: "greatest L a (Lower L {x, y})"  ballarin@27713  394  assume "greatest L b (Lower L {x', y})"  ballarin@27713  395  with carr  ballarin@27713  396  have greatestb: "greatest L b (Lower L {x, y})"  ballarin@27713  397  by (simp add: greatest_Lower_cong_r[OF _ _ seq])  ballarin@27713  398 ballarin@27713  399  from greatesta greatestb  ballarin@27713  400  show "a .= b" by (rule weak_greatest_unique)  ballarin@27713  401 qed (rule carr)+  ballarin@14551  402 ballarin@27713  403 lemma (in weak_lower_semilattice) meet_cong_r:  ballarin@27713  404  assumes carr: "x \ carrier L" "y \ carrier L" "y' \ carrier L"  ballarin@27713  405  and yy': "y .= y'"  ballarin@27713  406  shows "x \ y .= x \ y'"  ballarin@27713  407 proof (rule meetI, rule meetI)  ballarin@27713  408  fix a b  ballarin@27713  409  have "{x, y} = {y, x}" by fast  ballarin@27713  410  also from carr yy'  ballarin@27713  411  have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)  ballarin@27713  412  also have "{y', x} = {x, y'}" by fast  ballarin@27713  413  finally  ballarin@27713  414  have seq: "{x, y} {.=} {x, y'}" .  ballarin@27713  415 ballarin@27713  416  assume greatesta: "greatest L a (Lower L {x, y})"  ballarin@27713  417  assume "greatest L b (Lower L {x, y'})"  ballarin@27713  418  with carr  ballarin@27713  419  have greatestb: "greatest L b (Lower L {x, y})"  ballarin@27713  420  by (simp add: greatest_Lower_cong_r[OF _ _ seq])  ballarin@14551  421 ballarin@27713  422  from greatesta greatestb  ballarin@27713  423  show "a .= b" by (rule weak_greatest_unique)  ballarin@27713  424 qed (rule carr)+  ballarin@27713  425 ballarin@27713  426 lemma (in weak_partial_order) inf_of_singletonI: (* only reflexivity needed ? *)  ballarin@27713  427  "x \ carrier L ==> greatest L x (Lower L {x})"  ballarin@27713  428  by (rule greatest_LowerI) auto  ballarin@14551  429 ballarin@27713  430 lemma (in weak_partial_order) weak_inf_of_singleton [simp]:  ballarin@27713  431  "x \ carrier L ==> \{x} .= x"  ballarin@27713  432  unfolding inf_def  ballarin@27713  433  by (rule someI2) (auto intro: weak_greatest_unique inf_of_singletonI)  ballarin@27713  434 ballarin@27713  435 lemma (in weak_partial_order) inf_of_singleton_closed:  ballarin@27713  436  "x \ carrier L ==> \{x} \ carrier L"  ballarin@27713  437  unfolding inf_def  ballarin@27713  438  by (rule someI2) (auto intro: inf_of_singletonI)  ballarin@27713  439 wenzelm@63167  440 text \Condition on \A\: infimum exists.\  ballarin@27713  441 ballarin@27713  442 lemma (in weak_lower_semilattice) inf_insertI:  ballarin@22063  443  "[| !!i. greatest L i (Lower L (insert x A)) ==> P i;  ballarin@22063  444  greatest L a (Lower L A); x \ carrier L; A \ carrier L |]  wenzelm@14693  445  ==> P (\(insert x A))"  ballarin@14551  446 proof (unfold inf_def)  ballarin@22063  447  assume L: "x \ carrier L" "A \ carrier L"  ballarin@22063  448  and P: "!!g. greatest L g (Lower L (insert x A)) ==> P g"  ballarin@22063  449  and greatest_a: "greatest L a (Lower L A)"  ballarin@22063  450  from L greatest_a have La: "a \ carrier L" by simp  ballarin@14551  451  from L inf_of_two_exists greatest_a  ballarin@22063  452  obtain i where greatest_i: "greatest L i (Lower L {a, x})" by blast  ballarin@27713  453  show "P (SOME g. greatest L g (Lower L (insert x A)))"  ballarin@27713  454  proof (rule someI2)  ballarin@22063  455  show "greatest L i (Lower L (insert x A))"  ballarin@14551  456  proof (rule greatest_LowerI)  ballarin@14551  457  fix z  wenzelm@14693  458  assume "z \ insert x A"  wenzelm@14693  459  then show "i \ z"  wenzelm@14693  460  proof  wenzelm@14693  461  assume "z = x" then show ?thesis  ballarin@27700  462  by (simp add: greatest_Lower_below [OF greatest_i] L La)  wenzelm@14693  463  next  wenzelm@14693  464  assume "z \ A"  wenzelm@14693  465  with L greatest_i greatest_a show ?thesis  ballarin@27713  466  by (rule_tac le_trans [where y = a]) (auto dest: greatest_Lower_below)  wenzelm@14693  467  qed  wenzelm@14693  468  next  wenzelm@14693  469  fix y  ballarin@22063  470  assume y: "y \ Lower L (insert x A)"  wenzelm@14693  471  show "y \ i"  wenzelm@14693  472  proof (rule greatest_le [OF greatest_i], rule Lower_memI)  wenzelm@32960  473  fix z  wenzelm@32960  474  assume z: "z \ {a, x}"  wenzelm@32960  475  then show "y \ z"  wenzelm@32960  476  proof  ballarin@22063  477  have y': "y \ Lower L A"  ballarin@22063  478  apply (rule subsetD [where A = "Lower L (insert x A)"])  wenzelm@23463  479  apply (rule Lower_antimono)  wenzelm@32960  480  apply blast  wenzelm@32960  481  apply (rule y)  wenzelm@14693  482  done  wenzelm@14693  483  assume "z = a"  wenzelm@14693  484  with y' greatest_a show ?thesis by (fast dest: greatest_le)  wenzelm@32960  485  next  wenzelm@14693  486  assume "z \ {x}"  wenzelm@14693  487  with y L show ?thesis by blast  wenzelm@32960  488  qed  wenzelm@23350  489  qed (rule Lower_closed [THEN subsetD, OF y])  wenzelm@14693  490  next  ballarin@22063  491  from L show "insert x A \ carrier L" by simp  ballarin@22063  492  from greatest_i show "i \ carrier L" by simp  ballarin@14551  493  qed  wenzelm@23350  494  qed (rule P)  ballarin@14551  495 qed  ballarin@14551  496 ballarin@27713  497 lemma (in weak_lower_semilattice) finite_inf_greatest:  ballarin@22063  498  "[| finite A; A \ carrier L; A ~= {} |] ==> greatest L (\A) (Lower L A)"  berghofe@22265  499 proof (induct set: finite)  ballarin@14551  500  case empty then show ?case by simp  ballarin@14551  501 next  nipkow@15328  502  case (insert x A)  ballarin@14551  503  show ?case  ballarin@14551  504  proof (cases "A = {}")  ballarin@14551  505  case True  ballarin@27713  506  with insert show ?thesis  ballarin@27713  507  by simp (simp add: greatest_cong [OF weak_inf_of_singleton]  wenzelm@32960  508  inf_of_singleton_closed inf_of_singletonI)  ballarin@14551  509  next  ballarin@14551  510  case False  ballarin@14551  511  from insert show ?thesis  ballarin@14551  512  proof (rule_tac inf_insertI)  ballarin@22063  513  from False insert show "greatest L (\A) (Lower L A)" by simp  ballarin@14551  514  qed simp_all  ballarin@14551  515  qed  ballarin@14551  516 qed  ballarin@14551  517 ballarin@27713  518 lemma (in weak_lower_semilattice) finite_inf_insertI:  ballarin@22063  519  assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i"  ballarin@22063  520  and xA: "finite A" "x \ carrier L" "A \ carrier L"  ballarin@65099  521  shows "P (\ (insert x A))"  ballarin@14551  522 proof (cases "A = {}")  ballarin@14551  523  case True with P and xA show ?thesis  ballarin@27713  524  by (simp add: finite_inf_greatest)  ballarin@14551  525 next  ballarin@14551  526  case False with P and xA show ?thesis  ballarin@14551  527  by (simp add: inf_insertI finite_inf_greatest)  ballarin@14551  528 qed  ballarin@14551  529 ballarin@27713  530 lemma (in weak_lower_semilattice) finite_inf_closed [simp]:  ballarin@22063  531  "[| finite A; A \ carrier L; A ~= {} |] ==> \A \ carrier L"  berghofe@22265  532 proof (induct set: finite)  ballarin@14551  533  case empty then show ?case by simp  ballarin@14551  534 next  nipkow@15328  535  case insert then show ?case  ballarin@14551  536  by (rule_tac finite_inf_insertI) (simp_all)  ballarin@14551  537 qed  ballarin@14551  538 ballarin@27713  539 lemma (in weak_lower_semilattice) meet_left:  ballarin@22063  540  "[| x \ carrier L; y \ carrier L |] ==> x \ y \ x"  wenzelm@14693  541  by (rule meetI [folded meet_def]) (blast dest: greatest_mem)  ballarin@14551  542 ballarin@27713  543 lemma (in weak_lower_semilattice) meet_right:  ballarin@22063  544  "[| x \ carrier L; y \ carrier L |] ==> x \ y \ y"  wenzelm@14693  545  by (rule meetI [folded meet_def]) (blast dest: greatest_mem)  ballarin@14551  546 ballarin@27713  547 lemma (in weak_lower_semilattice) inf_of_two_greatest:  ballarin@22063  548  "[| x \ carrier L; y \ carrier L |] ==>  wenzelm@60585  549  greatest L (\{x, y}) (Lower L {x, y})"  ballarin@14551  550 proof (unfold inf_def)  ballarin@22063  551  assume L: "x \ carrier L" "y \ carrier L"  ballarin@22063  552  with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast  ballarin@14551  553  with L  ballarin@27713  554  show "greatest L (SOME z. greatest L z (Lower L {x, y})) (Lower L {x, y})"  ballarin@27713  555  by (fast intro: someI2 weak_greatest_unique) (* blast fails *)  ballarin@14551  556 qed  ballarin@14551  557 ballarin@27713  558 lemma (in weak_lower_semilattice) meet_le:  wenzelm@14693  559  assumes sub: "z \ x" "z \ y"  wenzelm@23350  560  and x: "x \ carrier L" and y: "y \ carrier L" and z: "z \ carrier L"  ballarin@14551  561  shows "z \ x \ y"  wenzelm@23350  562 proof (rule meetI [OF _ x y])  ballarin@14551  563  fix i  ballarin@22063  564  assume "greatest L i (Lower L {x, y})"  wenzelm@23350  565  with sub z show "z \ i" by (fast elim: greatest_le intro: Lower_memI)  ballarin@14551  566 qed  wenzelm@14693  567 ballarin@65099  568 lemma (in weak_lattice) weak_le_iff_join:  ballarin@65099  569  assumes "x \ carrier L" "y \ carrier L"  ballarin@65099  570  shows "x \ y \ x .= (x \ y)"  ballarin@65099  571  by (meson assms(1) assms(2) local.le_refl local.le_trans meet_closed meet_le meet_left meet_right weak_le_antisym weak_refl)  ballarin@65099  572   ballarin@27713  573 lemma (in weak_lower_semilattice) weak_meet_assoc_lemma:  ballarin@22063  574  assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L"  ballarin@27713  575  shows "x \ (y \ z) .= \{x, y, z}"  ballarin@14551  576 proof (rule finite_inf_insertI)  wenzelm@61382  577  txt \The textbook argument in Jacobson I, p 457\  ballarin@14551  578  fix i  ballarin@22063  579  assume inf: "greatest L i (Lower L {x, y, z})"  ballarin@27713  580  show "x \ (y \ z) .= i"  nipkow@33657  581  proof (rule weak_le_antisym)  ballarin@14551  582  from inf L show "i \ x \ (y \ z)"  nipkow@44890  583  by (fastforce intro!: meet_le elim: greatest_Lower_below)  ballarin@14551  584  next  ballarin@14551  585  from inf L show "x \ (y \ z) \ i"  ballarin@14551  586  by (erule_tac greatest_le)  ballarin@27713  587  (blast intro!: Lower_memI intro: le_trans meet_left meet_right meet_closed)  ballarin@27700  588  qed (simp_all add: L greatest_closed [OF inf])  ballarin@14551  589 qed (simp_all add: L)  ballarin@14551  590 ballarin@22063  591 lemma meet_comm:  ballarin@22063  592  fixes L (structure)  ballarin@22063  593  shows "x \ y = y \ x"  ballarin@14551  594  by (unfold meet_def) (simp add: insert_commute)  ballarin@14551  595 ballarin@27713  596 lemma (in weak_lower_semilattice) weak_meet_assoc:  ballarin@22063  597  assumes L: "x \ carrier L" "y \ carrier L" "z \ carrier L"  ballarin@27713  598  shows "(x \ y) \ z .= x \ (y \ z)"  ballarin@14551  599 proof -  ballarin@27713  600  (* FIXME: improved simp, see weak_join_assoc above *)  ballarin@14551  601  have "(x \ y) \ z = z \ (x \ y)" by (simp only: meet_comm)  ballarin@65099  602  also from L have "... .= \ {z, x, y}" by (simp add: weak_meet_assoc_lemma)  ballarin@65099  603  also from L have "... = \ {x, y, z}" by (simp add: insert_commute)  ballarin@27713  604  also from L have "... .= x \ (y \ z)" by (simp add: weak_meet_assoc_lemma [symmetric])  ballarin@27713  605  finally show ?thesis by (simp add: L)  ballarin@14551  606 qed  ballarin@14551  607 wenzelm@61382  608 text \Total orders are lattices.\  ballarin@24087  609 ballarin@65099  610 sublocale weak_total_order \ weak?: weak_lattice  haftmann@28823  611 proof  ballarin@24087  612  fix x y  ballarin@24087  613  assume L: "x \ carrier L" "y \ carrier L"  ballarin@24087  614  show "EX s. least L s (Upper L {x, y})"  ballarin@24087  615  proof -  ballarin@24087  616  note total L  ballarin@24087  617  moreover  ballarin@24087  618  {  ballarin@24087  619  assume "x \ y"  ballarin@24087  620  with L have "least L y (Upper L {x, y})"  ballarin@24087  621  by (rule_tac least_UpperI) auto  ballarin@24087  622  }  ballarin@24087  623  moreover  ballarin@24087  624  {  ballarin@24087  625  assume "y \ x"  ballarin@24087  626  with L have "least L x (Upper L {x, y})"  ballarin@24087  627  by (rule_tac least_UpperI) auto  ballarin@24087  628  }  ballarin@24087  629  ultimately show ?thesis by blast  ballarin@14551  630  qed  ballarin@24087  631 next  ballarin@24087  632  fix x y  ballarin@24087  633  assume L: "x \ carrier L" "y \ carrier L"  ballarin@24087  634  show "EX i. greatest L i (Lower L {x, y})"  ballarin@24087  635  proof -  ballarin@24087  636  note total L  ballarin@24087  637  moreover  ballarin@24087  638  {  ballarin@24087  639  assume "y \ x"  ballarin@24087  640  with L have "greatest L y (Lower L {x, y})"  ballarin@24087  641  by (rule_tac greatest_LowerI) auto  ballarin@24087  642  }  ballarin@24087  643  moreover  ballarin@24087  644  {  ballarin@24087  645  assume "x \ y"  ballarin@24087  646  with L have "greatest L x (Lower L {x, y})"  ballarin@24087  647  by (rule_tac greatest_LowerI) auto  ballarin@24087  648  }  ballarin@24087  649  ultimately show ?thesis by blast  ballarin@24087  650  qed  ballarin@24087  651 qed  ballarin@14551  652 wenzelm@14693  653 ballarin@65099  654 subsection \Weak Bounded Lattices\  ballarin@14551  655 ballarin@65099  656 locale weak_bounded_lattice =  ballarin@65099  657  weak_lattice +  ballarin@65099  658  weak_partial_order_bottom +  ballarin@65099  659  weak_partial_order_top  ballarin@27713  660 begin  ballarin@27713  661 ballarin@65099  662 lemma bottom_meet: "x \ carrier L \ \ \ x .= \"  ballarin@65099  663  by (metis bottom_least least_def meet_closed meet_left weak_le_antisym)  ballarin@27713  664 ballarin@65099  665 lemma bottom_join: "x \ carrier L \ \ \ x .= x"  ballarin@65099  666  by (metis bottom_least join_closed join_le join_right le_refl least_def weak_le_antisym)  ballarin@27713  667 ballarin@65099  668 lemma bottom_weak_eq:  ballarin@65099  669  "\ b \ carrier L; \ x. x \ carrier L \ b \ x \ \ b .= \"  ballarin@65099  670  by (metis bottom_closed bottom_lower weak_le_antisym)  ballarin@27713  671 ballarin@65099  672 lemma top_join: "x \ carrier L \ \ \ x .= \"  ballarin@65099  673  by (metis join_closed join_left top_closed top_higher weak_le_antisym)  ballarin@65099  674 ballarin@65099  675 lemma top_meet: "x \ carrier L \ \ \ x .= x"  ballarin@65099  676  by (metis le_refl meet_closed meet_le meet_right top_closed top_higher weak_le_antisym)  ballarin@65099  677 ballarin@65099  678 lemma top_weak_eq: "\ t \ carrier L; \ x. x \ carrier L \ x \ t \ \ t .= \"  ballarin@65099  679  by (metis top_closed top_higher weak_le_antisym)  ballarin@27713  680 ballarin@27713  681 end  ballarin@27713  682 ballarin@65099  683 sublocale weak_bounded_lattice \ weak_partial_order ..  ballarin@27713  684 ballarin@27713  685 ballarin@65099  686 subsection \Lattices where \eq\ is the Equality\  ballarin@27713  687 ballarin@27713  688 locale upper_semilattice = partial_order +  ballarin@27713  689  assumes sup_of_two_exists:  ballarin@27713  690  "[| x \ carrier L; y \ carrier L |] ==> EX s. least L s (Upper L {x, y})"  ballarin@27713  691 ballarin@65099  692 sublocale upper_semilattice \ weak?: weak_upper_semilattice  ballarin@65099  693  by unfold_locales (rule sup_of_two_exists)  ballarin@27713  694 ballarin@27713  695 locale lower_semilattice = partial_order +  ballarin@27713  696  assumes inf_of_two_exists:  ballarin@27713  697  "[| x \ carrier L; y \ carrier L |] ==> EX s. greatest L s (Lower L {x, y})"  ballarin@27713  698 ballarin@65099  699 sublocale lower_semilattice \ weak?: weak_lower_semilattice  ballarin@65099  700  by unfold_locales (rule inf_of_two_exists)  ballarin@27713  701 ballarin@27713  702 locale lattice = upper_semilattice + lower_semilattice  ballarin@27713  703 ballarin@65099  704 sublocale lattice \ weak_lattice ..  ballarin@27713  705 ballarin@65099  706 lemma (in lattice) dual_lattice:  ballarin@65099  707  "lattice (inv_gorder L)"  ballarin@65099  708 proof -  ballarin@65099  709  interpret dual: weak_lattice "inv_gorder L"  ballarin@65099  710  by (metis dual_weak_lattice)  ballarin@27713  711 ballarin@65099  712  show ?thesis  ballarin@65099  713  apply (unfold_locales)  ballarin@65099  714  apply (simp_all add: inf_of_two_exists sup_of_two_exists)  ballarin@65099  715  apply (simp add:eq_is_equal)  ballarin@65099  716  done  ballarin@65099  717 qed  ballarin@65099  718   ballarin@65099  719 lemma (in lattice) le_iff_join:  ballarin@65099  720  assumes "x \ carrier L" "y \ carrier L"  ballarin@65099  721  shows "x \ y \ x = (x \ y)"  ballarin@65099  722  by (simp add: assms(1) assms(2) eq_is_equal weak_le_iff_join)  ballarin@27713  723 ballarin@65099  724 lemma (in lattice) le_iff_meet:  ballarin@65099  725  assumes "x \ carrier L" "y \ carrier L"  ballarin@65099  726  shows "x \ y \ (x \ y) = y"  ballarin@65099  727  by (simp add: assms(1) assms(2) eq_is_equal weak_le_iff_meet)  ballarin@27713  728 ballarin@65099  729 text \ Total orders are lattices. \  ballarin@27713  730 ballarin@65099  731 sublocale total_order \ weak?: lattice  ballarin@65099  732  by standard (auto intro: weak.weak.sup_of_two_exists weak.weak.inf_of_two_exists)  ballarin@65099  733   ballarin@65099  734 text \Functions that preserve joins and meets\  ballarin@65099  735   ballarin@65099  736 definition join_pres :: "('a, 'c) gorder_scheme \ ('b, 'd) gorder_scheme \ ('a \ 'b) \ bool" where  ballarin@65099  737 "join_pres X Y f \ lattice X \ lattice Y \ (\ x \ carrier X. \ y \ carrier X. f (x \\<^bsub>X\<^esub> y) = f x \\<^bsub>Y\<^esub> f y)"  ballarin@27713  738 ballarin@65099  739 definition meet_pres :: "('a, 'c) gorder_scheme \ ('b, 'd) gorder_scheme \ ('a \ 'b) \ bool" where  ballarin@65099  740 "meet_pres X Y f \ lattice X \ lattice Y \ (\ x \ carrier X. \ y \ carrier X. f (x \\<^bsub>X\<^esub> y) = f x \\<^bsub>Y\<^esub> f y)"  ballarin@27713  741 ballarin@65099  742 lemma join_pres_isotone:  ballarin@65099  743  assumes "f \ carrier X \ carrier Y" "join_pres X Y f"  ballarin@65099  744  shows "isotone X Y f"  ballarin@65099  745  using assms  ballarin@65099  746  apply (rule_tac isotoneI)  ballarin@65099  747  apply (auto simp add: join_pres_def lattice.le_iff_meet funcset_carrier)  ballarin@65099  748  using lattice_def partial_order_def upper_semilattice_def apply blast  ballarin@65099  749  using lattice_def partial_order_def upper_semilattice_def apply blast  ballarin@65099  750  apply fastforce  ballarin@65099  751 done  ballarin@27713  752 ballarin@65099  753 lemma meet_pres_isotone:  ballarin@65099  754  assumes "f \ carrier X \ carrier Y" "meet_pres X Y f"  ballarin@65099  755  shows "isotone X Y f"  ballarin@65099  756  using assms  ballarin@65099  757  apply (rule_tac isotoneI)  ballarin@65099  758  apply (auto simp add: meet_pres_def lattice.le_iff_join funcset_carrier)  ballarin@65099  759  using lattice_def partial_order_def upper_semilattice_def apply blast  ballarin@65099  760  using lattice_def partial_order_def upper_semilattice_def apply blast  ballarin@65099  761  apply fastforce  ballarin@65099  762 done  ballarin@27713  763 ballarin@27713  764 ballarin@65099  765 subsection \Bounded Lattices\  ballarin@27713  766 ballarin@65099  767 locale bounded_lattice =  ballarin@65099  768  lattice +  ballarin@65099  769  weak_partial_order_bottom +  ballarin@65099  770  weak_partial_order_top  ballarin@27713  771 ballarin@65099  772 sublocale bounded_lattice \ weak_bounded_lattice ..  ballarin@27713  773 ballarin@65099  774 context bounded_lattice  ballarin@65099  775 begin  ballarin@14551  776 ballarin@65099  777 lemma bottom_eq:  ballarin@65099  778  "\ b \ carrier L; \ x. x \ carrier L \ b \ x \ \ b = \"  ballarin@65099  779  by (metis bottom_closed bottom_lower le_antisym)  ballarin@14551  780 ballarin@65099  781 lemma top_eq: "\ t \ carrier L; \ x. x \ carrier L \ x \ t \ \ t = \"  ballarin@65099  782  by (metis le_antisym top_closed top_higher)  ballarin@14551  783 wenzelm@14693  784 end  ballarin@65099  785 ballarin@65099  786 end