# HG changeset patch
# User huffman
# Date 1178759246 -7200
# Node ID f76298ee7bac846fa0ec7c1eaeb8735667c07e88
# Parent  c477862c566df708c321136c58a7d8fcaad5c3f5
lemmas iszero_(h)complex_number_of are no longer needed

diff -r c477862c566d -r f76298ee7bac src/HOL/Complex/Complex.thy
--- a/src/HOL/Complex/Complex.thy	Thu May 10 03:00:15 2007 +0200
+++ b/src/HOL/Complex/Complex.thy	Thu May 10 03:07:26 2007 +0200
@@ -744,16 +744,6 @@
 lemma complex_number_of [simp]: "complex_of_real (number_of w) = number_of w"
 by (rule of_real_number_of_eq)
 
-text{*This theorem is necessary because theorems such as
-   @{text iszero_number_of_0} only hold for ordered rings. They cannot
-   be generalized to fields in general because they fail for finite fields.
-   They work for type complex because the reals can be embedded in them.*}
-(* TODO: generalize and move to Real/RealVector.thy *)
-lemma iszero_complex_number_of [simp]:
-     "iszero (number_of w :: complex) = iszero (number_of w :: real)"
-by (simp only: complex_of_real_zero_iff complex_number_of [symmetric] 
-               iszero_def)
-
 lemma complex_number_of_cnj [simp]: "cnj(number_of v :: complex) = number_of v"
 by (simp only: complex_number_of [symmetric] complex_cnj_complex_of_real)
 
diff -r c477862c566d -r f76298ee7bac src/HOL/Complex/NSComplex.thy
--- a/src/HOL/Complex/NSComplex.thy	Thu May 10 03:00:15 2007 +0200
+++ b/src/HOL/Complex/NSComplex.thy	Thu May 10 03:07:26 2007 +0200
@@ -659,15 +659,6 @@
   "hcomplex_of_complex (number_of w) = hcomplex_of_hypreal(number_of w)"
 by transfer (rule complex_number_of [symmetric])
 
-text{*This theorem is necessary because theorems such as
-   @{text iszero_number_of_0} only hold for ordered rings. They cannot
-   be generalized to fields in general because they fail for finite fields.
-   They work for type complex because the reals can be embedded in them.*}
-lemma iszero_hcomplex_number_of [simp]:
-     "iszero (number_of w :: hcomplex) = iszero (number_of w :: real)"
-by (transfer iszero_def, simp)
-
-
 (*
 Goal "z + hcnj z =  
       hcomplex_of_hypreal (2 * hRe(z))"