|
bags [T: TYPE] : THEORY
%------------------------------------------------------------------------
%
% Fundamental definitions and properties of bags.
%
% Authors: Rick Butler NASA Langley
% Lee Pike NASA Langley
%------------------------------------------------------------------------
BEGIN
x,y,t: VAR T
bag: TYPE = [T -> nat]
a,b,c: VAR bag
n: VAR nat
count(x,b): nat = b(x)
emptybag : bag = (LAMBDA t: 0)
singleton_bag(t) : bag = (LAMBDA (x: T): IF x = t THEN 1 ELSE 0 ENDIF)
insert(x,b) : bag = (LAMBDA t: IF x = t THEN b(t) + 1 ELSE b(t) ENDIF)
purge(x,b) : bag = (LAMBDA t: IF x = t THEN 0 ELSE b(t) ENDIF)
delete(x,b,n) : bag = (LAMBDA t: IF x = t THEN
IF b(t) >= n THEN b(t) - n ELSE 0 ENDIF
ELSE b(t) ENDIF)
extract(x,b) : bag = (LAMBDA t: IF x = t THEN b(t) ELSE 0 ENDIF)
plus(a,b) : bag = (LAMBDA t: a(t) + b(t))
union(a,b) : bag = (LAMBDA t: max(a(t),b(t)))
intersection(a,b): bag = (LAMBDA t: min(a(t),b(t)))
% --------- some predicates over bags ------------
member(x,b) : bool = b(x) > 0
empty?(b) : bool = (FORALL x: b(x) = 0)
nonempty_bag?(b) : bool = NOT empty?(b)
eqmult(x,a,b) : bool = (a(x) = b(x))
subbag?(a,b) : bool = (FORALL x: a(x) <= b(x))
proper_subbag?(a,b): bool = (FORALL x: a(x) < b(x))
disjoint?(a, b) : bool = empty?(intersection(a, b))
% ---------- useful lemmas ----------
emptybag_is_empty? : LEMMA empty?(b) IFF b = emptybag
delete_purge : LEMMA n >= b(x) IMPLIES delete(x,b,n) = purge(x,b)
insert_unique : LEMMA insert(x,a) = insert(x,b) IMPLIES a = b
insert_exchange : LEMMA insert(x,insert(y,b)) = insert(y,insert(x,b))
delete_insert : LEMMA n > 0 IMPLIES
(delete(x,insert(x,b),n) = delete(x,b,n-1))
insert_delete : LEMMA b(x) > 0 IMPLIES insert(x,delete(x,b,1)) = b
delete_insert_diff : LEMMA x /= y IMPLIES
(delete(x,insert(y,b),n) = insert(y,delete(x,b,n)))
decomposition : LEMMA NOT empty?(b) IMPLIES
(EXISTS a,x: b = insert(x,a))
bag_equality : LEMMA a = b IFF (FORALL x: eqmult(x,a,b))
subbag_empty : LEMMA subbag?(emptybag,a)
subbag_equality : LEMMA a = b IFF subbag?(a,b) AND subbag?(b,a)
subbag_trans : LEMMA subbag?(a,b) AND subbag?(b,c) IMPLIES subbag?(a,c)
% because of empty types the following is not provable -- look into it later
% proper_subbag_rew : LEMMA proper_subbag?(a,b) IMPLIES subbag?(a,b) AND a /= b
bag_plus_union : LEMMA plus(union(a,b),intersection(a,b)) = plus(a,b)
bag_plus_comm : LEMMA plus(a,b) = plus(b,a)
plus_emptybag : LEMMA plus(emptybag,a) = a
bag_plus_insert : LEMMA plus(insert(x,a),b) = insert(x,plus(a,b))
bag_distributive : LEMMA intersection(a,union(b,c)) =
union(intersection(a,b),intersection(a,c))
extract_subbag : LEMMA subbag?(extract(x,a), a)
extract_disj : LEMMA x /= y IMPLIES disjoint?(extract(x,a), extract(y,a))
bag_disj_comm : LEMMA disjoint?(a,b) = disjoint?(b,a)
bag_union_comm : LEMMA union(a,b) = union(b,a)
bag_union_fix_pt : LEMMA union(a,a) = a
bag_purge_extract : LEMMA a = union(purge(x,a), extract(x,a))
bag_disj_extract_perge : LEMMA disjoint?(extract(x,a), purge(x,a))
bag_extract_union_subbag: LEMMA x /= y IMPLIES subbag?(union(extract(x,a),extract(y,a)),a)
union_upper_bound : LEMMA subbag?(a, c) and subbag?(b, c) IMPLIES
subbag?(union(a, b), c)
END bags
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
