src/HOL/Lattice/Bounds.thy
author haftmann
Fri Jun 17 16:12:49 2005 +0200 (2005-06-17)
changeset 16417 9bc16273c2d4
parent 11265 4f2e6c87a57f
child 19736 d8d0f8f51d69
permissions -rw-r--r--
migrated theory headers to new format
wenzelm@10157
     1
(*  Title:      HOL/Lattice/Bounds.thy
wenzelm@10157
     2
    ID:         $Id$
wenzelm@10157
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@10157
     4
*)
wenzelm@10157
     5
wenzelm@10157
     6
header {* Bounds *}
wenzelm@10157
     7
haftmann@16417
     8
theory Bounds imports Orders begin
wenzelm@10157
     9
wenzelm@10157
    10
subsection {* Infimum and supremum *}
wenzelm@10157
    11
wenzelm@10157
    12
text {*
wenzelm@10157
    13
  Given a partial order, we define infimum (greatest lower bound) and
wenzelm@10157
    14
  supremum (least upper bound) wrt.\ @{text \<sqsubseteq>} for two and for any
wenzelm@10157
    15
  number of elements.
wenzelm@10157
    16
*}
wenzelm@10157
    17
wenzelm@10157
    18
constdefs
wenzelm@10157
    19
  is_inf :: "'a::partial_order \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
wenzelm@10157
    20
  "is_inf x y inf \<equiv> inf \<sqsubseteq> x \<and> inf \<sqsubseteq> y \<and> (\<forall>z. z \<sqsubseteq> x \<and> z \<sqsubseteq> y \<longrightarrow> z \<sqsubseteq> inf)"
wenzelm@10157
    21
wenzelm@10157
    22
  is_sup :: "'a::partial_order \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
wenzelm@10157
    23
  "is_sup x y sup \<equiv> x \<sqsubseteq> sup \<and> y \<sqsubseteq> sup \<and> (\<forall>z. x \<sqsubseteq> z \<and> y \<sqsubseteq> z \<longrightarrow> sup \<sqsubseteq> z)"
wenzelm@10157
    24
wenzelm@10157
    25
  is_Inf :: "'a::partial_order set \<Rightarrow> 'a \<Rightarrow> bool"
wenzelm@10157
    26
  "is_Inf A inf \<equiv> (\<forall>x \<in> A. inf \<sqsubseteq> x) \<and> (\<forall>z. (\<forall>x \<in> A. z \<sqsubseteq> x) \<longrightarrow> z \<sqsubseteq> inf)"
wenzelm@10157
    27
wenzelm@10157
    28
  is_Sup :: "'a::partial_order set \<Rightarrow> 'a \<Rightarrow> bool"
wenzelm@10157
    29
  "is_Sup A sup \<equiv> (\<forall>x \<in> A. x \<sqsubseteq> sup) \<and> (\<forall>z. (\<forall>x \<in> A. x \<sqsubseteq> z) \<longrightarrow> sup \<sqsubseteq> z)"
wenzelm@10157
    30
wenzelm@10157
    31
text {*
wenzelm@10157
    32
  These definitions entail the following basic properties of boundary
wenzelm@10157
    33
  elements.
wenzelm@10157
    34
*}
wenzelm@10157
    35
wenzelm@10157
    36
lemma is_infI [intro?]: "inf \<sqsubseteq> x \<Longrightarrow> inf \<sqsubseteq> y \<Longrightarrow>
wenzelm@10157
    37
    (\<And>z. z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> inf) \<Longrightarrow> is_inf x y inf"
wenzelm@10157
    38
  by (unfold is_inf_def) blast
wenzelm@10157
    39
wenzelm@10157
    40
lemma is_inf_greatest [elim?]:
wenzelm@10157
    41
    "is_inf x y inf \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> inf"
wenzelm@10157
    42
  by (unfold is_inf_def) blast
wenzelm@10157
    43
wenzelm@10157
    44
