src/HOL/Divides.thy
 changeset 66837 6ba663ff2b1c parent 66817 0b12755ccbb2 child 66886 960509bfd47e
```     1.1 --- a/src/HOL/Divides.thy	Mon Oct 09 19:10:47 2017 +0200
1.2 +++ b/src/HOL/Divides.thy	Mon Oct 09 19:10:48 2017 +0200
1.3 @@ -1164,16 +1164,40 @@
1.4  apply (rule div_less_dividend, simp_all)
1.5  done
1.6
1.7 -lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y mod n" and xy:"y \<le> x"
1.8 +lemma mod_eq_dvd_iff_nat:
1.9 +  "m mod q = n mod q \<longleftrightarrow> q dvd m - n" if "m \<ge> n" for m n q :: nat
1.10 +proof -
1.11 +  have "int m mod int q = int n mod int q \<longleftrightarrow> int q dvd int m - int n"
1.12 +    by (simp add: mod_eq_dvd_iff)
1.13 +  with that have "int (m mod q) = int (n mod q) \<longleftrightarrow> int q dvd int (m - n)"
1.14 +    by (simp only: of_nat_mod of_nat_diff)
1.15 +  then show ?thesis
1.16 +    by (simp add: zdvd_int)
1.17 +qed
1.18 +
1.19 +lemma mod_eq_nat1E:
1.20 +  fixes m n q :: nat
1.21 +  assumes "m mod q = n mod q" and "m \<ge> n"
1.22 +  obtains s where "m = n + q * s"
1.23 +proof -
1.24 +  from assms have "q dvd m - n"
1.25 +    by (simp add: mod_eq_dvd_iff_nat)
1.26 +  then obtain s where "m - n = q * s" ..
1.27 +  with \<open>m \<ge> n\<close> have "m = n + q * s"
1.28 +    by simp
1.29 +  with that show thesis .
1.30 +qed
1.31 +
1.32 +lemma mod_eq_nat2E:
1.33 +  fixes m n q :: nat
1.34 +  assumes "m mod q = n mod q" and "n \<ge> m"
1.35 +  obtains s where "n = m + q * s"
1.36 +  using assms mod_eq_nat1E [of n q m] by (auto simp add: ac_simps)
1.37 +
1.38 +lemma nat_mod_eq_lemma:
1.39 +  assumes "(x::nat) mod n = y mod n" and "y \<le> x"
1.40    shows "\<exists>q. x = y + n * q"
1.41 -proof-
1.42 -  from xy have th: "int x - int y = int (x - y)" by simp
1.43 -  from xyn have "int x mod int n = int y mod int n"
1.44 -    by (simp add: zmod_int [symmetric])
1.45 -  hence "int n dvd int x - int y" by (simp only: mod_eq_dvd_iff [symmetric])
1.46 -  hence "n dvd x - y" by (simp add: th zdvd_int)
1.47 -  then show ?thesis using xy unfolding dvd_def apply clarsimp apply (rule_tac x="k" in exI) by arith
1.48 -qed
1.49 +  using assms by (rule mod_eq_nat1E) rule
1.50
1.51  lemma nat_mod_eq_iff: "(x::nat) mod n = y mod n \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)"
1.52    (is "?lhs = ?rhs")
```