src/HOL/Library/Euclidean_Space.thy
changeset 33269 3b7e2dbbd684
parent 32960 69916a850301
     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Fri Oct 23 14:33:07 2009 +0200
     1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Tue Oct 27 12:59:57 2009 +0000
     1.3 @@ -2297,242 +2297,9 @@
     1.4    ultimately show ?thesis by metis
     1.5  qed
     1.6  
     1.7 -(* Supremum and infimum of real sets *)
     1.8 -
     1.9 -
    1.10 -definition rsup:: "real set \<Rightarrow> real" where
    1.11 -  "rsup S = (SOME a. isLub UNIV S a)"
    1.12 -
    1.13 -lemma rsup_alt: "rsup S = (SOME a. (\<forall>x \<in> S. x \<le> a) \<and> (\<forall>b. (\<forall>x \<in> S. x \<le> b) \<longrightarrow> a \<le> b))"  by (auto simp  add: isLub_def rsup_def leastP_def isUb_def setle_def setge_def)
    1.14 -
    1.15 -lemma rsup: assumes Se: "S \<noteq> {}" and b: "\<exists>b. S *<= b"
    1.16 -  shows "isLub UNIV S (rsup S)"
    1.17 -using Se b
    1.18 -unfolding rsup_def
    1.19 -apply clarify
    1.20 -apply (rule someI_ex)
    1.21 -apply (rule reals_complete)
    1.22 -by (auto simp add: isUb_def setle_def)
    1.23 -
    1.24 -lemma rsup_le: assumes Se: "S \<noteq> {}" and Sb: "S *<= b" shows "rsup S \<le> b"
    1.25 -proof-
    1.26 -  from Sb have bu: "isUb UNIV S b" by (simp add: isUb_def setle_def)
    1.27 -  from rsup[OF Se] Sb have "isLub UNIV S (rsup S)"  by blast
    1.28 -  then show ?thesis using bu by (auto simp add: isLub_def leastP_def setle_def setge_def)
    1.29 -qed
    1.30 -
    1.31 -lemma rsup_finite_Max: assumes fS: "finite S" and Se: "S \<noteq> {}"
    1.32 -  shows "rsup S = Max S"
    1.33 -using fS Se
    1.34 -proof-
    1.35 -  let ?m = "Max S"
    1.36 -  from Max_ge[OF fS] have Sm: "\<forall> x\<in> S. x \<le> ?m" by metis
    1.37 -  with rsup[OF Se] have lub: "isLub UNIV S (rsup S)" by (metis setle_def)
    1.38 -  from Max_in[OF fS Se] lub have mrS: "?m \<le> rsup S"
    1.39 -    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
    1.40 -  moreover
    1.41 -  have "rsup S \<le> ?m" using Sm lub
    1.42 -    by (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)
    1.43 -  ultimately  show ?thesis by arith
    1.44 -qed
    1.45 -
    1.46 -lemma rsup_finite_in: assumes fS: "finite S" and Se: "S \<noteq> {}"
    1.47 -  shows "rsup S \<in> S"
    1.48 -  using rsup_finite_Max[OF fS Se] Max_in[OF fS Se] by metis
    1.49 -
    1.50 -lemma rsup_finite_Ub: assumes fS: "finite S" and Se: "S \<noteq> {}"
    1.51 -  shows "isUb S S (rsup S)"
    1.52 -  using rsup_finite_Max[OF fS Se] rsup_finite_in[OF fS Se] Max_ge[OF fS]
    1.53 -  unfolding isUb_def setle_def by metis
    1.54 -
    1.55 -lemma rsup_finite_ge_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
    1.56 -  shows "a \<le> rsup S \<longleftrightarrow> (\<exists> x \<in> S. a \<le> x)"
    1.57 -using rsup_finite_Ub[OF fS Se] by (auto simp add: isUb_def setle_def)
    1.58 -
    1.59 -lemma rsup_finite_le_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
    1.60 -  shows "a \<ge> rsup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> x)"
    1.61 -using rsup_finite_Ub[OF fS Se] by (auto simp add: isUb_def setle_def)
    1.62 -
    1.63 -lemma rsup_finite_gt_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
    1.64 -  shows "a < rsup S \<longleftrightarrow> (\<exists> x \<in> S. a < x)"
    1.65 -using rsup_finite_Ub[OF fS Se] by (auto simp add: isUb_def setle_def)
    1.66 -
    1.67 -lemma rsup_finite_lt_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
    1.68 -  shows "a > rsup S \<longleftrightarrow> (\<forall> x \<in> S. a > x)"
    1.69 -using rsup_finite_Ub[OF fS Se] by (auto simp add: isUb_def setle_def)
    1.70 -
    1.71 -lemma rsup_unique: assumes b: "S *<= b" and S: "\<forall>b' < b. \<exists>x \<in> S. b' < x"
    1.72 -  shows "rsup S = b"
    1.73 -using b S
    1.74 -unfolding setle_def rsup_alt
    1.75 -apply -
    1.76 -apply (rule some_equality)
    1.77 -apply (metis  linorder_not_le order_eq_iff[symmetric])+
    1.78 -done
    1.79 -
    1.80 -lemma rsup_le_subset: "S\<noteq>{} \<Longrightarrow> S \<subseteq> T \<Longrightarrow> (\<exists>b. T *<= b) \<Longrightarrow> rsup S \<le> rsup T"
    1.81 -  apply (rule rsup_le)
    1.82 -  apply simp
    1.83 -  using rsup[of T] by (auto simp add: isLub_def leastP_def setge_def setle_def isUb_def)
    1.84 -
    1.85 -lemma isUb_def': "isUb R S = (\<lambda>x. S *<= x \<and> x \<in> R)"
    1.86 -  apply (rule ext)
    1.87 -  by (metis isUb_def)
    1.88 -
    1.89 -lemma UNIV_trivial: "UNIV x" using UNIV_I[of x] by (metis mem_def)
    1.90 -lemma rsup_bounds: assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
    1.91 -  shows "a \<le> rsup S \<and> rsup S \<le> b"
    1.92 -proof-
    1.93 -  from rsup[OF Se] u have lub: "isLub UNIV S (rsup S)" by blast
    1.94 -  hence b: "rsup S \<le> b" using u by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def')
    1.95 -  from Se obtain y where y: "y \<in> S" by blast
    1.96 -  from lub l have "a \<le> rsup S" apply (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def')
    1.97 -    apply (erule ballE[where x=y])
    1.98 -    apply (erule ballE[where x=y])
    1.99 -    apply arith
   1.100 -    using y apply auto
   1.101 -    done
   1.102 -  with b show ?thesis by blast
   1.103 -qed
   1.104 -
   1.105 -lemma rsup_abs_le: "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>rsup S\<bar> \<le> a"
   1.106 -  unfolding abs_le_interval_iff  using rsup_bounds[of S "-a" a]
   1.107 -  by (auto simp add: setge_def setle_def)
   1.108 -
   1.109 -lemma rsup_asclose: assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>rsup S - l\<bar> \<le> e"
   1.110 -proof-
   1.111 -  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
   1.112 -  show ?thesis using S b rsup_bounds[of S "l - e" "l+e"] unfolding th
   1.113 -    by  (auto simp add: setge_def setle_def)
   1.114 -qed
   1.115 -
   1.116 -definition rinf:: "real set \<Rightarrow> real" where
   1.117 -  "rinf S = (SOME a. isGlb UNIV S a)"
   1.118 -
   1.119 -lemma rinf_alt: "rinf S = (SOME a. (\<forall>x \<in> S. x \<ge> a) \<and> (\<forall>b. (\<forall>x \<in> S. x \<ge> b) \<longrightarrow> a \<ge> b))"  by (auto simp  add: isGlb_def rinf_def greatestP_def isLb_def setle_def setge_def)
   1.120 -
   1.121 -lemma reals_complete_Glb: assumes Se: "\<exists>x. x \<in> S" and lb: "\<exists> y. isLb UNIV S y"
   1.122 -  shows "\<exists>(t::real). isGlb UNIV S t"
   1.123 -proof-
   1.124 -  let ?M = "uminus ` S"
   1.125 -  from lb have th: "\<exists>y. isUb UNIV ?M y" apply (auto simp add: isUb_def isLb_def setle_def setge_def)
   1.126 -    by (rule_tac x="-y" in exI, auto)
   1.127 -  from Se have Me: "\<exists>x. x \<in> ?M" by blast
   1.128 -  from reals_complete[OF Me th] obtain t where t: "isLub UNIV ?M t" by blast
   1.129 -  have "isGlb UNIV S (- t)" using t
   1.130 -    apply (auto simp add: isLub_def isGlb_def leastP_def greatestP_def setle_def setge_def isUb_def isLb_def)
   1.131 -    apply (erule_tac x="-y" in allE)
   1.132 -    apply auto
   1.133 -    done
   1.134 -  then show ?thesis by metis
   1.135 -qed
   1.136 -
   1.137 -lemma rinf: assumes Se: "S \<noteq> {}" and b: "\<exists>b. b <=* S"
   1.138 -  shows "isGlb UNIV S (rinf S)"
   1.139 -using Se b
   1.140 -unfolding rinf_def
   1.141 -apply clarify
   1.142 -apply (rule someI_ex)
   1.143 -apply (rule reals_complete_Glb)
   1.144 -apply (auto simp add: isLb_def setle_def setge_def)
   1.145 -done
   1.146 -
   1.147 -lemma rinf_ge: assumes Se: "S \<noteq> {}" and Sb: "b <=* S" shows "rinf S \<ge> b"
   1.148 -proof-
   1.149 -  from Sb have bu: "isLb UNIV S b" by (simp add: isLb_def setge_def)
   1.150 -  from rinf[OF Se] Sb have "isGlb UNIV S (rinf S)"  by blast
   1.151 -  then show ?thesis using bu by (auto simp add: isGlb_def greatestP_def setle_def setge_def)
   1.152 -qed
   1.153 -
   1.154 -lemma rinf_finite_Min: assumes fS: "finite S" and Se: "S \<noteq> {}"
   1.155 -  shows "rinf S = Min S"
   1.156 -using fS Se
   1.157 -proof-
   1.158 -  let ?m = "Min S"
   1.159 -  from Min_le[OF fS] have Sm: "\<forall> x\<in> S. x \<ge> ?m" by metis
   1.160 -  with rinf[OF Se] have glb: "isGlb UNIV S (rinf S)" by (metis setge_def)
   1.161 -  from Min_in[OF fS Se] glb have mrS: "?m \<ge> rinf S"
   1.162 -    by (auto simp add: isGlb_def greatestP_def setle_def setge_def isLb_def)
   1.163 -  moreover
   1.164 -  have "rinf S \<ge> ?m" using Sm glb
   1.165 -    by (auto simp add: isGlb_def greatestP_def isLb_def setle_def setge_def)
   1.166 -  ultimately  show ?thesis by arith
   1.167 -qed
   1.168 -
   1.169 -lemma rinf_finite_in: assumes fS: "finite S" and Se: "S \<noteq> {}"
   1.170 -  shows "rinf S \<in> S"
   1.171 -  using rinf_finite_Min[OF fS Se] Min_in[OF fS Se] by metis
   1.172 -
   1.173 -lemma rinf_finite_Lb: assumes fS: "finite S" and Se: "S \<noteq> {}"
   1.174 -  shows "isLb S S (rinf S)"
   1.175 -  using rinf_finite_Min[OF fS Se] rinf_finite_in[OF fS Se] Min_le[OF fS]
   1.176 -  unfolding isLb_def setge_def by metis
   1.177 -
   1.178 -lemma rinf_finite_ge_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
   1.179 -  shows "a \<le> rinf S \<longleftrightarrow> (\<forall> x \<in> S. a \<le> x)"
   1.180 -using rinf_finite_Lb[OF fS Se] by (auto simp add: isLb_def setge_def)
   1.181 -
   1.182 -lemma rinf_finite_le_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
   1.183 -  shows "a \<ge> rinf S \<longleftrightarrow> (\<exists> x \<in> S. a \<ge> x)"
   1.184 -using rinf_finite_Lb[OF fS Se] by (auto simp add: isLb_def setge_def)
   1.185 -
   1.186 -lemma rinf_finite_gt_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
   1.187 -  shows "a < rinf S \<longleftrightarrow> (\<forall> x \<in> S. a < x)"
   1.188 -using rinf_finite_Lb[OF fS Se] by (auto simp add: isLb_def setge_def)
   1.189 -
   1.190 -lemma rinf_finite_lt_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
   1.191 -  shows "a > rinf S \<longleftrightarrow> (\<exists> x \<in> S. a > x)"
   1.192 -using rinf_finite_Lb[OF fS Se] by (auto simp add: isLb_def setge_def)
   1.193 -
   1.194 -lemma rinf_unique: assumes b: "b <=* S" and S: "\<forall>b' > b. \<exists>x \<in> S. b' > x"
   1.195 -  shows "rinf S = b"
   1.196 -using b S
   1.197 -unfolding setge_def rinf_alt
   1.198 -apply -
   1.199 -apply (rule some_equality)
   1.200 -apply (metis  linorder_not_le order_eq_iff[symmetric])+
   1.201 -done
   1.202 -
   1.203 -lemma rinf_ge_subset: "S\<noteq>{} \<Longrightarrow> S \<subseteq> T \<Longrightarrow> (\<exists>b. b <=* T) \<Longrightarrow> rinf S >= rinf T"
   1.204 -  apply (rule rinf_ge)
   1.205 -  apply simp
   1.206 -  using rinf[of T] by (auto simp add: isGlb_def greatestP_def setge_def setle_def isLb_def)
   1.207 -
   1.208 -lemma isLb_def': "isLb R S = (\<lambda>x. x <=* S \<and> x \<in> R)"
   1.209 -  apply (rule ext)
   1.210 -  by (metis isLb_def)
   1.211 -
   1.212 -lemma rinf_bounds: assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
   1.213 -  shows "a \<le> rinf S \<and> rinf S \<le> b"
   1.214 -proof-
   1.215 -  from rinf[OF Se] l have lub: "isGlb UNIV S (rinf S)" by blast
   1.216 -  hence b: "a \<le> rinf S" using l by (auto simp add: isGlb_def greatestP_def setle_def setge_def isLb_def')
   1.217 -  from Se obtain y where y: "y \<in> S" by blast
   1.218 -  from lub u have "b \<ge> rinf S" apply (auto simp add: isGlb_def greatestP_def setle_def setge_def isLb_def')
   1.219 -    apply (erule ballE[where x=y])
   1.220 -    apply (erule ballE[where x=y])
   1.221 -    apply arith
   1.222 -    using y apply auto
   1.223 -    done
   1.224 -  with b show ?thesis by blast
   1.225 -qed
   1.226 -
   1.227 -lemma rinf_abs_ge: "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>rinf S\<bar> \<le> a"
   1.228 -  unfolding abs_le_interval_iff  using rinf_bounds[of S "-a" a]
   1.229 -  by (auto simp add: setge_def setle_def)
   1.230 -
   1.231 -lemma rinf_asclose: assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>rinf S - l\<bar> \<le> e"
   1.232 -proof-
   1.233 -  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
   1.234 -  show ?thesis using S b rinf_bounds[of S "l - e" "l+e"] unfolding th
   1.235 -    by  (auto simp add: setge_def setle_def)
   1.236 -qed
   1.237 -
   1.238 -
   1.239 -
   1.240  subsection{* Operator norm. *}
   1.241  
   1.242 -definition "onorm f = rsup {norm (f x)| x. norm x = 1}"
   1.243 +definition "onorm f = Sup {norm (f x)| x. norm x = 1}"
   1.244  
   1.245  lemma norm_bound_generalize:
   1.246    fixes f:: "real ^'n::finite \<Rightarrow> real^'m::finite"
   1.247 @@ -2578,7 +2345,7 @@
   1.248      have Se: "?S \<noteq> {}" using  norm_basis by auto
   1.249      from linear_bounded[OF lf] have b: "\<exists> b. ?S *<= b"
   1.250        unfolding norm_bound_generalize[OF lf, symmetric] by (auto simp add: setle_def)
   1.251 -    {from rsup[OF Se b, unfolded onorm_def[symmetric]]
   1.252 +    {from Sup[OF Se b, unfolded onorm_def[symmetric]]
   1.253        show "norm (f x) <= onorm f * norm x"
   1.254          apply -
   1.255          apply (rule spec[where x = x])
   1.256 @@ -2586,7 +2353,7 @@
   1.257          by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)}
   1.258      {
   1.259        show "\<forall>x. norm (f x) <= b * norm x \<Longrightarrow> onorm f <= b"
   1.260 -        using rsup[OF Se b, unfolded onorm_def[symmetric]]
   1.261 +        using Sup[OF Se b, unfolded onorm_def[symmetric]]
   1.262          unfolding norm_bound_generalize[OF lf, symmetric]
   1.263          by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)}
   1.264    }
   1.265 @@ -2612,7 +2379,7 @@
   1.266      by(auto intro: vector_choose_size set_ext)
   1.267    show ?thesis
   1.268      unfolding onorm_def th
   1.269 -    apply (rule rsup_unique) by (simp_all  add: setle_def)
   1.270 +    apply (rule Sup_unique) by (simp_all  add: setle_def)
   1.271  qed
   1.272  
   1.273  lemma onorm_pos_lt: assumes lf: "linear (f::real ^ 'n::finite \<Rightarrow> real ^'m::finite)"
   1.274 @@ -3055,31 +2822,6 @@
   1.275  qed
   1.276  
   1.277  (* ------------------------------------------------------------------------- *)
   1.278 -(* Relate max and min to sup and inf.                                        *)
   1.279 -(* ------------------------------------------------------------------------- *)
   1.280 -
   1.281 -lemma real_max_rsup: "max x y = rsup {x,y}"
   1.282 -proof-
   1.283 -  have f: "finite {x, y}" "{x,y} \<noteq> {}"  by simp_all
   1.284 -  from rsup_finite_le_iff[OF f, of "max x y"] have "rsup {x,y} \<le> max x y" by simp
   1.285 -  moreover
   1.286 -  have "max x y \<le> rsup {x,y}" using rsup_finite_ge_iff[OF f, of "max x y"]
   1.287 -    by (simp add: linorder_linear)
   1.288 -  ultimately show ?thesis by arith
   1.289 -qed
   1.290 -
   1.291 -lemma real_min_rinf: "min x y = rinf {x,y}"
   1.292 -proof-
   1.293 -  have f: "finite {x, y}" "{x,y} \<noteq> {}"  by simp_all
   1.294 -  from rinf_finite_le_iff[OF f, of "min x y"] have "rinf {x,y} \<le> min x y"
   1.295 -    by (simp add: linorder_linear)
   1.296 -  moreover
   1.297 -  have "min x y \<le> rinf {x,y}" using rinf_finite_ge_iff[OF f, of "min x y"]
   1.298 -    by simp
   1.299 -  ultimately show ?thesis by arith
   1.300 -qed
   1.301 -
   1.302 -(* ------------------------------------------------------------------------- *)
   1.303  (* Geometric progression.                                                    *)
   1.304  (* ------------------------------------------------------------------------- *)
   1.305  
   1.306 @@ -5048,7 +4790,7 @@
   1.307  
   1.308  (* Infinity norm.                                                            *)
   1.309  
   1.310 -definition "infnorm (x::real^'n::finite) = rsup {abs(x$i) |i. i\<in> (UNIV :: 'n set)}"
   1.311 +definition "infnorm (x::real^'n::finite) = Sup {abs(x$i) |i. i\<in> (UNIV :: 'n set)}"
   1.312  
   1.313  lemma numseg_dimindex_nonempty: "\<exists>i. i \<in> (UNIV :: 'n set)"
   1.314    by auto
   1.315 @@ -5065,7 +4807,7 @@
   1.316  
   1.317  lemma infnorm_pos_le: "0 \<le> infnorm (x::real^'n::finite)"
   1.318    unfolding infnorm_def
   1.319 -  unfolding rsup_finite_ge_iff[ OF infnorm_set_lemma]
   1.320 +  unfolding Sup_finite_ge_iff[ OF infnorm_set_lemma]
   1.321    unfolding infnorm_set_image
   1.322    by auto
   1.323  
   1.324 @@ -5076,13 +4818,13 @@
   1.325    have th2: "\<And>x (y::real). abs(x + y) - abs(x) <= abs(y)" by arith
   1.326    show ?thesis
   1.327    unfolding infnorm_def
   1.328 -  unfolding rsup_finite_le_iff[ OF infnorm_set_lemma]
   1.329 +  unfolding Sup_finite_le_iff[ OF infnorm_set_lemma]
   1.330    apply (subst diff_le_eq[symmetric])
   1.331 -  unfolding rsup_finite_ge_iff[ OF infnorm_set_lemma]
   1.332 +  unfolding Sup_finite_ge_iff[ OF infnorm_set_lemma]
   1.333    unfolding infnorm_set_image bex_simps
   1.334    apply (subst th)
   1.335    unfolding th1
   1.336 -  unfolding rsup_finite_ge_iff[ OF infnorm_set_lemma]
   1.337 +  unfolding Sup_finite_ge_iff[ OF infnorm_set_lemma]
   1.338  
   1.339    unfolding infnorm_set_image ball_simps bex_simps
   1.340    apply simp
   1.341 @@ -5094,7 +4836,7 @@
   1.342  proof-
   1.343    have "infnorm x <= 0 \<longleftrightarrow> x = 0"
   1.344      unfolding infnorm_def
   1.345 -    unfolding rsup_finite_le_iff[OF infnorm_set_lemma]
   1.346 +    unfolding Sup_finite_le_iff[OF infnorm_set_lemma]
   1.347      unfolding infnorm_set_image ball_simps
   1.348      by vector
   1.349    then show ?thesis using infnorm_pos_le[of x] by simp
   1.350 @@ -5105,7 +4847,7 @@
   1.351  
   1.352  lemma infnorm_neg: "infnorm (- x) = infnorm x"
   1.353    unfolding infnorm_def
   1.354 -  apply (rule cong[of "rsup" "rsup"])
   1.355 +  apply (rule cong[of "Sup" "Sup"])
   1.356    apply blast
   1.357    apply (rule set_ext)
   1.358    apply auto
   1.359 @@ -5140,14 +4882,15 @@
   1.360      apply (rule finite_imageI) unfolding Collect_def mem_def by simp
   1.361    have S0: "?S \<noteq> {}" by blast
   1.362    have th1: "\<And>S f. f ` S = { f i| i. i \<in> S}" by blast
   1.363 -  from rsup_finite_in[OF fS S0] rsup_finite_Ub[OF fS S0]
   1.364 -  show ?thesis unfolding infnorm_def isUb_def setle_def
   1.365 -    unfolding infnorm_set_image ball_simps by auto
   1.366 +  from Sup_finite_in[OF fS S0] 
   1.367 +  show ?thesis unfolding infnorm_def infnorm_set_image 
   1.368 +    by (metis Sup_finite_ge_iff finite finite_imageI UNIV_not_empty image_is_empty 
   1.369 +              rangeI real_le_refl)
   1.370  qed
   1.371  
   1.372  lemma infnorm_mul_lemma: "infnorm(a *s x) <= \<bar>a\<bar> * infnorm x"
   1.373    apply (subst infnorm_def)
   1.374 -  unfolding rsup_finite_le_iff[OF infnorm_set_lemma]
   1.375 +  unfolding Sup_finite_le_iff[OF infnorm_set_lemma]
   1.376    unfolding infnorm_set_image ball_simps
   1.377    apply (simp add: abs_mult)
   1.378    apply (rule allI)
   1.379 @@ -5180,7 +4923,7 @@
   1.380  (* Prove that it differs only up to a bound from Euclidean norm.             *)
   1.381  
   1.382  lemma infnorm_le_norm: "infnorm x \<le> norm x"
   1.383 -  unfolding infnorm_def rsup_finite_le_iff[OF infnorm_set_lemma]
   1.384 +  unfolding infnorm_def Sup_finite_le_iff[OF infnorm_set_lemma]
   1.385    unfolding infnorm_set_image  ball_simps
   1.386    by (metis component_le_norm)
   1.387  lemma card_enum: "card {1 .. n} = n" by auto
   1.388 @@ -5200,7 +4943,7 @@
   1.389      apply (rule setsum_bounded)
   1.390      apply (rule power_mono)
   1.391      unfolding abs_of_nonneg[OF infnorm_pos_le]
   1.392 -    unfolding infnorm_def  rsup_finite_ge_iff[OF infnorm_set_lemma]
   1.393 +    unfolding infnorm_def  Sup_finite_ge_iff[OF infnorm_set_lemma]
   1.394      unfolding infnorm_set_image bex_simps
   1.395      apply blast
   1.396      by (rule abs_ge_zero)