Theory Bell_Numbers_Spivey.Bell_Numbers

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

section ‹Bell Numbers and Spivey's Generalized Recurrence›

theory Bell_Numbers
imports
  "HOL-Library.FuncSet"
  "HOL-Library.Monad_Syntax"
  "HOL-Library.Code_Target_Nat"
  "HOL-Combinatorics.Stirling"
  Card_Partitions.Injectivity_Solver
  Card_Partitions.Card_Partitions
begin

subsection ‹Preliminaries›

subsubsection ‹Additions to FuncSet›

(* this is clearly to be added to FuncSet *)
lemma extensional_funcset_ext:
  assumes "f  A E B" "g  A E B"
  assumes "x. x  A  f x = g x"
  shows "f = g"
using assms by (metis PiE_iff extensionalityI)

subsubsection ‹Additions for Injectivity Proofs›

lemma inj_on_impl_inj_on_image:
  assumes "inj_on f A"
  assumes "x. x  X  x  A"
  shows "inj_on ((`) f) X"
using assms by (meson inj_onI inj_on_image_eq_iff)

lemma injectivity_union:
  assumes "A  B = C  D"
  assumes "P A" "P C"
  assumes "Q B" "Q D"
    "S T. P S  Q T  S  T = {}"
  shows "A = C  B = D"
using assms Int_Un_distrib Int_commute inf_sup_absorb by blast+

lemma injectivity_image:
  assumes "f ` A = g ` A"
  assumes "xA. invert (f x) = x  invert (g x) = x"
  shows "xA. f x = g x"
using assms by (metis (no_types, lifting) image_iff)

lemma injectivity_image_union:
  assumes "(λX. X  F X) ` P = (λX. X  G X) ` P'"
  assumes "X  P. X  A" "X  P'. X  A"
  assumes "X  P. yF X. y  A" "X  P'. yG X. y  A"
  shows "P = P'"
proof
  show "P  P'"
  proof
    fix X
    assume "X  P"
    from assms(1) this obtain X' where "X'  P'" and "X  F X = X'  G X'"
      by (metis imageE image_eqI)
    moreover from assms(2,4) X  P have X: "(X  F X)  A = X" by auto
    moreover from assms(3,5) X'  P' have X': "(X'  G X')  A = X'" by auto
    ultimately have "X = X'" by simp
    from this X'  P' show "X  P'" by auto
  qed
next
  show "P'  P"
  proof
    fix X'
    assume "X'  P'"
    from assms(1) this obtain X where "X  P" and "X  F X = X'  G X'"
      by (metis imageE image_eqI)
    moreover from assms(2,4) X  P have X: "(X  F X)  A = X" by auto
    moreover from assms(3,5) X'  P' have X': "(X'  G X')  A = X'" by auto
    ultimately have "X = X'" by simp
    from this X  P show "X'  P" by auto
  qed
qed

subsection ‹Definition of Bell Numbers›

definition Bell :: "nat  nat"
where
  "Bell n = card {P. partition_on {0..<n} P}"

lemma Bell_altdef:
  assumes "finite A"
  shows "Bell (card A) = card {P. partition_on A P}"
proof -
  from finite A obtain f where bij: "bij_betw f {0..<card A} A"
    using ex_bij_betw_nat_finite by blast
  from this have inj: "inj_on f {0..<card A}"
    using bij_betw_imp_inj_on by blast
  from bij have image_f_eq: "A = f ` {0..<card A}"
    using bij_betw_imp_surj_on by blast
  have "x  {P. partition_on {0..<card A} P}. x  Pow {0..<card A}"
    by (auto elim: partition_onE)
  from this inj have "inj_on ((`) ((`) f)) {P. partition_on {0..<card A} P}"
    by (intro inj_on_impl_inj_on_image[of _ "Pow {0..<card A}"]
     inj_on_impl_inj_on_image[of _ "{0..<card A}"]) blast+
  moreover from inj have "(`) ((`) f) ` {P. partition_on {0..<card A} P} = {P. partition_on A P}"
    by (subst image_f_eq, auto elim!: set_of_partition_on_map)
  ultimately have "bij_betw ((`) ((`) f)) {P. partition_on {0..<card A} P} {P. partition_on A P}"
    by (auto intro: bij_betw_imageI)
  from this finite A show ?thesis
    unfolding Bell_def
    by (subst bij_betw_iff_card[symmetric]) (auto intro: finitely_many_partition_on)
