[isabelle-dev] Factorials and binomial coefficients
florian.haftmann at informatik.tu-muenchen.de
Mon Feb 2 09:47:40 CET 2009
> 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,
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 252 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev