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



Hi René,

we currently have problems setting up the right cong-rules for our
parser such termination is provable.
[...]

Does someone have an idea, what went wrong in this case?

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.

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.

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):
http://www4.in.tum.de/~krauss/mrec/
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 :-)

Alex





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