# [isabelle] Defining infinite streams recursively

```Hello,

```
We've run into a problem in having Isabelle automatically prove the termination of Cryptol infinite streams that we are translating into Isabelle, when the body of the stream definition uses a let- expression. Below is a theory that illustrates the problem.
```
Thanks,
-john

theory fun_let
imports Main
begin

-- "Represent infinite streams as nat-indexed functions"
types 'a strm = "nat => 'a"

-- "Appends a finite list of elements to the front of a stream"
definition
strm_append :: "'a list => 'a strm => 'a strm" where
"strm_append xs ys
= (%n. let l = length xs
in (if n < l then xs ! n else ys (n - l)))"

lemma strm_append_cong[fundef_cong]:
"[| n = n';
xs = xs';
!!k. n = k + length xs ==> ys k = ys' k|]
==> (strm_append xs ys) n = (strm_append xs' ys') n'"
by (cases n', simp_all add: strm_append_def Let_def)

text {* "fun" can automatically prove termination of foo_1, but
not foo_2, even though the only difference between the two is a
let expression. *}

fun
foo_1 :: "nat strm" where
"foo_1 i = (strm_append  foo_1) i"

fun
foo_2 :: "nat strm" where
"foo_2 i = ((let q = (0::nat) in strm_append  foo_2) i)"

end

```

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