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