NASA logo

+ Contact NASA

  • + HOME
  • + TEAM
  • + LINKS

  • 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
     %---- Alfons Geser theories on order
      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
      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
      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
      sum_orders,             % Induced properties of union orders
      product_orders          % Induced properties of product orders
      %------- Bruno Dutertre
       mucalculus_prop           % originally in library fixedpoints
    END top

    The tag [*] identifies links that are outside the NASA domain