*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Problems with cong-rules for parser*From*: René Thiemann <rene.thiemann at uibk.ac.at>*Date*: Mon, 21 Jun 2010 16:10:33 +0200

Dear all, we currently have problems setting up the right cong-rules for our parser such termination is provable.

Consider the following theory: theory Test imports Main begin types ('t, 'a) parser = "'t list => string + ('a x 't 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

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"

shows "((bind m1 f1) ts1) = ((bind m2 f2) ts2)" using assms unfolding bind_def by (cases "m1 ts1", auto)

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

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" (*

*) Does someone have an idea, what went wrong in this case? Best regards, René PS: The small theory file is attached.

**Attachment:
Test.thy**

**Follow-Ups**:**Re: [isabelle] Problems with cong-rules for parser***From:*Tobias Nipkow

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

- Previous by Date: Re: [isabelle] Printing instantiations
- Next by Date: [isabelle] New AFP entry: Category Theory
- Previous by Thread: [isabelle] New AFP entries: Abstract Rewriting and Matrices
- 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