src/HOL/Divides.thy
changeset 69785 9e326f6f8a24
parent 69695 753ae9e9773d
     1.1 --- a/src/HOL/Divides.thy	Sat Feb 02 15:52:14 2019 +0100
     1.2 +++ b/src/HOL/Divides.thy	Mon Feb 04 12:16:03 2019 +0100
     1.3 @@ -881,6 +881,21 @@
     1.4      by (simp_all add: div mod)
     1.5  qed
     1.6  
     1.7 +lemma mod_double_modulus:
     1.8 +  assumes "m > 0" "x \<ge> 0"
     1.9 +  shows   "x mod (2 * m) = x mod m \<or> x mod (2 * m) = x mod m + m"
    1.10 +proof (cases "x mod (2 * m) < m")
    1.11 +  case True
    1.12 +  thus ?thesis using assms using divmod_digit_0(2)[of m x] by auto
    1.13 +next
    1.14 +  case False
    1.15 +  hence *: "x mod (2 * m) - m = x mod m"
    1.16 +    using assms by (intro divmod_digit_1) auto
    1.17 +  hence "x mod (2 * m) = x mod m + m"
    1.18 +    by (subst * [symmetric], subst le_add_diff_inverse2) (use False in auto)
    1.19 +  thus ?thesis by simp
    1.20 +qed
    1.21 +
    1.22  lemma fst_divmod:
    1.23    "fst (divmod m n) = numeral m div numeral n"
    1.24    by (simp add: divmod_def)