[isabelle-dev] Isabelle2016-RC0: potential changes

[Thiemann, Rene]

>> I’m puzzled. In ~~/src/HOL/Library/Poly_Deriv.thy I found no notion of algebraic number.
> Oh, yes, you're right. It's in https://bitbucket.org/isa-afp/afp-devel/src/363fdbc2f28c2503095a245f00db3d2805ed3ff9/thys/Liouville_Numbers/Liouville_Numbers_Misc.thy .

Ah, I see. Indeed: definitely equivalent.

> 
>> 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!)
> 
> I suggest this:
> 
> 
> function fold_atLeastAtMost_nat where
>  [simp del]: "fold_atLeastAtMost_nat f a (b::nat) acc =
>                 (if a > b then acc else fold_atLeastAtMost_nat f (a+1) b (f a acc))"
> by pat_completeness auto
> termination by (relation "measure (λ(_,a,b,_). Suc b - a)") auto
> ...

Looks good from my viewpoint.

Best,
René