src/HOL/Lattice/CompleteLattice.thy
author huffman
Mon Jan 12 12:09:54 2009 -0800 (2009-01-12)
changeset 29460 ad87e5d1488b
parent 25474 c41b433b0f65
child 35317 d57da4abb47d
permissions -rw-r--r--
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
     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   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