2.6 Library StructuredDatatypes

library Basic/StructuredDatatypes 
version 0.3
%% authors: M.Roggenbach, T.Mossakowski
%% date: 1.11.99

from

Basic/Orders version 0.3

get PartialOrder, DefineBooleanAlgebra

from

Basic/Algebra_I version 0.3 get Monoid

from

Basic/Numbers version 0.3 get Nat, Int

from

Basic/SimpleDatatypes version 0.3 get Char

spec

Elem =

sort

Elem

end

spec

GenerateFiniteSet  [Elem with sort Elem] =

free

{

type

FinSet[Elem]::=	{} | set(Elem) |
	__ u __ (FinSet[Elem];FinSet[Elem])

op

__ u __:	FinSet[Elem] ×FinSet[Elem] -> FinSet[Elem],
	assoc, comm, idem, unit {}

}

%%

intended system of representatives:

%%

{} and

%%

set(x₁) u ... u set(x_n),

%%

where n > 1, x_i e Elem, x_i =/= x_j for i =/= j, and

%%

x₁ < x₂ < ...< x_n (< is an arbitrary order on Elem)

end

spec

FiniteSet  [Elem with sort Elem] =

GenerateFiniteSet [Elem]

and

Nat

then

preds

__  elemOf __:	Elem ×FinSet[Elem];
__ c __:	FinSet[Elem] ×FinSet[Elem]

ops

__ + __ :	Elem ×FinSet[Elem] -> FinSet[Elem];
__ + __,
__ - __ :	FinSet[Elem] ×Elem -> FinSet[Elem];
__ n __,
__ - __,
__ symmDiff __:	FinSet[Elem] ×FinSet[Elem] -> FinSet[Elem];
#__:	FinSet[Elem] -> Nat;

vars

x,y : Elem; S,T,U,V:FinSet[Elem]

.

%[elemOf_empty] ¬ x  elemOf {}

.

%[elemOf_set] x  elemOf set(y) <=> (x=y)

.

%[elemOf_union] x  elemOf (S u T) <=> (x  elemOf S) \/ (x  elemOf T)

.

%[subset_empty] {} c S

.

%[subset_set] set(x) c S <=> x  elemOf S

.

%[subset_union] (S u T) c U <=> S c U /\ T c U

.

%[FinSet_add_def1] x + S = set(x) u S

.

%[FinSet_add_def2] S + x = x + S

.

%[FinSet_sub_empty] {} - x = {}

.

%[FinSet_sub_set1] set(y) - x = set(y) if ¬ x = y

.

%[FinSet_sub_set2] set(y) - x = {} if x = y

.

%[FinSet_sub_union] (S u T) - x = (S - x) u (T - x)

.

%[intersect_empty] {} n S = {}

.

%[intersect_set1] set(x) n S = {} if ¬ x  elemOf S

.

%[intersect_set2] set(x) n S = set(x) if x  elemOf S

.

%[intersect_union] (S u T) n U = ( S n U ) u (T n U)

.

%[diff_empty] {} - S = {}

.

%[diff_set1] set(x) - S = set(x) if ¬ x  elemOf S

.

%[diff_set2] set(x) - S = {} if x  elemOf S

.

%[diff_union] (S u T) - U = (S - U ) u (T - U)

.

%[symmDiff_def] S symmDiff T = (S - T) u (T - S)

.

%[FinSet_numberOf_empty] #{} = 0

.

%[numberOf_FinSet_set] #set(x) = 1

.

%[numberOf_FinSet_union] #(S u T) = #S + #T

then

%implies

ops

__ n __:	FinSet[Elem] ×FinSet[Elem] -> FinSet[Elem],
	assoc, comm, idem;
__ symmDiff __ :	FinSet[Elem] ×FinSet[Elem] -> FinSet[Elem],
	comm;

vars

x: Elem; S,T: FinSet[Elem]

.

%[subset_characterization]

S c T <=> ( forall x: Elem . x  elemOf S => x  elemOf T )

end

view

PartialOrder_in_FiniteSet  [Elem]:

PartialOrder to FiniteSet [Elem]

=

sort

Elem ^_|-> FinSet[Elem] ,

pred

__ < __ ^_|-> __ c __

end

spec

FinitePowerSet 

[FiniteSet [Elem with sort Elem] then op X: FinSet[Elem]]

=

sorts

FinitePowerSet[X]=	{ Y: FinSet[Elem] . Y c X };
Elem[X] =	{x : Elem . x  elemOf X }

preds

__  elemOf __ :	Elem[X] ×FinitePowerSet[X];
__ c __:	FinitePowerSet[X] ×FinitePowerSet[X]

ops

{}:	FinitePowerSet[X];
set :	Elem[X] -> FinitePowerSet[X];
add:	Elem[X] × FinitePowerSet[X] -> FinitePowerSet[X];
__ u __,
__ n __,
__ - __,
__ symmDiff __:	FinitePowerSet[X] ×FinitePowerSet[X]
	-> FinitePowerSet[X]

%%

These predicates and operations

%%

are determined by overloading.

end

