src/HOL/Lattice/CompleteLattice.thy
 author wenzelm Thu Oct 04 20:29:42 2007 +0200 (2007-10-04) changeset 24850 0cfd722ab579 parent 23373 ead82c82da9e child 25469 f81b3be9dfdd permissions -rw-r--r--
Name.uu, Name.aT;
     1 (*  Title:      HOL/Lattice/CompleteLattice.thy

     2     ID:         $Id$

     3     Author:     Markus Wenzel, TU Muenchen

     4 *)

     5

     6 header {* Complete lattices *}

     7

     8 theory CompleteLattice imports Lattice begin

     9

    10 subsection {* Complete lattice operations *}

    11

    12 text {*

    13   A \emph{complete lattice} is a partial order with general

    14   (infinitary) infimum of any set of elements.  General supremum

    15   exists as well, as a consequence of the connection of infinitary

    16   bounds (see \S\ref{sec:connect-bounds}).

    17 *}

    18

    19 axclass complete_lattice \<subseteq> partial_order

    20   ex_Inf: "\<exists>inf. is_Inf A inf"

    21

    22 theorem ex_Sup: "\<exists>sup::'a::complete_lattice. is_Sup A sup"

    23 proof -

    24   from ex_Inf obtain sup where "is_Inf {b. \<forall>a\<in>A. a \<sqsubseteq> b} sup" by blast

    25   then have "is_Sup A sup" by (rule Inf_Sup)

    26   then show ?thesis ..

    27 qed

    28

    29 text {*

    30   The general @{text \<Sqinter>} (meet) and @{text \<Squnion>} (join) operations select

    31   such infimum and supremum elements.

    32 *}

    33

    34 definition

    35   Meet :: "'a::complete_lattice set \<Rightarrow> 'a" where

    36   "Meet A = (THE inf. is_Inf A inf)"

    37 definition

    38   Join :: "'a::complete_lattice set \<Rightarrow> 'a" where

    39   "Join A = (THE sup. is_Sup A sup)"

    40

    41 notation (xsymbols)

    42   Meet  ("\<Sqinter>_"  90) and

    43   Join  ("\<Squnion>_"  90)

    44

    45 text {*

    46   Due to unique existence of bounds, the complete lattice operations

    47   may be exhibited as follows.

    48 *}

    49

    50 lemma Meet_equality [elim?]: "is_Inf A inf \<Longrightarrow> \<Sqinter>A = inf"

    51 proof (unfold Meet_def)

    52   assume "is_Inf A inf"

    53   then show "(THE inf. is_Inf A inf) = inf"

    54     by (rule the_equality) (rule is_Inf_uniq [OF _ is_Inf A inf])

    55 qed

    56

    57 lemma MeetI [intro?]:

    58   "(\<And>a. a \<in> A \<Longrightarrow> inf \<sqsubseteq> a) \<Longrightarrow>

    59     (\<And>b. \<forall>a \<in> A. b \<sqsubseteq> a \<Longrightarrow> b \<sqsubseteq> inf) \<Longrightarrow>

    60     \<Sqinter>A = inf"

    61   by (rule Meet_equality, rule is_InfI) blast+

    62

    63 lemma Join_equality [elim?]: "is_Sup A sup \<Longrightarrow> \<Squnion>A = sup"

    64 proof (unfold Join_def)

    65   assume "is_Sup A sup"

    66   then show "(THE sup. is_Sup A sup) = sup"

    67     by (rule the_equality) (rule is_Sup_uniq [OF _ is_Sup A sup])

    68 qed

    69

    70 lemma JoinI [intro?]:

    71   "(\<And>a. a \<in> A \<Longrightarrow> a \<sqsubseteq> sup) \<Longrightarrow>

    72     (\<And>b. \<forall>a \<in> A. a \<sqsubseteq> b \<Longrightarrow> sup \<sqsubseteq> b) \<Longrightarrow>

    73     \<Squnion>A = sup"

    74   by (rule Join_equality, rule is_SupI) blast+

    75

    76

    77 text {*

    78   \medskip The @{text \<Sqinter>} and @{text \<Squnion>} operations indeed determine

    79   bounds on a complete lattice structure.

    80 *}

    81

    82 lemma is_Inf_Meet [intro?]: "is_Inf A (\<Sqinter>A)"

    83 proof (unfold Meet_def)

    84   from ex_Inf obtain inf where "is_Inf A inf" ..

    85   then show "is_Inf A (THE inf. is_Inf A inf)"

    86     by (rule theI) (rule is_Inf_uniq [OF _ is_Inf A inf])

    87 qed

    88

    89 lemma Meet_greatest [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> x \<sqsubseteq> a) \<Longrightarrow> x \<sqsubseteq> \<Sqinter>A"

    90   by (rule is_Inf_greatest, rule is_Inf_Meet) blast

    91

    92 lemma Meet_lower [intro?]: "a \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> a"

    93   by (rule is_Inf_lower) (rule is_Inf_Meet)

    94

    95

    96 lemma is_Sup_Join [intro?]: "is_Sup A (\<Squnion>A)"

    97 proof (unfold Join_def)

    98   from ex_Sup obtain sup where "is_Sup A sup" ..

    99   then show "is_Sup A (THE sup. is_Sup A sup)"

   100     by (rule theI) (rule is_Sup_uniq [OF _ is_Sup A sup])

   101 qed

   102

   103 lemma Join_least [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> a \<sqsubseteq> x) \<Longrightarrow> \<Squnion>A \<sqsubseteq> x"

   104   by (rule is_Sup_least, rule is_Sup_Join) blast

   105 lemma Join_lower [intro?]: "a \<in> A \<Longrightarrow> a \<sqsubseteq> \<Squnion>A"

   106   by (rule is_Sup_upper) (rule is_Sup_Join)

   107

   108

   109 subsection {* The Knaster-Tarski Theorem *}

   110

   111 text {*

   112   The Knaster-Tarski Theorem (in its simplest formulation) states that

   113   any monotone function on a complete lattice has a least fixed-point

   114   (see \cite[pages 93--94]{Davey-Priestley:1990} for example).  This

   115   is a consequence of the basic boundary properties of the complete

   116   lattice operations.

   117 *}

   118

   119 theorem Knaster_Tarski:

   120   "(\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y) \<Longrightarrow> \<exists>a::'a::complete_lattice. f a = a"

   121 proof

   122   assume mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"

   123   let ?H = "{u. f u \<sqsubseteq> u}" let ?a = "\<Sqinter>?H"

   124   have ge: "f ?a \<sqsubseteq> ?a"

   125   proof

   126     fix x assume x: "x \<in> ?H"

   127     then have "?a \<sqsubseteq> x" ..

   128     then have "f ?a \<sqsubseteq> f x" by (rule mono)

   129     also from x have "... \<sqsubseteq> x" ..

   130     finally show "f ?a \<sqsubseteq> x" .

   131   qed

   132   also have "?a \<sqsubseteq> f ?a"

   133   proof

   134     from ge have "f (f ?a) \<sqsubseteq> f ?a" by (rule mono)

   135     then show "f ?a \<in> ?H" ..

   136   qed

   137   finally show "f ?a = ?a" .

   138 qed

   139

   140

   141 subsection {* Bottom and top elements *}

   142

   143 text {*

   144   With general bounds available, complete lattices also have least and

   145   greatest elements.

   146 *}

   147

   148 definition

   149   bottom :: "'a::complete_lattice"    ("\<bottom>") where

   150   "\<bottom> = \<Sqinter>UNIV"

   151 definition

   152   top :: "'a::complete_lattice"    ("\<top>") where

   153   "\<top> = \<Squnion>UNIV"

   154

   155 lemma bottom_least [intro?]: "\<bottom> \<sqsubseteq> x"

   156 proof (unfold bottom_def)

   157   have "x \<in> UNIV" ..

   158   then show "\<Sqinter>UNIV \<sqsubseteq> x" ..

   159 qed

   160

   161 lemma bottomI [intro?]: "(\<And>a. x \<sqsubseteq> a) \<Longrightarrow> \<bottom> = x"

   162 proof (unfold bottom_def)

   163   assume "\<And>a. x \<sqsubseteq> a"

   164   show "\<Sqinter>UNIV = x"

   165   proof

   166     fix a show "x \<sqsubseteq> a" by fact

   167   next

   168     fix b :: "'a::complete_lattice"

   169     assume b: "\<forall>a \<in> UNIV. b \<sqsubseteq> a"

   170     have "x \<in> UNIV" ..

   171     with b show "b \<sqsubseteq> x" ..

   172   qed

   173 qed

   174

   175 lemma top_greatest [intro?]: "x \<sqsubseteq> \<top>"

   176 proof (unfold top_def)

   177   have "x \<in> UNIV" ..

   178   then show "x \<sqsubseteq> \<Squnion>UNIV" ..

   179 qed

   180

   181 lemma topI [intro?]: "(\<And>a. a \<sqsubseteq> x) \<Longrightarrow> \<top> = x"

   182 proof (unfold top_def)

   183   assume "\<And>a. a \<sqsubseteq> x"

   184   show "\<Squnion>UNIV = x"

   185   proof

   186     fix a show "a \<sqsubseteq> x" by fact

   187   next

   188     fix b :: "'a::complete_lattice"

   189     assume b: "\<forall>a \<in> UNIV. a \<sqsubseteq> b"

   190     have "x \<in> UNIV" ..

   191     with b show "x \<sqsubseteq> b" ..

   192   qed

   193 qed

   194

   195

   196 subsection {* Duality *}

   197

   198 text {*

   199   The class of complete lattices is closed under formation of dual

   200   structures.

   201 *}

   202

   203 instance dual :: (complete_lattice) complete_lattice

   204 proof

   205   fix A' :: "'a::complete_lattice dual set"

   206   show "\<exists>inf'. is_Inf A' inf'"

   207   proof -

   208     have "\<exists>sup. is_Sup (undual  A') sup" by (rule ex_Sup)

   209     then have "\<exists>sup. is_Inf (dual  undual  A') (dual sup)" by (simp only: dual_Inf)

   210     then show ?thesis by (simp add: dual_ex [symmetric] image_compose [symmetric])

   211   qed

   212 qed

   213

   214 text {*

   215   Apparently, the @{text \<Sqinter>} and @{text \<Squnion>} operations are dual to each

   216   other.

   217 *}

   218

   219 theorem dual_Meet [intro?]: "dual (\<Sqinter>A) = \<Squnion>(dual  A)"

   220 proof -

   221   from is_Inf_Meet have "is_Sup (dual  A) (dual (\<Sqinter>A))" ..

   222   then have "\<Squnion>(dual  A) = dual (\<Sqinter>A)" ..

   223   then show ?thesis ..

   224 qed

   225

   226 theorem dual_Join [intro?]: "dual (\<Squnion>A) = \<Sqinter>(dual  A)"

   227 proof -

   228   from is_Sup_Join have "is_Inf (dual  A) (dual (\<Squnion>A))" ..

   229   then have "\<Sqinter>(dual  A) = dual (\<Squnion>A)" ..

   230   then show ?thesis ..

   231 qed

   232

   233 text {*

   234   Likewise are @{text \<bottom>} and @{text \<top>} duals of each other.

   235 *}

   236

   237 theorem dual_bottom [intro?]: "dual \<bottom> = \<top>"

   238 proof -

   239   have "\<top> = dual \<bottom>"

   240   proof

   241     fix a' have "\<bottom> \<sqsubseteq> undual a'" ..

   242     then have "dual (undual a') \<sqsubseteq> dual \<bottom>" ..

   243     then show "a' \<sqsubseteq> dual \<bottom>" by simp

   244   qed

   245   then show ?thesis ..

   246 qed

   247

   248 theorem dual_top [intro?]: "dual \<top> = \<bottom>"

   249 proof -

   250   have "\<bottom> = dual \<top>"

   251   proof

   252     fix a' have "undual a' \<sqsubseteq> \<top>" ..

   253     then have "dual \<top> \<sqsubseteq> dual (undual a')" ..

   254     then show "dual \<top> \<sqsubseteq> a'" by simp

   255   qed

   256   then show ?thesis ..

   257 qed

   258

   259

   260 subsection {* Complete lattices are lattices *}

   261

   262 text {*

   263   Complete lattices (with general bounds available) are indeed plain

   264   lattices as well.  This holds due to the connection of general

   265   versus binary bounds that has been formally established in

   266   \S\ref{sec:gen-bin-bounds}.

   267 *}

   268

   269 lemma is_inf_binary: "is_inf x y (\<Sqinter>{x, y})"

   270 proof -

   271   have "is_Inf {x, y} (\<Sqinter>{x, y})" ..

   272   then show ?thesis by (simp only: is_Inf_binary)

   273 qed

   274

   275 lemma is_sup_binary: "is_sup x y (\<Squnion>{x, y})"

   276 proof -

   277   have "is_Sup {x, y} (\<Squnion>{x, y})" ..

   278   then show ?thesis by (simp only: is_Sup_binary)

   279 qed

   280

   281 instance complete_lattice \<subseteq> lattice

   282 proof

   283   fix x y :: "'a::complete_lattice"

   284   from is_inf_binary show "\<exists>inf. is_inf x y inf" ..

   285   from is_sup_binary show "\<exists>sup. is_sup x y sup" ..

   286 qed

   287

   288 theorem meet_binary: "x \<sqinter> y = \<Sqinter>{x, y}"

   289   by (rule meet_equality) (rule is_inf_binary)

   290

   291 theorem join_binary: "x \<squnion> y = \<Squnion>{x, y}"

   292   by (rule join_equality) (rule is_sup_binary)

   293

   294

   295 subsection {* Complete lattices and set-theory operations *}

   296

   297 text {*

   298   The complete lattice operations are (anti) monotone wrt.\ set

   299   inclusion.

   300 *}

   301

   302 theorem Meet_subset_antimono: "A \<subseteq> B \<Longrightarrow> \<Sqinter>B \<sqsubseteq> \<Sqinter>A"

   303 proof (rule Meet_greatest)

   304   fix a assume "a \<in> A"

   305   also assume "A \<subseteq> B"

   306   finally have "a \<in> B" .

   307   then show "\<Sqinter>B \<sqsubseteq> a" ..

   308 qed

   309

   310 theorem Join_subset_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<sqsubseteq> \<Squnion>B"

   311 proof -

   312   assume "A \<subseteq> B"

   313   then have "dual  A \<subseteq> dual  B" by blast

   314   then have "\<Sqinter>(dual  B) \<sqsubseteq> \<Sqinter>(dual  A)" by (rule Meet_subset_antimono)

   315   then have "dual (\<Squnion>B) \<sqsubseteq> dual (\<Squnion>A)" by (simp only: dual_Join)

   316   then show ?thesis by (simp only: dual_leq)

   317 qed

   318

   319 text {*

   320   Bounds over unions of sets may be obtained separately.

   321 *}

   322

   323 theorem Meet_Un: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"

   324 proof

   325   fix a assume "a \<in> A \<union> B"

   326   then show "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> a"

   327   proof

   328     assume a: "a \<in> A"

   329     have "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> \<Sqinter>A" ..

   330     also from a have "\<dots> \<sqsubseteq> a" ..

   331     finally show ?thesis .

   332   next

   333     assume a: "a \<in> B"

   334     have "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> \<Sqinter>B" ..

   335     also from a have "\<dots> \<sqsubseteq> a" ..

   336     finally show ?thesis .

   337   qed

   338 next

   339   fix b assume b: "\<forall>a \<in> A \<union> B. b \<sqsubseteq> a"

   340   show "b \<sqsubseteq> \<Sqinter>A \<sqinter> \<Sqinter>B"

   341   proof

   342     show "b \<sqsubseteq> \<Sqinter>A"

   343     proof

   344       fix a assume "a \<in> A"

   345       then have "a \<in>  A \<union> B" ..

   346       with b show "b \<sqsubseteq> a" ..

   347     qed

   348     show "b \<sqsubseteq> \<Sqinter>B"

   349     proof

   350       fix a assume "a \<in> B"

   351       then have "a \<in>  A \<union> B" ..

   352       with b show "b \<sqsubseteq> a" ..

   353     qed

   354   qed

   355 qed

   356

   357 theorem Join_Un: "\<Squnion>(A \<union> B) = \<Squnion>A \<squnion> \<Squnion>B"

   358 proof -

   359   have "dual (\<Squnion>(A \<union> B)) = \<Sqinter>(dual  A \<union> dual  B)"

   360     by (simp only: dual_Join image_Un)

   361   also have "\<dots> = \<Sqinter>(dual  A) \<sqinter> \<Sqinter>(dual  B)"

   362     by (rule Meet_Un)

   363   also have "\<dots> = dual (\<Squnion>A \<squnion> \<Squnion>B)"

   364     by (simp only: dual_join dual_Join)

   365   finally show ?thesis ..

   366 qed

   367

   368 text {*

   369   Bounds over singleton sets are trivial.

   370 *}

   371

   372 theorem Meet_singleton: "\<Sqinter>{x} = x"

   373 proof

   374   fix a assume "a \<in> {x}"

   375   then have "a = x" by simp

   376   then show "x \<sqsubseteq> a" by (simp only: leq_refl)

   377 next

   378   fix b assume "\<forall>a \<in> {x}. b \<sqsubseteq> a"

   379   then show "b \<sqsubseteq> x" by simp

   380 qed

   381

   382 theorem Join_singleton: "\<Squnion>{x} = x"

   383 proof -

   384   have "dual (\<Squnion>{x}) = \<Sqinter>{dual x}" by (simp add: dual_Join)

   385   also have "\<dots> = dual x" by (rule Meet_singleton)

   386   finally show ?thesis ..

   387 qed

   388

   389 text {*

   390   Bounds over the empty and universal set correspond to each other.

   391 *}

   392

   393 theorem Meet_empty: "\<Sqinter>{} = \<Squnion>UNIV"

   394 proof

   395   fix a :: "'a::complete_lattice"

   396   assume "a \<in> {}"

   397   then have False by simp

   398   then show "\<Squnion>UNIV \<sqsubseteq> a" ..

   399 next

   400   fix b :: "'a::complete_lattice"

   401   have "b \<in> UNIV" ..

   402   then show "b \<sqsubseteq> \<Squnion>UNIV" ..

   403 qed

   404

   405 theorem Join_empty: "\<Squnion>{} = \<Sqinter>UNIV"

   406 proof -

   407   have "dual (\<Squnion>{}) = \<Sqinter>{}" by (simp add: dual_Join)

   408   also have "\<dots> = \<Squnion>UNIV" by (rule Meet_empty)

   409   also have "\<dots> = dual (\<Sqinter>UNIV)" by (simp add: dual_Meet)

   410   finally show ?thesis ..

   411 qed

   412

   413 end
`