Theory Digit_Expansions.Bits_Digits

section ‹Digit functions›

theory Bits_Digits
  imports Main
begin

text ‹We define the n-th bit of a number in base 2 representation ›
definition nth_bit :: "nat  nat  nat" (infix ¡ 100) where
  "nth_bit num k = (num div (2 ^ k)) mod 2"

lemma nth_bit_eq_of_bool_bit:
  nth_bit num k = of_bool (bit num k)
  by (simp add: nth_bit_def bit_iff_odd mod_2_eq_odd)

text ‹as well as the n-th digit of a number in an arbitrary base ›
definition nth_digit :: "nat  nat  nat  nat" where
  "nth_digit num k base = (num div (base ^ k)) mod base"

text ‹In base 2, the two definitions coincide. ›
lemma nth_digit_base2_equiv:"nth_bit a k = nth_digit a k (2::nat)"
  by (auto simp add:nth_bit_def nth_digit_def)

lemma general_digit_base:
  assumes "t1 > t2" and "b>1"
  shows "nth_digit (a * b^t1) t2 b = 0" 
proof -
  have 1: "b^t1 div b^t2 = b^(t1-t2)" using assms apply auto
    by (metis Suc_lessD less_imp_le less_numeral_extra(3) power_diff)
  have "b^t2 dvd b^t1" using `t1 > t2`
    by (simp add: le_imp_power_dvd)
  hence "(a * b^t1) div b^t2 = a * b^(t1-t2)" using div_mult_swap[of "b^t2" "b^t1" "a"] 1 by auto
  thus ?thesis using nth_digit_def assms by auto
qed

lemma nth_bit_bounded: "nth_bit a k  1"
  by (auto simp add: nth_bit_def)

lemma nth_digit_bounded: "b>1  nth_digit a k b  b-1"
  apply (auto simp add: nth_digit_def)
  using less_Suc_eq_le by fastforce

lemma obtain_smallest: "P (n::nat)  kn. P k  (a<k.¬(P a))"
  by (metis ex_least_nat_le not_less_zero zero_le)

subsection ‹Simple properties and equivalences›

text ‹Reduce the @{term nth_digit} function to @{term nth_bit} if the base is a power of 2›

lemma digit_gen_pow2_reduct:
  (nth_digit a t (2 ^ c)) ¡ k = a ¡ (c * t + k) if k < c
proof -
  have moddiv: "(x mod 2 ^ c) ¡ k = x ¡ k" for x
  proof-
    define n where n = c - k
    with k < c have c_nk: c = n + k
      by simp
    obtain a b where x_def: "x = a * 2 ^ c + b" and "b < 2 ^ c" 
      by (meson mod_div_decomp mod_less_divisor zero_less_numeral zero_less_power)
    then have bk: "(x mod 2 ^ c) ¡ k = b ¡ k" by simp
    from b < 2 ^ c have x div 2 ^ k = a * 2 ^ (c - k) + b div 2 ^ k
      by (simp add: x_def c_nk power_add flip: mult.commute [of 2 ^ k] mult.left_commute [of 2 ^ k])
    then have "x ¡ k = (a*2^(c-k) + b div 2^k) mod 2" by (simp add: nth_bit_def)
    then have "x ¡ k = b ¡ k" using nth_bit_def k < c by (simp add: mod2_eq_if)
    then show ?thesis using nth_bit_def bk by linarith
  qed
  have "a div ((2 ^ c) ^ t * 2 ^ k) = a div (2 ^ c) ^ t div 2 ^ k" using div_mult2_eq by blast
  moreover have "a div (2 ^ c) ^ t mod 2 ^ c div 2 ^ k mod 2 = a div (2 ^ c) ^ t div 2 ^ k mod 2"
    using moddiv nth_bit_def by auto 
  ultimately show "(nth_digit a t (2^c)) ¡ k = a ¡ (c*t+k)"
    using nth_digit_def nth_bit_def by (auto simp: power_add power_mult)
qed

text ‹Show equivalence of numbers by equivalence of all their bits (digits)›

lemma aux_even_pow2_factor: "a > 0  k b. ((a::nat) = (2^k) * b  odd b)"
proof(induction  a rule: full_nat_induct)
  case (1 n)
  then show ?case
  proof (cases "odd n")
    case True
    then show ?thesis by (metis nat_power_eq_Suc_0_iff power_Suc power_Suc0_right power_commutes)
  next
    case False
    have "(t. n = 2 * t)" using False by auto
    then obtain t where n_def:"n = 2 * t" ..
    then have "t < n" using "1.prems" by linarith
    then have ih:"r s. t = 2^r * s  odd s" using 1 n_def by simp
    then have "r s. n = 2^(Suc r) * s" using n_def by auto
    then show ?thesis by (metis ih n_def power_commutes semiring_normalization_rules(18)
                          semiring_normalization_rules(28))
  qed
