Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: closure_ops.pvs Sprache: PVS

Original von: PVS^©

% reflexive, symmetric, and transitive closures of a binary relation
% and their properties
%
% Author: Alfons Geser ([email protected]), 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 ([email protected]), 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) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.