src/HOL/Conditional_Complete_Lattices.thy
author hoelzl
Tue Apr 09 14:13:13 2013 +0200 (2013-04-09)
changeset 51643 b6675f4549d8
parent 51518 6a56b7088a6a
permissions -rw-r--r--
fixed spelling
hoelzl@51518
     1
(*  Title:      HOL/Conditional_Complete_Lattices.thy
hoelzl@51518
     2
    Author:     Amine Chaieb and L C Paulson, University of Cambridge
hoelzl@51643
     3
    Author:     Johannes Hölzl, TU München
hoelzl@51518
     4
*)
paulson@33269
     5
hoelzl@51518
     6
header {* Conditional Complete Lattices *}
paulson@33269
     7
hoelzl@51518
     8
theory Conditional_Complete_Lattices
hoelzl@51518
     9
imports Main Lubs
paulson@33269
    10
begin
paulson@33269
    11
hoelzl@51475
    12
lemma Sup_fin_eq_Max: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup_fin X = Max X"
hoelzl@51475
    13
  by (induct X rule: finite_ne_induct) (simp_all add: sup_max)
hoelzl@51475
    14
hoelzl@51475
    15
lemma Inf_fin_eq_Min: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf_fin X = Min X"
hoelzl@51475
    16
  by (induct X rule: finite_ne_induct) (simp_all add: inf_min)
hoelzl@51475
    17
hoelzl@51475
    18
text {*
hoelzl@51475
    19
hoelzl@51475
    20
To avoid name classes with the @{class complete_lattice}-class we prefix @{const Sup} and
hoelzl@51475
    21
@{const Inf} in theorem names with c.
hoelzl@51475
    22
hoelzl@51475
    23
*}
hoelzl@51475
    24
hoelzl@51475
    25
class conditional_complete_lattice = lattice + Sup + Inf +
hoelzl@51475
    26
  assumes cInf_lower: "x \<in> X \<Longrightarrow> (\<And>a. a \<in> X \<Longrightarrow> z \<le> a) \<Longrightarrow> Inf X \<le> x"
hoelzl@51475
    27
    and cInf_greatest: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf X"
hoelzl@51475
    28
  assumes cSup_upper: "x \<in> X \<Longrightarrow> (\<And>a. a \<in> X \<Longrightarrow> a \<le> z) \<Longrightarrow> x \<le> Sup X"
hoelzl@51475
    29
    and cSup_least: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X \<le> z"
paulson@33269
    30
begin
hoelzl@51475
    31
hoelzl@51475
    32
lemma cSup_eq_maximum: (*REAL_SUP_MAX in HOL4*)
hoelzl@51475
    33
  "z \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X = z"
hoelzl@51475
    34
  by (blast intro: antisym cSup_upper cSup_least)
hoelzl@51475
    35
hoelzl@51475
    36
lemma cInf_eq_minimum: (*REAL_INF_MIN in HOL4*)
hoelzl@51475
    37
  "z \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X = z"
hoelzl@51475
    38
  by (intro antisym cInf_lower[of z X z] cInf_greatest[of X z]) auto
hoelzl@51475
    39
hoelzl@51475
    40
lemma cSup_le_iff: "S \<noteq> {} \<Longrightarrow> (\<And>a. a \<in> S \<Longrightarrow> a \<le> z) \<Longrightarrow> Sup S \<le> a \<longleftrightarrow> (\<forall>x\<in>S. x \<le> a)"
hoelzl@51475
    41
  by (metis order_trans cSup_upper cSup_least)
hoelzl@51475
    42
hoelzl@51475
    43
lemma le_cInf_iff: "S \<noteq> {} \<Longrightarrow> (\<And>a. a \<in> S \<Longrightarrow> z \<le> a) \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall>x\<in>S. a \<le> x)"
hoelzl@51475
    44
  by (metis order_trans cInf_lower cInf_greatest)
hoelzl@51475
    45
hoelzl@51475
    46
lemma cSup_singleton [simp]: "Sup {x} = x"
hoelzl@51475
    47
  by (intro cSup_eq_maximum) auto
hoelzl@51475
    48
hoelzl@51475
    49
lemma cInf_singleton [simp]: "Inf {x} = x"
hoelzl@51475
    50
  by (intro cInf_eq_minimum) auto
hoelzl@51475
    51
hoelzl@51475
    52
lemma cSup_upper2: (*REAL_IMP_LE_SUP in HOL4*)
hoelzl@51475
    53
  "x \<in> X \<Longrightarrow> y \<le> x \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y \<le> Sup X"
