[isabelle-dev] Factorials and binomial coefficients

[Tobias Nipkow]

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.

Thanks
Tobias

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,
> Amine.
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev