--- 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;