|
bags_to_sets [T:TYPE]: THEORY
%------------------------------------------------------------------------
%
% This theory defines a function bag_to_set that collapses a bag
% to a set eliminating the count.
%
% Authors: Rick Butler (NASA Langley)
% David Griffioen (CWI Amsterdam and KUN)
% Lee Pike (NASA Langley)
%------------------------------------------------------------------------
BEGIN
IMPORTING bags[T]
t: VAR T
A,B,b: VAR bag
bag_to_set(b): set[T] = {t: T | b(t) > 0}
strict_subbag?(A,B): bool = strict_subset?(bag_to_set(A), bag_to_set(B))
insert_bag_lem : LEMMA bag_to_set(insert(t, B)) = add(t,bag_to_set(B))
purge_bag_lem : LEMMA bag_to_set(purge(t, B)) = remove(t,bag_to_set(B))
bag_union_lem : LEMMA bag_to_set(union(A, B)) =
union(bag_to_set(A), bag_to_set(B))
bag_intersection_lem : LEMMA bag_to_set(intersection(A,B)) =
intersection(bag_to_set(A),bag_to_set(B))
subbag_lem : LEMMA subbag?(A,B) IMPLIES
subset?(bag_to_set(A),bag_to_set(B))
bag_to_set_emptybag : LEMMA bag_to_set(emptybag) = emptyset
empty_bts_bag : LEMMA empty?(bag_to_set(b)) IMPLIES empty?(b)
bag_intersection_commutative: LEMMA intersection(A,B) = intersection(B, A)
bag_union_commutative: LEMMA union(A,B) = union(B, A)
bag_plus_lem : LEMMA bag_to_set(plus(A,B)) =
union(bag_to_set(A),bag_to_set(B))
extract_empty_or_singlton_set:
LEMMA singleton?(bag_to_set(extract(t,A))) OR
empty?(bag_to_set(extract(t,A)))
extract_singleton : LEMMA singleton?(bag_to_set(extract(t,A))) IMPLIES
singleton(t) = bag_to_set(extract(t,A))
bag_disj_set : LEMMA disjoint?(A,B) IMPLIES disjoint?(bag_to_set(A),bag_to_set(B))
bag_set_dist_union : LEMMA bag_to_set(union(A,B)) = union(bag_to_set(A),bag_to_set(B))
bag_non_empty : LEMMA NOT empty?(A) IMPLIES nonempty?(bag_to_set(A))
END bags_to_sets
¤ Dauer der Verarbeitung: 0.14 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.
|
