*To*: Alexander Krauss <krauss at in.tum.de>*Subject*: Re: [isabelle] Problems with cong-rules for parser*From*: René Thiemann <rene.thiemann at uibk.ac.at>*Date*: Tue, 22 Jun 2010 21:13:03 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4C20CF08.2030603@in.tum.de>*References*: <41A02B42-5183-455B-8E2B-C1AF6B8BAC1E@uibk.ac.at> <4C20CF08.2030603@in.tum.de>

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 atermination proof, but the proof obligation looks reasonable.)The difference is that you have to refer to the "2"-variables in theassumptions 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 youdeclare the rule, but I do not know what the general check wouldhave 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 terminationproof isn't actually crucial: I recently prototyped a functiondefinition facility for monadic functions of this kind which needsno termination proof at all. You may be interested in this, since itfits perfectly to your problem (the Ceta-Parser is actuallymentioned 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 youare not in a hurry, the problem might solve itself in a few months :-)

René -- René Thiemann mailto:rene.thiemann at uibk.ac.at Computational Logic Group http://cl-informatik.uibk.ac.at/~thiemann/ Institute of Computer Science phone: +43 512 507-6434 University of Innsbruck

**References**:**[isabelle] Problems with cong-rules for parser***From:*René Thiemann

**Re: [isabelle] Problems with cong-rules for parser***From:*Alexander Krauss

- Previous by Date: [isabelle] Dependencies on constants
- Next by Date: Re: [isabelle] Dependencies on constants
- Previous by Thread: Re: [isabelle] Problems with cong-rules for parser
- Next by Thread: [isabelle] New AFP entry: Category Theory
- Cl-isabelle-users June 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list