# HG changeset patch
# User haftmann
# Date 1383216260 -3600
# Node ID 56587960e444f5bd5585cb19f35c548830d3db04
# Parent  0e6645622f22ad199ce50b72fa3aff0637d88818
more lemmas on division

diff -r 0e6645622f22 -r 56587960e444 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu Oct 31 11:44:20 2013 +0100
+++ b/src/HOL/Divides.thy	Thu Oct 31 11:44:20 2013 +0100
@@ -53,6 +53,16 @@
   shows "(a + b * c) div b = c + a div b"
   using assms div_mult_self1 [of b a c] by (simp add: mult_commute)
 
+lemma div_mult_self3 [simp]:
+  assumes "b \<noteq> 0"
+  shows "(c * b + a) div b = c + a div b"
+  using assms by (simp add: add.commute)
+
+lemma div_mult_self4 [simp]:
+  assumes "b \<noteq> 0"
+  shows "(b * c + a) div b = c + a div b"
+  using assms by (simp add: add.commute)
+
 lemma mod_mult_self1 [simp]: "(a + c * b) mod b = a mod b"
 proof (cases "b = 0")
   case True then show ?thesis by simp
@@ -70,9 +80,18 @@
   then show ?thesis by simp
 qed
 
-lemma mod_mult_self2 [simp]: "(a + b * c) mod b = a mod b"
+lemma mod_mult_self2 [simp]: 
+  "(a + b * c) mod b = a mod b"
   by (simp add: mult_commute [of b])
 
+lemma mod_mult_self3 [simp]:
+  "(c * b + a) mod b = a mod b"
+  by (simp add: add.commute)
+
+lemma mod_mult_self4 [simp]:
+  "(b * c + a) mod b = a mod b"
+  by (simp add: add.commute)
+
 lemma div_mult_self1_is_id [simp]: "b \<noteq> 0 \<Longrightarrow> b * a div b = a"
   using div_mult_self2 [of b 0 a] by simp
 
@@ -477,6 +496,17 @@
 lemma mod_minus1_right [simp]: "a mod (-1) = 0"
   using mod_minus_right [of a 1] by simp
 
+lemma minus_mod_self2 [simp]: 
+  "(a - b) mod b = a mod b"
+  by (simp add: mod_diff_right_eq)
+
+lemma minus_mod_self1 [simp]: 
+  "(b - a) mod b = - a mod b"
+proof -
+  have "b - a = - a + b" by (simp add: diff_minus add.commute)
+  then show ?thesis by simp
+qed
+
 end
 
 
diff -r 0e6645622f22 -r 56587960e444 src/HOL/Old_Number_Theory/Pocklington.thy
--- a/src/HOL/Old_Number_Theory/Pocklington.thy	Thu Oct 31 11:44:20 2013 +0100
+++ b/src/HOL/Old_Number_Theory/Pocklington.thy	Thu Oct 31 11:44:20 2013 +0100
@@ -348,15 +348,11 @@
   let ?w = "x mod (a*b)"
   have wab: "?w < a*b" by (simp add: mod_less_divisor[OF abpos])
   from xq12(1) have "?w mod a = ((m + q1 * a) mod (a*b)) mod a" by simp
-  also have "\<dots> = m mod a" apply (simp add: mod_mult2_eq)
-    apply (subst mod_add_left_eq)
-    by simp
+  also have "\<dots> = m mod a" by (simp add: mod_mult2_eq)
   finally have th1: "[?w = m] (mod a)" by (simp add: modeq_def)
   from xq12(2) have "?w mod b = ((n + q2 * b) mod (a*b)) mod b" by simp
   also have "\<dots> = ((n + q2 * b) mod (b*a)) mod b" by (simp add: mult_commute)
-  also have "\<dots> = n mod b" apply (simp add: mod_mult2_eq)
-    apply (subst mod_add_left_eq)
-    by simp
+  also have "\<dots> = n mod b" by (simp add: mod_mult2_eq)
   finally have th2: "[?w = n] (mod b)" by (simp add: modeq_def)
   {fix y assume H: "y < a*b" "[y = m] (mod a)" "[y = n] (mod b)"
     with th1 th2 have H': "[y = ?w] (mod a)" "[y = ?w] (mod b)"
diff -r 0e6645622f22 -r 56587960e444 src/HOL/Word/Misc_Numeric.thy
--- a/src/HOL/Word/Misc_Numeric.thy	Thu Oct 31 11:44:20 2013 +0100
+++ b/src/HOL/Word/Misc_Numeric.thy	Thu Oct 31 11:44:20 2013 +0100
@@ -8,10 +8,6 @@
 imports Main Parity
 begin
 
-lemma zmod_zsub_self [simp]: (* FIXME move to Divides.thy *) 
-  "((b :: int) - a) mod a = b mod a"
-  by (simp add: mod_diff_right_eq)
-
 declare iszero_0 [iff]
 
 lemma min_pm [simp]: "min a b + (a - b) = (a :: nat)" by arith
diff -r 0e6645622f22 -r 56587960e444 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Thu Oct 31 11:44:20 2013 +0100
+++ b/src/HOL/Word/Word.thy	Thu Oct 31 11:44:20 2013 +0100
@@ -4238,7 +4238,7 @@
 
 lemma max_word_max [simp,intro!]: "n \<le> max_word"
   by (cases n rule: word_int_cases)
-     (simp add: max_word_def word_le_def int_word_uint int_mod_eq')
+    (simp add: max_word_def word_le_def int_word_uint int_mod_eq' del: minus_mod_self1)
   
 lemma word_of_int_2p_len: "word_of_int (2 ^ len_of TYPE('a)) = (0::'a::len0 word)"
   by (subst word_uint.Abs_norm [symmetric]) simp