[isabelle] Superfluous transfer rules



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?

In case of the former: What do I have to do to avoid these kind of boilerplate rules?

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.