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



Ondřej,

One thing led to another, and I did a bunch of searches, and it turns out you would be one of the two to ask for a tutorial on lifting, but I'm sure you don't have time.

I found this:

http://www4.in.tum.de/~kuncar/documents/huffman-kuncar-itp2012.pdf <http://www4.in.tum.de/%7Ekuncar/documents/huffman-kuncar-itp2012.pdf>

And it turns out you have connections to Josef Urban.

I got rid of my setup_lifting warning by importing Quotient_Product.thy, from a tip of yours here:

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-January/msg00127.html

Now, I do setup_lifting, and the line of code you gave me works, so I'm at an error for a simple thing I want to do, which will show you that I have a fundamental misunderstanding of how to use lifting:

   setup_lifting Quotient_int
   lift_definition of_int :: "int => 'a::ring_1" is "%(i, j). of_nat i
   - of_nat j"
      by(metis int.abs_eq_iff of_int.abs_eq)

   lift_definition foo45 :: "int => nat * nat" is "%(x,y). (nat x, nat y)"

The last line gives this error:

   Lifting failed for the following types:
   Raw type:  int
   Abstract type:  nat
   Reason:  No quotient type "Nat.nat" found.

But my "foo45" represents what I want, but you'll have to tell me exactly what I have to do to get something like that.

I've attached a screenshot which shows the four lines of code above, with the error.

Thanks for the help,
GB


On 5/21/2013 11:51 AM, Ondřej Kunčar wrote:
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



Attachment: 130521a__lifting_attempt.png
Description: PNG image



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