Re: [isabelle] Missing transfer rules in quotient type



Hi Daniel,

the pcr_... relations generalise the cr_... relations. For types with type variables, they allow other relations than equality for the type variables. If there is no type variable (as in your example), pcr_... and cr_... are logically equivalent (theorem bin.pcr_cr_eq). But since Isabelle2013-1, the lifting package expects that you use pcr_... in your custom transfer rules rather than cr_... If you replace cr_... with pcr_... in your theory file, transfer should work as you expect.

Best,
Andreas

On 17/12/13 16:17, Daniel Raggi wrote:
Dear transfer/lifting experts,

I've been experimenting with transfer and lifting and there is something
that I just haven't managed to understand.
I didn't have this problem before I upgraded from Isabelle2013 to
Isabelle2013-2 (and I suspect I would have also had it with Isabelle2013-1,
but I never used it)

Things similar to what I'm about to describe happen every time I define a
new type using quotient_type or typedef. I'll give a concrete example with
quotient_type (a type with two elements, as a quotient from integers):

quotient_type bin = int / "(λx y. [x = y] (mod 2))"
    <proof>

Then I instantiate bin to the numeral class successfully and prove the
transfer rule that lets one transfer every int numeral to the 'same' bin
numeral:

lemma cr_bin_numeral [transfer_rule]: "cr_bin (numeral x) (numeral x)".

As far as I understand, this should be enough to do:

lemma "2 = (4::bin)"
   apply transfer

to get subgoal  "[2 = (4::int)] (mod 2)".
However, I get:

  1. ?a5  (2::int)  (4::int)
  2. Transfer.Rel (cr_bin ===> cr_bin ===> op =)  ?a5  op =

Here, the obvious value for  ?a5  is the relation  "λx y. [x = y] (mod 2)",
and actually this is by default with every quotient type definition, so I
don't understand why the transfer rule was not generated automatically in
the first place when I defined the new type. I thought it was already
automatic in Isabelle2013, and my theories actually broke down once I tried
running them on Isabelle2013-2 because of this issue.

The issue doesn't stop here, because even if I define the transfer rule
  (cr_bin ===> cr_bin ===> op =)  (λx y. [x = y] (mod 2)) op =
by hand I still get a problem when I try:

lemma "1 = (3::bin)"
   apply transfer

What I get is

  1. ?a5  1  3
  2. Transfer.Rel (*pcr_bin *===> cr_bin ===> op =)  ?a5  op =

This is because 1 was actually lifted so that I could instantiate bin in
the numeral class, so it's transfer rule is generated differently. I'm not
familiar with the  pcr_  thing. Can anyone explain this?

So, If I wanted to write the transfer rules for equality manually I would
have to make four rules:

(cr_bin ===> cr_bin ===> op =)  (λx y. [x = y] (mod 2)) op =
(pcr_bin ===> cr_bin ===> op =)  (λx y. [x = y] (mod 2)) op =
(cr_bin ===> pcr_bin ===> op =)  (λx y. [x = y] (mod 2)) op =
(pcr_bin ===> pcr_bin ===> op =)  (λx y. [x = y] (mod 2)) op =


I keep thinking that there's something essential I'm not understanding, but
maybe it's not me. I would greatly benefit from your feedback. I'm
attaching a test file with this experiment, if anyone wants to have a look.

Best,
Daniel





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