| 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 closure_ops.pvs Sprache: PVS |
|||||||||
|
% reflexive, symmetric, and transitive closures of a binary relation
% and their properties % % Author: Alfons Geser (geser@nianet.org), National Institute of Aerospace % Date: Dec 2004 / Jan 2005 % % Rewriting identities added 19 Jan 2005, and generalization to order? added % 24 Feb 2005 by Jerry James (jamesj@acm.org), University of Kansas. closure_ops[T: TYPE]: THEORY BEGIN IMPORTING relation_iterate[T], indexed_sets_extra R, R1, R2: VAR pred[[T, T]] n: VAR nat p: VAR posnat % closures, i.e., least super-relations that satisfy a certain property % kernels, i.e., greatest sub-relations that satisfy a certain property reflexive_closure(R): (reflexive?) = union(R, =) irreflexive_kernel(R): (irreflexive?) = difference(R, =) symmetric_closure(R): (symmetric?) = union(R, converse(R)) symmetric_kernel(R): (symmetric?) = intersection(R, converse(R)) asymmetric_kernel(R): (asymmetric?) = difference(R, converse(R)) transitive_closure(R): (transitive?) = IUnion(LAMBDA p: iterate(R, p)) preorder_closure(R): (preorder?) = IUnion(LAMBDA n: iterate(R, n)) reflexive_irreflexive: LEMMA FORALL (R: (reflexive?)): reflexive_closure(irreflexive_kernel(R)) = R irreflexive_reflexive: LEMMA FORALL (R: (irreflexive?)): irreflexive_kernel(reflexive_closure(R)) = R reflexive_closure_preserves_transitive: JUDGEMENT reflexive_closure(R: (transitive?)) HAS_TYPE (preorder?) reflexive_closure_preserves_antisymmetric: JUDGEMENT reflexive_closure(R: (antisymmetric?)) HAS_TYPE (antisymmetric?) order_to_partial_order: JUDGEMENT reflexive_closure(R: (order?)) HAS_TYPE (partial_order?) reflexive_closure_dichotomous: JUDGEMENT reflexive_closure(R: (trichotomous?)) HAS_TYPE (dichotomous?) linear_order_to_total_order: JUDGEMENT reflexive_closure(R: (linear_order?)) HAS_TYPE (total_order?) order_to_strict_order: JUDGEMENT irreflexive_kernel(R: (order?)) HAS_TYPE (strict_order?) irreflexive_kernel_of_antisymmetric: JUDGEMENT irreflexive_kernel(R: (antisymmetric?)) HAS_TYPE (asymmetric?) irreflexive_kernel_trichotomous: JUDGEMENT irreflexive_kernel(R: (dichotomous?)) HAS_TYPE (trichotomous?) linear_order_to_strict_total_order: JUDGEMENT irreflexive_kernel(R: (total_order?)) HAS_TYPE (strict_total_order?) symmetric_kernel_of_preorder: JUDGEMENT symmetric_kernel(R: (preorder?)) HAS_TYPE (equivalence?) asymmetric_kernel_of_preorder: JUDGEMENT asymmetric_kernel(R: (preorder?)) HAS_TYPE (strict_order?) preorder_closure_converse: LEMMA preorder_closure(converse(R)) = converse(preorder_closure(R)) symmetry_char: LEMMA symmetric?[T](R) <=> subset?(R, converse(R)) transitive_closure_of_reflexive: JUDGEMENT transitive_closure(R: (reflexive?)) HAS_TYPE (preorder?) transitive_closure_is_monotone: LEMMA subset?(R1, R2) => subset?(transitive_closure(R1), transitive_closure(R2)) preorder_closure_is_monotone: LEMMA subset?(R1, R2) => subset?(preorder_closure(R1), preorder_closure(R2)) preorder_closure_preserves_symmetry: JUDGEMENT preorder_closure(R: (symmetric?)) HAS_TYPE (equivalence?) equivalence_closure(R): (equivalence?) = preorder_closure(symmetric_closure(R)) transitive_closure_step_r: THEOREM transitive_closure(R) = preorder_closure(R) o R transitive_closure_step_l: THEOREM transitive_closure(R) = R o preorder_closure(R) preorder_closure_reflexive_transitive: THEOREM preorder_closure(R) = reflexive_closure(transitive_closure(R)) preorder_closure_transitive_reflexive: THEOREM preorder_closure(R) = transitive_closure(reflexive_closure(R)) %% Rewriting identities / idempotency of the operators reflexive_closure_identity: LEMMA FORALL (<: (reflexive?)): reflexive_closure(<) = < irreflexive_kernel_identity: LEMMA FORALL (<: (irreflexive?)): irreflexive_kernel(<) = < symmetric_closure_identity: LEMMA FORALL (<: (symmetric?)): symmetric_closure(<) = < symmetric_kernel_identity: LEMMA FORALL (<: (symmetric?)): symmetric_kernel(<) = < asymmetric_kernel_identity: LEMMA FORALL (<: (asymmetric?)): asymmetric_kernel(<) = < transitive_closure_identity: LEMMA FORALL (<: (transitive?)): transitive_closure(<) = < preorder_closure_identity: LEMMA FORALL (<: (preorder?)): preorder_closure(<) = < preorder_closure_reflexive: LEMMA FORALL (<: (order?)): preorder_closure(<) = reflexive_closure(<) equivalence_closure_identity: LEMMA FORALL (<: (equivalence?)): equivalence_closure(<) = < END closure_ops ¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28