Theory HOL-Combinatorics.Transposition

```section ‹Transposition function›

theory Transposition
imports Main
begin

definition transpose :: ‹'a ⇒ 'a ⇒ 'a ⇒ 'a›
where ‹transpose a b c = (if c = a then b else if c = b then a else c)›

lemma transpose_apply_first [simp]:
‹transpose a b a = b›

lemma transpose_apply_second [simp]:
‹transpose a b b = a›

lemma transpose_apply_other [simp]:
‹transpose a b c = c› if ‹c ≠ a› ‹c ≠ b›
using that by (simp add: transpose_def)

lemma transpose_same [simp]:
‹transpose a a = id›

lemma transpose_eq_iff:
‹transpose a b c = d ⟷ (c ≠ a ∧ c ≠ b ∧ d = c) ∨ (c = a ∧ d = b) ∨ (c = b ∧ d = a)›

lemma transpose_eq_imp_eq:
‹c = d› if ‹transpose a b c = transpose a b d›
using that by (auto simp add: transpose_eq_iff)

lemma transpose_commute [ac_simps]:
‹transpose b a = transpose a b›
by (auto simp add: fun_eq_iff transpose_eq_iff)

lemma transpose_involutory [simp]:
‹transpose a b (transpose a b c) = c›

lemma transpose_comp_involutory [simp]:
‹transpose a b ∘ transpose a b = id›
by (rule ext) simp

lemma transpose_triple:
‹transpose a b (transpose b c (transpose a b d)) = transpose a c d›
if ‹a ≠ c› and ‹b ≠ c›
using that by (simp add: transpose_def)

lemma transpose_comp_triple:
‹transpose a b ∘ transpose b c ∘ transpose a b = transpose a c›
if ‹a ≠ c› and ‹b ≠ c›
using that by (simp add: fun_eq_iff transpose_triple)

lemma transpose_image_eq [simp]:
‹transpose a b ` A = A› if ‹a ∈ A ⟷ b ∈ A›
using that by (auto simp add: transpose_def [abs_def])

lemma inj_on_transpose [simp]:
‹inj_on (transpose a b) A›
by rule (drule transpose_eq_imp_eq)

lemma inj_transpose:
‹inj (transpose a b)›
by (fact inj_on_transpose)

lemma surj_transpose:
‹surj (transpose a b)›
by simp

lemma bij_betw_transpose_iff [simp]:
‹bij_betw (transpose a b) A A› if ‹a ∈ A ⟷ b ∈ A›
using that by (auto simp: bij_betw_def)

lemma bij_transpose [simp]:
‹bij (transpose a b)›
by (rule bij_betw_transpose_iff) simp

lemma bijection_transpose:
‹bijection (transpose a b)›
by standard (fact bij_transpose)

lemma inv_transpose_eq [simp]:
‹inv (transpose a b) = transpose a b›
by (rule inv_unique_comp) simp_all

lemma transpose_apply_commute:
‹transpose a b (f c) = f (transpose (inv f a) (inv f b) c)›
if ‹bij f›
proof -
from that have ‹surj f›
by (rule bij_is_surj)
with that show ?thesis
by (simp add: transpose_def bij_inv_eq_iff surj_f_inv_f)
qed

lemma transpose_comp_eq:
‹transpose a b ∘ f = f ∘ transpose (inv f a) (inv f b)›
if ‹bij f›
using that by (simp add: fun_eq_iff transpose_apply_commute)

lemma in_transpose_image_iff:
‹x ∈ transpose a b ` S ⟷ transpose a b x ∈ S›
by (auto intro!: image_eqI)

text ‹Legacy input alias›

setup ‹Context.theory_map (Name_Space.map_naming (Name_Space.qualified_path true \<^binding>‹Fun›))›

abbreviation (input) swap :: ‹'a ⇒ 'a ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'b›
where ‹swap a b f ≡ f ∘ transpose a b›

lemma swap_def:
‹Fun.swap a b f = f (a := f b, b:= f a)›

setup ‹Context.theory_map (Name_Space.map_naming (Name_Space.parent_path))›

lemma swap_apply:
"Fun.swap a b f a = f b"
"Fun.swap a b f b = f a"
"c ≠ a ⟹ c ≠ b ⟹ Fun.swap a b f c = f c"
by simp_all

lemma swap_self: "Fun.swap a a f = f"
by simp

lemma swap_commute: "Fun.swap a b f = Fun.swap b a f"

lemma swap_nilpotent: "Fun.swap a b (Fun.swap a b f) = f"

lemma swap_comp_involutory: "Fun.swap a b ∘ Fun.swap a b = id"

lemma swap_triple:
assumes "a ≠ c" and "b ≠ c"
shows "Fun.swap a b (Fun.swap b c (Fun.swap a b f)) = Fun.swap a c f"
using assms transpose_comp_triple [of a c b]

lemma comp_swap: "f ∘ Fun.swap a b g = Fun.swap a b (f ∘ g)"

lemma swap_image_eq:
assumes "a ∈ A" "b ∈ A"
shows "Fun.swap a b f ` A = f ` A"
using assms by (metis image_comp transpose_image_eq)

lemma inj_on_imp_inj_on_swap: "inj_on f A ⟹ a ∈ A ⟹ b ∈ A ⟹ inj_on (Fun.swap a b f) A"

lemma inj_on_swap_iff:
assumes A: "a ∈ A" "b ∈ A"
shows "inj_on (Fun.swap a b f) A ⟷ inj_on f A"
using assms by (metis inj_on_imageI inj_on_imp_inj_on_swap transpose_image_eq)

lemma surj_imp_surj_swap: "surj f ⟹ surj (Fun.swap a b f)"
by (meson comp_surj surj_transpose)

lemma surj_swap_iff: "surj (Fun.swap a b f) ⟷ surj f"
by (metis fun.set_map surj_transpose)

lemma bij_betw_swap_iff: "x ∈ A ⟹ y ∈ A ⟹ bij_betw (Fun.swap x y f) A B ⟷ bij_betw f A B"
by (meson bij_betw_comp_iff bij_betw_transpose_iff)

lemma bij_swap_iff: "bij (Fun.swap a b f) ⟷ bij f"

lemma swap_image:
‹Fun.swap i j f ` A = f ` (A - {i, j}
∪ (if i ∈ A then {j} else {}) ∪ (if j ∈ A then {i} else {}))›

lemma inv_swap_id: "inv (Fun.swap a b id) = Fun.swap a b id"
by simp

lemma bij_swap_comp:
assumes "bij p"
shows "Fun.swap a b id ∘ p = Fun.swap (inv p a) (inv p b) p"
using assms by (simp add: transpose_comp_eq)

lemma swap_id_eq: "Fun.swap a b id x = (if x = a then b else if x = b then a else x)"

lemma swap_unfold:
‹Fun.swap a b p = p ∘ Fun.swap a b id›
by simp

lemma swap_id_idempotent: "Fun.swap a b id ∘ Fun.swap a b id = id"
by simp

lemma bij_swap_compose_bij:
‹bij (Fun.swap a b id ∘ p)› if ‹bij p›
using that by (rule bij_comp) simp

end
```