Theory Set_Semigroups

(* Title: Examples/TTS_Foundations/Algebra/Set_Semigroups.thy
   Author: Mihails Milehins
   Copyright 2021 (C) Mihails Milehins
*)
section‹Abstract semigroups on sets›
theory Set_Semigroups
  imports 
    Type_Semigroups 
    FNDS_Auxiliary
    "../Foundations/FNDS_Lifting_Set_Ext"
begin



subsection‹Background›

text‹The results presented in this section were ported 
(with amendments and additions) from the theory \<^text>‹Groups› in the main 
library of Isabelle/HOL.›



subsection‹Binary operations›


text‹Abstract binary operation.›

locale binary_op_base_ow = 
  fixes U :: "'a set" and f :: "'a ⇒ 'a ⇒ 'a"

locale binary_op_ow = binary_op_base_ow U f for U :: "'a set" and f +
  assumes op_closed: "x ∈ U ⟹ y ∈ U ⟹ f x y ∈ U"

locale binary_op_syntax_ow = binary_op_base_ow U f for U :: "'a set" and f
begin

notation f (infixl ‹⊕⇩a› 70)

end


text‹Concrete syntax.›

locale plus_ow = binary_op_ow U plus for U :: "'a set" and plus
begin

notation plus (infixl ‹+⇩a› 65)

end

locale minus_ow = binary_op_ow U minus for U :: "'a set" and minus
begin

notation minus (infixl ‹-⇩a› 65)

end

locale times_ow = binary_op_ow U times for U :: "'a set" and times
begin

notation times (infixl ‹*⇩a› 70)

end

locale divide_ow = binary_op_ow U divide for U :: "'a set" and divide
begin

notation divide (infixl ‹'/⇩a› 70)

end


text‹Pairs.›

locale binary_op_base_pair_ow = 
  alg⇩a: binary_op_base_ow U⇩a f⇩a + alg⇩b: binary_op_base_ow U⇩b f⇩b
  for U⇩a :: "'a set" and f⇩a and U⇩b :: "'b set" and f⇩b

locale binary_op_pair_ow = alg⇩a: binary_op_ow U⇩a f⇩a + alg⇩b: binary_op_ow U⇩b f⇩b
  for U⇩a :: "'a set" and f⇩a and U⇩b :: "'b set" and f⇩b
begin

sublocale binary_op_base_pair_ow U⇩a f⇩a U⇩b f⇩b .
sublocale rev: binary_op_base_pair_ow U⇩b f⇩b U⇩a f⇩a .

end

locale binary_op_pair_syntax_ow = binary_op_base_pair_ow U⇩a f⇩a U⇩b f⇩b
  for U⇩a :: "'a set" and f⇩a and U⇩b :: "'b set" and f⇩b
begin

notation f⇩a (infixl ‹⊕⇩a› 70)
notation f⇩b (infixl ‹⊕⇩b› 70)

end


subsubsection‹Results›

context binary_op_ow
begin

interpretation binary_op_syntax_ow .

lemma op_closed'[simp]: "∀x∈U. ∀y∈U. x ⊕⇩a y ∈ U" by (simp add: op_closed)

tts_register_sbts ‹(⊕⇩a)› | U by (rule tts_AA_A_transfer[OF op_closed])

end



subsection‹Simple semigroups›


subsubsection‹Definitions›


text‹Abstract semigroup.›

locale semigroup_ow = binary_op_ow U f for U :: "'a set" and f +
  assumes assoc[tts_ac_simps]: 
    "⟦ a ∈ U; b ∈ U; c ∈ U ⟧ ⟹ f (f a b) c = f a (f b c)"

locale semigroup_syntax_ow = binary_op_syntax_ow U f for U :: "'a set" and f


text‹Concrete syntax.›

locale semigroup_add_ow = semigroup_ow U plus for U :: "'a set" and plus
begin

sublocale plus_ow U plus ..

end

locale semigroup_mult_ow = semigroup_ow U times for U :: "'a set" and times
begin

sublocale times_ow U times ..

end


text‹Pairs.›

locale semigroup_pair_ow = alg⇩a: semigroup_ow U⇩a f⇩a + alg⇩b: semigroup_ow U⇩b f⇩b 
  for U⇩a :: "'a set" and f⇩a and U⇩b :: "'b set" and f⇩b
begin

sublocale binary_op_pair_ow U⇩a f⇩a U⇩b f⇩b ..
sublocale rev: semigroup_pair_ow U⇩b f⇩b U⇩a f⇩a ..

end

locale semigroup_pair_syntax_ow = binary_op_pair_syntax_ow U⇩a f⇩a U⇩b f⇩b
  for U⇩a :: "'a set" and f⇩a and U⇩b :: "'b set" and f⇩b


subsubsection‹Transfer rules›

lemma semigroup_ow[ud_with]: "semigroup = semigroup_ow UNIV"
  unfolding 
    semigroup_def semigroup_ow_def semigroup_ow_axioms_def binary_op_ow_def
  by simp

lemma semigroup_pair_ow[ud_with]: 
  "semigroup_pair = (λf⇩a f⇩b. semigroup_pair_ow UNIV f⇩a UNIV f⇩b)"
  unfolding semigroup_pair_def semigroup_pair_ow_def ud_with by simp

context
  includes lifting_syntax
begin

lemma semigroup_ow_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "(rel_set A ===> (A ===> A ===> A) ===> (=)) semigroup_ow semigroup_ow"
  by 
    (
      ow_locale_transfer locale_defs: 
        semigroup_ow_def semigroup_ow_axioms_def binary_op_ow_def
    )

lemma semigroup_pair_ow_transfer[transfer_rule]:
  assumes [transfer_rule]: 
    "bi_unique A" "right_total A" "bi_unique B" "right_total B"
  shows 
    "(
      rel_set A ===> (A ===> A ===> A) ===>  
      rel_set B ===> (B ===> B ===> B) ===> 
      (=)
    ) 
    semigroup_pair_ow semigroup_pair_ow"
  by (ow_locale_transfer locale_defs: semigroup_pair_ow_def)

