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
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
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 Sub
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 s
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 e
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
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 [] = []) /\
(DE