src/HOL/Tools/Presburger/cooper_dec.ML

 (* Find the LCM of the coefficients of x.                                    *) 
 (* ------------------------------------------------------------------------- *) 
 (*gcd calculates gcd (a,b) and helps lcm_num calculating lcm (a,b)*) 
  
 (*BEWARE: replaces Library.gcd!! There is also Library.lcm!*)
-fun gcd a b = if a=0 then b else gcd (b mod a) a ; 
+fun gcd (a:IntInf.int) b = if a=0 then b else gcd (b mod a) a ; 
 fun lcm_num a b = (abs a*b) div (gcd (abs a) (abs b)); 
  
 fun formlcm x fm = case fm of 
     (Const (p,_)$ _ $(Const ("op +", _)$(Const ("op *",_)$ c $ y ) $z ) ) =>  if 
     (is_arith_rel fm) andalso (x = y) then  (abs(dest_numeral c)) else 1 

     |_  => foldr (fn(k,r) => r andalso (k mod dn = 0)) true ts
    end;
 
 
 val operations = 
-  [("op =",op=), ("op <",Int.<), ("op >",Int.>), ("op <=",Int.<=) , 
-   ("op >=",Int.>=), 
-   ("Divides.op dvd",fn (x,y) =>((y mod x) = 0))]; 
+  [("op =",op=), ("op <",IntInf.<), ("op >",IntInf.>), ("op <=",IntInf.<=) , 
+   ("op >=",IntInf.>=), 
+   ("Divides.op dvd",fn (x,y) =>((IntInf.mod(y, x)) = 0))]; 
  
 fun applyoperation (SOME f) (a,b) = f (a, b) 
     |applyoperation _ (_, _) = false; 
  
 (*Evaluation of constant atomic formulas*) 

     |mk_uni_int T (node $ rest) = (mk_uni_int T node) $ (mk_uni_int T rest )  
     |mk_uni_int T (Abs(AV,AT,p)) = Abs(AV,AT,mk_uni_int T p) 
     |mk_uni_int T tm = tm; 
  
 
-(* Minusinfinity Version*) 
+(* Minusinfinity Version*)    
+fun myupto (m:IntInf.int) n = if m > n then [] else m::(myupto (m+1) n)
+
 fun coopermi vars1 fm = 
   case fm of 
    Const ("Ex",_) $ Abs(x0,T,p0) => 
    let 
     val (xn,p1) = variant_abs (x0,T,p0) 
     val x = Free (xn,T)  
     val vars = (xn::vars1) 
     val p = unitycoeff x  (posineq (simpl p1))
     val p_inf = simpl (minusinf x p) 
     val bset = bset x p 
-    val js = 1 upto divlcm x p  
+    val js = myupto 1 (divlcm x p)
     fun p_element j b = linrep vars x (linear_add vars b (mk_numeral j)) p  
     fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) bset)  
    in (list_disj (map stage js))
     end 
   | _ => error "cooper: not an existential formula"; 

     val x = Free (xn,T)
     val vars = (xn::vars1)
     val p = unitycoeff x  (posineq (simpl p1))
     val p_inf = simpl (plusinf x p)
     val aset = aset x p
-    val js = 1 upto divlcm x p
+    val js = myupto 1 (divlcm x p)
     fun p_element j a = linrep vars x (linear_sub vars a (mk_numeral j)) p
     fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) aset)
    in (list_disj (map stage js))
    end
   | _ => error "cooper: not an existential formula";

       Const("True",_) => (SOME n,HOLogic.true_const)
       |F' => let val (rw,rf) = h nl 
              in (rw,HOLogic.mk_disj(F',rf)) 
 	     end)
     val f = if b then linear_add else linear_sub
-    val p_elements = foldr (fn (i,l) => l union (map (fn e => f [] e (mk_numeral i)) st)) [] (1 upto d)
+    val p_elements = foldr (fn (i,l) => l union (map (fn e => f [] e (mk_numeral i)) st)) [] (myupto 1 d)
     in h p_elements
     end;
 
 fun withness d b st vars x p = case (inf_w b d vars x p) of 
    (SOME n,_) => (SOME n,HOLogic.true_const)

     val vars = (xn::vars1)
 (*     val p = unitycoeff x  (posineq (simpl p1)) *)
     val p = unitycoeff x  p1 
     val ast = aset x p
     val bst = bset x p
-    val js = 1 upto divlcm x p
+    val js = myupto 1 (divlcm x p)
     val (p_inf,f,S ) = 
     if (length bst) <= (length ast) 
      then (simpl (minusinf x p),linear_add,bst)
      else (simpl (plusinf x p), linear_sub,ast)
     fun p_element j a = linrep vars x (f vars a (mk_numeral j)) p