Quelle  card_sets_lemmas.pvs

%-------------------------------------------------------------------------
%
%  Lemmas about set operations and their implications for the cardinality
%  comparison relations.
%
%  For PVS version 3.2.  November 4, 2004
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), University of Kansas
%
%  EXPORTS
%  -------
%  sets_aux: card_comp_set[T,T], card_comp_set_props[T,T], card_single[T],
%    card_comp_set_transitive[T,T,T], card_sets_lemmas[T]
%
%-------------------------------------------------------------------------
card_sets_lemmas[T: TYPE]: THEORY
 BEGIN

  IMPORTING card_single[T]

  t: VAR T
  S, R: VAR set[T]

  empty_card_le: LEMMA FORALL S: card_le(emptyset[T], S)

  nonempty_card_lt: LEMMA FORALL S: card_lt(emptyset[T], S) IFF nonempty?(S)

  full_card_le: LEMMA FORALL S: card_le(S, fullset[T])

  add_card_le: LEMMA FORALL S, t: card_le(S, add(t, S))

  remove_card_ge: LEMMA FORALL S, t: card_ge(S, remove(t, S))

  subset_card_le: LEMMA FORALL S, R: subset?(S, R) => card_le(S, R)

  strict_subset_card_lt: LEMMA
    FORALL S, R: subset?(S, R) AND card_lt(S, R) => strict_subset?(S, R)

  union_card_le1: LEMMA FORALL S, R: card_le(S, union(S, R))
  union_card_le2: LEMMA FORALL S, R: card_le(R, union(S, R))

  intersection_card_le1: LEMMA FORALL S, R: card_le(intersection(S, R), S)
  intersection_card_le2: LEMMA FORALL S, R: card_le(intersection(S, R), R)

  difference_card_le: LEMMA FORALL S, R: card_le(difference(S, R), S)

 END card_sets_lemmas