1.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Feb 17 17:57:37 2010 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Feb 17 18:33:45 2010 +0100
     1.3 @@ -1042,11 +1042,6 @@
     1.4    shows "norm x \<le> norm y  + norm (x - y)"
     1.5    using norm_triangle_ineq[of "y" "x - y"] by (simp add: ring_simps)
     1.6  
     1.7 -lemma norm_triangle_le: "norm(x::real ^ 'n) + norm y <= e ==> norm(x + y) <= e"
     1.8 -  by (metis order_trans norm_triangle_ineq)
     1.9 -lemma norm_triangle_lt: "norm(x::real ^ 'n) + norm(y) < e ==> norm(x + y) < e"
    1.10 -  by (metis basic_trans_rules(21) norm_triangle_ineq)
    1.11 -
    1.12  lemma component_le_norm: "\<bar>x$i\<bar> <= norm x"
    1.13    apply (simp add: norm_vector_def)
    1.14    apply (rule member_le_setL2, simp_all)
    1.15 @@ -1275,6 +1270,22 @@
    1.16    shows "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 \<Longrightarrow> dist x1 x2 < e"
    1.17  by (rule dist_triangle_half_l, simp_all add: dist_commute)
    1.18  
    1.19 +
    1.20 +lemma norm_triangle_half_r:
    1.21 +  shows "norm (y - x1) < e / 2 \<Longrightarrow> norm (y - x2) < e / 2 \<Longrightarrow> norm (x1 - x2) < e"
    1.22 +  using dist_triangle_half_r unfolding vector_dist_norm[THEN sym] by auto
    1.23 +
    1.24 +lemma norm_triangle_half_l: assumes "norm (x - y) < e / 2" "norm (x' - (y)) < e / 2" 
    1.25 +  shows "norm (x - x') < e"
    1.26 +  using dist_triangle_half_l[OF assms[unfolded vector_dist_norm[THEN sym]]]
    1.27 +  unfolding vector_dist_norm[THEN sym] .
    1.28 +
    1.29 +lemma norm_triangle_le: "norm(x) + norm y <= e ==> norm(x + y) <= e"
    1.30 +  by (metis order_trans norm_triangle_ineq)
    1.31 +
    1.32 +lemma norm_triangle_lt: "norm(x) + norm(y) < e ==> norm(x + y) < e"
    1.33 +  by (metis basic_trans_rules(21) norm_triangle_ineq)
    1.34 +
    1.35  lemma dist_triangle_add:
    1.36    fixes x y x' y' :: "'a::real_normed_vector"
    1.37    shows "dist (x + y) (x' + y') <= dist x x' + dist y y'"