Re: [isabelle] newbie: Binomial extensions

You simply need to use gchoose. Example:

value "(-1/2::real) gchoose 2"

"3 / 8"
  :: âreal"

The first argument has to be a field of characteristic zero, such as the reels.


> On 22 Feb 2017, at 18:23, Raymond Rogers <raymond.rogers72 at> wrote:
> 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:
> 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.