[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.