final(?) iteration of sgn saga.
--- a/src/HOL/Complex/Complex.thy Fri Aug 31 23:17:25 2007 +0200
+++ b/src/HOL/Complex/Complex.thy Sat Sep 01 01:21:48 2007 +0200
@@ -299,6 +299,9 @@
cmod :: "complex \<Rightarrow> real" where
"cmod \<equiv> norm"
+instance complex :: sgn
+ complex_sgn_def: "sgn x == x /\<^sub>R cmod x" ..
+
lemmas cmod_def = complex_norm_def
lemma complex_norm [simp]: "cmod (Complex x y) = sqrt (x\<twosuperior> + y\<twosuperior>)"
@@ -320,7 +323,8 @@
show "norm (x * y) = norm x * norm y"
by (induct x, induct y)
(simp add: real_sqrt_mult [symmetric] power2_eq_square ring_simps)
-qed
+ show "sgn x = x /\<^sub>R cmod x" by(simp add: complex_sgn_def)
+qed (* FIXME junk *) (rule refl)+
lemma cmod_unit_one [simp]: "cmod (Complex (cos a) (sin a)) = 1"
by simp
@@ -529,7 +533,7 @@
"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_def divide_inverse scaleR_conv_of_real mult_commute)
+by (simp add: complex_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)
@@ -542,10 +546,10 @@
by (simp add: complex_of_real_def)
lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z"
-unfolding sgn_def by (simp add: divide_inverse)
+by (simp add: complex_sgn_def divide_inverse)
lemma Im_sgn [simp]: "Im(sgn z) = Im(z)/cmod z"
-unfolding sgn_def by (simp add: divide_inverse)
+by (simp add: complex_sgn_def divide_inverse)
lemma complex_inverse_complex_split:
"inverse(complex_of_real x + ii * complex_of_real y) =
--- a/src/HOL/HOL.thy Fri Aug 31 23:17:25 2007 +0200
+++ b/src/HOL/HOL.thy Sat Sep 01 01:21:48 2007 +0200
@@ -233,6 +233,9 @@
class abs = type +
fixes abs :: "'a \<Rightarrow> 'a"
+class sgn = type +
+ fixes sgn :: "'a \<Rightarrow> 'a"
+
notation
uminus ("- _" [81] 80)
--- a/src/HOL/Hyperreal/StarClasses.thy Fri Aug 31 23:17:25 2007 +0200
+++ b/src/HOL/Hyperreal/StarClasses.thy Sat Sep 01 01:21:48 2007 +0200
@@ -30,6 +30,9 @@
instance star :: (abs) abs
star_abs_def: "abs \<equiv> *f* abs" ..
+instance star :: (sgn) sgn
+ star_sgn_def: "sgn \<equiv> *f* sgn" ..
+
instance star :: (inverse) inverse
star_divide_def: "(op /) \<equiv> *f2* (op /)"
star_inverse_def: "inverse \<equiv> *f* inverse" ..
@@ -52,7 +55,7 @@
star_zero_def star_one_def star_number_def
star_add_def star_diff_def star_minus_def
star_mult_def star_divide_def star_inverse_def
- star_le_def star_less_def star_abs_def
+ star_le_def star_less_def star_abs_def star_sgn_def
star_div_def star_mod_def star_power_def
text {* Class operations preserve standard elements *}
@@ -413,6 +416,9 @@
instance star :: (abs_if) abs_if
by (intro_classes, transfer, rule abs_if)
+instance star :: (sgn_if) sgn_if
+by (intro_classes, transfer, rule sgn_if)
+
instance star :: (ordered_ring_strict) ordered_ring_strict ..
instance star :: (pordered_comm_ring) pordered_comm_ring ..
--- a/src/HOL/IntDef.thy Fri Aug 31 23:17:25 2007 +0200
+++ b/src/HOL/IntDef.thy Sat Sep 01 01:21:48 2007 +0200
@@ -215,6 +215,8 @@
instance int :: abs
zabs_def: "\<bar>i\<Colon>int\<bar> \<equiv> if i < 0 then - i else i" ..
+instance int :: sgn
+ zsgn_def: "sgn(i\<Colon>int) \<equiv> (if i=0 then 0 else if 0<i then 1 else - 1)" ..
instance int :: distrib_lattice
"inf \<equiv> min"
@@ -230,6 +232,8 @@
by (rule zmult_zless_mono2)
show "\<bar>i\<bar> = (if i < 0 then -i else i)"
by (simp only: zabs_def)
+ show "sgn(i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
+ by (simp only: zsgn_def)
qed
lemma zless_imp_add1_zle: "w<z ==> w + (1::int) \<le> z"
--- a/src/HOL/Real/Rational.thy Fri Aug 31 23:17:25 2007 +0200
+++ b/src/HOL/Real/Rational.thy Sat Sep 01 01:21:48 2007 +0200
@@ -209,6 +209,9 @@
instance rat :: abs
abs_rat_def: "\<bar>q\<bar> == if q < 0 then -q else (q::rat)" ..
+instance rat :: sgn
+ sgn_rat_def: "sgn(q::rat) == (if q=0 then 0 else if 0<q then 1 else - 1)" ..
+
instance rat :: power ..
primrec (rat)
@@ -405,7 +408,7 @@
qed
show "\<bar>q\<bar> = (if q < 0 then -q else q)"
by (simp only: abs_rat_def)
-qed auto
+qed (auto simp: sgn_rat_def)
instance rat :: division_by_zero
proof
--- a/src/HOL/Real/RealDef.thy Fri Aug 31 23:17:25 2007 +0200
+++ b/src/HOL/Real/RealDef.thy Sat Sep 01 01:21:48 2007 +0200
@@ -65,6 +65,8 @@
instance real :: abs
real_abs_def: "abs (r::real) == (if r < 0 then - r else r)" ..
+instance real :: sgn
+ real_sgn_def: "sgn x == (if x=0 then 0 else if 0<x then 1 else - 1)" ..
subsection {* Equivalence relation over positive reals *}
@@ -412,6 +414,8 @@
show "x \<le> y ==> z + x \<le> z + y" by (rule real_add_left_mono)
show "x < y ==> 0 < z ==> z * x < z * y" by (rule real_mult_less_mono2)
show "\<bar>x\<bar> = (if x < 0 then -x else x)" by (simp only: real_abs_def)
+ show "sgn x = (if x=0 then 0 else if 0<x then 1 else - 1)"
+ by (simp only: real_sgn_def)
qed
text{*The function @{term real_of_preal} requires many proofs, but it seems
--- a/src/HOL/Real/RealVector.thy Fri Aug 31 23:17:25 2007 +0200
+++ b/src/HOL/Real/RealVector.thy Sat Sep 01 01:21:48 2007 +0200
@@ -376,8 +376,16 @@
instance real :: norm
real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>" ..
+ML"set Toplevel.debug"
-axclass real_normed_vector < real_vector, norm
+class sgn_div_norm = scaleR + inverse + norm + sgn +
+assumes sgn_div_norm: "sgn x = x /# norm x"
+(* FIXME junk needed because of bug in locales *)
+and "(sgn :: 'a::scaleR \<Rightarrow> 'a) = sgn"
+and "(inverse :: 'a::scaleR \<Rightarrow> 'a) = inverse"
+and "(scaleR :: real \<Rightarrow> 'a::scaleR \<Rightarrow> 'a) = scaleR"
+
+axclass real_normed_vector < real_vector, sgn_div_norm
norm_ge_zero [simp]: "0 \<le> norm x"
norm_eq_zero [simp]: "(norm x = 0) = (x = 0)"
norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y"
@@ -407,6 +415,9 @@
instance real :: real_normed_field
apply (intro_classes, unfold real_norm_def real_scaleR_def)
+apply (simp add: real_sgn_def)
+(* FIXME junk *)
+apply(rule refl)+
apply (rule abs_ge_zero)
apply (rule abs_eq_0)
apply (rule abs_triangle_ineq)
@@ -584,27 +595,25 @@
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::'a::real_normed_vector)) = (if x = 0 then 0 else 1)"
+by (simp add: sgn_div_norm norm_scaleR)
-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::'a::real_normed_vector) = 0"
+by (simp add: sgn_div_norm)
-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
+lemma sgn_zero_iff: "(sgn(x::'a::real_normed_vector) = 0) = (x = 0)"
+by (simp add: sgn_div_norm)
-lemma sgn_minus: "sgn (- x) = - sgn x"
-unfolding sgn_def by simp
+lemma sgn_minus: "sgn (- x) = - sgn(x::'a::real_normed_vector)"
+by (simp add: sgn_div_norm)
-lemma sgn_scaleR: "sgn (scaleR r x) = scaleR (sgn r) (sgn x)"
-unfolding sgn_def by (simp add: norm_scaleR mult_ac)
+lemma sgn_scaleR:
+ "sgn (scaleR r x) = scaleR (sgn r) (sgn(x::'a::real_normed_vector))"
+by (simp add: sgn_div_norm norm_scaleR mult_ac)
lemma sgn_one [simp]: "sgn (1::'a::real_normed_algebra_1) = 1"
-unfolding sgn_def by simp
+by (simp add: sgn_div_norm)
lemma sgn_of_real:
"sgn (of_real r::'a::real_normed_algebra_1) = of_real (sgn r)"
@@ -613,10 +622,10 @@
lemma sgn_mult:
fixes x y :: "'a::real_normed_div_algebra"
shows "sgn (x * y) = sgn x * sgn y"
-unfolding sgn_def by (simp add: norm_mult mult_commute)
+by (simp add: sgn_div_norm norm_mult mult_commute)
lemma real_sgn_eq: "sgn (x::real) = x / \<bar>x\<bar>"
-unfolding sgn_def by (simp add: divide_inverse)
+by (simp add: sgn_div_norm divide_inverse)
lemma real_sgn_pos: "0 < (x::real) \<Longrightarrow> sgn x = 1"
unfolding real_sgn_eq by simp
--- a/src/HOL/Ring_and_Field.thy Fri Aug 31 23:17:25 2007 +0200
+++ b/src/HOL/Ring_and_Field.thy Sat Sep 01 01:21:48 2007 +0200
@@ -299,6 +299,9 @@
class abs_if = minus + ord + zero + abs +
assumes abs_if: "abs a = (if a \<sqsubset> 0 then (uminus a) else a)"
+class sgn_if = sgn + zero + one + minus + ord +
+assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 \<sqsubset> x then 1 else uminus 1)"
+
(* The "strict" suffix can be seen as describing the combination of ordered_ring and no_zero_divisors.
Basically, ordered_ring + no_zero_divisors = ordered_ring_strict.
*)
@@ -311,7 +314,8 @@
by (simp only: abs_if sup_eq_if)
qed
-class ordered_ring_strict = ring + ordered_semiring_strict + lordered_ab_group + abs_if
+class ordered_ring_strict =
+ ring + ordered_semiring_strict + lordered_ab_group + abs_if
instance ordered_ring_strict \<subseteq> ordered_ring ..
@@ -330,12 +334,13 @@
shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
using add_strict_mono [of 0 a b c] by simp
-class ordered_idom = comm_ring_1 + ordered_comm_semiring_strict + lordered_ab_group + abs_if
+class ordered_idom =
+ comm_ring_1 +
+ ordered_comm_semiring_strict +
+ lordered_ab_group +
+ abs_if + sgn_if
(*previously ordered_ring*)
-definition (in ordered_idom) sgn where
-"sgn x = (if x = \<^loc>0 then \<^loc>0 else if \<^loc>0 \<sqsubset> x then \<^loc>1 else uminus \<^loc>1)"
-
instance ordered_idom \<subseteq> ordered_ring_strict ..
instance ordered_idom \<subseteq> pordered_comm_ring ..
@@ -1901,7 +1906,7 @@
lemma mult_sgn_abs: "sgn x * abs x = (x::'a::{ordered_idom,linorder})"
using less_linear[of x 0]
-by(auto simp: sgn_def abs_if)
+by(auto simp: sgn_if abs_if)
lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)"
by (simp add: abs_if zero_less_one [THEN order_less_not_sym])