Isabelle multiply both sides of an equation (equational reasoning in Isar)

Question

I want to prove that inverse element is unique in a monoid M

theorem inverse_unique:
  assumes "u ⋅ v' = 𝟭"
  assumes "v ⋅ u = 𝟭"
  assumes "u ∈ M"
  assumes "v ∈ M"
  assumes "v' ∈ M"
  shows "v = v'"
proof -
  have "v ⋅ u ⋅ v' = v ⋅ 𝟭"  
    apply (rule arg_cong[of "u ⋅ v'" 𝟭 "λ x. v⋅x"])

The idea is to show the following steps

v⋅u⋅v'=𝟭⋅v' by congruence (multiplying both sides)
v⋅𝟭=𝟭⋅v' by monoid neutral element axiom
v⋅𝟭=v' by monoid neutral element axiom
v=v' done

Unfortunately I am stuck on the very first step. I don't want to use auto or any other automatic approach. I want to do it by hand to learn how to do it. I've been trying with apply (subst) and apply (rule arg_cong) and many variations thereof. Nothing really works.

This is the definition of monoid that I am using

locale monoid =
  fixes M and composition (infixl "⋅" 70) and unit ("𝟭")
  assumes composition_closed [intro, simp]: "⟦ a ∈ M; b ∈ M ⟧ ⟹ a ⋅ b ∈ M"
    and unit_closed [intro, simp]: "𝟭 ∈ M"
    and associative [intro]: "⟦ a ∈ M; b ∈ M; c ∈ M ⟧ ⟹ (a ⋅ b) ⋅ c = a ⋅ (b ⋅ c)"
    and left_unit [intro, simp]: "a ∈ M ⟹ 𝟭 ⋅ a = a"
    and right_unit [intro, simp]: "a ∈ M ⟹ a ⋅ 𝟭 = a"

and the theorem is in context monoid begin

Other thing I've tried is this

theorem inverse_unique:
  assumes uv1:"u ⋅ v' = 𝟭"
  assumes vu1:"v ⋅ u = 𝟭"
  assumes um:"u ∈ M"
  assumes vm:"v ∈ M"
  assumes v'm:"v' ∈ M"
  shows "v = v'"
proof -
  from uv1 have "v ⋅ u ⋅ v' = v ⋅ 𝟭"
    apply(rule subst)
    apply(rule associative)

which gets me quite far but the associative rule requires now

 1. v ∈ M
 2. u ∈ M
 3. v' ∈ M

However, if I add those to from

from uv1 um vm v'm have "v ⋅ u ⋅ v' = v ⋅ 𝟭"

then apply(rule subst) yields Failed to apply proof method⌂.

Another thing I've tried is this

theorem inverse_unique:
  assumes uv1:"u ⋅ v' = 𝟭"
  assumes vu1:"v ⋅ u = 𝟭"
  assumes um:"u ∈ M"
  assumes vm:"v ∈ M"
  assumes v'm:"v' ∈ M"
  shows "v = v'"
proof -
  from uv1 have "v ⋅ (u ⋅ v') = v ⋅ 𝟭"
    apply (rule subst) 
    apply (rule refl)
    done
  from this um vm v'm have "v ⋅ u ⋅ v' = v ⋅ 𝟭"
    apply (subst associative)  
    apply (assumption)
    apply (assumption)
    apply (assumption)
    apply (assumption)
    done
  from this vu1 have "𝟭 ⋅ v' = v ⋅ 𝟭"

which actually works, but then again I get stuck at the last from this vu1 have "𝟭 ⋅ v' = v ⋅ 𝟭" because I still don't know how to substitute 𝟭 for vu1.

Answer 1

If substitution rules require assumptions, it's often convenient to supply these through the [OF ...] modifier behind the equality fact. Also, rewriting in Isar proofs usually makes more fun using the unfolding keyword. Your proof from https://stackoverflow.com/a/75362601/5158425 would then read:

theorem inverse_unique:
  assumes uv1: "u ⋅ v' = 𝟭"
  assumes vu1: "v ⋅ u = 𝟭"
  assumes um: "u ∈ M"
  assumes vm: "v ∈ M"
  assumes v'm: "v' ∈ M"
  shows "v = v'"
proof -
  have "v ⋅ (u ⋅ v') = v ⋅ 𝟭" unfolding uv1 by (rule refl)
  from this have "v ⋅ u ⋅ v' = v ⋅ 𝟭" unfolding associative[OF vm um v'm] by assumption
  from this have "𝟭 ⋅ v' = v ⋅ 𝟭" unfolding vu1 by assumption
  from this have "v' = v ⋅ 𝟭" unfolding left_unit[OF v'm] by assumption
  from this show "v = v'" unfolding right_unit[OF vm] by (rule sym)
qed

We can make this even simpler by use of the also have ... keywords to chain equalities:

proof -
  have ‹v = v ⋅ 𝟭› using right_unit[OF vm, symmetric] .
  also have ‹... = v ⋅ (u ⋅ v')› unfolding uv1 ..
  also have ‹... = v ⋅ u ⋅ v'› using associative[OF vm um v'm, symmetric] .
  also have ‹... = 𝟭 ⋅ v'› unfolding vu1 ..
  finally show ?thesis unfolding left_unit[OF v'm] .
qed

Here, the ... on the left-hand sides abbreviate the right-hand sides of the preceding lines. Moreover, the proof is elementar to a level that we can use the proof methods for immediate proof . and default proof ... They do roughly the same ”by assumption” and “by rule” would.