|
%--------------------------------------------------------------%
% 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.16 Sekunden
(vorverarbeitet)
¤
|
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.
|