qed

lemma aux0_digit_wise_equiv:"a > 0  (k. nth_bit a k = 1)"
proof -
  assume a_geq_0: "a > 0"
  consider (odd) "a mod 2 = 1" | (even) "a mod 2 = 0" by force
  then show ?thesis
  proof(cases)
    case odd
    then show ?thesis by (metis div_by_1 nth_bit_def power_0)
  next
    case even
    then have bk_def:"k b. (a = (2^k) * b  odd b)"
      using aux_even_pow2_factor a_geq_0 by simp
    then obtain b k where bk_cond:"(a = (2^k) * b  odd b)" by blast
    then have "b = a div (2^k)" by simp
    then have digi_b:"nth_bit b 0 = 1" using bk_def
      using bk_cond nth_bit_def odd_iff_mod_2_eq_one by fastforce
    then have "nth_bit a k = (nth_bit b 0)" using nth_bit_def bk_cond by force
    then have "nth_bit a k = 1" using digi_b by simp
    then show ?thesis by blast
  qed
qed

lemma aux1_digit_wise_equiv:"(k.(nth_bit a k = 0))  a = 0" (is "?P  ?Q")
proof
  assume "?Q"
  then show "?P" by (simp add: nth_bit_def)
next
  {
    assume a_neq_0:"¬?Q"
    then have "a > 0" by blast
    then have "¬?P" using aux0_digit_wise_equiv by (metis zero_neq_one)
  }
  thus "?P  ?Q" by blast
qed

lemma aux2_digit_wise_equiv: "(r<k. nth_bit a r = 0)  (a mod 2^k = 0)"
proof(induct k)
  case 0
  then show ?case
    by (auto simp add: nth_bit_def)
next
  case (Suc k)
  then show ?case
    by (auto simp add: nth_bit_def)
       (metis dvd_imp_mod_0 dvd_mult_div_cancel dvd_refl even_iff_mod_2_eq_zero
        lessI minus_mod_eq_div_mult minus_mod_eq_mult_div mult_dvd_mono)
qed

lemma digit_wise_equiv: "(a = b)  (k. nth_bit a k = nth_bit b k)" (is "?P  ?Q")
proof
  assume "?P"
  then show "?Q" by simp
next
  {
    assume notP: "¬?P"
    have "¬(k. nth_bit a k = nth_bit b k)" if ab: "a<b" for a b
    proof-
      define c::nat where "c = b - a"
      have b: "a+c=b" by (auto simp add: c_def "ab" less_imp_le)
      have  "k.(nth_bit c k = 1)" using nth_bit_def aux1_digit_wise_equiv
        by (metis c_def not_less0 not_mod_2_eq_1_eq_0 that zero_less_diff)
      then obtain k where k1:"nth_bit c k = 1" and k2:"r < k. (nth_bit c r  1)"
        by (auto dest: obtain_smallest)
      then have cr0: "r < k. (nth_bit c r = 0)" by (simp add: nth_bit_def)
      from aux2_digit_wise_equiv cr0 have "c mod 2^k = 0" by auto
      then have "a div 2 ^ k mod 2  b div 2 ^ k mod 2"
        by auto (metis b div_plus_div_distrib_dvd_right even_add k1 nth_bit_def odd_iff_mod_2_eq_one)
      then show ?thesis by (auto simp add: nth_bit_def)
    qed
    from this [of a b] this [of b a] notP have "k. nth_bit a k = nth_bit b k  a = b"
      using linorder_neqE_nat by auto
  }
  then show "?Q ==> ?P" by auto
qed

text ‹Represent natural numbers in their binary expansion›

lemma aux3_digit_sum_repr:
  assumes "b < 2^r"
  shows "(a*2^r + b) ¡ r = (a*2^r) ¡ r"
  by (auto simp add: nth_bit_def assms)

lemma aux2_digit_sum_repr:
  assumes "n < 2^c" "r < c"
  shows "(a*2^c+n) ¡ r = n ¡ r"
proof -
  have [simp]: a*(2::nat) ^ c div 2 ^ r = a*2 ^ (c - r)
    using assms(2)
    by (auto simp: less_iff_Suc_add
          monoid_mult_class.power_add ac_simps)
  show ?thesis
    using assms
    by (auto simp add: nth_bit_def
            div_plus_div_distrib_dvd_left
            le_imp_power_dvd
          simp flip: mod_add_left_eq)
qed

