# HG changeset patch
# User chaieb
# Date 1126731603 -7200
# Node ID df2b53a669379323638e0e86122e34ba92135e80
# Parent  b4743198b939553f4d022d6b3e22972ff5b6fe3d
Unfortunately patched to use IntInf.int instead of just int (SML compatibility)

diff -r b4743198b939 -r df2b53a66937 src/HOL/Integ/reflected_presburger.ML
--- a/src/HOL/Integ/reflected_presburger.ML	Wed Sep 14 22:18:55 2005 +0200
+++ b/src/HOL/Integ/reflected_presburger.ML	Wed Sep 14 23:00:03 2005 +0200
@@ -2,11 +2,11 @@
 
     (* Caution: This file should not be modified. *)
     (* It is autmatically generated from HOL/ex/Reflected_Presburger.thy *)
-fun nat i = if i < 0 then 0 else i;
+fun (nat: IntInf.int -> IntInf.int) i = if i < 0 then 0 else i;
 structure Generated =
 struct
 
-datatype intterm = Cst of int | Var of int | Neg of intterm
+datatype intterm = Cst of IntInf.int | Var of IntInf.int | Neg of intterm
   | Add of intterm * intterm | Sub of intterm * intterm
   | Mult of intterm * intterm;
 
@@ -178,7 +178,7 @@
 
 fun op_45_def0 m n = nat (op_45_def2 (m) (n));
 
-val id_1_def0 : int = (0 + 1);
+val id_1_def0 : IntInf.int = (0 + 1);
 
 fun decrvarsI (Cst i) = Cst i
   | decrvarsI (Var n) = Var (op_45_def0 n id_1_def0)
@@ -207,9 +207,9 @@
 fun map f [] = []
   | map f (x :: xs) = (f x :: map f xs);
 
-fun iupto (i, j) = (if (j < i) then [] else (i :: iupto ((i + 1), j)));
+fun iupto (i:IntInf.int, j:IntInf.int) = (if (j < i) then [] else (i :: iupto ((i + 1), j)));
 
-fun all_sums (j, []) = []
+fun all_sums (j:IntInf.int, []) = []
   | all_sums (j, (i :: is)) =
     op_64 (map (fn x => lin_add (i, Cst x)) (iupto (1, j))) (all_sums (j, is));
 
@@ -218,20 +218,20 @@
 fun negateSnd x = split (fn q => fn r => (q, ~ r)) x;
 
 fun adjust b =
-  (fn (q, r) =>
-    (if (0 <= op_45_def2 r b) then (((2 * q) + 1), op_45_def2 r b)
-      else ((2 * q), r)));
+  (fn (q:IntInf.int, r:IntInf.int) =>
+    (if (0 <= op_45_def2 r b) then ((((2:IntInf.int) * q) + (1:IntInf.int)), op_45_def2 r b)
+      else (((2:IntInf.int) * q), r)));
 
-fun negDivAlg (a, b) =
+fun negDivAlg (a:IntInf.int, b:IntInf.int) =
     (if ((0 <= (a + b)) orelse (b <= 0)) then (~1, (a + b))
       else adjust b (negDivAlg (a, (2 * b))));
 
-fun posDivAlg (a, b) =
+fun posDivAlg (a:IntInf.int, b:IntInf.int) =
     (if ((a < b) orelse (b <= 0)) then (0, a)
       else adjust b (posDivAlg (a, (2 * b))));
 
 fun divAlg x =
