[isabelle-dev] Factorials and binomial coefficients
ac638 at cam.ac.uk
Mon Feb 2 10:47:01 CET 2009
I left Fact.thy alone because it is necessary for building HOL. I moved
it upwards though (now it imports Nat instead of RealDef). I added the
other stuff to Binomial since it is "Library stuff" and not necessary
for building HOL.
This said, I have no objection (or strong opinion about) to merging
Florian Haftmann wrote:
> 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
> 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,
More information about the isabelle-dev