Quelle ordered_int.pvs Sprache: PVS

%-------------------------------------------------------------------------
%
%  Specialization of the ordered_subset theory to sets of integers.
%
%  For PVS version 3.2.  January 31, 2005
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), University of Kansas
%
%  EXPORTS
%  -------
%  prelude: finite_sets[int], infinite_sets_def[int], orders[int],
%    real_props, relation_props2[int, int, int, int], relations[int],
%    restrict_order_props[real, int], sets[int]
%  finite_sets: finite_sets_inductions, finite_sets_minmax
%  orders: bounded_orders[int], closure_ops[int], indexed_sets_extra,
%    minmax_orders[int], ordered_int, ordered_subset[int],
%    relation_iterate[int], relations_extra[int]
%
%-------------------------------------------------------------------------
ordered_int: THEORY
BEGIN

  IMPORTING infinite_sets_def[int], restrict_order_props[real, int]
  IMPORTING real_props, minmax_orders[int], ordered_subset[int]

  i: VAR int
  pre: VAR (prefix?(<=))
  suf: VAR (suffix?(<=))

  % Attempting to use the ordered_subset definitions directly in the
  % judgements below causes PVS 3.2 to complain that the variable '<=' is
  % undeclared.  Changing to 'reals.<=' causes the parser to choke on the '.'.
  upto(i): MACRO (prefix?(<=)) = upto(i, <=)
  below(i): MACRO (prefix?(<=)) = below(i, <=)
  above(i): MACRO (suffix?(<=)) = above(i, <=)
  upfrom(i): MACRO (suffix?(<=)) = upfrom(i, <=)

  upto_has_greatest: JUDGEMENT upto(i) HAS_TYPE (has_greatest?(<=))
  below_has_greatest: JUDGEMENT below(i) HAS_TYPE (has_greatest?(<=))
  above_has_least: JUDGEMENT above(i) HAS_TYPE (has_least?(<=))
  upfrom_has_least: JUDGEMENT upfrom(i) HAS_TYPE (has_least?(<=))

  prefix_empty: THEOREM FORALL pre: is_finite(pre) IMPLIES empty?(pre)

  prefix_below: THEOREM
    FORALL pre: empty?(pre) OR full?(pre) OR (EXISTS i: pre = below(i))

  prefix_upto: THEOREM
    FORALL pre: empty?(pre) OR full?(pre) OR (EXISTS i: pre = upto(i))

  suffix_empty: THEOREM FORALL suf: is_finite(suf) IMPLIES empty?(suf)

  suffix_upfrom: THEOREM
    FORALL suf: empty?(suf) OR full?(suf) OR (EXISTS i: suf = upfrom(i))

  suffix_above: THEOREM
    FORALL suf: empty?(suf) OR full?(suf) OR (EXISTS i: suf = above(i))

  unrelated_empty: THEOREM FORALL i: empty?(unrelated(i, <=))

END ordered_int

quality94%

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