Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problem with lift_definition


view this post on Zulip Email Gateway (Aug 19 2022 at 11:16):

From: Stefan Berghofer <berghofe@in.tum.de>
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
Test.thy

view this post on Zulip Email Gateway (Aug 19 2022 at 11:16):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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


Last updated: Mar 29 2024 at 08:18 UTC