[isabelle] change proposal: eliminating overloading for factorials

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.

Comments welcome!

Larry Paulson

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