Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy
On 05/22/2013 07:13 AM, Gottfried Barrow wrote:
One thing led to another, and I did a bunch of searches, and it turns
out you would be one of the two to ask for a tutorial on lifting, but
I'm sure you don't have time.
I found this:
And it turns out you have connections to Josef Urban.
I got rid of my setup_lifting warning by importing Quotient_Product.thy,
from a tip of yours here:
Now, I do setup_lifting, and the line of code you gave me works, so I'm
at an error for a simple thing I want to do, which will show you that I
have a fundamental misunderstanding of how to use lifting:
lift_definition of_int :: "int => 'a::ring_1" is "%(i, j). of_nat i
- of_nat j"
by(metis int.abs_eq_iff of_int.abs_eq)
lift_definition foo45 :: "int => nat * nat" is "%(x,y). (nat x, nat y)"
The last line gives this error:
Lifting failed for the following types:
Raw type: int
Abstract type: nat
Reason: No quotient type "Nat.nat" found.
But my "foo45" represents what I want, but you'll have to tell me
exactly what I have to do to get something like that.
The term "(nat x, nat y)" has type "int * int" and you want to lift it
to a term of the type "nat * nat". That's not possible because there is
not registered any such quotient (or subtype) (i.e., using integers to
represent natural numbers).
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
This gives you for each positive integer x a pair (x, 0) and for each
negative integer (0, 0).
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and