# Re: [isabelle] Defining finite list functions recursively

Thanks Alex, that did the trick nicely. It seems to be holding up for defining mutually-recursive lists as well.
```
-john

On Jun 12, 2008, at 12:40 AM, Alexander Krauss wrote:

```
```Hi John,

```
I'm having problems proving termination of the well-founded recursive function xs_strm defined below, and other functions like it.
```
```
Good to see that you are driving all available tools to their limits and beyond, as usual :-) But it might actually work...
```
```
The problem is that nth_take_cong has the premise about the lengths being equal. In the function definition, a "recursive call" will be generated by this premise because the instance occuring contains the function being defined. But this simplifies away in your manual proof because "length (strm_to_list n f)" does not depend on f.
```
So you need just one more cong rule to tell function about this:

lemma length_strm_to_list_cong[fundef_cong]:
"n = n' ==> length (strm_to_list n f) = length (strm_to_list n' f')"
by simp

Then it works.

Alex

```
```

```

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