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
