Theory Monoid_Action

theory Monoid_Action
  imports Main
begin

section ‹General Results on Groups›

lemma (in monoid) right_inverse_idem:
  fixes inv
  assumes right_inverse:  "⋀a. a ❙* inv a = ❙1"
  shows "⋀a. inv (inv a) = a"
    by (metis assoc right_inverse right_neutral)

lemma (in monoid) left_inverse_if_right_inverse:
  fixes inv
  assumes
    right_inverse:  "⋀a. a ❙* inv a = ❙1"
  shows "inv a ❙* a = ❙1"
  by (metis right_inverse_idem right_inverse)

lemma (in monoid) group_wrt_right_inverse:
  fixes inv
  assumes right_inverse:  "⋀a. a ❙* inv a = ❙1"
  shows "group (❙*) ❙1 inv"
proof unfold_locales
  show "⋀a. ❙1 ❙* a = a"
    by simp
next
  show "⋀a. inv a ❙* a = ❙1"
    by (metis left_inverse_if_right_inverse right_inverse)
qed


section ‹Monoid›

definition (in monoid) is_left_invertible ✐‹contributor ‹Balazs Toth›› where
  "is_left_invertible a ⟷ (∃a_inv. a_inv ❙* a = ❙1)"

definition (in monoid) is_right_invertible ✐‹contributor ‹Balazs Toth›› where
  "is_right_invertible a ⟷ (∃a_inv. a ❙* a_inv = ❙1)"

definition (in monoid) left_inverse ✐‹contributor ‹Balazs Toth›› where
  "is_left_invertible a ⟹ left_inverse a = (SOME a_inv. a_inv ❙* a = ❙1)"

definition (in monoid) right_inverse ✐‹contributor ‹Balazs Toth›› where
  "is_right_invertible a ⟹ right_inverse a = (SOME a_inv. a ❙* a_inv = ❙1)"

lemma (in monoid) comp_left_inverse [simp]: ✐‹contributor ‹Balazs Toth››
  "is_left_invertible a ⟹ left_inverse a ❙* a = ❙1"
  by (auto simp: is_left_invertible_def left_inverse_def intro: someI_ex)

lemma (in monoid) comp_right_inverse [simp]: ✐‹contributor ‹Balazs Toth››
  "is_right_invertible a ⟹ a ❙* right_inverse a = ❙1"
  by (auto simp: is_right_invertible_def right_inverse_def intro: someI_ex)

lemma (in monoid) neutral_is_left_invertible [simp]: ✐‹contributor ‹Balazs Toth››
  "is_left_invertible ❙1"
  by (simp add: is_left_invertible_def)

lemma (in monoid) neutral_is_right_invertible [simp]: ✐‹contributor ‹Balazs Toth››
  "is_right_invertible ❙1"
  by (simp add: is_right_invertible_def)


section ‹Semigroup Action›

text ‹We define both left and right semigroup actions. Left semigroup actions seem to be prevalent
in algebra, but right semigroup actions directly uses the usual notation of term/atom/literal/clause
substitution.›

locale left_semigroup_action = semigroup +
  fixes action :: "'a ⇒ 'b ⇒ 'b" (infix ‹⋅› 70)
  assumes action_compatibility[simp]: "⋀a b x. (a ❙* b) ⋅ x = a ⋅ (b ⋅ x)"

locale right_semigroup_action = semigroup +
  fixes action :: "'b ⇒ 'a ⇒ 'b" (infix ‹⋅› 70)
  assumes action_compatibility[simp]: "⋀x a b. x ⋅ (a ❙* b) = (x ⋅ a) ⋅ b"

text ‹We then instantiate the right action in the context of the left action in order to get access
to any lemma proven in the context of the other locale. We do analogously in the context of the
right locale.›

sublocale left_semigroup_action ⊆ right: right_semigroup_action where
  f = "λx y. f y x" and action = "λx y. action y x"
proof unfold_locales
  show "⋀a b c. c ❙* (b ❙* a) = c ❙* b ❙* a"
    by (simp only: assoc)
next
  show "⋀x a b. (b ❙* a) ⋅ x = b ⋅ (a ⋅ x)"
    by simp
qed

sublocale right_semigroup_action ⊆ left: left_semigroup_action where
  f = "λx y. f y x" and action = "λx y. action y x"
proof unfold_locales
  show "⋀a b c. c ❙* (b ❙* a) = c ❙* b ❙* a"
    by (simp only: assoc)
