theory Scratch
  imports "HOL-Computational_Algebra.Computational_Algebra"
begin

(* This should really go in the library *)
lemma tendsto_fpsI:
  assumes "\<And>m. eventually (\<lambda>x. fps_nth (f x) m = fps_nth g m) F"
  shows   "(f \<longlongrightarrow> g) F"
proof
  fix e :: real assume e: "e > 0"
  define m where "m = nat \<lceil>log 2 e\<rceil>"
  then obtain m where "2 ^ m > inverse e"
    by (metis ceiling_less_cancel ceiling_of_int  le_less
         le_less_trans nat_le_iff of_int_numeral of_int_power of_nat_less_two_power)
  with e have "inverse (2 ^ m) < e" by (simp add: field_simps)

  from assms have "eventually (\<lambda>x. \<forall>m'\<in>{..m}. fps_nth (f x) m' = fps_nth g m') F"
    by (subst eventually_ball_finite_distrib) auto
  thus "eventually (\<lambda>x. dist (f x) g < e) F"
  proof eventually_elim
    case (elim x)
    show ?case
    proof (cases "f x = g")
      case False
      hence "subdegree (f x - g) \<ge> m" using elim
        by (intro subdegree_geI) auto
      hence "dist (f x) g \<le> inverse (2 ^ m)" by (simp add: dist_fps_def)
      also have "\<dots> < e" by fact
      finally show ?thesis .
    qed (insert e, auto)
  qed
qed


text \<open>
  Decompose a natural number into bits, i.e. \<open>[a\<^sub>1 * 2 ^ 0, a\<^sub>2 * 2 ^ 1, \<dots>]\<close> where
  each of the \<open>a\<^sub>i\<close> are either 0 or 1.
\<close>
fun bitvec :: "nat \<Rightarrow> nat \<Rightarrow> nat list" where
  "bitvec 0 _ = []"
| "bitvec (Suc n) x = (x mod 2) # map (\<lambda>x. x * 2) (bitvec n (x div 2))"

lemma length_bitvec [simp]: "length (bitvec n x) = n"
  by (induction n x rule: bitvec.induct) simp_all

lemma sum_list_bitvec [simp]: "x < 2 ^ n \<Longrightarrow> sum_list (bitvec n x) = x"
proof (induction n x rule: bitvec.induct)
  case (2 n x)
  hence "x < 2 * 2 ^ n" by simp
  hence "x div 2 < 2 ^ n" by linarith
  from "2.IH"[OF this] show ?case by (simp add: sum_list_mult_const)
qed simp_all

lemma natpermute_Suc:
  "natpermute m (Suc n) = {k # v |k v. k \<le> m \<and> v \<in> natpermute (m - k) n}"
  by (auto simp: natpermute_def length_Suc_conv)

text \<open>
  This set is the set of all exponent vectors that can contribute to the \<open>m\<close>-th
  coefficient of the \<open>n\<close>-th partial product of our FPS.

  The key insight is that this set is a singleton set consisting of the unique
  bit vector of \<open>m\<close> if \<open>n\<close> is large enough, and empty otherwise.
\<close>
definition A where "A = (\<lambda>m n. {v. v \<in> natpermute m n \<and> (\<forall>j\<in>{0..<n}. v ! j \<in> {0, 2 ^ j})})"

