Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: EquivClass.thy Sprache: PVS

Original von: PVS^©

%-------------------------------------------------------------------------
%
%  Specialization of the ordered_subset theory to sets of integers.
%
%  For PVS version 3.2.  January 31, 2005
%  ---------------------------------------------------------------------
%      Author: Jerry James ([email protected]), 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

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.