1.1 --- a/src/Tools/isac/Knowledge/GCD_Poly_ML.thy Sun Sep 01 16:50:51 2013 +0200
1.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly_ML.thy Mon Sep 02 14:56:57 2013 +0200
1.3 @@ -658,10 +658,13 @@
1.4
1.5 subsection {* gcd_poly algorithm, code for [1] p.95 *}
1.6 ML {*
1.7 + fun gcd_monom (c1, es1) (c2, es2) = (Integer.gcd c1 c2, map2 Integer.min es1 es2)
1.8 +
1.9 (* naming of n, M, m, r, ... follows Winkler p. 95
1.10 - n: amount of variables
1.11 + assumes: n = length es1 = length es2
1.12 r: *)
1.13 - fun gcd_poly' [(c1, es1)] [(c2, es2)] _ _ = [(Integer.gcd c1 c2, map2 Integer.min es1 es2)]
1.14 + fun gcd_poly' a [monom as (c, es)] _ _ = [fold gcd_monom a monom]
1.15 + | gcd_poly' [monom as (c, es)] b _ _ = [fold gcd_monom b monom]
1.16 | gcd_poly' (a as (_, es1)::_ : poly) (b as (_, es2)::_ : poly) n r =
1.17 if lex_ord (lmonom b) (lmonom a) then gcd_poly' b a n r else
1.18 if n > 1
1.19 @@ -677,7 +680,10 @@
1.20 end
1.21
1.22 (* fn: poly -> poly -> int ->
1.23 - int -> int -> int list -> poly list -> poly*)
1.24 + int -> int -> int list -> poly list -> poly
1.25 + assumes length a > 1 \<and> length b > 1
1.26 + yields TODO
1.27 + *)
1.28 and try_new_r a b n M r r_list steps =
1.29 let
1.30 val r = find_new_r a b r;
1.31 @@ -688,7 +694,10 @@
1.32 in HENSEL_lifting a b n M 1 r r_list steps g_r ( zero_poly n ) [1] end
1.33 (* fn: poly -> poly -> int ->
1.34 int -> int -> int -> int list -> poly list ->
1.35 - | poly -> poly -> int list -> poly*)
1.36 + | poly -> poly -> int list -> poly
1.37 + assumes length a > 1 \<and> length b > 1
1.38 + yields TODO
1.39 + *)
1.40 and HENSEL_lifting a b n M m r r_list steps g g_n mult =
1.41 if m > M then if g_n %%|%% a andalso g_n %%|%% b then g_n else
1.42 try_new_r a b n M r r_list steps
2.1 --- a/test/Tools/isac/Knowledge/gcd_poly_ml.sml Sun Sep 01 16:50:51 2013 +0200
2.2 +++ b/test/Tools/isac/Knowledge/gcd_poly_ml.sml Mon Sep 02 14:56:57 2013 +0200
2.3 @@ -741,7 +741,6 @@
2.4 "----------- fun gcd_poly' ------------------------------";
2.5 "----------- fun gcd_poly' ------------------------------";
2.6 "----------- fun gcd_poly' ------------------------------";
2.7 -
2.8 if gcd_poly' [(~3,[2,0]),(1,[5,0]),(3,[0,1]),(~6,[1,1]),(~1,[3,1]),(2,[4,1]),(1,[3,2]),(~1,[1,3]),(2,[2,3])]
2.9 [(2,[2,0]),(~2,[0,1]),(4,[1,1]),(~1,[3,1]),(1,[1,2]),(~1,[2,2]),(~1,[0,3]),(2,[1,3])] 2 0
2.10 = [(1, [2, 0]), (~1, [0, 1]), (2, [1, 1])] then () else error
2.11 @@ -750,7 +749,7 @@
2.12 "= [(1, [2, 0]), (~1, [0, 1]), (2, [1, 1])] changed";
2.13 (* -xy +xy^2z+yz - 1*)(* xy +1*) (*=*) (*xy -1*)
2.14 if gcd_poly' [(~1,[0,0,0]),(1,[0,1,1]),(1,[1,2,1]),(~1,[1,1,0])] [(1,[0,0,0]),(1,[1,1,0])] 3 0
2.15 -= [(1, [0, 0, 0]), (1, [1, 1, 0])] then () else error
2.16 + = [(~1, [0, 0, 0]), (~1, [1, 1, 0])] then () else error
2.17 "gcd_poly' [(~1,[0,0,0]),(1,[0,1,1]),(1,[1,2,1]),(~1,[1,1,0])] [(1,[0,0,0]),(1,[1,1,0])] 3 0 "
2.18 "= [(1, [0, 0, 0]), (1, [1, 1, 0])] changed";
2.19
2.20 @@ -810,6 +809,16 @@
2.21 val ((a', b'), c) = gcd_poly a b;
2.22 if a = (a' %%*%% c) andalso b = (b' %%*%% c) then () else error "regression test changed";
2.23
2.24 +(* regression test for --- integration lev.1 -- lev.5 in rational.sml *)
2.25 +val a = [(1, [0, 1, 1, 0, 1]), (1, [1, 0, 0, 1, 1])]: poly
2.26 +val b = [(1, [0, 1, 0, 1, 1])]: poly
2.27 +val ((a', b'), c) = gcd_poly a b;
2.28 +
2.29 +a' = [(1, [0, 1, 1, 0, 0]), (1, [1, 0, 0, 1, 0])];
2.30 +b' = [(1, [0, 1, 0, 1, 0])];
2.31 +c = [(1, [0, 0, 0, 0, 1])];
2.32 +if a = (a' %%*%% c) andalso b = (b' %%*%% c) then () else error "gcd_monom changed";
2.33 +
2.34 "----------- fun gcd_poly downto division by zero -------";
2.35 "----------- fun gcd_poly downto division by zero -------";
2.36 "----------- fun gcd_poly downto division by zero -------";