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], VAR TVAR bagVAR nat%% bag_to_set(b): set[T] = {t: T | b(t) > 0} TYPE = {b: bag | is_finite(b)}TYPE = {b: finite_bag | NOT empty?(b)}VAR finite_bagJUDGEMENT 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. LAMBDA t: B(t)))THEOREM is_finite(B) IMPLIES is_finite(LAMBDA x: B(x) > 0)THEOREM is_finite(emptybag[T]);THEOREM is_finite(singleton_bag(t))THEOREM is_finite(insert(t, B))THEOREM is_finite(purge(t, B))THEOREM is_finite(delete[T](t, B, n))THEOREM is_finite(union(A, B))THEOREM is_finite(intersection[T](A, B))LEMMA is_finite(plus(A,B)) LEMMA is_finite(B WITH [x := xn])THEOREM is_finite(bag_to_set(A))THEOREM is_finite(extract(x,B)) JUDGEMENT nonempty_finite_bag SUBTYPE_OF (nonempty_bag?[T])JUDGEMENT singleton_bag(x) HAS_TYPE finite_bagJUDGEMENT union(A,B), intersection(A,B), plus(A,B) VAR nonempty_finite_bagJUDGEMENT union(A,NB), plus(A,NB) HAS_TYPE nonempty_finite_bagJUDGEMENT union(NA,B), plus(NA,B) HAS_TYPE nonempty_finite_bagJUDGEMENT insert(x,A) HAS_TYPE nonempty_finite_bagJUDGEMENT purge(x,A) HAS_TYPE finite_bagJUDGEMENT delete(x,A,n) HAS_TYPE finite_bagJUDGEMENT emptybag HAS_TYPE finite_bagJUDGEMENT extract(x,A) HAS_TYPE finite_bag % ---------- Some Useful Lemmas ---------- THEOREM card(emptybag[T]) = 0THEOREM (card(B) = 0) = empty?(B)THEOREM card(singleton_bag(t)) = 1THEOREM subbag?(A,B) IMPLIES card(A) <= card(B)THEOREM card(B WITH [x := xn]) = card(B) - B(x) + xn LEMMA card(delete(e,B,n)) = card(B) - min(B(e),n)LEMMA card(insert(x,B)) = card(B) + 1LEMMA card(B) > 0 IFF nonempty_bag?(B)LEMMA disjoint?(A,B) IMPLIES LEMMA disjoint?(A,B) IMPLIES LAMBDA (t:T): union(A,B)(t)))LAMBDA (t:T): A(t)))LEMMA card(extract(x,A)) <= card(A)LEMMA card(extract(x,A)) = A(x)LEMMA disjoint?(A,B) IMPLIES LEMMA card(purge(x,A)) = card(A) - card(extract(x,A))LEMMA x /= y IMPLIES LEMMA x /= y IMPLIES LEMMA A(x) <= card(A) LEMMA x /= y IMPLIES A(x) + A(y) <= card(A)END finite_bagsquality 89%
¤ Dauer der Verarbeitung: 0.10 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
