# Theory SML_Groups

```(* Title: Examples/SML_Relativization/Algebra/SML_Groups.thy
Author: Mihails Milehins
*)
section‹Relativization of the results about groups›
theory SML_Groups
imports SML_Monoids
begin

subsection‹Simple groups›

subsubsection‹Definitions and common properties›

locale group_ow = semigroup_ow U f for U :: "'ag set" and f +
fixes z (‹❙1⇩o⇩w›)
and inverse :: "'ag ⇒ 'ag"
assumes z_closed[simp]: "❙1⇩o⇩w ∈ U"
and inverse_closed[simp]: "a ∈ U ⟹ inverse a ∈ U"
and group_left_neutral: "a ∈ U ⟹ ❙1⇩o⇩w ❙*⇩o⇩w a = a"
and left_inverse[simp]: "a ∈ U ⟹ inverse a ❙*⇩o⇩w a = ❙1⇩o⇩w"
begin

notation z (‹❙1⇩o⇩w›)

lemma inverse_closed': "inverse ` U ⊆ U" by auto
lemma inverse_closed'': "∀x∈U. inverse x ∈ U" by auto

lemma left_cancel:
assumes "a ∈ U" and "b ∈ U" and "c ∈ U"
shows "a ❙*⇩o⇩w b = a ❙*⇩o⇩w c ⟷ b = c"
proof
assume "a ❙*⇩o⇩w b = a ❙*⇩o⇩w c"
then have "inverse a ❙*⇩o⇩w (a ❙*⇩o⇩w b) = inverse a ❙*⇩o⇩w (a ❙*⇩o⇩w c)" by simp
with assms have "(inverse a ❙*⇩o⇩w a) ❙*⇩o⇩w b = (inverse a ❙*⇩o⇩w a) ❙*⇩o⇩w c"
by (metis assoc inverse_closed)
with assms show "b = c"
using group_ow_axioms by (fastforce simp: group_ow.group_left_neutral)
qed simp

sublocale monoid_ow U ‹(❙*⇩o⇩w)› ‹❙1⇩o⇩w›
proof
show "a ∈ U ⟹ a ❙*⇩o⇩w ❙1⇩o⇩w = a" for a
proof-
assume "a ∈ U"
with left_inverse[OF this] have "inverse a ❙*⇩o⇩w (a ❙*⇩o⇩w ❙1⇩o⇩w) = inverse a ❙*⇩o⇩w a"
by (metis assoc group_left_neutral inverse_closed z_closed)
with ‹a ∈ U› z_closed show "a ❙*⇩o⇩w ❙1⇩o⇩w = a"
by (meson left_cancel f_closed inverse_closed)
qed

lemma inverse_image[simp]: "inverse ` U ⊆ U" by (simp add: image_subsetI)

end

lemma group_ow: "group = group_ow UNIV"
unfolding
group_def group_ow_def  group_axioms_def group_ow_axioms_def semigroup_ow
by simp

locale uminus_ow =
fixes U :: "'ag set" and uminus :: "'ag ⇒ 'ag" (‹-⇩o⇩w _› [81] 80)
assumes uminus_closed: "a ∈ U ⟹ -⇩o⇩w a ∈ U"
begin

notation uminus (‹-⇩o⇩w _› [81] 80)

lemma uminus_closed': "uminus ` U ⊆ U" by (auto simp: uminus_closed)
lemma uminus_closed'': "∀a∈U. -⇩o⇩w a ∈ U" by (simp add: uminus_closed)

