Top File of PVS orders Library

 
top: THEORY
%----------------------------------------------------------------------------
%
%  Orders Library
%  --------------
%
%  Version 1.0    Extracted From sets_aux library on 4/21/05
%  Version 1.1    Added finite_below, similarity, and similarity_props
% 
%  Authors:
%      Bruno Dutertre  SRI International
%      Jerry James        University of Kansas
%      Alfons Geser     National Institute For Aerospace
%----------------------------------------------------------------------------
BEGIN

 %---- Alfons Geser theories on order
 IMPORTING
  bounded_integers,         % nonempty, above/below bounded => greatest/least
  bounded_orders,           % definitions of lub, glb, (complete) lattice
  bounded_sets,             % judgements about boundedness properties of sets
  closure_ops,              % reflexive, symmetric, transitive, etc. closure
  complementary_lattices,   % lattices with a "complement" function
  complementary_orders,     % ordered sets with a "complement" function
  complete_lattices,        % every set is tightly bounded
  complete_lower_semilattices, % every set is greatest bounded below
  complete_upper_semilattices, % every set is least bounded above
  finite_orders,            % properties of an order on a finite type
  finite_pointwise_orders,  % orders on functions with a finite domain
  finite_total_orders,      % total orders on a finite type
  fixed_points,             % fixed points characterized by prefixed points
  integer_enumerations,     % infinite below bounded set of ints => enumerable
  lattices,                 % operations that preserve tight-boundedness
  lower_semilattices,       % definition of binary glb function
  minmax_orders,            % minimal, maximal, least, greatest elements
  monotone_sequences,       % infinite ascending/descending sequences
  new_mucalculus_prop,      % a simulation of fixedpoints@mucalculus_prop
  non_empty_bounded_sets,   % nonempty sets of reals bounded above/below
  pointwise_orders,         % lifting an order to functions
  sets_complete_lattices,   % sets ordered by "subset?" form a complete lattice
  total_lattices,           % a lattice defined by a total order
  upper_semilattices,       % definition of binary lub function
  well_foundedness          % well-foundedness = no infinite descending seq.

 %---- Jerry James theories on order
 IMPORTING
  bounded_nats,             % all nonempty sets of nats have a least element
  chain,                    % totally ordered subsets of a poset
  chain_chain,              % chains of chains in inclusion order
  converse_zorn,            % lower bound on all chains => min. element exists
  finite_below,             % finite set = monotonic bijection with below[N]
  isomorphism,              % isomorphisms between ordered sets
  isomorphism_equivalence,  % automorphisms and equivalence classes thereof
  isomorphism_symmetric,    % the isomorphic? relation is symmetric
  isomorphism_transitive,   % the isomorphic? relation is transitive
  kuratowski,               % there exists a maximal chain in any set
  monotone_functions,       % (non)in/decreasing functions on ordered sets
  numbers_infinite,         % the nats, ints, rats, and reals are infinite
  order_strength,           % strengthenings and weakenings of orders
  ordered_int,              % ordered subsets of the integers
  ordered_nat,              % ordered subsets of the natural numbers
  ordered_subset,           % prefix, suffix, upto, below, upfrom, etc.
  range,                    % open and closed ranges of numbers
  range_real,               % the range theory, tailored to ranges of reals
  set_antisymmetric,        % injective maps both ways => bijection exists
  set_dichotomous,          % injective map exists between any 2 sets
  similarity,               % similar ordered sets: order-preserving bijection
  similarity_props,         % least, greatest, and all finite sets are similar
  subset_chain,             % chains of sets in inclusion order
  well_nat,                 % well-ordered relations on sets of nats
  well_ordered_finite,      % linear order + finite below sets = well-ordered
  well_ordered_props,       % some properties of well-ordered sets
  well_ordered_traversal,   % first, last, next, & prev for well-ordered sets
  well_ordering,            % every set has a well-ordering relation
  zorn                      % upper bound on all chains => max. element exists

 %---- Alfons Geser prelude-style theories
 IMPORTING
  booleans_are_finite,      % the booleans are a finite type
  finite_types,             % if T is finite, then every set of T is finite
  function_image_extra,     % Two more rewrite rules for function_image
  indexed_sets_extra,       % IUnion and IIntersection are monotone
  infinite_pigeonhole,      % [infinite_domain -> finite_range] enumerates
                            % some range element infinitely often
  relation_iterate,         % R o R o ... o R  n times.
  relations_extra,          % rewrite rules and judgements for binary relations
  skolemization,            % how to eliminate inner quantifiers

 %--- New Content From David Lester, Manchester

  directed_orders,        % New theories for orders library
  bounded_order_props,    % Properties of bounded orders
  directed_order_props,   % Properties of directed orders
  partial_order_props,    % Properties of partial orders
  lift_props,             % Extras for the lift datatype
  lifted_orders,          % Induced properties of lifted orders
  partial_order_lift,
  sum_orders,             % Induced properties of union orders
  product_orders          % Induced properties of product orders
  
  %------- Bruno Dutertre
  IMPORTING
   mucalculus_prop           % originally in library fixedpoints
 
END top

The tag identifies links that are outside the NASA domain