I also second this proposal, the definition of fact_int is quite
strange.

What about defining fact semi-polymorphic? Like
fact :: nat => 'a::semiring_1

then we do not need to depend on coercions, only on typeclasses. And in
semiring_1 the defining fact-equations should hold.

- Johannes

Am Freitag, den 27.02.2015, 12:35 +0100 schrieb Manuel Eberl:
> I ran into this very problem a few days ago and it took me several
> minutes to figure out what was going on.
>
> I therefore second this proposal, particularly since there is no such
> thing as the factorial of a negative integer in the first place.
>
> Cheers,
> Manuel
>
> On 27/02/15 12:27, Larry Paulson wrote:
> > I would like to discuss the question of overloading on fact, the factorial function.
> >
> > Currently, this function (introduced in src/HOL/Fact.thy) is overloaded, with separate but equivalent definitions on the natural numbers and the integers. The domain of the factorial function is extended to negative integers like this:
> >
> >   "fact_int x = (if x >= 0 then int (fact (nat x)) else 0)"
> >
> > The point of the overloading is to allow fact to be used in both int and nat contexts. However, Isabelle now provides automatic coercions between types. This removes the original motivation while introducing a significant drawback: an occurrence of the function fact in an arithmetical context now becomes ambiguous, and it is possible to get equivalent-looking formulas that have different instances of the function fact, with implicit coercions making the types work out. But such formulas are not equal.
> >
> > I would like to propose removing the overloading on the factorial function and having the natural number version only. The natural numbers are the actual domain of this function, and implicit coercions allow its use or integers or reals are expected.
> >
> >
> > Larry Paulson
> >
> >
> >
>
>

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.