Theory Twelvefold_Way.Twelvefold_Way_Entry5

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

section ‹Injections from A to B up to a Permutation of A›

theory Twelvefold_Way_Entry5
imports
  Equiv_Relations_on_Functions
begin

subsection ‹Definition of Bijections›

definition subset_of :: "'a set ⇒ ('a  ⇒ 'b) set ⇒ 'b set"
where
  "subset_of A F = univ (λf. f ` A) F"

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

subsection ‹Properties for Bijections›

lemma functions_of_eq:
  assumes "finite A"
  assumes "f ∈ {f ∈ A →⇩E B. inj_on f A}"
  shows "functions_of A (f ` A) = domain_permutation A B `` {f}"
proof
  have bij: "bij_betw f A (f ` A)"
    using assms by (simp add: bij_betw_imageI)
  show "functions_of A (f ` A) ⊆ domain_permutation A B `` {f}"
  proof
    fix f'
    assume "f' ∈ functions_of A (f ` A)"
    from this have "f' ∈ A →⇩E f ` A" and "f' ` A = f ` A"
      unfolding functions_of_def by auto
    from this assms have "f' ∈ A →⇩E B" and "inj_on f A"
      using PiE_mem by fastforce+
    moreover have "∃p. p permutes A ∧ (∀x∈A. f x = f' (p x))"
    proof
      let ?p = "λx. if x ∈ A then inv_into A f' (f x) else x"
      show "?p permutes A ∧ (∀x∈A. f x = f' (?p x))"
      proof
        show "?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 "inv_into A f' (f a) = inv_into A f' (f a')" by auto
              from this ‹a ∈ A› ‹a' ∈ A› ‹f' ` A = f ` A› have "f a = f a'"
                using inv_into_injective by fastforce
              from this ‹a ∈ A› ‹a' ∈ A› show "a = a'"
                by (metis bij bij_betw_inv_into_left)
            qed
          next
            show "?p ` A = A"
            proof
              show "?p ` A ⊆ A"
                using ‹f' ` A = f ` A› by (simp add: image_subsetI inv_into_into)
            next
              show "A ⊆ ?p ` A"
              proof
                fix a
                assume "a ∈ A"
                have "inj_on f' A"
                  using ‹finite A› ‹f' ` A = f ` A› ‹inj_on f A›
                  by (simp add: card_image eq_card_imp_inj_on)
                from ‹a ∈ A› ‹f' ` A = f ` A› have "inv_into A f (f' a) ∈ A"
                  by (metis image_eqI inv_into_into)
                moreover have "a = inv_into A f' (f (inv_into A f (f' a)))"
                  using ‹a ∈ A› ‹f' ` A = f ` A› ‹inj_on f' A›
                  by (metis f_inv_into_f image_eqI inv_into_f_f)
                ultimately show "a ∈ ?p ` A" by auto
              qed
            qed
          qed
        next
          fix x
          assume "x ∉ A"
          from this show "?p x = x" by simp
        qed
      next
        from ‹f' ` A = f ` A› show "∀x∈A. f x = f' (?p x)"
          by (simp add: f_inv_into_f)
      qed
    qed
    moreover have "f ∈ A →⇩E B" using assms by auto
    ultimately show "f' ∈ domain_permutation A B `` {f}"
      unfolding domain_permutation_def by auto
  qed
next
  show "domain_permutation A B `` {f} ⊆ functions_of A (f ` A)"
  proof
    fix f'
    assume "f' ∈ domain_permutation A B `` {f}"
    from this obtain p where p: "p permutes A" "∀x∈A. f x = f' (p x)"
      and "f ∈ A →⇩E B" "f' ∈ A →⇩E B"
      unfolding domain_permutation_def by auto
    have "f' ` A = f ` A"
    proof
      show "f' ` A ⊆ f ` A"
      proof
        fix x
        assume "x ∈ f' ` A"
        from this obtain x' where "x = f' x'" and "x' ∈ A" ..
        from this have "x = f (inv p x')"
          using p by (metis (mono_tags, lifting) permutes_in_image permutes_inverses(1))
        moreover have "inv p x' ∈ A"
          using p ‹x' ∈ A› by (simp add: permutes_in_image permutes_inv)
        ultimately show "x ∈ f ` A" ..
      qed
    next
      show "f ` A ⊆ f' ` A"
        using p permutes_in_image by fastforce
    qed
    moreover from this ‹f' ∈ A →⇩E B› have "f' ∈ A →⇩E f ` A" by auto
    ultimately show "f' ∈ functions_of A (f ` A)"
      unfolding functions_of_def by auto
  qed
