src/HOL/Lattice/CompleteLattice.thy
author wenzelm
Mon Nov 26 22:59:24 2007 +0100 (2007-11-26)
changeset 25469 f81b3be9dfdd
parent 23373 ead82c82da9e
child 25474 c41b433b0f65
permissions -rw-r--r--
some more lemmas due to Peter Lammich;
wenzelm@10157
     1
(*  Title:      HOL/Lattice/CompleteLattice.thy
wenzelm@10157
     2
    ID:         $Id$
wenzelm@10157
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@10157
     4
*)
wenzelm@10157
     5
wenzelm@10157
     6
header {* Complete lattices *}
wenzelm@10157
     7
haftmann@16417
     8
theory CompleteLattice imports Lattice begin
wenzelm@10157
     9
wenzelm@10157
    10
subsection {* Complete lattice operations *}
wenzelm@10157
    11
wenzelm@10157
    12
text {*
wenzelm@10157
    13
  A \emph{complete lattice} is a partial order with general
wenzelm@10157
    14
  (infinitary) infimum of any set of elements.  General supremum
wenzelm@10157
    15
  exists as well, as a consequence of the connection of infinitary
wenzelm@10157
    16
  bounds (see \S\ref{sec:connect-bounds}).
wenzelm@10157
    17
*}
wenzelm@10157
    18
wenzelm@11099
    19
axclass complete_lattice \<subseteq> partial_order
wenzelm@10157
    20
  ex_Inf: "\<exists>inf. is_Inf A inf"
wenzelm@10157
    21
wenzelm@10157
    22
theorem ex_Sup: "\<exists>sup::'a::complete_lattice. is_Sup A sup"
wenzelm@10157
    23
proof -
wenzelm@10157
    24
  from ex_Inf obtain sup where "is_Inf {b. \<forall>a\<in>A. a \<sqsubseteq> b} sup" by blast
wenzelm@23373
    25
  then have "is_Sup A sup" by (rule Inf_Sup)
wenzelm@23373
    26
  then show ?thesis ..
wenzelm@10157
    27
qed
wenzelm@10157
    28
wenzelm@10157
    29
text {*
wenzelm@10157
    30
  The general @{text \<Sqinter>} (meet) and @{text \<Squnion>} (join) operations select
wenzelm@10157
    31
  such infimum and supremum elements.
wenzelm@10157
    32
*}
wenzelm@10157
    33
wenzelm@19736
    34
definition
wenzelm@21404
    35
  Meet :: "'a::complete_lattice set \<Rightarrow> 'a" where
wenzelm@19736
    36
  "Meet A = (THE inf. is_Inf A inf)"
wenzelm@21404
    37
definition
wenzelm@21404
    38
  Join :: "'a::complete_lattice set \<Rightarrow> 'a" where
wenzelm@19736
    39
  "Join A = (THE sup. is_Sup A sup)"
wenzelm@19736
    40
wenzelm@21210
    41
notation (xsymbols)
wenzelm@21404
    42
  Meet  ("\<Sqinter>_" [90] 90) and
wenzelm@19736
    43
  Join  ("\<Squnion>_" [90] 90)
wenzelm@10157
    44
wenzelm@10157
    45
text {*
wenzelm@10157
    46
  Due to unique existence of bounds, the complete lattice operations
wenzelm@10157
    47
  may be exhibited as follows.
wenzelm@10157
    48
*}
wenzelm@10157
    49
wenzelm@10157
    50
lemma Meet_equality [elim?]: "is_Inf A inf \<Longrightarrow> \<Sqinter>A = inf"
wenzelm@10157
    51
proof (unfold Meet_def)
wenzelm@10157
    52
  assume "is_Inf A inf"
wenzelm@23373
    53
  then show "(THE inf. is_Inf A inf) = inf"
wenzelm@23373
    54
    by (rule the_equality) (rule is_Inf_uniq [OF _ `is_Inf A inf`])
wenzelm@10157
    55
qed
wenzelm@10157
    56
wenzelm@10157
    57
