equal
deleted
inserted
replaced
479 |
479 |
480 recdef numgcdh "measure size" |
480 recdef numgcdh "measure size" |
481 "numgcdh (C i) = (\<lambda>g. zgcd i g)" |
481 "numgcdh (C i) = (\<lambda>g. zgcd i g)" |
482 "numgcdh (CN n c t) = (\<lambda>g. zgcd c (numgcdh t g))" |
482 "numgcdh (CN n c t) = (\<lambda>g. zgcd c (numgcdh t g))" |
483 "numgcdh t = (\<lambda>g. 1)" |
483 "numgcdh t = (\<lambda>g. 1)" |
484 defs numgcd_def [code func]: "numgcd t \<equiv> numgcdh t (maxcoeff t)" |
484 defs numgcd_def [code]: "numgcd t \<equiv> numgcdh t (maxcoeff t)" |
485 |
485 |
486 recdef reducecoeffh "measure size" |
486 recdef reducecoeffh "measure size" |
487 "reducecoeffh (C i) = (\<lambda> g. C (i div g))" |
487 "reducecoeffh (C i) = (\<lambda> g. C (i div g))" |
488 "reducecoeffh (CN n c t) = (\<lambda> g. CN n (c div g) (reducecoeffh t g))" |
488 "reducecoeffh (CN n c t) = (\<lambda> g. CN n (c div g) (reducecoeffh t g))" |
489 "reducecoeffh t = (\<lambda>g. t)" |
489 "reducecoeffh t = (\<lambda>g. t)" |