%%% NAME/LOGIN-ID _____________________/______________________ %%% ACKNOWLEDGMENTS: %%% %%% Our first example of a user-defined inductive set, a list of boolean values. %%% Every DATATYPE declaration generates two corresponding things: %%% %%% 1) A scheme for defining recursive functions over that type %%% 2) An induction principle specialized to that type %%% th_J: THEORY BEGIN 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 I(l): RECURSIVE boolist = CASES l OF null: null, cons(b, tl): cons(NOT b, I(tl)) ENDCASES MEASURE l by << A(l1, l2): RECURSIVE boolist = CASES l1 OF null: l2, cons(b, tl): cons(b, A(tl, l2)) ENDCASES MEASURE l1 by << R(l): RECURSIVE boolist = CASES l OF null: null, cons(b, tl): A(R(tl), cons(b, null)) ENDCASES MEASURE l by << I_self_inverse: THEOREM I(I(l)) = l A_associative: THEOREM A(l1, A(l2, l3)) = A(A(l1, l2), l3) A_right_identity: THEOREM A(l, null) = l I_distributes_over_A: THEOREM I(A(l1,l2)) = A(I(l1), I(l2)) R_distributes_over_I: THEOREM R(I(l)) = I(R(l)) %%% %%% You will need to discover a lemma to prove the following: %%% R_self_inverse: THEOREM R(R(l)) = l END th_J