hoelzl@51475
    54
  by (metis cSup_upper order_trans)
hoelzl@51475
    55
 
hoelzl@51475
    56
lemma cInf_lower2:
hoelzl@51475
    57
  "x \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X \<le> y"
hoelzl@51475
    58
  by (metis cInf_lower order_trans)
hoelzl@51475
    59
hoelzl@51475
    60
lemma cSup_upper_EX: "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> x \<le> z \<Longrightarrow> x \<le> Sup X"
hoelzl@51475
    61
  by (blast intro: cSup_upper)
hoelzl@51475
    62
hoelzl@51475
    63
lemma cInf_lower_EX:  "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> z \<le> x \<Longrightarrow> Inf X \<le> x"
hoelzl@51475
    64
  by (blast intro: cInf_lower)
hoelzl@51475
    65
hoelzl@51475
    66
lemma cSup_eq_non_empty:
hoelzl@51475
    67
  assumes 1: "X \<noteq> {}"
hoelzl@51475
    68
  assumes 2: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a"
hoelzl@51475
    69
  assumes 3: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y"
hoelzl@51475
    70
  shows "Sup X = a"
hoelzl@51475
    71
  by (intro 3 1 antisym cSup_least) (auto intro: 2 1 cSup_upper)
hoelzl@51475
    72
hoelzl@51475
    73
lemma cInf_eq_non_empty:
hoelzl@51475
    74
  assumes 1: "X \<noteq> {}"
hoelzl@51475
    75
  assumes 2: "\<And>x. x \<in> X \<Longrightarrow> a \<le> x"
hoelzl@51475
    76
  assumes 3: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a"
hoelzl@51475
    77
  shows "Inf X = a"
hoelzl@51475
    78
  by (intro 3 1 antisym cInf_greatest) (auto intro: 2 1 cInf_lower)
hoelzl@51475
    79
hoelzl@51518
    80
lemma cInf_cSup: "S \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf S = Sup {x. \<forall>s\<in>S. x \<le> s}"
hoelzl@51518
    81
  by (rule cInf_eq_non_empty) (auto intro: cSup_upper cSup_least)
hoelzl@51518
    82
hoelzl@51518
    83
lemma cSup_cInf: "S \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup S = Inf {x. \<forall>s\<in>S. s \<le> x}"
hoelzl@51518
    84
  by (rule cSup_eq_non_empty) (auto intro: cInf_lower cInf_greatest)
hoelzl@51518
    85
hoelzl@51475
    86
lemma cSup_insert: 
hoelzl@51475
    87
  assumes x: "X \<noteq> {}"
hoelzl@51475
    88
      and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
hoelzl@51475
    89
  shows "Sup (insert a X) = sup a (Sup X)"
hoelzl@51475
    90
proof (intro cSup_eq_non_empty)
hoelzl@51475
    91
  fix y assume "\<And>x. x \<in> insert a X \<Longrightarrow> x \<le> y" with x show "sup a (Sup X) \<le> y" by (auto intro: cSup_least)
hoelzl@51475
    92
qed (auto intro: le_supI2 z cSup_upper)
paulson@33269
    93
hoelzl@51475
    94
lemma cInf_insert: 
hoelzl@51475
    95
  assumes x: "X \<noteq> {}"
hoelzl@51475
    96
      and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
hoelzl@51475
    97
  shows "Inf (insert a X) = inf a (Inf X)"
hoelzl@51475
    98
proof (intro cInf_eq_non_empty)
hoelzl@51475
    99
  fix y assume "\<And>x. x \<in> insert a X \<Longrightarrow> y \<le> x" with x show "y \<le> inf a (Inf X)" by (auto intro: cInf_greatest)
hoelzl@51475
   100
qed (auto intro: le_infI2 z cInf_lower)
hoelzl@51475
   101
hoelzl@51475
   102
lemma cSup_insert_If: 
hoelzl@51475
   103
  "(\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup (insert a X) = (if X = {} then a else sup a (Sup X))"
hoelzl@51475
   104
  using cSup_insert[of X z] by simp
hoelzl@51475
   105
hoelzl@51475
   106
lemma cInf_insert_if: 
hoelzl@51475
   107
  "(\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf (insert a X) = (if X = {} then a else inf a (Inf X))"
hoelzl@51475
   108
  using cInf_insert[of X z] by simp
hoelzl@51475
   109
hoelzl@51475
   110
lemma le_cSup_finite: "finite X \<Longrightarrow> x \<in> X \<Longrightarrow> x \<le> Sup X"
hoelzl@51475
   111
