Re: [isabelle] Missing transfer rules in quotient type



Hi Daniel,
sorry for the inconvenience.
There is an easy fix: Rename cr_bin in your user-provided transfer rules to pcr_bin.

Long answer: The transfer relation that is used in rules that are generated by the Lifting package is now called pcr_T, which is a generalization of cr_T and uses cr_T internally. You can prove "pcr_bin = cr_bin" (thm bin.pcr_cr_eq) for your type bin because bin is not a polymorphic type. In general pcr_T op= ... op= = cr_t. So what is pcr_T? It's a relation that allows you to change the polymorphic argument of your type (if there is one). E.g., consider 'a fset defined in HOL/Library/FSet. Here cr_fset :: 'a set => 'a fset => bool, whereas pcr_fset :: ('a => 'b => bool) => 'a set => 'b fset => bool. And pcr_fset op= = cr_fset.

Btw, you don't have to import HOL/Library/Quotient_List since the content of this file that is relevant for Lifting and Transfer has been moved to Main. The syntax for Lifting (===> and --->) is now also local and can be reintroduced by this trick:

context
begin
  interpretation lifting_syntax .

...

end

Hope this helps.
Ondrej

On 12/17/2013 04:17 PM, 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.