# [isabelle] Defining finite list functions recursively

I'm having problems proving termination of the well-founded recursive function xs_strm defined below, and other functions like it.
```
```
The termination measure is just less_than, and I've installed appropriate congruence rules. However, the function package generates an unprovable termination condition.
```
```
On the other hand, I have been able to manually prove the identical function xs_strm2 below is well-founded by defining it in terms of the wfrec combinator and manually applying the congruence rules. Below are the definitions and lemmas needed to show the problem.
```
-john

section "Auxiliary function and lemma"

```
text {*Coerces a finite prefix of an infinite stream (represented as a @{typ "nat \<Rightarrow> 'a"} function) into a finite list. *}
```definition
```
strm_to_list :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> 'a list" where
``` "strm_to_list n f = map f [0..<n]"

lemma length_strm_to_list[simp]:
"length (strm_to_list n f) = n"

```
section {* Congruence rules for proving termination of @{term "xs_strm"} below. *}
```
lemma nth_cons_cong[fundef_cong]:
"\<lbrakk>i = i';
i' = 0 \<Longrightarrow> x = x';
```
\<And>j. i = Suc j \<Longrightarrow> xs ! j = xs' ! j\<rbrakk> \<Longrightarrow>
```   (x # xs) ! i = (x' # xs') ! i'"
by (cases i, auto)

lemma nth_out_of_bounds:
"length xs \<le> n \<Longrightarrow> xs ! n = [] ! (n - length xs)"
apply (induct xs arbitrary: n, auto simp add: nth_list_def)
by (case_tac n, auto)

lemma nth_take_cong[fundef_cong]:
assumes "i = i'"
and "n = n'"
and "i' < n' \<Longrightarrow> xs ! i' = xs' ! i'"
and "length xs = length xs'"
shows "(take n xs) ! i = (take n' xs') ! i'"
(is "?lhs = ?rhs")
using prems apply (cases "i' < n'", auto)
apply (subst nth_out_of_bounds, auto)
by (subst (2) nth_out_of_bounds, auto)

lemma nth_strm_to_list_cong[fundef_cong]:
"\<lbrakk>n = n';
i = i';
i < n \<Longrightarrow> f i' = f' i'\<rbrakk> \<Longrightarrow>
strm_to_list n f ! i = strm_to_list n' f' ! i'"
apply (cases "i' < n'", auto)
apply (subst nth_out_of_bounds, auto)
by (subst (2) nth_out_of_bounds, auto)

section "An unsuccessful attempt to prove termination of the
well-founded function @{term xs_strm} below"

function
xs_strm :: "nat \<Rightarrow> nat" where
"xs_strm i
= (0 # take 2 (strm_to_list 3 xs_strm)) ! i"
by pat_completeness auto
termination
apply (relation less_than)
apply auto
-- "I am left with an unprovable termination condition"
oops

section "Manually applying congruence rules to prove termination of the
identical function @{term xs_strm2}"

definition
xs_strm2 :: "nat \<Rightarrow> nat" where
```
"xs_strm2 = wfrec less_than (\<lambda>R i. (0 # take 2 (strm_to_list 3 R)) ! i)"
```
lemma def_xs_strm2:
"xs_strm2 i = (0 # take 2 (strm_to_list 3 xs_strm2)) ! i"
(is "?lhs = ?rhs")
proof -
let "?H R i" = "((0::nat) # take 2 (strm_to_list 3 R)) ! i"
from wfrec[OF wf_less_than, where H="?H" and a=i] xs_strm2_def
have "?lhs = ?H (cut xs_strm2 less_than i) i" by simp
also have "\<dots> = ?rhs"
-- "Manually applying congruence rules here"
apply (subst nth_cons_cong, simp_all)
apply (subst nth_take_cong, simp_all)
apply (subst nth_strm_to_list_cong, simp_all)