Theory Twelvefold_Way_Entry10

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

section ‹Functions from A to B up to a Permutation on A and B›

theory Twelvefold_Way_Entry10
imports Equiv_Relations_on_Functions
begin

subsection ‹Definition of Bijections›

definition number_partition_of :: "'a set ⇒ 'b set ⇒ ('a ⇒ 'b) set ⇒ nat multiset"
where
  "number_partition_of A B F = univ (λf. image_mset (λX. card X) (mset_set ((λb. {x ∈ A. f x = b}) ` B - {{}}))) F"

definition functions_of :: "'a set ⇒ 'b set ⇒ nat multiset ⇒ ('a ⇒ 'b) set"
where
  "functions_of A B N = {f ∈ A →E B. image_mset (λX. card X) (mset_set ((λb. {x ∈ A. f x = b}) ` B - {{}})) = N}"

subsection ‹Properties for Bijections›

lemma card_setsum_partition:
  assumes "finite A" "finite B" "f ∈ A →E B"
  shows "sum card ((λb. {x ∈ A. f x = b}) ` B - {{}}) = card A"
proof -
  have "finite ((λb. {x ∈ A. f x = b}) ` B - {{}})"
    using ‹finite B› by blast
  moreover have "∀X∈(λb. {x ∈ A. f x = b}) ` B - {{}}. finite X"
    using ‹finite A› by auto
  moreover have "⋃((λb. {x ∈ A. f x = b}) ` B - {{}}) = A"
    using ‹f ∈ A →E B› by auto
  ultimately show ?thesis
    by (subst card_Union_disjoint[symmetric]) (auto simp: pairwise_def disjnt_def)
qed

lemma number_partition_of:
  assumes "finite A" "finite B"
  assumes "F ∈ (A →E B) // domain_and_range_permutation A B"
  shows "number_partition (card A) (number_partition_of A B F)"
  and "size (number_partition_of A B F) ≤ card B"
