author huffman Sun, 17 Sep 2006 16:42:38 +0200 changeset 20560 49996715bc6e parent 20559 2116b7a371c7 child 20561 6a6d8004322f
norm_one is now proved from other class axioms
 src/HOL/Complex/Complex.thy file | annotate | diff | comparison | revisions src/HOL/Real/RealVector.thy file | annotate | diff | comparison | revisions
```--- 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"```
```--- 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)"```