*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*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Wed, 22 May 2013 00:13:59 -0500*In-reply-to*: <519BA5FB.2060602@in.tum.de>*References*: <519AE86B.2030208@gmx.com> <519BA5FB.2060602@in.tum.de>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

Ondřej,

I found this:

And it turns out you have connections to Josef Urban.

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

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.

Thanks for the help, GB On 5/21/2013 11:51 AM, Ondřej Kunčar wrote:

On 05/21/2013 05:22 AM, Gottfried Barrow wrote:I try to do some lifting, like on line 208: (208) lift_definition of_int :: "int => 'a" is "%x(i,j). of_nat i - of_nat j" However, on line 1661, there's this: (1661) declare Quotient_int [quot_del] In isar-ref.pdf, it tells me that's to disable lifting for int, and so I try to enable it blindly like, setup_lifting Quotient_int, but I get a warning, and lifting doesn't work for me.I guess "lifting doesn't work for me" means this: Lifting failed for the following term: Term: λ(i∷nat, j∷nat). of_nat i - of_nat j Type: nat × nat ⇒ ?'b∷{minus,semiring_1}Reason: The type of the term cannot be instantiated to "nat × nat ⇒'a∷type".And this gives you a hint where the problem is: you cannot instantied 'a::type for ?'b::{minus, semiring_1}. The original definition of of_int in Int.thy is done in a context ring_1. Try this:lift_definition of_int :: "int => 'a::ring_1" is "%(i,j). of_nat i -of_nat j"QUESTION: Can I enable lifting for int?Yes, by the command you used: setup_lifting Quotient_int or even better together with the reflexivity theorem: setup_lifting Quotient_int int_equivp[THEN equivp_reflp2] Ondrej

**Attachment:
130521a__lifting_attempt.png**

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

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

- Previous by Date: Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy
- 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