Theory Set_Semigroups

```(* Title: Examples/TTS_Foundations/Algebra/Set_Semigroups.thy
Author: Mihails Milehins
*)
section‹Abstract semigroups on sets›
theory Set_Semigroups
imports
Type_Semigroups
FNDS_Auxiliary
"../Foundations/FNDS_Lifting_Set_Ext"
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‹Binary operations›

text‹Abstract binary operation.›

locale binary_op_base_ow =
fixes U :: "'a set" and f :: "'a ⇒ 'a ⇒ 'a"

locale binary_op_ow = binary_op_base_ow U f for U :: "'a set" and f +
assumes op_closed: "x ∈ U ⟹ y ∈ U ⟹ f x y ∈ U"

locale binary_op_syntax_ow = binary_op_base_ow U f for U :: "'a set" and f
begin

notation f (infixl ‹⊕⇩a› 70)

end

text‹Concrete syntax.›

locale plus_ow = binary_op_ow U plus for U :: "'a set" and plus
begin

notation plus (infixl ‹+⇩a› 65)

end

locale minus_ow = binary_op_ow U minus for U :: "'a set" and minus
begin

notation minus (infixl ‹-⇩a› 65)

end

locale times_ow = binary_op_ow U times for U :: "'a set" and times
begin

notation times (infixl ‹*⇩a› 70)

end

locale divide_ow = binary_op_ow U divide for U :: "'a set" and divide
begin

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

end

text‹Pairs.›

locale binary_op_base_pair_ow =
alg⇩a: binary_op_base_ow U⇩a f⇩a + alg⇩b: binary_op_base_ow U⇩b f⇩b
for U⇩a :: "'a set" and f⇩a and U⇩b :: "'b set" and f⇩b

locale binary_op_pair_ow = alg⇩a: binary_op_ow U⇩a f⇩a + alg⇩b: binary_op_ow U⇩b f⇩b
for U⇩a :: "'a set" and f⇩a and U⇩b :: "'b set" and f⇩b
begin

sublocale binary_op_base_pair_ow U⇩a f⇩a U⇩b f⇩b .
sublocale rev: binary_op_base_pair_ow U⇩b f⇩b U⇩a f⇩a .

end

locale binary_op_pair_syntax_ow = binary_op_base_pair_ow U⇩a f⇩a U⇩b f⇩b
for U⇩a :: "'a set" and f⇩a and U⇩b :: "'b set" and f⇩b
begin

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

end

subsubsection‹Results›

context binary_op_ow
begin

interpretation binary_op_syntax_ow .

lemma op_closed'[simp]: "∀x∈U. ∀y∈U. x ⊕⇩a y ∈ U" by (simp add: op_closed)

tts_register_sbts ‹(⊕⇩a)› | U by (rule tts_AA_A_transfer[OF op_closed])

end

subsection‹Simple semigroups›

subsubsection‹Definitions›

text‹Abstract semigroup.›

locale semigroup_ow = binary_op_ow U f for U :: "'a set" and f +
assumes assoc[tts_ac_simps]:
"⟦ a ∈ U; b ∈ U; c ∈ U ⟧ ⟹ f (f a b) c = f a (f b c)"

locale semigroup_syntax_ow = binary_op_syntax_ow U f for U :: "'a set" and f

text‹Concrete syntax.›

locale semigroup_add_ow = semigroup_ow U plus for U :: "'a set" and plus
begin

sublocale plus_ow U plus ..

end

locale semigroup_mult_ow = semigroup_ow U times for U :: "'a set" and times
begin

sublocale times_ow U times ..

end

text‹Pairs.›

locale semigroup_pair_ow = alg⇩a: semigroup_ow U⇩a f⇩a + alg⇩b: semigroup_ow U⇩b f⇩b
for U⇩a :: "'a set" and f⇩a and U⇩b :: "'b set" and f⇩b
begin

sublocale binary_op_pair_ow U⇩a f⇩a U⇩b f⇩b ..
sublocale rev: semigroup_pair_ow U⇩b f⇩b U⇩a f⇩a ..

end

locale semigroup_pair_syntax_ow = binary_op_pair_syntax_ow U⇩a f⇩a U⇩b f⇩b
for U⇩a :: "'a set" and f⇩a and U⇩b :: "'b set" and f⇩b

subsubsection‹Transfer rules›

lemma semigroup_ow[ud_with]: "semigroup = semigroup_ow UNIV"
unfolding
semigroup_def semigroup_ow_def semigroup_ow_axioms_def binary_op_ow_def
by simp

lemma semigroup_pair_ow[ud_with]:
"semigroup_pair = (λf⇩a f⇩b. semigroup_pair_ow UNIV f⇩a UNIV f⇩b)"
unfolding semigroup_pair_def semigroup_pair_ow_def ud_with by simp

context
includes lifting_syntax
begin

lemma semigroup_ow_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_unique A" "right_total A"
shows
"(rel_set A ===> (A ===> A ===> A) ===> (=)) semigroup_ow semigroup_ow"
by
(
ow_locale_transfer locale_defs:
semigroup_ow_def semigroup_ow_axioms_def binary_op_ow_def
)

lemma semigroup_pair_ow_transfer[transfer_rule]:
assumes [transfer_rule]:
"bi_unique A" "right_total A" "bi_unique B" "right_total B"
shows
"(
rel_set A ===> (A ===> A ===> A) ===>
rel_set B ===> (B ===> B ===> B) ===>
(=)
)
semigroup_pair_ow semigroup_pair_ow"
by (ow_locale_transfer locale_defs: semigroup_pair_ow_def)

end

subsection‹Commutative semigroups›

subsubsection‹Definitions›

text‹Abstract commutative semigroup.›

locale comm_semigroup_ow = semigroup_ow U f for U :: "'a set" and f +
assumes commute[tts_ac_simps]: "a ∈ U ⟹ b ∈ U ⟹ f a b = f b a"

locale comm_semigroup_syntax_ow = semigroup_syntax_ow U f
for U :: "'a set" and f

text‹Concrete syntax.›

locale comm_semigroup_add_ow = comm_semigroup_ow U plus
for U :: "'a set" and plus
begin

end

locale comm_semigroup_mult_ow = comm_semigroup_ow U times
for U :: "'a set" and times
begin

sublocale semigroup_mult_ow U times ..

end

text‹Pairs.›

locale comm_semigroup_pair_ow =
alg⇩a: comm_semigroup_ow U⇩a f⇩a + alg⇩b: comm_semigroup_ow U⇩b f⇩b
for U⇩a :: "'a set" and f⇩a and U⇩b :: "'b set" and f⇩b
begin

sublocale semigroup_pair_ow U⇩a f⇩a U⇩b f⇩b ..
sublocale rev: comm_semigroup_pair_ow U⇩b f⇩b U⇩a f⇩a ..

end

locale comm_semigroup_pair_syntax_ow = semigroup_pair_syntax_ow U⇩a f⇩a U⇩b f⇩b
for U⇩a :: "'a set" and f⇩a and U⇩b :: "'b set" and f⇩b

subsubsection‹Transfer rules›

lemma comm_semigroup_ow[ud_with]: "comm_semigroup = comm_semigroup_ow UNIV"
unfolding
comm_semigroup_def comm_semigroup_axioms_def
comm_semigroup_ow_def comm_semigroup_ow_axioms_def
ud_with
by simp

lemma comm_semigroup_pair_ow[ud_with]:
"comm_semigroup_pair = (λf⇩a f⇩b. comm_semigroup_pair_ow UNIV f⇩a UNIV f⇩b)"
unfolding comm_semigroup_pair_def comm_semigroup_pair_ow_def ud_with
by simp

context
includes lifting_syntax
begin

lemma comm_semigroup_ow_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_unique A" "right_total A"
shows
"(rel_set A ===> (A ===> A ===> A) ===> (=))
comm_semigroup_ow comm_semigroup_ow"
by
(
ow_locale_transfer locale_defs:
comm_semigroup_ow_def comm_semigroup_ow_axioms_def
)

lemma comm_semigroup_pair_ow_transfer[transfer_rule]:
assumes [transfer_rule]:
"bi_unique A" "right_total A" "bi_unique B" "right_total B"
shows
"(
rel_set A ===> (A ===> A ===> A) ===>
rel_set B ===> (B ===> B ===> B) ===>
(=)
)
comm_semigroup_pair_ow comm_semigroup_pair_ow"
by (ow_locale_transfer locale_defs: comm_semigroup_pair_ow_def)

end

subsubsection‹Relativization›

context comm_semigroup_ow
begin

interpretation comm_semigroup_syntax_ow .

tts_context
tts: (?'a to U)
substituting comm_semigroup_ow_axioms
eliminating through auto
begin

tts_lemma left_commute:
assumes "b ∈ U"
and "a ∈ U"
and "c ∈ U"
shows "b ⊕⇩a (a ⊕⇩a c) = a ⊕⇩a (b ⊕⇩a c)"
is comm_semigroup.left_commute.

end

end

subsection‹Cancellative semigroups›

subsubsection‹Definitions›

text‹Abstract cancellative semigroup.›

locale cancel_semigroup_ow = semigroup_ow U f for U :: "'a set" and f +
"⟦ a ∈ U; b ∈ U; c ∈ U; f a b = f a c ⟧ ⟹ b = c"
"⟦ b ∈ U; a ∈ U; c ∈ U; f b a = f c a ⟧ ⟹ b = c"

locale cancel_semigroup_syntax_ow = semigroup_syntax_ow U f
for U :: "'a set" and f

text‹Concrete syntax.›

locale cancel_semigroup_add_ow = cancel_semigroup_ow U plus
for U :: "'a set" and plus
begin

end

locale cancel_semigroup_mult_ow = cancel_semigroup_ow U times
for U :: "'a set" and times
begin

sublocale semigroup_mult_ow U times ..

end

text‹Pairs.›

locale cancel_semigroup_pair_ow =
alg⇩a: cancel_semigroup_ow U⇩a f⇩a + alg⇩b: cancel_semigroup_ow U⇩b f⇩b
for U⇩a :: "'a set" and f⇩a and U⇩b :: "'b set" and f⇩b
begin

sublocale semigroup_pair_ow U⇩a f⇩a U⇩b f⇩b ..
sublocale rev: cancel_semigroup_pair_ow U⇩b f⇩b U⇩a f⇩a ..

end

locale cancel_semigroup_pair_syntax_ow = semigroup_pair_syntax_ow U⇩a f⇩a U⇩b f⇩b
for U⇩a :: "'a set" and f⇩a and U⇩b :: "'b set" and f⇩b

subsubsection‹Transfer rules›

lemma cancel_semigroup_ow[ud_with]:
"cancel_semigroup = cancel_semigroup_ow UNIV"
unfolding
cancel_semigroup_def cancel_semigroup_axioms_def
cancel_semigroup_ow_def cancel_semigroup_ow_axioms_def
ud_with
by simp

lemma cancel_semigroup_pair_ow[ud_with]:
"cancel_semigroup_pair = (λf⇩a f⇩b. cancel_semigroup_pair_ow UNIV f⇩a UNIV f⇩b)"
unfolding cancel_semigroup_pair_def cancel_semigroup_pair_ow_def ud_with
by simp

context
includes lifting_syntax
begin

lemma cancel_semigroup_ow_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_unique A" "right_total A"
shows
"(rel_set A ===> (A ===> A ===> A) ===> (=))
cancel_semigroup_ow cancel_semigroup_ow"
by
(
ow_locale_transfer locale_defs:
cancel_semigroup_ow_def cancel_semigroup_ow_axioms_def
)

lemma cancel_semigroup_pair_ow_transfer[transfer_rule]:
assumes [transfer_rule]:
"bi_unique A" "right_total A" "bi_unique B" "right_total B"
shows
"(
rel_set A ===> (A ===> A ===> A) ===>
rel_set B ===> (B ===> B ===> B) ===>
(=)
) cancel_semigroup_pair_ow cancel_semigroup_pair_ow"
by (ow_locale_transfer locale_defs: cancel_semigroup_pair_ow_def)

end

subsubsection‹Relativization›

context cancel_semigroup_ow
begin

interpretation cancel_semigroup_syntax_ow .

tts_context
tts: (?'a to U)
rewriting ctr_simps
substituting cancel_semigroup_ow_axioms
eliminating through auto
begin

assumes "b ∈ U" and "a ∈ U" and "c ∈ U"
shows "(b ⊕⇩a a = c ⊕⇩a a) = (b = c)"

assumes "a ∈ U" and "b ∈ U" and "c ∈ U"
shows "(a ⊕⇩a b = a ⊕⇩a c) = (b = c)"

assumes "a ∈ U" and "A ⊆ U"
shows "inj_on (λb. b ⊕⇩a a) A"

assumes "a ∈ U" and "A ⊆ U"
shows "inj_on ((⊕⇩a) a) A"

assumes "a ∈ U" and "A ⊆ U" and "B ⊆ U"
shows "bij_betw ((⊕⇩a) a) A B = ((⊕⇩a) a ` A = B)"

