th_K: THEORY
BEGIN
%%%
%%% Define a valuation function for binary lists.
%%% Define a function that adds two binary lists.
%%% Prove that the addition function is correct.
%%%

boolist: DATATYPE
 BEGIN
  null: null?
  cons (car: bool, cdr:boolist):cons?
 END boolist

l, l1, l2, l3: VAR boolist
a, b, c, b1, b2, b3: VAR bool

%%%
%%% evaluation of bit-lists as numbers
%%%
VAL(l:boolist): RECURSIVE nat =
  CASES l OF
    null: 0,
    cons(b, tl): (IF b THEN 1 ELSE 0 ENDIF) + 2 * VAL(tl)
  ENDCASES
  MEASURE l by <<

TEST_VAL: PROPOSITION VAL(cons(true, cons(false, cons(true, cons(true, null))))) = 13
%%%
%%% For practice, here's a function that increments a binary
%%% number and a theorem stating that it works.
%%%

INC(l:boolist): RECURSIVE boolist =
  CASES l OF
    null: cons(true, null),
    cons(b, tl): IF b THEN cons(false, INC(tl)) ELSE cons(true, tl) ENDIF
  ENDCASES
  MEASURE l by <<

TEST_VAL_INC: PROPOSITION VAL(INC(cons(true, cons(false, cons(true, cons(true, null)))))) = 14

INC_WORKS: LEMMA VAL(INC(l)) = 1 + VAL(l)

%%%
%%% Now define a function that adds two binary numbers and prove that
%%% it works.
%%%
%%% ADD(l1, l2: boolist, c:bool): RECURSIVE boolist =...
%%%
%%% maybe some lemmas...
%%%
%%% ADD_WORKS: THEOREM VAL(ADD(l1, l2, 0)) = VAL(l1) + VAL(l2)
%%%
 
END th_K