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