lemma aux1_digit_sum_repr:
assumes "n < 2^c" "r<c"
shows "(k<c.((n ¡ k)*2^k)) ¡ r = n ¡ r"
proof-
  define a where "a  (k=0..<Suc(r).((n ¡ k)*2^k))"
  define d where "d  (k=Suc(r)..<c.((n ¡ k)*2^k))"
  define e where "e  (k=Suc r..<c.((n ¡ k)*2^(k-Suc(r))))"
  define b where "b  (k=0..<r.((n ¡ k)*2^k))"
  have ad: "(k=0..<c.((n ¡ k)*2^k)) = a + d"
    using a_def d_def assms
    by (metis (no_types, lifting) Suc_leI a_def assms(2) d_def sum.atLeastLessThan_concat zero_le)
  have "d = (k=Suc(r)..<c.(2^(Suc r) * (n ¡ k *  2^(k - Suc r))))"
    using d_def apply (simp)
    apply (rule sum.cong; auto simp: algebra_simps)
    by (metis add_Suc le_add_diff_inverse numerals(2) power_Suc power_add)
  hence d2r: "d = 2^Suc(r)*e" using d_def e_def
     sum_distrib_left[of "2^(Suc r)" "λk. (n ¡ k) *  2^(k - Suc r)" "{Suc r..<c}"] by auto
  have "(k<c.((n ¡ k)*2^k)) = a +2^Suc(r)*e" by (simp add: d2r ad lessThan_atLeast0)
  moreover have "(k=0..<Suc(r).((n ¡ k)*2^k)) < 2 ^ Suc(r)" using assms
  proof(induct r)
    case 0
    then show ?case
    proof -
      have "n ¡ 0 < Suc 1" 
        by (metis (no_types) atLeastLessThan_empty atLeastLessThan_iff lessI linorder_not_less 
                  nth_bit_bounded)
      then show ?thesis
        by simp
    qed
    next
      case (Suc r)
      have r2: "n ¡ Suc(r) *  2 ^ Suc(r)   2 ^ Suc(r)" using nth_bit_bounded by simp
      have "(k=0..<Suc(r).((n ¡ k)*2^k)) < 2 ^ Suc(r)" 
        using Suc.hyps using Suc.prems(2) Suc_lessD assms(1) by blast
      then show ?case using "r2" 
        by (smt (verit) Suc_leI Suc_le_lessD add_Suc add_le_mono mult_2 power_Suc sum.atLeast0_lessThan_Suc)
    qed
    then have "a < 2 ^Suc(r)" using a_def by blast
  ultimately have ar:"(a+d) ¡ r = a ¡ r" using d2r
    by (metis (no_types, lifting) aux2_digit_sum_repr lessI semiring_normalization_rules(24) 
              semiring_normalization_rules(7))
    (* Second part of proof *)
  have ab: "a =(n ¡ r)*2^r + b" using a_def b_def d_def by simp
  have "(k=0..<r.((n ¡ k)*2^k)) <2^r"
  proof(induct r)
    case 0
      then show ?case by auto
    next
      case (Suc r)
      have r2: "n ¡ r *  2 ^ r   2 ^ r" using nth_bit_bounded by simp
      have "(k = 0..<r. n ¡ k * 2 ^ k) < 2^r" using Suc.hyps by auto
      then show ?case apply simp using "r2" by linarith
  qed
  then have b: "b < 2^r" using b_def by blast
  then have "a ¡ r = ((n ¡ r)*2^r) ¡ r" using ab aux3_digit_sum_repr by simp
  then have "a ¡ r = (n ¡ r)" using nth_bit_def by simp
  then show ?thesis using ar a_def by (simp add: ad lessThan_atLeast0)
qed

lemma digit_sum_repr:
  assumes "n < 2^c"
  shows "n = (k < c.((n ¡ k) * 2^k))"
proof -
  have "k. (ck  n<2^k)" using assms less_le_trans by fastforce
  then have nik: "k.( k c  (n ¡ k = 0))"  by (auto simp add: nth_bit_def)
  have "(r<c.((n ¡ r)*(2::nat)^r))<(2::nat)^c"
  proof (induct c)
    case 0
    then show ?case by simp
  next
    case (Suc c)
    then show ?case
      using nth_bit_bounded
            add_mono_thms_linordered_field[of "(n ¡ c)* 2 ^ c" " 2 ^ c" "(r<c. n ¡ r * 2 ^ r)" "2^c"]
      by simp
  qed
  then have "k. k c  (r<c.((n ¡ r)*2^r)) ¡ k = 0"
    using less_le_trans by (auto simp add: nth_bit_def) fastforce
  then have "rc.(n ¡ r  = (k<c.((n ¡ k)*2^k)) ¡ r)" by (simp add: nik)
  moreover have "r<c.(n ¡ r  = (k<c.((n ¡ k)*2^k)) ¡ r)" using aux1_digit_sum_repr assms by simp
  ultimately have "r.(k<c.((nth_bit n k)*2^k)) ¡ r = n ¡ r " by (metis not_less)
  then show ?thesis using digit_wise_equiv by presburger
