add lemma abs_norm_cancel

--- a/src/HOL/Real/RealVector.thy	Tue May 08 03:03:23 2007 +0200
+++ b/src/HOL/Real/RealVector.thy	Tue May 08 04:55:19 2007 +0200
@@ -488,7 +488,13 @@
   finally show ?thesis .
 qed
 
-lemma norm_of_real: "norm (of_real r :: 'a::real_normed_algebra_1) = \<bar>r\<bar>"
+lemma abs_norm_cancel [simp]:
+  fixes a :: "'a::real_normed_vector"
+  shows "\<bar>norm a\<bar> = norm a"
+by (rule abs_of_nonneg [OF norm_ge_zero])
+
+lemma norm_of_real [simp]:
+  "norm (of_real r :: 'a::real_normed_algebra_1) = \<bar>r\<bar>"
 unfolding of_real_def by (simp add: norm_scaleR)
 
 lemma nonzero_norm_inverse: