Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: test_rr.pvs Sprache: PVS

Original von: PVS^©

%--------------------------------------------------------------%
%   Author: Dragan Stosic                                      %
%--------------------------------------------------------------%

% domain:              finite
% codomain:            finite
% EquivClass domain:   finite
% EquivClass codomain: finite
singleton_example: THEORY
BEGIN
  T0: TYPE+ = {t}
  U0: TYPE+ = {u}
  IMPORTING relations[T0], relations[U0],
            rr_rel[T0, U0]

  ==(t0, t1: T0): bool = true;
  ==(u0, u1: U0): bool = true;
  g0: [T0 -> U0] = LAMBDA (t0: T0): u
  e0: [U0 -> T0] = LAMBDA (u0: U0): t
  ref0: predicate[[T0, U0]] = LAMBDA (p: [T0, U0]): true

relations_equality: LEMMA  RR(==,==, g0, e0) = ref0

relations_equality2: LEMMA RR2(==,==, g0, e0) = ref0

END singleton_example

% domain:              finite
% codomain:            finite
% EquivClass domain:   finite
% EquivClass codomain: finite
finite_nats_trivial: THEORY
BEGIN
  T1: TYPE+ = below(3)
  U1: TYPE+ = below(6)
  IMPORTING ints@div, relations[T1], relations[U1],
             rr_rel[T1, U1];

  ==(t0, t1: T1): bool = t0 = t1;
  ==(u0, u1: U1): bool = div(u0,2) = div(u1,2);

  g1: [T1 -> U1] = LAMBDA (t: T1): 2*t
  e1: [U1 -> T1] = LAMBDA (u: U1): div(u,2)
  ref1: predicate[[T1, U1]] =
    LAMBDA (p: [T1, U1]): 2*p`1 = p`2 OR 2*p`1+1 = p`2

  relations_equality: LEMMA  RR(==,==, g1, e1) = ref1

  relations_equality2: LEMMA RR2(==,==, g1, e1) = ref1

END finite_nats_trivial

% domain:              infinite
% codomain:            infinite
% EquivClass domain:   finite
% EquivClass codomain: infinite
infinite_to_infinite_trivial: THEORY
BEGIN
  IMPORTING ints@div
  T4: TYPE = nat
  U4: TYPE = nat
  IMPORTING relations[T4], relations[U4], rr_rel[T4, U4];

  equivT(t0, t1: T4): bool = div(t0,10) = div(t1,10)
  equivU(u0, u1: U4): bool = u0 = u1
  g4: [T4 -> U4] = LAMBDA (t: T4): div(t,10)
  e4: [U4 -> T4] = LAMBDA (u: U4): 10*u
  ref4: predicate[[T4, U4]] = LAMBDA (p: [T4, U4]): div(p`1,10) = p`2

  relations_equality: LEMMA  ref4 = RR(equivT, equivU, g4, e4)

  relations_equality2: LEMMA ref4 = RR2(equivT, equivU, g4, e4)

END infinite_to_infinite_trivial

% domain:              finite
% codomain:            infinite
% EquivClass domain:   finite
% EquivClass codomain: finite
finite_to_infinite: THEORY
BEGIN
  T6: TYPE = bool
  U6: TYPE = nat
  IMPORTING relations[T6], relations[U6],
            rr_rel[T6, U6]

  equivT(t0, t1: T6): bool = t0 = t1
  equivU(u0, u1: U6): bool = even?(u0) = even?(u1)
  g6: [T6 -> U6] = LAMBDA (t: T6): IF t THEN 0 ELSE 1 ENDIF
  e6: [U6 -> T6] = LAMBDA (u: U6): even?(u)
  ref6: predicate[[T6, U6]] = LAMBDA (p: [T6, U6]): p`1 = even?(p`2)

  relations_equality: LEMMA  ref6 = RR(equivT, equivU, g6, e6)

  relations_equality2: LEMMA  ref6 = RR2(equivT, equivU, g6, e6)

END finite_to_infinite

% domain:              infinite
% codomain:            finite
% EquivClass domain:   finite
% EquivClass codomain: finite
infinite_to_finite_finite_equival_finite_equival_classes : THEORY
BEGIN
  T7: TYPE = nat
  U7: TYPE = {0,1}
  IMPORTING relations[T7], relations[U7],
            rr_rel[T7, U7]

  equivT(t0, t1: T7): bool = even?(t0) = even?(t1)
  equivU(u0, u1: U7): bool = u0 = u1
  g7: [T7 -> U7] = LAMBDA (t: T7):  IF (even?(t)) THEN 0 ELSE 1 ENDIF
  e7: [U7 -> T7] = LAMBDA (u: U7): IF (u = 0) THEN 0 ELSE 1 ENDIF
  ref7: predicate[[T7, U7]] = LAMBDA (p: [T7, U7]):
                               IF (even?(p`1)) THEN p`2 = 0 ELSE p`2 = 1 ENDIF

  relations_equality: LEMMA  ref7 = RR(equivT, equivU, g7, e7)

  relations_equality2: LEMMA  ref7 = RR2(equivT, equivU, g7, e7)

END infinite_to_finite_finite_equival_finite_equival_classes

% domain:              infinite
% codomain:            finite
% EquivClass domain:   infinite
% EquivClass codomain: finite
infinite_to_finite_infinite_equival_finite_equival_classes: THEORY
BEGIN
  T8: TYPE+ = nat
  U8: TYPE+ = below(2)
  IMPORTING relations[T8], relations[U8],
            rr_rel[T8, U8]

  equivT(t0, t1: T8): bool = odd?(t0+1) = even?(t1) OR even?(t0) = even?(t1)
  equivU(u0, u1: U8): bool = odd?(u0+1) = even?(u1)
  g8: [T8 -> U8] = LAMBDA (t: T8): IF (even?(t)) THEN 0 ELSE 1 ENDIF
  e8: [U8 -> T8] = LAMBDA (u: U8): IF ( even?(u)) THEN 0 ELSE 1 ENDIF
  ref8: predicate[[T8, U8]] = LAMBDA (p: [T8, U8]):
                               IF ( even?(p`1)) THEN p`2 = 0 ELSE p`2 = 1 ENDIF

  relations_equality: LEMMA  ref8 = RR(equivT, equivU, g8, e8)

  relations_equality2: LEMMA  ref8 = RR2(equivT, equivU, g8, e8)

