*To*: Andreas Lochbihler <andreas.lochbihler at kit.edu>*Subject*: Re: [isabelle] Superfluous transfer rules*From*: Brian Huffman <huffman at in.tum.de>*Date*: Thu, 28 Jun 2012 07:46:17 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4FEAF1F7.3000802@kit.edu>*References*: <4FEAF1F7.3000802@kit.edu>

On Wed, Jun 27, 2012 at 1:43 PM, Andreas Lochbihler <andreas.lochbihler at kit.edu> wrote: > When I use the transfer package, I frequently have to prove extra transfer > rules for some operations when tuples are involved. Some examples can be > found in Coinductive_Stream.thy in the AFP entry Coinductive (development > version dd789a56473c). Here's a typical one: > > lemma SCons_prod_transfer [transfer_rule]: > "(prod_rel op = op = ===> cr_stream ===> cr_stream) LCons SCons" > unfolding prod_rel_eq by(rule SCons.transfer) > > These rules are straightforward to prove (by unfolding prod_rel_eq, > fun_rel_eq, etc. and using existing transfer rules), so I would prefer not > having to state and declare them separately. Is this to due insufficient > declarations of mine or a general limitation of the current implementation? This is a limitation of the current implementation -- not of the transfer method per se, but of the form of transfer rules generated by the lift_definition command. When lifting a polymorphic constant, the ideal transfer rule should have a form that looks just like the constant's type signature, with relation variables in place of type variables. For quotient types with type parameters, the transfer relation should ideally also have a relation parameter too, like this: SCons_prod.transfer [transfer_rule]: "(A ===> cr_stream A ===> cr_stream A) LCons SCons" A slightly less ambitious implementation might just replace occurrences of "op =" at type 'a with a variable, which is separately constrained to be an equality relation: definition "is_equality R = (R = (op =))" lemma is_equality_intros [transfer_rule]: "is_equality (op =)" "is_equality A ==> is_equality B ==> is_equality (fun_rel A B)" "is_equality A ==> is_equality B ==> is_equality (prod_rel A B)" SCons_prod.transfer [transfer_rule]: "is_equality A ==> (A ===> cr_stream ===> cr_stream) LCons SCons" I tested the latter style of rules on Coinductive_Stream.thy, and everything seems to work fine with just one transfer rule per constant. I guess we'll try to make lift_definition generate rules directly in this format. Anyway, thanks for the feedback on lifting/transfer! - Brian

**Follow-Ups**:**Re: [isabelle] Superfluous transfer rules***From:*Andreas Lochbihler

**References**:**[isabelle] Superfluous transfer rules***From:*Andreas Lochbihler

- Previous by Date: [isabelle] [Q]Question about Isabelle/hol
- Next by Date: Re: [isabelle] [Q]Question about Isabelle/hol
- Previous by Thread: [isabelle] Superfluous transfer rules
- Next by Thread: Re: [isabelle] Superfluous transfer rules
- Cl-isabelle-users June 2012 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