[isabelle] Problem with lift_definition



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

theory Test
imports "~~/src/HOL/Algebra/Ring"
begin

context ring
begin

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"

end

end



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