| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/orders/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 9 kB |
|
Quelle bounded_orders.pvs Sprache: PVS |
|||||||||
|
% Upper and lower bounds on subsets; lub, glb;
% (complete) upper and lower semilattices; (complete) lattices % % Author: Alfons Geser (geser@nianet.org), National Institute of Aerospace % Date: Oct 2004 / Jan 2005 % % lub_singleton, least_upper_bound_singleton, glb_singleton, and % greates_lower_bound_singleton added 23 Feb 2005 by Jerry James % <jamesj@acm.org>, University of Kansas. bounded_orders[T: TYPE]: THEORY BEGIN IMPORTING sets[T], finite_sets[T], relations_extra[T] t, u, r: VAR T S, R: VAR set NF: VAR non_empty_finite_set <=: VAR pred[[T,T]] % ========================================================================== % Upper bounds % ========================================================================== upper_bound?(t, S, <=): bool = FORALL (r: (S)): r <= t upper_bound?(S, <=)(t): MACRO bool = upper_bound?(t, S, <=) bounded_above?(S, <=): bool = EXISTS t: upper_bound?(t, S, <=) bounded_above?(<=)(S): MACRO bool = bounded_above?(S, <=) least_upper_bound?(t, S, <=): bool = upper_bound?(t, S, <=) AND (FORALL r: upper_bound?(r, S, <=) => t <= r) least_upper_bound?(S, <=)(t): MACRO bool = least_upper_bound?(t, S, <=) least_bounded_above?(S, <=): bool = EXISTS t: least_upper_bound?(t, S, <=) least_bounded_above?(<=)(S): MACRO bool = least_bounded_above?(S, <=) complete_upper_semilattice?(<=): bool = partial_order?(<=) AND FORALL S: least_bounded_above?(S, <=) upper_semilattice?(<=): bool = partial_order?(<=) AND FORALL NF: least_bounded_above?(NF, <=) lub(<=)(S: (least_bounded_above?(<=))): (least_upper_bound?(S, <=)) % Properties unique_least_upper_bound: THEOREM FORALL (<=: (antisymmetric?[T]), t, r: (least_upper_bound?(S, <=))): t = r subset_upper_bound: LEMMA (subset?(S, R) AND upper_bound?(t, R, <=)) => upper_bound?(t, S, <=) subset_least_upper_bound: COROLLARY subset?(S, R) AND least_upper_bound?(t, R, <=) AND least_upper_bound?(r, S, <=) IMPLIES r <= t lub_def: LEMMA FORALL (<=: (antisymmetric?[T]), S: (least_bounded_above?(<=))): (lub(<=)(S) = t IFF least_upper_bound?(S, <=)(t)) lub_eq: LEMMA FORALL (<=: (antisymmetric?[T]), S: (least_bounded_above?(<=)), t: (least_upper_bound?(S, <=))): lub(<=)(S) = t lub_ge: LEMMA FORALL (S: (least_bounded_above?(<=)), t: (S)): t <= lub(<=)(S) lub_le: LEMMA FORALL (<=: (transitive?[T]), S: (least_bounded_above?(<=))): (lub(<=)(S) <= t IFF upper_bound?(S, <=)(t)) all_least_bounded: LEMMA FORALL (<=: (complete_upper_semilattice?)): least_bounded_above?(S, <=) all_finite_least_bounded: LEMMA FORALL (<=: (upper_semilattice?)): least_bounded_above?(NF, <=) complete_upper_semilattice_upper: JUDGEMENT (complete_upper_semilattice?) SUBTYPE_OF (upper_semilattice?) upper_semilattice_is_partial_order: JUDGEMENT (upper_semilattice?) SUBTYPE_OF (partial_order?) % ========================================================================== % Lower bounds % ========================================================================== lower_bound?(t, S, <=): bool = FORALL (r: (S)): t <= r lower_bound?(S, <=)(t): MACRO bool = lower_bound?(t, S, <=) bounded_below?(S, <=): bool = EXISTS t: lower_bound?(t, S, <=) bounded_below?(<=)(S): MACRO bool = bounded_below?(S, <=) greatest_lower_bound?(t, S, <=): bool = lower_bound?(t, S, <=) AND (FORALL r: lower_bound?(r, S, <=) => r <= t) greatest_lower_bound?(S, <=)(t): MACRO bool = greatest_lower_bound?(t, S, <=) greatest_bounded_below?(S, <=): bool = EXISTS t: greatest_lower_bound?(t, S, <=) greatest_bounded_below?(<=)(S): MACRO bool = greatest_bounded_below?(S, <=) complete_lower_semilattice?(<=): bool = partial_order?(<=) AND FORALL S: greatest_bounded_below?(S, <=) lower_semilattice?(<=): bool = partial_order?(<=) AND FORALL NF: greatest_bounded_below?(NF, <=) glb(<=)(S: (greatest_bounded_below?(<=))): (greatest_lower_bound?(S, <=)) % Properties unique_greatest_lower_bound: THEOREM FORALL (<=: (antisymmetric?[T]), t, r: (greatest_lower_bound?(S, <=))): t = r subset_lower_bound: LEMMA FORALL S, R, t: (subset?(S, R) AND lower_bound?(t, R, <=)) => lower_bound?(t, S, <=) subset_greatest_lower_bound: COROLLARY subset?(S, R) AND greatest_lower_bound?(t, S, <=) AND greatest_lower_bound?(r, R, <=) IMPLIES r <= t glb_def: LEMMA FORALL (<=: (antisymmetric?[T]), S: (greatest_bounded_below?(<=))): (glb(<=)(S) = t IFF greatest_lower_bound?(S, <=)(t)) glb_eq: LEMMA FORALL (<=: (antisymmetric?[T]), S: (greatest_bounded_below?(<=)), t: (greatest_lower_bound?(S, <=))): glb(<=)(S) = t glb_le: LEMMA FORALL (S: (greatest_bounded_below?(<=)), t: (S)): glb(<=)(S) <= t glb_ge: LEMMA FORALL (<=: (transitive?[T]), S: (greatest_bounded_below?(<=))): (t <= glb(<=)(S) IFF lower_bound?(S, <=)(t)) all_greatest_bounded: LEMMA FORALL (<=: (complete_lower_semilattice?)): greatest_bounded_below?(S, <=) all_finite_greatest_bounded: LEMMA FORALL (<=: (lower_semilattice?)): greatest_bounded_below?(NF, <=) complete_lower_semilattice_lower: JUDGEMENT (complete_lower_semilattice?) SUBTYPE_OF (lower_semilattice?) lower_semilattice_is_partial_order: JUDGEMENT (lower_semilattice?) SUBTYPE_OF (partial_order?) % ========================================================================== % Upper and lower bounds % ========================================================================== bounded?(S, <=): bool = bounded_above?(S, <=) AND bounded_below?(S, <=) bounded?(<=)(S): MACRO bool = bounded?(S, <=) tightly_bounded?(S, <=): bool = least_bounded_above?(S, <=) AND greatest_bounded_below?(S, <=) tightly_bounded?(<=)(S): MACRO bool = tightly_bounded?(S, <=) complete_lattice?(<=): bool = complete_upper_semilattice?(<=) AND complete_lower_semilattice?(<=) lattice?(<=): bool = upper_semilattice?(<=) AND lower_semilattice?(<=) bounded_is_bounded_above: JUDGEMENT (bounded?) SUBTYPE_OF (bounded_above?) bounded_is_bounded_below: JUDGEMENT (bounded?) SUBTYPE_OF (bounded_below?) tightly_bounded_above: JUDGEMENT (tightly_bounded?) SUBTYPE_OF (least_bounded_above?) tightly_bounded_below: JUDGEMENT (tightly_bounded?) SUBTYPE_OF (greatest_bounded_below?) complete_lattice_upper: JUDGEMENT (complete_lattice?) SUBTYPE_OF (complete_upper_semilattice?) complete_lattice_lower: JUDGEMENT (complete_lattice?) SUBTYPE_OF (complete_lower_semilattice?) lattice_upper: JUDGEMENT (lattice?) SUBTYPE_OF (upper_semilattice?) lattice_lower: JUDGEMENT (lattice?) SUBTYPE_OF (lower_semilattice?) complete_lattice_is_lattice: JUDGEMENT (complete_lattice?) SUBTYPE_OF (lattice?) % bounds of singleton sets upper_bound_singleton: LEMMA upper_bound?[T](t, singleton(u), <=) IFF u <= t least_upper_bound_singleton: LEMMA FORALL (<=: (reflexive?)): least_upper_bound?[T](t, singleton(t), <=) lub_singleton: LEMMA FORALL (<=: (partial_order?)): lub(<=)(singleton(u)) = u lower_bound_singleton: LEMMA lower_bound?[T](t, singleton(u), <=) IFF t <= u greatest_lower_bound_singleton: LEMMA FORALL (<=: (reflexive?)): greatest_lower_bound?[T](t, singleton(t), <=) glb_singleton: LEMMA FORALL (<=: (partial_order?)): glb(<=)(singleton(u)) = u % bounds of the empty set upper_bound_emptyset: LEMMA upper_bound?(t, emptyset, <=) lower_bound_emptyset: LEMMA lower_bound?(t, emptyset, <=) lub_emptyset_is_glb_fullset: THEOREM least_upper_bound?(t, emptyset, <=) IFF greatest_lower_bound?(t, fullset, <=) glb_emptyset_is_lub_fullset: THEOREM greatest_lower_bound?(t, emptyset, <=) IFF least_upper_bound?(t, fullset, <=) least_bounded_above_emptyset: COROLLARY least_bounded_above?(emptyset, <=) IFF greatest_bounded_below?(fullset, <=) greatest_bounded_below_emptyset: COROLLARY greatest_bounded_below?(emptyset, <=) IFF least_bounded_above?(fullset, <=) % --------- New content from David Lester nonempty_least_bounded_above?(<=)(S):bool = nonempty?(S) AND least_bounded_above?(<=)(S) nonempty_greatest_bounded_below?(<=)(S):bool = nonempty?(S) AND greatest_bounded_below?(<=)(S) le_lub: LEMMA FORALL (<=:(partial_order?),S,R:(least_bounded_above?(<=))): (FORALL (s:(S)): EXISTS (r:(R)): s <= r) IMPLIES lub(<=)(S) <= lub(<=)(R) eq_lub: LEMMA FORALL (<=:(partial_order?),S,R:(least_bounded_above?(<=))): (FORALL (s:(S)): EXISTS (r:(R)): s <= r) AND (FORALL (r:(R)): EXISTS (s:(S)): r <= s) IMPLIES lub(<=)(S) = lub(<=)(R) lub_add: LEMMA FORALL (<=:(partial_order?),S:(least_bounded_above?(<=))): lub(<=)(add(lub(<=)(S),S)) = lub(<=)(S) le_glb: LEMMA FORALL (<=:(partial_order?),S,R:(greatest_bounded_below?(<=))): (FORALL (r:(R)): EXISTS (s:(S)): s <= r) IMPLIES glb(<=)(S) <= glb(<=)(R) eq_glb: LEMMA FORALL (<=:(partial_order?),S,R:(greatest_bounded_below?(<=))): (FORALL (s:(S)): EXISTS (r:(R)): r <= s) AND (FORALL (r:(R)): EXISTS (s:(S)): s <= r) IMPLIES glb(<=)(S) = glb(<=)(R) glb_add: LEMMA FORALL (<=:(partial_order?),S:(greatest_bounded_below?(<=))): glb(<=)(add(glb(<=)(S),S)) = glb(<=)(S) END bounded_orders ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28