On 31/07/11 16:33, Rob Arthan wrote:
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...

My current understanding is that z_%exists%_intro_conv1 is being passed a denormalized Z term. Are conversions supposed to handle denormalized Z terms? Thinking that they weren't, I was going to look into a fix to seq_binder_simple_%alpha%_conv or prot_%alpha%_conv to prevent this happening in the first place. If it can be made to work, is that an acceptable solution?

Phil


...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




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

Reply via email to