Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Thinking Intellekt

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/PVS/vectors/

Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: cauchy_scaf.prf Sprache: Lisp

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