# Re: [isabelle] Defining infinite streams recursively

Hi John,


I think the problem is that what is really needed is a "compound" congruence rule for when Let is itself applied as a higher order function, i.e.

lemma let_app_cong[fundef_cong]:
[| i = j;
M = N;
!!x. x = N ==> f x = g x|] ==>
(Let M f) i = (Let N g) j"

But when I added this rule I still ran into the same problem.


\begin{blackmagic}

Here is the rule you need:

lemma let_app_cong[fundef_cong]:
"s = t ==>
(!!a. a = t ==> f a y = g a y)
==> x = y
==> Let s f x = Let t g y"
by auto

\end{blackmagic}

Note how the extra argument y is moved "into" the let.

Alex



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