author huffman Sat Feb 21 10:58:25 2009 -0800 (2009-02-21) changeset 30040 e2cd1acda1ab parent 30039 7208c88df507 child 30041 9becd197a40e
real_normed_vector instance
```     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Sat Feb 21 09:55:32 2009 -0800
1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Sat Feb 21 10:58:25 2009 -0800
1.3 @@ -344,6 +344,209 @@
1.4    apply (auto simp add: vec_def Cart_eq vec_component Cart_lambda_beta )
1.5    using dimindex_ge_1 apply auto done
1.6
1.7 +subsection {* Square root of sum of squares *}
1.8 +
1.9 +definition
1.10 +  "setL2 f A = sqrt (\<Sum>i\<in>A. (f i)\<twosuperior>)"
1.11 +
1.12 +lemma setL2_cong:
1.13 +  "\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B"
1.14 +  unfolding setL2_def by simp
1.15 +
1.16 +lemma strong_setL2_cong:
1.17 +  "\<lbrakk>A = B; \<And>x. x \<in> B =simp=> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B"
1.18 +  unfolding setL2_def simp_implies_def by simp
1.19 +
1.20 +lemma setL2_infinite [simp]: "\<not> finite A \<Longrightarrow> setL2 f A = 0"
1.21 +  unfolding setL2_def by simp
1.22 +
1.23 +lemma setL2_empty [simp]: "setL2 f {} = 0"
1.24 +  unfolding setL2_def by simp
1.25 +
1.26 +lemma setL2_insert [simp]:
1.27 +  "\<lbrakk>finite F; a \<notin> F\<rbrakk> \<Longrightarrow>
1.28 +    setL2 f (insert a F) = sqrt ((f a)\<twosuperior> + (setL2 f F)\<twosuperior>)"
1.29 +  unfolding setL2_def by (simp add: setsum_nonneg)
1.30 +
1.31 +lemma setL2_nonneg [simp]: "0 \<le> setL2 f A"
1.32 +  unfolding setL2_def by (simp add: setsum_nonneg)
1.33 +
1.34 +lemma setL2_0': "\<forall>a\<in>A. f a = 0 \<Longrightarrow> setL2 f A = 0"
1.35 +  unfolding setL2_def by simp
1.36 +
1.37 +lemma setL2_mono:
1.38 +  assumes "\<And>i. i \<in> K \<Longrightarrow> f i \<le> g i"
1.39 +  assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"
1.40 +  shows "setL2 f K \<le> setL2 g K"
1.41 +  unfolding setL2_def
1.42 +  by (simp add: setsum_nonneg setsum_mono power_mono prems)
1.43 +
1.44 +lemma setL2_right_distrib:
1.45 +  "0 \<le> r \<Longrightarrow> r * setL2 f A = setL2 (\<lambda>x. r * f x) A"
1.46 +  unfolding setL2_def
1.47 +  apply (simp add: power_mult_distrib)
1.48 +  apply (simp add: setsum_right_distrib [symmetric])
1.49 +  apply (simp add: real_sqrt_mult setsum_nonneg)
1.50 +  done
1.51 +
1.52 +lemma setL2_left_distrib:
1.53 +  "0 \<le> r \<Longrightarrow> setL2 f A * r = setL2 (\<lambda>x. f x * r) A"
1.54 +  unfolding setL2_def
1.55 +  apply (simp add: power_mult_distrib)
1.56 +  apply (simp add: setsum_left_distrib [symmetric])
1.57 +  apply (simp add: real_sqrt_mult setsum_nonneg)
1.58 +  done
1.59 +
1.60 +lemma setsum_nonneg_eq_0_iff:
1.61 +  fixes f :: "'a \<Rightarrow> 'b::pordered_ab_group_add"
1.62 +  shows "\<lbrakk>finite A; \<forall>x\<in>A. 0 \<le> f x\<rbrakk> \<Longrightarrow> setsum f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
1.63 +  apply (induct set: finite, simp)
1.65 +  done
1.66 +
1.67 +lemma setL2_eq_0_iff: "finite A \<Longrightarrow> setL2 f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
1.68 +  unfolding setL2_def
1.69 +  by (simp add: setsum_nonneg setsum_nonneg_eq_0_iff)
1.70 +
1.71 +lemma setL2_triangle_ineq:
1.72 +  shows "setL2 (\<lambda>i. f i + g i) A \<le> setL2 f A + setL2 g A"
1.73 +proof (cases "finite A")
1.74 +  case False
1.75 +  thus ?thesis by simp
1.76 +next
1.77 +  case True
1.78 +  thus ?thesis
1.79 +  proof (induct set: finite)
1.80 +    case empty
1.81 +    show ?case by simp
1.82 +  next
1.83 +    case (insert x F)
1.84 +    hence "sqrt ((f x + g x)\<twosuperior> + (setL2 (\<lambda>i. f i + g i) F)\<twosuperior>) \<le>
1.85 +           sqrt ((f x + g x)\<twosuperior> + (setL2 f F + setL2 g F)\<twosuperior>)"
1.86 +      by (intro real_sqrt_le_mono add_left_mono power_mono insert
1.88 +    also have
1.89 +      "\<dots> \<le> sqrt ((f x)\<twosuperior> + (setL2 f F)\<twosuperior>) + sqrt ((g x)\<twosuperior> + (setL2 g F)\<twosuperior>)"
1.90 +      by (rule real_sqrt_sum_squares_triangle_ineq)
1.91 +    finally show ?case
1.92 +      using insert by simp
1.93 +  qed
1.94 +qed
1.95 +
1.96 +lemma sqrt_sum_squares_le_sum:
1.97 +  "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<twosuperior> + y\<twosuperior>) \<le> x + y"
1.98 +  apply (rule power2_le_imp_le)
1.99 +  apply (simp add: power2_sum)
1.100 +  apply (simp add: mult_nonneg_nonneg)
1.102 +  done
1.103 +
1.104 +lemma setL2_le_setsum [rule_format]:
1.105 +  "(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> setL2 f A \<le> setsum f A"
1.106 +  apply (cases "finite A")
1.107 +  apply (induct set: finite)
1.108 +  apply simp
1.109 +  apply clarsimp
1.110 +  apply (erule order_trans [OF sqrt_sum_squares_le_sum])
1.111 +  apply simp
1.112 +  apply simp
1.113 +  apply simp
1.114 +  done
1.115 +
1.116 +lemma sqrt_sum_squares_le_sum_abs: "sqrt (x\<twosuperior> + y\<twosuperior>) \<le> \<bar>x\<bar> + \<bar>y\<bar>"
1.117 +  apply (rule power2_le_imp_le)
1.118 +  apply (simp add: power2_sum)
1.119 +  apply (simp add: mult_nonneg_nonneg)
1.121 +  done
1.122 +
1.123 +lemma setL2_le_setsum_abs: "setL2 f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)"
1.124 +  apply (cases "finite A")
1.125 +  apply (induct set: finite)
1.126 +  apply simp
1.127 +  apply simp
1.128 +  apply (rule order_trans [OF sqrt_sum_squares_le_sum_abs])
1.129 +  apply simp
1.130 +  apply simp
1.131 +  done
1.132 +
1.133 +lemma setL2_mult_ineq_lemma:
1.134 +  fixes a b c d :: real
1.135 +  shows "2 * (a * c) * (b * d) \<le> a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior>"
1.136 +proof -
1.137 +  have "0 \<le> (a * d - b * c)\<twosuperior>" by simp
1.138 +  also have "\<dots> = a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior> - 2 * (a * d) * (b * c)"
1.139 +    by (simp only: power2_diff power_mult_distrib)
1.140 +  also have "\<dots> = a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior> - 2 * (a * c) * (b * d)"
1.141 +    by simp
1.142 +  finally show "2 * (a * c) * (b * d) \<le> a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior>"
1.143 +    by simp
1.144 +qed
1.145 +
1.146 +lemma setL2_mult_ineq: "(\<Sum>i\<in>A. \<bar>f i\<bar> * \<bar>g i\<bar>) \<le> setL2 f A * setL2 g A"
1.147 +  apply (cases "finite A")
1.148 +  apply (induct set: finite)
1.149 +  apply simp
1.150 +  apply (rule power2_le_imp_le, simp)
1.151 +  apply (rule order_trans)
1.152 +  apply (rule power_mono)
1.155 +  apply (simp add: power2_sum)
1.156 +  apply (simp add: power_mult_distrib)
1.157 +  apply (simp add: right_distrib left_distrib)
1.158 +  apply (rule ord_le_eq_trans)
1.159 +  apply (rule setL2_mult_ineq_lemma)
1.160 +  apply simp
1.161 +  apply (intro mult_nonneg_nonneg setL2_nonneg)
1.162 +  apply simp
1.163 +  done
1.164 +
1.165 +lemma member_le_setL2: "\<lbrakk>finite A; i \<in> A\<rbrakk> \<Longrightarrow> f i \<le> setL2 f A"
1.166 +  apply (rule_tac s="insert i (A - {i})" and t="A" in subst)
1.167 +  apply fast
1.168 +  apply (subst setL2_insert)
1.169 +  apply simp
1.170 +  apply simp
1.171 +  apply simp
1.172 +  done
1.173 +
1.174 +subsection {* Norms *}
1.175 +
1.176 +instantiation "^" :: (real_normed_vector, type) real_normed_vector
1.177 +begin
1.178 +
1.179 +definition vector_norm_def:
1.180 +  "norm (x::'a^'b) = setL2 (\<lambda>i. norm (x\$i)) {1 .. dimindex (UNIV:: 'b set)}"
1.181 +
1.182 +definition vector_sgn_def:
1.183 +  "sgn (x::'a^'b) = scaleR (inverse (norm x)) x"
1.184 +
1.185 +instance proof
1.186 +  fix a :: real and x y :: "'a ^ 'b"
1.187 +  show "0 \<le> norm x"
1.188 +    unfolding vector_norm_def
1.189 +    by (rule setL2_nonneg)
1.190 +  show "norm x = 0 \<longleftrightarrow> x = 0"
1.191 +    unfolding vector_norm_def
1.192 +    by (simp add: setL2_eq_0_iff Cart_eq)
1.193 +  show "norm (x + y) \<le> norm x + norm y"
1.194 +    unfolding vector_norm_def
1.195 +    apply (rule order_trans [OF _ setL2_triangle_ineq])
1.196 +    apply (rule setL2_mono)
1.197 +    apply (simp add: vector_component norm_triangle_ineq)
1.198 +    apply simp
1.199 +    done
1.200 +  show "norm (scaleR a x) = \<bar>a\<bar> * norm x"
1.201 +    unfolding vector_norm_def
1.202 +    by (simp add: vector_component norm_scaleR setL2_right_distrib
1.203 +             cong: strong_setL2_cong)
1.204 +  show "sgn x = scaleR (inverse (norm x)) x"
1.205 +    by (rule vector_sgn_def)
1.206 +qed
1.207 +
1.208 +end
1.209 +
1.210  subsection{* Properties of the dot product.  *}
1.211
1.212  lemma dot_sym: "(x::'a:: {comm_monoid_add, ab_semigroup_mult} ^ 'n) \<bullet> y = y \<bullet> x"
1.213 @@ -393,18 +596,7 @@
1.214  lemma dot_pos_lt: "(0 < x \<bullet> x) \<longleftrightarrow> (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n) \<noteq> 0" using dot_eq_0[of x] dot_pos_le[of x]
1.215    by (auto simp add: le_less)
1.216
1.217 -subsection {* Introduce norms, but defer many properties till we get square roots. *}
1.218 -text{* FIXME : This is ugly *}
1.220 -  real_of_real_def [code inline, simp]: "real == id"
1.221 -
1.222 -instantiation "^" :: ("{times, comm_monoid_add}", type) norm begin
1.223 -definition  real_vector_norm_def: "norm \<equiv> (\<lambda>x. sqrt (real (x \<bullet> x)))"
1.224 -instance ..
1.225 -end
1.226 -
1.227 -
1.228 -subsection{* The collapse of the general concepts to dimention one. *}
1.229 +subsection{* The collapse of the general concepts to dimension one. *}
1.230
1.231  lemma vector_one: "(x::'a ^1) = (\<chi> i. (x\$1))"
1.232    by (vector dimindex_def)
1.233 @@ -415,11 +607,15 @@
1.234    apply (simp only: vector_one[symmetric])
1.235    done
1.236
1.237 +lemma norm_vector_1: "norm (x :: _^1) = norm (x\$1)"
1.238 +  by (simp add: vector_norm_def dimindex_def)
1.239 +
1.240  lemma norm_real: "norm(x::real ^ 1) = abs(x\$1)"
1.241 -  by (simp add: real_vector_norm_def)
1.242 +  by (simp add: norm_vector_1)
1.243
1.244  text{* Metric *}
1.245
1.246 +text {* FIXME: generalize to arbitrary @{text real_normed_vector} types *}
1.247  definition dist:: "real ^ 'n \<Rightarrow> real ^ 'n \<Rightarrow> real" where
1.248    "dist x y = norm (x - y)"
1.249
1.250 @@ -531,27 +727,30 @@
1.251  text{* Hence derive more interesting properties of the norm. *}
1.252
1.253  lemma norm_0: "norm (0::real ^ 'n) = 0"
1.254 -  by (simp add: real_vector_norm_def dot_eq_0)
1.255 -
1.256 -lemma norm_pos_le: "0 <= norm (x::real^'n)"
1.257 -  by (simp add: real_vector_norm_def dot_pos_le)
1.258 +  by (rule norm_zero)
1.259 +
1.260 +lemma norm_pos_le: "0 <= norm (x::real^'n)"
1.261 +  by (rule norm_ge_zero)
1.262  lemma norm_neg: " norm(-x) = norm (x:: real ^ 'n)"
1.263 -  by (simp add: real_vector_norm_def dot_lneg dot_rneg)
1.264 +  by (rule norm_minus_cancel)
1.265  lemma norm_sub: "norm(x - y) = norm(y - (x::real ^ 'n))"
1.266 -  by (metis norm_neg minus_diff_eq)
1.267 +  by (rule norm_minus_commute)
1.268  lemma norm_mul: "norm(a *s x) = abs(a) * norm x"
1.269 -  by (simp add: real_vector_norm_def dot_lmult dot_rmult mult_assoc[symmetric] real_sqrt_mult)
1.270 +  by (simp add: vector_norm_def vector_component setL2_right_distrib
1.271 +           abs_mult cong: strong_setL2_cong)
1.272  lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (x \<bullet> x = (0::real))"
1.273 -  by (simp add: real_vector_norm_def)
1.274 +  by (simp add: vector_norm_def dot_def setL2_def power2_eq_square)
1.275  lemma norm_eq_0: "norm x = 0 \<longleftrightarrow> x = (0::real ^ 'n)"
1.276 -  by (simp add: real_vector_norm_def dot_eq_0)
1.277 +  by (rule norm_eq_zero)
1.278  lemma norm_pos_lt: "0 < norm x \<longleftrightarrow> x \<noteq> (0::real ^ 'n)"
1.279 -  by (metis less_le real_vector_norm_def norm_pos_le norm_eq_0)
1.280 +  by (rule zero_less_norm_iff)
1.281 +lemma real_vector_norm_def: "norm x = sqrt (x \<bullet> x)"
1.282 +  by (simp add: vector_norm_def setL2_def dot_def power2_eq_square)
1.283  lemma norm_pow_2: "norm x ^ 2 = x \<bullet> x"
1.284 -  by (simp add: real_vector_norm_def dot_pos_le)
1.285 +  by (simp add: real_vector_norm_def)
1.286  lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_0)
1.287  lemma norm_le_0: "norm x <= 0 \<longleftrightarrow> x = (0::real ^'n)"
1.288 -  by (metis norm_eq_0 norm_pos_le order_antisym)
1.289 +  by (rule norm_le_zero_iff)
1.290  lemma vector_mul_eq_0: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0"
1.291    by vector
1.292  lemma vector_mul_lcancel: "a *s x = a *s y \<longleftrightarrow> a = (0::real) \<or> x = y"
1.293 @@ -583,19 +782,14 @@
1.294    ultimately show ?thesis by metis
1.295  qed
1.296
1.297 -lemma norm_abs[simp]: "abs (norm x) = norm (x::real ^'n)"
1.298 -  using norm_pos_le[of x] by (simp add: real_abs_def linorder_linear)
1.299 +lemma norm_abs: "abs (norm x) = norm (x::real ^'n)"
1.300 +  by (rule abs_norm_cancel) (* already declared [simp] *)
1.301
1.302  lemma norm_cauchy_schwarz_abs: "\<bar>x \<bullet> y\<bar> \<le> norm x * norm y"
1.303    using norm_cauchy_schwarz[of x y] norm_cauchy_schwarz[of x "-y"]
1.304    by (simp add: real_abs_def dot_rneg norm_neg)
1.305  lemma norm_triangle: "norm(x + y) <= norm x + norm (y::real ^'n)"
1.306 -  unfolding real_vector_norm_def
1.307 -  apply (rule real_le_lsqrt)
1.308 -  apply (auto simp add: dot_pos_le real_vector_norm_def[symmetric] norm_pos_le norm_pow_2[symmetric] intro: add_nonneg_nonneg)[1]
1.309 -  apply (auto simp add: dot_pos_le real_vector_norm_def[symmetric] norm_pos_le norm_pow_2[symmetric] intro: add_nonneg_nonneg)[1]
1.311 -    by (simp add: norm_pow_2[symmetric] power2_eq_square ring_simps norm_cauchy_schwarz)
1.312 +  by (rule norm_triangle_ineq)
1.313
1.314  lemma norm_triangle_sub: "norm (x::real ^'n) <= norm(y) + norm(x - y)"
1.315    using norm_triangle[of "y" "x - y"] by (simp add: ring_simps)
1.316 @@ -627,19 +821,10 @@
1.317  qed
1.318
1.319  lemma component_le_norm: "i \<in> {1 .. dimindex(UNIV :: 'n set)} ==> \<bar>x\$i\<bar> <= norm (x::real ^ 'n)"
1.320 -proof(simp add: real_vector_norm_def, rule real_le_rsqrt, clarsimp)
1.321 -  assume i: "Suc 0 \<le> i" "i \<le> dimindex (UNIV :: 'n set)"
1.322 -  let ?S = "{1 .. dimindex(UNIV :: 'n set)}"
1.323 -  let ?f = "(\<lambda>k. if k = i then x\$i ^2 else 0)"
1.324 -  have fS: "finite ?S" by simp
1.325 -  from i setsum_delta[OF fS, of i "\<lambda>k. x\$i ^ 2"]
1.326 -  have th: "x\$i^2 = setsum ?f ?S" by simp
1.327 -  let ?g = "\<lambda>k. x\$k * x\$k"
1.328 -  {fix x assume x: "x \<in> ?S" have "?f x \<le> ?g x" by (simp add: power2_eq_square)}
1.329 -  with setsum_mono[of ?S ?f ?g]
1.330 -  have "setsum ?f ?S \<le> setsum ?g ?S" by blast
1.331 -  then show "x\$i ^2 \<le> x \<bullet> (x:: real ^ 'n)" unfolding dot_def th[symmetric] .
1.332 -qed
1.333 +  apply (simp add: vector_norm_def)
1.334 +  apply (rule member_le_setL2, simp_all)
1.335 +  done
1.336 +
1.337  lemma norm_bound_component_le: "norm(x::real ^ 'n) <= e
1.338                  ==> \<forall>i \<in> {1 .. dimindex(UNIV:: 'n set)}. \<bar>x\$i\<bar> <= e"
1.339    by (metis component_le_norm order_trans)
1.340 @@ -649,24 +834,12 @@
1.341    by (metis component_le_norm basic_trans_rules(21))
1.342
1.343  lemma norm_le_l1: "norm (x:: real ^'n) <= setsum(\<lambda>i. \<bar>x\$i\<bar>) {1..dimindex(UNIV::'n set)}"
1.345 -  case 0 thus ?case by simp
1.346 -next
1.347 -  case (Suc n)
1.348 -  have th: "2 * (\<bar>x\$(Suc n)\<bar> * (\<Sum>i = Suc 0..n. \<bar>x\$i\<bar>)) \<ge> 0"
1.349 -    apply simp
1.350 -    apply (rule mult_nonneg_nonneg)
1.351 -    by (simp_all add: setsum_abs_ge_zero)
1.352 -
1.353 -  from Suc
1.354 -  show ?case using th by (simp add: power2_eq_square ring_simps)
1.355 -qed
1.356 +  by (simp add: vector_norm_def setL2_le_setsum)
1.357
1.358  lemma real_abs_norm: "\<bar> norm x\<bar> = norm (x :: real ^'n)"
1.359 -  by (simp add: norm_pos_le)
1.360 +  by (rule abs_norm_cancel)
1.361  lemma real_abs_sub_norm: "\<bar>norm(x::real ^'n) - norm y\<bar> <= norm(x - y)"
1.362 -  apply (simp add: abs_le_iff ring_simps)
1.363 -  by (metis norm_triangle_sub norm_sub)
1.364 +  by (rule norm_triangle_ineq3)
1.365  lemma norm_le: "norm(x::real ^ 'n) <= norm(y) \<longleftrightarrow> x \<bullet> x <= y \<bullet> y"
1.367  lemma norm_lt: "norm(x::real ^'n) < norm(y) \<longleftrightarrow> x \<bullet> x < y \<bullet> y"
1.368 @@ -682,13 +855,7 @@
1.369    by (simp add: real_vector_norm_def  dot_pos_le )
1.370
1.371  lemma norm_eq_square: "norm(x) = a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x = a^2"
1.372 -proof-
1.373 -  have th: "\<And>x y::real. x^2 = y^2 \<longleftrightarrow> x = y \<or> x = -y" by algebra
1.374 -  show ?thesis using norm_pos_le[of x]
1.375 -  apply (simp add: dot_square_norm th)
1.376 -  apply arith
1.377 -  done
1.378 -qed
1.379 +  by (auto simp add: real_vector_norm_def)
1.380
1.381  lemma real_abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> (x::real)^2 \<le> y^2"
1.382  proof-
1.383 @@ -698,14 +865,14 @@
1.384  qed
1.385
1.386  lemma norm_le_square: "norm(x) <= a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x <= a^2"
1.387 +  apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric])
1.388    using norm_pos_le[of x]
1.389 -  apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric])
1.390    apply arith
1.391    done
1.392
1.393  lemma norm_ge_square: "norm(x) >= a \<longleftrightarrow> a <= 0 \<or> x \<bullet> x >= a ^ 2"
1.394 +  apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric])
1.395    using norm_pos_le[of x]
1.396 -  apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric])
1.397    apply arith
1.398    done
1.399
1.400 @@ -917,10 +1084,10 @@
1.401    assumes fS: "finite S"
1.402    shows "norm (setsum f S) <= setsum (\<lambda>x. norm(f x)) S"
1.403  proof(induct rule: finite_induct[OF fS])
1.404 -  case 1 thus ?case by simp norm
1.405 +  case 1 thus ?case by simp
1.406  next
1.407    case (2 x S)
1.408 -  from "2.hyps" have "norm (setsum f (insert x S)) \<le> norm (f x) + norm (setsum f S)" apply (simp add: norm_triangle_ineq) by norm
1.409 +  from "2.hyps" have "norm (setsum f (insert x S)) \<le> norm (f x) + norm (setsum f S)" by (simp add: norm_triangle_ineq)
1.410    also have "\<dots> \<le> norm (f x) + setsum (\<lambda>x. norm(f x)) S"
1.411      using "2.hyps" by simp
1.412    finally  show ?case  using "2.hyps" by simp
1.413 @@ -1552,7 +1719,9 @@
1.414      {fix x::"real ^ 'n"
1.415        have "norm (f x) \<le> ?K *  norm x"
1.416        using B[rule_format, of x] norm_pos_le[of x] norm_pos_le[of "f x"] Bp
1.419 +      apply (erule order_trans, simp)
1.420 +      done
1.421    }
1.422    then show ?thesis using Kp by blast
1.423  qed
1.424 @@ -2268,7 +2437,7 @@
1.425    {assume H: ?lhs
1.426      from H[rule_format, of "basis 1"]
1.427      have bp: "b \<ge> 0" using norm_pos_le[of "f (basis 1)"] dimindex_ge_1[of "UNIV:: 'n set"]
1.428 -      by (auto simp add: norm_basis)
1.429 +      by (auto simp add: norm_basis elim: order_trans [OF norm_ge_zero])
1.430      {fix x :: "real ^'n"
1.431        {assume "x = 0"
1.432  	then have "norm (f x) \<le> b * norm x" by (simp add: linear_0[OF lf] norm_0 bp)}
1.433 @@ -2276,7 +2445,7 @@
1.434        {assume x0: "x \<noteq> 0"
1.435  	hence n0: "norm x \<noteq> 0" by (metis norm_eq_0)
1.436  	let ?c = "1/ norm x"
1.437 -	have "norm (?c*s x) = 1" by (simp add: n0 norm_mul)
1.438 +	have "norm (?c*s x) = 1" using x0 by (simp add: n0 norm_mul)
1.439  	with H have "norm (f(?c*s x)) \<le> b" by blast
1.440  	hence "?c * norm (f x) \<le> b"
1.441  	  by (simp add: linear_cmul[OF lf] norm_mul)
1.442 @@ -2585,7 +2754,7 @@
1.443      by (simp add: dot_def setsum_add_split[OF th_0, of _ ?m] pastecart_def dimindex_finite_sum Cart_lambda_beta setsum_nonneg zero_le_square del: One_nat_def)
1.444    then show ?thesis
1.445      unfolding th0
1.446 -    unfolding real_vector_norm_def real_sqrt_le_iff real_of_real_def id_def
1.447 +    unfolding real_vector_norm_def real_sqrt_le_iff id_def
1.448      by (simp add: dot_def dimindex_finite_sum Cart_lambda_beta)
1.449  qed
1.450
1.451 @@ -2617,7 +2786,7 @@
1.452      by (simp add: dot_def setsum_add_split[OF th_0, of _ ?m] pastecart_def dimindex_finite_sum Cart_lambda_beta setsum_nonneg zero_le_square setsum_reindex[OF finj, unfolded fS] del: One_nat_def)
1.453    then show ?thesis
1.454      unfolding th0
1.455 -    unfolding real_vector_norm_def real_sqrt_le_iff real_of_real_def id_def
1.456 +    unfolding real_vector_norm_def real_sqrt_le_iff id_def
1.457      by (simp add: dot_def dimindex_finite_sum Cart_lambda_beta)
1.458  qed
1.459
1.460 @@ -2674,7 +2843,7 @@
1.461  qed
1.462
1.463  lemma norm_pastecart: "norm(pastecart x y) <= norm(x :: real ^ _) + norm(y)"
1.464 -  unfolding real_vector_norm_def dot_pastecart real_sqrt_le_iff real_of_real_def id_def
1.465 +  unfolding real_vector_norm_def dot_pastecart real_sqrt_le_iff id_def
1.466    apply (rule power2_le_imp_le)