[PVS-Help] (PVS novice) A doubt regarding lemma rewrites

["Nikhil D. Kikkeri" <nikhil23@hotmail.com>]

Hi--

I am using PVS to do  certain simple things for me. Right now I want to use 
PVS to build a library for redundant arithmetic systems like Carry-Save and 
Borrow-Save arithmetic. i am also sending the entire PVS theory.

I have a few expressions

CSVec2nat -- conversion from CS to natural
CSvec2nat_Proj(csnumber,upper,lower) - a projection of a certain CS number 
indexed between u and l
CSFraction -- CSVec2nat(CSProjection(csnumber,i,0)/2^(i+1)  the fractional 
value of the projection
i = upper index

CSVec2nat_Proj_bd_Correct -- Lemma  1 which shows that the CSVec2Nat(CSProj) 
< 2^(u-l+2)
This has been proved using PVS

CSFraction_UBound -- Lemma 2which shows that CSFraction < 2

This is true because CSVec2Nat(CSProj) < 2^(u-l+2)

The fractional value  CSFraction is  CSVec2Nat(CSProj)/2^(i+1) < 
2^(i-0+2)/2^(i+1)

which is  CSFraction < 2

this is clearly due to Lemma 1.
Proving Lemma 1 was no problem at all but I am struggling in the proof of 
Lemma 2.I dont see a way to use Lemma 1 to prove Lemma 2 even though Lemma 1 
is nothing but a division of 2^(i+1) on both sides.

Can someone provide some tips on how to do this?This is not for a class, 
just for messing around with PVS so do feel free to mail in your 
suggestions.

--------------------------------------------------------------------------------------------------------------

Here is the PVS theory

csnumber :THEORY

  BEGIN

    IMPORTING bitvectors@top
    n: VAR nat
    l: VAR nat
    u: VAR nat
    i: VAR nat

    CSVec(n): TYPE = [#C:bvec[n],S:bvec[n]#]

    CSVec2nat(n: nat,csv: CSVec(n)): nat = bv2nat(csv`C) + bv2nat(csv`S)

    CSVProj(n:nat,csv: CSVec(n),u:below(n), l:below(u)): CSVec(u-l+1) =
                                               (# C := csv`C^(u,l),S
                                               := csv`S^(u,l)#)

    CSDigitVal(n:nat,i:below(n),csv:CSVec(n)): nat =
                                                   
b2n(csv`C(i))+b2n(csv`S(i))

    bv22CSVec(n: nat,s:bvec[n],c:bvec[n]): CSVec(n) = (#C:= c, S:= s#)

    CSVec2nat_correct: LEMMA
                       FORALL(s,c: bvec[n]): LET csv = bv22CSVec(n,s,c) IN
                       CSVec2nat(n,csv) = bv2nat(s) + bv2nat(c)

    CSVec2Nat_BdCorrect: LEMMA
                             FORALL(csv: CSVec(n)):
                             LET i = CSVec2nat(n,csv) IN
                             i < exp2(n+1)

    CSVec2Nat_Proj_BdCorrect: LEMMA
                                  FORALL(n:nat,u:below(n),l:below(u),csv: 
CSVec(n)):
                                   LET csvproj = CSVProj(n,csv,u,l),
                                       i  = CSVec2nat(u-l+1,csvproj) IN
                                   i < exp2(u-l+2)

    %%%% FRACTION RANGES %%%%

    CSFraction(n: nat,i: below(n),csv: CSVec(n)): real =
                                                  LET csvproj = 
CSVProj(n,csv,i,0) IN
                                                    
CSVec2nat(i,csvproj)/exp2(i+1)

    CSFraction_LBound: LEMMA FORALL(n: nat,i: below(n),csv: CSVec(n)):
                            LET j = CSFraction(n,i,csv) IN
                            j >= 0

    CSFraction_UBound: LEMMA FORALL(n:nat,i: below(n), csv: CSVec(n)):
                             LET j = CSFraction(n,i,csv) IN
                             j < 2

  END csnumber


---
http://engr.smu.edu/~nikhil

_________________________________________________________________
MSN Hotmail now on your Mobile phone. 
http://server1.msn.co.in/sp03/mobilesms/ Click here.