# 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 (1ow)
and inverse :: "'ag  'ag"
assumes z_closed[simp]: "1ow  U"
and inverse_closed[simp]: "a  U  inverse a  U"
and group_left_neutral: "a  U  1ow *ow a = a"
and left_inverse[simp]: "a  U  inverse a *ow a = 1ow"
begin

notation z (1ow)

lemma inverse_closed': "inverse ` U  U" by auto
lemma inverse_closed'': "xU. inverse x  U" by auto

lemma left_cancel:
assumes "a  U" and "b  U" and "c  U"
shows "a *ow b = a *ow c  b = c"
proof
assume "a *ow b = a *ow c"
then have "inverse a *ow (a *ow b) = inverse a *ow (a *ow c)" by simp
with assms have "(inverse a *ow a) *ow b = (inverse a *ow a) *ow 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 (*ow) 1ow
proof
show "a  U  a *ow 1ow = a" for a
proof-
assume "a  U"
with left_inverse[OF this] have "inverse a *ow (a *ow 1ow) = inverse a *ow a"
by (metis assoc group_left_neutral inverse_closed z_closed)
with a  U z_closed show "a *ow 1ow = 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:
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" (-ow _› [81] 80)
assumes uminus_closed: "a  U  -ow a  U"
begin

notation uminus (-ow _› [81] 80)

lemma uminus_closed': "uminus ` U  U" by (auto simp: uminus_closed)
lemma uminus_closed'': "aU. -ow 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  (-ow a) +ow a = 0ow"
and add_inv_conv_diff: " a  U; b  U   a +ow (-ow b) = a -ow b"
begin

sublocale add: group_ow U (+ow) 0ow uminus
by unfold_locales (auto simp: uminus_closed left_inverse)

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

lemma inverse_neutral[simp]: "-ow 0ow = 0ow"
by
(
rule inverse_unique[
]
)

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

lemma right_inverse:
assumes "a  U"
shows "a +ow (-ow a) = 0ow"
proof -
from assms have "a +ow (-ow a) = -ow (-ow a) +ow (-ow a)"
moreover have " = 0ow" 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 +ow b = a +ow c"
from a  U b  U c  U this have
"((-ow a) +ow a) +ow b = ((-ow a) +ow a) +ow 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 +ow a = c +ow a"
then have "b +ow (a +ow (-ow a)) = c +ow (a +ow (-ow a))"
thus "b = c"
unfolding
right_inverse[OF a  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  (xUNIV. 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.
(xUNIV. yUNIV. fi x y  UNIV)
(xUNIV. 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 1ow = 1ow"
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 *ow inverse a = 1ow"
is group.right_inverse.

tts_lemma inverse_distrib_swap:
assumes "a  U" and "b  U"
shows "inverse (a *ow b) = inverse b *ow inverse a"
is group.inverse_distrib_swap.

tts_lemma right_cancel:
assumes "b  U" and "a  U" and "c  U"
shows "(b *ow a = c *ow a) = (b = c)"
is group.right_cancel.

tts_lemma inverse_unique:
assumes "a  U" and "b  U" and "a *ow b = 1ow"
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 "0ow -ow a = -ow a"

tts_lemma diff_0_right:
assumes "a  U"
shows "a -ow 0ow = a"

tts_lemma diff_self:
assumes "a  U"
shows "a -ow a = 0ow"

tts_lemma group_left_neutral:
assumes "a  U"
shows "0ow +ow a = a"

tts_lemma minus_minus:
assumes "a  U"
shows "-ow (-ow a) = a"

tts_lemma right_minus:
assumes "a  U"
shows "a +ow -ow a = 0ow"

tts_lemma left_minus:
assumes "a  U"
shows "-ow a +ow a = 0ow"

assumes "a  U" and "b  U"
shows "a +ow b -ow b = a"

assumes "a  U" and "b  U"
shows "a -ow b +ow b = a"

assumes "a  U" and "b  U"
shows "a -ow b = a +ow -ow b"

assumes "a  U" and "b  U"
shows "a -ow -ow b = a +ow b"

assumes "a  U" and "b  U"
shows "a +ow -ow b = a -ow b"

tts_lemma minus_diff_eq:
assumes "a  U" and "b  U"
shows "-ow (a -ow b) = b -ow a"

assumes "a  U" and "b  U"
shows "a +ow (-ow a +ow b) = b"

assumes "a  U" and "b  U"
shows "-ow a +ow (a +ow b) = b"

tts_lemma neg_0_equal_iff_equal:
assumes "a  U"
shows "(0ow = -ow a) = (0ow = a)"

tts_lemma neg_equal_0_iff_equal:
assumes "a  U"
shows "(-ow a = 0ow) = (a = 0ow)"

tts_lemma eq_iff_diff_eq_0:
assumes "a  U" and "b  U"
shows "(a = b) = (a -ow b = 0ow)"

tts_lemma equation_minus_iff:
assumes "a  U" and "b  U"
shows "(a = -ow b) = (b = -ow a)"

tts_lemma minus_equation_iff:
assumes "a  U" and "b  U"
shows "(-ow a = b) = (-ow b = a)"

tts_lemma neg_equal_iff_equal:
assumes "a  U" and "b  U"
shows "(-ow a = -ow b) = (a = b)"

tts_lemma right_minus_eq:
assumes "a  U" and "b  U"
shows "(a -ow b = 0ow) = (a = b)"

assumes "a  U" and "b  U"
shows "-ow (a +ow b) = -ow b +ow -ow a"

assumes "a  U" and "b  U"
shows "(a = -ow b) = (a +ow b = 0ow)"

assumes "a  U" and "b  U"
shows "(-ow a = b) = (a +ow b = 0ow)"

assumes "a  U" and "b  U"
shows "(a +ow b = 0ow) = (a = -ow b)"

assumes "a  U" and "b  U"
shows "(a +ow b = 0ow) = (b = -ow a)"

tts_lemma diff_diff_eq2:
assumes "a  U" and "b  U" and "c  U"
shows "a -ow (b -ow c) = a +ow c -ow b"

assumes "a  U" and "b  U" and "c  U"
shows "a -ow (b +ow c) = a -ow c -ow b"

assumes "a  U" and "b  U" and "c  U"
shows "a +ow (b -ow c) = a +ow b -ow c"

tts_lemma eq_diff_eq:
assumes "a  U" and "c  U" and "b  U"
shows "(a = c -ow b) = (a +ow b = c)"

tts_lemma diff_eq_eq:
assumes "a  U" and "b  U" and "c  U"
shows "(a -ow b = c) = (a = c +ow b)"

tts_lemma left_cancel:
assumes "a  U" and "b  U" and "c  U"
shows "(a +ow b = a +ow c) = (b = c)"

tts_lemma right_cancel:
assumes "b  U" and "a  U" and "c  U"
shows "(b +ow a = c +ow a) = (b = c)"

tts_lemma minus_unique:
assumes "a  U" and "b  U" and "a +ow b = 0ow"
shows "-ow a = b"

tts_lemma diff_eq_diff_eq:
assumes "a  U" and "b  U" and "c  U" and "d  U" and "a -ow b = c -ow 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  -ow a +ow a = 0ow"
" a  U; b  U   a -ow b = a +ow (-ow 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.
(xUNIV. yUNIV. minus x y  UNIV)
(xUNIV. 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 "-ow a +ow b = b -ow a"