author haftmann Fri Dec 30 18:02:27 2016 +0100 (2016-12-30) changeset 64713 9638c07283bc parent 64712 38adf0c59c35 child 64714 53bab28983f1
more facts on sgn, abs
 src/HOL/Rings.thy file | annotate | diff | revisions
```     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
```