| products/sources/formale Sprachen/PVS/orders/ (Beweissystem Isabelle Version 2025-1©) Datei vom 28.9.2014 mit Größe 3 kB |
|
Quelle pointwise_orders.pvs Sprache: PVS |
|||||||||
|
% A partial order on R induces a partial order on functions that range in R,
% called the pointwise order. The pointwise order preserves complete % lower semilattices, complete upper semilattices, and complete lattices. % % Author: Alfons Geser (geser@nianet.org), National Institute of Aerospace % Date: Dec 2004 pointwise_orders[ D, R: TYPE ]: THEORY BEGIN IMPORTING bounded_orders, skolemization[D, R], closure_ops x: VAR D r, s: VAR R rr: VAR set[R] f, g: VAR [D -> R] ff: VAR set[[D -> R]] nff: VAR non_empty_finite_set[[D -> R]] rel: VAR pred[[R,R]] alt: VAR (antisymmetric?[R]) % f is pointwise less than, or equal to, g if f(x) <= g(x) for all x. pointwise(rel)(f,g): bool = FORALL x: rel(f(x), g(x)) strictly_pointwise(rel): pred[[[D -> R], [D -> R]]] = irreflexive_kernel(pointwise(reflexive_closure(rel))) pointwise_preserves_reflexive: JUDGEMENT pointwise(rel: (reflexive?[R])) HAS_TYPE (reflexive?[[D -> R]]) pointwise_preserves_transitive: JUDGEMENT pointwise(rel: (transitive?[R])) HAS_TYPE (transitive?[[D -> R]]) pointwise_preserves_preorder: JUDGEMENT pointwise(lt: (preorder?[R])) HAS_TYPE (preorder?[[D -> R]]) pointwise_preserves_antisymmetric: JUDGEMENT pointwise(rel: (antisymmetric?[R])) HAS_TYPE (antisymmetric?[[D -> R]]) pointwise_preserves_partial_order: JUDGEMENT pointwise(lt: (partial_order?[R])) HAS_TYPE (partial_order?[[D -> R]]) % if nff is non-empty and finite, then so is every set of the form % {s | EXISTS f: nff(f) & s = f(x)} for any x finiteness_lemma: LEMMA nonempty?[R]({s | EXISTS f: nff(f) & s = f(x)}) AND is_finite[R]({s | EXISTS f: nff(f) & s = f(x)}) least_upper_bound_pointwise: THEOREM least_upper_bound?[[D -> R]](f, ff, pointwise(rel)) IFF FORALL x: least_upper_bound?[R](f(x), {s | EXISTS f: ff(f) AND s = f(x)}, rel) least_bounded_above_pointwise: LEMMA least_bounded_above?[[D -> R]](ff, pointwise(rel)) IFF FORALL x: least_bounded_above?[R]({s | EXISTS f: ff(f) AND s = f(x)}, rel) pointwise_preserves_upper_semilattices: JUDGEMENT pointwise(lt: (upper_semilattice?[R])) HAS_TYPE (upper_semilattice?[[D -> R]]) pointwise_preserves_complete_upper_semilattices: JUDGEMENT pointwise(lt: (complete_upper_semilattice?[R])) HAS_TYPE (complete_upper_semilattice?[[D -> R]]) greatest_lower_bound_pointwise: LEMMA greatest_lower_bound?[[D -> R]](f, ff, pointwise(rel)) IFF FORALL x: greatest_lower_bound?[R](f(x), {s | EXISTS f: ff(f) & s = f(x)}, rel) greatest_bounded_below_pointwise: LEMMA greatest_bounded_below?(ff, pointwise(alt)) IFF (FORALL x: greatest_bounded_below?(alt)({s | EXISTS f: ff(f) & s = f(x)})) pointwise_preserves_lower_semilattices: JUDGEMENT pointwise(lt: (lower_semilattice?[R])) HAS_TYPE (lower_semilattice?[[D -> R]]) pointwise_preserves_complete_lower_semilattices: JUDGEMENT pointwise(lt: (complete_lower_semilattice?[R])) HAS_TYPE (complete_lower_semilattice?[[D -> R]]) pointwise_preserves_lattices: JUDGEMENT pointwise(lt: (lattice?[R])) HAS_TYPE (lattice?[[D -> R]]) pointwise_preserves_complete_lattices: JUDGEMENT pointwise(lt: (complete_lattice?[R])) HAS_TYPE (complete_lattice?[[D -> R]]) lub_pointwise_def: LEMMA (FORALL x: least_bounded_above?(alt)({s | EXISTS f: ff(f) & s = f(x)})) => lub[[D -> R]](pointwise(alt))(ff) = LAMBDA x: lub[R](alt)({s | EXISTS f: ff(f) & s = f(x)}) glb_pointwise_def: LEMMA (FORALL x: greatest_bounded_below?(alt)({s | EXISTS f: ff(f) & s = f(x)})) => glb[[D -> R]](pointwise(alt))(ff) = LAMBDA x: glb[R](alt)({s | EXISTS f: ff(f) & s = f(x)}) END pointwise_orders ¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28