*To*: Stefan Berghofer <berghofe at in.tum.de>*Subject*: Re: [isabelle] Problem with lift_definition*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Fri, 14 Jun 2013 08:21:44 +0200*Cc*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <51B9E25A.5070108@in.tum.de>*References*: <51B9E25A.5070108@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130510 Thunderbird/17.0.6

Hi Stefan, you can re-register deleted quotients with Lifting_Info.update_quotients as follows: setup {* Context.theory_map (Lifting_Info.update_quotients @{type_name int} {quot_thm = @{thm Quotient_int}, pcrel_def = NONE}) *}

Hope this helps, Andreas On 13/06/13 17:16, Stefan Berghofer wrote:

Hi all, I am currently trying to define variants of the of_nat and of_int functions using the operations from HOL/Algebra (see attachment). While the definition of of_nat works as expected, attempting to define of_int using lift_definition leads to the error message 'No quotient type "Int.int" found', because int has been de-registered as a quotient at the end of Int.thy. Is there a way to re-register int as a quotient type or am I not supposed to do this? Also, has anyone else already tried to define of_nat and of_int using the operations from HOL/Algebra? I have tried to define of_int using a case distinction on whether the integer is positive or negative, but this leads to rather clumsy proofs. Greetings, Stefan

**References**:**[isabelle] Problem with lift_definition***From:*Stefan Berghofer

- Previous by Date: Re: [isabelle] HOL-Proofs
- Next by Date: [isabelle] Fwd: Installation problem
- Previous by Thread: [isabelle] Problem with lift_definition
- Next by Thread: [isabelle] Fwd: Installation problem
- Cl-isabelle-users June 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