# HG changeset patch
# User huffman
# Date 1179166471 -7200
# Node ID 3e96b98d37c65b2a6b301f7ac41e11c6c2d04496
# Parent  a6812b6a36a5456b97deac2fba255d3bb5791154
generalized sgn function to work on any real normed vector space

diff -r a6812b6a36a5 -r 3e96b98d37c6 NEWS
--- a/NEWS	Mon May 14 19:14:50 2007 +0200
+++ b/NEWS	Mon May 14 20:14:31 2007 +0200
@@ -887,19 +887,20 @@
 spaces. Type annotations may need to be added in some cases; potential
 INCOMPATIBILITY.
 
-  Infinitesimal  :: ('a::real_normed_vector) star set"
-  HFinite        :: ('a::real_normed_vector) star set"
-  HInfinite      :: ('a::real_normed_vector) star set"
+  Infinitesimal  :: ('a::real_normed_vector) star set
+  HFinite        :: ('a::real_normed_vector) star set
+  HInfinite      :: ('a::real_normed_vector) star set
   approx         :: ('a::real_normed_vector) star => 'a star => bool
   monad          :: ('a::real_normed_vector) star => 'a star set
   galaxy         :: ('a::real_normed_vector) star => 'a star set
-  (NS)LIMSEQ     :: [nat, 'a::real_normed_vector, 'a] => bool
+  (NS)LIMSEQ     :: [nat => 'a::real_normed_vector, 'a] => bool
   (NS)convergent :: (nat => 'a::real_normed_vector) => bool
   (NS)Bseq       :: (nat => 'a::real_normed_vector) => bool
   (NS)Cauchy     :: (nat => 'a::real_normed_vector) => bool
   (NS)LIM        :: ['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool
   is(NS)Cont     :: ['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool
   deriv          :: ['a::real_normed_field => 'a, 'a, 'a] => bool
+  sgn            :: 'a::real_normed_vector => 'a
 
 * Complex: Some complex-specific constants are now abbreviations for
 overloaded ones: complex_of_real = of_real, cmod = norm, hcmod =
diff -r a6812b6a36a5 -r 3e96b98d37c6 src/HOL/Complex/Complex.thy
--- a/src/HOL/Complex/Complex.thy	Mon May 14 19:14:50 2007 +0200
+++ b/src/HOL/Complex/Complex.thy	Mon May 14 20:14:31 2007 +0200
@@ -218,6 +218,12 @@
 defs (overloaded)
   complex_scaleR_def: "r *# x == Complex r 0 * x"
 
+lemma Re_scaleR [simp]: "Re (scaleR r x) = r * Re x"
+unfolding complex_scaleR_def by (induct x, simp)
+
+lemma Im_scaleR [simp]: "Im (scaleR r x) = r * Im x"
+unfolding complex_scaleR_def by (induct x, simp)
+
 instance complex :: real_field
 proof
   fix a b :: real
@@ -478,29 +484,16 @@
 by (simp add: i_def complex_zero_def)
 
 
-subsection{*The Function @{term sgn}*}
+subsection{*The Functions @{term sgn} and @{term arg}*}
 
-definition
-  (*------------ Argand -------------*)
-
-  sgn :: "complex => complex" where
-  "sgn z = z / complex_of_real(cmod z)"
+text {*------------ Argand -------------*}
 
 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_zero [simp]: "sgn 0 = 0"
-by (simp add: sgn_def)
-
-lemma sgn_one [simp]: "sgn 1 = 1"
-by (simp add: sgn_def)
-
-lemma sgn_minus: "sgn (-z) = - sgn(z)"
-by (simp add: sgn_def)
-
 lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)"
-by (simp add: sgn_def)
+by (simp add: sgn_def divide_inverse scaleR_conv_of_real mult_commute)
 
 lemma i_mult_eq: "ii * ii = complex_of_real (-1)"
 by (simp add: i_def complex_of_real_def)
@@ -513,23 +506,10 @@
 by (simp add: complex_of_real_def)
 
 lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z"
-proof (induct z)
-  case (Complex x y)
-    have "sqrt (x\<twosuperior> + y\<twosuperior>) * inverse (x\<twosuperior> + y\<twosuperior>) = inverse (sqrt (x\<twosuperior> + y\<twosuperior>))"
-      by (simp add: divide_inverse [symmetric] sqrt_divide_self_eq)
-    thus "Re (sgn (Complex x y)) = Re (Complex x y) /cmod (Complex x y)"
-       by (simp add: sgn_def complex_of_real_def divide_inverse)
-qed
-
+unfolding sgn_def by (simp add: divide_inverse)
 
 lemma Im_sgn [simp]: "Im(sgn z) = Im(z)/cmod z"
-proof (induct z)
-  case (Complex x y)
-    have "sqrt (x\<twosuperior> + y\<twosuperior>) * inverse (x\<twosuperior> + y\<twosuperior>) = inverse (sqrt (x\<twosuperior> + y\<twosuperior>))"
-      by (simp add: divide_inverse [symmetric] sqrt_divide_self_eq)
-    thus "Im (sgn (Complex x y)) = Im (Complex x y) /cmod (Complex x y)"
-       by (simp add: sgn_def complex_of_real_def divide_inverse)
-qed
+unfolding sgn_def by (simp add: divide_inverse)
 
 lemma complex_inverse_complex_split:
      "inverse(complex_of_real x + ii * complex_of_real y) =
diff -r a6812b6a36a5 -r 3e96b98d37c6 src/HOL/Real/RealVector.thy
--- a/src/HOL/Real/RealVector.thy	Mon May 14 19:14:50 2007 +0200
+++ b/src/HOL/Real/RealVector.thy	Mon May 14 20:14:31 2007 +0200
@@ -591,6 +591,46 @@
 by (induct n) (simp_all add: power_Suc norm_mult)
 
 
+subsection {* Sign function *}
+
+definition
+  sgn :: "'a::real_normed_vector \<Rightarrow> 'a" where
+  "sgn x = scaleR (inverse (norm x)) x"
+
+lemma norm_sgn: "norm (sgn x) = (if x = 0 then 0 else 1)"
+unfolding sgn_def by (simp add: norm_scaleR)
+
+lemma sgn_zero [simp]: "sgn 0 = 0"
+unfolding sgn_def by simp
+
+lemma sgn_zero_iff: "(sgn x = 0) = (x = 0)"
+unfolding sgn_def by (simp add: scaleR_eq_0_iff)
+
+lemma sgn_minus: "sgn (- x) = - sgn x"
+unfolding sgn_def by simp
+
+lemma sgn_one [simp]: "sgn (1::'a::real_normed_algebra_1) = 1"
+unfolding sgn_def by simp
+
+lemma sgn_scaleR: "sgn (scaleR r x) = scaleR (sgn r) (sgn x)"
+unfolding sgn_def
+by (simp add: real_scaleR_def norm_scaleR mult_ac)
+
+lemma sgn_of_real:
+  "sgn (of_real r::'a::real_normed_algebra_1) = of_real (sgn r)"
+unfolding of_real_def by (simp only: sgn_scaleR sgn_one)
+
+lemma real_sgn_eq: "sgn (x::real) = x / \<bar>x\<bar>"
+unfolding sgn_def real_scaleR_def
+by (simp add: divide_inverse)
+
+lemma real_sgn_pos: "0 < (x::real) \<Longrightarrow> sgn x = 1"
+unfolding real_sgn_eq by simp
+
+lemma real_sgn_neg: "(x::real) < 0 \<Longrightarrow> sgn x = -1"
+unfolding real_sgn_eq by simp
+
+
 subsection {* Bounded Linear and Bilinear Operators *}
 
 locale bounded_linear = additive +