Theory SML_Semigroups

(* Title: Examples/SML_Relativization/Algebra/SML_Semigroups.thy
   Author: Mihails Milehins
   Copyright 2021 (C) 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 ‹*ow› 70)
  assumes f_closed: "⟦ a ∈ U; b ∈ U ⟧ ⟹ a *ow b ∈ U"
  assumes assoc: "⟦ a ∈ U; b ∈ U; c ∈ U ⟧ ⟹ a *ow b *ow c = a *ow (b *ow c)"
begin

notation f (infixl ‹*ow› 70)

lemma f_closed'[simp]: "∀x∈U. ∀y∈U. x *ow y ∈ U" by (simp add: f_closed)

tts_register_sbts ‹(*ow)› | 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 ‹+ow› 65)
  assumes plus_closed[simp, intro]: "⟦ a ∈ U; b ∈ U ⟧ ⟹ a +ow b ∈ U"
begin

notation plus (infixl ‹+ow› 65)

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

tts_register_sbts ‹(+ow)› | U  by (rule tts_AA_A_transfer[OF plus_closed])

end

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

notation times (infixl ‹*ow› 70)

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

tts_register_sbts ‹(*ow)› | 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 +ow b +ow c = a +ow (b +ow c)"
begin

sublocale add: semigroup_ow U ‹(+ow)› 
  by unfold_locales (auto simp: plus_assoc)

end

lemma semigroup_add_ow: "class.semigroup_add = semigroup_add_ow UNIV"
  unfolding 
    class.semigroup_add_def semigroup_add_ow_def
    semigroup_add_ow_axioms_def plus_ow_def
  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 *ow b *ow c = a *ow (b *ow c)"
begin

sublocale mult: semigroup_ow U ‹(*ow)› 
  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

lemma semigroup_add_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "((A ===> A ===> A) ===> (=)) 
      (semigroup_add_ow (Collect (Domainp A))) class.semigroup_add"
proof -
  let ?P = "((A ===> A ===> A) ===> (=))"
  let ?semigroup_add_ow = "(λf. semigroup_add_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_add_ow (λf. ?rf_UNIV f ∧ class.semigroup_add f)"
    unfolding 
      semigroup_add_ow_def class.semigroup_add_def
      semigroup_add_ow_axioms_def plus_ow_def
    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›
 
locale cancel_semigroup_add_ow = semigroup_add_ow U plus
  for U :: "'ag set" and plus +
  assumes add_left_imp_eq: 
    "⟦ a ∈ U; b ∈ U; c ∈ U; a +ow b = a +ow c ⟧ ⟹ b = c"
  assumes add_right_imp_eq: 
    "⟦ b ∈ U; a ∈ U; c ∈ U; b +ow a = c +ow a ⟧ ⟹ b = c"

lemma cancel_semigroup_add_ow: 
  "class.cancel_semigroup_add = cancel_semigroup_add_ow UNIV"
  unfolding 
    class.cancel_semigroup_add_def cancel_semigroup_add_ow_def
    cancel_semigroup_add_ow_axioms_def class.cancel_semigroup_add_axioms_def
    semigroup_add_ow
  by simp


subsubsection‹Transfer rules›

context
  includes lifting_syntax
begin

lemma cancel_semigroup_add_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "((A ===> A ===> A) ===> (=)) 
      (cancel_semigroup_add_ow (Collect (Domainp A)))  
      class.cancel_semigroup_add"
  unfolding cancel_semigroup_add_ow_def class.cancel_semigroup_add_def
  unfolding 
    cancel_semigroup_add_ow_axioms_def class.cancel_semigroup_add_axioms_def
  apply transfer_prover_start
  apply transfer_step+
  by simp

end


subsubsection‹Relativization›

context cancel_semigroup_add_ow
begin

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

tts_lemma add_right_cancel:
  assumes "b ∈ U" and "a ∈ U" and "c ∈ U"
  shows "(b +ow a = c +ow a) = (b = c)"
  is cancel_semigroup_add_class.add_right_cancel.

tts_lemma add_left_cancel:
  assumes "a ∈ U" and "b ∈ U" and "c ∈ U"
  shows "(a +ow b = a +ow c) = (b = c)"
  is cancel_semigroup_add_class.add_left_cancel.
    
tts_lemma bij_betw_add:
  assumes "a ∈ U" and "A ⊆ U" and "B ⊆ U"
  shows "bij_betw ((+ow) a) A B = ((+ow) a ` A = B)"
    is cancel_semigroup_add_class.bij_betw_add.

tts_lemma inj_on_add:
  assumes "a ∈ U" and "A ⊆ U"
  shows "inj_on ((+ow) a) A"
    is cancel_semigroup_add_class.inj_on_add.

tts_lemma inj_on_add':
  assumes "a ∈ U" and "A ⊆ U"
  shows "inj_on (λb. b +ow a) A"
    is cancel_semigroup_add_class.inj_on_add'.

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 *ow b = b *ow a"
begin

