| products/sources/formale Sprachen/PVS/orders/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: top.pvs Sprache: PVSOriginal von: PVS© |
|
||||||
|
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 <[email protected]> SRI International % Jerry James <[email protected]> University of Kansas % Alfons Geser <[email protected]> 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 ¤ Dauer der Verarbeitung: 0.22 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.Bot Zugriff |
