Re: [isabelle] Superfluous transfer rules



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





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