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")