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) <binghe.l...@gmail.com>
wrote:
> 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 me, because "¬MEM x L1 ∧ ¬MEM x L2” is
> exactly what I needed from the uniqueness. Then I tried to prove the
> following two alternative definitions using above definition, with success:
>
> [UNIQUE_ALT] Theorem
>
> |- ∀x L. UNIQUE x L ⇔ (FILTER ($= x) L = [x])
>
> [UNIQUE_ALT_COUNT] Theorem
>
> |- ∀x L. UNIQUE x L ⇔ (LIST_ELEM_COUNT x L = 1)
>
> where LIST_ELEM_COUNT is a constant defined in rich_listTheory:
>
> [LIST_ELEM_COUNT_DEF] Definition
>
> |- ∀e l. LIST_ELEM_COUNT e l = LENGTH (FILTER (λx. x = e) l)
>
> From UNIQUE_ALT it’s easy to derive UNIQUE_ALT_COUNT, but the other
> direction is more difficult. I attached my proof scripts in case anyone
> needs it. But I’m new to listTheory, my scripts are very ugly, sorry for
> that (they will become better once I’ve learnt more).
>
> Regards,
>
> Chun Tian
>
>
>
> > Il giorno 05 ott 2017, alle ore 16:03, Chun Tian (binghe) <
> binghe.l...@gmail.com> ha scritto:
> >
> > 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
>
>
------------------------------------------------------------------------------
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
