Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

Great! sure, I’ll do that! —Chun > Il giorno 05 ott 2017, alle ore 23:16, Ramana Kumar > ha scritto: > > I think it would be good to add this UNIQUE constant to listTheory, if you > have time to make a pull request. > > On 6 October 2017 at 01:49, Chun Tian

Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

I think it would be good to add this UNIQUE constant to listTheory, if you have time to make a pull request. On 6 October 2017 at 01:49, Chun Tian (binghe) wrote: > Let me close this question (further comments are welcome, of course). > > I actually got another good

Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

Let me close this question (further comments are welcome, of course). I actually got another good definition from Robert Beers in a private email: [UNIQUE_DEF] Definition |- ∀x L. UNIQUE x L ⇔ ∃L1 L2. (L1 ⧺ [x] ⧺ L2 = L) ∧ ¬MEM x L1 ∧ ¬MEM x L2 This form is very useful for

Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

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

Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

Among others, LENGTH (FILTER (\e. X = e)) = 1 Scott > On 2017/10/05, at 15:55, Chun Tian (binghe) 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,

Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

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 > ha scritto: > > Hi Chun Tian, > > The constant ALL_DISTINCT in listTheory is

Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

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

Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

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) wrote: > Hi, > > (I'm new to HOL's listTheory). Suppose I have a list L which contains > possibly duplicated

[Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

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