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

[PVS-Help] Turning let declarations into name equalities



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.