Theory Twelvefold_Way.Twelvefold_Way_Entry4

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

section ‹Functions from A to B, up to a Permutation of A›

theory Twelvefold_Way_Entry4
imports Equiv_Relations_on_Functions
begin

subsection ‹Definition of Bijections›

definition msubset_of :: "'a set ⇒ ('a  ⇒ 'b) set ⇒ 'b multiset"
where
  "msubset_of A F = univ (λf. image_mset f (mset_set A)) F"

definition functions_of :: "'a set ⇒ 'b multiset ⇒ ('a ⇒ 'b) set"
where
  "functions_of A B = {f ∈ A →⇩E set_mset B. image_mset f (mset_set A) = B}"

subsection ‹Properties for Bijections›

lemma msubset_of:
  assumes "F ∈ (A →⇩E B) // domain_permutation A B"
  shows "size (msubset_of A F) = card A"
  and "set_mset (msubset_of A F) ⊆ B"
proof -
  from ‹F ∈ (A →⇩E B) // domain_permutation A B› obtain f where "f ∈ A →⇩E B"
    and F_eq: "F = domain_permutation A B `` {f}" using quotientE by blast
  have "msubset_of A F = univ (λf. image_mset f (mset_set A)) F"
    unfolding msubset_of_def ..
  also have "… = univ (λf. image_mset f (mset_set A)) (domain_permutation A B `` {f})"
    unfolding F_eq ..
  also have "… = image_mset f (mset_set A)"
    using equiv_domain_permutation image_mset_respects_domain_permutation ‹f ∈ A →⇩E B›
    by (subst univ_commute') auto
  finally have msubset_of_eq: "msubset_of A F = image_mset f (mset_set A)" .
  show "size (msubset_of A F) = card A"
  proof -
    have "size (msubset_of A F) = size (image_mset f (mset_set A))"
      unfolding msubset_of_eq ..
    also have "… = card A"
      by (cases ‹finite A›) auto
    finally show ?thesis .
  qed
  show "set_mset (msubset_of A F) ⊆ B"
  proof -
    have "set_mset (msubset_of A F) = set_mset (image_mset f (mset_set A))"
      unfolding msubset_of_eq ..
    also have "… ⊆ B"
      using ‹f ∈ A →⇩E B› by (cases "finite A") auto
    finally show ?thesis .
  qed
qed

lemma functions_of:
  assumes "finite A"
  assumes "set_mset M ⊆ B"
  assumes "size M = card A"
  shows "functions_of A M ∈ (A →⇩E B) // domain_permutation A B"
proof -
  obtain f where "f ∈ A →⇩E set_mset M" and "image_mset f (mset_set A) = M"
    using obtain_function_on_ext_funcset ‹finite A› ‹size M = card A› by blast
  from ‹f ∈ A →⇩E set_mset M› have "f ∈ A →⇩E B"
    using ‹set_mset M ⊆ B› PiE_iff subset_eq by blast
  have "functions_of A M = (domain_permutation A B) `` {f}"
  proof
    show "functions_of A M ⊆ domain_permutation A B `` {f}"
    proof
      fix f'
      assume "f' ∈ functions_of A M"
      from this have "M = image_mset f' (mset_set A)" and "f' ∈ A →⇩E f' ` A"
        using ‹finite A› unfolding functions_of_def by auto
      from this assms(1, 2) have "f' ∈ A →⇩E B"
        by (simp add: PiE_iff image_subset_iff)
      obtain p where "p permutes A ∧ (∀x∈A. f x = f' (p x))"
        using ‹finite A› ‹image_mset f (mset_set A) = M› ‹M = image_mset f' (mset_set A)›
          image_mset_eq_implies_permutes by blast
      from this show "f' ∈ domain_permutation A B `` {f}"
        using ‹f ∈ A →⇩E B› ‹f' ∈ A →⇩E B›
        unfolding domain_permutation_def by auto
    qed
  next
    show "domain_permutation A B `` {f} ⊆ functions_of A M"
    proof
      fix f'
      assume "f' ∈ domain_permutation A B `` {f}"
      from this have "(f, f') ∈ domain_permutation A B" by auto
      from this ‹image_mset f (mset_set A) = M› have "image_mset f' (mset_set A) = M"
        using congruentD[OF image_mset_respects_domain_permutation] by metis
      moreover from this ‹(f, f') ∈ domain_permutation A B› have "f' ∈ A →⇩E set_mset M"
        using ‹finite A› unfolding domain_permutation_def by auto
      ultimately show "f' ∈ functions_of A M"
        unfolding functions_of_def by auto
    qed
  qed
  from this ‹f ∈ A →⇩E B› show ?thesis by (auto intro: quotientI)
qed

lemma functions_of_msubset_of:
  assumes "finite A"
  assumes "F ∈ (A →⇩E B) // domain_permutation A B"
  shows "functions_of A (msubset_of A F) = F"
proof -
  from ‹F ∈ (A →⇩E B) // domain_permutation A B› obtain f where "f ∈ A →⇩E B"
    and F_eq: "F = domain_permutation A B `` {f}" using quotientE by blast
  have "msubset_of A F = univ (λf. image_mset f (mset_set A)) F"
    unfolding msubset_of_def ..
  also have "… = univ (λf. image_mset f (mset_set A)) (domain_permutation A B `` {f})"
    unfolding F_eq ..
  also have "… = image_mset f (mset_set A)"
    using equiv_domain_permutation image_mset_respects_domain_permutation ‹f ∈ A →⇩E B›
    by (subst univ_commute') auto
  finally have msubset_of_eq: "msubset_of A F = image_mset f (mset_set A)" .
  show ?thesis
  proof
    show "functions_of A (msubset_of A F) ⊆ F"
    proof
      fix f'
      assume "f' ∈ functions_of A (msubset_of A F)"
      from this have f': "f' ∈ A →⇩E f ` set_mset (mset_set A)"
      "image_mset f' (mset_set A) = image_mset f (mset_set A)"
        unfolding functions_of_def by (auto simp add: msubset_of_eq)
      from ‹f ∈ A →⇩E B› have "f ` A ⊆ B" by auto
      note ‹f ∈ A →⇩E B›
      moreover from f'(1) ‹finite A› ‹f ` A ⊆ B› have "f' ∈ A →⇩E B" by auto
      moreover obtain p where "p permutes A ∧ (∀x∈A. f x = f' (p x))"
        using ‹finite A› ‹image_mset f' (mset_set A) = image_mset f (mset_set A)›
          by (metis image_mset_eq_implies_permutes)
      ultimately show "f' ∈ F"
        unfolding F_eq domain_permutation_def by auto
    qed
  next
    show "F ⊆ functions_of A (msubset_of A F)"
    proof
      fix f'
      assume "f' ∈ F"
      from this have "f' ∈ A →⇩E B"
        unfolding F_eq domain_permutation_def by auto
      from ‹f' ∈ F› obtain p where "p permutes A ∧ (∀x∈A. f x = f' (p x))"
        unfolding F_eq domain_permutation_def by auto
      from this have eq: "image_mset f' (mset_set A) = image_mset f (mset_set A)"
        using permutes_implies_image_mset_eq by blast
      moreover have "f' ∈ A →⇩E set_mset (image_mset f (mset_set A))"
        using ‹finite A› ‹f' ∈ A →⇩E B› eq[symmetric] by auto
      ultimately show "f' ∈ functions_of A (msubset_of A F)"
        unfolding functions_of_def msubset_of_eq by auto
    qed
  qed
qed

lemma msubset_of_functions_of:
  assumes "set_mset M ⊆ B" "size M = card A" "finite A"
  shows "msubset_of A (functions_of A M) = M"
proof -
  from assms have "functions_of A M ∈ (A →⇩E B) // domain_permutation A B"
    using functions_of by fastforce
  from this obtain f where "f ∈ A →⇩E B" and "functions_of A M = domain_permutation A B `` {f}"
    by (rule quotientE)
  from this have "f ∈ functions_of A M"
    using equiv_domain_permutation equiv_class_self by fastforce
  have "msubset_of A (functions_of A M) = univ (λf. image_mset f (mset_set A)) (functions_of A M)"
    unfolding msubset_of_def ..
  also have "… = univ (λf. image_mset f (mset_set A)) (domain_permutation A B `` {f})"
    unfolding ‹functions_of A M = domain_permutation A B `` {f}› ..
  also have "… = image_mset f (mset_set A)"
    using equiv_domain_permutation image_mset_respects_domain_permutation ‹f ∈ A →⇩E B›
    by (subst univ_commute') auto
  also have "image_mset f (mset_set A) = M"
    using ‹f ∈ functions_of A M› unfolding functions_of_def by simp
  finally show ?thesis .
qed

subsection ‹Bijections›

lemma bij_betw_msubset_of:
  assumes "finite A"
  shows "bij_betw (msubset_of A) ((A →⇩E B) // domain_permutation A B) {M. set_mset M ⊆ B ∧ size M = card A}"
proof (rule bij_betw_byWitness[where f'="λM. functions_of A M"])
  show "∀F∈(A →⇩E B) // domain_permutation A B. functions_of A (msubset_of A F) = F"
    using ‹finite A› by (auto simp add: functions_of_msubset_of)
  show "∀M∈{M. set_mset M ⊆ B ∧ size M = card A}. msubset_of A (functions_of A M) = M"
    using ‹finite A› by (auto simp add: msubset_of_functions_of)
  show "msubset_of A ` ((A →⇩E B) // domain_permutation A B) ⊆ {M. set_mset M ⊆ B ∧ size M = card A}"
    using msubset_of by blast
  show "functions_of A ` {M. set_mset M ⊆ B ∧ size M = card A} ⊆ (A →⇩E B) // domain_permutation A B"
    using functions_of ‹finite A› by blast
qed

subsection ‹Cardinality›

lemma
  assumes "finite A" "finite B"
  shows "card ((A →⇩E B) // domain_permutation A B) = card B + card A - 1 choose card A"
proof -
  have "bij_betw (msubset_of A) ((A →⇩E B) // domain_permutation A B) {M. set_mset M ⊆ B ∧ size M = card A}"
    using ‹finite A› by (rule bij_betw_msubset_of)
  from this have "card ((A →⇩E B) // domain_permutation A B) = card {M. set_mset M ⊆ B ∧ size M = card A}"
    by (rule bij_betw_same_card)
  also have "card {M. set_mset M ⊆ B ∧ size M = card A} = card B + card A - 1 choose card A"
    using ‹finite B› by (rule card_multisets)
  finally show ?thesis .
qed

end