src/HOL/Presburger.thy
changeset 54227 63b441f49645
parent 49962 a8cc904a6820
child 56850 13a7bca533a3
     1.1 --- a/src/HOL/Presburger.thy	Thu Oct 31 11:44:20 2013 +0100
     1.2 +++ b/src/HOL/Presburger.thy	Thu Oct 31 11:44:20 2013 +0100
     1.3 @@ -360,11 +360,15 @@
     1.4    apply simp
     1.5    done
     1.6  
     1.7 -lemma zdvd_mono: assumes not0: "(k::int) \<noteq> 0"
     1.8 -shows "((m::int) dvd t) \<equiv> (k*m dvd k*t)" 
     1.9 -  using not0 by (simp add: dvd_def)
    1.10 +lemma zdvd_mono:
    1.11 +  fixes k m t :: int
    1.12 +  assumes "k \<noteq> 0"
    1.13 +  shows "m dvd t \<equiv> k * m dvd k * t" 
    1.14 +  using assms by simp
    1.15  
    1.16 -lemma uminus_dvd_conv: "(d dvd (t::int)) \<equiv> (-d dvd t)" "(d dvd (t::int)) \<equiv> (d dvd -t)"
    1.17 +lemma uminus_dvd_conv:
    1.18 +  fixes d t :: int
    1.19 +  shows "d dvd t \<equiv> - d dvd t" and "d dvd t \<equiv> d dvd - t"
    1.20    by simp_all
    1.21  
    1.22  text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}
    1.23 @@ -406,24 +410,23 @@
    1.24    end
    1.25  *} "Cooper's algorithm for Presburger arithmetic"
    1.26  
    1.27 -declare dvd_eq_mod_eq_0[symmetric, presburger]
    1.28 -declare mod_1[presburger] 
    1.29 -declare mod_0[presburger]
    1.30 -declare mod_by_1[presburger]
    1.31 -declare mod_self[presburger]
    1.32 -declare mod_by_0[presburger]
    1.33 -declare mod_div_trivial[presburger]
    1.34 -declare div_mod_equality2[presburger]
    1.35 -declare div_mod_equality[presburger]
    1.36 -declare mod_div_equality2[presburger]
    1.37 -declare mod_div_equality[presburger]
    1.38 -declare mod_mult_self1[presburger]
    1.39 -declare mod_mult_self2[presburger]
    1.40 -declare div_mod_equality[presburger]
    1.41 -declare div_mod_equality2[presburger]
    1.42 +declare dvd_eq_mod_eq_0 [symmetric, presburger]
    1.43 +declare mod_1 [presburger] 
    1.44 +declare mod_0 [presburger]
    1.45 +declare mod_by_1 [presburger]
    1.46 +declare mod_self [presburger]
    1.47 +declare div_by_0 [presburger]
    1.48 +declare mod_by_0 [presburger]
    1.49 +declare mod_div_trivial [presburger]
    1.50 +declare div_mod_equality2 [presburger]
    1.51 +declare div_mod_equality [presburger]
    1.52 +declare mod_div_equality2 [presburger]
    1.53 +declare mod_div_equality [presburger]
    1.54 +declare mod_mult_self1 [presburger]
    1.55 +declare mod_mult_self2 [presburger]
    1.56  declare mod2_Suc_Suc[presburger]
    1.57 -lemma [presburger]: "(a::int) div 0 = 0" and [presburger]: "a mod 0 = a"
    1.58 -by simp_all
    1.59 +declare not_mod_2_eq_0_eq_1 [presburger] 
    1.60 +declare nat_zero_less_power_iff [presburger]
    1.61  
    1.62  lemma [presburger, algebra]: "m mod 2 = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger
    1.63  lemma [presburger, algebra]: "m mod 2 = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
    1.64 @@ -432,3 +435,4 @@
    1.65  lemma [presburger, algebra]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
    1.66  
    1.67  end
    1.68 +