Theory Twelvefold_Way.Preliminaries

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

section ‹Preliminaries›

theory Preliminaries
imports
  Main
  "HOL-Library.Multiset"
  "HOL-Library.FuncSet"
  "HOL-Combinatorics.Permutations"
  "HOL-ex.Birthday_Paradox"
  Card_Partitions.Card_Partitions
  Bell_Numbers_Spivey.Bell_Numbers
  Card_Multisets.Card_Multisets
  Card_Number_Partitions.Card_Number_Partitions
begin

subsection ‹Additions to Finite Set Theory›

lemma subset_with_given_card_exists:
  assumes "n ≤ card A"
  shows "∃B ⊆ A. card B = n"
using assms proof (induct n)
  case 0
  then show ?case by auto
next
  case (Suc n)
  from this obtain B where "B ⊆ A" "card B = n" by auto
  from this ‹B ⊆ A› ‹card B = n› have "card B < card A"
    using Suc.prems by linarith
  from ‹Suc n ≤ card A› card.infinite have "finite A" by force
  from this ‹B ⊆ A› finite_subset have "finite B" by blast
  from ‹card B < card A› ‹B ⊆ A› obtain a where "a ∈ A" "a ∉ B"
    by (metis less_irrefl subsetI subset_antisym)
  have "insert a B ⊆ A" "card (insert a B) = Suc n"
    using ‹finite B› ‹a ∈ A› ‹a ∉ B› ‹B ⊆ A› ‹card B = n› by auto
  then show ?case by blast
qed

subsection ‹Additions to Equiv Relation Theory›

lemmas univ_commute' = univ_commute[unfolded Equiv_Relations.proj_def]

lemma univ_predicate_impl_forall:
  assumes "equiv A R"
  assumes "P respects R"
  assumes "X ∈ A // R"
  assumes "univ P X"
  shows "∀x∈X. P x"
proof -
  from assms(1,3) obtain x where "x ∈ X"
    by (metis equiv_class_self quotientE)
  from ‹x ∈ X› assms(1,3) have "X = R `` {x}"
    by (metis Image_singleton_iff equiv_class_eq quotientE)
  from assms(1,2,4) this show ?thesis
    using equiv_class_eq_iff univ_commute' by fastforce
qed

lemma univ_preserves_predicate:
  assumes "equiv A r"
  assumes "P respects r"
  shows "{x ∈ A. P x} // r = {X ∈ A // r. univ P X}"
proof
  show "{x ∈ A. P x} // r ⊆ {X ∈ A // r. univ P X}"
  proof
    fix X
    assume "X ∈ {x ∈ A. P x} // r"
    from this obtain x where "x ∈ {x ∈ A. P x}" and "X = r `` {x}"
      using quotientE by blast
    have "X ∈ A // r"
      using ‹X = r `` {x}› ‹x ∈ {x ∈ A. P x}›
      by (auto intro: quotientI)
    moreover have "univ P X"
      using ‹X = r `` {x}› ‹x ∈ {x ∈ A. P x}› assms
      by (simp add: proj_def[symmetric] univ_commute)
    ultimately show "X ∈ {X ∈ A // r. univ P X}" by auto
  qed
next
  show "{X ∈ A // r. univ P X} ⊆ {x ∈ A. P x} // r"
  proof
    fix X
    assume "X ∈ {X ∈ A // r. univ P X}"
    from this have "X ∈ A // r" and "univ P X" by auto
    from ‹X ∈ A // r› obtain x where "x ∈ A" and "X = r `` {x}"
      using quotientE by blast
    have "x ∈ {x ∈ A. P x}"
      using ‹x ∈ A› ‹X = r `` {x}› ‹univ P X› assms
      by (simp add: proj_def[symmetric] univ_commute)
    from this show "X ∈ {x ∈ A. P x} // r"
      using ‹X = r `` {x}› by (auto intro: quotientI)
  qed
qed

lemma Union_quotient_restricted:
  assumes "equiv A r"
  assumes "P respects r"
  shows "⋃({x ∈ A. P x} // r) = {x ∈ A. P x}"
