Unfortunately patched to use IntInf.int instead of just int (SML compatibility)
authorchaieb
Wed Sep 14 23:00:03 2005 +0200 (2005-09-14)
changeset 17390df2b53a66937
parent 17389 b4743198b939
child 17391 c6338ed6caf8
Unfortunately patched to use IntInf.int instead of just int (SML compatibility)
src/HOL/Integ/reflected_presburger.ML
src/HOL/Tools/Presburger/reflected_presburger.ML
     1.1 --- a/src/HOL/Integ/reflected_presburger.ML	Wed Sep 14 22:18:55 2005 +0200
     1.2 +++ b/src/HOL/Integ/reflected_presburger.ML	Wed Sep 14 23:00:03 2005 +0200
     1.3 @@ -2,11 +2,11 @@
     1.4  
     1.5      (* Caution: This file should not be modified. *)
     1.6      (* It is autmatically generated from HOL/ex/Reflected_Presburger.thy *)
     1.7 -fun nat i = if i < 0 then 0 else i;
     1.8 +fun (nat: IntInf.int -> IntInf.int) i = if i < 0 then 0 else i;
     1.9  structure Generated =
    1.10  struct
    1.11  
    1.12 -datatype intterm = Cst of int | Var of int | Neg of intterm
    1.13 +datatype intterm = Cst of IntInf.int | Var of IntInf.int | Neg of intterm
    1.14    | Add of intterm * intterm | Sub of intterm * intterm
    1.15    | Mult of intterm * intterm;
    1.16  
    1.17 @@ -178,7 +178,7 @@
    1.18  
    1.19  fun op_45_def0 m n = nat (op_45_def2 (m) (n));
    1.20  
    1.21 -val id_1_def0 : int = (0 + 1);
    1.22 +val id_1_def0 : IntInf.int = (0 + 1);
    1.23  
    1.24  fun decrvarsI (Cst i) = Cst i
    1.25    | decrvarsI (Var n) = Var (op_45_def0 n id_1_def0)
    1.26 @@ -207,9 +207,9 @@
    1.27  fun map f [] = []
    1.28    | map f (x :: xs) = (f x :: map f xs);
    1.29  
    1.30 -fun iupto (i, j) = (if (j < i) then [] else (i :: iupto ((i + 1), j)));
    1.31 +fun iupto (i:IntInf.int, j:IntInf.int) = (if (j < i) then [] else (i :: iupto ((i + 1), j)));
    1.32  
    1.33 -fun all_sums (j, []) = []
    1.34 +fun all_sums (j:IntInf.int, []) = []
    1.35    | all_sums (j, (i :: is)) =
    1.36      op_64 (map (fn x => lin_add (i, Cst x)) (iupto (1, j))) (all_sums (j, is));
    1.37  
    1.38 @@ -218,20 +218,20 @@
    1.39  fun negateSnd x = split (fn q => fn r => (q, ~ r)) x;
    1.40  
    1.41  fun adjust b =
    1.42 -  (fn (q, r) =>
    1.43 -    (if (0 <= op_45_def2 r b) then (((2 * q) + 1), op_45_def2 r b)
    1.44 -      else ((2 * q), r)));
    1.45 +  (fn (q:IntInf.int, r:IntInf.int) =>
    1.46 +    (if (0 <= op_45_def2 r b) then ((((2:IntInf.int) * q) + (1:IntInf.int)), op_45_def2 r b)
    1.47 +      else (((2:IntInf.int) * q), r)));
    1.48  
    1.49 -fun negDivAlg (a, b) =
    1.50 +fun negDivAlg (a:IntInf.int, b:IntInf.int) =
    1.51      (if ((0 <= (a + b)) orelse (b <= 0)) then (~1, (a + b))
    1.52        else adjust b (negDivAlg (a, (2 * b))));
    1.53  
    1.54 -fun posDivAlg (a, b) =
    1.55 +fun posDivAlg (a:IntInf.int, b:IntInf.int) =
    1.56      (if ((a < b) orelse (b <= 0)) then (0, a)
    1.57        else adjust b (posDivAlg (a, (2 * b))));
    1.58  
    1.59  fun divAlg x =
    1.60 -  split (fn a => fn b =>
    1.61 +  split (fn a:IntInf.int => fn b:IntInf.int =>
    1.62            (if (0 <= a)
    1.63              then (if (0 <= b) then posDivAlg (a, b)
    1.64                     else (if (a = 0) then (0, 0)
    1.65 @@ -240,7 +240,7 @@
    1.66                     else negateSnd (posDivAlg (~ a, ~ b)))))
    1.67      x;
    1.68  
    1.69 -fun op_mod_def1 a b = snd (divAlg (a, b));
    1.70 +fun op_mod_def1 (a:IntInf.int) (b:IntInf.int) = snd (divAlg (a, b));
    1.71  
    1.72  fun op_dvd m n = (op_mod_def1 n m = 0);
    1.73  
    1.74 @@ -1139,17 +1139,17 @@
    1.75    | minusinf (QAll ap) = QAll ap
    1.76    | minusinf (QEx aq) = QEx aq;
    1.77  
    1.78 -fun abs i = (if (i < 0) then ~ i else i);
    1.79 +fun (abs: IntInf.int -> IntInf.int) i = (if (i < 0) then ~ i else i);
    1.80  
    1.81 -fun op_div_def1 a b = fst (divAlg (a, b));
    1.82 +fun op_div_def1 (a:IntInf.int) (b:IntInf.int) = fst (divAlg (a, b));
    1.83  
    1.84  fun op_mod_def0 m n = nat (op_mod_def1 (m) (n));
    1.85  
    1.86 -fun ngcd (m, n) = (if (n = 0) then m else ngcd (n, op_mod_def0 m n));
    1.87 +fun ngcd (m:IntInf.int, n:IntInf.int) = (if (n = 0) then m else ngcd (n, op_mod_def0 m n));
    1.88  
    1.89  fun igcd x = split (fn a => fn b => (ngcd (nat (abs a), nat (abs b)))) x;
    1.90  
    1.91 -fun ilcm a b = op_div_def1 (a * b) (igcd (a, b));
    1.92 +fun ilcm (a:IntInf.int) (b:IntInf.int) = op_div_def1 (a * b) (igcd (a, b));
    1.93  
    1.94  fun divlcm (NOT p) = divlcm p
    1.95    | divlcm (And (p, q)) = ilcm (divlcm p) (divlcm q)
    1.96 @@ -1567,7 +1567,7 @@
    1.97  
    1.98  fun op_43_def0 m n = nat ((m) + (n));
    1.99  
   1.100 -fun size_def1 [] = 0
   1.101 +fun size_def1 [] = (0:IntInf.int)
   1.102    | size_def1 (a :: list) = op_43_def0 (size_def1 list) (0 + 1);
   1.103  
   1.104  fun aset (And (p, q)) = op_64 (aset p) (aset q)
   1.105 @@ -1776,7 +1776,7 @@
   1.106    | bset (QAll ap) = []
   1.107    | bset (QEx aq) = [];
   1.108  
   1.109 -fun adjustcoeff (l, Le (Add (Mult (Cst c, Var 0), r), Cst i)) =
   1.110 +fun adjustcoeff (l:IntInf.int, Le (Add (Mult (Cst c, Var 0), r), Cst i)) =
   1.111      (if (c <= 0)
   1.112        then Le (Add (Mult (Cst ~1, Var 0), lin_mul (~ (op_div_def1 l c), r)),
   1.113                  Cst 0)
     2.1 --- a/src/HOL/Tools/Presburger/reflected_presburger.ML	Wed Sep 14 22:18:55 2005 +0200
     2.2 +++ b/src/HOL/Tools/Presburger/reflected_presburger.ML	Wed Sep 14 23:00:03 2005 +0200
     2.3 @@ -2,11 +2,11 @@
     2.4  
     2.5      (* Caution: This file should not be modified. *)
     2.6      (* It is autmatically generated from HOL/ex/Reflected_Presburger.thy *)
     2.7 -fun nat i = if i < 0 then 0 else i;
     2.8 +fun (nat: IntInf.int -> IntInf.int) i = if i < 0 then 0 else i;
     2.9  structure Generated =
    2.10  struct
    2.11  
    2.12 -datatype intterm = Cst of int | Var of int | Neg of intterm
    2.13 +datatype intterm = Cst of IntInf.int | Var of IntInf.int | Neg of intterm
    2.14    | Add of intterm * intterm | Sub of intterm * intterm
    2.15    | Mult of intterm * intterm;
    2.16  
    2.17 @@ -178,7 +178,7 @@
    2.18  
    2.19  fun op_45_def0 m n = nat (op_45_def2 (m) (n));
    2.20  
    2.21 -val id_1_def0 : int = (0 + 1);
    2.22 +val id_1_def0 : IntInf.int = (0 + 1);
    2.23  
    2.24  fun decrvarsI (Cst i) = Cst i
    2.25    | decrvarsI (Var n) = Var (op_45_def0 n id_1_def0)
    2.26 @@ -207,9 +207,9 @@
    2.27  fun map f [] = []
    2.28    | map f (x :: xs) = (f x :: map f xs);
    2.29  
    2.30 -fun iupto (i, j) = (if (j < i) then [] else (i :: iupto ((i + 1), j)));
    2.31 +fun iupto (i:IntInf.int, j:IntInf.int) = (if (j < i) then [] else (i :: iupto ((i + 1), j)));
    2.32  
    2.33 -fun all_sums (j, []) = []
    2.34 +fun all_sums (j:IntInf.int, []) = []
    2.35    | all_sums (j, (i :: is)) =
    2.36      op_64 (map (fn x => lin_add (i, Cst x)) (iupto (1, j))) (all_sums (j, is));
    2.37  
    2.38 @@ -218,20 +218,20 @@
    2.39  fun negateSnd x = split (fn q => fn r => (q, ~ r)) x;
    2.40  
    2.41  fun adjust b =
    2.42 -  (fn (q, r) =>
    2.43 -    (if (0 <= op_45_def2 r b) then (((2 * q) + 1), op_45_def2 r b)
    2.44 -      else ((2 * q), r)));
    2.45 +  (fn (q:IntInf.int, r:IntInf.int) =>
    2.46 +    (if (0 <= op_45_def2 r b) then ((((2:IntInf.int) * q) + (1:IntInf.int)), op_45_def2 r b)
    2.47 +      else (((2:IntInf.int) * q), r)));
    2.48  
    2.49 -fun negDivAlg (a, b) =
    2.50 +fun negDivAlg (a:IntInf.int, b:IntInf.int) =
    2.51      (if ((0 <= (a + b)) orelse (b <= 0)) then (~1, (a + b))
    2.52        else adjust b (negDivAlg (a, (2 * b))));
    2.53  
    2.54 -fun posDivAlg (a, b) =
    2.55 +fun posDivAlg (a:IntInf.int, b:IntInf.int) =
    2.56      (if ((a < b) orelse (b <= 0)) then (0, a)
    2.57        else adjust b (posDivAlg (a, (2 * b))));
    2.58  
    2.59  fun divAlg x =
    2.60 -  split (fn a => fn b =>
    2.61 +  split (fn a:IntInf.int => fn b:IntInf.int =>
    2.62            (if (0 <= a)
    2.63              then (if (0 <= b) then posDivAlg (a, b)
    2.64                     else (if (a = 0) then (0, 0)
    2.65 @@ -240,7 +240,7 @@
    2.66                     else negateSnd (posDivAlg (~ a, ~ b)))))
    2.67      x;
    2.68  
    2.69 -fun op_mod_def1 a b = snd (divAlg (a, b));
    2.70 +fun op_mod_def1 (a:IntInf.int) (b:IntInf.int) = snd (divAlg (a, b));
    2.71  
    2.72  fun op_dvd m n = (op_mod_def1 n m = 0);
    2.73  
    2.74 @@ -1139,17 +1139,17 @@
    2.75    | minusinf (QAll ap) = QAll ap
    2.76    | minusinf (QEx aq) = QEx aq;
    2.77  
    2.78 -fun abs i = (if (i < 0) then ~ i else i);
    2.79 +fun (abs: IntInf.int -> IntInf.int) i = (if (i < 0) then ~ i else i);
    2.80  
    2.81 -fun op_div_def1 a b = fst (divAlg (a, b));
    2.82 +fun op_div_def1 (a:IntInf.int) (b:IntInf.int) = fst (divAlg (a, b));
    2.83  
    2.84  fun op_mod_def0 m n = nat (op_mod_def1 (m) (n));
    2.85  
    2.86 -fun ngcd (m, n) = (if (n = 0) then m else ngcd (n, op_mod_def0 m n));
    2.87 +fun ngcd (m:IntInf.int, n:IntInf.int) = (if (n = 0) then m else ngcd (n, op_mod_def0 m n));
    2.88  
    2.89  fun igcd x = split (fn a => fn b => (ngcd (nat (abs a), nat (abs b)))) x;
    2.90  
    2.91 -fun ilcm a b = op_div_def1 (a * b) (igcd (a, b));
    2.92 +fun ilcm (a:IntInf.int) (b:IntInf.int) = op_div_def1 (a * b) (igcd (a, b));
    2.93  
    2.94  fun divlcm (NOT p) = divlcm p
    2.95    | divlcm (And (p, q)) = ilcm (divlcm p) (divlcm q)
    2.96 @@ -1567,7 +1567,7 @@
    2.97  
    2.98  fun op_43_def0 m n = nat ((m) + (n));
    2.99  
   2.100 -fun size_def1 [] = 0
   2.101 +fun size_def1 [] = (0:IntInf.int)
   2.102    | size_def1 (a :: list) = op_43_def0 (size_def1 list) (0 + 1);
   2.103  
   2.104  fun aset (And (p, q)) = op_64 (aset p) (aset q)
   2.105 @@ -1776,7 +1776,7 @@
   2.106    | bset (QAll ap) = []
   2.107    | bset (QEx aq) = [];
   2.108  
   2.109 -fun adjustcoeff (l, Le (Add (Mult (Cst c, Var 0), r), Cst i)) =
   2.110 +fun adjustcoeff (l:IntInf.int, Le (Add (Mult (Cst c, Var 0), r), Cst i)) =
   2.111      (if (c <= 0)
   2.112        then Le (Add (Mult (Cst ~1, Var 0), lin_mul (~ (op_div_def1 l c), r)),
   2.113                  Cst 0)