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?                *)```