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.