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
    1.69 +  using advdd
    1.70 +  apply -
    1.71 +  apply (rule iffI)
    1.72 +  by algebra+
    1.73  
    1.74  end