final(?) iteration of sgn saga.
authornipkow
Sat Sep 01 01:21:48 2007 +0200 (2007-09-01)
changeset 24506020db6ec334a
parent 24505 9e6d91f8bb73
child 24507 ac22a2a67100
final(?) iteration of sgn saga.
src/HOL/Complex/Complex.thy
src/HOL/HOL.thy
src/HOL/Hyperreal/StarClasses.thy
src/HOL/IntDef.thy
src/HOL/Real/Rational.thy
src/HOL/Real/RealDef.thy
src/HOL/Real/RealVector.thy
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/Complex/Complex.thy	Fri Aug 31 23:17:25 2007 +0200
     1.2 +++ b/src/HOL/Complex/Complex.thy	Sat Sep 01 01:21:48 2007 +0200
     1.3 @@ -299,6 +299,9 @@
     1.4    cmod :: "complex \<Rightarrow> real" where
     1.5      "cmod \<equiv> norm"
     1.6  
     1.7 +instance complex :: sgn
     1.8 +  complex_sgn_def: "sgn x == x /\<^sub>R cmod x" ..
     1.9 +
    1.10  lemmas cmod_def = complex_norm_def
    1.11  
    1.12  lemma complex_norm [simp]: "cmod (Complex x y) = sqrt (x\<twosuperior> + y\<twosuperior>)"
    1.13 @@ -320,7 +323,8 @@
    1.14    show "norm (x * y) = norm x * norm y"
    1.15      by (induct x, induct y)
    1.16         (simp add: real_sqrt_mult [symmetric] power2_eq_square ring_simps)
    1.17 -qed
    1.18 +  show "sgn x = x /\<^sub>R cmod x" by(simp add: complex_sgn_def)
    1.19 +qed (* FIXME junk *) (rule refl)+
    1.20  
    1.21  lemma cmod_unit_one [simp]: "cmod (Complex (cos a) (sin a)) = 1"
    1.22  by simp
    1.23 @@ -529,7 +533,7 @@
    1.24    "arg z = (SOME a. Re(sgn z) = cos a & Im(sgn z) = sin a & -pi < a & a \<le> pi)"
    1.25  
    1.26  lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)"
    1.27 -by (simp add: sgn_def divide_inverse scaleR_conv_of_real mult_commute)
    1.28 +by (simp add: complex_sgn_def divide_inverse scaleR_conv_of_real mult_commute)
    1.29  
    1.30  lemma i_mult_eq: "ii * ii = complex_of_real (-1)"
    1.31  by (simp add: i_def complex_of_real_def)
    1.32 @@ -542,10 +546,10 @@
    1.33  by (simp add: complex_of_real_def)
    1.34  
    1.35  lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z"
    1.36 -unfolding sgn_def by (simp add: divide_inverse)
    1.37 +by (simp add: complex_sgn_def divide_inverse)
    1.38  
    1.39  lemma Im_sgn [simp]: "Im(sgn z) = Im(z)/cmod z"
    1.40 -unfolding sgn_def by (simp add: divide_inverse)
    1.41 +by (simp add: complex_sgn_def divide_inverse)
    1.42  
    1.43  lemma complex_inverse_complex_split:
    1.44       "inverse(complex_of_real x + ii * complex_of_real y) =
     2.1 --- a/src/HOL/HOL.thy	Fri Aug 31 23:17:25 2007 +0200
     2.2 +++ b/src/HOL/HOL.thy	Sat Sep 01 01:21:48 2007 +0200
     2.3 @@ -233,6 +233,9 @@
     2.4  class abs = type +
     2.5    fixes abs :: "'a \<Rightarrow> 'a"
     2.6  
     2.7 +class sgn = type +
     2.8 +  fixes sgn :: "'a \<Rightarrow> 'a"
     2.9 +
    2.10  notation
    2.11    uminus  ("- _" [81] 80)
    2.12  
     3.1 --- a/src/HOL/Hyperreal/StarClasses.thy	Fri Aug 31 23:17:25 2007 +0200
     3.2 +++ b/src/HOL/Hyperreal/StarClasses.thy	Sat Sep 01 01:21:48 2007 +0200
     3.3 @@ -30,6 +30,9 @@
     3.4  instance star :: (abs) abs
     3.5    star_abs_def:     "abs \<equiv> *f* abs" ..
     3.6  
     3.7 +instance star :: (sgn) sgn
     3.8 +  star_sgn_def:     "sgn \<equiv> *f* sgn" ..
     3.9 +
    3.10  instance star :: (inverse) inverse
    3.11    star_divide_def:  "(op /) \<equiv> *f2* (op /)"
    3.12    star_inverse_def: "inverse \<equiv> *f* inverse" ..
    3.13 @@ -52,7 +55,7 @@
    3.14    star_zero_def     star_one_def      star_number_def
    3.15    star_add_def      star_diff_def     star_minus_def
    3.16    star_mult_def     star_divide_def   star_inverse_def
    3.17 -  star_le_def       star_less_def     star_abs_def
    3.18 +  star_le_def       star_less_def     star_abs_def       star_sgn_def
    3.19    star_div_def      star_mod_def      star_power_def
    3.20  
    3.21  text {* Class operations preserve standard elements *}
    3.22 @@ -413,6 +416,9 @@
    3.23  instance star :: (abs_if) abs_if
    3.24  by (intro_classes, transfer, rule abs_if)
    3.25  
    3.26 +instance star :: (sgn_if) sgn_if
    3.27 +by (intro_classes, transfer, rule sgn_if)
    3.28 +
    3.29  instance star :: (ordered_ring_strict) ordered_ring_strict ..
    3.30  instance star :: (pordered_comm_ring) pordered_comm_ring ..
    3.31  
     4.1 --- a/src/HOL/IntDef.thy	Fri Aug 31 23:17:25 2007 +0200
     4.2 +++ b/src/HOL/IntDef.thy	Sat Sep 01 01:21:48 2007 +0200
     4.3 @@ -215,6 +215,8 @@
     4.4  
     4.5  instance int :: abs
     4.6    zabs_def: "\<bar>i\<Colon>int\<bar> \<equiv> if i < 0 then - i else i" ..
     4.7 +instance int :: sgn
     4.8 +  zsgn_def: "sgn(i\<Colon>int) \<equiv> (if i=0 then 0 else if 0<i then 1 else - 1)" ..
     4.9  
    4.10  instance int :: distrib_lattice
    4.11    "inf \<equiv> min"
    4.12 @@ -230,6 +232,8 @@
    4.13      by (rule zmult_zless_mono2)
    4.14    show "\<bar>i\<bar> = (if i < 0 then -i else i)"
    4.15      by (simp only: zabs_def)
    4.16 +  show "sgn(i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
    4.17 +    by (simp only: zsgn_def)
    4.18  qed
    4.19  
    4.20  lemma zless_imp_add1_zle: "w<z ==> w + (1::int) \<le> z"
     5.1 --- a/src/HOL/Real/Rational.thy	Fri Aug 31 23:17:25 2007 +0200
     5.2 +++ b/src/HOL/Real/Rational.thy	Sat Sep 01 01:21:48 2007 +0200
     5.3 @@ -209,6 +209,9 @@
     5.4  instance rat :: abs
     5.5    abs_rat_def: "\<bar>q\<bar> == if q < 0 then -q else (q::rat)" ..
     5.6  
     5.7 +instance rat :: sgn
     5.8 +  sgn_rat_def: "sgn(q::rat) == (if q=0 then 0 else if 0<q then 1 else - 1)" ..
     5.9 +
    5.10  instance rat :: power ..
    5.11  
    5.12  primrec (rat)
    5.13 @@ -405,7 +408,7 @@
    5.14    qed
    5.15    show "\<bar>q\<bar> = (if q < 0 then -q else q)"
    5.16      by (simp only: abs_rat_def)
    5.17 -qed auto
    5.18 +qed (auto simp: sgn_rat_def)
    5.19  
    5.20  instance rat :: division_by_zero
    5.21  proof
     6.1 --- a/src/HOL/Real/RealDef.thy	Fri Aug 31 23:17:25 2007 +0200
     6.2 +++ b/src/HOL/Real/RealDef.thy	Sat Sep 01 01:21:48 2007 +0200
     6.3 @@ -65,6 +65,8 @@
     6.4  instance real :: abs
     6.5    real_abs_def:  "abs (r::real) == (if r < 0 then - r else r)" ..
     6.6  
     6.7 +instance real :: sgn
     6.8 +  real_sgn_def: "sgn x == (if x=0 then 0 else if 0<x then 1 else - 1)" ..
     6.9  
    6.10  subsection {* Equivalence relation over positive reals *}
    6.11  
    6.12 @@ -412,6 +414,8 @@
    6.13    show "x \<le> y ==> z + x \<le> z + y" by (rule real_add_left_mono)
    6.14    show "x < y ==> 0 < z ==> z * x < z * y" by (rule real_mult_less_mono2)
    6.15    show "\<bar>x\<bar> = (if x < 0 then -x else x)" by (simp only: real_abs_def)
    6.16 +  show "sgn x = (if x=0 then 0 else if 0<x then 1 else - 1)"
    6.17 +    by (simp only: real_sgn_def)
    6.18  qed
    6.19  
    6.20  text{*The function @{term real_of_preal} requires many proofs, but it seems
     7.1 --- a/src/HOL/Real/RealVector.thy	Fri Aug 31 23:17:25 2007 +0200
     7.2 +++ b/src/HOL/Real/RealVector.thy	Sat Sep 01 01:21:48 2007 +0200
     7.3 @@ -376,8 +376,16 @@
     7.4  
     7.5  instance real :: norm
     7.6    real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>" ..
     7.7 +ML"set Toplevel.debug"
     7.8  
     7.9 -axclass real_normed_vector < real_vector, norm
    7.10 +class sgn_div_norm = scaleR + inverse + norm + sgn +
    7.11 +assumes sgn_div_norm: "sgn x = x /# norm x"
    7.12 +(* FIXME junk needed because of bug in locales *)
    7.13 +and "(sgn :: 'a::scaleR \<Rightarrow> 'a) = sgn"
    7.14 +and "(inverse :: 'a::scaleR \<Rightarrow> 'a) = inverse"
    7.15 +and "(scaleR :: real \<Rightarrow> 'a::scaleR \<Rightarrow> 'a) = scaleR"
    7.16 +
    7.17 +axclass real_normed_vector < real_vector, sgn_div_norm
    7.18    norm_ge_zero [simp]: "0 \<le> norm x"
    7.19    norm_eq_zero [simp]: "(norm x = 0) = (x = 0)"
    7.20    norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y"
    7.21 @@ -407,6 +415,9 @@
    7.22  
    7.23  instance real :: real_normed_field
    7.24  apply (intro_classes, unfold real_norm_def real_scaleR_def)
    7.25 +apply (simp add: real_sgn_def)
    7.26 +(* FIXME junk *)
    7.27 +apply(rule refl)+
    7.28  apply (rule abs_ge_zero)
    7.29  apply (rule abs_eq_0)
    7.30  apply (rule abs_triangle_ineq)
    7.31 @@ -584,27 +595,25 @@
    7.32  
    7.33  subsection {* Sign function *}
    7.34  
    7.35 -definition
    7.36 -  sgn :: "'a::real_normed_vector \<Rightarrow> 'a" where
    7.37 -  "sgn x = scaleR (inverse (norm x)) x"
    7.38 +lemma norm_sgn:
    7.39 +  "norm (sgn(x::'a::real_normed_vector)) = (if x = 0 then 0 else 1)"
    7.40 +by (simp add: sgn_div_norm norm_scaleR)
    7.41  
    7.42 -lemma norm_sgn: "norm (sgn x) = (if x = 0 then 0 else 1)"
    7.43 -unfolding sgn_def by (simp add: norm_scaleR)
    7.44 +lemma sgn_zero [simp]: "sgn(0::'a::real_normed_vector) = 0"
    7.45 +by (simp add: sgn_div_norm)
    7.46  
    7.47 -lemma sgn_zero [simp]: "sgn 0 = 0"
    7.48 -unfolding sgn_def by simp
    7.49 -
    7.50 -lemma sgn_zero_iff: "(sgn x = 0) = (x = 0)"
    7.51 -unfolding sgn_def by simp
    7.52 +lemma sgn_zero_iff: "(sgn(x::'a::real_normed_vector) = 0) = (x = 0)"
    7.53 +by (simp add: sgn_div_norm)
    7.54  
    7.55 -lemma sgn_minus: "sgn (- x) = - sgn x"
    7.56 -unfolding sgn_def by simp
    7.57 +lemma sgn_minus: "sgn (- x) = - sgn(x::'a::real_normed_vector)"
    7.58 +by (simp add: sgn_div_norm)
    7.59  
    7.60 -lemma sgn_scaleR: "sgn (scaleR r x) = scaleR (sgn r) (sgn x)"
    7.61 -unfolding sgn_def by (simp add: norm_scaleR mult_ac)
    7.62 +lemma sgn_scaleR:
    7.63 +  "sgn (scaleR r x) = scaleR (sgn r) (sgn(x::'a::real_normed_vector))"
    7.64 +by (simp add: sgn_div_norm norm_scaleR mult_ac)
    7.65  
    7.66  lemma sgn_one [simp]: "sgn (1::'a::real_normed_algebra_1) = 1"
    7.67 -unfolding sgn_def by simp
    7.68 +by (simp add: sgn_div_norm)
    7.69  
    7.70  lemma sgn_of_real:
    7.71    "sgn (of_real r::'a::real_normed_algebra_1) = of_real (sgn r)"
    7.72 @@ -613,10 +622,10 @@
    7.73  lemma sgn_mult:
    7.74    fixes x y :: "'a::real_normed_div_algebra"
    7.75    shows "sgn (x * y) = sgn x * sgn y"
    7.76 -unfolding sgn_def by (simp add: norm_mult mult_commute)
    7.77 +by (simp add: sgn_div_norm norm_mult mult_commute)
    7.78  
    7.79  lemma real_sgn_eq: "sgn (x::real) = x / \<bar>x\<bar>"
    7.80 -unfolding sgn_def by (simp add: divide_inverse)
    7.81 +by (simp add: sgn_div_norm divide_inverse)
    7.82  
    7.83  lemma real_sgn_pos: "0 < (x::real) \<Longrightarrow> sgn x = 1"
    7.84  unfolding real_sgn_eq by simp
     8.1 --- a/src/HOL/Ring_and_Field.thy	Fri Aug 31 23:17:25 2007 +0200
     8.2 +++ b/src/HOL/Ring_and_Field.thy	Sat Sep 01 01:21:48 2007 +0200
     8.3 @@ -299,6 +299,9 @@
     8.4  class abs_if = minus + ord + zero + abs +
     8.5    assumes abs_if: "abs a = (if a \<sqsubset> 0 then (uminus a) else a)"
     8.6  
     8.7 +class sgn_if = sgn + zero + one + minus + ord +
     8.8 +assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 \<sqsubset> x then 1 else uminus 1)"
     8.9 +
    8.10  (* The "strict" suffix can be seen as describing the combination of ordered_ring and no_zero_divisors.
    8.11     Basically, ordered_ring + no_zero_divisors = ordered_ring_strict.
    8.12   *)
    8.13 @@ -311,7 +314,8 @@
    8.14      by (simp only: abs_if sup_eq_if)
    8.15  qed
    8.16  
    8.17 -class ordered_ring_strict = ring + ordered_semiring_strict + lordered_ab_group + abs_if
    8.18 +class ordered_ring_strict =
    8.19 +  ring + ordered_semiring_strict + lordered_ab_group + abs_if
    8.20  
    8.21  instance ordered_ring_strict \<subseteq> ordered_ring ..
    8.22  
    8.23 @@ -330,12 +334,13 @@
    8.24    shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
    8.25    using add_strict_mono [of 0 a b c] by simp
    8.26  
    8.27 -class ordered_idom = comm_ring_1 + ordered_comm_semiring_strict + lordered_ab_group + abs_if
    8.28 +class ordered_idom =
    8.29 +  comm_ring_1 +
    8.30 +  ordered_comm_semiring_strict +
    8.31 +  lordered_ab_group +
    8.32 +  abs_if + sgn_if
    8.33    (*previously ordered_ring*)
    8.34  
    8.35 -definition (in ordered_idom) sgn where
    8.36 -"sgn x = (if x = \<^loc>0 then \<^loc>0 else if \<^loc>0 \<sqsubset> x then \<^loc>1 else uminus \<^loc>1)"
    8.37 -
    8.38  instance ordered_idom \<subseteq> ordered_ring_strict ..
    8.39  
    8.40  instance ordered_idom \<subseteq> pordered_comm_ring ..
    8.41 @@ -1901,7 +1906,7 @@
    8.42  
    8.43  lemma mult_sgn_abs: "sgn x * abs x = (x::'a::{ordered_idom,linorder})"
    8.44  using less_linear[of x 0]
    8.45 -by(auto simp: sgn_def abs_if)
    8.46 +by(auto simp: sgn_if abs_if)
    8.47  
    8.48  lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)"
    8.49  by (simp add: abs_if zero_less_one [THEN order_less_not_sym])