Re: [isabelle] newbie: Binomial extensions





On 02/23/2017 06:41 AM, Lawrence Paulson wrote:
You simply need to use gchoose. Example:

value "(-1/2::real) gchoose 2"

"3 / 8"
   :: âreal"

The first argument has to be a field of characteristic zero, such as the reels.

Larry

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







Thanks! Is there readable reference material for these lemma's? Normally in mathematics one is expected to provide references/bibliography. In my experience self-documenting code ends up being a little painful.
Ray

"




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