[isabelle-dev] Factorials and binomial coefficients

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Mon Feb 2 09:47:40 CET 2009

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

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,



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 252 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20090202/c0cde9b8/attachment.sig>

More information about the isabelle-dev mailing list