lemma is_inf_lower [elim?]:
wenzelm@10157
    45
    "is_inf x y inf \<Longrightarrow> (inf \<sqsubseteq> x \<Longrightarrow> inf \<sqsubseteq> y \<Longrightarrow> C) \<Longrightarrow> C"
wenzelm@10157
    46
  by (unfold is_inf_def) blast
wenzelm@10157
    47
wenzelm@10157
    48
wenzelm@10157
    49
lemma is_supI [intro?]: "x \<sqsubseteq> sup \<Longrightarrow> y \<sqsubseteq> sup \<Longrightarrow>
wenzelm@10157
    50
    (\<And>z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> sup \<sqsubseteq> z) \<Longrightarrow> is_sup x y sup"
wenzelm@10157
    51
  by (unfold is_sup_def) blast
wenzelm@10157
    52
wenzelm@10157
    53
lemma is_sup_least [elim?]:
wenzelm@10157
    54
    "is_sup x y sup \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> sup \<sqsubseteq> z"
wenzelm@10157
    55
  by (unfold is_sup_def) blast
wenzelm@10157
    56
wenzelm@10157
    57
lemma is_sup_upper [elim?]:
wenzelm@10157
    58
    "is_sup x y sup \<Longrightarrow> (x \<sqsubseteq> sup \<Longrightarrow> y \<sqsubseteq> sup \<Longrightarrow> C) \<Longrightarrow> C"
wenzelm@10157
    59
  by (unfold is_sup_def) blast
wenzelm@10157
    60
wenzelm@10157
    61
wenzelm@10157
    62
lemma is_InfI [intro?]: "(\<And>x. x \<in> A \<Longrightarrow> inf \<sqsubseteq> x) \<Longrightarrow>
wenzelm@10157
    63
    (\<And>z. (\<forall>x \<in> A. z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> inf) \<Longrightarrow> is_Inf A inf"
wenzelm@10157
    64
  by (unfold is_Inf_def) blast
wenzelm@10157
    65
wenzelm@10157
    66
lemma is_Inf_greatest [elim?]:
wenzelm@10157
    67
    "is_Inf A inf \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> inf"
wenzelm@10157
    68
  by (unfold is_Inf_def) blast
wenzelm@10157
    69
wenzelm@10157
    70
lemma is_Inf_lower [dest?]:
wenzelm@10157
    71
    "is_Inf A inf \<Longrightarrow> x \<in> A \<Longrightarrow> inf \<sqsubseteq> x"
wenzelm@10157
    72
  by (unfold is_Inf_def) blast
wenzelm@10157
    73
wenzelm@10157
    74
wenzelm@10157
    75
lemma is_SupI [intro?]: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> sup) \<Longrightarrow>
wenzelm@10157
    76
    (\<And>z. (\<forall>x \<in> A. x \<sqsubseteq> z) \<Longrightarrow> sup \<sqsubseteq> z) \<Longrightarrow> is_Sup A sup"
wenzelm@10157
    77
  by (unfold is_Sup_def) blast
wenzelm@10157
    78
wenzelm@10157
    79
lemma is_Sup_least [elim?]:
wenzelm@10157
    80
    "is_Sup A sup \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> sup \<sqsubseteq> z"
wenzelm@10157
    81
  by (unfold is_Sup_def) blast
wenzelm@10157
    82
wenzelm@10157
    83
lemma is_Sup_upper [dest?]:
wenzelm@10157
    84
    "is_Sup A sup \<Longrightarrow> x \<in> A \<Longrightarrow> x \<sqsubseteq> sup"
wenzelm@10157
    85
  by (unfold is_Sup_def) blast
wenzelm@10157
    86
wenzelm@10157
    87
wenzelm@10157
    88
subsection {* Duality *}
wenzelm@10157
    89
wenzelm@10157
    90
text {*
wenzelm@10157
    91
  Infimum and supremum are dual to each other.
wenzelm@10157
    92
*}
wenzelm@10157
    93
wenzelm@10157
    94
