Phil,

On 30 Jul 2011, at 17:18, Rob Arthan wrote:

> 
> On 28 Jul 2011, at 18:10, Phil Clayton wrote:
> 
>> There appears to be a bug in z_%mem%_seta_conv (see attached) when renaming 
>> of bound variables is required but the bound variables are introduced by a 
>> schema declaration.
> 
> Yes. This needs to be fixed.

I hope the work-around I posted was useful.

I have been thinking about how to fix z_%mem%_seta_conv and can do so, but I 
don't like the fix much, so I thought I would share it with you (and the list) 
to see if we can come up with something neater. The fundamental problem is with 
the conversion z_%exists%_intro_conv1 that turns HOL existentials of a suitable 
form (specifically the form returned by z_%exists%_elim_conv2) into Z 
existentials. z_%exists%_intro_conv1 doesn't know how to deal with the case 
when substitutions have caused bound variables to be renamed - but that case 
can fairly easily be fixed using z_dec_rename%down%s_conv. Unfortunately 
z_dec_rename%down%s_conv depends on z_rename%down%s_conv which is defined in 
the DTD043 module which depends on DTD042 (where  z_%mem%_seta_conv lieves) and 
DTD041 (where z_%exists%_intro_conv1 lives).

Teasing out the dependencies so that z_rename%down%s_conv can be moved into 
DTD041 doesn't look very promising, but maybe I haven't tried hard enough. 
There may be something I could do with the hated functors, but I don't know 
what. So the only option is to have a hook in DTD041 for setting a conversion 
that z_%exists%_intro_conv1 uses where z_dec_rename%down%s_conv is needed and 
calling that hook (and then filtering it out of the signature) at the end of 
DTD041.

Regards,

Rob.

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to