src/HOL/ex/coopereif.ML

 
 structure Coopereif =
 struct
 
 open GeneratedCooper;
-open Reflected_Presburger;
 
 fun i_of_term vs t = case t
  of Free(xn,xT) => (case AList.lookup (op aconv) vs t
    of NONE   => error "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.nat i)
+    | Term.Bound i => Bound (nat 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 _ => 

       | 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), Integer.nat 0) :: (map (fn(v,n) => (v,1 + n)) vs)
+             val vs' = (Free (xn',xT), nat 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), Integer.nat 0) :: (map (fn(v,n) => (v,1 + n)) vs)
+             val vs' = (Free (xn',xT), nat 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 => error "qf_of_term ps : unknown term!"
              | SOME n => Closed n);

 fun start_vs t =
   let
     val fs = term_frees t
     val ps = term_bools [] t
   in
-    (fs ~~ (map Integer.nat (0 upto  (length fs - 1))),
-      ps ~~ (map Integer.nat (0 upto  (length ps - 1))))
+    (fs ~~ (map nat (0 upto  (length fs - 1))),
+      ps ~~ (map nat (0 upto  (length ps - 1))))
   end;
 
 fun term_of_i vs t = case t
  of C i => HOLogic.mk_number HOLogic.intT i
   | Bound n => (fst o the) (find_first (fn (_, m) => m = n) vs)

   | Add (t1, t2) => @{term "op +:: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
   | Sub (t1, t2) => Const (@{const_name "HOL.minus"}, HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $
       term_of_i vs t1 $ term_of_i vs t2
   | Mul (i, t2) => Const (@{const_name "HOL.times"}, HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $
       HOLogic.mk_number HOLogic.intT i $ term_of_i vs t2
-  | Cx (i, t') => term_of_i vs (Add (Mul (i, Bound (Integer.nat 0)), t'));
+  | Cx (i, t') => term_of_i vs (Add (Mul (i, Bound (nat 0)), t'));
 
 fun term_of_qf ps vs t = case t
  of T => HOLogic.true_const 
   | F => HOLogic.false_const
   | Lt t' => @{term "op < :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}