[isabelle] Missing transfer rules in quotient type



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

Attachment: quot_experiment.thy
Description: Binary data



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