| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/orders/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 4 kB |
|
Quelle minmax_orders.pvs Sprache: PVS |
|||||||||
|
% Maximal, greatest, minimal, least elements on subsets, and their
% correlation with least upper and greatest lower bounds. % % Author: Alfons Geser (geser@nianet.org), National Institute of Aerospace % Date: Oct 2004 / Jan 2005 minmax_orders[T: TYPE]: THEORY BEGIN IMPORTING bounded_orders[T], finite_sets@finite_sets_minmax t, r: VAR T S: VAR set F: VAR finite_set NF: VAR non_empty_finite_set[T] <=, R: VAR pred[[T,T]] le: VAR (total_order?[T]) ale: VAR (antisymmetric?[T]) tle: VAR (dichotomous?[T]) % ========================================================================== % Maximal/greatest elements % ========================================================================== % Maximal elements maximal?(t, S, <=): bool = S(t) AND NOT (EXISTS (r: (S)): t <= r AND t /= r) % S(t) AND NOT lower_bound(t, S, irreflexive_kernel(<=)) maximal?(S, <=)(t): MACRO bool = maximal?(t, S, <=) has_maximal?(S, <=): bool = EXISTS t: maximal?(t, S, <=) % Greatest elements greatest?(t, S, <=): bool = S(t) AND upper_bound?(t, S, <=) greatest?(S, <=)(t): MACRO bool = greatest?(t, S, <=) has_greatest?(S, <=): bool = EXISTS t: greatest?(t, S, <=) has_greatest?(<=)(S): MACRO bool = has_greatest?(S, <=) greatest(<=)(S: (has_greatest?(<=))): {t: (S) | greatest?(t, S, <=)} % Properties greatest_iff_least_upper_bound: LEMMA greatest?(t, S, <=) IFF least_upper_bound?(t, S, <=) AND S(t) greatest_is_least_upper_bound: JUDGEMENT (greatest?) SUBTYPE_OF (least_upper_bound?) has_greatest_is_least_bounded_above: JUDGEMENT (has_greatest?) SUBTYPE_OF (least_bounded_above?) greatest_equals_lub: LEMMA FORALL (S: (has_greatest?(ale))): greatest(ale)(S) = lub(ale)(S) greatest_unique: LEMMA FORALL (<=: (antisymmetric?[T]), (s, t: (greatest?(S, <=)))): s = t greatest_is_maximal: LEMMA greatest?(t, S, ale) => maximal?(t, S, ale) maximal_is_greatest: LEMMA maximal?(t, S, tle) => greatest?(t, S, tle) non_empty_finite_has_greatest: LEMMA has_greatest?(NF, le) greatest_ge: LEMMA FORALL (S: (has_greatest?(<=)), m: (S)): m <= greatest(<=)(S) greatest_monotone: LEMMA FORALL (S1, S2: (has_greatest?(<=))): subset?(S1, S2) => greatest(<=)(S1) <= greatest(<=)(S2) greatest_def: LEMMA FORALL (S: (has_greatest?(ale))): greatest(ale)(S) = t IFF greatest?(t, S, ale) greatest_upper_bound: LEMMA FORALL (<=: (partial_order?[T]), S: (has_greatest?(<=))): greatest(<=)(S) <= t IFF upper_bound?[T](t, S, <=) % ========================================================================== % Minimal/least elements % ========================================================================== % Minimal elements minimal?(t, S, <=): bool = S(t) AND NOT (EXISTS (r: (S)): r <= t AND t /= r) minimal?(S, <=)(t): MACRO bool = minimal?(t, S, <=) has_minimal?(S, <=): bool = EXISTS t: minimal?(t, S, <=) % Least elements least?(t, S, <=): bool = S(t) AND lower_bound?(t, S, <=) least?(S, <=)(t): MACRO bool = least?(t, S, <=) has_least?(S, <=): bool = EXISTS t: least?(t, S, <=) has_least?(<=)(S): MACRO bool = has_least?(S, <=) least(<=)(S: (has_least?(<=))): {t: (S) | least?(t, S, <=)} % Properties least_iff_greatest_lower_bound: LEMMA least?(t, S, <=) IFF greatest_lower_bound?(t, S, <=) AND S(t) least_is_greatest_lower_bound: JUDGEMENT (least?) SUBTYPE_OF (greatest_lower_bound?) has_least_is_greatest_bounded_below: JUDGEMENT (has_least?) SUBTYPE_OF (greatest_bounded_below?) least_equals_glb: LEMMA FORALL (S: (has_least?(ale))): least(ale)(S) = glb(ale)(S) least_unique: LEMMA FORALL (<=: (antisymmetric?[T]), (s, t: (least?(S, <=)))): s = t least_is_minimal: LEMMA least?(t, S, ale) => minimal?(t, S, ale) minimal_is_least: LEMMA minimal?(t, S, tle) => least?(t, S, tle) non_empty_finite_has_least: LEMMA has_least?(NF, le) least_le: LEMMA FORALL (S: (has_least?(<=)), m: (S)): least(<=)(S) <= m least_monotone: LEMMA FORALL (S1, S2: (has_least?(<=))): subset?(S1, S2) => least(<=)(S2) <= least(<=)(S1) least_def: LEMMA FORALL (S: (has_least?(ale))): least(ale)(S) = t IFF least?(t, S, ale) least_lower_bound: LEMMA FORALL (<=: (partial_order?[T]), S: (has_least?(<=))): t <= least(<=)(S) IFF lower_bound?[T](t, S, <=) % ========================================================================== % Both greatest and least elements exist % ========================================================================== has_extrema?(S, <=): bool = has_greatest?(S, <=) AND has_least?(S, <=) % bounded_type?(<=): bool = has_extrema?(fullset, <=) has_extrema_has_greatest: JUDGEMENT (has_extrema?) SUBTYPE_OF (has_greatest?) has_extrema_has_least: JUDGEMENT (has_extrema?) SUBTYPE_OF (has_least?) total_order_is_lattice: JUDGEMENT (total_order?) SUBTYPE_OF (lattice?) END minmax_orders ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28