*To*: Raymond Rogers <raymond.rogers72 at gmail.com>*Subject*: Re: [isabelle] newbie: Binomial extensions*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Thu, 23 Feb 2017 16:29:52 +0000*Cc*: Chaitanya Mangla <cm772 at cam.ac.uk>, cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <b3b3def4-540f-4a79-73c9-54ff1e72099e@gmail.com>*References*: <b3b3def4-540f-4a79-73c9-54ff1e72099e@gmail.com>

There are quite a few ways of constructing new types in Isabelle, including inductive or coinductive constructions and quotients. But you shouldnât need to do that to prove these binomial identities. Several of the earlier ones on your list have been proved already in Isabelle. Larry Paulson > 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 > > > > > > >

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

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

- Previous by Date: Re: [isabelle] newbie: Binomial extensions
- Next by Date: Re: [isabelle] Formalization of soundness and completeness of natural deduction
- 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