# Re: [isabelle] Superfluous transfer rules

Hi Brian,
Thanks for looking into this.

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"

`This approach looks promising because most of the other rules I have also just
``to thread "op =" through.
`

Anyway, thanks for the feedback on lifting/transfer!

`When I'm at it: There's one FIXME comment in Coinductive_Stream. szip_iterates
``is actually lzip_iterates from Coinductive_List_Lib lifted over the morphism.
``Unfortunately, the transfer method only replaces the left hand side, but not the
``right hand side, so I had to prove the equation directly.
`

`If you have time to look into that, it would be great to know why it does not
``work here as expected.
`
- Andreas
--
Karlsruher Institut für Technologie
IPD Snelting
Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de

`KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum
``in der Helmholtz-Gemeinschaft
`

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