src/HOL/ex/Reflected_Presburger.thy

 theory Reflected_Presburger
-imports GCD Main EfficientNat
+imports GCD EfficientNat
 uses ("coopereif.ML") ("coopertac.ML")
 begin
 
 lemma allpairs_set: "set (allpairs Pair xs ys) = {(x,y). x\<in> set xs \<and> y \<in> set ys}"
 by (induct xs) auto

 constdefs pa:: "fm \<Rightarrow> fm"
   "pa \<equiv> (\<lambda> p. qelim (prep p) cooper)"
 
 theorem mirqe: "(Ifm bbs bs (pa p) = Ifm bbs bs p) \<and> qfree (pa p)"
   using qelim_ci cooper prep by (auto simp add: pa_def)
-declare zdvd_iff_zmod_eq_0 [code]
-
-code_module GeneratedCooper
-file "generated_cooper.ML"
-contains pa = "pa"
-test = "%x . pa (E(A(Imp (Ge (Sub (Bound 0) (Bound 1))) (E(E(Eq(Sub(Add(Mul 3 (Bound 1)) (Mul 5 (Bound 0))) (Bound 2))))))))"
-
-ML{* use "generated_cooper.ML"; 
-     GeneratedCooper.test (); *}
+
+definition
+  cooper_test :: "unit \<Rightarrow> fm"
+where
+  "cooper_test u = pa (E (A (Imp (Ge (Sub (Bound 0) (Bound 1)))
+    (E (E (Eq (Sub (Add (Mul 3 (Bound 1)) (Mul 5 (Bound 0)))
+      (Bound 2))))))))"
+
+code_gen pa cooper_test in SML
+
+ML {* structure GeneratedCooper = struct open ROOT end *}
+ML {* GeneratedCooper.Reflected_Presburger.cooper_test () *}
 use "coopereif.ML"
 oracle linzqe_oracle ("term") = Coopereif.cooper_oracle
-use"coopertac.ML"
+use "coopertac.ML"
 setup "LinZTac.setup"
 
   (* Tests *)
 lemma "\<exists> (j::int). \<forall> x\<ge>j. (\<exists> a b. x = 3*a+5*b)"
 by cooper