end

end

subsection‹Cancellative commutative semigroups›

subsubsection‹Definitions›

text‹Abstract cancellative commutative semigroups.›

locale cancel_comm_semigroup_ow = comm_semigroup_ow U f + binary_op_ow U fi
for U :: "'a set" and f fi +
assumes add_diff_cancel_left'[simp]: "⟦ a ∈ U; b ∈ U ⟧ ⟹ fi (f a b) a = b"
"⟦ a ∈ U; b ∈ U; c ∈ U ⟧ ⟹ fi (fi a b) c = fi a (f b c)"

locale cancel_comm_semigroup_syntax_ow =
comm_semigroup_syntax_ow U f + binary_op_base_ow U fi
for U :: "'a set" and f fi
begin

notation fi (infixl ‹⊖⇩a› 65)

end

text‹Concrete syntax.›

locale cancel_comm_semigroup_add_ow = cancel_comm_semigroup_ow U plus minus
for U :: "'a set" and plus minus
begin

sublocale minus_ow U minus ..

end

locale cancel_comm_semigroup_mult = cancel_comm_semigroup_ow U times divide
for U :: "'a set" and times divide
begin

sublocale comm_semigroup_mult_ow U times ..
sublocale divide_ow U divide ..

end

text‹Pairs.›

locale cancel_comm_semigroup_pair_ow =
alg⇩a: cancel_comm_semigroup_ow U⇩a f⇩a fi⇩a +
alg⇩b: cancel_comm_semigroup_ow U⇩b f⇩b fi⇩b
for U⇩a :: "'a set" and f⇩a fi⇩a and U⇩b :: "'b set" and f⇩b fi⇩b
begin

