Great! sure, I’ll do that! —Chun > Il giorno 05 ott 2017, alle ore 23:16, Ramana Kumar > <[email protected]> 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 (binghe) <[email protected]> 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) > > <[email protected]> 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 > [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
