author hoelzl Fri Mar 22 10:41:43 2013 +0100 (2013-03-22) changeset 51475 ebf9d4fd00ba parent 51474 1e9e68247ad1 child 51476 0c0efde246d1
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
```     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.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.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.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.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.755      done
9.756 @@ -424,73 +418,16 @@
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
```