# [isabelle] Problems with cong-rules for parser

```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
```

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.

```

Attachment: Test.thy
Description: Binary data

```
```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.