qed

lemma Bell_0:
  "Bell 0 = 1"
by (auto simp add: Bell_def partition_on_empty)

subsection ‹Construction of the Partitions›

definition construct_partition_on :: "'a set  'a set  'a set set set"
where
  "construct_partition_on B C =
    do {
       k   {0..card B};
       j   {0..card C};
       P   {P. partition_on C P  card P = j};
       B'  {B'. B'  B  card B' = k};
       Q   {Q. partition_on B' Q};
       f   (B - B') E P;
       P'   {(λX. X  {x  B - B'. f x = X}) ` P};
       {P'  Q}
    }"

lemma construct_partition_on:
  assumes "finite B" "finite C"
  assumes "B  C = {}"
  shows "construct_partition_on B C = {P. partition_on (B  C) P}"
proof (rule set_eqI')
  fix Q'
  assume "Q'  construct_partition_on B C"
  from this obtain j k P P' Q B' f
    where "j  card C"
    and "k  card B"
    and P: "partition_on C P  card P = j"
    and B': "B'  B  card B' = k"
    and Q: "partition_on B' Q"
    and f: "f  B - B' E P"
    and P': "P' = (λX. X  {x  B - B'. f x = X}) ` P"
    and Q': "Q' = P'  Q"
    unfolding construct_partition_on_def by auto
  from P f have "partition_on (B - B'  C) P'"
    unfolding P' using B  C = {}
    by (intro partition_on_insert_elements) auto
  from this Q have "partition_on ((B - B'  C)  B') Q'"
    unfolding Q' using B' B  C = {} by (auto intro: partition_on_union)
  from this have "partition_on (B  C) Q'"
    using B' by (metis Diff_partition sup.assoc sup.commute)
  from this show "Q'  {P. partition_on (B  C) P}" by auto
