[isabelle-dev] Isabelle2016-RC0: potential changes

[Manuel Eberl]

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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>