end



subsection‹Commutative semigroups›


subsubsection‹Definitions›


text‹Abstract commutative semigroup.›

locale comm_semigroup_ow = semigroup_ow U f for U :: "'a set" and f +
  assumes commute[tts_ac_simps]: "a ∈ U ⟹ b ∈ U ⟹ f a b = f b a"

locale comm_semigroup_syntax_ow = semigroup_syntax_ow U f 
  for U :: "'a set" and f


text‹Concrete syntax.›

locale comm_semigroup_add_ow = comm_semigroup_ow U plus 
  for U :: "'a set" and plus
begin

sublocale semigroup_add_ow U plus ..

end

locale comm_semigroup_mult_ow = comm_semigroup_ow U times 
  for U :: "'a set" and times
begin

sublocale semigroup_mult_ow U times ..

end


text‹Pairs.›

locale comm_semigroup_pair_ow = 
  alg⇩a: comm_semigroup_ow U⇩a f⇩a + alg⇩b: comm_semigroup_ow U⇩b f⇩b  
  for U⇩a :: "'a set" and f⇩a and U⇩b :: "'b set" and f⇩b
begin

sublocale semigroup_pair_ow U⇩a f⇩a U⇩b f⇩b ..
sublocale rev: comm_semigroup_pair_ow U⇩b f⇩b U⇩a f⇩a ..

end

locale comm_semigroup_pair_syntax_ow = semigroup_pair_syntax_ow U⇩a f⇩a U⇩b f⇩b
  for U⇩a :: "'a set" and f⇩a and U⇩b :: "'b set" and f⇩b


subsubsection‹Transfer rules›

lemma comm_semigroup_ow[ud_with]: "comm_semigroup = comm_semigroup_ow UNIV"
  unfolding 
    comm_semigroup_def comm_semigroup_axioms_def
    comm_semigroup_ow_def comm_semigroup_ow_axioms_def 
    ud_with
  by simp

lemma comm_semigroup_pair_ow[ud_with]: 
  "comm_semigroup_pair = (λf⇩a f⇩b. comm_semigroup_pair_ow UNIV f⇩a UNIV f⇩b)"
  unfolding comm_semigroup_pair_def comm_semigroup_pair_ow_def ud_with 
  by simp

context
  includes lifting_syntax
begin

lemma comm_semigroup_ow_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "(rel_set A ===> (A ===> A ===> A) ===> (=)) 
      comm_semigroup_ow comm_semigroup_ow"
  by 
    (
      ow_locale_transfer locale_defs: 
        comm_semigroup_ow_def comm_semigroup_ow_axioms_def
    )

