Theory SML_Groups

(* Title: Examples/SML_Relativization/Algebra/SML_Groups.thy
   Author: Mihails Milehins
   Copyright 2021 (C) 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'': "∀x∈U. 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
qed (simp add: group_left_neutral)+

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" (‹-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'': "∀a∈U. -ow a ∈ U" by (simp add: uminus_closed)

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

end

locale group_add_ow =
  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"
    by (metis add.assoc uminus_closed add.right_neutral_mow) 
  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[
        OF zero_closed zero_closed add.left_neutral_mow[OF zero_closed]
        ]                                     
    )

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)"
    by (simp add: inverse_inverse)
  moreover have "… = 0ow" by (rule left_inverse[OF uminus_closed[OF assms]])
  ultimately show ?thesis by simp
qed

sublocale cancel_semigroup_add_ow U ‹(+ow)›
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"
    by (auto simp: add.left_cancel)
  thus "b = c" 
    unfolding
      left_inverse[OF ‹a ∈ U›]
      add.left_neutral_mow[OF ‹b ∈ U›] 
      add.left_neutral_mow[OF ‹c ∈ 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))" 
    by (metis add.assoc uminus_closed)
  thus "b = c"
    unfolding 
      right_inverse[OF ‹a ∈ U›]
      add.left_neutral_mow[OF ‹b ∈ U›] 
      add.right_neutral_mow[OF ‹c ∈ U›]
    by (simp add: ‹b ∈ U›)
qed

end

lemma group_add_ow: "class.group_add = group_add_ow UNIV"
  unfolding 
    class.group_add_def group_add_ow_def
    class.group_add_axioms_def group_add_ow_axioms_def
    minus_ow_def uminus_ow_def
    monoid_add_ow 
  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

lemma group_add_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A"
  shows 
    "((A ===> A ===> A) ===> (A ===> A ===> A) ===> A ===> (A ===> A) ===> (=)) 
      (group_add_ow (Collect (Domainp A))) class.group_add"
proof -
  let ?P = 
    "((A ===> A ===> A) ===> (A ===> A ===> A) ===> A ===> (A ===> A) ===> (=))"
  let ?group_add_ow = "group_add_ow (Collect (Domainp 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) ∧  
          class.group_add fi f z inv_f
      )"
    unfolding 
      group_add_ow_def class.group_add_def
      group_add_ow_axioms_def class.group_add_axioms_def
      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

context group_add_ow
begin

