src/HOL/Divides.thy
 changeset 54221 56587960e444 parent 53374 a14d2a854c02 child 54226 e3df2a4e02fc
```     1.1 --- a/src/HOL/Divides.thy	Thu Oct 31 11:44:20 2013 +0100
1.2 +++ b/src/HOL/Divides.thy	Thu Oct 31 11:44:20 2013 +0100
1.3 @@ -53,6 +53,16 @@
1.4    shows "(a + b * c) div b = c + a div b"
1.5    using assms div_mult_self1 [of b a c] by (simp add: mult_commute)
1.6
1.7 +lemma div_mult_self3 [simp]:
1.8 +  assumes "b \<noteq> 0"
1.9 +  shows "(c * b + a) div b = c + a div b"
1.11 +
1.12 +lemma div_mult_self4 [simp]:
1.13 +  assumes "b \<noteq> 0"
1.14 +  shows "(b * c + a) div b = c + a div b"
1.16 +
1.17  lemma mod_mult_self1 [simp]: "(a + c * b) mod b = a mod b"
1.18  proof (cases "b = 0")
1.19    case True then show ?thesis by simp
1.20 @@ -70,9 +80,18 @@
1.21    then show ?thesis by simp
1.22  qed
1.23
1.24 -lemma mod_mult_self2 [simp]: "(a + b * c) mod b = a mod b"
1.25 +lemma mod_mult_self2 [simp]:
1.26 +  "(a + b * c) mod b = a mod b"
1.27    by (simp add: mult_commute [of b])
1.28
1.29 +lemma mod_mult_self3 [simp]:
1.30 +  "(c * b + a) mod b = a mod b"
1.32 +
1.33 +lemma mod_mult_self4 [simp]:
1.34 +  "(b * c + a) mod b = a mod b"
1.36 +
1.37  lemma div_mult_self1_is_id [simp]: "b \<noteq> 0 \<Longrightarrow> b * a div b = a"
1.38    using div_mult_self2 [of b 0 a] by simp
1.39
1.40 @@ -477,6 +496,17 @@
1.41  lemma mod_minus1_right [simp]: "a mod (-1) = 0"
1.42    using mod_minus_right [of a 1] by simp
1.43
1.44 +lemma minus_mod_self2 [simp]:
1.45 +  "(a - b) mod b = a mod b"
1.46 +  by (simp add: mod_diff_right_eq)
1.47 +
1.48 +lemma minus_mod_self1 [simp]:
1.49 +  "(b - a) mod b = - a mod b"
1.50 +proof -
1.51 +  have "b - a = - a + b" by (simp add: diff_minus add.commute)
1.52 +  then show ?thesis by simp
1.53 +qed
1.54 +
1.55  end
1.56
1.57
```