*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*: Tue, 21 May 2013 12:00:38 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <519AE86B.2030208@gmx.com>*References*: <519AE86B.2030208@gmx.com>

The simple answer is no. What your request is impossible. The integers are constructed as a quotient and therefore the representation of an integer is an equivalence class, in this case a set of pairs of natural numbers. The construction does not give you a map from integers to some distinguished element of this set. Of course, nothing stops you from writing your own function from integers to pairs of natural numbers. Some time ago I wrote a paper on such matters, which you may find useful: http://www.cl.cam.ac.uk/~lp15/papers/Reports/equivclasses.pdf Larry Paulson On 21 May 2013, at 04:22, Gottfried Barrow <gottfried.barrow at gmx.com> wrote: > I want to recover the ordered pair part of an int. I actually have a simple solution like this: > > definition myI :: "int => nat * nat" where > "myI x = (nat x, nat (-x))" > > In the process of getting to the above definition, I was trying to get the ordered pair using lower level methods. Even though I have a solution, I ask about these other methods in case there's something useful there for me to use. > > In Int.thy, on line 20, int is defined as a quotient_type: > > (020) quotient_type int = "nat * nat" / "intrel" > (021) morphisms Rep_Integ Abs_Integ > > The type of Rep_Integ is (int => (nat * nat)), so I try to use it with something like "Rep_Integ 3", but I can't ever get it to return an ordered pair like (3,0). > > QUESTION: Is there a way for me to get "Rep_Integ 3" to return (3,0)?

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

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

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