src/HOL/Complex.thy
changeset 44843 93d0f85cfe4a
parent 44842 282eef2c0f77
child 44844 f74a4175a3a8
--- a/src/HOL/Complex.thy	Thu Sep 08 07:16:47 2011 -0700
+++ b/src/HOL/Complex.thy	Thu Sep 08 07:27:57 2011 -0700
@@ -335,6 +335,17 @@
 lemma abs_Im_le_cmod: "\<bar>Im x\<bar> \<le> cmod x"
   by (cases x) simp
 
+text {* Properties of complex signum. *}
+
+lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)"
+  by (simp add: sgn_div_norm divide_inverse scaleR_conv_of_real mult_commute)
+
+lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z"
+  by (simp add: complex_sgn_def divide_inverse)
+
+lemma Im_sgn [simp]: "Im(sgn z) = Im(z)/cmod z"
+  by (simp add: complex_sgn_def divide_inverse)
+
 
 subsection {* Completeness of the Complexes *}
 
@@ -535,20 +546,11 @@
   bounded_linear.isCont [OF bounded_linear_cnj]
 
 
-subsection {* Complex Signum and Argument *}
+subsection {* Complex Argument *}
 
 definition arg :: "complex => real" where
   "arg z = (SOME a. Re(sgn z) = cos a & Im(sgn z) = sin a & -pi < a & a \<le> pi)"
 
-lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)"
-  by (simp add: sgn_div_norm divide_inverse scaleR_conv_of_real mult_commute)
-
-lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z"
-  by (simp add: complex_sgn_def divide_inverse)
-
-lemma Im_sgn [simp]: "Im(sgn z) = Im(z)/cmod z"
-  by (simp add: complex_sgn_def divide_inverse)
-
 (*----------------------------------------------------------------------------*)
 (* Many of the theorems below need to be moved elsewhere e.g. Transc. Also *)
 (* many of the theorems are not used - so should they be kept?                *)