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