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.10 +  using assms by (simp add: add.commute)
    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.15 +  using assms by (simp add: add.commute)
    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.31 +  by (simp add: add.commute)
    1.32 +
    1.33 +lemma mod_mult_self4 [simp]:
    1.34 +  "(b * c + a) mod b = a mod b"
    1.35 +  by (simp add: add.commute)
    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