1.1 --- a/src/HOL/Presburger.thy	Tue Jul 10 09:23:10 2007 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Tue Jul 10 09:23:11 2007 +0200
     1.3 @@ -473,6 +473,21 @@
     1.4  lemma [presburger]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
     1.5  
     1.6  
     1.7 +lemma zdvd_period:
     1.8 +  fixes a d :: int
     1.9 +  assumes advdd: "a dvd d"
    1.10 +  shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)"
    1.11 +proof-
    1.12 +  {
    1.13 +    fix x k
    1.14 +    from inf_period(3) [OF advdd, rule_format, where x=x and k="-k"]  
    1.15 +    have "a dvd (x + t) \<longleftrightarrow> a dvd (x + k * d + t)" by simp
    1.16 +  }
    1.17 +  hence "\<forall>x.\<forall>k. ((a::int) dvd (x + t)) = (a dvd (x+k*d + t))"  by simp
    1.18 +  then show ?thesis by simp
    1.19 +qed
    1.20 +
    1.21 +
    1.22  subsection {* Code generator setup *}
    1.23  
    1.24  text {*