Quelle partial_order_props.pvs Sprache: PVS

% Properties and definitions for ordered sets.

partial_order_props[T:TYPE,<=:(partial_order?[T])]: THEORY

BEGIN

  x,y,z: VAR T
  S:     VAR set[T]
  XS:    VAR setofsets[T]

  partial_order_reflexive:     LEMMA x <= x
  partial_order_antisymmetric: LEMMA x <= y AND y <= x IMPLIES x = y
  partial_order_transitive:    LEMMA x <= y AND y <= z IMPLIES x <= z

  AUTO_REWRITE+  partial_order_reflexive
  AUTO_REWRITE+  partial_order_antisymmetric
  AUTO_REWRITE+  partial_order_transitive

  lower_set?(S)  :bool = FORALL x,y: member(x,S) AND y <= x IMPLIES member(y,S)
  upper_set?(S)  :bool = FORALL x,y: member(x,S) AND x <= y IMPLIES member(y,S)
  lower_sets?(XS):bool = every(lower_set?,XS)
  upper_sets?(XS):bool = every(upper_set?,XS)

  lower_set:  TYPE+ = (lower_set?)  CONTAINING emptyset[T]
  upper_set:  TYPE+ = (upper_set?)  CONTAINING emptyset[T]
  lower_sets: TYPE+ = (lower_sets?) CONTAINING emptyset[set[T]]
  upper_sets: TYPE+ = (upper_sets?) CONTAINING emptyset[set[T]]

  L,L1,L2:  VAR lower_set
  U,U1,U2:  VAR upper_set
  LS:       VAR lower_sets
  US:       VAR upper_sets

  complement_lower_set:  JUDGEMENT complement(L)  HAS_TYPE upper_set
  complement_upper_set:  JUDGEMENT complement(U)  HAS_TYPE lower_set
  Complement_lower_sets: JUDGEMENT Complement(LS) HAS_TYPE upper_sets
  Complement_upper_sets: JUDGEMENT Complement(US) HAS_TYPE lower_sets

  down(x): lower_set = {y | y <= x}
  up(x):   upper_set = {y | x <= y}

  down_subset: LEMMA x <= y IMPLIES subset?(down(x),down(y))
  up_subset:   LEMMA x <= y IMPLIES subset?(up(y),up(x))

  lower_set_def: LEMMA lower_set?(S) IFF S = Union(image(down,S))
  upper_set_def: LEMMA upper_set?(S) IFF S = Union(image(up,S))

  Union_lower_set:        JUDGEMENT Union(LS)           HAS_TYPE lower_set
  Union_upper_set:        JUDGEMENT Union(US)           HAS_TYPE upper_set
  Intersection_lower_set: JUDGEMENT Intersection(LS)    HAS_TYPE lower_set
  Intersection_upper_set: JUDGEMENT Intersection(US)    HAS_TYPE upper_set
  union_lower_set:        JUDGEMENT union(L1,L2)        HAS_TYPE lower_set
  union_upper_set:        JUDGEMENT union(U1,U2)        HAS_TYPE upper_set
  intersection_lower_set: JUDGEMENT intersection(L1,L2) HAS_TYPE lower_set
  intersection_upper_set: JUDGEMENT intersection(U1,U2) HAS_TYPE upper_set

END partial_order_props

quality91%

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