Quelle scott.pvs Sprache: PVS

%------------------------------------------------------------------------------
% Scott Topology
%
% All references are to BA Davey and HA Priestly "Introduction to Lattices and
% Orders", CUP, 1990
%
% Notice that this is a T0 topology, and not Hausdorff (unless the order is
% equality).
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
%     Version 1.0            25/12/07  Initial Version
%------------------------------------------------------------------------------

scott[T:TYPE, (IMPORTING orders@directed_orders[T])
      <=:(directed_complete_partial_order?[T])]:THEORY

BEGIN

  IMPORTING topology@topology_def[T],
            orders@directed_order_props[T,<=]

  x,y: VAR T
  L:   VAR lower_set
  LS:  VAR lower_sets
  D:   VAR directed

  scott_closed_sets:setofsets[T]
    = {L | FORALL D: subset?(D,L) IMPLIES member(lub(D),L)}

  scott_open_sets:setofsets[T] = Complement(scott_closed_sets)

  down_is_closed:     LEMMA member(down(x),scott_closed_sets)

  scott_empty:        LEMMA member(emptyset, scott_closed_sets)

  scott_full:         LEMMA member(fullset,  scott_closed_sets)

  scott_union:        LEMMA FORALL (A,B:(scott_closed_sets)):
                              member(union(A,B), scott_closed_sets)

  scott_Intersection: LEMMA subset?(LS,scott_closed_sets) IMPLIES
                              member(Intersection(LS), scott_closed_sets)

  scott_topology:     LEMMA topology?(scott_open_sets)

  scott_open_sets_is_topology: JUDGEMENT scott_open_sets HAS_TYPE topology

  IMPORTING topology@topology[T,scott_open_sets]

  A: VAR open_set

  closed_is_lower:   JUDGEMENT (closed?) SUBTYPE_OF lower_set
  open_is_upper:     JUDGEMENT (open?)   SUBTYPE_OF upper_set

  closure_is_down:   LEMMA Cl(singleton(x)) = down(x)
  order_iff_closure: LEMMA x <= y IFF member(x,Cl(singleton(y)))
  order_iff_subset:  LEMMA x <= y IFF FORALL A: member(x,A) IMPLIES member(y,A)
  scott_is_T0:       LEMMA T0_space?(scott_open_sets)

  scott_hausdorff:   LEMMA
               hausdorff_space?(scott_open_sets) IFF trivial_partial_order?(<=)

END scott

quality83%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.