# HG changeset patch
# User haftmann
# Date 1273219224 -7200
# Node ID 912080b2c4495dc7bf99db1618b249b2e42600cd
# Parent  47ba1770da8e4a4464bca536807e01444c916907# Parent  a8dc19a352e6354febba914b1f38f49baed75811
merged

diff -r 47ba1770da8e -r 912080b2c449 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Fri May 07 09:59:59 2010 +0200
+++ b/src/HOL/Int.thy	Fri May 07 10:00:24 2010 +0200
@@ -2173,6 +2173,25 @@
   apply (auto simp add: dvd_imp_le)
   done
 
+lemma zdvd_period:
+  fixes a d :: int
+  assumes "a dvd d"
+  shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)"
+proof -
+  from assms obtain k where "d = a * k" by (rule dvdE)
+  show ?thesis proof
+    assume "a dvd (x + t)"
+    then obtain l where "x + t = a * l" by (rule dvdE)
+    then have "x = a * l - t" by simp
+    with `d = a * k` show "a dvd x + c * d + t" by simp
+  next
+    assume "a dvd x + c * d + t"
+    then obtain l where "x + c * d + t = a * l" by (rule dvdE)
+    then have "x = a * l - c * d - t" by simp
+    with `d = a * k` show "a dvd (x + t)" by simp
+  qed
+qed
+
 
 subsection {* Configuration of the code generator *}
 
diff -r 47ba1770da8e -r 912080b2c449 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Fri May 07 09:59:59 2010 +0200
+++ b/src/HOL/Presburger.thy	Fri May 07 10:00:24 2010 +0200
@@ -457,14 +457,4 @@
 lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
 lemma [presburger, algebra]: "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)"
-  using advdd
-  apply -
-  apply (rule iffI)
-  by algebra+
-
 end