%%%
%%% To prove equality of functions, arrays, and records, the prover
%%% command EXTENSIONALITY (and its variants) introduce the appropriate
%%% law of extensionality, which you must then instantiate properly.
%%% See the prover manual.
%%%
%%% Specification for the abstract data type of stacks
%%%
stacks_spec_1 [t: TYPE+] : THEORY
BEGIN

  %%
  %% Carrier type
  %%

  stack     : TYPE+

  s         : VAR stack
  x,y       : VAR t

  %%
  %% Tests
  %%

  mt   : stack
  non_mt?(s): bool = (s /= mt)

  %% 
  %% Signature
  %% 

  push :[t, stack -> (non_mt?)]
  pop  :[(non_mt?) -> stack]
  top  :[(non_mt?) -> t]



  %%
  %% Identities
  %%

  stack_law_1: AXIOM pop(push(x,s)) = s
  stack_law_2: AXIOM top(push(x, s)) = x
  stack_law_3: AXIOM non_mt?(s) IMPLIES push(top(s), pop(s)) = s

  %%
  %%  Sanity check:
  %%

  stack_prp_1: PROPOSITION pop(pop(push(x, push(y, s)))) = s

END stacks_spec_1

%%%
%%% Implementing stacks using arrays
%%%

stacks_impl_1 [T: TYPE+] : THEORY

BEGIN

  stack : TYPE = [# size:nat, content: ARRAY[nat -> T] #]

  s, s1, s2: VAR stack
  x,y: VAR T
  dontknow: T


 non_mt?(s): bool = (size(s) /= 0)

 mt: stack = (# size := 0, content := (LAMBDA (n:nat): dontknow) #)

 push(x, s): (non_mt?) = (# size := size(s) + 1,
                            content := (LAMBDA (n:nat): IF n = size(s)
                                                        THEN x
                                                        ELSE content(s)(n)
                                                        ENDIF)
                          #)

 ns: VAR (non_mt?)

 top(ns): T = content(ns)(size(ns)-1)

 pop(ns): stack = (ns WITH [size := size(ns) - 1])

%%%
%%% These propositions re-state the abstract-stack identities
%%%

 stack_law_1: CLAIM top(push(x,s)) = x
 stack_law_2: CLAIM pop(push(x,s)) = s
 stack_law_3: CLAIM non_mt?(s) IMPLIES push(top(s), pop(s)) = s

 stack_prp_1: PROPOSITION pop(pop(push(x, push(y, s)))) = s

END stacks_impl_1

%%%
%%% The same stack implementation as stacks_impl_1,
%%% plus represenation equivalence.
%%%

stacks_impl_2 [T: TYPE+] : THEORY

BEGIN

IMPORTING stacks_impl_1[T]
 
 s, s1, s2: VAR stack
 x,y: VAR T

 eq(s1, s2): bool = (size(s1) = size(s2))
           AND (forall (n:nat):
                  (n < size(s1)) IMPLIES (content(s1)(n) = content(s2)(n)))

 stack_law_1: PROPOSITION top(push(x, s)) = x
 stack_law_2: PROPOSITION eq(pop(push(x,s)), s)
 stack_law_3: PROPOSITION non_mt?(s) IMPLIES eq(push(top(s), pop(s)), s)

 stack_prp_1: PROPOSITION eq(pop(pop(push(x, push(y, s)))), s)

END stacks_impl_2

%%%
%%% stack implementation using dependent types
%%% 

stacks_impl_3 [T: TYPE+] : THEORY
BEGIN

 i,j: VAR nat

 stack : TYPE = [# size:nat, content: ARRAY[{i | i < size} -> T] #]

 s, s1, s2: VAR stack
 x,y: VAR T
 dontknow: T

 non_mt?(s): bool = (size(s) /= 0)

 me: stack = (# size := 0, content := (LAMBDA (j:{i|i<0}): dontknow) #)

 push(x, s): (non_mt?) = (# size := size(s) + 1,
                            content := content(s) WITH [(size(s)) := x]
                          #)

 ns: VAR (non_mt?)

 top(ns): T = content(ns)(size(ns)-1)
 pop(ns): stack = (# size := size(ns) - 1,
                     content := (LAMBDA (j: {i|i<size(ns) - 1}):
                                  content(ns)(j))
                   #)


 stack_law_1: PROPOSITION non_mt?(s) IMPLIES push(top(s), pop(s)) = s
 stack_law_2: PROPOSITION pop(push(x,s)) = s
 stack_law_3: PROPOSITION top(push(x, s)) = x

 stack_prp_1: PROPOSITION pop(pop(push(x, push(y, s)))) = s
 
END stacks_impl_3


%%%
%%% For an inductive type like stacks, use DATATYPE because it gives you
%%% a whole toolbox of reasoning tools, like induction.  However, this
%%% is not the end of the story.  Traditional Abstract Data Type theory
%%% is based on equivalence and does not assume recursion.  So an inductive
%%% definition is not satisfactory---and doesn't work for things like 
%%% QUEUES (try it).  See Owre & Shankar, 2001 [SRI-CSL-01-01] for a
%%% recent approach to generalizing this problem in PVS.
%%%

stacks_spec_2[T: TYPE+] : THEORY
BEGIN

stack: DATATYPE
BEGIN
 empty: empty?
 push(top:T, pop:stack) : non_empty?
END stack
 
s: VAR stack
x,y: VAR T

stack_law_1: PROPOSITION top(push(x, s)) = x
stack_law_2: PROPOSITION pop(push(x,s)) = s
stack_law_3: PROPOSITION non_empty?(s) IMPLIES push(top(s), pop(s)) = s

stack_prp_1: PROPOSITION pop(pop(push(x, push(y, s)))) = s

depth(s): RECURSIVE nat =
 CASES s OF
  empty: 0,
  push(x, s1): 1 + depth(s1)
 ENDCASES
 MEASURE s BY <<

stack_prp_2: PROPOSITION depth(s) < depth(push(x,s))

END stacks_spec_2