--- a/src/HOL/Library/Convex_Euclidean_Space.thy Fri Jun 12 11:39:23 2009 -0700
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy Fri Jun 12 12:00:30 2009 -0700
@@ -573,7 +573,7 @@
by (simp add: algebra_simps)
assume "\<bar>y - x\<bar> < e / norm (x1 - x2)"
hence "norm ((1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2)) < e"
- unfolding * and scaleR_right_diff_distrib[THEN sym] and norm_scaleR
+ unfolding * and scaleR_right_diff_distrib[THEN sym]
unfolding less_divide_eq using n by auto }
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"
apply(rule_tac x="e / norm (x1 - x2)" in exI) using as
@@ -669,7 +669,7 @@
hence *:"a - (u *\<^sub>R x + v *\<^sub>R y) = (u *\<^sub>R (a - x)) + (v *\<^sub>R (a - y))"
by (auto simp add: algebra_simps)
show "norm (a - (u *\<^sub>R x + v *\<^sub>R y)) \<le> u * norm (a - x) + v * norm (a - y)"
- unfolding * using norm_triangle_ineq[of "u *\<^sub>R (a - x)" "v *\<^sub>R (a - y)"] unfolding norm_scaleR
+ unfolding * using norm_triangle_ineq[of "u *\<^sub>R (a - x)" "v *\<^sub>R (a - y)"]
using `0 \<le> u` `0 \<le> v` by auto
qed
@@ -1694,7 +1694,7 @@
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)
using hull_subset[of c convex] unfolding subset_eq and dot_rmult [where 'a=real, unfolded smult_conv_scaleR]
apply- apply rule defer apply rule apply(rule mult_nonneg_nonneg)
- by(auto simp add: dot_sym norm_scaleR elim!: ballE)
+ by(auto simp add: dot_sym elim!: ballE)
thus "frontier (cball 0 1) \<inter> \<Inter>f \<noteq> {}" unfolding c(1) frontier_cball dist_norm by auto
qed(insert closed_halfspace_ge, auto)
then obtain x where "norm x = 1" "\<forall>y\<in>s. x\<in>?k y" unfolding frontier_cball dist_norm by auto
@@ -1934,11 +1934,11 @@
have "norm x > 0" using assms(3)[unfolded zero_less_norm_iff[THEN sym]] by auto
{ fix v assume as:"v > u" "v *\<^sub>R x \<in> s"
hence "v \<le> b / norm x" using b(2)[rule_format, OF as(2)]
- using `u\<ge>0` unfolding pos_le_divide_eq[OF `norm x > 0`] and norm_scaleR by auto
+ using `u\<ge>0` unfolding pos_le_divide_eq[OF `norm x > 0`] by auto
hence "norm (v *\<^sub>R x) \<le> norm y" apply(rule_tac obt(6)[rule_format, unfolded dist_0_norm]) apply(rule IntI) defer
apply(rule as(2)) unfolding mem_Collect_eq apply(rule_tac x=v in exI)
using as(1) `u\<ge>0` by(auto simp add:field_simps)
- hence False unfolding obt(3) unfolding norm_scaleR using `u\<ge>0` `norm x > 0` `v>u` by(auto simp add:field_simps)
+ hence False unfolding obt(3) using `u\<ge>0` `norm x > 0` `v>u` by(auto simp add:field_simps)
} note u_max = this
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]
@@ -1946,7 +1946,7 @@
fix e assume "0 < e" and as:"(u + e / 2 / norm x) *\<^sub>R x \<in> s"
hence "u + e / 2 / norm x > u" using`norm x > 0` by(auto simp del:zero_less_norm_iff intro!: divide_pos_pos)
thus False using u_max[OF _ as] by auto
- qed(insert `y\<in>s`, auto simp add: dist_norm scaleR_left_distrib obt(3) norm_scaleR)
+ qed(insert `y\<in>s`, auto simp add: dist_norm scaleR_left_distrib obt(3))
thus ?thesis apply(rule_tac that[of u]) apply(rule obt(1), assumption)
apply(rule,rule,rule ccontr) apply(rule u_max) by auto qed
@@ -1959,7 +1959,7 @@
def pi \<equiv> "\<lambda>x::real^'n. inverse (norm x) *\<^sub>R x"
have "0 \<notin> frontier s" unfolding frontier_straddle apply(rule ccontr) unfolding not_not apply(erule_tac x=1 in allE)
using assms(2)[unfolded subset_eq Ball_def mem_cball] by auto
- 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)
+ have injpi:"\<And>x y. pi x = pi y \<and> norm x = norm y \<longleftrightarrow> x = y" unfolding pi_def by auto
have contpi:"continuous_on (UNIV - {0}) pi" apply(rule continuous_at_imp_continuous_on)
apply rule unfolding pi_def
@@ -1970,7 +1970,7 @@
apply (rule continuous_at_id)
done
def sphere \<equiv> "{x::real^'n. norm x = 1}"
- 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)
+ 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
have "0\<in>s" using assms(2) and centre_in_cball[of 0 1] by auto
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)
@@ -1995,7 +1995,7 @@
next fix x assume "x\<in>sphere" hence "norm x = 1" "x\<noteq>0" unfolding sphere_def by auto
then obtain u where "0 \<le> u" "u *\<^sub>R x \<in> frontier s" "\<forall>v>u. v *\<^sub>R x \<notin> s"
using compact_frontier_line_lemma[OF assms(1) `0\<in>s`, of x] by auto
- 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)
+ 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
next fix x y assume as:"x \<in> frontier s" "y \<in> frontier s" "pi x = pi y"
hence xys:"x\<in>s" "y\<in>s" using fs by auto
from as(1,2) have nor:"norm x \<noteq> 0" "norm y \<noteq> 0" using `0\<notin>frontier s` by auto
@@ -2042,9 +2042,9 @@
moreover have "surf (pi x) \<in> frontier s" using surf(5) pix by auto
hence "dist 0 (inverse (norm (surf (pi x))) *\<^sub>R x) \<le> 1" unfolding dist_norm
using ** and * using front_smul[THEN bspec[where x="surf (pi x)"], THEN spec[where x="norm x * ?a"]]
- using False `x\<in>s` by(auto simp add:field_simps norm_scaleR)
+ using False `x\<in>s` by(auto simp add:field_simps)
ultimately show ?thesis unfolding image_iff apply(rule_tac x="inverse (norm (surf(pi x))) *\<^sub>R x" in bexI)
- apply(subst injpi[THEN sym]) unfolding norm_scaleR abs_mult abs_norm_cancel abs_of_pos[OF `?a > 0`]
+ apply(subst injpi[THEN sym]) unfolding abs_mult abs_norm_cancel abs_of_pos[OF `?a > 0`]
unfolding pi(2)[OF `?a > 0`] by auto
qed } note hom2 = this
@@ -2085,7 +2085,7 @@
using pi(2)[of "norm x" "surf (pi x)"] pi(2)[of "norm y" "surf (pi y)"] by auto
moreover have "pi x \<in> sphere" "pi y \<in> sphere" using pi(1) False by auto
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
- moreover have "norm x = norm y" using as(3)[unfolded *] using False by(auto dest:surf_0 simp add: scaleR_cancel_right)
+ moreover have "norm x = norm y" using as(3)[unfolded *] using False by(auto dest:surf_0)
ultimately show ?thesis using injpi by auto qed qed
qed auto qed
@@ -2100,7 +2100,7 @@
fix y assume "dist (u *\<^sub>R x) y < 1 - u"
hence "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> s"
using assms(3) apply(erule_tac subsetD) unfolding mem_cball dist_commute dist_norm
- unfolding group_add_class.diff_0 group_add_class.diff_0_right norm_minus_cancel norm_scaleR
+ unfolding group_add_class.diff_0 group_add_class.diff_0_right norm_minus_cancel norm_scaleR
apply (rule mult_left_le_imp_le[of "1 - u"])
unfolding class_semiring.mul_a using `u<1` by auto
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]
@@ -2116,7 +2116,7 @@
have "cball ?n 1 \<subseteq> (\<lambda>x. inverse d *\<^sub>R (x - a)) ` s"
apply(rule, rule_tac x="d *\<^sub>R x + a" in image_eqI) defer
apply(rule d[unfolded subset_eq, rule_format]) using `d>0` unfolding mem_cball dist_norm
- by(auto simp add: mult_right_le_one_le norm_scaleR)
+ by(auto simp add: mult_right_le_one_le)
hence "(\<lambda>x. inverse d *\<^sub>R (x - a)) ` s homeomorphic cball ?n 1"
using homeomorphic_convex_compact_lemma[of "(\<lambda>x. ?d *\<^sub>R -a + ?d *\<^sub>R x) ` s", OF convex_affinity compact_affinity]
using assms(1,2) by(auto simp add: uminus_add_conv_diff scaleR_right_diff_distrib)
@@ -2387,9 +2387,9 @@
apply(rule order_trans[of _ "2 * norm (x - y)"]) using as by(auto simp add: field_simps norm_minus_commute)
{ def w \<equiv> "x + t *\<^sub>R (y - x)"
have "w\<in>s" unfolding w_def apply(rule k[unfolded subset_eq,rule_format]) unfolding mem_cball dist_norm
- unfolding t_def using `k>0` by(auto simp add: norm_scaleR simp del: scaleR_right_diff_distrib)
+ unfolding t_def using `k>0` by auto
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)
- also have "\<dots> = 0" using `t>0` by(auto simp add:field_simps simp del:scaleR_left_distrib)
+ also have "\<dots> = 0" using `t>0` by(auto simp add:field_simps)
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)
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)
hence "(f w - f x) / t < e"
@@ -2400,9 +2400,9 @@
moreover
{ def w \<equiv> "x - t *\<^sub>R (y - x)"
have "w\<in>s" unfolding w_def apply(rule k[unfolded subset_eq,rule_format]) unfolding mem_cball dist_norm
- unfolding t_def using `k>0` by(auto simp add: norm_scaleR simp del: scaleR_right_diff_distrib)
+ unfolding t_def using `k>0` by auto
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)
- also have "\<dots>=x" using `t>0` by (auto simp add:field_simps simp del:scaleR_left_distrib)
+ also have "\<dots>=x" using `t>0` by (auto simp add:field_simps)
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)
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)
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)
@@ -2503,8 +2503,8 @@
"dist (midpoint a b) a = (dist a b) / 2" (is ?t3)
"dist (midpoint a b) b = (dist a b) / 2" (is ?t4)
proof-
- 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)
- have **:"\<And>x y::real^'n::finite. 2 *\<^sub>R x = y \<Longrightarrow> norm x = (norm y) / 2" by (auto simp add: norm_scaleR)
+ have *: "\<And>x y::real^'n::finite. 2 *\<^sub>R x = - y \<Longrightarrow> norm x = (norm y) / 2" unfolding equation_minus_iff by auto
+ have **:"\<And>x y::real^'n::finite. 2 *\<^sub>R x = y \<Longrightarrow> norm x = (norm y) / 2" by auto
note scaleR_right_distrib [simp]
show ?t1 unfolding midpoint_def dist_norm apply (rule **) by(auto,vector)
show ?t2 unfolding midpoint_def dist_norm apply (rule *) by(auto,vector)
@@ -2569,7 +2569,7 @@
hence *:"a - x = u *\<^sub>R (a - b)" "x - b = (1 - u) *\<^sub>R (a - b)"
unfolding as(1) by(auto simp add:algebra_simps)
show "norm (a - x) *\<^sub>R (x - b) = norm (x - b) *\<^sub>R (a - x)"
- unfolding norm_minus_commute[of x a] * norm_scaleR Cart_eq using as(2,3)
+ unfolding norm_minus_commute[of x a] * Cart_eq using as(2,3)
by(auto simp add: vector_component_simps field_simps)
next assume as:"dist a b = dist a x + dist x b"
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
@@ -2587,7 +2587,7 @@
lemma between_midpoint: fixes a::"real^'n::finite" shows
"between (a,b) (midpoint a b)" (is ?t1)
"between (b,a) (midpoint a b)" (is ?t2)
-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)
+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
show ?t1 ?t2 unfolding between midpoint_def dist_norm apply(rule_tac[!] *)
by(auto simp add:field_simps Cart_eq vector_component_simps) qed
@@ -2636,7 +2636,7 @@
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)
have "z\<in>interior s" apply(rule subset_interior[OF d,unfolded subset_eq,rule_format])
unfolding interior_open[OF open_ball] mem_ball z_def dist_norm using y and assms(4,5)
- by(auto simp del:scaleR_right_diff_distrib simp add:field_simps norm_minus_commute norm_scaleR)
+ by(auto simp add:field_simps norm_minus_commute)
thus ?thesis unfolding * apply - apply(rule mem_interior_convex_shrink)
using assms(1,4-5) `y\<in>s` by auto qed
@@ -2678,10 +2678,10 @@
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"
show "(\<forall>xa. 0 < x $ xa) \<and> setsum (op $ x) UNIV < 1" apply(rule,rule) proof-
fix i::'n show "0 < x $ i" using as[THEN spec[where x="x - (e / 2) *\<^sub>R basis i"]] and `e>0`
- unfolding dist_norm by(auto simp add: norm_basis vector_component_simps basis_component norm_scaleR elim:allE[where x=i])
+ unfolding dist_norm by(auto simp add: norm_basis vector_component_simps basis_component elim:allE[where x=i])
next guess a using UNIV_witness[where 'a='n] ..
have **:"dist x (x + (e / 2) *\<^sub>R basis a) < e" using `e>0` and norm_basis[of a]
- unfolding dist_norm by(auto simp add: vector_component_simps basis_component norm_scaleR intro!: mult_strict_left_mono_comm)
+ unfolding dist_norm by(auto simp add: vector_component_simps basis_component intro!: mult_strict_left_mono_comm)
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)
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)
have "setsum (op $ x) UNIV < setsum (op $ (x + (e / 2) *\<^sub>R basis a)) UNIV" unfolding * setsum_addf
@@ -2892,12 +2892,12 @@
hence "g1 (2 *\<^sub>R x) = g1 (2 *\<^sub>R y)" using xy(3) unfolding joinpaths_def dest_vec1_def by auto
moreover have "2 *\<^sub>R x \<in> {0..1}" "2 *\<^sub>R y \<in> {0..1}" using xy(1,2) as
unfolding mem_interval_1 dest_vec1_def by(auto simp add:vector_component_simps)
- ultimately show ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] by (auto simp add: scaleR_cancel_left)
+ ultimately show ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] by auto
next assume as:"x $ 1 > 1 / 2" "y $ 1 > 1 / 2"
hence "g2 (2 *\<^sub>R x - 1) = g2 (2 *\<^sub>R y - 1)" using xy(3) unfolding joinpaths_def dest_vec1_def by auto
moreover have "2 *\<^sub>R x - 1 \<in> {0..1}" "2 *\<^sub>R y - 1 \<in> {0..1}" using xy(1,2) as
unfolding mem_interval_1 dest_vec1_def by(auto simp add:vector_component_simps)
- ultimately show ?thesis using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] by (auto simp add: scaleR_cancel_left)
+ ultimately show ?thesis using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] by auto
next assume as:"x $ 1 \<le> 1 / 2" "y $ 1 > 1 / 2"
hence "?g x \<in> path_image g1" "?g y \<in> path_image g2" unfolding path_image_def joinpaths_def
using xy(1,2)[unfolded mem_interval_1] by(auto simp add:vector_component_simps intro!: imageI)
@@ -2934,9 +2934,9 @@
fix x y assume xy:"x \<in> {0..1}" "y \<in> {0..1}" "(g1 +++ g2) x = (g1 +++ g2) y"
show "x = y" proof(cases "x$1 \<le> 1/2", case_tac[!] "y$1 \<le> 1/2", unfold not_le)
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
- unfolding mem_interval_1 joinpaths_def by(auto simp add:vector_component_simps scaleR_cancel_left)
+ unfolding mem_interval_1 joinpaths_def by(auto simp add:vector_component_simps)
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
- unfolding mem_interval_1 joinpaths_def by(auto simp add:vector_component_simps scaleR_cancel_left)
+ unfolding mem_interval_1 joinpaths_def by(auto simp add:vector_component_simps)
next assume as:"x $ 1 \<le> 1 / 2" "y $ 1 > 1 / 2"
hence "?g x \<in> path_image g1" "?g y \<in> path_image g2" unfolding path_image_def joinpaths_def
using xy(1,2)[unfolded mem_interval_1] by(auto simp add:vector_component_simps intro!: imageI)
@@ -3248,10 +3248,10 @@
thus ?thesis using path_connected_empty by auto
qed(auto intro!:path_connected_singleton) next
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)
- 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)
+ 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)
have ***:"\<And>xa. (if xa = 0 then 0 else 1) \<noteq> 1 \<Longrightarrow> xa = 0" apply(rule ccontr) by auto
have **:"{x::real^'n. norm x = 1} = (\<lambda>x. (1/norm x) *\<^sub>R x) ` (UNIV - {0})" apply(rule set_ext,rule)
- unfolding image_iff apply(rule_tac x=x in bexI) unfolding mem_Collect_eq norm_scaleR by(auto intro!: *** simp add: norm_scaleR)
+ unfolding image_iff apply(rule_tac x=x in bexI) unfolding mem_Collect_eq by(auto intro!: ***)
have "continuous_on (UNIV - {0}) (\<lambda>x::real^'n. 1 / norm x)" unfolding o_def continuous_on_eq_continuous_within
apply(rule, rule continuous_at_within_inv[unfolded o_def inverse_eq_divide]) apply(rule continuous_at_within)
apply(rule continuous_at_norm[unfolded o_def]) by auto
--- a/src/HOL/Library/Euclidean_Space.thy Fri Jun 12 11:39:23 2009 -0700
+++ b/src/HOL/Library/Euclidean_Space.thy Fri Jun 12 12:00:30 2009 -0700
@@ -771,7 +771,7 @@
done
show "norm (scaleR a x) = \<bar>a\<bar> * norm x"
unfolding vector_norm_def
- by (simp add: norm_scaleR setL2_right_distrib)
+ by (simp add: setL2_right_distrib)
show "sgn x = scaleR (inverse (norm x)) x"
by (rule vector_sgn_def)
show "dist x y = norm (x - y)"
--- a/src/HOL/Library/Product_Vector.thy Fri Jun 12 11:39:23 2009 -0700
+++ b/src/HOL/Library/Product_Vector.thy Fri Jun 12 12:00:30 2009 -0700
@@ -347,7 +347,7 @@
done
show "norm (scaleR r x) = \<bar>r\<bar> * norm x"
unfolding norm_prod_def
- apply (simp add: norm_scaleR power_mult_distrib)
+ apply (simp add: power_mult_distrib)
apply (simp add: right_distrib [symmetric])
apply (simp add: real_sqrt_mult_distrib)
done
--- a/src/HOL/Library/Topology_Euclidean_Space.thy Fri Jun 12 11:39:23 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy Fri Jun 12 12:00:30 2009 -0700
@@ -1031,7 +1031,7 @@
unfolding trivial_limit_def Rep_net_at_infinity
apply (clarsimp simp add: expand_set_eq)
apply (drule_tac x="scaleR r (sgn 1)" in spec)
- apply (simp add: norm_scaleR norm_sgn)
+ apply (simp add: norm_sgn)
done
lemma trivial_limit_sequentially: "\<not> trivial_limit sequentially"
@@ -1757,7 +1757,7 @@
also have "\<dots> = \<bar>- 1 + d / (2 * norm (x - y))\<bar> * norm (x - y)"
using scaleR_left_distrib[of "- 1" "d / (2 * norm (y - x))", THEN sym, of "y - x"]
unfolding scaleR_minus_left scaleR_one
- by (auto simp add: norm_minus_commute norm_scaleR)
+ by (auto simp add: norm_minus_commute)
also have "\<dots> = \<bar>- norm (x - y) + d / 2\<bar>"
unfolding abs_mult_pos[of "norm (x - y)", OF norm_ge_zero[of "x - y"]]
unfolding real_add_mult_distrib using `x\<noteq>y`[unfolded dist_nz, unfolded dist_norm] by auto
@@ -1769,7 +1769,7 @@
have "(d / (2*dist y x)) *\<^sub>R (y - x) \<noteq> 0"
using `x\<noteq>y`[unfolded dist_nz] `d>0` unfolding scaleR_eq_0_iff by (auto simp add: dist_commute)
moreover
- 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
+ have "dist (y - (d / (2 * dist y x)) *\<^sub>R (y - x)) y < d" unfolding dist_norm apply simp unfolding norm_minus_cancel
using `d>0` `x\<noteq>y`[unfolded dist_nz] dist_commute[of x y]
unfolding dist_norm by auto
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
@@ -1808,11 +1808,11 @@
unfolding z_def by (simp add: algebra_simps)
have "dist z y < r"
unfolding z_def k_def using `0 < r`
- by (simp add: dist_norm norm_scaleR min_def)
+ by (simp add: dist_norm min_def)
hence "z \<in> T" using `\<forall>z. dist z y < r \<longrightarrow> z \<in> T` by simp
have "dist x z < dist x y"
unfolding z_def2 dist_norm
- apply (simp add: norm_scaleR norm_minus_commute)
+ apply (simp add: norm_minus_commute)
apply (simp only: dist_norm [symmetric])
apply (subgoal_tac "\<bar>1 - k\<bar> * dist x y < 1 * dist x y", simp)
apply (rule mult_strict_right_mono)
@@ -1875,7 +1875,7 @@
next
case False
have "dist (y + (d / 2 / dist y x) *\<^sub>R (y - x)) y < d" unfolding dist_norm
- using `d>0` norm_ge_zero[of "y - x"] `x \<noteq> y` by (auto simp add: norm_scaleR)
+ using `d>0` norm_ge_zero[of "y - x"] `x \<noteq> y` by auto
hence *:"y + (d / 2 / dist y x) *\<^sub>R (y - x) \<in> cball x e" using d as(1)[unfolded subset_eq] by blast
have "y - x \<noteq> 0" using `x \<noteq> y` by auto
hence **:"d / (2 * norm (y - x)) > 0" unfolding zero_less_norm_iff[THEN sym]
@@ -1886,7 +1886,7 @@
also have "\<dots> = norm ((1 + d / (2 * norm (y - x))) *\<^sub>R (y - x))"
by (auto simp add: algebra_simps)
also have "\<dots> = \<bar>1 + d / (2 * norm (y - x))\<bar> * norm (y - x)"
- using ** by (auto simp add: norm_scaleR)
+ using ** by auto
also have "\<dots> = (dist y x) + d/2"using ** by (auto simp add: left_distrib dist_norm)
finally have "e \<ge> dist x y +d/2" using *[unfolded mem_cball] by (auto simp add: dist_commute)
thus "y \<in> ball x e" unfolding mem_ball using `d>0` by auto
@@ -2073,7 +2073,7 @@
fix b::real assume b: "b >0"
have b1: "b +1 \<ge> 0" using b by simp
with `x \<noteq> 0` have "b < norm (scaleR (b + 1) (sgn x))"
- by (simp add: norm_scaleR norm_sgn)
+ by (simp add: norm_sgn)
then show "\<exists>x::'a. b < norm x" ..
qed
@@ -4514,7 +4514,7 @@
then obtain N where "\<forall>n\<ge>N. dist (x n) l < e * \<bar>c\<bar>"
using as(2)[unfolded Lim_sequentially, THEN spec[where x="e * abs c"]] by auto
hence "\<exists>N. \<forall>n\<ge>N. dist (scaleR (1 / c) (x n)) (scaleR (1 / c) l) < e"
- unfolding dist_norm unfolding scaleR_right_diff_distrib[THEN sym] norm_scaleR
+ unfolding dist_norm unfolding scaleR_right_diff_distrib[THEN sym]
using mult_imp_div_pos_less[of "abs c" _ e] `c\<noteq>0` by auto }
hence "((\<lambda>n. scaleR (1 / c) (x n)) ---> scaleR (1 / c) l) sequentially" unfolding Lim_sequentially by auto
ultimately have "l \<in> scaleR c ` s"
@@ -4888,7 +4888,7 @@
have "dist (x - (e / 2) *\<^sub>R basis i) x < e"
"dist (x + (e / 2) *\<^sub>R basis i) x < e"
unfolding dist_norm apply auto
- unfolding norm_minus_cancel and norm_scaleR using norm_basis[of i] and `e>0` by auto
+ unfolding norm_minus_cancel using norm_basis[of i] and `e>0` by auto
hence "a $ i \<le> (x - (e / 2) *\<^sub>R basis i) $ i"
"(x + (e / 2) *\<^sub>R basis i) $ i \<le> b $ i"
using e[THEN spec[where x="x - (e/2) *\<^sub>R basis i"]]
@@ -5485,7 +5485,7 @@
apply(rule_tac x="\<lambda>x. a + (d/e) *\<^sub>R (x - b)" in exI)
using assms apply (auto simp add: dist_commute)
unfolding dist_norm
- apply (auto simp add: norm_scaleR pos_divide_less_eq mult_strict_left_mono)
+ apply (auto simp add: pos_divide_less_eq mult_strict_left_mono)
unfolding continuous_on
by (intro ballI tendsto_intros, simp, assumption)+
next
@@ -5495,7 +5495,7 @@
apply(rule_tac x="\<lambda>x. a + (d/e) *\<^sub>R (x - b)" in exI)
using assms apply (auto simp add: dist_commute)
unfolding dist_norm
- apply (auto simp add: norm_scaleR pos_divide_le_eq)
+ apply (auto simp add: pos_divide_le_eq)
unfolding continuous_on
by (intro ballI tendsto_intros, simp, assumption)+
qed
@@ -5586,9 +5586,9 @@
case False
hence *:"0 < norm a / norm x" using `a\<noteq>0` unfolding zero_less_norm_iff[THEN sym] by(simp only: divide_pos_pos)
have "\<forall>c. \<forall>x\<in>s. c *\<^sub>R x \<in> s" using s[unfolded subspace_def smult_conv_scaleR] by auto
- 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)
+ 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
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"]]
- unfolding linear_cmul[OF f(1), unfolded smult_conv_scaleR] and norm_scaleR and ba using `x\<noteq>0` `a\<noteq>0`
+ unfolding linear_cmul[OF f(1), unfolded smult_conv_scaleR] and ba using `x\<noteq>0` `a\<noteq>0`
by (auto simp add: real_mult_commute pos_le_divide_eq pos_divide_le_eq)
qed }
ultimately