# Theory Type_Semigroups

```(* Title: Examples/TTS_Foundations/Algebra/Type_Semigroups.thy
Author: Mihails Milehins
*)
section‹Abstract semigroups on types›
theory Type_Semigroups
imports Main
begin

subsection‹Background›

text‹The results presented in this section were ported
(with amendments and additions) from the theory \<^text>‹Groups› in the main
library of Isabelle/HOL.›

subsection‹Preliminaries›

named_theorems tts_ac_simps "assoc. and comm. simplification rules"
and tts_algebra_simps "algebra simplification rules"
and tts_field_simps "algebra simplification rules for fields"

subsection‹Binary operations›

text‹Abstract operation.›

locale binary_op =
fixes f :: "'a ⇒ 'a ⇒ 'a"

locale binary_op_syntax = binary_op f for f :: "'a ⇒ 'a ⇒ 'a"
begin

notation f (infixl ‹⊕⇩a› 65)

end

text‹Concrete syntax.›

locale plus = binary_op plus for plus :: "'a ⇒ 'a ⇒ 'a"
begin

notation plus (infixl ‹+⇩a› 65)

end

locale minus = binary_op minus for minus :: "'a ⇒ 'a ⇒ 'a"
begin

notation minus (infixl ‹-⇩a› 65)

end

locale times = binary_op times for times :: "'a ⇒ 'a ⇒ 'a"
begin

notation times (infixl ‹*⇩a› 70)

end

locale divide = binary_op divide for divide :: "'a ⇒ 'a ⇒ 'a"
begin

notation divide (infixl ‹'/⇩a› 70)

end

text‹Pairs.›

locale binary_op_pair = alg⇩a: binary_op f⇩a + alg⇩b: binary_op f⇩b
for f⇩a :: "'a ⇒ 'a ⇒ 'a" and f⇩b :: "'b ⇒ 'b ⇒ 'b"

locale binary_op_pair_syntax = binary_op_pair f⇩a f⇩b
for f⇩a :: "'a ⇒ 'a ⇒ 'a" and f⇩b :: "'b ⇒ 'b ⇒ 'b"
begin

notation f⇩a (infixl ‹⊕⇩a› 65)
notation f⇩b (infixl ‹⊕⇩b› 65)

end

subsection‹Simple semigroups›

subsubsection‹Definitions›

text‹Abstract semigroups.›

locale semigroup = binary_op f for f :: "'a ⇒ 'a ⇒ 'a" +
assumes assoc[tts_ac_simps, tts_algebra_simps]: "f (f a b) c = f a (f b c)"

locale semigroup_syntax = binary_op_syntax f for f :: "'a ⇒ 'a ⇒ 'a"

text‹Concrete syntax.›

locale semigroup_add = semigroup plus for plus :: "'a ⇒ 'a ⇒ 'a"
begin

sublocale plus plus .

end

locale semigroup_mult = semigroup times for times :: "'a ⇒ 'a ⇒ 'a"
begin

sublocale times times .

end

text‹Pairs.›

locale semigroup_pair = alg⇩a: semigroup f⇩a + alg⇩b: semigroup f⇩b
for f⇩a :: "'a ⇒ 'a ⇒ 'a" and f⇩b :: "'b ⇒ 'b ⇒ 'b"
begin

sublocale binary_op_pair f⇩a f⇩b .
sublocale rev: semigroup_pair f⇩b f⇩a ..

end

locale semigroup_pair_syntax = binary_op_pair_syntax

subsection‹Commutative semigroups›

subsubsection‹Definitions›

text‹Abstract commutative semigroup.›

locale comm_semigroup = semigroup f for f :: "'a ⇒ 'a ⇒ 'a" +
assumes commute[tts_ac_simps, tts_algebra_simps]: "f a b = f b a"

locale comm_semigroup_syntax = semigroup_syntax

text‹Concrete syntax.›

locale comm_semigroup_add = comm_semigroup plus for plus :: "'a ⇒ 'a ⇒ 'a"
begin

end

locale comm_semigroup_mult = comm_semigroup times for times :: "'a ⇒ 'a ⇒ 'a"
begin

sublocale semigroup_mult times ..

end

text‹Pairs.›

locale comm_semigroup_pair = alg⇩a: comm_semigroup f⇩a + alg⇩b: comm_semigroup f⇩b
for f⇩a :: "'a ⇒ 'a ⇒ 'a" and f⇩b :: "'b ⇒ 'b ⇒ 'b"
begin

sublocale semigroup_pair f⇩a f⇩b ..
sublocale rev: comm_semigroup_pair f⇩b f⇩a ..

end

locale comm_semigroup_pair_syntax = semigroup_pair_syntax

subsubsection‹Results›

context comm_semigroup
begin

interpretation comm_semigroup_syntax f .

lemma left_commute[tts_ac_simps, tts_algebra_simps, field_simps]:
"b ⊕⇩a (a ⊕⇩a c) = a ⊕⇩a (b ⊕⇩a c)"
proof -
have "(b ⊕⇩a a) ⊕⇩a c = (a ⊕⇩a b) ⊕⇩a c" by (simp add: commute)
then show ?thesis by (simp only: assoc)
qed

end

subsection‹Cancellative semigroups›

subsubsection‹Definitions›

text‹Abstract cancellative semigroup.›

locale cancel_semigroup = semigroup f for f :: "'a ⇒ 'a ⇒ 'a" +
assumes add_left_imp_eq: "f a b = f a c ⟹ b = c"
assumes add_right_imp_eq: "f b a = f c a ⟹ b = c"

locale cancel_semigroup_syntax = semigroup_syntax f for f :: "'a ⇒ 'a ⇒ 'a"

text‹Concrete syntax.›

for plus :: "'a ⇒ 'a ⇒ 'a"
begin

end

locale cancel_semigroup_mult = cancel_semigroup times
for times :: "'a ⇒ 'a ⇒ 'a"
begin

sublocale semigroup_mult times ..

end

text‹Pairs.›

locale cancel_semigroup_pair =
alg⇩a: cancel_semigroup f⇩a + alg⇩b: cancel_semigroup f⇩b
for f⇩a :: "'a ⇒ 'a ⇒ 'a" and f⇩b :: "'b ⇒ 'b ⇒ 'b"
begin

sublocale semigroup_pair f⇩a f⇩b ..
sublocale rev: cancel_semigroup_pair f⇩b f⇩a ..

end

locale cancel_semigroup_pair_syntax = semigroup_pair_syntax f⇩a f⇩b
for f⇩a :: "'a ⇒ 'a ⇒ 'a" and f⇩b :: "'b ⇒ 'b ⇒ 'b"

subsubsection‹Results›

context cancel_semigroup
begin

interpretation cancel_semigroup_syntax f .

lemma add_left_cancel[simp]: "a ⊕⇩a b = a ⊕⇩a c ⟷ b = c"

lemma add_right_cancel[simp]: "b ⊕⇩a a = c ⊕⇩a a ⟷ b = c"

lemma inj_on_add[simp]: "inj_on ((⊕⇩a) a) A" by (rule inj_onI) simp

lemma inj_on_add'[simp]: "inj_on (λb. b ⊕⇩a a) A" by (rule inj_onI) simp

lemma bij_betw_add[simp]: "bij_betw ((⊕⇩a) a) A B ⟷ (⊕⇩a) a ` A = B"

