author haftmann Fri, 07 May 2010 09:51:55 +0200 changeset 36749 a8dc19a352e6 parent 36724 5779d9fbedd0 child 36750 912080b2c449
moved lemma zdvd_period to theory Int
 src/HOL/Int.thy file | annotate | diff | comparison | revisions src/HOL/Presburger.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Int.thy	Thu May 06 23:37:07 2010 +0200
+++ b/src/HOL/Int.thy	Fri May 07 09:51:55 2010 +0200
@@ -2173,6 +2173,25 @@
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	Thu May 06 23:37:07 2010 +0200
+++ b/src/HOL/Presburger.thy	Fri May 07 09:51:55 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)"