lemma MeetI [intro?]:
wenzelm@10157
    58
  "(\<And>a. a \<in> A \<Longrightarrow> inf \<sqsubseteq> a) \<Longrightarrow>
wenzelm@10157
    59
    (\<And>b. \<forall>a \<in> A. b \<sqsubseteq> a \<Longrightarrow> b \<sqsubseteq> inf) \<Longrightarrow>
wenzelm@10157
    60
    \<Sqinter>A = inf"
wenzelm@10157
    61
  by (rule Meet_equality, rule is_InfI) blast+
wenzelm@10157
    62
wenzelm@10157
    63
lemma Join_equality [elim?]: "is_Sup A sup \<Longrightarrow> \<Squnion>A = sup"
wenzelm@10157
    64
proof (unfold Join_def)
wenzelm@10157
    65
  assume "is_Sup A sup"
wenzelm@23373
    66
  then show "(THE sup. is_Sup A sup) = sup"
wenzelm@23373
    67
    by (rule the_equality) (rule is_Sup_uniq [OF _ `is_Sup A sup`])
wenzelm@10157
    68
qed
wenzelm@10157
    69
wenzelm@10157
    70
lemma JoinI [intro?]:
wenzelm@10157
    71
  "(\<And>a. a \<in> A \<Longrightarrow> a \<sqsubseteq> sup) \<Longrightarrow>
wenzelm@10157
    72
    (\<And>b. \<forall>a \<in> A. a \<sqsubseteq> b \<Longrightarrow> sup \<sqsubseteq> b) \<Longrightarrow>
wenzelm@10157
    73
    \<Squnion>A = sup"
wenzelm@10157
    74
  by (rule Join_equality, rule is_SupI) blast+
wenzelm@10157
    75
wenzelm@10157
    76
wenzelm@10157
    77
text {*
wenzelm@10157
    78
  \medskip The @{text \<Sqinter>} and @{text \<Squnion>} operations indeed determine
wenzelm@10157
    79
  bounds on a complete lattice structure.
wenzelm@10157
    80
*}
wenzelm@10157
    81
wenzelm@10157
    82
lemma is_Inf_Meet [intro?]: "is_Inf A (\<Sqinter>A)"
wenzelm@10157
    83
proof (unfold Meet_def)
wenzelm@11441
    84
  from ex_Inf obtain inf where "is_Inf A inf" ..
wenzelm@23373
    85
  then show "is_Inf A (THE inf. is_Inf A inf)"
wenzelm@23373
    86
    by (rule theI) (rule is_Inf_uniq [OF _ `is_Inf A inf`])
wenzelm@10157
    87
qed
wenzelm@10157
    88
wenzelm@10157
    89
lemma Meet_greatest [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> x \<sqsubseteq> a) \<Longrightarrow> x \<sqsubseteq> \<Sqinter>A"
wenzelm@10157
    90
  by (rule is_Inf_greatest, rule is_Inf_Meet) blast
wenzelm@10157
    91
wenzelm@10157
    92
lemma Meet_lower [intro?]: "a \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> a"
wenzelm@10157
    93
  by (rule is_Inf_lower) (rule is_Inf_Meet)
wenzelm@10157
    94
wenzelm@10157
    95
wenzelm@10157
    96
lemma is_Sup_Join [intro?]: "is_Sup A (\<Squnion>A)"
wenzelm@10157
    97
proof (unfold Join_def)
wenzelm@11441
    98
  from ex_Sup obtain sup where "is_Sup A sup" ..
wenzelm@23373
    99
  then show "is_Sup A (THE sup. is_Sup A sup)"
wenzelm@23373
   100
    by (rule theI) (rule is_Sup_uniq [OF _ `is_Sup A sup`])
wenzelm@10157
   101
qed
wenzelm@10157
   102
wenzelm@10157
   103
lemma Join_least [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> a \<sqsubseteq> x) \<Longrightarrow> \<Squnion>A \<sqsubseteq> x"
wenzelm@10157
   104
  by (rule is_Sup_least, rule is_Sup_Join) blast
wenzelm@10157
   105
