src/HOL/SupInf.thy
 author nipkow Fri Nov 13 14:14:04 2009 +0100 (2009-11-13) changeset 33657 a4179bf442d1 parent 33609 059cd49e4b1e child 35028 108662d50512 permissions -rw-r--r--
renamed lemmas "anti_sym" -> "antisym"
```     1 (*  Author: Amine Chaieb and L C Paulson, University of Cambridge *)
```
```     2
```
```     3 header {*Sup and Inf Operators on Sets of Reals.*}
```
```     4
```
```     5 theory SupInf
```
```     6 imports RComplete
```
```     7 begin
```
```     8
```
```     9 lemma minus_max_eq_min:
```
```    10   fixes x :: "'a::{lordered_ab_group_add, linorder}"
```
```    11   shows "- (max x y) = min (-x) (-y)"
```
```    12 by (metis le_imp_neg_le linorder_linear min_max.inf_absorb2 min_max.le_iff_inf min_max.le_iff_sup min_max.sup_absorb1)
```
```    13
```
```    14 lemma minus_min_eq_max:
```
```    15   fixes x :: "'a::{lordered_ab_group_add, linorder}"
```
```    16   shows "- (min x y) = max (-x) (-y)"
```
```    17 by (metis minus_max_eq_min minus_minus)
```
```    18
```
```    19 lemma minus_Max_eq_Min [simp]:
```
```    20   fixes S :: "'a::{lordered_ab_group_add, linorder} set"
```
```    21   shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Max S) = Min (uminus ` S)"
```
```    22 proof (induct S rule: finite_ne_induct)
```
```    23   case (singleton x)
```
```    24   thus ?case by simp
```
```    25 next
```
```    26   case (insert x S)
```
```    27   thus ?case by (simp add: minus_max_eq_min)
```
```    28 qed
```
```    29
```
```    30 lemma minus_Min_eq_Max [simp]:
```
```    31   fixes S :: "'a::{lordered_ab_group_add, linorder} set"
```
```    32   shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Min S) = Max (uminus ` S)"
```
```    33 proof (induct S rule: finite_ne_induct)
```
```    34   case (singleton x)
```
```    35   thus ?case by simp
```
```    36 next
```
```    37   case (insert x S)
```
```    38   thus ?case by (simp add: minus_min_eq_max)
```
```    39 qed
```
```    40
```
```    41 instantiation real :: Sup
```
```    42 begin
```
```    43 definition
```
```    44   Sup_real_def [code del]: "Sup X == (LEAST z::real. \<forall>x\<in>X. x\<le>z)"
```
```    45
```
```    46 instance ..
```
```    47 end
```
```    48
```
```    49 instantiation real :: Inf
```
```    50 begin
```
```    51 definition
```
```    52   Inf_real_def [code del]: "Inf (X::real set) == - (Sup (uminus ` X))"
```
```    53
```
```    54 instance ..
```
```    55 end
```
```    56
```
```    57 subsection{*Supremum of a set of reals*}
```
```    58
```
```    59 lemma Sup_upper [intro]: (*REAL_SUP_UBOUND in HOL4*)
```
```    60   fixes x :: real
```
```    61   assumes x: "x \<in> X"
```
```    62       and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
```
```    63   shows "x \<le> Sup X"
```
```    64 proof (auto simp add: Sup_real_def)
```
```    65   from reals_complete2
```
```    66   obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
```
```    67     by (blast intro: x z)
```
```    68   hence "x \<le> s"
```
```    69     by (blast intro: x z)
```
```    70   also with s have "... = (LEAST z. \<forall>x\<in>X. x \<le> z)"
```
```    71     by (fast intro: Least_equality [symmetric])
```
```    72   finally show "x \<le> (LEAST z. \<forall>x\<in>X. x \<le> z)" .
```
```    73 qed
```
```    74
```
```    75 lemma Sup_least [intro]: (*REAL_IMP_SUP_LE in HOL4*)
```
```    76   fixes z :: real
```
```    77   assumes x: "X \<noteq> {}"
```
```    78       and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
```
```    79   shows "Sup X \<le> z"
```
```    80 proof (auto simp add: Sup_real_def)
```
```    81   from reals_complete2 x
```
```    82   obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
```
```    83     by (blast intro: z)
```
```    84   hence "(LEAST z. \<forall>x\<in>X. x \<le> z) = s"
```
```    85     by (best intro: Least_equality)
```
```    86   also with s z have "... \<le> z"
```
```    87     by blast
```
```    88   finally show "(LEAST z. \<forall>x\<in>X. x \<le> z) \<le> z" .
```
```    89 qed
```
```    90
```
```    91 lemma less_SupE:
```
```    92   fixes y :: real
```
```    93   assumes "y < Sup X" "X \<noteq> {}"
```
```    94   obtains x where "x\<in>X" "y < x"
```
```    95 by (metis SupInf.Sup_least assms linorder_not_less that)
```
```    96
```
```    97 lemma Sup_singleton [simp]: "Sup {x::real} = x"
```
```    98   by (force intro: Least_equality simp add: Sup_real_def)
```
```    99
```
```   100 lemma Sup_eq_maximum: (*REAL_SUP_MAX in HOL4*)
```
```   101   fixes z :: real
```
```   102   assumes X: "z \<in> X" and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
```
```   103   shows  "Sup X = z"
```
```   104   by (force intro: Least_equality X z simp add: Sup_real_def)
```
```   105
```
```   106 lemma Sup_upper2: (*REAL_IMP_LE_SUP in HOL4*)
```
```   107   fixes x :: real
```
```   108   shows "x \<in> X \<Longrightarrow> y \<le> x \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y \<le> Sup X"
```
```   109   by (metis Sup_upper real_le_trans)
```
```   110
```
```   111 lemma Sup_real_iff : (*REAL_SUP_LE in HOL4*)
```
```   112   fixes z :: real
```
```   113   shows "X ~= {} ==> (!!x. x \<in> X ==> x \<le> z) ==> (\<exists>x\<in>X. y<x) <-> y < Sup X"
```
```   114   by (metis Sup_least Sup_upper linorder_not_le le_less_trans)
```
```   115
```
```   116 lemma Sup_eq:
```
```   117   fixes a :: real
```
```   118   shows "(!!x. x \<in> X \<Longrightarrow> x \<le> a)
```
```   119         \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y) \<Longrightarrow> Sup X = a"
```
```   120   by (metis Sup_least Sup_upper add_le_cancel_left diff_add_cancel insert_absorb
```
```   121         insert_not_empty real_le_antisym)
```
```   122
```
```   123 lemma Sup_le:
```
```   124   fixes S :: "real set"
```
```   125   shows "S \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b"
```
```   126 by (metis SupInf.Sup_least setle_def)
```
```   127
```
```   128 lemma Sup_upper_EX:
```
```   129   fixes x :: real
```
```   130   shows "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> x \<le> z \<Longrightarrow>  x \<le> Sup X"
```
```   131   by blast
```
```   132
```
```   133 lemma Sup_insert_nonempty:
```
```   134   fixes x :: real
```
```   135   assumes x: "x \<in> X"
```
```   136       and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
```
```   137   shows "Sup (insert a X) = max a (Sup X)"
```
```   138 proof (cases "Sup X \<le> a")
```
```   139   case True
```
```   140   thus ?thesis
```
```   141     apply (simp add: max_def)
```
```   142     apply (rule Sup_eq_maximum)
```
```   143     apply (metis insertCI)
```
```   144     apply (metis Sup_upper insertE le_iff_sup real_le_linear real_le_trans sup_absorb1 z)
```
```   145     done
```
```   146 next
```
```   147   case False
```
```   148   hence 1:"a < Sup X" by simp
```
```   149   have "Sup X \<le> Sup (insert a X)"
```
```   150     apply (rule Sup_least)
```
```   151     apply (metis empty_psubset_nonempty psubset_eq x)
```
```   152     apply (rule Sup_upper_EX)
```
```   153     apply blast
```
```   154     apply (metis insert_iff real_le_linear real_le_refl real_le_trans z)
```
```   155     done
```
```   156   moreover
```
```   157   have "Sup (insert a X) \<le> Sup X"
```
```   158     apply (rule Sup_least)
```
```   159     apply blast
```
```   160     apply (metis False Sup_upper insertE real_le_linear z)
```
```   161     done
```
```   162   ultimately have "Sup (insert a X) = Sup X"
```
```   163     by (blast intro:  antisym )
```
```   164   thus ?thesis
```
```   165     by (metis 1 min_max.le_iff_sup real_less_def)
```
```   166 qed
```
```   167
```
```   168 lemma Sup_insert_if:
```
```   169   fixes X :: "real set"
```
```   170   assumes z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
```
```   171   shows "Sup (insert a X) = (if X={} then a else max a (Sup X))"
```
```   172 by auto (metis Sup_insert_nonempty z)
```
```   173
```
```   174 lemma Sup:
```
```   175   fixes S :: "real set"
```
```   176   shows "S \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> isLub UNIV S (Sup S)"
```
```   177 by  (auto simp add: isLub_def setle_def leastP_def isUb_def intro!: setgeI)
```
```   178
```
```   179 lemma Sup_finite_Max:
```
```   180   fixes S :: "real set"
```
```   181   assumes fS: "finite S" and Se: "S \<noteq> {}"
```
```   182   shows "Sup S = Max S"
```
```   183 using fS Se
```
```   184 proof-
```
```   185   let ?m = "Max S"
```
```   186   from Max_ge[OF fS] have Sm: "\<forall> x\<in> S. x \<le> ?m" by metis
```
```   187   with Sup[OF Se] have lub: "isLub UNIV S (Sup S)" by (metis setle_def)
```
```   188   from Max_in[OF fS Se] lub have mrS: "?m \<le> Sup S"
```
```   189     by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
```
```   190   moreover
```
```   191   have "Sup S \<le> ?m" using Sm lub
```
```   192     by (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)
```
```   193   ultimately  show ?thesis by arith
```
```   194 qed
```
```   195
```
```   196 lemma Sup_finite_in:
```
```   197   fixes S :: "real set"
```
```   198   assumes fS: "finite S" and Se: "S \<noteq> {}"
```
```   199   shows "Sup S \<in> S"
```
```   200   using Sup_finite_Max[OF fS Se] Max_in[OF fS Se] by metis
```
```   201
```
```   202 lemma Sup_finite_ge_iff:
```
```   203   fixes S :: "real set"
```
```   204   assumes fS: "finite S" and Se: "S \<noteq> {}"
```
```   205   shows "a \<le> Sup S \<longleftrightarrow> (\<exists> x \<in> S. a \<le> x)"
```
```   206 by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS linorder_not_le less_le_trans)
```
```   207
```
```   208 lemma Sup_finite_le_iff:
```
```   209   fixes S :: "real set"
```
```   210   assumes fS: "finite S" and Se: "S \<noteq> {}"
```
```   211   shows "a \<ge> Sup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> x)"
```
```   212 by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS le_iff_sup real_le_trans)
```
```   213
```
```   214 lemma Sup_finite_gt_iff:
```
```   215   fixes S :: "real set"
```
```   216   assumes fS: "finite S" and Se: "S \<noteq> {}"
```
```   217   shows "a < Sup S \<longleftrightarrow> (\<exists> x \<in> S. a < x)"
```
```   218 by (metis Se Sup_finite_le_iff fS linorder_not_less)
```
```   219
```
```   220 lemma Sup_finite_lt_iff:
```
```   221   fixes S :: "real set"
```
```   222   assumes fS: "finite S" and Se: "S \<noteq> {}"
```
```   223   shows "a > Sup S \<longleftrightarrow> (\<forall> x \<in> S. a > x)"
```
```   224 by (metis Se Sup_finite_ge_iff fS linorder_not_less)
```
```   225
```
```   226 lemma Sup_unique:
```
```   227   fixes S :: "real set"
```
```   228   shows "S *<= b \<Longrightarrow> (\<forall>b' < b. \<exists>x \<in> S. b' < x) \<Longrightarrow> Sup S = b"
```
```   229 unfolding setle_def
```
```   230 apply (rule Sup_eq, auto)
```
```   231 apply (metis linorder_not_less)
```
```   232 done
```
```   233
```
```   234 lemma Sup_abs_le:
```
```   235   fixes S :: "real set"
```
```   236   shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a"
```
```   237 by (auto simp add: abs_le_interval_iff) (metis Sup_upper2)
```
```   238
```
```   239 lemma Sup_bounds:
```
```   240   fixes S :: "real set"
```
```   241   assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
```
```   242   shows "a \<le> Sup S \<and> Sup S \<le> b"
```
```   243 proof-
```
```   244   from Sup[OF Se] u have lub: "isLub UNIV S (Sup S)" by blast
```
```   245   hence b: "Sup S \<le> b" using u
```
```   246     by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
```
```   247   from Se obtain y where y: "y \<in> S" by blast
```
```   248   from lub l have "a \<le> Sup S"
```
```   249     by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
```
```   250        (metis le_iff_sup le_sup_iff y)
```
```   251   with b show ?thesis by blast
```
```   252 qed
```
```   253
```
```   254 lemma Sup_asclose:
```
```   255   fixes S :: "real set"
```
```   256   assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Sup S - l\<bar> \<le> e"
```
```   257 proof-
```
```   258   have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e" by arith
```
```   259   thus ?thesis using S b Sup_bounds[of S "l - e" "l+e"] unfolding th
```
```   260     by  (auto simp add: setge_def setle_def)
```
```   261 qed
```
```   262
```
```   263
```
```   264 subsection{*Infimum of a set of reals*}
```
```   265
```
```   266 lemma Inf_lower [intro]:
```
```   267   fixes z :: real
```
```   268   assumes x: "x \<in> X"
```
```   269       and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
```
```   270   shows "Inf X \<le> x"
```
```   271 proof -
```
```   272   have "-x \<le> Sup (uminus ` X)"
```
```   273     by (rule Sup_upper [where z = "-z"]) (auto simp add: image_iff x z)
```
```   274   thus ?thesis
```
```   275     by (auto simp add: Inf_real_def)
```
```   276 qed
```
```   277
```
```   278 lemma Inf_greatest [intro]:
```
```   279   fixes z :: real
```
```   280   assumes x: "X \<noteq> {}"
```
```   281       and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
```
```   282   shows "z \<le> Inf X"
```
```   283 proof -
```
```   284   have "Sup (uminus ` X) \<le> -z" using x z by (force intro: Sup_least)
```
```   285   hence "z \<le> - Sup (uminus ` X)"
```
```   286     by simp
```
```   287   thus ?thesis
```
```   288     by (auto simp add: Inf_real_def)
```
```   289 qed
```
```   290
```
```   291 lemma Inf_singleton [simp]: "Inf {x::real} = x"
```
```   292   by (simp add: Inf_real_def)
```
```   293
```
```   294 lemma Inf_eq_minimum: (*REAL_INF_MIN in HOL4*)
```
```   295   fixes z :: real
```
```   296   assumes x: "z \<in> X" and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
```
```   297   shows  "Inf X = z"
```
```   298 proof -
```
```   299   have "Sup (uminus ` X) = -z" using x z
```
```   300     by (force intro: Sup_eq_maximum x z)
```
```   301   thus ?thesis
```
```   302     by (simp add: Inf_real_def)
```
```   303 qed
```
```   304
```
```   305 lemma Inf_lower2:
```
```   306   fixes x :: real
```
```   307   shows "x \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X \<le> y"
```
```   308   by (metis Inf_lower real_le_trans)
```
```   309
```
```   310 lemma Inf_real_iff:
```
```   311   fixes z :: real
```
```   312   shows "X \<noteq> {} \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> (\<exists>x\<in>X. x<y) \<longleftrightarrow> Inf X < y"
```
```   313   by (metis Inf_greatest Inf_lower less_le_not_le real_le_linear
```
```   314             order_less_le_trans)
```
```   315
```
```   316 lemma Inf_eq:
```
```   317   fixes a :: real
```
```   318   shows "(!!x. x \<in> X \<Longrightarrow> a \<le> x) \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a) \<Longrightarrow> Inf X = a"
```
```   319   by (metis Inf_greatest Inf_lower add_le_cancel_left diff_add_cancel
```
```   320         insert_absorb insert_not_empty real_le_antisym)
```
```   321
```
```   322 lemma Inf_ge:
```
```   323   fixes S :: "real set"
```
```   324   shows "S \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b"
```
```   325 by (metis SupInf.Inf_greatest setge_def)
```
```   326
```
```   327 lemma Inf_lower_EX:
```
```   328   fixes x :: real
```
```   329   shows "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> z \<le> x \<Longrightarrow> Inf X \<le> x"
```
```   330   by blast
```
```   331
```
```   332 lemma Inf_insert_nonempty:
```
```   333   fixes x :: real
```
```   334   assumes x: "x \<in> X"
```
```   335       and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
```
```   336   shows "Inf (insert a X) = min a (Inf X)"
```
```   337 proof (cases "a \<le> Inf X")
```
```   338   case True
```
```   339   thus ?thesis
```
```   340     by (simp add: min_def)
```
```   341        (blast intro: Inf_eq_minimum Inf_lower real_le_refl real_le_trans z)
```
```   342 next
```
```   343   case False
```
```   344   hence 1:"Inf X < a" by simp
```
```   345   have "Inf (insert a X) \<le> Inf X"
```
```   346     apply (rule Inf_greatest)
```
```   347     apply (metis empty_psubset_nonempty psubset_eq x)
```
```   348     apply (rule Inf_lower_EX)
```
```   349     apply (blast intro: elim:)
```
```   350     apply (metis insert_iff real_le_linear real_le_refl real_le_trans z)
```
```   351     done
```
```   352   moreover
```
```   353   have "Inf X \<le> Inf (insert a X)"
```
```   354     apply (rule Inf_greatest)
```
```   355     apply blast
```
```   356     apply (metis False Inf_lower insertE real_le_linear z)
```
```   357     done
```
```   358   ultimately have "Inf (insert a X) = Inf X"
```
```   359     by (blast intro:  antisym )
```
```   360   thus ?thesis
```
```   361     by (metis False min_max.inf_absorb2 real_le_linear)
```
```   362 qed
```
```   363
```
```   364 lemma Inf_insert_if:
```
```   365   fixes X :: "real set"
```
```   366   assumes z:  "!!x. x \<in> X \<Longrightarrow> z \<le> x"
```
```   367   shows "Inf (insert a X) = (if X={} then a else min a (Inf X))"
```
```   368 by auto (metis Inf_insert_nonempty z)
```
```   369
```
```   370 lemma Inf_greater:
```
```   371   fixes z :: real
```
```   372   shows "X \<noteq> {} \<Longrightarrow>  Inf X < z \<Longrightarrow> \<exists>x \<in> X. x < z"
```
```   373   by (metis Inf_real_iff mem_def not_leE)
```
```   374
```
```   375 lemma Inf_close:
```
```   376   fixes e :: real
```
```   377   shows "X \<noteq> {} \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>x \<in> X. x < Inf X + e"
```
```   378   by (metis add_strict_increasing comm_monoid_add.mult_commute Inf_greater linorder_not_le pos_add_strict)
```
```   379
```
```   380 lemma Inf_finite_Min:
```
```   381   fixes S :: "real set"
```
```   382   shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> Inf S = Min S"
```
```   383 by (simp add: Inf_real_def Sup_finite_Max image_image)
```
```   384
```
```   385 lemma Inf_finite_in:
```
```   386   fixes S :: "real set"
```
```   387   assumes fS: "finite S" and Se: "S \<noteq> {}"
```
```   388   shows "Inf S \<in> S"
```
```   389   using Inf_finite_Min[OF fS Se] Min_in[OF fS Se] by metis
```
```   390
```
```   391 lemma Inf_finite_ge_iff:
```
```   392   fixes S :: "real set"
```
```   393   shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall> x \<in> S. a \<le> x)"
```
```   394 by (metis Inf_finite_Min Inf_finite_in Min_le real_le_trans)
```
```   395
```
```   396 lemma Inf_finite_le_iff:
```
```   397   fixes S :: "real set"
```
```   398   shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists> x \<in> S. a \<ge> x)"
```
```   399 by (metis Inf_finite_Min Inf_finite_ge_iff Inf_finite_in Min_le
```
```   400           real_le_antisym real_le_linear)
```
```   401
```
```   402 lemma Inf_finite_gt_iff:
```
```   403   fixes S :: "real set"
```
```   404   shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a < Inf S \<longleftrightarrow> (\<forall> x \<in> S. a < x)"
```
```   405 by (metis Inf_finite_le_iff linorder_not_less)
```
```   406
```
```   407 lemma Inf_finite_lt_iff:
```
```   408   fixes S :: "real set"
```
```   409   shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a > Inf S \<longleftrightarrow> (\<exists> x \<in> S. a > x)"
```
```   410 by (metis Inf_finite_ge_iff linorder_not_less)
```
```   411
```
```   412 lemma Inf_unique:
```
```   413   fixes S :: "real set"
```
```   414   shows "b <=* S \<Longrightarrow> (\<forall>b' > b. \<exists>x \<in> S. b' > x) \<Longrightarrow> Inf S = b"
```
```   415 unfolding setge_def
```
```   416 apply (rule Inf_eq, auto)
```
```   417 apply (metis less_le_not_le linorder_not_less)
```
```   418 done
```
```   419
```
```   420 lemma Inf_abs_ge:
```
```   421   fixes S :: "real set"
```
```   422   shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Inf S\<bar> \<le> a"
```
```   423 by (simp add: Inf_real_def) (rule Sup_abs_le, auto)
```
```   424
```
```   425 lemma Inf_asclose:
```
```   426   fixes S :: "real set"
```
```   427   assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Inf S - l\<bar> \<le> e"
```
```   428 proof -
```
```   429   have "\<bar>- Sup (uminus ` S) - l\<bar> =  \<bar>Sup (uminus ` S) - (-l)\<bar>"
```
```   430     by auto
```
```   431   also have "... \<le> e"
```
```   432     apply (rule Sup_asclose)
```
```   433     apply (auto simp add: S)
```
```   434     apply (metis abs_minus_add_cancel b comm_monoid_add.mult_commute real_diff_def)
```
```   435     done
```
```   436   finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" .
```
```   437   thus ?thesis
```
```   438     by (simp add: Inf_real_def)
```
```   439 qed
```
```   440
```
```   441 subsection{*Relate max and min to Sup and Inf.*}
```
```   442
```
```   443 lemma real_max_Sup:
```
```   444   fixes x :: real
```
```   445   shows "max x y = Sup {x,y}"
```
```   446 proof-
```
```   447   have f: "finite {x, y}" "{x,y} \<noteq> {}"  by simp_all
```
```   448   from Sup_finite_le_iff[OF f, of "max x y"] have "Sup {x,y} \<le> max x y" by simp
```
```   449   moreover
```
```   450   have "max x y \<le> Sup {x,y}" using Sup_finite_ge_iff[OF f, of "max x y"]
```
```   451     by (simp add: linorder_linear)
```
```   452   ultimately show ?thesis by arith
```
```   453 qed
```
```   454
```
```   455 lemma real_min_Inf:
```
```   456   fixes x :: real
```
```   457   shows "min x y = Inf {x,y}"
```
```   458 proof-
```
```   459   have f: "finite {x, y}" "{x,y} \<noteq> {}"  by simp_all
```
```   460   from Inf_finite_le_iff[OF f, of "min x y"] have "Inf {x,y} \<le> min x y"
```
```   461     by (simp add: linorder_linear)
```
```   462   moreover
```
```   463   have "min x y \<le> Inf {x,y}" using Inf_finite_ge_iff[OF f, of "min x y"]
```
```   464     by simp
```
```   465   ultimately show ?thesis by arith
```
```   466 qed
```
```   467
```
```   468 lemma reals_complete_interval:
```
```   469   fixes a::real and b::real
```
```   470   assumes "a < b" and "P a" and "~P b"
```
```   471   shows "\<exists>c. a \<le> c & c \<le> b & (\<forall>x. a \<le> x & x < c --> P x) &
```
```   472              (\<forall>d. (\<forall>x. a \<le> x & x < d --> P x) --> d \<le> c)"
```
```   473 proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x & x < d --> P x}"], auto)
```
```   474   show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
```
```   475     by (rule SupInf.Sup_upper [where z=b], auto)
```
```   476        (metis prems real_le_linear real_less_def)
```
```   477 next
```
```   478   show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b"
```
```   479     apply (rule SupInf.Sup_least)
```
```   480     apply (auto simp add: )
```
```   481     apply (metis less_le_not_le)
```
```   482     apply (metis `a<b` `~ P b` real_le_linear real_less_def)
```
```   483     done
```
```   484 next
```
```   485   fix x
```
```   486   assume x: "a \<le> x" and lt: "x < Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
```
```   487   show "P x"
```
```   488     apply (rule less_SupE [OF lt], auto)
```
```   489     apply (metis less_le_not_le)
```
```   490     apply (metis x)
```
```   491     done
```
```   492 next
```
```   493   fix d
```
```   494     assume 0: "\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x"
```
```   495     thus "d \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
```
```   496       by (rule_tac z="b" in SupInf.Sup_upper, auto)
```
```   497          (metis `a<b` `~ P b` real_le_linear real_less_def)
```
```   498 qed
```
```   499
```
```   500 end
```