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