lemma comm_semigroup_pair_ow_transfer[transfer_rule]:
  assumes [transfer_rule]: 
    "bi_unique A" "right_total A" "bi_unique B" "right_total B"
  shows 
    "(
      rel_set A ===> (A ===> A ===> A) ===>  
      rel_set B ===> (B ===> B ===> B) ===> 
      (=)
    ) 
    comm_semigroup_pair_ow comm_semigroup_pair_ow"
  by (ow_locale_transfer locale_defs: comm_semigroup_pair_ow_def)

end


subsubsection‹Relativization›

context comm_semigroup_ow
begin

interpretation comm_semigroup_syntax_ow .

tts_context
  tts: (?'a to U)
  substituting comm_semigroup_ow_axioms
  eliminating through auto
begin

tts_lemma left_commute:
  assumes "b ∈ U"
    and "a ∈ U"
    and "c ∈ U"
  shows "b ⊕⇩a (a ⊕⇩a c) = a ⊕⇩a (b ⊕⇩a c)"
    is comm_semigroup.left_commute.

end

end



subsection‹Cancellative semigroups›


subsubsection‹Definitions›


text‹Abstract cancellative semigroup.›

locale cancel_semigroup_ow = semigroup_ow U f for U :: "'a set" and f +
  assumes add_left_imp_eq: 
    "⟦ a ∈ U; b ∈ U; c ∈ U; f a b = f a c ⟧ ⟹ b = c"
  assumes add_right_imp_eq: 
    "⟦ b ∈ U; a ∈ U; c ∈ U; f b a = f c a ⟧ ⟹ b = c"

locale cancel_semigroup_syntax_ow = semigroup_syntax_ow U f 
  for U :: "'a set" and f


text‹Concrete syntax.›

locale cancel_semigroup_add_ow = cancel_semigroup_ow U plus 
  for U :: "'a set" and plus
begin

sublocale semigroup_add_ow U plus ..

end

locale cancel_semigroup_mult_ow = cancel_semigroup_ow U times 
  for U :: "'a set" and times
begin

sublocale semigroup_mult_ow U times ..

end


text‹Pairs.›

locale cancel_semigroup_pair_ow = 
  alg⇩a: cancel_semigroup_ow U⇩a f⇩a + alg⇩b: cancel_semigroup_ow U⇩b f⇩b 
  for U⇩a :: "'a set" and f⇩a and U⇩b :: "'b set" and f⇩b
begin

sublocale semigroup_pair_ow U⇩a f⇩a U⇩b f⇩b ..
sublocale rev: cancel_semigroup_pair_ow U⇩b f⇩b U⇩a f⇩a ..

end

locale cancel_semigroup_pair_syntax_ow = semigroup_pair_syntax_ow U⇩a f⇩a U⇩b f⇩b
  for U⇩a :: "'a set" and f⇩a and U⇩b :: "'b set" and f⇩b


subsubsection‹Transfer rules›

lemma cancel_semigroup_ow[ud_with]: 
  "cancel_semigroup = cancel_semigroup_ow UNIV"
  unfolding 
    cancel_semigroup_def cancel_semigroup_axioms_def
    cancel_semigroup_ow_def cancel_semigroup_ow_axioms_def 
    ud_with
  by simp

lemma cancel_semigroup_pair_ow[ud_with]: 
  "cancel_semigroup_pair = (λf⇩a f⇩b. cancel_semigroup_pair_ow UNIV f⇩a UNIV f⇩b)"
  unfolding cancel_semigroup_pair_def cancel_semigroup_pair_ow_def ud_with 
  by simp

context
  includes lifting_syntax
begin

lemma cancel_semigroup_ow_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "(rel_set A ===> (A ===> A ===> A) ===> (=)) 
      cancel_semigroup_ow cancel_semigroup_ow"
  by 
    (
      ow_locale_transfer locale_defs: 
        cancel_semigroup_ow_def cancel_semigroup_ow_axioms_def
    )

lemma cancel_semigroup_pair_ow_transfer[transfer_rule]:
  assumes [transfer_rule]: 
    "bi_unique A" "right_total A" "bi_unique B" "right_total B"
  shows 
    "(
      rel_set A ===> (A ===> A ===> A) ===>  
      rel_set B ===> (B ===> B ===> B) ===> 
      (=)
    ) cancel_semigroup_pair_ow cancel_semigroup_pair_ow"
  by (ow_locale_transfer locale_defs: cancel_semigroup_pair_ow_def)

