%-------------------------------------------------------------------------
%
% The Well-Ordering Principle: every set can be well-ordered. This is
% equivalent to the Axiom of Choice, Zorn's Lemma, and Kuratowski's Lemma.
%
% For PVS version 3.2. February 28, 2005
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), University of Kansas
%
% EXPORTS
% -------
% prelude: finite_sets[T], orders[T], relations[T], sets[T]
% orders: bounded_orders[T], relations_extra[T], well_ordering[T]
%
%-------------------------------------------------------------------------
well_ordering[T: TYPE]: THEORY
% Hide all the technical details from public view
EXPORTING well_ordering WITH bounded_orders[T], finite_sets[T], orders[T],
relations_extra[T], relations[T], sets[T]
BEGIN
IMPORTING bounded_orders
% ==========================================================================
% A partial order on well-ordered sets
% ==========================================================================
%% Types
ordered_set: TYPE = [A: set[T], (well_ordered?[(A)])]
%% Variables
t: VAR T
<: VAR pred[[T, T]]
ord1, ord2: VAR ordered_set
%% Functions
ordered_set_order(ord1, ord2): bool =
subset?(ord1`1, ord2`1) AND
(FORALL (t, r: (ord1`1)): ord1`2(t, r) IFF ord2`2(t, r)) AND
(FORALL (t: (difference(ord2`1, ord1`1))):
upper_bound?[(ord2`1)](t, ord1`1, ord2`2))
partial_ordered_set: JUDGEMENT
ordered_set_order HAS_TYPE (partial_order?[ordered_set])
IMPORTING zorn[ordered_set, ordered_set_order]
C: VAR chain
ordered_set_union(C): ordered_set =
({t | EXISTS (S: (C)): S`1(t)},
LAMBDA (t, r: ({t | EXISTS (S: (C)): S`1(t)})):
EXISTS (ord: (C)): ord`1(t) AND ord`1(r) AND ord`2(t, r))
chain_upper_bound: LEMMA
FORALL C: bounded_above?[ordered_set](C, ordered_set_order)
% ==========================================================================
% The well-ordering theorem
% ==========================================================================
well_ordering: THEOREM EXISTS <: well_ordered?(<)
END well_ordering
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
