diff -r 58b695d10cdf -r 52c7c42e7e27 src/HOL/ex/Reflected_Presburger.thy
--- a/src/HOL/ex/Reflected_Presburger.thy	Thu Jul 03 11:16:09 2008 +0200
+++ b/src/HOL/ex/Reflected_Presburger.thy	Thu Jul 03 11:16:33 2008 +0200
@@ -1,6 +1,10 @@
+(*  Title:      HOL/ex/Reflected_Presburger.thy
+    Author:     Amine Chaieb
+*)
+
 theory Reflected_Presburger
 imports Main GCD Efficient_Nat
-uses ("coopereif.ML") ("coopertac.ML")
+uses ("coopertac.ML")
 begin
 
 function
@@ -23,25 +27,23 @@
   | Mul int num
 
   (* A size for num to make inductive proofs simpler*)
-consts num_size :: "num \<Rightarrow> nat" 
-primrec 
+primrec num_size :: "num \<Rightarrow> nat" where
   "num_size (C c) = 1"
-  "num_size (Bound n) = 1"
-  "num_size (Neg a) = 1 + num_size a"
-  "num_size (Add a b) = 1 + num_size a + num_size b"
-  "num_size (Sub a b) = 3 + num_size a + num_size b"
-  "num_size (CN n c a) = 4 + num_size a"
-  "num_size (Mul c a) = 1 + num_size a"
+| "num_size (Bound n) = 1"
+| "num_size (Neg a) = 1 + num_size a"
+| "num_size (Add a b) = 1 + num_size a + num_size b"
+| "num_size (Sub a b) = 3 + num_size a + num_size b"
+| "num_size (CN n c a) = 4 + num_size a"
+| "num_size (Mul c a) = 1 + num_size a"
 
-consts Inum :: "int list \<Rightarrow> num \<Rightarrow> int"
-primrec
+primrec Inum :: "int list \<Rightarrow> num \<Rightarrow> int" where
   "Inum bs (C c) = c"
-  "Inum bs (Bound n) = bs!n"
-  "Inum bs (CN n c a) = c * (bs!n) + (Inum bs a)"
-  "Inum bs (Neg a) = -(Inum bs a)"
-  "Inum bs (Add a b) = Inum bs a + Inum bs b"
-  "Inum bs (Sub a b) = Inum bs a - Inum bs b"
-  "Inum bs (Mul c a) = c* Inum bs a"
+| "Inum bs (Bound n) = bs!n"
+| "Inum bs (CN n c a) = c * (bs!n) + (Inum bs a)"
+| "Inum bs (Neg a) = -(Inum bs a)"
+| "Inum bs (Add a b) = Inum bs a + Inum bs b"
+| "Inum bs (Sub a b) = Inum bs a - Inum bs b"
+| "Inum bs (Mul c a) = c* Inum bs a"
 
 datatype fm  = 
   T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| Dvd int num| NDvd int num|
@@ -177,7 +179,7 @@
 using bp numbound0_I[where b="b" and bs="bs" and b'="b'"]
 by (induct p rule: bound0.induct) (auto simp add: gr0_conv_Suc)
 
-fun   numsubst0:: "num \<Rightarrow> num \<Rightarrow> num" where
+fun numsubst0:: "num \<Rightarrow> num \<Rightarrow> num" where
   "numsubst0 t (C c) = (C c)"
 | "numsubst0 t (Bound n) = (if n=0 then t else Bound n)"
 | "numsubst0 t (CN 0 i a) = Add (Mul i t) (numsubst0 t a)"
@@ -1898,8 +1900,8 @@
   ultimately show ?thesis by blast
 qed
 
-constdefs pa:: "fm \<Rightarrow> fm"
-  "pa \<equiv> (\<lambda> p. qelim (prep p) cooper)"
+definition pa :: "fm \<Rightarrow> fm" where
+  "pa 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)
@@ -1911,21 +1913,150 @@
     (E (E (Eq (Sub (Add (Mul 3 (Bound 1)) (Mul 5 (Bound 0)))
       (Bound 2))))))))"
 
