Hi, I’d like to close an old question. 3 months ago I was trying to define the free names in CCS process but failed to deal with list deletions. Today I found another way to delete elements from list, inspired by DROP:
val DELETE_ELEMENT_def = Define `
(DELETE_ELEMENT e [] = []) /\
(DELETE_ELEMENT e (x::l) = if (e = x) then DELETE_ELEMENT e l
else x::DELETE_ELEMENT e l)`;
And the previous definition suggested by Ramana based on FILTER now becomes a
theorem as alternative definition:
[DELETE_ELEMENT_FILTER] Theorem
|- ∀e L. DELETE_ELEMENT e L = FILTER (λy. e ≠ y) L
I found it’s easier to use the recursive definition, because many useful
results can be proved easily by induction on the list. For example:
[EVERY_DELETE_ELEMENT] Theorem
|- ∀e L P. P e ∧ EVERY P (DELETE_ELEMENT e L) ⇒ EVERY P L
[LENGTH_DELETE_ELEMENT_LE] Theorem
|- ∀e L. MEM e L ⇒ LENGTH (DELETE_ELEMENT e L) < LENGTH L
[LENGTH_DELETE_ELEMENT_LEQ] Theorem
|- ∀e L. LENGTH (DELETE_ELEMENT e L) ≤ LENGTH L
[NOT_MEM_DELETE_ELEMENT] Theorem
|- ∀e L. ¬MEM e (DELETE_ELEMENT e L)
What I actually needed is LENGTH_DELETE_ELEMENT_LE, but 3 months ago I just
couldn’t prove it!
However, I still have one more question: how can I express the fact that all
elements in (DELETE_ELEMENT e L) are also elements of L, with exactly the same
order and number of appearances? In another words, by inserting some “e” into
(DELETE_ELEMENT e L) I got the original list L?
Regards,
Chun Tian
> Il giorno 02 lug 2017, alle ore 10:23, Ramana Kumar
> <ramana.ku...@cl.cam.ac.uk> ha scritto:
>
> Sure, that's fine. I probably wouldn't even define such a constant but would
> instead use ``FILTER ((<>) x) ls`` in place.
>
> Stylistically it's usually better to use Define instead of new_definition,
> and to name defining theorems with a "_def" suffix. I'd also keep the name
> short like "DELETE" or even "delete".
>
> On 2 Jul 2017 17:04, "Chun Tian (binghe)" <binghe.l...@gmail.com> wrote:
> Hi,
>
> It seems that ListTheory didn’t provide a way to remove elements from list?
> What’s the recommended way to do such operation? Should I use FILTER, for
> example, like this?
>
> val DELETE_FROM_LIST = new_definition (
> "DELETE_FROM_LIST", ``DELETE_FROM_LIST x list = (FILTER (\i. ~(i = x))
> list)``);
>
> Regards,
>
> Chun
>
>
> ------------------------------------------------------------------------------
> 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
