Re: [isabelle] function (tailrec,sequential) fails



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
Description: This is a digitally signed message part



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