Quelle minmax_orders.pvs Sprache: PVS

%  Maximal, greatest, minimal, least elements on subsets, and their
%  correlation with least upper and greatest lower bounds.
%
%  Author: Alfons Geser (geser@nianet.org), National Institute of Aerospace
%  Date: Oct 2004 / Jan 2005

minmax_orders[T: TYPE]: THEORY

BEGIN

  IMPORTING bounded_orders[T], finite_sets@finite_sets_minmax

  t, r: VAR T
  S: VAR set
  F: VAR finite_set
  NF: VAR non_empty_finite_set[T]
  <=, R: VAR pred[[T,T]]
  le: VAR (total_order?[T])
  ale: VAR (antisymmetric?[T])
  tle: VAR (dichotomous?[T])

  % ==========================================================================
  % Maximal/greatest elements
  % ==========================================================================

  % Maximal elements
  maximal?(t, S, <=): bool =
    S(t) AND NOT (EXISTS (r: (S)): t <= r AND t /= r)
%    S(t) AND NOT lower_bound(t, S, irreflexive_kernel(<=))
  maximal?(S, <=)(t): MACRO bool = maximal?(t, S, <=)
  has_maximal?(S, <=): bool = EXISTS t: maximal?(t, S, <=)

  % Greatest elements
  greatest?(t, S, <=): bool = S(t) AND upper_bound?(t, S, <=)
  greatest?(S, <=)(t): MACRO bool = greatest?(t, S, <=)
  has_greatest?(S, <=): bool = EXISTS t: greatest?(t, S, <=)
  has_greatest?(<=)(S): MACRO bool = has_greatest?(S, <=)
  greatest(<=)(S: (has_greatest?(<=))): {t: (S) | greatest?(t, S, <=)}

  % Properties
  greatest_iff_least_upper_bound: LEMMA
    greatest?(t, S, <=) IFF least_upper_bound?(t, S, <=) AND S(t)

  greatest_is_least_upper_bound: JUDGEMENT
    (greatest?) SUBTYPE_OF (least_upper_bound?)

  has_greatest_is_least_bounded_above: JUDGEMENT
    (has_greatest?) SUBTYPE_OF (least_bounded_above?)

  greatest_equals_lub: LEMMA
    FORALL (S: (has_greatest?(ale))): greatest(ale)(S) = lub(ale)(S)

  greatest_unique: LEMMA
    FORALL (<=: (antisymmetric?[T]), (s, t: (greatest?(S, <=)))): s = t

  greatest_is_maximal: LEMMA
    greatest?(t, S, ale) => maximal?(t, S, ale)

  maximal_is_greatest: LEMMA
    maximal?(t, S, tle) => greatest?(t, S, tle)

  non_empty_finite_has_greatest: LEMMA
    has_greatest?(NF, le)

  greatest_ge: LEMMA
    FORALL (S: (has_greatest?(<=)), m: (S)): m <= greatest(<=)(S)

  greatest_monotone: LEMMA
    FORALL (S1, S2: (has_greatest?(<=))):
      subset?(S1, S2) => greatest(<=)(S1) <= greatest(<=)(S2)

  greatest_def: LEMMA
    FORALL (S: (has_greatest?(ale))):
      greatest(ale)(S) = t IFF greatest?(t, S, ale)

  greatest_upper_bound: LEMMA
    FORALL (<=: (partial_order?[T]), S: (has_greatest?(<=))):
      greatest(<=)(S) <= t IFF upper_bound?[T](t, S, <=)

  % ==========================================================================
  % Minimal/least elements
  % ==========================================================================

  % Minimal elements
  minimal?(t, S, <=): bool =
    S(t) AND NOT (EXISTS (r: (S)): r <= t AND t /= r)
  minimal?(S, <=)(t): MACRO bool = minimal?(t, S, <=)
  has_minimal?(S, <=): bool = EXISTS t: minimal?(t, S, <=)

  % Least elements
  least?(t, S, <=): bool = S(t) AND lower_bound?(t, S, <=)
  least?(S, <=)(t): MACRO bool = least?(t, S, <=)
  has_least?(S, <=): bool = EXISTS t: least?(t, S, <=)
  has_least?(<=)(S): MACRO bool = has_least?(S, <=)
  least(<=)(S: (has_least?(<=))): {t: (S) | least?(t, S, <=)}

  % Properties
  least_iff_greatest_lower_bound: LEMMA
    least?(t, S, <=) IFF greatest_lower_bound?(t, S, <=) AND S(t)

  least_is_greatest_lower_bound: JUDGEMENT
    (least?) SUBTYPE_OF (greatest_lower_bound?)

  has_least_is_greatest_bounded_below: JUDGEMENT
    (has_least?) SUBTYPE_OF (greatest_bounded_below?)

  least_equals_glb: LEMMA
    FORALL (S: (has_least?(ale))): least(ale)(S) = glb(ale)(S)

  least_unique: LEMMA
    FORALL (<=: (antisymmetric?[T]), (s, t: (least?(S, <=)))): s = t

  least_is_minimal: LEMMA
    least?(t, S, ale) => minimal?(t, S, ale)

  minimal_is_least: LEMMA
    minimal?(t, S, tle) => least?(t, S, tle)

  non_empty_finite_has_least: LEMMA
    has_least?(NF, le)

  least_le: LEMMA
    FORALL (S: (has_least?(<=)), m: (S)): least(<=)(S) <= m

  least_monotone: LEMMA
    FORALL (S1, S2: (has_least?(<=))):
      subset?(S1, S2) => least(<=)(S2) <= least(<=)(S1)

  least_def: LEMMA
    FORALL (S: (has_least?(ale))):
      least(ale)(S) = t IFF least?(t, S, ale)

  least_lower_bound: LEMMA
    FORALL (<=: (partial_order?[T]), S: (has_least?(<=))):
      t <= least(<=)(S) IFF lower_bound?[T](t, S, <=)

  % ==========================================================================
  % Both greatest and least elements exist
  % ==========================================================================

  has_extrema?(S, <=): bool = has_greatest?(S, <=) AND has_least?(S, <=)
%  bounded_type?(<=): bool = has_extrema?(fullset, <=)

  has_extrema_has_greatest: JUDGEMENT
    (has_extrema?) SUBTYPE_OF (has_greatest?)

  has_extrema_has_least: JUDGEMENT
    (has_extrema?) SUBTYPE_OF (has_least?)

  total_order_is_lattice: JUDGEMENT
    (total_order?) SUBTYPE_OF (lattice?)

END minmax_orders

quality90%

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