Assume I have the following theorem:
comm_group ⦇carrier = e_aff, mult = add, one = (1, 0)⦈
and I want to show that:
add (add (x1,y1) (x2,y2)) (i (x2,y2)) = (x1,y1)
where i is the inverse operation of the group. This obviously holds in a group. How can I extract this knowledge from the assumption?
The comm_group … is the locale predicate, i.e. the thing that shows that you actually have an instance of the locale. To actually use it, one typically interprets the locale:
interpret comm_group "⦇carrier = e_aff, mult = add, one = (1, 0)⦈"
by (fact <insert your theorem here>)
After this, all the theorems proven in the context of the comm_group locale become available to you (e.g. m_assoc). You can optionally add a prefix to those names (particularly useful if there are name clashes, especially when you have several interpretations of the same locale):
interpret G: comm_group "⦇carrier = e_aff, mult = add, one = (1, 0)⦈"
by (fact <insert your theorem here>)
Then the theorem would be called G.m_assoc. This is covered in Section 5 of the locale tutorial.
By the way, you may want to consider introducing an abbreviation for your group, e.g.
define G where "G = ⦇carrier = e_aff, mult = add, one = (1, 0)⦈"
to make writing down statements about it less cumbersome. You can also make Isabelle's simplifier unfold that definition automatically by doing
define G where [simp]: "G = ⦇carrier = e_aff, mult = add, one = (1, 0)⦈"