Theory Twelvefold_Way.Twelvefold_Way_Core

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

section ‹Main Observations on Operations and Permutations›

theory Twelvefold_Way_Core
imports Preliminaries
begin

subsection ‹Range Multiset›

subsubsection ‹Existence of a Suitable Finite Function›

lemma obtain_function:
  assumes "finite A"
  assumes "size M = card A"
  shows "f. image_mset f (mset_set A) = M"
using assms
proof (induct arbitrary: M rule: finite_induct)
  case empty
  from this show ?case by simp
next
  case (insert x A)
  from insert(1,2,4) have "size M > 0"
    by (simp add: card_gt_0_iff)
  from this obtain y where "y ∈# M"
    using gr0_implies_Suc size_eq_Suc_imp_elem by blast
  from insert(1,2,4) this have "size (M - {#y#}) = card A"
    by (simp add: Diff_insert_absorb card_Diff_singleton_if insertI1 size_Diff_submset)
  from insert.hyps this obtain f' where "image_mset f' (mset_set A) = M - {#y#}" by blast
  from this have "image_mset (f'(x := y)) (mset_set (insert x A)) = M"
    using finite A x  A y ∈# M by (simp add: image_mset_fun_upd)
  from this show ?case by blast
qed

lemma obtain_function_on_ext_funcset:
  assumes "finite A"
  assumes "size M = card A"
  shows "f  A E set_mset M. image_mset f (mset_set A) = M"
proof -
  obtain f where range_eq_M: "image_mset f (mset_set A) = M"
    using obtain_function finite A size M = card A by blast
  let ?f = "λx. if x  A then f x else undefined"
  have "?f  A E set_mset M"
    using range_eq_M finite A by auto
  moreover have "image_mset ?f (mset_set A) = M"
    using range_eq_M finite A by (auto intro: multiset.map_cong0)
  ultimately show ?thesis by auto
qed

subsubsection ‹Existence of Permutation›

lemma image_mset_eq_implies_bij_betw:
  fixes f :: "'a1  'b" and f' :: "'a2  'b"
  assumes "finite A" "finite A'"
  assumes mset_eq: "image_mset f (mset_set A) = image_mset f' (mset_set A')"
  obtains bij where "bij_betw bij A A'" and "xA. f x = f' (bij x)"
proof -
  from finite A have [simp]: "finite {a  A. f a = (b::'b)}" for b by auto
  from finite A' have [simp]: "finite {a  A'. f' a = (b::'b)}" for b by auto
  have "f ` A = f' ` A'"
  proof -
    have "f ` A = f ` (set_mset (mset_set A))" using finite A by simp
    also have " = f' ` (set_mset (mset_set A'))"
      by (metis mset_eq multiset.set_map)
    also have " = f' ` A'" using finite A' by simp
    finally show ?thesis .
  qed
  have "b(f ` A). bij. bij_betw bij {a  A. f a = b} {a  A'. f' a = b}"
  proof
    fix b
    from mset_eq have
      "count (image_mset f (mset_set A)) b = count (image_mset f' (mset_set A')) b" by simp
    from this have "card {a  A. f a = b} = card {a  A'. f' a = b}"
      using finite A finite A'
      by (simp add: count_image_mset_eq_card_vimage)
    from this show "bij. bij_betw bij {a  A. f a = b} {a  A'. f' a = b}"
      by (intro finite_same_card_bij) simp_all
  qed
  from bchoice [OF this]
  obtain bij where bij: "bf ` A. bij_betw (bij b) {a  A. f a = b} {a  A'. f' a = b}"
    by auto
  define bij' where "bij' = (λa. bij (f a) a)"
  have "bij_betw bij' A A'"
  proof -
    have "disjoint_family_on (λi. {a  A'. f' a = i}) (f ` A)"
      unfolding disjoint_family_on_def by auto
    moreover have "bij_betw (λa. bij (f a) a) {a  A. f a = b} {a  A'. f' a = b}" if b: "b  f ` A" for b
      using bij b by (subst bij_betw_cong[where g="bij b"]) auto
    ultimately have "bij_betw (λa. bij (f a) a) (bf ` A. {a  A. f a = b}) (bf ` A. {a  A'. f' a = b})"
      by (rule bij_betw_UNION_disjoint)
    moreover have "(bf ` A. {a  A. f a = b}) = A" by auto
    moreover have "(bf ` A. {a  A'. f' a = b}) = A'" using f ` A = f' ` A' by auto
    ultimately show "bij_betw bij' A A'"
      unfolding bij'_def by (subst bij_betw_cong[where g="(λa. bij (f a) a)"]) auto
  qed
  moreover from bij have "xA. f x = f' (bij' x)"
    unfolding bij'_def using bij_betwE by fastforce
  ultimately show ?thesis by (rule that)
qed

lemma image_mset_eq_implies_permutes:
  fixes f :: "'a  'b"
  assumes "finite A"
  assumes mset_eq: "image_mset f (mset_set A) = image_mset f' (mset_set A)"
  obtains p where "p permutes A" and "xA. f x = f' (p x)"
proof -
  from assms obtain b where "bij_betw b A A" and "xA. f x = f' (b x)"
    using image_mset_eq_implies_bij_betw by blast
  define p where "p = (λa. if a  A then b a else a)"
  have "p permutes A"
  proof (rule bij_imp_permutes)
    show "bij_betw p A A"
      unfolding p_def by (simp add: bij_betw b A A bij_betw_cong)
  next
    fix x
    assume "x  A"
    from this show "p x = x"
      unfolding p_def by simp
  qed
  moreover from xA. f x = f' (b x) have "xA. f x = f' (p x)"
    unfolding p_def by simp
  ultimately show ?thesis by (rule that)
qed

subsection ‹Domain Partition›

subsubsection ‹Existence of a Suitable Finite Function›

