# [isabelle] newbie: Binomial extensions

I am a complete newbie to Isabelle.

`I am trying to implement a library that is capable, more or less, of
``validating some of Gould's identities. In particular the ones listed in:
`http://www.dsi.dsi.unifi.it/~resp/GouldBK.pdf
I have managed "verify" the first equation "BS"
lemma Isa_BS:
assumes kn: "m â n"
shows "(n choose m) = (n choose (n-m))"
using assms
apply (rule Binomial.binomial_symmetric)
done
(suggestions appreciated!!)
I wish to extend/expand/define the choose function to
(n choose m) to n negative.
This is the second item in GouldBK.pdf
and in
Riordan's "Introduction to Combinatorial Analysis" page 5
and elsewhere

`My question is strategic. Should I just introduce a new "type" and
``filter the input into Binomial.thy or go through the whole definition
``phase copying (or something) Binomial.thy. Possibly there is a way to
``use "gbinomial" but I am not there yet. Or use the normal field
``extension process somehow? Using (a,b) over a; and defining
``multiplication and addition.
``Is there a tutorial with examples using Binomial.thy (and the fps
``theory)? There seems to be some peculiarities using "=" instead of
``"-->" but that is probably just ignorance.
`
Ray

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*