Re: [isabelle] newbie: Binomial extensions



Hi Raymond,

If you're looking for reference material for lemmas in Binomial.thy, then
you can look at Concrete Mathematics by Graham, Knuth, and Patashnik. Some
of the lemmas in the theory were taken from the chapter on Binomial
coefficients (implemented using gchoose). Comments in some lemmas even
reference pages from the book.

Regards,
Chaitanya

On Thu, 23 Feb 2017 at 13:55 Raymond Rogers <raymond.rogers72 at gmail.com>
wrote:

>
>
> On 02/23/2017 06:41 AM, Lawrence Paulson wrote:
> > 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.
> >
> > Larry
> >
> >> On 22 Feb 2017, at 18:23, Raymond Rogers <raymond.rogers72 at gmail.com>
> 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:
> >> 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
> >>
> >>
> >>
> >>
> >>
> >>
> >>
> Thanks!   Is there readable reference material for these lemma's?
> Normally in mathematics one is expected to provide
> references/bibliography.   In my experience self-documenting code ends
> up being a little painful.
> Ray
>
> "
>
>



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