author haftmann Fri May 07 09:51:55 2010 +0200 (2010-05-07) changeset 36749 a8dc19a352e6 parent 36724 5779d9fbedd0 child 36750 912080b2c449
moved lemma zdvd_period to theory Int
 src/HOL/Int.thy file | annotate | diff | revisions src/HOL/Presburger.thy file | annotate | diff | revisions
1.1 --- a/src/HOL/Int.thy	Thu May 06 23:37:07 2010 +0200
1.2 +++ b/src/HOL/Int.thy	Fri May 07 09:51:55 2010 +0200
1.3 @@ -2173,6 +2173,25 @@
1.4    apply (auto simp add: dvd_imp_le)
1.5    done
1.7 +lemma zdvd_period:
1.8 +  fixes a d :: int
1.9 +  assumes "a dvd d"
1.10 +  shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)"
1.11 +proof -
1.12 +  from assms obtain k where "d = a * k" by (rule dvdE)
1.13 +  show ?thesis proof
1.14 +    assume "a dvd (x + t)"
1.15 +    then obtain l where "x + t = a * l" by (rule dvdE)
1.16 +    then have "x = a * l - t" by simp
1.17 +    with `d = a * k` show "a dvd x + c * d + t" by simp
1.18 +  next
1.19 +    assume "a dvd x + c * d + t"
1.20 +    then obtain l where "x + c * d + t = a * l" by (rule dvdE)
1.21 +    then have "x = a * l - c * d - t" by simp
1.22 +    with `d = a * k` show "a dvd (x + t)" by simp
1.23 +  qed
1.24 +qed
1.25 +
1.27  subsection {* Configuration of the code generator *}
2.1 --- a/src/HOL/Presburger.thy	Thu May 06 23:37:07 2010 +0200
2.2 +++ b/src/HOL/Presburger.thy	Fri May 07 09:51:55 2010 +0200
2.3 @@ -457,14 +457,4 @@
2.4  lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
2.5  lemma [presburger, algebra]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
2.7 -
2.8 -lemma zdvd_period:
2.9 -  fixes a d :: int
2.10 -  assumes advdd: "a dvd d"
2.11 -  shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)"