*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] change proposal: eliminating overloading for factorials*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Fri, 27 Feb 2015 15:07:44 +0100*In-reply-to*: <54F05674.5060601@in.tum.de>*Organization*: TU München*References*: <63B40738-A33F-493D-AFD0-AEB07E7DF7D4@cam.ac.uk> <54F05674.5060601@in.tum.de>

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. > > > > Comments welcome! > > > > Larry Paulson > > > > > > > >

**Follow-Ups**:**Re: [isabelle] change proposal: eliminating overloading for factorials***From:*Larry Paulson

**Re: [isabelle] change proposal: eliminating overloading for factorials***From:*Florian Haftmann

**References**:**[isabelle] change proposal: eliminating overloading for factorials***From:*Larry Paulson

**Re: [isabelle] change proposal: eliminating overloading for factorials***From:*Manuel Eberl

- Previous by Date: Re: [isabelle] change proposal: eliminating overloading for factorials
- Next by Date: Re: [isabelle] flatten of tuples
- Previous by Thread: Re: [isabelle] change proposal: eliminating overloading for factorials
- Next by Thread: Re: [isabelle] change proposal: eliminating overloading for factorials
- Cl-isabelle-users February 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list