theorem dual_inf [iff?]:
wenzelm@10157
    95
    "is_inf (dual x) (dual y) (dual sup) = is_sup x y sup"
wenzelm@10157
    96
  by (simp add: is_inf_def is_sup_def dual_all [symmetric] dual_leq)
wenzelm@10157
    97
wenzelm@10157
    98
theorem dual_sup [iff?]:
wenzelm@10157
    99
    "is_sup (dual x) (dual y) (dual inf) = is_inf x y inf"
wenzelm@10157
   100
  by (simp add: is_inf_def is_sup_def dual_all [symmetric] dual_leq)
wenzelm@10157
   101
wenzelm@10157
   102
theorem dual_Inf [iff?]:
nipkow@10834
   103
    "is_Inf (dual ` A) (dual sup) = is_Sup A sup"
wenzelm@10157
   104
  by (simp add: is_Inf_def is_Sup_def dual_all [symmetric] dual_leq)
wenzelm@10157
   105
wenzelm@10157
   106
theorem dual_Sup [iff?]:
nipkow@10834
   107
    "is_Sup (dual ` A) (dual inf) = is_Inf A inf"
wenzelm@10157
   108
  by (simp add: is_Inf_def is_Sup_def dual_all [symmetric] dual_leq)
wenzelm@10157
   109
wenzelm@10157
   110
wenzelm@10157
   111
subsection {* Uniqueness *}
wenzelm@10157
   112
wenzelm@10157
   113
text {*
wenzelm@10157
   114
  Infima and suprema on partial orders are unique; this is mainly due
wenzelm@10157
   115
  to anti-symmetry of the underlying relation.
wenzelm@10157
   116
*}
wenzelm@10157
   117
wenzelm@10157
   118
theorem is_inf_uniq: "is_inf x y inf \<Longrightarrow> is_inf x y inf' \<Longrightarrow> inf = inf'"
wenzelm@10157
   119
proof -
wenzelm@10157
   120
  assume inf: "is_inf x y inf"
wenzelm@10157
   121
  assume inf': "is_inf x y inf'"
wenzelm@10157
   122
  show ?thesis
wenzelm@10157
   123
  proof (rule leq_antisym)
wenzelm@10157
   124
    from inf' show "inf \<sqsubseteq> inf'"
wenzelm@10157
   125
    proof (rule is_inf_greatest)
wenzelm@10157
   126
      from inf show "inf \<sqsubseteq> x" ..
wenzelm@10157
   127
      from inf show "inf \<sqsubseteq> y" ..
wenzelm@10157
   128
    qed
wenzelm@10157
   129
    from inf show "inf' \<sqsubseteq> inf"
wenzelm@10157
   130
    proof (rule is_inf_greatest)
wenzelm@10157
   131
      from inf' show "inf' \<sqsubseteq> x" ..
wenzelm@10157
   132
      from inf' show "inf' \<sqsubseteq> y" ..
wenzelm@10157
   133
    qed
wenzelm@10157
   134
  qed
wenzelm@10157
   135
qed
wenzelm@10157
   136
wenzelm@10157
   137
theorem is_sup_uniq: "is_sup x y sup \<Longrightarrow> is_sup x y sup' \<Longrightarrow> sup = sup'"
wenzelm@10157
   138
proof -
wenzelm@10157
   139
  assume sup: "is_sup x y sup" and sup': "is_sup x y sup'"
wenzelm@10157
   140
  have "dual sup = dual sup'"
wenzelm@10157
   141
  proof (rule is_inf_uniq)
wenzelm@10157
   142
    from sup show "is_inf (dual x) (dual y) (dual sup)" ..
wenzelm@10157
   143
    from sup' show "is_inf (dual x) (dual y) (dual sup')" ..
wenzelm@10157
   144
  qed
wenzelm@10157
   145
  thus "sup = sup'" ..
wenzelm@10157
   146
qed
wenzelm@10157
   147
wenzelm@10157
   148
theorem is_Inf_uniq: "is_Inf A inf \<Longrightarrow> is_Inf A inf' \<Longrightarrow> inf = inf'"
wenzelm@10157
   149