tts_register_sbts uminus | U by (rule tts_AB_transfer[OF uminus_closed'])

end

minus_ow U minus + uminus_ow U uminus + monoid_add_ow U plus zero
for U :: "'ag set" and minus plus zero uminus +
assumes left_inverse: "a ∈ U ⟹ (-⇩o⇩w a) +⇩o⇩w a = 0⇩o⇩w"
and add_inv_conv_diff: "⟦ a ∈ U; b ∈ U ⟧ ⟹ a +⇩o⇩w (-⇩o⇩w b) = a -⇩o⇩w b"
begin

sublocale add: group_ow U ‹(+⇩o⇩w)› ‹0⇩o⇩w› uminus
by unfold_locales (auto simp: uminus_closed left_inverse)

lemma inverse_unique:
assumes "a ∈ U" and "b ∈ U" and "a +⇩o⇩w b = 0⇩o⇩w"
shows "-⇩o⇩w a = b"
proof-
from assms have "(-⇩o⇩w a +⇩o⇩w a) +⇩o⇩w b = -⇩o⇩w a"
thus ?thesis
unfolding left_inverse[OF ‹a ∈ U›] add.left_neutral_mow[OF ‹b ∈ U›] by simp
qed

lemma inverse_neutral[simp]: "-⇩o⇩w 0⇩o⇩w = 0⇩o⇩w"
by
(
rule inverse_unique[
]
)

lemma inverse_inverse:
assumes "a ∈ U"
shows "-⇩o⇩w (-⇩o⇩w a) = a"
by
(
rule inverse_unique[
OF uminus_closed[OF assms] assms left_inverse[OF assms]
]
)

lemma right_inverse:
assumes "a ∈ U"
shows "a +⇩o⇩w (-⇩o⇩w a) = 0⇩o⇩w"
proof -
from assms have "a +⇩o⇩w (-⇩o⇩w a) = -⇩o⇩w (-⇩o⇩w a) +⇩o⇩w (-⇩o⇩w a)"
moreover have "… = 0⇩o⇩w" by (rule left_inverse[OF uminus_closed[OF assms]])
ultimately show ?thesis by simp
qed

proof
fix a b c assume "a ∈ U" and "b ∈ U" and "c ∈ U" and "a +⇩o⇩w b = a +⇩o⇩w c"
from ‹a ∈ U› ‹b ∈ U› ‹c ∈ U› this have
"((-⇩o⇩w a) +⇩o⇩w a) +⇩o⇩w b = ((-⇩o⇩w a) +⇩o⇩w a) +⇩o⇩w c"
thus "b = c"
unfolding
left_inverse[OF ‹a ∈ U›]
by simp
next
fix a b c assume "a ∈ U" and "b ∈ U" and "c ∈ U" and "b +⇩o⇩w a = c +⇩o⇩w a"
then have "b +⇩o⇩w (a +⇩o⇩w (-⇩o⇩w a)) = c +⇩o⇩w (a +⇩o⇩w (-⇩o⇩w a))"
thus "b = c"
unfolding
right_inverse[OF ‹a ∈ U›]
by (simp add: ‹b ∈ U›)
qed

end

unfolding
minus_ow_def uminus_ow_def
by simp

subsubsection‹Transfer rules›

context
includes lifting_syntax
begin

lemma group_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_unique A" "right_total A"
shows "((A ===> A ===> A) ===> A ===> (A ===> A) ===> (=))
(group_ow (Collect (Domainp A))) group"
proof -
let ?P = "((A ===> A ===> A) ===> A ===> (A ===> A) ===> (=))"
let ?group_ow = "group_ow (Collect (Domainp A))"
have
"?P
(λf z inv. ?group_ow f z inv)
(λf z inv. z ∈ UNIV ∧ (∀x∈UNIV. inv x ∈ UNIV) ∧ group f z inv)"
unfolding group_ow_def group_def group_ow_axioms_def group_axioms_def
apply transfer_prover_start
apply transfer_step+
by blast
thus ?thesis by simp
qed

assumes [transfer_rule]: "bi_unique A" "right_total A"
shows
"((A ===> A ===> A) ===> (A ===> A ===> A) ===> A ===> (A ===> A) ===> (=))
proof -
let ?P =
"((A ===> A ===> A) ===> (A ===> A ===> A) ===> A ===> (A ===> A) ===> (=))"
have
"?P
(λminus plus zero uminus. ?group_add_ow minus plus zero uminus)
(
λfi f z inv_f.
(∀x∈UNIV. ∀y∈UNIV. fi x y ∈ UNIV) ∧
(∀x∈UNIV. inv_f x ∈ UNIV) ∧
)"
unfolding
minus_ow_def uminus_ow_def
apply transfer_prover_start
apply transfer_step+
by simp
thus ?thesis by simp
qed

end

subsubsection‹Relativization›

context group_ow
begin

tts_context
tts: (?'a to U)
rewriting ctr_simps
substituting group_ow_axioms and not_empty
applying [OF f_closed' z_closed inverse_closed'']
begin

tts_lemma inverse_neutral: "inverse ❙1⇩o⇩w = ❙1⇩o⇩w"
is group.inverse_neutral.

tts_lemma inverse_inverse:
assumes "a ∈ U"
shows "inverse (inverse a) = a"
is group.inverse_inverse.

tts_lemma right_inverse:
assumes "a ∈ U"
shows "a ❙*⇩o⇩w inverse a = ❙1⇩o⇩w"
is group.right_inverse.

tts_lemma inverse_distrib_swap:
assumes "a ∈ U" and "b ∈ U"
shows "inverse (a ❙*⇩o⇩w b) = inverse b ❙*⇩o⇩w inverse a"
is group.inverse_distrib_swap.

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

tts_lemma inverse_unique:
assumes "a ∈ U" and "b ∈ U" and "a ❙*⇩o⇩w b = ❙1⇩o⇩w"
shows "inverse a = b"
is group.inverse_unique.
end

end

begin

tts_context
tts: (?'a to U)
rewriting ctr_simps
applying [OF minus_closed' plus_closed' zero_closed add.inverse_closed'']
begin

tts_lemma diff_0:
assumes "a ∈ U"
shows "0⇩o⇩w -⇩o⇩w a = -⇩o⇩w a"

tts_lemma diff_0_right:
assumes "a ∈ U"
shows "a -⇩o⇩w 0⇩o⇩w = a"

tts_lemma diff_self:
assumes "a ∈ U"
shows "a -⇩o⇩w a = 0⇩o⇩w"

tts_lemma group_left_neutral:
assumes "a ∈ U"
shows "0⇩o⇩w +⇩o⇩w a = a"

tts_lemma minus_minus:
assumes "a ∈ U"
shows "-⇩o⇩w (-⇩o⇩w a) = a"

tts_lemma right_minus:
assumes "a ∈ U"
shows "a +⇩o⇩w -⇩o⇩w a = 0⇩o⇩w"

tts_lemma left_minus:
assumes "a ∈ U"
shows "-⇩o⇩w a +⇩o⇩w a = 0⇩o⇩w"

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

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

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

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

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

tts_lemma minus_diff_eq:
assumes "a ∈ U" and "b ∈ U"
shows "-⇩o⇩w (a -⇩o⇩w b) = b -⇩o⇩w a"

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

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

tts_lemma neg_0_equal_iff_equal:
assumes "a ∈ U"
shows "(0⇩o⇩w = -⇩o⇩w a) = (0⇩o⇩w = a)"

tts_lemma neg_equal_0_iff_equal:
assumes "a ∈ U"
shows "(-⇩o⇩w a = 0⇩o⇩w) = (a = 0⇩o⇩w)"

tts_lemma eq_iff_diff_eq_0:
assumes "a ∈ U" and "b ∈ U"
shows "(a = b) = (a -⇩o⇩w b = 0⇩o⇩w)"

tts_lemma equation_minus_iff:
assumes "a ∈ U" and "b ∈ U"
shows "(a = -⇩o⇩w b) = (b = -⇩o⇩w a)"

tts_lemma minus_equation_iff:
assumes "a ∈ U" and "b ∈ U"
shows "(-⇩o⇩w a = b) = (-⇩o⇩w b = a)"

tts_lemma neg_equal_iff_equal:
assumes "a ∈ U" and "b ∈ U"
shows "(-⇩o⇩w a = -⇩o⇩w b) = (a = b)"

tts_lemma right_minus_eq:
assumes "a ∈ U" and "b ∈ U"
shows "(a -⇩o⇩w b = 0⇩o⇩w) = (a = b)"

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

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

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

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

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

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

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

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

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

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

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

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

tts_lemma minus_unique:
assumes "a ∈ U" and "b ∈ U" and "a +⇩o⇩w b = 0⇩o⇩w"
shows "-⇩o⇩w a = b"

tts_lemma diff_eq_diff_eq:
assumes "a ∈ U" and "b ∈ U" and "c ∈ U" and "d ∈ U" and "a -⇩o⇩w b = c -⇩o⇩w d"
shows "(a = b) = (c = d)"

end

end

subsection‹Abelian groups›

subsubsection‹Definitions and common properties›

minus_ow U minus + uminus_ow U uminus + comm_monoid_add_ow U plus zero
for U :: "'ag set" and plus zero minus uminus +
assumes ab_left_minus: "a ∈ U ⟹ -⇩o⇩w a +⇩o⇩w a = 0⇩o⇩w"
"⟦ a ∈ U; b ∈ U ⟧ ⟹ a -⇩o⇩w b = a +⇩o⇩w (-⇩o⇩w b)"
begin

apply unfold_locales
done

end

unfolding
minus_ow_def uminus_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 ===> A) ===> (A ===> A) ===> (=))
proof -
let ?P =
"((A ===> A ===> A) ===> A ===> (A ===> A ===> A) ===> (A ===> A) ===> (=))"
have
"?P
(
λplus zero minus uminus.
(∀x∈UNIV. ∀y∈UNIV. minus x y ∈ UNIV) ∧
(∀x∈UNIV. uminus x ∈ UNIV) ∧
)"
unfolding
minus_ow_def uminus_ow_def
apply transfer_prover_start
apply transfer_step+
by simp
thus ?thesis by simp
qed

end

subsubsection‹Relativization›

begin

tts_context
tts: (?'a to U)
rewriting ctr_simps
applying [OF plus_closed' zero_closed minus_closed' add.inverse_closed'']
begin

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