Email Gateway (Aug 19 2022 at 11:16): 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
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: Nov 21 2024 at 12:39 UTC