proof
  show "⋃({x ∈ A. P x} // r) ⊆ {x ∈ A. P x}"
  proof
    fix x
    assume "x ∈ ⋃({x ∈ A. P x} // r)"
    from this obtain X where "x ∈ X" and "X ∈ {x ∈ A. P x} // r" by blast
    from this obtain x' where "X = r `` {x'}" and "x' ∈ {x ∈ A. P x}"
      using quotientE by blast
    from this ‹x ∈ X› have "x ∈ A"
      using ‹equiv A r› by (simp add: equiv_class_eq_iff)
    moreover from ‹X = r `` {x'}› ‹x ∈ X› ‹x' ∈ {x ∈ A. P x}› have "P x"
      using ‹P respects r› congruentD by fastforce
    ultimately show "x ∈ {x ∈ A. P x}" by auto
  qed
next
  show "{x ∈ A. P x} ⊆ ⋃({x ∈ A. P x} // r)"
  proof
    fix x
    assume "x ∈ {x ∈ A. P x}"
    from this have "x ∈ r `` {x}"
      using ‹equiv A r› equiv_class_self by fastforce
    from ‹x ∈ {x ∈ A. P x}› have "r `` {x} ∈ {x ∈ A. P x} // r"
      by (auto intro: quotientI)
    from this ‹x ∈ r `` {x}› show "x ∈ ⋃({x ∈ A. P x} // r)" by auto
  qed
qed

lemma finite_equiv_implies_finite_carrier:
  assumes "equiv A R"
  assumes "finite (A // R)"
  assumes "∀X ∈ A // R. finite X"
  shows "finite A"
proof -
  from ‹equiv A R› have "A = ⋃(A // R)"
    by (simp add: Union_quotient)
  from this ‹finite (A // R)› ‹∀X ∈ A // R. finite X› show "finite A"
    using finite_Union by fastforce
qed

lemma finite_quotient_iff:
  assumes "equiv A R"
  shows "finite A ⟷ (finite (A // R) ∧ (∀X ∈ A // R. finite X))"
using assms by (meson equiv_type finite_equiv_class finite_equiv_implies_finite_carrier finite_quotient)

subsubsection ‹Counting Sets by Splitting into Equivalence Classes›

lemma card_equiv_class_restricted:
  assumes "finite {x ∈ A. P x}"
  assumes "equiv A R"
  assumes "P respects R"
  shows "card {x ∈ A. P x} = sum card ({x ∈ A. P x} // R)"
proof -
  have "card {x ∈ A. P x} = card (⋃({x ∈ A. P x} // R))"
    using ‹equiv A R› ‹P respects R› by (simp add: Union_quotient_restricted)
  also have "card (⋃({x ∈ A. P x} // R)) = (∑C∈{x ∈ A. P x} // R. card C)"
  proof -
    from ‹finite {x ∈ A. P x}› have "finite ({x ∈ A. P x} // R)"
      using ‹equiv A R› by (metis finite_imageI proj_image)
    moreover from ‹finite {x ∈ A. P x}› have "∀C∈{x ∈ A. P x} // R. finite C"
      using ‹equiv A R› ‹P respects R› Union_quotient_restricted
        Union_upper finite_subset by fastforce
    moreover have "∀C1 ∈ {x ∈ A. P x} // R. ∀C2 ∈ {x ∈ A. P x} // R. C1 ≠ C2 ⟶ C1 ∩ C2 = {}"
      using ‹equiv A R› quotient_disj
      by (metis (no_types, lifting) mem_Collect_eq quotientE quotientI)
    ultimately show ?thesis
      by (subst card_Union_disjoint) (auto simp: pairwise_def disjnt_def)
  qed
  finally show ?thesis .
qed

lemma card_equiv_class_restricted_same_size:
  assumes "equiv A R"
  assumes "P respects R"
  assumes "⋀F. F ∈ {x ∈ A. P x} // R ⟹ card F = k"
  shows "card {x ∈ A. P x} = k * card ({x ∈ A. P x} // R)"
proof cases
  assume "finite {x ∈ A. P x}"
  have "card {x ∈ A. P x} = sum card ({x ∈ A. P x} // R)"
    using ‹finite {x ∈ A. P x}› ‹equiv A R› ‹P respects R›
    by (simp add: card_equiv_class_restricted)
  also have "sum card ({x ∈ A. P x} // R) = k * card ({x ∈ A. P x} // R)"
    by (simp add: ‹⋀F. F ∈ {x ∈ A. P x} // R ⟹ card F = k›)
  finally show ?thesis .
next
  assume "infinite {x ∈ A. P x}"
  from this have "infinite (⋃({a ∈ A. P a} // R))"
    using ‹equiv A R› ‹P respects R› by (simp add: Union_quotient_restricted)
  from this have "infinite ({x ∈ A. P x} // R) ∨ (∃X ∈ {x ∈ A. P x} // R. infinite X)"
    by auto
  from this show ?thesis
  proof
    assume "infinite ({x ∈ A. P x} // R)"
    from this ‹infinite {x ∈ A. P x}› show ?thesis by simp
  next
    assume "∃X ∈ {x ∈ A. P x} // R. infinite X"
    from this ‹infinite {x ∈ A. P x}› show ?thesis
      using ‹⋀F. F ∈ {x ∈ A. P x} // R ⟹ card F = k› card.infinite by auto
  qed
qed

lemma card_equiv_class:
  assumes "finite A"
  assumes "equiv A R"
  shows "card A = sum card (A // R)"
proof -
  have "(λx. True) respects R" by (simp add: congruentI)
  from ‹finite A› ‹equiv A R› this show ?thesis
    using card_equiv_class_restricted[where P="λx. True"] by auto
qed

lemma card_equiv_class_same_size:
  assumes "equiv A R"
  assumes "⋀F. F ∈ A // R ⟹ card F = k"
  shows "card A = k * card (A // R)"
proof -
  have "(λx. True) respects R" by (simp add: congruentI)
  from ‹equiv A R› ‹⋀F. F ∈ A // R ⟹ card F = k› this show ?thesis
    using card_equiv_class_restricted_same_size[where P="λx. True"] by auto
qed

subsection ‹Additions to FuncSet Theory›

lemma finite_same_card_bij_on_ext_funcset:
  assumes "finite A" "finite B" "card A = card B"
  shows "∃f. f ∈ A →⇩E B ∧ bij_betw f A B"
proof -
  from assms obtain f' where f': "bij_betw f' A B"
    using finite_same_card_bij by auto
  define f where "⋀x. f x = (if x ∈ A then f' x else undefined)"
  have "f ∈ A →⇩E B"
    using f' unfolding f_def by (auto simp add: bij_betwE)
  moreover have "bij_betw f A B"
  proof -
    have "bij_betw f' A B ⟷ bij_betw f A B"
      unfolding f_def by (auto intro!: bij_betw_cong)
    from this ‹bij_betw f' A B› show ?thesis by auto
  qed
  ultimately show ?thesis by auto
qed

lemma card_extensional_funcset:
  assumes "finite A"
  shows "card (A →⇩E B) = card B ^ card A"
using assms by (simp add: card_PiE prod_constant)

lemma bij_betw_implies_inj_on_and_card_eq:
  assumes "finite B"
  assumes "f ∈ A →⇩E B"
  shows "bij_betw f A B ⟷ inj_on f A ∧ card A = card B"
proof
  assume "bij_betw f A B"
  from this show "inj_on f A ∧ card A = card B"
    by (simp add: bij_betw_imp_inj_on bij_betw_same_card)
next
  assume "inj_on f A ∧ card A = card B"
  from this have "inj_on f A" and "card A = card B" by auto
  from ‹f ∈ A →⇩E B› have "f ` A ⊆ B" by auto
  from ‹inj_on f A› have "card (f ` A) = card A" by (simp add: card_image)
  from ‹f ` A ⊆ B› ‹card A = card B› this have "f ` A = B"
    by (simp add: ‹finite B› card_subset_eq)
  from ‹inj_on f A› this show "bij_betw f A B" by (rule bij_betw_imageI)
qed

lemma bij_betw_implies_surj_on_and_card_eq:
  assumes "finite A"
  assumes "f ∈ A →⇩E B"
  shows "bij_betw f A B ⟷ f ` A = B ∧ card A = card B"
proof
  assume "bij_betw f A B"
  show "f ` A = B ∧ card A = card B"
    using ‹bij_betw f A B› bij_betw_imp_surj_on bij_betw_same_card by blast
next
  assume "f ` A = B ∧ card A = card B"
  from this have "f ` A = B" and "card A = card B" by auto
  from this have "inj_on f A"
    by (simp add: ‹finite A› inj_on_iff_eq_card)
  from this ‹f ` A = B› show "bij_betw f A B" by (rule bij_betw_imageI)
qed

subsection ‹Additions to Permutations Theory›

lemma
  assumes "f ∈ A →⇩E B" "f ` A = B"
  assumes "p permutes B" "(∀x. f' x = p (f x))"
  shows "(λb. {x∈A. f x = b}) ` B = (λb. {x∈A. f' x = b}) ` B"
proof
  show "(λb. {x ∈ A. f x = b}) ` B ⊆ (λb. {x ∈ A. f' x = b}) ` B"
  proof
    fix X
    assume "X ∈ (λb. {x ∈ A. f x = b}) ` B"
    from this obtain b where X_eq: "X = {x ∈ A. f x = b}" and "b ∈ B" by blast
    from assms(3, 4) have "⋀x. f x = b ⟷ f' x = p b" by (metis permutes_def)
    from ‹p permutes B› X_eq this have "X = {x ∈ A. f' x = p b}"
      using Collect_cong by auto
    moreover from ‹b ∈ B› ‹p permutes B› have "p b ∈ B"
      by (simp add: permutes_in_image)
    ultimately show "X ∈ (λb. {x ∈ A. f' x = b}) ` B" by blast
  qed
next
  show "(λb. {x ∈ A. f' x = b}) ` B ⊆ (λb. {x ∈ A. f x = b}) ` B"
  proof
    fix X
    assume "X ∈ (λb. {x ∈ A. f' x = b}) ` B"
    from this obtain b where X_eq: "X = {x ∈ A. f' x = b}" and "b ∈ B" by blast
    from assms(3, 4) have "⋀x. f' x = b ⟷ f x = inv p b"
      by (auto simp add: permutes_inverses(1, 2))
    from ‹p permutes B› X_eq this have "X = {x ∈ A. f x = inv p b}"
      using Collect_cong by auto
    moreover from ‹b ∈ B› ‹p permutes B› have "inv p b ∈ B"
      by (simp add: permutes_in_image permutes_inv)
    ultimately show "X ∈ (λb. {x ∈ A. f x = b}) ` B" by blast
  qed
qed

subsection ‹Additions to List Theory›

text ‹
The theorem @{thm [source] card_lists_length_eq} contains the superfluous assumption @{term "finite A"}.
Here, we derive that fact without that unnecessary assumption.
›

lemma lists_length_eq_Suc_eq_image_Cons:
  "{xs. set xs ⊆ A ∧ length xs = Suc n} = (λ(x, xs). x#xs) ` (A × {xs. set xs ⊆ A ∧ length xs = n})"
  (is "?A = ?B")
proof
  show "?A ⊆ ?B"
  proof
    fix xs
    assume "xs ∈ ?A"
    from this show "xs ∈ ?B" by (cases xs) auto
  qed
next
  show "?B ⊆ ?A" by auto
qed

lemma lists_length_eq_Suc_eq_empty_iff:
  "{xs. set xs ⊆ A ∧ length xs = Suc n} = {} ⟷ A = {}"
proof (induct n)
  case 0
  have "{xs. set xs ⊆ A ∧ length xs = Suc 0} = {x#[] |x. x ∈ A}"
  proof
    show "{[x] |x. x ∈ A} ⊆ {xs. set xs ⊆ A ∧ length xs = Suc 0}" by auto
  next
    show "{xs. set xs ⊆ A ∧ length xs = Suc 0} ⊆ {[x] |x. x ∈ A}"
    proof
      fix xs
      assume "xs ∈ {xs. set xs ⊆ A ∧ length xs = Suc 0}"
      from this have "set xs ⊆ A ∧ length xs = Suc 0" by simp
      from this have "∃x. xs = [x] ∧ x ∈ A"
        by (metis Suc_length_conv insert_subset length_0_conv list.set(2))
      from this show "xs ∈ {[x] |x. x ∈ A}" by simp
    qed
  qed
  then show ?case by simp
next
  case (Suc n)
  from this show ?case by (auto simp only: lists_length_eq_Suc_eq_image_Cons)
qed

lemma lists_length_eq_eq_empty_iff:
  "{xs. set xs ⊆ A ∧ length xs = n} = {} ⟷ (A = {} ∧ n > 0)"
proof (cases n)
  case 0
  then show ?thesis by auto
next
  case (Suc n)
  then show ?thesis by (auto simp only: lists_length_eq_Suc_eq_empty_iff)
qed

lemma finite_lists_length_eq_iff:
  "finite {xs. set xs ⊆ A ∧ length xs = n} ⟷ (finite A ∨ n = 0)"
proof
  assume "finite {xs. set xs ⊆ A ∧ length xs = n}"
  from this show "finite A ∨ n = 0"
  proof (induct n)
    case 0
    then show ?case by simp
  next
    case (Suc n)
    have "inj (λ(x, xs). x#xs)"
      by (auto intro: inj_onI)
    from this Suc(2) have "finite (A × {xs. set xs ⊆ A ∧ length xs = n})"
      using finite_imageD inj_on_subset subset_UNIV lists_length_eq_Suc_eq_image_Cons[of A n]
      by fastforce
    from this have "finite A"
      by (cases "A = {}")
        (auto simp only: lists_length_eq_eq_empty_iff dest: finite_cartesian_productD1)
    from this show ?case by auto
  qed
next
  assume "finite A ∨ n = 0"
  from this show "finite {xs. set xs ⊆ A ∧ length xs = n}"
    by (auto intro: finite_lists_length_eq)
qed

lemma card_lists_length_eq:
  shows "card {xs. set xs ⊆ B ∧ length xs = n} = card B ^ n"
proof cases
  assume "finite B"
  then show ?thesis by (rule card_lists_length_eq)
next
  assume "infinite B"
  then show ?thesis
  proof cases
    assume "n = 0"
    from this have "{xs. set xs ⊆ B ∧ length xs = n} = {[]}" by auto
    from this ‹n = 0› show ?thesis by simp
  next
    assume "n ≠ 0"
    from this ‹infinite B› have "infinite {xs. set xs ⊆ B ∧ length xs = n}"
      by (simp add: finite_lists_length_eq_iff)
    from this ‹infinite B› show ?thesis by auto
  qed
qed

subsection ‹Additions to Disjoint Set Theory›

lemma bij_betw_congI:
  assumes "bij_betw f A A'"
  assumes "∀a ∈ A. f a = g a"
  shows "bij_betw g A A'"
using assms bij_betw_cong by fastforce

lemma disjoint_family_onI[intro]:
  assumes "⋀m n. m ∈ S ⟹ n ∈ S ⟹ m ≠ n ⟹ A m ∩ A n = {}"
  shows "disjoint_family_on A S"
using assms unfolding disjoint_family_on_def by simp

text ‹
The following lemma is not needed for this development, but is useful
and could be moved to Disjoint Set theory or Equiv Relation theory if
translated from set partitions to equivalence relations.
›

lemma infinite_partition_on:
  assumes "infinite A"
  shows "infinite {P. partition_on A P}"
proof -
  from ‹infinite A› obtain x where "x ∈ A"
    by (meson finite.intros(1) finite_subset subsetI)
  from ‹infinite A› have "infinite (A - {x})"
    by (simp add: infinite_remove)
  define singletons_except_one
    where "singletons_except_one = (λa'. (λa. if a = a' then {a, x} else {a}) ` (A - {x}))"
  have "infinite (singletons_except_one ` (A - {x}))"
  proof -
    have "inj_on singletons_except_one (A - {x})"
      unfolding singletons_except_one_def by (rule inj_onI) auto
    from ‹infinite (A - {x})› this show ?thesis
      using finite_imageD by blast
  qed
  moreover have "singletons_except_one ` (A - {x}) ⊆ {P. partition_on A P}"
  proof
    fix P
    assume "P ∈ singletons_except_one ` (A - {x})"
    from this obtain a' where "a' ∈ A - {x}" and P: "P = singletons_except_one a'" by blast
    have "partition_on A ((λa. if a = a' then {a, x} else {a}) ` (A - {x}))"
      using ‹x ∈ A› ‹a' ∈ A - {x}› by (auto intro: partition_onI)
    from this have "partition_on A P"
      unfolding P singletons_except_one_def .
    from this show "P ∈ {P. partition_on A P}" ..
  qed
  ultimately show ?thesis by (simp add: infinite_super)
qed

lemma finitely_many_partition_on_iff:
  "finite {P. partition_on A P} ⟷ finite A"
using finitely_many_partition_on infinite_partition_on by blast

subsection ‹Additions to Multiset Theory›

lemma mset_set_subseteq_mset_set:
  assumes "finite B" "A ⊆ B"
  shows "mset_set A ⊆# mset_set B"
proof -
  from ‹A ⊆ B› ‹finite B› have "finite A" using finite_subset by blast
  {
    fix x
    have "count (mset_set A) x ≤ count (mset_set B) x"
      using ‹finite A› ‹finite B› ‹A ⊆ B›
      by (metis count_mset_set(1, 3) eq_iff subsetCE zero_le_one)
  }
  from this show "mset_set A ⊆# mset_set B"
    using mset_subset_eqI by blast
qed

lemma mset_set_set_mset:
  assumes "M ⊆# mset_set A"
  shows "mset_set (set_mset M) = M"
proof -
  {
    fix x
    from ‹M ⊆# mset_set A› have "count M x ≤ count (mset_set A) x"
      by (simp add: mset_subset_eq_count)
    from this have "count (mset_set (set_mset M)) x = count M x"
      by (metis count_eq_zero_iff count_greater_eq_one_iff count_mset_set
        dual_order.antisym dual_order.trans finite_set_mset)
  }
  from this show ?thesis by (simp add: multiset_eq_iff)
qed

lemma mset_set_set_mset':
  assumes "∀x. count M x ≤ 1"
  shows "mset_set (set_mset M) = M"
proof -
  {
    fix x
    from assms have "count M x = 0 ∨ count M x = 1" by (auto elim: le_SucE)
    from this have "count (mset_set (set_mset M)) x = count M x"
      by (metis count_eq_zero_iff count_mset_set(1,3) finite_set_mset)
  }
  from this show ?thesis by (simp add: multiset_eq_iff)
qed

lemma card_set_mset:
  assumes "M ⊆# mset_set A"
  shows "card (set_mset M) = size M"
using assms
by (metis mset_set_set_mset size_mset_set)

lemma card_set_mset':
  assumes "∀x. count M x ≤ 1"
  shows "card (set_mset M) = size M"
using assms
by (metis mset_set_set_mset' size_mset_set)

lemma count_mset_set_leq:
  assumes "finite A"
  shows "count (mset_set A) x ≤ 1"
using assms by (metis count_mset_set(1,3) eq_iff zero_le_one)

lemma count_mset_set_leq':
  assumes "finite A"
  shows "count (mset_set A) x ≤ Suc 0"
using assms count_mset_set_leq by fastforce

lemma msubset_mset_set_iff:
  assumes "finite A"
  shows "set_mset M ⊆ A ∧ (∀x. count M x ≤ 1) ⟷ (M ⊆# mset_set A)"
proof
  assume "set_mset M ⊆ A ∧ (∀x. count M x ≤ 1)"
  from this assms show "M ⊆# mset_set A"
    by (metis count_inI count_mset_set(1) le0 mset_subset_eqI subsetCE)
next
  assume "M ⊆# mset_set A"
  from this assms have "set_mset M ⊆ A"
    using mset_subset_eqD by fastforce
  moreover {
    fix x
    from ‹M ⊆# mset_set A› have "count M x ≤ count (mset_set A) x"
      by (simp add: mset_subset_eq_count)
    from this ‹finite A› have "count M x ≤ 1"
      by (meson count_mset_set_leq le_trans)
  }
  ultimately show "set_mset M ⊆ A ∧ (∀x. count M x ≤ 1)" by simp
qed

lemma image_mset_fun_upd:
  assumes "x ∉# M"
  shows "image_mset (f(x := y)) M = image_mset f M"
using assms by (induct M) auto

subsection ‹Additions to Number Partitions Theory›

lemma Partition_diag:
  shows "Partition n n = 1"
by (cases n) (auto simp only: Partition_diag Partition.simps(1))

subsection ‹Cardinality Theorems with Iverson Function›

definition iverson :: "bool ⇒ nat"
where
  "iverson b = (if b then 1 else 0)"

lemma card_partition_on_size1_eq_iverson:
  assumes "finite A"
  shows "card {P. partition_on A P ∧ card P ≤ k ∧ (∀X∈P. card X = 1)} = iverson (card A ≤ k)"
proof (cases "card A ≤ k")
  case True
  from this ‹finite A› show ?thesis
    unfolding iverson_def
    using card_partition_on_size1_eq_1 by fastforce
next
  case False
  from this ‹finite A› show ?thesis
    unfolding iverson_def
    using card_partition_on_size1_eq_0 by fastforce
qed

lemma card_number_partitions_with_only_parts_1:
  "card {N. (∀n. n∈# N ⟶ n = 1) ∧ number_partition n N ∧ size N ≤ x} = iverson (n ≤ x)"
proof -
  show ?thesis
  proof cases
    assume "n ≤ x"
    from this show ?thesis
      using card_number_partitions_with_only_parts_1_eq_1
      unfolding iverson_def by auto
  next
    assume "¬ n ≤ x"
    from this show ?thesis
      using card_number_partitions_with_only_parts_1_eq_0
      unfolding iverson_def by auto
  qed
qed

end