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
`