Quelle  card_finite.pvs

%-------------------------------------------------------------------------
%
%  The relationship between the cardinality comparison functions when
%  applied to finite sets, and the finite_sets card(S) function.
%
%  For PVS version 3.2.  November 4, 2004
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), University of Kansas
%
%  EXPORTS
%  -------
%  prelude: finite_sets[T1], finite_sets[T2]
%  sets_aux: card_comp_set[T1,T2], card_comp_set[T2,T1],
%    card_comp_set_props[T1,T2], card_finite[T1,T2]
%
%-------------------------------------------------------------------------
card_finite[T1: TYPE, T2: TYPE]: THEORY
 BEGIN

  IMPORTING card_comp_set_props[T1, T2], finite_sets[T1], finite_sets[T2]

  n, m: VAR nat
  F1: VAR finite_set[T1]
  F2: VAR finite_set[T2]

  card_less_than: THEOREM
    FORALL F1, F2: card(F1) < card(F2) IFF card_lt(F1, F2)

  card_less_than_equal: THEOREM
    FORALL F1, F2: card(F1) <= card(F2) IFF card_le(F1, F2)

  card_equal: THEOREM FORALL F1, F2: card(F1) = card(F2) IFF card_eq(F1, F2)

  card_greater_than_equal: THEOREM
    FORALL F1, F2: card(F1) >= card(F2) IFF card_ge(F1, F2)

  card_greater_than: THEOREM
    FORALL F1, F2: card(F1) > card(F2) IFF card_gt(F1, F2)

 END card_finite