# Re: [isabelle] Defining finite list functions recursively

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.*