-- ---------------------------------------------------------------------------- -- -- adt.cafe -- Abstract Data Types in CafeOBJ. -- -- (c) 2016, Wolfgang Schreiner: Thinking Programs. -- -- ---------------------------------------------------------------------------- -- an initial specification of the type "integer numbers": int(m,n) = m-n module! MYINTCORE { protecting (NAT) -- the sort and its constructor [ Int ] op int : Nat Nat -> Int -- the axiom (N1+1)-(N2+1) = N1-N2 -- eq int(s(N1),s(N2)) = int(N1,N2) . -- we use the conditional equation, because for the builtin type Nat -- above pattern-matching equation does not work vars N1 N2 : Nat ceq int(N1,N2) = int(p(N1),p(N2)) if N1 =/= 0 and N2 =/= 0 . } -- computing with integers open MYINTCORE . -- optionally: set trace on . reduce int(5,3) . close . -- the type "integer numbers" with auxiliary operations module* MYINT { protecting (MYINTCORE) op 0 : -> Int op _ + _ : Int Int -> Int op _ <= _ : Int Int -> Bool vars N1 N2 M1 M2 : Nat eq 0 = int(0,0) . eq int(N1,N2) + int(M1,M2) = int(N1 + M1,N2 + M2) . eq int(N1,N2) <= int(M1,M2) = N1 + M2 <= M1 + N2 . } -- computing with integers open MYINT . reduce int(5,3) + int(2,7) . close . -- the loose specification of an arbitrary element type module* ELEM { [ Elem ] } -- an initial specification of the type "list of elements" module! LISTCORE[ E :: ELEM ] { [ List ] op empty : -> List op cons : Elem List -> List } -- the type "list of elements" extended by auxiliary operations module* LIST[ E :: ELEM ] { protecting (LISTCORE(E)) protecting (NAT) op head : List -> Elem op tail : List -> List op append : List List -> List op length : List -> Nat var E : Elem vars L L1 L2 : List eq head(cons(E, L)) = E . eq tail(cons(E, L)) = L . eq append(empty, L2) = L2 . eq append(cons(E,L1), L2) = cons(E, append(L1, L2)) . eq length(empty) = 0 . eq length(cons(E,L)) = 1 + length(L) . } -- viewing integers as list elements view INT->ELEM from ELEM to MYINT { sort Elem -> Int } -- the type "list of integers" module* INTLIST { protecting (LIST(INT->ELEM)) } -- computing with lists of integers open INTLIST . let L = append(cons(int(3,1),cons(int(5,8),empty)), cons(int(12,7),empty)) . reduce L . reduce length(L) . close . -- a proof of the property -- forall L1, L2. length(append(L1,L2)) == length(L1)+length(L2) -- by structural induction on L1 open INTLIST . -- the base case L1=empty op L2 : -> List . reduce length(append(empty,L2)) == length(empty) + length(L2) . -- the induction assumption op L1 : -> List . eq length(append(L1,L2)) = length(L1) + length(L2) . -- the induction step op I : -> Int . reduce length(append(cons(I,L1),L2)) == length(cons(I,L1)) + length(L2) . close . -- ---------------------------------------------------------------------------- -- end of file -- ----------------------------------------------------------------------------