Theory Permutation

```theory Permutation
imports Main
begin

type_synonym 'a swp = "'a × 'a"
type_synonym 'a preprm = "'a swp list"

definition preprm_id :: "'a preprm" where "preprm_id = []"

fun swp_apply :: "'a swp ⇒ 'a ⇒ 'a" where
"swp_apply (a, b) x = (if x = a then b else (if x = b then a else x))"

fun preprm_apply :: "'a preprm ⇒ 'a ⇒ 'a" where
"preprm_apply [] x = x"
| "preprm_apply (s # ss) x = swp_apply s (preprm_apply ss x)"

definition preprm_compose :: "'a preprm ⇒ 'a preprm ⇒ 'a preprm" where
"preprm_compose f g ≡ f @ g"

definition preprm_unit :: "'a ⇒ 'a ⇒ 'a preprm" where
"preprm_unit a b ≡ [(a, b)]"

definition preprm_ext :: "'a preprm ⇒ 'a preprm ⇒ bool" (infix "=p" 100) where
"π =p σ ≡ ∀x. preprm_apply π x = preprm_apply σ x"

definition preprm_inv :: "'a preprm ⇒ 'a preprm" where
"preprm_inv π ≡ rev π"

lemma swp_apply_unequal:
assumes "x ≠ y"
shows "swp_apply s x ≠ swp_apply s y"
proof(cases s)
case (Pair a b)
consider "x = a" | "x = b" | "x ≠ a ∧ x ≠ b" by auto
thus ?thesis proof(cases)
case 1
have "swp_apply s x = b" using ‹s = (a, b)› ‹x = a› by simp
moreover have "swp_apply s y ≠ b" using ‹s = (a, b)› ‹x = a› ‹x ≠ y›
by(cases "y = b", simp_all)
ultimately show ?thesis by metis
next
case 2
have "swp_apply s x = a" using ‹s = (a, b)› ‹x = b› by simp
moreover have "swp_apply s y ≠ a" using ‹s = (a, b)› ‹x = b› ‹x ≠ y›
by(cases "y = a", simp_all)
ultimately show ?thesis by metis
next
case 3
have "swp_apply s x = x" using ‹s = (a, b)› ‹x ≠ a ∧ x ≠ b› by simp
consider "y = a" | "y = b" | "y ≠ a ∧ y ≠ b" by auto
hence "swp_apply s y ≠ x" proof(cases)
case 1
hence "swp_apply s y = b" using ‹s = (a, b)› by simp
thus ?thesis using ‹x ≠ a ∧ x ≠ b› by metis
next
case 2
hence "swp_apply s y = a" using ‹s = (a, b)› by simp
thus ?thesis using ‹x ≠ a ∧ x ≠ b› by metis
next
case 3
hence "swp_apply s y = y" using ‹s = (a, b)› by simp
thus ?thesis using ‹x ≠ y› by metis
next
qed
thus ?thesis using ‹swp_apply s x = x› ‹x ≠ y› by metis
next
qed
next
qed

lemma preprm_ext_reflexive:
shows "x =p x"
unfolding preprm_ext_def by auto

corollary preprm_ext_reflp:
shows "reflp preprm_ext"
unfolding reflp_def using preprm_ext_reflexive by auto

lemma preprm_ext_symmetric:
assumes "x =p y"
shows "y =p x"
using assms unfolding preprm_ext_def by auto

corollary preprm_ext_symp:
shows "symp preprm_ext"
unfolding symp_def using preprm_ext_symmetric by auto

lemma preprm_ext_transitive:
assumes "x =p y" and "y =p z"
shows "x =p z"
using assms unfolding preprm_ext_def by auto

corollary preprm_ext_transp:
shows "transp preprm_ext"
unfolding transp_def using preprm_ext_transitive by auto

lemma preprm_apply_composition:
shows "preprm_apply (preprm_compose f g) x = preprm_apply f (preprm_apply g x)"
unfolding preprm_compose_def
by(induction f, simp_all)

lemma preprm_apply_unequal:
assumes "x ≠ y"
shows "preprm_apply π x ≠ preprm_apply π y"
using assms proof(induction π, simp)
case (Cons s ss)
have  "preprm_apply (s # ss) x = swp_apply s (preprm_apply ss x)"
and "preprm_apply (s # ss) y = swp_apply s (preprm_apply ss y)" by auto
thus ?case using Cons.IH ‹x ≠ y› swp_apply_unequal by metis
next
qed

lemma preprm_unit_equal_id:
shows "preprm_unit a a =p preprm_id"
unfolding preprm_ext_def preprm_unit_def preprm_id_def
by simp

lemma preprm_unit_inaction:
assumes "x ≠ a" and "x ≠ b"
shows "preprm_apply (preprm_unit a b) x = x"
unfolding preprm_unit_def using assms by simp

lemma preprm_unit_action:
shows "preprm_apply (preprm_unit a b) a = b"
unfolding preprm_unit_def by simp

lemma preprm_unit_commutes:
shows "preprm_unit a b =p preprm_unit b a"
unfolding preprm_ext_def preprm_unit_def
by simp

lemma preprm_singleton_involution:
shows "preprm_compose [s] [s] =p preprm_id"
unfolding preprm_ext_def preprm_compose_def preprm_unit_def preprm_id_def
proof -
obtain s1 s2 where "s1 = fst s" "s2 = snd s" by auto
hence "s = (s1, s2)" by simp
thus "∀x. preprm_apply ([s] @ [s]) x = preprm_apply [] x"
by simp
qed

lemma preprm_unit_involution:
shows "preprm_compose (preprm_unit a b) (preprm_unit a b) =p preprm_id"
unfolding preprm_unit_def
using preprm_singleton_involution.

lemma preprm_apply_id:
shows "preprm_apply preprm_id x = x"
unfolding preprm_id_def
by simp

lemma preprm_apply_injective:
shows "inj (preprm_apply π)"
unfolding inj_on_def proof(rule+)
fix x y
assume "preprm_apply π x = preprm_apply π y"
thus "x = y" proof(induction π)
case Nil
thus ?case by auto
next
case (Cons s ss)
hence "swp_apply s (preprm_apply ss x) = swp_apply s (preprm_apply ss y)" by auto
thus ?case using swp_apply_unequal Cons.IH by metis
next
qed
qed

lemma preprm_disagreement_composition:
assumes "a ≠ b" "b ≠ c" "a ≠ c"
shows "{x.
preprm_apply (preprm_compose (preprm_unit a b) (preprm_unit b c)) x ≠
preprm_apply (preprm_unit a c) x
} = {a, b}"
unfolding preprm_unit_def preprm_compose_def proof
show "{x. preprm_apply ([(a, b)] @ [(b, c)]) x ≠ preprm_apply [(a, c)] x} ⊆ {a, b}"
proof
fix x
have "x ∉ {a, b} ⟹ x ∉ {x. preprm_apply ([(a, b)] @ [(b, c)]) x ≠ preprm_apply [(a, c)] x}"
proof -
assume "x ∉ {a, b}"
hence "x ≠ a ∧ x ≠ b" by auto
hence "preprm_apply ([(a, b)] @ [(b, c)]) x = preprm_apply [(a, c)] x" by simp
thus "x ∉ {x. preprm_apply ([(a, b)] @ [(b, c)]) x ≠ preprm_apply [(a, c)] x}" by auto
qed
thus "x ∈ {x. preprm_apply ([(a, b)] @ [(b, c)]) x ≠ preprm_apply [(a, c)] x} ⟹ x ∈ {a, b}"
by blast
qed
show "{a, b} ⊆ {x. preprm_apply ([(a, b)] @ [(b, c)]) x ≠ preprm_apply [(a, c)] x}"
proof
fix x
assume "x ∈ {a, b}"
from this consider "x = a" | "x = b" by auto
thus "x ∈ {x. preprm_apply ([(a, b)] @ [(b, c)]) x ≠ preprm_apply [(a, c)] x}"
using assms by(cases, simp_all)
qed
qed

lemma preprm_compose_push:
shows "
preprm_compose π (preprm_unit a b) =p
preprm_compose (preprm_unit (preprm_apply π a) (preprm_apply π b)) π
"
unfolding preprm_ext_def preprm_unit_def
by (simp add: inj_eq preprm_apply_composition preprm_apply_injective)

lemma preprm_ext_compose_left:
assumes "P =p S"
shows "preprm_compose π P =p preprm_compose π S"
using assms unfolding preprm_ext_def
using preprm_apply_composition by metis

lemma preprm_ext_compose_right:
assumes "P =p S"
shows "preprm_compose P π =p preprm_compose S π"
using assms unfolding preprm_ext_def
using preprm_apply_composition by metis

lemma preprm_ext_uncompose:
assumes "π =p σ" "preprm_compose π P =p preprm_compose σ S"
shows "P =p S"
using assms unfolding preprm_ext_def
proof -
assume *: "∀x. preprm_apply π x = preprm_apply σ x"

assume "∀x. preprm_apply (preprm_compose π P) x = preprm_apply (preprm_compose σ S) x"
hence "∀x. preprm_apply π (preprm_apply P x) = preprm_apply σ (preprm_apply S x)"
using preprm_apply_composition by metis
hence "∀x. preprm_apply π (preprm_apply P x) = preprm_apply π (preprm_apply S x)"
using * by metis
thus "∀x. preprm_apply P x = preprm_apply S x"
using preprm_apply_injective unfolding inj_on_def by fastforce
qed

lemma preprm_inv_compose:
shows "preprm_compose (preprm_inv π) π =p preprm_id"
unfolding preprm_inv_def
proof(induction π, simp add: preprm_ext_def preprm_id_def preprm_compose_def)
case (Cons p ps)
hence IH: "(preprm_compose (rev ps) ps) =p preprm_id" by auto

have "(preprm_compose (rev (p # ps)) (p # ps)) =p (preprm_compose (rev ps) (preprm_compose (preprm_compose [p] [p]) ps))"
unfolding preprm_compose_def using preprm_ext_reflexive by simp
moreover have "... =p (preprm_compose (rev ps) (preprm_compose preprm_id ps))"
using preprm_singleton_involution preprm_ext_compose_left preprm_ext_compose_right by metis
moreover have "... =p (preprm_compose (rev ps) ps)"
unfolding preprm_compose_def preprm_id_def using preprm_ext_reflexive by simp
moreover have "... =p preprm_id" using IH.
ultimately show ?case using preprm_ext_transitive by metis
next
qed

lemma preprm_inv_involution:
shows "preprm_inv (preprm_inv π) = π"
unfolding preprm_inv_def by simp

lemma preprm_inv_ext:
assumes "π =p σ"
shows "preprm_inv π =p preprm_inv σ"
proof -
have
"(preprm_compose (preprm_inv (preprm_inv π)) (preprm_inv π)) =p preprm_id"
"(preprm_compose (preprm_inv (preprm_inv σ)) (preprm_inv σ)) =p preprm_id"
using preprm_inv_compose by metis+
hence
"(preprm_compose π (preprm_inv π)) =p preprm_id"
"(preprm_compose σ (preprm_inv σ)) =p preprm_id"
using preprm_inv_involution by metis+
hence "(preprm_compose π (preprm_inv π)) =p (preprm_compose σ (preprm_inv σ))"
using preprm_ext_transitive preprm_ext_symmetric by metis
thus "preprm_inv π =p preprm_inv σ"
using preprm_ext_uncompose assms by metis
qed

quotient_type 'a prm = "'a preprm" / preprm_ext
proof(rule equivpI)
show "reflp preprm_ext" using preprm_ext_reflp.
show "symp preprm_ext" using preprm_ext_symp.
show "transp preprm_ext" using preprm_ext_transp.
qed

lift_definition prm_id :: "'a prm" ("ε") is preprm_id.

lift_definition prm_apply :: "'a prm ⇒ 'a ⇒ 'a" (infix "\$" 140) is preprm_apply
unfolding preprm_ext_def
using preprm_apply.simps by auto

lift_definition prm_compose :: "'a prm ⇒ 'a prm ⇒ 'a prm" (infixr "⋄" 145) is preprm_compose
unfolding preprm_ext_def
by(simp only: preprm_apply_composition, simp)

lift_definition prm_unit :: "'a ⇒ 'a ⇒ 'a prm" ("[_ ↔ _]") is preprm_unit.

lift_definition prm_inv :: "'a prm ⇒ 'a prm" is preprm_inv
using preprm_inv_ext.

lemma prm_apply_composition:
fixes f g :: "'a prm" and x :: 'a
shows "f ⋄ g \$ x = f \$ (g \$ x)"
by(transfer, metis preprm_apply_composition)

lemma prm_apply_unequal:
fixes π :: "'a prm" and x y :: 'a
assumes "x ≠ y"
shows "π \$ x ≠ π \$ y"
using assms by (transfer, metis preprm_apply_unequal)

lemma prm_unit_equal_id:
fixes a :: 'a
shows "[a ↔ a] = ε"
by (transfer, metis preprm_unit_equal_id)

lemma prm_unit_inaction:
fixes a b x :: 'a
assumes "x ≠ a" and "x ≠ b"
shows "[a ↔ b] \$ x = x"
using assms
by (transfer, metis preprm_unit_inaction)

lemma prm_unit_action:
fixes a b :: 'a
shows "[a ↔ b] \$ a = b"
by (transfer, metis preprm_unit_action)

lemma prm_unit_commutes:
fixes a b :: 'a
shows "[a ↔ b] = [b ↔ a]"
by (transfer, metis preprm_unit_commutes)

lemma prm_unit_involution:
fixes a b :: 'a
shows "[a ↔ b] ⋄ [a ↔ b] = ε"
by (transfer, metis preprm_unit_involution)

lemma prm_apply_id:
fixes x :: 'a
shows "ε \$ x = x"
by(transfer, metis preprm_apply_id)

lemma prm_apply_injective:
shows "inj (prm_apply π)"
by(transfer, metis preprm_apply_injective)

lemma prm_inv_compose:
shows "(prm_inv π) ⋄ π = ε"
by(transfer, metis preprm_inv_compose)

interpretation "'a prm": semigroup prm_compose
unfolding semigroup_def by(transfer, simp add: preprm_compose_def preprm_ext_def)

interpretation "'a prm": group prm_compose prm_id prm_inv
unfolding group_def group_axioms_def
proof -
have "semigroup (⋄)" using "'a prm.semigroup_axioms".
moreover have "∀a. ε ⋄ a = a" by(transfer, simp add: preprm_id_def preprm_compose_def preprm_ext_def)
moreover have "∀a. prm_inv a ⋄ a = ε" using prm_inv_compose by blast
ultimately show "semigroup (⋄) ∧ (∀a. ε ⋄ a = a) ∧ (∀a. prm_inv a ⋄ a = ε)" by blast
qed

definition prm_set :: "'a prm ⇒ 'a set ⇒ 'a set" (infix "{\$}" 140) where
"prm_set π S ≡ image (prm_apply π) S"

lemma prm_set_apply_compose:
shows "π {\$} (σ {\$} S) = (π ⋄ σ) {\$} S"
unfolding prm_set_def proof -
have "(\$) π ` (\$) σ ` S = (λx. π \$ x) ` (λx. σ \$ x) ` S" by simp
moreover have "... = (λx. π \$ (σ \$ x)) ` S" by auto
moreover have "... = (λx. (π ⋄ σ) \$ x) ` S" using prm_apply_composition by metis
moreover have "... = (π ⋄ σ) {\$} S" using prm_set_def by metis
ultimately show "(\$) π ` (\$) σ ` S = (\$) (π ⋄ σ) ` S" by metis
qed

