*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] newbie: Binomial extensions*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Tue, 28 Feb 2017 12:01:31 +0100*In-reply-to*: <e210d1a9-15c8-f397-3d25-67e9b4bb2618@gmail.com>*References*: <b3b3def4-540f-4a79-73c9-54ff1e72099e@gmail.com> <760CE815-C19B-4586-8CE1-83BF4E6AF15F@cam.ac.uk> <e210d1a9-15c8-f397-3d25-67e9b4bb2618@gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.7.0

I'm pretty sure we don't have anything on Umbral Calculus. We might have a few stray identities that fall in that category by accident, but I'm reasonably sure nobody I know of ever attempted to formalise Umbral Calculus systematically. Note that we have the falling factorial ("pochhammer") and Bernoulli numbers and Bernoulli polynomials ("bernoulli" and "bernpoly" in the AFP entry "Bernoulli"), I think are relevant for umbral calculus. Cheers, Manuel On 25/02/17 15:33, Raymond Rogers wrote: > Thanks! I have worked my way through the beginning facts. Mostly on > auto-pilot but I have to start somewhere; I'm kinda slow. Starting on > Formal_Power_Series (fps) theory. That looks a little harder but is > great; since it has examples in the .thy file. Actually the fps is quite > impressive and probably has all of the obvious Gould requirements. > As another exercise: do you know if anybody has encoded Roman's "Umbral > Calculus" reasoning? If not, I might do it. He does an excellent job > explaining and > 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. 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 >>> <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, of >>> validating 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 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 >>> >>> >>> >>> >>> >>> >>> >> >

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