[isabelle-dev] Factorials and binomial coefficients

[Florian Haftmann]

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

-- 

Home:
http://wwwbroy.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

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