[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:
http://twitter.com/kasterma
http://kasterma.wordpress.com/






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.