Re: [isabelle] How to use o_assoc more efficiently?



Bart Kastermans wrote:
> 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
>
An apply (simp add: o_assoc) does the job:
  ultimately have "?left = ..." by auto
  thus "?left = ?right" by (auto simp add: o_assoc)
should work.

If not, try:
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)"
    by (simp only: o_assoc)
  thus "?left = ?right" by auto;
 
Regards,
  Peter


>   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;
>
>
>
>






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