Re: [isabelle] Superfluous transfer rules



On Thu, Jun 28, 2012 at 10:23 AM, Andreas Lochbihler
<andreas.lochbihler at kit.edu> wrote:
>> 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"
[...]
> 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.

It seems that this was an instance of the same kind of problem. After
generalizing the transfer rules, the transfer proof works now. See the
changeset on AFP:

http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/a05edd1f98f8

- Brian





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