--- a/src/HOL/Real/RealVector.thy Sun Sep 17 02:56:25 2006 +0200
+++ b/src/HOL/Real/RealVector.thy Sun Sep 17 16:42:38 2006 +0200
@@ -279,7 +279,6 @@
axclass real_normed_div_algebra < normed, real_algebra_1, division_ring
norm_of_real: "norm (of_real r) = abs r"
norm_mult: "norm (x * y) = norm x * norm y"
- norm_one [simp]: "norm 1 = 1"
instance real_normed_div_algebra < real_normed_algebra
proof
@@ -302,7 +301,6 @@
apply (rule abs_triangle_ineq)
apply simp
apply (rule abs_mult)
-apply (rule abs_one)
done
lemma norm_zero [simp]: "norm (0::'a::real_normed_vector) = 0"
@@ -366,6 +364,13 @@
finally show ?thesis .
qed
+lemma norm_one [simp]: "norm (1::'a::real_normed_div_algebra) = 1"
+proof -
+ have "norm (of_real 1 :: 'a) = abs 1"
+ by (rule norm_of_real)
+ thus ?thesis by simp
+qed
+
lemma nonzero_norm_inverse:
fixes a :: "'a::real_normed_div_algebra"
shows "a \<noteq> 0 \<Longrightarrow> norm (inverse a) = inverse (norm a)"