lemma obtain_function_with_partition:
  assumes "finite A" "finite B"
  assumes "partition_on A P"
  assumes "card P  card B"
  shows "f  A E B. (λb. {x  A. f x = b}) ` B - {{}} = P"
proof -
  obtain g' where "bij_betw g' P (g' ` P)" and "g' ` P  B"
    by (meson assms card_le_inj finite_elements inj_on_imp_bij_betw)
  define f where "a. f a = (if a  A then g' (THE X. a  X  X  P) else undefined)"
  have "f  A E B"
  unfolding f_def
  using g' ` P  B assms(3) partition_on_the_part_mem by fastforce
  moreover have "(λb. {x  A. f x = b}) ` B - {{}} = P"
  proof
    show "(λb. {x  A. f x = b}) ` B - {{}}  P"
    proof
      fix X
      assume X:"X  (λb. {x  A. f x = b}) ` B - {{}}"
      from this obtain b where "b  B" and "X = {x'  A. f x' = b}" by auto
      from this X obtain a where "a  A" and "a  X" and "f a = b" by blast
      have "(THE X. a  X  X  P)  P"
        using a  A partition_on A P by (simp add: partition_on_the_part_mem)
      from X = {x'  A. f x' = b} have X_eq1: "X = {x'  A. g' (THE X. x'  X  X  P) = b}"
        unfolding f_def by auto
      also have " = {x'  A. (THE X. x'  X  X  P) = inv_into P g' b}"
      proof -
        {
          fix x'
          assume "x'  A"
          have "(THE X. x'  X  X  P)  P"
            using partition_on A P x'  A by (simp add: partition_on_the_part_mem)
          from X_eq1 a  X have "g' (THE X. a  X  X  P) = b"
            unfolding f_def by auto
          from this (THE X. a  X  X  P)  P have "b  g' ` P" by auto
          have "(g' (THE X. x'  X  X  P) = b)  ((THE X. x'  X  X  P) = inv_into P g' b)"
          proof -
            from (THE X. x'  X  X  P)  P
            have "(g' (THE X. x'  X  X  P) = b)  (inv_into P g' (g' (THE X. x'  X  X  P)) = inv_into P g' b)"
              using b  g' ` P by (auto intro: inv_into_injective)
            moreover have "inv_into P g' (g' (THE X. x'  X  X  P)) = (THE X. x'  X  X  P)"
              using bij_betw g' P (g' ` P) (THE X. x'  X  X  P)  P
              by (simp add: bij_betw_inv_into_left)
            ultimately show ?thesis by simp
          qed
        }
        from this show ?thesis by auto
      qed
      finally have X_eq: "X = {x'  A. (THE X. x'  X  X  P) = inv_into P g' b}" .
      moreover have "inv_into P g' b  P"
      proof -
        from X_eq have eq: "inv_into P g' b = (THE X. a  X  X  P)"
          using a  X a  A by auto
        from this show ?thesis
          using (THE X. a  X  X  P)  P by simp
      qed
      ultimately have "X = inv_into P g' b"
        using partition_on_all_in_part_eq_part[OF partition_on A P] by blast
      from this inv_into P g' b  P show "X  P" by blast
    qed
  next
    show "P  (λb. {x  A. f x = b}) ` B - {{}}"
    proof
      fix X
      assume "X  P"
      from assms(3) this have "X  {}"
        by (auto elim: partition_onE)
      moreover have "X  (λb. {x  A. f x = b}) ` B"
      proof
        show "g' X  B"
          using X  P g' ` P  B by blast
        show "X = {x  A. f x = g' X}"
        proof
          show "X  {x  A. f x = g' X}"
          proof
            fix x
            assume "x  X"
            from this have "x  A"
              using X  P assms(3) by (fastforce elim: partition_onE)
            have "(THE X. x  X  X  P) = X"
              using X  P x  X assms(3) partition_on_the_part_eq by fastforce
            from this x  A have "f x = g' X"
              unfolding f_def by auto
            from this x  A show "x  {x  A. f x = g' X}" by auto
          qed
        next
          show "{x  A. f x = g' X}  X"
          proof
            fix x
            assume "x  {x  A. f x = g' X}"
            from this have "x  A" and g_eq: "g' (THE X. x  X  X  P) = g' X"
              unfolding f_def by auto
            from x  A have "(THE X. x  X  X  P)  P"
              using assms(3) by (simp add: partition_on_the_part_mem)
            from this g_eq have "(THE X. x  X  X  P) = X"
              using X  P bij_betw g' P (g' ` P)
              by (metis bij_betw_inv_into_left)
            from this x  A assms(3) show "x  X"
              using partition_on_in_the_unique_part by fastforce
          qed
        qed
      qed
      ultimately show "X  (λb. {x  A. f x = b}) ` B - {{}}"
        by auto
    qed
  qed
  ultimately show ?thesis by blast
qed

subsubsection ‹Equality under Permutation Application›

lemma permutes_implies_inv_image_on_eq:
  assumes "p permutes B"
  shows "(λb. {x  A. p (f x) = b}) ` B = (λb. {x  A. f x = b}) ` B"
proof -
  have "b  B. x  A. p (f x) = b  f x = inv p b"
    using p permutes B by (auto simp add: permutes_inverses)
  from this have "(λb. {x  A. p (f x) = b}) ` B = (λb. {x  A. f x = inv p b}) ` B"
    using image_cong by blast
  also have " = (λb. {x  A. f x = b}) ` inv p ` B"
    by (auto simp add: image_comp)
  also have " = (λb. {x  A. f x = b}) ` B"
    by (simp add: p permutes B permutes_inv permutes_image)
  finally show ?thesis .
qed

subsubsection ‹Existence of Permutation›

lemma the_elem:
  assumes "f  A E B" "f'  A E B"
  assumes partitions_eq: "(λb. {x  A. f x = b}) ` B - {{}} = (λb. {x  A. f' x = b}) ` B - {{}}"
  assumes "x  A"
  shows "the_elem (f ` {xa  A. f' xa = f' x}) = f x"
proof -
  from x  A have x: "x  {x'  A. f' x' = f' x}" by blast
  have "f' x  B"
    using x  A f'  A E B by blast
  from this have "{x'  A. f' x' = f' x}  (λb. {x  A. f' x = b}) ` B - {{}}"
    using x  A by blast
  from this have "{x'  A. f' x' = f' x}  (λb. {x  A. f x = b}) ` B - {{}}"
    using partitions_eq by blast
  from this obtain b where eq: "{x'  A. f' x' = f' x} = {x'  A. f x' = b}" by blast
  also from x this show "the_elem (f ` {x'  A. f' x' = f' x}) = f x"
    by (metis (mono_tags, lifting) empty_iff mem_Collect_eq the_elem_image_unique)
qed

lemma the_elem_eq:
  assumes "f  A E B"
  assumes "b  f ` A"
  shows "the_elem (f ` {x'  A. f x' = b}) = b"
proof -
  from b  f ` A obtain a where "a  A" and "b = f a" by blast
  from this show "the_elem (f ` {x'  A. f x' = b}) = b"
    using the_elem[OF f  A E B f  A E B] by simp
qed

lemma partitions_eq_implies:
  assumes "f  A E B" "f'  A E B"
  assumes partitions_eq: "(λb. {x  A. f x = b}) ` B - {{}} = (λb. {x  A. f' x = b}) ` B - {{}}"
  assumes "x  A" "x'  A"
  assumes "f x = f x'"
  shows "f' x = f' x'"
proof -
  have "f x  B" and "x  {a  A. f a = f x}" and "x'  {a  A. f a = f x}"
    using f  A E B x  A x'  A f x = f x' by auto
  moreover have "{a  A. f a = f x}  (λb. {x  A. f x = b}) ` B - {{}}"
    using f x  B x  {a  A. f a = f x} by auto
  ultimately obtain b where "x  {a  A. f' a = b}" and "x'  {a  A. f' a = b}"
    using partitions_eq by (metis (no_types, lifting) Diff_iff imageE)
  from this show "f' x = f' x'" by auto
qed

lemma card_domain_partitions:
  assumes "f  A E B"
  assumes "finite B"
  shows "card ((λb. {x  A. f x = b}) ` B - {{}}) = card (f ` A)"
proof -
  note [simp] = the_elem_eq[OF f  A E B]
  have "bij_betw (λX. the_elem (f ` X)) ((λb. {x  A. f x = b}) ` B - {{}}) (f ` A)"
  proof (rule bij_betw_imageI)
    show "inj_on (λX. the_elem (f ` X)) ((λb. {x  A. f x = b}) ` B - {{}})"
    proof (rule inj_onI)
      fix X X'
      assume X: "X  (λb. {x  A. f x = b}) ` B - {{}}"
      assume X': "X'  (λb. {x  A. f x = b}) ` B - {{}}"
      assume eq: "the_elem (f ` X) = the_elem (f ` X')"
      from X obtain b where "b  B" and X_eq: "X = {x  A. f x = b}" by blast
      from X this have "b  f ` A"
        using Collect_empty_eq Diff_iff image_iff insertCI by auto
      from X' obtain b' where "b'  B" and X'_eq: "X' = {x  A. f x = b'}" by blast
      from X' this have "b'  f ` A"
        using Collect_empty_eq Diff_iff image_iff insertCI by auto
      from X_eq X'_eq eq b. b  f ` A  the_elem (f ` {x'  A. f x' = b}) = b b  f ` A b'  f ` A
        have "b = b'" by auto
      from this show "X = X'"
        using X_eq X'_eq by simp
    qed
    show "(λX. the_elem (f ` X)) ` ((λb. {x  A. f x = b}) ` B - {{}}) = f ` A"
    proof
      show "(λX. the_elem (f ` X)) ` ((λb. {x  A. f x = b}) ` B - {{}})  f ` A"
        using b. b  f ` A  the_elem (f ` {x'  A. f x' = b}) = b by auto 
    next
      show "f ` A  (λX. the_elem (f ` X)) ` ((λb. {x  A. f x = b}) ` B - {{}})"
      proof
        fix b
        assume "b  f ` A"
        from this have "b = the_elem (f ` {x  A. f x = b})"
          using b. b  f ` A  the_elem (f ` {x'  A. f x' = b}) = b by auto
        moreover from b  f ` A have " {x  A. f x = b}  (λb. {x  A. f x = b}) ` B - {{}}"
          using f  A E B by auto
        ultimately show "b  (λX. the_elem (f ` X)) ` ((λb. {x  A. f x = b}) ` B - {{}})" ..
      qed
    qed
  qed
  from this show ?thesis by (rule bij_betw_same_card)
qed

lemma partitions_eq_implies_permutes:
  assumes "f  A E B" "f'  A E B"
  assumes "finite B"
  assumes partitions_eq: "(λb. {x  A. f x = b}) ` B - {{}} = (λb. {x  A. f' x = b}) ` B - {{}}"
  shows "p. p permutes B  (xA. f x = p (f' x))"
proof -
  have card_eq: "card (f' ` A) = card (f ` A)"
    using card_domain_partitions[OF f  A E B finite B]
    using card_domain_partitions[OF f'  A E B finite B]
    using partitions_eq by simp
  have "f' ` A  B" "f ` A  B"
    using f  A E B f'  A E B by auto
  from this card_eq have "card (B - f' ` A) = card (B - f ` A)"
    using finite B by (auto simp add: card_Diff_subset finite_subset)
  from this obtain p' where "bij_betw p' (B - f' ` A) (B - f ` A)"
    using finite B by (metis finite_same_card_bij finite_Diff)
  from this have "p' ` (B - f' ` A) = (B - f ` A)"
    by (simp add: bij_betw_imp_surj_on)
  define p where "b. p b = (if b  B then
    (if b  f' ` A then the_elem (f ` {x  A. f' x = b}) else p' b) else b)"
  have "xA. f x = p (f' x)"
  proof
    fix x
    assume "x  A"
    from this partitions_eq have "the_elem (f ` {xa  A. f' xa = f' x}) = f x"
      using the_elem[OF f  A E B f'  A E B] by auto
    from this show "f x = p (f' x)"
      using x  A p_def f'  A E B by auto
  qed
  moreover have "p permutes B"
  proof (rule bij_imp_permutes)
    let ?invp = "λb. if b  f ` A then the_elem (f' ` {x  A. f x = b}) else b"
    note [simp] = the_elem[OF f  A E B f'  A E B partitions_eq]
    show "bij_betw p B B"
    proof (rule bij_betw_imageI)
      show "p ` B = B"
      proof
        have "(λb. the_elem (f ` {x  A. f' x = b})) ` (f' ` A)  B"
          using f  A E B by auto
        from p' ` (B - f' ` A) = (B - f ` A) this show "p ` B  B"
          unfolding p_def f  A E B by force
      next
        show "B  p ` B"
        proof
          fix b
          assume "b  B"
          show "b  p ` B"
          proof (cases "b  f ` A")
            assume "b  f ` A"
            note p' ` (B - f' ` A) = (B - f ` A)
            from this b  B b  f ` A show ?thesis
              unfolding p_def by auto
          next
            assume "b  f ` A"
            from this xA. f x = p (f' x) b  B show ?thesis
              using f'  A E B by auto
          qed
        qed
      qed
    next
      show "inj_on p B"
      proof (rule inj_onI)
        fix b b'
        assume "b  B" "b'  B" "p b = p b'"
        have "b  f' ` A  b'  f' ` A"
        proof -
          have "b  f' ` A  p b  f ` A"
            unfolding p_def using b  B p' ` (B - f' ` A) = B - f ` A by auto
          also have "p b  f ` A  p b'  f ` A"
            using p b = p b' by simp
          also have "p b'  f ` A  b'  f' ` A"
            unfolding p_def using b'  B p' ` (B - f' ` A) = B - f ` A by auto
          finally show ?thesis .
        qed
        from this have "(b  f' ` A  b'  f' ` A)  (b  f' ` A  b'  f' ` A)" by blast
        from this show "b = b'"
        proof
          assume "b  f' ` A  b'  f' ` A"
          from this obtain a a' where "a  A" "b = f' a" and "a'  A" "b' = f' a'" by auto
          from this b  B b'  B have "p b = f a" "p b' = f a'"
            unfolding p_def by auto
          from this p b = p b' have "f a = f a'" by simp
          from this have "f' a = f' a'"
            using partitions_eq_implies[OF f  A E B f'  A E B partitions_eq]
            using a  A a'  A by blast
          from this show "b = b'"
            using b' = f' a' b = f' a by simp
        next
          assume "b  f' ` A  b'  f' ` A"
          from this b  B b'  B have "p b' = p' b'" "p b = p' b"
            unfolding p_def by auto
          from this p b = p b' have "p' b = p' b'" by simp
          moreover have "b  B - f' ` A" "b'  B - f' ` A"
            using b  B b'  B b  f' ` A  b'  f' ` A by auto
          ultimately show "b = b'"
            using bij_betw p' _ _ by (metis bij_betw_inv_into_left)
        qed
      qed
    qed
  next
    fix x
    assume "x  B"
    from this show "p x = x"
      using f'  A E B p_def by auto
  qed
  ultimately show ?thesis by blast
qed

subsection ‹Number Partition of Range›

subsubsection ‹Existence of a Suitable Finite Function›

lemma obtain_partition:
  assumes "finite A"
  assumes "number_partition (card A) N"
  shows "P. partition_on A P  image_mset card (mset_set P) = N"
using assms
proof (induct N arbitrary: A)
  case empty
  from this have "A = {}"
    unfolding number_partition_def by auto
  from this have "partition_on A {}" by (simp add: partition_on_empty)
  moreover have "image_mset card (mset_set {}) = {#}" by simp
  ultimately show ?case by blast
next
  case (add x N)
  from add.prems(2) have "0 ∉# add_mset x N" and "sum_mset (add_mset x N) = card A"
    unfolding number_partition_def by auto
  from this have "x  card A" by auto
  from this obtain X where "X  A" and "card X = x"
    using subset_with_given_card_exists by auto
  from this have "X  {}"
    using 0 ∉# add_mset x N finite A by auto
  have "sum_mset N = card (A - X)"
    using sum_mset (add_mset x N) = card A card X = x X  A
    by (metis add.commute add.prems(1) add_diff_cancel_right' card_Diff_subset infinite_super sum_mset.add_mset)
  from this 0 ∉# add_mset x N have "number_partition (card (A - X)) N"
    unfolding number_partition_def by auto
  from this obtain P where "partition_on (A - X) P" and eq_N: "image_mset card (mset_set P) = N"
    using add.hyps finite A by auto
  from partition_on (A - X) P have "finite P"
    using finite A finite_elements by blast
  from partition_on (A - X) P have "X  P"
    using X  {} partition_onD1 by fastforce
  have "partition_on A (insert X P)"
    using partition_on (A - X) P X  A X  {}
    by (rule partition_on_insert')
  moreover have "image_mset card (mset_set (insert X P)) = add_mset x N"
    using eq_N card X = x finite P X  P by simp
  ultimately show ?case by blast
qed

lemma obtain_extensional_function_from_number_partition:
  assumes "finite A" "finite B"
  assumes "number_partition (card A) N"
  assumes "size N  card B"
  shows "fA E B. image_mset (λX. card X) (mset_set (((λb. {x  A. f x = b})) ` B - {{}})) = N"
proof -
  obtain P where "partition_on A P" and eq_N: "image_mset card (mset_set P) = N"
    using assms obtain_partition by blast
  from eq_N[symmetric] size N  card B have "card P  card B" by simp
  from partition_on A P this obtain f where "f  A E B"
    and eq_P: "(λb. {x  A. f x = b}) ` B - {{}} = P"
    using obtain_function_with_partition[OF finite A finite B] by blast
  have "image_mset (λX. card X) (mset_set (((λb. {x  A. f x = b})) ` B - {{}})) = N"
    using eq_P eq_N by simp
  from this f  A E B show ?thesis by auto
qed

subsubsection ‹Equality under Permutation Application›

lemma permutes_implies_multiset_of_partition_cards_eq:
  assumes "pA permutes A" "pB permutes B"
  shows "image_mset card (mset_set ((λb. {x  A. pB (f' (pA x)) = b}) ` B - {{}})) = image_mset card (mset_set ((λb. {x  A. f' x = b}) ` B - {{}}))"
proof -
  have "inj_on ((`) (inv pA)) ((λb. {x  A. f' x = b}) ` B - {{}})"
    by (meson pA permutes A inj_image_eq_iff inj_onI permutes_surj surj_imp_inj_inv)
  have "image_mset card (mset_set ((λb. {x  A. pB (f' (pA x)) = b}) ` B - {{}})) =
    image_mset card (mset_set ((λX. inv pA ` X) ` ((λb. {x  A. f' x = b}) ` B - {{}})))"
  proof -
    have "(λb. {x  A. pB (f' (pA x)) = b}) ` B - {{}} = (λb. {x  A. f' (pA x) = b}) ` B - {{}}"
      using permutes_implies_inv_image_on_eq[OF pB permutes B] by metis
    also have " = (λb. inv pA ` {x  A. f' x = b}) ` B - {{}}"
    proof -
      have "{x  A. f' (pA x) = b} = inv pA ` {x  A. f' x = b}" for b
      proof
        show "{x  A. f' (pA x) = b}  inv pA ` {x  A. f' x = b}"
        proof
          fix x
          assume "x  {x  A. f' (pA x) = b}"
          from this have "x  A" "f' (pA x) = b" by auto
          moreover from this pA permutes A have "pA x  A" by (simp add: permutes_in_image)
          moreover from pA permutes A have "x = inv pA (pA x)"
            using permutes_inverses(2) by fastforce
          ultimately show "x  inv pA ` {x  A. f' x = b}" by auto
        qed
      next
        show "inv pA ` {x  A. f' x = b}  {x  A. f' (pA x) = b}"
        proof
          fix x
          assume "x  inv pA ` {x  A. f' x = b}"
          from this obtain x' where x: "x = inv pA x'" "x'  A" "f' x' = b" by auto
          from this pA permutes A have "x  A" by (simp add: permutes_in_image permutes_inv)
          from x = inv pA x' f' x' = b have "f' (pA x) = b"
            using pA permutes A permutes_inverses(1) by fastforce
          from this x  A show "x  {x  A. f' (pA x) = b}" by auto
        qed
      qed
      from this show ?thesis by blast
    qed
    also have " = (λX. inv pA ` X) ` ((λb. {x  A. f' x = b}) ` B - {{}})" by auto
    finally show ?thesis by simp
  qed
  also have " = image_mset (λX. card (inv pA ` X)) (mset_set ((λb. {x  A. f' x = b}) ` B - {{}}))"
    using inj_on ((`) (inv pA)) ((λb. {x  A. f' x = b}) ` B - {{}})
    by (simp only: image_mset_mset_set[symmetric] image_mset.compositionality) (meson comp_apply)
  also have " = image_mset card (mset_set ((λb. {x  A. f' x = b}) ` B - {{}}))"
    using pA permutes A by (simp add: card_image inj_on_inv_into permutes_surj)
  finally show ?thesis .
qed

subsubsection ‹Existence of Permutation›

lemma partition_implies_permutes:
  assumes "finite A"
  assumes "partition_on A P" "partition_on A P'"
  assumes "image_mset card (mset_set P') = image_mset card (mset_set P)"
  obtains p where "p permutes A" "P' = (λX. p ` X) ` P"
proof -
  from partition_on A P partition_on A P' have "finite P" "finite P'"
    using finite A finite_elements by blast+
  from this image_mset card (mset_set P') = image_mset card (mset_set P)
  obtain bij where "bij_betw bij P P'" and "XP. card X = card (bij X)"
    using image_mset_eq_implies_bij_betw by metis
  have "XP. p'. bij_betw p' X (bij X)"
  proof
    fix X
    assume "X  P"
    from this have "X  A"
      using partition_on A P partition_onD1 by fastforce
    from this have "finite X"
      using finite A rev_finite_subset by blast
    from X  P have "bij X  P'"
      using bij_betw bij P P' bij_betwE by blast
    from this have "bij X  A"
      using partition_on A P' partition_onD1 by fastforce
    from this have "finite (bij X)"
      using finite A rev_finite_subset by blast
    from X  P have "card X = card (bij X)"
      using XP. card X = card (bij X) by blast
    from this show "p'. bij_betw p' X (bij X)"
      using finite (bij X) finite X finite_same_card_bij by blast
  qed
  from this have "p'. XP. bij_betw (p' X) X (bij X)" by metis
  from this obtain p' where p': "XP. bij_betw (p' X) X (bij X)" ..
  define p where "a. p a = (if a  A then p' (THE X. a  X  X  P) a else a)"
  have "p permutes A"
  proof -
    have "bij_betw p A A"
    proof -
      have "disjoint_family_on bij P"
      proof
        fix X X'
        assume XX': "X  P" "X'  P" "X  X'"
        from this have "bij X  P'" "bij X'  P'"
          using bij_betw bij P P' bij_betwE by blast+
        moreover from XX' have "bij X  bij X'"
          using bij_betw bij P P' by (metis bij_betw_inv_into_left)
        ultimately show "bij X  bij X' = {}"
          using partition_on A P' by (meson partition_onE)
      qed
      moreover have "bij_betw (λa. p' (THE X. a  X  X  P) a) X (bij X)" if "X  P" for X
      proof -
        from X  P have "bij_betw (p' X) X (bij X)"
          using XP. bij_betw (p' X) X (bij X) by blast
        moreover from X  P have "aX. (THE X. a  X  X  P) = X"
          using partition_on A P partition_on_the_part_eq by fastforce
        ultimately show ?thesis by (auto intro: bij_betw_congI)
      qed
      ultimately have "bij_betw (λa. p' (THE X. a  X  X  P) a) (XP. X) (XP. bij X)"
        by (rule bij_betw_UNION_disjoint)
      moreover have "(XP. X) = A" "(XP'. X) = A"
        using partition_on A P partition_on A P' partition_onD1 by auto
      moreover have "(XP. bij X) = (XP'. X)"
        using bij_betw bij P P' bij_betw_imp_surj_on by force
      ultimately have "bij_betw (λa. p' (THE X. a  X  X  P) a) A A" by simp
      moreover have "a  A. p' (THE X. a  X  X  P) a = p a"
        unfolding p_def by auto
      ultimately show ?thesis by (rule bij_betw_congI)
    qed
    moreover have "p x = x" if "x  A" for x
      using x  A p_def by auto
    ultimately show ?thesis by (rule bij_imp_permutes)
  qed
  moreover have "P' = (λX. p ` X) ` P"
  proof
    show "P'  (λX. p ` X) ` P"
    proof
      fix X
      assume "X  P'"
      have in_P: "the_inv_into P bij X  P"
        using X  P' bij_betw bij P P' bij_betwE bij_betw_the_inv_into by blast
      have eq_X: "bij (the_inv_into P bij X) = X"
        using X  P' bij_betw bij P P'
        by (meson f_the_inv_into_f_bij_betw)
      have "X = p ` (the_inv_into P bij X)"
      proof
        from in_P have "the_inv_into P bij X  A"
          using partition_on A P partition_onD1 by fastforce
        have "(λa. p' (THE X. a  X  X  P) a) ` the_inv_into P bij X = X"
        proof
          show "(λa. p' (THE X. a  X  X  P) a) ` the_inv_into P bij X  X"
          proof
            fix x
            assume "x  (λa. p' (THE X. a  X  X  P) a) ` the_inv_into P bij X"
            from this obtain a where a_in: "a  the_inv_into P bij X"
              and x_eq: "x = p' (THE X. a  X  X  P) a" by blast
            have "(THE X. a  X  X  P) = the_inv_into P bij X"
              using a_in in_P partition_on A P partition_on_the_part_eq
              by fastforce
            from this x_eq have x_eq: "x = p' (the_inv_into P bij X) a"
              by auto
            from this have "x  bij (the_inv_into P bij X)"
              using a_in in_P bij_betwE p' by blast
            from this eq_X show "x  X" by blast
          qed
        next
          show "X  (λa. p' (THE X. a  X  X  P) a) ` the_inv_into P bij X"
          proof
            fix x
            assume "x  X"
            let ?X' = "the_inv_into P bij X"
            define x' where "x' = the_inv_into ?X' (p' ?X') x"
            from in_P p' eq_X have bij_betw: "bij_betw (p' ?X') ?X' X" by auto
            from bij_betw x  X have "x'  ?X'"
              unfolding x'_def
              using bij_betwE bij_betw_the_inv_into by blast
            from this in_P have "(THE X. x'  X  X  P) = ?X'"
              using partition_on A P partition_on_the_part_eq by fastforce
            from this x  X have "x = p' (THE X. x'  X  X  P) x'"
              unfolding x'_def
              using bij_betw f_the_inv_into_f_bij_betw by fastforce
            from this x'  ?X' show "x  (λa. p' (THE X. a  X  X  P) a) ` the_inv_into P bij X" ..
          qed
        qed
        from this the_inv_into P bij X  A show "X  p ` the_inv_into P bij X"
          unfolding p_def by auto
      next
        show "p ` the_inv_into P bij X  X"
        proof
          fix x
          assume "x  p ` the_inv_into P bij X"
          from this obtain x' where "x = p x'" and "x'  the_inv_into P bij X"
            by auto
          have "x'  A"
            using x'  the_inv_into P bij X assms(2) in_P partition_onD1 by fastforce
          have eq: "(THE X. x'  X  X  P) = the_inv_into P bij X"
            using x'  the_inv_into P bij X assms(2) in_P partition_on_the_part_eq by fastforce
          have p': "p' (the_inv_into P bij X) x'  X"
            using x'  the_inv_into P bij X bij_betwE eq_X in_P p' by blast
          from x = p x' x'  A eq p' show "x  X"
            unfolding p_def by auto
        qed
      qed
      moreover from X  P' bij_betw bij P P' have "the_inv_into P bij X  P"
        using bij_betwE bij_betw_the_inv_into by blast
      ultimately show "X  (λX. p ` X) ` P" ..
    qed
  next
    show "(λX. p ` X) ` P  P'"
    proof
      fix X'
      assume "X'  (λX. p ` X) ` P"
      from this obtain X where X'_eq: "X' = p ` X" and "X  P" ..
      from X  P have "X  A"
        using assms(2) partition_onD1 by force
      from X  P p' have bij: "bij_betw (p' X) X (bij X)" by auto
      have "p ` X  P'"
      proof -
        from X  P bij_betw bij P P' have "bij X  P'"
          using bij_betwE by blast
        moreover have "(λa. p' (THE X. a  X  X  P) a) ` X = bij X"
        proof
          show "(λa. p' (THE X. a  X  X  P) a) ` X  bij X"
          proof
            fix x'
            assume "x'  (λa. p' (THE X. a  X  X  P) a) ` X"
            from this obtain x where "x  X" and x'_eq: "x' = p' (THE X. x  X  X  P) x" ..
            from X  P x  X have eq_X: "(THE X. x  X  X  P) = X"
              using assms(2) partition_on_the_part_eq by fastforce
            from bij x  X x'_eq eq_X show "x'  bij X"
              using bij_betwE by blast
          qed
        next
          show "bij X  (λa. p' (THE X. a  X  X  P) a) ` X"
          proof
            fix x'
            assume "x'  bij X"
            let ?x = "inv_into X (p' X) x'"
            from x'  bij X bij have "?x  X"
              by (metis  bij_betw_imp_surj_on inv_into_into)
            from this X  P have "(THE X. ?x  X  X  P) = X"
              using assms(2) partition_on_the_part_eq by fastforce
            from this x'  bij X bij have "x' = p' (THE X. ?x  X  X  P) ?x"
              using bij_betw_inv_into_right by fastforce
            moreover from x'  bij X bij have "?x  X"
              by (metis bij_betw_imp_surj_on inv_into_into)
            ultimately show "x'  (λa. p' (THE X. a  X  X  P) a) ` X" ..
          qed
        qed
        ultimately have "(λa. p' (THE X. a  X  X  P) a) ` X  P'" by simp
        have "(λa. p' (THE X. a  X  X  P) a) ` X = (λa. if a  A then p' (THE X. a  X  X  P) a else a) ` X "
          using X  A by (auto intro: image_cong)
        from this show ?thesis
         using (λa. p' (THE X. a  X  X  P) a) ` X  P' unfolding p_def by auto
      qed
      from this X'_eq show "X'  P'" by simp
    qed
  qed
  ultimately show thesis using that by blast
qed

lemma permutes_domain_partition_eq:
  assumes "f  A  B"
  assumes "pA permutes A"
  assumes "b  B"
  shows "pA ` {x  A. f x = b} = {x  A. f (inv pA x) = b}"
proof
  show "pA ` {x  A. f x = b}  {x  A. f (inv pA x) = b}"
    using pA permutes A permutes_in_image permutes_inverses(2) by fastforce
next
  show "{x  A. f (inv pA x) = b}  pA ` {x  A. f x = b}"
  proof
    fix x
    assume "x  {x  A. f (inv pA x) = b}"
    from this have "x  A" "f (inv pA x) = b" by auto
    from x  A have "x = pA (inv pA x)"
      using pA permutes A permutes_inverses(1) by fastforce
    moreover from f (inv pA x) = b x  A have "inv pA x  {x  A. f x = b}"
      by (simp add: pA permutes A permutes_in_image permutes_inv)
    ultimately show "x  pA ` {x  A. f x = b}" ..
  qed
qed

lemma image_domain_partition_eq:
  assumes "f  A E B"
  assumes "pA permutes A"
  shows "(λX. pA ` X) ` ((λb. {x  A. f x = b}) ` B) = (λb. {x  A. f (inv pA x) = b}) ` B"
proof
  from f  A E B have "f  A  B" by auto
  note eq = permutes_domain_partition_eq[OF f  A  B pA permutes A]
  show "(λX. pA ` X) ` (λb. {x  A. f x = b}) ` B  (λb. {x  A. f (inv pA x) = b}) ` B"
  proof
    fix X
    assume "X  (λX. pA ` X) ` (λb. {x  A. f x = b}) ` B"
    from this obtain b where "b  B" and X_eq: "X = pA ` {x  A. f x = b}" by auto
    from this eq have "X = {x  A. f (inv pA x) = b}" by simp
    from this b  B show "X  (λb. {x  A. f (inv pA x) = b}) ` B" ..
  qed
next
  from f  A E B have "f  A  B" by auto
  note eq = permutes_domain_partition_eq[OF f  A  B pA permutes A, symmetric]
  show "(λb. {x  A. f (inv pA x) = b}) ` B  (λX. pA ` X) ` (λb. {x  A. f x = b}) ` B"
  proof
    fix X
    assume "X  (λb. {x  A. f (inv pA x) = b}) ` B"
    from this obtain b where "b  B" and X_eq: "X = {x  A. f (inv pA x) = b}" by auto
    from this eq have "X = pA ` {x  A. f x = b}" by simp
    from this b  B show "X  (λX. pA ` X) ` (λb. {x  A. f x = b}) ` B" by auto
  qed
qed

lemma multiset_of_partition_cards_eq_implies_permutes:
  assumes "finite A" "finite B" "f  A E B" "f'  A E B"
  assumes eq: "image_mset card (mset_set ((λb. {x  A. f x = b}) ` B - {{}})) = image_mset card (mset_set ((λb. {x  A. f' x = b}) ` B - {{}}))"
  obtains pA pB where "pA permutes A" "pB permutes B" "xA. f x = pB (f' (pA x))"
proof -
  have "partition_on A ((λb. {x  A. f x = b}) ` B - {{}})"
    using f  A E B by (auto intro!: partition_onI)
  moreover have "partition_on A ((λb. {x  A. f' x = b}) ` B - {{}})"
    using f'  A E B by (auto intro!: partition_onI)
  moreover note partition_implies_permutes[OF finite A _ _ eq]
  ultimately obtain pA where "pA permutes A" and
    inv_image_eq: "(λb. {x  A. f x = b}) ` B - {{}} =
      (`) pA ` ((λb. {x  A. f' x = b}) ` B - {{}})" by blast
  from pA permutes A have "inj ((`) pA)"
    by (meson injI inj_image_eq_iff permutes_inj)
  have inv_image_eq': "(λb. {x  A. f x = b}) ` B - {{}} = (λb. {x  A. f' (inv pA x) = b}) ` B - {{}}"
  proof -
    note inv_image_eq
    also have "(λX. pA ` X) ` ((λb. {x  A. f' x = b}) ` B - {{}}) = (λb. {x  A. f' (inv pA x) = b}) ` B - {{}}"
      using image_domain_partition_eq[OF f'  A E B pA permutes A]
      by (simp add: image_set_diff[OF inj ((`) pA)])
    finally show ?thesis .
  qed
  from pA permutes A have "inv pA permutes A"
    using permutes_inv by blast
  have "(λx. f' (inv pA x))  A E B"
    using f'  A E B inv pA permutes A permutes_in_image by fastforce
  from f  A E B this finite B obtain pB
    where "pB permutes B" and eq'': "xA. f x = pB (f' (inv pA x))"
    using partitions_eq_implies_permutes[OF _ _ _ inv_image_eq'] by blast
  from inv pA permutes A pB permutes B eq'' that show thesis by blast
qed

subsection ‹Bijections on Same Domain and Range›

subsubsection ‹Existence of Domain Permutation›

lemma obtain_domain_permutation_for_two_bijections:
  assumes "bij_betw f A B" "bij_betw f' A B"
  obtains p where "p permutes A" and "aA. f a = f' (p a)"
proof -
  let ?p = "λa. if a  A then the_inv_into A f' (f a) else a"
  have "?p permutes A"
  proof (rule bij_imp_permutes)
    show "bij_betw ?p A A"
    proof (rule bij_betw_imageI)
      show "inj_on ?p A"
      proof (rule inj_onI)
        fix a a'
        assume "a  A" "a'  A" "?p a = ?p a'"
        from this have "the_inv_into A f' (f a) = the_inv_into A f' (f a')"
          using a  A a'  A by simp
        from this have "f a = f a'"
          using a  A a'  A assms
          by (metis bij_betwE f_the_inv_into_f_bij_betw)
        from this show "a = a'"
          using a  A a'  A assms
          by (metis bij_betw_inv_into_left)
      qed
    next
      show "?p ` A = A"
      proof
        show "?p ` A  A"
        proof
          fix a
          assume "a  ?p ` A"
          from this obtain a' where "a'  A" and "a = the_inv_into A f' (f a')" by auto
          from this assms show "a  A"
            by (metis bij_betwE bij_betw_imp_inj_on bij_betw_imp_surj_on subset_iff the_inv_into_into)
        qed
      next
        show "A  ?p ` A"
        proof
          fix a
          assume "a  A"
          from this assms have "the_inv_into A f (f' a)  A"
            by (meson bij_betwE bij_betw_the_inv_into)
          moreover from  a  A assms have "a = the_inv_into A f' (f (the_inv_into A f (f' a)))"
            by (metis bij_betwE bij_betw_imp_inj_on f_the_inv_into_f_bij_betw the_inv_into_f_eq)
          ultimately show "a  ?p ` A" by auto
        qed
      qed
    qed
  next
    fix a
    assume "a  A"
    from this show "?p a = a" by auto
  qed
  moreover have "aA. f a = f' (?p a)"
    using bij_betw f A B bij_betw f' A B
    using bij_betwE f_the_inv_into_f_bij_betw by fastforce
  moreover note that
  ultimately show thesis by auto
qed

subsubsection ‹Existence of Range Permutation›

lemma obtain_range_permutation_for_two_bijections:
  assumes "bij_betw f A B" "bij_betw f' A B"
  obtains p where "p permutes B" and "aA. f a = p (f' a)"
proof -
  let ?p = "λb. if b  B then f (inv_into A f' b) else b"
  have "?p permutes B"
  proof (rule bij_imp_permutes)
    show "bij_betw ?p B B"
    proof (rule bij_betw_imageI)
      show "inj_on ?p B"
      proof (rule inj_onI)
        fix b b'
        assume "b  B" "b'  B" "?p b = ?p b'"
        from this have "f (inv_into A f' b) = f (inv_into A f' b')"
          using b  B b'  B by simp
        from this have "inv_into A f' b = inv_into A f' b'"
          using b  B b'  B assms
          by (metis bij_betw_imp_surj_on bij_betw_inv_into_left inv_into_into)
        from this show "b = b'"
          using b  B b'  B assms(2)
          by (metis bij_betw_inv_into_right)
      qed
    next
      show "?p ` B = B"
      proof
        from assms show "?p ` B  B"
          by (auto simp add: bij_betwE bij_betw_def inv_into_into)
      next
        show "B  ?p ` B"
        proof
          fix b
          assume "b  B"
          from this assms have "f' (inv_into A f b)  B"
            by (metis bij_betwE bij_betw_imp_surj_on inv_into_into)
          moreover have "b = ?p (f' (inv_into A f b))"
            using assms f' (inv_into A f b)  B b  B
            by (auto simp add: bij_betw_imp_surj_on bij_betw_inv_into_left bij_betw_inv_into_right inv_into_into)
          ultimately show "b  ?p ` B" by auto
        qed
      qed
    qed
  next
    fix b
    assume "b  B"
    from this show "?p b = b" by auto
  qed
  moreover have "aA. f a = ?p (f' a)"
    using bij_betw f' A B bij_betw_inv_into_left bij_betwE by fastforce
  moreover note that
  ultimately show thesis by auto
qed

end