lemma Join_lower [intro?]: "a \<in> A \<Longrightarrow> a \<sqsubseteq> \<Squnion>A"
wenzelm@10157
   106
  by (rule is_Sup_upper) (rule is_Sup_Join)
wenzelm@10157
   107
wenzelm@10157
   108
wenzelm@10157
   109
subsection {* The Knaster-Tarski Theorem *}
wenzelm@10157
   110
wenzelm@10157
   111
text {*
wenzelm@10157
   112
  The Knaster-Tarski Theorem (in its simplest formulation) states that
wenzelm@10157
   113
  any monotone function on a complete lattice has a least fixed-point
wenzelm@10157
   114
  (see \cite[pages 93--94]{Davey-Priestley:1990} for example).  This
wenzelm@10157
   115
  is a consequence of the basic boundary properties of the complete
wenzelm@10157
   116
  lattice operations.
wenzelm@10157
   117
*}
wenzelm@10157
   118
wenzelm@10157
   119
theorem Knaster_Tarski:
wenzelm@25469
   120
  assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
wenzelm@25469
   121
  shows "\<exists>a::'a::complete_lattice. f a = a \<and> (\<forall>a'. f a' = a' \<longrightarrow> a \<sqsubseteq> a')"
wenzelm@25469
   122
proof -
wenzelm@25469
   123
  let ?H = "{u. f u \<sqsubseteq> u}"
wenzelm@25469
   124
  let ?a = "\<Sqinter>?H"
wenzelm@25469
   125
  have "f ?a = ?a"
wenzelm@25469
   126
  proof -
wenzelm@25469
   127
    have ge: "f ?a \<sqsubseteq> ?a"
wenzelm@25469
   128
    proof
wenzelm@25469
   129
      fix x assume x: "x \<in> ?H"
wenzelm@25469
   130
      then have "?a \<sqsubseteq> x" ..
wenzelm@25469
   131
      then have "f ?a \<sqsubseteq> f x" by (rule mono)
wenzelm@25469
   132
      also from x have "... \<sqsubseteq> x" ..
wenzelm@25469
   133
      finally show "f ?a \<sqsubseteq> x" .
wenzelm@25469
   134
    qed
wenzelm@25469
   135
    also have "?a \<sqsubseteq> f ?a"
wenzelm@25469
   136
    proof
wenzelm@25469
   137
      from ge have "f (f ?a) \<sqsubseteq> f ?a" by (rule mono)
wenzelm@25469
   138
      then show "f ?a \<in> ?H" ..
wenzelm@25469
   139
    qed
wenzelm@25469
   140
    finally show ?thesis .
wenzelm@10157
   141
  qed
wenzelm@25469
   142
  moreover {
wenzelm@25469
   143
    fix a'
wenzelm@25469
   144
    assume "f a' = a'"
wenzelm@25469
   145
    then have "f a' \<sqsubseteq> a'" by (simp only: leq_refl)
wenzelm@25469
   146
    then have "a' \<in> ?H" ..
wenzelm@25469
   147
    then have "?a \<sqsubseteq> a'" ..
wenzelm@25469
   148
  }
wenzelm@25469
   149
  ultimately show ?thesis by blast
wenzelm@25469
   150
qed
wenzelm@25469
   151
wenzelm@25469
   152
wenzelm@25469
   153
theorem Knaster_Tarski_dual:
wenzelm@25469
   154
  assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
wenzelm@25469
   155
  shows "\<exists>a::'a::complete_lattice. f a = a \<and> (\<forall>a'. f a' = a' \<longrightarrow> a' \<sqsubseteq> a)"
wenzelm@25469
   156
proof -
wenzelm@25469
   157
  let ?H = "{u. u \<sqsubseteq> f u}"
wenzelm@25469
   158
  let ?a = "\<Squnion>?H"
wenzelm@25469
   159
  have "f ?a = ?a"
wenzelm@25469
   160
  proof -
wenzelm@25469
   161
    have le: "?a \<sqsubseteq> f ?a"
wenzelm@25469
   162
    proof
