src/HOL/Library/Euclidean_Space.thy
 changeset 30240 5b25fee0362c parent 29906 80369da39838 child 30242 aea5d7fa7ef5
```     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Wed Mar 04 10:43:39 2009 +0100
1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Wed Mar 04 10:45:52 2009 +0100
1.3 @@ -8,6 +8,7 @@
1.4  theory Euclidean_Space
1.5    imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Complex_Main
1.6    Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type
1.7 +  Inner_Product
1.8    uses ("normarith.ML")
1.9  begin
1.10
1.11 @@ -84,7 +85,13 @@
1.12  instance by (intro_classes)
1.13  end
1.14
1.15 -text{* Also the scalar-vector multiplication. FIXME: We should unify this with the scalar multiplication in @{text real_vector} *}
1.16 +instantiation "^" :: (scaleR, type) scaleR
1.17 +begin
1.18 +definition vector_scaleR_def: "scaleR = (\<lambda> r x.  (\<chi> i. scaleR r (x\$i)))"
1.19 +instance ..
1.20 +end
1.21 +
1.22 +text{* Also the scalar-vector multiplication. *}
1.23
1.24  definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^'n \<Rightarrow> 'a ^ 'n" (infixr "*s" 75)
1.25    where "c *s x = (\<chi> i. c * (x\$i))"
1.26 @@ -118,6 +125,7 @@
1.27               [@{thm vector_add_def}, @{thm vector_mult_def},
1.28                @{thm vector_minus_def}, @{thm vector_uminus_def},
1.29                @{thm vector_one_def}, @{thm vector_zero_def}, @{thm vec_def},
1.30 +              @{thm vector_scaleR_def},
1.31                @{thm Cart_lambda_beta'}, @{thm vector_scalar_mult_def}]
1.32   fun vector_arith_tac ths =
1.33     simp_tac ss1
1.34 @@ -166,9 +174,18 @@
1.35    shows "(- x)\$i = - (x\$i)"
1.36    using i by vector
1.37
1.38 +lemma vector_scaleR_component:
1.39 +  fixes x :: "'a::scaleR ^ 'n"
1.40 +  assumes i: "i \<in> {1 .. dimindex(UNIV :: 'n set)}"
1.41 +  shows "(scaleR r x)\$i = scaleR r (x\$i)"
1.42 +  using i by vector
1.43 +
1.44  lemma cond_component: "(if b then x else y)\$i = (if b then x\$i else y\$i)" by vector
1.45
1.46 -lemmas vector_component = vec_component vector_add_component vector_mult_component vector_smult_component vector_minus_component vector_uminus_component cond_component
1.47 +lemmas vector_component =
1.48 +  vec_component vector_add_component vector_mult_component
1.49 +  vector_smult_component vector_minus_component vector_uminus_component
1.50 +  vector_scaleR_component cond_component
1.51
1.52  subsection {* Some frequently useful arithmetic lemmas over vectors. *}
1.53
1.54 @@ -199,6 +216,9 @@
1.55    apply (intro_classes)
1.56    by (vector Cart_eq)
1.57
1.58 +instance "^" :: (real_vector, type) real_vector
1.59 +  by default (vector scaleR_left_distrib scaleR_right_distrib)+
1.60 +
1.61  instance "^" :: (semigroup_mult,type) semigroup_mult
1.62    apply (intro_classes) by (vector mult_assoc)
1.63
1.64 @@ -242,6 +262,18 @@
1.65  instance "^" :: (ring,type) ring by (intro_classes)
1.66  instance "^" :: (semiring_1_cancel,type) semiring_1_cancel by (intro_classes)
1.67  instance "^" :: (comm_semiring_1,type) comm_semiring_1 by (intro_classes)
1.68 +
1.69 +instance "^" :: (ring_1,type) ring_1 ..
1.70 +
1.71 +instance "^" :: (real_algebra,type) real_algebra
1.72 +  apply intro_classes
1.73 +  apply (simp_all add: vector_scaleR_def ring_simps)
1.74 +  apply vector
1.75 +  apply vector
1.76 +  done
1.77 +
1.78 +instance "^" :: (real_algebra_1,type) real_algebra_1 ..
1.79 +
1.80  lemma of_nat_index:
1.81    "i\<in>{1 .. dimindex (UNIV :: 'n set)} \<Longrightarrow> (of_nat n :: 'a::semiring_1 ^'n)\$i = of_nat n"
1.82    apply (induct n)
1.83 @@ -290,8 +322,7 @@
1.84  qed
1.85
1.86  instance "^" :: (comm_ring_1,type) comm_ring_1 by intro_classes
1.87 -  (* FIXME!!! Why does the axclass package complain here !!*)
1.88 -(* instance "^" :: (ring_char_0,type) ring_char_0 by intro_classes *)
1.89 +instance "^" :: (ring_char_0,type) ring_char_0 by intro_classes
1.90
1.91  lemma vector_smult_assoc: "a *s (b *s x) = ((a::'a::semigroup_mult) * b) *s x"
1.92    by (vector mult_assoc)
1.93 @@ -314,6 +345,241 @@
1.94    apply (auto simp add: vec_def Cart_eq vec_component Cart_lambda_beta )
1.95    using dimindex_ge_1 apply auto done
1.96
1.97 +subsection {* Square root of sum of squares *}
1.98 +
1.99 +definition
1.100 +  "setL2 f A = sqrt (\<Sum>i\<in>A. (f i)\<twosuperior>)"
1.101 +
1.102 +lemma setL2_cong:
1.103 +  "\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B"
1.104 +  unfolding setL2_def by simp
1.105 +
1.106 +lemma strong_setL2_cong:
1.107 +  "\<lbrakk>A = B; \<And>x. x \<in> B =simp=> f x = g x\<rbrakk> \<Longrightarrow> setL2 f A = setL2 g B"
1.108 +  unfolding setL2_def simp_implies_def by simp
1.109 +
1.110 +lemma setL2_infinite [simp]: "\<not> finite A \<Longrightarrow> setL2 f A = 0"
1.111 +  unfolding setL2_def by simp
1.112 +
1.113 +lemma setL2_empty [simp]: "setL2 f {} = 0"
1.114 +  unfolding setL2_def by simp
1.115 +
1.116 +lemma setL2_insert [simp]:
1.117 +  "\<lbrakk>finite F; a \<notin> F\<rbrakk> \<Longrightarrow>
1.118 +    setL2 f (insert a F) = sqrt ((f a)\<twosuperior> + (setL2 f F)\<twosuperior>)"
1.119 +  unfolding setL2_def by (simp add: setsum_nonneg)
1.120 +
1.121 +lemma setL2_nonneg [simp]: "0 \<le> setL2 f A"
1.122 +  unfolding setL2_def by (simp add: setsum_nonneg)
1.123 +
1.124 +lemma setL2_0': "\<forall>a\<in>A. f a = 0 \<Longrightarrow> setL2 f A = 0"
1.125 +  unfolding setL2_def by simp
1.126 +
1.127 +lemma setL2_mono:
1.128 +  assumes "\<And>i. i \<in> K \<Longrightarrow> f i \<le> g i"
1.129 +  assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"
1.130 +  shows "setL2 f K \<le> setL2 g K"
1.131 +  unfolding setL2_def
1.132 +  by (simp add: setsum_nonneg setsum_mono power_mono prems)
1.133 +
1.134 +lemma setL2_right_distrib:
1.135 +  "0 \<le> r \<Longrightarrow> r * setL2 f A = setL2 (\<lambda>x. r * f x) A"
1.136 +  unfolding setL2_def
1.137 +  apply (simp add: power_mult_distrib)
1.138 +  apply (simp add: setsum_right_distrib [symmetric])
1.139 +  apply (simp add: real_sqrt_mult setsum_nonneg)
1.140 +  done
1.141 +
1.142 +lemma setL2_left_distrib:
1.143 +  "0 \<le> r \<Longrightarrow> setL2 f A * r = setL2 (\<lambda>x. f x * r) A"
1.144 +  unfolding setL2_def
1.145 +  apply (simp add: power_mult_distrib)
1.146 +  apply (simp add: setsum_left_distrib [symmetric])
1.147 +  apply (simp add: real_sqrt_mult setsum_nonneg)
1.148 +  done
1.149 +
1.150 +lemma setsum_nonneg_eq_0_iff:
1.151 +  fixes f :: "'a \<Rightarrow> 'b::pordered_ab_group_add"
1.152 +  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.153 +  apply (induct set: finite, simp)
1.154 +  apply (simp add: add_nonneg_eq_0_iff setsum_nonneg)
1.155 +  done
1.156 +
1.157 +lemma setL2_eq_0_iff: "finite A \<Longrightarrow> setL2 f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
1.158 +  unfolding setL2_def
1.159 +  by (simp add: setsum_nonneg setsum_nonneg_eq_0_iff)
1.160 +
1.161 +lemma setL2_triangle_ineq:
1.162 +  shows "setL2 (\<lambda>i. f i + g i) A \<le> setL2 f A + setL2 g A"
1.163 +proof (cases "finite A")
1.164 +  case False
1.165 +  thus ?thesis by simp
1.166 +next
1.167 +  case True
1.168 +  thus ?thesis
1.169 +  proof (induct set: finite)
1.170 +    case empty
1.171 +    show ?case by simp
1.172 +  next
1.173 +    case (insert x F)
1.174 +    hence "sqrt ((f x + g x)\<twosuperior> + (setL2 (\<lambda>i. f i + g i) F)\<twosuperior>) \<le>
1.175 +           sqrt ((f x + g x)\<twosuperior> + (setL2 f F + setL2 g F)\<twosuperior>)"
1.176 +      by (intro real_sqrt_le_mono add_left_mono power_mono insert
1.177 +                setL2_nonneg add_increasing zero_le_power2)
1.178 +    also have
1.179 +      "\<dots> \<le> sqrt ((f x)\<twosuperior> + (setL2 f F)\<twosuperior>) + sqrt ((g x)\<twosuperior> + (setL2 g F)\<twosuperior>)"
1.180 +      by (rule real_sqrt_sum_squares_triangle_ineq)
1.181 +    finally show ?case
1.182 +      using insert by simp
1.183 +  qed
1.184 +qed
1.185 +
1.186 +lemma sqrt_sum_squares_le_sum:
1.187 +  "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<twosuperior> + y\<twosuperior>) \<le> x + y"
1.188 +  apply (rule power2_le_imp_le)
1.189 +  apply (simp add: power2_sum)
1.190 +  apply (simp add: mult_nonneg_nonneg)
1.191 +  apply (simp add: add_nonneg_nonneg)
1.192 +  done
1.193 +
1.194 +lemma setL2_le_setsum [rule_format]:
1.195 +  "(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> setL2 f A \<le> setsum f A"
1.196 +  apply (cases "finite A")
1.197 +  apply (induct set: finite)
1.198 +  apply simp
1.199 +  apply clarsimp
1.200 +  apply (erule order_trans [OF sqrt_sum_squares_le_sum])
1.201 +  apply simp
1.202 +  apply simp
1.203 +  apply simp
1.204 +  done
1.205 +
1.206 +lemma sqrt_sum_squares_le_sum_abs: "sqrt (x\<twosuperior> + y\<twosuperior>) \<le> \<bar>x\<bar> + \<bar>y\<bar>"
1.207 +  apply (rule power2_le_imp_le)
1.208 +  apply (simp add: power2_sum)
1.209 +  apply (simp add: mult_nonneg_nonneg)
1.210 +  apply (simp add: add_nonneg_nonneg)
1.211 +  done
1.212 +
1.213 +lemma setL2_le_setsum_abs: "setL2 f A \<le> (\<Sum>i\<in>A. \<bar>f i\<bar>)"
1.214 +  apply (cases "finite A")
1.215 +  apply (induct set: finite)
1.216 +  apply simp
1.217 +  apply simp
1.218 +  apply (rule order_trans [OF sqrt_sum_squares_le_sum_abs])
1.219 +  apply simp
1.220 +  apply simp
1.221 +  done
1.222 +
1.223 +lemma setL2_mult_ineq_lemma:
1.224 +  fixes a b c d :: real
1.225 +  shows "2 * (a * c) * (b * d) \<le> a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior>"
1.226 +proof -
1.227 +  have "0 \<le> (a * d - b * c)\<twosuperior>" by simp
1.228 +  also have "\<dots> = a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior> - 2 * (a * d) * (b * c)"
1.229 +    by (simp only: power2_diff power_mult_distrib)
1.230 +  also have "\<dots> = a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior> - 2 * (a * c) * (b * d)"
1.231 +    by simp
1.232 +  finally show "2 * (a * c) * (b * d) \<le> a\<twosuperior> * d\<twosuperior> + b\<twosuperior> * c\<twosuperior>"
1.233 +    by simp
1.234 +qed
1.235 +
1.236 +lemma setL2_mult_ineq: "(\<Sum>i\<in>A. \<bar>f i\<bar> * \<bar>g i\<bar>) \<le> setL2 f A * setL2 g A"
1.237 +  apply (cases "finite A")
1.238 +  apply (induct set: finite)
1.239 +  apply simp
1.240 +  apply (rule power2_le_imp_le, simp)
1.241 +  apply (rule order_trans)
1.242 +  apply (rule power_mono)
1.243 +  apply (erule add_left_mono)
1.244 +  apply (simp add: add_nonneg_nonneg mult_nonneg_nonneg setsum_nonneg)
1.245 +  apply (simp add: power2_sum)
1.246 +  apply (simp add: power_mult_distrib)
1.247 +  apply (simp add: right_distrib left_distrib)
1.248 +  apply (rule ord_le_eq_trans)
1.249 +  apply (rule setL2_mult_ineq_lemma)
1.250 +  apply simp
1.251 +  apply (intro mult_nonneg_nonneg setL2_nonneg)
1.252 +  apply simp
1.253 +  done
1.254 +
1.255 +lemma member_le_setL2: "\<lbrakk>finite A; i \<in> A\<rbrakk> \<Longrightarrow> f i \<le> setL2 f A"
1.256 +  apply (rule_tac s="insert i (A - {i})" and t="A" in subst)
1.257 +  apply fast
1.258 +  apply (subst setL2_insert)
1.259 +  apply simp
1.260 +  apply simp
1.261 +  apply simp
1.262 +  done
1.263 +
1.264 +subsection {* Norms *}
1.265 +
1.266 +instantiation "^" :: (real_normed_vector, type) real_normed_vector
1.267 +begin
1.268 +
1.269 +definition vector_norm_def:
1.270 +  "norm (x::'a^'b) = setL2 (\<lambda>i. norm (x\$i)) {1 .. dimindex (UNIV:: 'b set)}"
1.271 +
1.272 +definition vector_sgn_def:
1.273 +  "sgn (x::'a^'b) = scaleR (inverse (norm x)) x"
1.274 +
1.275 +instance proof
1.276 +  fix a :: real and x y :: "'a ^ 'b"
1.277 +  show "0 \<le> norm x"
1.278 +    unfolding vector_norm_def
1.279 +    by (rule setL2_nonneg)
1.280 +  show "norm x = 0 \<longleftrightarrow> x = 0"
1.281 +    unfolding vector_norm_def
1.282 +    by (simp add: setL2_eq_0_iff Cart_eq)
1.283 +  show "norm (x + y) \<le> norm x + norm y"
1.284 +    unfolding vector_norm_def
1.285 +    apply (rule order_trans [OF _ setL2_triangle_ineq])
1.286 +    apply (rule setL2_mono)
1.287 +    apply (simp add: vector_component norm_triangle_ineq)
1.288 +    apply simp
1.289 +    done
1.290 +  show "norm (scaleR a x) = \<bar>a\<bar> * norm x"
1.291 +    unfolding vector_norm_def
1.292 +    by (simp add: vector_component norm_scaleR setL2_right_distrib
1.293 +             cong: strong_setL2_cong)
1.294 +  show "sgn x = scaleR (inverse (norm x)) x"
1.295 +    by (rule vector_sgn_def)
1.296 +qed
1.297 +
1.298 +end
1.299 +
1.300 +subsection {* Inner products *}
1.301 +
1.302 +instantiation "^" :: (real_inner, type) real_inner
1.303 +begin
1.304 +
1.305 +definition vector_inner_def:
1.306 +  "inner x y = setsum (\<lambda>i. inner (x\$i) (y\$i)) {1 .. dimindex(UNIV::'b set)}"
1.307 +
1.308 +instance proof
1.309 +  fix r :: real and x y z :: "'a ^ 'b"
1.310 +  show "inner x y = inner y x"
1.311 +    unfolding vector_inner_def
1.312 +    by (simp add: inner_commute)
1.313 +  show "inner (x + y) z = inner x z + inner y z"
1.314 +    unfolding vector_inner_def
1.315 +    by (vector inner_left_distrib)
1.316 +  show "inner (scaleR r x) y = r * inner x y"
1.317 +    unfolding vector_inner_def
1.318 +    by (vector inner_scaleR_left)
1.319 +  show "0 \<le> inner x x"
1.320 +    unfolding vector_inner_def
1.321 +    by (simp add: setsum_nonneg)
1.322 +  show "inner x x = 0 \<longleftrightarrow> x = 0"
1.323 +    unfolding vector_inner_def
1.324 +    by (simp add: Cart_eq setsum_nonneg_eq_0_iff)
1.325 +  show "norm x = sqrt (inner x x)"
1.326 +    unfolding vector_inner_def vector_norm_def setL2_def
1.327 +    by (simp add: power2_norm_eq_inner)
1.328 +qed
1.329 +
1.330 +end
1.331 +
1.332  subsection{* Properties of the dot product.  *}
1.333
1.334  lemma dot_sym: "(x::'a:: {comm_monoid_add, ab_semigroup_mult} ^ 'n) \<bullet> y = y \<bullet> x"
1.335 @@ -363,18 +629,7 @@
1.336  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.337    by (auto simp add: le_less)
1.338
1.339 -subsection {* Introduce norms, but defer many properties till we get square roots. *}
1.340 -text{* FIXME : This is ugly *}
1.341 -defs (overloaded)
1.342 -  real_of_real_def [code inline, simp]: "real == id"
1.343 -
1.344 -instantiation "^" :: ("{times, comm_monoid_add}", type) norm begin
1.345 -definition  real_vector_norm_def: "norm \<equiv> (\<lambda>x. sqrt (real (x \<bullet> x)))"
1.346 -instance ..
1.347 -end
1.348 -
1.349 -
1.350 -subsection{* The collapse of the general concepts to dimention one. *}
1.351 +subsection{* The collapse of the general concepts to dimension one. *}
1.352
1.353  lemma vector_one: "(x::'a ^1) = (\<chi> i. (x\$1))"
1.354    by (vector dimindex_def)
1.355 @@ -385,11 +640,15 @@
1.356    apply (simp only: vector_one[symmetric])
1.357    done
1.358
1.359 +lemma norm_vector_1: "norm (x :: _^1) = norm (x\$1)"
1.360 +  by (simp add: vector_norm_def dimindex_def)
1.361 +
1.362  lemma norm_real: "norm(x::real ^ 1) = abs(x\$1)"
1.363 -  by (simp add: real_vector_norm_def)
1.364 +  by (simp add: norm_vector_1)
1.365
1.366  text{* Metric *}
1.367
1.368 +text {* FIXME: generalize to arbitrary @{text real_normed_vector} types *}
1.369  definition dist:: "real ^ 'n \<Rightarrow> real ^ 'n \<Rightarrow> real" where
1.370    "dist x y = norm (x - y)"
1.371
1.372 @@ -501,27 +760,18 @@
1.373  text{* Hence derive more interesting properties of the norm. *}
1.374
1.375  lemma norm_0: "norm (0::real ^ 'n) = 0"
1.376 -  by (simp add: real_vector_norm_def dot_eq_0)
1.377 -
1.378 -lemma norm_pos_le: "0 <= norm (x::real^'n)"
1.379 -  by (simp add: real_vector_norm_def dot_pos_le)
1.380 -lemma norm_neg: " norm(-x) = norm (x:: real ^ 'n)"
1.381 -  by (simp add: real_vector_norm_def dot_lneg dot_rneg)
1.382 -lemma norm_sub: "norm(x - y) = norm(y - (x::real ^ 'n))"
1.383 -  by (metis norm_neg minus_diff_eq)
1.384 +  by (rule norm_zero)
1.385 +
1.386  lemma norm_mul: "norm(a *s x) = abs(a) * norm x"
1.387 -  by (simp add: real_vector_norm_def dot_lmult dot_rmult mult_assoc[symmetric] real_sqrt_mult)
1.388 +  by (simp add: vector_norm_def vector_component setL2_right_distrib
1.389 +           abs_mult cong: strong_setL2_cong)
1.390  lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (x \<bullet> x = (0::real))"
1.391 +  by (simp add: vector_norm_def dot_def setL2_def power2_eq_square)
1.392 +lemma real_vector_norm_def: "norm x = sqrt (x \<bullet> x)"
1.393 +  by (simp add: vector_norm_def setL2_def dot_def power2_eq_square)
1.394 +lemma norm_pow_2: "norm x ^ 2 = x \<bullet> x"
1.395    by (simp add: real_vector_norm_def)
1.396 -lemma norm_eq_0: "norm x = 0 \<longleftrightarrow> x = (0::real ^ 'n)"
1.397 -  by (simp add: real_vector_norm_def dot_eq_0)
1.398 -lemma norm_pos_lt: "0 < norm x \<longleftrightarrow> x \<noteq> (0::real ^ 'n)"
1.399 -  by (metis less_le real_vector_norm_def norm_pos_le norm_eq_0)
1.400 -lemma norm_pow_2: "norm x ^ 2 = x \<bullet> x"
1.401 -  by (simp add: real_vector_norm_def dot_pos_le)
1.402 -lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_0)
1.403 -lemma norm_le_0: "norm x <= 0 \<longleftrightarrow> x = (0::real ^'n)"
1.404 -  by (metis norm_eq_0 norm_pos_le order_antisym)
1.405 +lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero)
1.406  lemma vector_mul_eq_0: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0"
1.407    by vector
1.408  lemma vector_mul_lcancel: "a *s x = a *s y \<longleftrightarrow> a = (0::real) \<or> x = y"
1.409 @@ -535,14 +785,14 @@
1.410  lemma norm_cauchy_schwarz: "x \<bullet> y <= norm x * norm y"
1.411  proof-
1.412    {assume "norm x = 0"
1.413 -    hence ?thesis by (simp add: norm_eq_0 dot_lzero dot_rzero norm_0)}
1.414 +    hence ?thesis by (simp add: dot_lzero dot_rzero)}
1.415    moreover
1.416    {assume "norm y = 0"
1.417 -    hence ?thesis by (simp add: norm_eq_0 dot_lzero dot_rzero norm_0)}
1.418 +    hence ?thesis by (simp add: dot_lzero dot_rzero)}
1.419    moreover
1.420    {assume h: "norm x \<noteq> 0" "norm y \<noteq> 0"
1.421      let ?z = "norm y *s x - norm x *s y"
1.422 -    from h have p: "norm x * norm y > 0" by (metis norm_pos_le le_less zero_compare_simps)
1.423 +    from h have p: "norm x * norm y > 0" by (metis norm_ge_zero le_less zero_compare_simps)
1.424      from dot_pos_le[of ?z]
1.425      have "(norm x * norm y) * (x \<bullet> y) \<le> norm x ^2 * norm y ^2"
1.426        apply (simp add: dot_rsub dot_lsub dot_lmult dot_rmult ring_simps)
1.427 @@ -553,26 +803,16 @@
1.428    ultimately show ?thesis by metis
1.429  qed
1.430
1.431 -lemma norm_abs[simp]: "abs (norm x) = norm (x::real ^'n)"
1.432 -  using norm_pos_le[of x] by (simp add: real_abs_def linorder_linear)
1.433 -
1.434  lemma norm_cauchy_schwarz_abs: "\<bar>x \<bullet> y\<bar> \<le> norm x * norm y"
1.435    using norm_cauchy_schwarz[of x y] norm_cauchy_schwarz[of x "-y"]
1.436 -  by (simp add: real_abs_def dot_rneg norm_neg)
1.437 -lemma norm_triangle: "norm(x + y) <= norm x + norm (y::real ^'n)"
1.438 -  unfolding real_vector_norm_def
1.439 -  apply (rule real_le_lsqrt)
1.440 -  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.441 -  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.442 -  apply (simp add: dot_ladd dot_radd dot_sym )
1.443 -    by (simp add: norm_pow_2[symmetric] power2_eq_square ring_simps norm_cauchy_schwarz)
1.444 +  by (simp add: real_abs_def dot_rneg)
1.445
1.446  lemma norm_triangle_sub: "norm (x::real ^'n) <= norm(y) + norm(x - y)"
1.447 -  using norm_triangle[of "y" "x - y"] by (simp add: ring_simps)
1.448 +  using norm_triangle_ineq[of "y" "x - y"] by (simp add: ring_simps)
1.449  lemma norm_triangle_le: "norm(x::real ^'n) + norm y <= e ==> norm(x + y) <= e"
1.450 -  by (metis order_trans norm_triangle)
1.451 +  by (metis order_trans norm_triangle_ineq)
1.452  lemma norm_triangle_lt: "norm(x::real ^'n) + norm(y) < e ==> norm(x + y) < e"
1.453 -  by (metis basic_trans_rules(21) norm_triangle)
1.454 +  by (metis basic_trans_rules(21) norm_triangle_ineq)
1.455
1.456  lemma setsum_delta:
1.457    assumes fS: "finite S"
1.458 @@ -597,19 +837,10 @@
1.459  qed
1.460
1.461  lemma component_le_norm: "i \<in> {1 .. dimindex(UNIV :: 'n set)} ==> \<bar>x\$i\<bar> <= norm (x::real ^ 'n)"
1.462 -proof(simp add: real_vector_norm_def, rule real_le_rsqrt, clarsimp)
1.463 -  assume i: "Suc 0 \<le> i" "i \<le> dimindex (UNIV :: 'n set)"
1.464 -  let ?S = "{1 .. dimindex(UNIV :: 'n set)}"
1.465 -  let ?f = "(\<lambda>k. if k = i then x\$i ^2 else 0)"
1.466 -  have fS: "finite ?S" by simp
1.467 -  from i setsum_delta[OF fS, of i "\<lambda>k. x\$i ^ 2"]
1.468 -  have th: "x\$i^2 = setsum ?f ?S" by simp
1.469 -  let ?g = "\<lambda>k. x\$k * x\$k"
1.470 -  {fix x assume x: "x \<in> ?S" have "?f x \<le> ?g x" by (simp add: power2_eq_square)}
1.471 -  with setsum_mono[of ?S ?f ?g]
1.472 -  have "setsum ?f ?S \<le> setsum ?g ?S" by blast
1.473 -  then show "x\$i ^2 \<le> x \<bullet> (x:: real ^ 'n)" unfolding dot_def th[symmetric] .
1.474 -qed
1.475 +  apply (simp add: vector_norm_def)
1.476 +  apply (rule member_le_setL2, simp_all)
1.477 +  done
1.478 +
1.479  lemma norm_bound_component_le: "norm(x::real ^ 'n) <= e
1.480                  ==> \<forall>i \<in> {1 .. dimindex(UNIV:: 'n set)}. \<bar>x\$i\<bar> <= e"
1.481    by (metis component_le_norm order_trans)
1.482 @@ -619,24 +850,12 @@
1.483    by (metis component_le_norm basic_trans_rules(21))
1.484
1.485  lemma norm_le_l1: "norm (x:: real ^'n) <= setsum(\<lambda>i. \<bar>x\$i\<bar>) {1..dimindex(UNIV::'n set)}"
1.486 -proof (simp add: real_vector_norm_def, rule real_le_lsqrt,simp add: dot_pos_le, simp add: setsum_mono, simp add: dot_def, induct "dimindex(UNIV::'n set)")
1.487 -  case 0 thus ?case by simp
1.488 -next
1.489 -  case (Suc n)
1.490 -  have th: "2 * (\<bar>x\$(Suc n)\<bar> * (\<Sum>i = Suc 0..n. \<bar>x\$i\<bar>)) \<ge> 0"
1.491 -    apply simp
1.492 -    apply (rule mult_nonneg_nonneg)
1.493 -    by (simp_all add: setsum_abs_ge_zero)
1.494 -
1.495 -  from Suc
1.496 -  show ?case using th by (simp add: power2_eq_square ring_simps)
1.497 -qed
1.498 +  by (simp add: vector_norm_def setL2_le_setsum)
1.499
1.500  lemma real_abs_norm: "\<bar> norm x\<bar> = norm (x :: real ^'n)"
1.501 -  by (simp add: norm_pos_le)
1.502 +  by (rule abs_norm_cancel)
1.503  lemma real_abs_sub_norm: "\<bar>norm(x::real ^'n) - norm y\<bar> <= norm(x - y)"
1.504 -  apply (simp add: abs_le_iff ring_simps)
1.505 -  by (metis norm_triangle_sub norm_sub)
1.506 +  by (rule norm_triangle_ineq3)
1.507  lemma norm_le: "norm(x::real ^ 'n) <= norm(y) \<longleftrightarrow> x \<bullet> x <= y \<bullet> y"
1.508    by (simp add: real_vector_norm_def)
1.509  lemma norm_lt: "norm(x::real ^'n) < norm(y) \<longleftrightarrow> x \<bullet> x < y \<bullet> y"
1.510 @@ -652,13 +871,7 @@
1.511    by (simp add: real_vector_norm_def  dot_pos_le )
1.512
1.513  lemma norm_eq_square: "norm(x) = a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x = a^2"
1.514 -proof-
1.515 -  have th: "\<And>x y::real. x^2 = y^2 \<longleftrightarrow> x = y \<or> x = -y" by algebra
1.516 -  show ?thesis using norm_pos_le[of x]
1.517 -  apply (simp add: dot_square_norm th)
1.518 -  apply arith
1.519 -  done
1.520 -qed
1.521 +  by (auto simp add: real_vector_norm_def)
1.522
1.523  lemma real_abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> (x::real)^2 \<le> y^2"
1.524  proof-
1.525 @@ -668,14 +881,14 @@
1.526  qed
1.527
1.528  lemma norm_le_square: "norm(x) <= a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x <= a^2"
1.529 -  using norm_pos_le[of x]
1.530    apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric])
1.531 +  using norm_ge_zero[of x]
1.532    apply arith
1.533    done
1.534
1.535  lemma norm_ge_square: "norm(x) >= a \<longleftrightarrow> a <= 0 \<or> x \<bullet> x >= a ^ 2"
1.536 -  using norm_pos_le[of x]
1.537    apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric])
1.538 +  using norm_ge_zero[of x]
1.539    apply arith
1.540    done
1.541
1.542 @@ -746,14 +959,14 @@
1.543  lemma pth_d: "x + (0::real ^'n) == x" by (atomize (full)) vector
1.544
1.545  lemma norm_imp_pos_and_ge: "norm (x::real ^ 'n) == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
1.546 -  by (atomize) (auto simp add: norm_pos_le)
1.547 +  by (atomize) (auto simp add: norm_ge_zero)
1.548
1.549  lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \<ge> 0 \<and> -x \<ge> 0" by arith
1.550
1.551  lemma norm_pths:
1.552    "(x::real ^'n) = y \<longleftrightarrow> norm (x - y) \<le> 0"
1.553    "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
1.554 -  using norm_pos_le[of "x - y"] by (auto simp add: norm_0 norm_eq_0)
1.555 +  using norm_ge_zero[of "x - y"] by auto
1.556
1.557  use "normarith.ML"
1.558
1.559 @@ -797,11 +1010,6 @@
1.560
1.561  lemma dist_le_0: "dist x y <= 0 \<longleftrightarrow> x = y" by norm
1.562
1.563 -instantiation "^" :: (monoid_add,type) monoid_add
1.564 -begin
1.565 -  instance by (intro_classes)
1.566 -end
1.567 -
1.568  lemma setsum_eq: "setsum f S = (\<chi> i. setsum (\<lambda>x. (f x)\$i ) S)"
1.569    apply vector
1.570    apply auto
1.571 @@ -873,7 +1081,7 @@
1.572    assumes fS: "finite S"
1.573    shows "norm (setsum f S) <= setsum (\<lambda>x. norm(f x)) S"
1.574  proof(induct rule: finite_induct[OF fS])
1.575 -  case 1 thus ?case by (simp add: norm_zero)
1.576 +  case 1 thus ?case by simp
1.577  next
1.578    case (2 x S)
1.579    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.580 @@ -887,10 +1095,10 @@
1.581    assumes fS: "finite S"
1.582    shows "norm (setsum f S) <= setsum (\<lambda>x. norm(f x)) S"
1.583  proof(induct rule: finite_induct[OF fS])
1.584 -  case 1 thus ?case by simp norm
1.585 +  case 1 thus ?case by simp
1.586  next
1.587    case (2 x S)
1.588 -  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.589 +  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.590    also have "\<dots> \<le> norm (f x) + setsum (\<lambda>x. norm(f x)) S"
1.591      using "2.hyps" by simp
1.592    finally  show ?case  using "2.hyps" by simp
1.593 @@ -936,45 +1144,6 @@
1.594    using real_setsum_norm_le[OF fS K] setsum_constant[symmetric]
1.595    by simp
1.596
1.597 -instantiation "^" :: ("{scaleR, one, times}",type) scaleR
1.598 -begin
1.599 -
1.600 -definition vector_scaleR_def: "(scaleR :: real \<Rightarrow> 'a ^'b \<Rightarrow> 'a ^'b) \<equiv> (\<lambda> c x . (scaleR c 1) *s x)"
1.601 -instance ..
1.602 -end
1.603 -
1.604 -instantiation "^" :: ("ring_1",type) ring_1
1.605 -begin
1.606 -instance by intro_classes
1.607 -end
1.608 -
1.609 -instantiation "^" :: (real_algebra_1,type) real_vector
1.610 -begin
1.611 -
1.612 -instance
1.613 -  apply intro_classes
1.614 -  apply (simp_all  add: vector_scaleR_def)
1.615 -  apply (simp_all add: vector_sadd_rdistrib vector_add_ldistrib vector_smult_lid vector_smult_assoc scaleR_left_distrib mult_commute)
1.616 -  done
1.617 -end
1.618 -
1.619 -instantiation "^" :: (real_algebra_1,type) real_algebra
1.620 -begin
1.621 -
1.622 -instance
1.623 -  apply intro_classes
1.624 -  apply (simp_all add: vector_scaleR_def ring_simps)
1.625 -  apply vector
1.626 -  apply vector
1.627 -  done
1.628 -end
1.629 -
1.630 -instantiation "^" :: (real_algebra_1,type) real_algebra_1
1.631 -begin
1.632 -
1.633 -instance ..
1.634 -end
1.635 -
1.636  lemma setsum_vmul:
1.637    fixes f :: "'a \<Rightarrow> 'b::{real_normed_vector,semiring, mult_zero}"
1.638    assumes fS: "finite S"
1.639 @@ -1211,7 +1380,7 @@
1.640        by (auto simp add: setsum_component intro: abs_le_D1)
1.641      have Pne: "setsum (\<lambda>x. \<bar>f x \$ i\<bar>) ?Pn \<le> e"
1.642        using i component_le_norm[OF i, of "setsum (\<lambda>x. - f x) ?Pn"]  fPs[OF PnP]
1.643 -      by (auto simp add: setsum_negf norm_neg setsum_component vector_component intro: abs_le_D1)
1.644 +      by (auto simp add: setsum_negf setsum_component vector_component intro: abs_le_D1)
1.645      have "setsum (\<lambda>x. \<bar>f x \$ i\<bar>) P = setsum (\<lambda>x. \<bar>f x \$ i\<bar>) ?Pp + setsum (\<lambda>x. \<bar>f x \$ i\<bar>) ?Pn"
1.646        apply (subst thp)
1.647        apply (rule setsum_Un_nonzero)
1.648 @@ -1535,7 +1704,7 @@
1.649        unfolding norm_mul
1.650        apply (simp only: mult_commute)
1.651        apply (rule mult_mono)
1.652 -      by (auto simp add: ring_simps norm_pos_le) }
1.653 +      by (auto simp add: ring_simps norm_ge_zero) }
1.654      then have th: "\<forall>i\<in> ?S. norm ((x\$i) *s f (basis i :: real ^'m)) \<le> norm (f (basis i)) * norm x" by metis
1.655      from real_setsum_norm_le[OF fS, of "\<lambda>i. (x\$i) *s (f (basis i))", OF th]
1.656      have "norm (f x) \<le> ?B * norm x" unfolding th0 setsum_left_distrib by metis}
1.657 @@ -1552,16 +1721,18 @@
1.658    let ?K = "\<bar>B\<bar> + 1"
1.659    have Kp: "?K > 0" by arith
1.660      {assume C: "B < 0"
1.661 -      have "norm (1::real ^ 'n) > 0" by (simp add: norm_pos_lt)
1.662 +      have "norm (1::real ^ 'n) > 0" by (simp add: zero_less_norm_iff)
1.663        with C have "B * norm (1:: real ^ 'n) < 0"
1.664  	by (simp add: zero_compare_simps)
1.665 -      with B[rule_format, of 1] norm_pos_le[of "f 1"] have False by simp
1.666 +      with B[rule_format, of 1] norm_ge_zero[of "f 1"] have False by simp
1.667      }
1.668      then have Bp: "B \<ge> 0" by ferrack
1.669      {fix x::"real ^ 'n"
1.670        have "norm (f x) \<le> ?K *  norm x"
1.671 -      using B[rule_format, of x] norm_pos_le[of x] norm_pos_le[of "f x"] Bp
1.672 -      by (auto simp add: ring_simps split add: abs_split)
1.673 +      using B[rule_format, of x] norm_ge_zero[of x] norm_ge_zero[of "f x"] Bp
1.674 +      apply (auto simp add: ring_simps split add: abs_split)
1.675 +      apply (erule order_trans, simp)
1.676 +      done
1.677    }
1.678    then show ?thesis using Kp by blast
1.679  qed
1.680 @@ -1641,9 +1812,9 @@
1.681        apply simp
1.682        apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh] norm_mul ring_simps)
1.683        apply (rule mult_mono)
1.684 -      apply (auto simp add: norm_pos_le zero_le_mult_iff component_le_norm)
1.685 +      apply (auto simp add: norm_ge_zero zero_le_mult_iff component_le_norm)
1.686        apply (rule mult_mono)
1.687 -      apply (auto simp add: norm_pos_le zero_le_mult_iff component_le_norm)
1.688 +      apply (auto simp add: norm_ge_zero zero_le_mult_iff component_le_norm)
1.689        done}
1.690    then show ?thesis by metis
1.691  qed
1.692 @@ -1663,7 +1834,7 @@
1.693      have "B * norm x * norm y \<le> ?K * norm x * norm y"
1.694        apply -
1.695        apply (rule mult_right_mono, rule mult_right_mono)
1.696 -      by (auto simp add: norm_pos_le)
1.697 +      by (auto simp add: norm_ge_zero)
1.698      then have "norm (h x y) \<le> ?K * norm x * norm y"
1.699        using B[rule_format, of x y] by simp}
1.700    with Kp show ?thesis by blast
1.701 @@ -2276,21 +2447,21 @@
1.702    moreover
1.703    {assume H: ?lhs
1.704      from H[rule_format, of "basis 1"]
1.705 -    have bp: "b \<ge> 0" using norm_pos_le[of "f (basis 1)"] dimindex_ge_1[of "UNIV:: 'n set"]
1.706 -      by (auto simp add: norm_basis)
1.707 +    have bp: "b \<ge> 0" using norm_ge_zero[of "f (basis 1)"] dimindex_ge_1[of "UNIV:: 'n set"]
1.708 +      by (auto simp add: norm_basis elim: order_trans [OF norm_ge_zero])
1.709      {fix x :: "real ^'n"
1.710        {assume "x = 0"
1.711 -	then have "norm (f x) \<le> b * norm x" by (simp add: linear_0[OF lf] norm_0 bp)}
1.712 +	then have "norm (f x) \<le> b * norm x" by (simp add: linear_0[OF lf] bp)}
1.713        moreover
1.714        {assume x0: "x \<noteq> 0"
1.715 -	hence n0: "norm x \<noteq> 0" by (metis norm_eq_0)
1.716 +	hence n0: "norm x \<noteq> 0" by (metis norm_eq_zero)
1.717  	let ?c = "1/ norm x"
1.718 -	have "norm (?c*s x) = 1" by (simp add: n0 norm_mul)
1.719 +	have "norm (?c*s x) = 1" using x0 by (simp add: n0 norm_mul)
1.720  	with H have "norm (f(?c*s x)) \<le> b" by blast
1.721  	hence "?c * norm (f x) \<le> b"
1.722  	  by (simp add: linear_cmul[OF lf] norm_mul)
1.723  	hence "norm (f x) \<le> b * norm x"
1.724 -	  using n0 norm_pos_le[of x] by (auto simp add: field_simps)}
1.725 +	  using n0 norm_ge_zero[of x] by (auto simp add: field_simps)}
1.726        ultimately have "norm (f x) \<le> b * norm x" by blast}
1.727      then have ?rhs by blast}
1.728    ultimately show ?thesis by blast
1.729 @@ -2322,12 +2493,12 @@
1.730  qed
1.731
1.732  lemma onorm_pos_le: assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'m)" shows "0 <= onorm f"
1.733 -  using order_trans[OF norm_pos_le onorm(1)[OF lf, of "basis 1"], unfolded norm_basis_1] by simp
1.734 +  using order_trans[OF norm_ge_zero onorm(1)[OF lf, of "basis 1"], unfolded norm_basis_1] by simp
1.735
1.736  lemma onorm_eq_0: assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'m)"
1.737    shows "onorm f = 0 \<longleftrightarrow> (\<forall>x. f x = 0)"
1.738    using onorm[OF lf]
1.739 -  apply (auto simp add: norm_0 onorm_pos_le norm_le_0)
1.740 +  apply (auto simp add: onorm_pos_le)
1.741    apply atomize
1.742    apply (erule allE[where x="0::real"])
1.743    using onorm_pos_le[OF lf]
1.744 @@ -2365,7 +2536,7 @@
1.745  lemma onorm_neg_lemma: assumes lf: "linear (f::real ^'n \<Rightarrow> real^'m)"
1.746    shows "onorm (\<lambda>x. - f x) \<le> onorm f"
1.747    using onorm[OF linear_compose_neg[OF lf]] onorm[OF lf]
1.748 -  unfolding norm_neg by metis
1.749 +  unfolding norm_minus_cancel by metis
1.750
1.751  lemma onorm_neg: assumes lf: "linear (f::real ^'n \<Rightarrow> real^'m)"
1.752    shows "onorm (\<lambda>x. - f x) = onorm f"
1.753 @@ -2377,7 +2548,7 @@
1.754    shows "onorm (\<lambda>x. f x + g x) <= onorm f + onorm g"
1.755    apply(rule onorm(2)[OF linear_compose_add[OF lf lg], rule_format])
1.756    apply (rule order_trans)
1.757 -  apply (rule norm_triangle)
1.758 +  apply (rule norm_triangle_ineq)
1.759    apply (simp add: distrib)
1.760    apply (rule add_mono)
1.761    apply (rule onorm(1)[OF lf])
1.762 @@ -2594,7 +2765,7 @@
1.763      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.764    then show ?thesis
1.765      unfolding th0
1.766 -    unfolding real_vector_norm_def real_sqrt_le_iff real_of_real_def id_def
1.767 +    unfolding real_vector_norm_def real_sqrt_le_iff id_def
1.768      by (simp add: dot_def dimindex_finite_sum Cart_lambda_beta)
1.769  qed
1.770
1.771 @@ -2626,7 +2797,7 @@
1.772      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.773    then show ?thesis
1.774      unfolding th0
1.775 -    unfolding real_vector_norm_def real_sqrt_le_iff real_of_real_def id_def
1.776 +    unfolding real_vector_norm_def real_sqrt_le_iff id_def
1.777      by (simp add: dot_def dimindex_finite_sum Cart_lambda_beta)
1.778  qed
1.779
1.780 @@ -2683,7 +2854,7 @@
1.781  qed
1.782
1.783  lemma norm_pastecart: "norm(pastecart x y) <= norm(x :: real ^ _) + norm(y)"
1.784 -  unfolding real_vector_norm_def dot_pastecart real_sqrt_le_iff real_of_real_def id_def
1.785 +  unfolding real_vector_norm_def dot_pastecart real_sqrt_le_iff id_def
1.786    apply (rule power2_le_imp_le)
1.787    apply (simp add: real_sqrt_pow2[OF add_nonneg_nonneg[OF dot_pos_le[of x] dot_pos_le[of y]]])
1.788    apply (auto simp add: power2_eq_square ring_simps)
1.789 @@ -5007,7 +5178,7 @@
1.790      apply blast
1.791      by (rule abs_ge_zero)
1.792    from real_le_lsqrt[OF dot_pos_le th th1]
1.793 -  show ?thesis unfolding real_vector_norm_def  real_of_real_def id_def .
1.794 +  show ?thesis unfolding real_vector_norm_def id_def .
1.795  qed
1.796
1.797  (* Equality in Cauchy-Schwarz and triangle inequalities.                     *)
1.798 @@ -5015,10 +5186,10 @@
1.799  lemma norm_cauchy_schwarz_eq: "(x::real ^'n) \<bullet> y = norm x * norm y \<longleftrightarrow> norm x *s y = norm y *s x" (is "?lhs \<longleftrightarrow> ?rhs")
1.800  proof-
1.801    {assume h: "x = 0"
1.802 -    hence ?thesis by (simp add: norm_0)}
1.803 +    hence ?thesis by simp}
1.804    moreover
1.805    {assume h: "y = 0"
1.806 -    hence ?thesis by (simp add: norm_0)}
1.807 +    hence ?thesis by simp}
1.808    moreover
1.809    {assume x: "x \<noteq> 0" and y: "y \<noteq> 0"
1.810      from dot_eq_0[of "norm y *s x - norm x *s y"]
1.811 @@ -5032,7 +5203,7 @@
1.812      also have "\<dots> \<longleftrightarrow> (2 * norm x * norm y * (norm x * norm y - x \<bullet> y) = 0)" using x y
1.813        by (simp add: ring_simps dot_sym)
1.814      also have "\<dots> \<longleftrightarrow> ?lhs" using x y
1.815 -      apply (simp add: norm_eq_0)
1.816 +      apply simp
1.817        by metis
1.818      finally have ?thesis by blast}
1.819    ultimately show ?thesis by blast
1.820 @@ -5043,14 +5214,14 @@
1.821  proof-
1.822    have th: "\<And>(x::real) a. a \<ge> 0 \<Longrightarrow> abs x = a \<longleftrightarrow> x = a \<or> x = - a" by arith
1.823    have "?rhs \<longleftrightarrow> norm x *s y = norm y *s x \<or> norm (- x) *s y = norm y *s (- x)"
1.824 -    apply (simp add: norm_neg) by vector
1.825 +    apply simp by vector
1.826    also have "\<dots> \<longleftrightarrow>(x \<bullet> y = norm x * norm y \<or>
1.827       (-x) \<bullet> y = norm x * norm y)"
1.828      unfolding norm_cauchy_schwarz_eq[symmetric]
1.829 -    unfolding norm_neg
1.830 +    unfolding norm_minus_cancel
1.831        norm_mul by blast
1.832    also have "\<dots> \<longleftrightarrow> ?lhs"
1.833 -    unfolding th[OF mult_nonneg_nonneg, OF norm_pos_le[of x] norm_pos_le[of y]] dot_lneg
1.834 +    unfolding th[OF mult_nonneg_nonneg, OF norm_ge_zero[of x] norm_ge_zero[of y]] dot_lneg
1.835      by arith
1.836    finally show ?thesis ..
1.837  qed
1.838 @@ -5058,17 +5229,17 @@
1.839  lemma norm_triangle_eq: "norm(x + y) = norm x + norm y \<longleftrightarrow> norm x *s y = norm y *s x"
1.840  proof-
1.841    {assume x: "x =0 \<or> y =0"
1.842 -    hence ?thesis by (cases "x=0", simp_all add: norm_0)}
1.843 +    hence ?thesis by (cases "x=0", simp_all)}
1.844    moreover
1.845    {assume x: "x \<noteq> 0" and y: "y \<noteq> 0"
1.846      hence "norm x \<noteq> 0" "norm y \<noteq> 0"
1.847 -      by (simp_all add: norm_eq_0)
1.848 +      by simp_all
1.849      hence n: "norm x > 0" "norm y > 0"
1.850 -      using norm_pos_le[of x] norm_pos_le[of y]
1.851 +      using norm_ge_zero[of x] norm_ge_zero[of y]
1.852        by arith+
1.853      have th: "\<And>(a::real) b c. a + b + c \<noteq> 0 ==> (a = b + c \<longleftrightarrow> a^2 = (b + c)^2)" by algebra
1.854      have "norm(x + y) = norm x + norm y \<longleftrightarrow> norm(x + y)^ 2 = (norm x + norm y) ^2"
1.855 -      apply (rule th) using n norm_pos_le[of "x + y"]
1.856 +      apply (rule th) using n norm_ge_zero[of "x + y"]
1.857        by arith
1.858      also have "\<dots> \<longleftrightarrow> norm x *s y = norm y *s x"
1.859        unfolding norm_cauchy_schwarz_eq[symmetric]
1.860 @@ -5138,8 +5309,8 @@
1.861
1.862  lemma norm_cauchy_schwarz_equal: "abs(x \<bullet> y) = norm x * norm y \<longleftrightarrow> collinear {(0::real^'n),x,y}"
1.863  unfolding norm_cauchy_schwarz_abs_eq
1.864 -apply (cases "x=0", simp_all add: collinear_2 norm_0)
1.865 -apply (cases "y=0", simp_all add: collinear_2 norm_0 insert_commute)
1.866 +apply (cases "x=0", simp_all add: collinear_2)
1.867 +apply (cases "y=0", simp_all add: collinear_2 insert_commute)
1.868  unfolding collinear_lemma
1.869  apply simp
1.870  apply (subgoal_tac "norm x \<noteq> 0")
1.871 @@ -5164,8 +5335,8 @@
1.872  apply (simp add: ring_simps)
1.873  apply (case_tac "c <= 0", simp add: ring_simps)
1.874  apply (simp add: ring_simps)
1.875 -apply (simp add: norm_eq_0)
1.876 -apply (simp add: norm_eq_0)
1.877 +apply simp
1.878 +apply simp
1.879  done
1.880
1.881 -end
1.882 \ No newline at end of file
1.883 +end
```