*To*: Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] newbie: Binomial extensions*From*: Raymond Rogers <raymond.rogers72 at gmail.com>*Date*: Sat, 25 Feb 2017 09:33:42 -0500*Cc*: Chaitanya Mangla <cm772 at cam.ac.uk>, cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <760CE815-C19B-4586-8CE1-83BF4E6AF15F@cam.ac.uk>*References*: <b3b3def4-540f-4a79-73c9-54ff1e72099e@gmail.com> <760CE815-C19B-4586-8CE1-83BF4E6AF15F@cam.ac.uk>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.7.0

I have a variation that would be interesting to tie down. Ray On 02/23/2017 11:29 AM, Lawrence Paulson wrote:

There are quite a few ways of constructing new types in Isabelle,including inductive or coinductive constructions and quotients. Butyou shouldnât need to do that to prove these binomial identities.Several of the earlier ones on your list have been proved already inIsabelle.Larry PaulsonOn 22 Feb 2017, at 18:23, Raymond Rogers <raymond.rogers72 at gmail.com<mailto: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, ofvalidating some of Gould's identities. In particular the ones listed in:http://www.dsi.dsi.unifi.it/~resp/GouldBK.pdf<http://www.dsi.dsi.unifi.it/%7Eresp/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 elsewhereMy question is strategic. Should I just introduce a new "type" andfilter the input into Binomial.thy or go through the whole definitionphase copying (or something) Binomial.thy. Possibly there is a wayto use "gbinomial" but I am not there yet. Or use the normal fieldextension process somehow? Using (a,b) over a; and definingmultiplication and addition.Is there a tutorial with examples using Binomial.thy (and the fpstheory)? There seems to be some peculiarities using "=" instead of"-->" but that is probably just ignorance.Ray

-- From the QED manifesto: https://www.cs.ru.nl/~freek/qed/qed.html " Mathematics is arguably the foremost creation of the human mind. "

**Follow-Ups**:**Re: [isabelle] newbie: Binomial extensions***From:*Manuel Eberl

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

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

- Previous by Date: [isabelle] Cancellation simprocs
- Next by Date: [isabelle] Call for participation: Workshop on Computer-aided Mathematical Proof, Cambridge UK, 10-14 July 2017
- 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