Re: [isabelle] newbie: Binomial extensions

On 02/23/2017 06:36 AM, Manuel Eberl wrote:
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?



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).
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 consistency. 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 MHonArc.