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



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.