Theory Equiv_Relations_on_Functions

(*  Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com> *)

section ‹Definition of Equivalence Classes›

theory Equiv_Relations_on_Functions
imports
  Preliminaries
  Twelvefold_Way_Core
begin

subsection ‹Permutation on the Domain›

definition domain_permutation
where
  "domain_permutation A B = {(f, f') ∈ (A →⇩E B) × (A →⇩E B). ∃p. p permutes A ∧ (∀x ∈ A. f x = f' (p x))}"

lemma equiv_domain_permutation:
  "equiv (A →⇩E B) (domain_permutation A B)"
proof (rule equivI)
  show "domain_permutation A B ⊆ (A →⇩E B) × (A →⇩E B)"
    unfolding domain_permutation_def by auto
next
  show "refl_on (A →⇩E B) (domain_permutation A B)"
  proof (rule refl_onI)
    fix f
    assume "f ∈ A →⇩E B"
    from this show "(f, f) ∈ domain_permutation A B"
      using permutes_id unfolding domain_permutation_def by fastforce
  qed
next
  show "sym (domain_permutation A B)"
  proof (rule symI)
    fix f f'
    assume "(f, f') ∈ domain_permutation A B"
    from this obtain p where "p permutes A" and "∀x∈A. f x = f' (p x)"
      unfolding domain_permutation_def by auto
    from ‹(f, f') ∈ domain_permutation A B› have "f ∈ A →⇩E B" "f' ∈ A →⇩E B"
      unfolding domain_permutation_def by auto
    moreover from ‹p permutes A› have "inv p permutes A"
      by (simp add: permutes_inv)
    moreover from ‹p permutes A› ‹∀x∈A. f x = f' (p x)› have "∀x∈A. f' x = f (inv p x)"
      using permutes_in_image permutes_inverses(1) by (metis (mono_tags, opaque_lifting))
    ultimately show "(f', f) ∈ domain_permutation A B"
      unfolding domain_permutation_def by auto
  qed
next
  show "trans (domain_permutation A B)"
  proof (rule transI)
    fix f f' f''
    assume "(f, f') ∈ domain_permutation A B" "(f', f'') ∈ domain_permutation A B"
    from ‹(f, f') ∈ _› obtain p where "p permutes A" and "∀x∈A. f x = f' (p x)"
      unfolding domain_permutation_def by auto
    from ‹(f', f'') ∈ _› obtain p' where "p' permutes A" and "∀x∈A. f' x = f'' (p' x)"
      unfolding domain_permutation_def by auto
    from ‹(f, f') ∈ domain_permutation A B› have "f ∈ A →⇩E B"
      unfolding domain_permutation_def by auto
    moreover from ‹(f', f'') ∈ domain_permutation A B› have "f'' ∈ A →⇩E B"
      unfolding domain_permutation_def by auto
    moreover from ‹p permutes A› ‹p' permutes A› have "(p' ∘ p) permutes A"
      by (simp add: permutes_compose)
    moreover have "∀x∈A. f x = f'' ((p' ∘ p) x)"
      using ‹∀x∈A. f x = f' (p x)› ‹∀x∈A. f' x = f'' (p' x)› ‹p permutes A›
      by (simp add: permutes_in_image)
    ultimately show "(f, f'') ∈ domain_permutation A B"
      unfolding domain_permutation_def by auto
  qed
qed

subsubsection ‹Respecting Functions›

lemma inj_on_respects_domain_permutation:
  "(λf. inj_on f A) respects domain_permutation A B"
proof (rule congruentI)
  fix f f'
  assume "(f, f') ∈ domain_permutation A B"
  from this obtain p where p: "p permutes A" "∀x∈A. f x = f' (p x)"
    unfolding domain_permutation_def by auto
  have inv_p: "∀x∈A. f' x = f (inv p x)"
    using p by (metis permutes_inverses(1) permutes_not_in)
  show "inj_on f A ⟷ inj_on f' A"
  proof
    assume "inj_on f A"
    show "inj_on f' A"
    proof (rule inj_onI)
      fix a a'
      assume "a ∈ A" "a' ∈ A" "f' a = f' a'"
      from this ‹p permutes A› have "inv p a ∈ A" "inv p a' ∈ A"
        by (simp add:  permutes_in_image permutes_inv)+
      have "f (inv p a) = f (inv p a')"
        using ‹f' a = f' a'› ‹a ∈ A› ‹a' ∈ A› inv_p by auto
      from ‹inj_on f A› this ‹inv p a ∈ A› ‹inv p a' ∈ A› have "inv p a = inv p a'"
        using inj_on_contraD by fastforce
      from this show "a = a'"
        by (metis ‹p permutes A› permutes_inverses(1))
    qed
  next
    assume "inj_on f' A"
    from this p show "inj_on f A"
      unfolding inj_on_def
      by (metis inj_on_contraD permutes_in_image permutes_inj_on)
  qed
qed

lemma image_respects_domain_permutation:
  "(λf. f ` A) respects (domain_permutation A B)"
proof (rule congruentI)
  fix f f'
  assume "(f, f') ∈ domain_permutation A B"
  from this obtain p where p: "p permutes A" and f_eq: "∀x∈A. f x = f' (p x)"
    unfolding domain_permutation_def by auto
  show "f ` A = f' ` A"
  proof
    from p f_eq show "f ` A ⊆ f' ` A"
      by (auto simp add: permutes_in_image)
  next
    from ‹p permutes A› ‹∀x∈A. f x = f' (p x)› have "∀x∈A. f' x = f (inv p x)"
      using permutes_in_image permutes_inverses(1) by (metis (mono_tags, opaque_lifting))
    from this show "f' ` A ⊆ f ` A"
      using ‹p permutes A› by (auto simp add: permutes_inv permutes_in_image)
  qed
qed

lemma surjective_respects_domain_permutation:
  "(λf. f ` A = B) respects domain_permutation A B"
by (metis image_respects_domain_permutation congruentD congruentI)

lemma bij_betw_respects_domain_permutation:
  "(λf. bij_betw f A B) respects domain_permutation A B"
proof (rule congruentI)
  fix f f'
  assume "(f, f') ∈ domain_permutation A B"
  from this obtain p where "p permutes A" and "∀x∈A. f x = f' (p x)"
    unfolding domain_permutation_def by auto
  have "bij_betw f A B ⟷ bij_betw (f' o p) A B"
    using ‹∀x∈A. f x = f' (p x)›
    by (metis (mono_tags, opaque_lifting) comp_apply[of f' p] bij_betw_cong[of A f "f' ∘ p" B])
  also have "... ⟷ bij_betw f' A B"
    using ‹p permutes A›
    by (auto intro!: bij_betw_comp_iff[symmetric] permutes_imp_bij)
  finally show "bij_betw f A B ⟷ bij_betw f' A B" .
qed

lemma image_mset_respects_domain_permutation:
  shows "(λf. image_mset f (mset_set A)) respects (domain_permutation A B)"
proof (rule congruentI)
  fix f f'
  assume "(f, f') ∈ domain_permutation A B"
  from this obtain p where "p permutes A" and "∀x∈A. f x = f' (p x)"
    unfolding domain_permutation_def by auto
  from this show "image_mset f (mset_set A) = image_mset f' (mset_set A)"
    using permutes_implies_image_mset_eq by fastforce
qed

subsection ‹Permutation on the Range›

definition range_permutation
where
  "range_permutation A B = {(f, f') ∈ (A →⇩E B) × (A →⇩E B). ∃p. p permutes B ∧ (∀x ∈ A. f x = p (f' x))}"

lemma equiv_range_permutation:
  "equiv (A →⇩E B) (range_permutation A B)"
proof (rule equivI)
  show "range_permutation A B ⊆ (A →⇩E B) × (A →⇩E B)"
    unfolding range_permutation_def by auto
next
  show "refl_on (A →⇩E B) (range_permutation A B)"
  proof (rule refl_onI)
    fix f
    assume "f ∈ A →⇩E B"
    from this show "(f, f) ∈ range_permutation A B"
      using permutes_id unfolding range_permutation_def by fastforce
  qed
next
  show "sym (range_permutation A B)"
  proof (rule symI)
    fix f f'
    assume "(f, f') ∈ range_permutation A B"
    from this obtain p where "p permutes B" and "∀x∈A. f x = p (f' x)"
      unfolding range_permutation_def by auto
    from ‹(f, f') ∈ range_permutation A B› have "f ∈ A →⇩E B" "f' ∈ A →⇩E B"
      unfolding range_permutation_def by auto
    moreover from ‹p permutes B› have "inv p permutes B"
      by (simp add: permutes_inv)
    moreover from ‹p permutes B› ‹∀x∈A. f x = p (f' x)› have "∀x∈A. f' x = inv p (f x)"
      by (simp add: permutes_inverses(2))
    ultimately show "(f', f) ∈ range_permutation A B"
      unfolding range_permutation_def by auto
  qed
next
  show "trans (range_permutation A B)"
  proof (rule transI)
    fix f f' f''
    assume "(f, f') ∈ range_permutation A B" "(f', f'') ∈ range_permutation A B"
    from ‹(f, f') ∈ _› obtain p where "p permutes B" and "∀x∈A. f x = p (f' x)"
      unfolding range_permutation_def by auto
    from ‹(f', f'') ∈ _› obtain p' where "p' permutes B" and "∀x∈A. f' x = p' (f'' x)"
      unfolding range_permutation_def by auto
    from ‹(f, f') ∈ range_permutation A B› have "f ∈ A →⇩E B"
      unfolding range_permutation_def by auto
    moreover from ‹(f', f'') ∈ range_permutation A B› have "f'' ∈ A →⇩E B"
      unfolding range_permutation_def by auto
    moreover from ‹p permutes B› ‹p' permutes B› have "(p ∘ p') permutes B"
      by (simp add: permutes_compose)
    moreover have "∀x∈A. f x = (p ∘ p') (f'' x)"
      using ‹∀x∈A. f x = p (f' x)› ‹∀x∈A. f' x = p' (f'' x)› by auto
    ultimately show "(f, f'') ∈ range_permutation A B"
      unfolding range_permutation_def by auto
  qed
qed

subsubsection ‹Respecting Functions›

lemma inj_on_respects_range_permutation:
  "(λf. inj_on f A) respects range_permutation A B"
proof (rule congruentI)
  fix f f'
  assume "(f, f') ∈ range_permutation A B"
  from this obtain p where p: "p permutes B" "∀x∈A. f x = p (f' x)"
    unfolding range_permutation_def by auto
  have inv_p: "∀x∈A. f' x = inv p (f x)"
    using p by (simp add: permutes_inverses(2))
  show "inj_on f A ⟷ inj_on f' A"
  proof
    assume "inj_on f A"
    from this p show "inj_on f' A"
      unfolding inj_on_def by auto
  next
    assume "inj_on f' A"
    from this inv_p show "inj_on f A"
      unfolding inj_on_def by auto
  qed
qed

lemma surj_on_respects_range_permutation:
  "(λf. f ` A = B) respects range_permutation A B"
proof (rule congruentI)
  fix f f'
  assume a: "(f, f') ∈ range_permutation A B"
  from this have "f ∈ A →⇩E B" "f' ∈ A →⇩E B"
    unfolding range_permutation_def by auto
  from a obtain p where p: "p permutes B" "∀x∈A. f x = p (f' x)"
    unfolding range_permutation_def by auto
  have 1: "f ` A = (λx. p (f' x)) ` A"
    using p by (meson image_cong)
  have 2: "inv p ` ((λx. p (f' x)) ` A) = f' ` A"
    using p by (simp add: image_image image_inv_f_f permutes_inj)
  show "(f ` A = B) = (f' ` A = B)"
  proof
    assume "f ` A = B"
    from this 1 2 show "f' ` A = B"
      using p by (simp add: permutes_image permutes_inv)
  next
    assume "f' ` A = B"
    from this 1 2 show "f ` A = B"
      using p by (metis image_image permutes_image)
  qed
qed

lemma bij_betw_respects_range_permutation:
  "(λf. bij_betw f A B) respects range_permutation A B"
proof (rule congruentI)
  fix f f'
  assume "(f, f') ∈ range_permutation A B"
  from this obtain p where "p permutes B" and "∀x∈A. f x = p (f' x)"
    and "f' ∈ A →⇩E B"
    unfolding range_permutation_def by auto
  have "bij_betw f A B ⟷ bij_betw (p o f') A B"
    using ‹∀x∈A. f x = p (f' x)›
    by (metis (mono_tags, opaque_lifting) bij_betw_cong comp_apply)
  also have "... ⟷ bij_betw f' A B"
    using ‹f' ∈ A →⇩E B› ‹p permutes B›
    by (auto intro!: bij_betw_comp_iff2[symmetric] permutes_imp_bij)
  finally show "bij_betw f A B ⟷ bij_betw f' A B" .
qed

lemma domain_partitions_respects_range_permutation:
  "(λf. (λb. {x ∈ A. f x = b}) ` B - {{}}) respects range_permutation A B"
proof (rule congruentI)
  fix f f'
  assume "(f, f') ∈ range_permutation A B"
  from this obtain p where p: "p permutes B" "∀x ∈ A. f x = p (f' x)"
    unfolding range_permutation_def by blast
  have "{} ∈ (λb. {x ∈ A. f' x = b}) ` B ⟷ ¬ (∀b ∈ B. ∃x ∈ A. f' x = b)" by auto
  also have "(∀b ∈ B. ∃x ∈ A. f' x = b) ⟷ (∀b ∈ B. ∃x ∈ A. p (f' x) = b)"
  proof
    assume "∀b∈B. ∃x∈A. f' x = b"
    from this show "∀b∈B. ∃x∈A. p (f' x) = b"
      using ‹p permutes B› unfolding permutes_def by metis
  next
    assume "∀b∈B. ∃x∈A. p (f' x) = b"
    from this show "∀b∈B. ∃x∈A. f' x = b"
      using ‹p permutes B› by (metis bij_betwE permutes_imp_bij permutes_inverses(2))
  qed
  also have "¬ (∀b∈B. ∃x∈A. p (f' x) = b) ⟷ {} ∈ (λb. {x ∈ A. p (f' x) = b}) ` B" by auto
  finally have "{} ∈ (λb. {x ∈ A. f' x = b}) ` B ⟷ {} ∈ (λb. {x ∈ A. p (f' x) = b}) ` B" .
  moreover have "(λb. {x ∈ A. f' x = b}) ` B = (λb. {x ∈ A. p (f' x) = b}) ` B"
    using ‹p permutes B› permutes_implies_inv_image_on_eq by blast
  ultimately have "(λb. {x ∈ A. f' x = b}) ` B - {{}} = (λb. {x ∈ A. p (f' x) = b}) ` B - {{}}" by auto
  also have "… = (λb. {x ∈ A. f x = b}) ` B - {{}}"
    using ‹∀x ∈ A. f x = p (f' x)› Collect_cong image_cong by auto
  finally show "(λb. {x ∈ A. f x = b}) ` B - {{}} = (λb. {x ∈ A. f' x = b}) ` B - {{}}" ..
qed

subsection ‹Permutation on the Domain and the Range›

definition domain_and_range_permutation
where
  "domain_and_range_permutation A B = {(f, f') ∈ (A →⇩E B) × (A →⇩E B).
    ∃p⇩A p⇩B. p⇩A permutes A ∧ p⇩B permutes B ∧ (∀x ∈ A. f x = p⇩B (f' (p⇩A x)))}"

lemma equiv_domain_and_range_permutation:
  "equiv (A →⇩E B) (domain_and_range_permutation A B)"
proof (rule equivI)
  show "domain_and_range_permutation A B ⊆ (A →⇩E B) × (A →⇩E B)"
    unfolding domain_and_range_permutation_def by auto
next
  show "refl_on (A →⇩E B) (domain_and_range_permutation A B)"
  proof (rule refl_onI)
    fix f
    assume "f ∈ A →⇩E B"
    from this show "(f, f) ∈ domain_and_range_permutation A B"
      using permutes_id[of A] permutes_id[of B]
      unfolding domain_and_range_permutation_def by fastforce
  qed
next
  show "sym (domain_and_range_permutation A B)"
  proof (rule symI)
    fix f f'
    assume "(f, f') ∈ domain_and_range_permutation A B"
    from this obtain p⇩A p⇩B where "p⇩A permutes A" "p⇩B permutes B" and "∀x∈A. f x = p⇩B (f' (p⇩A x))"
      unfolding domain_and_range_permutation_def by auto
    from ‹(f, f') ∈ domain_and_range_permutation A B› have f: "f ∈ A →⇩E B" "f' ∈ A →⇩E B"
      unfolding domain_and_range_permutation_def by auto
    moreover from ‹p⇩A permutes A› ‹p⇩B permutes B› have "inv p⇩A permutes A" "inv p⇩B permutes B"
      by (auto simp add: permutes_inv)
    moreover from ‹∀x∈A. f x = p⇩B (f' (p⇩A x))› have "∀x∈A. f' x = inv p⇩B (f (inv p⇩A x))"
      using ‹p⇩A permutes A› ‹p⇩B permutes B› ‹inv p⇩A permutes A› ‹inv p⇩B permutes B›
      by (metis (no_types, lifting) bij_betwE bij_inv_eq_iff permutes_bij permutes_imp_bij)
    ultimately show "(f', f) ∈ domain_and_range_permutation A B"
      unfolding domain_and_range_permutation_def by auto
  qed
next
  show "trans (domain_and_range_permutation A B)"
  proof (rule transI)
    fix f f' f''
    assume "(f, f') ∈ domain_and_range_permutation A B"
    assume "(f', f'') ∈ domain_and_range_permutation A B"
    from ‹(f, f') ∈ _› obtain p⇩A p⇩B where
      "p⇩A permutes A" "p⇩B permutes B" and "∀x∈A. f x = p⇩B (f' (p⇩A x))"
      unfolding domain_and_range_permutation_def by auto
    from ‹(f', f'') ∈ _› obtain p'⇩A p'⇩B where
      "p'⇩A permutes A" "p'⇩B permutes B" and "∀x∈A. f' x = p'⇩B (f'' (p'⇩A x))"
      unfolding domain_and_range_permutation_def by auto
    from ‹(f, f') ∈ domain_and_range_permutation A B› have "f ∈ A →⇩E B"
      unfolding domain_and_range_permutation_def by auto
    moreover from ‹(f', f'') ∈ domain_and_range_permutation A B› have "f'' ∈ A →⇩E B"
      unfolding domain_and_range_permutation_def by auto
    moreover from ‹p⇩A permutes A› ‹p'⇩A permutes A› have "(p'⇩A ∘ p⇩A) permutes A"
      by (simp add: permutes_compose)
    moreover from ‹p⇩B permutes B› ‹p'⇩B permutes B› have "(p⇩B ∘ p'⇩B) permutes B"
      by (simp add: permutes_compose)
    moreover have "∀x∈A. f x = (p⇩B ∘ p'⇩B) (f'' ((p'⇩A ∘ p⇩A) x))"
      using ‹∀x∈A. f' x = p'⇩B (f'' (p'⇩A x))› ‹∀x∈A. f x = p⇩B (f' (p⇩A x))› ‹p⇩A permutes A›
      by (simp add: permutes_in_image)
    ultimately show "(f, f'') ∈ domain_and_range_permutation A B"
      unfolding domain_and_range_permutation_def by fastforce
  qed
qed

subsubsection ‹Respecting Functions›

lemma inj_on_respects_domain_and_range_permutation:
  "(λf. inj_on f A) respects domain_and_range_permutation A B"
proof (rule congruentI)
  fix f f'
  assume "(f, f') ∈ domain_and_range_permutation A B"
  from this obtain p⇩A p⇩B where "p⇩A permutes A" "p⇩B permutes B" and "∀x∈A. f x = p⇩B (f' (p⇩A x))"
    unfolding domain_and_range_permutation_def by auto
  from ‹(f, f') ∈ domain_and_range_permutation A B› have "f' ` A ⊆ B"
    unfolding domain_and_range_permutation_def by auto
  from ‹p⇩A permutes A› have "p⇩A ` A = A" by (auto simp add: permutes_image)
  from ‹p⇩A permutes A› have "inj_on p⇩A A"
    using bij_betw_imp_inj_on permutes_imp_bij by blast
  from ‹p⇩B permutes B› have "inj_on p⇩B B"
    using bij_betw_imp_inj_on permutes_imp_bij by blast
  show "inj_on f A ⟷ inj_on f' A"
  proof -
    have "inj_on f A ⟷ inj_on (λx. p⇩B (f' (p⇩A x))) A"
      using ‹∀x∈A. f x = p⇩B (f' (p⇩A x))› inj_on_cong comp_apply by fastforce
    have "inj_on f A ⟷ inj_on (p⇩B o f' o p⇩A) A"
      by (simp add: ‹∀x∈A. f x = p⇩B (f' (p⇩A x))› inj_on_def)
    also have "inj_on (p⇩B o f' o p⇩A) A ⟷ inj_on (p⇩B o f') A"
      using ‹inj_on p⇩A A› ‹p⇩A ` A = A›
      by (auto dest: inj_on_imageI intro: comp_inj_on)
    also have "inj_on (p⇩B o f') A ⟷ inj_on f' A"
      using ‹inj_on p⇩B B› ‹f' ` A ⊆ B›
      by (auto dest: inj_on_imageI2 intro: comp_inj_on inj_on_subset)
    finally show ?thesis .
  qed
qed

lemma surjective_respects_domain_and_range_permutation:
  "(λf. f ` A = B) respects domain_and_range_permutation A B"
proof (rule congruentI)
  fix f f'
  assume "(f, f') ∈ domain_and_range_permutation A B"
  from this obtain p⇩A p⇩B where
    permutes: "p⇩A permutes A" "p⇩B permutes B" and "∀x∈A. f x = p⇩B (f' (p⇩A x))"
    unfolding domain_and_range_permutation_def by auto
  from permutes have "p⇩A ` A = A" "p⇩B ` B = B" by (auto simp add: permutes_image)
  from ‹p⇩B permutes B› have "inj p⇩B" by (simp add: permutes_inj)
  show "(f ` A = B) ⟷ (f' ` A = B)"
  proof -
    have "f ` A = B ⟷ (λx. p⇩B (f' (p⇩A x))) ` A = B"
      using ‹∀x∈A. f x = p⇩B (f' (p⇩A x))› by (metis (mono_tags, lifting) image_cong)
    also have "(λx. p⇩B (f' (p⇩A x))) ` A = B ⟷ (λx. p⇩B (f' x)) ` A = B"
      using ‹p⇩A ` A = A› by (metis image_image)
    also have "(λx. p⇩B (f' x)) ` A = B ⟷ (f' ` A = B)"
      using ‹p⇩B ` B = B› ‹inj p⇩B› by (metis image_image image_inv_f_f)
    finally show ?thesis .
  qed
qed

lemma bij_betw_respects_domain_and_range_permutation:
  "(λf. bij_betw f A B) respects domain_and_range_permutation A B"
proof (rule congruentI)
  fix f f'
  assume "(f, f') ∈ domain_and_range_permutation A B"
  from this obtain p⇩A p⇩B where "p⇩A permutes A" "p⇩B permutes B"
    and "∀x∈A. f x = p⇩B (f' (p⇩A x))" and "f' ∈ A →⇩E B"
    unfolding domain_and_range_permutation_def by auto
  have "bij_betw f A B ⟷ bij_betw (p⇩B o f' o p⇩A) A B"
    using ‹∀x∈A. f x = p⇩B (f' (p⇩A x))› bij_betw_congI by fastforce
  also have "... ⟷ bij_betw (p⇩B o f')  A B"
    using ‹p⇩A permutes A›
    by (auto intro!: bij_betw_comp_iff[symmetric] permutes_imp_bij)
  also have "... ⟷ bij_betw f' A B"
    using ‹f' ∈ A →⇩E B› ‹p⇩B permutes B›
    by (auto intro!: bij_betw_comp_iff2[symmetric] permutes_imp_bij)
  finally show "bij_betw f A B ⟷ bij_betw f' A B" .
qed

lemma count_image_mset':
  "count (image_mset f A) x = sum (count A) {x' ∈ set_mset A. f x' = x}"
proof -
  have "count (image_mset f A) x = sum (count A) (f -` {x} ∩ set_mset A)"
    unfolding count_image_mset ..
  also have "… = sum (count A) {x' ∈ set_mset A. f x' = x}"
  proof -
    have "(f -` {x} ∩ set_mset A) = {x' ∈ set_mset A. f x' = x}" by blast
    from this show ?thesis by simp
  qed
  finally show ?thesis .
qed

lemma multiset_of_partition_cards_respects_domain_and_range_permutation:
  assumes "finite B"
  shows "(λf. image_mset (λX. card X) (mset_set (((λb. {x ∈ A. f x = b})) ` B - {{}}))) respects domain_and_range_permutation A B"
proof (rule congruentI)
  fix f f'
  assume "(f, f') ∈ domain_and_range_permutation A B"
  from this obtain p⇩A p⇩B where "p⇩A permutes A" "p⇩B permutes B" "∀x∈A. f x = p⇩B (f' (p⇩A x))"
    unfolding domain_and_range_permutation_def by auto
  have "(λb. {x ∈ A. f x = b}) ` B = (λb. {x ∈ A. p⇩B (f' (p⇩A x)) = b}) ` B"
    using ‹∀x∈A. f x = p⇩B (f' (p⇩A x))› by auto
  from this have "image_mset card (mset_set ((λb. {x ∈ A. f x = b}) ` B - {{}})) =
    image_mset card (mset_set ((λb. {x ∈ A. p⇩B (f' (p⇩A x)) = b}) ` B - {{}}))" by simp
  also have "image_mset card (mset_set ((λb. {x ∈ A. p⇩B (f' (p⇩A x)) = b}) ` B - {{}})) =
    image_mset card (mset_set ((λb. {x ∈ A. f' (p⇩A x) = b}) ` B - {{}}))"
    using permutes_implies_inv_image_on_eq[OF ‹p⇩B permutes B›, of A] by metis
  also have "image_mset card (mset_set ((λb. {x ∈ A. f' (p⇩A x) = b}) ` B - {{}})) =
    image_mset card (mset_set ((λb. {x ∈ A. f' x = b}) ` B - {{}}))"
  proof (rule multiset_eqI)
    fix n
    have "bij_betw (λX. p⇩A ` X) {X ∈ (λb. {x ∈ A. f' (p⇩A x) = b}) ` B - {{}}. card X = n} {X ∈ (λb. {x ∈ A. f' x = b}) ` B - {{}}. card X = n}"
    proof (rule bij_betw_byWitness)
      show "∀X∈{X ∈ (λb. {x ∈ A. f' (p⇩A x) = b}) ` B - {{}}. card X = n}. inv p⇩A ` p⇩A ` X = X"
        by (meson ‹p⇩A permutes A› image_inv_f_f permutes_inj)
      show "∀X∈{X ∈ (λb. {x ∈ A. f' x = b}) ` B - {{}}. card X = n}. p⇩A ` inv p⇩A ` X = X"
        by (meson ‹p⇩A permutes A› image_f_inv_f permutes_surj)
      show "(λX. p⇩A ` X) ` {X ∈ (λb. {x ∈ A. f' (p⇩A x) = b}) ` B - {{}}. card X = n} ⊆ {X ∈ (λb. {x ∈ A. f' x = b}) ` B - {{}}. card X = n}"
      proof -
        have "card (p⇩A ` {x ∈ A. f' (p⇩A x) = b}) = card {x ∈ A. f' (p⇩A x) = b}" for b
        proof -
          have "inj_on p⇩A {x ∈ A. f' (p⇩A x) = b}"
            by (metis (no_types, lifting) ‹p⇩A permutes A› injD inj_onI permutes_inj)
          from this show ?thesis by (simp add: card_image)
        qed
        moreover have "p⇩A ` {x ∈ A. f' (p⇩A x) = b} = {x ∈ A. f' x = b}" for b
        proof
          show "p⇩A ` {x ∈ A. f' (p⇩A x) = b} ⊆ {x ∈ A. f' x = b}"
            by (auto simp add: ‹p⇩A permutes A› permutes_in_image)
          show "{x ∈ A. f' x = b} ⊆ p⇩A ` {x ∈ A. f' (p⇩A x) = b}"
          proof
            fix x
            assume "x ∈ {x ∈ A. f' x = b}"
            moreover have "p⇩A (inv p⇩A x) = x"
              using ‹p⇩A permutes A› permutes_inverses(1) by fastforce
            moreover from ‹x ∈ {x ∈ A. f' x = b}› have "inv p⇩A x ∈ A"
              by (simp add: ‹p⇩A permutes A› permutes_in_image permutes_inv)
            ultimately show "x ∈ p⇩A ` {x ∈ A. f' (p⇩A x) = b}"
              by (auto intro: image_eqI[where x="inv p⇩A x"])
          qed
        qed
        ultimately show ?thesis by auto
      qed
      show "(λX. inv p⇩A ` X) ` {X ∈ (λb. {x ∈ A. f' x = b}) ` B - {{}}. card X = n} ⊆ {X ∈ (λb. {x ∈ A. f' (p⇩A x) = b}) ` B - {{}}. card X = n}"
      proof -
        have "card (inv p⇩A ` {x ∈ A. f' x = b}) = card {x ∈ A. f' x = b}" for b
        proof -
          have "inj_on (inv p⇩A) {x ∈ A. f' x = b}"
            by (metis (no_types, lifting) ‹p⇩A permutes A› injD inj_onI permutes_surj surj_imp_inj_inv)
          from this show ?thesis by (simp add: card_image)
        qed
        moreover have "inv p⇩A ` {x ∈ A. f' x = b} = {x ∈ A. f' (p⇩A x) = b}" for b
        proof
          show "inv p⇩A ` {x ∈ A. f' x = b} ⊆ {x ∈ A. f' (p⇩A x) = b}"
            using ‹p⇩A permutes A›
            by (auto simp add: permutes_in_image permutes_inv permutes_inverses(1))
          show "{x ∈ A. f' (p⇩A x) = b} ⊆ inv p⇩A ` {x ∈ A. f' x = b}"
          proof
            fix x
            assume "x ∈ {x ∈ A. f' (p⇩A x) = b}"
            moreover have "inv p⇩A (p⇩A x) = x"
              by (meson ‹p⇩A permutes A› permutes_inverses(2))
            moreover from ‹x ∈ {x ∈ A. f' (p⇩A x) = b}› have "p⇩A x ∈ A"
              by (simp add: ‹p⇩A permutes A› permutes_in_image)
            ultimately show "x ∈ inv p⇩A ` {x ∈ A. f' x = b}"
              by (auto intro: image_eqI[where x="p⇩A x"])
          qed
        qed
        ultimately show ?thesis by auto
      qed
    qed
    from this have "card {x' ∈ (λb. {x ∈ A. f' (p⇩A x) = b}) ` B - {{}}. card x' = n} = card {x' ∈ (λb. {x ∈ A. f' x = b}) ` B - {{}}. card x' = n}"
      by (rule bij_betw_same_card)
    from this show "count (image_mset card (mset_set ((λb. {x ∈ A. f' (p⇩A x) = b}) ` B - {{}}))) n =
      count (image_mset card (mset_set ((λb. {x ∈ A. f' x = b}) ` B - {{}}))) n"
      using ‹finite B› by (simp add: count_image_mset')
  qed
  finally show "image_mset card (mset_set ((λb. {x ∈ A. f x = b}) ` B - {{}})) =
    image_mset card (mset_set ((λb. {x ∈ A. f' x = b}) ` B - {{}}))" .
qed

end