sublocale comm_semigroup_pair_ow U⇩a f⇩a U⇩b f⇩b ..
sublocale rev: cancel_comm_semigroup_pair_ow U⇩b f⇩b fi⇩b U⇩a f⇩a fi⇩a ..

end

locale cancel_comm_semigroup_pair_syntax_ow =
comm_semigroup_pair_syntax_ow U⇩a f⇩a U⇩b f⇩b +
binary_op_ow U⇩a fi⇩a +
binary_op_ow U⇩b fi⇩b
for U⇩a :: "'a set" and f⇩a fi⇩a and U⇩b :: "'b set" and f⇩b fi⇩b
begin

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

end

subsubsection‹Transfer rules›

lemma cancel_comm_semigroup_ow[ud_with]:
"cancel_comm_semigroup = cancel_comm_semigroup_ow UNIV"
unfolding
cancel_comm_semigroup_def cancel_comm_semigroup_axioms_def
cancel_comm_semigroup_ow_def cancel_comm_semigroup_ow_axioms_def
binary_op_ow_def
ud_with
by simp

lemma cancel_comm_semigroup_pair_ow[ud_with]:
"cancel_comm_semigroup_pair =
(λf⇩a fi⇩a f⇩b fi⇩b. cancel_comm_semigroup_pair_ow UNIV f⇩a fi⇩a UNIV f⇩b fi⇩b)"
unfolding
cancel_comm_semigroup_pair_def cancel_comm_semigroup_pair_ow_def ud_with
by simp

