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:
Ondřej,

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:

http://www4.in.tum.de/~kuncar/documents/huffman-kuncar-itp2012.pdf
<http://www4.in.tum.de/%7Ekuncar/documents/huffman-kuncar-itp2012.pdf>

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:

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-January/msg00127.html


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:

    setup_lifting Quotient_int
    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 (http://www.inf.kcl.ac.uk/staff/urbanc/Publications/sac-11.pdf).

Ondrej





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