src/HOL/Presburger.thy
 changeset 27668 6eb20b2cecf8 parent 27651 16a26996c30e child 28290 4cc2b6046258
```     1.1 --- a/src/HOL/Presburger.thy	Mon Jul 21 13:36:44 2008 +0200
1.2 +++ b/src/HOL/Presburger.thy	Mon Jul 21 13:36:59 2008 +0200
1.3 @@ -62,7 +62,8 @@
1.4    "\<forall>x k. F = F"
1.5  apply (auto elim!: dvdE simp add: ring_simps)
1.6  unfolding mult_assoc [symmetric] left_distrib [symmetric] left_diff_distrib [symmetric]
1.7 -unfolding dvd_def mult_commute [of d] by auto
1.8 +unfolding dvd_def mult_commute [of d]
1.9 +by auto
1.10
1.11  subsection{* The A and B sets *}
1.12  lemma bset:
1.13 @@ -84,12 +85,13 @@
1.14  proof (blast, blast)
1.15    assume dp: "D > 0" and tB: "t - 1\<in> B"
1.16    show "(\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x = t) \<longrightarrow> (x - D = t))"
1.17 -    apply (rule allI, rule impI,erule ballE[where x="1"],erule ballE[where x="t - 1"])
1.18 -    using dp tB by simp_all
1.19 +    apply (rule allI, rule impI,erule ballE[where x="1"],erule ballE[where x="t - 1"])
1.20 +    apply algebra using dp tB by simp_all
1.21  next
1.22    assume dp: "D > 0" and tB: "t \<in> B"
1.23    show "(\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x \<noteq> t) \<longrightarrow> (x - D \<noteq> t))"
1.24      apply (rule allI, rule impI,erule ballE[where x="D"],erule ballE[where x="t"])
1.25 +    apply algebra
1.26      using dp tB by simp_all
1.27  next
1.28    assume dp: "D > 0" thus "(\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x < t) \<longrightarrow> (x - D < t))" by arith
1.29 @@ -113,9 +115,7 @@
1.30    thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x \<ge> t) \<longrightarrow> (x - D \<ge> t)" by blast
1.31  next
1.32    assume d: "d dvd D"
1.33 -  {fix x assume H: "d dvd x + t" with d have "d dvd (x - D) + t"
1.34 -      by (auto elim!: dvdE simp add: ring_simps)
1.35 -        (auto simp only: left_diff_distrib [symmetric] dvd_def mult_commute)}
1.36 +  {fix x assume H: "d dvd x + t" with d have "d dvd (x - D) + t" by algebra}
1.37    thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (d dvd x+t) \<longrightarrow> (d dvd (x - D) + t)" by simp
1.38  next
1.39    assume d: "d dvd D"
1.40 @@ -470,25 +470,20 @@
1.41  end
1.42  *} "Cooper's algorithm for Presburger arithmetic"
1.43
1.44 -lemma [presburger]: "m mod 2 = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger
1.45 -lemma [presburger]: "m mod 2 = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
1.46 -lemma [presburger]: "m mod (Suc (Suc 0)) = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger
1.47 -lemma [presburger]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
1.48 -lemma [presburger]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
1.49 +lemma [presburger, algebra]: "m mod 2 = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger
1.50 +lemma [presburger, algebra]: "m mod 2 = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
1.51 +lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger
1.52 +lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
1.53 +lemma [presburger, algebra]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
1.54
1.55
1.56  lemma zdvd_period:
1.57    fixes a d :: int
1.58    assumes advdd: "a dvd d"
1.59    shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)"
1.60 -proof-
1.61 -  {
1.62 -    fix x k
1.63 -    from inf_period(3) [OF advdd, rule_format, where x=x and k="-k"]
1.64 -    have "a dvd (x + t) \<longleftrightarrow> a dvd (x + k * d + t)" by simp
1.65 -  }
1.66 -  hence "\<forall>x.\<forall>k. ((a::int) dvd (x + t)) = (a dvd (x+k*d + t))"  by simp
1.67 -  then show ?thesis by simp
1.68 -qed