src/HOL/Lattice/CompleteLattice.thy
 author wenzelm Sun Sep 18 20:33:48 2016 +0200 (2016-09-18) changeset 63915 bab633745c7f parent 61986 2461779da2b8 permissions -rw-r--r--
tuned proofs;
     1 (*  Title:      HOL/Lattice/CompleteLattice.thy

     2     Author:     Markus Wenzel, TU Muenchen

     3 *)

     4

     5 section \<open>Complete lattices\<close>

     6

     7 theory CompleteLattice imports Lattice begin

     8

     9 subsection \<open>Complete lattice operations\<close>

    10

    11 text \<open>

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

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

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

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

    16 \<close>

    17

    18 class complete_lattice =

    19   assumes ex_Inf: "\<exists>inf. is_Inf A inf"

    20

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

    22 proof -

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

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

    25   then show ?thesis ..

    26 qed

    27

    28 text \<open>

    29   The general \<open>\<Sqinter>\<close> (meet) and \<open>\<Squnion>\<close> (join) operations select

    30   such infimum and supremum elements.

    31 \<close>

    32

    33 definition

    34   Meet :: "'a::complete_lattice set \<Rightarrow> 'a"  ("\<Sqinter>_" [90] 90) where

    35   "\<Sqinter>A = (THE inf. is_Inf A inf)"

    36 definition

    37   Join :: "'a::complete_lattice set \<Rightarrow> 'a"  ("\<Squnion>_" [90] 90) where

    38   "\<Squnion>A = (THE sup. is_Sup A sup)"

    39

    40 text \<open>

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

    42   may be exhibited as follows.

    43 \<close>

    44

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

    46 proof (unfold Meet_def)

    47   assume "is_Inf A inf"

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

    49     by (rule the_equality) (rule is_Inf_uniq [OF _ \<open>is_Inf A inf\<close>])

    50 qed

    51

    52 lemma MeetI [intro?]:

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

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

    55     \<Sqinter>A = inf"

    56   by (rule Meet_equality, rule is_InfI) blast+

    57

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

    59 proof (unfold Join_def)

    60   assume "is_Sup A sup"

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

    62     by (rule the_equality) (rule is_Sup_uniq [OF _ \<open>is_Sup A sup\<close>])

    63 qed

    64

    65 lemma JoinI [intro?]:

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

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

    68     \<Squnion>A = sup"

    69   by (rule Join_equality, rule is_SupI) blast+

    70

    71

    72 text \<open>

    73   \medskip The \<open>\<Sqinter>\<close> and \<open>\<Squnion>\<close> operations indeed determine

    74   bounds on a complete lattice structure.

    75 \<close>

    76

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

    78 proof (unfold Meet_def)

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

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

    81     by (rule theI) (rule is_Inf_uniq [OF _ \<open>is_Inf A inf\<close>])

    82 qed

    83

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

    85   by (rule is_Inf_greatest, rule is_Inf_Meet) blast

    86

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

    88   by (rule is_Inf_lower) (rule is_Inf_Meet)

    89

    90

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

    92 proof (unfold Join_def)

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

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

    95     by (rule theI) (rule is_Sup_uniq [OF _ \<open>is_Sup A sup\<close>])

    96 qed

    97

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

    99   by (rule is_Sup_least, rule is_Sup_Join) blast

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

   101   by (rule is_Sup_upper) (rule is_Sup_Join)

   102

   103

   104 subsection \<open>The Knaster-Tarski Theorem\<close>

   105

   106 text \<open>

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

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

   109   (see @{cite \<open>pages 93--94\<close> "Davey-Priestley:1990"} for example).  This

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

   111   lattice operations.

   112 \<close>

   113

   114 theorem Knaster_Tarski:

   115   assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"

   116   obtains a :: "'a::complete_lattice" where

   117     "f a = a" and "\<And>a'. f a' = a' \<Longrightarrow> a \<sqsubseteq> a'"

   118 proof

   119   let ?H = "{u. f u \<sqsubseteq> u}"

   120   let ?a = "\<Sqinter>?H"

   121   show "f ?a = ?a"

   122   proof -

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

   124     proof

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

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

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

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

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

   130     qed

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

   132     proof

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

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

   135     qed

   136     finally show ?thesis .

   137   qed

   138

   139   fix a'

   140   assume "f a' = a'"

   141   then have "f a' \<sqsubseteq> a'" by (simp only: leq_refl)

   142   then have "a' \<in> ?H" ..

   143   then show "?a \<sqsubseteq> a'" ..

   144 qed

   145

   146 theorem Knaster_Tarski_dual:

   147   assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"

   148   obtains a :: "'a::complete_lattice" where

   149     "f a = a" and "\<And>a'. f a' = a' \<Longrightarrow> a' \<sqsubseteq> a"

   150 proof

   151   let ?H = "{u. u \<sqsubseteq> f u}"

   152   let ?a = "\<Squnion>?H"

   153   show "f ?a = ?a"

   154   proof -

   155     have le: "?a \<sqsubseteq> f ?a"

   156     proof

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

   158       then have "x \<sqsubseteq> f x" ..

   159       also from x have "x \<sqsubseteq> ?a" ..

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

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

   162     qed

   163     have "f ?a \<sqsubseteq> ?a"

   164     proof

   165       from le have "f ?a \<sqsubseteq> f (f ?a)" by (rule mono)

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

   167     qed

   168     from this and le show ?thesis by (rule leq_antisym)

   169   qed

   170

   171   fix a'

   172   assume "f a' = a'"

   173   then have "a' \<sqsubseteq> f a'" by (simp only: leq_refl)

   174   then have "a' \<in> ?H" ..

   175   then show "a' \<sqsubseteq> ?a" ..

   176 qed

   177

   178

   179 subsection \<open>Bottom and top elements\<close>

   180

   181 text \<open>

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

   183   greatest elements.

   184 \<close>

   185

   186 definition

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

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

   189

   190 definition

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

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

   193

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

   195 proof (unfold bottom_def)

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

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

   198 qed

   199

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

   201 proof (unfold bottom_def)

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

   203   show "\<Sqinter>UNIV = x"

   204   proof

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

   206   next

   207     fix b :: "'a::complete_lattice"

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

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

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

   211   qed

   212 qed

   213

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

   215 proof (unfold top_def)

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

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

   218 qed

   219

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

   221 proof (unfold top_def)

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

   223   show "\<Squnion>UNIV = x"

   224   proof

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

   226   next

   227     fix b :: "'a::complete_lattice"

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

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

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

   231   qed

   232 qed

   233

   234

   235 subsection \<open>Duality\<close>

   236

   237 text \<open>

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

   239   structures.

   240 \<close>

   241

   242 instance dual :: (complete_lattice) complete_lattice

   243 proof

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

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

   246   proof -

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

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

   249     then show ?thesis by (simp add: dual_ex [symmetric] image_comp)

   250   qed

   251 qed

   252

   253 text \<open>

   254   Apparently, the \<open>\<Sqinter>\<close> and \<open>\<Squnion>\<close> operations are dual to each

   255   other.

   256 \<close>

   257

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

   259 proof -

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

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

   262   then show ?thesis ..

   263 qed

   264

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

   266 proof -

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

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

   269   then show ?thesis ..

   270 qed

   271

   272 text \<open>

   273   Likewise are \<open>\<bottom>\<close> and \<open>\<top>\<close> duals of each other.

   274 \<close>

   275

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

   277 proof -

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

   279   proof

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

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

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

   283   qed

   284   then show ?thesis ..

   285 qed

   286

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

   288 proof -

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

   290   proof

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

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

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

   294   qed

   295   then show ?thesis ..

   296 qed

   297

   298

   299 subsection \<open>Complete lattices are lattices\<close>

   300

   301 text \<open>

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

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

   304   versus binary bounds that has been formally established in

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

   306 \<close>

   307

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

   309 proof -

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

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

   312 qed

   313

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

   315 proof -

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

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

   318 qed

   319

   320 instance complete_lattice \<subseteq> lattice

   321 proof

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

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

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

   325 qed

   326

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

   328   by (rule meet_equality) (rule is_inf_binary)

   329

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

   331   by (rule join_equality) (rule is_sup_binary)

   332

   333

   334 subsection \<open>Complete lattices and set-theory operations\<close>

   335

   336 text \<open>

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

   338   inclusion.

   339 \<close>

   340

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

   342 proof (rule Meet_greatest)

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

   344   also assume "A \<subseteq> B"

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

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

   347 qed

   348

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

   350 proof -

   351   assume "A \<subseteq> B"

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

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

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

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

   356 qed

   357

   358 text \<open>

   359   Bounds over unions of sets may be obtained separately.

   360 \<close>

   361

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

   363 proof

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

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

   366   proof

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

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

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

   370     finally show ?thesis .

   371   next

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

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

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

   375     finally show ?thesis .

   376   qed

   377 next

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

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

   380   proof

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

   382     proof

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

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

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

   386     qed

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

   388     proof

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

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

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

   392     qed

   393   qed

   394 qed

   395

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

   397 proof -

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

   399     by (simp only: dual_Join image_Un)

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

   401     by (rule Meet_Un)

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

   403     by (simp only: dual_join dual_Join)

   404   finally show ?thesis ..

   405 qed

   406

   407 text \<open>

   408   Bounds over singleton sets are trivial.

   409 \<close>

   410

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

   412 proof

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

   414   then have "a = x" by simp

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

   416 next

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

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

   419 qed

   420

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

   422 proof -

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

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

   425   finally show ?thesis ..

   426 qed

   427

   428 text \<open>

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

   430 \<close>

   431

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

   433 proof

   434   fix a :: "'a::complete_lattice"

   435   assume "a \<in> {}"

   436   then have False by simp

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

   438 next

   439   fix b :: "'a::complete_lattice"

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

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

   442 qed

   443

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

   445 proof -

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

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

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

   449   finally show ?thesis ..

   450 qed

   451

   452 end
`