Isabelle手动证明幺半群逆元唯一性的步骤卡壳求助

我想要证明幺半群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"])

我的思路是完成以下证明步骤：

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

遗憾的是我卡在了第一步。我不想使用auto或其他自动证明方法，希望手动完成以学习推导过程。我尝试了apply (subst)、apply (rule arg_cong)及多种变体，但都没有成功。

我使用的幺半群定义如下：

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"

定理处于context monoid begin环境中。

我还尝试了以下写法：

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)

这让我取得了一定进展，但结合律规则现在需要满足：

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

然而，如果我将这些条件添加到from中：

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

那么apply(rule subst)会提示Failed to apply proof method⌂。

我另一个尝试是：

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 ⋅ 𝟭"

这实际上可行，但我又卡在了最后一行from this vu1 have "𝟭 ⋅ v' = v ⋅ 𝟭"，因为我不知道如何将vu1替换为𝟭。

内容的提问来源于stack exchange，提问作者alagris