[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [LET .. IN ..]

On Thu, Feb 07, 2002 at 04:31:18PM +0100, Gwen Salaun wrote:
> I have got a problem with the LET statement of the pvs language. I work
> on an embedding of a simple process algebra with value passing. To
> express the substitution of an input variable by an output value, I
> chooses to use the LET construction. Yet, I face a problem at the proof
> level. Indeed, when I apply the 'skosimp' and 'lemma' rules, I am
> surprised to note that the variable 'x' appearing in LET x=t IN is not
> renamed with 'x!1'. Then, the substitution becomes impossible. I try
> different ways to get round this lock, but my attempts do not succeed.


you are confusing using defined names (as in LET x=t) and skolemized
variables here.

(SKOSIMP) will replace variables bound by FORALL quantors (or EXISTS
quantors in the antecedent) with skolem constants like "x!1", whereas
"LET x=t IN..." just introduces "x" as an 'abbreviation' for "t" in
the "..." part. In the proof, you will notice that LET expressions
disappear after doing (ASSERT), and the abbreviations are expanded.

> ax1 : AXIOM n1=n2 AND F = I(n1,x) o H AND G = O(n2,t) o I IMPLIES F/G =
> I(n1,x) o (H/G) + O(n2,t) o (F/I) + tau o ((LET x=t IN H) / I)

You cannot use LET here to 'substitute' an occurrence of "x" in a
previously defined expression. If there was a previous definition of
"x", it will not be visible in the scope of the LET expression.
(Remember: H is a closed expression without free variables.)

One way to do substitutions is to make H a function with parameter x.
Then you can just write H(x) or H(x!1).

Christoph Berg
cb@cs.uni-sb.de, http://www-wjp.cs.uni-sb.de/~cb/
Office +49/681/302-4129, Fax -4290, Home +49/681/9657944
Computer Science Dept., Universität des Saarlandes, Saarbrücken

PGP signature