src/HOL/Lattice/CompleteLattice.thy
author wenzelm
Fri Nov 17 02:20:03 2006 +0100 (2006-11-17)
changeset 21404 eb85850d3eb7
parent 21210 c17fd2df4e9e
child 23373 ead82c82da9e
permissions -rw-r--r--
more robust syntax for definition/abbreviation/notation;
     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   hence "is_Sup A sup" by (rule Inf_Sup)
    26   thus ?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   thus "(THE inf. is_Inf A inf) = inf"
    54     by (rule the_equality) (rule is_Inf_uniq)
    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   thus "(THE sup. is_Sup A sup) = sup"
    67     by (rule the_equality) (rule is_Sup_uniq)
    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   thus "is_Inf A (THE inf. is_Inf A inf)" by (rule theI) (rule is_Inf_uniq)
    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   thus "is_Sup A (THE sup. is_Sup A sup)" by (rule theI) (rule is_Sup_uniq)
    99 qed
   100 
   101 lemma Join_least [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> a \<sqsubseteq> x) \<Longrightarrow> \<Squnion>A \<sqsubseteq> x"
   102   by (rule is_Sup_least, rule is_Sup_Join) blast
   103 lemma Join_lower [intro?]: "a \<in> A \<Longrightarrow> a \<sqsubseteq> \<Squnion>A"
   104   by (rule is_Sup_upper) (rule is_Sup_Join)
   105 
   106 
   107 subsection {* The Knaster-Tarski Theorem *}
   108 
   109 text {*
   110   The Knaster-Tarski Theorem (in its simplest formulation) states that
   111   any monotone function on a complete lattice has a least fixed-point
   112   (see \cite[pages 93--94]{Davey-Priestley:1990} for example).  This
   113   is a consequence of the basic boundary properties of the complete
   114   lattice operations.
   115 *}
   116 
   117 theorem Knaster_Tarski:
   118   "(\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y) \<Longrightarrow> \<exists>a::'a::complete_lattice. f a = a"
   119 proof
   120   assume mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
   121   let ?H = "{u. f u \<sqsubseteq> u}" let ?a = "\<Sqinter>?H"
   122   have ge: "f ?a \<sqsubseteq> ?a"
   123   proof
   124     fix x assume x: "x \<in> ?H"
   125     hence "?a \<sqsubseteq> x" ..
   126     hence "f ?a \<sqsubseteq> f x" by (rule mono)
   127     also from x have "... \<sqsubseteq> x" ..
   128     finally show "f ?a \<sqsubseteq> x" .
   129   qed
   130   also have "?a \<sqsubseteq> f ?a"
   131   proof
   132     from ge have "f (f ?a) \<sqsubseteq> f ?a" by (rule mono)
   133     thus "f ?a \<in> ?H" ..
   134   qed
   135   finally show "f ?a = ?a" .
   136 qed
   137 
   138 
   139 subsection {* Bottom and top elements *}
   140 
   141 text {*
   142   With general bounds available, complete lattices also have least and
   143   greatest elements.
   144 *}
   145 
   146 definition
   147   bottom :: "'a::complete_lattice"    ("\<bottom>") where
   148   "\<bottom> = \<Sqinter>UNIV"
   149 definition
   150   top :: "'a::complete_lattice"    ("\<top>") where
   151   "\<top> = \<Squnion>UNIV"
   152 
   153 lemma bottom_least [intro?]: "\<bottom> \<sqsubseteq> x"
   154 proof (unfold bottom_def)
   155   have "x \<in> UNIV" ..
   156   thus "\<Sqinter>UNIV \<sqsubseteq> x" ..
   157 qed
   158 
   159 lemma bottomI [intro?]: "(\<And>a. x \<sqsubseteq> a) \<Longrightarrow> \<bottom> = x"
   160 proof (unfold bottom_def)
   161   assume "\<And>a. x \<sqsubseteq> a"
   162   show "\<Sqinter>UNIV = x"
   163   proof
   164     fix a show "x \<sqsubseteq> a" .
   165   next
   166     fix b :: "'a::complete_lattice"
   167     assume b: "\<forall>a \<in> UNIV. b \<sqsubseteq> a"
   168     have "x \<in> UNIV" ..
   169     with b show "b \<sqsubseteq> x" ..
   170   qed
   171 qed
   172 
   173 lemma top_greatest [intro?]: "x \<sqsubseteq> \<top>"
   174 proof (unfold top_def)
   175   have "x \<in> UNIV" ..
   176   thus "x \<sqsubseteq> \<Squnion>UNIV" ..
   177 qed
   178 
   179 lemma topI [intro?]: "(\<And>a. a \<sqsubseteq> x) \<Longrightarrow> \<top> = x"
   180 proof (unfold top_def)
   181   assume "\<And>a. a \<sqsubseteq> x"
   182   show "\<Squnion>UNIV = x"
   183   proof
   184     fix a show "a \<sqsubseteq> x" .
   185   next
   186     fix b :: "'a::complete_lattice"
   187     assume b: "\<forall>a \<in> UNIV. a \<sqsubseteq> b"
   188     have "x \<in> UNIV" ..
   189     with b show "x \<sqsubseteq> b" ..
   190   qed
   191 qed
   192 
   193 
   194 subsection {* Duality *}
   195 
   196 text {*
   197   The class of complete lattices is closed under formation of dual
   198   structures.
   199 *}
   200 
   201 instance dual :: (complete_lattice) complete_lattice
   202 proof
   203   fix A' :: "'a::complete_lattice dual set"
   204   show "\<exists>inf'. is_Inf A' inf'"
   205   proof -
   206     have "\<exists>sup. is_Sup (undual ` A') sup" by (rule ex_Sup)
   207     hence "\<exists>sup. is_Inf (dual ` undual ` A') (dual sup)" by (simp only: dual_Inf)
   208     thus ?thesis by (simp add: dual_ex [symmetric] image_compose [symmetric])
   209   qed
   210 qed
   211 
   212 text {*
   213   Apparently, the @{text \<Sqinter>} and @{text \<Squnion>} operations are dual to each
   214   other.
   215 *}
   216 
   217 theorem dual_Meet [intro?]: "dual (\<Sqinter>A) = \<Squnion>(dual ` A)"
   218 proof -
   219   from is_Inf_Meet have "is_Sup (dual ` A) (dual (\<Sqinter>A))" ..
   220   hence "\<Squnion>(dual ` A) = dual (\<Sqinter>A)" ..
   221   thus ?thesis ..
   222 qed
   223 
   224 theorem dual_Join [intro?]: "dual (\<Squnion>A) = \<Sqinter>(dual ` A)"
   225 proof -
   226   from is_Sup_Join have "is_Inf (dual ` A) (dual (\<Squnion>A))" ..
   227   hence "\<Sqinter>(dual ` A) = dual (\<Squnion>A)" ..
   228   thus ?thesis ..
   229 qed
   230 
   231 text {*
   232   Likewise are @{text \<bottom>} and @{text \<top>} duals of each other.
   233 *}
   234 
   235 theorem dual_bottom [intro?]: "dual \<bottom> = \<top>"
   236 proof -
   237   have "\<top> = dual \<bottom>"
   238   proof
   239     fix a' have "\<bottom> \<sqsubseteq> undual a'" ..
   240     hence "dual (undual a') \<sqsubseteq> dual \<bottom>" ..
   241     thus "a' \<sqsubseteq> dual \<bottom>" by simp
   242   qed
   243   thus ?thesis ..
   244 qed
   245 
   246 theorem dual_top [intro?]: "dual \<top> = \<bottom>"
   247 proof -
   248   have "\<bottom> = dual \<top>"
   249   proof
   250     fix a' have "undual a' \<sqsubseteq> \<top>" ..
   251     hence "dual \<top> \<sqsubseteq> dual (undual a')" ..
   252     thus "dual \<top> \<sqsubseteq> a'" by simp
   253   qed
   254   thus ?thesis ..
   255 qed
   256 
   257 
   258 subsection {* Complete lattices are lattices *}
   259 
   260 text {*
   261   Complete lattices (with general bounds available) are indeed plain
   262   lattices as well.  This holds due to the connection of general
   263   versus binary bounds that has been formally established in
   264   \S\ref{sec:gen-bin-bounds}.
   265 *}
   266 
   267 lemma is_inf_binary: "is_inf x y (\<Sqinter>{x, y})"
   268 proof -
   269   have "is_Inf {x, y} (\<Sqinter>{x, y})" ..
   270   thus ?thesis by (simp only: is_Inf_binary)
   271 qed
   272 
   273 lemma is_sup_binary: "is_sup x y (\<Squnion>{x, y})"
   274 proof -
   275   have "is_Sup {x, y} (\<Squnion>{x, y})" ..
   276   thus ?thesis by (simp only: is_Sup_binary)
   277 qed
   278 
   279 instance complete_lattice \<subseteq> lattice
   280 proof
   281   fix x y :: "'a::complete_lattice"
   282   from is_inf_binary show "\<exists>inf. is_inf x y inf" ..
   283   from is_sup_binary show "\<exists>sup. is_sup x y sup" ..
   284 qed
   285 
   286 theorem meet_binary: "x \<sqinter> y = \<Sqinter>{x, y}"
   287   by (rule meet_equality) (rule is_inf_binary)
   288 
   289 theorem join_binary: "x \<squnion> y = \<Squnion>{x, y}"
   290   by (rule join_equality) (rule is_sup_binary)
   291 
   292 
   293 subsection {* Complete lattices and set-theory operations *}
   294 
   295 text {*
   296   The complete lattice operations are (anti) monotone wrt.\ set
   297   inclusion.
   298 *}
   299 
   300 theorem Meet_subset_antimono: "A \<subseteq> B \<Longrightarrow> \<Sqinter>B \<sqsubseteq> \<Sqinter>A"
   301 proof (rule Meet_greatest)
   302   fix a assume "a \<in> A"
   303   also assume "A \<subseteq> B"
   304   finally have "a \<in> B" .
   305   thus "\<Sqinter>B \<sqsubseteq> a" ..
   306 qed
   307 
   308 theorem Join_subset_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<sqsubseteq> \<Squnion>B"
   309 proof -
   310   assume "A \<subseteq> B"
   311   hence "dual ` A \<subseteq> dual ` B" by blast
   312   hence "\<Sqinter>(dual ` B) \<sqsubseteq> \<Sqinter>(dual ` A)" by (rule Meet_subset_antimono)
   313   hence "dual (\<Squnion>B) \<sqsubseteq> dual (\<Squnion>A)" by (simp only: dual_Join)
   314   thus ?thesis by (simp only: dual_leq)
   315 qed
   316 
   317 text {*
   318   Bounds over unions of sets may be obtained separately.
   319 *}
   320 
   321 theorem Meet_Un: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
   322 proof
   323   fix a assume "a \<in> A \<union> B"
   324   thus "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> a"
   325   proof
   326     assume a: "a \<in> A"
   327     have "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> \<Sqinter>A" ..
   328     also from a have "\<dots> \<sqsubseteq> a" ..
   329     finally show ?thesis .
   330   next
   331     assume a: "a \<in> B"
   332     have "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> \<Sqinter>B" ..
   333     also from a have "\<dots> \<sqsubseteq> a" ..
   334     finally show ?thesis .
   335   qed
   336 next
   337   fix b assume b: "\<forall>a \<in> A \<union> B. b \<sqsubseteq> a"
   338   show "b \<sqsubseteq> \<Sqinter>A \<sqinter> \<Sqinter>B"
   339   proof
   340     show "b \<sqsubseteq> \<Sqinter>A"
   341     proof
   342       fix a assume "a \<in> A"
   343       hence "a \<in>  A \<union> B" ..
   344       with b show "b \<sqsubseteq> a" ..
   345     qed
   346     show "b \<sqsubseteq> \<Sqinter>B"
   347     proof
   348       fix a assume "a \<in> B"
   349       hence "a \<in>  A \<union> B" ..
   350       with b show "b \<sqsubseteq> a" ..
   351     qed
   352   qed
   353 qed
   354 
   355 theorem Join_Un: "\<Squnion>(A \<union> B) = \<Squnion>A \<squnion> \<Squnion>B"
   356 proof -
   357   have "dual (\<Squnion>(A \<union> B)) = \<Sqinter>(dual ` A \<union> dual ` B)"
   358     by (simp only: dual_Join image_Un)
   359   also have "\<dots> = \<Sqinter>(dual ` A) \<sqinter> \<Sqinter>(dual ` B)"
   360     by (rule Meet_Un)
   361   also have "\<dots> = dual (\<Squnion>A \<squnion> \<Squnion>B)"
   362     by (simp only: dual_join dual_Join)
   363   finally show ?thesis ..
   364 qed
   365 
   366 text {*
   367   Bounds over singleton sets are trivial.
   368 *}
   369 
   370 theorem Meet_singleton: "\<Sqinter>{x} = x"
   371 proof
   372   fix a assume "a \<in> {x}"
   373   hence "a = x" by simp
   374   thus "x \<sqsubseteq> a" by (simp only: leq_refl)
   375 next
   376   fix b assume "\<forall>a \<in> {x}. b \<sqsubseteq> a"
   377   thus "b \<sqsubseteq> x" by simp
   378 qed
   379 
   380 theorem Join_singleton: "\<Squnion>{x} = x"
   381 proof -
   382   have "dual (\<Squnion>{x}) = \<Sqinter>{dual x}" by (simp add: dual_Join)
   383   also have "\<dots> = dual x" by (rule Meet_singleton)
   384   finally show ?thesis ..
   385 qed
   386 
   387 text {*
   388   Bounds over the empty and universal set correspond to each other.
   389 *}
   390 
   391 theorem Meet_empty: "\<Sqinter>{} = \<Squnion>UNIV"
   392 proof
   393   fix a :: "'a::complete_lattice"
   394   assume "a \<in> {}"
   395   hence False by simp
   396   thus "\<Squnion>UNIV \<sqsubseteq> a" ..
   397 next
   398   fix b :: "'a::complete_lattice"
   399   have "b \<in> UNIV" ..
   400   thus "b \<sqsubseteq> \<Squnion>UNIV" ..
   401 qed
   402 
   403 theorem Join_empty: "\<Squnion>{} = \<Sqinter>UNIV"
   404 proof -
   405   have "dual (\<Squnion>{}) = \<Sqinter>{}" by (simp add: dual_Join)
   406   also have "\<dots> = \<Squnion>UNIV" by (rule Meet_empty)
   407   also have "\<dots> = dual (\<Sqinter>UNIV)" by (simp add: dual_Meet)
   408   finally show ?thesis ..
   409 qed
   410 
   411 end