Hi Michael, thanks for detailed explanations. Then I guess I should choose another name for the conflicted symbols in the PR.
—Chun
> Il giorno 28 mag 2018, alle ore 11:55, <michael.norr...@data61.csiro.au>
> <michael.norr...@data61.csiro.au> ha scritto:
>
> 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
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
