1.1 --- a/test/Tools/isac/Knowledge/gcd_poly_ml.sml Fri Aug 30 13:43:30 2013 +0200
1.2 +++ b/test/Tools/isac/Knowledge/gcd_poly_ml.sml Sun Sep 01 15:54:48 2013 +0200
1.3 @@ -69,9 +69,10 @@
1.4 "----------- fun NEWTON --------------------------------";
1.5 "----------- fun all_geq -------------------------------";
1.6 "----------- fun greater_deg ---------------------------";
1.7 -"----------- finfix %%|%% -----------------------------";
1.8 +"----------- infix %%|%% --------------------------------";
1.9 "----------- fun gcd_poly' -----------------------------";
1.10 "----------- fun gcd_poly ------------------------------";
1.11 +"----------- fun gcd_poly downto division by zero -------";
1.12 "=========== prep Lucas-Interpretation ==================";
1.13 "----------- fun for_quot_regarding ---------------------";
1.14 "----------- fun mult_to_deg - --------------------------";
1.15 @@ -722,14 +723,19 @@
1.16 if greater_deg [1,4,5,4] [0,3,4,5] = 2 then ()
1.17 else error "greater_deg [1,2,3,4] [0,3,4,5] = 2 changed ";
1.18
1.19 -"----------- finfix %%|%% ------------------------------";
1.20 -"----------- finfix %%|%% ------------------------------";
1.21 -"----------- finfix %%|%% ------------------------------";
1.22 -if [(1, [0, 0]), (~1, [0, 1])] %%|%% [(1, [0, 0]), (~1, [0, 1])] then ()
1.23 +"----------- infix %%|%% --------------------------------";
1.24 +"----------- infix %%|%% --------------------------------";
1.25 +"----------- infix %%|%% --------------------------------";
1.26 +if [(1, [0, 0]), (~1, [0, 1])] %%|%% [(1, [0, 0]), (~1, [0, 1])] then ()
1.27 +(* 1 - y | 1 - y*)
1.28 else error "[(1, [0, 0]), (~1, [0, 1])] %%|%% [(1, [0, 0]), (~1, [0, 1])] = true changed";
1.29 +
1.30 if [(3,[1,0])] %%|%% [(9,[1,1]),(12,[2,1]),(~3,[1,2])] then ()
1.31 +(* 3 x | 9 x y + 12 x^2 y - 3 x y^2 *)
1.32 else error "[(3,[1,0])] %%|%% [(9,[1,1]),(12,[2,1]),(~3,[1,2])] = true changed";
1.33 +
1.34 if [(3,[2,1])] %%|%% [(9,[1,1]),(12,[2,1]),(~3,[1,2])]
1.35 +(* 3 x^2 y | 9 x y + 12 x^2 y - 3 x y^2 *)
1.36 then error "[(3,[2,1])] %%|%% [(9,[1,1]),(12,[2,1]),(~3,[1,2])] = false changed" else ();
1.37
1.38 "----------- fun gcd_poly' ------------------------------";
1.39 @@ -798,6 +804,110 @@
1.40 if a = (a' %%*%% c) andalso b = (b' %%*%% c) then () else error "gcd_poly mail changed";
1.41 (* \<forall>c'. (c' dvd\<^isub>p a \<and> c' dvd\<^isub>p b) \<longrightarrow> c' \<le>\<^isub>p c) can NOT be checked this way, of course *)
1.42
1.43 +"----------- fun gcd_poly downto division by zero -------";
1.44 +"----------- fun gcd_poly downto division by zero -------";
1.45 +"----------- fun gcd_poly downto division by zero -------";
1.46 +"-------- example 187a: exception Div raised...";
1.47 +val a = [(12, [1, 1])]: poly
1.48 +val b = [(8, [0, 2])]: poly;
1.49 +(* val ((a', b'), c) = gcd_poly a b
1.50 +exception Div raised*)
1.51 +"~~~~~ fun gcd_poly, args:"; val ((a as (_, es)::_ : poly), b) = (a, b);
1.52 +(* val c = gcd_poly' a b (length es) 0
1.53 +exception Div raised*)
1.54 +"~~~~~ fun gcd_poly', args:"; val ((a as (_, es1)::_ : poly), (b as (_, es2)::_ : poly), n, r) =
1.55 + (a, b, (length es), 0);
1.56 +lex_ord (lmonom b) (lmonom a) = true;
1.57 +(*gcd_poly' b a n r
1.58 +exception Div raised*)
1.59 +"~~~~~ fun gcd_poly', args:"; val ((a as (_, es1)::_ : poly), (b as (_, es2)::_ : poly), n, r) =
1.60 + (b, a, n, r);
1.61 +lex_ord (lmonom b) (lmonom a) = false;
1.62 +n > 1 = true;
1.63 + val M = 1 + Int.min (max_deg_var a (length es1 - 2), max_deg_var b (length es2 - 2));
1.64 +(*try_new_r a b n M r [] []
1.65 +exception Div raised*)
1.66 +"~~~~~ and try_new_r, args:"; val (a, b, n, M, r, r_list, steps) = (a, b, n, M, r, [], []);
1.67 + val r = find_new_r a b r;
1.68 + val r_list = r_list @ [r];
1.69 + val g_r = gcd_poly' (order (eval a (n - 2) r))
1.70 + (order (eval b (n - 2) r)) (n - 1) 0
1.71 + val steps = steps @ [g_r];
1.72 +(*HENSEL_lifting a b n M 1 r r_list steps g_r ( zero_poly n ) [1]
1.73 +exception Div raised*)
1.74 +"~~~~~ and HENSEL_lifting, args:"; val (a, b, n, M, m, r, r_list, steps, g, g_n, mult) =
1.75 + (a, b, n, M, 1, r, r_list, steps, g_r, (zero_poly n), [1]);
1.76 +m > M = false;
1.77 + val r = find_new_r a b r;
1.78 + val r_list = r_list @ [r];
1.79 + val g_r = gcd_poly' (order (eval a (n - 2) r))
1.80 + (order (eval b (n - 2) r)) (n - 1) 0;
1.81 +lex_ord (lmonom g) (lmonom g_r) = false;
1.82 +lexp g = lexp g_r = true;
1.83 +val (g_n, new, steps) = NEWTON r_list [g, g_r] steps mult g_n (n - 2);
1.84 +nth steps (length steps - 1) = zero_poly (n - 1) = false;
1.85 +(*HENSEL_lifting a b n M (m + 1) r r_list steps g_r g_n new
1.86 +exception Div raised*)
1.87 +"~~~~~ and HENSEL_lifting, args:"; val (a, b, n, M, m, r, r_list, steps, g, g_n, mult) =
1.88 + (a, b, n, M, m + 1, r, r_list, steps, g_r, g_n, new);
1.89 +m > M = true;
1.90 +(g_n %%|%% a andalso (g_n %%|%% b)) = false;
1.91 +(*try_new_r a b n M r r_list steps
1.92 +exception Div raised*)
1.93 +"~~~~~ and try_new_r, args:"; val (a, b, n, M, r, r_list, steps) = (a, b, n, M, r, r_list, steps);
1.94 + val r = find_new_r a b r;
1.95 + val r_list = r_list @ [r];
1.96 + val g_r = gcd_poly' (order (eval a (n - 2) r))
1.97 + (order (eval b (n - 2) r)) (n - 1) 0
1.98 + val steps = steps @ [g_r];
1.99 +(*HENSEL_lifting a b n M 1 r r_list steps g_r (zero_poly n) [1]
1.100 +exception Div raised*)
1.101 +"~~~~~ and HENSEL_lifting, args:"; val (a, b, n, M, m, r, r_list, steps, g, g_n, mult) =
1.102 + (a, b, n, M, 1, r, r_list, steps, g_r, zero_poly n, [1]);
1.103 +m > M = false;
1.104 + val r = find_new_r a b r;
1.105 + val r_list = r_list @ [r];
1.106 + val g_r = gcd_poly' (order (eval a (n - 2) r))
1.107 + (order (eval b (n - 2) r)) (n - 1) 0;
1.108 +lex_ord (lmonom g) (lmonom g_r) = false;
1.109 +lexp g = lexp g_r = true;
1.110 +val (g_n, new, steps) = NEWTON r_list [g, g_r] steps mult g_n (n - 2);
1.111 +(nth steps (length steps - 1) = zero_poly (n - 1)) = false;
1.112 +(*HENSEL_lifting a b n M (m + 1) r r_list steps g_r g_n new
1.113 +exception Div raised*)
1.114 +"~~~~~ and HENSEL_lifting, args:"; val (a, b, n, M, m, r, r_list, steps, g, g_n, mult) =
1.115 + (a, b, n, M, m + 1, r, r_list, steps, g_r, g_n, new);
1.116 +m > M = true;
1.117 +(g_n %%|%% a andalso g_n %%|%% b) = false;
1.118 +(*try_new_r a b n M r r_list steps
1.119 +exception Div raised*)
1.120 +"~~~~~ and try_new_r, args:"; val (a, b, n, M, r, r_list, steps) = (a, b, n, M, r, r_list, steps);
1.121 + val r = find_new_r a b r;
1.122 + val r_list = r_list @ [r];
1.123 + val g_r = gcd_poly' (order (eval a (n - 2) r))
1.124 + (order (eval b (n - 2) r)) (n - 1) 0
1.125 + val steps = steps @ [g_r];
1.126 +(*HENSEL_lifting a b n M 1 r r_list steps g_r (zero_poly n) [1]
1.127 +exception Div raised*)
1.128 +"~~~~~ and HENSEL_lifting, args:"; val (a, b, n, M, m, r, r_list, steps, g, g_n, mult) =
1.129 + (a, b, n, M, 1, r, r_list, steps, g_r, zero_poly n, [1]);
1.130 +m > M = false;
1.131 + val r = find_new_r a b r;
1.132 + val r_list = r_list @ [r];
1.133 + val g_r = gcd_poly' (order (eval a (n - 2) r))
1.134 + (order (eval b (n - 2) r)) (n - 1) 0;
1.135 +lex_ord (lmonom g) (lmonom g_r) = false;
1.136 +lexp g = lexp g_r = true;
1.137 +val (g_n, new, steps) = NEWTON r_list [g, g_r] steps mult g_n (n - 2);
1.138 +nth steps (length steps - 1) = zero_poly (n - 1) = true;
1.139 +(*HENSEL_lifting a b n M (M + 1) r r_list steps g_r g_n new
1.140 +exception Div raised*)
1.141 +"~~~~~ and HENSEL_lifting, args:"; val (a, b, n, M, m, r, r_list, steps, g, g_n, mult) =
1.142 + (a, b, n, M, m + 1, r, r_list, steps, g_r, g_n, new);
1.143 +m > M = true;
1.144 +(*(g_n %%|%% a andalso g_n %%|%% b);
1.145 +exception Div raised: !!!!! g_n = [(0, [0, 0])] !!!!!*)
1.146 +
1.147 "=========== prep Lucas-Interpretation ==================";
1.148 "----------- fun for_quot_regarding ---------------------";
1.149 "----------- fun for_quot_regarding ---------------------";