proof -
  from ‹F ∈ (A →E B) // domain_and_range_permutation A B› obtain f where "f ∈ A →E B"
    and F_eq: "F = domain_and_range_permutation A B `` {f}" using quotientE by blast
  have number_partition_of_eq: "number_partition_of A B F = image_mset card (mset_set ((λb. {x ∈ A. f x = b}) ` B - {{}}))"
  proof -
    have "number_partition_of A B F = univ (λf. image_mset card (mset_set ((λb. {x ∈ A. f x = b}) ` B - {{}}))) F"
      unfolding number_partition_of_def ..
    also have "… = univ (λf. image_mset card (mset_set ((λb. {x ∈ A. f x = b}) ` B - {{}}))) (domain_and_range_permutation A B `` {f})"
      unfolding F_eq ..
    also have "… = image_mset card (mset_set ((λb. {x ∈ A. f x = b}) ` B - {{}}))"
      using ‹finite B› equiv_domain_and_range_permutation multiset_of_partition_cards_respects_domain_and_range_permutation ‹f ∈ A →E B›
      by (subst univ_commute') auto
    finally show ?thesis .
  qed
  show "number_partition (card A) (number_partition_of A B F)"
  proof -
    have "sum_mset (number_partition_of A B F) = card A"
      using number_partition_of_eq ‹finite A› ‹finite B› ‹f ∈ A →E B›
      by (simp only: sum_unfold_sum_mset[symmetric] card_setsum_partition)
    moreover have "0 ∉# number_partition_of A B F"
    proof -
      have "∀X ∈ (λb. {x ∈ A. f x = b}) ` B. finite X"
        using ‹finite A› by simp
      from this have "∀X ∈ (λb. {x ∈ A. f x = b}) ` B - {{}}. card X ≠ 0" by auto
      from this show ?thesis
        using number_partition_of_eq ‹finite B› by (simp add: image_iff)
    qed
    ultimately show ?thesis unfolding number_partition_def by simp
  qed
  show "size (number_partition_of A B F) ≤ card B"
    using number_partition_of_eq ‹finite A› ‹finite B›
    by (metis (no_types, lifting) card_Diff1_le card_image_le finite_imageI le_trans size_image_mset size_mset_set)
qed

lemma functions_of:
  assumes "finite A" "finite B"
  assumes "number_partition (card A) N"
  assumes "size N ≤ card B"
  shows "functions_of A B N ∈ (A →E B) // domain_and_range_permutation A B"
proof -
  obtain f where "f ∈ A →E B" and eq_N: "image_mset (λX. card X) (mset_set (((λb. {x ∈ A. f x = b})) ` B - {{}})) = N"
    using obtain_extensional_function_from_number_partition ‹finite A› ‹finite B› ‹number_partition (card A) N› ‹size N ≤ card B› by blast
  have "functions_of A B N = (domain_and_range_permutation A B) `` {f}"
  proof
    show "functions_of A B N ⊆ domain_and_range_permutation A B `` {f}"
    proof
      fix f'
      assume "f' ∈ functions_of A B N"
      from this have eq_N': "N = image_mset (λX. card X) (mset_set (((λb. {x ∈ A. f' x = b})) ` B - {{}}))"
        and "f' ∈ A →E B"
        unfolding functions_of_def by auto
      from ‹finite A› ‹finite B› ‹f ∈ A →E B› ‹f' ∈ A →E B›
      obtain pA pB where "pA permutes A" "pB permutes B" "∀x∈A. f x = pB (f' (pA x))"
        using eq_N eq_N' multiset_of_partition_cards_eq_implies_permutes[of A B f f'] by blast
      from this show "f' ∈ domain_and_range_permutation A B `` {f}"
        using ‹f ∈ A →E B› ‹f' ∈ A →E B›
        unfolding domain_and_range_permutation_def by auto
    qed
  next
    show "domain_and_range_permutation A B `` {f} ⊆ functions_of A B N"
    proof
      fix f'
      assume "f' ∈ domain_and_range_permutation A B `` {f}"
      from this have in_equiv_relation: "(f, f') ∈ domain_and_range_permutation A B" by auto
      from eq_N ‹finite B› have "image_mset (λX. card X) (mset_set (((λb. {x ∈ A. f' x = b})) ` B - {{}})) = N"
        using congruentD[OF multiset_of_partition_cards_respects_domain_and_range_permutation in_equiv_relation]
        by metis
      moreover from ‹(f, f') ∈ domain_and_range_permutation A B› have "f' ∈ A →E B"
        unfolding domain_and_range_permutation_def by auto
      ultimately show "f' ∈ functions_of A B N"
        unfolding functions_of_def by auto
    qed
  qed
  from this ‹f ∈ A →E B› show ?thesis by (auto intro: quotientI)
qed

lemma functions_of_number_partition_of:
  assumes "finite A" "finite B"
  assumes "F ∈ (A →E B) // domain_and_range_permutation A B"
  shows "functions_of A B (number_partition_of A B F) = F"
proof -
  from ‹F ∈ (A →E B) // domain_and_range_permutation A B› obtain f where "f ∈ A →E B"
    and F_eq: "F = domain_and_range_permutation A B `` {f}" using quotientE by blast
  have "number_partition_of A B F = univ (λf. image_mset card (mset_set ((λb. {x ∈ A. f x = b}) ` B - {{}}))) F"
    unfolding number_partition_of_def ..
  also have "… = univ (λf. image_mset card (mset_set ((λb. {x ∈ A. f x = b}) ` B - {{}}))) (domain_and_range_permutation A B `` {f})"
    unfolding F_eq ..
  also have "… = image_mset card (mset_set ((λb. {x ∈ A. f x = b}) ` B - {{}}))"
    using ‹finite B›
    using equiv_domain_and_range_permutation multiset_of_partition_cards_respects_domain_and_range_permutation ‹f ∈ A →E B›
    by (subst univ_commute') auto
  finally have number_partition_of_eq: "number_partition_of A B F = image_mset card (mset_set ((λb. {x ∈ A. f x = b}) ` B - {{}}))" .
  show ?thesis
  proof
    show "functions_of A B (number_partition_of A B F) ⊆ F"
    proof
      fix f'
      assume "f' ∈ functions_of A B (number_partition_of A B F)"
      from this have "f' ∈ A →E B"
        and 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 - {{}}))"
        unfolding functions_of_def by (auto simp add: number_partition_of_eq)
      note ‹f ∈ A →E B› ‹f' ∈ A →E B›
      moreover obtain pA pB where "pA permutes A" "pB permutes B" "∀x∈A. f x = pB (f' (pA x))"
        using ‹finite A› ‹finite B› ‹f ∈ A →E B› ‹f' ∈ A →E B› eq
          multiset_of_partition_cards_eq_implies_permutes[of A B f f']
        by metis
      ultimately show "f' ∈ F"
        unfolding F_eq domain_and_range_permutation_def by auto
    qed
  next
    show "F ⊆ functions_of A B (number_partition_of A B F)"
    proof
      fix f'
      assume "f' ∈ F"
      from ‹f' ∈ F› obtain pA pB where "pA permutes A" "pB permutes B" "∀x∈A. f x = pB (f' (pA x))"
        unfolding F_eq domain_and_range_permutation_def by auto
      have 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 - {{}}))"
      proof -
        have "(λb. {x ∈ A. f x = b}) ` B = (λb. {x ∈ A. pB (f' (pA x)) = b}) ` B"
          using ‹∀x∈A. f x = pB (f' (pA 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. pB (f' (pA x)) = b}) ` B - {{}}))" by simp
        also have "… = image_mset card (mset_set ((λb. {x ∈ A. f' x = b}) ` B - {{}}))"
          using ‹pA permutes A› ‹pB permutes B› permutes_implies_multiset_of_partition_cards_eq by blast
        finally show ?thesis .
      qed
      moreover from ‹f' ∈ F› have "f' ∈ A →E B"
        unfolding F_eq domain_and_range_permutation_def by auto
      ultimately show "f' ∈ functions_of A B (number_partition_of A B F)"
        unfolding functions_of_def number_partition_of_eq by auto
    qed
  qed
