Phil, On 2 Aug 2011, at 16:26, Phil Clayton wrote:
> 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? There is no convention on what a conversion should or shouldn't do other than return an equation whose LHS is alpha-equivalent to the term passed as argument to the conversion. I don't quite know what you mean by "denormalized". I would just say "not Z". But the argument of z_%exists%_intro_conv1 is expected to be Z, it's expected to be an HOL existential quantification whose matrix is like the matrix of a Z existential quantification when viewed as HOL. It make sense to me for z_%exists%G_intro_conv1 to make up for something that is very likely to have gone wrong with the matrix from the Z point of view when it was being manipulated as HOL. (This applies to the analogous conversions for universal and unique existential quantifications too). > 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? I don't think it is desirable (a) because it is unnecessary in several of the places where those conversions are used (the documentation is overcautious/wrong about this as far as I can see, e.g. I don't believe z_%mu%_rule ever needs rename Z bound variables) and (b) because it requires a "deep" term traversal: essentially you will have to map z_dec_rename%down%s_conv over the whole term. I would rather leave it to the user to decide whether to do that. I think it will be more useful to make z_%exists%_intro_conv and friends more accommodating. Regards, Rob.
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com