1.1 --- a/src/Tools/isac/Knowledge/GCD_Poly.thy	Wed Aug 14 16:30:47 2013 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly.thy	Wed Aug 14 17:14:11 2013 +0200
     1.3 @@ -51,8 +51,9 @@
     1.4  
     1.5  (* find the primitive part of a polynomial, see [1].p.83
     1.6     primitive p = p'
     1.7 -    assumes p = [:c\<^isub>1, .., c\<^isub>n :]
     1.8 -    yields p' = [:c\<^isub>1', .., c\<^isub>n':]  \<and>  gcds c\<^isub>1', .., c\<^isub>n' = 1 *)
     1.9 +    assumes p = [:c\<^isub>1, .., c\<^isub>n:]
    1.10 +    yields p' = [:c\<^isub>1, .., c\<^isub>n:] = [:c\<^isub>1', .., c\<^isub>n':] * d
    1.11 +      \<and>  d = gcds c\<^isub>1, .., c\<^isub>n *)
    1.12  definition primitive :: "int poly \<Rightarrow> int poly" where
    1.13  "primitive p = sdiv p (gcds (coeffs p))"
    1.14  
    1.15 @@ -60,6 +61,22 @@
    1.16  value "primitive [:2::int, 4, 6:]"             --"Poly [1, 2, 3]"
    1.17  value "primitive [:2000::int, 4000, 6000:]"    --"Poly [1, 2, 3]"
    1.18  
    1.19 +(* arguments from the example from [1].p.94 *)
    1.20 +value "       primitive [:-5000595353600, -2500297676800, 2500297676800::int:]" 
    1.21 +  --"= Poly [-2, -1, 1]  OK"
    1.22 +value [simp] "primitive [:-5000595353600, -2500297676800, 2500297676800::int:]" 
    1.23 +  --"= [:-2, -1, 1, 0:]  incorrect ???????????????????????????????????????????????????????????"
    1.24 +(* goes forever:
    1.25 +value [nbe]  "primitive [:-5000595353600, -2500297676800, 2500297676800::int:]" 
    1.26 +*)
    1.27 +value [code] "primitive [:-5000595353600, -2500297676800, 2500297676800::int:]" 
    1.28 +  --"= Poly [-2, -1, 1] ...ok"
    1.29 +
    1.30 +value        "gcds [(-5000595353600::int), -2500297676800, 2500297676800]" --"= 2500297676800  OK"
    1.31 +value [simp] "gcds [(-5000595353600::int), -2500297676800, 2500297676800]" --"= 2500297676800  OK"
    1.32 +value [nbe]  "gcds [(-5000595353600::int), -2500297676800, 2500297676800]" --"= 2500297676800  OK"
    1.33 +value [code] "gcds [(-5000595353600::int), -2500297676800, 2500297676800]" --"= 2500297676800  OK"
    1.34 +
    1.35  (* regard zeros occurring in the quotient, also in the last step of division *)
    1.36  fun for_quot_regarding :: "int poly \<Rightarrow> int poly \<Rightarrow> int poly \<Rightarrow> int poly \<Rightarrow> int poly \<Rightarrow> nat" where
    1.37  "for_quot_regarding p1 p2 p1' quot remd =