Theory Type_Semigroups

(* Title: Examples/TTS_Foundations/Algebra/Type_Semigroups.thy
   Author: Mihails Milehins
   Copyright 2021 (C) Mihails Milehins
*)
section‹Abstract semigroups on types›
theory Type_Semigroups
  imports Main
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‹Preliminaries›

named_theorems tts_ac_simps "assoc. and comm. simplification rules"
  and tts_algebra_simps "algebra simplification rules"
  and tts_field_simps "algebra simplification rules for fields"



subsection‹Binary operations›


text‹Abstract operation.›

locale binary_op = 
  fixes f :: "'a ⇒ 'a ⇒ 'a"

locale binary_op_syntax = binary_op f for f :: "'a ⇒ 'a ⇒ 'a"
begin

notation f (infixl ‹⊕⇩a› 65)

end


text‹Concrete syntax.›

locale plus = binary_op plus for plus :: "'a ⇒ 'a ⇒ 'a"
begin

notation plus (infixl ‹+⇩a› 65)

end

locale minus = binary_op minus for minus :: "'a ⇒ 'a ⇒ 'a"
begin

notation minus (infixl ‹-⇩a› 65)

end

locale times = binary_op times for times :: "'a ⇒ 'a ⇒ 'a"
begin

notation times (infixl ‹*⇩a› 70)

end

locale divide = binary_op divide for divide :: "'a ⇒ 'a ⇒ 'a"
begin

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

end


text‹Pairs.›

locale binary_op_pair = alg⇩a: binary_op f⇩a + alg⇩b: binary_op f⇩b
  for f⇩a :: "'a ⇒ 'a ⇒ 'a" and f⇩b :: "'b ⇒ 'b ⇒ 'b"

locale binary_op_pair_syntax = binary_op_pair f⇩a f⇩b
  for f⇩a :: "'a ⇒ 'a ⇒ 'a" and f⇩b :: "'b ⇒ 'b ⇒ 'b"
begin

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

end



subsection‹Simple semigroups›


subsubsection‹Definitions›


text‹Abstract semigroups.›

locale semigroup = binary_op f for f :: "'a ⇒ 'a ⇒ 'a" +
  assumes assoc[tts_ac_simps, tts_algebra_simps]: "f (f a b) c = f a (f b c)"

locale semigroup_syntax = binary_op_syntax f for f :: "'a ⇒ 'a ⇒ 'a"


text‹Concrete syntax.›

locale semigroup_add = semigroup plus for plus :: "'a ⇒ 'a ⇒ 'a"
begin

sublocale plus plus .

end

locale semigroup_mult = semigroup times for times :: "'a ⇒ 'a ⇒ 'a"
begin

sublocale times times .

end


text‹Pairs.›

locale semigroup_pair = alg⇩a: semigroup f⇩a + alg⇩b: semigroup f⇩b 
  for f⇩a :: "'a ⇒ 'a ⇒ 'a" and f⇩b :: "'b ⇒ 'b ⇒ 'b"
begin

sublocale binary_op_pair f⇩a f⇩b .
sublocale rev: semigroup_pair f⇩b f⇩a ..

end

locale semigroup_pair_syntax = binary_op_pair_syntax



subsection‹Commutative semigroups›


subsubsection‹Definitions›


text‹Abstract commutative semigroup.›

locale comm_semigroup = semigroup f for f :: "'a ⇒ 'a ⇒ 'a" +
  assumes commute[tts_ac_simps, tts_algebra_simps]: "f a b = f b a"

locale comm_semigroup_syntax = semigroup_syntax


text‹Concrete syntax.›

locale comm_semigroup_add = comm_semigroup plus for plus :: "'a ⇒ 'a ⇒ 'a"
begin

sublocale semigroup_add plus ..

end

locale comm_semigroup_mult = comm_semigroup times for times :: "'a ⇒ 'a ⇒ 'a"
begin

sublocale semigroup_mult times ..

end


text‹Pairs.›

locale comm_semigroup_pair = alg⇩a: comm_semigroup f⇩a + alg⇩b: comm_semigroup f⇩b 
  for f⇩a :: "'a ⇒ 'a ⇒ 'a" and f⇩b :: "'b ⇒ 'b ⇒ 'b"
begin

sublocale semigroup_pair f⇩a f⇩b ..
sublocale rev: comm_semigroup_pair f⇩b f⇩a ..

end

locale comm_semigroup_pair_syntax = semigroup_pair_syntax



subsubsection‹Results›

context comm_semigroup
begin

interpretation comm_semigroup_syntax f .

lemma left_commute[tts_ac_simps, tts_algebra_simps, field_simps]: 
  "b ⊕⇩a (a ⊕⇩a c) = a ⊕⇩a (b ⊕⇩a c)"
proof -
  have "(b ⊕⇩a a) ⊕⇩a c = (a ⊕⇩a b) ⊕⇩a c" by (simp add: commute)
  then show ?thesis by (simp only: assoc)
qed

end



subsection‹Cancellative semigroups›


subsubsection‹Definitions›


text‹Abstract cancellative semigroup.›

locale cancel_semigroup = semigroup f for f :: "'a ⇒ 'a ⇒ 'a" +
  assumes add_left_imp_eq: "f a b = f a c ⟹ b = c"
  assumes add_right_imp_eq: "f b a = f c a ⟹ b = c"

locale cancel_semigroup_syntax = semigroup_syntax f for f :: "'a ⇒ 'a ⇒ 'a"


text‹Concrete syntax.›

locale cancel_semigroup_add = cancel_semigroup plus 
  for plus :: "'a ⇒ 'a ⇒ 'a"
begin

sublocale semigroup_add plus ..

end