proof (induct X arbitrary: x rule: finite_induct)
hoelzl@51475
   112
  case (insert x X y) then show ?case
hoelzl@51475
   113
    apply (cases "X = {}")
hoelzl@51475
   114
    apply simp
hoelzl@51475
   115
    apply (subst cSup_insert[of _ "Sup X"])
hoelzl@51475
   116
    apply (auto intro: le_supI2)
hoelzl@51475
   117
    done
hoelzl@51475
   118
qed simp
hoelzl@51475
   119
hoelzl@51475
   120
lemma cInf_le_finite: "finite X \<Longrightarrow> x \<in> X \<Longrightarrow> Inf X \<le> x"
hoelzl@51475
   121
proof (induct X arbitrary: x rule: finite_induct)
hoelzl@51475
   122
  case (insert x X y) then show ?case
hoelzl@51475
   123
    apply (cases "X = {}")
hoelzl@51475
   124
    apply simp
hoelzl@51475
   125
    apply (subst cInf_insert[of _ "Inf X"])
hoelzl@51475
   126
    apply (auto intro: le_infI2)
hoelzl@51475
   127
    done
hoelzl@51475
   128
qed simp
hoelzl@51475
   129
hoelzl@51475
   130
lemma cSup_eq_Sup_fin: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup X = Sup_fin X"
hoelzl@51475
   131
proof (induct X rule: finite_ne_induct)
hoelzl@51475
   132
  case (insert x X) then show ?case
hoelzl@51475
   133
    using cSup_insert[of X "Sup_fin X" x] le_cSup_finite[of X] by simp
hoelzl@51475
   134
qed simp
hoelzl@51475
   135
hoelzl@51475
   136
lemma cInf_eq_Inf_fin: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Inf_fin X"
hoelzl@51475
   137
proof (induct X rule: finite_ne_induct)
hoelzl@51475
   138
  case (insert x X) then show ?case
hoelzl@51475
   139
    using cInf_insert[of X "Inf_fin X" x] cInf_le_finite[of X] by simp
hoelzl@51475
   140
qed simp
hoelzl@51475
   141
hoelzl@51475
   142
lemma cSup_atMost[simp]: "Sup {..x} = x"
hoelzl@51475
   143
  by (auto intro!: cSup_eq_maximum)
hoelzl@51475
   144
hoelzl@51475
   145
lemma cSup_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Sup {y<..x} = x"
hoelzl@51475
   146
  by (auto intro!: cSup_eq_maximum)
hoelzl@51475
   147
hoelzl@51475
   148
lemma cSup_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Sup {y..x} = x"
hoelzl@51475
   149
  by (auto intro!: cSup_eq_maximum)
hoelzl@51475
   150
hoelzl@51475
   151
lemma cInf_atLeast[simp]: "Inf {x..} = x"
hoelzl@51475
   152
  by (auto intro!: cInf_eq_minimum)
hoelzl@51475
   153
hoelzl@51475
   154
lemma cInf_atLeastLessThan[simp]: "y < x \<Longrightarrow> Inf {y..<x} = y"
hoelzl@51475
   155
  by (auto intro!: cInf_eq_minimum)
hoelzl@51475
   156
hoelzl@51475
   157
lemma cInf_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Inf {y..x} = y"
hoelzl@51475
   158
  by (auto intro!: cInf_eq_minimum)
hoelzl@51475
   159
paulson@33269
   160
end
paulson@33269
   161
hoelzl@51475
   162
instance complete_lattice \<subseteq> conditional_complete_lattice
hoelzl@51475
   163
  by default (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest)
hoelzl@51475
   164
hoelzl@51475
   165
lemma isLub_cSup: 
hoelzl@51475
   166
  "(S::'a :: conditional_complete_lattice set) \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> isLub UNIV S (Sup S)"
hoelzl@51475
   167
  by  (auto simp add: isLub_def setle_def leastP_def isUb_def
hoelzl@51475
   168
            intro!: setgeI intro: cSup_upper cSup_least)
hoelzl@51475
   169
hoelzl@51475
   170
lemma cSup_eq:
hoelzl@51475
   171
  fixes a :: "'a :: {conditional_complete_lattice, no_bot}"
hoelzl@51475
   172
  assumes upper: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a"
hoelzl@51475
   173
  assumes least: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y"
hoelzl@51475
   174
  shows "Sup X = a"
hoelzl@51475
   175
proof cases
hoelzl@51475
   176
  assume "X = {}" with lt_ex[of a] least show ?thesis by (auto simp: less_le_not_le)
