Re: [isabelle] Problems with cong-rules for parser

Hi Alex,

I think your cong rule is slightly wrong. When I change it to

lemma bind_cong[fundef_cong]:
 fixes m1 :: "('t,'a)parser"
 assumes "m1 ts2 = m2 ts2"
 and "\<And> y ts. m2 ts2 = Inr (y,ts) ==> f1 y ts = f2 y ts"
 and "ts1 = ts2"
 shows "((bind m1 f1) ts1) = ((bind m2 f2) ts2)"

then the function definition works for me. (I haven't attempted a termination proof, but the proof obligation looks reasonable.)

The difference is that you have to refer to the "2"-variables in the assumptions of the branches, cf. eg. if_cong.

thanks, that was it. Now termination of the XML-parser is proven.

It would be nice if there was a helpful error at the time where you declare the rule, but I do not know what the general check would have to be... The format of cong-rules isn't really well-defined, except for the way they are used internally.

:-) I never would have seen from the error message, that I just would have to swap the 1's and 2's.

Since you are working with a state-exception monad, the termination proof isn't actually crucial: I recently prototyped a function definition facility for monadic functions of this kind which needs no termination proof at all. You may be interested in this, since it fits perfectly to your problem (the Ceta-Parser is actually mentioned in the paper as an application):
However, the tool is not quite ready for integration yet, but if you are not in a hurry, the problem might solve itself in a few months :-)

okay, nice to know. Perhaps we'll wait a bit before proving termination of the full CPF-parser.

René Thiemann                    mailto:rene.thiemann at
Computational Logic Group
Institute of Computer Science    phone: +43 512 507-6434
University of Innsbruck

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