[isabelle] Problem with lift_definition
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.
definition of_nat :: "nat \<Rightarrow> 'a" where
"of_nat n = (op \<oplus> \<one> ^^ n) \<zero>"
lift_definition of_int :: "int \<Rightarrow> 'a" is "\<lambda>(i, j). of_nat i \<ominus> of_nat j"
This archive was generated by a fusion of
Pipermail (Mailman edition) and