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
     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   assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"

   121   obtains a :: "'a::complete_lattice" where

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

   123 proof

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

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

   126   show "f ?a = ?a"

   127   proof -

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

   129     proof

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

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

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

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

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

   135     qed

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

   137     proof

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

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

   140     qed

   141     finally show ?thesis .

   142   qed

   143

   144   fix a'

   145   assume "f a' = a'"

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

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

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

   149 qed

   150

   151 theorem Knaster_Tarski_dual:

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

   153   obtains a :: "'a::complete_lattice" where

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

   155 proof

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

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

   158   show "f ?a = ?a"

   159   proof -

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

   161     proof

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

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

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

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

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

   167     qed

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

   169     proof

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

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

   172     qed

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

   174   qed

   175

   176   fix a'

   177   assume "f a' = a'"

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

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

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

   181 qed

   182

   183

   184 subsection {* Bottom and top elements *}

   185

   186 text {*

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

   188   greatest elements.

   189 *}

   190

   191 definition

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

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

   194

   195 definition

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

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

   198

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

   200 proof (unfold bottom_def)

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

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

   203 qed

   204

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

   206 proof (unfold bottom_def)

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

   208   show "\<Sqinter>UNIV = x"

   209   proof

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

   211   next

   212     fix b :: "'a::complete_lattice"

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

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

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

   216   qed

   217 qed

   218

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

   220 proof (unfold top_def)

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

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

   223 qed

   224

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

   226 proof (unfold top_def)

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

   228   show "\<Squnion>UNIV = x"

   229   proof

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

   231   next

   232     fix b :: "'a::complete_lattice"

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

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

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

   236   qed

   237 qed

   238

   239

   240 subsection {* Duality *}

   241

   242 text {*

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

   244   structures.

   245 *}

   246

   247 instance dual :: (complete_lattice) complete_lattice

   248 proof

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

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

   251   proof -

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

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

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

   255   qed

   256 qed

   257

   258 text {*

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

   260   other.

   261 *}

   262

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

   264 proof -

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

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

   267   then show ?thesis ..

   268 qed

   269

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

   271 proof -

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

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

   274   then show ?thesis ..

   275 qed

   276

   277 text {*

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

   279 *}

   280

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

   282 proof -

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

   284   proof

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

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

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

   288   qed

   289   then show ?thesis ..

   290 qed

   291

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

   293 proof -

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

   295   proof

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

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

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

   299   qed

   300   then show ?thesis ..

   301 qed

   302

   303

   304 subsection {* Complete lattices are lattices *}

   305

   306 text {*

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

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

   309   versus binary bounds that has been formally established in

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

   311 *}

   312

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

   314 proof -

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

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

   317 qed

   318

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

   320 proof -

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

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

   323 qed

   324

   325 instance complete_lattice \<subseteq> lattice

   326 proof

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

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

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

   330 qed

   331

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

   333   by (rule meet_equality) (rule is_inf_binary)

   334

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

   336   by (rule join_equality) (rule is_sup_binary)

   337

   338

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

   340

   341 text {*

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

   343   inclusion.

   344 *}

   345

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

   347 proof (rule Meet_greatest)

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

   349   also assume "A \<subseteq> B"

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

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

   352 qed

   353

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

   355 proof -

   356   assume "A \<subseteq> B"

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

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

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

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

   361 qed

   362

   363 text {*

   364   Bounds over unions of sets may be obtained separately.

   365 *}

   366

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

   368 proof

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

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

   371   proof

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

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

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

   375     finally show ?thesis .

   376   next

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

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

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

   380     finally show ?thesis .

   381   qed

   382 next

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

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

   385   proof

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

   387     proof

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

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

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

   391     qed

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

   393     proof

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

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

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

   397     qed

   398   qed

   399 qed

   400

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

   402 proof -

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

   404     by (simp only: dual_Join image_Un)

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

   406     by (rule Meet_Un)

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

   408     by (simp only: dual_join dual_Join)

   409   finally show ?thesis ..

   410 qed

   411

   412 text {*

   413   Bounds over singleton sets are trivial.

   414 *}

   415

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

   417 proof

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

   419   then have "a = x" by simp

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

   421 next

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

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

   424 qed

   425

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

   427 proof -

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

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

   430   finally show ?thesis ..

   431 qed

   432

   433 text {*

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

   435 *}

   436

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

   438 proof

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

   440   assume "a \<in> {}"

   441   then have False by simp

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

   443 next

   444   fix b :: "'a::complete_lattice"

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

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

   447 qed

   448

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

   450 proof -

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

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

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

   454   finally show ?thesis ..

   455 qed

   456

   457 end
`