[ProofPower] Problems using var_subst

[Rob Arthan]

On Thursday 06 May 2004 6:48 pm, Marcel Oliveira wrote:
> Hi all,
>
> I am trying to use the function var_subst but I am not getting what I
> believe it should return. As far as I understood, this function receives a
> list of pairs, a term and returns a term replacing all the free occurences
> of each first element (variable) in the list by the corresponding second
> element. However, my example (attached) is not working as it "should"!!!
> Does anyone have any idea why?

In a word: types.

Two variables with the same name but different types are different and subst 
and var_subst will not identify them. The term quotations all get given the 
most general polymorphic typing they can by the HOL type checker. For each 
term, separately, it will assign type variables 'a, 'b, ... to any unknown 
types. The upshot is that the term quotations for the individual variables 
all get type 'a. The x's in the equations will get type 'a (and so get 
substituted), but the y's get type 'b (and so don't get substituted).

My attachment shows it working properly with type ascriptions to control the 
types.

Regards,

Rob.
-------------- next part --------------
=TEX
\documentstyle[hol1,12pt]{article}

\begin{document}

=SML
map (map dest_var o  frees) [%<%x_0%>%,%<%x%>%, %<%y_0%>%,%<%y%>%, %<%x'=x %and% y'=y%>%];

subst [(%<%x_0 : 'a %>%,%<%x : 'a%>%),(%<%y_0 : 'b%>%,%<%y : 'b%>%)] %<%(x' : 'a)=x %and% (y' : 'b) =y%>%;
=GFT Output
val it = %SZT%x' = x_0 %and% y' = y_0%>% : TERM

=SML
var_subst [(%<%x_0 : 'a%>%,%<%x : 'a%>%),(%<%y_0 : 'b%>%,%<%y : 'b%>%)] %<%(x' : 'a)=x %and% (y' : 'b) =y%>%;

=GFT Output
val it = %SZT%x' = x_0 %and% y' = y_0%>% : TERM

=TEX
\end{document}