view

DefineBooleanAlgebra_in_FinitePowerSet 

[FiniteSet[Elem with sort Elem] then op X: FinSet[Elem]]

:

DefineBooleanAlgebra to

FinitePowerSet [FiniteSet [Elem with sort Elem] then op X: FinSet[Elem]]

=

sort

Elem ^_|-> FinitePowerSet[X],

ops

0 |-> {},

1 |-> X,

__ |¯| __ |-> __ n __,

__ |_| __ |-> __ u __

end

spec

GenerateList  [Elem with sort Elem] =

free

types

List[Elem]	::=	nil | sort NeList[Elem];
NeList[Elem]	::=	__ :: __ (first : Elem; rest : List[Elem])

op

__ :: __: Elem × List[Elem] -> NeList[Elem] %right assoc

end

spec

List  [Elem with sort Elem]

=

GenerateList[Elem]

and

Nat

then

type

List[Elem]::= nil | __ ::__ (Elem; List[Elem])

%list

[__], nil, __::__

pred

isEmpty: List[Elem]

ops

first, last:	List[Elem] ->? Elem;
first, last:	NeList[Elem] -> Elem;
#__:	List[Elem] -> Nat;
__ + + __ :	List[Elem] × List[Elem] -> List[Elem];
__ + + __ :	NeList[Elem] × List[Elem] -> NeList[Elem];
__ + + __ :	List[Elem] × NeList[Elem] -> NeList[Elem];
reverse:	List[Elem] -> List[Elem];
take,drop:	Nat × List[Elem] ->? List[Elem]

vars

x: Elem; n: Nat; L,K: List[Elem]; N: NeList[Elem]

.

%[isEmpty_def] isEmpty(L) <=> L=nil

.

%[first_partial_nil] ¬ def first(nil)

%%

first: List[Elem] ->? Elem on NeLists is determined by

%%

overloading

.

%[last_partial_nil] ¬ def last(nil)

.

%[last_partial_NeList1] last (x :: L) = x if isEmpty(L)

.

%[last_partial_NeList2] last (x :: L) = last(L) if ¬ isEmpty(L)

.

%[numberOf_List_nil] # nil = 0

.

%[numberOf_List_NeList] # (x :: L) = suc( # L )

.

%[concat_nil_List] nil + + K = K

.

%[concat_NeList_List] (x::L) + + K = x :: (L + + K)

.

%[reverse_nil] reverse(nil)=nil

.

%[reverse_NeList] reverse(x::L) = reverse(L) + + (x::nil)

.

%[take_def]

take (n,L) = K <=> exists S: List[Elem] . K + + S = L /\ # K = n

.

%[drop_def]

drop (n,L) = K <=> exists S: List[Elem] . S + + K = L /\ # S = n

then

%implies

vars

x: Elem; n: Nat; L: List[Elem]; N: NeList[Elem]

.

%[first_domain] def first(L) <=> ¬ isEmpty(L)

.

%[last_total_nil] last (x :: nil) = x

.

%[last_total_NeList] last (x :: N) = last(N)

.

%[last_domain] def last(L) <=> ¬ isEmpty(L)

.

%[take_dom] def take(n,L) <=> # L > n

.

%[drop_dom] def drop(n,L) <=> # L > n

end

view

Monoid_in_List  [Elem]:

Monoid to List [Elem]

=

sort

Elem ^_|-> List[Elem],

ops

0 |-> Nil,

__+__ |-> __ + + __

end

spec

String =

List [Char]

with

sorts	List[Char] |-> String,
	NeList[Char] |-> NonEmptyString

then

%string nil, __::__

end

spec

GenerateBag  [Elem with sort Elem]

=

Nat

and

List[Elem]

then

op

count : Elem × List[Elem] -> Nat

vars

x,y:Elem; L: List[Elem]

.

%[frequency_List_nil] count (x,nil) = 0

.

%[frequency_NeList_def1] count (x, y::L) = count (x, L) if ¬ x=y

.

%[frequency_NeList_def2] count (x, y::L) = suc(count (x, L)) if x=y

then

free

{

type

Bag[Elem] ::= quotient(List[Elem])

vars

K,L: List[Elem]

.

%[quotient_def]

quotient(K)=quotient(L) <=> forall x: Elem . count(x,K) = count(x,L)

}

%%

intended system of representatives:

%%

functions B: Elem -> Nat,

%%

where B(x)>0 for finitely many x. Any such function B

%%

represents a set of lists L

%%

with count(x,L)=B(x) for all x e Elem.

end

spec

Bag [Elem with sort Elem] =

GenerateBag[Elem]

then

preds

__ elemOf __:	Elem ×Bag[Elem];
__ c __:	Bag[Elem] ×Bag[Elem]

ops

empty:	Bag[Elem];
count :	Elem × Bag[Elem] -> Nat;
__ + __ :	Elem × Bag[Elem] -> Bag[Elem];
__ + __, __- __:	Bag[Elem] × Elem -> Bag[Elem];
__ u __, __ n __:	Bag[Elem] ×Bag[Elem] -> Bag[Elem]

