%%%
%%% The tree data type.  Note the parameterization of values.
%%%
tree[T:TYPE]: DATATYPE
  BEGIN
  leaf : leaf?
  node(val: T, left: tree, right: tree): node?
  END tree

th_L: THEORY
BEGIN

IMPORTING tree_adt[int]

itree: TYPE = tree[int] 

i,j,k,l,m : VAR int
t,rt,lt : VAR itree

%%
%% seek searches a tree depth-first, left-to-right
%% for an occurance of a node containing value i.
%%
seek(i:int, tr:itree): RECURSIVE itree =
  CASES tr OF
   leaf: tr,
   node(j, lt, rt): IF (j = i)
                    THEN tr
                    ELSE LET st = seek(i, lt) IN
                         IF leaf?(st)
                            THEN seek(i, rt)
                            ELSE st
                         ENDIF
                    ENDIF
  ENDCASES
  MEASURE tr BY <<

test_tree_1:itree = node(1, node(2, leaf, leaf), node(3, leaf, leaf))

L0: PROPOSITION val(seek(3, test_tree_1)) = 3

%%
%% This proposition says 'seek' always returns a node with the right
%% value.

L1: PROPOSITION
    (FORALL (i:int, t:itree) : node?(seek(i,t)) => val(seek(i,t)) = i)

%%
%% count the interior nodes in a tree
%%

count_nodes(tr:itree): RECURSIVE nat =
  CASES tr OF
   leaf: 0,
   node(j, lt, rt): 1 + count_nodes(lt) + count_nodes(rt)
  ENDCASES
  MEASURE tr BY <<

%%
%% count the leaves in a tree
%%

count_leaves(tr:itree): RECURSIVE nat =
  CASES tr OF
   leaf: 1,
   node(j, lt, rt): count_leaves(lt) + count_leaves(rt)
  ENDCASES
  MEASURE tr BY <<

%%
%% size(tr) = #nodes + #leaves
%%

size_of(tr:itree):nat = count_leaves(tr) + count_nodes(tr)

%%
%% A tree always has exactly one more leaves than nodes.
%%

L2: PROPOSITION
    (FORALL (t:itree) : count_leaves(t) = count_nodes(t) + 1)

%%
%% depth calculates the depth of a tree
%%

depth(tr:itree): RECURSIVE nat =
  CASES tr OF
    leaf: 1,
    node(j, lt, rt): 1 + max(depth(lt), depth(rt))
  ENDCASES
  MEASURE tr BY <<

%%
%% a FULL tree has uniform depth and balance.
%%

full_tree(tr:itree): RECURSIVE bool =
  CASES tr OF
    leaf: TRUE,
    node(j, lt, rt): depth(lt) = depth(rt)
                    AND full_tree(lt)
                    AND full_tree(rt)
  ENDCASES
  MEASURE tr BY <<

%% 
%% The size of a full tree is one less than a power of two
%%

l3: PROPOSITION (FORALL (t:itree) :
     full_tree(t)
     IMPLIES
     size_of(t) = 2^(depth(t)) - 1)

%%%
%%% What is another way to state Proposition l3, using predicative sub-typing?
%%%
END th_L