Quelle  convergence_set.pvs

convergence_set[T:TYPE]: THEORY
%------------------------------------------------------------------------------
% Convergence properties for uncountable sets
%
%  MODIFICATIONS:
%
%     Author: David Lester, Manchester University 20/4/05
%
%------------------------------------------------------------------------------


BEGIN

  IMPORTING countable_convergence[T]

  a:   VAR real
  nz:  VAR nzreal
  X,Y: VAR set[T]
  t:   VAR T
  f,g: VAR [T -> real]

  nonzero_elts(f,X):set[T] = {t | X(t) AND f(t) /= 0}

  convergent?(X)(f): bool
    = is_countable(nonzero_elts(f,X)) AND convergent?(nonzero_elts(f,X))(f)

  convergent_zero:   LEMMA convergent?(X)(LAMBDA t: 0)

  convergent_plus:   LEMMA convergent?(X)(f) AND convergent?(X)(g) =>
                           convergent?(X)(f+g)

  convergent_scal:   LEMMA convergent?(X)(f) => convergent?(X)(a*f)

  convergent_opp:    LEMMA convergent?(X)(f) => convergent?(X)(-f)

  convergent_diff:   LEMMA convergent?(X)(f) AND convergent?(X)(g) =>
                           convergent?(X)(f-g)

  convergent_le:     LEMMA (FORALL t: abs(g(t)) <= abs(f(t))) AND
                           convergent?(X)(f) => convergent?(X)(g)

  convergent_empty:  LEMMA convergent?(emptyset[T])(g)

  convergent_singleton: LEMMA convergent?(singleton(t))(g)

  convergent_subset: LEMMA subset?(X,Y) AND convergent?(Y)(g) =>
                           convergent?(X)(g)

  convergent_intersection: LEMMA
    convergent?(X)(g) OR convergent?(Y)(g) => convergent?(intersection(X,Y))(g)

  convergent_difference: LEMMA
    convergent?(X)(g) => convergent?(difference(X,Y))(g)

  convergent_disjoint_union: LEMMA
    disjoint?(X,Y) AND convergent?(X)(g) AND convergent?(Y)(g) =>
                            convergent?(union(X,Y))(g)

  convergent_union: LEMMA
         convergent?(X)(g) AND convergent?(Y)(g) => convergent?(union(X,Y))(g)

  convergent_add: LEMMA convergent?(X)(g) =>
                        convergence_set.convergent?(add(t,X))(g)

  convergent_remove: LEMMA convergent?(X)(g) => convergent?(remove(t,X))(g)

  convergent_abs: LEMMA convergent?(X)(g) IFF convergent?(X)(abs(g))

END convergence_set