# [isabelle] How to use o_assoc more efficiently?

```What is the right way to do a proof like the one below?  I have a
composition of functions in one order (paren placement), and I
```
need it in another order (paren placement). The rule for this is o_assoc, but I couldn't get Isabelle to do larger steps than on application at a time.
```
```
I think this is probably related to me not knowing which bit of automation to use when (blast, fast, auto, simp, ...). Any general ideas or references
```about that would also be greatly appreciated.

Thanks,

Best,
Bart

ultimately
have "?left =
```
(inv ni_bij) \<circ> ((f \<circ> (ni_bij \<circ> (inv ni_bij))) \<circ> g) \<circ> ni_bij"
```    by auto;
hence "?left =
```
(inv ni_bij) \<circ> ((f \<circ> (ni_bij \<circ> (inv ni_bij))) \<circ> g) \<circ> ni_bij"
```    using o_assoc[of f "ni_bij \<circ> (inv ni_bij)" g] by auto;
hence "?left =
```
(inv ni_bij) \<circ> ((f \<circ> ni_bij) \<circ> (inv ni_bij) \<circ> g) \<circ> ni_bij"
```    using o_assoc[of f ni_bij "inv ni_bij"] by auto;
hence "?left =
```
(inv ni_bij) \<circ> ((f \<circ> ni_bij) \<circ> ((inv ni_bij) \<circ> g)) \<circ> ni_bij"
```    using o_assoc[of "f \<circ> ni_bij" "inv ni_bij" g] by auto;
hence "?left =
```
((inv ni_bij) \<circ> (f \<circ> ni_bij)) \<circ> ((inv ni_bij) \<circ> g) \<circ> ni_bij" using o_assoc[of "inv ni_bij" "f \<circ> ni_bij" "(inv ni_bij) \<circ> g"]
```    by auto;
hence "?left =
```
((inv ni_bij) \<circ> (f \<circ> ni_bij)) \<circ> ((inv ni_bij) \<circ> g \<circ> ni_bij)" using o_assoc[of "inv ni_bij \<circ> (f \<circ> ni_bij)" "(inv ni_bij) \<circ> g"
```      "ni_bij"] by auto;
hence "?left =
```
((inv ni_bij) \<circ> f \<circ> ni_bij) \<circ> ((inv ni_bij) \<circ> g \<circ> ni_bij)"
```    using o_assoc[of "inv ni_bij" f ni_bij] by auto;
thus "?left = ?right" by auto;

--
homepage: http://www.bartk.nl/

also: