# 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.*