@*Theory of sequences.
The theory of sequences is built on the theory of stacks.
The stack theory provides most of the machinery needed for the elementary
operations on lists: |insert|, |head|, |tail|, and |is_empty|.
The sequence trait includes
additional machinery that allows easy specification of concatenation.
@c
sequence: trait
imports Stack_theory with [nil for empty_stack,
cons for push, first for top, rest for pop]
introduces
enter: C,E -> C % adds e to back of c
last: C -> E
prefix: C -> C % c with last deleted
#.[#]:C, Card -> E % indexed selection (starts at 1)
append: C,C -> C % concatenation
constrains [C] so that C is generated by [new, insert]
C is generated by [new, enter]
C is partitioned by [first, rest, isEmpty]
C is partitioned by [last, prefix, isEmpty]
for all [e:E]
last(enter(new,e)) = e
prefix(enter(new,e)) = new
for all [c:C, e:E]
not isEmpty(enter(c,e))
last(enter(c,e)) = e
prefix(enter(c,e)) = stk
for all [c:C, e, e1: E]
insert(new,e) = enter(new,e)
insert(enter(c,e),e1) = enter(insert(c,e1),e)
for all [c:C, i:Card]
c.[1] = first(c)
c.[i+1] = rest(c).[i]
for all [c,c1:C, e:E]
append(c,new) = c
append(c,insert(c1,e)) = insert(append(c,c1), e)
implies
converts [insert, first, last, rest, prefix],
[enter, first, last, rest, prefix],
[append],
[isEmpty],
[size],
[#.[#]]
exempts last(new), prefix(new), first(new), rest(new)
% for all [c:C], c(0)
@*Index.