OK, thanks everyone! So FILTER is what I must use. I think I’m going to use ``(FILTER (\e. e = X) L = [X])`` to assert the unique appearance of X in list L, and after I split the list using MEM_SPLIT, my target props (~MEM X l1) could be re-expressed by EVERY and FILTER, then it may be provable for me.
—Chun > Il giorno 05 ott 2017, alle ore 17:03, Scott Owens <[email protected]> ha > scritto: > > Among others, LENGTH (FILTER (\e. X = e)) = 1 > > Scott > >> On 2017/10/05, at 15:55, Chun Tian (binghe) <[email protected]> wrote: >> >> But my list is not ALL_DISTINCT … there’re duplicated elements for sure, >> just the appearance of certain element is only one. —Chun >> >>> Il giorno 05 ott 2017, alle ore 16:48, Konrad Slind >>> <[email protected]> ha scritto: >>> >>> Hi Chun Tian, >>> >>> The constant ALL_DISTINCT in listTheory is what you are looking for, I >>> think. >>> >>> Konrad. >>> >>> >>> On Thu, Oct 5, 2017 at 9:03 AM, Chun Tian (binghe) <[email protected]> >>> wrote: >>> Hi, >>> >>> (I'm new to HOL's listTheory). Suppose I have a list L which contains >>> possibly duplicated elements, and I want to express certain element X is >>> unique (i.e. has only one copy) in that list. How can I do this? It seems >>> "?!" doesn't work here, e.g. ``?!e. MEM e L /\ (e = X)``. >>> >>> Regards, >>> >>> Chun Tian >>> >>> -- >>> Chun Tian (binghe) >>> University of Bologna (Italy) >>> >>> >>> ------------------------------------------------------------------------------ >>> 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 >>> [email protected] >>> https://lists.sourceforge.net/lists/listinfo/hol-info >>> >>> >> >> ------------------------------------------------------------------------------ >> 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 >> [email protected] >> 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 [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
