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