*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy*From*: Ondřej Kunčar <kuncar at in.tum.de>*Date*: Wed, 22 May 2013 13:49:45 +0200*In-reply-to*: <519C5417.9040006@gmx.com>*References*: <519AE86B.2030208@gmx.com> <519BA5FB.2060602@in.tum.de> <519C5417.9040006@gmx.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130329 Thunderbird/17.0.5

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.

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

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

Ondrej

**Follow-Ups**:**Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy***From:*Gottfried Barrow

**References**:**[isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy***From:*Gottfried Barrow

**Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy***From:*Ondřej Kunčar

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

- Previous by Date: Re: [isabelle] [isabelle-dev] Partial functions
- Next by Date: Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy
- Previous by Thread: Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy
- Next by Thread: Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy
- Cl-isabelle-users May 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list