*To*: Giuliano Losa <giuliano.losa at epfl.ch>*Subject*: Re: [isabelle] definition using "function": proving pattern compatibility*From*: Alexander Krauss <krauss at in.tum.de>*Date*: Wed, 09 Mar 2011 15:39:33 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <AANLkTikAYtfFmwLtT8On-PgN1P1QrER4cikQVgoBC2rf@mail.gmail.com>*References*: <AANLkTikAYtfFmwLtT8On-PgN1P1QrER4cikQVgoBC2rf@mail.gmail.com>*User-agent*: Mozilla-Thunderbird 2.0.0.22 (X11/20091109)

Hi Giuliano,

function l_c_p :: "'a list set => 'a list" where "[| l ~: ls; ls ~= {}; finite ls |] ==> l_c_p ({l} Un ls) = l_c_p_2 l (l_c_p ls)" | "l_c_p {l} = l" | "l_c_p {} = []" | "~ finite ls ==> l_c_p ls = dontcare" One of the things I have to solve to complete the definition is the following: "!! l ls la lsa x xa. [| l ~: ls; la ~: lsa; insert l ls = insert la lsa; l_c_postfix l (l_c_p_test_sumC ls) ~= l_c_postfix la (l_c_p_test_sumC lsa); x : ls; xa : lsa; finite ls; finite lsa |] ==> False" Since there are no assumptions about l_c_p_sumC I can't prove the goal. Is there a way to make it work?

If not, how could I define l_c_p differently?

"l_c_p S = (THE xs. (ALL ys : s. is_suffix xs ys) & (EX ys : s. ALL x. ~ is_suffix (x # xs) ys))" Then you can derive the recursive equations.

Hope this helps, Alex

**Follow-Ups**:**Re: [isabelle] definition using "function": proving pattern compatibility***From:*Tim McKenzie

**References**:**[isabelle] definition using "function": proving pattern compatibility***From:*Giuliano Losa

- Previous by Date: [isabelle] definition using "function": proving pattern compatibility
- Next by Date: [isabelle] Code generation for sets of sets
- Previous by Thread: [isabelle] definition using "function": proving pattern compatibility
- Next by Thread: Re: [isabelle] definition using "function": proving pattern compatibility
- Cl-isabelle-users March 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list