Theory Twelvefold_Way_Entry6

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

section ‹Surjections from A to B up to a Permutation on A›

theory Twelvefold_Way_Entry6
imports Twelvefold_Way_Entry4
begin

subsection ‹Properties for Bijections›

lemma set_mset_eq_implies_surj_on:
  assumes "finite A"
  assumes "size M = card A" "set_mset M = B"
  assumes "f ∈ functions_of A M"
  shows   "f ` A = B"
proof -
  from ‹f ∈ functions_of A M› have "image_mset f (mset_set A) = M"
    unfolding functions_of_def by auto
  from ‹image_mset f (mset_set A) = M› show "f ` A = B"
    using ‹set_mset M = B› ‹finite A› finite_set_mset_mset_set set_image_mset by force
qed

lemma surj_on_implies_set_mset_eq:
  assumes "finite A"
  assumes "F ∈ (A →⇩E B) // domain_permutation A B"
  assumes "univ (λf. f ` A = B) F"
  shows "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 eq: "msubset_of A F = image_mset f (mset_set A)" .
  from iffD1[OF univ_commute', OF equiv_domain_permutation, OF surjective_respects_domain_permutation, OF ‹f ∈ A →⇩E B›]
    ‹univ (λf. f ` A = B) F› have "f ` A = B" by (simp add: F_eq)
  have "set_mset (image_mset f (mset_set A)) = B"
  proof
    show "set_mset (image_mset f (mset_set A)) ⊆ B"
      using ‹finite A› ‹f ` A = B› by auto
  next
    show "B ⊆ set_mset (image_mset f (mset_set A))"
      using ‹finite A› by (simp add: ‹f ` A = B›[symmetric] in_image_mset)
  qed
  from this show "set_mset (msubset_of A F) = B"
    unfolding eq .
qed

lemma functions_of_is_surj_on:
  assumes "finite A"
  assumes "size M = card A" "set_mset M = B"
  shows "univ (λf. f ` A = B) (functions_of A M)"
proof -
  have "functions_of A M ∈ (A →⇩E B) // domain_permutation A B"
    using functions_of ‹finite A› ‹size M = card A› ‹set_mset M = B›  by fastforce
  from this obtain f where eq_f: "functions_of A M = domain_permutation A B `` {f}" and "f ∈ A →⇩E B"
    using quotientE by blast
  from eq_f have "f ∈ functions_of A M"
    using ‹f ∈ A →⇩E B› equiv_domain_permutation equiv_class_self by fastforce
  have "f ` A = B"
    using ‹f ∈ functions_of A M› assms set_mset_eq_implies_surj_on by fastforce
  from this show ?thesis
    unfolding eq_f using equiv_domain_permutation surjective_respects_domain_permutation ‹f ∈ A →⇩E B›
    by (subst univ_commute') assumption+
qed

subsection ‹Bijections›

lemma bij_betw_msubset_of:
  assumes "finite A"
  shows "bij_betw (msubset_of A) ({f ∈ A →⇩E B. f ` A = B} // domain_permutation A B)
    {M. set_mset M = B ∧ size M = card A}"
    (is "bij_betw _ ?FSet ?MSet")
proof (rule bij_betw_byWitness[where f'="λM. functions_of A M"])
  have quotient_eq: "?FSet = {F ∈ ((A →⇩E B) // domain_permutation A B). univ (λf. f ` A = B) F}"
    using equiv_domain_permutation[of A B] surjective_respects_domain_permutation[of A B]
    by (simp only: univ_preserves_predicate)
  show "∀f∈?FSet. functions_of A (msubset_of A f) = f"
    using ‹finite A› by (auto simp only: quotient_eq functions_of_msubset_of)
  show "∀M∈?MSet. msubset_of A (functions_of A M) = M"
    using ‹finite A› msubset_of_functions_of by blast
  show "msubset_of A ` ?FSet ⊆ ?MSet"
    using ‹finite A› by (auto simp add: quotient_eq surj_on_implies_set_mset_eq msubset_of)
  show "functions_of A ` ?MSet ⊆ ?FSet"
    using ‹finite A› by (auto simp add: quotient_eq intro: functions_of functions_of_is_surj_on)
qed

subsection ‹Cardinality›

lemma card_surjective_functions_domain_permutation:
  assumes "finite A" "finite B"
  assumes "card B ≤ card A"
  shows "card ({f ∈ A →⇩E B. f ` A = B} // domain_permutation A B) = (card A - 1) choose (card A - card B)"
proof -
  let ?FSet = "{f ∈ A →⇩E B. f ` A = B} // domain_permutation A B"
  and ?MSet = "{M. set_mset M = B ∧ size M = card A}"
  have "bij_betw (msubset_of A) ?FSet ?MSet"
    using ‹finite A› by (rule bij_betw_msubset_of)
  from this have "card ?FSet = card ?MSet"
    by (rule bij_betw_same_card)
  also have "card ?MSet = (card A - 1) choose (card A - card B)"
    using ‹finite B› ‹card B ≤ card A› by (rule card_multisets_covering_set)
  finally show ?thesis .
qed

end