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

Reply via email to