# HG changeset patch
# User wenzelm
# Date 1181061369 -7200
# Node ID ccee01b8d1c5130e634df42c950c8eed6a32a137
# Parent  9062e98fdab1a6b4605cda8d04b2c3e384f6f360
fixed type int vs. integer;

diff -r 9062e98fdab1 -r ccee01b8d1c5 src/HOL/Tools/Groebner_Basis/groebner.ML
--- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Tue Jun 05 18:36:07 2007 +0200
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Tue Jun 05 18:36:09 2007 +0200
@@ -52,8 +52,8 @@
 (* ------------------------------------------------------------------------- *)
 
 datatype history =
-   Start of int
- | Mmul of (Rat.rat * (int list)) * history
+   Start of integer
+ | Mmul of (Rat.rat * (integer list)) * history
  | Add of history * history;
 
 
@@ -65,8 +65,8 @@
                 ([],[]) => false
               | (x1::o1,x2::o2) => x1 > x2 orelse x1 = x2 andalso lexorder o1 o2
               | _ => error "morder: inconsistent monomial lengths"
-        val n1 = fold (curry op +) m1 0
-        val n2 = fold (curry op +) m2 0 in
+        val n1 = fold Integer.add m1 0
+        val n2 = fold Integer.add m2 0 in
     n1 < n2 orelse n1 = n2 andalso lexorder m1 m2
     end;
 
@@ -91,7 +91,7 @@
 
 fun grob_sub l1 l2 = grob_add l1 (grob_neg l2);
 
-fun grob_mmul (c1,m1) (c2,m2) = (c1*/c2,map2 (curry op +) m1 m2);
+fun grob_mmul (c1,m1) (c2,m2) = (c1*/c2,map2 Integer.add m1 m2);
 
 fun grob_cmul cm pol = map (grob_mmul cm) pol;
 
@@ -119,9 +119,9 @@
 fun grob_pow vars l n =
   if n < 0 then error "grob_pow: negative power"
   else if n = 0 then [(rat_1,map (fn v => 0) vars)]
-  else grob_mul l (grob_pow vars l (n - 1));
+  else grob_mul l (grob_pow vars l (n -% 1));
 
-val max = fn x => fn y => if x < y then y else x;
+val max = fn (x: integer) => fn y => if x < y then y else x;
 
 fun degree vn p =
  case p of
@@ -132,16 +132,16 @@
 fun head_deg vn p = let val d = degree vn p in
  (d,fold (fn (c,r) => fn q => grob_add q [(c, map_index (fn (i,n) => if i = vn then 0 else n) r)]) (filter (fn (c,ns) => c <>/ rat_0 andalso nth ns vn = d) p) []) end;
 
-val is_zerop = forall (fn (c,ns) => c =/ rat_0 andalso forall (curry (op =) 0) ns);
+val is_zerop = forall (fn (c,ns) => c =/ rat_0 andalso forall (curry (op =) (0: integer)) ns);
 val grob_pdiv =
  let fun pdiv_aux vn (n,a) p k s =
   if is_zerop s then (k,s) else
   let val (m,b) = head_deg vn s
   in if m < n then (k,s) else
-     let val p' = grob_mul p [(rat_1, map_index (fn (i,v) => if i = vn then m - n else 0)
+     let val p' = grob_mul p [(rat_1, map_index (fn (i,v) => if i = vn then m -% n else 0)
                                                 (snd (hd s)))]
      in if a = b then pdiv_aux vn (n,a) p k (grob_sub s p')
-        else pdiv_aux vn (n,a) p (k + 1) (grob_sub (grob_mul a s) (grob_mul b p'))
+        else pdiv_aux vn (n,a) p (k +% 1) (grob_sub (grob_mul a s) (grob_mul b p'))
      end
   end
  in fn vn => fn s => fn p => pdiv_aux vn (head_deg vn p) p 0 s
@@ -151,7 +151,7 @@
 
 fun mdiv (c1,m1) (c2,m2) =
   (c1//c2,
-   map2 (fn n1 => fn n2 => if n1 < n2 then error "mdiv" else n1-n2) m1 m2);
+   map2 (fn n1 => fn n2 => if n1 < n2 then error "mdiv" else n1 -% n2) m1 m2);
 
 (* Lowest common multiple of two monomials. *)
 
@@ -248,7 +248,7 @@
 (* Test for hitting constant polynomial.                                     *)
 
 fun constant_poly p =
-  length p = 1 andalso forall (fn x=>x=0) (snd(hd p));
+  length p = 1 andalso forall (fn x => x = (0: integer)) (snd(hd p));
 
 (* ------------------------------------------------------------------------- *)
 (* Grobner basis algorithm.                                                  *)
@@ -310,7 +310,8 @@
 (* ------------------------------------------------------------------------- *)
 
 fun grobner pols =
-    let val npols = map2 (fn p => fn n => (p,Start n)) pols (0 upto (length pols - 1))
+    let val npols = map2 (fn p => fn n => (p,Start n)) pols
+          (map Integer.int (0 upto (length pols - 1)))
         val phists = filter (fn (p,_) => p <> []) npols
         val bas = grobner_interreduce [] (map monic phists)
         val prs0 = product bas bas
@@ -403,7 +404,7 @@
                                       (fn (e,(i,s)) =>
                                           (i+ 1,
                                            (nth vars i
-                                                     |>cterm_of (the_context())
+                                                     |>cterm_of (the_context())  (* FIXME *)
                                                      |> string_of_cterm)^ "^"
                                            ^ (Int.toString e) ^" * " ^ s)) (0,"0") m))
                             ^ ") + ") ^ s) "" pol;
