Re: [isabelle] Defining infinite streams recursively



Thanks Alex, I forgot that I also needed to eta-expand the body of the let-expression.

-john

On Jun 7, 2008, at 2:41 AM, Alexander Krauss wrote:

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.