end


subsubsection‹Relativization›

context cancel_semigroup_ow
begin

interpretation cancel_semigroup_syntax_ow .

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

tts_lemma add_right_cancel:
  assumes "b ∈ U" and "a ∈ U" and "c ∈ U"
  shows "(b ⊕⇩a a = c ⊕⇩a a) = (b = c)"
    is cancel_semigroup.add_right_cancel.

tts_lemma add_left_cancel:
  assumes "a ∈ U" and "b ∈ U" and "c ∈ U"
  shows "(a ⊕⇩a b = a ⊕⇩a c) = (b = c)"
    is cancel_semigroup.add_left_cancel.    
  
tts_lemma inj_on_add':
  assumes "a ∈ U" and "A ⊆ U"
  shows "inj_on (λb. b ⊕⇩a a) A"
    is cancel_semigroup.inj_on_add'.

tts_lemma inj_on_add:
  assumes "a ∈ U" and "A ⊆ U"
  shows "inj_on ((⊕⇩a) a) A"
    is cancel_semigroup.inj_on_add.

tts_lemma bij_betw_add:
  assumes "a ∈ U" and "A ⊆ U" and "B ⊆ U"
  shows "bij_betw ((⊕⇩a) a) A B = ((⊕⇩a) a ` A = B)"
    is cancel_semigroup.bij_betw_add.

end

end



subsection‹Cancellative commutative semigroups›


subsubsection‹Definitions›


text‹Abstract cancellative commutative semigroups.›

locale cancel_comm_semigroup_ow = comm_semigroup_ow U f + binary_op_ow U fi 
  for U :: "'a set" and f fi +
  assumes add_diff_cancel_left'[simp]: "⟦ a ∈ U; b ∈ U ⟧ ⟹ fi (f a b) a = b"
    and diff_diff_add[tts_algebra_simps, tts_field_simps]: 
    "⟦ a ∈ U; b ∈ U; c ∈ U ⟧ ⟹ fi (fi a b) c = fi a (f b c)"

locale cancel_comm_semigroup_syntax_ow = 
  comm_semigroup_syntax_ow U f + binary_op_base_ow U fi 
  for U :: "'a set" and f fi 
begin

notation fi (infixl ‹⊖⇩a› 65)

end


text‹Concrete syntax.›

locale cancel_comm_semigroup_add_ow = cancel_comm_semigroup_ow U plus minus 
  for U :: "'a set" and plus minus
begin

sublocale comm_semigroup_add_ow U plus ..
sublocale minus_ow U minus ..

end

locale cancel_comm_semigroup_mult = cancel_comm_semigroup_ow U times divide 
  for U :: "'a set" and times divide
begin

sublocale comm_semigroup_mult_ow U times ..
sublocale divide_ow U divide ..

end


text‹Pairs.›

locale cancel_comm_semigroup_pair_ow = 
  alg⇩a: cancel_comm_semigroup_ow U⇩a f⇩a fi⇩a + 
  alg⇩b: cancel_comm_semigroup_ow U⇩b f⇩b fi⇩b
  for U⇩a :: "'a set" and f⇩a fi⇩a and U⇩b :: "'b set" and f⇩b fi⇩b
begin

sublocale comm_semigroup_pair_ow U⇩a f⇩a U⇩b f⇩b ..
sublocale rev: cancel_comm_semigroup_pair_ow U⇩b f⇩b fi⇩b U⇩a f⇩a fi⇩a ..

end

locale cancel_comm_semigroup_pair_syntax_ow = 
  comm_semigroup_pair_syntax_ow U⇩a f⇩a U⇩b f⇩b + 
  binary_op_ow U⇩a fi⇩a + 
  binary_op_ow U⇩b fi⇩b
  for U⇩a :: "'a set" and f⇩a fi⇩a and U⇩b :: "'b set" and f⇩b fi⇩b
begin

notation fi⇩a (infixl ‹⊖⇩a› 65)
notation fi⇩b (infixl ‹⊖⇩b› 65)

