Re: [isabelle] Missing transfer rules in quotient type



Thank you, Andreas and Ondřej. It works now! I didn't understand why I was
getting both cr_T and pcr_T in different places. Now I see that cr appeared
because I had introduced it myself with my user defined transfer rules, and
pcr appeared because that's the way the transfer method works now. By
changing cr to pcr things work smoothly. Thanks!

Daniel


On 17 December 2013 16:31, Ondřej Kunčar <kuncar at in.tum.de> wrote:

> 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.