-  split (fn a => fn b =>
+  split (fn a:IntInf.int => fn b:IntInf.int =>
           (if (0 <= a)
             then (if (0 <= b) then posDivAlg (a, b)
                    else (if (a = 0) then (0, 0)
@@ -240,7 +240,7 @@
                    else negateSnd (posDivAlg (~ a, ~ b)))))
     x;
 
-fun op_mod_def1 a b = snd (divAlg (a, b));
+fun op_mod_def1 (a:IntInf.int) (b:IntInf.int) = snd (divAlg (a, b));
 
 fun op_dvd m n = (op_mod_def1 n m = 0);
 
@@ -1139,17 +1139,17 @@
   | minusinf (QAll ap) = QAll ap
   | minusinf (QEx aq) = QEx aq;
 
-fun abs i = (if (i < 0) then ~ i else i);
+fun (abs: IntInf.int -> IntInf.int) i = (if (i < 0) then ~ i else i);
 
-fun op_div_def1 a b = fst (divAlg (a, b));
+fun op_div_def1 (a:IntInf.int) (b:IntInf.int) = fst (divAlg (a, b));
 
 fun op_mod_def0 m n = nat (op_mod_def1 (m) (n));
 
-fun ngcd (m, n) = (if (n = 0) then m else ngcd (n, op_mod_def0 m n));
+fun ngcd (m:IntInf.int, n:IntInf.int) = (if (n = 0) then m else ngcd (n, op_mod_def0 m n));
 
 fun igcd x = split (fn a => fn b => (ngcd (nat (abs a), nat (abs b)))) x;
 
-fun ilcm a b = op_div_def1 (a * b) (igcd (a, b));
+fun ilcm (a:IntInf.int) (b:IntInf.int) = op_div_def1 (a * b) (igcd (a, b));
 
 fun divlcm (NOT p) = divlcm p
   | divlcm (And (p, q)) = ilcm (divlcm p) (divlcm q)
@@ -1567,7 +1567,7 @@
 
 fun op_43_def0 m n = nat ((m) + (n));
 
-fun size_def1 [] = 0
+fun size_def1 [] = (0:IntInf.int)
   | size_def1 (a :: list) = op_43_def0 (size_def1 list) (0 + 1);
 
 fun aset (And (p, q)) = op_64 (aset p) (aset q)
@@ -1776,7 +1776,7 @@
   | bset (QAll ap) = []
   | bset (QEx aq) = [];
 
-fun adjustcoeff (l, Le (Add (Mult (Cst c, Var 0), r), Cst i)) =
+fun adjustcoeff (l:IntInf.int, Le (Add (Mult (Cst c, Var 0), r), Cst i)) =
     (if (c <= 0)
       then Le (Add (Mult (Cst ~1, Var 0), lin_mul (~ (op_div_def1 l c), r)),
                 Cst 0)
diff -r b4743198b939 -r df2b53a66937 src/HOL/Tools/Presburger/reflected_presburger.ML
--- a/src/HOL/Tools/Presburger/reflected_presburger.ML	Wed Sep 14 22:18:55 2005 +0200
+++ b/src/HOL/Tools/Presburger/reflected_presburger.ML	Wed Sep 14 23:00:03 2005 +0200
@@ -2,11 +2,11 @@
 
     (* Caution: This file should not be modified. *)
     (* It is autmatically generated from HOL/ex/Reflected_Presburger.thy *)
-fun nat i = if i < 0 then 0 else i;
+fun (nat: IntInf.int -> IntInf.int) i = if i < 0 then 0 else i;
 structure Generated =
 struct
 
-datatype intterm = Cst of int | Var of int | Neg of intterm
+datatype intterm = Cst of IntInf.int | Var of IntInf.int | Neg of intterm
   | Add of intterm * intterm | Sub of intterm * intterm
   | Mult of intterm * intterm;
 
@@ -178,7 +178,7 @@
 
 fun op_45_def0 m n = nat (op_45_def2 (m) (n));
 
-val id_1_def0 : int = (0 + 1);
+val id_1_def0 : IntInf.int = (0 + 1);
 
 fun decrvarsI (Cst i) = Cst i
   | decrvarsI (Var n) = Var (op_45_def0 n id_1_def0)
@@ -207,9 +207,9 @@
 fun map f [] = []
   | map f (x :: xs) = (f x :: map f xs);
 
-fun iupto (i, j) = (if (j < i) then [] else (i :: iupto ((i + 1), j)));
+fun iupto (i:IntInf.int, j:IntInf.int) = (if (j < i) then [] else (i :: iupto ((i + 1), j)));
 
-fun all_sums (j, []) = []
+fun all_sums (j:IntInf.int, []) = []
   | all_sums (j, (i :: is)) =
     op_64 (map (fn x => lin_add (i, Cst x)) (iupto (1, j))) (all_sums (j, is));
 
@@ -218,20 +218,20 @@
 fun negateSnd x = split (fn q => fn r => (q, ~ r)) x;
 
 fun adjust b =
-  (fn (q, r) =>
-    (if (0 <= op_45_def2 r b) then (((2 * q) + 1), op_45_def2 r b)
-      else ((2 * q), r)));
+  (fn (q:IntInf.int, r:IntInf.int) =>
+    (if (0 <= op_45_def2 r b) then ((((2:IntInf.int) * q) + (1:IntInf.int)), op_45_def2 r b)
+      else (((2:IntInf.int) * q), r)));
 
-fun negDivAlg (a, b) =
+fun negDivAlg (a:IntInf.int, b:IntInf.int) =
     (if ((0 <= (a + b)) orelse (b <= 0)) then (~1, (a + b))
       else adjust b (negDivAlg (a, (2 * b))));
 
-fun posDivAlg (a, b) =
+fun posDivAlg (a:IntInf.int, b:IntInf.int) =
     (if ((a < b) orelse (b <= 0)) then (0, a)
       else adjust b (posDivAlg (a, (2 * b))));
 
 fun divAlg x =
-  split (fn a => fn b =>
+  split (fn a:IntInf.int => fn b:IntInf.int =>
           (if (0 <= a)
             then (if (0 <= b) then posDivAlg (a, b)
                    else (if (a = 0) then (0, 0)
@@ -240,7 +240,7 @@
                    else negateSnd (posDivAlg (~ a, ~ b)))))
     x;
 
-fun op_mod_def1 a b = snd (divAlg (a, b));
+fun op_mod_def1 (a:IntInf.int) (b:IntInf.int) = snd (divAlg (a, b));
 
 fun op_dvd m n = (op_mod_def1 n m = 0);
 
@@ -1139,17 +1139,17 @@
   | minusinf (QAll ap) = QAll ap
   | minusinf (QEx aq) = QEx aq;
 
-fun abs i = (if (i < 0) then ~ i else i);
+fun (abs: IntInf.int -> IntInf.int) i = (if (i < 0) then ~ i else i);
 
-fun op_div_def1 a b = fst (divAlg (a, b));
+fun op_div_def1 (a:IntInf.int) (b:IntInf.int) = fst (divAlg (a, b));
 
 fun op_mod_def0 m n = nat (op_mod_def1 (m) (n));
 
-fun ngcd (m, n) = (if (n = 0) then m else ngcd (n, op_mod_def0 m n));
+fun ngcd (m:IntInf.int, n:IntInf.int) = (if (n = 0) then m else ngcd (n, op_mod_def0 m n));
 
 fun igcd x = split (fn a => fn b => (ngcd (nat (abs a), nat (abs b)))) x;
 
-fun ilcm a b = op_div_def1 (a * b) (igcd (a, b));
+fun ilcm (a:IntInf.int) (b:IntInf.int) = op_div_def1 (a * b) (igcd (a, b));
 
 fun divlcm (NOT p) = divlcm p
   | divlcm (And (p, q)) = ilcm (divlcm p) (divlcm q)
@@ -1567,7 +1567,7 @@
 
 fun op_43_def0 m n = nat ((m) + (n));
 
-fun size_def1 [] = 0
+fun size_def1 [] = (0:IntInf.int)
   | size_def1 (a :: list) = op_43_def0 (size_def1 list) (0 + 1);
 
 fun aset (And (p, q)) = op_64 (aset p) (aset q)
@@ -1776,7 +1776,7 @@
   | bset (QAll ap) = []
   | bset (QEx aq) = [];
 
-fun adjustcoeff (l, Le (Add (Mult (Cst c, Var 0), r), Cst i)) =
+fun adjustcoeff (l:IntInf.int, Le (Add (Mult (Cst c, Var 0), r), Cst i)) =
     (if (c <= 0)
       then Le (Add (Mult (Cst ~1, Var 0), lin_mul (~ (op_div_def1 l c), r)),
                 Cst 0)