src/HOL/Lattice/CompleteLattice.thy
 author wenzelm Fri Nov 17 02:20:03 2006 +0100 (2006-11-17) changeset 21404 eb85850d3eb7 parent 21210 c17fd2df4e9e child 23373 ead82c82da9e permissions -rw-r--r--
more robust syntax for definition/abbreviation/notation;
     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   hence "is_Sup A sup" by (rule Inf_Sup)

    26   thus ?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   thus "(THE inf. is_Inf A inf) = inf"

    54     by (rule the_equality) (rule is_Inf_uniq)

    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   thus "(THE sup. is_Sup A sup) = sup"

    67     by (rule the_equality) (rule is_Sup_uniq)

    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   thus "is_Inf A (THE inf. is_Inf A inf)" by (rule theI) (rule is_Inf_uniq)

    86 qed

    87

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

    89   by (rule is_Inf_greatest, rule is_Inf_Meet) blast

    90

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

    92   by (rule is_Inf_lower) (rule is_Inf_Meet)

    93

    94

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

    96 proof (unfold Join_def)

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

    98   thus "is_Sup A (THE sup. is_Sup A sup)" by (rule theI) (rule is_Sup_uniq)

    99 qed

   100

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

   102   by (rule is_Sup_least, rule is_Sup_Join) blast

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

   104   by (rule is_Sup_upper) (rule is_Sup_Join)

   105

   106

   107 subsection {* The Knaster-Tarski Theorem *}

   108

   109 text {*

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

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

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

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

   114   lattice operations.

   115 *}

   116

   117 theorem Knaster_Tarski:

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

   119 proof

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

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

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

   123   proof

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

   125     hence "?a \<sqsubseteq> x" ..

   126     hence "f ?a \<sqsubseteq> f x" by (rule mono)

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

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

   129   qed

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

   131   proof

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

   133     thus "f ?a \<in> ?H" ..

   134   qed

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

   136 qed

   137

   138

   139 subsection {* Bottom and top elements *}

   140

   141 text {*

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

   143   greatest elements.

   144 *}

   145

   146 definition

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

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

   149 definition

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

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

   152

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

   154 proof (unfold bottom_def)

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

   156   thus "\<Sqinter>UNIV \<sqsubseteq> x" ..

   157 qed

   158

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

   160 proof (unfold bottom_def)

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

   162   show "\<Sqinter>UNIV = x"

   163   proof

   164     fix a show "x \<sqsubseteq> a" .

   165   next

   166     fix b :: "'a::complete_lattice"

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

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

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

   170   qed

   171 qed

   172

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

   174 proof (unfold top_def)

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

   176   thus "x \<sqsubseteq> \<Squnion>UNIV" ..

   177 qed

   178

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

   180 proof (unfold top_def)

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

   182   show "\<Squnion>UNIV = x"

   183   proof

   184     fix a show "a \<sqsubseteq> x" .

   185   next

   186     fix b :: "'a::complete_lattice"

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

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

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

   190   qed

   191 qed

   192

   193

   194 subsection {* Duality *}

   195

   196 text {*

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

   198   structures.

   199 *}

   200

   201 instance dual :: (complete_lattice) complete_lattice

   202 proof

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

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

   205   proof -

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

   207     hence "\<exists>sup. is_Inf (dual  undual  A') (dual sup)" by (simp only: dual_Inf)

   208     thus ?thesis by (simp add: dual_ex [symmetric] image_compose [symmetric])

   209   qed

   210 qed

   211

   212 text {*

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

   214   other.

   215 *}

   216

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

   218 proof -

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

   220   hence "\<Squnion>(dual  A) = dual (\<Sqinter>A)" ..

   221   thus ?thesis ..

   222 qed

   223

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

   225 proof -

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

   227   hence "\<Sqinter>(dual  A) = dual (\<Squnion>A)" ..

   228   thus ?thesis ..

   229 qed

   230

   231 text {*

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

   233 *}

   234

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

   236 proof -

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

   238   proof

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

   240     hence "dual (undual a') \<sqsubseteq> dual \<bottom>" ..

   241     thus "a' \<sqsubseteq> dual \<bottom>" by simp

   242   qed

   243   thus ?thesis ..

   244 qed

   245

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

   247 proof -

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

   249   proof

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

   251     hence "dual \<top> \<sqsubseteq> dual (undual a')" ..

   252     thus "dual \<top> \<sqsubseteq> a'" by simp

   253   qed

   254   thus ?thesis ..

   255 qed

   256

   257

   258 subsection {* Complete lattices are lattices *}

   259

   260 text {*

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

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

   263   versus binary bounds that has been formally established in

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

   265 *}

   266

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

   268 proof -

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

   270   thus ?thesis by (simp only: is_Inf_binary)

   271 qed

   272

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

   274 proof -

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

   276   thus ?thesis by (simp only: is_Sup_binary)

   277 qed

   278

   279 instance complete_lattice \<subseteq> lattice

   280 proof

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

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

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

   284 qed

   285

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

   287   by (rule meet_equality) (rule is_inf_binary)

   288

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

   290   by (rule join_equality) (rule is_sup_binary)

   291

   292

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

   294

   295 text {*

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

   297   inclusion.

   298 *}

   299

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

   301 proof (rule Meet_greatest)

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

   303   also assume "A \<subseteq> B"

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

   305   thus "\<Sqinter>B \<sqsubseteq> a" ..

   306 qed

   307

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

   309 proof -

   310   assume "A \<subseteq> B"

   311   hence "dual  A \<subseteq> dual  B" by blast

   312   hence "\<Sqinter>(dual  B) \<sqsubseteq> \<Sqinter>(dual  A)" by (rule Meet_subset_antimono)

   313   hence "dual (\<Squnion>B) \<sqsubseteq> dual (\<Squnion>A)" by (simp only: dual_Join)

   314   thus ?thesis by (simp only: dual_leq)

   315 qed

   316

   317 text {*

   318   Bounds over unions of sets may be obtained separately.

   319 *}

   320

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

   322 proof

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

   324   thus "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> a"

   325   proof

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

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

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

   329     finally show ?thesis .

   330   next

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

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

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

   334     finally show ?thesis .

   335   qed

   336 next

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

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

   339   proof

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

   341     proof

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

   343       hence "a \<in>  A \<union> B" ..

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

   345     qed

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

   347     proof

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

   349       hence "a \<in>  A \<union> B" ..

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

   351     qed

   352   qed

   353 qed

   354

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

   356 proof -

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

   358     by (simp only: dual_Join image_Un)

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

   360     by (rule Meet_Un)

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

   362     by (simp only: dual_join dual_Join)

   363   finally show ?thesis ..

   364 qed

   365

   366 text {*

   367   Bounds over singleton sets are trivial.

   368 *}

   369

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

   371 proof

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

   373   hence "a = x" by simp

   374   thus "x \<sqsubseteq> a" by (simp only: leq_refl)

   375 next

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

   377   thus "b \<sqsubseteq> x" by simp

   378 qed

   379

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

   381 proof -

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

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

   384   finally show ?thesis ..

   385 qed

   386

   387 text {*

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

   389 *}

   390

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

   392 proof

   393   fix a :: "'a::complete_lattice"

   394   assume "a \<in> {}"

   395   hence False by simp

   396   thus "\<Squnion>UNIV \<sqsubseteq> a" ..

   397 next

   398   fix b :: "'a::complete_lattice"

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

   400   thus "b \<sqsubseteq> \<Squnion>UNIV" ..

   401 qed

   402

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

   404 proof -

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

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

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

   408   finally show ?thesis ..

   409 qed

   410

   411 end
`