type

Bag[Elem]::= empty | __ + __(Elem; Bag[Elem])

%list

[{ __ }], empty , __+__

axiom

%[empty_Bag_def] empty = quotient(nil)

vars

x: Elem; B,C,D: Bag[Elem]; L: List[Elem]

.

%[frequency_Bag] count(x,quotient(L)) = count(x,L)

.

%[elemOf_Bag] x elemOf B <=> count(x,B) > 0

.

%[add_Bag_def1]

x + B = C <=>

(forall y: Elem . (¬ y = x => count (y,B) = count(y,C)) /\ ( y = x => count (y,B)+1 = count(y,C)) )

.

%[add_Bag_def2] B + x = x + B

.

%[sub_Bag_def1] B - x = B if count(x,B) = 0

.

%[sub_Bag_def2]

( B - x = C <=>

(forall y: Elem . (¬ y = x => count (y,B) = count(y,C)) /\ ( y = x => count (y,B)-1 = count (y,C)))

) if count(x,B)>0

.

%[subseteq_Bag] B c C <=> forall x: Elem . count(x,B) < count(x,C)

.

%[cup_Bag] B u C = D <=> forall x: Elem . count(x,D) = count(x,B) + count(x,C)

.

%[cap_Bag] B n C = D <=> forall x: Elem . count(x,D) = min ( count(x,B), count(x,C) )

end

view

PartialOrder_in_Bag  [Elem]:

PartialOrder to Bag[Elem]

=

sort

Elem ^_|-> Bag[Elem],

pred

__ < __ ^_|-> __ c __

end

spec

Pair  [sort S] [sort T] =

free

type Pair[S,T] ::= pair(first:S; second:T)

end

spec

FiniteMap  [sort S] [sort T] =

FiniteSet

[Pair [sort S] [sort T] with

sorts	Pair[S,T],
ops	pair, first, second

fit sort Elem ^_|-> Pair[S,T]

]

then

 

sort

FiniteMap = {	F : FinSet[Pair[S,T]] . forall g,h: Pair[S,T] .
	(g elemOf F /\ h elemOf F /\ first(g)=first(h))
	=> second(g)=second(h) }

preds

isEmpty:	FiniteMap;
__elemOf__:	Pair[S,T] × FiniteMap;
__canBeAddedTo __:	Pair[S,T] × FiniteMap;

%%

elemOf is determined by overloading

ops

emptyMap:	FiniteMap;
add:	Pair[S,T] × FiniteMap ->? FiniteMap;
remove:	Pair[S,T] × FiniteMap -> FiniteMap;
evaluate:	S × FiniteMap ->? T;

axiom

%[emptyMap_def

] emptyMap = {} as FiniteMap

vars

p:Pair[S,T]; F: FiniteMap; s:S; t: T

.

%[isEmpty_def] isEmpty(F) <=> F=emptyMap

.

%[add_FiniteMap_def] add(p,F) = F u set(p) as FiniteMap

.

%[canBeAddedTo_def] p canBeAddedTo F <=> def add(p,F)

.

%[remove_def] remove(p,F) = (F - p) as FiniteMap

.

%[evaluate_def] evaluate(s,F) = t <=> pair(s,t) elemOf F

then

%implies

vars

p: Pair[S,T]; F: FiniteMap; s: S

.

%[add_FiniteMap_domain]

defadd(p,F) <=> forall q : Pair[S,T] .

(q elemOf F /\ first(p)=first(q)) => second(p)=second(q)

.

%[evaluate_domain]

defevaluate(s,F) <=> exists t:T . pair(s,t) elemOf F

end

spec

Array 

[ops min, max: Int axiom %[Cond_nonEmptyIndex] min < max]

[Elem with sort Elem]

given Int

=

sort

Index = { i : Int . min < i /\ i < max }

then

{

FiniteMap [sort Index] [Elem]

reveal sort FiniteMap |-> Array[Elem], preds isEmpty, __elemOf__, __canBeAddedTo __, ops emptyMap |-> emptyArray, add, remove, evaluate, pair

then

ops

init:	Array[Elem] -> Array[Elem];
__!__:	Array[Elem] × Index ->? Elem;
__!__:=__ :	Array[Elem] × Index × Elem -> Array[Elem];

vars

A: Array[Elem]; i: Index; e: Elem

.

%[init_Array_def] init(A)=emptyArray

.

%[evaluate_Array_def] A!i = evaluate(i,A)

.

%[assignment_Array_def] A!i:=e =
add(pair(i,e),remove(pair(i,A!i),A))

}

reveal

sort	Array[Elem],
ops	emptyArray, init, __!__, __!__:=__

then

%implies

vars

A: Array[Elem]; i,j: Index; e,f: Elem

.

%[evaluate_Array_domain1] ¬ def init(A)!i

.

%[evaluate_Array_domain2] def (A!i:=e)!i

.

%[evaluate_Array_assignment1] (A!i:=e)!j = e if i=j

.

%[evaluate_Array_assignment2] (A!i:=e)!j = A!j if ¬ (i=j)

end