src/HOL/Lattice/CompleteLattice.thy
 author blanchet Wed Feb 12 08:35:57 2014 +0100 (2014-02-12) changeset 55415 05f5fdb8d093 parent 35317 d57da4abb47d child 56154 f0a927235162 permissions -rw-r--r--
renamed 'nat_{case,rec}' to '{case,rec}_nat'
     1 (*  Title:      HOL/Lattice/CompleteLattice.thy

     2     Author:     Markus Wenzel, TU Muenchen

     3 *)

     4

     5 header {* Complete lattices *}

     6

     7 theory CompleteLattice imports Lattice begin

     8

     9 subsection {* Complete lattice operations *}

    10

    11 text {*

    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 *}

    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 {*

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

    30   such infimum and supremum elements.

    31 *}

    32

    33 definition

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

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

    36 definition

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

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

    39

    40 notation (xsymbols)

    41   Meet  ("\<Sqinter>_" [90] 90) and

    42   Join  ("\<Squnion>_" [90] 90)

    43

    44 text {*

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

    46   may be exhibited as follows.

    47 *}

    48

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

    50 proof (unfold Meet_def)

    51   assume "is_Inf A inf"

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

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

    54 qed

    55

    56 lemma MeetI [intro?]:

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

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

    59     \<Sqinter>A = inf"

    60   by (rule Meet_equality, rule is_InfI) blast+

    61

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

    63 proof (unfold Join_def)

    64   assume "is_Sup A sup"

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

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

    67 qed

    68

    69 lemma JoinI [intro?]:

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

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

    72     \<Squnion>A = sup"

    73   by (rule Join_equality, rule is_SupI) blast+

    74

    75

    76 text {*

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

    78   bounds on a complete lattice structure.

    79 *}

    80

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

    82 proof (unfold Meet_def)

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

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

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

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

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

   100 qed

   101

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

   103   by (rule is_Sup_least, rule is_Sup_Join) blast

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

   105   by (rule is_Sup_upper) (rule is_Sup_Join)

   106

   107

   108 subsection {* The Knaster-Tarski Theorem *}

   109

   110 text {*

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

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

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

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

   115   lattice operations.

   116 *}

   117

   118 theorem Knaster_Tarski:

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

   120   obtains a :: "'a::complete_lattice" where

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

   122 proof

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

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

   125   show "f ?a = ?a"

   126   proof -

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

   128     proof

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

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

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

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

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

   134     qed

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

   136     proof

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

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

   139     qed

   140     finally show ?thesis .

   141   qed

   142

   143   fix a'

   144   assume "f a' = a'"

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

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

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

   148 qed

   149

   150 theorem Knaster_Tarski_dual:

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

   152   obtains a :: "'a::complete_lattice" where

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

   154 proof

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

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

   157   show "f ?a = ?a"

   158   proof -

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

   160     proof

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

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

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

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

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

   166     qed

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

   168     proof

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

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

   171     qed

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

   173   qed

   174

   175   fix a'

   176   assume "f a' = a'"

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

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

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

   180 qed

   181

   182

   183 subsection {* Bottom and top elements *}

   184

   185 text {*

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

   187   greatest elements.

   188 *}

   189

   190 definition

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

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

   193

   194 definition

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

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

   197

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

   199 proof (unfold bottom_def)

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

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

   202 qed

   203

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

   205 proof (unfold bottom_def)

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

   207   show "\<Sqinter>UNIV = x"

   208   proof

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

   210   next

   211     fix b :: "'a::complete_lattice"

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

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

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

   215   qed

   216 qed

   217

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

   219 proof (unfold top_def)

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

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

   222 qed

   223

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

   225 proof (unfold top_def)

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

   227   show "\<Squnion>UNIV = x"

   228   proof

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

   230   next

   231     fix b :: "'a::complete_lattice"

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

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

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

   235   qed

   236 qed

   237

   238

   239 subsection {* Duality *}

   240

   241 text {*

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

   243   structures.

   244 *}

   245

   246 instance dual :: (complete_lattice) complete_lattice

   247 proof

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

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

   250   proof -

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

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

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

   254   qed

   255 qed

   256

   257 text {*

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

   259   other.

   260 *}

   261

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

   263 proof -

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

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

   266   then show ?thesis ..

   267 qed

   268

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

   270 proof -

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

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

   273   then show ?thesis ..

   274 qed

   275

   276 text {*

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

   278 *}

   279

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

   281 proof -

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

   283   proof

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

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

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

   287   qed

   288   then show ?thesis ..

   289 qed

   290

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

   292 proof -

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

   294   proof

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

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

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

   298   qed

   299   then show ?thesis ..

   300 qed

   301

   302

   303 subsection {* Complete lattices are lattices *}

   304

   305 text {*

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

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

   308   versus binary bounds that has been formally established in

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

   310 *}

   311

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

   313 proof -

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

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

   316 qed

   317

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

   319 proof -

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

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

   322 qed

   323

   324 instance complete_lattice \<subseteq> lattice

   325 proof

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

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

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

   329 qed

   330

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

   332   by (rule meet_equality) (rule is_inf_binary)

   333

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

   335   by (rule join_equality) (rule is_sup_binary)

   336

   337

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

   339

   340 text {*

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

   342   inclusion.

   343 *}

   344

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

   346 proof (rule Meet_greatest)

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

   348   also assume "A \<subseteq> B"

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

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

   351 qed

   352

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

   354 proof -

   355   assume "A \<subseteq> B"

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

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

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

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

   360 qed

   361

   362 text {*

   363   Bounds over unions of sets may be obtained separately.

   364 *}

   365

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

   367 proof

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

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

   370   proof

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

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

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

   374     finally show ?thesis .

   375   next

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

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

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

   379     finally show ?thesis .

   380   qed

   381 next

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

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

   384   proof

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

   386     proof

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

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

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

   390     qed

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

   392     proof

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

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

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

   396     qed

   397   qed

   398 qed

   399

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

   401 proof -

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

   403     by (simp only: dual_Join image_Un)

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

   405     by (rule Meet_Un)

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

   407     by (simp only: dual_join dual_Join)

   408   finally show ?thesis ..

   409 qed

   410

   411 text {*

   412   Bounds over singleton sets are trivial.

   413 *}

   414

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

   416 proof

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

   418   then have "a = x" by simp

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

   420 next

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

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

   423 qed

   424

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

   426 proof -

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

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

   429   finally show ?thesis ..

   430 qed

   431

   432 text {*

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

   434 *}

   435

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

   437 proof

   438   fix a :: "'a::complete_lattice"

   439   assume "a \<in> {}"

   440   then have False by simp

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

   442 next

   443   fix b :: "'a::complete_lattice"

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

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

   446 qed

   447

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

   449 proof -

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

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

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

   453   finally show ?thesis ..

   454 qed

   455

   456 end
`