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