wenzelm@25469
   163
      fix x assume x: "x \<in> ?H"
wenzelm@25469
   164
      then have "x \<sqsubseteq> f x" ..
wenzelm@25469
   165
      also from x have "x \<sqsubseteq> ?a" ..
wenzelm@25469
   166
      then have "f x \<sqsubseteq> f ?a" by (rule mono)
wenzelm@25469
   167
      finally show "x \<sqsubseteq> f ?a" .
wenzelm@25469
   168
    qed
wenzelm@25469
   169
    have "f ?a \<sqsubseteq> ?a"
wenzelm@25469
   170
    proof
wenzelm@25469
   171
      from le have "f ?a \<sqsubseteq> f (f ?a)" by (rule mono)
wenzelm@25469
   172
      then show "f ?a \<in> ?H" ..
wenzelm@25469
   173
    qed
wenzelm@25469
   174
    from this and le show ?thesis by (rule leq_antisym)
wenzelm@10157
   175
  qed
wenzelm@25469
   176
  moreover {
wenzelm@25469
   177
    fix a'
wenzelm@25469
   178
    assume "f a' = a'"
wenzelm@25469
   179
    then have "a' \<sqsubseteq> f a'" by (simp only: leq_refl)
wenzelm@25469
   180
    then have "a' \<in> ?H" ..
wenzelm@25469
   181
    then have "a' \<sqsubseteq> ?a" ..
wenzelm@25469
   182
  }
wenzelm@25469
   183
  ultimately show ?thesis by blast
wenzelm@10157
   184
qed
wenzelm@10157
   185
wenzelm@10157
   186
wenzelm@10157
   187
subsection {* Bottom and top elements *}
wenzelm@10157
   188
wenzelm@10157
   189
text {*
wenzelm@10157
   190
  With general bounds available, complete lattices also have least and
wenzelm@10157
   191
  greatest elements.
wenzelm@10157
   192
*}
wenzelm@10157
   193
wenzelm@19736
   194
definition
wenzelm@25469
   195
  bottom :: "'a::complete_lattice"  ("\<bottom>") where
wenzelm@19736
   196
  "\<bottom> = \<Sqinter>UNIV"
wenzelm@25469
   197
wenzelm@21404
   198
definition
wenzelm@25469
   199
  top :: "'a::complete_lattice"  ("\<top>") where
wenzelm@19736
   200
  "\<top> = \<Squnion>UNIV"
wenzelm@10157
   201
wenzelm@10157
   202
lemma bottom_least [intro?]: "\<bottom> \<sqsubseteq> x"
wenzelm@10157
   203
proof (unfold bottom_def)
wenzelm@10157
   204
  have "x \<in> UNIV" ..
wenzelm@23373
   205
  then show "\<Sqinter>UNIV \<sqsubseteq> x" ..
wenzelm@10157
   206
qed
wenzelm@10157
   207
wenzelm@10157
   208
lemma bottomI [intro?]: "(\<And>a. x \<sqsubseteq> a) \<Longrightarrow> \<bottom> = x"
wenzelm@10157
   209
proof (unfold bottom_def)
wenzelm@10157
   210
  assume "\<And>a. x \<sqsubseteq> a"
wenzelm@10157
   211
  show "\<Sqinter>UNIV = x"
wenzelm@10157
   212
  proof
wenzelm@23373
   213
    fix a show "x \<sqsubseteq> a" by fact
wenzelm@10157
   214
  next
wenzelm@10157
   215
    fix b :: "'a::complete_lattice"
wenzelm@10157
   216
    assume b: "\<forall>a \<in> UNIV. b \<sqsubseteq> a"
wenzelm@10157
   217
    have "x \<in> UNIV" ..
wenzelm@10157
   218
    with b show "b \<sqsubseteq> x" ..
wenzelm@10157
   219
  qed
wenzelm@10157
   220
qed
wenzelm@10157
   221
wenzelm@10157
   222
lemma top_greatest [intro?]: "x \<sqsubseteq> \<top>"
wenzelm@10157
   223
