Re: [isabelle] Defining infinite streams recursively
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