src/HOL/Real/RealVector.thy

   norm_mult_ineq: "norm (x * y) \<le> norm x * norm y"
 
 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
   fix a :: real and x :: 'a
   have "norm (a *# x) = norm (of_real a * x)"

 apply (rule abs_ge_zero)
 apply (rule abs_eq_0)
 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"
 by simp
 

   also have "\<dots> \<le> norm (a - c) + norm (b - d)"
     by (rule norm_triangle_ineq)
   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)"
 apply (rule inverse_unique [symmetric])
 apply (simp add: norm_mult [symmetric])