@@ -599,7 +600,7 @@
  let fun holify_varpow (v,n) =
   if n = 1 then v else ring_mk_pow v (mk_cnumber @{ctyp "nat"} n)  (* FIXME *)
  fun holify_monomial vars (c,m) =
-  let val xps = map holify_varpow (filter (fn (_,n) => n <> 0) (vars ~~ m))
+  let val xps = map holify_varpow (filter (fn (_,n) => n <> (0: integer)) (vars ~~ m))
    in end_itlist ring_mk_mul (mk_const c :: xps)
   end
  fun holify_polynomial vars p =
@@ -648,7 +649,7 @@
           grobify_equations(list_mk_conj(Thm.dest_arg(concl nth)::map concl eths))
        val (deg,l,cert) = grobner_strong vars pols pol
        val th1 = Conv.fconv_rule((arg_conv o arg_conv)(binop_conv ring_normalize_conv)) nth
-       val th2 = funpow deg (idom_rule o conji th1) neq_01
+       val th2 = funpow (Integer.machine_int deg) (idom_rule o conji th1) neq_01
       in (vars,l,cert,th2)
       end)
     val _ = writeln ("Translating certificate to HOL inferences")
@@ -660,7 +661,8 @@
     fun thm_fn pols =
         if null pols then reflexive(mk_const rat_0) else
         end_itlist mk_add
-            (map (fn (i,p) => Drule.arg_cong_rule (mk_comb ring_mul_tm p) (nth eths i |> mk_meta_eq)) pols)
+            (map (fn (i,p) => Drule.arg_cong_rule (mk_comb ring_mul_tm p)
+              (nth eths (Integer.machine_int i) |> mk_meta_eq)) pols)
     val th1 = thm_fn herts_pos
     val th2 = thm_fn herts_neg
     val th3 = conji(mk_add (symmetric th1) th2 |> mk_object_eq) noteqth
@@ -704,7 +706,7 @@
   val pol = grobify_term vars tm
   val cert = grobner_ideal vars pols pol
  in map (fn n => let val p = assocd n cert [] in holify_polynomial vars p end)
-        (0 upto (length pols-1))
+        (map Integer.int (0 upto (length pols - 1)))
  end
 in (ring,ideal)
 end;
diff -r 9062e98fdab1 -r ccee01b8d1c5 src/HOL/Tools/Groebner_Basis/normalizer.ML
--- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Tue Jun 05 18:36:07 2007 +0200
+++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Tue Jun 05 18:36:09 2007 +0200
@@ -5,8 +5,8 @@
 
 signature NORMALIZER = 
 sig
- val mk_cnumber : ctyp -> int -> cterm
- val mk_cnumeral : int -> cterm
+ val mk_cnumber : ctyp -> integer -> cterm
+ val mk_cnumeral : integer -> cterm
  val semiring_normalize_conv : Proof.context -> Conv.conv
  val semiring_normalize_tac : Proof.context -> int -> tactic
  val semiring_normalize_wrapper :  NormalizerData.entry -> Conv.conv
@@ -36,9 +36,8 @@
 fun mk_cnumeral 0 = pls_const
   | mk_cnumeral ~1 = min_const
   | mk_cnumeral i =
-      let val (q, r) = IntInf.divMod (i, 2)
-      in Thm.capply (Thm.capply bit_const (mk_cnumeral q)) (mk_cbit (IntInf.toInt r)) 
-      end;
+      let val (q, r) = Integer.divmod i 2
+      in Thm.capply (Thm.capply bit_const (mk_cnumeral q)) (mk_cbit (Integer.machine_int r)) end;
 
 fun mk_cnumber cT = 
  let