src/HOL/Lattice/CompleteLattice.thy
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (22 months ago)
changeset 66695 91500c024c7f
parent 61986 2461779da2b8
permissions -rw-r--r--
tuned;
     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