1 (* Title: test/../rational2
3 Copyright (c) Diana Meindl 2011
4 12345678901234567890123456789012345678901234567890123456789012345678901234567890
5 10 20 30 40 50 60 70 80
8 (*fun nth _ [] = error "nth _ []" (*Isabelle2002, still saved the hours of update*)
10 | nth n (_::xs) = nth (n-1) xs;*)
11 fun nth xs i = List.nth (xs, i); (*recent Isabelle: TODO update all isac code *)
13 "--------------------------------------------------------";
14 "table of contents --------------------------------------";
15 "--------------------------------------------------------";
16 "----------- fun div2 -- --------------------------------";
17 "----------- fun mod_inv --------------------------------";
18 "----------- fun mod_div --------------------------------";
19 "----------- fun chinese_remainder ----------------------";
20 "----------- fun is_prime -------------------------------";
21 "----------- fun make_primes ----------------------------";
22 "----------- fun primes_upto ----------------------------";
23 "----------- fun next_prime_not_dvd ---------------------";
24 "----------- fun lcoeff_up ------------------------------";
25 "----------- fun deg_up ---------------------------------";
26 "----------- fun drop_lc0_up ----------------------------";
27 "----------- fun normalise ------------------------------";
28 (* order until here: (GCD_Poly_FP =) GCD_Poly = gcd_poly *)
29 "----------- fun %* -------------------------------------";
30 "----------- fun %/ -------------------------------------";
31 "----------- fun %-% ------------------------------------";
32 "----------- fun %|% ------------------------------------";
33 (*"----------- fun %+% ------------------------------------";*)
34 (*"----------- fun centr_up -----------------------------";*)
35 "----------- fun LANDAU_MIGNOTTE_bound ------------------";
36 "----------- fun chinese_remainder_up -------------------";
37 "----------- fun mod_up ---------------------------------";
38 "----------- fun mod_up_gcd -----------------------------";
39 "----------- fun primitive_up ---------------------------";
40 "----------- fun try_new_prime_up -----------------------";
41 "----------- fun gcd_up ---------------------------------";
42 "=========== Multivariate Case ==========================";
43 "----------- fun lcoeff ---------------------------------";
44 "----------- fun lexp -----------------------------------";
45 "----------- fun add_variable ---------------------------";
46 "----------- fun zero_poly ------------------------------";
47 "----------- drop_lc0 -----------------------------------";
48 "----------- fun add_monoms -----------------------------";
49 "----------- fun lex_ord --------------------------------";
50 "----------- fun order ----------------------------------";
51 (*"----------- fun lcoeff_up_poly ---------------------------";*)
52 "----------- fun lexp -----------------------------------";
53 "----------- fun max_deg_var ----------------------------";
54 "----------- infix %%/ ----------------------------------";
55 "----------- infix %%*%% --------------------------------";
56 "----------- fun gcd_coeff ------------------------------";
57 (*"----------- fun gcd_coeff_poly -------------------------";*)
58 "----------- fun eval -----------------------------------";
59 "----------- fun multi_to_uni ---------------------------";
60 "----------- fun uni_to_multi ---------------------------";
61 "----------- fun find_new_r ----------------------------";
62 "----------- fun mult_with_new_var ---------------------";
63 (*"----------- fun greater_deg -----------------";*)
64 "----------- infix %%+%% -------------------------------";
65 "----------- infix %%-%% -------------------------------";
66 "----------- infix %%*%% -------------------------------";
67 "----------- infix %%/%% -------------------------------";
68 "----------- fun newton_first --------------------------";
69 "----------- fun NEWTON --------------------------------";
70 "----------- fun all_geq -------------------------------";
71 "----------- fun greater_deg ---------------------------";
72 "----------- infix %%|%% --------------------------------";
73 "----------- fun gcd_poly' -----------------------------";
74 "----------- fun gcd_poly ------------------------------";
75 "----------- fun gcd_poly downto division by zero -------";
76 "=========== prep Lucas-Interpretation ==================";
77 "----------- fun for_quot_regarding ---------------------";
78 "----------- fun mult_to_deg - --------------------------";
79 "----------- fun fact_quot ------------------------------";
80 "----------- fun %+% ------------------------------------";
81 "----------- fun %*% ------------------------------------";
82 "----------- fun %*/% -----------------------------------";
83 "----------- fun %*/% Subscript raised (line 509 of lib--";
84 "----------- fun EUCLID_naive_up ------------------------";
85 "----------- last step in EUCLID ------------------------";
86 " ========== END ======================================= ";
89 "----------- fun div2 -- --------------------------------";
90 "----------- fun div2 -- --------------------------------";
91 "----------- fun div2 -- --------------------------------";
93 if 5 div 2 = 2 then () else error "5 div 2 = 2 changed";
94 if (5 div2 2) = 2 then () else error "5 div2 2 = 2 changed";
95 if ~5 div 2 = ~3 then () else error "~5 div 2 = ~3 changed";
96 if (~5 div2 2) = ~2 then () else error "~5 div2 2 = ~2 changed";
97 if ~5 div ~2 = 2 then () else error "~5 div ~2 = 2 changed";
98 if (~5 div2 ~2) = 2 then () else error "~5 div2 ~2 = 2 changed";
99 if 5 div ~2 = ~3 then () else error "5 div ~2 = ~3 changed";
100 if (5 div2 ~2) = ~2 then () else error "5 div2 ~2 = ~2 changed";
103 "----------- fun mod_inv --------------------------------";
104 "----------- fun mod_inv --------------------------------";
105 "----------- fun mod_inv--- -----------------------------";
106 "~~~~~ fun mod_inv, args:"; val (r, m) = (5,7);
107 "~~~~~ fun modi, args:"; val (r, rold, m, rinv) = (r, r, m, 1);
109 r mod m = 1; (*=false*)
110 "~~~~~ fun modi, args:"; val (r, rold, m, rinv) = (rold * (rinv + 1), rold, m, rinv + 1);
112 r mod m = 1; (*=false*)
113 "~~~~~ fun modi, args:"; val (r, rold, m, rinv) = (rold * (rinv + 1), rold, m, rinv + 1);
115 r mod m = 1; (*=true*)
116 "~~~~~ to mod_inv return val:"; val (rinv) = (rinv);
118 if mod_inv 5 7 = 3 then () else error "mod_inv 5 7 = 3 changed";
119 if mod_inv 3 7 = 5 then () else error "mod_inv 3 7 = 5 changed";
120 if mod_inv 4 339 = 85 then () else error "mod_inv 4 339 = 85 changed";
122 "----------- fun mod_div --------------------------------";
123 "----------- fun mod_div --------------------------------";
124 "----------- fun mod_div --------------------------------";
125 if mod_div 21 3 5 = 2 then () else error "mod_div changed"; 21 mod 5 = (3 * 2) mod 5;
126 if mod_div 22 3 5 = 4 then () else error "mod_div changed"; 22 mod 5 = (3 * 4) mod 5;
127 if mod_div 23 3 5 = 1 then () else error "mod_div changed"; 23 mod 5 = (3 * 1) mod 5;
128 if mod_div 24 3 5 = 3 then () else error "mod_div changed"; 24 mod 5 = (3 * 3) mod 5;
129 if mod_div 25 3 5 = 0 then () else error "mod_div changed"; 25 mod 5 = (3 * 0) mod 5;
131 if mod_div 21 4 5 = 4 then () else error "mod_div 21 4 5 = 4 changed";
132 if mod_div 1 4 5 = 4 then () else error "mod_div 1 4 5 = 4 changed";
133 if mod_div 0 4 5 = 0 then () else error "mod_div 0 4 5 = 0 changed";
135 "----------- fun chinese_remainder ----------------------";
136 "----------- fun chinese_remainder ----------------------";
137 "----------- fun chinese_remainder ----------------------";
139 if chinese_remainder(17,9) (3,4) = 35 then () else error "chinese_remainder(17,9)(3,4)=35 changed";
140 if chinese_remainder(7,2) (6,11) = 17 then () else error "chinese_remainder(7,2)(6,11)=17 changed";
142 "----------- fun is_prime -------------------------------";
143 "----------- fun is_prime -------------------------------";
144 "----------- fun is_prime -------------------------------";
145 if is_prime [2, 3] 2 = false then () else error "is_prime changed";
146 if is_prime [2, 3] 3 = false then () else error "is_prime changed";
147 if is_prime [2, 3] 4 = false then () else error "is_prime changed";
148 if is_prime [2, 3] 5 = true then () else error "is_prime changed";
149 if is_prime [2, 3, 5] 5 = false then () else error "is_prime changed";
150 if is_prime [2, 3] 6 = false then () else error "is_prime changed";
151 if is_prime [2, 3] 7 = true then () else error "is_prime changed";
152 if is_prime [2, 3] 25 = true then () else error "is_prime changed";
154 "----------- fun make_primes ----------------------------";
155 "----------- fun make_primes ----------------------------";
156 "----------- fun make_primes ----------------------------";
157 if make_primes [2, 3] 3 4 = [2, 3, 5] then () else error "make_primes changed";
158 if make_primes [2, 3] 3 5 = [2, 3, 5] then () else error "make_primes changed";
159 if make_primes [2, 3] 3 6 = [2, 3, 5, 7] then () else error "make_primes changed";
160 if make_primes [2, 3] 3 7 = [2, 3, 5, 7] then () else error "make_primes changed";
161 if make_primes [2, 3] 3 8 = [2, 3, 5, 7, 11] then () else error "make_primes changed";
162 if make_primes [2, 3] 3 9 = [2, 3, 5, 7, 11] then () else error "make_primes changed";
163 if make_primes [2, 3] 3 10 = [2, 3, 5, 7, 11] then () else error "make_primes changed";
164 if make_primes [2, 3] 3 11 = [2, 3, 5, 7, 11] then () else error "make_primes changed";
165 if make_primes [2, 3] 3 12 = [2, 3, 5, 7, 11, 13] then () else error "make_primes changed";
166 if make_primes [2, 3] 3 13 = [2, 3, 5, 7, 11, 13] then () else error "make_primes changed";
167 if make_primes [2, 3] 3 14 = [2, 3, 5, 7, 11, 13, 17] then () else error "make_primes changed";
168 if make_primes [2, 3] 3 15 = [2, 3, 5, 7, 11, 13, 17] then () else error "make_primes changed";
169 if make_primes [2, 3] 3 16 = [2, 3, 5, 7, 11, 13, 17] then () else error "make_primes changed";
170 if make_primes [2, 3] 3 17 = [2, 3, 5, 7, 11, 13, 17] then () else error "make_primes changed";
171 if make_primes [2, 3] 3 18 = [2, 3, 5, 7, 11, 13, 17, 19] then () else error "make_primes changed";
172 if make_primes [2, 3] 3 19 = [2, 3, 5, 7, 11, 13, 17, 19] then () else error "make_primes changed";
173 if make_primes [2, 3, 5, 7] 7 4 = [2, 3, 5, 7] then () else error "make_primes changed";
175 "----------- fun primes_upto ----------------------------";
176 "----------- fun primes_upto ----------------------------";
177 "----------- fun primes_upto ----------------------------";
178 if primes_upto 1 = [2] then () else error " primes_upto 1 = [2] changed";
179 if primes_upto 3 = [2,3] then () else error " primes_upto 3 = [2,3] changed";
180 if primes_upto 6 = [2,3,5,7] then () else error " primes_upto 6 = [2,3,5,7] changed";
181 if primes_upto 7 = [2,3,5,7] then () else error " primes_upto 7 = [2,3,5,7] changed";
183 "----------- fun next_prime_not_dvd ----------------";
184 "----------- fun next_prime_not_dvd ----------------";
185 "----------- fun next_prime_not_dvd ----------------";
186 if ( 1 next_prime_not_dvd 15) = 2 then () else error "next_prime_not_dvd ..changed";
187 if ( 2 next_prime_not_dvd 15) = 7 then () else error "next_prime_not_dvd ..changed";
188 if ( 3 next_prime_not_dvd 15) = 7 then () else error "next_prime_not_dvd ..changed";
189 if ( 4 next_prime_not_dvd 15) = 7 then () else error "next_prime_not_dvd ..changed";
190 if ( 5 next_prime_not_dvd 15) = 7 then () else error "next_prime_not_dvd ..changed";
191 if ( 6 next_prime_not_dvd 15) = 7 then () else error "next_prime_not_dvd ..changed";
192 if ( 7 next_prime_not_dvd 15) = 11 then () else error "next_prime_not_dvd ..changed";
194 "----------- fun lcoeff_up ------------------------------";
195 "----------- fun lcoeff_up ------------------------------";
196 "----------- fun lcoeff_up ------------------------------";
197 if lcoeff_up [3,4,5,6] = 6 then () else error "lcoeff_up (3,4,5,6) = 6 changed" ;
198 if lcoeff_up [3,4,5,6,0] = 6 then () else error "lcoeff_up (3,4,5,6,0) = 6 changed" ;
200 "----------- fun deg_up ---------------------------------";
201 "----------- fun deg_up ---------------------------------";
202 "----------- fun deg_up ---------------------------------";
203 if deg_up [3,4,5,6] = 3 then () else error "deg_up [3,4,5,6] = 3 changed" ;
204 if deg_up [3,4,5,6,0] = 3 then () else error "deg_up [3,4,5,6,0] = 3 changed";
206 "----------- fun drop_lc0_up ----------------------------";
207 "----------- fun drop_lc0_up ----------------------------";
208 "----------- fun drop_lc0_up ----------------------------";
209 if drop_lc0_up [0, 1, 2, 3, 4, 5, 0, 0] = [0, 1, 2, 3, 4, 5] then ()
210 else error "drop_lc0_up [0, 1, 2, 3, 4, 5, 0, 0] = [0, 1, 2, 3, 4, 5] changed";
211 if drop_lc0_up [0, 1, 2, 3, 4, 5] = [0, 1, 2, 3, 4, 5] then ()
212 else error "drop_lc0_up [0, 1, 2, 3, 4, 5]=[0, 1, 2, 3, 4, 5] changed";
214 "----------- fun normalise ------------------------------";
215 "----------- fun normalise ------------------------------";
216 "----------- fun normalise ------------------------------";
217 if (normalise [~18, ~15, ~20, 12, 20, ~13, 2] 5) = [1, 0, 0, 1, 0, 1, 1 ] then ()
218 else error "(normalise [~18, ~15, ~20, 12, 20, ~13, 2] 5) = [1, 0, 0, 1, 0, 1, 1 ] changed"
220 "----------- fun %* ------------------------------";
221 "----------- fun %* ------------------------------";
222 "----------- fun %* ------------------------------";
223 if ([5, 4, 7, 8, 1] %* 5) = [25, 20, 35, 40, 5] then ()
224 else error "[5, 4, 7, 8, 1] %* 5 = [25, 20, 35, 40, 5] changed";
225 if ([5, 4, ~7, 8, ~1] %* 5) = [25, 20, ~35, 40, ~5] then ()
226 else error "[5, 4, ~7, 8, ~1] %* 5 = [25, 20, ~35, 40, ~5] changed";
228 "----------- fun %/ -------------------------------";
229 "----------- fun %/ -------------------------------";
230 "----------- fun %/ -------------------------------";
231 if ([4, 3, 2, 5, 6] %/ 3) = [1, 1, 0, 1, 2] then ()
232 else error "%/ [4, 3, 2, 5, 6] 3 = [1, 1, 0, 1, 2] changed";
233 if ([4, 3, 2, 0] %/ 3) = [1, 1, 0, 0] then ()
234 else error "%/ [4, 3, 2, 0] 3 = [1, 1, 0, 0] changed";
236 "----------- fun %-% ------------------------------";
237 "----------- fun %-% ------------------------------";
238 "----------- fun %-% -----------------------------";
239 if ([8, ~7, 0, 1] %-% [~2, 2, 3, 0]) = [10, ~9, ~3, 1] then ()
240 else error "([8, ~7, 0, 1] %-% [~2, 2, 3, 0]) = [10, ~9, ~3, 1] changed";
241 if ([8, 7, 6, 5, 4] %-% [2, 2, 3, 1, 1]) = [6, 5, 3, 4, 3] then ()
242 else error "([8, 7, 6, 5, 4] %-% [2, 2, 3, 1, 1]) = [6, 5, 3, 4, 3] changed";
244 "----------- fun %|% -------------------------------";
245 "----------- fun %|% -------------------------------";
246 "----------- fun %|% -------------------------------";
247 if ([2, 3] %|% [8, 22, 15]) = true then () else error "[2, 3] %|% [8, 22, 15] = true changed";
248 if ([4] %|% [6]) = false then () else error "[4] %|% [6] = false changed";
249 if ([12] %|% [6]) = false then () else error "[12] %|% [6] = false changed";
250 if ([8] %|% [16, 0]) = true then () else error "[8] %|% [16, 0] = true changed";
251 if ([3, 2] %|% [0, 0, 9, 12, 4] ) = true then () else error "[3, 2] %|% [0,0,9..] = true changed";
252 if ([8, 0] %|% [16]) = true then () else error "[8,0] %|% [16] = true changed";
254 "----------- fun centr_up -----------------------------";
255 "----------- fun centr_up -----------------------------";
256 "----------- fun centr_up -----------------------------";
257 if centr_up [7, 3, 5, 8, 1, 3] 10 = [~3, 3, 5, ~2, 1, 3] then ()
258 else error "centr_up [7, 3, 5, 8, 1, 3] 10 = [~3, 3, 5, ~2, 1, 3] changed";
259 if centr_up [1, 2, 3, 4, 5] 2 = [1, 0, 1, 2, 3] then () else error "centr_up [1,.] 2 changed";
260 if centr_up [1, 2, 3, 4, 5] 3 = [1, ~1, 0, 1, 2] then () else error "centr_up [1,.] 3 changed";
261 if centr_up [1, 2, 3, 4, 5] 4 = [1, 2, ~1, 0, 1] then () else error "centr_up [1,.] 4 changed";
262 if centr_up [1, 2, 3, 4, 5] 5 = [1, 2, 3, ~1, 0] then () else error "centr_up [1,.] 5 changed";
263 if centr_up [1, 2, 3, 4, 5] 6 = [1, 2, 3, ~2, ~1] then () else error "centr_up [1,.]6 changed";
264 if centr_up [1, 2, 3, 4, 5] 7 = [1, 2, 3, 4, ~2] then () else error "centr_up [1,.] 7 changed";
265 if centr_up [1, 2, 3, 4, 5] 8 = [1, 2, 3, 4, ~3] then () else error "centr_up [1,.] 8 changed";
266 if centr_up [1, 2, 3, 4, 5] 9 = [1, 2, 3, 4, 5] then () else error "centr_up [1,.] 9 changed";
267 if centr_up [1, 2, 3, 4, 5] 10 = [1, 2, 3, 4, 5] then () else error "centr_up [1,.] 10 changed";
268 if centr_up [1, 2, 3, 4, 5] 11 = [1, 2, 3, 4, 5] then () else error "centr_up [1,.] 11 changed";
270 "----------- fun sum_lmb --------------------------------";
271 "----------- fun sum_lmb --------------------------------";
272 "----------- fun sum_lmb --------------------------------";
273 if sum_lmb [1, 2, 3, 4, 5] 1 = 15 then () else error "sum_lmb [1, 2, 3, 4, 5] 1 changed";
274 if sum_lmb [1, 2, 3, 4, 5] 2 = 55 then () else error "sum_lmb [1, 2, 3, 4, 5] 2 changed";
275 if sum_lmb [1, 2, 3, 4, 5] 3 = 225 then () else error "sum_lmb [1, 2, 3, 4, 5] 3 changed";
276 if sum_lmb [1, 2, 3, 4, 5] 4 = 979 then () else error "sum_lmb [1, 2, 3, 4, 5] 4 changed";
277 if sum_lmb [1, 2, 3, 4, 5] 5 = 4425 then () else error "sum_lmb [1, 2, 3, 4, 5] 5 changed";
278 if sum_lmb [1, 2, 3, 4, 5] 6 = 20515 then () else error "sum_lmb [1, 2, 3, 4, 5] 6 changed";
279 if sum_lmb [~1, 2, ~3, 4, ~5] 1 = ~3 then () else error "sum_lmb [~1, 2, ~3, 4, ~5] 1 changed";
280 if sum_lmb [~1, 2, ~3, 4, ~5] 2 = 55 then () else error "sum_lmb [~1, 2, ~3, 4, ~5] 2 changed";
281 if sum_lmb [~1, 2, ~3, 4, ~5] 3 = ~81 then () else error "sum_lmb [~1, 2, ~3, 4, ~5] 3 changed";
282 if sum_lmb [~1, 2, ~3, 4, ~5] 4 = 979 then () else error "sum_lmb [~1, 2, ~3, 4, ~5] 4 changed";
283 if sum_lmb [~1, 2, ~3, 4, ~5] 5 = ~2313 then () else error "sum_lmb [~1, 2, ~3, 4, ~5] 5 changed";
284 if sum_lmb [~1, 2, ~3, 4, ~5] 6 = 20515 then () else error "sum_lmb [~1, 2, ~3, 4, ~5] 6 changed";
286 "----------- fun LANDAU_MIGNOTTE_bound ------------------";
287 "----------- fun LANDAU_MIGNOTTE_bound ------------------";
288 "----------- fun LANDAU_MIGNOTTE_bound ------------------";
289 if LANDAU_MIGNOTTE_bound [1] [4, 5] = 1 then () else error "LANDAU_MIGNOTTE_bound 1";
290 if LANDAU_MIGNOTTE_bound [1, 2] [4, 5] = 2 then () else error "LANDAU_MIGNOTTE_bound 2";
291 if LANDAU_MIGNOTTE_bound [1, 2, 3] [4, 5] = 2 then () else error "LANDAU_MIGNOTTE_bound 3";
292 if LANDAU_MIGNOTTE_bound [1, 2, 3] [4] = 1 then () else error "LANDAU_MIGNOTTE_bound 4";
293 if LANDAU_MIGNOTTE_bound [1, 2, 3] [4, 5] = 2 then () else error "LANDAU_MIGNOTTE_bound 5";
294 if LANDAU_MIGNOTTE_bound [1, 2, 3] [4, 5, 6] = 12 then () else error "LANDAU_MIGNOTTE_bound 6";
295 if LANDAU_MIGNOTTE_bound [1, 2, 3] [4, 5] = LANDAU_MIGNOTTE_bound [4, 5] [1, 2, 3] then ()
296 else error "LANDAU_MIGNOTTE_bound 7";
297 if LANDAU_MIGNOTTE_bound [~1] [4, 5] = 1 then () else error "LANDAU_MIGNOTTE_bound 11";
298 if LANDAU_MIGNOTTE_bound [~1, 2] [4, 5] = 2 then () else error "LANDAU_MIGNOTTE_bound 12";
299 if LANDAU_MIGNOTTE_bound [~1, 2, ~3] [4, ~5] = 2 then () else error "LANDAU_MIGNOTTE_bound 13";
300 if LANDAU_MIGNOTTE_bound [~1, 2, ~3] [4] = 1 then () else error "LANDAU_MIGNOTTE_bound 14";
301 if LANDAU_MIGNOTTE_bound [~1, 2, ~3] [4, ~5] = 2 then () else error "LANDAU_MIGNOTTE_bound 15";
302 if LANDAU_MIGNOTTE_bound [~1, 2, ~3] [4, ~5, 6] = 12 then () else error "LANDAU_MIGNOTTE_bound 16";
303 if LANDAU_MIGNOTTE_bound [~1, 2, ~3] [4, ~5] = LANDAU_MIGNOTTE_bound [4, 5] [1, 2, 3] then ()
304 else error "LANDAU_MIGNOTTE_bound 17"
306 "----------- fun chinese_remainder_up -------------------";
307 "----------- fun chinese_remainder_up -------------------";
308 "----------- fun chinese_remainder_up -------------------";
309 if (chinese_remainder_up (5, 7) ([2, 2, 4, 3], [3, 2, 3, 5])) = [17, 2, 24, 33] then ()
310 else error "chinese_remainder_up (5, 7)... changed";
312 "----------- fun mod_up ---------------------------------";
313 "----------- fun mod_up ---------------------------------";
314 "----------- fun mod_up ---------------------------------";
315 if ([5, 4, 7, 8, 1] mod_up 5) = [0, 4, 2, 3, 1] then ()
316 else error "[5, 4, 7, 8, 1] mod_up 5 = [0, 4, 2, 3, 1] changed" ;
317 if ([5, 4, ~7, 8, ~1] mod_up 5) = [0, 4, 3, 3, 4] then ()
318 else error "[5, 4, ~7, 8, ~1] mod_up 5 = [0, 4, 3, 3, 4] changed" ;
320 "----------- fun mod_up_gcd -----------------------------";
321 "----------- fun mod_up_gcd -----------------------------";
322 "----------- fun mod_up_gcd -----------------------------";
323 if mod_up_gcd [~18, ~15, ~20, 12, 20, ~13, 2] [8, 28, 22, ~11, ~14, 1, 2] 7 =
324 [2, 6, 0, 2, 6] then ()
325 else error "( mod_up_gcd [~18, ~15, ~20, ...] [8, 28, 22, ...] 7 = [5, 1, 0, ..] changed";
326 if mod_up_gcd [8, 28, 22, ~11, ~14, 1, 2] [2, 6, 0, 2, 6] 7 = [2, 6, 0, 2, 6] then ()
327 else error "mod_up_gcd [8, 28, 22, ...] [2, 6, 0, ...] 7 = [1, 3, 0, 1, 3] changed";
328 if mod_up_gcd [20, 15, 8, 6] [8, ~2, ~2, 3] 2 = [0, 1] then ()
329 else error " mod_up_gcd [20, 15, 8, 6] [8, ~2, ~2, 3] 2 = [0, 1] changed";
331 "~~~~~ fun mod_up_gcd , args:";
332 val (a,b,m) = ([ ~13, 2,12],[ ~14, 2],5);
333 val moda = a mod_up m;
334 val modb = (replicate (length a - length(drop_lc0_up b)) 0) @ (drop_lc0_up b mod_up m) ;
335 val c = mod_div (lcoeff_up moda) (lcoeff_up modb) m;
336 val rest = drop_lc0_up (moda %-% (modb %* c) mod_up m) mod_up m;
337 rest = []; (*=false*)
338 length rest < length b; (*=false*)
339 "~~~~~ fun mod_up_gcd , args:";
340 val (a,b,m) = (rest, b , m );
341 val moda = a mod_up m
342 val modb = (replicate (length a - length(drop_lc0_up b)) 0) @ (drop_lc0_up b mod_up m) ;
343 val c = mod_div (lcoeff_up moda) (lcoeff_up modb) m
344 val rest = drop_lc0_up ((moda %-% (modb %* c)) mod_up m);
346 length rest < length b; (*=true*)
347 "~~~~~ fun mod_up_gcd , args:";
348 val (a,b,m) = (b, rest, m);
349 val moda = a mod_up m
350 val modb = (replicate (length a - length(drop_lc0_up b)) 0) @ (drop_lc0_up b mod_up m) ;
351 val c = mod_div (lcoeff_up moda) (lcoeff_up modb) m
352 val rest = drop_lc0_up ((moda %-% (modb %* c)) mod_up m);
354 length rest < length b; (*=false*)
355 "~~~~~ fun mod_up_gcd , args:";
356 val (a,b,m) = (rest,b, m);
357 val moda = a mod_up m
358 val modb = (replicate (length a - length(drop_lc0_up b)) 0) @ (drop_lc0_up b mod_up m) ;
359 val c = mod_div (lcoeff_up moda) (lcoeff_up modb) m
360 val rest = drop_lc0_up ((moda %-% (modb %* c)) mod_up m);
362 "~~~~~ to return val:"; val b = b;
364 "----------- fun primitive_up ---------------------------";
365 "----------- fun primitive_up ---------------------------";
366 "----------- fun primitive_up ---------------------------";
367 if primitive_up [12, 16, 32, 44] = [3, 4, 8, 11] then ()
368 else error "primitive_up [12, 16, 32, 44] = [3, 4, 8, 11] changed";
369 if primitive_up [4, 5, 12] = [4, 5, 12] then () else error "primitive_up [4, 5, 12] =[4, 5, 12] changed";
370 if primitive_up [0] = [0] then () else error "primitive_up [0] = [0] changed";
371 if primitive_up [6] = [1] then () else error "primitive_up [6] = [1] changed";
373 "----------- fun try_new_prime_up -----------------------";
374 "----------- fun try_new_prime_up -----------------------";
375 "----------- fun try_new_prime_up -----------------------";
376 "~~~~~ fun gcd_up, args:"; val (a, b) = ([~18, ~15, ~20, 12, 20, ~13, 2],
377 [8, 28, 22, ~11, ~14, 1, 2]);
378 "~~~~~ fun HENSEL_lifting_up, args:"; val (a, b, d, M, p) =
379 (a, b, (abs (Integer.gcd (lcoeff_up a) (lcoeff_up b))),
380 (2 * (abs (Integer.gcd (lcoeff_up a) (lcoeff_up b))) * LANDAU_MIGNOTTE_bound a b), 1);
381 val p = p next_prime_not_dvd d
383 val p = p next_prime_not_dvd d
384 val g_p = centr_up (((normalise (mod_up_gcd a b p) p) %* (d mod p)) mod_up p) p;
385 deg_up g_p = 0 (* = false*);
386 (*val g = primitive_up (try_new_prime_up a b d M p g_p p)*)
387 "~~~~~ fun try_new_prime_up, args:"; val (a, b, d, M, P, g, p) = (a, b, d, M, p, g_p, p);
389 val p' = p next_prime_not_dvd d;
390 val g_p = centr_up (( (normalise (mod_up_gcd a b p') p')
395 val (a, b, d, M, P, g, p) = (0, 0, 0, 0, 0, 0, 0) (*isolate test below*)
397 val (a, b) = ([~18, ~15, ~20, 12, 20, ~13, 2], [8, 28, 22, ~11, ~14, 1, 2])
398 val d = abs (Integer.gcd (lcoeff_up a) (lcoeff_up b))
399 val M = 2 * d * LANDAU_MIGNOTTE_bound a b
400 val p = 1 (*-> p in head of HENSEL_lifting_up*) next_prime_not_dvd d
401 val g_p = centr_up (((normalise (mod_up_gcd a b p) p) %* (d mod p)) mod_up p) p (*see above*)
402 val (a, b, d, M, P, g, p) = (a, b, d, M, p, g_p, p);
404 if try_new_prime_up a b d M P g p = [~1, 1, ~1] then () else error "try_new_prime_up changed";
406 (* ---- output from changeset cf55b1438731
407 try_new_prime_up: a = [~18, ~15, ~20, 12, 20, ~13, 2], b = [8, 28, 22, ~11, ~14, 1, 2],
408 d = 2, M = 10240, P = 12597, g = [~1, 1, ~1], p = 19
409 try_new_prime_up 1 -----> [~1, 1, ~1] *)
410 val (a, b, d, M, P, g, p) =
411 ([~18, ~15, ~20, 12, 20, ~13, 2], [8, 28, 22, ~11, ~14, 1, 2],
412 2, 10240, 3, [~1, 1, ~1], 3);
414 if try_new_prime_up a b d M P g p = [~1, 1, ~1]
415 then () else error "try_new_prime_up I [~18, ~15, ... changed";
417 (* ---- output from changeset cf55b1438731
418 try_new_prime_up: a = [~18, ~15, ~20, 12, 20, ~13, 2], b = [8, 28, 22, ~11, ~14, 1, 2],
419 d = 2, M = 10240, P = 96577, g = [~4, ~2, 2], p = 23
420 try_new_prime_up 1 -----> [~4, ~2, 2] *)
421 val (a, b, d, M, P, g, p) =
422 ([~18, ~15, ~20, 12, 20, ~13, 2], [8, 28, 22, ~11, ~14, 1, 2],
423 2, 10240, 5, [2, 2, 2, 2], 5);
424 if try_new_prime_up a b d M P g p = [~4, ~2, 2]
425 then () else error "try_new_prime_up II [~18, ~15, ... changed";
427 (* output for "gcd_up [~1, 0 ,1] [0, 1, 1] = [1, 1]" from changeset cf55b1438731
428 try_new_prime_up: a = [~1, 0, 1], b = [0, 1, 1], d = 1, M = 16, P = 2, g = [1, 1], p = 2
429 try_new_prime_up: a = [~1, 0, 1], b = [0, 1, 1], d = 1, M = 16, P = 6, g = [1, 1], p = 3
430 try_new_prime_up: a = [~1, 0, 1], b = [0, 1, 1], d = 1, M = 16, P = 30, g = [1, 1], p = 5
431 try_new_prime_up 1 -----> [1, 1]*)
432 val (a, b, d, M, P, g, p) = ([~1, 0, 1], [0, 1, 1], 1, 16, 2, [1, 1], 2);
433 if try_new_prime_up a b d M P g p = [1, 1]
434 then () else error "try_new_prime_up [~1, 0, ... changed";
436 "----------- fun gcd_up ---------------------------------";
437 "----------- fun gcd_up ---------------------------------";
438 "----------- fun gcd_up ---------------------------------";
439 if gcd_up [~18, ~15, ~20, 12, 20, ~13, 2] [8, 28, 22, ~11, ~14, 1, 2] = [~2, ~1, 1]
440 then () else error "gcd_up [~1, 0 ... changed";
441 if gcd_up [~1, 0 ,1] [0, 1, 1] = [1, 1]
442 then () else error "gcd_up [~1, 0 ... changed";
444 "=========== Multivariate Case ==========================";
445 "=========== Multivariate Case ==========================";
446 "=========== Multivariate Case ==========================";
448 "----------- fun lcoeff ---------------------------------";
449 "----------- fun lcoeff ---------------------------------";
450 "----------- fun lcoeff ---------------------------------";
451 if lcoeff [(1,[1,1]),(2,[1,2]),(3,[1,3]),(4,[1,4]),(5,[1,5])] = 5 then () else
452 error "lcoeff [(1,[1,1]),(2,[1,2]),(3,[1,3]),(4,[1,4]),(5,[1,5])] = 5 changed";
454 "----------- fun lexp -----------------------------------";
455 "----------- fun lexp -----------------------------------";
456 "----------- fun lexp -----------------------------------";
457 if lexp [(1,[1,1]),(2,[1,2]),(3,[1,3]),(4,[1,4]),(5,[1,5])] = [1,5] then () else
458 error "get_coeff [(1,[1,1]),(2,[1,2]),(3,[1,3]),(4,[1,4]),(5,[1,5])] = [1,5] changed";
460 "----------- fun add_variable ---------------------------";
461 "----------- fun add_variable ---------------------------";
462 "----------- fun add_variable ---------------------------";
464 [(1,[1,2]),(2,[2,3])] = [(1, [0, 1, 2]), (2, [0, 2, 3])] then () else
465 error "add_variable [(1,[1,2]),(2,[2,3])] 0 = [(1, [0, 1, 2]), (2, [0, 2, 3])] changed";
467 [(1,[1,2]),(2,[2,3])] = [(1, [1, 0, 2]), (2, [2, 0, 3])] then () else
468 error "add_variable [(1,[1,2]),(2,[2,3])] 1 = [(1, [1, 0, 2]), (2, [2, 0, 3]) changed";
470 [(1,[1,2]),(2,[2,3])] = [(1, [1, 2, 0]), (2, [2, 3, 0])] then () else
471 error "add_variable [(1,[1,2]),(2,[2,3])] 2 = [(1, [1, 2, 0]), (2, [2, 3, 0])] changed";
473 "----------- fun zero_poly ------------------------------";
474 "----------- fun zero_poly ------------------------------";
475 "----------- fun zero_poly ------------------------------";
476 if zero_poly 1 = [(0, [0])] then () else
477 error "zero_poly 1 = [(0, [0])] changed";
478 if zero_poly 5 = [(0, [0, 0, 0, 0, 0])] then () else
479 error "zero_poly 1 = [(0, [0, 0, 0, 0, 0])] changed";
481 "----------- drop_lc0 -----------------------------------";
482 "----------- drop_lc0 -----------------------------------";
483 "----------- drop_lc0 -----------------------------------";
484 if drop_lc0 [(4,[2]),(3,[3])] = [(4,[2]),(3,[3])] then ()
485 else error "drop_lc0 [(4,[2]),(3,[3])] = [(4,[2]),(3,[3])] changed";
486 if drop_lc0 [(4,[2]),(0,[3])] = [(4,[2])] then ()
487 else error "drop_lc0 [(4,[2]),(3,[3])] = [(4,[2])] changed";
488 if drop_lc0 [(0,[2]),(3,[3])] = [(0,[2]),(3,[3])] then ()
489 else error "drop_lc0 [(0,[2]),(3,[3])] = [(0,[2]),(3,[3])] changed";
490 if drop_lc0 [(0,[2]),(0,[3])] = [(0,[0])] then ()
491 else error "drop_lc0 [(0,[2]),(0,[3])] = [(0,[0])] changed";
493 "----------- fun add_monoms -----------------------------";
494 "----------- fun add_monoms -----------------------------";
495 "----------- fun add_monoms -----------------------------";
496 if add_monoms [(~3,[0,0]),(4,[0,0]),(3,[1,1]),(~3,[1,1]),(2,[1,2]),(~3,[1,2])] =
497 [(1, [0, 0]), (~1, [1, 2])]
498 then () else error ("add_monoms [(~3,[0,0]),(4,[0,0]),(3,[1,1]),(~3,[1,1]),(2,[1,2]),(~3,[1,2])] " ^
499 "= [(1, [0, 0]), (~1, [1, 2])] changed")
501 "----------- fun lex_ord --------------------------------";
502 "----------- fun lex_ord --------------------------------";
503 "----------- fun lex_ord --------------------------------";
504 if lex_ord (000, [3]) (000, [4])
505 then error " lex_ord (000, [3]) (000, [4]) changed = false" else ();
506 if lex_ord (000, [1,2]) (000, [0,3])
507 then error " lex_ord [1,2] [0,3] changed = false" else ();
508 if lex_ord (000, [1,2]) (000, [3,0])
509 then () else error " lex_ord [1,2] [3,0] = true changed";
510 if lex_ord (000, [1,2]) (000, [1,2])
511 then error " lex_ord [1,2] [1,2] changed = false" else ();
513 "----------- fun order ----------------------------------";
514 "----------- fun order ----------------------------------";
515 "----------- fun order ----------------------------------";
516 if order [(3,[1,1]),(2,[1,2]),(~3,[0,0]),(~3,[1,1]),(~3,[1,2]),(4,[0,0])] =
517 [(1, [0, 0]), (~1, [1, 2])]
518 then () else error ("order [(3,[1,1]),(2,[1,2]),(~3,[0,0]),(~3,[1,1]),(~3,[1,2]),(4,[0,0])]" ^
519 " = [(1, [0, 0]), (~1, [1, 2])] changed")
521 (*"----------- fun lcoeff ---------------------------";
522 "----------- fun lcoeff ---------------------------";
523 "----------- fun lcoeff ---------------------------";
524 if lcoeff [(~3,[0,0]),(4,[0,0]),(3,[1,1]),(~3,[1,1]),(2,[1,2]),(~3,[1,2])] = ~1
525 then () else error "lcoeff [(~3,[0,0]),(4,[0,0]),(3,[1,1]),(~3,[1,1]),(2,[1,2]),(~3,[1,2])] = ~1 changed";
526 if lcoeff [(3,[1,1]),(2,[1,2]),(~3,[0,0])] = 2
527 then () else error "lcoeff [(3,[1,1]),(2,[1,2]),(~3,[0,0])] = 2 changed";*)
529 "----------- fun lexp -----------------------------------";
530 "----------- fun lexp -----------------------------------";
531 "----------- fun lexp -----------------------------------";
532 if lexp [(~3,[0,0]),(4,[0,0]),(3,[1,1]),(~3,[1,1]),(2,[1,2])] = [1,2]
533 then () else error "lexp [(~3,[0,0]),(4,[0,0]),(3,[1,1]),(~3,[1,1]),(2,[1,2])] = ~1 changed";
535 "----------- fun max_deg_var ----------------------------";
536 "----------- fun max_deg_var ----------------------------";
537 "----------- fun max_deg_var ----------------------------";
538 if max_deg_var [(1,[1,2]),(2,[2,3]),(3,[5,4]),(1,[0,0])] 0 = 5 then ()
539 else error " max_deg_var [(1,[1,2]),(2,[2,3]),(3,[5,4]),(1,[0,0])] 0 = 5 changed";
540 if max_deg_var [(1,[1,2]),(2,[2,3]),(3,[5,4]),(1,[0,0])] 1 = 4 then ()
541 else error " max_deg_var [(1,[1,2]),(2,[2,3]),(3,[5,4]),(1,[0,0])] 1 = 4 changed";
543 "----------- infix %%/ ----------------------------------";
544 "----------- infix %%/ ----------------------------------";
545 "----------- infix %%/ ----------------------------------";
546 if ([(~3, [2, 0]), (~6, [1, 1]), (~1, [3, 1]),(1, [5, 0]), (2, [4, 1])] %%/ 2) =
547 [(~1, [2, 0]), (~3, [1, 1]), (1, [4, 1])] then ()
548 else error ("[(~3, [2, 0]), (~6, [1, 1]), (~1, [3, 1]),(1, [5, 0]), (2, [4, 1])] %%/ 2 = " ^
549 "[(~1, [2, 0]), (~3, [1, 1]), (1, [4, 1])] changed");
551 "----------- infix %%*%% --------------------------------";
552 "----------- infix %%*%% --------------------------------";
553 "----------- infix %%*%% --------------------------------";
554 val p1 = [(1,[1,0]), (1,[0,1])]; (* a + b *)
555 val p2 = [(1,[1,0]), (~1,[0,1])]; (* a - b *)
556 val p = [(1, [2, 0]), (~1, [0, 2])]; (* a^2 - b^2 *)
557 if (p1 %%*%% p2) = p then () else error "%%*%% changed";
559 val p1 = order [(1,[1,2,3]), (2,[2,2,2]), (3,[3,2,1])]: poly;
560 val p2 = order [(10,[1,2,3]), (20,[1,1,1]), (30,[3,2,1])]: poly;
562 [(60, [4, 3, 2]), (90, [6, 4, 2]), (40, [3, 3, 3]), (60, [5, 4, 3]),
563 (20, [2, 3, 4]), (60, [4, 4, 4]), (20, [3, 4, 5]), (10, [2, 4, 6])] then ()
564 else error "%%*%% changed"
566 "----------- fun gcd_coeff ------------------------------";
567 "----------- fun gcd_coeff ------------------------------";
568 "----------- fun gcd_coeff ------------------------------";
569 if gcd_coeff [4,8,12,~2,0,~4] = 2 then () else error " gcd_coeff [4,8,12,~2,0,~4] = 2 changed";
570 if gcd_coeff [3,6,9,19] = 1 then () else error " gcd_coeff [3,6,9,19] = 1 changed";
572 (*"----------- fun gcd_coeff_poly -------------------------";
573 "----------- fun gcd_coeff_poly -------------------------";
574 "----------- fun gcd_coeff_poly -------------------------";
575 if gcd_coeff_poly [(3,[1,2,3,1])] = 3 then () else error " gcd_coeff_poly [(3,[1,2,3,1])] = 3 changed";
576 if gcd_coeff_poly [(~2, [2, 0]), (4, [5, 0]),(~4, [3, 2]), (2, [2, 3])] = 2 then ()
577 else error "gcd_coeff_poly [(~2, [2, 0]), (4, [5, 0]),(~4, [3, 2]), (2, [2, 3])] = 2 changed";
578 if gcd_coeff_poly [(~2, [2, 0]), (5, [5, 0]),(~4, [3, 2]), (2, [2, 3])] = 1 then ()
579 else error "gcd_coeff_poly [(~2, [2, 0]), (5, [5, 0]),(~4, [3, 2]), (2, [2, 3])] = 1 changed";*)
581 "----------- fun eval -----------------------------------";
582 "----------- fun eval -----------------------------------";
583 "----------- fun eval -----------------------------------";
584 if eval [(~3, [2, 1]), (2, [0, 1]), (1,[2, 0])] 0 1 = [(1, [0]), (~1, [1])] then ()
585 else error " eval [(~3, [2, 1]), (2, [0, 1]),(1,[2,0])] 0 1 = [(1, [0]), (~1, [1])] changed";
586 if eval [(~3, [2, 1]), (2, [0, 1]), (1,[2, 0])] 1 1 = [(2, [0]), (~2, [2])] then ()
587 else error " eval [(~3, [2, 1]), (2, [0, 1]),(1,[2,0])] 1 1 =[(2, [0]), (~2, [2])] changed";
588 if eval [(~3, [2, 1]), (2, [0, 1]), (1,[2, 0])] 0 3 = [(9, [0]), (~25, [1])] then ()
589 else error " eval [(~3, [2, 1]), (2, [0, 1]),(1,[2,0])] 0 3 = [(9, [0]), (~25, [1])] changed";
590 if eval [(~3, [2, 1]), (2, [0, 1]), (1,[2, 0])] 1 3 = [(6, [0]), (~8, [2])] then ()
591 else error " eval [(~3, [2, 1]), (2, [0, 1]),(1,[2,0])] 1 3 = [ (6, [0]), (~8, [2])] changed";
593 "----------- fun multi_to_uni ---------------------------";
594 "----------- fun multi_to_uni ---------------------------";
595 "----------- fun multi_to_uni ---------------------------";
596 if multi_to_uni [(~3, [1]), (2, [1]), (1, [0])] = [1, ~1]
597 then () else error " multi_to_uni [(~3, [1]), (2, [1]), (1, [0])] = [1, ~1] changed";
599 "----------- fun uni_to_multi ---------------------------";
600 "----------- fun uni_to_multi ---------------------------";
601 "----------- fun uni_to_multi ---------------------------";
602 if uni_to_multi [~11, 11, 22, 33, 44, 55] =
603 [(~11, [0]), (11, [1]), (22, [2]), (33, [3]), (44, [4]), (55, [5])] then ()
604 else error "uni_to_multi changed";
606 if uni_to_multi [1,2,1,1,3,4] = [(1, [0]), (2, [1]), (1, [2]), (1, [3]), (3, [4]), (4, [5])] then ()
607 else error "uni_to_multi [1,2,1,1,3,4] = [(1, [0]), (2, [1]), (1, [2]), (1, [3]), (3, [4]), (4, [5])] changed";
608 if uni_to_multi [1,2,0,0,5,6] = [(1, [0]), (2, [1]), (5, [4]), (6, [5])] then ()
609 else error "uni_to_multi [1,2,0,0,5,6] = [(1, [0]), (2, [1]), (5, [4]), (6, [5])] changed";
612 "----------- fun find_new_r ----------------------------";
613 "----------- fun find_new_r ----------------------------";
614 "----------- fun find_new_r ----------------------------";
615 if find_new_r [(2,[0,0]),(1,[1,2])] [(4,[2,2]),(1,[1,2])] ~1 = 1 then ()
616 else error " find_new_r [(2,[0,0]),(1,[1,2])] [(4,[2,2]),(1,[1,2])] ~1 = 1 changed";
617 if find_new_r [(2,[0,0]),(1,[1,2])] [(4,[2,2]),(1,[1,2])] 1 = 2 then ()
618 else error "find_new_r [(2,[0,0]),(1,[1,2])] [(4,[2,2]),(1,[1,2])] 1 = 2 changed";
619 if find_new_r [(2,[1,2]),(~4,[0,2]),(2,[1,1])] [(1,[1,3]),(~2,[0,3])] 1 = 3 then ()
620 else error "find_new_r [(2,[1,2]),(~4,[0,2]),(2,[1,1])] [(1,[1,3]),(~2,[0,3])] 1 = 3 changed";
622 "----------- fun mult_with_new_var ---------------------";
623 "----------- fun mult_with_new_var ---------------------";
624 "----------- fun mult_with_new_var ---------------------";
625 if mult_with_new_var [(3,[0]),(2,[1])] [~1,1] 0 = [(~3, [0, 0]), (3, [1, 0]), (~2, [0, 1]), (2, [1, 1])] then ()
626 else error "mult_with_new_var [(3,[0]),(2,[1])] [~1,1] 0 = [(~3, [0, 0]), (3, [1, 0]), (~2, [0, 1]), (2, [1, 1])] changed";
628 (*"----------- fun greater_deg -----------------";
629 "----------- fun greater_deg -----------------";475
630 "----------- fun greater_deg -----------------";
631 greater_deg [1,2,3] [1,2,4] =2;*)
633 "----------- infix %%+%% -------------------------------";
634 "----------- infix %%+%% -------------------------------";
635 "----------- infix %%+%% -------------------------------";
636 if ([(3,[0,0]),(2,[3,2]),(~3,[1,3])] %%+%% [(3,[3,2]),(~1,[0,0]),(2,[1,1])]) = [(2, [0, 0]), (2, [1, 1]), (5, [3, 2]), (~3, [1, 3])]
637 then () else error "([(3,[0,0]),(2,[3,2]),(~3,[1,3])] %%+%% [(3,[3,2]),(~1,[0,0]),(2,[1,1])]) = [(2, [0, 0]), (2, [1, 1]), (5, [3, 2]), (~3, [1, 3])] changed";
639 "----------- infix %%-%% -------------------------------";
640 "----------- infix %%-%% -------------------------------";
641 "----------- infix %%-%% -------------------------------";
642 if ([(2, [0, 0]), (2, [1, 1]), (5, [3, 2]), (~3, [1, 3])] %%-%% [(3,[3,2]),(~1,[0,0]),(2,[1,1])]) = [(3, [0, 0]), (2, [3, 2]), (~3, [1, 3])]
643 then () else error "([(2, [0, 0]), (2, [1, 1]), (5, [3, 2]), (~3, [1, 3])] %%-%% [(3,[3,2]),(~1,[0,0]),(2,[1,1])]) = [(3, [0, 0]), (2, [3, 2]), (~3, [1, 3])] changed";
645 "----------- infix %%*%% -------------------------------";
646 "----------- infix %%*%% -------------------------------";
647 "----------- infix %%*%% -------------------------------";
648 if ([(~1,[0]),(1,[1])] %%*%% [(~2,[0]),(1,[1])]) = [(2, [0]), (~3, [1]), (1, [2])]
649 then () else error "([(~1,[0]),(1,[1])] %%*%% [(~2,[0]),(1,[1])]) = [(2, [0]), (~3, [1]), (1, [2])] changed";
650 if ([(~2,[0]),(1,[1])] %%*%% [(1,[1]),(2,[0])]) = [(~4, [0]), (1, [2])] then ()
651 else error "([(~2,[0]),(1,[1])] %%*%% [(1,[1]),(2,[0])]) = [(~4, [0]), (1, [2])] changed";
652 if ([(3,[0,0]),(2,[0,1])] %%*%% [(1,[1,0]),(~1,[0,0])]) = mult_with_new_var [(3,[0]),(2,[1])] [~1,1] 0
654 "([(3,[0,0]),(2,[0,1])] %%*%% [(1,[1,0]),(~1,[0,0])]) = mult_with_new_var [(3,[0]),(2,[1])] [~1,1] 0 changed";
656 "----------- infix %%/%% -------------------------------";
657 "----------- infix %%/%% -------------------------------";
658 "----------- infix %%/%% -------------------------------";
659 val a = [(1,[2, 0]), (1,[1, 1]), (~1,[0, 2])]; (* (x^2 + x - y) / (x - y) = *)
660 val b = [(~1, [1, 0]), (1, [0, 1])];
661 val (c, r) = (a %%/%% b);
662 if (c, r) = ([(~1, [0, 1])], [(1, [2, 0])]) then () else error "%%/%% changed";
663 if ((c %%*%% b) %%+%% r) = a then () else error "%%/%% changed";
665 "----------- fun newton_first --------------------------";
666 "----------- fun newton_first --------------------------";
667 "----------- fun newton_first --------------------------";
668 if newton_first [1, 2] [[(1,[1,1])], [(4,[1,1])]] 1 =
669 ([(~2, [1, 0, 1]), (3, [1, 1, 1])], [~1, 1], [[(3, [1, 1])]])
671 "newton_first [1, 2] [[(1,[1,1])], [(4,[1,1])]] 1 = "
672 "([(~2, [1, 0, 1]), (3, [1, 1, 1])], [~1, 1], [[(3, [1, 1])]]) changed";
674 "----------- fun NEWTON --------------------------------";
675 "----------- fun NEWTON --------------------------------";
676 "----------- fun NEWTON --------------------------------";
677 if NEWTON [1, 2 ] [[(1,[1,1])], [(4,[1,1])]] [] [1] (zero_poly 2) 1 =
678 ([(~2, [1, 0, 1]), (3, [1, 1, 1])], [~1, 1], [[(3, [1, 1])]])
680 "NEWTON [1, 2 ] [[(1,[1,1])], [(4,[1,1])]] [] [1] (zero_poly 2) 1 = "
681 "([(~2, [1, 0, 1]), (3, [1, 1, 1])], [~1, 1], [[(3, [1, 1])]]) changed";
682 if NEWTON [1, 2, 3 ] [[(4,[1,1])], [(9,[1,1])]] [[(3, [1, 1])]] [~1, 1] [(~2, [1, 0, 1]), (3, [1, 1, 1])] 1 =
683 ([(1, [1, 2, 1])], [2, ~3, 1], [[(5, [1, 1])], [(1, [1, 1])]])
685 "NEWTON [1, 2, 3 ] [[(4,[1,1])], [(9,[1,1])]] [[(3, [1, 1])]] [~1, 1] [(~2, [1, 0, 1]), (3, [1, 1, 1])] 1 ="
686 " ([(1, [1, 2, 1])], [2, ~3, 1], [[(5, [1, 1])], [(1, [1, 1])]]) changed";
689 "~~~~~ fun NEWTON, args:"; val (x,f,steps,t,p,ord) = ([1, 2, 3, 4],[[(9, [0]), (5, [1])], [(16, [0]), (7, [1])]], [[(5, [0]), (2, [1])], [(1, [0])]], [2, ~3, 1], [(1, [2, 0]), (~1, [0, 1]), (2, [1, 1])], 0 );
690 length x = 2; (* false *)
691 val new_value_poly = multi_to_uni((uni_to_multi t) %%*%% (uni_to_multi [(nth x (length x -2) )* ~1, 1]));
692 val new_steps = [((nth f (length f -1)) %%/ ((nth x (length x - 1)) - (nth x (length x - 2)))) %%-%% ((nth f (length f -2)))];
694 "~~~~~ fun next_step, args:"; val (steps,new_steps, x') = (steps, new_steps, x);
695 steps = []; (*false*)
697 "~~~~~ fun next_step, args:"; val (steps,new_steps, x') = (nth_drop 0 steps, new_steps @ [(((nth new_steps (length new_steps -1)) %%-%%(nth steps 0))) %%/
698 ((nth x' (length x' - 1)) - (nth x' (length x' - 3)))], nth_drop (length x' -2) x');steps = []; (*false*)
700 "~~~~~ fun next_step, args:"; val (steps,new_steps, x') = (nth_drop 0 steps, new_steps @ [(((nth new_steps (length new_steps -1)) %%-%%(nth steps 0))) %%/
701 ((nth x' (length x' - 1)) - (nth x' (length x' - 3)))], nth_drop (length x' -2) x');
703 val steps = new_steps;
704 val polynom' = p %%+%% (mult_with_new_var (nth steps (length steps -1)) new_value_poly ord);
706 "----------- fun all_geq -------------------------------";
707 "----------- fun all_geq -------------------------------";
708 "----------- fun all_geq -------------------------------";
709 if all_geq [1,2,3,4,5] [1,2,3,4,5] = true then ()
710 else error " all_geq [1,2,3,4,5] [1,2,3,4,5] = true changed";
711 if all_geq [1,2,3,4] [1,2,3,5] = false then ()
712 else error "all_geq [1,2,3,4] [1,2,3,5] = false changed" ;
713 if all_geq [1,4,5,4] [0,3,4,5] = false then ()
714 else error "all_geq [1,2,3,4] [0,3,4,5] = false changed ";
716 "----------- fun greater_deg ---------------------------";
717 "----------- fun greater_deg ---------------------------";
718 "----------- fun greater_deg ---------------------------";
719 if greater_deg [1,2,3,4,5] [1,2,3,4,5] = 0 then ()
720 else error " greater_deg [1,2,3,4,5] [1,2,3,4,5] = 0 changed";
721 if greater_deg [1,2,3,4] [5,2,8,1] = 1 then ()
722 else error "greater_deg [1,2,3,4] [1,2,3,5] = 1 changed" ;
723 if greater_deg [1,4,5,4] [0,3,4,5] = 2 then ()
724 else error "greater_deg [1,2,3,4] [0,3,4,5] = 2 changed ";
726 "----------- infix %%|%% --------------------------------";
727 "----------- infix %%|%% --------------------------------";
728 "----------- infix %%|%% --------------------------------";
729 if [(1, [0, 0]), (~1, [0, 1])] %%|%% [(1, [0, 0]), (~1, [0, 1])] then ()
731 else error "[(1, [0, 0]), (~1, [0, 1])] %%|%% [(1, [0, 0]), (~1, [0, 1])] = true changed";
733 if [(3,[1,0])] %%|%% [(9,[1,1]),(12,[2,1]),(~3,[1,2])] then ()
734 (* 3 x | 9 x y + 12 x^2 y - 3 x y^2 *)
735 else error "[(3,[1,0])] %%|%% [(9,[1,1]),(12,[2,1]),(~3,[1,2])] = true changed";
737 if [(3,[2,1])] %%|%% [(9,[1,1]),(12,[2,1]),(~3,[1,2])]
738 (* 3 x^2 y | 9 x y + 12 x^2 y - 3 x y^2 *)
739 then error "[(3,[2,1])] %%|%% [(9,[1,1]),(12,[2,1]),(~3,[1,2])] = false changed" else ();
741 "----------- fun gcd_poly' ------------------------------";
742 "----------- fun gcd_poly' ------------------------------";
743 "----------- fun gcd_poly' ------------------------------";
744 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])]
745 [(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
746 = [(1, [2, 0]), (~1, [0, 1]), (2, [1, 1])] then () else error
747 "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])]"
748 "[(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 "
749 "= [(1, [2, 0]), (~1, [0, 1]), (2, [1, 1])] changed";
750 (* -xy +xy^2z+yz - 1*)(* xy +1*) (*=*) (*xy -1*)
751 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
752 = [(~1, [0, 0, 0]), (~1, [1, 1, 0])] then () else error
753 "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 "
754 "= [(1, [0, 0, 0]), (1, [1, 1, 0])] changed";
756 "----------- fun gcd_poly ------------------------------";
757 "----------- fun gcd_poly ------------------------------";
758 "----------- fun gcd_poly ------------------------------";
760 [(~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])]
761 (* ~3 x^2 + x^5 + 3 y - 6 x y - x^3 y + 2 x^4 y + x^3 y^2 - x y^3 + 2 x^2 y^3*)
762 [(2,[2,0]),(~2,[0,1]),(4,[1,1]),(~1,[3,1]),(1,[1,2]),(~1,[2,2]),(~1,[0,3]),(2,[1,3])]
763 (* 2 x^2 - 2 y + 4 x y - x^3 y + x y^2 - x^2 y^2 - y^3 + 2 x y^3*)
764 = (([(~3, [0, 0]), (1, [3, 0]), (1, [1, 2])], [(2, [0, 0]), (~1, [1, 1]), (1, [0, 2])]),
765 (*( 3 + x^3 + x y^2 ,, 2 - x y + y^2 ),,*)
766 [(1, [2, 0]), (~1, [0, 1]), (2, [1, 1])])
768 then () else error "gcd_poly ex1 changed";
771 [(~1,[0,0,0]),(1,[0,1,1]),(1,[1,2,1]),(~1,[1,1,0])]
772 (* ~1 + y z + x y^2 z - x y *)
773 [(1,[0,0,0]),(1,[1,1,0])]
775 = (([(~1, [0,0,0]), (1, [0,1,1])], [(1, [0,0,0])]), [(1, [0,0,0]), (1, [1,1,0])])
776 (* ( ~1 + y z ,, 1 ),, 1 + x y *)
777 then () else error "gcd_poly ex2 changed";
779 (* example from unipoly: *)
780 val a = uni_to_multi [~18, ~15, ~20, 12, 20, ~13, 2];
781 val b = uni_to_multi [8, 28, 22, ~11, ~14, 1, 2];
782 val ((a', b'), c) = gcd_poly a b;
784 a' = [(9, [0]), (3, [1]), (13, [2]), (~11, [3]), (2, [4])];
785 b' = [(~4, [0]), (~12, [1]), (~7, [2]), (3, [3]), (2, [4])];
786 c = [(~2, [0]), (~1, [1]), (1, [2])];
787 (* checking the postcondition: *)
788 if a = (a' %%*%% c) andalso b = (b' %%*%% c) then () else error "gcd_poly ex-unipoly changed";
789 (* \<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 *)
791 val cu = gcd_up [~18, ~15, ~20, 12, 20, ~13, 2] [8, 28, 22, ~11, ~14, 1, 2];
792 if cu = multi_to_uni c then () else error "gcd_up <> gcd_poly";
794 (* example from mail to Tobias Nipkos *)
795 val a = [(1,[2, 0]), (~1,[0, 2])]; (* x^2 - y^2 *)
796 val b = [(1,[2, 0]), (~1,[1, 1])]; (* x^2 - x y *)
797 val ((a', b'), c) = gcd_poly a b;
799 a' = [(1, [1, 0]), (1, [0, 1])]; (* x + y *)
800 b' = [(1, [1, 0])]; (* x *)
801 c = [(1, [1, 0]), (~1, [0, 1])]; (* x - y *)
802 (* checking the postcondition: *)
803 if a = (a' %%*%% c) andalso b = (b' %%*%% c) then () else error "gcd_poly mail changed";
804 (* \<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 *)
806 (* regression test for --- fun gcd_poly downto division by zero ---*)
807 val a = [(9, [5, 2, 4])]: poly
808 val b = [(15, [6, 3, 1])]: poly
809 val ((a', b'), c) = gcd_poly a b;
810 if a = (a' %%*%% c) andalso b = (b' %%*%% c) then () else error "regression test changed";
812 (* regression test for --- integration lev.1 -- lev.5 in rational.sml *)
813 val a = [(1, [0, 1, 1, 0, 1]), (1, [1, 0, 0, 1, 1])]: poly
814 val b = [(1, [0, 1, 0, 1, 1])]: poly
815 val ((a', b'), c) = gcd_poly a b;
817 a' = [(1, [0, 1, 1, 0, 0]), (1, [1, 0, 0, 1, 0])];
818 b' = [(1, [0, 1, 0, 1, 0])];
819 c = [(1, [0, 0, 0, 0, 1])];
820 if a = (a' %%*%% c) andalso b = (b' %%*%% c) then () else error "gcd_monom changed";
822 "----------- fun gcd_poly downto division by zero -------";
823 "----------- fun gcd_poly downto division by zero -------";
824 "----------- fun gcd_poly downto division by zero -------";
825 "-------- example 187a: exception Div raised... REGRSSION TEST FOR REMOVAL OF THIS BUG IS ABOVE";
826 val a = [(12, [1, 1])]: poly
827 val b = [(8, [0, 2])]: poly;
828 (* val ((a', b'), c) = gcd_poly a b
829 exception Div raised*)
830 "~~~~~ fun gcd_poly, args:"; val ((a as (_, es)::_ : poly), b) = (a, b);
831 (* val c = gcd_poly' a b (length es) 0
832 exception Div raised*)
833 "~~~~~ fun gcd_poly', args:"; val ((a as (_, es1)::_ : poly), (b as (_, es2)::_ : poly), n, r) =
834 (a, b, (length es), 0);
835 lex_ord (lmonom b) (lmonom a) = true;
837 exception Div raised*)
838 "~~~~~ fun gcd_poly', args:"; val ((a as (_, es1)::_ : poly), (b as (_, es2)::_ : poly), n, r) =
840 lex_ord (lmonom b) (lmonom a) = false;
842 val M = 1 + Int.min (max_deg_var a (length es1 - 2), max_deg_var b (length es2 - 2));
843 (*try_new_r a b n M r [] []
844 exception Div raised*)
845 "~~~~~ and try_new_r, args:"; val (a, b, n, M, r, r_list, steps) = (a, b, n, M, r, [], []);
846 val r = find_new_r a b r;
847 val r_list = r_list @ [r];
848 val g_r = gcd_poly' (order (eval a (n - 2) r))
849 (order (eval b (n - 2) r)) (n - 1) 0
850 val steps = steps @ [g_r];
851 (*HENSEL_lifting a b n M 1 r r_list steps g_r ( zero_poly n ) [1]
852 exception Div raised*)
853 "~~~~~ and HENSEL_lifting, args:"; val (a, b, n, M, m, r, r_list, steps, g, g_n, mult) =
854 (a, b, n, M, 1, r, r_list, steps, g_r, (zero_poly n), [1]);
856 val r = find_new_r a b r;
857 val r_list = r_list @ [r];
858 val g_r = gcd_poly' (order (eval a (n - 2) r))
859 (order (eval b (n - 2) r)) (n - 1) 0;
860 lex_ord (lmonom g) (lmonom g_r) = false;
861 lexp g = lexp g_r = true;
862 val (g_n, new, steps) = NEWTON r_list [g, g_r] steps mult g_n (n - 2);
863 nth steps (length steps - 1) = zero_poly (n - 1) = false;
864 (*HENSEL_lifting a b n M (m + 1) r r_list steps g_r g_n new
865 exception Div raised*)
866 "~~~~~ and HENSEL_lifting, args:"; val (a, b, n, M, m, r, r_list, steps, g, g_n, mult) =
867 (a, b, n, M, m + 1, r, r_list, steps, g_r, g_n, new);
869 (g_n %%|%% a andalso (g_n %%|%% b)) = false;
870 (*try_new_r a b n M r r_list steps
871 exception Div raised*)
872 "~~~~~ and try_new_r, args:"; val (a, b, n, M, r, r_list, steps) = (a, b, n, M, r, r_list, steps);
873 val r = find_new_r a b r;
874 val r_list = r_list @ [r];
875 val g_r = gcd_poly' (order (eval a (n - 2) r))
876 (order (eval b (n - 2) r)) (n - 1) 0
877 val steps = steps @ [g_r];
878 (*HENSEL_lifting a b n M 1 r r_list steps g_r (zero_poly n) [1]
879 exception Div raised*)
880 "~~~~~ and HENSEL_lifting, args:"; val (a, b, n, M, m, r, r_list, steps, g, g_n, mult) =
881 (a, b, n, M, 1, r, r_list, steps, g_r, zero_poly n, [1]);
883 val r = find_new_r a b r;
884 val r_list = r_list @ [r];
885 val g_r = gcd_poly' (order (eval a (n - 2) r))
886 (order (eval b (n - 2) r)) (n - 1) 0;
887 lex_ord (lmonom g) (lmonom g_r) = false;
888 lexp g = lexp g_r = true;
889 val (g_n, new, steps) = NEWTON r_list [g, g_r] steps mult g_n (n - 2);
890 (nth steps (length steps - 1) = zero_poly (n - 1)) = false;
891 (*HENSEL_lifting a b n M (m + 1) r r_list steps g_r g_n new
892 exception Div raised*)
893 "~~~~~ and HENSEL_lifting, args:"; val (a, b, n, M, m, r, r_list, steps, g, g_n, mult) =
894 (a, b, n, M, m + 1, r, r_list, steps, g_r, g_n, new);
896 (g_n %%|%% a andalso g_n %%|%% b) = false;
897 (*try_new_r a b n M r r_list steps
898 exception Div raised*)
899 "~~~~~ and try_new_r, args:"; val (a, b, n, M, r, r_list, steps) = (a, b, n, M, r, r_list, steps);
900 val r = find_new_r a b r;
901 val r_list = r_list @ [r];
902 val g_r = gcd_poly' (order (eval a (n - 2) r))
903 (order (eval b (n - 2) r)) (n - 1) 0
904 val steps = steps @ [g_r];
905 (*HENSEL_lifting a b n M 1 r r_list steps g_r (zero_poly n) [1]
906 exception Div raised*)
907 "~~~~~ and HENSEL_lifting, args:"; val (a, b, n, M, m, r, r_list, steps, g, g_n, mult) =
908 (a, b, n, M, 1, r, r_list, steps, g_r, zero_poly n, [1]);
910 val r = find_new_r a b r;
911 val r_list = r_list @ [r];
912 val g_r = gcd_poly' (order (eval a (n - 2) r))
913 (order (eval b (n - 2) r)) (n - 1) 0;
914 lex_ord (lmonom g) (lmonom g_r) = false;
915 lexp g = lexp g_r = true;
916 val (g_n, new, steps) = NEWTON r_list [g, g_r] steps mult g_n (n - 2);
917 nth steps (length steps - 1) = zero_poly (n - 1) = true;
918 (*HENSEL_lifting a b n M (M + 1) r r_list steps g_r g_n new
919 exception Div raised*)
920 "~~~~~ and HENSEL_lifting, args:"; val (a, b, n, M, m, r, r_list, steps, g, g_n, mult) =
921 (a, b, n, M, m + 1, r, r_list, steps, g_r, g_n, new);
923 (*(g_n %%|%% a andalso g_n %%|%% b);
924 exception Div raised: !!!!! g_n = [(0, [0, 0])] !!!!!*)
926 "=========== prep Lucas-Interpretation ==================";
927 "----------- fun for_quot_regarding ---------------------";
928 "----------- fun for_quot_regarding ---------------------";
929 "----------- fun for_quot_regarding ---------------------";
930 (* -> quot' = [] @ [2] @ (3 * [])*)
931 "~~~~~ fun for_quot_regarding, args:"; val (p1, p2, p1', quot, remd) =
932 ([2, 2, 2, 2, 2], [1, 2, 3], [2, 2, 2, 2, 2], [], [6, 6, 4, 2]);
933 val zeros = deg_up p1' - deg_up remd - 1(*length [q]*) (* = 0*)
934 val max_qot_deg = deg_up p1 - deg_up p2 (* = 2*)
936 zeros + 1(*length [q]*) + deg_up quot > max_qot_deg = false
938 if for_quot_regarding p1 p2 p1' quot remd = 0 then ()
939 else error "for_quot_regarding 1 changed"
942 (* -> quot' = [0, 0, 0] @ [1] @ (1 * [])*)
943 "~~~~~ fun for_quot_regarding, args:"; val (p1, p2, p1', quot, remd) =
944 ([3, 2, 2, 2, 1, 1, 1, 1], [1, 1, 1, 1], [3, 2, 2, 2, 1, 1, 1, 1], [], [3, 2, 2, 2]);
945 val zeros = deg_up p1' - deg_up remd - 1(*length [q]*) (* = 3*)
946 val max_qot_deg = deg_up p1 - deg_up p2 (* = 4*)
948 zeros + 1(*length [q]*) + deg_up quot > max_qot_deg = false
950 if for_quot_regarding p1 p2 p1' quot remd = 3 then ()
951 else error "for_quot_regarding 2 changed"
954 (* -> quot' = [] @ [2] @ (1 * [0, 0, 0, 1])*)
955 "~~~~~ fun for_quot_regarding, args:"; val (p1, p2, p1', quot, remd) =
956 ([3, 2, 2, 2, 1, 1, 1, 1], [1, 1, 1, 1], [3, 2, 2, 2], [0, 0, 0, 1], [1]);
957 val zeros = deg_up p1' - deg_up remd - 1(*length [q]*) (* = 2*)
958 val max_qot_deg = deg_up p1 - deg_up p2 (* = 4*)
960 zeros + 1(*length [q]*) + deg_up quot > max_qot_deg = true
962 for_quot_regarding p1 p2 p1' quot remd;
963 if for_quot_regarding p1 p2 p1' quot remd = 0 then ()
964 else error "for_quot_regarding 3 changed";
967 "----------- fun mult_to_deg - --------------------------";
968 "----------- fun mult_to_deg - --------------------------";
969 "----------- fun mult_to_deg - --------------------------";
970 val p1 = [2,2,2, 2,2,2];
972 if mult_to_deg (deg_up p1) p2 = [0, 0, 0, 7, 8, 6] then () else error "fun mult_to_deg changed";
974 "----------- fun fact_quot ------------------------------";
975 "----------- fun fact_quot ------------------------------";
976 "----------- fun fact_quot ------------------------------";
977 fact_quot 18 8 = (4, 9);
978 fact_quot 2 6 = (3, 1);
979 fact_quot ~2 6 = (3, ~1);
980 fact_quot 5 6 = (6, 5);
981 if fact_quot 110 6 = (3, 55) then () else error "fun fact_quot changed 1";
982 (* this works, if (several) position(s) in the dividend are 0: *)
983 if fact_quot 0 3 = (1, 0) then () else error "fun fact_quot changed 2";
985 "----------- fun %+% ------------------------------------";
986 "----------- fun %+% ------------------------------------";
987 "----------- fun %+% ------------------------------------";
988 if (p1 %+% p2) = [9, 10, 8, 2, 2, 2] andalso (p2 %+% p1) = [9, 10, 8, 2, 2, 2]
989 then () else error "fun %+% changed";
991 "----------- fun %*% ------------------------------------";
992 "----------- fun %*% ------------------------------------";
993 "----------- fun %*% ------------------------------------";
994 if ([1,2,1] %*% [1,3,3,1]) = [1, 5, 10, 10, 5, 1] then () else error "fun %*% changed";
996 "----------- fun %*/% -----------------------------------";
997 "----------- fun %*/% -----------------------------------";
998 "----------- fun %*/% -----------------------------------";
999 val p1 = [2,2,2, 2,2,2];
1002 q (* = [29, ~33, ~18, 54]*),
1003 r (* = [317, 295]*)) = p1 %*/% p2;
1004 if (p1 %* n) = ((q %*% p2) %+% r) then () else error "fun %*/% changed 1";
1006 (* demo in GCD_Poly *)
1007 val p1 = [2, 2, 2, 2, 2];
1010 q (* = [8, 6, 18]*),
1011 r (* = [46, 32]*)) = p1 %*/% p2;
1012 if (p1 %* n) = ((q %*% p2) %+% r) then () else error "fun %*/% changed 2";
1014 "~~~~~ fun div_int_up, args:"; val (p1, p1', p2, quot, ns) = (p1, p1, p2, [], 1);
1015 val (n, q) = fact_quot (lcoeff_up p1') (lcoeff_up p2);
1016 val remd = drop_tl_zeros ((p1' %* n) %-% (mult_to_deg (deg_up p1') p2 %* q));
1017 val zeros = for_quot_regarding p1 p2 p1' quot remd;
1018 "~~~~~ fun writeln_trace, args:"; val (p1, p1', p2, quot, n, q ,(zeros:int), remd, (ns: int)) =
1019 (p1, p1', p2, quot, n, q, zeros, remd, ns);
1020 "~~~~~ fun div_invariant2, args:"; val (p1, p2, n, ns, zeros, q, quot, remd) =
1021 (p1, p2, n, ns, zeros, q, quot, remd);
1022 if (p1 %* (n * ns)) =
1023 ((mult_to_deg (deg_up p1 - deg_up p2) ((replicate zeros 0) @ [q] @ (quot %* n))) %*% p2 %+% remd)
1024 then () else error "div_int_up: invariant 2 does not hold"
1027 "----------- fun %*/% Subscript raised (line 509 of lib--";
1028 "----------- fun %*/% Subscript raised (line 509 of lib--";
1029 "----------- fun %*/% Subscript raised (line 509 of lib--";
1030 val p1 = [3,2,2,2,1,1,1,1];
1032 "~~~~~ fun div_int_up, args:"; val (p1, p1', p2, quot, ns) = (p1, p1, p2, [], 1);
1033 val (n, q) = fact_quot (lcoeff_up p1') (lcoeff_up p2);
1034 val remd = drop_tl_zeros ((p1' %* n) %-% (mult_to_deg (deg_up p1') p2 %* q));
1035 val zeros = for_quot_regarding p1 p2 p1' quot remd
1036 val _ = writeln_trace p1 p1' p2 quot n q zeros remd ns
1037 val quot = (replicate zeros 0) @ [q] @ (quot %* n)
1039 deg_up remd >= deg_up p2 = true;
1040 "~~~~~ fun div_int_up, args:"; val (p1, p1', p2, quot, ns) = (p1, remd, p2, quot, ns);
1041 val (n, q) = fact_quot (lcoeff_up p1') (lcoeff_up p2);
1042 val remd = drop_tl_zeros ((p1' %* n) %-% (mult_to_deg (deg_up p1') p2 %* q));
1043 val zeros = for_quot_regarding p1 p2 p1' quot remd;
1044 "~~~~~ fun writeln_trace, args:"; val (p1, p1', p2, quot, n, q, (zeros:int), remd, (ns: int))=
1045 (p1, p1', p2, quot, n, q, zeros, remd, ns);
1046 if (p1 %* (n * ns)) =
1047 ((mult_to_deg (deg_up p1 - deg_up p2)
1048 (((replicate zeros 0) @ [q] @ (quot %* n))) %*% p2 %+% remd))
1049 then () else error "writeln_trace changed"
1053 val quot = (replicate zeros 0) @ [q] @ (quot %* n)
1055 deg_up remd >= deg_up p2 = false;
1057 q (* = [2, 0, 0, 0, 1]*),
1058 r (* = [1]*)) = (ns, quot, remd)
1060 if (p1 %* n) = ((q %*% p2) %+% r) then () else error "fun %*/% changed x"
1062 "----------- fun EUCLID_naive_up ------------------------";
1063 "----------- fun EUCLID_naive_up ------------------------";
1064 "----------- fun EUCLID_naive_up ------------------------";
1065 val a = [0,~1,1]; (* -x + x^2 = x *(-1 + x) *)
1066 val b = [~1,0,1]; (* -1 + x^2 = (1+x)*(-1 + x) *)
1067 (*EUCLID_naive_up a b; (* = [1, ~1]*) (*( 1 - x) *)
1068 ERROR: invariant 2 does not hold: [~1, 0, 1] * ~1 = [~1, ~1] ** [1, ~1] ++ [0, 0, 0, 0]*)
1070 "~~~~~ fun EUCLID_naive_up, args:"; val (a, b) = (a, b);
1071 deg_up a < deg_up b = false;
1072 val (n, q, r) = a %*/% b
1073 (*EUCLID_naive_up b r
1074 ERROR: invariant 2 does not hold: [~1, 0, 1] * ~1 = [~1, ~1] ** [1, ~1] ++ [0, 0, 0, 0]*)
1076 "~~~~~ fun EUCLID_naive_up, args:"; val (a, b) = (b, r);
1077 (* val (n, q, r) = a %*/% b
1078 invariant 2 does not hold: [~1, 0, 1] * ~1 = [~1, ~1] ** [1, ~1] ++ [0, 0, 0, 0]*)
1080 "~~~~~ fun %*/%, args:"; val (p1, p2) = (a, b);
1081 (* val (n, q, r) = div_int_up p1 p1 p2 [] 1
1082 invariant 2 does not hold: [~1, 0, 1] * ~1 = [~1, ~1] ** [1, ~1] ++ [0, 0, 0, 0]*)
1084 "~~~~~ fun div_int_up, args:"; val (p1, p1', p2, quot, ns) = (p1, p1, p2, [], 1);
1085 val (n, q) = fact_quot (lcoeff_up p1') (lcoeff_up p2);
1086 val remd = drop_tl_zeros ((p1' %* n) %-% (mult_to_deg (deg_up p1') p2 %* q));
1087 val zeros = for_quot_regarding p1 p2 p1' quot remd
1088 val _ = writeln_trace p1 p1' p2 quot n q zeros remd ns
1089 val quot = (replicate zeros 0) @ [q] @ (quot %* n)
1091 deg_up remd >= deg_up p2 = true;
1092 (*div_int_up p1 remd p2 quot ns
1093 invariant 2 does not hold: [~1, 0, 1] * ~1 = [~1, ~1] ** [1, ~1] ++ [0, 0, 0, 0]*)
1095 "~~~~~ fun div_int_up, args:"; val (p1, p1', p2, quot, ns) = ( p1, remd, p2, quot, ns);
1096 val (n, q) = fact_quot (lcoeff_up p1') (lcoeff_up p2);
1097 val remd = drop_tl_zeros ((p1' %* n) %-% (mult_to_deg (deg_up p1') p2 %* q));
1098 val zeros = for_quot_regarding p1 p2 p1' quot remd
1099 (* val _ = writeln_trace p1 p1' p2 quot n q zeros remd ns
1100 invariant 2 does not hold: [~1, 0, 1] * ~1 = [~1, ~1] ** [1, ~1] ++ [0, 0, 0, 0]*)
1102 "~~~~~ fun writeln_trace, args:"; val (p1, p1', p2, quot, n, q ,(zeros:int), remd, (ns: int))=
1103 (p1, p1', p2, quot, n, q, zeros, remd, ns);
1104 (*if (p1 %* (n * ns)) =
1105 ((mult_to_deg (deg_up p1 - deg_up p2) ((replicate zeros 0) @ [q] @ (quot %* n))) %*% p2 %+% remd)
1106 then () else error "div_int_up: invariant 2 does not hold"
1107 ERROR: div_int_up: invariant 2 does not hold*)
1108 (p1 %* (n * ns)) = [1, 0, ~1]; (* ERROR came from fact_quot with n<0 *)
1109 ((mult_to_deg (deg_up p1 - deg_up p2) ((replicate zeros 0) @ [q] @ (quot %* n))) %*% p2 %+% remd) =
1112 if (p1 %* (abs n * ns)) =
1113 ((mult_to_deg (deg_up p1 - deg_up p2) ((replicate zeros 0) @ [q] @ (quot %* n))) %*% p2 %+% remd)
1114 then () else error "div_int_up: invariant 2 does not hold in ~~~~~ fun Euclid_naive";
1117 val a = [~1,0,0,1]; (* -1 + x^3 = (1+x+x^2)*(-1 + x) *)
1118 val b = [0,~1,1]; (* -x + x^2 = x *(-1 + x) *)
1119 if EUCLID_naive_up a b = [~1, 1] (*(-1 + x) *)
1120 then () else error "fun EUCLID_naive_up changed 1";
1122 val a = [0,~1,0,0,1]; (* -x + x^4 = x*(1+x+x^2)*(-1 + x) *)
1123 val b = [~2,2]; (* -x + x^2 = 2 *(-1 + x) *)
1124 if EUCLID_naive_up a b = [~1, 1] then () else error "fun EUCLID_naive_up changed 2";
1126 val a = [~5,2,8,~3,~3,0,1,0,1];
1127 val b = [21,~9,~4,5,0,3];
1128 if EUCLID_naive_up a b = [1] then () else error "fun EUCLID_naive_up changed 3";
1130 val a = [~18, ~15, ~20, 12, 20, ~13, 2];
1131 val b = [8, 28, 22, ~11, ~14, 1, 2];
1132 if EUCLID_naive_up a b = [~2, ~1, 1] then () else error "fun EUCLID_naive_up changed 4";
1134 "----------- last step in EUCLID ------------------------";
1135 "----------- last step in EUCLID ------------------------";
1136 "----------- last step in EUCLID ------------------------";
1138 trace_div_invariant := false;
1139 trace_Euclid := false;
1140 val a = [~18, ~15, ~20, 12, 20, ~13, 2];
1141 val b = [8, 28, 22, ~11, ~14, 1, 2];
1142 "~1~~~~ fun EUCLID_naive_up, args:"; val (a, b) = (a, b);
1143 val (n, q, r) = a %*/% b;
1144 "~2~~~~ fun EUCLID_naive_up, args:"; val (a, b) = (b, r);
1145 val (n, q, r) = a %*/% b;
1146 "~3~~~~ fun EUCLID_naive_up, args:"; val (a, b) = (b, r);
1147 val (n, q, r) = a %*/% b;
1148 "~4~~~~ fun EUCLID_naive_up, args:"; val (a, b) = (b, r);
1149 val (n, q, r) = a %*/% b;
1150 "~5~~~~ fun EUCLID_naive_up, args:"; val (a, b) = (b, r);
1151 (* val (n, q, r) = a %*/% b;*)
1152 "~~~~~ fun %*/%, args:"; val (p1, p2) = (a, b);
1153 (*div_int_up p1 p1 p2 [] 1*)
1154 "~~~~~ fun div_int_up, args:"; val (p1, p1', p2, quot, ns) = (p1, p1, p2, [], 1);
1156 val p1 = [~1316434, ~3708859, ~867104, 1525321]: int list
1157 val p1' = [~1316434, ~3708859, ~867104, 1525321]: int list
1158 val p2 = [~5000595353600, ~2500297676800, 2500297676800]: int list
1159 val quot = []: 'a list
1162 val (n, q) = fact_quot (lcoeff_up p1') (lcoeff_up p2)
1163 (*n = 7289497600, q = 4447*)
1164 val remd = drop_tl_zeros ((p1' %* n) %-% (mult_to_deg (deg_up p1') p2 %* q))
1165 (*remd = [~9596142483558400, ~4798071241779200, 4798071241779200]*)
1166 val zeros = for_quot_regarding p1 p2 p1' quot remd
1168 val _ = writeln_trace p1 p1' p2 quot n q zeros remd ns
1170 val quot = (replicate zeros 0) @ [q] @ (quot %* n)
1174 val (n, q, r) = a %*/% b;
1175 "~6~~~~ fun EUCLID_naive_up, args:"; val (a, []) = (b, r);
1177 " ========== END ======================================= ";
1178 fun nth _ [] = error "nth _ []" (*Isabelle2002, still saved the hours of update*)
1180 | nth n (_::xs) = nth (n-1) xs;
1181 (*fun nth xs i = List.nth (xs, i); recent Isabelle: TODO update all isac code *)