Quelle  infinite_card.pvs   Sprache: PVS

%-------------------------------------------------------------------------
%
%  Implications for finiteness and infiniteness of cardinal relations.
%
%  For PVS version 3.2.  November 4, 2004
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), University of Kansas
%
%  EXPORTS
%  -------
%  prelude: infinite_sets_def[T1], infinite_sets_def[T2]
%  sets_aux: card_comp_set[T1,T2], card_comp_set[T2,T1],
%    card_comp_set_props[T1,T2], infinite_card[T1,T2]
%
%-------------------------------------------------------------------------
infinite_card[T1: TYPE, T2: TYPE]: THEORY
 BEGIN

  IMPORTING infinite_sets_def[T1], infinite_sets_def[T2]
  IMPORTING card_comp_set_props[T1, T2]

  S1: VAR set[T1]
  S2: VAR set[T2]

  finite_card_eq: THEOREM
    FORALL S1, S2: card_eq(S1, S2) => (is_finite(S1) IFF is_finite(S2))

  infinite_card_eq: COROLLARY
    FORALL S1, S2: card_eq(S1, S2) => (is_infinite(S1) IFF is_infinite(S2))

  infinite_card_le: THEOREM
    FORALL S1, S2: card_le(S1, S2) AND is_infinite(S1) => is_infinite(S2)

  infinite_card_ge: THEOREM
    FORALL S1, S2: card_ge(S1, S2) AND is_infinite(S2) => is_infinite(S1)

  finite_card_le: THEOREM
    FORALL S1, S2: card_le(S1, S2) AND is_finite(S2) => is_finite(S1)

  finite_card_ge: THEOREM
    FORALL S1, S2: card_ge(S1, S2) AND is_finite(S1) => is_finite(S2)

 END infinite_card