next
  fix Q'
  assume Q': "Q'  {Q'. partition_on (B  C) Q'}"
  from Q' have "{}  Q'" by (auto elim!: partition_onE)
  obtain Q where Q: "Q = ((λX. if X  B then X else {}) ` Q') - {{}}" by blast
  obtain P' where P': "P' = ((λX. if X  B then {} else X) ` Q') - {{}}" by blast
  from P' Q {}  Q' have Q'_prop: "Q' = P'  Q" by auto
  have P'_nosubset: "X  P'. ¬ X  B"
    unfolding P' by auto
  moreover have "X  P'. X  B  C"
    using Q' P' by (auto elim: partition_onE)
  ultimately have P'_witness: "X  P'. x. x  X  C"
    using B  C = {} by fastforce
  obtain B' where B': "B' = Q" by blast
  have Q_prop: "partition_on B' Q"
    using B' Q' Q'_prop partition_on_split2 mem_Collect_eq by blast
  have "P' = B - B'  C"
  proof
    have "Q' = B  C" "XQ'. X'Q'. X  X'  X  X' = {}"
      using Q' unfolding partition_on_def disjoint_def by auto
    from this show "P'  B - B'  C"
      unfolding P' B' Q by auto blast
  next
    show "B - B'  C  P'"
    proof
      fix x
      assume "x  B - B'  C"
      from this obtain X where X: "x  X" "X  Q'"
        using Q' by (metis Diff_iff Un_iff mem_Collect_eq partition_on_partition_on_unique)
      have "X  Q'. X  B  X  B'"
        unfolding B' Q by auto
      from this X x  B - B'  C have "¬ X  B"
        using B  C = {} by auto
      from this X  Q' have "X  P'" using P' by auto
      from this x  X show "x  P'" by auto
    qed
  qed
  from this have partition_on_P': "partition_on (B - B'  C) P'"
    using partition_on_split1 Q'_prop Q' mem_Collect_eq by fastforce
  obtain P where P: "P = (λX. X  C) ` P'" by blast
  from P partition_on_P' P'_witness have "partition_on C P"
    using partition_on_intersect_on_elements by auto
  obtain f where f: "f = (λx. if x  B - B' then (THE X. x  X  X  P')  C else undefined)" by blast
  have P'_prop: "P' = (λX. X  {x  B - B'. f x = X}) ` P"
  proof
    {
      fix X
      assume "X  P'"
      have X_subset: "X  (B - B')  C"
        using partition_on_P' X  P' by (auto elim: partition_onE)
      have "X = X  C  {x  B - B'. f x = X  C}"
      proof
        {
          fix x
          assume  "x  X"
          from this X_subset have "x  (B - B')  C" by auto
          from this have "x  X  C  {xa  B - B'. f xa = X  C}"
          proof
            assume "x  C"
            from this x  X show ?thesis by simp
          next
            assume "x  B - B'"
            from partition_on_P' x  X X  P' have "(THE X. x  X  X  P') = X"
              by (simp add: partition_on_the_part_eq)
            from x  B - B' this show ?thesis unfolding f by auto
          qed
        }
        from this show "X  X  C  {x  B - B'. f x = X  C}" by auto
      next
        show "X  C  {xa  B - B'. f xa = X  C}  X"
        proof
          fix x
          assume "x  X  C  {x  B - B'. f x = X  C}"
          from this show "x  X"
          proof
            assume "x  X  C"
            from this show ?thesis by simp
          next
            assume x_in: "x  {x  B - B'. f x = X  C}"
            from this have ex1: "∃!X. x  X  X  P'"
              using partition_on_P' by (auto intro!: partition_on_partition_on_unique)
            from x_in X_subset have eq: "(THE X. x  X  X  P')  C = X  C"
              unfolding f by auto
           from P'_nosubset X  P' have "¬ X  B" by simp
           from this have "X  C  {}"
             using X_subset assms(3) by blast
           from this obtain y where y: "y  X  C" by auto
           from this eq have y_in: "y  (THE X. x  X  X  P')  C" by simp
           from y y_in have "y  X" "y  (THE X. x  X  X  P')" by auto
           moreover from y have "∃!X. y  X  X  P'"
             using partition_on_P' by (simp add: partition_on_partition_on_unique)
           moreover have "(THE X. x  X  X  P')  P'"
             using ex1 by (rule the1I2) auto
           ultimately have "(THE X. x  X  X  P') = X" using X  P' by auto
           from this ex1 show ?thesis by (auto intro: the1I2)
          qed
        qed
      qed
      from X  P' this have "X  (λX. X  {x  B - B'. f x = X}) ` P"
        unfolding P by simp
    }
    from this show "P'  (λX. X  {x  B - B'. f x = X}) ` P" ..
  next
    {
      fix x
      assume x_in_image: "x  (λX. X  {x  B - B'. f x = X}) ` P"
      {
        fix X
        assume "X  P'"
        have "{x  B - B'. f x = X  C} =  {x  B - B'. x  X}"
        proof -
          {
            fix x
            assume "x  B - B'"
            from this have ex1: "∃!X. x  X  X  P'"
              using partition_on_P' by (auto intro!: partition_on_partition_on_unique)
            from this have in_p: "(THE X. x  X  X  P')  P'"
              and x_in: "x  (THE X. x  X  X  P')"
              by (metis (mono_tags, lifting) theI)+
            have "f x = X  C  (THE X. x  X  X  P')  C = X  C"
              using x  B - B' unfolding f by auto
            also have "...  (THE X. x  X  X  P') = X"
            proof
              assume "(THE X. x  X  X  P') = X"
              from this show "(THE X. x  X  X  P')  C = X  C" by auto
            next
              assume "(THE X. x  X  X  P')  C = X  C"
              have "(THE X. x  X  X  P')  X  {}"
                using P'_witness (THE X. x  X  X  P')  C = X  C X  P' by fastforce
              from this show "(THE X. x  X  X  P') = X"
                using partition_on_P'[unfolded partition_on_def disjoint_def] in_p X  P' by metis
            qed
            also have "...  x  X"
              using ex1 X  P' x_in by (auto; metis (no_types, lifting) the_equality)
            finally have "f x = X  C  x  X" .
          }
          from this show ?thesis by auto
        qed
        moreover have  "X  B - B'  C"
          using partition_on_P' X  P' by (blast elim: partition_onE)
        ultimately have "X  C  {x  B. x  B'  f x = X  C} = X" by auto
      }
      from this x_in_image have "x  P'" unfolding P by auto
    }
    from this show "(λX. X  {x  B - B'. f x = X}) ` P  P'" ..
  qed
  from partition_on_P' have f_prop: "f  (B - B') E P"
    unfolding f P by (auto simp add: partition_on_the_part_mem)
  from Q B' have "B'  B" by auto
  obtain k where k: "k = card B'" by blast
  from finite B B'  B k have k_prop: "k  {0..card B}" by (simp add: card_mono)
  obtain j where j: "j = card P" by blast
  from j partition_on C P have j_prop: "j  {0..card C}"
    by (simp add: assms(2) partition_on_le_set_elements)
  from partition_on C P j have P_prop: "partition_on C P  card P = j" by auto
  from k B'  B have B'_prop: "B'  B  card B' = k" by auto
  show "Q'  construct_partition_on B C"
    using j_prop k_prop P_prop B'_prop Q_prop P'_prop f_prop Q'_prop
    unfolding construct_partition_on_def
    by (auto simp del: atLeastAtMost_iff) blast
