Oh whoops I misunderstood - it deletes all of them. Never mind.
On 11 October 2017 at 22:38, Ramana Kumar <ramana.ku...@cl.cam.ac.uk> wrote:
> Just based on your final question, I suggest:
> ?l1 l2. (DELETE_ELEMENT e L = l1 ++ l2) /\ (L = l1 ++ [e] ++ l2)
>
> On 11 October 2017 at 22:34, <michael.norr...@data61.csiro.au> wrote:
>
>> You might define the sublist relation :
>>
>> Sublist [] l = T
>> Sublist _ [] = F
>> Sublist (h1::t1) (h2::t2) = if h1 = h2 then Sublist t1 t2 else Sublist
>> (h1::t1) t2
>>
>> And show that
>>
>> Sublist (DELETE_ELEMENT e l) l
>>
>> This doesn’t capture the idea that the only missing elements are e’s
>> though. This definition of Sublist might not be the easiest to work with…
>>
>> Michael
>>
>> On 11/10/17, 22:31, "Chun Tian" <binghe.l...@gmail.com> wrote:
>>
>> 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
>> >
>>
>>
>>
>> ------------------------------------------------------------
>> ------------------
>> 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
