# HG changeset patch
# User huffman
# Date 1178759463 -7200
# Node ID 681700e1d6932e648014d1bf52609edafabfbe3d
# Parent  f76298ee7bac846fa0ec7c1eaeb8735667c07e88
remove redundant lemmas

diff -r f76298ee7bac -r 681700e1d693 src/HOL/Complex/Complex.thy
--- a/src/HOL/Complex/Complex.thy	Thu May 10 03:07:26 2007 +0200
+++ b/src/HOL/Complex/Complex.thy	Thu May 10 03:11:03 2007 +0200
@@ -447,15 +447,6 @@
 lemma complex_mod_triangle_ineq2 [simp]: "cmod(b + a) - cmod b \<le> cmod a"
 by (rule ord_le_eq_trans [OF norm_triangle_ineq2], simp)
 
-lemma complex_mod_diff_ineq [simp]: "cmod(a) - cmod(b) \<le> cmod(a + b)"
-(* TODO: generalize *)
-proof -
-  have "cmod a - cmod b = cmod a - cmod (- b)" by simp
-  also have "\<dots> \<le> cmod (a - - b)" by (rule norm_triangle_ineq2)
-  also have "\<dots> = cmod (a + b)" by simp
-  finally show ?thesis .
-qed
-
 lemmas real_sum_squared_expand = power2_sum [where 'a=real]
 
 
@@ -561,9 +552,6 @@
 (* many of the theorems are not used - so should they be kept?                *)
 (*----------------------------------------------------------------------------*)
 
-lemma complex_of_real_zero_iff: "(complex_of_real y = 0) = (y = 0)"
-by (rule of_real_eq_0_iff)
-
 lemma cos_arg_i_mult_zero_pos:
    "0 < y ==> cos (arg(Complex 0 y)) = 0"
 apply (simp add: arg_def abs_if)
@@ -739,9 +727,7 @@
 instance complex :: number_ring
 by (intro_classes, simp add: complex_number_of_def)
 
-
-text{*Collapse applications of @{term complex_of_real} to @{term number_of}*}
-lemma complex_number_of [simp]: "complex_of_real (number_of w) = number_of w"
+lemma complex_number_of: "complex_of_real (number_of w) = number_of w"
 by (rule of_real_number_of_eq)
 
 lemma complex_number_of_cnj [simp]: "cnj(number_of v :: complex) = number_of v"
diff -r f76298ee7bac -r 681700e1d693 src/HOL/Complex/NSComplex.thy
--- a/src/HOL/Complex/NSComplex.thy	Thu May 10 03:07:26 2007 +0200
+++ b/src/HOL/Complex/NSComplex.thy	Thu May 10 03:11:03 2007 +0200
@@ -349,7 +349,7 @@
 by transfer (rule complex_mod_triangle_ineq2)
 
 lemma hcmod_diff_ineq [simp]: "!!a b. hcmod(a) - hcmod(b) \<le> hcmod(a + b)"
-by transfer (rule complex_mod_diff_ineq)
+by transfer (rule norm_diff_ineq)
 
 
 subsection{*Exponentiation*}