[isabelle-dev] Factorials and binomial coefficients

[Amine Chaieb]

Hi,
I left Fact.thy alone because it is necessary for building HOL. I moved 
it upwards though (now it imports Nat instead of RealDef). I added the 
other stuff to Binomial since it is "Library stuff" and not necessary 
for building HOL.

This said, I have no objection (or strong opinion about) to merging 
these developments.

Best wishes,
Amine.

Florian Haftmann wrote:
> Hi Amine,
> 
>> For now HOL/Fact.thy defines factorials (over natural numbers) and
>> strangely imports the reals. The theorem involving the reals, however,
>> hold in any (ordered) (ring/field) of charachteristic Zero.
>>
>> Apart from that, I have a formalization of Pochhammer's symbol (raising
>> factorials) which generalize factorials (I have also relation theorems
>> to fact) and the generalized binomial coefficient.
>>
>> Since Fact.thy is needed for building HOL but Library/Binomial is not,
>> my question is whether we should unify these two developments or should
>> I add my formalization into Libray or ex? Any comments are welcome!
> 
> I would encourage to go the way through:  replace Binomial/Fact by your
> development.
> 
> In the examples you sent with your rewrite orientation problem there is
> still a separate Fact.thy (which a few dozens of lines).  I would
> strongly suggest to integrate this into your Binomal.thy
> 
> Thanks a lot,
> 	Florian
>