remove simp add: norm_scaleR
authorhuffman
Fri Jun 12 12:00:30 2009 -0700 (2009-06-12)
changeset 31587a7e187205fc0
parent 31586 d4707b99e631
child 31588 2651f172c38b
remove simp add: norm_scaleR
src/HOL/Library/Convex_Euclidean_Space.thy
src/HOL/Library/Euclidean_Space.thy
src/HOL/Library/Product_Vector.thy
src/HOL/Library/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Library/Convex_Euclidean_Space.thy	Fri Jun 12 11:39:23 2009 -0700
     1.2 +++ b/src/HOL/Library/Convex_Euclidean_Space.thy	Fri Jun 12 12:00:30 2009 -0700
     1.3 @@ -573,7 +573,7 @@
     1.4            by (simp add: algebra_simps)
     1.5  	assume "\<bar>y - x\<bar> < e / norm (x1 - x2)"
     1.6  	hence "norm ((1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2)) < e"
     1.7 -	  unfolding * and scaleR_right_diff_distrib[THEN sym] and norm_scaleR 
     1.8 +	  unfolding * and scaleR_right_diff_distrib[THEN sym]
     1.9  	  unfolding less_divide_eq using n by auto  }
    1.10        hence "\<exists>d>0. \<forall>y. \<bar>y - x\<bar> < d \<longrightarrow> norm ((1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2)) < e"
    1.11  	apply(rule_tac x="e / norm (x1 - x2)" in exI) using as
    1.12 @@ -669,7 +669,7 @@
    1.13    hence *:"a - (u *\<^sub>R x + v *\<^sub>R y) = (u *\<^sub>R (a - x)) + (v *\<^sub>R (a - y))"
    1.14      by (auto simp add: algebra_simps)
    1.15    show "norm (a - (u *\<^sub>R x + v *\<^sub>R y)) \<le> u * norm (a - x) + v * norm (a - y)"
    1.16 -    unfolding * using norm_triangle_ineq[of "u *\<^sub>R (a - x)" "v *\<^sub>R (a - y)"] unfolding norm_scaleR
    1.17 +    unfolding * using norm_triangle_ineq[of "u *\<^sub>R (a - x)" "v *\<^sub>R (a - y)"]
    1.18      using `0 \<le> u` `0 \<le> v` by auto
    1.19  qed
    1.20  
    1.21 @@ -1694,7 +1694,7 @@
    1.22      hence "\<exists>x. norm x = 1 \<and> (\<forall>y\<in>c. 0 \<le> y \<bullet> x)" apply(rule_tac x="inverse(norm a) *\<^sub>R a" in exI)
    1.23         using hull_subset[of c convex] unfolding subset_eq and dot_rmult [where 'a=real, unfolded smult_conv_scaleR]
    1.24         apply- apply rule defer apply rule apply(rule mult_nonneg_nonneg)
    1.25 -       by(auto simp add: dot_sym norm_scaleR elim!: ballE) 
    1.26 +       by(auto simp add: dot_sym elim!: ballE)
    1.27      thus "frontier (cball 0 1) \<inter> \<Inter>f \<noteq> {}" unfolding c(1) frontier_cball dist_norm by auto
    1.28    qed(insert closed_halfspace_ge, auto)
    1.29    then obtain x where "norm x = 1" "\<forall>y\<in>s. x\<in>?k y" unfolding frontier_cball dist_norm by auto
    1.30 @@ -1934,11 +1934,11 @@
    1.31    have "norm x > 0" using assms(3)[unfolded zero_less_norm_iff[THEN sym]] by auto
    1.32    { fix v assume as:"v > u" "v *\<^sub>R x \<in> s"
    1.33      hence "v \<le> b / norm x" using b(2)[rule_format, OF as(2)] 
    1.34 -      using `u\<ge>0` unfolding pos_le_divide_eq[OF `norm x > 0`] and norm_scaleR by auto
    1.35 +      using `u\<ge>0` unfolding pos_le_divide_eq[OF `norm x > 0`] by auto
    1.36      hence "norm (v *\<^sub>R x) \<le> norm y" apply(rule_tac obt(6)[rule_format, unfolded dist_0_norm]) apply(rule IntI) defer 
    1.37        apply(rule as(2)) unfolding mem_Collect_eq apply(rule_tac x=v in exI) 
    1.38        using as(1) `u\<ge>0` by(auto simp add:field_simps) 
    1.39 -    hence False unfolding obt(3) unfolding norm_scaleR using `u\<ge>0` `norm x > 0` `v>u` by(auto simp add:field_simps)
    1.40 +    hence False unfolding obt(3) using `u\<ge>0` `norm x > 0` `v>u` by(auto simp add:field_simps)
    1.41    } note u_max = this
    1.42  
    1.43    have "u *\<^sub>R x \<in> frontier s" unfolding frontier_straddle apply(rule,rule,rule) apply(rule_tac x="u *\<^sub>R x" in bexI) unfolding obt(3)[THEN sym]
    1.44 @@ -1946,7 +1946,7 @@
    1.45      fix e  assume "0 < e" and as:"(u + e / 2 / norm x) *\<^sub>R x \<in> s"
    1.46      hence "u + e / 2 / norm x > u" using`norm x > 0` by(auto simp del:zero_less_norm_iff intro!: divide_pos_pos)
    1.47      thus False using u_max[OF _ as] by auto
    1.48 -  qed(insert `y\<in>s`, auto simp add: dist_norm scaleR_left_distrib obt(3) norm_scaleR)
    1.49 +  qed(insert `y\<in>s`, auto simp add: dist_norm scaleR_left_distrib obt(3))
    1.50    thus ?thesis apply(rule_tac that[of u]) apply(rule obt(1), assumption)
    1.51      apply(rule,rule,rule ccontr) apply(rule u_max) by auto qed
    1.52  
    1.53 @@ -1959,7 +1959,7 @@
    1.54    def pi \<equiv> "\<lambda>x::real^'n. inverse (norm x) *\<^sub>R x"
    1.55    have "0 \<notin> frontier s" unfolding frontier_straddle apply(rule ccontr) unfolding not_not apply(erule_tac x=1 in allE)
    1.56      using assms(2)[unfolded subset_eq Ball_def mem_cball] by auto
    1.57 -  have injpi:"\<And>x y. pi x = pi y \<and> norm x = norm y \<longleftrightarrow> x = y" unfolding pi_def by (auto simp add: scaleR_cancel_left)
    1.58 +  have injpi:"\<And>x y. pi x = pi y \<and> norm x = norm y \<longleftrightarrow> x = y" unfolding pi_def by auto
    1.59  
    1.60    have contpi:"continuous_on (UNIV - {0}) pi" apply(rule continuous_at_imp_continuous_on)
    1.61      apply rule unfolding pi_def
    1.62 @@ -1970,7 +1970,7 @@
    1.63      apply (rule continuous_at_id)
    1.64      done
    1.65    def sphere \<equiv> "{x::real^'n. norm x = 1}"
    1.66 -  have pi:"\<And>x. x \<noteq> 0 \<Longrightarrow> pi x \<in> sphere" "\<And>x u. u>0 \<Longrightarrow> pi (u *\<^sub>R x) = pi x" unfolding pi_def sphere_def by (auto simp add: norm_scaleR scaleR_cancel_right)
    1.67 +  have pi:"\<And>x. x \<noteq> 0 \<Longrightarrow> pi x \<in> sphere" "\<And>x u. u>0 \<Longrightarrow> pi (u *\<^sub>R x) = pi x" unfolding pi_def sphere_def by auto
    1.68  
    1.69    have "0\<in>s" using assms(2) and centre_in_cball[of 0 1] by auto
    1.70    have front_smul:"\<forall>x\<in>frontier s. \<forall>u\<ge>0. u *\<^sub>R x \<in> s \<longleftrightarrow> u \<le> 1" proof(rule,rule,rule)
    1.71 @@ -1995,7 +1995,7 @@
    1.72    next fix x assume "x\<in>sphere" hence "norm x = 1" "x\<noteq>0" unfolding sphere_def by auto
    1.73      then obtain u where "0 \<le> u" "u *\<^sub>R x \<in> frontier s" "\<forall>v>u. v *\<^sub>R x \<notin> s"
    1.74        using compact_frontier_line_lemma[OF assms(1) `0\<in>s`, of x] by auto
    1.75 -    thus "x \<in> pi ` frontier s" unfolding image_iff le_less pi_def apply(rule_tac x="u *\<^sub>R x" in bexI) using `norm x = 1` `0\<notin>frontier s` by (auto simp add: norm_scaleR)
    1.76 +    thus "x \<in> pi ` frontier s" unfolding image_iff le_less pi_def apply(rule_tac x="u *\<^sub>R x" in bexI) using `norm x = 1` `0\<notin>frontier s` by auto
    1.77    next fix x y assume as:"x \<in> frontier s" "y \<in> frontier s" "pi x = pi y"
    1.78      hence xys:"x\<in>s" "y\<in>s" using fs by auto
    1.79      from as(1,2) have nor:"norm x \<noteq> 0" "norm y \<noteq> 0" using `0\<notin>frontier s` by auto 
    1.80 @@ -2042,9 +2042,9 @@
    1.81        moreover have "surf (pi x) \<in> frontier s" using surf(5) pix by auto
    1.82        hence "dist 0 (inverse (norm (surf (pi x))) *\<^sub>R x) \<le> 1" unfolding dist_norm
    1.83  	using ** and * using front_smul[THEN bspec[where x="surf (pi x)"], THEN spec[where x="norm x * ?a"]]
    1.84 -	using False `x\<in>s` by(auto simp add:field_simps norm_scaleR)
    1.85 +	using False `x\<in>s` by(auto simp add:field_simps)
    1.86        ultimately show ?thesis unfolding image_iff apply(rule_tac x="inverse (norm (surf(pi x))) *\<^sub>R x" in bexI)
    1.87 -	apply(subst injpi[THEN sym]) unfolding norm_scaleR abs_mult abs_norm_cancel abs_of_pos[OF `?a > 0`]
    1.88 +	apply(subst injpi[THEN sym]) unfolding abs_mult abs_norm_cancel abs_of_pos[OF `?a > 0`]
    1.89  	unfolding pi(2)[OF `?a > 0`] by auto
    1.90      qed } note hom2 = this
    1.91  
    1.92 @@ -2085,7 +2085,7 @@
    1.93  	  using pi(2)[of "norm x" "surf (pi x)"] pi(2)[of "norm y" "surf (pi y)"] by auto
    1.94  	moreover have "pi x \<in> sphere" "pi y \<in> sphere" using pi(1) False by auto
    1.95  	ultimately have *:"pi x = pi y" using surf(4)[THEN bspec[where x="pi x"]] surf(4)[THEN bspec[where x="pi y"]] by auto 
    1.96 -	moreover have "norm x = norm y" using as(3)[unfolded *] using False by(auto dest:surf_0 simp add: scaleR_cancel_right)
    1.97 +	moreover have "norm x = norm y" using as(3)[unfolded *] using False by(auto dest:surf_0)
    1.98  	ultimately show ?thesis using injpi by auto qed qed
    1.99    qed auto qed
   1.100  
   1.101 @@ -2100,7 +2100,7 @@
   1.102      fix y assume "dist (u *\<^sub>R x) y < 1 - u"
   1.103      hence "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> s"
   1.104        using assms(3) apply(erule_tac subsetD) unfolding mem_cball dist_commute dist_norm
   1.105 -      unfolding group_add_class.diff_0 group_add_class.diff_0_right norm_minus_cancel norm_scaleR      
   1.106 +      unfolding group_add_class.diff_0 group_add_class.diff_0_right norm_minus_cancel norm_scaleR
   1.107        apply (rule mult_left_le_imp_le[of "1 - u"])
   1.108        unfolding class_semiring.mul_a using `u<1` by auto
   1.109      thus "y \<in> s" using assms(1)[unfolded convex_def, rule_format, of "inverse(1 - u) *\<^sub>R (y - u *\<^sub>R x)" x "1 - u" u]
   1.110 @@ -2116,7 +2116,7 @@
   1.111    have "cball ?n 1 \<subseteq> (\<lambda>x. inverse d *\<^sub>R (x - a)) ` s"
   1.112      apply(rule, rule_tac x="d *\<^sub>R x + a" in image_eqI) defer
   1.113      apply(rule d[unfolded subset_eq, rule_format]) using `d>0` unfolding mem_cball dist_norm
   1.114 -    by(auto simp add: mult_right_le_one_le norm_scaleR)
   1.115 +    by(auto simp add: mult_right_le_one_le)
   1.116    hence "(\<lambda>x. inverse d *\<^sub>R (x - a)) ` s homeomorphic cball ?n 1"
   1.117      using homeomorphic_convex_compact_lemma[of "(\<lambda>x. ?d *\<^sub>R -a + ?d *\<^sub>R x) ` s", OF convex_affinity compact_affinity]
   1.118      using assms(1,2) by(auto simp add: uminus_add_conv_diff scaleR_right_diff_distrib)
   1.119 @@ -2387,9 +2387,9 @@
   1.120  	apply(rule order_trans[of _ "2 * norm (x - y)"]) using as by(auto simp add: field_simps norm_minus_commute) 
   1.121        { def w \<equiv> "x + t *\<^sub>R (y - x)"
   1.122  	have "w\<in>s" unfolding w_def apply(rule k[unfolded subset_eq,rule_format]) unfolding mem_cball dist_norm 
   1.123 -	  unfolding t_def using `k>0` by(auto simp add: norm_scaleR simp del: scaleR_right_diff_distrib) 
   1.124 +	  unfolding t_def using `k>0` by auto
   1.125  	have "(1 / t) *\<^sub>R x + - x + ((t - 1) / t) *\<^sub>R x = (1 / t - 1 + (t - 1) / t) *\<^sub>R x" by (auto simp add: algebra_simps)
   1.126 -	also have "\<dots> = 0"  using `t>0` by(auto simp add:field_simps simp del:scaleR_left_distrib)
   1.127 +	also have "\<dots> = 0"  using `t>0` by(auto simp add:field_simps)
   1.128  	finally have w:"(1 / t) *\<^sub>R w + ((t - 1) / t) *\<^sub>R x = y" unfolding w_def using False and `t>0` by (auto simp add: algebra_simps)
   1.129  	have  "2 * B < e * t" unfolding t_def using `0<e` `0<k` `B>0` and as and False by (auto simp add:field_simps) 
   1.130  	hence "(f w - f x) / t < e"
   1.131 @@ -2400,9 +2400,9 @@
   1.132        moreover 
   1.133        { def w \<equiv> "x - t *\<^sub>R (y - x)"
   1.134  	have "w\<in>s" unfolding w_def apply(rule k[unfolded subset_eq,rule_format]) unfolding mem_cball dist_norm 
   1.135 -	  unfolding t_def using `k>0` by(auto simp add: norm_scaleR simp del: scaleR_right_diff_distrib) 
   1.136 +	  unfolding t_def using `k>0` by auto
   1.137  	have "(1 / (1 + t)) *\<^sub>R x + (t / (1 + t)) *\<^sub>R x = (1 / (1 + t) + t / (1 + t)) *\<^sub>R x" by (auto simp add: algebra_simps)
   1.138 -	also have "\<dots>=x" using `t>0` by (auto simp add:field_simps simp del:scaleR_left_distrib)
   1.139 +	also have "\<dots>=x" using `t>0` by (auto simp add:field_simps)
   1.140  	finally have w:"(1 / (1+t)) *\<^sub>R w + (t / (1 + t)) *\<^sub>R y = x" unfolding w_def using False and `t>0` by (auto simp add: algebra_simps)
   1.141  	have  "2 * B < e * t" unfolding t_def using `0<e` `0<k` `B>0` and as and False by (auto simp add:field_simps) 
   1.142  	hence *:"(f w - f y) / t < e" using B(2)[OF `w\<in>s`] and B(2)[OF `y\<in>s`] using `t>0` by(auto simp add:field_simps) 
   1.143 @@ -2503,8 +2503,8 @@
   1.144    "dist (midpoint a b) a = (dist a b) / 2" (is ?t3)
   1.145    "dist (midpoint a b) b = (dist a b) / 2" (is ?t4)
   1.146  proof-
   1.147 -  have *: "\<And>x y::real^'n::finite. 2 *\<^sub>R x = - y \<Longrightarrow> norm x = (norm y) / 2" unfolding equation_minus_iff by (auto simp add: norm_scaleR)
   1.148 -  have **:"\<And>x y::real^'n::finite. 2 *\<^sub>R x =   y \<Longrightarrow> norm x = (norm y) / 2" by (auto simp add: norm_scaleR)
   1.149 +  have *: "\<And>x y::real^'n::finite. 2 *\<^sub>R x = - y \<Longrightarrow> norm x = (norm y) / 2" unfolding equation_minus_iff by auto
   1.150 +  have **:"\<And>x y::real^'n::finite. 2 *\<^sub>R x =   y \<Longrightarrow> norm x = (norm y) / 2" by auto
   1.151    note scaleR_right_distrib [simp]
   1.152    show ?t1 unfolding midpoint_def dist_norm apply (rule **) by(auto,vector)
   1.153    show ?t2 unfolding midpoint_def dist_norm apply (rule *)  by(auto,vector)
   1.154 @@ -2569,7 +2569,7 @@
   1.155        hence *:"a - x = u *\<^sub>R (a - b)" "x - b = (1 - u) *\<^sub>R (a - b)"
   1.156  	unfolding as(1) by(auto simp add:algebra_simps)
   1.157        show "norm (a - x) *\<^sub>R (x - b) = norm (x - b) *\<^sub>R (a - x)"
   1.158 -	unfolding norm_minus_commute[of x a] * norm_scaleR Cart_eq using as(2,3)
   1.159 +	unfolding norm_minus_commute[of x a] * Cart_eq using as(2,3)
   1.160  	by(auto simp add: vector_component_simps field_simps)
   1.161      next assume as:"dist a b = dist a x + dist x b"
   1.162        have "norm (a - x) / norm (a - b) \<le> 1" unfolding divide_le_eq_1_pos[OF Fal2] unfolding as[unfolded dist_norm] norm_ge_zero by auto 
   1.163 @@ -2587,7 +2587,7 @@
   1.164  lemma between_midpoint: fixes a::"real^'n::finite" shows
   1.165    "between (a,b) (midpoint a b)" (is ?t1) 
   1.166    "between (b,a) (midpoint a b)" (is ?t2)
   1.167 -proof- have *:"\<And>x y z. x = (1/2::real) *\<^sub>R z \<Longrightarrow> y = (1/2) *\<^sub>R z \<Longrightarrow> norm z = norm x + norm y" by (auto simp add: norm_scaleR)
   1.168 +proof- have *:"\<And>x y z. x = (1/2::real) *\<^sub>R z \<Longrightarrow> y = (1/2) *\<^sub>R z \<Longrightarrow> norm z = norm x + norm y" by auto
   1.169    show ?t1 ?t2 unfolding between midpoint_def dist_norm apply(rule_tac[!] *)
   1.170      by(auto simp add:field_simps Cart_eq vector_component_simps) qed
   1.171  
   1.172 @@ -2636,7 +2636,7 @@
   1.173    have *:"x - e *\<^sub>R (x - c) = y - e *\<^sub>R (y - z)" unfolding z_def using `e>0` by (auto simp add: scaleR_right_diff_distrib scaleR_right_distrib scaleR_left_diff_distrib)
   1.174    have "z\<in>interior s" apply(rule subset_interior[OF d,unfolded subset_eq,rule_format])
   1.175      unfolding interior_open[OF open_ball] mem_ball z_def dist_norm using y and assms(4,5)
   1.176 -    by(auto simp del:scaleR_right_diff_distrib simp add:field_simps norm_minus_commute norm_scaleR)
   1.177 +    by(auto simp add:field_simps norm_minus_commute)
   1.178    thus ?thesis unfolding * apply - apply(rule mem_interior_convex_shrink) 
   1.179      using assms(1,4-5) `y\<in>s` by auto qed
   1.180  
   1.181 @@ -2678,10 +2678,10 @@
   1.182    fix x::"real^'n" and e assume "0<e" and as:"\<forall>xa. dist x xa < e \<longrightarrow> (\<forall>x. 0 \<le> xa $ x) \<and> setsum (op $ xa) UNIV \<le> 1"
   1.183    show "(\<forall>xa. 0 < x $ xa) \<and> setsum (op $ x) UNIV < 1" apply(rule,rule) proof-
   1.184      fix i::'n show "0 < x $ i" using as[THEN spec[where x="x - (e / 2) *\<^sub>R basis i"]] and `e>0`
   1.185 -      unfolding dist_norm by(auto simp add: norm_basis vector_component_simps basis_component norm_scaleR elim:allE[where x=i])
   1.186 +      unfolding dist_norm by(auto simp add: norm_basis vector_component_simps basis_component elim:allE[where x=i])
   1.187    next guess a using UNIV_witness[where 'a='n] ..
   1.188      have **:"dist x (x + (e / 2) *\<^sub>R basis a) < e" using  `e>0` and norm_basis[of a]
   1.189 -      unfolding dist_norm by(auto simp add: vector_component_simps basis_component norm_scaleR intro!: mult_strict_left_mono_comm)
   1.190 +      unfolding dist_norm by(auto simp add: vector_component_simps basis_component intro!: mult_strict_left_mono_comm)
   1.191      have "\<And>i. (x + (e / 2) *\<^sub>R basis a) $ i = x$i + (if i = a then e/2 else 0)" by(auto simp add:vector_component_simps)
   1.192      hence *:"setsum (op $ (x + (e / 2) *\<^sub>R basis a)) UNIV = setsum (\<lambda>i. x$i + (if a = i then e/2 else 0)) UNIV" by(rule_tac setsum_cong, auto) 
   1.193      have "setsum (op $ x) UNIV < setsum (op $ (x + (e / 2) *\<^sub>R basis a)) UNIV" unfolding * setsum_addf
   1.194 @@ -2892,12 +2892,12 @@
   1.195      hence "g1 (2 *\<^sub>R x) = g1 (2 *\<^sub>R y)" using xy(3) unfolding joinpaths_def dest_vec1_def by auto
   1.196      moreover have "2 *\<^sub>R x \<in> {0..1}" "2 *\<^sub>R y \<in> {0..1}" using xy(1,2) as
   1.197        unfolding mem_interval_1 dest_vec1_def by(auto simp add:vector_component_simps)
   1.198 -    ultimately show ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] by (auto simp add: scaleR_cancel_left)
   1.199 +    ultimately show ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] by auto
   1.200    next assume as:"x $ 1 > 1 / 2" "y $ 1 > 1 / 2"
   1.201      hence "g2 (2 *\<^sub>R x - 1) = g2 (2 *\<^sub>R y - 1)" using xy(3) unfolding joinpaths_def dest_vec1_def by auto
   1.202      moreover have "2 *\<^sub>R x - 1 \<in> {0..1}" "2 *\<^sub>R y - 1 \<in> {0..1}" using xy(1,2) as
   1.203        unfolding mem_interval_1 dest_vec1_def by(auto simp add:vector_component_simps)
   1.204 -    ultimately show ?thesis using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] by (auto simp add: scaleR_cancel_left)
   1.205 +    ultimately show ?thesis using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] by auto
   1.206    next assume as:"x $ 1 \<le> 1 / 2" "y $ 1 > 1 / 2"
   1.207      hence "?g x \<in> path_image g1" "?g y \<in> path_image g2" unfolding path_image_def joinpaths_def
   1.208        using xy(1,2)[unfolded mem_interval_1] by(auto simp add:vector_component_simps intro!: imageI)
   1.209 @@ -2934,9 +2934,9 @@
   1.210    fix x y assume xy:"x \<in> {0..1}" "y \<in> {0..1}" "(g1 +++ g2) x = (g1 +++ g2) y"
   1.211    show "x = y" proof(cases "x$1 \<le> 1/2", case_tac[!] "y$1 \<le> 1/2", unfold not_le)
   1.212      assume "x $ 1 \<le> 1 / 2" "y $ 1 \<le> 1 / 2" thus ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] and xy
   1.213 -      unfolding mem_interval_1 joinpaths_def by(auto simp add:vector_component_simps scaleR_cancel_left)
   1.214 +      unfolding mem_interval_1 joinpaths_def by(auto simp add:vector_component_simps)
   1.215    next assume "x $ 1 > 1 / 2" "y $ 1 > 1 / 2" thus ?thesis using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] and xy
   1.216 -      unfolding mem_interval_1 joinpaths_def by(auto simp add:vector_component_simps scaleR_cancel_left)
   1.217 +      unfolding mem_interval_1 joinpaths_def by(auto simp add:vector_component_simps)
   1.218    next assume as:"x $ 1 \<le> 1 / 2" "y $ 1 > 1 / 2" 
   1.219      hence "?g x \<in> path_image g1" "?g y \<in> path_image g2" unfolding path_image_def joinpaths_def
   1.220        using xy(1,2)[unfolded mem_interval_1] by(auto simp add:vector_component_simps intro!: imageI)
   1.221 @@ -3248,10 +3248,10 @@
   1.222      thus ?thesis using path_connected_empty by auto
   1.223    qed(auto intro!:path_connected_singleton) next
   1.224    case False hence *:"{x::real^'n. norm(x - a) = r} = (\<lambda>x. a + r *\<^sub>R x) ` {x. norm x = 1}" unfolding not_le apply -apply(rule set_ext,rule)
   1.225 -    unfolding image_iff apply(rule_tac x="(1/r) *\<^sub>R (x - a)" in bexI) unfolding mem_Collect_eq norm_scaleR by (auto simp add: scaleR_right_diff_distrib norm_scaleR)
   1.226 +    unfolding image_iff apply(rule_tac x="(1/r) *\<^sub>R (x - a)" in bexI) unfolding mem_Collect_eq norm_scaleR by (auto simp add: scaleR_right_diff_distrib)
   1.227    have ***:"\<And>xa. (if xa = 0 then 0 else 1) \<noteq> 1 \<Longrightarrow> xa = 0" apply(rule ccontr) by auto
   1.228    have **:"{x::real^'n. norm x = 1} = (\<lambda>x. (1/norm x) *\<^sub>R x) ` (UNIV - {0})" apply(rule set_ext,rule)
   1.229 -    unfolding image_iff apply(rule_tac x=x in bexI) unfolding mem_Collect_eq norm_scaleR by(auto intro!: *** simp add: norm_scaleR)
   1.230 +    unfolding image_iff apply(rule_tac x=x in bexI) unfolding mem_Collect_eq by(auto intro!: ***)
   1.231    have "continuous_on (UNIV - {0}) (\<lambda>x::real^'n. 1 / norm x)" unfolding o_def continuous_on_eq_continuous_within
   1.232      apply(rule, rule continuous_at_within_inv[unfolded o_def inverse_eq_divide]) apply(rule continuous_at_within)
   1.233      apply(rule continuous_at_norm[unfolded o_def]) by auto
     2.1 --- a/src/HOL/Library/Euclidean_Space.thy	Fri Jun 12 11:39:23 2009 -0700
     2.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Fri Jun 12 12:00:30 2009 -0700
     2.3 @@ -771,7 +771,7 @@
     2.4      done
     2.5    show "norm (scaleR a x) = \<bar>a\<bar> * norm x"
     2.6      unfolding vector_norm_def
     2.7 -    by (simp add: norm_scaleR setL2_right_distrib)
     2.8 +    by (simp add: setL2_right_distrib)
     2.9    show "sgn x = scaleR (inverse (norm x)) x"
    2.10      by (rule vector_sgn_def)
    2.11    show "dist x y = norm (x - y)"
     3.1 --- a/src/HOL/Library/Product_Vector.thy	Fri Jun 12 11:39:23 2009 -0700
     3.2 +++ b/src/HOL/Library/Product_Vector.thy	Fri Jun 12 12:00:30 2009 -0700
     3.3 @@ -347,7 +347,7 @@
     3.4      done
     3.5    show "norm (scaleR r x) = \<bar>r\<bar> * norm x"
     3.6      unfolding norm_prod_def
     3.7 -    apply (simp add: norm_scaleR power_mult_distrib)
     3.8 +    apply (simp add: power_mult_distrib)
     3.9      apply (simp add: right_distrib [symmetric])
    3.10      apply (simp add: real_sqrt_mult_distrib)
    3.11      done
     4.1 --- a/src/HOL/Library/Topology_Euclidean_Space.thy	Fri Jun 12 11:39:23 2009 -0700
     4.2 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Fri Jun 12 12:00:30 2009 -0700
     4.3 @@ -1031,7 +1031,7 @@
     4.4    unfolding trivial_limit_def Rep_net_at_infinity
     4.5    apply (clarsimp simp add: expand_set_eq)
     4.6    apply (drule_tac x="scaleR r (sgn 1)" in spec)
     4.7 -  apply (simp add: norm_scaleR norm_sgn)
     4.8 +  apply (simp add: norm_sgn)
     4.9    done
    4.10  
    4.11  lemma trivial_limit_sequentially: "\<not> trivial_limit sequentially"
    4.12 @@ -1757,7 +1757,7 @@
    4.13  	also have "\<dots> = \<bar>- 1 + d / (2 * norm (x - y))\<bar> * norm (x - y)"
    4.14  	  using scaleR_left_distrib[of "- 1" "d / (2 * norm (y - x))", THEN sym, of "y - x"]
    4.15  	  unfolding scaleR_minus_left scaleR_one
    4.16 -	  by (auto simp add: norm_minus_commute norm_scaleR)
    4.17 +	  by (auto simp add: norm_minus_commute)
    4.18  	also have "\<dots> = \<bar>- norm (x - y) + d / 2\<bar>"
    4.19  	  unfolding abs_mult_pos[of "norm (x - y)", OF norm_ge_zero[of "x - y"]]
    4.20  	  unfolding real_add_mult_distrib using `x\<noteq>y`[unfolded dist_nz, unfolded dist_norm] by auto
    4.21 @@ -1769,7 +1769,7 @@
    4.22  	have "(d / (2*dist y x)) *\<^sub>R (y - x) \<noteq> 0"
    4.23  	  using `x\<noteq>y`[unfolded dist_nz] `d>0` unfolding scaleR_eq_0_iff by (auto simp add: dist_commute)
    4.24  	moreover
    4.25 -	have "dist (y - (d / (2 * dist y x)) *\<^sub>R (y - x)) y < d" unfolding dist_norm apply simp unfolding norm_minus_cancel norm_scaleR
    4.26 +	have "dist (y - (d / (2 * dist y x)) *\<^sub>R (y - x)) y < d" unfolding dist_norm apply simp unfolding norm_minus_cancel
    4.27  	  using `d>0` `x\<noteq>y`[unfolded dist_nz] dist_commute[of x y]
    4.28  	  unfolding dist_norm by auto
    4.29  	ultimately show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d" by (rule_tac  x="y - (d / (2*dist y x)) *\<^sub>R (y - x)" in bexI) auto
    4.30 @@ -1808,11 +1808,11 @@
    4.31      unfolding z_def by (simp add: algebra_simps)
    4.32    have "dist z y < r"
    4.33      unfolding z_def k_def using `0 < r`
    4.34 -    by (simp add: dist_norm norm_scaleR min_def)
    4.35 +    by (simp add: dist_norm min_def)
    4.36    hence "z \<in> T" using `\<forall>z. dist z y < r \<longrightarrow> z \<in> T` by simp
    4.37    have "dist x z < dist x y"
    4.38      unfolding z_def2 dist_norm
    4.39 -    apply (simp add: norm_scaleR norm_minus_commute)
    4.40 +    apply (simp add: norm_minus_commute)
    4.41      apply (simp only: dist_norm [symmetric])
    4.42      apply (subgoal_tac "\<bar>1 - k\<bar> * dist x y < 1 * dist x y", simp)
    4.43      apply (rule mult_strict_right_mono)
    4.44 @@ -1875,7 +1875,7 @@
    4.45      next
    4.46        case False
    4.47        have "dist (y + (d / 2 / dist y x) *\<^sub>R (y - x)) y < d" unfolding dist_norm
    4.48 -	using `d>0` norm_ge_zero[of "y - x"] `x \<noteq> y` by (auto simp add: norm_scaleR)
    4.49 +	using `d>0` norm_ge_zero[of "y - x"] `x \<noteq> y` by auto
    4.50        hence *:"y + (d / 2 / dist y x) *\<^sub>R (y - x) \<in> cball x e" using d as(1)[unfolded subset_eq] by blast
    4.51        have "y - x \<noteq> 0" using `x \<noteq> y` by auto
    4.52        hence **:"d / (2 * norm (y - x)) > 0" unfolding zero_less_norm_iff[THEN sym]
    4.53 @@ -1886,7 +1886,7 @@
    4.54        also have "\<dots> = norm ((1 + d / (2 * norm (y - x))) *\<^sub>R (y - x))"
    4.55          by (auto simp add: algebra_simps)
    4.56        also have "\<dots> = \<bar>1 + d / (2 * norm (y - x))\<bar> * norm (y - x)"
    4.57 -        using ** by (auto simp add: norm_scaleR)
    4.58 +        using ** by auto
    4.59        also have "\<dots> = (dist y x) + d/2"using ** by (auto simp add: left_distrib dist_norm)
    4.60        finally have "e \<ge> dist x y +d/2" using *[unfolded mem_cball] by (auto simp add: dist_commute)
    4.61        thus "y \<in> ball x e" unfolding mem_ball using `d>0` by auto
    4.62 @@ -2073,7 +2073,7 @@
    4.63    fix b::real  assume b: "b >0"
    4.64    have b1: "b +1 \<ge> 0" using b by simp
    4.65    with `x \<noteq> 0` have "b < norm (scaleR (b + 1) (sgn x))"
    4.66 -    by (simp add: norm_scaleR norm_sgn)
    4.67 +    by (simp add: norm_sgn)
    4.68    then show "\<exists>x::'a. b < norm x" ..
    4.69  qed
    4.70  
    4.71 @@ -4514,7 +4514,7 @@
    4.72  	then obtain N where "\<forall>n\<ge>N. dist (x n) l < e * \<bar>c\<bar>"
    4.73            using as(2)[unfolded Lim_sequentially, THEN spec[where x="e * abs c"]] by auto
    4.74  	hence "\<exists>N. \<forall>n\<ge>N. dist (scaleR (1 / c) (x n)) (scaleR (1 / c) l) < e"
    4.75 -          unfolding dist_norm unfolding scaleR_right_diff_distrib[THEN sym] norm_scaleR
    4.76 +          unfolding dist_norm unfolding scaleR_right_diff_distrib[THEN sym]
    4.77  	  using mult_imp_div_pos_less[of "abs c" _ e] `c\<noteq>0` by auto  }
    4.78        hence "((\<lambda>n. scaleR (1 / c) (x n)) ---> scaleR (1 / c) l) sequentially" unfolding Lim_sequentially by auto
    4.79        ultimately have "l \<in> scaleR c ` s"
    4.80 @@ -4888,7 +4888,7 @@
    4.81        have "dist (x - (e / 2) *\<^sub>R basis i) x < e"
    4.82  	   "dist (x + (e / 2) *\<^sub>R basis i) x < e"
    4.83  	unfolding dist_norm apply auto
    4.84 -	unfolding norm_minus_cancel and norm_scaleR using norm_basis[of i] and `e>0` by auto
    4.85 +	unfolding norm_minus_cancel using norm_basis[of i] and `e>0` by auto
    4.86        hence "a $ i \<le> (x - (e / 2) *\<^sub>R basis i) $ i"
    4.87                      "(x + (e / 2) *\<^sub>R basis i) $ i \<le> b $ i"
    4.88  	using e[THEN spec[where x="x - (e/2) *\<^sub>R basis i"]]
    4.89 @@ -5485,7 +5485,7 @@
    4.90      apply(rule_tac x="\<lambda>x. a + (d/e) *\<^sub>R (x - b)" in exI)
    4.91      using assms apply (auto simp add: dist_commute)
    4.92      unfolding dist_norm
    4.93 -    apply (auto simp add: norm_scaleR pos_divide_less_eq mult_strict_left_mono)
    4.94 +    apply (auto simp add: pos_divide_less_eq mult_strict_left_mono)
    4.95      unfolding continuous_on
    4.96      by (intro ballI tendsto_intros, simp, assumption)+
    4.97  next
    4.98 @@ -5495,7 +5495,7 @@
    4.99      apply(rule_tac x="\<lambda>x. a + (d/e) *\<^sub>R (x - b)" in exI)
   4.100      using assms apply (auto simp add: dist_commute)
   4.101      unfolding dist_norm
   4.102 -    apply (auto simp add: norm_scaleR pos_divide_le_eq)
   4.103 +    apply (auto simp add: pos_divide_le_eq)
   4.104      unfolding continuous_on
   4.105      by (intro ballI tendsto_intros, simp, assumption)+
   4.106  qed
   4.107 @@ -5586,9 +5586,9 @@
   4.108        case False
   4.109        hence *:"0 < norm a / norm x" using `a\<noteq>0` unfolding zero_less_norm_iff[THEN sym] by(simp only: divide_pos_pos)
   4.110        have "\<forall>c. \<forall>x\<in>s. c *\<^sub>R x \<in> s" using s[unfolded subspace_def smult_conv_scaleR] by auto
   4.111 -      hence "(norm a / norm x) *\<^sub>R x \<in> {x \<in> s. norm x = norm a}" using `x\<in>s` and `x\<noteq>0` by (auto simp add: norm_scaleR)
   4.112 +      hence "(norm a / norm x) *\<^sub>R x \<in> {x \<in> s. norm x = norm a}" using `x\<in>s` and `x\<noteq>0` by auto
   4.113        thus "norm (f b) / norm b * norm x \<le> norm (f x)" using b[THEN bspec[where x="(norm a / norm x) *\<^sub>R x"]]
   4.114 -	unfolding linear_cmul[OF f(1), unfolded smult_conv_scaleR] and norm_scaleR and ba using `x\<noteq>0` `a\<noteq>0`
   4.115 +	unfolding linear_cmul[OF f(1), unfolded smult_conv_scaleR] and ba using `x\<noteq>0` `a\<noteq>0`
   4.116  	by (auto simp add: real_mult_commute pos_le_divide_eq pos_divide_le_eq)
   4.117      qed }
   4.118    ultimately