author nipkow Sat Sep 01 01:21:48 2007 +0200 (2007-09-01) changeset 24506 020db6ec334a parent 24505 9e6d91f8bb73 child 24507 ac22a2a67100
final(?) iteration of sgn saga.
 src/HOL/Complex/Complex.thy file | annotate | diff | revisions src/HOL/HOL.thy file | annotate | diff | revisions src/HOL/Hyperreal/StarClasses.thy file | annotate | diff | revisions src/HOL/IntDef.thy file | annotate | diff | revisions src/HOL/Real/Rational.thy file | annotate | diff | revisions src/HOL/Real/RealDef.thy file | annotate | diff | revisions src/HOL/Real/RealVector.thy file | annotate | diff | revisions src/HOL/Ring_and_Field.thy file | annotate | diff | revisions
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.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.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.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.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.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.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.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.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.7 +class sgn = type +
2.8 +  fixes sgn :: "'a \<Rightarrow> 'a"
2.9 +
2.10  notation
2.11    uminus  ("- _" [81] 80)
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.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.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.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.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 ..
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.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.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.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.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.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.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.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.10  subsection {* Equivalence relation over positive reals *}
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.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.5  instance real :: norm
7.6    real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>" ..
7.7 +ML"set Toplevel.debug"
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.23  instance real :: real_normed_field
7.24  apply (intro_classes, unfold real_norm_def real_scaleR_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.33  subsection {* Sign function *}
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.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.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.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.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.66  lemma sgn_one [simp]: "sgn (1::'a::real_normed_algebra_1) = 1"
7.67 -unfolding sgn_def by simp
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.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.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.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.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.21  instance ordered_ring_strict \<subseteq> ordered_ring ..
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.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.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.40  instance ordered_idom \<subseteq> pordered_comm_ring ..
8.41 @@ -1901,7 +1906,7 @@
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.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])