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

I defined it as follows, using Library/List_Prefix.thy (">>=" is list
postfix).
definition c_p :: "'a list set => 'a list => bool"
where
"c_p == % xss xs .
if xss = {}
then xs = []
else ALL xs' . xs' : xss --> xs' >>= xs"
definition l_c_p :: "'a list set => 'a list"
where
"l_c_p == % xss . THE xs . c_p xss xs & (ALL xs' . c_p xss xs' --> xs >>=
xs')"
I then proved that "c_p xss (l_c_p xss) & (ALL xs' . c_p xss xs' --> (l_c_p
xss) >>= xs')", which is what I needed.
Thanks for you answers,
Giuliano
On Thu, Mar 10, 2011 at 10:37 PM, Tim McKenzie <tjm1983 at gmail.com> wrote:
> 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
> <><
>

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