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