tts_context
  tts: (?'a to U)
  rewriting ctr_simps
  substituting group_add_ow_axioms and zero.not_empty
  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"
    is group_add_class.diff_0.

tts_lemma diff_0_right:
  assumes "a ∈ U"
  shows "a -ow 0ow = a"
    is group_add_class.diff_0_right.
    
tts_lemma diff_self:
  assumes "a ∈ U"
  shows "a -ow a = 0ow"
    is group_add_class.diff_self.
    
tts_lemma group_left_neutral:
  assumes "a ∈ U"
  shows "0ow +ow a = a"
    is group_add_class.add.group_left_neutral.
    
tts_lemma minus_minus:
  assumes "a ∈ U"
  shows "-ow (-ow a) = a"
  is group_add_class.minus_minus.
    
tts_lemma right_minus:
  assumes "a ∈ U"
  shows "a +ow -ow a = 0ow"
  is group_add_class.right_minus.

tts_lemma left_minus:
  assumes "a ∈ U"
  shows "-ow a +ow a = 0ow"
    is group_add_class.left_minus.
    
tts_lemma add_diff_cancel:
  assumes "a ∈ U" and "b ∈ U"
  shows "a +ow b -ow b = a"
  is group_add_class.add_diff_cancel.
    
tts_lemma diff_add_cancel:
  assumes "a ∈ U" and "b ∈ U"
  shows "a -ow b +ow b = a"
    is group_add_class.diff_add_cancel.
    
tts_lemma diff_conv_add_uminus:
  assumes "a ∈ U" and "b ∈ U"
  shows "a -ow b = a +ow -ow b"
    is group_add_class.diff_conv_add_uminus.
    
tts_lemma diff_minus_eq_add:
  assumes "a ∈ U" and "b ∈ U"
  shows "a -ow -ow b = a +ow b"
    is group_add_class.diff_minus_eq_add.
  
tts_lemma add_uminus_conv_diff:
  assumes "a ∈ U" and "b ∈ U"
  shows "a +ow -ow b = a -ow b"
    is group_add_class.add_uminus_conv_diff.

tts_lemma minus_diff_eq:
  assumes "a ∈ U" and "b ∈ U"
  shows "-ow (a -ow b) = b -ow a"
    is group_add_class.minus_diff_eq.

tts_lemma add_minus_cancel:
  assumes "a ∈ U" and "b ∈ U"
  shows "a +ow (-ow a +ow b) = b"
    is group_add_class.add_minus_cancel.
    
tts_lemma minus_add_cancel:
  assumes "a ∈ U" and "b ∈ U"
  shows "-ow a +ow (a +ow b) = b"
    is group_add_class.minus_add_cancel.

tts_lemma neg_0_equal_iff_equal:
  assumes "a ∈ U"
  shows "(0ow = -ow a) = (0ow = a)"
    is group_add_class.neg_0_equal_iff_equal.
    
tts_lemma neg_equal_0_iff_equal:
  assumes "a ∈ U"
  shows "(-ow a = 0ow) = (a = 0ow)"
    is group_add_class.neg_equal_0_iff_equal.
    
tts_lemma eq_iff_diff_eq_0:
  assumes "a ∈ U" and "b ∈ U"
  shows "(a = b) = (a -ow b = 0ow)"
    is group_add_class.eq_iff_diff_eq_0.

tts_lemma equation_minus_iff:
  assumes "a ∈ U" and "b ∈ U"
  shows "(a = -ow b) = (b = -ow a)"
    is group_add_class.equation_minus_iff.

tts_lemma minus_equation_iff:
  assumes "a ∈ U" and "b ∈ U"
  shows "(-ow a = b) = (-ow b = a)"
    is group_add_class.minus_equation_iff.

tts_lemma neg_equal_iff_equal:
  assumes "a ∈ U" and "b ∈ U"
  shows "(-ow a = -ow b) = (a = b)"
    is group_add_class.neg_equal_iff_equal.

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

tts_lemma minus_add:
  assumes "a ∈ U" and "b ∈ U"
  shows "-ow (a +ow b) = -ow b +ow -ow a"
    is group_add_class.minus_add.

tts_lemma eq_neg_iff_add_eq_0:
  assumes "a ∈ U" and "b ∈ U"
  shows "(a = -ow b) = (a +ow b = 0ow)"
    is group_add_class.eq_neg_iff_add_eq_0.

tts_lemma neg_eq_iff_add_eq_0:
  assumes "a ∈ U" and "b ∈ U"
  shows "(-ow a = b) = (a +ow b = 0ow)"
    is group_add_class.neg_eq_iff_add_eq_0.

tts_lemma add_eq_0_iff2:
  assumes "a ∈ U" and "b ∈ U"
  shows "(a +ow b = 0ow) = (a = -ow b)"
    is group_add_class.add_eq_0_iff2.

tts_lemma add_eq_0_iff:
  assumes "a ∈ U" and "b ∈ U"
  shows "(a +ow b = 0ow) = (b = -ow a)"
    is group_add_class.add_eq_0_iff.

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"
    is group_add_class.diff_diff_eq2.

tts_lemma diff_add_eq_diff_diff_swap:
  assumes "a ∈ U" and "b ∈ U" and "c ∈ U"
  shows "a -ow (b +ow c) = a -ow c -ow b"
    is group_add_class.diff_add_eq_diff_diff_swap.

tts_lemma add_diff_eq:
  assumes "a ∈ U" and "b ∈ U" and "c ∈ U"
  shows "a +ow (b -ow c) = a +ow b -ow c"
    is group_add_class.add_diff_eq.

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

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

tts_lemma left_cancel:
  assumes "a ∈ U" and "b ∈ U" and "c ∈ U"
  shows "(a +ow b = a +ow c) = (b = c)"
    is group_add_class.add.left_cancel.

tts_lemma right_cancel:
  assumes "b ∈ U" and "a ∈ U" and "c ∈ U"
  shows "(b +ow a = c +ow a) = (b = c)"
    is group_add_class.add.right_cancel.

tts_lemma minus_unique:
  assumes "a ∈ U" and "b ∈ U" and "a +ow b = 0ow"
  shows "-ow a = b"
    is group_add_class.minus_unique.

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)"
    is group_add_class.diff_eq_diff_eq.