end

subsection‹Cancellative commutative semigroups›

subsubsection‹Definitions›

text‹Abstract cancellative commutative semigroups.›

locale cancel_comm_semigroup = comm: comm_semigroup f + binary_op fi
for f fi :: "'a ⇒ 'a ⇒ 'a" +
assumes add_diff_cancel_left'[simp]: "fi (f a b) a = b"
"fi (fi a b) c = fi a (f b c)"

locale cancel_comm_semigroup_syntax = comm_semigroup_syntax f + binary_op fi
for f fi :: "'a ⇒ 'a ⇒ 'a"
begin

notation fi (infixl ‹⊖⇩a› 65)

end

text‹Concrete syntax.›

locale cancel_comm_semigroup_add = cancel_comm_semigroup plus minus
for plus minus :: "'a ⇒ 'a ⇒ 'a"
begin

sublocale minus minus .

end

locale cancel_comm_semigroup_mult = cancel_comm_semigroup times divide
for times divide :: "'a ⇒ 'a ⇒ 'a"
begin

sublocale comm_semigroup_mult times ..
sublocale divide divide .

end

text‹Pairs.›

locale cancel_comm_semigroup_pair =
alg⇩a: cancel_comm_semigroup f⇩a fi⇩a + alg⇩b: cancel_comm_semigroup f⇩b fi⇩b
for f⇩a fi⇩a :: "'a ⇒ 'a ⇒ 'a" and f⇩b fi⇩b :: "'b ⇒ 'b ⇒ 'b"
begin

sublocale comm_semigroup_pair f⇩a f⇩b ..
sublocale rev: cancel_comm_semigroup_pair f⇩b fi⇩b f⇩a fi⇩a ..

end

locale cancel_comm_semigroup_pair_syntax =
comm_semigroup_pair_syntax f⇩a f⇩b + binary_op fi⇩a + binary_op fi⇩b
for f⇩a fi⇩a f⇩b fi⇩b
begin

notation fi⇩a (infixl ‹⊖⇩a› 65)
notation fi⇩b (infixl ‹⊖⇩b› 65)

end

subsubsection‹Results›

context cancel_comm_semigroup
begin

interpretation cancel_comm_semigroup_syntax .

lemma add_diff_cancel_right'[simp]: "(a ⊕⇩a b) ⊖⇩a b = a"

sublocale cancel: cancel_semigroup
proof
fix a b c :: 'a
assume "a ⊕⇩a b = a ⊕⇩a c"
then have "a ⊕⇩a b ⊖⇩a a = a ⊕⇩a c ⊖⇩a a" by simp
then show "b = c" by simp
next
fix a b c :: 'a
assume "b ⊕⇩a a = c ⊕⇩a a"
then have "b ⊕⇩a a ⊖⇩a a = c ⊕⇩a a ⊖⇩a a" by simp
then show "b = c" by simp
qed

lemmas cancel_semigroup_axioms = cancel.cancel_semigroup_axioms

lemma add_diff_cancel_left[simp]: "(c ⊕⇩a a) ⊖⇩a (c ⊕⇩a b) = a ⊖⇩a b"

lemma add_diff_cancel_right[simp]: "(a ⊕⇩a c) ⊖⇩a (b ⊕⇩a c) = a ⊖⇩a b"

lemma diff_right_commute: "a ⊖⇩a c ⊖⇩a b = a ⊖⇩a b ⊖⇩a c"

end

context cancel_comm_semigroup_pair
begin

sublocale cancel: cancel_semigroup_pair ..

lemmas cancel_semigroup_pair_axioms = cancel.cancel_semigroup_pair_axioms

end

text‹\newpage›

end```