qed

lemma digit_sum_repr_variant:
  "n =(k<n.((nth_bit n k)*2^k))"
  using less_exp digit_sum_repr by auto

lemma digit_sum_index_variant:
  "r>n  ((k< n.((n ¡ k)*2^k)) = (k< r.(n ¡ k)*2^k))"
proof-
  have "r.(2^r > r)" using less_exp by simp
  then have pow2: "r.(r>n  2^r>n)" using less_trans by blast
  then have "r.(r > n  (n ¡ r = 0))" by (auto simp add: nth_bit_def)
  then have "r. r > n  (n ¡ r)*2^r = 0" by auto
  then show ?thesis using digit_sum_repr digit_sum_repr_variant pow2 by auto
qed

text ‹Digits are preserved under shifts›

lemma digit_shift_preserves_digits:
  assumes "b>1" 
  shows "nth_digit (b * y) (Suc t) b = nth_digit y t b" 
  using nth_digit_def assms by auto

lemma digit_shift_inserts_zero_least_siginificant_digit:
  assumes "t>0" and "b>1"
  shows "nth_digit (1 + b * y) t b = nth_digit (b * y) t b" 
  using nth_digit_def assms apply auto
proof -
  assume "0 < t"
  assume "Suc 0 < b"
  hence "Suc (b * y) mod b = 1"
    by (simp add: Suc_times_mod_eq)
  hence "b * y div b = Suc (b * y) div b"
    using b>1 by (metis (no_types) One_nat_def diff_Suc_Suc gr_implies_not0 minus_mod_eq_div_mult 
                 mod_mult_self1_is_0 nonzero_mult_div_cancel_right)
  then show "Suc (b * y) div b ^ t mod b = b * y div b ^ t mod b"
    using t>0 by (metis Suc_pred div_mult2_eq power_Suc)
qed

text ‹Represent natural numbers in their base-b digitwise expansion›

lemma aux3_digit_gen_sum_repr:
  assumes "d < b^r" and "b > 1"
  shows "nth_digit (a*b^r + d) r b = nth_digit (a*b^r) r b"
  using b>1 by (auto simp: nth_digit_def assms)

lemma aux2_digit_gen_sum_repr:
  assumes "n < b^c" "r < c"
  shows "nth_digit (a*b^c+n) r b = nth_digit n r b"
proof -
  have [simp]: a*b ^ c div b ^ r = a*b ^ (c - r)
    using assms(2)
    by (auto simp: less_iff_Suc_add
          monoid_mult_class.power_add ac_simps)
  show ?thesis
    using assms
    by (auto simp add: nth_digit_def
            div_plus_div_distrib_dvd_left
            le_imp_power_dvd
          simp flip: mod_add_left_eq) 
qed

lemma aux1_digit_gen_sum_repr:
assumes "n < b^c" "r<c" and "b>1"
shows "nth_digit (k<c.((nth_digit n k b)*b^k)) r b = nth_digit n r b"
proof-
  define a where "a  (k=0..<Suc(r).((nth_digit n k b)*b^k))"
  define d where "d  (k=Suc(r)..<c.((nth_digit n k b)*b^k))"
  define e where "e  (k=Suc r..<c.((nth_digit n k b)*b^(k-Suc(r))))"
  define f where "f  (k=0..<r.((nth_digit n k b)*b^k))"
  have ad: "(k=0..<c.((nth_digit n k b)*b^k)) = a + d"
    using a_def d_def assms
    by (metis (no_types, lifting) Suc_leI a_def assms(2) d_def sum.atLeastLessThan_concat zero_le)
  have "d = (k=Suc(r)..<c.(b^(Suc r) * (nth_digit n k b * b^(k - Suc r))))" 
    using d_def apply (auto) apply (rule sum.cong; auto simp: algebra_simps)
    by (metis add_Suc le_add_diff_inverse power_Suc power_add)
  hence d2r: "d = b^Suc(r)*e" using d_def e_def sum_distrib_left[of "b^(Suc r)" 
                          "λk. (nth_digit n k b) *  b^(k - Suc r)" "{Suc r..<c}"] by auto
  have "(k<c.((nth_digit n k b)*b^k)) = a +b^Suc(r)*e" 
    by (simp add: d2r ad lessThan_atLeast0)
  moreover have "(k=0..<Suc(r).((nth_digit n k b)*b^k)) < b ^ Suc(r)" using assms
  proof(induct r)
    case 0
    then show ?case
    proof -
      have "nth_digit n 0 b < b" 
        using nth_digit_bounded[of "b" "n" "0"] b>1 by auto
      then show ?thesis
        by simp
    qed
    next
      case (Suc r)
      have r2: "(nth_digit n (Suc r) b) * b ^ Suc(r)  (b-1) * b ^ Suc(r)" 
        using nth_digit_bounded[of "b" "n" "Suc r"] b>1 by auto
      moreover have "(k=0..<Suc(r).((nth_digit n k b)*b^k)) < b ^ Suc(r)" 
        using Suc.hyps using Suc.prems(2) Suc_lessD assms(1) b>1 by blast
      ultimately have "(nth_digit n (Suc r) b) * b ^ Suc(r) 
                     + (k=0..<Suc(r).((nth_digit n k b)*b^k)) < b ^ Suc (Suc r)" 
        using assms(3) mult_eq_if by auto 
      then show ?case by auto
    qed
    hence "a < b^Suc(r)" using a_def by blast
  ultimately have ar:"nth_digit (a+d) r b = nth_digit a r b" using d2r
    by (metis (no_types, lifting) aux2_digit_gen_sum_repr lessI semiring_normalization_rules(24) 
              semiring_normalization_rules(7))
    (* Second part of proof *)
  have ab: "a =(nth_digit n r b)*b^r + f" using a_def f_def d_def by simp
  have "(k=0..<r.((nth_digit n k b)*b^k)) < b^r"
  proof(induct r)
    case 0
      then show ?case by auto
    next
      case (Suc r)
      have r2: "nth_digit n r b * b ^ r  (b-1) * b ^ r" 
        using nth_digit_bounded[of "b"] b>1 by auto
      have "(k = 0..<r. nth_digit n k b * b ^ k) < b^r" using Suc.hyps by auto
      then show ?case using "r2" assms(3) mult_eq_if by auto
  qed
  hence f: "f < b^r" using f_def by blast
  hence "nth_digit a r b = (nth_digit (nth_digit n r b * b^r) r b)" 
    using ab aux3_digit_gen_sum_repr b>1 by simp
  hence "nth_digit a r b = nth_digit n r b" 
    using nth_digit_def b>1 by simp
  then show ?thesis using ar a_def by (simp add: ad lessThan_atLeast0)
