The two definitions are not equivalent. The BIJ overload permits functions to
be designated permutations that the definition does not. BIJ can be used to
identify bijections between different types so it can't/shouldn't require
anything much of functions outside their domain. I think one's choice of
definition will depend on the sort of theorems one wants to prove. In
particular, the definition approach only lets one function serve as a
particular permutation. The BIJ-overload approach will let many functions be
the "same" permutation.
Michael
On 28/5/18, 19:01, "Chun Tian" <binghe.l...@gmail.com> wrote:
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
------------------------------------------------------------------------------
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
