Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: ordered_nat.pvs Sprache: PVS

Original von: PVS^©

%-------------------------------------------------------------------------
%
%  Specializations of the ordered_subset theory to sets of natural numbers.
%
%  For PVS version 3.2.  February 8, 2005
%  ---------------------------------------------------------------------
%      Author: Jerry James ([email protected]), University of Kansas
%
%  EXPORTS
%  -------
%  prelude: finite_sets[nat], infinite_sets_def[nat], orders[nat],
%    real_props, relation_props2[nat,nat,nat,nat], relations[nat],
%    restrict_order_props[real,nat], sets[nat]
%  finite_sets: finite_sets_inductions, finite_sets_minmax
%  orders: bounded_integers[nat], bounded_nats[nat], bounded_orders[nat],
%    bounded_sets[nat,<=], closure_ops[nat], indexed_sets_extra,
%    lattices[nat,<=], lower_semilattices[nat,<=], minmax_orders[nat],
%    non_empty_bounded_sets[nat], ordered_nat, ordered_subset[nat],
%    relation_iterate[nat], relations_extra[nat], total_lattices[nat,<=],
%    upper_semilattices[nat,<=]
%
%-------------------------------------------------------------------------
ordered_nat: THEORY
BEGIN

  IMPORTING infinite_sets_def[nat], restrict_order_props[real, nat]
  IMPORTING real_props, ordered_subset[nat]
  IMPORTING bounded_nats[nat] % Proofs only

  n: VAR nat
  pre, pre1, pre2: VAR (prefix?(<=))
  suf: VAR (suffix?(<=))

  % A convenient shorthand
  lesseq: MACRO pred[[nat, nat]] =
      restrict[[real, real], [nat, nat], boolean](<=)

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

  upto_has_greatest: JUDGEMENT upto(n) HAS_TYPE (has_greatest?(lesseq))
  above_has_least: JUDGEMENT above(n) HAS_TYPE (has_least?(lesseq))
  upfrom_has_least: JUDGEMENT upfrom(n) HAS_TYPE (has_least?(lesseq))

  nonzero_below_greatest: LEMMA
    FORALL n:
      n > 0 IMPLIES
       has_greatest?(below(n), lesseq) AND
        greatest(lesseq)(below(n)) = n - 1

  upto_greatest: LEMMA FORALL n: greatest(lesseq)(upto(n)) = n
  above_least: LEMMA FORALL n: least(lesseq)(above(n)) = n + 1
  upfrom_least: LEMMA FORALL n: least(lesseq)(upfrom(n)) = n

  below_prelude: LEMMA
    FORALL n:
      below(n) =
       extend[nat, naturalnumbers.below(n), bool, FALSE]
           (fullset[naturalnumbers.below(n)])

  upto_prelude: LEMMA
    FORALL n:
      upto(n) =
       extend[nat, naturalnumbers.upto(n), bool, FALSE]
           (fullset[naturalnumbers.upto(n)])

  prefix_finite: THEOREM FORALL pre: is_finite(pre) OR full?(pre)

  prefix_below: THEOREM
    FORALL pre: is_finite(pre) IMPLIES pre = below(card(pre))

  prefix_upto: THEOREM
    FORALL pre:
      is_finite(pre) IMPLIES empty?(pre) OR pre = upto(card(pre) - 1)

  below_is_finite: JUDGEMENT below(n) HAS_TYPE finite_set
  upto_is_finite: JUDGEMENT upto(n) HAS_TYPE finite_set

  below_card: LEMMA FORALL n: card(below(n)) = n
  upto_card: LEMMA FORALL n: card(upto(n)) = 1 + n

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

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

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

  unrelated_empty: THEOREM FORALL n: empty?(unrelated(n, lesseq))

  prefix_finite_full: LEMMA
    FORALL pre1, pre2:
      is_finite(pre1) AND full?(pre2) IMPLIES
       (FORALL (f: [(pre1) -> (pre2)]): NOT surjective?(f))

  prefix_bijective: THEOREM
    FORALL pre1, pre2:
      (EXISTS (f: [(pre1) -> (pre2)]): bijective?(f)) IMPLIES pre1 = pre2

END ordered_nat

¤ 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.