# 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

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 =
alga: binary_op_base_ow Ua fa + algb: binary_op_base_ow Ub fb
for Ua :: "'a set" and fa and Ub :: "'b set" and fb

locale binary_op_pair_ow = alga: binary_op_ow Ua fa + algb: binary_op_ow Ub fb
for Ua :: "'a set" and fa and Ub :: "'b set" and fb
begin

sublocale binary_op_base_pair_ow Ua fa Ub fb .
sublocale rev: binary_op_base_pair_ow Ub fb Ua fa .

end

locale binary_op_pair_syntax_ow = binary_op_base_pair_ow Ua fa Ub fb
for Ua :: "'a set" and fa and Ub :: "'b set" and fb
begin

notation fa (infixl a 70)
notation fb (infixl b 70)

end

subsubsection‹Results›

context binary_op_ow
begin

interpretation binary_op_syntax_ow .

lemma op_closed'[simp]: "xU. yU. 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 = alga: semigroup_ow Ua fa + algb: semigroup_ow Ub fb
for Ua :: "'a set" and fa and Ub :: "'b set" and fb
begin

sublocale binary_op_pair_ow Ua fa Ub fb ..
sublocale rev: semigroup_pair_ow Ub fb Ua fa ..

end

locale semigroup_pair_syntax_ow = binary_op_pair_syntax_ow Ua fa Ub fb
for Ua :: "'a set" and fa and Ub :: "'b set" and fb

subsubsection‹Transfer rules›

lemma semigroup_ow[ud_with]:
unfolding
semigroup_def semigroup_ow_def semigroup_ow_axioms_def binary_op_ow_def
by simp

lemma semigroup_pair_ow[ud_with]:
"semigroup_pair = (λfa fb. semigroup_pair_ow UNIV fa UNIV fb)"
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

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

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 =
alga: comm_semigroup_ow Ua fa + algb: comm_semigroup_ow Ub fb
for Ua :: "'a set" and fa and Ub :: "'b set" and fb
begin

sublocale semigroup_pair_ow Ua fa Ub fb ..
sublocale rev: comm_semigroup_pair_ow Ub fb Ua fa ..

end

locale comm_semigroup_pair_syntax_ow = semigroup_pair_syntax_ow Ua fa Ub fb
for Ua :: "'a set" and fa and Ub :: "'b set" and fb

subsubsection‹Transfer rules›

lemma comm_semigroup_ow[ud_with]:
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 = (λfa fb. comm_semigroup_pair_ow UNIV fa UNIV fb)"
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

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

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 =
alga: cancel_semigroup_ow Ua fa + algb: cancel_semigroup_ow Ub fb
for Ua :: "'a set" and fa and Ub :: "'b set" and fb
begin

sublocale semigroup_pair_ow Ua fa Ub fb ..
sublocale rev: cancel_semigroup_pair_ow Ub fb Ua fa ..

end

locale cancel_semigroup_pair_syntax_ow = semigroup_pair_syntax_ow Ua fa Ub fb
for Ua :: "'a set" and fa and Ub :: "'b set" and fb

subsubsection‹Transfer rules›

lemma cancel_semigroup_ow[ud_with]:

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 = (λfa fb. cancel_semigroup_pair_ow UNIV fa UNIV fb)"
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

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

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 =
alga: cancel_comm_semigroup_ow Ua fa fia +
algb: cancel_comm_semigroup_ow Ub fb fib
for Ua :: "'a set" and fa fia and Ub :: "'b set" and fb fib
begin

sublocale comm_semigroup_pair_ow Ua fa Ub fb ..
sublocale rev: cancel_comm_semigroup_pair_ow Ub fb fib Ua fa fia ..

end

locale cancel_comm_semigroup_pair_syntax_ow =
comm_semigroup_pair_syntax_ow Ua fa Ub fb +
binary_op_ow Ua fia +
binary_op_ow Ub fib
for Ua :: "'a set" and fa fia and Ub :: "'b set" and fb fib
begin

notation fia (infixl a 65)
notation fib (infixl b 65)

end

subsubsection‹Transfer rules›

lemma cancel_comm_semigroup_ow[ud_with]:

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 =
(λfa fia fb fib. cancel_comm_semigroup_pair_ow UNIV fa fia UNIV fb fib)"
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

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

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