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



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.





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