Hi, (I’m trying to convert the current pending PR into acceptable code changes)
in pred_setTheory, I saw there’s a definition of PERMUTES (permutation
functions over a set) as overloading of BIJ (bijections):
val _ = overload_on("PERMUTES", ``\f s. BIJ f s s``);
val _ = set_fixity "PERMUTES" (Infix(NONASSOC, 450)); (* same as relation *)
val SUM_IMAGE_PERMUTES = store_thm(
"SUM_IMAGE_PERMUTES",
``!s. FINITE s ==> !g. g PERMUTES s ==> !f. SIGMA (f o g) s = SIGMA f s``,
…);
this definition seems clear: a function is a permutation over a set if it’s a
bijection from the set to itself. But let’s recall HOL is a logic of total
functions, and what about the value of this permutation function over values
NOT in the set? Does above definition automatically indicate ``f(x) = x`` for
all elements not in the set?
On the other side, I saw the following (possible) alternative definition: (in
that pending PR)
PERMUTES p s = (!x. ~(x IN s) ==> (p(x) = x)) /\ (!y. ?!x. p x = y)
it explicitly states that, for all values not in the set s, a permutation
function acts like identity function; and it must be a total bijection (c.f.
BIJ_ALT in pred_setTheory).
Are these two definitions really equivalent?
Regards,
Chun
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
