I already moved a few small lemmas. I also defined the notion of an
algebraic number; as soon as your AFP entry works with the development
version of Isabelle again (is that already the case?), I will prove
equivalence of my definition in Poly_Deriv.thy to your definition in
Algebraic_Numbers and adapt the AFP entry accordingly.
(I needed this for Liouville_Numbers)
As for the binomial numbers: that looks a bit suboptimal to me. I would
have expected something like "listprod [k+1..n] div fact (n - k)" plus
an additional check if "2*k >= n", reducing "n choose k" to "n choose (n
- k)" if appropriate.
(Not sure what code generation makes of "listprod [k+1..n]", a
code_unfold rule to compute this efficiently with an accumulator and
without constructing the list explicitly might be required. Same for
"fact".)
Cheers,
Manuel
On 11/01/16 09:57, Thiemann, Rene wrote:
Dear all,
there are some changes I would like to add for the upcoming release. It would
be nice, if someone can integrate them:
- improved code equations for binomial coefficients and certain
divmod-algorithms.
(cf.
http://afp.sourceforge.net/browser_info/devel/AFP/Algebraic_Numbers/Improved_Code_Equations.html)
- change type in definition and lemmas about pderiv from real to arbitrary
fields, or even more general, cf. lines starting with
(* TODO: inform Isabelle developers *) in
http://afp.sourceforge.net/browser_info/devel/AFP/Algebraic_Numbers/Square_Free_Factorization.html
- change type of divides_degree from complex to 'a :: idom, cf beginning of
http://afp.sourceforge.net/browser_info/devel/AFP/Jordan_Normal_Form/Missing_Polynomial.html
Moreover, everything of
http://afp.sourceforge.net/browser_info/devel/AFP/Jordan_Normal_Form/Missing_*
http://afp.sourceforge.net/browser_info/devel/AFP/Algebraic_Numbers/Missing_*
can freely be moved from the AFP into the distribution, where I ask the
developers to judge which parts
belong in the distribution and which are too specific, etc.
With best regards,
René
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
