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.