proof (unfold top_def)
wenzelm@10157
   224
  have "x \<in> UNIV" ..
wenzelm@23373
   225
  then show "x \<sqsubseteq> \<Squnion>UNIV" ..
wenzelm@10157
   226
qed
wenzelm@10157
   227
wenzelm@10157
   228
lemma topI [intro?]: "(\<And>a. a \<sqsubseteq> x) \<Longrightarrow> \<top> = x"
wenzelm@10157
   229
proof (unfold top_def)
wenzelm@10157
   230
  assume "\<And>a. a \<sqsubseteq> x"
wenzelm@10157
   231
  show "\<Squnion>UNIV = x"
wenzelm@10157
   232
  proof
wenzelm@23373
   233
    fix a show "a \<sqsubseteq> x" by fact
wenzelm@10157
   234
  next
wenzelm@10157
   235
    fix b :: "'a::complete_lattice"
wenzelm@10157
   236
    assume b: "\<forall>a \<in> UNIV. a \<sqsubseteq> b"
wenzelm@10157
   237
    have "x \<in> UNIV" ..
wenzelm@10157
   238
    with b show "x \<sqsubseteq> b" ..
wenzelm@10157
   239
  qed
wenzelm@10157
   240
qed
wenzelm@10157
   241
wenzelm@10157
   242
wenzelm@10157
   243
subsection {* Duality *}
wenzelm@10157
   244
wenzelm@10157
   245
text {*
wenzelm@10157
   246
  The class of complete lattices is closed under formation of dual
wenzelm@10157
   247
  structures.
wenzelm@10157
   248
*}
wenzelm@10157
   249
wenzelm@10157
   250
instance dual :: (complete_lattice) complete_lattice
wenzelm@10309
   251
proof
wenzelm@10157
   252
  fix A' :: "'a::complete_lattice dual set"
wenzelm@10157
   253
  show "\<exists>inf'. is_Inf A' inf'"
wenzelm@10157
   254
  proof -
nipkow@10834
   255
    have "\<exists>sup. is_Sup (undual ` A') sup" by (rule ex_Sup)
wenzelm@23373
   256
    then have "\<exists>sup. is_Inf (dual ` undual ` A') (dual sup)" by (simp only: dual_Inf)
wenzelm@23373
   257
    then show ?thesis by (simp add: dual_ex [symmetric] image_compose [symmetric])
wenzelm@10157
   258
  qed
wenzelm@10157
   259
qed
wenzelm@10157
   260
wenzelm@10157
   261
text {*
wenzelm@10157
   262
  Apparently, the @{text \<Sqinter>} and @{text \<Squnion>} operations are dual to each
wenzelm@10157
   263
  other.
wenzelm@10157
   264
*}
wenzelm@10157
   265
nipkow@10834
   266
theorem dual_Meet [intro?]: "dual (\<Sqinter>A) = \<Squnion>(dual ` A)"
wenzelm@10157
   267
proof -
nipkow@10834
   268
  from is_Inf_Meet have "is_Sup (dual ` A) (dual (\<Sqinter>A))" ..
wenzelm@23373
   269
  then have "\<Squnion>(dual ` A) = dual (\<Sqinter>A)" ..
wenzelm@23373
   270
  then show ?thesis ..
wenzelm@10157
   271
qed
wenzelm@10157
   272
nipkow@10834
   273
theorem dual_Join [intro?]: "dual (\<Squnion>A) = \<Sqinter>(dual ` A)"
wenzelm@10157
   274
proof -
nipkow@10834
   275
  from is_Sup_Join have "is_Inf (dual ` A) (dual (\<Squnion>A))" ..
wenzelm@23373
   276
  then have "\<Sqinter>(dual ` A) = dual (\<Squnion>A)" ..
wenzelm@23373
   277
  then show ?thesis ..
wenzelm@10157
   278
qed
wenzelm@10157
   279
wenzelm@10157
   280
text {*
wenzelm@10157
   281
  Likewise are @{text \<bottom>} and @{text \<top>} duals of each other.
wenzelm@10157
   282
*}
wenzelm@10157
   283
