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

Phonebook example from WIFT'95 paper not working?

Hi, I'm just starting " A Tutorial Intro. to PVS" from WIFT;95, and PVS's
response to the second example is not what the paper promises.  On page
11, relating to CONJECTURE DelAdd2, the paper says that "(grind :theories
("phone_1")) strategy proves this".  however,  PVS Version 2.1 (patch
level 2.417) says:

  DelAdd2 :  

  {1}    FORALL (bk: B), (nm: N), (pn: P):
          FindPhone(bk, nm) = n0 => DelPhone(AddPhone(bk, nm, pn), nm) =bk

  Rule? (grind :theories ("phone_1"))
  FindAx rewrites FindPhone(bk, nm)
    to  bk(nm)
  Addax rewrites AddPhone(bk, nm, pn)
  to  bk WITH [(nm) := pn]
  Delax rewrites DelPhone(bk WITH [(nm) := pn], nm)
    to  bk WITH [(nm) := n0]
  Trying repeated skolemization, instantiation, and if-lifting,
  this simplifies to: 
  DelAdd2 :  

  {-1}    bk!1(nm!1) = n0
  {1}    bk!1 WITH [(nm!1) := n0] = bk!1


Help, What do I do now?  


btw, here is my phone_1.pvs file:
phone_1 : THEORY


  N : TYPE 
  P : TYPE
  B : TYPE = [N -> P]

  n0: P
  emptybook : B
  emptyax: AXIOM FORALL (nm: N) : emptybook(nm) = n0
  FindPhone : [B, N -> P]
  FindAx : AXIOM FORALL (bk:B) (nm: N): FindPhone(bk,nm) = bk(nm)

  AddPhone : [B,N,P->B]
  Addax : AXIOM FORALL (bk:B),(nm:N),(pn:P):
         AddPhone(bk,nm,pn) = bk WITH [(nm) := pn]

  FindAdd: CONJECTURE FORALL (bk:B), (nm:N), (pn:P): 
         FindPhone(AddPhone(bk,nm,pn),nm) = pn

  DelPhone : [B, N -> B]
  Delax : AXIOM FORALL (bk:B),(nm:N): DelPhone (bk,nm) = bk WITH [(nm) := n0]
  DelAdd2: CONJECTURE FORALL (bk:B),(nm:N),(pn:P) :
      FindPhone(bk,nm) = n0 =>  DelPhone(AddPhone(bk,nm,pn),nm) = bk

  END phone_1

- Byron