qed

subsection ‹Injectivity of the Set Construction›

lemma injectivity:
  assumes "B  C = {}"
  assumes P: "(partition_on C P  card P = j)  (partition_on C P'  card P' = j')"
  assumes B': "(B'  B  card B' = k)  (B''  B  card B'' = k')"
  assumes Q: "partition_on B' Q  partition_on B'' Q'"
  assumes f: "f  B - B' E P  g  B - B'' E P'"
  assumes P': "P'' = (λX. X  {x  B - B'. f x = X}) ` P 
    P''' = (λX. X  {x  B - B''. g x = X}) ` P'"
  assumes eq_result: "P''  Q = P'''  Q'"
  shows "f = g" and "Q = Q'" and "B' = B''"
    and "P = P'" and "j = j'" and "k = k'"
proof -
  have P_nonempty_sets: "XP. cC. c  X" "XP'. cC. c  X"
    using P by (force elim: partition_onE)+
  have 1: "XP''. cC. c  X" "XP'''. cC. c  X"
    using P' P_nonempty_sets by fastforce+
  have 2: "XQ. xX. x  C" "XQ'. xX. x  C"
    using B  C = {} Q B' by (auto elim: partition_onE)
  from eq_result have "P'' = P'''" and "Q = Q'"
    by (auto dest: injectivity_union[OF _ 1 2])
  from this Q show "Q = Q'" and "B' = B''"
    by (auto intro!: partition_on_eq_implies_eq_carrier)
  have subset_C: "XP. X  C" "XP'. X  C"
    using P by (auto elim: partition_onE)
  have eq_image: "(λX. X  {x  B - B'. f x = X}) ` P = (λX. X  {x  B - B''. g x = X}) ` P'"
    using P' P'' = P''' by auto
  from this B  C = {}  show "P = P'"
    by (auto dest: injectivity_image_union[OF _ subset_C])
  have eq2: "(λX. X  {x  B - B'. f x = X}) ` P = (λX. X  {x  B - B'. g x = X}) ` P"
    using P = P' B' = B'' eq_image by simp
  from P have P_props: "X  P. X  C" "X  P. X  {}" by (auto elim: partition_onE)
  have invert: "XP. (X  {x  B - B'. f x = X})  C = X  (X  {x  B - B'. g x = X})  C = X"
    using B  C = {} P_props by auto
  have eq3: "X  P. (X  {x  B - B'. f x = X}) = (X  {x  B - B'. g x = X})"
    using injectivity_image[OF eq2 invert] by blast
  have eq4: "X  P. {x  B - B'. f x = X} = {x  B - B'. g x = X}"
  proof
    fix X
    assume "X  P"
    from this P have "X  C" by (auto elim: partition_onE)
    have disjoint: "X  {x  B - B'. f x = X} = {}" "X  {x  B - B'. g x = X} = {}"
      using B  C = {} X  C by auto
    from eq3 X  P have "X  {x  B - B'. f x = X} = X  {x  B - B'. g x = X}" by auto
    from this disjoint show "{x  B - B'. f x = X} = {x  B - B'. g x = X}"
      by (auto intro: injectivity_union)
  qed
  from eq4 f have eq5: "bB - B'. f b = g b" by blast
  from eq5 f B' = B'' P = P' show eq6: "f = g" by (auto intro: extensional_funcset_ext)
  from P P = P' show "j = j'" by simp
  from B' B' = B'' show "k = k'" by simp
