# Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy

On 05/21/2013 05:22 AM, Gottfried Barrow wrote:

I try to do some lifting, like on line 208:
(208) lift_definition of_int :: "int => 'a" is "%x(i,j). of_nat i -
of_nat j"
However, on line 1661, there's this:
(1661) declare Quotient_int [quot_del]
In isar-ref.pdf, it tells me that's to disable lifting for int, and so I
try to enable it blindly like,
setup_lifting Quotient_int,
but I get a warning, and lifting doesn't work for me.

I guess "lifting doesn't work for me" means this:
Lifting failed for the following term:
Term: λ(i∷nat, j∷nat). of_nat i - of_nat j
Type: nat × nat ⇒ ?'b∷{minus,semiring_1}

`Reason: The type of the term cannot be instantiated to "nat × nat ⇒
``'a∷type".
`
And this gives you a hint where the problem is:
you cannot instantied 'a::type for ?'b::{minus, semiring_1}.
The original definition of of_int in Int.thy is done in a context ring_1.
Try this:

`lift_definition of_int :: "int => 'a::ring_1" is "%(i,j). of_nat i -
``of_nat j"
`

QUESTION: Can I enable lifting for int?

Yes, by the command you used:
setup_lifting Quotient_int
or even better together with the reflexivity theorem:
setup_lifting Quotient_int int_equivp[THEN equivp_reflp2]
Ondrej

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