context
includes lifting_syntax
begin

lemma cancel_comm_semigroup_ow_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_unique A" "right_total A"
shows
"(rel_set A ===> (A ===> A ===> A) ===> (A ===> A ===> A) ===> (=))
cancel_comm_semigroup_ow cancel_comm_semigroup_ow"
by
(
ow_locale_transfer locale_defs:
cancel_comm_semigroup_ow_def
cancel_comm_semigroup_ow_axioms_def
binary_op_ow_def
)

lemma cancel_comm_semigroup_pair_ow_transfer[transfer_rule]:
assumes [transfer_rule]:
"bi_unique A" "right_total A" "bi_unique B" "right_total B"
shows
"(
rel_set A ===> (A ===> A ===> A) ===> (A ===> A ===> A) ===>
rel_set B ===> (B ===> B ===> B) ===> (B ===> B ===> B) ===>
(=)
) cancel_comm_semigroup_pair_ow cancel_comm_semigroup_pair_ow"
by (ow_locale_transfer locale_defs: cancel_comm_semigroup_pair_ow_def)

end

subsubsection‹Relativization›

context cancel_comm_semigroup_ow
begin

interpretation cancel_comm_semigroup_syntax_ow .

tts_context
tts: (?'a to U)
sbterms: (‹?f::?'a ⇒ ?'a ⇒ ?'a› to f)
and (‹?fi::?'a ⇒ ?'a ⇒ ?'a› to fi)
rewriting ctr_simps
substituting cancel_comm_semigroup_ow_axioms
eliminating through auto
begin

assumes "a ∈ U" and "b ∈ U"
shows "a ⊕⇩a b ⊖⇩a b = a"

assumes "a ∈ U" and "c ∈ U" and "b ∈ U"
shows "a ⊕⇩a c ⊖⇩a b ⊕⇩a c = a ⊖⇩a b"

assumes "c ∈ U" and "a ∈ U" and "b ∈ U"
shows "c ⊕⇩a a ⊖⇩a c ⊕⇩a b = a ⊖⇩a b"

tts_lemma diff_right_commute:
assumes "a ∈ U" and "c ∈ U" and "b ∈ U"
shows "a ⊖⇩a c ⊖⇩a b = a ⊖⇩a b ⊖⇩a c"
is cancel_comm_semigroup.diff_right_commute.

tts_lemma cancel_semigroup_axioms:
assumes "U ≠ {}"
shows "cancel_semigroup_ow U (⊕⇩a)"
is cancel_comm_semigroup.cancel_semigroup_axioms.

end

sublocale cancel_semigroup_ow
using
cancel_semigroup_axioms
cancel_semigroup_ow.intro
cancel_semigroup_ow_axioms_def
semigroup_ow_axioms
by auto

end

context cancel_comm_semigroup_pair_ow
begin

sublocale cancel_semigroup_pair_ow ..

end

text‹\newpage›

end```