[isabelle-dev] Factorials and binomial coefficients
nipkow at in.tum.de
Thu Jan 29 16:59:26 CET 2009
That theory should be cleaned up and separated into its core and the
real-related lemmas that are trivial consequences. The real-related
stuff should go where it is used, or better, be removed: eg
real (fact n) = 0
is pointless, at least as a simp rule. Such cleaning up is greatly
appreciated and necessary.
Amine Chaieb wrote:
> Dear all,
> 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!
> best wishes,
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
More information about the isabelle-dev