1.1 --- a/src/HOL/Int.thy	Fri May 07 09:59:59 2010 +0200
     1.2 +++ b/src/HOL/Int.thy	Fri May 07 10:00:24 2010 +0200
     1.3 @@ -2173,6 +2173,25 @@
     1.4    apply (auto simp add: dvd_imp_le)
     1.5    done
     1.6  
     1.7 +lemma zdvd_period:
     1.8 +  fixes a d :: int
     1.9 +  assumes "a dvd d"
    1.10 +  shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)"
    1.11 +proof -
    1.12 +  from assms obtain k where "d = a * k" by (rule dvdE)
    1.13 +  show ?thesis proof
    1.14 +    assume "a dvd (x + t)"
    1.15 +    then obtain l where "x + t = a * l" by (rule dvdE)
    1.16 +    then have "x = a * l - t" by simp
    1.17 +    with `d = a * k` show "a dvd x + c * d + t" by simp
    1.18 +  next
    1.19 +    assume "a dvd x + c * d + t"
    1.20 +    then obtain l where "x + c * d + t = a * l" by (rule dvdE)
    1.21 +    then have "x = a * l - c * d - t" by simp
    1.22 +    with `d = a * k` show "a dvd (x + t)" by simp
    1.23 +  qed
    1.24 +qed
    1.25 +
    1.26  
    1.27  subsection {* Configuration of the code generator *}
    1.28  

     2.1 --- a/src/HOL/Presburger.thy	Fri May 07 09:59:59 2010 +0200
     2.2 +++ b/src/HOL/Presburger.thy	Fri May 07 10:00:24 2010 +0200
     2.3 @@ -457,14 +457,4 @@
     2.4  lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
     2.5  lemma [presburger, algebra]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
     2.6  
     2.7 -
     2.8 -lemma zdvd_period:
     2.9 -  fixes a d :: int
    2.10 -  assumes advdd: "a dvd d"
    2.11 -  shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)"
    2.12 -  using advdd
    2.13 -  apply -
    2.14 -  apply (rule iffI)
    2.15 -  by algebra+
    2.16 -
    2.17  end