Quelle  countability_aux.pvs

%------------------------------------------------------------------------------
% Extras for countability. Somewhere in sets_aux.
%
%  MODIFICATIONS:
%
%     Author: David Lester, Manchester University 12/12/07
%
%------------------------------------------------------------------------------
countability_aux[T:TYPE]: THEORY

BEGIN

  IMPORTING countability[T],
            countable_props[T]

  t:     VAR T
  S:     VAR set[T]
  A,X,Y: VAR (is_countable)

  countably_infinite_is_nonempty: JUDGEMENT
    countably_infinite_set SUBTYPE_OF (nonempty?[T])

  countably_infinite_is_infinite: JUDGEMENT
    countably_infinite_set SUBTYPE_OF (is_infinite[T])

  countable_emptyset:      LEMMA is_countable(emptyset[T])
  countable_singleton:     LEMMA is_countable(singleton(t))
  countable_add:           LEMMA is_countable(add(t,X))
  countable_remove:        LEMMA is_countable(remove(t,X))
  countable_intersection1: LEMMA is_countable(intersection(X,S))
  countable_intersection2: LEMMA is_countable(intersection(S,X))
  countable_difference:    LEMMA is_countable(difference(X,S))

END countability_aux