src/HOL/Presburger.thy

--- a/src/HOL/Presburger.thy	Mon May 10 12:25:49 2010 +0200
+++ b/src/HOL/Presburger.thy	Mon May 10 13:58:18 2010 +0200
@@ -8,14 +8,11 @@
 imports Groebner_Basis SetInterval
 uses
   "Tools/Qelim/qelim.ML"
-  "Tools/Qelim/cooper_data.ML"
-  "Tools/Qelim/generated_cooper.ML"
+  "Tools/Qelim/cooper_procedure.ML"
   ("Tools/Qelim/cooper.ML")
   ("Tools/Qelim/presburger.ML")
 begin
 
-setup CooperData.setup
-
 subsection{* The @{text "-\<infinity>"} and @{text "+\<infinity>"} Properties *}
 
 
@@ -405,28 +402,9 @@
   "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)"
   by (rule eq_number_of_eq)
 
-declare dvd_eq_mod_eq_0[symmetric, presburger]
-declare mod_1[presburger] 
-declare mod_0[presburger]
-declare mod_by_1[presburger]
-declare zmod_zero[presburger]
-declare zmod_self[presburger]
-declare mod_self[presburger]
-declare mod_by_0[presburger]
-declare 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"
-by simp_all
+use "Tools/Qelim/cooper.ML"
 
-use "Tools/Qelim/cooper.ML"
+setup CooperData.setup
 oracle linzqe_oracle = Coopereif.cooper_oracle
 
 use "Tools/Qelim/presburger.ML"
@@ -451,6 +429,27 @@
 end
 *} "Cooper's algorithm for Presburger arithmetic"
 
+declare dvd_eq_mod_eq_0[symmetric, presburger]
+declare mod_1[presburger] 
+declare mod_0[presburger]
+declare mod_by_1[presburger]
+declare zmod_zero[presburger]
+declare zmod_self[presburger]
+declare mod_self[presburger]
+declare mod_by_0[presburger]
+declare 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"
+by simp_all
+
 lemma [presburger, algebra]: "m mod 2 = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger
 lemma [presburger, algebra]: "m mod 2 = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
 lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger