%-------------------------------------------------------------------------
%
% Set cardinality. This theory operates on both finite and infinite
% sets. This theory produces and compares cardinals only for sets of a
% given type. There is no facility for comparing cardinals of sets of
% different types. I do not intend to rectify that omission.
%
% For PVS version 3.2. March 8, 2005
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), University of Kansas
%
% EXPORTS
% -------
% prelude: finite_sets[T], QuotientDefinition[set[T]]
% sets_aux: card_comp_set[T,T], card_comp_set_props[T,T],
% card_comp_set_transitive[T,T,T], card_finite[T,T], card_single[T],
% cardinal[T]
%
%-------------------------------------------------------------------------
cardinal[T: TYPE]: THEORY
BEGIN
IMPORTING QuotientDefinition[set[T]], card_finite[T, T], card_single[T]
R, S: VAR set[T]
% A cardinal number is a maximal set of bijective sets. We form the
% cardinal numbers from the quotient of the card_eq relation.
cardinal_number: TYPE = Quotient(card_eq)
A, B, C: VAR cardinal_number
cardinal(S): cardinal_number = quotient_map(card_eq)(S)
cardinal_member: LEMMA FORALL S: cardinal(S)(S)
cardinal_closed: LEMMA FORALL A, (S: (A)): A = cardinal(S)
cardinal_empty: LEMMA cardinal(emptyset[T]) = singleton(emptyset[T])
cardinal_finite: LEMMA
FORALL (S: finite_set[T]), (R: (cardinal(S))): is_finite(R)
cardinal_finite_card: LEMMA
FORALL (S: finite_set[T]), (R: (cardinal(S))): card(R) = card(S);
% ==========================================================================
% Comparing cardinal numbers
% ==========================================================================
<(A, B): bool = card_lt(rep(card_eq)(A), rep(card_eq)(B));
<=(A, B): bool = card_le(rep(card_eq)(A), rep(card_eq)(B));
>=(A, B): bool = card_ge(rep(card_eq)(A), rep(card_eq)(B));
>(A, B): bool = card_gt(rep(card_eq)(A), rep(card_eq)(B));
% We don't need to define an analogous = operator
cardinal_equality: LEMMA
FORALL A, B: card_eq(rep(card_eq)(A), rep(card_eq)(B)) IFF A = B
% Alternative way of expressing cardinality (in)equalities
cardinal_lt: LEMMA
FORALL A, B: A < B IFF (FORALL (S: (A)), (R: (B)): card_lt(S, R))
cardinal_le: LEMMA
FORALL A, B: A <= B IFF (FORALL (S: (A)), (R: (B)): card_le(S, R))
cardinal_eq: LEMMA
FORALL A, B: A = B IFF (FORALL (S: (A)), (R: (B)): card_eq(S, R))
cardinal_ge: LEMMA
FORALL A, B: A >= B IFF (FORALL (S: (A)), (R: (B)): card_ge(S, R))
cardinal_gt: LEMMA
FORALL A, B: A > B IFF (FORALL (S: (A)), (R: (B)): card_gt(S, R))
% ==========================================================================
% Relationship between the card_comp operators and cardinal (in)equalities
% ==========================================================================
cardinal_card_lt: LEMMA
FORALL R, S: card_lt(R, S) IFF cardinal(R) < cardinal(S)
cardinal_card_le: LEMMA
FORALL R, S: card_le(R, S) IFF cardinal(R) <= cardinal(S)
cardinal_card_eq: LEMMA
FORALL R, S: card_eq(R, S) IFF cardinal(R) = cardinal(S)
cardinal_card_ge: LEMMA
FORALL R, S: card_ge(R, S) IFF cardinal(R) >= cardinal(S)
cardinal_card_gt: LEMMA
FORALL R, S: card_gt(R, S) IFF cardinal(R) > cardinal(S)
% ==========================================================================
% Relationship between the cardinal (in)equalities
% ==========================================================================
cardinal_lt_gt: LEMMA FORALL A, B: A < B IFF B > A
cardinal_le_ge: LEMMA FORALL A, B: A <= B IFF B >= A
cardinal_lt_le: LEMMA FORALL A, B: A < B IFF A <= B AND NOT A = B
cardinal_le_lt: LEMMA FORALL A, B: A <= B IFF A < B OR A = B
cardinal_eq_lg: LEMMA FORALL A, B: A = B IFF A <= B AND A >= B
cardinal_ge_gt: LEMMA FORALL A, B: A >= B IFF A > B OR A = B
cardinal_gt_ge: LEMMA FORALL A, B: A > B IFF A >= B AND NOT A = B
cardinal_lt_not_ge: LEMMA FORALL A, B: A < B IFF NOT A >= B
cardinal_le_not_gt: LEMMA FORALL A, B: A <= B IFF NOT A > B
cardinal_eq_not_lg: LEMMA FORALL A, B: A = B IFF NOT (A < B OR A > B)
cardinal_ge_not_lt: LEMMA FORALL A, B: A >= B IFF NOT A < B
cardinal_gt_not_le: LEMMA FORALL A, B: A > B IFF NOT A <= B
% ==========================================================================
% Order properties of the cardinal (in)equalities
% ==========================================================================
cardinal_lt_strict_total_order: JUDGEMENT
< HAS_TYPE (strict_total_order?[cardinal_number])
cardinal_le_total_order: JUDGEMENT
<= HAS_TYPE (total_order?[cardinal_number])
% This is already known:
% cardinal_eq_equivalence: JUDGEMENT = HAS_TYPE equivalence[cardinal_number]
cardinal_ge_total_order: JUDGEMENT
>= HAS_TYPE (total_order?[cardinal_number])
cardinal_gt_strict_total_order: JUDGEMENT
> HAS_TYPE (strict_total_order?[cardinal_number])
% ==========================================================================
% Transitivity properties of the cardinal (in)equalities
% ==========================================================================
cardinal_lt_le_transitive: LEMMA
FORALL A, B, C: A < B AND B <= C IMPLIES A < C
cardinal_le_lt_transitive: LEMMA
FORALL A, B, C: A <= B AND B < C IMPLIES A < C
cardinal_ge_gt_transitive: LEMMA
FORALL A, B, C: A >= B AND B > C IMPLIES A > C
cardinal_gt_ge_transitive: LEMMA
FORALL A, B, C: A > B AND B >= C IMPLIES A > C
% ==========================================================================
% Least/greatest elements
% ==========================================================================
cardinal_empty_least: LEMMA FORALL A: cardinal(emptyset[T]) <= A
cardinal_full_greatest: LEMMA FORALL A: A <= cardinal(fullset[T])
END cardinal
¤ Dauer der Verarbeitung: 0.19 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.
|