qed

lemma aux_gen_b_factor: "a > 0  b>1  k c. ((a::nat) = (b^k) * c  ¬(c mod b = 0))"
proof(induction  a rule: full_nat_induct)
  case (1 n)
  show ?case 
  proof(cases "n mod b = 0")
    case True
    then obtain t where n_def: "n = b * t" by blast
    hence "t < n"
      using 1 by auto 
    with 1 have ih:"r s. t = b^r * s  ¬(s mod b = 0)"
      by (metis Suc_leI gr0I mult_0_right n_def) 
    hence "r s. n = b^(Suc r) * s" using n_def by auto
    then show ?thesis by (metis ih mult.commute mult.left_commute n_def power_Suc)
  next
    case False
    then show ?thesis by (metis mult.commute power_0 power_Suc power_Suc0_right)
  qed
qed

lemma aux0_digit_wise_gen_equiv:
  assumes "b>1" and a_geq_0: "a > 0"
  shows "(k. nth_digit a k b  0)"
proof(cases "a mod b = 0")
  case True
  hence "k c. a = (b^k) * c  ¬(c mod b = 0)"
    using aux_gen_b_factor a_geq_0 assms by simp
  then obtain c k where ck_cond:"a = (b^k) * c  ¬(c mod b = 0)" by blast
  hence c_cond:"c = a div (b^k)" using a_geq_0 by auto
  hence digi_b:"nth_digit c 0 b  0"
    using ck_cond nth_digit_def by force
  hence "nth_digit a k b = nth_digit c 0 b" 
    using nth_digit_def c_cond by simp
  hence "nth_digit a k b  0" using digi_b by simp
  then show ?thesis by blast next
  case False
  then show ?thesis
    by (metis div_by_1 nth_digit_def power.simps(1))
qed

lemma aux1_digit_wise_gen_equiv:
  assumes "b>1"
  shows "(k.(nth_digit a k b = 0))  a = 0" (is "?P  ?Q")
proof
  assume "?Q"
  then show "?P" by (simp add: nth_digit_def)
next
  {
    assume a_neq_0:"¬?Q"
    hence "a > 0" by blast
    hence "¬?P" using aux0_digit_wise_gen_equiv b>1 by auto
  } from this show "?P  ?Q" by blast
qed

lemma aux2_digit_wise_gen_equiv: "(r<k. nth_digit a r b = 0)  (a mod b^k = 0)"
proof(induct k)
  case 0
  then show ?case by auto
next
  case (Suc k)
  then show ?case apply(auto simp add: nth_digit_def)
    using dvd_imp_mod_0 dvd_mult_div_cancel dvd_refl
        lessI minus_mod_eq_div_mult minus_mod_eq_mult_div mult_dvd_mono
    by (metis mod_0_imp_dvd)
qed

text ‹Two numbers are the same if and only if their digits are the same›

