%-------------------------------------------------------------------------
%
% Basic properties of the type cardinality comparison functions
%
% For PVS version 3.2. November 4, 2004
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), 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
¤ 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.
|
