# HG changeset patch
# User haftmann
# Date 1184081454 -7200
# Node ID db10cf19f1f8f2b8ea3e7747dc7534078125d696
# Parent  6219d40c4f739b753f3574114fb979332fc04f5b
now works with SML/NJ

diff -r 6219d40c4f73 -r db10cf19f1f8 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Tue Jul 10 17:30:53 2007 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Tue Jul 10 17:30:54 2007 +0200
@@ -535,55 +535,53 @@
 structure Coopereif =
 struct
 
-open GeneratedCooper.Reflected_Presburger;
+open GeneratedCooper;
+
+fun cooper s = raise Cooper.COOPER ("Cooper oracle failed", ERROR s);
+fun i_of_term vs t = case t
+ of Free (xn, xT) => (case AList.lookup (op aconv) vs t
+     of NONE   => cooper "Variable not found in the list!"
+      | SOME n => Bound n)
+  | @{term "0::int"} => C 0
+  | @{term "1::int"} => C 1
+  | Term.Bound i => Bound (Integer.int i)
+  | Const(@{const_name HOL.uminus},_)$t' => Neg (i_of_term vs t')
+  | Const(@{const_name HOL.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
+  | Const(@{const_name HOL.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
+  | Const(@{const_name HOL.times},_)$t1$t2 => 
+     (Mul (HOLogic.dest_number t1 |> snd, i_of_term vs t2)
+    handle TERM _ => 
+       (Mul (HOLogic.dest_number t2 |> snd, i_of_term vs t1)
+        handle TERM _ => cooper "Reification: Unsupported kind of multiplication"))
+  | _ => (C (HOLogic.dest_number t |> snd) 
+           handle TERM _ => cooper "Reification: unknown term");
 
-fun cooper s = raise Cooper.COOPER ("Cooper Oracle Failed", ERROR s);
-fun i_of_term vs t = 
-    case t of
-	Free(xn,xT) => (case AList.lookup (op aconv) vs t of 
-			   NONE   => cooper "Variable not found in the list!!"
-			 | SOME n => Bound n)
-      | @{term "0::int"} => C 0
-      | @{term "1::int"} => C 1
-      | Term.Bound i => Bound i
-      | Const(@{const_name "HOL.uminus"},_)$t' => Neg (i_of_term vs t')
-      | Const(@{const_name "HOL.plus"},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
-      | Const(@{const_name "HOL.minus"},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
-      | Const(@{const_name "HOL.times"},_)$t1$t2 => 
-	     (Mul (HOLogic.dest_number t1 |> snd |> Integer.machine_int,i_of_term vs t2)
-        handle TERM _ => 
-           (Mul (HOLogic.dest_number t2 |> snd |> Integer.machine_int,i_of_term vs t1)
-            handle TERM _ => cooper "Reification: Unsupported kind of multiplication"))
-      | _ => (C (HOLogic.dest_number t |> snd |> Integer.machine_int) 
-               handle TERM _ => cooper "Reification: unknown term");
-	
-fun qf_of_term ps vs t = 
-    case t of 
-	Const("True",_) => T
-      | Const("False",_) => F
-      | Const(@{const_name "Orderings.less"},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
-      | Const(@{const_name "Orderings.less_eq"},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
-      | Const(@{const_name Divides.dvd},_)$t1$t2 => 
-	(Dvd(HOLogic.dest_number t1 |> snd |> Integer.machine_int, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd")
-      | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
-      | @{term "op = :: bool => _ "}$t1$t2 => Iffa(qf_of_term ps vs t1,qf_of_term ps vs t2)
-      | Const("op &",_)$t1$t2 => And(qf_of_term ps vs t1,qf_of_term ps vs t2)
-      | Const("op |",_)$t1$t2 => Or(qf_of_term ps vs t1,qf_of_term ps vs t2)
-      | Const("op -->",_)$t1$t2 => Impa(qf_of_term ps vs t1,qf_of_term ps vs t2)
-      | Const("Not",_)$t' => Nota(qf_of_term ps vs t')
-      | 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,1+ n)) vs)
-         in E (qf_of_term ps vs' p')
-         end
-      | 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,1+ n)) vs)
-         in A (qf_of_term ps vs' p')
-         end
-      | _ =>(case AList.lookup (op aconv) ps t of 
-               NONE => cooper "Reification: unknown term!"
-             | SOME n => Closed n);
+fun qf_of_term ps vs t =  case t
+ of Const("True",_) => T
+  | Const("False",_) => F
+  | Const(@{const_name Orderings.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
+  | Const(@{const_name Orderings.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
+  | Const(@{const_name Divides.dvd},_)$t1$t2 => 
+      (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd")
+  | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
+  | @{term "op = :: bool => _ "}$t1$t2 => Iffa(qf_of_term ps vs t1,qf_of_term ps vs t2)
+  | Const("op &",_)$t1$t2 => And(qf_of_term ps vs t1,qf_of_term ps vs t2)
+  | Const("op |",_)$t1$t2 => Or(qf_of_term ps vs t1,qf_of_term ps vs t2)
+  | Const("op -->",_)$t1$t2 => Impa(qf_of_term ps vs t1,qf_of_term ps vs t2)
+  | Const("Not",_)$t' => Nota(qf_of_term ps vs t')
+  | 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,1+ n)) vs)
+     in E (qf_of_term ps vs' p')
+     end
+  | 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,1+ n)) vs)
+     in A (qf_of_term ps vs' p')
+     end
+  | _ =>(case AList.lookup (op aconv) ps t of 
+           NONE => cooper "Reification: unknown term!"
+         | SOME n => Closed n);
 
 local
  val ops = [@{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"},
@@ -602,33 +600,21 @@
   | _ => if ty t orelse t mem ops then acc else insert (op aconv) t acc
 end;
  
-
-fun start_vs t =
-let
- val fs = term_frees t
- val ps = term_bools [] t
-in (fs ~~ (0 upto  (length fs - 1)), ps ~~ (0 upto  (length ps - 1)))
-end ;
-
-val iT = HOLogic.intT;
-val bT = HOLogic.boolT;
 fun myassoc2 l v =
     case l of
 	[] => NONE
       | (x,v')::xs => if v = v' then SOME x
 		      else myassoc2 xs v;
 
-fun term_of_i vs t =
-    case t of 
-	C i => HOLogic.mk_number HOLogic.intT (Integer.int i)
-      | Bound n => valOf (myassoc2 vs n)
-      | Neg t' => @{term "uminus :: int => _"}$(term_of_i vs t')
-      | Add(t1,t2) => @{term "op +:: int => _"}$ (term_of_i vs t1)$(term_of_i vs t2)
-      | Sub(t1,t2) => Const(@{const_name "HOL.minus"},[iT,iT] ---> iT)$
-			   (term_of_i vs t1)$(term_of_i vs t2)
-      | Mul(i,t2) => Const(@{const_name "HOL.times"},[iT,iT] ---> iT)$
-			   (HOLogic.mk_number HOLogic.intT (Integer.int i))$(term_of_i vs t2)
-      | Cx(i,t')=> term_of_i vs (Add(Mul (i, Bound 0),t'));
+fun term_of_i vs t = case t
+ of C i => HOLogic.mk_number HOLogic.intT i
+  | Bound n => the (myassoc2 vs n)
+  | Neg t' => @{term "uminus :: int => _"} $ term_of_i vs t'
+  | Add (t1, t2) => @{term "op + :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
+  | Sub (t1, t2) => @{term "op - :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
+  | Mul (i, t2) => @{term "op * :: int => _"} $
+      HOLogic.mk_number HOLogic.intT i $ term_of_i vs t2
+  | Cx (i, t') => term_of_i vs (Add (Mul (i, Bound 0), t'));
 
 fun term_of_qf ps vs t = 
  case t of 
@@ -639,24 +625,26 @@
  | Gt t' => @{term "op < :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
  | Ge t' => @{term "op <= :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
  | Eq t' => @{term "op = :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
- | NEq t' => term_of_qf ps vs (Nota(Eq t'))
- | Dvd(i,t') => @{term "op dvd :: int => _ "}$ 
-                 (HOLogic.mk_number HOLogic.intT (Integer.int i))$(term_of_i vs t')
+ | NEq t' => term_of_qf ps vs (Nota (Eq t'))
+ | Dvd(i,t') => @{term "op dvd :: int => _ "} $ 
+    HOLogic.mk_number HOLogic.intT i $ term_of_i vs t'
  | NDvd(i,t')=> term_of_qf ps vs (Nota(Dvd(i,t')))
  | Nota t' => HOLogic.Not$(term_of_qf ps vs t')
  | And(t1,t2) => HOLogic.conj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
  | Or(t1,t2) => HOLogic.disj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
  | Impa(t1,t2) => HOLogic.imp$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
- | Iffa(t1,t2) => (HOLogic.eq_const bT)$(term_of_qf ps vs t1)$ (term_of_qf ps vs t2)
- | Closed n => valOf (myassoc2 ps n)
+ | Iffa(t1,t2) => @{term "op = :: bool => _"} $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
+ | Closed n => the (myassoc2 ps n)
  | NClosed n => term_of_qf ps vs (Nota (Closed n))
  | _ => cooper "If this is raised, Isabelle/HOL or generate_code is inconsistent!";
 
-(* The oracle *)
 fun cooper_oracle thy t = 
-    let val (vs,ps) = start_vs t
-    in (equals propT) $ (HOLogic.mk_Trueprop t) $ 
-            (HOLogic.mk_Trueprop (term_of_qf ps vs (pa (qf_of_term ps vs t))))
-    end;
+  let
+    val (vs, ps) = pairself (map_index (swap o apfst Integer.int))
+      (term_frees t, term_bools [] t);
+  in
+    equals propT $ HOLogic.mk_Trueprop t $
+      HOLogic.mk_Trueprop (term_of_qf ps vs (pa (qf_of_term ps vs t)))
+  end;
 
 end;