lemma digit_wise_gen_equiv: 
  assumes "b>1"
  shows "(x = y)  (k. nth_digit x k b = nth_digit y k b)" (is "?P  ?Q")
proof
  assume "?P"
  then show "?Q" by simp
next{
    assume notP: "¬?P"
    have"¬(k. nth_digit x k b = nth_digit y k b)" if xy: "x<y" for x y
    proof-
      define c::nat where "c = y - x"
      have y: "x+c=y" by (auto simp add: c_def "xy" less_imp_le)
      have  "k.(nth_digit c k b  0)" 
        using nth_digit_def b>1 aux0_digit_wise_gen_equiv 
        by (metis c_def that zero_less_diff)
      then obtain k where k1:"nth_digit c k b  0" 
                      and k2:"r < k. (nth_digit c r b = 0)"
        apply(auto dest: obtain_smallest) done
      hence cr0: "r < k. (nth_digit c r b = 0)" by (simp add: nth_digit_def)
      from aux2_digit_wise_gen_equiv cr0 have "c mod b^k = 0" by auto
      hence "x div b ^ k mod b  y div b ^ k mod b"
        using y k1 b>1 aux1_digit_wise_gen_equiv[of "b" "c"] nth_digit_def apply auto
                proof - (* this ISAR proof was found by sledgehammer  *)
                        fix ka :: nat
                        assume a1: "b ^ k dvd c"
                        assume a2: "x div b ^ k mod b = (x + c) div b ^ k mod b"
                        assume a3: "y = x + c"
                        assume a4: "num k base. nth_digit num k base 
                                    = num div base ^ k mod base"
                have f5: "n na. (na::nat) + n - na = n"
                  by simp
                  have f6: "x div b ^ k + c div b ^ k = y div b ^ k"
                    using a3 a1 by (simp add: add.commute div_plus_div_distrib_dvd_left)
                  have f7: "n. (x div b ^ k + n) mod b = (y div b ^ k + n) mod b"
                    using a3 a2 by (metis add.commute mod_add_right_eq)
                  have "n na nb. ((nb::nat) mod na + n - (nb + n) mod na) mod na = 0"
                    by (metis (no_types) add.commute minus_mod_eq_mult_div mod_add_right_eq 
                        mod_mult_self1_is_0)
                  then show "c div b ^ ka mod b = 0"
                    using f7 f6 f5 a4 by (metis (no_types) k1)
                qed
      then show ?thesis by (auto simp add: nth_digit_def)
    qed
    from this [of x y] this [of y x] notP 
      have "k. nth_digit x k b = nth_digit y k b  x = y" apply(auto)
      using linorder_neqE_nat by blast}then show "?Q ==> ?P" by auto
qed

text ‹A number is equal to the sum of its digits multiplied by powers of two›

lemma digit_gen_sum_repr:
  assumes "n < b^c" and "b>1"
  shows "n = (k < c.((nth_digit n k b) * b^k))"
proof -
  have 1: "(ck  n<b^k)" for k using assms less_le_trans by fastforce
  hence nik: "ck  (nth_digit n k b = 0)" for k 
    by (auto simp add: nth_digit_def)
  have "(r<c.((nth_digit n r b)*b^r))<b^c" apply(induct c, auto)
    subgoal for c
    proof -
      assume IH: "(r<c. nth_digit n r b * b ^ r) < b ^ c"
      have bound: "(nth_digit n c b) * b ^ c  (b-1) * b^c" 
        using nth_digit_bounded b>1 by auto
      thus ?thesis using assms IH
        by (metis (no_types, lifting) bound add_mono_thms_linordered_field(1) 
            add_mono_thms_linordered_field(5) le_less mult_eq_if not_one_le_zero)
    qed
    done
  hence "kc  nth_digit (r<c.((nth_digit n r b)*b^r)) k b = 0" for k
    apply(auto simp add: nth_digit_def) using less_le_trans assms(2) by fastforce 
  hence "rc.(nth_digit n r b 
    = nth_digit (k<c.((nth_digit n k b)*b^k)) r b)" by (simp add: nik)
  moreover have "r<c.(nth_digit n r b 
               = nth_digit (k<c.((nth_digit n k b) * b^k)) r b)" 
    using aux1_digit_gen_sum_repr assms by simp
  ultimately have "r. nth_digit (k<c.((nth_digit n k b)*b^k)) r b 
                    = nth_digit n r b" by (metis not_less)
  then show ?thesis 
    using digit_wise_gen_equiv[of "b" "(k<c. nth_digit n k b * b ^ k)" "n"] b>1 by auto 
qed

lemma digit_gen_sum_repr_variant:
  assumes "b>1"
  shows "n = (k<n.((nth_digit n k b)*b^k))"
