# [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 [1] foo_1) i"
fun
foo_2 :: "nat strm" where
"foo_2 i = ((let q = (0::nat) in strm_append [1] foo_2) i)"
end

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