# HG changeset patch
# User huffman
# Date 1315492077 25200
# Node ID 93d0f85cfe4a8797dd7de3b73a67e898429f482d
# Parent  282eef2c0f7704cfcc385316ee0c0d291dadca05
tuned

diff -r 282eef2c0f77 -r 93d0f85cfe4a src/HOL/Complex.thy
--- 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?                *)