wenzelm@10157
   284
theorem dual_bottom [intro?]: "dual \<bottom> = \<top>"
wenzelm@10157
   285
proof -
wenzelm@10157
   286
  have "\<top> = dual \<bottom>"
wenzelm@10157
   287
  proof
wenzelm@10157
   288
    fix a' have "\<bottom> \<sqsubseteq> undual a'" ..
wenzelm@23373
   289
    then have "dual (undual a') \<sqsubseteq> dual \<bottom>" ..
wenzelm@23373
   290
    then show "a' \<sqsubseteq> dual \<bottom>" by simp
wenzelm@10157
   291
  qed
wenzelm@23373
   292
  then show ?thesis ..
wenzelm@10157
   293
qed
wenzelm@10157
   294
wenzelm@10157
   295
theorem dual_top [intro?]: "dual \<top> = \<bottom>"
wenzelm@10157
   296
proof -
wenzelm@10157
   297
  have "\<bottom> = dual \<top>"
wenzelm@10157
   298
  proof
wenzelm@10157
   299
    fix a' have "undual a' \<sqsubseteq> \<top>" ..
wenzelm@23373
   300
    then have "dual \<top> \<sqsubseteq> dual (undual a')" ..
wenzelm@23373
   301
    then show "dual \<top> \<sqsubseteq> a'" by simp
wenzelm@10157
   302
  qed
wenzelm@23373
   303
  then show ?thesis ..
wenzelm@10157
   304
qed
wenzelm@10157
   305
wenzelm@10157
   306
wenzelm@10157
   307
subsection {* Complete lattices are lattices *}
wenzelm@10157
   308
wenzelm@10157
   309
text {*
wenzelm@10176
   310
  Complete lattices (with general bounds available) are indeed plain
wenzelm@10157
   311
  lattices as well.  This holds due to the connection of general
wenzelm@10157
   312
  versus binary bounds that has been formally established in
wenzelm@10157
   313
  \S\ref{sec:gen-bin-bounds}.
wenzelm@10157
   314
*}
wenzelm@10157
   315
wenzelm@10157
   316
lemma is_inf_binary: "is_inf x y (\<Sqinter>{x, y})"
wenzelm@10157
   317
proof -
wenzelm@10157
   318
  have "is_Inf {x, y} (\<Sqinter>{x, y})" ..
wenzelm@23373
   319
  then show ?thesis by (simp only: is_Inf_binary)
wenzelm@10157
   320
qed
wenzelm@10157
   321
wenzelm@10157
   322
lemma is_sup_binary: "is_sup x y (\<Squnion>{x, y})"
wenzelm@10157
   323
proof -
wenzelm@10157
   324
  have "is_Sup {x, y} (\<Squnion>{x, y})" ..
wenzelm@23373
   325
  then show ?thesis by (simp only: is_Sup_binary)
wenzelm@10157
   326
qed
wenzelm@10157
   327
wenzelm@11099
   328
instance complete_lattice \<subseteq> lattice
wenzelm@10309
   329
proof
wenzelm@10157
   330
  fix x y :: "'a::complete_lattice"
wenzelm@10157
   331
  from is_inf_binary show "\<exists>inf. is_inf x y inf" ..
wenzelm@10157
   332
  from is_sup_binary show "\<exists>sup. is_sup x y sup" ..
wenzelm@10157
   333
qed
wenzelm@10157
   334
wenzelm@10157
   335
theorem meet_binary: "x \<sqinter> y = \<Sqinter>{x, y}"
wenzelm@10157
   336
  by (rule meet_equality) (rule is_inf_binary)
wenzelm@10157
   337
wenzelm@10157
   338
theorem join_binary: "x \<squnion> y = \<Squnion>{x, y}"
wenzelm@10157
   339
  by (rule join_equality) (rule is_sup_binary)
wenzelm@10157
   340
wenzelm@10157
   341
wenzelm@10157
   342
subsection {* Complete lattices and set-theory operations *}
wenzelm@10157
   343
wenzelm@10157
   344
