%-------------------------------------------------------------------------
%
% Compare set cardinalities for any two sets, whether finite or infinite.
% See cardinal.pvs for a cardinality(S) function that operates on any
% set, whether finite or infinite, using these definitions as a basis.
%
% We have to take great care with empty sets. The basic problem is that
% there is NO function from a nonempty domain to an empty range. This is
% why card_lt and card_ge deal with functions that are "reversed" from
% those in the other definitions, so that we can talk about injective
% functions (which exist from empty domains to nonempty ranges) instead
% of surjective functions (which do not exist from nonempty domains to
% empty ranges).
%
% 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[T1: TYPE, T2: TYPE]: THEORY
BEGIN
IMPORTING functions[T1, T2], functions[T2, T1]
card_lt: bool = NOT (EXISTS (f: [T2 -> T1]): injective?(f))
card_le: bool = EXISTS (f: [T1 -> T2]): injective?(f)
card_eq: bool = EXISTS (f: [T1 -> T2]): bijective?(f)
card_ge: bool = EXISTS (f: [T2 -> T1]): injective?(f)
card_gt: bool = NOT (EXISTS (f: [T1 -> T2]): injective?(f))
END card_comp
¤ Dauer der Verarbeitung: 0.1 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.
|
