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