*To*: Johannes Hölzl <hoelzl at in.tum.de>*Subject*: Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Wed, 22 May 2013 08:16:03 -0500*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1369205906.2505.14.camel@macbroy12.informatik.tu-muenchen.de>*References*: <519AE86B.2030208@gmx.com> <3E3AEE15-2181-46D1-A676-85F7EC6FE1A4@cam.ac.uk> <519C3A46.3080901@gmx.com> <1369205906.2505.14.camel@macbroy12.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 5/22/2013 1:58 AM, Johannes Hölzl 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.In my experience it is quite the other way round. The first semesters mathematics course I attended introduced the integers, the rational numbers and the real numbers as equivalence classes. Only the natural numbers and the complex numbers where introduced like a datatype.

Johannes,

Regards, GB

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

**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

**Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy***From:*Johannes Hölzl

- Previous by Date: Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy
- Next by Date: Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy
- 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