Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 18 2022 at 13:50):

From: Bart Kastermans <Bart.Kastermans@Colorado.EDU>
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;

Email Gateway (Aug 18 2022 at 13:50):

From: Peter Lammich <peter.lammich@uni-muenster.de>
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;

Last updated: May 03 2024 at 04:19 UTC