Impressum top.pvs   Sprache: PVS

top: THEORY
%----------------------------------------------------------------------------
%
%  Additional Set Theory (sets_aux)
%  --------------------------------
%
%  Version 1.0    Powersets merged with finite_sets_aux    2/10/04
%  Version 2.0    Jerry James libraries added              5/5/04
%  Version 2.1    Updates for PVS 3.2; removed theories    11/3/04
%                 now in the prelude or finite_sets
%  Version 3.0    Merged in Alfons Geser's order theories  2/10/05
%  Version 3.1    Added some theories from David Lester    4/12/05
%  Version 3.2    Added cardinal and sets_lemmas_extra     5/11/05
%  Version 3.3    Updated countable sets theories          9/15/09
% 
%  Authors:
%      Bruno Dutertre <bruno@sdl.sri.com>    SRI International
%      Jerry James    <jamesj@acm.org>       University of Kansas
%      David Lester   <dlester@cs.man.ac.uk> Manchester University
%----------------------------------------------------------------------------
BEGIN

 %---- Bruno Dutertre theories on powersets
 IMPORTING
  fun_below_props,          % bijections with Cartesian products
  power_sets,               % cardinality and finiteness
  set_of_functions          % functions from finite set A to B

 %---- Jerry James theories on infinite cardinalities
 IMPORTING
  bits,                     % sets of bit numbers (used to show countability)
  card_comp,                % compare the cardinality of any two types
  card_comp_props,          % properties of the card_comp predicates
  card_comp_set,            % compare the cardinality of any two sets
  card_comp_set_props,      % properties of the card_comp_set predicates
  card_comp_set_transitive, % transitivity of the card_comp_set predicates
  card_comp_transitive,     % transitivity of the card_comp predicates
  card_finite,              % card_comp vs. card(S) from finite_sets
  card_power,               % card[T] < card[set[T]]
  card_power_set,           % card(S) < card(powerset(S))
  card_sets_lemmas,         % relationships of set operations to cardinality
  card_single,              % single type properties of card_comp_set preds
  card_function,            % surjection/injection image properties
  cardinal,                 % cardinality(S) for any set S
  countability,             % definition of (un)countable sets
  countable_image,          % countable image
  countable_props,          % properties of (un)countable sets
  countable_set,            % some countable sets of numbers (e.g., integers)
  countable_setofsets,      % operations on countable families of sets
  countable_types,          % countability of some prelude types
  infinite_card,            % card_comp implications for finiteness
  infinite_image,           % infinite images of a set under some function
  infinite_sets,            % cardinality of infinite set add and remove
  sets_lemmas_extra         % disjoint? is commutative

 %--- David Lester theories on infinite/countable sets
 IMPORTING
  countable_image,          % image of a countable set is countable
  card_function,            % finite/infinite properties of functions
  infinite_nat_def,         % infinite IFF injective map from the naturals


  indexed_sets_aux,      % Additional prelude indexed set lemmas
  countable_indexed_sets,% countable setsofsets vs indexed sets
  nat_indexed_sets,      % increasing/decresing indexed sets
  inverse_image_Union,   % inverse_image(f,Union(X))

  countability_aux,      %% RWB

  cantor_bernstein_schroeder  %% Proved by Anthony Narkawicz

 IMPORTING
 % Dragan Stosic's relational and functional choice facts based on Axiom of Choice
   top_choice_facts,
 % Dragan Stosic's refinement relations
   top_refinement_relations
 
END top