Quelle lower_semilattices.pvs Sprache: PVS

% lower semilattices; binary glb function
% Author: Alfons Geser (geser@nianet.org), National Institute of Aerospace
% Date: Oct 2004 / Jan 2005

lower_semilattices[
  T: TYPE,
  (IMPORTING bounded_orders[T])
  <=: (lower_semilattice?[T])
]: THEORY

BEGIN

  IMPORTING bounded_sets[T, <=]

  s, t, u, t1, t2: VAR T
  S, S1, S2: VAR (greatest_bounded_below?[T](<=))

  finite_set_is_greatest_bounded_below: JUDGEMENT
    non_empty_finite_set[T] SUBTYPE_OF (greatest_bounded_below?(<=))

  greatest_lower_bound_singleton: LEMMA
    greatest_lower_bound?[T](t, singleton(t), <=)

  glb_singleton: LEMMA
    glb(<=)(singleton(t)) = t

  glb(t, u): T = glb[T](<=)(union(singleton(t), singleton(u)))

  le_glb: LEMMA s <= glb(t, u) IFF s <= t AND s <= u
  glb_le_1: LEMMA t <= s => glb(t, u) <= s
  glb_le_2: LEMMA u <= s => glb(t, u) <= s

  union_preserves_bounded_below: JUDGEMENT
    union(S1, S2: (bounded_below?[T](<=))) HAS_TYPE (bounded_below?[T](<=))

  add_preserves_bounded_below: JUDGEMENT
    add(s: T, S: (bounded_below?[T](<=))) HAS_TYPE (bounded_below?[T](<=))

  greatest_lower_bound_union: LEMMA
    greatest_lower_bound?[T](t1, S1, <=) &
    greatest_lower_bound?[T](t2, S2, <=) =>
      greatest_lower_bound?[T](glb(t1, t2), union(S1, S2), <=)

  greatest_lower_bound_add: LEMMA
    greatest_lower_bound?[T](t, S, <=) =>
      greatest_lower_bound?[T](glb(t, s), add(s, S), <=)

  union_preserves_greatest_bounded_below: JUDGEMENT
    union(S1, S2) HAS_TYPE (greatest_bounded_below?[T](<=))

  add_preserves_greatest_bounded_below: JUDGEMENT
    add(s, S) HAS_TYPE (greatest_bounded_below?[T](<=))

  glb_union: LEMMA
    glb[T](<=)(union(S1, S2)) = glb(glb[T](<=)(S1), glb[T](<=)(S2))

  glb_add: LEMMA
    glb[T](<=)(add(s, S)) = glb(glb[T](<=)(S), s)

END lower_semilattices

quality80%

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