%-------------------------------------------------------------------------
%
% Basic properties of the set cardinality comparison functions
%
% For PVS version 3.2. November 4, 2004
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), University of Kansas
%
% EXPORTS
% -------
% sets_aux: card_comp_set[T1,T2], card_comp_set[T2,T1],
% card_comp_set_props[T1,T2]
%
%-------------------------------------------------------------------------
card_comp_set_props[T1: TYPE, T2: TYPE]: THEORY
EXPORTING ALL WITH card_comp_set[T1, T2], card_comp_set[T2, T1]
BEGIN
IMPORTING card_comp_set[T1, T2], card_comp_set[T2, T1]
% The following imports are for the proofs only
IMPORTING orders@set_dichotomous, orders@set_antisymmetric
S1: VAR set[T1]
S2: VAR set[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
FORALL S1, S2:
card_lt(S1, S2) IFF
(EXISTS (t: (S2)): TRUE) AND
NOT (EXISTS (f: [(S1) -> (S2)]): surjective?(f))
card_ge_surj: LEMMA
FORALL S1, S2:
card_ge(S1, S2) IFF
((EXISTS (t: (S1)): TRUE) AND (FORALL (t: (S2)): FALSE)) OR
(EXISTS (f: [(S1) -> (S2)]): surjective?(f))
% ==========================================================================
% The relationships of the functions
% ==========================================================================
card_lt_le: LEMMA FORALL S1, S2: card_lt(S1, S2) => card_le(S1, S2)
card_gt_ge: LEMMA FORALL S1, S2: card_gt(S1, S2) => card_ge(S1, S2)
card_lt_gt: LEMMA FORALL S1, S2: card_lt(S1, S2) = card_gt(S2, S1)
card_le_ge: LEMMA FORALL S1, S2: card_le(S1, S2) = card_ge(S2, S1)
card_gt_lt: LEMMA FORALL S1, S2: card_gt(S1, S2) = card_lt(S2, S1)
card_ge_le: LEMMA FORALL S1, S2: card_ge(S1, S2) = card_le(S2, S1)
card_lt_ge: LEMMA FORALL S1, S2: card_lt(S1, S2) XOR card_ge(S1, S2)
card_le_gt: LEMMA FORALL S1, S2: card_le(S1, S2) XOR card_gt(S1, S2)
card_eq_le_ge: LEMMA
FORALL S1, S2: card_eq(S1, S2) IFF card_le(S1, S2) AND card_ge(S1, S2)
card_le_lt_eq: LEMMA
FORALL S1, S2: card_le(S1, S2) IFF card_lt(S1, S2) OR card_eq(S1, S2)
card_ge_gt_eq: LEMMA
FORALL S1, S2: card_ge(S1, S2) IFF card_gt(S1, S2) OR card_eq(S1, S2)
card_lt_neq_ngt: LEMMA
FORALL S1, S2:
card_lt(S1, S2) => NOT card_eq(S1, S2) AND NOT card_gt(S1, S2)
card_gt_neq_nlt: LEMMA
FORALL S1, S2:
card_gt(S1, S2) => NOT card_eq(S1, S2) AND NOT card_lt(S1, S2)
% ==========================================================================
% (anti)commutativity and (anti)symmetry of the functions
% ==========================================================================
card_lt_anticommutative: LEMMA
FORALL S1, S2: card_lt(S1, S2) => NOT card_lt(S2, S1)
card_le_antisymmetric: LEMMA
FORALL S1, S2: card_le(S1, S2) AND card_le(S2, S1) => card_eq(S1, S2)
card_eq_symmetric: LEMMA FORALL S1, S2: card_eq(S1, S2) = card_eq(S2, S1)
card_ge_antisymmetric: LEMMA
FORALL S1, S2: card_ge(S1, S2) AND card_ge(S2, S1) => card_eq(S1, S2)
card_gt_anticommutative: LEMMA
FORALL S1, S2: card_gt(S1, S2) => NOT card_gt(S2, S1)
% ==========================================================================
% dichotomy and trichotomy of the functions
% ==========================================================================
card_lt_trichotomous: LEMMA
FORALL S1, S2: card_lt(S1, S2) OR card_lt(S2, S1) OR card_eq(S1, S2)
card_le_dichotomous: LEMMA
FORALL S1, S2: card_le(S1, S2) OR card_le(S2, S1)
card_ge_dichotomous: LEMMA
FORALL S1, S2: card_ge(S1, S2) OR card_ge(S2, S1)
card_gt_trichotomous: LEMMA
FORALL S1, S2: card_gt(S1, S2) OR card_gt(S2, S1) OR card_eq(S1, S2)
END card_comp_set_props
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
