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

*To*: Gwen Salaun <Gwen.Salaun@irin.univ-nantes.fr>*Subject*: Re: [LET .. IN ..]*From*: Christoph Berg <cb@cs.uni-sb.de>*Date*: Fri, 8 Feb 2002 01:02:54 +0100*Cc*: pvs-help@csl.sri.com, salaun@irin.univ-nantes.fr*In-Reply-To*: <3C629DC6.832B2261@irin.univ-nantes.fr>*References*: <3C629DC6.832B2261@irin.univ-nantes.fr>*Sender*: pvs-help-owner@csl.sri.com*User-Agent*: Mutt/1.3.25i

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

**References**:**[LET .. IN ..]***From:*Gwen Salaun <Gwen.Salaun@irin.univ-nantes.fr>

- Prev by Date:
**[LET .. IN ..]** - Next by Date:
**library importings** - Prev by thread:
**[LET .. IN ..]** - Next by thread:
**Generalizations** - Index(es):