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


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?


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