*To*: Raymond Rogers <raymond.rogers72 at gmail.com>, Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] newbie: Binomial extensions*From*: Chaitanya Mangla <cm772 at cam.ac.uk>*Date*: Tue, 28 Feb 2017 01:26:41 +0000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <0246bfd0-1735-621e-6c2e-afd04ff3feca@gmail.com>*References*: <b3b3def4-540f-4a79-73c9-54ff1e72099e@gmail.com> <5F7B7137-7875-4155-91F3-77AD7C1D5DA0@cam.ac.uk> <0246bfd0-1735-621e-6c2e-afd04ff3feca@gmail.com>

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 > > " > >

**References**:**[isabelle] newbie: Binomial extensions***From:*Raymond Rogers

**Re: [isabelle] newbie: Binomial extensions***From:*Lawrence Paulson

**Re: [isabelle] newbie: Binomial extensions***From:*Raymond Rogers

- Previous by Date: Re: [isabelle] Formalization of soundness and completeness of natural deduction
- Next by Date: Re: [isabelle] newbie: Binomial extensions
- Previous by Thread: Re: [isabelle] newbie: Binomial extensions
- Next by Thread: Re: [isabelle] newbie: Binomial extensions
- Cl-isabelle-users February 2017 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list