*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Missing transfer rules in quotient type*From*: Daniel Raggi <danielraggi at gmail.com>*Date*: Tue, 17 Dec 2013 15:17:36 +0000

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

**Follow-Ups**:**Re: [isabelle] Missing transfer rules in quotient type***From:*Andreas Lochbihler

**Re: [isabelle] Missing transfer rules in quotient type***From:*Ondřej Kunčar

- Previous by Date: Re: [isabelle] Interpretation inside locale raises DUP
- Next by Date: Re: [isabelle] lift_definition + constructor
- Previous by Thread: Re: [isabelle] (no subject)
- Next by Thread: Re: [isabelle] Missing transfer rules in quotient type
- Cl-isabelle-users December 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list