# HG changeset patch
# User nipkow
# Date 1188602508 -7200
# Node ID 020db6ec334a0d30ac9d3e632e6c18090e91b1c5
# Parent  9e6d91f8bb73ca73d918109e9225eae7d6b4133d
final(?) iteration of sgn saga.

diff -r 9e6d91f8bb73 -r 020db6ec334a src/HOL/Complex/Complex.thy
--- 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) =
diff -r 9e6d91f8bb73 -r 020db6ec334a src/HOL/HOL.thy
--- 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)
 
diff -r 9e6d91f8bb73 -r 020db6ec334a src/HOL/Hyperreal/StarClasses.thy
--- 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 ..
 
diff -r 9e6d91f8bb73 -r 020db6ec334a src/HOL/IntDef.thy
--- 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"
diff -r 9e6d91f8bb73 -r 020db6ec334a src/HOL/Real/Rational.thy
--- 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
diff -r 9e6d91f8bb73 -r 020db6ec334a src/HOL/Real/RealDef.thy
--- 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
diff -r 9e6d91f8bb73 -r 020db6ec334a src/HOL/Real/RealVector.thy
--- 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
diff -r 9e6d91f8bb73 -r 020db6ec334a src/HOL/Ring_and_Field.thy
--- 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])