| products/sources/formale Sprachen/PVS/orders/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: progtest.m4 Sprache: PVSOriginal 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) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
