Theory Action
section "Right group actions"
theory Action
imports "HOL-Algebra.Group"
begin
locale action = group +
fixes act :: "'b ⇒ 'a ⇒ 'b" (infixl ‹<o› 69)
assumes id_act [simp]: "b <o 𝟭 = b"
and act_act':
"g ∈ carrier G ∧ h ∈ carrier G ⟶ (b <o g) <o h = b <o (g ⊗ h)"
begin
lemma act_act:
assumes "g ∈ carrier G" and "h ∈ carrier G"
shows "(b <o g) <o h = b <o (g ⊗ h)"
proof -
from ‹g ∈ carrier G› and ‹h ∈ carrier G› and act_act'
show "(b <o g) <o h = b <o (g ⊗ h)" by simp
qed
lemma act_act_inv [simp]:
assumes "g ∈ carrier G"
shows "b <o g <o inv g = b"
proof -
from ‹g ∈ carrier G› have "inv g ∈ carrier G" by (rule inv_closed)
with ‹g ∈ carrier G› have "b <o g <o inv g = b <o g ⊗ inv g" by (rule act_act)
with ‹g ∈ carrier G› show "b <o g <o inv g = b" by simp
qed
lemma act_inv_act [simp]:
assumes "g ∈ carrier G"
shows "b <o inv g <o g = b"
using ‹g ∈ carrier G› and act_act_inv [of "inv g"]
by simp
lemma act_inv_iff:
assumes "g ∈ carrier G"
shows "b <o inv g = c ⟷ b = c <o g"
proof
assume "b <o inv g = c"
hence "b <o inv g <o g = c <o g" by simp
with ‹g ∈ carrier G› show "b = c <o g" by simp
next
assume "b = c <o g"
hence "b <o inv g = c <o g <o inv g" by simp
with ‹g ∈ carrier G› show "b <o inv g = c" by simp
qed
end
end