hoelzl@51475
   177
qed (intro cSup_eq_non_empty assms)
hoelzl@51475
   178
hoelzl@51475
   179
lemma cInf_eq:
hoelzl@51475
   180
  fixes a :: "'a :: {conditional_complete_lattice, no_top}"
hoelzl@51475
   181
  assumes upper: "\<And>x. x \<in> X \<Longrightarrow> a \<le> x"
hoelzl@51475
   182
  assumes least: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a"
hoelzl@51475
   183
  shows "Inf X = a"
hoelzl@51475
   184
proof cases
hoelzl@51475
   185
  assume "X = {}" with gt_ex[of a] least show ?thesis by (auto simp: less_le_not_le)
hoelzl@51475
   186
qed (intro cInf_eq_non_empty assms)
hoelzl@51475
   187
hoelzl@51475
   188
lemma cSup_le: "(S::'a::conditional_complete_lattice set) \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b"
hoelzl@51475
   189
  by (metis cSup_least setle_def)
hoelzl@51475
   190
hoelzl@51475
   191
lemma cInf_ge: "(S::'a :: conditional_complete_lattice set) \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b"
hoelzl@51475
   192
  by (metis cInf_greatest setge_def)
hoelzl@51475
   193
hoelzl@51475
   194
class conditional_complete_linorder = conditional_complete_lattice + linorder
paulson@33269
   195
begin
hoelzl@51475
   196
hoelzl@51475
   197
lemma less_cSup_iff : (*REAL_SUP_LE in HOL4*)
hoelzl@51475
   198
  "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y < Sup X \<longleftrightarrow> (\<exists>x\<in>X. y < x)"
hoelzl@51475
   199
  by (rule iffI) (metis cSup_least not_less, metis cSup_upper less_le_trans)
hoelzl@51475
   200
hoelzl@51475
   201
lemma cInf_less_iff: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X < y \<longleftrightarrow> (\<exists>x\<in>X. x < y)"
hoelzl@51475
   202
  by (rule iffI) (metis cInf_greatest not_less, metis cInf_lower le_less_trans)
hoelzl@51475
   203
hoelzl@51475
   204
lemma less_cSupE:
hoelzl@51475
   205
  assumes "y < Sup X" "X \<noteq> {}" obtains x where "x \<in> X" "y < x"
hoelzl@51475
   206
  by (metis cSup_least assms not_le that)
hoelzl@51475
   207
hoelzl@51518
   208
lemma less_cSupD:
hoelzl@51518
   209
  "X \<noteq> {} \<Longrightarrow> z < Sup X \<Longrightarrow> \<exists>x\<in>X. z < x"
hoelzl@51518
   210
  by (metis less_cSup_iff not_leE)
hoelzl@51518
   211
hoelzl@51518
   212
lemma cInf_lessD:
hoelzl@51518
   213
  "X \<noteq> {} \<Longrightarrow> Inf X < z \<Longrightarrow> \<exists>x\<in>X. x < z"
hoelzl@51518
   214
  by (metis cInf_less_iff not_leE)
hoelzl@51518
   215
hoelzl@51475
   216
lemma complete_interval:
hoelzl@51475
   217
  assumes "a < b" and "P a" and "\<not> P b"
hoelzl@51475
   218
  shows "\<exists>c. a \<le> c \<and> c \<le> b \<and> (\<forall>x. a \<le> x \<and> x < c \<longrightarrow> P x) \<and>
hoelzl@51475
   219
             (\<forall>d. (\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x) \<longrightarrow> d \<le> c)"
hoelzl@51475
   220
proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x & x < d --> P x}"], auto)
hoelzl@51475
   221
  show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
hoelzl@51475
   222
    by (rule cSup_upper [where z=b], auto)
hoelzl@51475
   223
       (metis `a < b` `\<not> P b` linear less_le)
hoelzl@51475
   224
next
hoelzl@51475
   225
  show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b"
hoelzl@51475
   226
    apply (rule cSup_least) 
hoelzl@51475
   227
    apply auto
hoelzl@51475
   228
    apply (metis less_le_not_le)
hoelzl@51475
   229
    apply (metis `a<b` `~ P b` linear less_le)
hoelzl@51475
   230
    done
hoelzl@51475
   231
next
hoelzl@51475
   232
  fix x
hoelzl@51475
   233
  assume x: "a \<le> x" and lt: "x < Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
hoelzl@51475
   234
  show "P x"
hoelzl@51475
   235
    apply (rule less_cSupE [OF lt], auto)
