src/HOL/Real/RealVector.thy
changeset 22972 3e96b98d37c6
parent 22942 bf718970e5ef
child 22973 64d300e16370
     1.1 --- a/src/HOL/Real/RealVector.thy	Mon May 14 19:14:50 2007 +0200
     1.2 +++ b/src/HOL/Real/RealVector.thy	Mon May 14 20:14:31 2007 +0200
     1.3 @@ -591,6 +591,46 @@
     1.4  by (induct n) (simp_all add: power_Suc norm_mult)
     1.5  
     1.6  
     1.7 +subsection {* Sign function *}
     1.8 +
     1.9 +definition
    1.10 +  sgn :: "'a::real_normed_vector \<Rightarrow> 'a" where
    1.11 +  "sgn x = scaleR (inverse (norm x)) x"
    1.12 +
    1.13 +lemma norm_sgn: "norm (sgn x) = (if x = 0 then 0 else 1)"
    1.14 +unfolding sgn_def by (simp add: norm_scaleR)
    1.15 +
    1.16 +lemma sgn_zero [simp]: "sgn 0 = 0"
    1.17 +unfolding sgn_def by simp
    1.18 +
    1.19 +lemma sgn_zero_iff: "(sgn x = 0) = (x = 0)"
    1.20 +unfolding sgn_def by (simp add: scaleR_eq_0_iff)
    1.21 +
    1.22 +lemma sgn_minus: "sgn (- x) = - sgn x"
    1.23 +unfolding sgn_def by simp
    1.24 +
    1.25 +lemma sgn_one [simp]: "sgn (1::'a::real_normed_algebra_1) = 1"
    1.26 +unfolding sgn_def by simp
    1.27 +
    1.28 +lemma sgn_scaleR: "sgn (scaleR r x) = scaleR (sgn r) (sgn x)"
    1.29 +unfolding sgn_def
    1.30 +by (simp add: real_scaleR_def norm_scaleR mult_ac)
    1.31 +
    1.32 +lemma sgn_of_real:
    1.33 +  "sgn (of_real r::'a::real_normed_algebra_1) = of_real (sgn r)"
    1.34 +unfolding of_real_def by (simp only: sgn_scaleR sgn_one)
    1.35 +
    1.36 +lemma real_sgn_eq: "sgn (x::real) = x / \<bar>x\<bar>"
    1.37 +unfolding sgn_def real_scaleR_def
    1.38 +by (simp add: divide_inverse)
    1.39 +
    1.40 +lemma real_sgn_pos: "0 < (x::real) \<Longrightarrow> sgn x = 1"
    1.41 +unfolding real_sgn_eq by simp
    1.42 +
    1.43 +lemma real_sgn_neg: "(x::real) < 0 \<Longrightarrow> sgn x = -1"
    1.44 +unfolding real_sgn_eq by simp
    1.45 +
    1.46 +
    1.47  subsection {* Bounded Linear and Bilinear Operators *}
    1.48  
    1.49  locale bounded_linear = additive +