Theory Twelvefold_Way_Entry7

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

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

theory Twelvefold_Way_Entry7
imports Equiv_Relations_on_Functions
begin

subsection ‹Definition of Bijections›

definition partitions_of :: "'a set ⇒ 'b set ⇒ ('a ⇒ 'b) set ⇒ 'a set set"
where
  "partitions_of A B F = univ (λf. (λb. {x ∈ A. f x = b}) ` B - {{}}) F"

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

subsection ‹Properties for Bijections›

lemma partitions_of:
  assumes "finite B"
  assumes "F ∈ (A →⇩E B) // range_permutation A B"
  shows "card (partitions_of A B F) ≤ card B"
  and "partition_on A (partitions_of A B F)"
proof -
  from ‹F ∈ (A →⇩E B) // range_permutation A B› obtain f where "f ∈ A →⇩E B"
    and F_eq: "F = range_permutation A B `` {f}" using quotientE by blast
  have "partitions_of A B F = univ (λf. (λb. {x ∈ A. f x = b}) ` B - {{}}) F"
    unfolding partitions_of_def ..
  also have "… = univ (λf. (λb. {x ∈ A. f x = b}) ` B - {{}}) (range_permutation A B `` {f})"
    unfolding F_eq ..
  also have "… = (λb. {x ∈ A. f x = b}) ` B - {{}}"
    using equiv_range_permutation domain_partitions_respects_range_permutation ‹f ∈ A →⇩E B›
    by (subst univ_commute') auto
  finally have partitions_of_eq: "partitions_of A B F = (λb. {x ∈ A. f x = b}) ` B - {{}}" .
  show "card (partitions_of A B F) ≤ card B"
  proof -
    have "card (partitions_of A B F) = card ((λb. {x ∈ A. f x = b}) ` B - {{}})"
      unfolding partitions_of_eq ..
    also have "… ≤ card ((λb. {x ∈ A. f x = b}) ` B)"
      using ‹finite B› by (auto intro: card_mono)
    also have "… ≤ card B"
      using ‹finite B› by (rule card_image_le)
    finally show ?thesis .
  qed
  show "partition_on A (partitions_of A B F)"
  proof -
    have "partition_on A ((λb. {x ∈ A. f x = b}) ` B - {{}})"
      using ‹f ∈ A →⇩E B› by (auto intro!: partition_onI)
    from this show ?thesis
      unfolding partitions_of_eq .
  qed
qed

lemma functions_of:
  assumes "finite A" "finite B"
  assumes "partition_on A P"
  assumes "card P ≤ card B"
  shows "functions_of P A B ∈ (A →⇩E B) // range_permutation A B"
proof -
  obtain f where "f ∈ A →⇩E B" and r1: "(λb. {x ∈ A. f x = b}) ` B - {{}} = P"
    using obtain_function_with_partition[OF ‹finite A› ‹finite B› ‹partition_on A P› ‹card P ≤ card B›]
    by blast
  have "functions_of P A B = range_permutation A B `` {f}"
  proof
    show "functions_of P A B ⊆ range_permutation A B `` {f}"
    proof
      fix f'
      assume "f' ∈ functions_of P A B"
      from this have "f' ∈ A →⇩E B" and r2: "(λb. {x ∈ A. f' x = b}) ` B - {{}} = P"
        unfolding functions_of_def by auto
      from r1 r2
      obtain p where "p permutes B ∧ (∀x∈A. f x = p (f' x))"
        using partitions_eq_implies_permutes[OF ‹f ∈ A →⇩E B› ‹f' ∈ A →⇩E B›] ‹finite B› by metis
      from this show "f' ∈ range_permutation A B `` {f}"
        using ‹f ∈ A →⇩E B› ‹f' ∈ A →⇩E B›
        unfolding range_permutation_def by auto
    qed
  next
    show "range_permutation A B `` {f} ⊆ functions_of P A B"
    proof
      fix f'
      assume "f' ∈ range_permutation A B `` {f}"
      from this have "(f, f') ∈ range_permutation A B" by auto
      from this have "f' ∈ A →⇩E B"
        unfolding range_permutation_def by auto
      from ‹(f, f') ∈ range_permutation A B› have
        "(λb. {x ∈ A. f x = b}) ` B - {{}} = (λb. {x ∈ A. f' x = b}) ` B - {{}}"
        using congruentD[OF domain_partitions_respects_range_permutation] by blast
      from ‹f' ∈ A →⇩E B› this r1 show "f' ∈ functions_of P A B"
        unfolding functions_of_def by auto
    qed
  qed
  from this ‹f ∈ A →⇩E B› show ?thesis by (auto intro: quotientI)
qed

lemma functions_of_partitions_of:
  assumes "finite B"
  assumes "F ∈ (A →⇩E B) // range_permutation A B"
  shows "functions_of (partitions_of A B F) A B = F"
proof -
  from ‹F ∈ (A →⇩E B) // range_permutation A B› obtain f where "f ∈ A →⇩E B"
    and F_eq: "F = range_permutation A B `` {f}" using quotientE by blast
  have partitions_of_eq: "partitions_of A B F = (λb. {x ∈ A. f x = b}) ` B - {{}}"
        unfolding partitions_of_def F_eq
        using equiv_range_permutation domain_partitions_respects_range_permutation ‹f ∈ A →⇩E B›
        by (subst univ_commute') auto
  show ?thesis
  proof
    show "functions_of (partitions_of A B F) A B ⊆ F"
    proof
      fix f'
      assume f': "f' ∈ functions_of (partitions_of A B F) A B"
      from this have "(λb. {x ∈ A. f x = b}) ` B - {{}} = (λb. {x ∈ A. f' x = b}) ` B - {{}}"
        unfolding functions_of_def by (auto simp add: partitions_of_eq)
      note ‹f ∈ A →⇩E B›
      moreover from f' have "f' ∈ A →⇩E B"
        unfolding functions_of_def by auto
      moreover obtain p where "p permutes B ∧ (∀x∈A. f x = p (f' x))"
        using partitions_eq_implies_permutes[OF ‹f ∈ A →⇩E B› ‹f' ∈ A →⇩E B› ‹finite B›
          ‹(λb. {x ∈ A. f x = b}) ` B - {{}} = (λb. {x ∈ A. f' x = b}) ` B - {{}}›]
        by metis
      ultimately show "f' ∈ F"
        unfolding F_eq range_permutation_def by auto
    qed
  next
    show "F ⊆ functions_of (partitions_of A B F) A B"
    proof
      fix f'
      assume "f' ∈ F"
      from this have "f' ∈ A →⇩E B"
        unfolding F_eq range_permutation_def by auto
      from ‹f' ∈ F› obtain p where "p permutes B" "∀x∈A. f x = p (f' x)"
        unfolding F_eq range_permutation_def by auto
      have eq: "(λb. {x ∈ A. f' x = b}) ` B - {{}} = (λb. {x ∈ A. f x = b}) ` B - {{}}"
      proof -
        have "(λb. {x ∈ A. f' x = b}) ` B - {{}} = (λb. {x ∈ A. p (f' x) = b}) ` B - {{}}"
          using permutes_implies_inv_image_on_eq[OF ‹p permutes B›, of A f'] by simp
        also have "… =  (λb. {x ∈ A. f x = b}) ` B - {{}}"
          using ‹∀x∈A. f x = p (f' x)› by auto
        finally show ?thesis .
      qed
      from this ‹f' ∈ A →⇩E B› show "f' ∈ functions_of (partitions_of A B F) A B"
        unfolding functions_of_def partitions_of_eq by auto
    qed
  qed
qed

lemma partitions_of_functions_of:
  assumes "finite A" "finite B"
  assumes "partition_on A P"
  assumes "card P ≤ card B"
  shows "partitions_of A B (functions_of P A B) = P"
proof -
  have "functions_of P A B ∈ (A →⇩E B) // range_permutation A B"
    using ‹finite A› ‹finite B› ‹partition_on A P› ‹card P ≤ card B› by (rule functions_of)
  from this obtain f where "f ∈ A →⇩E B" and functions_of_eq: "functions_of P A B = range_permutation A B `` {f}"
    using quotientE by metis
  from functions_of_eq ‹f ∈ A →⇩E B› have "f ∈ functions_of P A B"
    using equiv_range_permutation equiv_class_self by fastforce
  have "partitions_of A B (functions_of P A B) = univ (λf. (λb. {x ∈ A. f x = b}) ` B - {{}}) (functions_of P A B)"
    unfolding partitions_of_def ..
  also have "… = univ (λf. (λb. {x ∈ A. f x = b}) ` B - {{}}) (range_permutation A B `` {f})"
    unfolding ‹functions_of P A B = range_permutation A B `` {f}› ..
  also have "… = (λb. {x ∈ A. f x = b}) ` B - {{}}"
    using equiv_range_permutation domain_partitions_respects_range_permutation ‹f ∈ A →⇩E B›
    by (subst univ_commute') auto
  also have "(λb. {x ∈ A. f x = b}) ` B - {{}} = P"
    using ‹f ∈ functions_of P A B› unfolding functions_of_def by simp
  finally show ?thesis .
qed

subsection ‹Bijections›

lemma bij_betw_partitions_of:
  assumes "finite A" "finite B"
  shows "bij_betw (partitions_of A B) ((A →⇩E B) // range_permutation A B) {P. partition_on A P ∧ card P ≤ card B}"
proof (rule bij_betw_byWitness[where f'="λP. functions_of P A B"])
  show "∀F∈(A →⇩E B) // range_permutation A B. functions_of (partitions_of A B F) A B = F"
    using ‹finite B› by (simp add: functions_of_partitions_of)
  show "∀P∈{P. partition_on A P ∧ card P ≤ card B}. partitions_of A B (functions_of P A B) = P"
    using ‹finite A› ‹finite B› by (auto simp add: partitions_of_functions_of)
  show "partitions_of A B ` ((A →⇩E B) // range_permutation A B) ⊆ {P. partition_on A P ∧ card P ≤ card B}"
    using ‹finite B› partitions_of by auto
  show "(λP. functions_of P A B) ` {P. partition_on A P ∧ card P ≤ card B} ⊆ (A →⇩E B) // range_permutation A B"
    using functions_of ‹finite A› ‹finite B› by auto
qed

subsection ‹Cardinality›

lemma
  assumes "finite A" "finite B"
  shows "card ((A →⇩E B) // range_permutation A B) = (∑j≤card B. Stirling (card A) j)"
proof -
  have "bij_betw (partitions_of A B) ((A →⇩E B) // range_permutation A B) {P. partition_on A P ∧ card P ≤ card B}"
    using ‹finite A› ‹finite B› by (rule bij_betw_partitions_of)
  from this have "card ((A →⇩E B) // range_permutation A B) = card {P. partition_on A P ∧ card P ≤ card B}"
    by (rule bij_betw_same_card)
  also have "card  {P. partition_on A P ∧ card P ≤ card B} = (∑j≤card B. Stirling (card A) j)"
    using ‹finite A› by (rule card_partition_on_at_most_size)
  finally show ?thesis .
qed

end