Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: GoodCovar.java Sprache: PVS

Original von: PVS^©

% lattices formed by a total order.
%
% Author: Alfons Geser ([email protected]), National Institute of Aerospace
% Date: Dec 2004
%
% 8 Feb 2005, Jerry James added singleton_has_X, union_preserves_has_X,
%   add_preserves_has_X, X_singleton, X_union, and X_add, where
%   X ranges over {greatest, least}.

total_lattices[T: TYPE, <=: (total_order?[T])]: THEORY

BEGIN

  IMPORTING minmax_orders[T], lattices[T, <=]

  G, G1, G2: VAR (has_greatest?(<=))
  L, L1, L2: VAR (has_least?(<=))
  t: VAR T

  singleton_has_greatest: JUDGEMENT
    singleton(t) HAS_TYPE (has_greatest?(<=))

  union_preserves_has_greatest: JUDGEMENT
    union(G1, G2) HAS_TYPE (has_greatest?(<=))

  add_preserves_has_greatest: JUDGEMENT
    add(t, G) HAS_TYPE (has_greatest?(<=))

  greatest_singleton: LEMMA FORALL t: greatest(<=)(singleton(t)) = t

  greatest_union: LEMMA
    FORALL G1, G2:
      greatest(<=)(union(G1, G2)) =
       IF greatest(<=)(G1) <= greatest(<=)(G2) THEN greatest(<=)(G2)
       ELSE greatest(<=)(G1)
       ENDIF

  greatest_add: LEMMA
    FORALL G, t:
      greatest(<=)(add(t, G)) =
       IF greatest(<=)(G) <= t THEN t ELSE greatest(<=)(G) ENDIF

  singleton_has_least: JUDGEMENT singleton(t) HAS_TYPE (has_least?(<=))

  union_preserves_has_least: JUDGEMENT
    union(L1, L2) HAS_TYPE (has_least?(<=))

  add_preserves_has_least: JUDGEMENT add(t, L) HAS_TYPE (has_least?(<=))

  least_singleton: LEMMA FORALL t: least(<=)(singleton(t)) = t

  least_union: LEMMA
    FORALL L1, L2:
      least(<=)(union(L1, L2)) =
       IF least(<=)(L1) <= least(<=)(L2) THEN least(<=)(L1)
       ELSE least(<=)(L2)
       ENDIF

  least_add: LEMMA
    FORALL L, t:
      least(<=)(add(t, L)) =
       IF least(<=)(L) <= t THEN least(<=)(L) ELSE t ENDIF

END total_lattices

¤ Dauer der Verarbeitung: 0.22 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
Eigene Datei ansehen

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.