[PVS-Help] Confused about proving extensionality of overriddenfunctions

[David Coppit <sri@coppit.org>]

Hello all,

I'm trying to learn PVS, and need a gentle push in the right direction.

Assume this specification for a function-based implementation of stacks:

   stacks: THEORY BEGIN

     stack: TYPE = [# size: nat, elements: ARRAY[nat->int] #]
     empty: stack = (# size:=0, elements:=(LAMBDA (j: nat): 0) #)

     push(x: int, s:stack): { s: stack | s`size>=1 } =
       (# size:=s`size+1,
          elements:=s`elements WITH [(s`size):=x] #)

     pop(s:stack | s`size>=1): stack =
       (# size:=s`size-1,
          elements:=s`elements WITH [(s`size-1):=0] #)

     % Hack for now
     all_above_are_zero: LEMMA
       FORALL (s: stack, x: int): x>s`size => s`elements(x) = 0

     push_pop: THEOREM
       FORALL (s: stack, x: int): pop(push(x, s))=s

   END stacks

When proving push_pop, I start with

   (skolem!)
   (expand* "push" "pop")
   (lemma "all_above_are_zero" ("s" "s!1" "x" "s!1`size"))
   (assert)
   (apply-extensionality)

This results in the sequent:

[-1]  s!1`elements(s!1`size) = 0
   |-------
{1}   s!1`elements WITH [(s!1`size) := 0] = s!1`elements
[2]   (# size := s!1`size,
          elements := s!1`elements WITH [(s!1`size) := 0] #)
        = s!1

Question #1: Now what? Shouldn't formula -1 be enough for formula 1?

Question #2: I tried writing all_above_are_zero as an axiom, but didn't
know how to utilize it in my proof. Is there some way to "use" an axiom?

Question #3: How do I rewrite my axiom so that it is higher-level, stating
that all stacks are either the empty stack, or derived from it?

Thanks,
David

_____________________________________________________________________
David Coppit                           david@coppit.org
The College of William and Mary        http://coppit.org/

"They have computers, and they may have other weapons of mass destruction."
Former Attorney General Janet Reno, speaking at LLNL of modern criminals