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] 90) and
    43   Join  ("\<Squnion>_" [90] 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