# HG changeset patch
# User chaieb
# Date 1181854779 -7200
# Node ID 01ef1135de7333bcea3977548bac72211b8660cf
# Parent  aaca6a8e5414a2259e0155d8bb8c5c87f4b24401
Added some lemmas to default presburger simpset; tuned proofs

diff -r aaca6a8e5414 -r 01ef1135de73 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Thu Jun 14 18:33:31 2007 +0200
+++ b/src/HOL/Presburger.thy	Thu Jun 14 22:59:39 2007 +0200
@@ -408,6 +408,30 @@
   "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)"
   by simp
 
+lemma mod_eq0_dvd_iff[presburger]: "(m::nat) mod n = 0 \<longleftrightarrow> n dvd m"
+unfolding dvd_eq_mod_eq_0[symmetric] ..
+
+lemma zmod_eq0_zdvd_iff[presburger]: "(m::int) mod n = 0 \<longleftrightarrow> n dvd m"
+unfolding zdvd_iff_zmod_eq_0[symmetric] ..
+declare mod_1[presburger]
+declare mod_0[presburger]
+declare zmod_1[presburger]
+declare zmod_zero[presburger]
+declare zmod_self[presburger]
+declare mod_self[presburger]
+declare DIVISION_BY_ZERO_MOD[presburger]
+declare nat_mod_div_trivial[presburger]
+declare div_mod_equality2[presburger]
+declare div_mod_equality[presburger]
+declare mod_div_equality2[presburger]
+declare mod_div_equality[presburger]
+declare mod_mult_self1[presburger]
+declare mod_mult_self2[presburger]
+declare zdiv_zmod_equality2[presburger]
+declare zdiv_zmod_equality[presburger]
+declare mod2_Suc_Suc[presburger]
+lemma [presburger]: "(a::int) div 0 = 0" and [presburger]: "a mod 0 = a"
+using IntDiv.DIVISION_BY_ZERO by blast+
 
 use "Tools/Presburger/cooper.ML"
 oracle linzqe_oracle ("term") = Coopereif.cooper_oracle
@@ -441,6 +465,12 @@
 end
 *} ""
 
+lemma [presburger]: "m mod 2 = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger
+lemma [presburger]: "m mod 2 = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
+lemma [presburger]: "m mod (Suc (Suc 0)) = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger
+lemma [presburger]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
+lemma [presburger]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
+
 subsection {* Code generator setup *}
 text {*
   Presburger arithmetic is convenient to prove some
@@ -448,68 +478,68 @@
 *}
 
 lemma eq_Pls_Pls:
-  "Numeral.Pls = Numeral.Pls \<longleftrightarrow> True" by rule+
+  "Numeral.Pls = Numeral.Pls \<longleftrightarrow> True" by presburger
 
 lemma eq_Pls_Min:
   "Numeral.Pls = Numeral.Min \<longleftrightarrow> False"
-  unfolding Pls_def Min_def by auto
+  unfolding Pls_def Min_def by presburger
 
 lemma eq_Pls_Bit0:
   "Numeral.Pls = Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls = k"
-  unfolding Pls_def Bit_def bit.cases by auto
+  unfolding Pls_def Bit_def bit.cases by presburger
 
 lemma eq_Pls_Bit1:
   "Numeral.Pls = Numeral.Bit k bit.B1 \<longleftrightarrow> False"
-  unfolding Pls_def Bit_def bit.cases by arith
+  unfolding Pls_def Bit_def bit.cases by presburger
 
 lemma eq_Min_Pls:
   "Numeral.Min = Numeral.Pls \<longleftrightarrow> False"
-  unfolding Pls_def Min_def by auto
+  unfolding Pls_def Min_def by presburger
 
 lemma eq_Min_Min:
-  "Numeral.Min = Numeral.Min \<longleftrightarrow> True" by rule+
+  "Numeral.Min = Numeral.Min \<longleftrightarrow> True" by presburger
 
 lemma eq_Min_Bit0:
   "Numeral.Min = Numeral.Bit k bit.B0 \<longleftrightarrow> False"
-  unfolding Min_def Bit_def bit.cases by arith
+  unfolding Min_def Bit_def bit.cases by presburger
 
 lemma eq_Min_Bit1:
   "Numeral.Min = Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min = k"
