Quellcode-Bibliothek ordered_nat.pvs

%-------------------------------------------------------------------------
%
%  Specializations of the ordered_subset theory to sets of natural numbers.
%
%  For PVS version 3.2.  February 8, 2005
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), 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