Re: [isabelle] Defining infinite streams recursively
Thanks Alex, I forgot that I also needed to eta-expand the body of the
On Jun 7, 2008, at 2:41 AM, Alexander Krauss wrote:
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
[| 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.
Here is the rule you need:
"s = t ==>
(!!a. a = t ==> f a y = g a y)
==> x = y
==> Let s f x = Let t g y"
Note how the extra argument y is moved "into" the let.
This archive was generated by a fusion of
Pipermail (Mailman edition) and