Re: [Hol-info] What's the recommended way to delete elements from list?

2017-10-11 Thread Chun Tian (binghe) 
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  wrote:

> Oh whoops I misunderstood - it deletes all of them. Never mind.
>
> On 11 October 2017 at 22:38, Ramana Kumar 
> 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,  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"  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)" 
>>> 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
>>>

Re: [Hol-info] What's the recommended way to delete elements from list?

2017-10-11 Thread Chun Tian (binghe) 
Hi Michael,

Thanks, this SUBLIST relation is good enough for my potential needs.

Regards,

Chun Tian


On 11 October 2017 at 13:34,  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"  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)" 
> 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
>



-- 
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

Re: [Hol-info] What's the recommended way to delete elements from list?

2017-10-11 Thread Ramana Kumar 
Oh whoops I misunderstood - it deletes all of them. Never mind.

On 11 October 2017 at 22:38, Ramana Kumar  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,  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"  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)" 
>> 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

Re: [Hol-info] What's the recommended way to delete elements from list?

2017-10-11 Thread Ramana Kumar 
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,  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"  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)" 
> 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

Re: [Hol-info] What's the recommended way to delete elements from list?

2017-10-11 Thread Michael.Norrish 
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"  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 
 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)"  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

Re: [Hol-info] What's the recommended way to delete elements from list?

2017-10-11 Thread Chun Tian 
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 
>  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)"  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

Re: [Hol-info] What's the recommended way to delete elements from list?

2017-07-02 Thread Chun Tian (binghe) 
Hi Ramana,

Thank you very much, I’ll follow your suggestions.

Regards,

Chun

> Il giorno 02 lug 2017, alle ore 10:23, Ramana Kumar 
>  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)"  > 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