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.