introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
authorhoelzl
Fri Mar 22 10:41:43 2013 +0100 (2013-03-22)
changeset 51475ebf9d4fd00ba
parent 51474 1e9e68247ad1
child 51476 0c0efde246d1
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
src/HOL/Multivariate_Analysis/Fashoda.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/Multivariate_Analysis/Operator_Norm.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Probability/Probability_Measure.thy
src/HOL/SupInf.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Mar 22 10:41:43 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Mar 22 10:41:43 2013 +0100
     1.3 @@ -3491,11 +3491,11 @@
     1.4      apply(rule,rule) defer apply(rule) unfolding inner_minus_left and neg_less_iff_less proof-
     1.5      from ab have "((\<lambda>x. inner a x) ` t) *<= (inner a y - b)"
     1.6        apply(erule_tac x=y in ballE) apply(rule setleI) using `y\<in>s` by auto
     1.7 -    hence k:"isLub UNIV ((\<lambda>x. inner a x) ` t) k" unfolding k_def apply(rule_tac Sup) using assms(5) by auto
     1.8 +    hence k:"isLub UNIV ((\<lambda>x. inner a x) ` t) k" unfolding k_def apply(rule_tac isLub_cSup) using assms(5) by auto
     1.9      fix x assume "x\<in>t" thus "inner a x < (k + b / 2)" using `0<b` and isLubD2[OF k, of "inner a x"] by auto
    1.10    next
    1.11      fix x assume "x\<in>s"
    1.12 -    hence "k \<le> inner a x - b" unfolding k_def apply(rule_tac Sup_least) using assms(5)
    1.13 +    hence "k \<le> inner a x - b" unfolding k_def apply(rule_tac cSup_least) using assms(5)
    1.14        using ab[THEN bspec[where x=x]] by auto
    1.15      thus "k + b / 2 < inner a x" using `0 < b` by auto
    1.16    qed
    1.17 @@ -3544,9 +3544,9 @@
    1.18    thus ?thesis
    1.19      apply(rule_tac x=a in exI, rule_tac x="Sup ((\<lambda>x. inner a x) ` s)" in exI) using `a\<noteq>0`
    1.20      apply auto
    1.21 -    apply (rule Sup[THEN isLubD2])
    1.22 +    apply (rule isLub_cSup[THEN isLubD2])
    1.23      prefer 4
    1.24 -    apply (rule Sup_least)
    1.25 +    apply (rule cSup_least)
    1.26       using assms(3-5) apply (auto simp add: setle_def)
    1.27      apply metis
    1.28      done
    1.29 @@ -6208,7 +6208,7 @@
    1.30      using interior_subset[of I] `x \<in> interior I` by auto
    1.31  
    1.32    have "Inf (?F x) \<le> (f x - f y) / (x - y)"
    1.33 -  proof (rule Inf_lower2)
    1.34 +  proof (rule cInf_lower2)
    1.35      show "(f x - f t) / (x - t) \<in> ?F x"
    1.36        using `t \<in> I` `x < t` by auto
    1.37      show "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)"
    1.38 @@ -6231,7 +6231,7 @@
    1.39    with `x \<in> interior I` e interior_subset[of I] have "t \<in> I" "x \<in> I" by auto
    1.40  
    1.41    have "(f x - f y) / (x - y) \<le> Inf (?F x)"
    1.42 -  proof (rule Inf_greatest)
    1.43 +  proof (rule cInf_greatest)
    1.44      have "(f x - f y) / (x - y) = (f y - f x) / (y - x)"
    1.45        using `y < x` by (auto simp: field_simps)
    1.46      also
     2.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Fri Mar 22 10:41:43 2013 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Fri Mar 22 10:41:43 2013 +0100
     2.3 @@ -523,7 +523,7 @@
     2.4  proof -
     2.5    { assume "S ~= {}"
     2.6      { assume ex: "EX B. ALL x:S. B<=x"
     2.7 -      then have *: "ALL x:S. Inf S <= x" using Inf_lower_EX[of _ S] ex by metis
     2.8 +      then have *: "ALL x:S. Inf S <= x" using cInf_lower_EX[of _ S] ex by metis
     2.9        then have "Inf S : S" apply (subst closed_contains_Inf) using ex `S ~= {}` `closed S` by auto
    2.10        then have "ALL x. (Inf S <= x <-> x:S)" using mono[rule_format, of "Inf S"] * by auto
    2.11        then have "S = {Inf S ..}" by auto
     3.1 --- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Fri Mar 22 10:41:43 2013 +0100
     3.2 +++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Fri Mar 22 10:41:43 2013 +0100
     3.3 @@ -18,7 +18,7 @@
     3.4  subsection {*Fashoda meet theorem. *}
     3.5  
     3.6  lemma infnorm_2: "infnorm (x::real^2) = max (abs(x$1)) (abs(x$2))"
     3.7 -  unfolding infnorm_cart UNIV_2 apply(rule Sup_eq) by auto
     3.8 +  unfolding infnorm_cart UNIV_2 apply(rule cSup_eq) by auto
     3.9  
    3.10  lemma infnorm_eq_1_2: "infnorm (x::real^2) = 1 \<longleftrightarrow>
    3.11          (abs(x$1) \<le> 1 \<and> abs(x$2) \<le> 1 \<and> (x$1 = -1 \<or> x$1 = 1 \<or> x$2 = -1 \<or> x$2 = 1))"
     4.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri Mar 22 10:41:43 2013 +0100
     4.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri Mar 22 10:41:43 2013 +0100
     4.3 @@ -8,6 +8,45 @@
     4.4    "~~/src/HOL/Library/Indicator_Function"
     4.5  begin
     4.6  
     4.7 +lemma cSup_finite_ge_iff: 
     4.8 +  fixes S :: "real set"
     4.9 +  assumes fS: "finite S" and Se: "S \<noteq> {}"
    4.10 +  shows "a \<le> Sup S \<longleftrightarrow> (\<exists> x \<in> S. a \<le> x)"
    4.11 +by (metis Max_ge Se cSup_eq_Max Max_in fS linorder_not_le less_le_trans)
    4.12 +
    4.13 +lemma cSup_finite_le_iff: 
    4.14 +  fixes S :: "real set"
    4.15 +  assumes fS: "finite S" and Se: "S \<noteq> {}"
    4.16 +  shows "a \<ge> Sup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> x)"
    4.17 +by (metis Max_ge Se cSup_eq_Max Max_in fS order_trans)
    4.18 +
    4.19 +lemma Inf: (* rename *)
    4.20 +  fixes S :: "real set"
    4.21 +  shows "S \<noteq> {} ==> (\<exists>b. b <=* S) ==> isGlb UNIV S (Inf S)"
    4.22 +by (auto simp add: isLb_def setle_def setge_def isGlb_def greatestP_def intro: cInf_lower cInf_greatest) 
    4.23 + 
    4.24 +lemma real_le_inf_subset:
    4.25 +  assumes "t \<noteq> {}" "t \<subseteq> s" "\<exists>b. b <=* s"
    4.26 +  shows "Inf s <= Inf (t::real set)"
    4.27 +  apply (rule isGlb_le_isLb)
    4.28 +  apply (rule Inf[OF assms(1)])
    4.29 +  apply (insert assms)
    4.30 +  apply (erule exE)
    4.31 +  apply (rule_tac x = b in exI)
    4.32 +  apply (auto simp: isLb_def setge_def intro: cInf_lower cInf_greatest)
    4.33 +  done
    4.34 +
    4.35 +lemma real_ge_sup_subset:
    4.36 +  assumes "t \<noteq> {}" "t \<subseteq> s" "\<exists>b. s *<= b"
    4.37 +  shows "Sup s >= Sup (t::real set)"
    4.38 +  apply (rule isLub_le_isUb)
    4.39 +  apply (rule isLub_cSup[OF assms(1)])
    4.40 +  apply (insert assms)
    4.41 +  apply (erule exE)
    4.42 +  apply (rule_tac x = b in exI)
    4.43 +  apply (auto simp: isUb_def setle_def intro: cSup_upper cSup_least)
    4.44 +  done
    4.45 +
    4.46  (*declare not_less[simp] not_le[simp]*)
    4.47  
    4.48  lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
    4.49 @@ -49,33 +88,6 @@
    4.50    shows "bounded_linear f"
    4.51    unfolding bounded_linear_def additive_def bounded_linear_axioms_def using assms by auto
    4.52  
    4.53 -lemma Inf: (* rename *)
    4.54 -  fixes S :: "real set"
    4.55 -  shows "S \<noteq> {} ==> (\<exists>b. b <=* S) ==> isGlb UNIV S (Inf S)"
    4.56 -by (auto simp add: isLb_def setle_def setge_def isGlb_def greatestP_def) 
    4.57 - 
    4.58 -lemma real_le_inf_subset:
    4.59 -  assumes "t \<noteq> {}" "t \<subseteq> s" "\<exists>b. b <=* s"
    4.60 -  shows "Inf s <= Inf (t::real set)"
    4.61 -  apply (rule isGlb_le_isLb)
    4.62 -  apply (rule Inf[OF assms(1)])
    4.63 -  apply (insert assms)
    4.64 -  apply (erule exE)
    4.65 -  apply (rule_tac x = b in exI)
    4.66 -  apply (auto simp: isLb_def setge_def)
    4.67 -  done
    4.68 -
    4.69 -lemma real_ge_sup_subset:
    4.70 -  assumes "t \<noteq> {}" "t \<subseteq> s" "\<exists>b. s *<= b"
    4.71 -  shows "Sup s >= Sup (t::real set)"
    4.72 -  apply (rule isLub_le_isUb)
    4.73 -  apply (rule Sup[OF assms(1)])
    4.74 -  apply (insert assms)
    4.75 -  apply (erule exE)
    4.76 -  apply (rule_tac x = b in exI)
    4.77 -  apply (auto simp: isUb_def setle_def)
    4.78 -  done
    4.79 -
    4.80  lemma bounded_linear_component [intro]: "bounded_linear (\<lambda>x::'a::euclidean_space. x \<bullet> k)"
    4.81    by (rule bounded_linear_inner_left)
    4.82  
    4.83 @@ -387,14 +399,14 @@
    4.84      interval_upperbound {a..b} = (b::'a::ordered_euclidean_space)"
    4.85    unfolding interval_upperbound_def euclidean_representation_setsum
    4.86    by (auto simp del: ex_simps simp add: Bex_def ex_simps[symmetric] eucl_le[where 'a='a] setle_def
    4.87 -           intro!: Sup_unique)
    4.88 +           intro!: cSup_unique)
    4.89  
    4.90  lemma interval_lowerbound[simp]:
    4.91    "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
    4.92      interval_lowerbound {a..b} = (a::'a::ordered_euclidean_space)"
    4.93    unfolding interval_lowerbound_def euclidean_representation_setsum
    4.94    by (auto simp del: ex_simps simp add: Bex_def ex_simps[symmetric] eucl_le[where 'a='a] setge_def
    4.95 -           intro!: Inf_unique)
    4.96 +           intro!: cInf_unique)
    4.97  
    4.98  lemmas interval_bounds = interval_upperbound interval_lowerbound
    4.99  
   4.100 @@ -3201,7 +3213,7 @@
   4.101        let ?goal = "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) < e"
   4.102        { presume "p\<noteq>{} \<Longrightarrow> ?goal" thus ?goal apply(cases "p={}") using goal1 by auto  }
   4.103        assume as':"p \<noteq> {}" from real_arch_simple[of "Sup((\<lambda>(x,k). norm(f x)) ` p)"] guess N ..
   4.104 -      hence N:"\<forall>x\<in>(\<lambda>(x, k). norm (f x)) ` p. x \<le> real N" apply(subst(asm) Sup_finite_le_iff) using as as' by auto
   4.105 +      hence N:"\<forall>x\<in>(\<lambda>(x, k). norm (f x)) ` p. x \<le> real N" apply(subst(asm) cSup_finite_le_iff) using as as' by auto
   4.106        have "\<forall>i. \<exists>q. q tagged_division_of {a..b} \<and> (d i) fine q \<and> (\<forall>(x, k)\<in>p. k \<subseteq> (d i) x \<longrightarrow> (x, k) \<in> q)"
   4.107          apply(rule,rule tagged_division_finer[OF as(1) d(1)]) by auto
   4.108        from choice[OF this] guess q .. note q=conjunctD3[OF this[rule_format]]
   4.109 @@ -5480,7 +5492,7 @@
   4.110    "\<forall>d. d division_of {a..b} \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
   4.111    shows "f absolutely_integrable_on {a..b}"
   4.112  proof- let ?S = "(\<lambda>d. setsum (\<lambda>k. norm(integral k f)) d) ` {d. d division_of {a..b} }" def i \<equiv> "Sup ?S"
   4.113 -  have i:"isLub UNIV ?S i" unfolding i_def apply(rule Sup)
   4.114 +  have i:"isLub UNIV ?S i" unfolding i_def apply(rule isLub_cSup)
   4.115      apply(rule elementary_interval) defer apply(rule_tac x=B in exI)
   4.116      apply(rule setleI) using assms(2) by auto
   4.117    show ?thesis apply(rule,rule assms) apply rule apply(subst has_integral[of _ i])
   4.118 @@ -5693,7 +5705,7 @@
   4.119    shows "f absolutely_integrable_on UNIV"
   4.120  proof(rule absolutely_integrable_onI,fact,rule)
   4.121    let ?S = "(\<lambda>d. setsum (\<lambda>k. norm(integral k f)) d) ` {d. d division_of  (\<Union>d)}" def i \<equiv> "Sup ?S"
   4.122 -  have i:"isLub UNIV ?S i" unfolding i_def apply(rule Sup)
   4.123 +  have i:"isLub UNIV ?S i" unfolding i_def apply(rule isLub_cSup)
   4.124      apply(rule elementary_interval) defer apply(rule_tac x=B in exI)
   4.125      apply(rule setleI) using assms(2) by auto
   4.126    have f_int:"\<And>a b. f absolutely_integrable_on {a..b}"
   4.127 @@ -6044,7 +6056,7 @@
   4.128          prefer 5
   4.129          unfolding real_norm_def
   4.130          apply rule
   4.131 -        apply (rule Inf_abs_ge)
   4.132 +        apply (rule cInf_abs_ge)
   4.133          prefer 5
   4.134          apply rule
   4.135          apply (rule_tac g = h in absolutely_integrable_integrable_bound_real)
   4.136 @@ -6065,11 +6077,11 @@
   4.137      fix x
   4.138      assume x: "x \<in> s"
   4.139      show "Inf {f j x |j. j \<in> {m..m + Suc k}} \<le> Inf {f j x |j. j \<in> {m..m + k}}"
   4.140 -      apply (rule Inf_ge)
   4.141 +      apply (rule cInf_ge)
   4.142        unfolding setge_def
   4.143        defer
   4.144        apply rule
   4.145 -      apply (subst Inf_finite_le_iff)
   4.146 +      apply (subst cInf_finite_le_iff)
   4.147        prefer 3
   4.148        apply (rule_tac x=xa in bexI)
   4.149        apply auto
   4.150 @@ -6119,7 +6131,7 @@
   4.151              prefer 3
   4.152              apply (rule,rule isGlbD1[OF i])
   4.153              prefer 3
   4.154 -            apply (subst Inf_finite_le_iff)
   4.155 +            apply (subst cInf_finite_le_iff)
   4.156              prefer 3
   4.157              apply (rule_tac x=y in bexI)
   4.158              using N goal1
   4.159 @@ -6146,7 +6158,7 @@
   4.160          apply(rule absolutely_integrable_sup_real)
   4.161          prefer 5 unfolding real_norm_def
   4.162          apply rule
   4.163 -        apply (rule Sup_abs_le)
   4.164 +        apply (rule cSup_abs_le)
   4.165          prefer 5
   4.166          apply rule
   4.167          apply (rule_tac g=h in absolutely_integrable_integrable_bound_real)
   4.168 @@ -6167,11 +6179,11 @@
   4.169      fix x
   4.170      assume x: "x\<in>s"
   4.171      show "Sup {f j x |j. j \<in> {m..m + Suc k}} \<ge> Sup {f j x |j. j \<in> {m..m + k}}"
   4.172 -      apply (rule Sup_le)
   4.173 +      apply (rule cSup_le)
   4.174        unfolding setle_def
   4.175        defer
   4.176        apply rule
   4.177 -      apply (subst Sup_finite_ge_iff)
   4.178 +      apply (subst cSup_finite_ge_iff)
   4.179        prefer 3
   4.180        apply (rule_tac x=y in bexI)
   4.181        apply auto
   4.182 @@ -6183,7 +6195,7 @@
   4.183        case goal1 note r=this
   4.184        have i: "isLub UNIV ?S i"
   4.185          unfolding i_def
   4.186 -        apply (rule Sup)
   4.187 +        apply (rule isLub_cSup)
   4.188          defer
   4.189          apply (rule_tac x="h x" in exI)
   4.190          unfolding setle_def
   4.191 @@ -6221,7 +6233,7 @@
   4.192            prefer 3
   4.193            apply (rule, rule isLubD1[OF i])
   4.194            prefer 3
   4.195 -          apply (subst Sup_finite_ge_iff)
   4.196 +          apply (subst cSup_finite_ge_iff)
   4.197            prefer 3
   4.198            apply (rule_tac x = y in bexI)
   4.199            using N goal1
   4.200 @@ -6246,7 +6258,7 @@
   4.201          apply fact+
   4.202          unfolding real_norm_def
   4.203          apply rule
   4.204 -        apply (rule Inf_abs_ge)
   4.205 +        apply (rule cInf_abs_ge)
   4.206          using assms(3)
   4.207          apply auto
   4.208          done
   4.209 @@ -6276,7 +6288,7 @@
   4.210          apply (rule_tac x=N in exI,safe)
   4.211          unfolding real_norm_def
   4.212          apply (rule le_less_trans[of _ "r/2"])
   4.213 -        apply (rule Inf_asclose)
   4.214 +        apply (rule cInf_asclose)
   4.215          apply safe
   4.216          defer
   4.217          apply (rule less_imp_le)
   4.218 @@ -6302,7 +6314,7 @@
   4.219          apply fact+
   4.220          unfolding real_norm_def
   4.221          apply rule
   4.222 -        apply (rule Sup_abs_le)
   4.223 +        apply (rule cSup_abs_le)
   4.224          using assms(3)
   4.225          apply auto
   4.226          done
   4.227 @@ -6330,7 +6342,7 @@
   4.228          apply (rule_tac x=N in exI,safe)
   4.229          unfolding real_norm_def
   4.230          apply (rule le_less_trans[of _ "r/2"])
   4.231 -        apply (rule Sup_asclose)
   4.232 +        apply (rule cSup_asclose)
   4.233          apply safe
   4.234          defer
   4.235          apply (rule less_imp_le)
   4.236 @@ -6364,7 +6376,7 @@
   4.237            assume x: "x \<in> s" 
   4.238            have *: "\<And>x y::real. x \<ge> - y \<Longrightarrow> - x \<le> y" by auto
   4.239            show "Inf {f j x |j. n \<le> j} \<le> f n x"
   4.240 -            apply (rule Inf_lower[where z="- h x"])
   4.241 +            apply (rule cInf_lower[where z="- h x"])
   4.242              defer
   4.243              apply (rule *)
   4.244              using assms(3)[rule_format,OF x]
   4.245 @@ -6377,7 +6389,7 @@
   4.246            fix x
   4.247            assume x: "x \<in> s"
   4.248            show "f n x \<le> Sup {f j x |j. n \<le> j}"
   4.249 -            apply (rule Sup_upper[where z="h x"])
   4.250 +            apply (rule cSup_upper[where z="h x"])
   4.251              defer
   4.252              using assms(3)[rule_format,OF x]
   4.253              unfolding real_norm_def abs_le_iff
     5.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Fri Mar 22 10:41:43 2013 +0100
     5.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Fri Mar 22 10:41:43 2013 +0100
     5.3 @@ -2498,6 +2498,9 @@
     5.4    "{ abs ((x::'a::euclidean_space) \<bullet> i) |i. i \<in> Basis} = (\<lambda>i. abs(x \<bullet> i)) ` Basis"
     5.5    by blast
     5.6  
     5.7 +lemma infnorm_Max: "infnorm (x::'a::euclidean_space) = Max ((\<lambda>i. abs(x \<bullet> i)) ` Basis)"
     5.8 +  by (simp add: infnorm_def infnorm_set_image cSup_eq_Max)
     5.9 +
    5.10  lemma infnorm_set_lemma:
    5.11    shows "finite {abs((x::'a::euclidean_space) \<bullet> i) |i. i \<in> Basis}"
    5.12    and "{abs(x \<bullet> i) |i. i \<in> Basis} \<noteq> {}"
    5.13 @@ -2505,41 +2508,22 @@
    5.14    by auto
    5.15  
    5.16  lemma infnorm_pos_le: "0 \<le> infnorm (x::'a::euclidean_space)"
    5.17 -  unfolding infnorm_def
    5.18 -  unfolding Sup_finite_ge_iff[ OF infnorm_set_lemma]
    5.19 -  unfolding infnorm_set_image
    5.20 -  by (auto simp: ex_in_conv)
    5.21 +  by (simp add: infnorm_Max Max_ge_iff ex_in_conv)
    5.22  
    5.23  lemma infnorm_triangle: "infnorm ((x::'a::euclidean_space) + y) \<le> infnorm x + infnorm y"
    5.24  proof -
    5.25 -  have th: "\<And>x y (z::real). x - y <= z \<longleftrightarrow> x - z <= y" by arith
    5.26 -  have th1: "\<And>S f. f ` S = { f i| i. i \<in> S}" by blast
    5.27 -  have th2: "\<And>x (y::real). abs(x + y) - abs(x) <= abs(y)" by arith
    5.28 +  have *: "\<And>a b c d :: real. \<bar>a\<bar> \<le> c \<Longrightarrow> \<bar>b\<bar> \<le> d \<Longrightarrow> \<bar>a + b\<bar> \<le> c + d"
    5.29 +    by simp
    5.30    show ?thesis
    5.31 -    unfolding infnorm_def 
    5.32 -    unfolding Sup_finite_le_iff[ OF infnorm_set_lemma[where 'a='a]]
    5.33 -    apply (subst diff_le_eq[symmetric])
    5.34 -    unfolding Sup_finite_ge_iff[ OF infnorm_set_lemma]
    5.35 -    unfolding infnorm_set_image bex_simps
    5.36 -    apply (subst th)
    5.37 -    unfolding th1
    5.38 -    unfolding Sup_finite_ge_iff[ OF infnorm_set_lemma[where 'a='a]]
    5.39 -    unfolding infnorm_set_image ball_simps bex_simps
    5.40 -    apply (simp add: inner_add_left)
    5.41 -    apply (metis th2)
    5.42 -    done
    5.43 +    by (auto simp: infnorm_Max inner_add_left intro!: *)
    5.44  qed
    5.45  
    5.46  lemma infnorm_eq_0: "infnorm x = 0 \<longleftrightarrow> (x::_::euclidean_space) = 0"
    5.47  proof -
    5.48 -  have "infnorm x <= 0 \<longleftrightarrow> x = 0"
    5.49 -    unfolding infnorm_def
    5.50 -    unfolding Sup_finite_le_iff[OF infnorm_set_lemma]
    5.51 -    unfolding infnorm_set_image ball_simps
    5.52 -    apply (subst (1) euclidean_eq_iff)
    5.53 -    apply auto
    5.54 -    done
    5.55 -  then show ?thesis using infnorm_pos_le[of x] by simp
    5.56 +  have "infnorm x \<le> 0 \<longleftrightarrow> x = 0"
    5.57 +    unfolding infnorm_Max by (simp add: euclidean_all_zero_iff)
    5.58 +  then show ?thesis
    5.59 +    using infnorm_pos_le[of x] by simp
    5.60  qed
    5.61  
    5.62  lemma infnorm_0: "infnorm 0 = 0"
    5.63 @@ -2573,40 +2557,24 @@
    5.64    using infnorm_pos_le[of x] by arith
    5.65  
    5.66  lemma Basis_le_infnorm:
    5.67 -  assumes b: "b \<in> Basis" shows "\<bar>x \<bullet> b\<bar> \<le> infnorm (x::'a::euclidean_space)"
    5.68 -  unfolding infnorm_def
    5.69 -proof (subst Sup_finite_ge_iff)
    5.70 -  let ?S = "{\<bar>x \<bullet> i\<bar> |i. i \<in> Basis}"
    5.71 -  show "finite ?S" by (rule infnorm_set_lemma)
    5.72 -  show "?S \<noteq> {}" by auto
    5.73 -  show "Bex ?S (op \<le> \<bar>x \<bullet> b\<bar>)"
    5.74 -     using b by (auto intro!: exI[of _ b])
    5.75 -qed
    5.76 -
    5.77 -lemma infnorm_mul_lemma: "infnorm(a *\<^sub>R x) <= \<bar>a\<bar> * infnorm x"
    5.78 -  apply (subst infnorm_def)
    5.79 -  unfolding Sup_finite_le_iff[OF infnorm_set_lemma]
    5.80 -  unfolding infnorm_set_image ball_simps inner_scaleR abs_mult
    5.81 -  using Basis_le_infnorm[of _ x]
    5.82 -  apply (auto intro: mult_mono)
    5.83 -  done
    5.84 +  "b \<in> Basis \<Longrightarrow> \<bar>x \<bullet> b\<bar> \<le> infnorm (x::'a::euclidean_space)"
    5.85 +  by (simp add: infnorm_Max)
    5.86  
    5.87  lemma infnorm_mul: "infnorm(a *\<^sub>R x) = abs a * infnorm x"
    5.88 -proof -
    5.89 -  { assume a0: "a = 0" then have ?thesis by (simp add: infnorm_0) }
    5.90 -  moreover
    5.91 -  { assume a0: "a \<noteq> 0"
    5.92 -    from a0 have th: "(1/a) *\<^sub>R (a *\<^sub>R x) = x" by simp
    5.93 -    from a0 have ap: "\<bar>a\<bar> > 0" by arith
    5.94 -    from infnorm_mul_lemma[of "1/a" "a *\<^sub>R x"]
    5.95 -    have "infnorm x \<le> 1/\<bar>a\<bar> * infnorm (a*\<^sub>R x)"
    5.96 -      unfolding th by simp
    5.97 -    with ap have "\<bar>a\<bar> * infnorm x \<le> \<bar>a\<bar> * (1/\<bar>a\<bar> * infnorm (a *\<^sub>R x))" by (simp add: field_simps)
    5.98 -    then have "\<bar>a\<bar> * infnorm x \<le> infnorm (a*\<^sub>R x)"
    5.99 -      using ap by (simp add: field_simps)
   5.100 -    with infnorm_mul_lemma[of a x] have ?thesis by arith }
   5.101 -  ultimately show ?thesis by blast
   5.102 -qed
   5.103 +  unfolding infnorm_Max
   5.104 +proof (safe intro!: Max_eqI)
   5.105 +  let ?B = "(\<lambda>i. \<bar>x \<bullet> i\<bar>) ` Basis"
   5.106 +  show "\<And>b :: 'a. b \<in> Basis \<Longrightarrow> \<bar>a *\<^sub>R x \<bullet> b\<bar> \<le> \<bar>a\<bar> * Max ?B"
   5.107 +    by (simp add: abs_mult mult_left_mono)
   5.108 +
   5.109 +  from Max_in[of ?B] obtain b where "b \<in> Basis" "Max ?B = \<bar>x \<bullet> b\<bar>"
   5.110 +    by (auto simp del: Max_in)
   5.111 +  then show "\<bar>a\<bar> * Max ((\<lambda>i. \<bar>x \<bullet> i\<bar>) ` Basis) \<in> (\<lambda>i. \<bar>a *\<^sub>R x \<bullet> i\<bar>) ` Basis"
   5.112 +    by (intro image_eqI[where x=b]) (auto simp: abs_mult)
   5.113 +qed simp
   5.114 +
   5.115 +lemma infnorm_mul_lemma: "infnorm(a *\<^sub>R x) \<le> \<bar>a\<bar> * infnorm x"
   5.116 +  unfolding infnorm_mul ..
   5.117  
   5.118  lemma infnorm_pos_lt: "infnorm x > 0 \<longleftrightarrow> x \<noteq> 0"
   5.119    using infnorm_pos_le[of x] infnorm_eq_0[of x] by arith
   5.120 @@ -2614,15 +2582,13 @@
   5.121  text {* Prove that it differs only up to a bound from Euclidean norm. *}
   5.122  
   5.123  lemma infnorm_le_norm: "infnorm x \<le> norm x"
   5.124 -  unfolding infnorm_def Sup_finite_le_iff[OF infnorm_set_lemma]
   5.125 -  unfolding infnorm_set_image  ball_simps
   5.126 -  by (metis Basis_le_norm)
   5.127 +  by (simp add: Basis_le_norm infnorm_Max)
   5.128  
   5.129  lemma euclidean_inner: "inner x y = (\<Sum>b\<in>Basis. (x \<bullet> b) * (y \<bullet> b))"
   5.130    by (subst (1 2) euclidean_representation[symmetric, where 'a='a])
   5.131       (simp add: inner_setsum_left inner_setsum_right setsum_cases inner_Basis ac_simps if_distrib)
   5.132  
   5.133 -lemma norm_le_infnorm: "norm(x) <= sqrt DIM('a) * infnorm(x::'a::euclidean_space)"
   5.134 +lemma norm_le_infnorm: "norm x \<le> sqrt DIM('a) * infnorm(x::'a::euclidean_space)"
   5.135  proof -
   5.136    let ?d = "DIM('a)"
   5.137    have "real ?d \<ge> 0" by simp
   5.138 @@ -2639,10 +2605,7 @@
   5.139      apply (auto simp add: power2_eq_square[symmetric])
   5.140      apply (subst power2_abs[symmetric])
   5.141      apply (rule power_mono)
   5.142 -    unfolding infnorm_def Sup_finite_ge_iff[OF infnorm_set_lemma]
   5.143 -    unfolding infnorm_set_image bex_simps
   5.144 -    apply (rule_tac x=i in bexI)
   5.145 -    apply auto
   5.146 +    apply (auto simp: infnorm_Max)
   5.147      done
   5.148    from real_le_lsqrt[OF inner_ge_zero th th1]
   5.149    show ?thesis unfolding norm_eq_sqrt_inner id_def .
     6.1 --- a/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Fri Mar 22 10:41:43 2013 +0100
     6.2 +++ b/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Fri Mar 22 10:41:43 2013 +0100
     6.3 @@ -58,7 +58,7 @@
     6.4      hence Se: "?S \<noteq> {}" by auto
     6.5      from linear_bounded[OF lf] have b: "\<exists> b. ?S *<= b"
     6.6        unfolding norm_bound_generalize[OF lf, symmetric] by (auto simp add: setle_def)
     6.7 -    {from Sup[OF Se b, unfolded onorm_def[symmetric]]
     6.8 +    { from isLub_cSup[OF Se b, unfolded onorm_def[symmetric]]
     6.9        show "norm (f x) <= onorm f * norm x"
    6.10          apply -
    6.11          apply (rule spec[where x = x])
    6.12 @@ -66,7 +66,7 @@
    6.13          by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)}
    6.14      {
    6.15        show "\<forall>x. norm (f x) <= b * norm x \<Longrightarrow> onorm f <= b"
    6.16 -        using Sup[OF Se b, unfolded onorm_def[symmetric]]
    6.17 +        using isLub_cSup[OF Se b, unfolded onorm_def[symmetric]]
    6.18          unfolding norm_bound_generalize[OF lf, symmetric]
    6.19          by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)}
    6.20    }
    6.21 @@ -93,7 +93,7 @@
    6.22      by (auto simp: SOME_Basis intro!: exI[of _ "SOME i. i \<in> Basis"])
    6.23    show ?thesis
    6.24      unfolding onorm_def th
    6.25 -    apply (rule Sup_unique) by (simp_all  add: setle_def)
    6.26 +    apply (rule cSup_unique) by (simp_all  add: setle_def)
    6.27  qed
    6.28  
    6.29  lemma onorm_pos_lt: assumes lf: "linear (f::'a::euclidean_space \<Rightarrow> 'b::euclidean_space)"
     7.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Mar 22 10:41:43 2013 +0100
     7.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Mar 22 10:41:43 2013 +0100
     7.3 @@ -1401,7 +1401,7 @@
     7.4      show "(\<lambda>n. f (S n)) ----> Inf (f ` ({x<..} \<inter> I))"
     7.5      proof (rule LIMSEQ_I, rule ccontr)
     7.6        fix r :: real assume "0 < r"
     7.7 -      with Inf_close[of "f ` ({x<..} \<inter> I)" r]
     7.8 +      with cInf_close[of "f ` ({x<..} \<inter> I)" r]
     7.9        obtain y where y: "x < y" "y \<in> I" "f y < Inf (f ` ({x <..} \<inter> I)) + r" by auto
    7.10        from `x < y` have "0 < y - x" by auto
    7.11        from S(2)[THEN LIMSEQ_D, OF this]
    7.12 @@ -1409,7 +1409,7 @@
    7.13        
    7.14        assume "\<not> (\<exists>N. \<forall>n\<ge>N. norm (f (S n) - Inf (f ` ({x<..} \<inter> I))) < r)"
    7.15        moreover have "\<And>n. Inf (f ` ({x<..} \<inter> I)) \<le> f (S n)"
    7.16 -        using S bnd by (intro Inf_lower[where z=K]) auto
    7.17 +        using S bnd by (intro cInf_lower[where z=K]) auto
    7.18        ultimately obtain n where n: "N \<le> n" "r + Inf (f ` ({x<..} \<inter> I)) \<le> f (S n)"
    7.19          by (auto simp: not_less field_simps)
    7.20        with N[OF n(1)] mono[OF _ `y \<in> I`, of "S n"] S(1)[THEN spec, of n] y
    7.21 @@ -1727,11 +1727,11 @@
    7.22    unfolding closure_approachable
    7.23  proof safe
    7.24    have *: "\<forall>x\<in>S. Inf S \<le> x"
    7.25 -    using Inf_lower_EX[of _ S] assms by metis
    7.26 +    using cInf_lower_EX[of _ S] assms by metis
    7.27  
    7.28    fix e :: real assume "0 < e"
    7.29    then obtain x where x: "x \<in> S" "x < Inf S + e"
    7.30 -    using Inf_close `S \<noteq> {}` by auto
    7.31 +    using cInf_close `S \<noteq> {}` by auto
    7.32    moreover then have "x > Inf S - e" using * by auto
    7.33    ultimately have "abs (x - Inf S) < e" by (simp add: abs_diff_less_iff)
    7.34    then show "\<exists>x\<in>S. dist x (Inf S) < e"
    7.35 @@ -1785,13 +1785,13 @@
    7.36  
    7.37  lemma infdist_nonneg:
    7.38    shows "0 \<le> infdist x A"
    7.39 -  using assms by (auto simp add: infdist_def)
    7.40 +  using assms by (auto simp add: infdist_def intro: cInf_greatest)
    7.41  
    7.42  lemma infdist_le:
    7.43    assumes "a \<in> A"
    7.44    assumes "d = dist x a"
    7.45    shows "infdist x A \<le> d"
    7.46 -  using assms by (auto intro!: SupInf.Inf_lower[where z=0] simp add: infdist_def)
    7.47 +  using assms by (auto intro!: cInf_lower[where z=0] simp add: infdist_def)
    7.48  
    7.49  lemma infdist_zero[simp]:
    7.50    assumes "a \<in> A" shows "infdist a A = 0"
    7.51 @@ -1807,13 +1807,13 @@
    7.52  next
    7.53    assume "A \<noteq> {}" then obtain a where "a \<in> A" by auto
    7.54    have "infdist x A \<le> Inf {dist x y + dist y a |a. a \<in> A}"
    7.55 -  proof
    7.56 +  proof (rule cInf_greatest)
    7.57      from `A \<noteq> {}` show "{dist x y + dist y a |a. a \<in> A} \<noteq> {}" by simp
    7.58      fix d assume "d \<in> {dist x y + dist y a |a. a \<in> A}"
    7.59      then obtain a where d: "d = dist x y + dist y a" "a \<in> A" by auto
    7.60      show "infdist x A \<le> d"
    7.61        unfolding infdist_notempty[OF `A \<noteq> {}`]
    7.62 -    proof (rule Inf_lower2)
    7.63 +    proof (rule cInf_lower2)
    7.64        show "dist x a \<in> {dist x a |a. a \<in> A}" using `a \<in> A` by auto
    7.65        show "dist x a \<le> d" unfolding d by (rule dist_triangle)
    7.66        fix d assume "d \<in> {dist x a |a. a \<in> A}"
    7.67 @@ -1822,20 +1822,19 @@
    7.68      qed
    7.69    qed
    7.70    also have "\<dots> = dist x y + infdist y A"
    7.71 -  proof (rule Inf_eq, safe)
    7.72 +  proof (rule cInf_eq, safe)
    7.73      fix a assume "a \<in> A"
    7.74      thus "dist x y + infdist y A \<le> dist x y + dist y a" by (auto intro: infdist_le)
    7.75    next
    7.76      fix i assume inf: "\<And>d. d \<in> {dist x y + dist y a |a. a \<in> A} \<Longrightarrow> i \<le> d"
    7.77      hence "i - dist x y \<le> infdist y A" unfolding infdist_notempty[OF `A \<noteq> {}`] using `a \<in> A`
    7.78 -      by (intro Inf_greatest) (auto simp: field_simps)
    7.79 +      by (intro cInf_greatest) (auto simp: field_simps)
    7.80      thus "i \<le> dist x y + infdist y A" by simp
    7.81    qed
    7.82    finally show ?thesis by simp
    7.83  qed
    7.84  
    7.85 -lemma
    7.86 -  in_closure_iff_infdist_zero:
    7.87 +lemma in_closure_iff_infdist_zero:
    7.88    assumes "A \<noteq> {}"
    7.89    shows "x \<in> closure A \<longleftrightarrow> infdist x A = 0"
    7.90  proof
    7.91 @@ -1859,13 +1858,12 @@
    7.92      assume "\<not> (\<exists>y\<in>A. dist y x < e)"
    7.93      hence "infdist x A \<ge> e" using `a \<in> A`
    7.94        unfolding infdist_def
    7.95 -      by (force simp: dist_commute)
    7.96 +      by (force simp: dist_commute intro: cInf_greatest)
    7.97      with x `0 < e` show False by auto
    7.98    qed
    7.99  qed
   7.100  
   7.101 -lemma
   7.102 -  in_closed_iff_infdist_zero:
   7.103 +lemma in_closed_iff_infdist_zero:
   7.104    assumes "closed A" "A \<noteq> {}"
   7.105    shows "x \<in> A \<longleftrightarrow> infdist x A = 0"
   7.106  proof -
   7.107 @@ -2326,16 +2324,19 @@
   7.108  proof
   7.109    fix x assume "x\<in>S"
   7.110    thus "x \<le> Sup S"
   7.111 -    by (metis SupInf.Sup_upper abs_le_D1 assms(1) bounded_real)
   7.112 +    by (metis cSup_upper abs_le_D1 assms(1) bounded_real)
   7.113  next
   7.114    show "\<forall>b. (\<forall>x\<in>S. x \<le> b) \<longrightarrow> Sup S \<le> b" using assms
   7.115 -    by (metis SupInf.Sup_least)
   7.116 +    by (metis cSup_least)
   7.117  qed
   7.118  
   7.119  lemma Sup_insert:
   7.120    fixes S :: "real set"
   7.121    shows "bounded S ==> Sup(insert x S) = (if S = {} then x else max x (Sup S))" 
   7.122 -by auto (metis Int_absorb Sup_insert_nonempty assms bounded_has_Sup(1) disjoint_iff_not_equal) 
   7.123 +  apply (subst cSup_insert_If)
   7.124 +  apply (rule bounded_has_Sup(1)[of S, rule_format])
   7.125 +  apply (auto simp: sup_max)
   7.126 +  done
   7.127  
   7.128  lemma Sup_insert_finite:
   7.129    fixes S :: "real set"
   7.130 @@ -2352,16 +2353,19 @@
   7.131    fix x assume "x\<in>S"
   7.132    from assms(1) obtain a where a:"\<forall>x\<in>S. \<bar>x\<bar> \<le> a" unfolding bounded_real by auto
   7.133    thus "x \<ge> Inf S" using `x\<in>S`
   7.134 -    by (metis Inf_lower_EX abs_le_D2 minus_le_iff)
   7.135 +    by (metis cInf_lower_EX abs_le_D2 minus_le_iff)
   7.136  next
   7.137    show "\<forall>b. (\<forall>x\<in>S. x >= b) \<longrightarrow> Inf S \<ge> b" using assms
   7.138 -    by (metis SupInf.Inf_greatest)
   7.139 +    by (metis cInf_greatest)
   7.140  qed
   7.141  
   7.142  lemma Inf_insert:
   7.143    fixes S :: "real set"
   7.144    shows "bounded S ==> Inf(insert x S) = (if S = {} then x else min x (Inf S))" 
   7.145 -by auto (metis Int_absorb Inf_insert_nonempty bounded_has_Inf(1) disjoint_iff_not_equal)
   7.146 +  apply (subst cInf_insert_if)
   7.147 +  apply (rule bounded_has_Inf(1)[of S, rule_format])
   7.148 +  apply (auto simp: inf_min)
   7.149 +  done
   7.150  
   7.151  lemma Inf_insert_finite:
   7.152    fixes S :: "real set"
   7.153 @@ -3125,7 +3129,7 @@
   7.154  
   7.155  lemma cauchy_def:
   7.156    "Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N --> dist(s m)(s n) < e)"
   7.157 -unfolding Cauchy_def by blast
   7.158 +unfolding Cauchy_def by metis
   7.159  
   7.160  fun helper_1::"('a::metric_space set) \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> 'a" where
   7.161    "helper_1 s e n = (SOME y::'a. y \<in> s \<and> (\<forall>m<n. \<not> (dist (helper_1 s e m) y < e)))"
   7.162 @@ -5197,7 +5201,7 @@
   7.163    from s obtain z d where z: "\<And>x. x \<in> s \<Longrightarrow> dist z x \<le> d"
   7.164      unfolding bounded_def by auto
   7.165    have "dist x y \<le> Sup ?D"
   7.166 -  proof (rule Sup_upper, safe)
   7.167 +  proof (rule cSup_upper, safe)
   7.168      fix a b assume "a \<in> s" "b \<in> s"
   7.169      with z[of a] z[of b] dist_triangle[of a b z]
   7.170      show "dist a b \<le> 2 * d"
   7.171 @@ -5219,7 +5223,7 @@
   7.172      by (auto simp: diameter_def)
   7.173    then have "?D \<noteq> {}" by auto
   7.174    ultimately have "Sup ?D \<le> d"
   7.175 -    by (intro Sup_least) (auto simp: not_less)
   7.176 +    by (intro cSup_least) (auto simp: not_less)
   7.177    with `d < diameter s` `s \<noteq> {}` show False
   7.178      by (auto simp: diameter_def)
   7.179  qed
   7.180 @@ -5239,7 +5243,7 @@
   7.181    then obtain x y where xys:"x\<in>s" "y\<in>s" and xy:"\<forall>u\<in>s. \<forall>v\<in>s. dist u v \<le> dist x y"
   7.182      using compact_sup_maxdistance[OF assms] by auto
   7.183    hence "diameter s \<le> dist x y"
   7.184 -    unfolding diameter_def by clarsimp (rule Sup_least, fast+)
   7.185 +    unfolding diameter_def by clarsimp (rule cSup_least, fast+)
   7.186    thus ?thesis
   7.187      by (metis b diameter_bounded_bound order_antisym xys)
   7.188  qed
   7.189 @@ -6675,5 +6679,4 @@
   7.190  
   7.191  declare tendsto_const [intro] (* FIXME: move *)
   7.192  
   7.193 -
   7.194  end
     8.1 --- a/src/HOL/Probability/Probability_Measure.thy	Fri Mar 22 10:41:43 2013 +0100
     8.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Fri Mar 22 10:41:43 2013 +0100
     8.3 @@ -159,11 +159,11 @@
     8.4    moreover
     8.5    { fix y assume y: "y \<in> I"
     8.6      with q(2) `open I` have "Sup ((\<lambda>x. q x + ?F x * (y - x)) ` I) = q y"
     8.7 -      by (auto intro!: Sup_eq_maximum convex_le_Inf_differential image_eqI[OF _ y] simp: interior_open) }
     8.8 +      by (auto intro!: cSup_eq_maximum convex_le_Inf_differential image_eqI[OF _ y] simp: interior_open) }
     8.9    ultimately have "q (expectation X) = Sup ((\<lambda>x. q x + ?F x * (expectation X - x)) ` I)"
    8.10      by simp
    8.11    also have "\<dots> \<le> expectation (\<lambda>w. q (X w))"
    8.12 -  proof (rule Sup_least)
    8.13 +  proof (rule cSup_least)
    8.14      show "(\<lambda>x. q x + ?F x * (expectation X - x)) ` I \<noteq> {}"
    8.15        using `I \<noteq> {}` by auto
    8.16    next
     9.1 --- a/src/HOL/SupInf.thy	Fri Mar 22 10:41:43 2013 +0100
     9.2 +++ b/src/HOL/SupInf.thy	Fri Mar 22 10:41:43 2013 +0100
     9.3 @@ -6,210 +6,341 @@
     9.4  imports RComplete
     9.5  begin
     9.6  
     9.7 -instantiation real :: Sup 
     9.8 +lemma Sup_fin_eq_Max: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup_fin X = Max X"
     9.9 +  by (induct X rule: finite_ne_induct) (simp_all add: sup_max)
    9.10 +
    9.11 +lemma Inf_fin_eq_Min: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf_fin X = Min X"
    9.12 +  by (induct X rule: finite_ne_induct) (simp_all add: inf_min)
    9.13 +
    9.14 +text {*
    9.15 +
    9.16 +To avoid name classes with the @{class complete_lattice}-class we prefix @{const Sup} and
    9.17 +@{const Inf} in theorem names with c.
    9.18 +
    9.19 +*}
    9.20 +
    9.21 +class conditional_complete_lattice = lattice + Sup + Inf +
    9.22 +  assumes cInf_lower: "x \<in> X \<Longrightarrow> (\<And>a. a \<in> X \<Longrightarrow> z \<le> a) \<Longrightarrow> Inf X \<le> x"
    9.23 +    and cInf_greatest: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf X"
    9.24 +  assumes cSup_upper: "x \<in> X \<Longrightarrow> (\<And>a. a \<in> X \<Longrightarrow> a \<le> z) \<Longrightarrow> x \<le> Sup X"
    9.25 +    and cSup_least: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X \<le> z"
    9.26  begin
    9.27 -definition
    9.28 -  Sup_real_def: "Sup X == (LEAST z::real. \<forall>x\<in>X. x\<le>z)"
    9.29 +
    9.30 +lemma cSup_eq_maximum: (*REAL_SUP_MAX in HOL4*)
    9.31 +  "z \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X = z"
    9.32 +  by (blast intro: antisym cSup_upper cSup_least)
    9.33 +
    9.34 +lemma cInf_eq_minimum: (*REAL_INF_MIN in HOL4*)
    9.35 +  "z \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X = z"
    9.36 +  by (intro antisym cInf_lower[of z X z] cInf_greatest[of X z]) auto
    9.37 +
    9.38 +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)"
    9.39 +  by (metis order_trans cSup_upper cSup_least)
    9.40 +
    9.41 +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)"
    9.42 +  by (metis order_trans cInf_lower cInf_greatest)
    9.43 +
    9.44 +lemma cSup_singleton [simp]: "Sup {x} = x"
    9.45 +  by (intro cSup_eq_maximum) auto
    9.46 +
    9.47 +lemma cInf_singleton [simp]: "Inf {x} = x"
    9.48 +  by (intro cInf_eq_minimum) auto
    9.49 +
    9.50 +lemma cSup_upper2: (*REAL_IMP_LE_SUP in HOL4*)
    9.51 +  "x \<in> X \<Longrightarrow> y \<le> x \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y \<le> Sup X"
    9.52 +  by (metis cSup_upper order_trans)
    9.53 + 
    9.54 +lemma cInf_lower2:
    9.55 +  "x \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X \<le> y"
    9.56 +  by (metis cInf_lower order_trans)
    9.57 +
    9.58 +lemma cSup_upper_EX: "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> x \<le> z \<Longrightarrow> x \<le> Sup X"
    9.59 +  by (blast intro: cSup_upper)
    9.60 +
    9.61 +lemma cInf_lower_EX:  "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> z \<le> x \<Longrightarrow> Inf X \<le> x"
    9.62 +  by (blast intro: cInf_lower)
    9.63 +
    9.64 +lemma cSup_eq_non_empty:
    9.65 +  assumes 1: "X \<noteq> {}"
    9.66 +  assumes 2: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a"
    9.67 +  assumes 3: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y"
    9.68 +  shows "Sup X = a"
    9.69 +  by (intro 3 1 antisym cSup_least) (auto intro: 2 1 cSup_upper)
    9.70 +
    9.71 +lemma cInf_eq_non_empty:
    9.72 +  assumes 1: "X \<noteq> {}"
    9.73 +  assumes 2: "\<And>x. x \<in> X \<Longrightarrow> a \<le> x"
    9.74 +  assumes 3: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a"
    9.75 +  shows "Inf X = a"
    9.76 +  by (intro 3 1 antisym cInf_greatest) (auto intro: 2 1 cInf_lower)
    9.77 +
    9.78 +lemma cSup_insert: 
    9.79 +  assumes x: "X \<noteq> {}"
    9.80 +      and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
    9.81 +  shows "Sup (insert a X) = sup a (Sup X)"
    9.82 +proof (intro cSup_eq_non_empty)
    9.83 +  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)
    9.84 +qed (auto intro: le_supI2 z cSup_upper)
    9.85  
    9.86 -instance ..
    9.87 +lemma cInf_insert: 
    9.88 +  assumes x: "X \<noteq> {}"
    9.89 +      and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
    9.90 +  shows "Inf (insert a X) = inf a (Inf X)"
    9.91 +proof (intro cInf_eq_non_empty)
    9.92 +  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)
    9.93 +qed (auto intro: le_infI2 z cInf_lower)
    9.94 +
    9.95 +lemma cSup_insert_If: 
    9.96 +  "(\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup (insert a X) = (if X = {} then a else sup a (Sup X))"
    9.97 +  using cSup_insert[of X z] by simp
    9.98 +
    9.99 +lemma cInf_insert_if: 
   9.100 +  "(\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf (insert a X) = (if X = {} then a else inf a (Inf X))"
   9.101 +  using cInf_insert[of X z] by simp
   9.102 +
   9.103 +lemma le_cSup_finite: "finite X \<Longrightarrow> x \<in> X \<Longrightarrow> x \<le> Sup X"
   9.104 +proof (induct X arbitrary: x rule: finite_induct)
   9.105 +  case (insert x X y) then show ?case
   9.106 +    apply (cases "X = {}")
   9.107 +    apply simp
   9.108 +    apply (subst cSup_insert[of _ "Sup X"])
   9.109 +    apply (auto intro: le_supI2)
   9.110 +    done
   9.111 +qed simp
   9.112 +
   9.113 +lemma cInf_le_finite: "finite X \<Longrightarrow> x \<in> X \<Longrightarrow> Inf X \<le> x"
   9.114 +proof (induct X arbitrary: x rule: finite_induct)
   9.115 +  case (insert x X y) then show ?case
   9.116 +    apply (cases "X = {}")
   9.117 +    apply simp
   9.118 +    apply (subst cInf_insert[of _ "Inf X"])
   9.119 +    apply (auto intro: le_infI2)
   9.120 +    done
   9.121 +qed simp
   9.122 +
   9.123 +lemma cSup_eq_Sup_fin: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup X = Sup_fin X"
   9.124 +proof (induct X rule: finite_ne_induct)
   9.125 +  case (insert x X) then show ?case
   9.126 +    using cSup_insert[of X "Sup_fin X" x] le_cSup_finite[of X] by simp
   9.127 +qed simp
   9.128 +
   9.129 +lemma cInf_eq_Inf_fin: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Inf_fin X"
   9.130 +proof (induct X rule: finite_ne_induct)
   9.131 +  case (insert x X) then show ?case
   9.132 +    using cInf_insert[of X "Inf_fin X" x] cInf_le_finite[of X] by simp
   9.133 +qed simp
   9.134 +
   9.135 +lemma cSup_atMost[simp]: "Sup {..x} = x"
   9.136 +  by (auto intro!: cSup_eq_maximum)
   9.137 +
   9.138 +lemma cSup_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Sup {y<..x} = x"
   9.139 +  by (auto intro!: cSup_eq_maximum)
   9.140 +
   9.141 +lemma cSup_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Sup {y..x} = x"
   9.142 +  by (auto intro!: cSup_eq_maximum)
   9.143 +
   9.144 +lemma cInf_atLeast[simp]: "Inf {x..} = x"
   9.145 +  by (auto intro!: cInf_eq_minimum)
   9.146 +
   9.147 +lemma cInf_atLeastLessThan[simp]: "y < x \<Longrightarrow> Inf {y..<x} = y"
   9.148 +  by (auto intro!: cInf_eq_minimum)
   9.149 +
   9.150 +lemma cInf_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Inf {y..x} = y"
   9.151 +  by (auto intro!: cInf_eq_minimum)
   9.152 +
   9.153  end
   9.154  
   9.155 -instantiation real :: Inf 
   9.156 +instance complete_lattice \<subseteq> conditional_complete_lattice
   9.157 +  by default (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest)
   9.158 +
   9.159 +lemma isLub_cSup: 
   9.160 +  "(S::'a :: conditional_complete_lattice set) \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> isLub UNIV S (Sup S)"
   9.161 +  by  (auto simp add: isLub_def setle_def leastP_def isUb_def
   9.162 +            intro!: setgeI intro: cSup_upper cSup_least)
   9.163 +
   9.164 +lemma cSup_eq:
   9.165 +  fixes a :: "'a :: {conditional_complete_lattice, no_bot}"
   9.166 +  assumes upper: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a"
   9.167 +  assumes least: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y"
   9.168 +  shows "Sup X = a"
   9.169 +proof cases
   9.170 +  assume "X = {}" with lt_ex[of a] least show ?thesis by (auto simp: less_le_not_le)
   9.171 +qed (intro cSup_eq_non_empty assms)
   9.172 +
   9.173 +lemma cInf_eq:
   9.174 +  fixes a :: "'a :: {conditional_complete_lattice, no_top}"
   9.175 +  assumes upper: "\<And>x. x \<in> X \<Longrightarrow> a \<le> x"
   9.176 +  assumes least: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a"
   9.177 +  shows "Inf X = a"
   9.178 +proof cases
   9.179 +  assume "X = {}" with gt_ex[of a] least show ?thesis by (auto simp: less_le_not_le)
   9.180 +qed (intro cInf_eq_non_empty assms)
   9.181 +
   9.182 +lemma cSup_le: "(S::'a::conditional_complete_lattice set) \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b"
   9.183 +  by (metis cSup_least setle_def)
   9.184 +
   9.185 +lemma cInf_ge: "(S::'a :: conditional_complete_lattice set) \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b"
   9.186 +  by (metis cInf_greatest setge_def)
   9.187 +
   9.188 +class conditional_complete_linorder = conditional_complete_lattice + linorder
   9.189  begin
   9.190 +
   9.191 +lemma less_cSup_iff : (*REAL_SUP_LE in HOL4*)
   9.192 +  "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y < Sup X \<longleftrightarrow> (\<exists>x\<in>X. y < x)"
   9.193 +  by (rule iffI) (metis cSup_least not_less, metis cSup_upper less_le_trans)
   9.194 +
   9.195 +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)"
   9.196 +  by (rule iffI) (metis cInf_greatest not_less, metis cInf_lower le_less_trans)
   9.197 +
   9.198 +lemma less_cSupE:
   9.199 +  assumes "y < Sup X" "X \<noteq> {}" obtains x where "x \<in> X" "y < x"
   9.200 +  by (metis cSup_least assms not_le that)
   9.201 +
   9.202 +lemma complete_interval:
   9.203 +  assumes "a < b" and "P a" and "\<not> P b"
   9.204 +  shows "\<exists>c. a \<le> c \<and> c \<le> b \<and> (\<forall>x. a \<le> x \<and> x < c \<longrightarrow> P x) \<and>
   9.205 +             (\<forall>d. (\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x) \<longrightarrow> d \<le> c)"
   9.206 +proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x & x < d --> P x}"], auto)
   9.207 +  show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
   9.208 +    by (rule cSup_upper [where z=b], auto)
   9.209 +       (metis `a < b` `\<not> P b` linear less_le)
   9.210 +next
   9.211 +  show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b"
   9.212 +    apply (rule cSup_least) 
   9.213 +    apply auto
   9.214 +    apply (metis less_le_not_le)
   9.215 +    apply (metis `a<b` `~ P b` linear less_le)
   9.216 +    done
   9.217 +next
   9.218 +  fix x
   9.219 +  assume x: "a \<le> x" and lt: "x < Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
   9.220 +  show "P x"
   9.221 +    apply (rule less_cSupE [OF lt], auto)
   9.222 +    apply (metis less_le_not_le)
   9.223 +    apply (metis x) 
   9.224 +    done
   9.225 +next
   9.226 +  fix d
   9.227 +    assume 0: "\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x"
   9.228 +    thus "d \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
   9.229 +      by (rule_tac z="b" in cSup_upper, auto) 
   9.230 +         (metis `a<b` `~ P b` linear less_le)
   9.231 +qed
   9.232 +
   9.233 +end
   9.234 +
   9.235 +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"
   9.236 +  by (rule cSup_eq) (auto simp: not_le[symmetric] setle_def)
   9.237 +
   9.238 +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"
   9.239 +  by (rule cInf_eq) (auto simp: not_le[symmetric] setge_def)
   9.240 +
   9.241 +lemma cSup_eq_Max: "finite (X::'a::conditional_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup X = Max X"
   9.242 +  using cSup_eq_Sup_fin[of X] Sup_fin_eq_Max[of X] by simp
   9.243 +
   9.244 +lemma cInf_eq_Min: "finite (X::'a::conditional_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Min X"
   9.245 +  using cInf_eq_Inf_fin[of X] Inf_fin_eq_Min[of X] by simp
   9.246 +
   9.247 +lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditional_complete_linorder, dense_linorder}} = x"
   9.248 +  by (auto intro!: cSup_eq_non_empty intro: dense_le)
   9.249 +
   9.250 +lemma cSup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x::'a::{conditional_complete_linorder, dense_linorder}} = x"
   9.251 +  by (auto intro!: cSup_eq intro: dense_le_bounded)
   9.252 +
   9.253 +lemma cSup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x::'a::{conditional_complete_linorder, dense_linorder}} = x"
   9.254 +  by (auto intro!: cSup_eq intro: dense_le_bounded)
   9.255 +
   9.256 +lemma cInf_greaterThan[simp]: "Inf {x::'a::{conditional_complete_linorder, dense_linorder} <..} = x"
   9.257 +  by (auto intro!: cInf_eq intro: dense_ge)
   9.258 +
   9.259 +lemma cInf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x::'a::{conditional_complete_linorder, dense_linorder}} = y"
   9.260 +  by (auto intro!: cInf_eq intro: dense_ge_bounded)
   9.261 +
   9.262 +lemma cInf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x::'a::{conditional_complete_linorder, dense_linorder}} = y"
   9.263 +  by (auto intro!: cInf_eq intro: dense_ge_bounded)
   9.264 +
   9.265 +instantiation real :: conditional_complete_linorder
   9.266 +begin
   9.267 +
   9.268 +subsection{*Supremum of a set of reals*}
   9.269 +
   9.270  definition
   9.271 -  Inf_real_def: "Inf (X::real set) == - (Sup (uminus ` X))"
   9.272 +  Sup_real_def: "Sup X \<equiv> LEAST z::real. \<forall>x\<in>X. x\<le>z"
   9.273 +
   9.274 +definition
   9.275 +  Inf_real_def: "Inf (X::real set) \<equiv> - Sup (uminus ` X)"
   9.276 +
   9.277 +instance
   9.278 +proof
   9.279 +  { fix z x :: real and X :: "real set"
   9.280 +    assume x: "x \<in> X" and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
   9.281 +    show "x \<le> Sup X"
   9.282 +    proof (auto simp add: Sup_real_def) 
   9.283 +      from complete_real[of X]
   9.284 +      obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
   9.285 +        by (blast intro: x z)
   9.286 +      hence "x \<le> s"
   9.287 +        by (blast intro: x z)
   9.288 +      also with s have "... = (LEAST z. \<forall>x\<in>X. x \<le> z)"
   9.289 +        by (fast intro: Least_equality [symmetric])  
   9.290 +      finally show "x \<le> (LEAST z. \<forall>x\<in>X. x \<le> z)" .
   9.291 +    qed }
   9.292 +  note Sup_upper = this
   9.293  
   9.294 -instance ..
   9.295 +  { fix z :: real and X :: "real set"
   9.296 +    assume x: "X \<noteq> {}"
   9.297 +        and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
   9.298 +    show "Sup X \<le> z"
   9.299 +    proof (auto simp add: Sup_real_def) 
   9.300 +      from complete_real x
   9.301 +      obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
   9.302 +        by (blast intro: z)
   9.303 +      hence "(LEAST z. \<forall>x\<in>X. x \<le> z) = s"
   9.304 +        by (best intro: Least_equality)  
   9.305 +      also with s z have "... \<le> z"
   9.306 +        by blast
   9.307 +      finally show "(LEAST z. \<forall>x\<in>X. x \<le> z) \<le> z" .
   9.308 +    qed }
   9.309 +  note Sup_least = this
   9.310 +
   9.311 +  { fix x z :: real and X :: "real set"
   9.312 +    assume x: "x \<in> X" and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
   9.313 +    show "Inf X \<le> x"
   9.314 +    proof -
   9.315 +      have "-x \<le> Sup (uminus ` X)"
   9.316 +        by (rule Sup_upper[of _ _ "- z"]) (auto simp add: image_iff x z)
   9.317 +      thus ?thesis 
   9.318 +        by (auto simp add: Inf_real_def)
   9.319 +    qed }
   9.320 +
   9.321 +  { fix z :: real and X :: "real set"
   9.322 +    assume x: "X \<noteq> {}"
   9.323 +      and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
   9.324 +    show "z \<le> Inf X"
   9.325 +    proof -
   9.326 +      have "Sup (uminus ` X) \<le> -z"
   9.327 +        using x z by (force intro: Sup_least)
   9.328 +      hence "z \<le> - Sup (uminus ` X)"
   9.329 +        by simp
   9.330 +      thus ?thesis 
   9.331 +        by (auto simp add: Inf_real_def)
   9.332 +    qed }
   9.333 +qed
   9.334  end
   9.335  
   9.336  subsection{*Supremum of a set of reals*}
   9.337  
   9.338 -lemma Sup_upper [intro]: (*REAL_SUP_UBOUND in HOL4*)
   9.339 -  fixes x :: real
   9.340 -  assumes x: "x \<in> X"
   9.341 -      and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
   9.342 -  shows "x \<le> Sup X"
   9.343 -proof (auto simp add: Sup_real_def) 
   9.344 -  from complete_real
   9.345 -  obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
   9.346 -    by (blast intro: x z)
   9.347 -  hence "x \<le> s"
   9.348 -    by (blast intro: x z)
   9.349 -  also with s have "... = (LEAST z. \<forall>x\<in>X. x \<le> z)"
   9.350 -    by (fast intro: Least_equality [symmetric])  
   9.351 -  finally show "x \<le> (LEAST z. \<forall>x\<in>X. x \<le> z)" .
   9.352 -qed
   9.353 -
   9.354 -lemma Sup_least [intro]: (*REAL_IMP_SUP_LE in HOL4*)
   9.355 -  fixes z :: real
   9.356 -  assumes x: "X \<noteq> {}"
   9.357 -      and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
   9.358 -  shows "Sup X \<le> z"
   9.359 -proof (auto simp add: Sup_real_def) 
   9.360 -  from complete_real x
   9.361 -  obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
   9.362 -    by (blast intro: z)
   9.363 -  hence "(LEAST z. \<forall>x\<in>X. x \<le> z) = s"
   9.364 -    by (best intro: Least_equality)  
   9.365 -  also with s z have "... \<le> z"
   9.366 -    by blast
   9.367 -  finally show "(LEAST z. \<forall>x\<in>X. x \<le> z) \<le> z" .
   9.368 -qed
   9.369 -
   9.370 -lemma less_SupE:
   9.371 -  fixes y :: real
   9.372 -  assumes "y < Sup X" "X \<noteq> {}"
   9.373 -  obtains x where "x\<in>X" "y < x"
   9.374 -by (metis SupInf.Sup_least assms linorder_not_less that)
   9.375 -
   9.376 -lemma Sup_singleton [simp]: "Sup {x::real} = x"
   9.377 -  by (force intro: Least_equality simp add: Sup_real_def)
   9.378 - 
   9.379 -lemma Sup_eq_maximum: (*REAL_SUP_MAX in HOL4*)
   9.380 -  fixes z :: real
   9.381 -  assumes X: "z \<in> X" and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
   9.382 -  shows  "Sup X = z"
   9.383 -  by (force intro: Least_equality X z simp add: Sup_real_def)
   9.384 - 
   9.385 -lemma Sup_upper2: (*REAL_IMP_LE_SUP in HOL4*)
   9.386 -  fixes x :: real
   9.387 -  shows "x \<in> X \<Longrightarrow> y \<le> x \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y \<le> Sup X"
   9.388 -  by (metis Sup_upper order_trans)
   9.389 -
   9.390 -lemma Sup_real_iff : (*REAL_SUP_LE in HOL4*)
   9.391 -  fixes z :: real
   9.392 -  shows "X ~= {} ==> (!!x. x \<in> X ==> x \<le> z) ==> (\<exists>x\<in>X. y<x) <-> y < Sup X"
   9.393 -  by (rule iffI, metis less_le_trans Sup_upper, metis Sup_least not_less)
   9.394 -
   9.395 -lemma Sup_eq:
   9.396 -  fixes a :: real
   9.397 -  shows "(!!x. x \<in> X \<Longrightarrow> x \<le> a) 
   9.398 -        \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y) \<Longrightarrow> Sup X = a"
   9.399 -  by (metis Sup_least Sup_upper add_le_cancel_left diff_add_cancel insert_absorb
   9.400 -        insert_not_empty order_antisym)
   9.401 -
   9.402 -lemma Sup_le:
   9.403 -  fixes S :: "real set"
   9.404 -  shows "S \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b"
   9.405 -by (metis SupInf.Sup_least setle_def)
   9.406 -
   9.407 -lemma Sup_upper_EX: 
   9.408 -  fixes x :: real
   9.409 -  shows "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> x \<le> z \<Longrightarrow>  x \<le> Sup X"
   9.410 -  by blast
   9.411 -
   9.412 -lemma Sup_insert_nonempty: 
   9.413 -  fixes x :: real
   9.414 -  assumes x: "x \<in> X"
   9.415 -      and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
   9.416 -  shows "Sup (insert a X) = max a (Sup X)"
   9.417 -proof (cases "Sup X \<le> a")
   9.418 -  case True
   9.419 -  thus ?thesis
   9.420 -    apply (simp add: max_def)
   9.421 -    apply (rule Sup_eq_maximum)
   9.422 -    apply (rule insertI1)
   9.423 -    apply (metis Sup_upper [OF _ z] insertE linear order_trans)
   9.424 -    done
   9.425 -next
   9.426 -  case False
   9.427 -  hence 1:"a < Sup X" by simp
   9.428 -  have "Sup X \<le> Sup (insert a X)"
   9.429 -    apply (rule Sup_least)
   9.430 -    apply (metis ex_in_conv x)
   9.431 -    apply (rule Sup_upper_EX) 
   9.432 -    apply blast
   9.433 -    apply (metis insert_iff linear order_trans z)
   9.434 -    done
   9.435 -  moreover 
   9.436 -  have "Sup (insert a X) \<le> Sup X"
   9.437 -    apply (rule Sup_least)
   9.438 -    apply blast
   9.439 -    apply (metis False Sup_upper insertE linear z)
   9.440 -    done
   9.441 -  ultimately have "Sup (insert a X) = Sup X"
   9.442 -    by (blast intro:  antisym )
   9.443 -  thus ?thesis
   9.444 -    by (metis 1 min_max.le_iff_sup less_le)
   9.445 -qed
   9.446 -
   9.447 -lemma Sup_insert_if: 
   9.448 -  fixes X :: "real set"
   9.449 -  assumes z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
   9.450 -  shows "Sup (insert a X) = (if X={} then a else max a (Sup X))"
   9.451 -by auto (metis Sup_insert_nonempty z) 
   9.452 -
   9.453 -lemma Sup: 
   9.454 -  fixes S :: "real set"
   9.455 -  shows "S \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> isLub UNIV S (Sup S)"
   9.456 -by  (auto simp add: isLub_def setle_def leastP_def isUb_def intro!: setgeI) 
   9.457 -
   9.458 -lemma Sup_finite_Max: 
   9.459 -  fixes S :: "real set"
   9.460 -  assumes fS: "finite S" and Se: "S \<noteq> {}"
   9.461 -  shows "Sup S = Max S"
   9.462 -using fS Se
   9.463 -proof-
   9.464 -  let ?m = "Max S"
   9.465 -  from Max_ge[OF fS] have Sm: "\<forall> x\<in> S. x \<le> ?m" by metis
   9.466 -  with Sup[OF Se] have lub: "isLub UNIV S (Sup S)" by (metis setle_def)
   9.467 -  from Max_in[OF fS Se] lub have mrS: "?m \<le> Sup S"
   9.468 -    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
   9.469 -  moreover
   9.470 -  have "Sup S \<le> ?m" using Sm lub
   9.471 -    by (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)
   9.472 -  ultimately  show ?thesis by arith
   9.473 -qed
   9.474 -
   9.475 -lemma Sup_finite_in:
   9.476 -  fixes S :: "real set"
   9.477 -  assumes fS: "finite S" and Se: "S \<noteq> {}"
   9.478 -  shows "Sup S \<in> S"
   9.479 -  using Sup_finite_Max[OF fS Se] Max_in[OF fS Se] by metis
   9.480 -
   9.481 -lemma Sup_finite_ge_iff: 
   9.482 -  fixes S :: "real set"
   9.483 -  assumes fS: "finite S" and Se: "S \<noteq> {}"
   9.484 -  shows "a \<le> Sup S \<longleftrightarrow> (\<exists> x \<in> S. a \<le> x)"
   9.485 -by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS linorder_not_le less_le_trans)
   9.486 -
   9.487 -lemma Sup_finite_le_iff: 
   9.488 -  fixes S :: "real set"
   9.489 -  assumes fS: "finite S" and Se: "S \<noteq> {}"
   9.490 -  shows "a \<ge> Sup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> x)"
   9.491 -by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS order_trans)
   9.492 -
   9.493 -lemma Sup_finite_gt_iff: 
   9.494 -  fixes S :: "real set"
   9.495 -  assumes fS: "finite S" and Se: "S \<noteq> {}"
   9.496 -  shows "a < Sup S \<longleftrightarrow> (\<exists> x \<in> S. a < x)"
   9.497 -by (metis Se Sup_finite_le_iff fS linorder_not_less)
   9.498 -
   9.499 -lemma Sup_finite_lt_iff: 
   9.500 -  fixes S :: "real set"
   9.501 -  assumes fS: "finite S" and Se: "S \<noteq> {}"
   9.502 -  shows "a > Sup S \<longleftrightarrow> (\<forall> x \<in> S. a > x)"
   9.503 -by (metis Se Sup_finite_ge_iff fS linorder_not_less)
   9.504 -
   9.505 -lemma Sup_unique:
   9.506 -  fixes S :: "real set"
   9.507 -  shows "S *<= b \<Longrightarrow> (\<forall>b' < b. \<exists>x \<in> S. b' < x) \<Longrightarrow> Sup S = b"
   9.508 -unfolding setle_def
   9.509 -apply (rule Sup_eq, auto) 
   9.510 -apply (metis linorder_not_less) 
   9.511 -done
   9.512 -
   9.513 -lemma Sup_abs_le:
   9.514 +lemma cSup_abs_le:
   9.515    fixes S :: "real set"
   9.516    shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a"
   9.517 -by (auto simp add: abs_le_interval_iff) (metis Sup_upper2) 
   9.518 +by (auto simp add: abs_le_interval_iff intro: cSup_least) (metis cSup_upper2) 
   9.519  
   9.520 -lemma Sup_bounds:
   9.521 +lemma cSup_bounds:
   9.522    fixes S :: "real set"
   9.523    assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
   9.524    shows "a \<le> Sup S \<and> Sup S \<le> b"
   9.525  proof-
   9.526 -  from Sup[OF Se] u have lub: "isLub UNIV S (Sup S)" by blast
   9.527 +  from isLub_cSup[OF Se] u have lub: "isLub UNIV S (Sup S)" by blast
   9.528    hence b: "Sup S \<le> b" using u 
   9.529      by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) 
   9.530    from Se obtain y where y: "y \<in> S" by blast
   9.531 @@ -219,203 +350,66 @@
   9.532    with b show ?thesis by blast
   9.533  qed
   9.534  
   9.535 -lemma Sup_asclose: 
   9.536 +lemma cSup_asclose: 
   9.537    fixes S :: "real set"
   9.538    assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Sup S - l\<bar> \<le> e"
   9.539  proof-
   9.540    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
   9.541 -  thus ?thesis using S b Sup_bounds[of S "l - e" "l+e"] unfolding th
   9.542 +  thus ?thesis using S b cSup_bounds[of S "l - e" "l+e"] unfolding th
   9.543      by  (auto simp add: setge_def setle_def)
   9.544  qed
   9.545  
   9.546 -lemma Sup_lessThan[simp]: "Sup {..<x} = (x::real)"
   9.547 -  by (auto intro!: Sup_eq intro: dense_le)
   9.548 -
   9.549 -lemma Sup_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Sup {y<..<x} = (x::real)"
   9.550 -  by (auto intro!: Sup_eq intro: dense_le_bounded)
   9.551 -
   9.552 -lemma Sup_atLeastLessThan[simp]: "y < x \<Longrightarrow> Sup {y..<x} = (x::real)"
   9.553 -  by (auto intro!: Sup_eq intro: dense_le_bounded)
   9.554 -
   9.555 -lemma Sup_atMost[simp]: "Sup {..x} = (x::real)"
   9.556 -  by (auto intro!: Sup_eq_maximum)
   9.557 -
   9.558 -lemma Sup_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Sup {y<..x} = (x::real)"
   9.559 -  by (auto intro!: Sup_eq_maximum)
   9.560 -
   9.561 -lemma Sup_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Sup {y..x} = (x::real)"
   9.562 -  by (auto intro!: Sup_eq_maximum)
   9.563 -
   9.564 -
   9.565  subsection{*Infimum of a set of reals*}
   9.566  
   9.567 -lemma Inf_lower [intro]: 
   9.568 -  fixes z :: real
   9.569 -  assumes x: "x \<in> X"
   9.570 -      and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
   9.571 -  shows "Inf X \<le> x"
   9.572 -proof -
   9.573 -  have "-x \<le> Sup (uminus ` X)"
   9.574 -    by (rule Sup_upper [where z = "-z"]) (auto simp add: image_iff x z)
   9.575 -  thus ?thesis 
   9.576 -    by (auto simp add: Inf_real_def)
   9.577 -qed
   9.578 -
   9.579 -lemma Inf_greatest [intro]: 
   9.580 +lemma cInf_greater:
   9.581    fixes z :: real
   9.582 -  assumes x: "X \<noteq> {}"
   9.583 -      and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
   9.584 -  shows "z \<le> Inf X"
   9.585 -proof -
   9.586 -  have "Sup (uminus ` X) \<le> -z" using x z by force
   9.587 -  hence "z \<le> - Sup (uminus ` X)"
   9.588 -    by simp
   9.589 -  thus ?thesis 
   9.590 -    by (auto simp add: Inf_real_def)
   9.591 -qed
   9.592 -
   9.593 -lemma Inf_singleton [simp]: "Inf {x::real} = x"
   9.594 -  by (simp add: Inf_real_def) 
   9.595 - 
   9.596 -lemma Inf_eq_minimum: (*REAL_INF_MIN in HOL4*)
   9.597 -  fixes z :: real
   9.598 -  assumes x: "z \<in> X" and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
   9.599 -  shows  "Inf X = z"
   9.600 -proof -
   9.601 -  have "Sup (uminus ` X) = -z" using x z
   9.602 -    by (force intro: Sup_eq_maximum x z)
   9.603 -  thus ?thesis
   9.604 -    by (simp add: Inf_real_def) 
   9.605 -qed
   9.606 - 
   9.607 -lemma Inf_lower2:
   9.608 -  fixes x :: real
   9.609 -  shows "x \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X \<le> y"
   9.610 -  by (metis Inf_lower order_trans)
   9.611 -
   9.612 -lemma Inf_real_iff:
   9.613 -  fixes z :: real
   9.614 -  shows "X \<noteq> {} \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> (\<exists>x\<in>X. x<y) \<longleftrightarrow> Inf X < y"
   9.615 -  by (metis Inf_greatest Inf_lower less_le_not_le linear
   9.616 -            order_less_le_trans)
   9.617 +  shows "X \<noteq> {} \<Longrightarrow> Inf X < z \<Longrightarrow> \<exists>x\<in>X. x < z"
   9.618 +  by (metis cInf_less_iff not_leE)
   9.619  
   9.620 -lemma Inf_eq:
   9.621 -  fixes a :: real
   9.622 -  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"
   9.623 -  by (metis Inf_greatest Inf_lower add_le_cancel_left diff_add_cancel
   9.624 -        insert_absorb insert_not_empty order_antisym)
   9.625 -
   9.626 -lemma Inf_ge: 
   9.627 -  fixes S :: "real set"
   9.628 -  shows "S \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b"
   9.629 -by (metis SupInf.Inf_greatest setge_def)
   9.630 -
   9.631 -lemma Inf_lower_EX: 
   9.632 -  fixes x :: real
   9.633 -  shows "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> z \<le> x \<Longrightarrow> Inf X \<le> x"
   9.634 -  by blast
   9.635 -
   9.636 -lemma Inf_insert_nonempty: 
   9.637 -  fixes x :: real
   9.638 -  assumes x: "x \<in> X"
   9.639 -      and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
   9.640 -  shows "Inf (insert a X) = min a (Inf X)"
   9.641 -proof (cases "a \<le> Inf X")
   9.642 -  case True
   9.643 -  thus ?thesis
   9.644 -    by (simp add: min_def)
   9.645 -       (blast intro: Inf_eq_minimum order_trans z)
   9.646 -next
   9.647 -  case False
   9.648 -  hence 1:"Inf X < a" by simp
   9.649 -  have "Inf (insert a X) \<le> Inf X"
   9.650 -    apply (rule Inf_greatest)
   9.651 -    apply (metis ex_in_conv x)
   9.652 -    apply (rule Inf_lower_EX)
   9.653 -    apply (erule insertI2)
   9.654 -    apply (metis insert_iff linear order_trans z)
   9.655 -    done
   9.656 -  moreover 
   9.657 -  have "Inf X \<le> Inf (insert a X)"
   9.658 -    apply (rule Inf_greatest)
   9.659 -    apply blast
   9.660 -    apply (metis False Inf_lower insertE linear z) 
   9.661 -    done
   9.662 -  ultimately have "Inf (insert a X) = Inf X"
   9.663 -    by (blast intro:  antisym )
   9.664 -  thus ?thesis
   9.665 -    by (metis False min_max.inf_absorb2 linear)
   9.666 -qed
   9.667 -
   9.668 -lemma Inf_insert_if: 
   9.669 -  fixes X :: "real set"
   9.670 -  assumes z:  "!!x. x \<in> X \<Longrightarrow> z \<le> x"
   9.671 -  shows "Inf (insert a X) = (if X={} then a else min a (Inf X))"
   9.672 -by auto (metis Inf_insert_nonempty z) 
   9.673 -
   9.674 -lemma Inf_greater:
   9.675 -  fixes z :: real
   9.676 -  shows "X \<noteq> {} \<Longrightarrow> Inf X < z \<Longrightarrow> \<exists>x \<in> X. x < z"
   9.677 -  by (metis Inf_real_iff not_leE)
   9.678 -
   9.679 -lemma Inf_close:
   9.680 +lemma cInf_close:
   9.681    fixes e :: real
   9.682    shows "X \<noteq> {} \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>x \<in> X. x < Inf X + e"
   9.683 -  by (metis add_strict_increasing add_commute Inf_greater linorder_not_le pos_add_strict)
   9.684 +  by (metis add_strict_increasing add_commute cInf_greater linorder_not_le pos_add_strict)
   9.685  
   9.686 -lemma Inf_finite_Min:
   9.687 -  fixes S :: "real set"
   9.688 -  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> Inf S = Min S"
   9.689 -by (simp add: Inf_real_def Sup_finite_Max image_image) 
   9.690 -
   9.691 -lemma Inf_finite_in: 
   9.692 +lemma cInf_finite_in: 
   9.693    fixes S :: "real set"
   9.694    assumes fS: "finite S" and Se: "S \<noteq> {}"
   9.695    shows "Inf S \<in> S"
   9.696 -  using Inf_finite_Min[OF fS Se] Min_in[OF fS Se] by metis
   9.697 +  using cInf_eq_Min[OF fS Se] Min_in[OF fS Se] by metis
   9.698  
   9.699 -lemma Inf_finite_ge_iff: 
   9.700 +lemma cInf_finite_ge_iff: 
   9.701    fixes S :: "real set"
   9.702    shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall> x \<in> S. a \<le> x)"
   9.703 -by (metis Inf_finite_Min Inf_finite_in Min_le order_trans)
   9.704 +by (metis cInf_eq_Min cInf_finite_in Min_le order_trans)
   9.705  
   9.706 -lemma Inf_finite_le_iff:
   9.707 +lemma cInf_finite_le_iff:
   9.708    fixes S :: "real set"
   9.709    shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists> x \<in> S. a \<ge> x)"
   9.710 -by (metis Inf_finite_Min Inf_finite_ge_iff Inf_finite_in Min_le
   9.711 -          order_antisym linear)
   9.712 +by (metis cInf_eq_Min cInf_finite_ge_iff cInf_finite_in Min_le order_antisym linear)
   9.713  
   9.714 -lemma Inf_finite_gt_iff: 
   9.715 +lemma cInf_finite_gt_iff: 
   9.716    fixes S :: "real set"
   9.717    shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a < Inf S \<longleftrightarrow> (\<forall> x \<in> S. a < x)"
   9.718 -by (metis Inf_finite_le_iff linorder_not_less)
   9.719 +by (metis cInf_finite_le_iff linorder_not_less)
   9.720  
   9.721 -lemma Inf_finite_lt_iff: 
   9.722 +lemma cInf_finite_lt_iff: 
   9.723    fixes S :: "real set"
   9.724    shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a > Inf S \<longleftrightarrow> (\<exists> x \<in> S. a > x)"
   9.725 -by (metis Inf_finite_ge_iff linorder_not_less)
   9.726 +by (metis cInf_finite_ge_iff linorder_not_less)
   9.727  
   9.728 -lemma Inf_unique:
   9.729 -  fixes S :: "real set"
   9.730 -  shows "b <=* S \<Longrightarrow> (\<forall>b' > b. \<exists>x \<in> S. b' > x) \<Longrightarrow> Inf S = b"
   9.731 -unfolding setge_def
   9.732 -apply (rule Inf_eq, auto) 
   9.733 -apply (metis less_le_not_le linorder_not_less) 
   9.734 -done
   9.735 -
   9.736 -lemma Inf_abs_ge:
   9.737 +lemma cInf_abs_ge:
   9.738    fixes S :: "real set"
   9.739    shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Inf S\<bar> \<le> a"
   9.740 -by (simp add: Inf_real_def) (rule Sup_abs_le, auto) 
   9.741 +by (simp add: Inf_real_def) (rule cSup_abs_le, auto) 
   9.742  
   9.743 -lemma Inf_asclose:
   9.744 +lemma cInf_asclose:
   9.745    fixes S :: "real set"
   9.746    assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Inf S - l\<bar> \<le> e"
   9.747  proof -
   9.748    have "\<bar>- Sup (uminus ` S) - l\<bar> =  \<bar>Sup (uminus ` S) - (-l)\<bar>"
   9.749      by auto
   9.750    also have "... \<le> e" 
   9.751 -    apply (rule Sup_asclose) 
   9.752 +    apply (rule cSup_asclose) 
   9.753      apply (auto simp add: S)
   9.754      apply (metis abs_minus_add_cancel b add_commute diff_minus)
   9.755      done
   9.756 @@ -424,73 +418,16 @@
   9.757      by (simp add: Inf_real_def)
   9.758  qed
   9.759  
   9.760 -lemma Inf_greaterThanLessThan[simp]: "y < x \<Longrightarrow> Inf {y<..<x} = (y::real)"
   9.761 -  by (simp add: Inf_real_def)
   9.762 -
   9.763 -lemma Inf_atLeastLessThan[simp]: "y < x \<Longrightarrow> Inf {y..<x} = (y::real)"
   9.764 -  by (simp add: Inf_real_def)
   9.765 -
   9.766 -lemma Inf_atLeast[simp]: "Inf {x..} = (x::real)"
   9.767 -  by (simp add: Inf_real_def)
   9.768 -
   9.769 -lemma Inf_greaterThanAtMost[simp]: "y < x \<Longrightarrow> Inf {y<..x} = (y::real)"
   9.770 -  by (simp add: Inf_real_def)
   9.771 -
   9.772 -lemma Inf_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Inf {y..x} = (y::real)"
   9.773 -  by (simp add: Inf_real_def)
   9.774 -
   9.775  subsection{*Relate max and min to Sup and Inf.*}
   9.776  
   9.777 -lemma real_max_Sup:
   9.778 +lemma real_max_cSup:
   9.779    fixes x :: real
   9.780    shows "max x y = Sup {x,y}"
   9.781 -proof-
   9.782 -  have "Sup {x,y} \<le> max x y" by (simp add: Sup_finite_le_iff)
   9.783 -  moreover
   9.784 -  have "max x y \<le> Sup {x,y}" by (simp add: linorder_linear Sup_finite_ge_iff)
   9.785 -  ultimately show ?thesis by arith
   9.786 -qed
   9.787 +  by (subst cSup_insert[of _ y]) (simp_all add: sup_max)
   9.788  
   9.789 -lemma real_min_Inf: 
   9.790 +lemma real_min_cInf: 
   9.791    fixes x :: real
   9.792    shows "min x y = Inf {x,y}"
   9.793 -proof-
   9.794 -  have "Inf {x,y} \<le> min x y" by (simp add: linorder_linear Inf_finite_le_iff)
   9.795 -  moreover
   9.796 -  have "min x y \<le> Inf {x,y}" by (simp add:  Inf_finite_ge_iff)
   9.797 -  ultimately show ?thesis by arith
   9.798 -qed
   9.799 -
   9.800 -lemma reals_complete_interval:
   9.801 -  fixes a::real and b::real
   9.802 -  assumes "a < b" and "P a" and "~P b"
   9.803 -  shows "\<exists>c. a \<le> c & c \<le> b & (\<forall>x. a \<le> x & x < c --> P x) &
   9.804 -             (\<forall>d. (\<forall>x. a \<le> x & x < d --> P x) --> d \<le> c)"
   9.805 -proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x & x < d --> P x}"], auto)
   9.806 -  show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
   9.807 -    by (rule SupInf.Sup_upper [where z=b], auto)
   9.808 -       (metis `a < b` `\<not> P b` linear less_le)
   9.809 -next
   9.810 -  show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b"
   9.811 -    apply (rule SupInf.Sup_least) 
   9.812 -    apply (auto simp add: )
   9.813 -    apply (metis less_le_not_le)
   9.814 -    apply (metis `a<b` `~ P b` linear less_le)
   9.815 -    done
   9.816 -next
   9.817 -  fix x
   9.818 -  assume x: "a \<le> x" and lt: "x < Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
   9.819 -  show "P x"
   9.820 -    apply (rule less_SupE [OF lt], auto)
   9.821 -    apply (metis less_le_not_le)
   9.822 -    apply (metis x) 
   9.823 -    done
   9.824 -next
   9.825 -  fix d
   9.826 -    assume 0: "\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x"
   9.827 -    thus "d \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
   9.828 -      by (rule_tac z="b" in SupInf.Sup_upper, auto) 
   9.829 -         (metis `a<b` `~ P b` linear less_le)
   9.830 -qed
   9.831 +  by (subst cInf_insert[of _ y]) (simp_all add: inf_min)
   9.832  
   9.833  end