lemma A_Suc: "A m (Suc n) = (\<lambda>v. m mod 2 # map (\<lambda>x. x * 2) v) ` A (m div 2) n"
proof safe
  fix v assume v: "v \<in> A m (Suc n)"
  have nth: "v ! j \<in> {0, 2 ^ j}" if j: "j < Suc n" for j
    using that v by (auto simp: A_def)
  from v obtain x v' where v': "v = x # v'" "v' \<in> natpermute (m - x) n"
    by (auto simp: A_def natpermute_Suc)
  define v'' where "v'' = map (\<lambda>x. x div 2) v'"
  from v' have [simp]: "length v' = n" by (auto simp: natpermute_def)
  have "even (v' ! j)" if "j < n" for j
    using that nth[of "Suc j"] by (auto simp: v')
  hence even: "\<forall>y\<in>set v'. even y" by (auto simp: set_conv_nth)
  hence even': "even (sum_list v')" by (induction v') auto
  hence mod: "sum_list v' mod 2 = 0" by simp

  from v have "m = sum_list v" by (simp add: A_def natpermute_def)
  hence "m mod 2 = (x + sum_list v') mod 2" by (simp add: v')
  also have "\<dots> = x mod 2" using mod
    by (subst mod_add_right_eq [symmetric]) simp
  also have "\<dots> = x"
    using nth[of 0] by (intro mod_less) (auto simp: v')
  finally have [simp]: "x = m mod 2" ..

  {
    have "(\<Sum>x\<leftarrow>v'. x div 2) = sum_list v' div 2" using even
      by (induction v') auto
    moreover have "(m mod 2 + sum_list v') div 2 = sum_list v' div 2"
      using even' by presburger
    ultimately have "sum_list v'' = m div 2" using v
      by (simp add: v' v''_def A_def natpermute_def)
  }
  moreover have "v'' ! j \<in> {0, 2 ^ j}" if "j < n" for j
    using nth[of "Suc j"] that by (auto simp: v''_def v')
  moreover have "length v'' = n" by (simp add: v''_def)
  ultimately have "v'' \<in> A (m div 2) n" using nth[of "Suc j" for j]
    by (auto simp: A_def natpermute_def o_def)
  moreover have "map (\<lambda>x. x * 2) v'' = v'" unfolding v''_def map_map o_def
    using even by (intro map_idI) auto
  ultimately show "v \<in> (\<lambda>v. m mod 2 # map (\<lambda>x. x * 2) v) ` A (m div 2) n"
    by (auto simp: v')
next
  fix v assume "v \<in> A (m div 2) n"
  thus "m mod 2 # map (\<lambda>x. x * 2) v \<in> A m (Suc n)"
    by (auto simp: A_def natpermute_def sum_list_mult_const nth_Cons split: nat.splits)
qed

lemma A_0: "A m 0 = (if m = 0 then {[]} else {})"
  by (auto simp: A_def natpermute_0)

lemma A_eq:
  "A m n = (if m < 2 ^ n then {bitvec n m} else {})"
  by (induction n m rule: bitvec.induct) (auto simp: A_Suc A_0)

text \<open>
  The key result: All coefficients of our product are eventually 1.
\<close>
lemma fps_nth_myprod:
  "fps_nth (\<Prod>k=0..n. 1 + fps_X ^ (2 ^ k) :: real fps) m = (if m < 2 ^ Suc n then 1 else 0)"
proof -
  have "fps_nth (\<Prod>k=0..n. 1 + fps_X ^ (2 ^ k) :: real fps) m =
          (\<Sum>v\<in>natpermute m (Suc n). \<Prod>j = 0..n. 
             if v ! j = 0 \<or> v ! j = 2 ^ j then 1 else 0)" unfolding fps_prod_nth
    by (intro sum.cong prod.cong refl) (auto split: if_splits intro: Nat.gr0I)
  also have "\<dots> = (\<Sum>v\<in>natpermute m (Suc n). if (\<forall>j\<in>{0..n}. v ! j = 0 \<or> v ! j = 2 ^ j) then 1 else 0)"
    by (intro sum.cong refl) auto
  also have "\<dots> = (\<Sum>v | v \<in> natpermute m (Suc n) \<and> (\<forall>j\<in>{0..n}. v ! j = 0 \<or> v ! j = 2 ^ j). 1)"
    by (intro sum.mono_neutral_cong_right natpermute_finite) auto
  also have "\<dots> = card (A m (Suc n))" by (simp add: A_def atLeastLessThanSuc_atLeastAtMost)
  also have "\<dots> = (if m < 2 ^ Suc n then 1 else 0)"
    by (simp add: A_eq)
  finally show ?thesis .
qed

lemma myprod: "(\<lambda>n. \<Prod>k=0..n. 1 + fps_X ^ (2 ^ k) :: real fps) \<longlonglongrightarrow> Abs_fps (\<lambda>_. 1)"
proof (rule tendsto_fpsI, goal_cases)
  case (1 m)
  have "eventually (\<lambda>n. n \<ge> m) sequentially" by (rule eventually_ge_at_top)
  thus ?case
  proof eventually_elim
    case (elim n)
    note \<open>m \<le> n\<close>
    also have "n < 2 ^ n" by (induction n) auto
    also have "\<dots> \<le> 2 ^ Suc n" by simp
    finally have "m < 2 ^ Suc n" .
    thus ?case by (subst fps_nth_myprod) auto
  qed
qed

end