src/HOL/Presburger.thy
changeset 23390 01ef1135de73
parent 23389 aaca6a8e5414
child 23405 8993b3144358
     1.1 --- a/src/HOL/Presburger.thy	Thu Jun 14 18:33:31 2007 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Thu Jun 14 22:59:39 2007 +0200
     1.3 @@ -408,6 +408,30 @@
     1.4    "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)"
     1.5    by simp
     1.6  
     1.7 +lemma mod_eq0_dvd_iff[presburger]: "(m::nat) mod n = 0 \<longleftrightarrow> n dvd m"
     1.8 +unfolding dvd_eq_mod_eq_0[symmetric] ..
     1.9 +
    1.10 +lemma zmod_eq0_zdvd_iff[presburger]: "(m::int) mod n = 0 \<longleftrightarrow> n dvd m"
    1.11 +unfolding zdvd_iff_zmod_eq_0[symmetric] ..
    1.12 +declare mod_1[presburger]
    1.13 +declare mod_0[presburger]
    1.14 +declare zmod_1[presburger]
    1.15 +declare zmod_zero[presburger]
    1.16 +declare zmod_self[presburger]
    1.17 +declare mod_self[presburger]
    1.18 +declare DIVISION_BY_ZERO_MOD[presburger]
    1.19 +declare nat_mod_div_trivial[presburger]
    1.20 +declare div_mod_equality2[presburger]
    1.21 +declare div_mod_equality[presburger]
    1.22 +declare mod_div_equality2[presburger]
    1.23 +declare mod_div_equality[presburger]
    1.24 +declare mod_mult_self1[presburger]
    1.25 +declare mod_mult_self2[presburger]
    1.26 +declare zdiv_zmod_equality2[presburger]
    1.27 +declare zdiv_zmod_equality[presburger]
    1.28 +declare mod2_Suc_Suc[presburger]
    1.29 +lemma [presburger]: "(a::int) div 0 = 0" and [presburger]: "a mod 0 = a"
    1.30 +using IntDiv.DIVISION_BY_ZERO by blast+
    1.31  
    1.32  use "Tools/Presburger/cooper.ML"
    1.33  oracle linzqe_oracle ("term") = Coopereif.cooper_oracle
    1.34 @@ -441,6 +465,12 @@
    1.35  end
    1.36  *} ""
    1.37  
    1.38 +lemma [presburger]: "m mod 2 = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger
    1.39 +lemma [presburger]: "m mod 2 = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
    1.40 +lemma [presburger]: "m mod (Suc (Suc 0)) = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger
    1.41 +lemma [presburger]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
    1.42 +lemma [presburger]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
    1.43 +
    1.44  subsection {* Code generator setup *}
    1.45  text {*
    1.46    Presburger arithmetic is convenient to prove some
    1.47 @@ -448,68 +478,68 @@
    1.48  *}
    1.49  
    1.50  lemma eq_Pls_Pls:
    1.51 -  "Numeral.Pls = Numeral.Pls \<longleftrightarrow> True" by rule+
    1.52 +  "Numeral.Pls = Numeral.Pls \<longleftrightarrow> True" by presburger
    1.53  
    1.54  lemma eq_Pls_Min:
    1.55    "Numeral.Pls = Numeral.Min \<longleftrightarrow> False"
    1.56 -  unfolding Pls_def Min_def by auto
    1.57 +  unfolding Pls_def Min_def by presburger
    1.58  
    1.59  lemma eq_Pls_Bit0:
    1.60    "Numeral.Pls = Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls = k"
    1.61 -  unfolding Pls_def Bit_def bit.cases by auto
    1.62 +  unfolding Pls_def Bit_def bit.cases by presburger
    1.63  
    1.64  lemma eq_Pls_Bit1:
    1.65    "Numeral.Pls = Numeral.Bit k bit.B1 \<longleftrightarrow> False"
    1.66 -  unfolding Pls_def Bit_def bit.cases by arith
    1.67 +  unfolding Pls_def Bit_def bit.cases by presburger
    1.68  
    1.69  lemma eq_Min_Pls:
    1.70    "Numeral.Min = Numeral.Pls \<longleftrightarrow> False"
    1.71 -  unfolding Pls_def Min_def by auto
    1.72 +  unfolding Pls_def Min_def by presburger
    1.73  
    1.74  lemma eq_Min_Min:
    1.75 -  "Numeral.Min = Numeral.Min \<longleftrightarrow> True" by rule+
    1.76 +  "Numeral.Min = Numeral.Min \<longleftrightarrow> True" by presburger
    1.77  
    1.78  lemma eq_Min_Bit0:
    1.79    "Numeral.Min = Numeral.Bit k bit.B0 \<longleftrightarrow> False"
    1.80 -  unfolding Min_def Bit_def bit.cases by arith
    1.81 +  unfolding Min_def Bit_def bit.cases by presburger
    1.82  
    1.83  lemma eq_Min_Bit1:
    1.84    "Numeral.Min = Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min = k"
    1.85 -  unfolding Min_def Bit_def bit.cases by auto
    1.86 +  unfolding Min_def Bit_def bit.cases by presburger
    1.87  
    1.88  lemma eq_Bit0_Pls:
    1.89    "Numeral.Bit k bit.B0 = Numeral.Pls \<longleftrightarrow> Numeral.Pls = k"
    1.90 -  unfolding Pls_def Bit_def bit.cases by auto
    1.91 +  unfolding Pls_def Bit_def bit.cases by presburger
    1.92  
    1.93  lemma eq_Bit1_Pls:
    1.94    "Numeral.Bit k bit.B1 = Numeral.Pls \<longleftrightarrow> False"
    1.95 -  unfolding Pls_def Bit_def bit.cases by arith
    1.96 +  unfolding Pls_def Bit_def bit.cases  by presburger
    1.97  
    1.98  lemma eq_Bit0_Min:
    1.99    "Numeral.Bit k bit.B0 = Numeral.Min \<longleftrightarrow> False"
   1.100 -  unfolding Min_def Bit_def bit.cases by arith
   1.101 +  unfolding Min_def Bit_def bit.cases  by presburger
   1.102  
   1.103  lemma eq_Bit1_Min:
   1.104    "(Numeral.Bit k bit.B1) = Numeral.Min \<longleftrightarrow> Numeral.Min = k"
   1.105 -  unfolding Min_def Bit_def bit.cases by auto
   1.106 +  unfolding Min_def Bit_def bit.cases  by presburger
   1.107  
   1.108  lemma eq_Bit_Bit:
   1.109    "Numeral.Bit k1 v1 = Numeral.Bit k2 v2 \<longleftrightarrow>
   1.110 -    v1 = v2 \<and> k1 = k2"
   1.111 +    v1 = v2 \<and> k1 = k2" 
   1.112    unfolding Bit_def
   1.113    apply (cases v1)
   1.114    apply (cases v2)
   1.115    apply auto
   1.116 -  apply arith
   1.117 +  apply presburger
   1.118    apply (cases v2)
   1.119    apply auto
   1.120 -  apply arith
   1.121 +  apply presburger
   1.122    apply (cases v2)
   1.123    apply auto
   1.124  done
   1.125  
   1.126  lemma eq_number_of:
   1.127 -  "(number_of k \<Colon> int) = number_of l \<longleftrightarrow> k = l"
   1.128 +  "(number_of k \<Colon> int) = number_of l \<longleftrightarrow> k = l" 
   1.129    unfolding number_of_is_id ..
   1.130  
   1.131  
   1.132 @@ -518,7 +548,7 @@
   1.133  
   1.134  lemma less_eq_Pls_Min:
   1.135    "Numeral.Pls \<le> Numeral.Min \<longleftrightarrow> False"
   1.136 -  unfolding Pls_def Min_def by auto
   1.137 +  unfolding Pls_def Min_def by presburger
   1.138  
   1.139  lemma less_eq_Pls_Bit:
   1.140    "Numeral.Pls \<le> Numeral.Bit k v \<longleftrightarrow> Numeral.Pls \<le> k"
   1.141 @@ -526,7 +556,7 @@
   1.142  
   1.143  lemma less_eq_Min_Pls:
   1.144    "Numeral.Min \<le> Numeral.Pls \<longleftrightarrow> True"
   1.145 -  unfolding Pls_def Min_def by auto
   1.146 +  unfolding Pls_def Min_def by presburger
   1.147  
   1.148  lemma less_eq_Min_Min:
   1.149    "Numeral.Min \<le> Numeral.Min \<longleftrightarrow> True" by rule+
   1.150 @@ -569,11 +599,11 @@
   1.151  
   1.152  
   1.153  lemma less_Pls_Pls:
   1.154 -  "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by auto
   1.155 +  "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by presburger 
   1.156  
   1.157  lemma less_Pls_Min:
   1.158    "Numeral.Pls < Numeral.Min \<longleftrightarrow> False"
   1.159 -  unfolding Pls_def Min_def by auto
   1.160 +  unfolding Pls_def Min_def  by presburger 
   1.161  
   1.162  lemma less_Pls_Bit0:
   1.163    "Numeral.Pls < Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls < k"
   1.164 @@ -585,10 +615,10 @@
   1.165  
   1.166  lemma less_Min_Pls:
   1.167    "Numeral.Min < Numeral.Pls \<longleftrightarrow> True"
   1.168 -  unfolding Pls_def Min_def by auto
   1.169 +  unfolding Pls_def Min_def by presburger 
   1.170  
   1.171  lemma less_Min_Min:
   1.172 -  "Numeral.Min < Numeral.Min \<longleftrightarrow> False" by auto
   1.173 +  "Numeral.Min < Numeral.Min \<longleftrightarrow> False"  by presburger 
   1.174  
   1.175  lemma less_Min_Bit:
   1.176    "Numeral.Min < Numeral.Bit k v \<longleftrightarrow> Numeral.Min < k"
   1.177 @@ -616,7 +646,7 @@
   1.178  
   1.179  lemma less_Bit0_Bit1:
   1.180    "Numeral.Bit k1 bit.B0 < Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
   1.181 -  unfolding Bit_def bit.cases by auto
   1.182 +  unfolding Bit_def bit.cases  by arith
   1.183  
   1.184  lemma less_number_of:
   1.185    "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"