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

section ‹Some algebraic identities derived from group axioms -- proof notepad version›

theory Group_Notepad
  imports Main
begin

notepad
begin
  txt ‹hypothetical group axiomatization›

  fix prod :: "'a → 'a → 'a"  (infixl ‹⊙› 70)
    and one :: "'a"
    and inverse :: "'a → 'a"
  assume assoc: "(x ⊙ y) ⊙ z = x ⊙ (y ⊙ z)"
    and left_one: "one ⊙ x = x"
    and left_inverse: "inverse x ⊙ x = one"
    for x y z

  txt ‹some consequences›

  have right_inverse: "x ⊙ inverse x = one" for x
  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

  have right_one: "x ⊙ one = x" for 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

  have one_equality: "one = e" if eq: "e ⊙ x = x" for e x
  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

  have inverse_equality: "inverse x = x'" if eq: "x' ⊙ x = one" for 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