Quelle  card_comp_props.pvs   Sprache: PVS

%-------------------------------------------------------------------------
%
%  Basic properties of the type cardinality comparison functions
%
%  For PVS version 3.2.  November 4, 2004
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), University of Kansas
%
%  EXPORTS
%  -------
%  prelude: functions[T1,T2], functions[T2,T1]
%  sets_aux: card_comp[T1,T2], card_comp[T2,T1], card_comp_props[T1,T2]
%
%-------------------------------------------------------------------------
card_comp_props[T1: TYPE, T2: TYPE]: THEORY

 EXPORTING ALL WITH functions[T1, T2], functions[T2, T1],
                    card_comp[T1, T2], card_comp[T2, T1]

 BEGIN

  IMPORTING card_comp[T1, T2], card_comp[T2, T1]

  % The following imports are for the proofs only
  IMPORTING function_inverse_def[T1, T2]
  IMPORTING function_inverse_def[T2, T1]
  IMPORTING orders@set_dichotomous[T1, T2], 
            orders@set_antisymmetric[T1, T2]


  % ==========================================================================
  % We defined card_lt and card_ge as we did to avoid special casing empty
  % sets, which these results show would be necessary.
  % ==========================================================================

  card_lt_surj: LEMMA
    card_lt[T1, T2] IFF
     (EXISTS (t: T2): TRUE) AND NOT (EXISTS (f: [T1 -> T2]): surjective?(f))

  card_ge_surj: LEMMA
    card_ge[T1, T2] IFF
     ((EXISTS (t: T1): TRUE) AND (FORALL (t: T2): FALSE)) OR
      (EXISTS (f: [T1 -> T2]): surjective?(f))


  % ==========================================================================
  % The relationships of the functions
  % ==========================================================================

  card_lt_le: LEMMA card_lt[T1, T2] => card_le[T1, T2]
  card_gt_ge: LEMMA card_gt[T1, T2] => card_ge[T1, T2]

  card_lt_gt: LEMMA card_lt[T1, T2] = card_gt[T2, T1]
  card_le_ge: LEMMA card_le[T1, T2] = card_ge[T2, T1]
  card_gt_lt: LEMMA card_gt[T1, T2] = card_lt[T2, T1]
  card_ge_le: LEMMA card_ge[T1, T2] = card_le[T2, T1]

  card_lt_ge: LEMMA card_lt[T1, T2] XOR card_ge[T1, T2]
  card_le_gt: LEMMA card_le[T1, T2] XOR card_gt[T1, T2]

  card_eq_le_ge: LEMMA
    card_eq[T1, T2] IFF card_le[T1, T2] AND card_ge[T1, T2]
  card_le_lt_eq: LEMMA
    card_le[T1, T2] IFF card_lt[T1, T2] OR card_eq[T1, T2]
  card_ge_gt_eq: LEMMA
    card_ge[T1, T2] IFF card_gt[T1, T2] OR card_eq[T1, T2]

  card_lt_neq_ngt: LEMMA
    card_lt[T1, T2] => NOT card_eq[T1, T2] AND NOT card_gt[T1, T2]
  card_gt_neq_nlt: LEMMA
    card_gt[T1, T2] => NOT card_eq[T1, T2] AND NOT card_lt[T1, T2]


  % ==========================================================================
  % (anti)commutativity and (anti)symmetry of the functions
  % ==========================================================================

  card_lt_anticommutative: LEMMA card_lt[T1, T2] => NOT card_lt[T2, T1]

  card_le_antisymmetric: LEMMA
    card_le[T1, T2] AND card_le[T2, T1] => card_eq[T1, T2]

  card_eq_symmetric: LEMMA card_eq[T1, T2] = card_eq[T2, T1]

  card_ge_antisymmetric: LEMMA
    card_ge[T1, T2] AND card_ge[T2, T1] => card_eq[T1, T2]

  card_gt_anticommutative: LEMMA card_gt[T1, T2] => NOT card_gt[T2, T1]


  % ==========================================================================
  % dichotomy and trichotomy of the functions
  % ==========================================================================

  card_lt_trichotomous: LEMMA
    card_lt[T1, T2] OR card_lt[T2, T1] OR card_eq[T1, T2]

  card_le_dichotomous: LEMMA card_le[T1, T2] OR card_le[T2, T1]

  card_ge_dichotomous: LEMMA card_ge[T1, T2] OR card_ge[T2, T1]

  card_gt_trichotomous: LEMMA
    card_gt[T1, T2] OR card_gt[T2, T1] OR card_eq[T1, T2]

 END card_comp_props