*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 17:57:58 -0500*In-reply-to*: <519CB0D9.70701@in.tum.de>*References*: <519AE86B.2030208@gmx.com> <519BA5FB.2060602@in.tum.de> <519C5417.9040006@gmx.com> <519CB0D9.70701@in.tum.de>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

Ondřej,

What you probably meant (but I don't know I am just guessing yourintentions), is this definition:lift_definition foo45 :: "int => nat * nat" is "%(x,y). (x, y)"

Yes.

This is type correct but you can't prove the respectfulness theoremsince this theorem implies that each equivalence class in a definitionof integers contains exactly one element. That's not true.You need some kind of a normalization function that picks up oneelement for each class. For example:lift_definition foo45 :: "int => nat * nat" is "%(x,y). (x - y, 0)" byauto

This gives you for each positive integer x a pair (x, 0) and for eachnegative integer (0, 0).

For deep understanding I recommend read the paper that Brian and Iwrote about Lifting/Transfer and it is also good to know how typedefworks. You can also read a paper by Kaliszyk, Urban(http://www.inf.kcl.ac.uk/staff/urbanc/Publications/sac-11.pdf).

/ /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?"

Thanks, GB

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

**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] Two lemmas about lists constructed from finite sets that I'd like Isabelle to provide
- Next by Date: Re: [isabelle] Two lemmas about lists constructed from finite sets that I'd like Isabelle to provide
- Previous by Thread: Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy
- Next by Thread: Re: [isabelle] Problems with code generation for the reals
- 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