|
doubletons[T: TYPE]: THEORY
BEGIN
x,y,z: VAR T
dbl(x,y): set[T] = {t: T | t = x OR t = y}
S: VAR set[T]
doubleton?(S): bool = (EXISTS x,y: x /= y AND S = dbl(x,y))
doubleton: TYPE = {S | EXISTS x,y: x /= y AND S = dbl(x,y)}
Dbl: TYPE = doubleton
dbl_comm: LEMMA dbl(x,y) = dbl(y,x)
D: VAR doubleton
doubleton_irreflexive : LEMMA NOT doubleton?(dbl(x,x))
doubleton_nonempty : LEMMA nonempty?(D)
doubleton_rest_nonempty: LEMMA nonempty?(rest(D))
dbl_choose : LEMMA choose(dbl(x,y)) = x or choose(dbl(x,y)) = y
dbl_rest_choose : LEMMA x /= y IMPLIES
(choose(dbl(x,y)) /= choose(rest(dbl(x,y)))) AND
(choose(rest(dbl(x,y))) = x
OR choose(rest(dbl(x,y))) = y)
dbl_to_pair(D) : {(x,y) | D = dbl(x,y)}
dbl_def : LEMMA dbl(PROJ_1(dbl_to_pair(D)), PROJ_2(dbl_to_pair(D))) = D
dbl_in : LEMMA D = dbl(x,y) IMPLIES D(x) AND D(y)
dbl_not_in : LEMMA D = dbl(x,y) AND z /= x AND z /= y IMPLIES NOT D(z)
dbl_to_pair_lem : LEMMA x /= y IMPLIES
dbl_to_pair(dbl(x,y)) = (x,y) OR
dbl_to_pair(dbl(x,y)) = (y,x)
dbl_to_pair_inverse_l : LEMMA dbl(dbl_to_pair(D)) = D
dbl_proj : LEMMA D(PROJ_1(dbl_to_pair(D))) AND
D(PROJ_2(dbl_to_pair(D)))
v: VAR T
proj_dbl: LEMMA (PROJ_1(dbl_to_pair(D)) = v OR PROJ_2(dbl_to_pair(D)) = v)
IMPLIES D(v)
dbl_eq: LEMMA dbl(x,y) = dbl(v,z) IMPLIES
(x = v AND y = z) OR (x = z AND y = v)
finite_dbl: LEMMA is_finite(dbl(x,y))
e: VAR doubleton
finite_doubleton: LEMMA is_finite(e)
card_dbl: LEMMA x /= y IMPLIES card(dbl(x,y)) = 2
JUDGEMENT dbl(x,y) HAS_TYPE finite_set[T]
AUTO_REWRITE+ doubleton_irreflexive % NOT doubleton?(dbl(x,x))
AUTO_REWRITE+ doubleton_nonempty % nonempty?(D)
AUTO_REWRITE+ dbl_def % dbl(PROJ_1(dbl_to_pair(D)),
% PROJ_2(dbl_to_pair(D))) = D
AUTO_REWRITE+ dbl_to_pair_inverse_l % dbl(dbl_to_pair(D)) = D
AUTO_REWRITE+ dbl_proj
AUTO_REWRITE+ finite_dbl
AUTO_REWRITE+ finite_doubleton
% ------------- The following two cause wierd PVS bug -------
AUTO_REWRITE+ dbl_in % D = dbl(x,y) IMPLIES D(x) AND D(y)
AUTO_REWRITE+ dbl_not_in % D = dbl(x,y) AND z /= x AND z /= y
rev(fs: finseq[T]): finseq[T] = (# length := length(fs),
seq := (LAMBDA (i: below(length(fs))): seq(fs)(length(fs)-1-i))
#)
END doubletons
¤ Dauer der Verarbeitung: 0.26 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.
|
