FDL > PVS > Prelude > sets_lemmas : Theory

PVS-2.4 prelude.pvs

 Lemmas about sets - many of these came from Bruno Dutertre in the
 more_set_lemmas theory of the finite_sets library

sets_lemmas [T:TYPE] : THEORY
BEGIN

a: VAR set[T]

b: VAR set[T]

c: VAR set[T]

x: VAR T

y: VAR T

extensionality: LEMMA (FORALL x : member(x, a) IFF member(x, b)) IMPLIES (a = b)

emptyset is empty?: LEMMA empty?(a) IFF (a = emptyset)

empty no members: LEMMA NOT member(x, emptyset)

emptyset min: LEMMA subset?(a, emptyset) IMPLIES (a = emptyset)

nonempty member: LEMMA nonempty?(a) IFF (EXISTS x : member(x, a))

fullset member: LEMMA member(x, fullset)

fullset max: LEMMA subset?(fullset, a) IMPLIES (a = fullset)

nonempty exists: LEMMA nonempty?(a) IFF (EXISTS (x:(a) ) : TRUE)

subset reflexive: LEMMA subset?(a, a)

subset antisymmetric: LEMMA (subset?(a, b) AND subset?(b, a)) IMPLIES (a = b)

subset transitive: LEMMA (subset?(a, b) AND subset?(b, c)) IMPLIES subset?(a, c)

subset partial order: LEMMA partial order?(subset?[T])

subset emptyset: LEMMA subset?(emptyset, a)

subset fullset: LEMMA subset?(a, fullset)

union idempotent: LEMMA union(a, a) = a

union commutative: LEMMA union(a, b) = union(b, a)

union associative: LEMMA union(union(a, b), c) = union(a, union(b, c))

union empty: LEMMA union(a, emptyset) = a

union full: LEMMA union(a, fullset) = fullset

union subset1: LEMMA subset?(a, union(a, b))

union subset2: LEMMA subset?(a, b) IMPLIES (union(a, b) = b)

union upper bound: LEMMA (subset?(a, c) AND subset?(b, c)) IMPLIES subset?(union(a, b), c)

union difference: LEMMA union(a, b) = union(a, difference(b, a))

union diff subset: LEMMA subset?(a, b) IMPLIES (union(a, difference(b, a)) = b)

intersection idempotent: LEMMA intersection(a, a) = a

intersection commutative: LEMMA intersection(a, b) = intersection(b, a)

intersection associative: LEMMA intersection(intersection(a, b), c) = intersection(a, intersection(b, c))

intersection empty: LEMMA intersection(a, emptyset) = emptyset

intersection full: LEMMA intersection(a, fullset) = a

intersection subset1: LEMMA subset?(intersection(a, b), a)

intersection subset2: LEMMA subset?(a, b) IMPLIES (intersection(a, b) = a)

intersection lower bound: LEMMA (subset?(c, a) AND subset?(c, b)) IMPLIES subset?(c, intersection(a, b))

distribute intersection union: LEMMA intersection(a, union(b, c)) = union(intersection(a, b), intersection(a, c))

distribute union intersection: LEMMA union(a, intersection(b, c)) = intersection(union(a, b), union(a, c))

complement emptyset: LEMMA complement(emptyset[T]) = fullset

complement fullset: LEMMA complement(fullset[T]) = emptyset

complement complement: LEMMA complement(complement(a)) = a

subset complement: LEMMA subset?(complement(a), complement(b)) IFF subset?(b, a)

demorgan1: LEMMA complement(union(a, b)) = intersection(complement(a), complement(b))

demorgan2: LEMMA complement(intersection(a, b)) = union(complement(a), complement(b))

difference emptyset1: LEMMA difference(a, emptyset) = a

difference emptyset2: LEMMA difference(emptyset, a) = emptyset

difference fullset1: LEMMA difference(a, fullset) = emptyset

difference fullset2: LEMMA difference(fullset, a) = complement(a)

difference intersection: LEMMA difference(a, b) = intersection(a, complement(b))

difference difference1: LEMMA difference(difference(a, b), c) = difference(a, union(b, c))

difference difference2: LEMMA difference(a, difference(b, c)) = union(difference(a, b), intersection(a, c))

difference subset: LEMMA subset?(difference(a, b), a)

difference disjoint: LEMMA disjoint?(a, difference(b, a))

diff union inter: LEMMA difference(union(a, b), a) = difference(b, intersection(a, b))

nonempty add: LEMMA NOT empty?(add(x, a))

member add: LEMMA member(x, a) IMPLIES (add(x, a) = a)

member remove: LEMMA (NOT member(x, a)) IMPLIES (remove(x, a) = a)

add remove member: LEMMA member(x, a) IMPLIES (add(x, remove(x, a)) = a)

remove add member: LEMMA (NOT member(x, a)) IMPLIES (remove(x, add(x, a)) = a)

subset add: LEMMA subset?(a, add(x, a))

add as union: LEMMA add(x, a) = union(a, singleton(x))

singleton as add: LEMMA singleton(x) = add(x, emptyset)

subset remove: LEMMA subset?(remove(x, a), a)

remove as difference: LEMMA remove(x, a) = difference(a, singleton(x))

remove member singleton: LEMMA remove(x, singleton(x)) = emptyset

%%(TCC) choose_rest_TCC1: OBLIGATION

choose rest: LEMMA (NOT empty?(a)) IMPLIES (add(choose(a), rest(a)) = a)

choose member: LEMMA (NOT empty?(a)) IMPLIES member(choose(a), a)

choose not member: LEMMA (NOT empty?(a)) IMPLIES (NOT member(choose(a), rest(a)))

rest not equal: LEMMA (NOT empty?(a)) IMPLIES (rest(a) /= a)

rest member: LEMMA member(x, rest(a)) IMPLIES member(x, a)

rest subset: LEMMA subset?(rest(a), a)

choose add: LEMMA (choose(add(x, a)) = x) OR member(choose(add(x, a)), a)

%%(TCC) choose_rest_or_TCC1: OBLIGATION

choose rest or: LEMMA member(x, a) IMPLIES (member(x, rest(a)) OR (x = choose(a)))

%%(TCC) choose_singleton_TCC1: OBLIGATION

choose singleton: LEMMA choose(singleton(x)) = x

rest singleton: LEMMA rest(singleton(x)) = emptyset[T]

singleton subset: LEMMA member(x, a) IFF subset?(singleton(x), a)

rest empty lem: LEMMA ((NOT empty?(a)) AND empty?(rest(a))) IMPLIES (a = singleton(choose(a)))

singleton disjoint: LEMMA (NOT member(x, a)) IMPLIES disjoint?(singleton(x), a)

disjoint remove left: LEMMA disjoint?(a, b) IMPLIES disjoint?(remove(x, a), b)

disjoint remove right: LEMMA disjoint?(a, b) IMPLIES disjoint?(a, remove(x, b))

union disj remove left: LEMMA (disjoint?(a, b) AND a(x)) IMPLIES (union(remove(x, a), b) = remove(x, union(a, b)))

union disj remove right: LEMMA (disjoint?(a, b) AND b(x)) IMPLIES (union(a, remove(x, b)) = remove(x, union(a, b)))

END sets_lemmas