lemma prm_set_membership:
assumes "x ∈ S"
shows "π \$ x ∈ π {\$} S"
using assms unfolding prm_set_def by simp

lemma prm_set_notmembership:
assumes "x ∉ S"
shows "π \$ x ∉ π {\$} S"
using assms unfolding prm_set_def

lemma prm_set_singleton:
shows "π {\$} {x} = {π \$ x}"
unfolding prm_set_def by auto

lemma prm_set_id:
shows "ε {\$} S = S"
unfolding prm_set_def
proof -
have "(\$) ε ` S = (λx. ε \$ x) ` S" by simp
moreover have "... = (λx. x) ` S" using prm_apply_id by metis
moreover have "... = S" by auto
ultimately show "(\$) ε ` S = S" by metis
qed

lemma prm_set_unit_inaction:
assumes "a ∉ S" and "b ∉ S"
shows "[a ↔ b] {\$} S = S"
proof
show "[a ↔ b] {\$} S ⊆ S" proof
fix x
assume H: "x ∈ [a ↔ b] {\$} S"
from this obtain y where "x = [a ↔ b] \$ y" unfolding prm_set_def using imageE by metis
hence "y ∈ S" using H inj_image_mem_iff prm_apply_injective prm_set_def by metis
hence "y ≠ a" and "y ≠ b" using assms by auto
hence "x = y" using prm_unit_inaction ‹x = [a ↔ b] \$ y› by metis
thus "x ∈ S" using ‹y ∈ S› by auto
qed
show "S ⊆ [a ↔ b] {\$} S" proof
fix x
assume H: "x ∈ S"
hence "x ≠ a" and "x ≠ b" using assms by auto
hence "x = [a ↔ b] \$ x" using prm_unit_inaction by metis
thus "x ∈ [a ↔ b] {\$} S" unfolding prm_set_def using H by simp
qed
qed

