more facts on sgn, abs
authorhaftmann
Fri Dec 30 18:02:27 2016 +0100 (2016-12-30)
changeset 647139638c07283bc
parent 64712 38adf0c59c35
child 64714 53bab28983f1
more facts on sgn, abs
src/HOL/Rings.thy
     1.1 --- a/src/HOL/Rings.thy	Fri Dec 30 18:02:27 2016 +0100
     1.2 +++ b/src/HOL/Rings.thy	Fri Dec 30 18:02:27 2016 +0100
     1.3 @@ -2126,6 +2126,49 @@
     1.4  lemma abs_sgn_eq: "\<bar>sgn a\<bar> = (if a = 0 then 0 else 1)"
     1.5    by (simp add: sgn_if)
     1.6  
     1.7 +lemma sgn_mult_self_eq [simp]:
     1.8 +  "sgn a * sgn a = of_bool (a \<noteq> 0)"
     1.9 +  by (cases "a > 0") simp_all
    1.10 +
    1.11 +lemma abs_mult_self_eq [simp]:
    1.12 +  "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
    1.13 +  by (cases "a > 0") simp_all
    1.14 +
    1.15 +lemma same_sgn_sgn_add:
    1.16 +  "sgn (a + b) = sgn a" if "sgn b = sgn a"
    1.17 +proof (cases a 0 rule: linorder_cases)
    1.18 +  case equal
    1.19 +  with that show ?thesis
    1.20 +    by simp
    1.21 +next
    1.22 +  case less
    1.23 +  with that have "b < 0"
    1.24 +    by (simp add: sgn_1_neg)
    1.25 +  with \<open>a < 0\<close> have "a + b < 0"
    1.26 +    by (rule add_neg_neg)
    1.27 +  with \<open>a < 0\<close> show ?thesis
    1.28 +    by simp
    1.29 +next
    1.30 +  case greater
    1.31 +  with that have "b > 0"
    1.32 +    by (simp add: sgn_1_pos)
    1.33 +  with \<open>a > 0\<close> have "a + b > 0"
    1.34 +    by (rule add_pos_pos)
    1.35 +  with \<open>a > 0\<close> show ?thesis
    1.36 +    by simp
    1.37 +qed
    1.38 +
    1.39 +lemma same_sgn_abs_add:
    1.40 +  "\<bar>a + b\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" if "sgn b = sgn a"
    1.41 +proof -
    1.42 +  have "a + b = sgn a * \<bar>a\<bar> + sgn b * \<bar>b\<bar>"
    1.43 +    by (simp add: sgn_mult_abs)
    1.44 +  also have "\<dots> = sgn a * (\<bar>a\<bar> + \<bar>b\<bar>)"
    1.45 +    using that by (simp add: algebra_simps)
    1.46 +  finally show ?thesis
    1.47 +    by (auto simp add: abs_mult)
    1.48 +qed
    1.49 +
    1.50  lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"
    1.51    by (simp add: abs_if)
    1.52