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
extra_listScript.sml
Description: application/smil
> 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) >
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
