Quelle cardinal.pvs Sprache: PVS

%-------------------------------------------------------------------------
%
% 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 (jamesj@acm.org), 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 A

 cardinal_le_ge: LEMMA FORALL A, B: A <= B IFF B >= A

 cardinal_lt_le: LEMMA FORALL A, B: 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

 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)

 cardinal_ge_not_lt: LEMMA FORALL A, B: A >= B IFF NOT 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_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

quality91%

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.