proof -
wenzelm@10157
   150
  assume inf: "is_Inf A inf"
wenzelm@10157
   151
  assume inf': "is_Inf A inf'"
wenzelm@10157
   152
  show ?thesis
wenzelm@10157
   153
  proof (rule leq_antisym)
wenzelm@10157
   154
    from inf' show "inf \<sqsubseteq> inf'"
wenzelm@10157
   155
    proof (rule is_Inf_greatest)
wenzelm@10157
   156
      fix x assume "x \<in> A"
wenzelm@10157
   157
      from inf show "inf \<sqsubseteq> x" ..
wenzelm@10157
   158
    qed
wenzelm@10157
   159
    from inf show "inf' \<sqsubseteq> inf"
wenzelm@10157
   160
    proof (rule is_Inf_greatest)
wenzelm@10157
   161
      fix x assume "x \<in> A"
wenzelm@10157
   162
      from inf' show "inf' \<sqsubseteq> x" ..
wenzelm@10157
   163
    qed
wenzelm@10157
   164
  qed
wenzelm@10157
   165
qed
wenzelm@10157
   166
wenzelm@10157
   167
theorem is_Sup_uniq: "is_Sup A sup \<Longrightarrow> is_Sup A sup' \<Longrightarrow> sup = sup'"
wenzelm@10157
   168
proof -
wenzelm@10157
   169
  assume sup: "is_Sup A sup" and sup': "is_Sup A sup'"
wenzelm@10157
   170
  have "dual sup = dual sup'"
wenzelm@10157
   171
  proof (rule is_Inf_uniq)
nipkow@10834
   172
    from sup show "is_Inf (dual ` A) (dual sup)" ..
nipkow@10834
   173
    from sup' show "is_Inf (dual ` A) (dual sup')" ..
wenzelm@10157
   174
  qed
wenzelm@10157
   175
  thus "sup = sup'" ..
wenzelm@10157
   176
qed
wenzelm@10157
   177
wenzelm@10157
   178
wenzelm@10157
   179
subsection {* Related elements *}
wenzelm@10157
   180
wenzelm@10157
   181
text {*
wenzelm@10157
   182
  The binary bound of related elements is either one of the argument.
wenzelm@10157
   183
*}
wenzelm@10157
   184
wenzelm@10157
   185
theorem is_inf_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> is_inf x y x"
wenzelm@10157
   186
proof -
wenzelm@10157
   187
  assume "x \<sqsubseteq> y"
wenzelm@10157
   188
  show ?thesis
wenzelm@10157
   189
  proof
wenzelm@10157
   190
    show "x \<sqsubseteq> x" ..
wenzelm@10157
   191
    show "x \<sqsubseteq> y" .
wenzelm@10157
   192
    fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" show "z \<sqsubseteq> x" .
wenzelm@10157
   193
  qed
wenzelm@10157
   194
qed
wenzelm@10157
   195
wenzelm@10157
   196
theorem is_sup_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> is_sup x y y"
wenzelm@10157
   197
proof -
wenzelm@10157
   198
  assume "x \<sqsubseteq> y"
wenzelm@10157
   199
  show ?thesis
wenzelm@10157
   200
  proof
wenzelm@10157
   201
    show "x \<sqsubseteq> y" .
wenzelm@10157
   202
    show "y \<sqsubseteq> y" ..
wenzelm@10157
   203
    fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z"
wenzelm@10157
   204
    show "y \<sqsubseteq> z" .
wenzelm@10157
   205
  qed
wenzelm@10157
   206
qed
wenzelm@10157
   207
wenzelm@10157
   208
wenzelm@10157
   209
subsection {* General versus binary bounds \label{sec:gen-bin-bounds} *}
wenzelm@10157
   210
wenzelm@10157
   211
text {*
wenzelm@10157
   212
  General bounds of two-element sets coincide with binary bounds.
wenzelm@10157
   213
*}
wenzelm@10157
   214
