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

```Larry,

```
Alright, your paper will be the explanatory comments to Int.thy that everyone forgot to put in. Your slides will also be useful:
```
```
http://www.cl.cam.ac.uk/~lp15/papers/Reports/equivclasses-slides.pdf <http://www.cl.cam.ac.uk/%7Elp15/papers/Reports/equivclasses-slides.pdf>
```
```
I just need to match up a little of your notation in the paper with the newer Isar that's in Int.thy, and a lot of the naming is the same.
```
```
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.
```
```
I only need one representation of an integer, like (3,0) for 3, which I can use to tie into an equivalence class of my own, if that's the way I should do things, and it will work out.
```
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)?
```
```
```
```

```

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