Re: [isabelle] Problems with cong-rules for parser
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
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):
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 :-)
This archive was generated by a fusion of
Pipermail (Mailman edition) and