Re: [isabelle] remdups_adj crucial lemma



And since I already proved soundness (also in a lengthy version), I copied my proof into Lars
file, which now contains the equivalence proof.

Cheers,
René

Attachment: Scratch.thy
Description: Binary data

Am 26.08.2014 um 11:40 schrieb Lars Noschinski <noschinl at in.tum.de>:

> On 26.08.2014 10:05, René Thiemann wrote:
>> Dear all,
>> 
>>> It seems to me that we need an abstract nonrecursive characterisation of
>>> remdups_adj from which specific lemmas follow easily. Is the following correct?
>>> 
>>> remdups_adj xs = ys <->
>>> EX f::nat => nat. mono f & f ` {0 ..< size xs} = {0 ..< size ys}
>>> & (ALL i < size xs. xs!i = ys!(f i)
>>>      & (xs!i = xs!(i+1) <-> f i = f(i+1)))
>>> It should be sound (-->), but is it complete (<--)?
>> At least there needs to be one more implication added, since
>> otherwise the reference to xs!(i+1) is critical.
>> 
>> remdups_adj xs = ys <->
>> EX f::nat => nat. mono f & f ` {0 ..< size xs} = {0 ..< size ys}
>> & (ALL i < size xs. xs!i = ys!(f i)
>>      & (i + 1 < size xs --> (xs!i = xs!(i+1) <-> f i = f(i+1))))
>> 
>> Otherwise, it looks good (soundness and completeness can easily be proven
>> for lists upto length 1, but the inductive case became quite tedious in my proof attempt)
> I've got a (lenghty, but otherwise straightforward) proof of
> completeness for the modified theorem.
> <Scratch.thy>



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.