qed

lemma number_partition_of_functions_of:
  assumes "finite A" "finite B"
  assumes "number_partition (card A) N" "size N ≤ card B"
  shows "number_partition_of A B (functions_of A B N) = N"
proof -
  from assms have "functions_of A B N ∈ (A →E B) // domain_and_range_permutation A B"
    using functions_of assms by fastforce
  from this obtain f where "f ∈ A →E B" and "functions_of A B N = domain_and_range_permutation A B `` {f}"
    by (meson quotientE)
  from this have "f ∈ functions_of A B N"
    using equiv_domain_and_range_permutation equiv_class_self by fastforce
  have "number_partition_of A B (functions_of A B N) = univ (λf. image_mset card (mset_set ((λb. {x ∈ A. f x = b}) ` B - {{}}))) (functions_of A B N)"
    unfolding number_partition_of_def ..
  also have "… = univ (λf.  image_mset card (mset_set ((λb. {x ∈ A. f x = b}) ` B - {{}}))) (domain_and_range_permutation A B `` {f})"
    unfolding ‹functions_of A B N = domain_and_range_permutation A B `` {f}› ..
  also have "… = image_mset card (mset_set ((λb. {x ∈ A. f x = b}) ` B - {{}}))"
    using ‹finite B› ‹f ∈ A →E B› equiv_domain_and_range_permutation
      multiset_of_partition_cards_respects_domain_and_range_permutation
    by (subst univ_commute') auto
  also have "image_mset card (mset_set ((λb. {x ∈ A. f x = b}) ` B - {{}})) = N"
    using ‹f ∈ functions_of A B N› unfolding functions_of_def by simp
  finally show ?thesis .
qed

subsection ‹Bijections›

lemma bij_betw_number_partition_of:
  assumes "finite A" "finite B"
  shows "bij_betw (number_partition_of A B) ((A →E B) // domain_and_range_permutation A B) {N. number_partition (card A) N ∧ size N ≤ card B}"
proof (rule bij_betw_byWitness[where f'="λM. functions_of A B M"])
  show "∀F∈(A →E B) // domain_and_range_permutation A B. functions_of A B (number_partition_of A B F) = F"
    using ‹finite A› ‹finite B› by (auto simp add: functions_of_number_partition_of)
  show "∀N∈{N. number_partition (card A) N ∧ size N ≤ card B}. number_partition_of A B (functions_of A B N) = N"
    using ‹finite A› ‹finite B› by (auto simp add: number_partition_of_functions_of)
  show "number_partition_of A B ` ((A →E B) // domain_and_range_permutation A B) ⊆ {N. number_partition (card A) N ∧ size N ≤ card B}"
    using number_partition_of[of A B] ‹finite A› ‹finite B› by auto
  show "functions_of A B ` {N. number_partition (card A) N ∧ size N ≤ card B} ⊆ (A →E B) // domain_and_range_permutation A B"
    using functions_of ‹finite A› ‹finite B› by blast
qed

subsection ‹Cardinality›

lemma card_domain_and_range_permutation:
  assumes "finite A" "finite B"
  shows "card ((A →E B) // domain_and_range_permutation A B) = Partition (card A + card B) (card B)"
proof -
  have "bij_betw (number_partition_of A B) ((A →E B) // domain_and_range_permutation A B) {N. number_partition (card A) N ∧ size N ≤ card B}"
    using ‹finite A› ‹finite B› by (rule bij_betw_number_partition_of)
  from this have "card ((A →E B) // domain_and_range_permutation A B) = card {N. number_partition (card A) N ∧ size N ≤ card B}"
    by (rule bij_betw_same_card)
  also have "card {N. number_partition (card A) N ∧ size N ≤ card B} = Partition (card A + card B) (card B)"
    by (rule card_number_partitions_with_atmost_k_parts)
  finally show ?thesis .
qed

end