*To*: Alexander Krauss <krauss at in.tum.de>*Subject*: Re: [isabelle] function (tailrec,sequential) fails*From*: Joachim Breitner <mail at joachim-breitner.de>*Date*: Tue, 31 Aug 2010 11:37:42 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4C7CBF25.1020200@in.tum.de>*References*: <1283186199.8506.19.camel@kirk> <4C7CBB01.1060906@in.tum.de> <1283243394.2483.6.camel@kirk> <4C7CBF25.1020200@in.tum.de>*Sender*: Joachim Breitner <msg at joachim-breitner.de>

Dear Alex, Am Dienstag, den 31.08.2010, 10:36 +0200 schrieb Alexander Krauss: > Joachim Breitner wrote: > > thanks. Now a beginner question: Do you have to rebuild Isabelle to have > > this fix, or can I just patch the file and it will work? > > You have to rebuild, by running the "build" script at the root of the > Isabelle tree. thanks. I applied the fix, and it worked so far. But when I tried to reduce the number of equations generated by sequential by simplifying the pattern matches, I get an error message that does not occur without tailrec. I could not cook up a simple example though. This change worked: http://git.nomeata.de/?p=funcCF.git;a=commitdiff;h=e9a10e7b004fbb1eb6f71a4195c39d6366338302 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/CFGraph/Eval.thy b/CFGraph/Eval.thy index ee507b5..4e75111 100644 --- a/CFGraph/Eval.thy +++ b/CFGraph/Eval.thy @@ -39,8 +39,8 @@ function (sequential,tailrec,domintros) = ( let b' = Suc b in if v \<noteq> 0 then evalF contt [] ve b' else evalF contt [] ve b')" - | "evalF Stop [DI i] _ _ - = (i)" + | "evalF Stop as _ _ + = (case as of [DI i] \<Rightarrow> i)" | "evalC (App lab f vs) \<beta> ve b = (let f' = evalV f \<beta> ve; %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% while this change of the (seemingly) same kind fails: http://git.nomeata.de/?p=funcCF.git;a=commitdiff;h=04c9da1123e3dc8aec3212a0a7bfaf8f9d66849d %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/CFGraph/Eval.thy b/CFGraph/Eval.thy index 4e75111..c71295f 100644 --- a/CFGraph/Eval.thy +++ b/CFGraph/Eval.thy @@ -35,8 +35,9 @@ function (sequential,tailrec,domintros) | "evalF (DP (Plus c)) [DI a1, DI a2, cont] ve b = (let b' = Suc b in evalF cont [DI (a1 + a2)] ve b')" - | "evalF (DP (If ct cf)) [DI v, contt, contf] ve b - = ( let b' = Suc b + | "evalF (DP (If ct cf)) as ve b + = (case as of [DI v, contt, contf] \<Rightarrow> + let b' = Suc b in if v \<noteq> 0 then evalF contt [] ve b' else evalF contt [] ve b')" | "evalF Stop as _ _ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% The error message I get is: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *** Proof failed. *** accp evalF_evalC_rel x *** 1. ⋀evalF_evalC_sum ct cf as ve b y cta cfa asa vea ba a list int aa lista *** ab listb x. *** ⟦⋀a list inta aaa lista aba listb x. *** ⟦int = inta ∧ aa = aaa ∧ ab = aba; a = DI inta; *** list = [aaa, aba]; lista = [aba]; listb = []; x = Suc ba⟧ *** ⟹ evalF_evalC_graph (Inl (aaa, [], vea, Suc ba)) *** (evalF_evalC_sum (Inl (aaa, [], vea, Suc ba))); *** ⋀a list inta aaa lista aba listb x. *** ⟦int = inta ∧ aa = aaa ∧ ab = aba; a = DI inta; *** list = [aaa, aba]; lista = [aba]; listb = []; x = Suc ba⟧ *** ⟹ accp evalF_evalC_rel (Inl (aaa, [], vea, Suc ba)); *** ⋀a list int aa lista ab listb x. *** ⟦False; a = DI 0; list = [aa, ab]; lista = [ab]; listb = []; *** x = Suc ba; int = 0⟧ *** ⟹ evalF_evalC_graph (Inl (aa, [], vea, Suc ba)) *** (evalF_evalC_sum (Inl (aa, [], vea, Suc ba))); *** ⋀a list int aa lista ab listb x. *** ⟦False; a = DI 0; list = [aa, ab]; lista = [ab]; listb = []; *** x = Suc ba; int = 0⟧ *** ⟹ accp evalF_evalC_rel (Inl (aa, [], vea, Suc ba)); *** y = Inl (aa, [], vea, Suc ba); *** ct = cta ∧ cf = cfa ∧ as = [DI int, aa, ab] ∧ ve = vea ∧ b = ba; *** asa = [DI int, aa, ab]; a = DI int; list = [aa, ab]; lista = [ab]; *** listb = []; x = Suc ba; int ≠ 0⟧ *** ⟹ accp evalF_evalC_rel (Inl (aa, [], vea, Suc ba)) *** 1 unsolved goal(s)! *** The error(s) above occurred for the goal statement: *** evalF_evalC_graph x y ⟹ accp evalF_evalC_rel x *** At command "done". %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% TIA for helping me out here, Joachim -- Joachim Breitner e-Mail: mail at joachim-breitner.de Homepage: http://www.joachim-breitner.de ICQ#: 74513189 Jabber-ID: nomeata at joachim-breitner.de

**Attachment:
signature.asc**

**References**:**[isabelle] function (tailrec,sequential) fails***From:*Joachim Breitner

**Re: [isabelle] function (tailrec,sequential) fails***From:*Alexander Krauss

**Re: [isabelle] function (tailrec,sequential) fails***From:*Joachim Breitner

**Re: [isabelle] function (tailrec,sequential) fails***From:*Alexander Krauss

- Previous by Date: Re: [isabelle] function (tailrec,sequential) fails
- Next by Date: [isabelle] Why can't auto prove that goal: f (x+(y+z)) = f ((x+y)+z)
- Previous by Thread: Re: [isabelle] function (tailrec,sequential) fails
- Next by Thread: [isabelle] Why can't auto prove that goal: f (x+(y+z)) = f ((x+y)+z)
- Cl-isabelle-users August 2010 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