[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