Quelle scott_continuity.pvs Sprache: PVS

%------------------------------------------------------------------------------
% Continuous Functions bewteen Scott Topologies
%
% All references are to BA Davey and HA Priestly "Introduction to Lattices and
% Orders", CUP, 1990
%
% We give the Domain Theoretical formulation of Continuity
% (scott_continuous_def) and show that the pointwise order on functions is
% itself directed complete (pointwise_complete).
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
%     Version 1.0            25/12/07  Initial Version
%------------------------------------------------------------------------------

scott_continuity[T1,T2:TYPE, (IMPORTING orders@directed_orders)
                 le1:(directed_complete_partial_order?[T1]),
                 le2:(directed_complete_partial_order?[T2])]: THEORY

BEGIN

  IMPORTING scott[T1,le1], scott[T2,le2], fun_preds_partial[T1,T2,le1,le2],
            topology@continuity_def[T1,scott_open_sets[T1,le1],
                                    T2,scott_open_sets[T2,le2]],
            topology@continuity[T1,scott_open_sets[T1,le1],
                                T2,scott_open_sets[T2,le2]]

  D: VAR directed[T1,le1]
  a: VAR T2
  f: VAR [T1->T2]
  g: VAR (increasing?)

% The following three Lemmata are D&P 3.15 (i)

  lub_set_image:  LEMMA lub_set?(image(g,D))
  directed_image: LEMMA directed?[T2,le2](image(g,D))
  lub_image:      LEMMA le2(lub(image(g,D)),g(lub(D)))

% The following is D&P 3.15 (ii)

  lub_image_increasing: LEMMA
       (FORALL D: directed?[T2,le2](image(f,D)) AND
                  le2(lub[T2,le2](image(f,D)),f(lub[T1,le1](D))))
       IMPLIES increasing?(f)

  lub_preserving?(f):bool = FORALL D: lub_set?(image(f,D)) IMPLIES
                                        f(lub(D)) = lub(image(f,D))

  scott_continuous?(f):bool = increasing?(f) AND lub_preserving?(f)

  scott_continuous: TYPE = (scott_continuous?)

  scott_continuous_def: LEMMA continuous?(f) IFF scott_continuous?(f)

  scott_continuous_is_continuous:
                   JUDGEMENT (scott_continuous?) SUBTYPE_OF (continuous?)
  continuous_is_scott_continuous:
                   JUDGEMENT (continuous?)       SUBTYPE_OF (scott_continuous?)
  continuous_is_increasing:
                   JUDGEMENT (continuous?)       SUBTYPE_OF (increasing?)
  continuous_is_lub_preserving:
                   JUDGEMENT (continuous?)       SUBTYPE_OF (lub_preserving?)

  IMPORTING structures@const_fun_def[T1,T2],
            topology@constant_continuity[T1,scott_open_sets[T1,le1],
                                         T2,scott_open_sets[T2,le2]]

  const_scott_continuous: JUDGEMENT const_fun(a) HAS_TYPE scott_continuous

  IMPORTING orders@directed_orders[(scott_continuous?)],
            orders@pointwise_orders[T1,T2]

  pointwise_complete: LEMMA
    directed_complete?[(scott_continuous?)](pointwise(le2))

  scott_continuous_dcpo: LEMMA
    directed_complete_partial_order?[(scott_continuous?)](pointwise(le2))

  IMPORTING scott[(scott_continuous?),(pointwise(le2))]

END scott_continuity

quality98%

¤ Dauer der Verarbeitung: 0.12 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.