abstract_datatypes[T: TYPE+]: THEORY

  BEGIN

  importing list_props[T]

  l, l1, l2, l3: VAR list[T]

%  The PVS prelude theory list_props contains the following function
%  definitions:
%
%  append(l1, l2): RECURSIVE list[T] =
%    CASES l1 OF
%      null: l2,
%      cons(x, y): cons(x, append(y, l2))
%    ENDCASES
%    MEASURE length(l1)
%
%  reverse(l): RECURSIVE list[T] =
%    CASES l OF
%      null: l,
%      cons(x, y): append(reverse(y), cons(x, null))
%    ENDCASES
%    MEASURE length
%
% The following results are also found in prelude theory list_props:
  
  append_null: LEMMA append(l, null) = l

  append_assoc: LEMMA
    append(l1, append(l2, l3)) = append(append(l1, l2), l3)

  reverse_append: LEMMA % Hint: try rewriting with the above two results
    reverse(append(l1, l2)) = append(reverse(l2), reverse(l1))

  reverse_reverse: LEMMA 
    reverse(reverse(l)) = l


% The following illustrates a useful built-in abbreviation for literal lists

  a, b, c: T

  list_rep: LEMMA (: a, b, c :) = cons(a, cons(b, cons(c, null)))

  END abstract_datatypes