# HG changeset patch
# User huffman
# Date 1158504158 -7200
# Node ID 49996715bc6e8bc416bf2a7e26550ae35ef95c3c
# Parent  2116b7a371c7d52efc4ea7571196da175f510de6
norm_one is now proved from other class axioms

diff -r 2116b7a371c7 -r 49996715bc6e src/HOL/Complex/Complex.thy
--- a/src/HOL/Complex/Complex.thy	Sun Sep 17 02:56:25 2006 +0200
+++ b/src/HOL/Complex/Complex.thy	Sun Sep 17 16:42:38 2006 +0200
@@ -507,8 +507,6 @@
     by (rule complex_mod_complex_of_real)
   show "cmod (x * y) = cmod x * cmod y"
     by (rule complex_mod_mult)
-  show "cmod 1 = 1"
-    by (rule complex_mod_one)
 qed
 
 lemma complex_mod_triangle_ineq2 [simp]: "cmod(b + a) - cmod b \<le> cmod a"
diff -r 2116b7a371c7 -r 49996715bc6e src/HOL/Real/RealVector.thy
--- 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)"