Quelle total_lattices.pvs Sprache: PVS

% lattices formed by a total order.
%
% Author: Alfons Geser (geser@nianet.org), 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

quality89%

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