*To*: Gottfried Barrow <gottfried.barrow at gmx.com>*Subject*: Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Wed, 22 May 2013 12:22:09 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <519C3A46.3080901@gmx.com>*References*: <519AE86B.2030208@gmx.com> <3E3AEE15-2181-46D1-A676-85F7EC6FE1A4@cam.ac.uk> <519C3A46.3080901@gmx.com>

My slides briefly hint at the reason why the integers and rationals are almost invariably defined using equivalence classes and not using particular representations such as signed natural numbers or reduced fractions. It is simply that equivalence classes make everything much easier. Imagine defining addition on signed natural numbers. You will need at least three cases: (1) the signs agree (2) left operand is greater (3) right operand is greater. To prove the associative law, you will have four occurrences of the addition operator and therefore 81 separate cases. With equivalence classes, there is only one case and it is shown in full on one of the slides. For fractions in reduced form, the situation is even worse, because you're constantly reasoning about greatest common divisors. With equivalent classes, there is no need for that. Larry Paulson On 22 May 2013, at 04:23, Gottfried Barrow <gottfried.barrow at gmx.com> wrote: > It'd be interesting to know if it's common these days for other languages to use the classic definition of the integers as equivalence classes like you did with Int.thy: > > https://en.wikipedia.org/wiki/Integer#Construction > > It seems it's common for the natural numbers to be built using the successor function, but I'm guessing it's not so common for the integers to be equivalence classes.

**References**:**[isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy***From:*Gottfried Barrow

**Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy***From:*Lawrence Paulson

**Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy***From:*Gottfried Barrow

- Previous by Date: Re: [isabelle] Problems with code generation for the reals
- Next by Date: Re: [isabelle] Partial functions
- Previous by Thread: Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy
- Next by Thread: Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy
- Cl-isabelle-users May 2013 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