Quelle  Group_Context.thy   Sprache: Isabelle

(*  Title:      HOL/Isar_Examples/Group_Context.thy
    Author:     Makarius
*)

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