Theory Twelvefold_Way_Entry8

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

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

theory Twelvefold_Way_Entry8
imports Twelvefold_Way_Entry7
begin

subsection ‹Properties for Bijections›

lemma inj_on_implies_partitions_of:
  assumes "F ∈ (A →⇩E B) // range_permutation A B"
  assumes "univ (λf. inj_on f A) F"
  shows "∀X ∈ partitions_of A B F. card X = 1"
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
  from this ‹univ (λf. inj_on f A) F› have "inj_on f A"
    using univ_commute'[OF equiv_range_permutation inj_on_respects_range_permutation ‹f ∈ A →⇩E B›] by simp
  have "∀X∈(λb. {x ∈ A. f x = b}) ` B - {{}}. card X = 1"
  proof
    fix X
    assume "X ∈ (λb. {x ∈ A. f x = b}) ` B - {{}}"
    from this obtain x where "X = {xa ∈ A. f xa = f x}" "x ∈ A" by auto
    from this have "X = {x}"
      using ‹inj_on f A› by (auto dest!: inj_onD)
    from this show "card X = 1" by simp
  qed
  from this show ?thesis
    unfolding partitions_of_def F_eq
    using equiv_range_permutation domain_partitions_respects_range_permutation ‹f ∈ A →⇩E B›
    by (subst univ_commute') assumption+
qed

lemma unique_part_eq_singleton:
  assumes "partition_on A P"
  assumes "∀X∈P. card X = 1"
  assumes "x ∈ A"
  shows "(THE X. x ∈ X ∧ X ∈ P) = {x}"
proof -
  have "(THE X. x ∈ X ∧ X ∈ P) ∈ P"
    using ‹partition_on A P› ‹x ∈ A› by (simp add: partition_on_the_part_mem)
  from this have "card (THE X. x ∈ X ∧ X ∈ P) = 1"
    using ‹∀X∈P. card X = 1› by auto
  moreover have "x ∈ (THE X. x ∈ X ∧ X ∈ P)"
    using ‹partition_on A P› ‹x ∈ A› by (simp add: partition_on_in_the_unique_part)
  ultimately show ?thesis
    by (metis card_1_singletonE singleton_iff)
qed

lemma functions_of_is_inj_on:
  assumes "finite A" "finite B" "partition_on A P" "card P ≤ card B"
  assumes "∀X∈P. card X = 1"
  shows "univ (λf. inj_on f A) (functions_of P A B)"
proof -
  have "functions_of P A B ∈ (A →⇩E B) // range_permutation A B"
    using functions_of ‹finite A› ‹finite B› ‹partition_on A P› ‹card P ≤ card B› by blast
  from this obtain f where eq_f: "functions_of P A B = range_permutation A B `` {f}" and "f ∈ A →⇩E B"
    using quotientE by blast
  from eq_f have "f ∈ functions_of P A B"
    using ‹f ∈ A →⇩E B› equiv_range_permutation equiv_class_self by fastforce
  from this have eq: "(λb. {x ∈ A. f x = b}) ` B - {{}} = P"
    unfolding functions_of_def by auto
  have "inj_on f A"
  proof (rule inj_onI)
    fix x y
    assume "x ∈ A" "y ∈ A" "f x = f y"
    from ‹x ∈ A› have "x ∈ {x' ∈ A. f x' = f x}" by auto
    moreover from ‹y ∈ A› ‹f x = f y› have "y ∈ {x' ∈ A. f x' = f x}" by auto
    moreover have "card {x' ∈ A. f x' = f x} = 1"
    proof -
      from ‹x ∈ A› ‹f ∈ A →⇩E B› have "f x ∈ B" by auto
      from this ‹x ∈ A› have "{x' ∈ A. f x' = f x} ∈ (λb. {x ∈ A. f x = b}) ` B - {{}}" by auto
      from this ‹∀X∈P. card X = 1› eq show ?thesis by auto
    qed
    ultimately show "x = y" by (metis card_1_singletonE singletonD)
  qed
  from this show ?thesis
    unfolding eq_f using equiv_range_permutation inj_on_respects_range_permutation ‹f ∈ A →⇩E B›
    by (subst univ_commute') assumption+
qed

subsection ‹Bijections›

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

subsection ‹Cardinality›

lemma card_injective_functions_range_permutation:
  assumes "finite A" "finite B"
  shows "card ({f ∈ A →⇩E B. inj_on f A} // range_permutation A B) = iverson (card A ≤ card B)"
proof -
  obtain enum where "bij_betw enum {0..<card A} A"
    using ‹finite A› ex_bij_betw_nat_finite by blast
  have "bij_betw (partitions_of A B) ({f ∈ A →⇩E B. inj_on f A} // range_permutation A B) {P. partition_on A P ∧ card P ≤ card B ∧ (∀X∈P. card X = 1)}"
    using ‹finite A› ‹finite B› by (rule bij_betw_partitions_of)
  from this have "card ({f ∈ A →⇩E B. inj_on f A} // range_permutation A B) = card {P. partition_on A P ∧ card P ≤ card B ∧ (∀X∈P. card X = 1)}"
    by (rule bij_betw_same_card)
  also have "card {P. partition_on A P ∧ card P ≤ card B ∧ (∀X∈P. card X = 1)} = iverson (card A ≤ card B)"
    using ‹finite A› by (rule card_partition_on_size1_eq_iverson)
  finally show ?thesis .
qed

end