proof-
  have "n < b^n" using b>1 apply (induct n, auto) by (simp add: less_trans_Suc) 
  then show ?thesis using digit_gen_sum_repr b>1 by auto
qed

lemma digit_gen_sum_index_variant:
  assumes "b>1" shows "r>n  
  (k< n.((nth_digit n k b )*b^k)) = (k< r.(nth_digit n k b)*b^k)"
proof -
  assume "r>n"
  have "b^r > r" for r using b>1  by (induction r, auto simp add: less_trans_Suc)
  hence powb: "r.(r>n  b^r>n)" using less_trans by auto
  hence "r > n  (nth_digit n r b = 0)" for r 
    by (auto simp add: nth_digit_def)
  hence "r > n  (nth_digit n r b) * b^r = 0" for r by auto
  then show ?thesis using digit_gen_sum_repr digit_gen_sum_repr_variant powb n < r assms by auto
qed

text @{text nth_digit} extracts coefficients from a base-b digitwise expansion›

lemma nth_digit_gen_power_series:
  fixes c b k q
  defines "b  2^(Suc c)"
  assumes bound: "k. (f k) < b" (* < 2^c makes proof easier, but is too strong for const f *)
  shows "nth_digit (k=0..q. (f k) * b^k) t b = (if tq then (f t) else 0)"
proof (induction q arbitrary: t)
  case 0
  have "b>1" using b_def
    using one_less_numeral_iff power_gt1 semiring_norm(76) by blast
  have "f 0 < b" using bound by auto
  hence "t>0  f 0 < b^t" using b>1
    using bound less_imp_le_nat less_le_trans by (metis self_le_power)
  thus ?case using nth_digit_def bound by auto 
next
  case (Suc q)
  thus ?case 
  proof (cases "t  Suc q")
    case True
    have f_le_bound: "f k  b-1" for k using bound apply auto 
      by (metis Suc_pred b_def less_Suc_eq_le numeral_2_eq_2 zero_less_Suc zero_less_power)
    have series_bound: "(k = 0..q. f k * b ^ k) < b^(Suc q)"
      apply (induct q)
        subgoal using bound by (simp add: less_imp_le_nat) 
        subgoal for q
          proof -
            assume asm: "(k = 0..q. f k * b ^ k) < b ^ Suc q"
            have "(k = 0..q. f k * b ^ k) + f (Suc q) * (b * b ^ q) 
                 (k = 0..q. f k * b ^ k) + (b-1) * (b * b ^ q)" using f_le_bound by auto  
            also have "... < b^(Suc q) + (b-1) * (b * b ^ q)" using asm by auto
            also have "...  b * b * b^q" apply auto
              by (metis One_nat_def Suc_neq_Zero b_def eq_imp_le mult.assoc mult_eq_if numerals(2) 
                  power_not_zero)
            finally show ?thesis using asm by auto
          qed 
        done
    hence "nth_digit ((k = 0..q. f k * b ^ k) + f (Suc q) * (b * b ^ q)) t b = f t" 
      using Suc nth_digit_def apply (cases "t = Suc q", auto)
        subgoal using  Suc_n_not_le_n add.commute add.left_neutral b_def bound div_mult_self1 
              less_imp_le_nat less_mult_imp_div_less mod_less not_one_le_zero one_less_numeral_iff 
              one_less_power power_Suc semiring_norm(76) zero_less_Suc by auto
        subgoal 
          proof -
            assume "t  Suc q"
            hence "t < Suc q" using True by auto
            hence "nth_digit (f (Suc q) * b ^ Suc q + (k = 0..q. f k * b ^ k)) t b 
                = nth_digit (k = 0..q. f k * b ^ k) t b"
              using aux2_digit_gen_sum_repr[of "k = 0..q. f k * b ^ k" "b" "Suc q" "t" 
                    "f (Suc q)"] series_bound by auto
            hence "((k = 0..q. f k * b ^ k) + f (Suc q) * (b * b ^ q)) div b ^ t mod b
                  = (k = 0..q. f k * b ^ k) div b ^ t mod b" 
              using nth_digit_def by (auto simp:add.commute)
            thus ?thesis using Suc[of "t"] nth_digit_def True t  Suc q by auto
          qed
        done
    thus ?thesis using True by auto
  next
    case False (* t > Suc q *)
    hence "t  Suc (Suc q)" by auto
    have f_le_bound: "f k  b-1" for k using bound apply auto 
      by (metis Suc_pred b_def less_Suc_eq_le numeral_2_eq_2 zero_less_Suc zero_less_power)
    have bound: "(k = 0..q. f k * b ^ k) < b^(Suc q)" for q
      apply (induct q)
        subgoal using bound by (simp add: less_imp_le_nat) 
        subgoal for q
          proof -
            assume asm: "(k = 0..q. f k * b ^ k) < b ^ Suc q"
            have "(k = 0..q. f k * b ^ k) + f (Suc q) * (b * b ^ q) 
                 (k = 0..q. f k * b ^ k) + (b-1) * (b * b ^ q)" using f_le_bound by auto  
            also have "... < b^(Suc q) + (b-1) * (b * b ^ q)" using asm by auto
            also have "...  b * b * b^q" apply auto
              by (metis One_nat_def Suc_neq_Zero b_def eq_imp_le mult.assoc mult_eq_if numerals(2) 
                  power_not_zero)
            finally show ?thesis using asm by auto
          qed 
        done
    have "(k = 0..q. f k * b ^ k) + f (Suc q) * (b * b ^ q) < (b ^ Suc (Suc q))" 
      using bound[of "Suc q"] by auto 
    also have "...  b^t" using t  Suc (Suc q) 
      apply auto by (metis b_def nat_power_less_imp_less not_le numeral_2_eq_2 power_Suc 
                     zero_less_Suc zero_less_power)
    finally show ?thesis using t  Suc (Suc q) bound[of "Suc q"] nth_digit_def by auto
  qed
