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

Hi,

`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)?
I try to do some lifting, like on line 208:

`(208) lift_definition of_int :: "int => 'a" is "%x(i,j). of_nat i -
``of_nat j"
`
However, on line 1661, there's this:
(1661) declare Quotient_int [quot_del]

`In isar-ref.pdf, it tells me that's to disable lifting for int, and so I
``try to enable it blindly like,
`
setup_lifting Quotient_int,
but I get a warning, and lifting doesn't work for me.
QUESTION: Can I enable lifting for int?
Thanks,
GB

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