[isabelle-dev] Isabelle2016-RC0: potential changes

[Thiemann, Rene]

Hi Manuel,

> I already moved a few small lemmas.

Thanks.

> 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?),

Yes, it should work. (At least, on Friday afternoon, it worked)

> I will prove equivalence of my definition in Poly_Deriv.thy to your definition in Algebraic_Numbers and adapt the AFP entry accordingly.

I’m puzzled. In ~~/src/HOL/Library/Poly_Deriv.thy I found no notion of algebraic number.

> 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“.)

Its definitely not optimal, and you’re right that one can improve it by using an inline-version of listprod [k+1..n], 
but even the version that is mentioned in Algebraic_Numbers/Improved_Code_Equations.html is by far better than the current setup, since that just uses the recursive direct definition of binomial. (I noticed this since I got timeouts in my experiments with algebraic numbers and one of the culprits was binomial!)

Cheers,
René