Re: [isabelle] Problem with lift_definition



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

If you want transfer to work properly, you also have to re-install the transfer rules for the operations on int, i.e., declare the lemmas at the end of Int.thy as [transfer_rule].

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





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