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