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