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

Re: Question about With

> As my understanding 'WITH' can be use to define constraint over a
> partial function.  I try to built 'env' and 'builtEnv' function which
> generate the constraint over 'env'.  I define a lemma that I hope can do
> the evaluation recursively.  Where is my mistakes ?

I'm not quite sure what you're trying to accomplish here.  Your definition
of env is a total function from extNode to signal[boolean].  builtEnv
updates it at the points indicated by the list el2, but the result is
still a total function, defaulting to the initial el1 on those parts not
updated.  Your lemma env_lm1 is basically the definition of the WITH
construct, and should prove with (then (skolem!)(lift-if)).

If you're trying to emulate a true partial function from extNode to
signal[boolean], then you'll find some methods of doing this in the
"Less Elementary Tutorial" available from


In particular, check the appendix.


Dr Dave Stringer-Calvert, Software Engineer, Computer Science Laboratory
SRI International, 333 Ravenswood Avenue, Menlo Park, CA 94025-3493, USA
Phone: (650) 859-3291 Fax: (650) 859-2844 David.Stringer-Calvert@sri.com