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

*To*: Aditya Kanade <aditya@cse.iitb.ac.in>*Subject*: Re: [PVS-Help] Turning let declarations into name equalities*From*: "Cesar A. Munoz" <munoz@nianet.org>*Date*: Fri, 29 Jul 2005 15:33:56 -0400*Cc*: pvs-help@csl.sri.com*In-Reply-To*: <42EA804F.9000409@cse.iitb.ac.in>*List-Help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-Id*: PVS-Help <pvs-help.csl.sri.com>*List-Post*: <mailto:pvs-help@csl.sri.com>*List-Subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-Unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*Organization*: NIA*References*: <42EA804F.9000409@cse.iitb.ac.in>*Sender*: pvs-help-bounces+archive=csl.sri.com@csl.sri.com

Aditya, If you have the package Field (http://research.nianet.org/~munoz/Field), which is pre-installed with the NASA PVS Libraries, then what you want is the strategy skoletin (see also, skoletin*, redlet) l : |------- {1} f(a) Rule? (expand "f" :assert? none) Expanding the definition of f, this simplifies to: l : |------- {1} LET x = a IN x OR NOT a Rule? (skoletin 1) Reducing a let-in expression in 1, this simplifies to: l : {-1} x = a |------- {1} x OR NOT a Cesar On Fri, 2005-07-29 at 15:15, Aditya Kanade wrote: > Hi, > > Consider a function "f" defined as a (chained) let expression. When one > expands it's definition, the let bindings are substituted in the > function body. Instead of that I want to maintain the function > definition as it is and turn the let bindings into name expression. > > t:theory > begin > > f(a:bool):bool = let x = a implies a in x or not a > ;; In general, rhs of let binding can be very complicated > l:lemma forall (a:bool): f(a) > > end t > > For instance, instead of following sequent > > |----- > [1] a or not a > > I want this one > > [1] a = x > |---- > [1] x or not a > > Both are equivalent but the latter is more convenient in presence of > complicated and large function definitions/rewrites. It still allows one > to concentrate on proof goal without getting lost in the details arising > out of rewrites. The replacement can be done only when needed. I tried > declaring various forms of "auto_rewrite+" for "f" but it didn't work. > > Clearly, it is possible to get the latter form from the first by using > (name "x" "a") and selectively replacing "a" by "x". This does not > always work when restrict/extend etc. are present. Any suggestions? How > can this be automated in general? Besides, I'm automatically generating > these definitions and lemmas (in a formal similar to above declarations) > so can that processing be used? I would call such feature an > "abbreviation" mechanism (to keep sequents readable) where "a" is > abbreviated by "x". > > Regards, > Aditya. -- Cesar A. Munoz H., Senior Staff Scientist mailto:munoz@nianet.org National Institute of Aerospace mailto:C.A.Munoz@larc.nasa.gov 100 Exploration Way http://research.nianet.org/~munoz Hampton, VA 23666, USA Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988

**References**:**[PVS-Help] Turning let declarations into name equalities***From:*Aditya Kanade <aditya@cse.iitb.ac.in>

- Prev by Date:
**[PVS-Help] Turning let declarations into name equalities** - Next by Date:
**[PVS-Help] adt_union** - Prev by thread:
**[PVS-Help] Turning let declarations into name equalities** - Next by thread:
**[PVS-Help] Measure Induction** - Index(es):