Re: [isabelle] Superfluous transfer rules
Thanks for looking into this.
This approach looks promising because most of the other rules I have also just
to thread "op =" through.
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)"
"is_equality A ==> (A ===> cr_stream ===> cr_stream) LCons SCons"
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.
Anyway, thanks for the feedback on lifting/transfer!
If you have time to look into that, it would be great to know why it does not
work here as expected.
Karlsruher Institut für Technologie
Am Fasanengarten 5, Geb. 50.34, Raum 025
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
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