--- a/src/HOL/Integ/cooper_dec.ML Wed Jun 15 11:54:13 2005 +0200
+++ b/src/HOL/Integ/cooper_dec.ML Wed Jun 15 13:46:00 2005 +0200
@@ -247,7 +247,7 @@
(*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
@@ -455,9 +455,9 @@
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;
@@ -679,7 +679,9 @@
|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) =>
@@ -690,7 +692,7 @@
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))
@@ -709,7 +711,7 @@
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))
@@ -747,7 +749,7 @@
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;
@@ -775,7 +777,7 @@
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)
--- a/src/HOL/Tools/Presburger/cooper_dec.ML Wed Jun 15 11:54:13 2005 +0200
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML Wed Jun 15 13:46:00 2005 +0200
@@ -247,7 +247,7 @@
(*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
@@ -455,9 +455,9 @@
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;
@@ -679,7 +679,9 @@
|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) =>
@@ -690,7 +692,7 @@
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))
@@ -709,7 +711,7 @@
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))
@@ -747,7 +749,7 @@
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;
@@ -775,7 +777,7 @@
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)