Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: well_ordering.pvs Sprache: PVS

Original von: PVS^©

%------------------------------------------------------------------------------
% Properties of Lifted Orders
%
%       Author: David Lester <[email protected]> Manchester University
%
% We define a lifting operator on relations, and show that this operation
% preserves directed completeness and pointedness.
%
%       Version 1.0          03/30/06
%------------------------------------------------------------------------------

lifted_orders[T:TYPE]: THEORY

BEGIN

  rel: VAR pred[[T,T]]
  x,y: VAR lift[T]

  IMPORTING lift_props[T]

  lift(rel)(x,y):bool = (NOT up?(x)) OR (up?(y) AND rel(down(x),down(y)))

  lift_preserves_reflexive: JUDGEMENT
   lift(r:(reflexive?[T])) HAS_TYPE (reflexive?[lift[T]])

  lift_preserves_transitive: JUDGEMENT
   lift(r:(transitive?[T])) HAS_TYPE (transitive?[lift[T]])

  lift_preserves_antisymmetric: JUDGEMENT
   lift(r:(antisymmetric?[T]))  HAS_TYPE (antisymmetric?[lift[T]])

  lift_preserves_preorder: JUDGEMENT
   lift(r:(preorder?[T])) HAS_TYPE (preorder?[lift[T]])

  lift_preserves_partial_order: JUDGEMENT
   lift(r:(partial_order?[T])) HAS_TYPE (partial_order?[lift[T]])

  IMPORTING directed_orders[T], directed_orders[lift[T]]

  lift_lub_emptyset: LEMMA lub(lift(rel))(emptyset[lift[T]]) = bottom

  lift_lub_bounded:  LEMMA FORALL (rel:(antisymmetric?[T]),
                                   S:(nonempty_least_bounded_above?(rel))):
       lub(lift(rel))(image[T,lift[T]](up,S)) = up(lub(rel)(S))

  lift_preserves_directed_complete: JUDGEMENT
   lift(r:(directed_complete?[T]))      HAS_TYPE (directed_complete?[lift[T]])

  lift_preserves_directed_complete_partial_order: JUDGEMENT
   lift(r:(directed_complete_partial_order?[T]))
                   HAS_TYPE (pointed_directed_complete_partial_order?[lift[T]])

END lifted_orders

¤ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.