lemma prm_set_unit_action:
assumes "a ∈ S" and "b ∉ S"
shows "[a ↔ b] {\$} S = S - {a} ∪ {b}"
proof
show "[a ↔ b] {\$} S ⊆ S - {a} ∪ {b}" proof
fix x
assume H: "x ∈ [a ↔ b] {\$} S"
from this obtain y where "x = [a ↔ b] \$ y" unfolding prm_set_def using imageE by metis
hence "y ∈ S" using H inj_image_mem_iff prm_apply_injective prm_set_def by metis
hence "y ≠ b" using assms by auto
consider "y = a" | "y ≠ a" by auto
thus "x ∈ S - {a} ∪ {b}" proof(cases)
case 1
hence "x = b" using ‹x = [a ↔ b] \$ y› using prm_unit_action by metis
thus ?thesis by auto
next
case 2
hence "x = y" using ‹x = [a ↔ b] \$ y› using prm_unit_inaction ‹y ≠ b› by metis
hence "x ∈ S" and "x ≠ a" using ‹y ∈ S› ‹y ≠ a› by auto
thus ?thesis by auto
next
qed
qed
show "S - {a} ∪ {b} ⊆ [a ↔ b] {\$} S" proof
fix x
assume H: "x ∈ S - {a} ∪ {b}"
hence "x ≠ a" using assms by auto
consider "x = b" | "x ≠ b" by auto
thus "x ∈ [a ↔ b] {\$} S" proof(cases)
case 1
hence "x = [a ↔ b] \$ a" using prm_unit_action by metis
thus ?thesis using ‹a ∈ S› prm_set_membership by metis
next
case 2
hence "x ∈ S" using H by auto
moreover have "x = [a ↔ b] \$ x" using prm_unit_inaction ‹x ≠ a› ‹x ≠ b› by metis
ultimately show ?thesis using prm_set_membership by metis
next
qed
qed
qed

lemma prm_set_distributes_union:
shows "π {\$} (S ∪ T) = (π {\$} S) ∪ (π {\$} T)"
unfolding prm_set_def by auto

lemma prm_set_distributes_difference:
shows "π {\$} (S - T) = (π {\$} S) - (π {\$} T)"
unfolding prm_set_def using prm_apply_injective image_set_diff by metis

definition prm_disagreement :: "'a prm ⇒ 'a prm ⇒ 'a set" ("ds") where
"prm_disagreement π σ ≡ {x. π \$ x ≠ σ \$ x}"

lemma prm_disagreement_ext:
shows "x ∈ ds π σ ≡ π \$ x ≠ σ \$ x"
unfolding prm_disagreement_def by simp

lemma prm_disagreement_composition:
assumes "a ≠ b" "b ≠ c" "a ≠ c"
shows "ds ([a ↔ b] ⋄ [b ↔ c]) [a ↔ c] = {a, b}"
using assms unfolding prm_disagreement_def by(transfer, metis preprm_disagreement_composition)

lemma prm_compose_push:
shows "π ⋄ [a ↔ b] = [π \$ a ↔ π \$ b] ⋄ π"
by(transfer, metis preprm_compose_push)

end
```