Quelle relations_closure.pvs Sprache: PVS

%%-------------------** Abstract Reduction System (ARS) **-------------------
%%
%% Authors         : Andre Luiz Galdino
%%                   Universidade Federal de Goiás - Brasil
%%
%%                         and
%%
%%                   Mauricio Ayala Rincon
%%                   Universidade de Brasília - Brasil
%%
%% Last Modified On: December 02, 2006
%%
%%---------------------------------------------------------------------------

%%---------------------------------------------------------------------------
%%
%% We defined reflexive, symmetric, transitive, reflexive and transitive,
%% and equivalence closures of a binary relation in the same way that
%% Alfons Geser defined in .../lib/../closure_ops.pvs. We just changed
%% the names of the definitions and we proved some additional properties.
%%
%%---------------------------------------------------------------------------

relations_closure[T : TYPE] : THEORY
BEGIN

IMPORTING
    orders@closure_ops[T],
    sets_lemmas[T]

   S, R: VAR pred[[T, T]]
   n: VAR nat
   p: VAR posnat

   reflexive: TYPE = (reflexive?)

   symmetric: TYPE = (symmetric?)

   transitive: TYPE = (transitive?)

   reflexive_transitive?(R): bool = reflexive?(R) & transitive?(R)

   reflexive_transitive: TYPE = (reflexive_transitive?)

   equivalence: TYPE = (equivalence?)

% % Reflexive Closure (RC)

    RC(R): reflexive = union(R, =)

% %% Properties

   change_to_RC : LEMMA reflexive_closure(R) = RC(R)

   R_subset_RC : LEMMA subset?(R, RC(R))

   RC_idempotent : LEMMA  RC(RC(R)) = RC(R)

   RC_characterization : LEMMA  reflexive?(S) <=> (S = RC(S))

% % Symmetric Closure (SC)

    SC(R): symmetric = union(R, converse(R))

% %% Properties

   change_to_SC : LEMMA symmetric_closure(R) = SC(R)

   R_subset_SC : LEMMA subset?(R, SC(R))

   SC_idempotent : LEMMA  SC(SC(R)) = SC(R)

   SC_characterization : LEMMA  symmetric?(S) <=> (S = SC(S))

% % Transitive Closure (TC)

    TC(R): transitive = IUnion(LAMBDA p: iterate(R, p))

% %% Properties

   change_to_TC : LEMMA transitive_closure(R) = TC(R)

   R_subset_TC :LEMMA subset?(R, TC(R))

   TC_converse: LEMMA  TC(converse(R)) = converse(TC(R))

   TC_idempotent : LEMMA  TC(TC(R)) = TC(R)

   TC_characterization : LEMMA  transitive?(S) <=> (S = TC(S))



% % Reflexive Transitive Closure (RTC)

   RTC(R): reflexive_transitive = IUnion(LAMBDA n: iterate(R, n))

% %% Properties

   change_to_RTC : LEMMA preorder_closure(R) = RTC(R)

   R_subset_RTC: LEMMA subset?(R, RTC(R))

   iterate_RTC: LEMMA FORALL n : subset?(iterate(R, n), RTC(R))

   RTC_idempotent : LEMMA  RTC(RTC(R)) = RTC(R)

   RTC_characterization : LEMMA reflexive_transitive?(S) <=> (S = RTC(S))

% % Equivalence Closure (EC)

    EC(R): equivalence = RTC(SC(R))

% %% Properties

    change_to_EC : LEMMA equivalence_closure(R) = EC(R)

    R_subset_EC: LEMMA subset?(R, EC(R))

    RTC_subset_EC: LEMMA subset?(RTC(R), EC(R))

    EC_idempotent : LEMMA  EC(EC(R)) = EC(R)

    EC_characterization : LEMMA  equivalence?(S) <=> (S = EC(S))

END relations_closure

quality83%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.