# HG changeset patch
# User haftmann
# Date 1483168351 -3600
# Node ID 33d5fa0ce6e550b9315fbc89caa6490c0a4c4e4e
# Parent  53bab28983f1a5050bbf766dfc025305e14767bb
more elementary rules about div / mod on int

diff -r 53bab28983f1 -r 33d5fa0ce6e5 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Fri Dec 30 18:02:27 2016 +0100
+++ b/src/HOL/Divides.thy	Sat Dec 31 08:12:31 2016 +0100
@@ -1823,6 +1823,103 @@
   "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
   by auto
 
+lemma zdiv_int:
+  "int (a div b) = int a div int b"
+  by (simp add: divide_int_def)
+
+lemma zmod_int:
+  "int (a mod b) = int a mod int b"
+  by (simp add: modulo_int_def int_dvd_iff)
+
+lemma div_abs_eq_div_nat:
+  "\<bar>k\<bar> div \<bar>l\<bar> = int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)"
+  by (simp add: divide_int_def)
+
+lemma mod_abs_eq_div_nat:
+  "\<bar>k\<bar> mod \<bar>l\<bar> = int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)"
+  by (simp add: modulo_int_def dvd_int_unfold_dvd_nat)
+
+lemma div_sgn_abs_cancel:
+  fixes k l v :: int
+  assumes "v \<noteq> 0"
+  shows "(sgn v * \<bar>k\<bar>) div (sgn v * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
+proof -
+  from assms have "sgn v = - 1 \<or> sgn v = 1"
+    by (cases "v \<ge> 0") auto
+  then show ?thesis
+  using assms unfolding divide_int_def [of "sgn v * \<bar>k\<bar>" "sgn v * \<bar>l\<bar>"]
+    by (auto simp add: not_less div_abs_eq_div_nat)
+qed
+
+lemma div_eq_sgn_abs:
+  fixes k l v :: int
+  assumes "sgn k = sgn l"
+  shows "k div l = \<bar>k\<bar> div \<bar>l\<bar>"
+proof (cases "l = 0")
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  with assms have "(sgn k * \<bar>k\<bar>) div (sgn l * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
+    by (simp add: div_sgn_abs_cancel)
+  then show ?thesis
+    by (simp add: sgn_mult_abs)
+qed
+
+lemma div_dvd_sgn_abs:
+  fixes k l :: int
+  assumes "l dvd k"
+  shows "k div l = (sgn k * sgn l) * (\<bar>k\<bar> div \<bar>l\<bar>)"
+proof (cases "k = 0")
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  show ?thesis
+  proof (cases "sgn l = sgn k")
+    case True
+    then show ?thesis
+      by (simp add: div_eq_sgn_abs)
+  next
+    case False
+    with \<open>k \<noteq> 0\<close> assms show ?thesis
+      unfolding divide_int_def [of k l]
+        by (auto simp add: zdiv_int)
+  qed
+qed
+
+lemma div_noneq_sgn_abs:
+  fixes k l :: int
+  assumes "l \<noteq> 0"
+  assumes "sgn k \<noteq> sgn l"
+  shows "k div l = - (\<bar>k\<bar> div \<bar>l\<bar>) - of_bool (\<not> l dvd k)"
+  using assms
+  by (simp only: divide_int_def [of k l], auto simp add: not_less zdiv_int)
+  
+lemma sgn_mod:
+  fixes k l :: int
+  assumes "l \<noteq> 0" "\<not> l dvd k"
+  shows "sgn (k mod l) = sgn l"
+proof -
+  from \<open>\<not> l dvd k\<close>
+  have "k mod l \<noteq> 0"
+    by (simp add: dvd_eq_mod_eq_0)
+  show ?thesis
+    using \<open>l \<noteq> 0\<close> \<open>\<not> l dvd k\<close>
+    unfolding modulo_int_def [of k l]
+    by (auto simp add: sgn_1_pos sgn_1_neg mod_greater_zero_iff_not_dvd nat_dvd_iff not_less
+      zless_nat_eq_int_zless [symmetric] elim: nonpos_int_cases)
+qed
+
+lemma abs_mod_less:
+  fixes k l :: int
+  assumes "l \<noteq> 0"
+  shows "\<bar>k mod l\<bar> < \<bar>l\<bar>"
+  using assms unfolding modulo_int_def [of k l]
+  by (auto simp add: not_less int_dvd_iff mod_greater_zero_iff_not_dvd elim: pos_int_cases neg_int_cases nonneg_int_cases nonpos_int_cases)
+
 instance int :: ring_div
 proof
   fix k l s :: int
