--- 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 *}
--- 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