Re: [isabelle] definition using "function": proving pattern compatibility



On Thu, 10 Mar 2011 03:39:33 Alexander Krauss wrote:
> In such cases it is often easier to give a "purely logical"
> definition  using definite description in the style of
> "l_c_p S = (THE xs.
>    (ALL ys : s. is_suffix xs ys)
>     & (EX ys : s. ALL x. ~ is_suffix (x # xs) ys))"

I think you want to switch the quantifiers in the the last line to 
give
    & (ALL x. EX ys : s. ~ is_suffix (x # xs) ys))"
Otherwise "l_c_p s" is only well-defined when the longest common 
suffix is also an element of s.  Also, it looks like you put a 
capital S in the first line, and lower-case s elsewhere.

Tim
<><

Attachment: signature.asc
Description: This is a digitally signed message part.



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