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