text {*
wenzelm@10157
   345
  The complete lattice operations are (anti) monotone wrt.\ set
wenzelm@10157
   346
  inclusion.
wenzelm@10157
   347
*}
wenzelm@10157
   348
wenzelm@10157
   349
theorem Meet_subset_antimono: "A \<subseteq> B \<Longrightarrow> \<Sqinter>B \<sqsubseteq> \<Sqinter>A"
wenzelm@10157
   350
proof (rule Meet_greatest)
wenzelm@10157
   351
  fix a assume "a \<in> A"
wenzelm@10157
   352
  also assume "A \<subseteq> B"
wenzelm@10157
   353
  finally have "a \<in> B" .
wenzelm@23373
   354
  then show "\<Sqinter>B \<sqsubseteq> a" ..
wenzelm@10157
   355
qed
wenzelm@10157
   356
wenzelm@10157
   357
theorem Join_subset_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<sqsubseteq> \<Squnion>B"
wenzelm@10157
   358
proof -
wenzelm@10157
   359
  assume "A \<subseteq> B"
wenzelm@23373
   360
  then have "dual ` A \<subseteq> dual ` B" by blast
wenzelm@23373
   361
  then have "\<Sqinter>(dual ` B) \<sqsubseteq> \<Sqinter>(dual ` A)" by (rule Meet_subset_antimono)
wenzelm@23373
   362
  then have "dual (\<Squnion>B) \<sqsubseteq> dual (\<Squnion>A)" by (simp only: dual_Join)
wenzelm@23373
   363
  then show ?thesis by (simp only: dual_leq)
wenzelm@10157
   364
qed
wenzelm@10157
   365
wenzelm@10157
   366
text {*
wenzelm@10157
   367
  Bounds over unions of sets may be obtained separately.
wenzelm@10157
   368
*}
wenzelm@10157
   369
wenzelm@10157
   370
theorem Meet_Un: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
wenzelm@10157
   371
proof
wenzelm@10157
   372
  fix a assume "a \<in> A \<union> B"
wenzelm@23373
   373
  then show "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> a"
wenzelm@10157
   374
  proof
wenzelm@10157
   375
    assume a: "a \<in> A"
wenzelm@10157
   376
    have "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> \<Sqinter>A" ..
wenzelm@10157
   377
    also from a have "\<dots> \<sqsubseteq> a" ..
wenzelm@10157
   378
    finally show ?thesis .
wenzelm@10157
   379
  next
wenzelm@10157
   380
    assume a: "a \<in> B"
wenzelm@10157
   381
    have "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> \<Sqinter>B" ..
wenzelm@10157
   382
    also from a have "\<dots> \<sqsubseteq> a" ..
wenzelm@10157
   383
    finally show ?thesis .
wenzelm@10157
   384
  qed
wenzelm@10157
   385
next
wenzelm@10157
   386
  fix b assume b: "\<forall>a \<in> A \<union> B. b \<sqsubseteq> a"
wenzelm@10157
   387
  show "b \<sqsubseteq> \<Sqinter>A \<sqinter> \<Sqinter>B"
wenzelm@10157
   388
  proof
wenzelm@10157
   389
    show "b \<sqsubseteq> \<Sqinter>A"
wenzelm@10157
   390
    proof
wenzelm@10157
   391
      fix a assume "a \<in> A"
wenzelm@23373
   392
      then have "a \<in>  A \<union> B" ..
wenzelm@10157
   393
      with b show "b \<sqsubseteq> a" ..
wenzelm@10157
   394
    qed
wenzelm@10157
   395
    show "b \<sqsubseteq> \<Sqinter>B"
wenzelm@10157
   396
    proof
wenzelm@10157
   397
      fix a assume "a \<in> B"
wenzelm@23373
   398
      then have "a \<in>  A \<union> B" ..
wenzelm@10157
   399
      with b show "b \<sqsubseteq> a" ..
wenzelm@10157
   400
    qed
wenzelm@10157
   401
  qed
wenzelm@10157
   402
qed
wenzelm@10157
   403
