%-------------------------------------------------------------------------
%
%  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 <  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