src/HOL/Lattice/CompleteLattice.thy
 author nipkow Thu Dec 11 08:52:50 2008 +0100 (2008-12-11) changeset 29106 25e28a4070f3 parent 25474 c41b433b0f65 child 35317 d57da4abb47d permissions -rw-r--r--
Testfile for Stefan's code generator
 wenzelm@10157  1 (* Title: HOL/Lattice/CompleteLattice.thy  wenzelm@10157  2  ID: $Id$  wenzelm@10157  3  Author: Markus Wenzel, TU Muenchen  wenzelm@10157  4 *)  wenzelm@10157  5 wenzelm@10157  6 header {* Complete lattices *}  wenzelm@10157  7 haftmann@16417  8 theory CompleteLattice imports Lattice begin  wenzelm@10157  9 wenzelm@10157  10 subsection {* Complete lattice operations *}  wenzelm@10157  11 wenzelm@10157  12 text {*  wenzelm@10157  13  A \emph{complete lattice} is a partial order with general  wenzelm@10157  14  (infinitary) infimum of any set of elements. General supremum  wenzelm@10157  15  exists as well, as a consequence of the connection of infinitary  wenzelm@10157  16  bounds (see \S\ref{sec:connect-bounds}).  wenzelm@10157  17 *}  wenzelm@10157  18 wenzelm@11099  19 axclass complete_lattice \ partial_order  wenzelm@10157  20  ex_Inf: "\inf. is_Inf A inf"  wenzelm@10157  21 wenzelm@10157  22 theorem ex_Sup: "\sup::'a::complete_lattice. is_Sup A sup"  wenzelm@10157  23 proof -  wenzelm@10157  24  from ex_Inf obtain sup where "is_Inf {b. \a\A. a \ b} sup" by blast  wenzelm@23373  25  then have "is_Sup A sup" by (rule Inf_Sup)  wenzelm@23373  26  then show ?thesis ..  wenzelm@10157  27 qed  wenzelm@10157  28 wenzelm@10157  29 text {*  wenzelm@10157  30  The general @{text \} (meet) and @{text \} (join) operations select  wenzelm@10157  31  such infimum and supremum elements.  wenzelm@10157  32 *}  wenzelm@10157  33 wenzelm@19736  34 definition  wenzelm@21404  35  Meet :: "'a::complete_lattice set \ 'a" where  wenzelm@19736  36  "Meet A = (THE inf. is_Inf A inf)"  wenzelm@21404  37 definition  wenzelm@21404  38  Join :: "'a::complete_lattice set \ 'a" where  wenzelm@19736  39  "Join A = (THE sup. is_Sup A sup)"  wenzelm@19736  40 wenzelm@21210  41 notation (xsymbols)  wenzelm@21404  42  Meet ("\_" [90] 90) and  wenzelm@19736  43  Join ("\_" [90] 90)  wenzelm@10157  44 wenzelm@10157  45 text {*  wenzelm@10157  46  Due to unique existence of bounds, the complete lattice operations  wenzelm@10157  47  may be exhibited as follows.  wenzelm@10157  48 *}  wenzelm@10157  49 wenzelm@10157  50 lemma Meet_equality [elim?]: "is_Inf A inf \ \A = inf"  wenzelm@10157  51 proof (unfold Meet_def)  wenzelm@10157  52  assume "is_Inf A inf"  wenzelm@23373  53  then show "(THE inf. is_Inf A inf) = inf"  wenzelm@23373  54  by (rule the_equality) (rule is_Inf_uniq [OF _ is_Inf A inf])  wenzelm@10157  55 qed  wenzelm@10157  56 wenzelm@10157  57 lemma MeetI [intro?]:  wenzelm@10157  58  "(\a. a \ A \ inf \ a) \  wenzelm@10157  59  (\b. \a \ A. b \ a \ b \ inf) \  wenzelm@10157  60  \A = inf"  wenzelm@10157  61  by (rule Meet_equality, rule is_InfI) blast+  wenzelm@10157  62 wenzelm@10157  63 lemma Join_equality [elim?]: "is_Sup A sup \ \A = sup"  wenzelm@10157  64 proof (unfold Join_def)  wenzelm@10157  65  assume "is_Sup A sup"  wenzelm@23373  66  then show "(THE sup. is_Sup A sup) = sup"  wenzelm@23373  67  by (rule the_equality) (rule is_Sup_uniq [OF _ is_Sup A sup])  wenzelm@10157  68 qed  wenzelm@10157  69 wenzelm@10157  70 lemma JoinI [intro?]:  wenzelm@10157  71  "(\a. a \ A \ a \ sup) \  wenzelm@10157  72  (\b. \a \ A. a \ b \ sup \ b) \  wenzelm@10157  73  \A = sup"  wenzelm@10157  74  by (rule Join_equality, rule is_SupI) blast+  wenzelm@10157  75 wenzelm@10157  76 wenzelm@10157  77 text {*  wenzelm@10157  78  \medskip The @{text \} and @{text \} operations indeed determine  wenzelm@10157  79  bounds on a complete lattice structure.  wenzelm@10157  80 *}  wenzelm@10157  81 wenzelm@10157  82 lemma is_Inf_Meet [intro?]: "is_Inf A (\A)"  wenzelm@10157  83 proof (unfold Meet_def)  wenzelm@11441  84  from ex_Inf obtain inf where "is_Inf A inf" ..  wenzelm@23373  85  then show "is_Inf A (THE inf. is_Inf A inf)"  wenzelm@23373  86  by (rule theI) (rule is_Inf_uniq [OF _ is_Inf A inf])  wenzelm@10157  87 qed  wenzelm@10157  88 wenzelm@10157  89 lemma Meet_greatest [intro?]: "(\a. a \ A \ x \ a) \ x \ \A"  wenzelm@10157  90  by (rule is_Inf_greatest, rule is_Inf_Meet) blast  wenzelm@10157  91 wenzelm@10157  92 lemma Meet_lower [intro?]: "a \ A \ \A \ a"  wenzelm@10157  93  by (rule is_Inf_lower) (rule is_Inf_Meet)  wenzelm@10157  94 wenzelm@10157  95 wenzelm@10157  96 lemma is_Sup_Join [intro?]: "is_Sup A (\A)"  wenzelm@10157  97 proof (unfold Join_def)  wenzelm@11441  98  from ex_Sup obtain sup where "is_Sup A sup" ..  wenzelm@23373  99  then show "is_Sup A (THE sup. is_Sup A sup)"  wenzelm@23373  100  by (rule theI) (rule is_Sup_uniq [OF _ is_Sup A sup])  wenzelm@10157  101 qed  wenzelm@10157  102 wenzelm@10157  103 lemma Join_least [intro?]: "(\a. a \ A \ a \ x) \ \A \ x"  wenzelm@10157  104  by (rule is_Sup_least, rule is_Sup_Join) blast  wenzelm@10157  105 lemma Join_lower [intro?]: "a \ A \ a \ \A"  wenzelm@10157  106  by (rule is_Sup_upper) (rule is_Sup_Join)  wenzelm@10157  107 wenzelm@10157  108 wenzelm@10157  109 subsection {* The Knaster-Tarski Theorem *}  wenzelm@10157  110 wenzelm@10157  111 text {*  wenzelm@10157  112  The Knaster-Tarski Theorem (in its simplest formulation) states that  wenzelm@10157  113  any monotone function on a complete lattice has a least fixed-point  wenzelm@10157  114  (see \cite[pages 93--94]{Davey-Priestley:1990} for example). This  wenzelm@10157  115  is a consequence of the basic boundary properties of the complete  wenzelm@10157  116  lattice operations.  wenzelm@10157  117 *}  wenzelm@10157  118 wenzelm@10157  119 theorem Knaster_Tarski:  wenzelm@25469  120  assumes mono: "\x y. x \ y \ f x \ f y"  wenzelm@25474  121  obtains a :: "'a::complete_lattice" where  wenzelm@25474  122  "f a = a" and "\a'. f a' = a' \ a \ a'"  wenzelm@25474  123 proof  wenzelm@25469  124  let ?H = "{u. f u \ u}"  wenzelm@25469  125  let ?a = "\?H"  wenzelm@25474  126  show "f ?a = ?a"  wenzelm@25469  127  proof -  wenzelm@25469  128  have ge: "f ?a \ ?a"  wenzelm@25469  129  proof  wenzelm@25469  130  fix x assume x: "x \ ?H"  wenzelm@25469  131  then have "?a \ x" ..  wenzelm@25469  132  then have "f ?a \ f x" by (rule mono)  wenzelm@25469  133  also from x have "... \ x" ..  wenzelm@25469  134  finally show "f ?a \ x" .  wenzelm@25469  135  qed  wenzelm@25469  136  also have "?a \ f ?a"  wenzelm@25469  137  proof  wenzelm@25469  138  from ge have "f (f ?a) \ f ?a" by (rule mono)  wenzelm@25469  139  then show "f ?a \ ?H" ..  wenzelm@25469  140  qed  wenzelm@25469  141  finally show ?thesis .  wenzelm@10157  142  qed  wenzelm@25474  143 wenzelm@25474  144  fix a'  wenzelm@25474  145  assume "f a' = a'"  wenzelm@25474  146  then have "f a' \ a'" by (simp only: leq_refl)  wenzelm@25474  147  then have "a' \ ?H" ..  wenzelm@25474  148  then show "?a \ a'" ..  wenzelm@25469  149 qed  wenzelm@25469  150 wenzelm@25469  151 theorem Knaster_Tarski_dual:  wenzelm@25469  152  assumes mono: "\x y. x \ y \ f x \ f y"  wenzelm@25474  153  obtains a :: "'a::complete_lattice" where  wenzelm@25474  154  "f a = a" and "\a'. f a' = a' \ a' \ a"  wenzelm@25474  155 proof  wenzelm@25469  156  let ?H = "{u. u \ f u}"  wenzelm@25469  157  let ?a = "\?H"  wenzelm@25474  158  show "f ?a = ?a"  wenzelm@25469  159  proof -  wenzelm@25469  160  have le: "?a \ f ?a"  wenzelm@25469  161  proof  wenzelm@25469  162  fix x assume x: "x \ ?H"  wenzelm@25469  163  then have "x \ f x" ..  wenzelm@25469  164  also from x have "x \ ?a" ..  wenzelm@25469  165  then have "f x \ f ?a" by (rule mono)  wenzelm@25469  166  finally show "x \ f ?a" .  wenzelm@25469  167  qed  wenzelm@25469  168  have "f ?a \ ?a"  wenzelm@25469  169  proof  wenzelm@25469  170  from le have "f ?a \ f (f ?a)" by (rule mono)  wenzelm@25469  171  then show "f ?a \ ?H" ..  wenzelm@25469  172  qed  wenzelm@25469  173  from this and le show ?thesis by (rule leq_antisym)  wenzelm@10157  174  qed  wenzelm@25474  175 wenzelm@25474  176  fix a'  wenzelm@25474  177  assume "f a' = a'"  wenzelm@25474  178  then have "a' \ f a'" by (simp only: leq_refl)  wenzelm@25474  179  then have "a' \ ?H" ..  wenzelm@25474  180  then show "a' \ ?a" ..  wenzelm@10157  181 qed  wenzelm@10157  182 wenzelm@10157  183 wenzelm@10157  184 subsection {* Bottom and top elements *}  wenzelm@10157  185 wenzelm@10157  186 text {*  wenzelm@10157  187  With general bounds available, complete lattices also have least and  wenzelm@10157  188  greatest elements.  wenzelm@10157  189 *}  wenzelm@10157  190 wenzelm@19736  191 definition  wenzelm@25469  192  bottom :: "'a::complete_lattice" ("\") where  wenzelm@19736  193  "\ = \UNIV"  wenzelm@25469  194 wenzelm@21404  195 definition  wenzelm@25469  196  top :: "'a::complete_lattice" ("\") where  wenzelm@19736  197  "\ = \UNIV"  wenzelm@10157  198 wenzelm@10157  199 lemma bottom_least [intro?]: "\ \ x"  wenzelm@10157  200 proof (unfold bottom_def)  wenzelm@10157  201  have "x \ UNIV" ..  wenzelm@23373  202  then show "\UNIV \ x" ..  wenzelm@10157  203 qed  wenzelm@10157  204 wenzelm@10157  205 lemma bottomI [intro?]: "(\a. x \ a) \ \ = x"  wenzelm@10157  206 proof (unfold bottom_def)  wenzelm@10157  207  assume "\a. x \ a"  wenzelm@10157  208  show "\UNIV = x"  wenzelm@10157  209  proof  wenzelm@23373  210  fix a show "x \ a" by fact  wenzelm@10157  211  next  wenzelm@10157  212  fix b :: "'a::complete_lattice"  wenzelm@10157  213  assume b: "\a \ UNIV. b \ a"  wenzelm@10157  214  have "x \ UNIV" ..  wenzelm@10157  215  with b show "b \ x" ..  wenzelm@10157  216  qed  wenzelm@10157  217 qed  wenzelm@10157  218 wenzelm@10157  219 lemma top_greatest [intro?]: "x \ \"  wenzelm@10157  220 proof (unfold top_def)  wenzelm@10157  221  have "x \ UNIV" ..  wenzelm@23373  222  then show "x \ \UNIV" ..  wenzelm@10157  223 qed  wenzelm@10157  224 wenzelm@10157  225 lemma topI [intro?]: "(\a. a \ x) \ \ = x"  wenzelm@10157  226 proof (unfold top_def)  wenzelm@10157  227  assume "\a. a \ x"  wenzelm@10157  228  show "\UNIV = x"  wenzelm@10157  229  proof  wenzelm@23373  230  fix a show "a \ x" by fact  wenzelm@10157  231  next  wenzelm@10157  232  fix b :: "'a::complete_lattice"  wenzelm@10157  233  assume b: "\a \ UNIV. a \ b"  wenzelm@10157  234  have "x \ UNIV" ..  wenzelm@10157  235  with b show "x \ b" ..  wenzelm@10157  236  qed  wenzelm@10157  237 qed  wenzelm@10157  238 wenzelm@10157  239 wenzelm@10157  240 subsection {* Duality *}  wenzelm@10157  241 wenzelm@10157  242 text {*  wenzelm@10157  243  The class of complete lattices is closed under formation of dual  wenzelm@10157  244  structures.  wenzelm@10157  245 *}  wenzelm@10157  246 wenzelm@10157  247 instance dual :: (complete_lattice) complete_lattice  wenzelm@10309  248 proof  wenzelm@10157  249  fix A' :: "'a::complete_lattice dual set"  wenzelm@10157  250  show "\inf'. is_Inf A' inf'"  wenzelm@10157  251  proof -  nipkow@10834  252  have "\sup. is_Sup (undual  A') sup" by (rule ex_Sup)  wenzelm@23373  253  then have "\sup. is_Inf (dual  undual  A') (dual sup)" by (simp only: dual_Inf)  wenzelm@23373  254  then show ?thesis by (simp add: dual_ex [symmetric] image_compose [symmetric])  wenzelm@10157  255  qed  wenzelm@10157  256 qed  wenzelm@10157  257 wenzelm@10157  258 text {*  wenzelm@10157  259  Apparently, the @{text \} and @{text \} operations are dual to each  wenzelm@10157  260  other.  wenzelm@10157  261 *}  wenzelm@10157  262 nipkow@10834  263 theorem dual_Meet [intro?]: "dual (\A) = \(dual  A)"  wenzelm@10157  264 proof -  nipkow@10834  265  from is_Inf_Meet have "is_Sup (dual  A) (dual (\A))" ..  wenzelm@23373  266  then have "\(dual  A) = dual (\A)" ..  wenzelm@23373  267  then show ?thesis ..  wenzelm@10157  268 qed  wenzelm@10157  269 nipkow@10834  270 theorem dual_Join [intro?]: "dual (\A) = \(dual  A)"  wenzelm@10157  271 proof -  nipkow@10834  272  from is_Sup_Join have "is_Inf (dual  A) (dual (\A))" ..  wenzelm@23373  273  then have "\(dual  A) = dual (\A)" ..  wenzelm@23373  274  then show ?thesis ..  wenzelm@10157  275 qed  wenzelm@10157  276 wenzelm@10157  277 text {*  wenzelm@10157  278  Likewise are @{text \} and @{text \} duals of each other.  wenzelm@10157  279 *}  wenzelm@10157  280 wenzelm@10157  281 theorem dual_bottom [intro?]: "dual \ = \"  wenzelm@10157  282 proof -  wenzelm@10157  283  have "\ = dual \"  wenzelm@10157  284  proof  wenzelm@10157  285  fix a' have "\ \ undual a'" ..  wenzelm@23373  286  then have "dual (undual a') \ dual \" ..  wenzelm@23373  287  then show "a' \ dual \" by simp  wenzelm@10157  288  qed  wenzelm@23373  289  then show ?thesis ..  wenzelm@10157  290 qed  wenzelm@10157  291 wenzelm@10157  292 theorem dual_top [intro?]: "dual \ = \"  wenzelm@10157  293 proof -  wenzelm@10157  294  have "\ = dual \"  wenzelm@10157  295  proof  wenzelm@10157  296  fix a' have "undual a' \ \" ..  wenzelm@23373  297  then have "dual \ \ dual (undual a')" ..  wenzelm@23373  298  then show "dual \ \ a'" by simp  wenzelm@10157  299  qed  wenzelm@23373  300  then show ?thesis ..  wenzelm@10157  301 qed  wenzelm@10157  302 wenzelm@10157  303 wenzelm@10157  304 subsection {* Complete lattices are lattices *}  wenzelm@10157  305 wenzelm@10157  306 text {*  wenzelm@10176  307  Complete lattices (with general bounds available) are indeed plain  wenzelm@10157  308  lattices as well. This holds due to the connection of general  wenzelm@10157  309  versus binary bounds that has been formally established in  wenzelm@10157  310  \S\ref{sec:gen-bin-bounds}.  wenzelm@10157  311 *}  wenzelm@10157  312 wenzelm@10157  313 lemma is_inf_binary: "is_inf x y (\{x, y})"  wenzelm@10157  314 proof -  wenzelm@10157  315  have "is_Inf {x, y} (\{x, y})" ..  wenzelm@23373  316  then show ?thesis by (simp only: is_Inf_binary)  wenzelm@10157  317 qed  wenzelm@10157  318 wenzelm@10157  319 lemma is_sup_binary: "is_sup x y (\{x, y})"  wenzelm@10157  320 proof -  wenzelm@10157  321  have "is_Sup {x, y} (\{x, y})" ..  wenzelm@23373  322  then show ?thesis by (simp only: is_Sup_binary)  wenzelm@10157  323 qed  wenzelm@10157  324 wenzelm@11099  325 instance complete_lattice \ lattice  wenzelm@10309  326 proof  wenzelm@10157  327  fix x y :: "'a::complete_lattice"  wenzelm@10157  328  from is_inf_binary show "\inf. is_inf x y inf" ..  wenzelm@10157  329  from is_sup_binary show "\sup. is_sup x y sup" ..  wenzelm@10157  330 qed  wenzelm@10157  331 wenzelm@10157  332 theorem meet_binary: "x \ y = \{x, y}"  wenzelm@10157  333  by (rule meet_equality) (rule is_inf_binary)  wenzelm@10157  334 wenzelm@10157  335 theorem join_binary: "x \ y = \{x, y}"  wenzelm@10157  336  by (rule join_equality) (rule is_sup_binary)  wenzelm@10157  337 wenzelm@10157  338 wenzelm@10157  339 subsection {* Complete lattices and set-theory operations *}  wenzelm@10157  340 wenzelm@10157  341 text {*  wenzelm@10157  342  The complete lattice operations are (anti) monotone wrt.\ set  wenzelm@10157  343  inclusion.  wenzelm@10157  344 *}  wenzelm@10157  345 wenzelm@10157  346 theorem Meet_subset_antimono: "A \ B \ \B \ \A"  wenzelm@10157  347 proof (rule Meet_greatest)  wenzelm@10157  348  fix a assume "a \ A"  wenzelm@10157  349  also assume "A \ B"  wenzelm@10157  350  finally have "a \ B" .  wenzelm@23373  351  then show "\B \ a" ..  wenzelm@10157  352 qed  wenzelm@10157  353 wenzelm@10157  354 theorem Join_subset_mono: "A \ B \ \A \ \B"  wenzelm@10157  355 proof -  wenzelm@10157  356  assume "A \ B"  wenzelm@23373  357  then have "dual  A \ dual  B" by blast  wenzelm@23373  358  then have "\(dual  B) \ \(dual  A)" by (rule Meet_subset_antimono)  wenzelm@23373  359  then have "dual (\B) \ dual (\A)" by (simp only: dual_Join)  wenzelm@23373  360  then show ?thesis by (simp only: dual_leq)  wenzelm@10157  361 qed  wenzelm@10157  362 wenzelm@10157  363 text {*  wenzelm@10157  364  Bounds over unions of sets may be obtained separately.  wenzelm@10157  365 *}  wenzelm@10157  366 wenzelm@10157  367 theorem Meet_Un: "\(A \ B) = \A \ \B"  wenzelm@10157  368 proof  wenzelm@10157  369  fix a assume "a \ A \ B"  wenzelm@23373  370  then show "\A \ \B \ a"  wenzelm@10157  371  proof  wenzelm@10157  372  assume a: "a \ A"  wenzelm@10157  373  have "\A \ \B \ \A" ..  wenzelm@10157  374  also from a have "\ \ a" ..  wenzelm@10157  375  finally show ?thesis .  wenzelm@10157  376  next  wenzelm@10157  377  assume a: "a \ B"  wenzelm@10157  378  have "\A \ \B \ \B" ..  wenzelm@10157  379  also from a have "\ \ a" ..  wenzelm@10157  380  finally show ?thesis .  wenzelm@10157  381  qed  wenzelm@10157  382 next  wenzelm@10157  383  fix b assume b: "\a \ A \ B. b \ a"  wenzelm@10157  384  show "b \ \A \ \B"  wenzelm@10157  385  proof  wenzelm@10157  386  show "b \ \A"  wenzelm@10157  387  proof  wenzelm@10157  388  fix a assume "a \ A"  wenzelm@23373  389  then have "a \ A \ B" ..  wenzelm@10157  390  with b show "b \ a" ..  wenzelm@10157  391  qed  wenzelm@10157  392  show "b \ \B"  wenzelm@10157  393  proof  wenzelm@10157  394  fix a assume "a \ B"  wenzelm@23373  395  then have "a \ A \ B" ..  wenzelm@10157  396  with b show "b \ a" ..  wenzelm@10157  397  qed  wenzelm@10157  398  qed  wenzelm@10157  399 qed  wenzelm@10157  400 wenzelm@10157  401 theorem Join_Un: "\(A \ B) = \A \ \B"  wenzelm@10157  402 proof -  nipkow@10834  403  have "dual (\(A \ B)) = \(dual  A \ dual  B)"  wenzelm@10157  404  by (simp only: dual_Join image_Un)  nipkow@10834  405  also have "\ = \(dual  A) \ \(dual  B)"  wenzelm@10157  406  by (rule Meet_Un)  wenzelm@10157  407  also have "\ = dual (\A \ \B)"  wenzelm@10157  408  by (simp only: dual_join dual_Join)  wenzelm@10157  409  finally show ?thesis ..  wenzelm@10157  410 qed  wenzelm@10157  411 wenzelm@10157  412 text {*  wenzelm@10157  413  Bounds over singleton sets are trivial.  wenzelm@10157  414 *}  wenzelm@10157  415 wenzelm@10157  416 theorem Meet_singleton: "\{x} = x"  wenzelm@10157  417 proof  wenzelm@10157  418  fix a assume "a \ {x}"  wenzelm@23373  419  then have "a = x" by simp  wenzelm@23373  420  then show "x \ a" by (simp only: leq_refl)  wenzelm@10157  421 next  wenzelm@10157  422  fix b assume "\a \ {x}. b \ a"  wenzelm@23373  423  then show "b \ x" by simp  wenzelm@10157  424 qed  wenzelm@10157  425 wenzelm@10157  426 theorem Join_singleton: "\{x} = x"  wenzelm@10157  427 proof -  wenzelm@10157  428  have "dual (\{x}) = \{dual x}" by (simp add: dual_Join)  wenzelm@10157  429  also have "\ = dual x" by (rule Meet_singleton)  wenzelm@10157  430  finally show ?thesis ..  wenzelm@10157  431 qed  wenzelm@10157  432 wenzelm@10157  433 text {*  wenzelm@10157  434  Bounds over the empty and universal set correspond to each other.  wenzelm@10157  435 *}  wenzelm@10157  436 wenzelm@10157  437 theorem Meet_empty: "\{} = \UNIV"  wenzelm@10157  438 proof  wenzelm@10157  439  fix a :: "'a::complete_lattice"  wenzelm@10157  440  assume "a \ {}"  wenzelm@23373  441  then have False by simp  wenzelm@23373  442  then show "\UNIV \ a" ..  wenzelm@10157  443 next  wenzelm@10157  444  fix b :: "'a::complete_lattice"  wenzelm@10157  445  have "b \ UNIV" ..  wenzelm@23373  446  then show "b \ \UNIV" ..  wenzelm@10157  447 qed  wenzelm@10157  448 wenzelm@10157  449 theorem Join_empty: "\{} = \UNIV"  wenzelm@10157  450 proof -  wenzelm@10157  451  have "dual (\{}) = \{}" by (simp add: dual_Join)  wenzelm@10157  452  also have "\ = \UNIV" by (rule Meet_empty)  wenzelm@10157  453  also have "\ = dual (\UNIV)" by (simp add: dual_Meet)  wenzelm@10157  454  finally show ?thesis ..  wenzelm@10157  455 qed  wenzelm@10157  456 wenzelm@10157  457 end `