Hello, I just started to learn Isabelle and am trying to prove function fusion of the algorithm design with Haskell book. The theorem I have is as follows,

```
lemma master_fusion : "h(f x y) = g x (h y) ⟹ h (foldr f xs e) = foldr g xs (h e)"
apply(induction xs arbitrary: x y)
apply(auto)
```

I got stuck after the second apply. The goal is as follows,

```
goal (1 subgoal):
1. ⋀a xs x y.
(⋀x y. h (f x y) = g x (h y) ⟹ h (foldr f xs e) = foldr g xs (h e)) ⟹
h (f x y) = g x (h y) ⟹ h (f a (foldr f xs e)) = g a (foldr g xs (h e))
```

I think I'm close to complete the proof: if I can use the premise of one of the implications to rewrite `h (f a (foldr f xs e)) = g a (foldr g xs (h e))`

into `g a (h (foldr f xs e))`

and use the induction assumption in the first implication to rewrite the previous result. I was wondering if you could give me any pointers? Thanks!

I do not think your lemma holds in the current form and quickcheck also finds a counterexample. I think you want your assumption to hold for all `x`

,`y`

, but currently it only requires there to be such `x`

,`y`

.

The following goes through:

```
lemma master_fusion:
"(⋀x y . h(f x y) = g x (h y)) ⟹ h (foldr f xs e) = foldr g xs (h e)"
by(induction xs ) (auto)
```

Last updated: Sep 25 2022 at 23:25 UTC