generalized sgn function to work on any real normed vector space
authorhuffman
Mon May 14 20:14:31 2007 +0200 (2007-05-14)
changeset 229723e96b98d37c6
parent 22971 a6812b6a36a5
child 22973 64d300e16370
generalized sgn function to work on any real normed vector space
NEWS
src/HOL/Complex/Complex.thy
src/HOL/Real/RealVector.thy
     1.1 --- a/NEWS	Mon May 14 19:14:50 2007 +0200
     1.2 +++ b/NEWS	Mon May 14 20:14:31 2007 +0200
     1.3 @@ -887,19 +887,20 @@
     1.4  spaces. Type annotations may need to be added in some cases; potential
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 -  Infinitesimal  :: ('a::real_normed_vector) star set"
     1.8 -  HFinite        :: ('a::real_normed_vector) star set"
     1.9 -  HInfinite      :: ('a::real_normed_vector) star set"
    1.10 +  Infinitesimal  :: ('a::real_normed_vector) star set
    1.11 +  HFinite        :: ('a::real_normed_vector) star set
    1.12 +  HInfinite      :: ('a::real_normed_vector) star set
    1.13    approx         :: ('a::real_normed_vector) star => 'a star => bool
    1.14    monad          :: ('a::real_normed_vector) star => 'a star set
    1.15    galaxy         :: ('a::real_normed_vector) star => 'a star set
    1.16 -  (NS)LIMSEQ     :: [nat, 'a::real_normed_vector, 'a] => bool
    1.17 +  (NS)LIMSEQ     :: [nat => 'a::real_normed_vector, 'a] => bool
    1.18    (NS)convergent :: (nat => 'a::real_normed_vector) => bool
    1.19    (NS)Bseq       :: (nat => 'a::real_normed_vector) => bool
    1.20    (NS)Cauchy     :: (nat => 'a::real_normed_vector) => bool
    1.21    (NS)LIM        :: ['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool
    1.22    is(NS)Cont     :: ['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool
    1.23    deriv          :: ['a::real_normed_field => 'a, 'a, 'a] => bool
    1.24 +  sgn            :: 'a::real_normed_vector => 'a
    1.25  
    1.26  * Complex: Some complex-specific constants are now abbreviations for
    1.27  overloaded ones: complex_of_real = of_real, cmod = norm, hcmod =
     2.1 --- a/src/HOL/Complex/Complex.thy	Mon May 14 19:14:50 2007 +0200
     2.2 +++ b/src/HOL/Complex/Complex.thy	Mon May 14 20:14:31 2007 +0200
     2.3 @@ -218,6 +218,12 @@
     2.4  defs (overloaded)
     2.5    complex_scaleR_def: "r *# x == Complex r 0 * x"
     2.6  
     2.7 +lemma Re_scaleR [simp]: "Re (scaleR r x) = r * Re x"
     2.8 +unfolding complex_scaleR_def by (induct x, simp)
     2.9 +
    2.10 +lemma Im_scaleR [simp]: "Im (scaleR r x) = r * Im x"
    2.11 +unfolding complex_scaleR_def by (induct x, simp)
    2.12 +
    2.13  instance complex :: real_field
    2.14  proof
    2.15    fix a b :: real
    2.16 @@ -478,29 +484,16 @@
    2.17  by (simp add: i_def complex_zero_def)
    2.18  
    2.19  
    2.20 -subsection{*The Function @{term sgn}*}
    2.21 +subsection{*The Functions @{term sgn} and @{term arg}*}
    2.22  
    2.23 -definition
    2.24 -  (*------------ Argand -------------*)
    2.25 -
    2.26 -  sgn :: "complex => complex" where
    2.27 -  "sgn z = z / complex_of_real(cmod z)"
    2.28 +text {*------------ Argand -------------*}
    2.29  
    2.30  definition
    2.31    arg :: "complex => real" where
    2.32    "arg z = (SOME a. Re(sgn z) = cos a & Im(sgn z) = sin a & -pi < a & a \<le> pi)"
    2.33  
    2.34 -lemma sgn_zero [simp]: "sgn 0 = 0"
    2.35 -by (simp add: sgn_def)
    2.36 -
    2.37 -lemma sgn_one [simp]: "sgn 1 = 1"
    2.38 -by (simp add: sgn_def)
    2.39 -
    2.40 -lemma sgn_minus: "sgn (-z) = - sgn(z)"
    2.41 -by (simp add: sgn_def)
    2.42 -
    2.43  lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)"
    2.44 -by (simp add: sgn_def)
    2.45 +by (simp add: sgn_def divide_inverse scaleR_conv_of_real mult_commute)
    2.46  
    2.47  lemma i_mult_eq: "ii * ii = complex_of_real (-1)"
    2.48  by (simp add: i_def complex_of_real_def)
    2.49 @@ -513,23 +506,10 @@
    2.50  by (simp add: complex_of_real_def)
    2.51  
    2.52  lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z"
    2.53 -proof (induct z)
    2.54 -  case (Complex x y)
    2.55 -    have "sqrt (x\<twosuperior> + y\<twosuperior>) * inverse (x\<twosuperior> + y\<twosuperior>) = inverse (sqrt (x\<twosuperior> + y\<twosuperior>))"
    2.56 -      by (simp add: divide_inverse [symmetric] sqrt_divide_self_eq)
    2.57 -    thus "Re (sgn (Complex x y)) = Re (Complex x y) /cmod (Complex x y)"
    2.58 -       by (simp add: sgn_def complex_of_real_def divide_inverse)
    2.59 -qed
    2.60 -
    2.61 +unfolding sgn_def by (simp add: divide_inverse)
    2.62  
    2.63  lemma Im_sgn [simp]: "Im(sgn z) = Im(z)/cmod z"
    2.64 -proof (induct z)
    2.65 -  case (Complex x y)
    2.66 -    have "sqrt (x\<twosuperior> + y\<twosuperior>) * inverse (x\<twosuperior> + y\<twosuperior>) = inverse (sqrt (x\<twosuperior> + y\<twosuperior>))"
    2.67 -      by (simp add: divide_inverse [symmetric] sqrt_divide_self_eq)
    2.68 -    thus "Im (sgn (Complex x y)) = Im (Complex x y) /cmod (Complex x y)"
    2.69 -       by (simp add: sgn_def complex_of_real_def divide_inverse)
    2.70 -qed
    2.71 +unfolding sgn_def by (simp add: divide_inverse)
    2.72  
    2.73  lemma complex_inverse_complex_split:
    2.74       "inverse(complex_of_real x + ii * complex_of_real y) =
     3.1 --- a/src/HOL/Real/RealVector.thy	Mon May 14 19:14:50 2007 +0200
     3.2 +++ b/src/HOL/Real/RealVector.thy	Mon May 14 20:14:31 2007 +0200
     3.3 @@ -591,6 +591,46 @@
     3.4  by (induct n) (simp_all add: power_Suc norm_mult)
     3.5  
     3.6  
     3.7 +subsection {* Sign function *}
     3.8 +
     3.9 +definition
    3.10 +  sgn :: "'a::real_normed_vector \<Rightarrow> 'a" where
    3.11 +  "sgn x = scaleR (inverse (norm x)) x"
    3.12 +
    3.13 +lemma norm_sgn: "norm (sgn x) = (if x = 0 then 0 else 1)"
    3.14 +unfolding sgn_def by (simp add: norm_scaleR)
    3.15 +
    3.16 +lemma sgn_zero [simp]: "sgn 0 = 0"
    3.17 +unfolding sgn_def by simp
    3.18 +
    3.19 +lemma sgn_zero_iff: "(sgn x = 0) = (x = 0)"
    3.20 +unfolding sgn_def by (simp add: scaleR_eq_0_iff)
    3.21 +
    3.22 +lemma sgn_minus: "sgn (- x) = - sgn x"
    3.23 +unfolding sgn_def by simp
    3.24 +
    3.25 +lemma sgn_one [simp]: "sgn (1::'a::real_normed_algebra_1) = 1"
    3.26 +unfolding sgn_def by simp
    3.27 +
    3.28 +lemma sgn_scaleR: "sgn (scaleR r x) = scaleR (sgn r) (sgn x)"
    3.29 +unfolding sgn_def
    3.30 +by (simp add: real_scaleR_def norm_scaleR mult_ac)
    3.31 +
    3.32 +lemma sgn_of_real:
    3.33 +  "sgn (of_real r::'a::real_normed_algebra_1) = of_real (sgn r)"
    3.34 +unfolding of_real_def by (simp only: sgn_scaleR sgn_one)
    3.35 +
    3.36 +lemma real_sgn_eq: "sgn (x::real) = x / \<bar>x\<bar>"
    3.37 +unfolding sgn_def real_scaleR_def
    3.38 +by (simp add: divide_inverse)
    3.39 +
    3.40 +lemma real_sgn_pos: "0 < (x::real) \<Longrightarrow> sgn x = 1"
    3.41 +unfolding real_sgn_eq by simp
    3.42 +
    3.43 +lemma real_sgn_neg: "(x::real) < 0 \<Longrightarrow> sgn x = -1"
    3.44 +unfolding real_sgn_eq by simp
    3.45 +
    3.46 +
    3.47  subsection {* Bounded Linear and Bilinear Operators *}
    3.48  
    3.49  locale bounded_linear = additive +