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

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

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

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)

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

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 [] = []) /\

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

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,

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

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

[Hol-info] [fm-announcements] NFM 2018 - 2nd CFP - Extended Deadlines

NFM 2018 - 2nd Call for Papers *** EXTENDED DEADLINES *** The 10th NASA Formal Methods Symposium 30 Years of Formal Methods at NASA - https://shemesh.larc.nasa.gov/NFM2018/ April 17-19, 2018 Newport News Marriott at City Center Newport News, VA, USA Theme of

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

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