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


What you probably meant (but I don't know I am just guessing your intentions), is this definition:

lift_definition foo45 :: "int => nat * nat" is "%(x,y). (x, y)"


This is type correct but you can't prove the respectfulness theorem since this theorem implies that each equivalence class in a definition of integers contains exactly one element. That's not true.

You need some kind of a normalization function that picks up one element for each class. For example:

lift_definition foo45 :: "int => nat * nat" is "%(x,y). (x - y, 0)" by auto

And so telling me that I need to prove "respectfulness" represents this big need of people like me to have some understanding of what's going on under the hood of the engine. Things like "fun" and lifting are great because they take care of a lot of overhead, until I stray outside of some example/template I have.

This gives you for each positive integer x a pair (x, 0) and for each negative integer (0, 0).

This is one more time in which lifting appears to not be the best solution. I think it'll be hard to beat the simple definition that I came up with. But the value in these attempts to use lifting is in getting closer to knowing what lifting is.

For deep understanding I recommend read the paper that Brian and I wrote about Lifting/Transfer and it is also good to know how typedef works. You can also read a paper by Kaliszyk, Urban (

And so I have 3 papers to pull from now, yours, Peter's and this one you just listed. All along it's been, "Something's being lifted from somewhere, to some thing, but what's being lifted is not clear to me, and neither are the restrictions on what the some thing can be."

It looks like Urban and Kaliszyk's paper provides a good conceptual overview. From section 5:/

   /The main benefit of a quotient package is to lift automatically
   theorems over raw types to theorems over quotient types. We will
   perform this lifting in three phases, called regularization,
   injection and cleaning according to procedures in Homeier’s ML-code./

So I was asking myself, "What's this Homeier's ML-code?"

And then I replied, "Oh, that would be Peter Homeier, who sent me a link to his paper on quotients earlier in the day, in response to my global request for docs on quotients and lifting."

With quotients and lifting, it appears that if you learn the one, you learn the other.


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