@@ -1870,12 +1967,6 @@
 
 text\<open>Basic laws about division and remainder\<close>
 
-lemma zdiv_int: "int (a div b) = int a div int b"
-  by (simp add: divide_int_def)
-
-lemma zmod_int: "int (a mod b) = int a mod int b"
-  by (simp add: modulo_int_def int_dvd_iff)
-
 lemma pos_mod_conj: "(0::int) < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b"
   using eucl_rel_int [of a b]
   by (auto simp add: eucl_rel_int_iff prod_eq_iff)
diff -r 53bab28983f1 -r 33d5fa0ce6e5 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Fri Dec 30 18:02:27 2016 +0100
+++ b/src/HOL/Power.thy	Sat Dec 31 08:12:31 2016 +0100
@@ -582,10 +582,22 @@
 context linordered_idom
 begin
 
-lemma power_abs: "\<bar>a ^ n\<bar> = \<bar>a\<bar> ^ n"
-  by (induct n) (auto simp add: abs_mult)
+lemma zero_le_power2 [simp]: "0 \<le> a\<^sup>2"
+  by (simp add: power2_eq_square)
+
+lemma zero_less_power2 [simp]: "0 < a\<^sup>2 \<longleftrightarrow> a \<noteq> 0"
+  by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
 
-lemma abs_power_minus [simp]: "\<bar>(-a) ^ n\<bar> = \<bar>a ^ n\<bar>"
+lemma power2_less_0 [simp]: "\<not> a\<^sup>2 < 0"
+  by (force simp add: power2_eq_square mult_less_0_iff)
+
+lemma power_abs: "\<bar>a ^ n\<bar> = \<bar>a\<bar> ^ n" -- \<open>FIXME simp?\<close>
+  by (induct n) (simp_all add: abs_mult)
+
+lemma power_sgn [simp]: "sgn (a ^ n) = sgn a ^ n"
+  by (induct n) (simp_all add: sgn_mult)
+    
+lemma abs_power_minus [simp]: "\<bar>(- a) ^ n\<bar> = \<bar>a ^ n\<bar>"
   by (simp add: power_abs)
 
 lemma zero_less_power_abs_iff [simp]: "0 < \<bar>a\<bar> ^ n \<longleftrightarrow> a \<noteq> 0 \<or> n = 0"
@@ -600,15 +612,6 @@
 lemma zero_le_power_abs [simp]: "0 \<le> \<bar>a\<bar> ^ n"
   by (rule zero_le_power [OF abs_ge_zero])
 
-lemma zero_le_power2 [simp]: "0 \<le> a\<^sup>2"
-  by (simp add: power2_eq_square)
-
-lemma zero_less_power2 [simp]: "0 < a\<^sup>2 \<longleftrightarrow> a \<noteq> 0"
-  by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
-
-lemma power2_less_0 [simp]: "\<not> a\<^sup>2 < 0"
-  by (force simp add: power2_eq_square mult_less_0_iff)
-
 lemma power2_less_eq_zero_iff [simp]: "a\<^sup>2 \<le> 0 \<longleftrightarrow> a = 0"
   by (simp add: le_less)
 
@@ -618,7 +621,7 @@
 lemma power2_abs [simp]: "\<bar>a\<bar>\<^sup>2 = a\<^sup>2"
   by (simp add: power2_eq_square)
 
-lemma odd_power_less_zero: "a < 0 \<Longrightarrow> a ^ Suc (2*n) < 0"
+lemma odd_power_less_zero: "a < 0 \<Longrightarrow> a ^ Suc (2 * n) < 0"
 proof (induct n)
   case 0
   then show ?case by simp
@@ -630,11 +633,11 @@
     by (simp del: power_Suc add: Suc mult_less_0_iff mult_neg_neg)
 qed
 
-lemma odd_0_le_power_imp_0_le: "0 \<le> a ^ Suc (2*n) \<Longrightarrow> 0 \<le> a"
+lemma odd_0_le_power_imp_0_le: "0 \<le> a ^ Suc (2 * n) \<Longrightarrow> 0 \<le> a"
   using odd_power_less_zero [of a n]
   by (force simp add: linorder_not_less [symmetric])
 
-lemma zero_le_even_power'[simp]: "0 \<le> a ^ (2*n)"
+lemma zero_le_even_power'[simp]: "0 \<le> a ^ (2 * n)"
 proof (induct n)
   case 0
   show ?case by simp