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 %%% %%% VAL is the "abstraction" function, mapping a numeral to the number it represents. %%% %%% Scheme translation: %%% %%% (define VAL (lambda (l) %%% (if (null? l) %%% 0 %%% (+ (if (car l) 1 0) (* 2 (VAL (cdr l))))))))))))))))) %%% 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, false)) = VAL(l1) + VAL(l2) %%% END th_K