qed

subsection ‹The Generalized Bell Recurrence Relation›

theorem Bell_eq:
  "Bell (n + m) = (kn. jm. j ^ (n - k) * Stirling m j * (n choose k) * Bell k)"
proof -
  define A where "A = {0..<n + m}"
  define B where "B = {0..<n}"
  define C where "C = {n..<n + m}"
  have "A = B  C" "B  C = {}" "finite B" "card B = n" "finite C" "card C = m"
    unfolding A_def B_def C_def by auto
  have step1: "Bell (n + m) = card {P. partition_on A P}"
    unfolding Bell_def A_def ..
  from A = B  C B  C = {} finite B finite C
  have step2: "card {P. partition_on A P} = card (construct_partition_on B C)"
    by (simp add: construct_partition_on)
  note injectivity = injectivity[OF B  C = {}]
  let ?expr = "do {
    k   {0..card B};
    j   {0..card C};
    P   {P. partition_on C P  card P = j};
    B'  {B'. B'  B  card B' = k};
    Q   {Q. partition_on B' Q};
    f   (B - B') E P;
    P'   {(λX. X  {x  B - B'. f x = X}) ` P};
    {P'  Q}
  }"
  let "?S  ?comp" = ?expr
  {
    fix k
    assume k: "k  {..card B}"
    let ?expr = "?comp k"
    let "?S  ?comp" = ?expr
    {
      fix j
      assume "j  {.. card C}"
      let ?expr = "?comp j"
      let "?S  ?comp" = ?expr
      from finite C have "finite ?S"
        by (intro finite_Collect_conjI disjI1 finitely_many_partition_on)
      {
        fix P
        assume P: "P  {P. partition_on C P  card P = j}"
        from this have "partition_on C P" by simp
        let ?expr = "?comp P"
        let "?S  ?comp" = ?expr
        have "finite P"
         using P finite C by (auto intro: finite_elements)
        from finite B have "finite ?S" by (auto simp add: finite_subset)
        moreover
        {
          fix B'
          assume B': "B'  {B'. B'  B  card B' = k}"
          from this have "B'  B" by simp
          let ?expr = "?comp B'"
          let "?S  ?comp" = ?expr
          from finite B have "finite B'"
            using B' by (auto simp add: finite_subset)
          from finite B' have "finite {Q. partition_on B' Q}"
            by (rule finitely_many_partition_on)
          moreover
          {
            fix Q
            assume Q: "Q  {Q. partition_on B' Q}"
            let ?expr = "?comp Q"
            let "?S  ?comp" = ?expr
            {
              fix f
              assume "f  B - B' E P"
              let ?expr = "?comp f"
              let "?S  ?comp" = ?expr
              have "disjoint_family_on ?comp ?S"
                by (auto intro: disjoint_family_onI)
              from this have "card ?expr = 1"
                by (simp add: card_bind_constant)
              moreover have "finite ?expr"
                by (simp add: finite_bind)
              ultimately have "finite ?expr  card ?expr = 1" by blast
            }
            moreover have "finite ?S"
              using finite B finite P by (auto intro: finite_PiE)
            moreover have "disjoint_family_on ?comp ?S"
              using P B' Q
              by (injectivity_solver rule: local.injectivity(1))
            moreover have "card ?S = j ^ (n - k)"
            proof -
              have "card (B - B') = n - k"
                using B' finite B' card B = n
                by (subst card_Diff_subset) auto
              from this show ?thesis
                using finite B P
                by (subst card_PiE) (simp add: prod_constant)+
            qed
            ultimately have "card ?expr = j ^ (n - k)"
              by (simp add: card_bind_constant)
            moreover have "finite ?expr"
              using finite ?S finite {P. partition_on C P  card P = j}
              by (auto intro!: finite_bind)
            ultimately have "finite ?expr  card ?expr = j ^ (n - k)" by blast
          } note inner = this
          moreover have "card ?S = Bell k"
            using B' finite B' by (auto simp add: Bell_altdef[symmetric])
          moreover have "disjoint_family_on ?comp ?S"
            using P B'
            by (injectivity_solver rule: local.injectivity(2))
          ultimately have "card ?expr = j ^ (n - k) * Bell k"
            by (subst card_bind_constant) auto
          moreover have "finite ?expr"
            using inner finite ?S by (auto intro: finite_bind)
          ultimately have "finite ?expr  card ?expr = j ^ (n - k) * Bell k" by blast
        } note inner = this
        moreover have "card ?S = n choose k"
          using card B = n finite B by (simp add: n_subsets)
        moreover have "disjoint_family_on ?comp ?S"
          using P
          by (injectivity_solver rule: local.injectivity(3))
        ultimately have "card ?expr = j ^ (n - k) * (n choose k) * Bell k"
          by (subst card_bind_constant) auto
        moreover have "finite ?expr"
          using inner finite ?S by (auto intro: finite_bind)
        ultimately have "finite ?expr  card ?expr = j ^ (n - k) * (n choose k) * Bell k" by blast
      } note inner = this
      moreover note finite ?S
      moreover have "card ?S = Stirling m j"
        using finite C card C = m by (simp add: card_partition_on)
      moreover have "disjoint_family_on ?comp ?S"
        by (injectivity_solver rule: local.injectivity(4))
      ultimately have "card ?expr = j ^ (n - k) * Stirling m j * (n choose k) * Bell k"
        by (subst card_bind_constant) auto
      moreover have "finite ?expr"
        using inner finite ?S by (auto intro: finite_bind)
      ultimately have "finite ?expr  card ?expr = j ^ (n - k) * Stirling m j * (n choose k) * Bell k" by blast
    } note inner = this
    moreover have "finite ?S" by simp
    moreover have "disjoint_family_on ?comp ?S"
      by (injectivity_solver rule: local.injectivity(5))
    ultimately have "card ?expr = (jm. j ^ (n - k) * Stirling m j * (n choose k) * Bell k)" (is "_ = ?formula")
      using card C = m by (subst card_bind) (auto intro: sum.cong)
    moreover have "finite ?expr"
      using inner finite ?S by (auto intro: finite_bind)
    ultimately have "finite ?expr  card ?expr = ?formula" by blast
  }
  moreover have "finite ?S" by simp
  moreover have "disjoint_family_on ?comp ?S"
    by (injectivity_solver rule: local.injectivity(6))
  ultimately have step3: "card (construct_partition_on B C) = (kn. jm. j ^ (n - k) * Stirling m j * (n choose k) * Bell k)"
    unfolding construct_partition_on_def
    using card B = n by (subst card_bind) (auto intro: sum.cong)
  from step1 step2 step3 show ?thesis by auto
qed

subsection ‹Corollaries of the Generalized Bell Recurrence›

corollary Bell_Stirling_eq:
  "Bell m = (jm. Stirling m j)"
proof -
  have "Bell m = Bell (0 + m)" by simp
  also have "... = (jm. Stirling m j)"
    unfolding Bell_eq[of 0] by (simp add: Bell_0)
  finally show ?thesis .
qed

corollary Bell_recursive_eq:
  "Bell (n + 1) = (kn. (n choose k) * Bell k)"
unfolding Bell_eq[of _ 1] by simp

subsection ‹Code equations for the computation of Bell numbers› (* contributed by Emin Karayel *)

text ‹It is slow to compute Bell numbers without dynamic programming (DP). The following is a DP 
algorithm derived from the previous recursion formula @{thm [source] Bell_recursive_eq}.›

fun Bell_list_aux :: "nat  nat list"
  where 
  "Bell_list_aux 0 = [1]" |
  "Bell_list_aux (Suc n) = (
    let prev_list = Bell_list_aux n; 
        next_val = ((k,z)  List.enumerate 0 prev_list. z * (n choose (n-k))) 
    in next_val#prev_list)"

definition Bell_list :: "nat  nat list"
  where "Bell_list n = rev (Bell_list_aux n)"

lemma bell_list_eq: "Bell_list n = map Bell [0..<n+1]"
proof -
  have "Bell_list_aux n = rev (map Bell [0..<Suc n])"
  proof (induction n)
    case 0
    then show ?case by (simp add:Bell_0)
  next
    case (Suc n)
    define x where "x = Bell_list_aux n"
    define y where "y = ((k,z)  List.enumerate 0 x. z * (n choose (n-k)))"
    define sn where "sn = n+1"
    have b:"x = rev (map Bell [0..<sn])"
      using Suc x_def sn_def by simp
    have c: "length x = sn"
      unfolding b by simp

    have "snd i = Bell (n - fst i)" if "i  set (List.enumerate 0 x)" for i
    proof -
      have "fst i < length x" "snd i = x ! fst i" 
        using iffD1[OF in_set_enumerate_eq that] by auto
      hence "snd i = Bell (sn - Suc (fst i))"
        unfolding b by (simp add:rev_nth)
      thus ?thesis
        unfolding sn_def by simp
    qed

    hence "y = (ienumerate 0 x. Bell (n - fst i) * (n choose (n - fst i)))"
      unfolding y_def by (intro arg_cong[where f="sum_list"] map_cong refl)  
        (simp add:case_prod_beta)
    also have "... = (imap fst (enumerate 0 x). Bell (n - i) * (n choose (n - i)))"
      by (subst map_map) (simp add:comp_def)
    also have "... = (i = 0..<length x. Bell (n-i) * (n choose (n-i)))"
      by (simp add:interv_sum_list_conv_sum_set_nat)
    also have "... = (in. Bell (n-i) * (n choose (n-i)))"
      using c sn_def by (intro sum.cong) auto
    also have "... = (i  (λk. n- k) ` {..n}. Bell i * (n choose i))"
      by (subst sum.reindex, auto simp add:inj_on_def)
    also have "... = (i  n. Bell i * (n choose i))"
      by (intro sum.cong refl iffD2[OF set_eq_iff] allI)
        (simp add:image_iff atMost_def, presburger)  
    also have "... = Bell (Suc n)"
      using Bell_recursive_eq by (simp add:mult.commute)
    finally have a: "y = Bell (Suc n)" by simp

    have "Bell_list_aux (Suc n) = y#x"
      unfolding x_def y_def by (simp add:Let_def)
    also have "... = Bell (Suc n)#(rev (map Bell [0..<Suc n]))"
      unfolding a b sn_def by simp
    also have "... = rev (map Bell [0..<Suc (Suc n)])"
      by simp
    finally show ?case by simp
  qed
  thus "Bell_list n = map Bell [0..<n+1]"
    by (simp add:Bell_list_def)
qed

lemma Bell_eval[code]: "Bell n = last (Bell_list n)"
  unfolding bell_list_eq by simp

end