wenzelm@10157
   404
theorem Join_Un: "\<Squnion>(A \<union> B) = \<Squnion>A \<squnion> \<Squnion>B"
wenzelm@10157
   405
proof -
nipkow@10834
   406
  have "dual (\<Squnion>(A \<union> B)) = \<Sqinter>(dual ` A \<union> dual ` B)"
wenzelm@10157
   407
    by (simp only: dual_Join image_Un)
nipkow@10834
   408
  also have "\<dots> = \<Sqinter>(dual ` A) \<sqinter> \<Sqinter>(dual ` B)"
wenzelm@10157
   409
    by (rule Meet_Un)
wenzelm@10157
   410
  also have "\<dots> = dual (\<Squnion>A \<squnion> \<Squnion>B)"
wenzelm@10157
   411
    by (simp only: dual_join dual_Join)
wenzelm@10157
   412
  finally show ?thesis ..
wenzelm@10157
   413
qed
wenzelm@10157
   414
wenzelm@10157
   415
text {*
wenzelm@10157
   416
  Bounds over singleton sets are trivial.
wenzelm@10157
   417
*}
wenzelm@10157
   418
wenzelm@10157
   419
theorem Meet_singleton: "\<Sqinter>{x} = x"
wenzelm@10157
   420
proof
wenzelm@10157
   421
  fix a assume "a \<in> {x}"
wenzelm@23373
   422
  then have "a = x" by simp
wenzelm@23373
   423
  then show "x \<sqsubseteq> a" by (simp only: leq_refl)
wenzelm@10157
   424
next
wenzelm@10157
   425
  fix b assume "\<forall>a \<in> {x}. b \<sqsubseteq> a"
wenzelm@23373
   426
  then show "b \<sqsubseteq> x" by simp
wenzelm@10157
   427
qed
wenzelm@10157
   428
wenzelm@10157
   429
theorem Join_singleton: "\<Squnion>{x} = x"
wenzelm@10157
   430
proof -
wenzelm@10157
   431
  have "dual (\<Squnion>{x}) = \<Sqinter>{dual x}" by (simp add: dual_Join)
wenzelm@10157
   432
  also have "\<dots> = dual x" by (rule Meet_singleton)
wenzelm@10157
   433
  finally show ?thesis ..
wenzelm@10157
   434
qed
wenzelm@10157
   435
wenzelm@10157
   436
text {*
wenzelm@10157
   437
  Bounds over the empty and universal set correspond to each other.
wenzelm@10157
   438
*}
wenzelm@10157
   439
wenzelm@10157
   440
theorem Meet_empty: "\<Sqinter>{} = \<Squnion>UNIV"
wenzelm@10157
   441
proof
wenzelm@10157
   442
  fix a :: "'a::complete_lattice"
wenzelm@10157
   443
  assume "a \<in> {}"
wenzelm@23373
   444
  then have False by simp
wenzelm@23373
   445
  then show "\<Squnion>UNIV \<sqsubseteq> a" ..
wenzelm@10157
   446
next
wenzelm@10157
   447
  fix b :: "'a::complete_lattice"
wenzelm@10157
   448
  have "b \<in> UNIV" ..
wenzelm@23373
   449
  then show "b \<sqsubseteq> \<Squnion>UNIV" ..
wenzelm@10157
   450
qed
wenzelm@10157
   451
wenzelm@10157
   452
theorem Join_empty: "\<Squnion>{} = \<Sqinter>UNIV"
wenzelm@10157
   453
proof -
wenzelm@10157
   454
  have "dual (\<Squnion>{}) = \<Sqinter>{}" by (simp add: dual_Join)
wenzelm@10157
   455
  also have "\<dots> = \<Squnion>UNIV" by (rule Meet_empty)
wenzelm@10157
   456
  also have "\<dots> = dual (\<Sqinter>UNIV)" by (simp add: dual_Meet)
wenzelm@10157
   457
  finally show ?thesis ..
wenzelm@10157
   458
qed
wenzelm@10157
   459
wenzelm@10157
   460
end