end


subsubsection‹Transfer rules›

lemma cancel_comm_semigroup_ow[ud_with]: 
  "cancel_comm_semigroup = cancel_comm_semigroup_ow UNIV"
  unfolding 
    cancel_comm_semigroup_def cancel_comm_semigroup_axioms_def
    cancel_comm_semigroup_ow_def cancel_comm_semigroup_ow_axioms_def 
    binary_op_ow_def
    ud_with
  by simp

lemma cancel_comm_semigroup_pair_ow[ud_with]: 
  "cancel_comm_semigroup_pair = 
    (λf⇩a fi⇩a f⇩b fi⇩b. cancel_comm_semigroup_pair_ow UNIV f⇩a fi⇩a UNIV f⇩b fi⇩b)"
  unfolding 
    cancel_comm_semigroup_pair_def cancel_comm_semigroup_pair_ow_def ud_with 
  by simp

context
  includes lifting_syntax
begin

lemma cancel_comm_semigroup_ow_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A" 
  shows 
    "(rel_set A ===> (A ===> A ===> A) ===> (A ===> A ===> A) ===> (=)) 
      cancel_comm_semigroup_ow cancel_comm_semigroup_ow"
  by 
    (
      ow_locale_transfer locale_defs: 
        cancel_comm_semigroup_ow_def 
        cancel_comm_semigroup_ow_axioms_def
        binary_op_ow_def
    )

lemma cancel_comm_semigroup_pair_ow_transfer[transfer_rule]:
  assumes [transfer_rule]: 
    "bi_unique A" "right_total A" "bi_unique B" "right_total B"
  shows 
    "(
      rel_set A ===> (A ===> A ===> A) ===> (A ===> A ===> A) ===>  
      rel_set B ===> (B ===> B ===> B) ===> (B ===> B ===> B) ===> 
      (=)
    ) cancel_comm_semigroup_pair_ow cancel_comm_semigroup_pair_ow"
  by (ow_locale_transfer locale_defs: cancel_comm_semigroup_pair_ow_def)

end


subsubsection‹Relativization›

context cancel_comm_semigroup_ow
begin

interpretation cancel_comm_semigroup_syntax_ow .

tts_context
  tts: (?'a to U)
  sbterms: (‹?f::?'a ⇒ ?'a ⇒ ?'a› to f)
    and (‹?fi::?'a ⇒ ?'a ⇒ ?'a› to fi)
  rewriting ctr_simps
  substituting cancel_comm_semigroup_ow_axioms
  eliminating through auto
begin

tts_lemma add_diff_cancel_right':
  assumes "a ∈ U" and "b ∈ U"
  shows "a ⊕⇩a b ⊖⇩a b = a"
    is cancel_comm_semigroup.add_diff_cancel_right'.
    
tts_lemma add_diff_cancel_right:
  assumes "a ∈ U" and "c ∈ U" and "b ∈ U"
  shows "a ⊕⇩a c ⊖⇩a b ⊕⇩a c = a ⊖⇩a b"
    is cancel_comm_semigroup.add_diff_cancel_right.

tts_lemma add_diff_cancel_left:
  assumes "c ∈ U" and "a ∈ U" and "b ∈ U"
  shows "c ⊕⇩a a ⊖⇩a c ⊕⇩a b = a ⊖⇩a b"
    is cancel_comm_semigroup.add_diff_cancel_left.

tts_lemma diff_right_commute:
  assumes "a ∈ U" and "c ∈ U" and "b ∈ U"
  shows "a ⊖⇩a c ⊖⇩a b = a ⊖⇩a b ⊖⇩a c"
    is cancel_comm_semigroup.diff_right_commute.

tts_lemma cancel_semigroup_axioms:
  assumes "U ≠ {}"
  shows "cancel_semigroup_ow U (⊕⇩a)"
    is cancel_comm_semigroup.cancel_semigroup_axioms.

end

sublocale cancel_semigroup_ow
  using 
    cancel_semigroup_axioms 
    cancel_semigroup_ow.intro 
    cancel_semigroup_ow_axioms_def 
    semigroup_ow_axioms 
  by auto

end

context cancel_comm_semigroup_pair_ow
begin

sublocale cancel_semigroup_pair_ow ..

end

text‹\newpage›

end