locale cancel_semigroup_mult = cancel_semigroup times 
  for times :: "'a ⇒ 'a ⇒ 'a"
begin

sublocale semigroup_mult times ..

end


text‹Pairs.›

locale cancel_semigroup_pair = 
  alg⇩a: cancel_semigroup f⇩a + alg⇩b: cancel_semigroup f⇩b 
  for f⇩a :: "'a ⇒ 'a ⇒ 'a" and f⇩b :: "'b ⇒ 'b ⇒ 'b"
begin

sublocale semigroup_pair f⇩a f⇩b ..
sublocale rev: cancel_semigroup_pair f⇩b f⇩a ..

end

locale cancel_semigroup_pair_syntax = semigroup_pair_syntax f⇩a f⇩b
  for f⇩a :: "'a ⇒ 'a ⇒ 'a" and f⇩b :: "'b ⇒ 'b ⇒ 'b"


subsubsection‹Results›

context cancel_semigroup
begin

interpretation cancel_semigroup_syntax f .

lemma add_left_cancel[simp]: "a ⊕⇩a b = a ⊕⇩a c ⟷ b = c"
  by (blast dest: add_left_imp_eq)

lemma add_right_cancel[simp]: "b ⊕⇩a a = c ⊕⇩a a ⟷ b = c"
  by (blast dest: add_right_imp_eq)

lemma inj_on_add[simp]: "inj_on ((⊕⇩a) a) A" by (rule inj_onI) simp

lemma inj_on_add'[simp]: "inj_on (λb. b ⊕⇩a a) A" by (rule inj_onI) simp

lemma bij_betw_add[simp]: "bij_betw ((⊕⇩a) a) A B ⟷ (⊕⇩a) a ` A = B"
  by (simp add: bij_betw_def)

end



subsection‹Cancellative commutative semigroups›


subsubsection‹Definitions›


text‹Abstract cancellative commutative semigroups.›

locale cancel_comm_semigroup = comm: comm_semigroup f + binary_op fi 
  for f fi :: "'a ⇒ 'a ⇒ 'a" +
  assumes add_diff_cancel_left'[simp]: "fi (f a b) a = b"
    and diff_diff_add[tts_algebra_simps, tts_field_simps]: 
    "fi (fi a b) c = fi a (f b c)"

locale cancel_comm_semigroup_syntax = comm_semigroup_syntax f + binary_op fi 
  for f fi :: "'a ⇒ 'a ⇒ 'a"
begin

notation fi (infixl ‹⊖⇩a› 65)

end


text‹Concrete syntax.›

locale cancel_comm_semigroup_add = cancel_comm_semigroup plus minus 
  for plus minus :: "'a ⇒ 'a ⇒ 'a"
begin

sublocale comm_semigroup_add plus ..
sublocale minus minus .

end

locale cancel_comm_semigroup_mult = cancel_comm_semigroup times divide 
  for times divide :: "'a ⇒ 'a ⇒ 'a"
begin

sublocale comm_semigroup_mult times ..
sublocale divide divide .

end


text‹Pairs.›

locale cancel_comm_semigroup_pair = 
  alg⇩a: cancel_comm_semigroup f⇩a fi⇩a + alg⇩b: cancel_comm_semigroup f⇩b fi⇩b
  for f⇩a fi⇩a :: "'a ⇒ 'a ⇒ 'a" and f⇩b fi⇩b :: "'b ⇒ 'b ⇒ 'b"
begin

sublocale comm_semigroup_pair f⇩a f⇩b ..
sublocale rev: cancel_comm_semigroup_pair f⇩b fi⇩b f⇩a fi⇩a ..

end

locale cancel_comm_semigroup_pair_syntax = 
  comm_semigroup_pair_syntax f⇩a f⇩b + binary_op fi⇩a + binary_op fi⇩b
  for f⇩a fi⇩a f⇩b fi⇩b
begin

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

end


subsubsection‹Results›

context cancel_comm_semigroup
begin

interpretation cancel_comm_semigroup_syntax .

lemma add_diff_cancel_right'[simp]: "(a ⊕⇩a b) ⊖⇩a b = a"
  using add_diff_cancel_left'[of b a] by (simp add: tts_ac_simps)

sublocale cancel: cancel_semigroup
proof
  fix a b c :: 'a
  assume "a ⊕⇩a b = a ⊕⇩a c"
  then have "a ⊕⇩a b ⊖⇩a a = a ⊕⇩a c ⊖⇩a a" by simp
  then show "b = c" by simp
next
  fix a b c :: 'a
  assume "b ⊕⇩a a = c ⊕⇩a a"
  then have "b ⊕⇩a a ⊖⇩a a = c ⊕⇩a a ⊖⇩a a" by simp
  then show "b = c" by simp
qed

lemmas cancel_semigroup_axioms = cancel.cancel_semigroup_axioms

lemma add_diff_cancel_left[simp]: "(c ⊕⇩a a) ⊖⇩a (c ⊕⇩a b) = a ⊖⇩a b"
  unfolding diff_diff_add[symmetric] by simp

lemma add_diff_cancel_right[simp]: "(a ⊕⇩a c) ⊖⇩a (b ⊕⇩a c) = a ⊖⇩a b"
  using add_diff_cancel_left[symmetric] by (simp add: tts_ac_simps)

lemma diff_right_commute: "a ⊖⇩a c ⊖⇩a b = a ⊖⇩a b ⊖⇩a c"
  by (simp add: diff_diff_add comm.commute)

end

context cancel_comm_semigroup_pair
begin

sublocale cancel: cancel_semigroup_pair ..

lemmas cancel_semigroup_pair_axioms = cancel.cancel_semigroup_pair_axioms

end

text‹\newpage›

end