By the way, it's amazing that your original definition (based on FILTER)
can be used to prove the following theorem so easily:
val DELETE_ELEMENT_APPEND = store_thm (
"DELETE_ELEMENT_APPEND",
``!a L L'. DELETE_ELEMENT a (L ++ L') = DELETE_ELEMENT a L ++
DELETE_ELEMENT a L'``,
REWRITE_TAC [DELETE_ELEMENT_FILTER]
>> REWRITE_TAC [GSYM FILTER_APPEND_DISTRIB]);
Regards,
Chun Tian
On 11 October 2017 at 13:41, Ramana Kumar <ramana.ku...@cl.cam.ac.uk> wrote:
> 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
>
>
--
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
