equal
deleted
inserted
replaced
88 5 div 2 = 2; ~5 div 2 = ~3; BUT WEE NEED ~5 div2 2 = ~2; *) |
88 5 div 2 = 2; ~5 div 2 = ~3; BUT WEE NEED ~5 div2 2 = ~2; *) |
89 infix div2 |
89 infix div2 |
90 fun a div2 b = |
90 fun a div2 b = |
91 if a div b < 0 then (abs a) div (abs b) * ~1 else a div b |
91 if a div b < 0 then (abs a) div (abs b) * ~1 else a div b |
92 |
92 |
93 (* why has this been removed since 2002 ? *) |
93 (* why has "last" been removed since 2002, although "last" is in List.thy ? *) |
94 fun last_elem ls = (hd o rev) ls |
94 fun last ls = (hd o rev) ls |
95 |
95 |
96 (* drop tail elements equal 0 *) |
96 (* drop tail elements equal 0 *) |
97 fun drop_hd_zeros (0 :: ps) = drop_hd_zeros ps |
97 fun drop_hd_zeros (0 :: ps) = drop_hd_zeros ps |
98 | drop_hd_zeros p = p |
98 | drop_hd_zeros p = p |
99 fun drop_tl_zeros p = (rev o drop_hd_zeros o rev) p; |
99 fun drop_tl_zeros p = (rev o drop_hd_zeros o rev) p; |
157 assumes last_p = maxs ps \<and> (\<forall>p. List.member ps p \<longrightarrow> Primes.prime p) \<and> |
157 assumes last_p = maxs ps \<and> (\<forall>p. List.member ps p \<longrightarrow> Primes.prime p) \<and> |
158 (\<forall>p. p < last_p \<and> Primes.prime p \<longrightarrow> List.member ps p) |
158 (\<forall>p. p < last_p \<and> Primes.prime p \<longrightarrow> List.member ps p) |
159 yields n \<le> maxs pps \<and> (\<forall>p. List.member pps p \<longrightarrow> Primes.prime p) \<and> |
159 yields n \<le> maxs pps \<and> (\<forall>p. List.member pps p \<longrightarrow> Primes.prime p) \<and> |
160 (\<forall>p. (p < maxs pps \<and> Primes.prime p) \<longrightarrow> List.member pps p)*) |
160 (\<forall>p. (p < maxs pps \<and> Primes.prime p) \<longrightarrow> List.member pps p)*) |
161 fun make_primes ps last_p n = |
161 fun make_primes ps last_p n = |
162 if n <= last_elem ps then ps else |
162 if n <= last ps then ps else |
163 if is_prime ps (last_p + 2) |
163 if is_prime ps (last_p + 2) |
164 then make_primes (ps @ [(last_p + 2)]) (last_p + 2) n |
164 then make_primes (ps @ [(last_p + 2)]) (last_p + 2) n |
165 else make_primes ps (last_p + 2) n |
165 else make_primes ps (last_p + 2) n |
166 |
166 |
167 (* primes_upto :: nat \<Rightarrow> nat list |
167 (* primes_upto :: nat \<Rightarrow> nat list |
189 *} |
189 *} |
190 |
190 |
191 subsection {* basic notions for univariate polynomials *} |
191 subsection {* basic notions for univariate polynomials *} |
192 ML {* |
192 ML {* |
193 (* leading coefficient, includes drop_lc0_up ?FIXME130507 *) |
193 (* leading coefficient, includes drop_lc0_up ?FIXME130507 *) |
194 fun lcoeff_up (p: unipoly) = (last_elem o drop_tl_zeros) p |
194 fun lcoeff_up (p: unipoly) = (last o drop_tl_zeros) p |
195 |
195 |
196 (* drop leading coefficients equal 0 *) |
196 (* drop leading coefficients equal 0 *) |
197 fun drop_lc0_up (p: unipoly) = drop_tl_zeros p : unipoly; |
197 fun drop_lc0_up (p: unipoly) = drop_tl_zeros p : unipoly; |
198 |
198 |
199 (* degree, includes drop_lc0_up ?FIXME130507 *) |
199 (* degree, includes drop_lc0_up ?FIXME130507 *) |
450 ML {* |
450 ML {* |
451 (* monomial order: lexicographic order on exponents *) |
451 (* monomial order: lexicographic order on exponents *) |
452 fun lex_ord ((_, a): monom) ((_, b): monom) = |
452 fun lex_ord ((_, a): monom) ((_, b): monom) = |
453 let val d = drop_tl_zeros (a %-% b) |
453 let val d = drop_tl_zeros (a %-% b) |
454 in |
454 in |
455 if d = [] then false else last_elem d > 0 |
455 if d = [] then false else last d > 0 |
456 end |
456 end |
457 fun lex_ord' ((_, a): monom, (_, b): monom) = |
457 fun lex_ord' ((_, a): monom, (_, b): monom) = |
458 let val d = drop_tl_zeros (a %-% b) |
458 let val d = drop_tl_zeros (a %-% b) |
459 in |
459 in |
460 if d = [] then EQUAL |
460 if d = [] then EQUAL |
461 else if last_elem d > 0 then GREATER else LESS |
461 else if last d > 0 then GREATER else LESS |
462 end |
462 end |
463 |
463 |
464 (* add monomials in ordered polynomal *) |
464 (* add monomials in ordered polynomal *) |
465 fun add_monoms (p: poly) = |
465 fun add_monoms (p: poly) = |
466 let |
466 let |
648 |
648 |
649 fun next_step ([]: poly list) (new_steps: poly list) (_: int list) = new_steps |
649 fun next_step ([]: poly list) (new_steps: poly list) (_: int list) = new_steps |
650 | next_step steps new_steps x = |
650 | next_step steps new_steps x = |
651 next_step (tl steps) |
651 next_step (tl steps) |
652 (new_steps @ |
652 (new_steps @ |
653 [((last_elem new_steps) %%-%% (hd steps)) %%/ ((last_elem x) - (nth x (length x - 3)))]) |
653 [((last new_steps) %%-%% (hd steps)) %%/ ((last x) - (nth x (length x - 3)))]) |
654 (nth_drop (length x -2) x) |
654 (nth_drop (length x -2) x) |
655 |
655 |
656 fun NEWTON x f (steps: poly list) (up: unipoly) (p: poly) ord = |
656 fun NEWTON x f (steps: poly list) (up: unipoly) (p: poly) ord = |
657 if length x = 2 |
657 if length x = 2 |
658 then |
658 then |
661 else |
661 else |
662 let |
662 let |
663 val new_vals = |
663 val new_vals = |
664 multi_to_uni ((uni_to_multi up) %%*%% (uni_to_multi [(nth x (length x -2) ) * ~1, 1])); |
664 multi_to_uni ((uni_to_multi up) %%*%% (uni_to_multi [(nth x (length x -2) ) * ~1, 1])); |
665 val new_steps = [((nth f (length f - 1)) %%-%% (nth f (length f - 2))) %%/ |
665 val new_steps = [((nth f (length f - 1)) %%-%% (nth f (length f - 2))) %%/ |
666 ((last_elem x) - (nth x (length x - 2)))]; |
666 ((last x) - (nth x (length x - 2)))]; |
667 val steps = next_step steps new_steps x; |
667 val steps = next_step steps new_steps x; |
668 val p' = p %%+%% (mult_with_new_var (last_elem steps) new_vals ord); |
668 val p' = p %%+%% (mult_with_new_var (last steps) new_vals ord); |
669 in (order p', new_vals, steps) end |
669 in (order p', new_vals, steps) end |
670 *} |
670 *} |
671 |
671 |
672 subsection {* gcd_poly algorithm, code for [1] p.95 *} |
672 subsection {* gcd_poly algorithm, code for [1] p.95 *} |
673 ML {* |
673 ML {* |