Quelle  well_ordering.pvs   Sprache: unbekannt

%-------------------------------------------------------------------------
%
%  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 (jamesj@acm.org), 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