\begin{isabelle}%
\isanewline
\isacommand{theory}~Group~=~Main:\isanewline
\isanewline
\isanewline
\isacommand{consts}\isanewline
~~times~::~{"}'a~=>~'a~=>~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOtimes}{"}~70)\isanewline
~~inverse~::~{"}'a~=>~'a{"}~~~~~~~~({"}(\_{\isasyminv}){"}~[1000]~999)\isanewline
~~one~::~'a~~~~~~~~~~~~~~~~~~~~({"}{\isasymunit}{"})\isanewline
\isanewline
\isanewline
\isacommand{axclass}\isanewline
~~monoid~<~{"}term{"}\isanewline
~~assoc:~~~~~~{"}(x~{\isasymOtimes}~y)~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}\isanewline
~~left\_unit:~~{"}{\isasymunit}~{\isasymOtimes}~x~=~x{"}\isanewline
~~right\_unit:~{"}x~{\isasymOtimes}~{\isasymunit}~=~x{"}\isanewline
\isanewline
\isanewline
\isacommand{axclass}\isanewline
~~semigroup~<~{"}term{"}\isanewline
~~assoc:~{"}(x~{\isasymOtimes}~y)~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}\isanewline
\isanewline
\isacommand{axclass}\isanewline
~~group~<~semigroup\isanewline
~~left\_unit:~~~~{"}{\isasymunit}~{\isasymOtimes}~x~=~x{"}\isanewline
~~left\_inverse:~{"}inverse~x~{\isasymOtimes}~x~=~{\isasymunit}{"}%
\begin{isamarkuptext}%
The group axioms only state the properties of left unit and inverse,
the right versions may be derived as follows.%
\end{isamarkuptext}%
\isacommand{theorem}~group\_right\_inverse:~{"}x~{\isasymOtimes}~x{\isasyminv}~=~({\isasymunit}::'a::group){"}\isanewline
\isacommand{proof}~-\isanewline
~~\isacommand{have}~{"}x~{\isasymOtimes}~x{\isasyminv}~=~{\isasymunit}~{\isasymOtimes}~(x~{\isasymOtimes}~x{\isasyminv}){"}\isanewline
~~~~\isacommand{by}~(simp~only:~group.left\_unit)\isanewline
~~\isacommand{also}~\isacommand{have}~{"}...~=~({\isasymunit}~{\isasymOtimes}~x)~{\isasymOtimes}~x{\isasyminv}{"}\isanewline
~~~~\isacommand{by}~(simp~only:~semigroup.assoc)\isanewline
~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~x{\isasyminv}~{\isasymOtimes}~x~{\isasymOtimes}~x{\isasyminv}{"}\isanewline
~~~~\isacommand{by}~(simp~only:~group.left\_inverse)\isanewline
~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~(x{\isasyminv}~{\isasymOtimes}~x)~{\isasymOtimes}~x{\isasyminv}{"}\isanewline
~~~~\isacommand{by}~(simp~only:~semigroup.assoc)\isanewline
~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~{\isasymunit}~{\isasymOtimes}~x{\isasyminv}{"}\isanewline
~~~~\isacommand{by}~(simp~only:~group.left\_inverse)\isanewline
~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~({\isasymunit}~{\isasymOtimes}~x{\isasyminv}){"}\isanewline
~~~~\isacommand{by}~(simp~only:~semigroup.assoc)\isanewline
~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~x{\isasyminv}{"}\isanewline
~~~~\isacommand{by}~(simp~only:~group.left\_unit)\isanewline
~~\isacommand{also}~\isacommand{have}~{"}...~=~{\isasymunit}{"}\isanewline
~~~~\isacommand{by}~(simp~only:~group.left\_inverse)\isanewline
~~\isacommand{finally}~\isacommand{show}~?thesis~\isacommand{.}\isanewline
\isacommand{qed}%
\begin{isamarkuptext}%
With $group_right_inverse$ already available,
$group_right_unit$\label{thm:group-right-unit} is now established
much easier.%
\end{isamarkuptext}%
\isacommand{theorem}~group\_right\_unit:~{"}x~{\isasymOtimes}~{\isasymunit}~=~(x::'a::group){"}\isanewline
\isacommand{proof}~-\isanewline
~~\isacommand{have}~{"}x~{\isasymOtimes}~{\isasymunit}~=~x~{\isasymOtimes}~(x{\isasyminv}~{\isasymOtimes}~x){"}\isanewline
~~~~\isacommand{by}~(simp~only:~group.left\_inverse)\isanewline
~~\isacommand{also}~\isacommand{have}~{"}...~=~x~{\isasymOtimes}~x{\isasyminv}~{\isasymOtimes}~x{"}\isanewline
~~~~\isacommand{by}~(simp~only:~semigroup.assoc)\isanewline
~~\isacommand{also}~\isacommand{have}~{"}...~=~{\isasymunit}~{\isasymOtimes}~x{"}\isanewline
~~~~\isacommand{by}~(simp~only:~group\_right\_inverse)\isanewline
~~\isacommand{also}~\isacommand{have}~{"}...~=~x{"}\isanewline
~~~~\isacommand{by}~(simp~only:~group.left\_unit)\isanewline
~~\isacommand{finally}~\isacommand{show}~?thesis~\isacommand{.}\isanewline
\isacommand{qed}\isanewline
\isanewline
\isanewline
\isacommand{axclass}\isanewline
~~agroup~<~group\isanewline
~~commute:~{"}x~{\isasymOtimes}~y~=~y~{\isasymOtimes}~x{"}\isanewline
\isanewline
\isanewline
\isanewline
\isacommand{instance}~monoid~<~semigroup\isanewline
\isacommand{proof}~intro\_classes\isanewline
~~\isacommand{fix}~x~y~z~::~{"}'a::monoid{"}\isanewline
~~\isacommand{show}~{"}x~{\isasymOtimes}~y~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}\isanewline
~~~~\isacommand{by}~(rule~monoid.assoc)\isanewline
\isacommand{qed}\isanewline
\isanewline
\isanewline
\isacommand{instance}~group~<~monoid\isanewline
\isacommand{proof}~intro\_classes\isanewline
~~\isacommand{fix}~x~y~z~::~{"}'a::group{"}\isanewline
~~\isacommand{show}~{"}x~{\isasymOtimes}~y~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}\isanewline
~~~~\isacommand{by}~(rule~semigroup.assoc)\isanewline
~~\isacommand{show}~{"}{\isasymunit}~{\isasymOtimes}~x~=~x{"}\isanewline
~~~~\isacommand{by}~(rule~group.left\_unit)\isanewline
~~\isacommand{show}~{"}x~{\isasymOtimes}~{\isasymunit}~=~x{"}\isanewline
~~~~\isacommand{by}~(rule~group\_right\_unit)\isanewline
\isacommand{qed}\isanewline
\isanewline
\isanewline
\isanewline
\isacommand{defs}\isanewline
~~times\_bool\_def:~~~{"}x~{\isasymOtimes}~y~{\isasymequiv}~x~{\isasymnoteq}~(y{\isasymColon}bool){"}\isanewline
~~inverse\_bool\_def:~{"}x{\isasyminv}~{\isasymequiv}~x{\isasymColon}bool{"}\isanewline
~~unit\_bool\_def:~~~~{"}{\isasymunit}~{\isasymequiv}~False{"}\isanewline
\isanewline
\isacommand{instance}~bool~::~agroup\isanewline
\isacommand{proof}~(intro\_classes,\isanewline
~~~~unfold~times\_bool\_def~inverse\_bool\_def~unit\_bool\_def)\isanewline
~~\isacommand{fix}~x~y~z~::~bool\isanewline
~~\isacommand{show}~{"}((x~{\isasymnoteq}~y)~{\isasymnoteq}~z)~=~(x~{\isasymnoteq}~(y~{\isasymnoteq}~z)){"}~\isacommand{by}~blast\isanewline
~~\isacommand{show}~{"}(False~{\isasymnoteq}~x)~=~x{"}~\isacommand{by}~blast\isanewline
~~\isacommand{show}~{"}(x~{\isasymnoteq}~x)~=~False{"}~\isacommand{by}~blast\isanewline
~~\isacommand{show}~{"}(x~{\isasymnoteq}~y)~=~(y~{\isasymnoteq}~x){"}~\isacommand{by}~blast\isanewline
\isacommand{qed}\isanewline
\isanewline
\isanewline
\isacommand{defs}\isanewline
~~prod\_prod\_def:~{"}p~{\isasymOtimes}~q~{\isasymequiv}~(fst~p~{\isasymOtimes}~fst~q,~snd~p~{\isasymOtimes}~snd~q){"}\isanewline
\isanewline
\isacommand{instance}~*~::~(semigroup,~semigroup)~semigroup\isanewline
\isacommand{proof}~(intro\_classes,~unfold~prod\_prod\_def)\isanewline
~~\isacommand{fix}~p~q~r~::~{"}'a::semigroup~*~'b::semigroup{"}\isanewline
~~\isacommand{show}\isanewline
~~~~{"}(fst~(fst~p~{\isasymOtimes}~fst~q,~snd~p~{\isasymOtimes}~snd~q)~{\isasymOtimes}~fst~r,\isanewline
~~~~~~snd~(fst~p~{\isasymOtimes}~fst~q,~snd~p~{\isasymOtimes}~snd~q)~{\isasymOtimes}~snd~r)~=\isanewline
~~~~~~~(fst~p~{\isasymOtimes}~fst~(fst~q~{\isasymOtimes}~fst~r,~snd~q~{\isasymOtimes}~snd~r),\isanewline
~~~~~~~~snd~p~{\isasymOtimes}~snd~(fst~q~{\isasymOtimes}~fst~r,~snd~q~{\isasymOtimes}~snd~r)){"}\isanewline
~~~~\isacommand{by}~(simp~add:~semigroup.assoc)\isanewline
\isacommand{qed}\isanewline
\isanewline
\isacommand{end}\end{isabelle}%