Re: [isabelle] newbie: Binomial extensions
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
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.
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.
> 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
>> 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
>>> 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)
>>> (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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and