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

Re: [PVS-Help] Turning let declarations into name equalities

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