>> 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é _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