END infinite_to_finite_infinite_equival_finite_equival_classes

% domain:              infinite
% codomain:            infinite
% EquivClass domain:   infinite
% EquivClass codomain: infinite
infinite_to_infinite_infinite_equival_infinite_equival_classes: THEORY
BEGIN
  T9: TYPE = nat
  U9: TYPE = posnat
  IMPORTING relations[T9], relations[U9],
            rr_rel[T9, U9]

  equivT(t0, t1: T9): bool = t0 = t1
  equivU(u0, u1: U9): bool = u0 = u1
  g9: [T9 -> U9] = LAMBDA (t: T9): t+1
  e9: [U9 -> T9] = LAMBDA (u: U9): u-1
  ref9: predicate[[T9, U9]] = LAMBDA (p: [T9, U9]): p`1+1= p`2

  relations_equality: LEMMA  ref9 = RR(equivT, equivU, g9, e9)

  relations_equality2: LEMMA  ref9 = RR2(equivT, equivU, g9, e9)

END infinite_to_infinite_infinite_equival_infinite_equival_classes

% domain:              infinite
% codomain:            infinite
% EquivClass domain:   infinite
% EquivClass codomain: finite
infinite_to_infinite_infinite_equival_finite_equival_classes: THEORY
BEGIN
  IMPORTING ints@div
  T10: TYPE+ = nat
  U10: TYPE+ = nat
  IMPORTING relations[T10], relations[U10],
            rr_rel[T10, U10];

  equivT(t0, t1: T10): bool = t0 = t1
  equivU(u0, u1: U10): bool = div(u0,10) = div(u1,10)
  g10: [T10 -> U10] = LAMBDA (t: T10): 10*t
  e10: [U10 -> T10] = LAMBDA (u: U10): div(u,10)
  ref10: predicate[[T10, U10]] = LAMBDA (p: [T10, U10]): p`1=div(p`2,10)

  relations_equality: LEMMA  ref10 = RR(equivT, equivU, g10, e10)

  relations_equality2: LEMMA  ref10 = RR2(equivT, equivU, g10, e10)

END infinite_to_infinite_infinite_equival_finite_equival_classes

% domain:              finite
% codomain:            infinite
% EquivClass domain:   finite
% EquivClass codomain: infinite
finite_to_infinite_finite_equival_infinite_equival_classes: THEORY
BEGIN
  T11: TYPE+ = below(2)
  U11: TYPE+ = nat
  IMPORTING relations[T11], relations[U11],
             rr_rel[T11, U11];

  equivT(t0, t1: T11): bool = odd?(t0+1) = even?(t1)
  equivU(u0, u1: U11): bool = odd?(u0+1) = even?(u1) OR even?(u0) = even?(u1)
  g11: [T11 -> U11] = LAMBDA (t: T11): IF (even?(t)) THEN 0 ELSE 1 ENDIF
  e11: [U11 -> T11] = LAMBDA (u: U11): IF (even?(u)) THEN 0 ELSE 1 ENDIF
  ref11: predicate[[T11, U11]] = (LAMBDA (p: [T11, U11]):
                               IF (even?(p`2)) THEN p`1 = 0 ELSE p`1 = 1 ENDIF)

  relations_equality: LEMMA  ref11 = RR(equivT, equivU, g11, e11)

  relations_equality2: LEMMA  ref11 = RR2(equivT, equivU, g11, e11)

END finite_to_infinite_finite_equival_infinite_equival_classes

simplest_examples: THEORY
BEGIN
  IMPORTING singleton_example,
            finite_nats_trivial,
            infinite_to_infinite_trivial,
            finite_to_infinite,
            infinite_to_finite_finite_equival_finite_equival_classes,
            infinite_to_finite_infinite_equival_finite_equival_classes,
            infinite_to_infinite_infinite_equival_infinite_equival_classes,
            infinite_to_infinite_infinite_equival_finite_equival_classes,
            finite_to_infinite_finite_equival_infinite_equival_classes

END simplest_examples

¤ Dauer der Verarbeitung: 0.14 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.