lemma fun_left_comm: 
  assumes "x ∈ U" and "y ∈ U" and "z ∈ U" 
  shows "y *ow (x *ow z) = x *ow (y *ow 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

locale ab_semigroup_add_ow =
  semigroup_add_ow U plus for U :: "'ag set" and plus +
  assumes add_commute: "⟦ a ∈ U; b ∈ U ⟧ ⟹ a +ow b = b +ow a"
begin

sublocale add: abel_semigroup_ow U ‹(+ow)› 
  by unfold_locales (rule add_commute)
  
end

lemma ab_semigroup_add_ow: "class.ab_semigroup_add = ab_semigroup_add_ow UNIV"
  unfolding 
    class.ab_semigroup_add_def ab_semigroup_add_ow_def
    class.ab_semigroup_add_axioms_def ab_semigroup_add_ow_axioms_def
    semigroup_add_ow
  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 *ow b = b *ow a"
begin

sublocale mult: abel_semigroup_ow U ‹(*ow)› 
  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

lemma ab_semigroup_add_transfer[transfer_rule]:
  assumes[transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "((A ===> A ===> A) ===> (=)) 
      (ab_semigroup_add_ow (Collect (Domainp A))) class.ab_semigroup_add"
  unfolding 
    ab_semigroup_add_ow_def class.ab_semigroup_add_def
    ab_semigroup_add_ow_axioms_def class.ab_semigroup_add_axioms_def
  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 *ow (a *ow c) = a *ow (b *ow c)"
    is abel_semigroup.left_commute.

end

end

context ab_semigroup_add_ow
begin

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

tts_lemma add_ac:
  shows "⟦a ∈ U; b ∈ U; c ∈ U⟧ ⟹ a +ow b +ow c = a +ow (b +ow c)"
    is ab_semigroup_add_class.add_ac(1)
    and "⟦a ∈ U; b ∈ U⟧ ⟹ a +ow b = b +ow a"
    is ab_semigroup_add_class.add_ac(2)
    and "⟦b ∈ U; a ∈ U; c ∈ U⟧ ⟹ b +ow (a +ow c) = a +ow (b +ow c)"
    is ab_semigroup_add_class.add_ac(3).

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 *ow b *ow c = a *ow (b *ow c)"
    is ab_semigroup_mult_class.mult_ac(1)
    and "⟦a ∈ U; b ∈ U⟧ ⟹ a *ow b = b *ow a"
    is ab_semigroup_mult_class.mult_ac(2)
    and "⟦b ∈ U; a ∈ U; c ∈ U⟧ ⟹ b *ow (a *ow c) = a *ow (b *ow 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 ‹-ow› 65)
  assumes minus_closed[simp,intro]: "⟦ a ∈ U; b ∈ U ⟧ ⟹ a -ow b ∈ U"
begin

notation minus (infixl ‹-ow› 65)

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

tts_register_sbts ‹(-ow)› | U by (rule tts_AA_A_transfer[OF minus_closed])

end

locale cancel_ab_semigroup_add_ow = 
  ab_semigroup_add_ow U plus + minus_ow U minus
  for U :: "'ag set" and plus minus +
  assumes add_diff_cancel_left'[simp]: 
    "⟦ a ∈ U; b ∈ U ⟧ ⟹ (a +ow b) -ow a = b"
  assumes diff_diff_add: 
    "⟦ a ∈ U; b ∈ U; c ∈ U ⟧ ⟹ a -ow b -ow c = a -ow (b +ow c)"
begin

sublocale cancel_semigroup_add_ow U ‹(+ow)›
  apply unfold_locales
  subgoal by (metis add_diff_cancel_left')
  subgoal by (metis add.commute add_diff_cancel_left')
  done

end

lemma cancel_ab_semigroup_add_ow: 
  "class.cancel_ab_semigroup_add = cancel_ab_semigroup_add_ow UNIV"
  unfolding 
    class.cancel_ab_semigroup_add_def 
    cancel_ab_semigroup_add_ow_def
    class.cancel_ab_semigroup_add_axioms_def
    cancel_ab_semigroup_add_ow_axioms_def
    minus_ow_def
    ab_semigroup_add_ow
  by simp


subsubsection‹Transfer rules›

context
  includes lifting_syntax
begin

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

end


subsubsection‹Relativization›

context cancel_ab_semigroup_add_ow
begin

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

tts_lemma add_diff_cancel_right':
  assumes "a ∈ U" and "b ∈ U"
  shows "a +ow b -ow b = a"
    is cancel_ab_semigroup_add_class.add_diff_cancel_right'.

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

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

tts_lemma diff_right_commute:
  assumes "a ∈ U" and "c ∈ U" and "b ∈ U"
  shows "a -ow c -ow b = a -ow b -ow c"
    is cancel_ab_semigroup_add_class.diff_right_commute.

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

end

end

text‹\newpage›

end