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.