qed

lemma subset_of:
  assumes "F ∈ {f ∈ A →⇩E B. inj_on f A} // domain_permutation A B"
  shows "subset_of A F ⊆ B" and "card (subset_of A F) = card A"
proof -
  from assms obtain f where F_eq: "F = (domain_permutation A B) `` {f}"
    and f: "f ∈ A →⇩E B" "inj_on f A"
    using mem_Collect_eq quotientE by force
  from this have "subset_of A (domain_permutation A B `` {f}) = f ` A"
    using equiv_domain_permutation image_respects_domain_permutation
    unfolding subset_of_def by (intro univ_commute') auto
  from this f F_eq show "subset_of A F ⊆ B" and "card (subset_of A F) = card A"
    by (auto simp add: card_image)
qed

lemma functions_of:
  assumes "finite A" "finite B" "X ⊆ B" "card X = card A"
  shows "functions_of A X ∈ {f ∈ A →⇩E B. inj_on f A} // domain_permutation A B"
proof -
  from assms obtain f where f: "f ∈ A →⇩E X ∧ bij_betw f A X"
    using ‹finite A› ‹finite B› by (metis finite_same_card_bij_on_ext_funcset finite_subset)
  from this have "X = f ` A" by (simp add: bij_betw_def)
  from f ‹X ⊆ B› have "f ∈ {f ∈ A →⇩E B. inj_on f A}"
    by (auto simp add: bij_betw_imp_inj_on)
  have "functions_of A X = domain_permutation A B `` {f}"
    using ‹finite A› ‹X = f ` A› ‹f ∈ {f ∈ A →⇩E B. inj_on f A}›
    by (simp add: functions_of_eq)
  from this show "functions_of A X ∈ {f ∈ A →⇩E B. inj_on f A} // domain_permutation A B"
    using ‹f ∈ {f ∈ A →⇩E B. inj_on f A}› by (auto intro: quotientI)
qed

lemma subset_of_functions_of:
  assumes "finite A" "finite X" "card A = card X"
  shows "subset_of A (functions_of A X) = X"
proof -
  from assms obtain f where "f ∈ A →⇩E X" and "bij_betw f A X"
    using finite_same_card_bij_on_ext_funcset by blast
  from this have subset_of: "subset_of A (domain_permutation A X `` {f}) = f ` A"
    using equiv_domain_permutation image_respects_domain_permutation
    unfolding subset_of_def by (intro univ_commute') auto
  from ‹bij_betw f A X› have "inj_on f A" and "f ` A = X"
    by (auto simp add: bij_betw_def)
  have "subset_of A (functions_of A X) = subset_of A (functions_of A (f ` A))"
    using ‹f ` A = X› by simp
  also have "… = subset_of A (domain_permutation A X `` {f})"
    using ‹finite A› ‹inj_on f A› ‹f ∈ A →⇩E X› by (auto simp add: functions_of_eq)
  also have "… = f ` A"
    using ‹inj_on f A› ‹f ∈ A →⇩E X› by (simp add: subset_of)
  also have "… = X"
    using ‹f ` A = X› by simp
  finally show ?thesis .
qed

lemma functions_of_subset_of:
  assumes "finite A"
  assumes "F ∈ {f ∈ A →⇩E B. inj_on f A} // domain_permutation A B"
  shows "functions_of A (subset_of A F) = F"
using assms(2) proof (rule quotientE)
  fix f
  assume f: "f ∈ {f ∈ A →⇩E B. inj_on f A}"
    and F_eq: "F = domain_permutation A B `` {f}"
  from this have "subset_of A (domain_permutation A B `` {f}) = f ` A"
    using equiv_domain_permutation image_respects_domain_permutation
    unfolding subset_of_def by (intro univ_commute') auto
  from this f F_eq ‹finite A› show "functions_of A (subset_of A F) = F"
    by (simp add: functions_of_eq)
qed

subsection ‹Bijections›

lemma bij_betw_subset_of:
  assumes "finite A" "finite B"
  shows "bij_betw (subset_of A) ({f ∈ A →⇩E B. inj_on f A} // domain_permutation A B) {X. X ⊆ B ∧ card X = card A}"
proof (rule bij_betw_byWitness[where f'="functions_of A"])
  show "∀F∈{f ∈ A →⇩E B. inj_on f A} // domain_permutation A B. functions_of A (subset_of A F) = F"
    using ‹finite A› functions_of_subset_of by auto
  show "∀X∈{X. X ⊆ B ∧ card X = card A}. subset_of A (functions_of A X) = X"
    using subset_of_functions_of ‹finite A› ‹finite B›
    by (metis (mono_tags) finite_subset mem_Collect_eq)
  show "subset_of A ` ({f ∈ A →⇩E B. inj_on f A} // domain_permutation A B) ⊆ {X. X ⊆ B ∧ card X = card A}"
    using subset_of by fastforce
  show "functions_of A ` {X. X ⊆ B ∧ card X = card A} ⊆ {f ∈ A →⇩E B. inj_on f A} // domain_permutation A B"
    using ‹finite A› ‹finite B› functions_of by auto
qed

lemma bij_betw_functions_of:
  assumes "finite A" "finite B"
  shows "bij_betw (functions_of A) {X. X ⊆ B ∧ card X = card A} ({f ∈ A →⇩E B. inj_on f A} // domain_permutation A B)"
proof (rule bij_betw_byWitness[where f'="subset_of A"])
  show "∀F∈{f ∈ A →⇩E B. inj_on f A} // domain_permutation A B. functions_of A (subset_of A F) = F"
    using ‹finite A› functions_of_subset_of by auto
  show "∀X∈{X. X ⊆ B ∧ card X = card A}. subset_of A (functions_of A X) = X"
    using subset_of_functions_of ‹finite A› ‹finite B›
    by (metis (mono_tags) finite_subset mem_Collect_eq)
  show "subset_of A ` ({f ∈ A →⇩E B. inj_on f A} // domain_permutation A B) ⊆ {X. X ⊆ B ∧ card X = card A}"
    using subset_of by fastforce
  show "functions_of A ` {X. X ⊆ B ∧ card X = card A} ⊆ {f ∈ A →⇩E B. inj_on f A} // domain_permutation A B"
    using ‹finite A› ‹finite B› functions_of by auto
qed

lemma bij_betw_mset_set:
  shows "bij_betw mset_set {A. finite A} {M. ∀x. count M x ≤ 1}"
proof (rule bij_betw_byWitness[where f'="set_mset"])
  show "∀A∈{A. finite A}. set_mset (mset_set A) = A" by auto
  show "∀M∈{M. ∀x. count M x ≤ 1}. mset_set (set_mset M) = M"
    by (auto simp add: mset_set_set_mset')
  show "mset_set ` {A. finite A} ⊆ {M. ∀x. count M x ≤ 1}"
    using nat_le_linear by fastforce
  show "set_mset ` {M. ∀x. count M x ≤ 1} ⊆ {A. finite A}" by auto
qed

lemma bij_betw_mset_set_card:
  assumes "finite A"
  shows "bij_betw mset_set {X. X ⊆ A ∧ card X = k} {M. M ⊆# mset_set A ∧ size M = k}"
proof (rule bij_betw_byWitness[where f'="set_mset"])
  show "∀X∈{X. X ⊆ A ∧ card X = k}. set_mset (mset_set X) = X"
    using ‹finite A› rev_finite_subset[of A] by auto
  show "∀M∈{M. M ⊆# mset_set A ∧ size M = k}. mset_set (set_mset M) = M"
    by (auto simp add: mset_set_set_mset)
  show "mset_set ` {X. X ⊆ A ∧ card X = k} ⊆ {M. M ⊆# mset_set A ∧ size M = k}"
    using ‹finite A› rev_finite_subset[of A]
    by (auto simp add: mset_set_subseteq_mset_set)
  show "set_mset ` {M. M ⊆# mset_set A ∧ size M = k} ⊆ {X. X ⊆ A ∧ card X = k}"
    using assms mset_subset_eqD card_set_mset by fastforce
qed

lemma bij_betw_mset_set_card':
  assumes "finite A"
  shows "bij_betw mset_set {X. X ⊆ A ∧ card X = k} {M. set_mset M ⊆ A ∧ size M = k ∧ (∀x. count M x ≤ 1)}"
proof (rule bij_betw_byWitness[where f'="set_mset"])
  show "∀X∈{X. X ⊆ A ∧ card X = k}. set_mset (mset_set X) = X"
    using ‹finite A› rev_finite_subset[of A] by auto
  show "∀M∈{M. set_mset M ⊆ A ∧ size M = k ∧ (∀x. count M x ≤ 1)}. mset_set (set_mset M) = M"
    by (auto simp add: mset_set_set_mset')
  show "mset_set ` {X. X ⊆ A ∧ card X = k} ⊆ {M. set_mset M ⊆ A ∧ size M = k ∧ (∀x. count M x ≤ 1)}"
    using ‹finite A› rev_finite_subset[of A] by (auto simp add: count_mset_set_leq')
  show "set_mset ` {M. set_mset M ⊆ A ∧ size M = k ∧ (∀x. count M x ≤ 1)} ⊆ {X. X ⊆ A ∧ card X = k}"
    by (auto simp add: card_set_mset')
qed

subsection ‹Cardinality›

lemma card_injective_functions_domain_permutation:
  assumes "finite A" "finite B"
  shows "card ({f ∈ A →⇩E B. inj_on f A} // domain_permutation A B) = card B choose card A"
proof -
  have "bij_betw (subset_of A) ({f ∈ A →⇩E B. inj_on f A} // domain_permutation A B) {X. X ⊆ B ∧ card X = card A}"
    using ‹finite A› ‹finite B› by (rule bij_betw_subset_of)
  from this have "card ({f ∈ A →⇩E B. inj_on f A} // domain_permutation A B) = card {X. X ⊆ B ∧ card X = card A}"
    by (rule bij_betw_same_card)
  also have "card {X. X ⊆ B ∧ card X = card A} = card B choose card A"
    using ‹finite B› by (rule n_subsets)
  finally show ?thesis .
qed

lemma card_multiset_only_sets:
  assumes "finite A"
  shows "card {M. M ⊆# mset_set A ∧ size M = k} = card A choose k"
proof -
  have "bij_betw mset_set {X. X ⊆ A ∧ card X = k} {M. M ⊆# mset_set A ∧ size M = k}"
    using ‹finite A› by (rule bij_betw_mset_set_card)
  from this have "card {M. M ⊆# mset_set A ∧ size M = k} = card {X. X ⊆ A ∧ card X = k}"
    by (simp add: bij_betw_same_card)
  also have " card {X. X ⊆ A ∧ card X = k} = card A choose k"
    using ‹finite A› by (rule n_subsets)
  finally show ?thesis .
qed

lemma card_multiset_only_sets':
  assumes "finite A"
  shows "card {M. set_mset M ⊆ A ∧ size M = k ∧ (∀x. count M x ≤ 1)} = card A choose k"
proof -
  from ‹finite A› have "{M. set_mset M ⊆ A ∧ size M = k ∧ (∀x. count M x ≤ 1)} =
    {M. M ⊆# mset_set A ∧ size M = k}"
    using msubset_mset_set_iff by auto
  from this ‹finite A› card_multiset_only_sets show ?thesis by simp
qed

end