49 value "sdiv [:2,4,6::int:] 2" --"Poly [1, 2, 3]" |
49 value "sdiv [:2,4,6::int:] 2" --"Poly [1, 2, 3]" |
50 (*\------------------------------------------------------------------------------/*) |
50 (*\------------------------------------------------------------------------------/*) |
51 |
51 |
52 (* find the primitive part of a polynomial, see [1].p.83 |
52 (* find the primitive part of a polynomial, see [1].p.83 |
53 primitive p = p' |
53 primitive p = p' |
54 assumes p = [:c\<^isub>1, .., c\<^isub>n :] |
54 assumes p = [:c\<^isub>1, .., c\<^isub>n:] |
55 yields p' = [:c\<^isub>1', .., c\<^isub>n':] \<and> gcds c\<^isub>1', .., c\<^isub>n' = 1 *) |
55 yields p' = [:c\<^isub>1, .., c\<^isub>n:] = [:c\<^isub>1', .., c\<^isub>n':] * d |
|
56 \<and> d = gcds c\<^isub>1, .., c\<^isub>n *) |
56 definition primitive :: "int poly \<Rightarrow> int poly" where |
57 definition primitive :: "int poly \<Rightarrow> int poly" where |
57 "primitive p = sdiv p (gcds (coeffs p))" |
58 "primitive p = sdiv p (gcds (coeffs p))" |
58 |
59 |
59 value "primitive [:1::int, 2, 3:]" --"Poly [1, 2, 3]" |
60 value "primitive [:1::int, 2, 3:]" --"Poly [1, 2, 3]" |
60 value "primitive [:2::int, 4, 6:]" --"Poly [1, 2, 3]" |
61 value "primitive [:2::int, 4, 6:]" --"Poly [1, 2, 3]" |
61 value "primitive [:2000::int, 4000, 6000:]" --"Poly [1, 2, 3]" |
62 value "primitive [:2000::int, 4000, 6000:]" --"Poly [1, 2, 3]" |
|
63 |
|
64 (* arguments from the example from [1].p.94 *) |
|
65 value " primitive [:-5000595353600, -2500297676800, 2500297676800::int:]" |
|
66 --"= Poly [-2, -1, 1] OK" |
|
67 value [simp] "primitive [:-5000595353600, -2500297676800, 2500297676800::int:]" |
|
68 --"= [:-2, -1, 1, 0:] incorrect ???????????????????????????????????????????????????????????" |
|
69 (* goes forever: |
|
70 value [nbe] "primitive [:-5000595353600, -2500297676800, 2500297676800::int:]" |
|
71 *) |
|
72 value [code] "primitive [:-5000595353600, -2500297676800, 2500297676800::int:]" |
|
73 --"= Poly [-2, -1, 1] ...ok" |
|
74 |
|
75 value "gcds [(-5000595353600::int), -2500297676800, 2500297676800]" --"= 2500297676800 OK" |
|
76 value [simp] "gcds [(-5000595353600::int), -2500297676800, 2500297676800]" --"= 2500297676800 OK" |
|
77 value [nbe] "gcds [(-5000595353600::int), -2500297676800, 2500297676800]" --"= 2500297676800 OK" |
|
78 value [code] "gcds [(-5000595353600::int), -2500297676800, 2500297676800]" --"= 2500297676800 OK" |
62 |
79 |
63 (* regard zeros occurring in the quotient, also in the last step of division *) |
80 (* regard zeros occurring in the quotient, also in the last step of division *) |
64 fun for_quot_regarding :: "int poly \<Rightarrow> int poly \<Rightarrow> int poly \<Rightarrow> int poly \<Rightarrow> int poly \<Rightarrow> nat" where |
81 fun for_quot_regarding :: "int poly \<Rightarrow> int poly \<Rightarrow> int poly \<Rightarrow> int poly \<Rightarrow> int poly \<Rightarrow> nat" where |
65 "for_quot_regarding p1 p2 p1' quot remd = |
82 "for_quot_regarding p1 p2 p1' quot remd = |
66 (let |
83 (let |