next
  show "⋀a b x. x ⋅ (b ❙* a) = (x ⋅ b) ⋅ a"
    by simp
qed

lemma (in right_semigroup_action) lifting_semigroup_action_to_set:
  "right_semigroup_action (❙*) (λX a. (λx. action x a) ` X)"
proof unfold_locales
  show "⋀x a b. (λx. x ⋅ (a ❙* b)) ` x = (λx. x ⋅ b) ` (λx. x ⋅ a) ` x"
    by (simp add: image_comp)
qed

lemma (in right_semigroup_action) lifting_semigroup_action_to_list:
  "right_semigroup_action (❙*) (λxs a. map (λx. action x a) xs)"
proof unfold_locales
  show "⋀x a b. map (λx. x ⋅ (a ❙* b)) x = map (λx. x ⋅ b) (map (λx. x ⋅ a) x)"
    by (simp add: image_comp)
qed


section ‹Monoid Action›

locale left_monoid_action = monoid +
  fixes action :: "'a ⇒ 'b ⇒ 'b" (infix ‹⋅› 70)
  assumes
    monoid_action_compatibility: "⋀a b x. (a ❙* b) ⋅ x = a ⋅ (b ⋅ x)" and
    action_neutral[simp]: "⋀x. ❙1 ⋅ x = x"

locale right_monoid_action = monoid +
  fixes action :: "'b ⇒ 'a ⇒ 'b" (infix ‹⋅› 70)
  assumes
    monoid_action_compatibility: "⋀x a b. x ⋅ (a ❙* b) = (x ⋅ a) ⋅ b" and
    action_neutral[simp]: "⋀x. x ⋅ ❙1 = x"

sublocale left_monoid_action ⊆ left_semigroup_action
  by unfold_locales (fact monoid_action_compatibility)

sublocale right_monoid_action ⊆ right_semigroup_action
  by unfold_locales (fact monoid_action_compatibility)

sublocale left_monoid_action ⊆ right: right_monoid_action where
  f = "λx y. f y x" and action = "λx y. action y x"
  by unfold_locales simp_all

sublocale right_monoid_action ⊆ left: left_monoid_action where
  f = "λx y. f y x" and action = "λx y. action y x"
  by unfold_locales simp_all

lemma (in right_monoid_action) lifting_monoid_action_to_set:
  "right_monoid_action (❙*) ❙1 (λX a. (λx. action x a) ` X)"
proof (unfold_locales)
  show "⋀x a b. (λx. x ⋅ (a ❙* b)) ` x = (λx. x ⋅ b) ` (λx. x ⋅ a) ` x"
    by (simp add: image_comp)
next
  show "⋀x. (λx. x ⋅ ❙1) ` x = x"
    by simp
qed

lemma (in right_monoid_action) lifting_monoid_action_to_list:
  "right_monoid_action (❙*) ❙1 (λxs a. map (λx. action x a) xs)"
proof unfold_locales
  show "⋀x a b. map (λx. x ⋅ (a ❙* b)) x = map (λx. x ⋅ b) (map (λx. x ⋅ a) x)"
    by simp
next
  show "⋀x. map (λx. x ⋅ ❙1) x = x"
    by simp
qed


section ‹Group Action›

locale left_group_action = group +
  fixes action :: "'a ⇒ 'b ⇒ 'b" (infix ‹⋅› 70)
  assumes
    group_action_compatibility: "⋀a b x. (a ❙* b) ⋅ x = a ⋅ (b ⋅ x)" and
    group_action_neutral: "⋀x. ❙1 ⋅ x = x"

locale right_group_action = group +
  fixes action :: "'b ⇒ 'a ⇒ 'b" (infixl ‹⋅› 70)
  assumes
    group_action_compatibility: "⋀x a b. x ⋅ (a ❙* b) = (x ⋅ a) ⋅ b" and
    group_action_neutral: "⋀x. x ⋅ ❙1 = x"

sublocale left_group_action ⊆ left_monoid_action
  by unfold_locales (fact group_action_compatibility group_action_neutral)+

sublocale right_group_action ⊆ right_monoid_action
  by unfold_locales (fact group_action_compatibility group_action_neutral)+

sublocale left_group_action ⊆ right: right_group_action where
  f = "λx y. f y x" and action = "λx y. action y x"
  by unfold_locales simp_all

sublocale right_group_action ⊆ left: left_group_action where
  f = "λx y. f y x" and action = "λx y. action y x"
  by unfold_locales simp_all

end