*To*: René Thiemann <rene.thiemann at uibk.ac.at>*Subject*: Re: [isabelle] Problems with cong-rules for parser*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Tue, 22 Jun 2010 13:11:32 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <41A02B42-5183-455B-8E2B-C1AF6B8BAC1E@uibk.ac.at>*References*: <41A02B42-5183-455B-8E2B-C1AF6B8BAC1E@uibk.ac.at>*User-agent*: Thunderbird 2.0.0.24 (Macintosh/20100228)

Not an answer but a thought: maybe result checking can simplify your life? Maybe you can write your parser directly in ML and verify each run of the parser by unparsing and comparison with the input? Tobias René Thiemann schrieb: > Dear all, > > we currently have problems setting up the right cong-rules for our > parser such termination is provable. > > Here, the major problems are parsers which call themselves twice in a row. > > Consider the following theory: > > theory Test imports Main > begin > > types > ('t, 'a) parser = "'t list => string + ('a x 't list)" > > take a token list and produce a string error-message or a pair of result > and remaining token list > > (state-monad with errors) > > now we can define the standard return and bind operations > > abbreviation > return :: "'a => ('t, 'a)parser" > where > "return x = (%ts. Inr (x, ts))" > > definition > bind :: "('t, 'a) parser => ('a => ('t, 'b) parser) => ('t, 'b) parser" > where > "bind m f ts = (case m ts of > Inl e => Inl e > | Inr (x,ts') => f x ts')" > > consuming one character > > fun consume :: "('t,'t)parser" > where "consume [] = Inl ''error''" > | "consume (t # ts) = Inr (t, ts)" > > now, here is the difficult function: > > function foo :: "('t, 't list)parser" > where "foo ts = (bind consume > (% t. bind foo > (% us. bind foo > (% vs. return (t # us @ vs))))) ts" > by pat_completeness auto > termination > proof > (* impossible, since there is no link between input ts and the list > of tokens that is used for recursive foo-calls *) > oops > > so, let us add some congruence rule: > > lemma bind_cong[fundef_cong]: > fixes m1 :: "('t,'a)parser" > assumes "m1 ts1 = m2 ts1" and "!! y ts. m1 ts1 = Inr (y,ts) ==> f1 y > ts = f2 y ts" and "ts1 = ts2" > shows "((bind m1 f1) ts1) = ((bind m2 f2) ts2)" > using assms unfolding bind_def by (cases "m1 ts1", auto) > > now, indeed a simplied version of foo can be proven to be terminating > (if there is only one recursive call) > > function foo' :: "('t, 't list)parser" > where "foo' ts = (bind consume > (% t. bind foo' > (% vs. return (t # vs)))) ts" > by pat_completeness auto > termination by ... tedious reasoning > > but, if we want to have the full version which two recursive calls, then > not even the function > definition is accepted: > > function foo'' :: "('t, 't list)parser" > where "foo'' ts = (bind consume > (% t. bind foo'' > (% us. bind foo'' > (% vs. return (t # us @ vs))))) ts" > (* > exception THM 0 raised (line 709 of "thm.ML"): implies_elim: major premise > *) > > Does someone have an idea, what went wrong in this case? > > Best regards, > René > > PS: The small theory file is attached. > >

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

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

- Previous by Date: Re: [isabelle] 'symmetric' and full proofs
- Next by Date: Re: [isabelle] 'symmetric' and full proofs
- Previous by Thread: [isabelle] Problems with cong-rules for parser
- Next by Thread: Re: [isabelle] Problems with cong-rules for parser
- 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