wenzelm@47295: (* Title: HOL/Isar_Examples/Group_Notepad.thy
wenzelm@47295: Author: Makarius
wenzelm@47295: *)
wenzelm@47295:
wenzelm@47295: header {* Some algebraic identities derived from group axioms -- proof notepad version *}
wenzelm@47295:
wenzelm@47295: theory Group_Notepad
wenzelm@47295: imports Main
wenzelm@47295: begin
wenzelm@47295:
wenzelm@47295: notepad
wenzelm@47295: begin
wenzelm@47295: txt {* hypothetical group axiomatization *}
wenzelm@47295:
wenzelm@47295: fix prod :: "'a \ 'a \ 'a" (infixl "**" 70)
wenzelm@47295: and one :: "'a"
wenzelm@55656: and inverse :: "'a \ 'a"
wenzelm@47295: assume assoc: "\x y z. (x ** y) ** z = x ** (y ** z)"
wenzelm@47295: and left_one: "\x. one ** x = x"
wenzelm@47295: and left_inverse: "\x. inverse x ** x = one"
wenzelm@47295:
wenzelm@47295: txt {* some consequences *}
wenzelm@47295:
wenzelm@47295: have right_inverse: "\x. x ** inverse x = one"
wenzelm@47295: proof -
wenzelm@47295: fix x
wenzelm@47295: have "x ** inverse x = one ** (x ** inverse x)"
wenzelm@47295: by (simp only: left_one)
wenzelm@47295: also have "\ = one ** x ** inverse x"
wenzelm@47295: by (simp only: assoc)
wenzelm@47295: also have "\ = inverse (inverse x) ** inverse x ** x ** inverse x"
wenzelm@47295: by (simp only: left_inverse)
wenzelm@47295: also have "\ = inverse (inverse x) ** (inverse x ** x) ** inverse x"
wenzelm@47295: by (simp only: assoc)
wenzelm@47295: also have "\ = inverse (inverse x) ** one ** inverse x"
wenzelm@47295: by (simp only: left_inverse)
wenzelm@47295: also have "\ = inverse (inverse x) ** (one ** inverse x)"
wenzelm@47295: by (simp only: assoc)
wenzelm@47295: also have "\ = inverse (inverse x) ** inverse x"
wenzelm@47295: by (simp only: left_one)
wenzelm@47295: also have "\ = one"
wenzelm@47295: by (simp only: left_inverse)
wenzelm@47295: finally show "x ** inverse x = one" .
wenzelm@47295: qed
wenzelm@47295:
wenzelm@47295: have right_one: "\x. x ** one = x"
wenzelm@47295: proof -
wenzelm@47295: fix x
wenzelm@47295: have "x ** one = x ** (inverse x ** x)"
wenzelm@47295: by (simp only: left_inverse)
wenzelm@47295: also have "\ = x ** inverse x ** x"
wenzelm@47295: by (simp only: assoc)
wenzelm@47295: also have "\ = one ** x"
wenzelm@47295: by (simp only: right_inverse)
wenzelm@47295: also have "\ = x"
wenzelm@47295: by (simp only: left_one)
wenzelm@47295: finally show "x ** one = x" .
wenzelm@47295: qed
wenzelm@47295:
wenzelm@47295: have one_equality: "\e x. e ** x = x \ one = e"
wenzelm@47295: proof -
wenzelm@47295: fix e x
wenzelm@47295: assume eq: "e ** x = x"
wenzelm@47295: have "one = x ** inverse x"
wenzelm@47295: by (simp only: right_inverse)
wenzelm@47295: also have "\ = (e ** x) ** inverse x"
wenzelm@47295: by (simp only: eq)
wenzelm@47295: also have "\ = e ** (x ** inverse x)"
wenzelm@47295: by (simp only: assoc)
wenzelm@47295: also have "\ = e ** one"
wenzelm@47295: by (simp only: right_inverse)
wenzelm@47295: also have "\ = e"
wenzelm@47295: by (simp only: right_one)
wenzelm@47295: finally show "one = e" .
wenzelm@47295: qed
wenzelm@47295:
wenzelm@47295: have inverse_equality: "\x x'. x' ** x = one \ inverse x = x'"
wenzelm@47295: proof -
wenzelm@47295: fix x x'
wenzelm@47295: assume eq: "x' ** x = one"
wenzelm@47295: have "inverse x = one ** inverse x"
wenzelm@47295: by (simp only: left_one)
wenzelm@47295: also have "\ = (x' ** x) ** inverse x"
wenzelm@47295: by (simp only: eq)
wenzelm@47295: also have "\ = x' ** (x ** inverse x)"
wenzelm@47295: by (simp only: assoc)
wenzelm@47295: also have "\ = x' ** one"
wenzelm@47295: by (simp only: right_inverse)
wenzelm@47295: also have "\ = x'"
wenzelm@47295: by (simp only: right_one)
wenzelm@47295: finally show "inverse x = x'" .
wenzelm@47295: qed
wenzelm@47295:
wenzelm@47295: end
wenzelm@47295:
wenzelm@47295: end