qed

text ‹Equivalence condition for the @{text nth_digit} function cite"h10lecturenotes"
      (see equation 2.29)›

lemma digit_gen_equiv:
  assumes "b>1"
  shows "d = nth_digit a k b  (x.y.(a = x * b^(k+1) + d*b^k +y  d < b  y < b^k))"
  (is "?P  ?Q")
proof
  assume p: ?P
  then show ?Q
  proof(cases "k<a")
    case True

    (* 3rd condition *)
    have "(i<k.((nth_digit a i b)*b^i)) < b^k"
    proof(induct k)
      case 0
      then show ?case by auto
    next
      case (Suc k)
      have "(i<Suc k. nth_digit a i b * b ^ i) = (nth_digit a k b) * b^k  
            + (i<k.((nth_digit a i b)*b^i))" by simp
      moreover have " (nth_digit a k b) * b^k  (b-1) * b^ k"
        using assms mult_le_mono nth_digit_bounded by auto
      moreover have "(i<k.((nth_digit a i b)*b^i)) < b ^ (Suc k)" 
        using Suc.hyps assms order.strict_trans2 by fastforce
      ultimately show ?case using assms using Suc.hyps mult_eq_if by auto
    qed
    moreover define y where "y = (i<k.((nth_digit a i b)*b^i))"
    ultimately have 3: "y < b^k"  by blast

    (* 2nd condition*)
     have 2: "d < b" using nth_digit_bounded[of b a k] p assms by linarith

    (* 1st condition *)
    define x where "x =  (i=Suc k..<a. ((nth_digit a i b)*b^(i-Suc k)))"
    have "a = (i<a.((nth_digit a i b)*b^i))" using assms digit_gen_sum_repr_variant by blast
    hence s:"a = y + d * b^k  
            + (i=Suc k..<a.((nth_digit a i b)*b^i))" using True y_def p
      by (metis (no_types, lifting) Suc_leI atLeast0LessThan gr_implies_not0 
          linorder_not_less sum.atLeastLessThan_concat sum.lessThan_Suc)
    have "(n = Suc k..<a. nth_digit a n b * b ^ (n - Suc k) * b ^ Suc k) 
          =  (i = Suc k..<a. nth_digit a i b * b ^ i)"
      apply (rule sum.cong; auto simp: algebra_simps)
      by (metis Suc_le_lessD Zero_not_Suc add_diff_cancel_left' diff_Suc_1 diff_Suc_Suc 
          less_imp_Suc_add power_add power_eq_if)
    hence "x * b^(k+1) = (i=Suc k..<a.((nth_digit a i b)*b^i))" 
      using x_def sum_distrib_right[of "λi. (nth_digit a i b) *  b^(i - Suc k)"] by simp
    hence "a = x * b^(k+1) + d*b^k +y" using s by auto
    thus ?thesis using 2 3 by blast
  next
    case False
    then have "a < b^k" using assms power_gt_expt[of b k] by auto
    moreover have "d = 0" by (simp add: calculation nth_digit_def p)
    ultimately show ?thesis
      using assms by force   
  qed
next
  assume ?Q
  then obtain x y where conds: "a = x * b^(k+1) + d*b^k +y  d < b  y < b^k" by auto
  hence "nth_digit a k b = nth_digit(x * b^(k+1) + d*b^k) k b"
    using aux3_digit_gen_sum_repr[of y b "k" "x*b + d"] assms by (auto simp: algebra_simps)
  hence "nth_digit a k b = nth_digit(d*b^k) k b" 
    using aux2_digit_gen_sum_repr[of "d*b^k" "b" "k+1" k x] conds by auto
  then show ?P using conds nth_digit_def by simp
qed


end