# Theory SML_Semigroups

```(* Title: Examples/SML_Relativization/Algebra/SML_Semigroups.thy
Author: Mihails Milehins
*)
section‹Relativization of the results about semigroups›
theory SML_Semigroups
imports
"../SML_Introduction"
"../Foundations/Lifting_Set_Ext"
begin

subsection‹Simple semigroups›

subsubsection‹Definitions and common properties›

locale semigroup_ow =
fixes U :: "'ag set" and f :: "['ag, 'ag] ⇒ 'ag" (infixl ‹❙*⇩o⇩w› 70)
assumes f_closed: "⟦ a ∈ U; b ∈ U ⟧ ⟹ a ❙*⇩o⇩w b ∈ U"
assumes assoc: "⟦ a ∈ U; b ∈ U; c ∈ U ⟧ ⟹ a ❙*⇩o⇩w b ❙*⇩o⇩w c = a ❙*⇩o⇩w (b ❙*⇩o⇩w c)"
begin

notation f (infixl ‹❙*⇩o⇩w› 70)

lemma f_closed'[simp]: "∀x∈U. ∀y∈U. x ❙*⇩o⇩w y ∈ U" by (simp add: f_closed)

tts_register_sbts ‹(❙*⇩o⇩w)› | U by (rule tts_AA_A_transfer[OF f_closed])

end

lemma semigroup_ow: "semigroup = semigroup_ow UNIV"
unfolding semigroup_def semigroup_ow_def by simp

locale plus_ow =
fixes U :: "'ag set" and plus :: "['ag, 'ag] ⇒ 'ag" (infixl ‹+⇩o⇩w› 65)
assumes plus_closed[simp, intro]: "⟦ a ∈ U; b ∈ U ⟧ ⟹ a +⇩o⇩w b ∈ U"
begin

notation plus (infixl ‹+⇩o⇩w› 65)

lemma plus_closed'[simp]: "∀x∈U. ∀y∈U. x +⇩o⇩w y ∈ U" by simp

tts_register_sbts ‹(+⇩o⇩w)› | U  by (rule tts_AA_A_transfer[OF plus_closed])

end

locale times_ow =
fixes U :: "'ag set" and times :: "['ag, 'ag] ⇒ 'ag" (infixl ‹*⇩o⇩w› 70)
assumes times_closed[simp, intro]: "⟦ a ∈ U; b ∈ U ⟧ ⟹ a *⇩o⇩w b ∈ U"
begin

notation times (infixl ‹*⇩o⇩w› 70)

lemma times_closed'[simp]: "∀x∈U. ∀y∈U. x *⇩o⇩w y ∈ U" by simp

tts_register_sbts ‹(*⇩o⇩w)› | U  by (rule tts_AA_A_transfer[OF times_closed])

end

locale semigroup_add_ow = plus_ow U plus
for U :: "'ag set" and plus +
assumes plus_assoc:
"⟦ a ∈ U; b ∈ U; c ∈ U ⟧ ⟹ a +⇩o⇩w b +⇩o⇩w c = a +⇩o⇩w (b +⇩o⇩w c)"
begin

by unfold_locales (auto simp: plus_assoc)

end

unfolding
by simp

locale semigroup_mult_ow = times_ow U times
for U :: "'ag set" and times +
assumes mult_assoc:
"⟦ a ∈ U; b ∈ U; c ∈ U ⟧ ⟹ a *⇩o⇩w b *⇩o⇩w c = a *⇩o⇩w (b *⇩o⇩w c)"
begin

sublocale mult: semigroup_ow U ‹(*⇩o⇩w)›
by unfold_locales (auto simp: times_closed' mult_assoc)

end

lemma semigroup_mult_ow: "class.semigroup_mult = semigroup_mult_ow UNIV"
unfolding
class.semigroup_mult_def semigroup_mult_ow_def
semigroup_mult_ow_axioms_def times_ow_def
by simp

subsubsection‹Transfer rules›

context
includes lifting_syntax
begin

lemma semigroup_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_unique A" "right_total A"
shows
"((A ===> A ===> A) ===> (=))
(semigroup_ow (Collect (Domainp A))) semigroup"
proof -
let ?P = "((A ===> A ===> A) ===> (=))"
let ?semigroup_ow = "semigroup_ow (Collect (Domainp A))"
let ?rf_UNIV =
"(λf::['b, 'b] ⇒ 'b. (∀x y. x ∈ UNIV ⟶ y ∈ UNIV ⟶ f x y ∈ UNIV))"
have "?P ?semigroup_ow (λf. ?rf_UNIV f ∧ semigroup f)"
unfolding semigroup_ow_def semigroup_def
apply transfer_prover_start
apply transfer_step+
by simp
thus ?thesis by simp
qed

assumes [transfer_rule]: "bi_unique A" "right_total A"
shows
"((A ===> A ===> A) ===> (=))
proof -
let ?P = "((A ===> A ===> A) ===> (=))"
let ?rf_UNIV =
"(λf::['b, 'b] ⇒ 'b. (∀x y. x ∈ UNIV ⟶ y ∈ UNIV ⟶ f x y ∈ UNIV))"
unfolding
apply transfer_prover_start
apply transfer_step+
by simp
thus ?thesis by simp
qed

lemma semigroup_mult_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_unique A" "right_total A"
shows
"((A ===> A ===> A) ===> (=))
(semigroup_mult_ow (Collect (Domainp A))) class.semigroup_mult"
proof -
let ?P = "((A ===> A ===> A) ===> (=))"
let ?semigroup_mult_ow = "(λf. semigroup_mult_ow (Collect (Domainp A)) f)"
let ?rf_UNIV =
"(λf::['b, 'b] ⇒ 'b. (∀x y. x ∈ UNIV ⟶ y ∈ UNIV ⟶ f x y ∈ UNIV))"
have "?P ?semigroup_mult_ow (λf. ?rf_UNIV f ∧ class.semigroup_mult f)"
unfolding
semigroup_mult_ow_def class.semigroup_mult_def
semigroup_mult_ow_axioms_def times_ow_def
apply transfer_prover_start
apply transfer_step+
by simp
thus ?thesis by simp
qed

end

subsection‹Cancellative semigroups›

subsubsection‹Definitions and common properties›

for U :: "'ag set" and plus +
"⟦ a ∈ U; b ∈ U; c ∈ U; a +⇩o⇩w b = a +⇩o⇩w c ⟧ ⟹ b = c"
"⟦ b ∈ U; a ∈ U; c ∈ U; b +⇩o⇩w a = c +⇩o⇩w a ⟧ ⟹ b = c"

unfolding
by simp

subsubsection‹Transfer rules›

context
includes lifting_syntax
begin

assumes [transfer_rule]: "bi_unique A" "right_total A"
shows
"((A ===> A ===> A) ===> (=))
unfolding
apply transfer_prover_start
apply transfer_step+
by simp

end

subsubsection‹Relativization›

begin

tts_context
tts: (?'a to U)
rewriting ctr_simps
eliminating through simp
begin

assumes "b ∈ U" and "a ∈ U" and "c ∈ U"
shows "(b +⇩o⇩w a = c +⇩o⇩w a) = (b = c)"

assumes "a ∈ U" and "b ∈ U" and "c ∈ U"
shows "(a +⇩o⇩w b = a +⇩o⇩w c) = (b = c)"

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

assumes "a ∈ U" and "A ⊆ U"
shows "inj_on ((+⇩o⇩w) a) A"

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

end

end

subsection‹Commutative semigroups›

subsubsection‹Definitions and common properties›

locale abel_semigroup_ow =
semigroup_ow U f for U :: "'ag set" and f +
assumes commute: "⟦ a ∈ U; b ∈ U ⟧ ⟹ a ❙*⇩o⇩w b = b ❙*⇩o⇩w a"
begin

lemma fun_left_comm:
assumes "x ∈ U" and "y ∈ U" and "z ∈ U"
shows "y ❙*⇩o⇩w (x ❙*⇩o⇩w z) = x ❙*⇩o⇩w (y ❙*⇩o⇩w z)"
using assms by (metis assoc commute)

end

lemma abel_semigroup_ow: "abel_semigroup = abel_semigroup_ow UNIV"
unfolding
abel_semigroup_def abel_semigroup_ow_def
abel_semigroup_axioms_def abel_semigroup_ow_axioms_def
semigroup_ow
by simp

semigroup_add_ow U plus for U :: "'ag set" and plus +
assumes add_commute: "⟦ a ∈ U; b ∈ U ⟧ ⟹ a +⇩o⇩w b = b +⇩o⇩w a"
begin

end

unfolding
by simp

locale ab_semigroup_mult_ow =
semigroup_mult_ow U times for U :: "'ag set" and times+
assumes mult_commute: "⟦ a ∈ U; b ∈ U ⟧ ⟹ a *⇩o⇩w b = b *⇩o⇩w a"
begin

sublocale mult: abel_semigroup_ow U ‹(*⇩o⇩w)›
by unfold_locales (rule mult_commute)

end

lemma ab_semigroup_mult_ow:
"class.ab_semigroup_mult = ab_semigroup_mult_ow UNIV"
unfolding
class.ab_semigroup_mult_def ab_semigroup_mult_ow_def
class.ab_semigroup_mult_axioms_def ab_semigroup_mult_ow_axioms_def
semigroup_mult_ow
by simp

subsubsection‹Transfer rules›

context
includes lifting_syntax
begin

lemma abel_semigroup_transfer[transfer_rule]:
assumes[transfer_rule]: "bi_unique A" "right_total A"
shows
"((A ===> A ===> A) ===> (=))
(abel_semigroup_ow (Collect (Domainp A))) abel_semigroup"
unfolding
abel_semigroup_ow_def abel_semigroup_def
abel_semigroup_ow_axioms_def abel_semigroup_axioms_def
apply transfer_prover_start
apply transfer_step+
unfolding Ball_def by simp

assumes[transfer_rule]: "bi_unique A" "right_total A"
shows
"((A ===> A ===> A) ===> (=))
unfolding
apply transfer_prover_start
apply transfer_step+
by simp

lemma ab_semigroup_mult_transfer[transfer_rule]:
assumes[transfer_rule]: "bi_unique A" "right_total A"
shows
"((A ===> A ===> A) ===> (=))
(ab_semigroup_mult_ow (Collect (Domainp A))) class.ab_semigroup_mult"
unfolding ab_semigroup_mult_ow_def class.ab_semigroup_mult_def
unfolding ab_semigroup_mult_ow_axioms_def class.ab_semigroup_mult_axioms_def
apply transfer_prover_start
apply transfer_step+
by simp

end

subsubsection‹Relativization›

context abel_semigroup_ow
begin

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

tts_lemma left_commute:
assumes "b ∈ U" and "a ∈ U" and "c ∈ U"
shows "b ❙*⇩o⇩w (a ❙*⇩o⇩w c) = a ❙*⇩o⇩w (b ❙*⇩o⇩w c)"
is abel_semigroup.left_commute.

end

end

begin

tts_context
tts: (?'a to U)
rewriting ctr_simps
eliminating through simp
begin

shows "⟦a ∈ U; b ∈ U; c ∈ U⟧ ⟹ a +⇩o⇩w b +⇩o⇩w c = a +⇩o⇩w (b +⇩o⇩w c)"
and "⟦a ∈ U; b ∈ U⟧ ⟹ a +⇩o⇩w b = b +⇩o⇩w a"
and "⟦b ∈ U; a ∈ U; c ∈ U⟧ ⟹ b +⇩o⇩w (a +⇩o⇩w c) = a +⇩o⇩w (b +⇩o⇩w c)"

end

end

context ab_semigroup_mult_ow
begin

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

tts_lemma mult_ac:
shows "⟦a ∈ U; b ∈ U; c ∈ U⟧ ⟹ a *⇩o⇩w b *⇩o⇩w c = a *⇩o⇩w (b *⇩o⇩w c)"
is ab_semigroup_mult_class.mult_ac(1)
and "⟦a ∈ U; b ∈ U⟧ ⟹ a *⇩o⇩w b = b *⇩o⇩w a"
is ab_semigroup_mult_class.mult_ac(2)
and "⟦b ∈ U; a ∈ U; c ∈ U⟧ ⟹ b *⇩o⇩w (a *⇩o⇩w c) = a *⇩o⇩w (b *⇩o⇩w c)"
is ab_semigroup_mult_class.mult_ac(3).

end

end

subsection‹Cancellative commutative semigroups›

subsubsection‹Definitions and common properties›

locale minus_ow =
fixes U :: "'ag set" and minus :: "['ag, 'ag] ⇒ 'ag" (infixl ‹-⇩o⇩w› 65)
assumes minus_closed[simp,intro]: "⟦ a ∈ U; b ∈ U ⟧ ⟹ a -⇩o⇩w b ∈ U"
begin

notation minus (infixl ‹-⇩o⇩w› 65)

lemma minus_closed'[simp]: "∀x∈U. ∀y∈U. x -⇩o⇩w y ∈ U" by simp

tts_register_sbts ‹(-⇩o⇩w)› | U by (rule tts_AA_A_transfer[OF minus_closed])

end

ab_semigroup_add_ow U plus + minus_ow U minus
for U :: "'ag set" and plus minus +
"⟦ a ∈ U; b ∈ U ⟧ ⟹ (a +⇩o⇩w b) -⇩o⇩w a = b"
"⟦ a ∈ U; b ∈ U; c ∈ U ⟧ ⟹ a -⇩o⇩w b -⇩o⇩w c = a -⇩o⇩w (b +⇩o⇩w c)"
begin

apply unfold_locales
done

end

unfolding
minus_ow_def
by simp

subsubsection‹Transfer rules›

context
includes lifting_syntax
begin

assumes [transfer_rule]: "bi_unique A" "right_total A"
shows
"((A ===> A ===> A) ===> (A ===> A ===> A) ===> (=))
proof -
let ?P = "((A ===> A ===> A) ===> (A ===> A ===> A) ===> (=))"
let ?rf_UNIV =
"(λf::['b, 'b] ⇒ 'b. (∀x y. x ∈ UNIV ⟶ y ∈ UNIV ⟶ f x y ∈ UNIV))"
have
"?P
(λf fi. ?rf_UNIV fi ∧ class.cancel_ab_semigroup_add f fi)"
unfolding
minus_ow_def
apply transfer_prover_start
apply transfer_step+
unfolding Ball_def by auto
thus ?thesis by simp
qed

end

subsubsection‹Relativization›

begin

tts_context
tts: (?'a to U)
rewriting ctr_simps
eliminating through simp
begin

assumes "a ∈ U" and "b ∈ U"
shows "a +⇩o⇩w b -⇩o⇩w b = a"

assumes "a ∈ U" and "c ∈ U" and "b ∈ U"
shows "a +⇩o⇩w c -⇩o⇩w (b +⇩o⇩w c) = a -⇩o⇩w b"

assumes "c ∈ U" and "a ∈ U" and "b ∈ U"
shows "c +⇩o⇩w a -⇩o⇩w (c +⇩o⇩w b) = a -⇩o⇩w b"

tts_lemma diff_right_commute:
assumes "a ∈ U" and "c ∈ U" and "b ∈ U"
shows "a -⇩o⇩w c -⇩o⇩w b = a -⇩o⇩w b -⇩o⇩w c"