Re: [isabelle] newbie: Binomial extensions

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 Isabelle.

Larry Paulson

On 22 Feb 2017, at 18:23, Raymond Rogers <raymond.rogers72 at <mailto:raymond.rogers72 at>> 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: <>
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.


From the QED manifesto:
Mathematics is arguably the foremost creation of the human mind.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.