hoelzl@51475
   236
    apply (metis less_le_not_le)
hoelzl@51475
   237
    apply (metis x) 
hoelzl@51475
   238
    done
hoelzl@51475
   239
next
hoelzl@51475
   240
  fix d
hoelzl@51475
   241
    assume 0: "\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x"
hoelzl@51475
   242
    thus "d \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
hoelzl@51475
   243
      by (rule_tac z="b" in cSup_upper, auto) 
hoelzl@51475
   244
         (metis `a<b` `~ P b` linear less_le)
hoelzl@51475
   245
qed
hoelzl@51475
   246
hoelzl@51475
   247
end
hoelzl@51475
   248
hoelzl@51518
   249
lemma cSup_bounds:
hoelzl@51518
   250
  fixes S :: "'a :: conditional_complete_lattice set"
hoelzl@51518
   251
  assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
hoelzl@51518
   252
  shows "a \<le> Sup S \<and> Sup S \<le> b"
hoelzl@51518
   253
proof-
hoelzl@51518
   254
  from isLub_cSup[OF Se] u have lub: "isLub UNIV S (Sup S)" by blast
hoelzl@51518
   255
  hence b: "Sup S \<le> b" using u 
hoelzl@51518
   256
    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) 
hoelzl@51518
   257
  from Se obtain y where y: "y \<in> S" by blast
hoelzl@51518
   258
  from lub l have "a \<le> Sup S"
hoelzl@51518
   259
    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
hoelzl@51518
   260
       (metis le_iff_sup le_sup_iff y)
hoelzl@51518
   261
  with b show ?thesis by blast
hoelzl@51518
   262
qed
hoelzl@51518
   263
hoelzl@51518
   264
hoelzl@51475
   265
lemma cSup_unique: "(S::'a :: {conditional_complete_linorder, no_bot} set) *<= b \<Longrightarrow> (\<forall>b'<b. \<exists>x\<in>S. b' < x) \<Longrightarrow> Sup S = b"
hoelzl@51475
   266
  by (rule cSup_eq) (auto simp: not_le[symmetric] setle_def)
hoelzl@51475
   267
hoelzl@51475
   268
lemma cInf_unique: "b <=* (S::'a :: {conditional_complete_linorder, no_top} set) \<Longrightarrow> (\<forall>b'>b. \<exists>x\<in>S. b' > x) \<Longrightarrow> Inf S = b"
hoelzl@51475
   269
  by (rule cInf_eq) (auto simp: not_le[symmetric] setge_def)
hoelzl@51475
   270
hoelzl@51475
   271
lemma cSup_eq_Max: "finite (X::'a::conditional_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup X = Max X"
hoelzl@51475
   272
  using cSup_eq_Sup_fin[of X] Sup_fin_eq_Max[of X] by simp
hoelzl@51475
   273
hoelzl@51475
   274
lemma cInf_eq_Min: "finite (X::'a::conditional_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Min X"
hoelzl@51475
   275
  using cInf_eq_Inf_fin[of X] Inf_fin_eq_Min[of X] by simp
hoelzl@51475
   276
hoelzl@51475
   277
lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditional_complete_linorder, dense_linorder}} = x"
hoelzl@51475
   278
  by (auto intro!: cSup_eq_non_empty intro: dense_le)
hoelzl@51475
   279
hoelzl@51475
   280
lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditional_complete_linorder, dense_linorder}} = x"
hoelzl@51475
   281
  by (auto intro!: cSup_eq intro: dense_le_bounded)
hoelzl@51475
   282
hoelzl@51475
   283
lemma cSup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x::'a::{conditional_complete_linorder, dense_linorder}} = x"
hoelzl@51475
   284
  by (auto intro!: cSup_eq intro: dense_le_bounded)
hoelzl@51475
   285
hoelzl@51475
   286
lemma cInf_greaterThan[simp]: "Inf {x::'a::{conditional_complete_linorder, dense_linorder} <..} = x"
hoelzl@51475
   287
  by (auto intro!: cInf_eq intro: dense_ge)
hoelzl@51475
   288
hoelzl@51475
   289
lemma cInf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x::'a::{conditional_complete_linorder, dense_linorder}} = y"
hoelzl@51475
   290
  by (auto intro!: cInf_eq intro: dense_ge_bounded)
hoelzl@51475
   291
hoelzl@51475
   292
lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditional_complete_linorder, dense_linorder}} = y"
hoelzl@51475
   293
  by (auto intro!: cInf_eq intro: dense_ge_bounded)
hoelzl@51475
   294
paulson@33269
   295
end