|
finite_bags[T: TYPE]: THEORY
%------------------------------------------------------------------------
%
% This theory defines finite bags and its cardinality
%
% Authors: Rick Butler (NASA Langley)
% David.Griffioen (CWI Amsterdam and KUN)
% Lee Pike (NASA Langley)
%------------------------------------------------------------------------
BEGIN
IMPORTING bags[T],
finite_sets@finite_sets_sum_real[T],
finite_sets@finite_sets_inductions[T], bags_to_sets[T]
x,y,t,e: VAR T
b: VAR bag
n,xn: VAR nat
%% bag_to_set(b): set[T] = {t: T | b(t) > 0}
is_finite(b): bool = is_finite(bag_to_set(b))
finite_bag: TYPE = {b: bag | is_finite(b)}
nonempty_finite_bag: TYPE = {b: finite_bag | NOT empty?(b)}
A,B,C: VAR finite_bag
JUDGEMENT bag_to_set(B) HAS_TYPE finite_set
% The card_TCC1: OBLIGATION relies on a JUDGEMENT in finite_sets_sum_real
% that is no longer firing. Since it is unnamed it is difficult to fix it.
card(B): nat = sum(bag_to_set(B),(LAMBDA t: B(t)))
finite_bag : THEOREM is_finite(B) IMPLIES is_finite(LAMBDA x: B(x) > 0)
finite_emptybag : THEOREM is_finite(emptybag[T]);
finite_singleton_bag: THEOREM is_finite(singleton_bag(t))
finite_insert : THEOREM is_finite(insert(t, B))
finite_purge : THEOREM is_finite(purge(t, B))
finite_delete : THEOREM is_finite(delete[T](t, B, n))
finite_bag_union : THEOREM is_finite(union(A, B))
finite_bag_intersection: THEOREM is_finite(intersection[T](A, B))
finite_bag_plus : LEMMA is_finite(plus(A,B))
finite_update : LEMMA is_finite(B WITH [x := xn])
finite_set : THEOREM is_finite(bag_to_set(A))
finite_extract : THEOREM is_finite(extract(x,B))
JUDGEMENT nonempty_finite_bag SUBTYPE_OF (nonempty_bag?[T])
JUDGEMENT singleton_bag(x) HAS_TYPE finite_bag
JUDGEMENT union(A,B), intersection(A,B), plus(A,B)
HAS_TYPE finite_bag
NA,NB: VAR nonempty_finite_bag
JUDGEMENT union(A,NB), plus(A,NB) HAS_TYPE nonempty_finite_bag
JUDGEMENT union(NA,B), plus(NA,B) HAS_TYPE nonempty_finite_bag
JUDGEMENT insert(x,A) HAS_TYPE nonempty_finite_bag
JUDGEMENT purge(x,A) HAS_TYPE finite_bag
JUDGEMENT delete(x,A,n) HAS_TYPE finite_bag
JUDGEMENT emptybag HAS_TYPE finite_bag
JUDGEMENT extract(x,A) HAS_TYPE finite_bag
% ---------- Some Useful Lemmas ----------
card_emptybag : THEOREM card(emptybag[T]) = 0
card_bag_empty? : THEOREM (card(B) = 0) = empty?(B)
card_singleton_bag : THEOREM card(singleton_bag(t)) = 1
card_subbag? : THEOREM subbag?(A,B) IMPLIES card(A) <= card(B)
card_bag_particular: THEOREM card(B WITH [x := xn]) = card(B) - B(x) + xn
card_bag_delete : LEMMA card(delete(e,B,n)) = card(B) - min(B(e),n)
card_bag_insert : LEMMA card(insert(x,B)) = card(B) + 1
card_nonempty_bag? : LEMMA card(B) > 0 IFF nonempty_bag?(B)
card_disj_intersection : LEMMA disjoint?(A,B) IMPLIES
card(intersection(A,B)) = 0
sum_bag_disj_union : LEMMA disjoint?(A,B) IMPLIES
sum(bag_to_set(A),(LAMBDA (t:T): union(A,B)(t)))
= sum(bag_to_set(A), (LAMBDA (t:T): A(t)))
card_extract : LEMMA card(extract(x,A)) <= card(A)
card_extract_bag : LEMMA card(extract(x,A)) = A(x)
card_disjoint_add : LEMMA disjoint?(A,B) IMPLIES
card(union(A,B)) = card(A) + card(B)
card_purge_extract : LEMMA card(purge(x,A)) = card(A) - card(extract(x,A))
card_union_extract_add : LEMMA x /= y IMPLIES
card(union(extract(x,A),extract(y,A))) = A(x) + A(y)
card_union_extract : LEMMA x /= y IMPLIES
card(union(extract(x,A),extract(y,A))) <= card(A)
card_geq_count : LEMMA A(x) <= card(A)
card_geq_count_add : LEMMA x /= y IMPLIES A(x) + A(y) <= card(A)
END finite_bags
¤ 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.
|
