[isabelle-dev] Isabelle2016-RC0: potential changes
eberlm at in.tum.de
Mon Jan 11 10:04:46 CET 2016
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
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
> Moreover, everything of
> 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,
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev