Re: [isabelle] newbie: Binomial extensions
On 02/23/2017 06:36 AM, Manuel Eberl wrote:
Thanks: I want to twist some of the results in Gouldbk.pdf and want to
see how robust the basic results are and check if my conclusions are
correct usages. Some of the techniques in the paper are long and not
too obvious (to me).
gbinomial (syntax: "n gchoose k") is already that generalisation. It
works for pretty much anything as the first argument, but the second
argument must be a natural numbers. Seeing as we have the Gamma and Beta
functions in HOL-Analysis, one could also easily extend it to complex
I'm not sure what field extensions have to do with any of this. What
field are you talking about? What do you want to extend it to? What does
that have to do with binomial coefficients?
Perhaps my use of "field extension" was inappropriate.
My intuition is that if you are lacking something that is reasonable you
can extend a base set a by (a,b) and form a new set. For instance:
adding negative numbers to the naturals,
creating fractions from integers
solutions to x^2-2=0
and of course "imaginary numbers"
Of course you have to prove consistency and such.
The procedures seem fairly standard at an intuitive level.
Is there a standard template/example/constructor in Isabelle for this
sort of thing? So a construct can be introduced and checked for
For binomials: I could imagine (a choose b, -c choose d) with a,b,c,d
natural numbers and then defining equivalence relations between the
first and second slots. Putting this sort of thing into Isabelle seems
reasonable but I don't know how (yet) and hopefully I don't have to
since gchoose exists.
This archive was generated by a fusion of
Pipermail (Mailman edition) and