wenzelm@10157
   215
theorem is_Inf_binary: "is_Inf {x, y} inf = is_inf x y inf"
wenzelm@10157
   216
proof -
wenzelm@10157
   217
  let ?A = "{x, y}"
wenzelm@10157
   218
  show ?thesis
wenzelm@10157
   219
  proof
wenzelm@10157
   220
    assume is_Inf: "is_Inf ?A inf"
wenzelm@10157
   221
    show "is_inf x y inf"
wenzelm@10157
   222
    proof
wenzelm@10157
   223
      have "x \<in> ?A" by simp
wenzelm@10157
   224
      with is_Inf show "inf \<sqsubseteq> x" ..
wenzelm@10157
   225
      have "y \<in> ?A" by simp
wenzelm@10157
   226
      with is_Inf show "inf \<sqsubseteq> y" ..
wenzelm@10157
   227
      fix z assume zx: "z \<sqsubseteq> x" and zy: "z \<sqsubseteq> y"
wenzelm@10157
   228
      from is_Inf show "z \<sqsubseteq> inf"
wenzelm@10157
   229
      proof (rule is_Inf_greatest)
wenzelm@10157
   230
        fix a assume "a \<in> ?A"
wenzelm@10157
   231
        hence "a = x \<or> a = y" by blast
wenzelm@10157
   232
        thus "z \<sqsubseteq> a"
wenzelm@10157
   233
        proof
wenzelm@10157
   234
          assume "a = x"
wenzelm@10157
   235
          with zx show ?thesis by simp
wenzelm@10157
   236
        next
wenzelm@10157
   237
          assume "a = y"
wenzelm@10157
   238
          with zy show ?thesis by simp
wenzelm@10157
   239
        qed
wenzelm@10157
   240
      qed
wenzelm@10157
   241
    qed
wenzelm@10157
   242
  next
wenzelm@10157
   243
    assume is_inf: "is_inf x y inf"
wenzelm@10157
   244
    show "is_Inf {x, y} inf"
wenzelm@10157
   245
    proof
wenzelm@10157
   246
      fix a assume "a \<in> ?A"
wenzelm@10157
   247
      hence "a = x \<or> a = y" by blast
wenzelm@10157
   248
      thus "inf \<sqsubseteq> a"
wenzelm@10157
   249
      proof
wenzelm@10157
   250
        assume "a = x"
wenzelm@10157
   251
        also from is_inf have "inf \<sqsubseteq> x" ..
wenzelm@10157
   252
        finally show ?thesis .
wenzelm@10157
   253
      next
wenzelm@10157
   254
        assume "a = y"
wenzelm@10157
   255
        also from is_inf have "inf \<sqsubseteq> y" ..
wenzelm@10157
   256
        finally show ?thesis .
wenzelm@10157
   257
      qed
wenzelm@10157
   258
    next
wenzelm@10157
   259
      fix z assume z: "\<forall>a \<in> ?A. z \<sqsubseteq> a"
wenzelm@10157
   260
      from is_inf show "z \<sqsubseteq> inf"
wenzelm@10157
   261
      proof (rule is_inf_greatest)
wenzelm@10157
   262
        from z show "z \<sqsubseteq> x" by blast
wenzelm@10157
   263
        from z show "z \<sqsubseteq> y" by blast
wenzelm@10157
   264
      qed
wenzelm@10157
   265
    qed
wenzelm@10157
   266
  qed
wenzelm@10157
   267
qed
wenzelm@10157
   268
wenzelm@10157
   269
theorem is_Sup_binary: "is_Sup {x, y} sup = is_sup x y sup"
wenzelm@10157
   270
proof -
nipkow@10834
   271
  have "is_Sup {x, y} sup = is_Inf (dual ` {x, y}) (dual sup)"
wenzelm@10157
   272
    by (simp only: dual_Inf)
nipkow@10834
   273
  also have "dual ` {x, y} = {dual x, dual y}"
wenzelm@10157
   274
    by simp
