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

lemma transpose_apply_second [simp]:
  transpose a b b = a
  by (simp add: transpose_def)

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
  by (simp add: fun_eq_iff transpose_def)

lemma transpose_eq_iff:
  transpose a b c = d  (c  a  c  b  d = c)  (c = a  d = b)  (c = b  d = a)
  by (auto simp add: transpose_def)

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
  by (auto simp add: transpose_eq_iff)

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

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"
  by (simp add: ac_simps)

lemma swap_nilpotent: "Fun.swap a b (Fun.swap a b f) = f"
  by (simp add: comp_assoc)

lemma swap_comp_involutory: "Fun.swap a b  Fun.swap a b = id"
  by (simp add: fun_eq_iff)

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]
  by (simp add: comp_assoc)

lemma comp_swap: "f  Fun.swap a b g = Fun.swap a b (f  g)"
  by (simp add: comp_assoc)

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"
  by (simp add: comp_inj_on)
  
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"
  by (simp add: bij_betw_swap_iff)

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 {}))
  by (auto simp add: Fun.swap_def)

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)"
  by (simp add: Fun.swap_def)

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