%-------------------------------------------------------------------------
%
%  Cardinality properties of infinite sets.
%
%  For PVS version 3.2.  February 10, 2005
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), University of Kansas
%
%  EXPORTS
%  -------
%  prelude: finite_sets[T], infinite_sets_def[T]
%  sets_aux: card_comp_set[nat,T], card_comp_set[T,nat], card_comp_set[T,T],
%    card_comp_set_props[T,nat], card_comp_set_props[T,T],
%    card_sets_lemmas[T], card_single[T], countable_props[T],
%    countability[T], infinite_sets[T]
%
%-------------------------------------------------------------------------
infinite_sets[T: TYPE]: THEORY
 BEGIN

  IMPORTING countable_props[T], card_sets_lemmas[T]

  t: VAR T
  S, R: VAR set[T]
  Fin: VAR finite_set[T]
  Inf: VAR infinite_set[T]

  infinite_add_card: THEOREM FORALL Inf, t: card_eq(Inf, add(t, Inf))

  infinite_remove_card: THEOREM FORALL Inf, t: card_eq(Inf, remove(t, Inf))

  finite_infinite_lt: THEOREM
    FORALL S: (FORALL Fin: card_lt(Fin, S)) IFF is_infinite(S)

 END infinite_sets