# HG changeset patch
# User haftmann
# Date 1184052191 -7200
# Node ID 1b0f4071946c495b89684b9bd169debd14c83d7a
# Parent  8c508c4dc53bcacf98275f2d6300b94bc1949d8a
moved lemma zdvd_period here

diff -r 8c508c4dc53b -r 1b0f4071946c src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Tue Jul 10 09:23:10 2007 +0200
+++ b/src/HOL/Presburger.thy	Tue Jul 10 09:23:11 2007 +0200
@@ -473,6 +473,21 @@
 lemma [presburger]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
 
 
+lemma zdvd_period:
+  fixes a d :: int
+  assumes advdd: "a dvd d"
+  shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)"
+proof-
+  {
+    fix x k
+    from inf_period(3) [OF advdd, rule_format, where x=x and k="-k"]  
+    have "a dvd (x + t) \<longleftrightarrow> a dvd (x + k * d + t)" by simp
+  }
+  hence "\<forall>x.\<forall>k. ((a::int) dvd (x + t)) = (a dvd (x+k*d + t))"  by simp
+  then show ?thesis by simp
+qed
+
+
 subsection {* Code generator setup *}
 
 text {*