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