# HG changeset patch
# User haftmann
# Date 1483117347 -3600
# Node ID 9638c07283bc4d8a5dd1f996c6c6e1b02d798058
# Parent  38adf0c59c35b7faebb1a624dfad47fb07487bf5
more facts on sgn, abs

diff -r 38adf0c59c35 -r 9638c07283bc src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Fri Dec 30 18:02:27 2016 +0100
+++ b/src/HOL/Rings.thy	Fri Dec 30 18:02:27 2016 +0100
@@ -2126,6 +2126,49 @@
 lemma abs_sgn_eq: "\<bar>sgn a\<bar> = (if a = 0 then 0 else 1)"
   by (simp add: sgn_if)
 
+lemma sgn_mult_self_eq [simp]:
+  "sgn a * sgn a = of_bool (a \<noteq> 0)"
+  by (cases "a > 0") simp_all
+
+lemma abs_mult_self_eq [simp]:
+  "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
+  by (cases "a > 0") simp_all
+
+lemma same_sgn_sgn_add:
+  "sgn (a + b) = sgn a" if "sgn b = sgn a"
+proof (cases a 0 rule: linorder_cases)
+  case equal
+  with that show ?thesis
+    by simp
+next
+  case less
+  with that have "b < 0"
+    by (simp add: sgn_1_neg)
+  with \<open>a < 0\<close> have "a + b < 0"
+    by (rule add_neg_neg)
+  with \<open>a < 0\<close> show ?thesis
+    by simp
+next
+  case greater
+  with that have "b > 0"
+    by (simp add: sgn_1_pos)
+  with \<open>a > 0\<close> have "a + b > 0"
+    by (rule add_pos_pos)
+  with \<open>a > 0\<close> show ?thesis
+    by simp
+qed
+
+lemma same_sgn_abs_add:
+  "\<bar>a + b\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" if "sgn b = sgn a"
+proof -
+  have "a + b = sgn a * \<bar>a\<bar> + sgn b * \<bar>b\<bar>"
+    by (simp add: sgn_mult_abs)
+  also have "\<dots> = sgn a * (\<bar>a\<bar> + \<bar>b\<bar>)"
+    using that by (simp add: algebra_simps)
+  finally show ?thesis
+    by (auto simp add: abs_mult)
+qed
+
 lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"
   by (simp add: abs_if)