+ML {* @{code cooper_test} () *}
+
+(*
 code_reserved SML oo
-export_code pa cooper_test in SML module_name GeneratedCooper
-(*export_code pa in SML module_name GeneratedCooper file "~~/src/HOL/Tools/Qelim/raw_generated_cooper.ML"*)
+export_code pa in SML module_name GeneratedCooper file "~~/src/HOL/Tools/Qelim/raw_generated_cooper.ML"
+*)
+
+oracle linzqe_oracle ("term") = {*
+let
+
+fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t
+     of NONE => error "Variable not found in the list!"
+      | SOME n => @{code Bound} n)
+  | num_of_term vs @{term "0::int"} = @{code C} 0
+  | num_of_term vs @{term "1::int"} = @{code C} 1
+  | num_of_term vs (@{term "number_of :: int \<Rightarrow> int"} $ t) = @{code C} (HOLogic.dest_numeral t)
+  | num_of_term vs (Bound i) = @{code Bound} i
+  | num_of_term vs (@{term "uminus :: int \<Rightarrow> int"} $ t') = @{code Neg} (num_of_term vs t')
+  | num_of_term vs (@{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} $ t1 $ t2) =
+      @{code Add} (num_of_term vs t1, num_of_term vs t2)
+  | num_of_term vs (@{term "op - :: int \<Rightarrow> int \<Rightarrow> int"} $ t1 $ t2) =
+      @{code Sub} (num_of_term vs t1, num_of_term vs t2)
+  | num_of_term vs (@{term "op * :: int \<Rightarrow> int \<Rightarrow> int"} $ t1 $ t2) =
+      (case try HOLogic.dest_number t1
+       of SOME (_, i) => @{code Mul} (i, num_of_term vs t2)
+        | NONE => (case try HOLogic.dest_number t2
+                of SOME (_, i) => @{code Mul} (i, num_of_term vs t1)
+                 | NONE => error "num_of_term: unsupported multiplication"))
+  | num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term_global @{theory} t);
+
+fun fm_of_term ps vs @{term True} = @{code T}
+  | fm_of_term ps vs @{term False} = @{code F}
+  | fm_of_term ps vs (@{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"} $ t1 $ t2) =
+      @{code Lt} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
+  | fm_of_term ps vs (@{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"} $ t1 $ t2) =
+      @{code Le} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
+  | fm_of_term ps vs (@{term "op = :: int \<Rightarrow> int \<Rightarrow> bool"} $ t1 $ t2) =
+      @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2)) 
+  | fm_of_term ps vs (@{term "op dvd :: int \<Rightarrow> int \<Rightarrow> bool"} $ t1 $ t2) =
+      (case try HOLogic.dest_number t1
+       of SOME (_, i) => @{code Dvd} (i, num_of_term vs t2)
+        | NONE => error "num_of_term: unsupported dvd")
+  | fm_of_term ps vs (@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
+      @{code Iff} (fm_of_term ps vs t1, fm_of_term ps vs t2)
+  | fm_of_term ps vs (@{term "op &"} $ t1 $ t2) =
+      @{code And} (fm_of_term ps vs t1, fm_of_term ps vs t2)
+  | fm_of_term ps vs (@{term "op |"} $ t1 $ t2) =
+      @{code Or} (fm_of_term ps vs t1, fm_of_term ps vs t2)
+  | fm_of_term ps vs (@{term "op -->"} $ t1 $ t2) =
+      @{code Imp} (fm_of_term ps vs t1, fm_of_term ps vs t2)
+  | fm_of_term ps vs (@{term "Not"} $ t') =
+      @{code NOT} (fm_of_term ps vs t')
+  | fm_of_term ps vs (Const ("Ex", _) $ Abs (xn, xT, p)) =
+      let
+        val (xn', p') = variant_abs (xn, xT, p);
+        val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
+      in @{code E} (fm_of_term ps vs' p) end
+  | fm_of_term ps vs (Const ("All", _) $ Abs (xn, xT, p)) =
+      let
+        val (xn', p') = variant_abs (xn, xT, p);
+        val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
+      in @{code A} (fm_of_term ps vs' p) end
+  | fm_of_term ps vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term_global @{theory} t);
 
-ML {* GeneratedCooper.cooper_test () *}
-use "coopereif.ML"
-oracle linzqe_oracle ("term") = Coopereif.cooper_oracle
+fun term_of_num vs (@{code C} i) = HOLogic.mk_number HOLogic.intT i
+  | term_of_num vs (@{code Bound} n) = fst (the (find_first (fn (_, m) => n = m) vs))
+  | term_of_num vs (@{code Neg} t') = @{term "uminus :: int \<Rightarrow> int"} $ term_of_num vs t'
+  | term_of_num vs (@{code Add} (t1, t2)) = @{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} $
+      term_of_num vs t1 $ term_of_num vs t2
+  | term_of_num vs (@{code Sub} (t1, t2)) = @{term "op - :: int \<Rightarrow> int \<Rightarrow> int"} $
+      term_of_num vs t1 $ term_of_num vs t2
+  | term_of_num vs (@{code Mul} (i, t2)) = @{term "op * :: int \<Rightarrow> int \<Rightarrow> int"} $
+      term_of_num vs (@{code C} i) $ term_of_num vs t2
+  | term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t))
+
+fun term_of_fm ps vs @{code T} = HOLogic.true_const 
+  | term_of_fm ps vs @{code F} = HOLogic.false_const
+  | term_of_fm ps vs (@{code Lt} t) =
+      @{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"} $ term_of_num vs t $ @{term "0::int"}
+  | term_of_fm ps vs (@{code Le} t) =
+      @{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"} $ term_of_num vs t $ @{term "0::int"}
+  | term_of_fm ps vs (@{code Gt} t) =
+      @{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"} $ @{term "0::int"} $ term_of_num vs t
+  | term_of_fm ps vs (@{code Ge} t) =
+      @{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"} $ @{term "0::int"} $ term_of_num vs t
+  | term_of_fm ps vs (@{code Eq} t) =
+      @{term "op = :: int \<Rightarrow> int \<Rightarrow> bool"} $ term_of_num vs t $ @{term "0::int"}
+  | term_of_fm ps vs (@{code NEq} t) =
+      term_of_fm ps vs (@{code NOT} (@{code Eq} t))
+  | term_of_fm ps vs (@{code Dvd} (i, t)) =
+      @{term "op dvd :: int \<Rightarrow> int \<Rightarrow> bool"} $ term_of_num vs (@{code C} i) $ term_of_num vs t
+  | term_of_fm ps vs (@{code NDvd} (i, t)) =
+      term_of_fm ps vs (@{code NOT} (@{code Dvd} (i, t)))
+  | term_of_fm ps vs (@{code NOT} t') =
+      HOLogic.Not $ term_of_fm ps vs t'
+  | term_of_fm ps vs (@{code And} (t1, t2)) =
+      HOLogic.conj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
+  | term_of_fm ps vs (@{code Or} (t1, t2)) =
+      HOLogic.disj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
+  | term_of_fm ps vs (@{code Imp} (t1, t2)) =
+      HOLogic.imp $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
+  | term_of_fm ps vs (@{code Iff} (t1, t2)) =
+      @{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
+  | term_of_fm ps vs (@{code Closed} n) = (fst o the) (find_first (fn (_, m) => m = n) ps)
+  | term_of_fm ps vs (@{code NClosed} n) = term_of_fm ps vs (@{code NOT} (@{code Closed} n))
+
+fun term_bools acc t =
+  let
+    val is_op = member (op =) [@{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"},
+      @{term "op = :: int => _"}, @{term "op < :: int => _"},
+      @{term "op <= :: int => _"}, @{term "Not"}, @{term "All :: (int => _) => _"},
+      @{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}]
+    fun is_ty t = not (fastype_of t = HOLogic.boolT) 
+  in case t
+   of (l as f $ a) $ b => if is_ty t orelse is_op t then term_bools (term_bools acc l)b 
+        else insert (op aconv) t acc
+    | f $ a => if is_ty t orelse is_op t then term_bools (term_bools acc f) a  
+        else insert (op aconv) t acc
+    | Abs p => term_bools acc (snd (variant_abs p))
+    | _ => if is_ty t orelse is_op t then acc else insert (op aconv) t acc
+  end;
+
+in fn thy => fn t =>
+  let 
+    val fs = term_frees t;
+    val bs = term_bools [] t;
+    val vs = fs ~~ (0 upto (length fs - 1))
+    val ps = bs ~~ (0 upto (length bs - 1))
+    val t' = (term_of_fm ps vs o @{code pa} o fm_of_term ps vs) t;
+  in (HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
+end;
+*}
+
 use "coopertac.ML"
 setup "LinZTac.setup"
 
-  (* Tests *)
+text {* Tests *}
+
 lemma "\<exists> (j::int). \<forall> x\<ge>j. (\<exists> a b. x = 3*a+5*b)"
-by cooper
+  by cooper
 
-lemma "ALL (x::int) >=8. EX i j. 5*i + 3*j = x" by cooper
+lemma "ALL (x::int) >=8. EX i j. 5*i + 3*j = x"
+  by cooper
+
 theorem "(\<forall>(y::int). 3 dvd y) ==> \<forall>(x::int). b < x --> a \<le> x"
   by cooper
 
@@ -1940,20 +2071,41 @@
 theorem "\<forall>(x::nat). \<exists>(y::nat). (0::nat) \<le> 5 --> y = 5 + x "
   by cooper
 
-lemma "ALL (x::int) >=8. EX i j. 5*i + 3*j = x" by cooper 
-lemma "ALL (y::int) (z::int) (n::int). 3 dvd z --> 2 dvd (y::int) --> (EX (x::int).  2*x =  y) & (EX (k::int). 3*k = z)" by cooper
-lemma "ALL(x::int) y. x < y --> 2 * x + 1 < 2 * y" by cooper
-lemma "ALL(x::int) y. 2 * x + 1 ~= 2 * y" by cooper
-lemma "EX(x::int) y. 0 < x  & 0 <= y  & 3 * x - 5 * y = 1" by cooper
-lemma "~ (EX(x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)" by cooper
-lemma "ALL(x::int). (2 dvd x) --> (EX(y::int). x = 2*y)" by cooper
-lemma "ALL(x::int). (2 dvd x) --> (EX(y::int). x = 2*y)" by cooper
-lemma "ALL(x::int). (2 dvd x) = (EX(y::int). x = 2*y)" by cooper
-lemma "ALL(x::int). ((2 dvd x) = (ALL(y::int). x ~= 2*y + 1))" by cooper
-lemma "~ (ALL(x::int). ((2 dvd x) = (ALL(y::int). x ~= 2*y+1) | (EX(q::int) (u::int) i. 3*i + 2*q - u < 17) --> 0 < x | ((~ 3 dvd x) &(x + 8 = 0))))" by cooper
+lemma "ALL (x::int) >=8. EX i j. 5*i + 3*j = x"
+  by cooper 
+
+lemma "ALL (y::int) (z::int) (n::int). 3 dvd z --> 2 dvd (y::int) --> (EX (x::int).  2*x =  y) & (EX (k::int). 3*k = z)"
+  by cooper
+
+lemma "ALL(x::int) y. x < y --> 2 * x + 1 < 2 * y"
+  by cooper
+
+lemma "ALL(x::int) y. 2 * x + 1 ~= 2 * y"
+  by cooper
+
+lemma "EX(x::int) y. 0 < x  & 0 <= y  & 3 * x - 5 * y = 1"
+  by cooper
+
+lemma "~ (EX(x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)"
+  by cooper
+
+lemma "ALL(x::int). (2 dvd x) --> (EX(y::int). x = 2*y)"
+  by cooper
+
+lemma "ALL(x::int). (2 dvd x) = (EX(y::int). x = 2*y)"
+  by cooper
+
+lemma "ALL(x::int). ((2 dvd x) = (ALL(y::int). x ~= 2*y + 1))"
+  by cooper
+
+lemma "~ (ALL(x::int). ((2 dvd x) = (ALL(y::int). x ~= 2*y+1) | (EX(q::int) (u::int) i. 3*i + 2*q - u < 17) --> 0 < x | ((~ 3 dvd x) &(x + 8 = 0))))"
+  by cooper
+
 lemma "~ (ALL(i::int). 4 <= i --> (EX x y. 0 <= x & 0 <= y & 3 * x + 5 * y = i))" 
   by cooper
-lemma "EX j. ALL (x::int) >= j. EX i j. 5*i + 3*j = x" by cooper
+
+lemma "EX j. ALL (x::int) >= j. EX i j. 5*i + 3*j = x"
+  by cooper
 
 theorem "(\<forall>(y::int). 3 dvd y) ==> \<forall>(x::int). b < x --> a \<le> x"
   by cooper