end

end



subsection‹Abelian groups›


subsubsection‹Definitions and common properties›

locale ab_group_add_ow =
  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"
  assumes ab_diff_conv_add_uminus: 
    "⟦ a ∈ U; b ∈ U ⟧ ⟹ a -ow b = a +ow (-ow b)"
begin

sublocale group_add_ow 
  by unfold_locales (simp_all add: ab_left_minus ab_diff_conv_add_uminus)

sublocale cancel_comm_monoid_add_ow 
  apply unfold_locales
  subgoal using add.commute by (fastforce simp: add_diff_cancel)
  subgoal by (metis add.commute diff_add_eq_diff_diff_swap)
  done

end

lemma ab_group_add_ow: "class.ab_group_add = ab_group_add_ow UNIV"
  unfolding 
  class.ab_group_add_def ab_group_add_ow_def
  class.ab_group_add_axioms_def ab_group_add_ow_axioms_def
  minus_ow_def uminus_ow_def
  comm_monoid_add_ow
  by simp

lemma ab_group_add_ow_UNIV_axioms: 
  "ab_group_add_ow (UNIV::'a::ab_group_add set) (+) 0 (-) uminus"
  by (fold ab_group_add_ow) (rule ab_group_add_class.ab_group_add_axioms)


subsubsection‹Transfer rules›

context
  includes lifting_syntax
begin

lemma ab_group_add_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "((A ===> A ===> A) ===> A ===> (A ===> A ===> A) ===> (A ===> A) ===> (=))
      (ab_group_add_ow (Collect (Domainp A))) class.ab_group_add"
proof -
  let ?P = 
    "((A ===> A ===> A) ===> A ===> (A ===> A ===> A) ===> (A ===> A) ===> (=))"
  let ?ab_group_add_ow = "ab_group_add_ow (Collect (Domainp A))"
  have 
    "?P 
      ?ab_group_add_ow 
      (
        λplus zero minus uminus. 
          (∀x∈UNIV. ∀y∈UNIV. minus x y ∈ UNIV) ∧
          (∀x∈UNIV. uminus x ∈ UNIV) ∧  
          class.ab_group_add plus zero minus uminus
      )"
    unfolding 
      ab_group_add_ow_def class.ab_group_add_def
      ab_group_add_ow_axioms_def class.ab_group_add_axioms_def
      minus_ow_def uminus_ow_def
    apply transfer_prover_start
    apply transfer_step+
    by simp
  thus ?thesis by simp
qed

end


subsubsection‹Relativization›

context ab_group_add_ow
begin

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

tts_lemma uminus_add_conv_diff:
  assumes "a ∈ U" and "b ∈ U"
  shows "-ow a +ow b = b -ow a"
    is ab_group_add_class.uminus_add_conv_diff.
    
tts_lemma diff_add_eq:
  assumes "a ∈ U" and "b ∈ U" and "c ∈ U"
  shows "a -ow b +ow c = a +ow c -ow b"
    is ab_group_add_class.diff_add_eq.

end

end

text‹\newpage›

end