# HG changeset patch
# User huffman
# Date 1178592919 -7200
# Node ID cb84e886cc90959c920f7342153fc67312d859f3
# Parent  eb0e0582092aa5e67d9a77d96536af31575431ab
add lemma abs_norm_cancel

diff -r eb0e0582092a -r cb84e886cc90 src/HOL/Real/RealVector.thy
--- 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: