*To*: Lawrence Paulson <lp15 at cam.ac.uk>*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*: Tue, 21 May 2013 22:23:50 -0500*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <3E3AEE15-2181-46D1-A676-85F7EC6FE1A4@cam.ac.uk>*References*: <519AE86B.2030208@gmx.com> <3E3AEE15-2181-46D1-A676-85F7EC6FE1A4@cam.ac.uk>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

Larry,

https://en.wikipedia.org/wiki/Integer#Construction

Thanks for the help, GB On 5/21/2013 6:00 AM, Lawrence Paulson wrote:

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:*Johannes Hölzl

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

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

- Previous by Date: [isabelle] LFMTP'13: Logical Frameworks and Meta-Languages (CFP)
- 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