--- 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 =
--- 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) =
--- 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 +