[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 -
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,
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