Hi Anthony, Thanks. This definition may work (at least I can see it’s correct), at least that’s what I can start with. But in my proof the next move will be using MEM_SPLIT to divide the list into three pieces:
[MEM_SPLIT] Theorem
|- ∀x l. MEM x l ⇔ ∃l1 l2. l = l1 ⧺ x::l2
and what I finally need are ``~MEM X l1`` and ``~MEM X l2``. But from FILTER
and LENGTH how can I reach my targets? A little hints may help me a lot …
Regards,
Chun
> Il giorno 05 ott 2017, alle ore 16:21, Anthony Fox <ac...@cam.ac.uk> ha
> scritto:
>
> Perhaps something like
>
> val unique_def = Define`unique x l = LENGTH (FILTER ($= x) l) = 1`
>
> is what you’re after?
>
> Anthony
>
>> On 5 Oct 2017, at 15:03, Chun Tian (binghe) <binghe.l...@gmail.com> 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
>> 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
