# Theory Group_Context

section ‹Some algebraic identities derived from group axioms -- theory context version›
theory Group_Context
imports Main
begin
text ‹hypothetical group axiomatization›
context
fixes prod :: "'a ⇒ 'a ⇒ 'a" (infixl "⊙" 70)
and one :: "'a"
and inverse :: "'a ⇒ 'a"
assumes assoc: "(x ⊙ y) ⊙ z = x ⊙ (y ⊙ z)"
and left_one: "one ⊙ x = x"
and left_inverse: "inverse x ⊙ x = one"
begin
text ‹some consequences›
lemma right_inverse: "x ⊙ inverse x = one"
proof -
have "x ⊙ inverse x = one ⊙ (x ⊙ inverse x)"
by (simp only: left_one)
also have "… = one ⊙ x ⊙ inverse x"
by (simp only: assoc)
also have "… = inverse (inverse x) ⊙ inverse x ⊙ x ⊙ inverse x"
by (simp only: left_inverse)
also have "… = inverse (inverse x) ⊙ (inverse x ⊙ x) ⊙ inverse x"
by (simp only: assoc)
also have "… = inverse (inverse x) ⊙ one ⊙ inverse x"
by (simp only: left_inverse)
also have "… = inverse (inverse x) ⊙ (one ⊙ inverse x)"
by (simp only: assoc)
also have "… = inverse (inverse x) ⊙ inverse x"
by (simp only: left_one)
also have "… = one"
by (simp only: left_inverse)
finally show ?thesis .
qed
lemma right_one: "x ⊙ one = x"
proof -
have "x ⊙ one = x ⊙ (inverse x ⊙ x)"
by (simp only: left_inverse)
also have "… = x ⊙ inverse x ⊙ x"
by (simp only: assoc)
also have "… = one ⊙ x"
by (simp only: right_inverse)
also have "… = x"
by (simp only: left_one)
finally show ?thesis .
qed
lemma one_equality:
assumes eq: "e ⊙ x = x"
shows "one = e"
proof -
have "one = x ⊙ inverse x"
by (simp only: right_inverse)
also have "… = (e ⊙ x) ⊙ inverse x"
by (simp only: eq)
also have "… = e ⊙ (x ⊙ inverse x)"
by (simp only: assoc)
also have "… = e ⊙ one"
by (simp only: right_inverse)
also have "… = e"
by (simp only: right_one)
finally show ?thesis .
qed
lemma inverse_equality:
assumes eq: "x' ⊙ x = one"
shows "inverse x = x'"
proof -
have "inverse x = one ⊙ inverse x"
by (simp only: left_one)
also have "… = (x' ⊙ x) ⊙ inverse x"
by (simp only: eq)
also have "… = x' ⊙ (x ⊙ inverse x)"
by (simp only: assoc)
also have "… = x' ⊙ one"
by (simp only: right_inverse)
also have "… = x'"
by (simp only: right_one)
finally show ?thesis .
qed
end
end