FDL > PVS > Finite Sets > finite_sets : Theory

PVS-2.4 finite sets/finite sets.pvs

finite_sets [T:TYPE] : THEORY
BEGIN

IMPORTING card def[T]

A: VAR finite set

B: VAR finite set

S: VAR finite set

x: VAR T

n: VAR nat

card emptyset: THEOREM card(emptyset[T]) = 0

empty card: THEOREM empty?(S) IFF (card(S) = 0)

card empty?: THEOREM card(S) = 0 = empty?(S)

card is 0: THEOREM card(S) = 0 = (S = emptyset)

nonempty card: THEOREM nonempty?(S) IFF (card(S) > 0)

card singleton: THEOREM card(singleton(x)) = 1

card one: THEOREM (card(S) = 1) IFF (EXISTS x : S = singleton(x))

card disj union: THEOREM disjoint?(A, B) IMPLIES (card(union(A, B)) = (card(A) + card(B)))

card diff subset: THEOREM subset?(A, B) IMPLIES (card(difference(B, A)) = (card(B) - card(A)))

card subset: THEOREM subset?(A, B) IMPLIES (card(A) < = card(B))

card plus: THEOREM (card(A) + card(B)) = (card(union(A, B)) + card(intersection(A, B)))

card union: THEOREM card(union(A, B)) = ((card(A) + card(B)) - card(intersection(A, B)))

card add: THEOREM card(add(x, S)) = (card(S) + IF S(x) THEN 0 ELSE 1 ENDIF)

card remove: THEOREM card(remove(x, S)) = (card(S) - IF S(x) THEN 1 ELSE 0 ENDIF)

card rest: THEOREM (NOT empty?(S)) IMPLIES (card(rest(S)) = (card(S) - 1))

same card subset: THEOREM (subset?(A, B) AND (card(A) = card(B))) IMPLIES (A = B)

smaller card subset: THEOREM (subset?(A, B) AND (card(A) < card(B))) IMPLIES (EXISTS x : member(x, B) AND (NOT member(x, A)))

card 1 has 1: THEOREM (card(S) > = 1) IMPLIES (EXISTS (x:T) : S(x))

card 2 has 2: THEOREM (card(S) > = 2) IMPLIES (EXISTS (x:T), (y:T) : (x /= y) AND S(x) AND S(y))

card intersection le: THEOREM (card(intersection(A, B)) < = card(A)) AND (card(intersection(A, B)) < = card(B))

N: VAR nat

card bij: THEOREM (card(S) = N) IFF (EXISTS (f:[(S) - > below[N]]) : bijective?(f))

bij exists: COROLLARY EXISTS (f:[(S) - > below(card(S))]) : bijective?(f)

END finite_sets