-  unfolding Min_def Bit_def bit.cases by auto
+  unfolding Min_def Bit_def bit.cases by presburger
 
 lemma eq_Bit0_Pls:
   "Numeral.Bit k bit.B0 = Numeral.Pls \<longleftrightarrow> Numeral.Pls = k"
-  unfolding Pls_def Bit_def bit.cases by auto
+  unfolding Pls_def Bit_def bit.cases by presburger
 
 lemma eq_Bit1_Pls:
   "Numeral.Bit k bit.B1 = Numeral.Pls \<longleftrightarrow> False"
-  unfolding Pls_def Bit_def bit.cases by arith
+  unfolding Pls_def Bit_def bit.cases  by presburger
 
 lemma eq_Bit0_Min:
   "Numeral.Bit k bit.B0 = Numeral.Min \<longleftrightarrow> False"
-  unfolding Min_def Bit_def bit.cases by arith
+  unfolding Min_def Bit_def bit.cases  by presburger
 
 lemma eq_Bit1_Min:
   "(Numeral.Bit k bit.B1) = Numeral.Min \<longleftrightarrow> Numeral.Min = k"
-  unfolding Min_def Bit_def bit.cases by auto
+  unfolding Min_def Bit_def bit.cases  by presburger
 
 lemma eq_Bit_Bit:
   "Numeral.Bit k1 v1 = Numeral.Bit k2 v2 \<longleftrightarrow>
-    v1 = v2 \<and> k1 = k2"
+    v1 = v2 \<and> k1 = k2" 
   unfolding Bit_def
   apply (cases v1)
   apply (cases v2)
   apply auto
-  apply arith
+  apply presburger
   apply (cases v2)
   apply auto
-  apply arith
+  apply presburger
   apply (cases v2)
   apply auto
 done
 
 lemma eq_number_of:
-  "(number_of k \<Colon> int) = number_of l \<longleftrightarrow> k = l"
+  "(number_of k \<Colon> int) = number_of l \<longleftrightarrow> k = l" 
   unfolding number_of_is_id ..
 
 
@@ -518,7 +548,7 @@
 
 lemma less_eq_Pls_Min:
   "Numeral.Pls \<le> Numeral.Min \<longleftrightarrow> False"
-  unfolding Pls_def Min_def by auto
+  unfolding Pls_def Min_def by presburger
 
 lemma less_eq_Pls_Bit:
   "Numeral.Pls \<le> Numeral.Bit k v \<longleftrightarrow> Numeral.Pls \<le> k"
@@ -526,7 +556,7 @@
 
 lemma less_eq_Min_Pls:
   "Numeral.Min \<le> Numeral.Pls \<longleftrightarrow> True"
-  unfolding Pls_def Min_def by auto
+  unfolding Pls_def Min_def by presburger
 
 lemma less_eq_Min_Min:
   "Numeral.Min \<le> Numeral.Min \<longleftrightarrow> True" by rule+
@@ -569,11 +599,11 @@
 
 
 lemma less_Pls_Pls:
-  "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by auto
+  "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by presburger 
 
 lemma less_Pls_Min:
   "Numeral.Pls < Numeral.Min \<longleftrightarrow> False"
-  unfolding Pls_def Min_def by auto
+  unfolding Pls_def Min_def  by presburger 
 
 lemma less_Pls_Bit0:
   "Numeral.Pls < Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls < k"
@@ -585,10 +615,10 @@
 
 lemma less_Min_Pls:
   "Numeral.Min < Numeral.Pls \<longleftrightarrow> True"
-  unfolding Pls_def Min_def by auto
+  unfolding Pls_def Min_def by presburger 
 
 lemma less_Min_Min:
-  "Numeral.Min < Numeral.Min \<longleftrightarrow> False" by auto
+  "Numeral.Min < Numeral.Min \<longleftrightarrow> False"  by presburger 
 
 lemma less_Min_Bit:
   "Numeral.Min < Numeral.Bit k v \<longleftrightarrow> Numeral.Min < k"
@@ -616,7 +646,7 @@
 
 lemma less_Bit0_Bit1:
   "Numeral.Bit k1 bit.B0 < Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
-  unfolding Bit_def bit.cases by auto
+  unfolding Bit_def bit.cases  by arith
 
 lemma less_number_of:
   "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"