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 
by (simp add: inj_image_mem_iff prm_apply_injective)

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