wenzelm@10157
   275
  also have "is_Inf \<dots> (dual sup) = is_inf (dual x) (dual y) (dual sup)"
wenzelm@10157
   276
    by (rule is_Inf_binary)
wenzelm@10157
   277
  also have "\<dots> = is_sup x y sup"
wenzelm@10157
   278
    by (simp only: dual_inf)
wenzelm@10157
   279
  finally show ?thesis .
wenzelm@10157
   280
qed
wenzelm@10157
   281
wenzelm@10157
   282
wenzelm@10157
   283
subsection {* Connecting general bounds \label{sec:connect-bounds} *}
wenzelm@10157
   284
wenzelm@10157
   285
text {*
wenzelm@10157
   286
  Either kind of general bounds is sufficient to express the other.
wenzelm@10157
   287
  The least upper bound (supremum) is the same as the the greatest
wenzelm@10157
   288
  lower bound of the set of all upper bounds; the dual statements
wenzelm@10157
   289
  holds as well; the dual statement holds as well.
wenzelm@10157
   290
*}
wenzelm@10157
   291
wenzelm@10157
   292
theorem Inf_Sup: "is_Inf {b. \<forall>a \<in> A. a \<sqsubseteq> b} sup \<Longrightarrow> is_Sup A sup"
wenzelm@10157
   293
proof -
wenzelm@10157
   294
  let ?B = "{b. \<forall>a \<in> A. a \<sqsubseteq> b}"
wenzelm@10157
   295
  assume is_Inf: "is_Inf ?B sup"
wenzelm@10157
   296
  show "is_Sup A sup"
wenzelm@10157
   297
  proof
wenzelm@10157
   298
    fix x assume x: "x \<in> A"
wenzelm@10157
   299
    from is_Inf show "x \<sqsubseteq> sup"
wenzelm@10157
   300
    proof (rule is_Inf_greatest)
wenzelm@10157
   301
      fix y assume "y \<in> ?B"
wenzelm@10157
   302
      hence "\<forall>a \<in> A. a \<sqsubseteq> y" ..
wenzelm@10157
   303
      from this x show "x \<sqsubseteq> y" ..
wenzelm@10157
   304
    qed
wenzelm@10157
   305
  next
wenzelm@10157
   306
    fix z assume "\<forall>x \<in> A. x \<sqsubseteq> z"
wenzelm@10157
   307
    hence "z \<in> ?B" ..
wenzelm@10157
   308
    with is_Inf show "sup \<sqsubseteq> z" ..
wenzelm@10157
   309
  qed
wenzelm@10157
   310
qed
wenzelm@10157
   311
wenzelm@10157
   312
theorem Sup_Inf: "is_Sup {b. \<forall>a \<in> A. b \<sqsubseteq> a} inf \<Longrightarrow> is_Inf A inf"
wenzelm@10157
   313
proof -
wenzelm@10157
   314
  assume "is_Sup {b. \<forall>a \<in> A. b \<sqsubseteq> a} inf"
nipkow@10834
   315
  hence "is_Inf (dual ` {b. \<forall>a \<in> A. dual a \<sqsubseteq> dual b}) (dual inf)"
wenzelm@10157
   316
    by (simp only: dual_Inf dual_leq)
nipkow@10834
   317
  also have "dual ` {b. \<forall>a \<in> A. dual a \<sqsubseteq> dual b} = {b'. \<forall>a' \<in> dual ` A. a' \<sqsubseteq> b'}"
paulson@11265
   318
    by (auto iff: dual_ball dual_Collect simp add: image_Collect)  (* FIXME !? *)
wenzelm@10157
   319
  finally have "is_Inf \<dots> (dual inf)" .
nipkow@10834
   320
  hence "is_Sup (dual ` A) (dual inf)"
wenzelm@10157
   321
    by (rule Inf_Sup)
wenzelm@10157
   322
  thus ?thesis ..
wenzelm@10157
   323
qed
wenzelm@10157
   324
wenzelm@10157
   325
end