Theory DigitsInBase

theory DigitsInBase
  imports "HOL-Computational_Algebra.Computational_Algebra" "HOL-Number_Theory.Number_Theory"
begin

section‹Infinite sums›
text‹In this section, it is shown that an infinite series \emph{of natural numbers} converges if
and only if its terms are eventually zero. Additionally, the notion of a summation starting from an
index other than zero is defined. A few obvious lemmas about these notions are established.›

definition eventually_zero :: "(nat  _)  bool" where
"eventually_zero (D :: nat  _)  ( n. D n = 0)"

lemma eventually_zero_char:
  shows "eventually_zero D  (s. is. D i = 0)"
  unfolding eventually_zero_def
  using MOST_nat_le .

text‹There's a lot of commonality between this setup and univariate polynomials, but drawing out
the similarities and proving them is beyond the scope of the current version of this theory except
for the following lemma.›
lemma eventually_zero_poly:
  shows "eventually_zero D  D = poly.coeff (Abs_poly D)"
  by (metis Abs_poly_inverse MOST_coeff_eq_0 eventually_zero_def mem_Collect_eq)

lemma eventually_zero_imp_summable [simp]:
  assumes "eventually_zero D"
  shows "summable D"
  using summable_finite assms eventually_zero_char
  by (metis (mono_tags) atMost_iff finite_atMost nat_le_linear)

lemma summable_bounded:
  fixes my_seq :: "nat  nat" and n :: nat
  assumes " i . i  n  my_seq i = 0"
  shows "summable my_seq"
  using assms eventually_zero_char eventually_zero_imp_summable by blast

lemma sum_bounded:
  fixes my_seq :: "nat  nat" and n :: nat
  assumes " i . i  n  my_seq i = 0"
  shows "(i. my_seq i) = (i<n. my_seq i)"
  by (meson assms finite_lessThan lessThan_iff linorder_not_le suminf_finite)  

lemma product_seq_eventually_zero:
  fixes seq1 seq2 :: "nat  nat"
  assumes "eventually_zero seq1"
  shows "eventually_zero (λ i. seq1 i * seq2 i)"
  using mult_0 eventually_zero_char
  by (metis (no_types, lifting) assms)

abbreviation upper_sum
  where "upper_sum seq n  i. seq (i + n)"
syntax
  "_from_sum" :: "idt  'a  'b  'b"  ("(3__./ _)" [0,0,10] 10)
translations
  "in. t" == "CONST upper_sum (λi. t) n"

text ‹The following two statements are proved as a sanity check. They are not intended to be used
anywhere.›
corollary
  fixes seq :: "nat  nat" and a :: nat
  assumes seq_def: " i. seq i = (if i = 0 then a else 0)"
  shows "(i0. seq i) = upper_sum (λ i. seq i) 0"
  by simp

corollary
  fixes seq :: "nat  nat" and a :: nat
  assumes seq_def: " i. seq i = (if i = 0 then a else 0)"
  shows "(i0. seq i) = a"
  by (smt (verit) group_cancel.rule0 lessI lessThan_0 linorder_not_less seq_def sum.empty
      sum.lessThan_Suc_shift sum_bounded)

lemma bounded_sum_from:
  fixes seq :: "nat  nat" and n s :: nat
  assumes "i>s. seq i = 0" and "n  s"
  shows "(in. seq i) = (i=n..s. seq i)"
proof -  
  have "i. i > (s - n)  seq (i + n) = 0"
    using assms by (meson less_diff_conv2)
  then have "(in. seq i) = (is-n. seq (i + n))"
    by (meson atMost_iff finite_atMost leI suminf_finite)
  also have " = (i=n..s. seq i)"
  proof -
    have "na. (nana. seq (na + n)) = sum seq {0 + n..na + n}"
      by (metis (no_types) atLeast0AtMost sum.shift_bounds_cl_nat_ivl)
    then show ?thesis
      by (simp add: assms(2))
  qed
  finally show ?thesis .
qed

lemma split_suminf:
  fixes seq :: "nat  nat" and n :: nat
  assumes "eventually_zero seq"
  shows "(i. seq i) = (i<n. seq i) + (in. seq i)"
proof -
  obtain s where s: "i. is  seq i = 0"
    using assms unfolding eventually_zero_char by presburger
  then have sum_s: "(i. seq i) = (i<s. seq i)"
    using sum_bounded by presburger
  show "(i. seq i) = (i<n. seq i) + (i(n). seq i)"
  proof (cases "n  s")
    case True
    then have "(i(n). seq i) = 0"
      using s by force
    moreover have "(i<n. seq i) = (i<s. seq i)"
      by (metis True dual_order.trans s sum_bounded sum_s)
    ultimately show ?thesis using sum_s by simp
  next
    case False
    have 0: "(i=n..s. seq i) = (in. seq i)"
      by (metis False bounded_sum_from le_eq_less_or_eq nle_le s)
    from False have "n  s"
      by simp
    then have "(i<s. seq i) = (i<n. seq i) + (i=n..s. seq i)"
      by (metis add_cancel_left_right nat_le_iff_add s sum.atLeastLessThan_concat add_0 
          lessThan_atLeast0 sum.last_plus)
    then show ?thesis using 0 sum_s
      by presburger
  qed
qed

lemma dvd_suminf:
  fixes seq :: "nat  nat" and b :: nat
  assumes "eventually_zero seq" and "i. b dvd seq i"
  shows "b dvd (i. seq i)"
proof -
  obtain s::nat where s: "i  s  seq i = 0" for i
    using assms(1) eventually_zero_char by blast
  then have "(i. seq i) = (i<s. seq i)"
    using sum_bounded by blast
  moreover have "b dvd (i<s. seq i)"
    using assms(2) by (simp add: dvd_sum)
  ultimately show ?thesis by presburger
qed

lemma eventually_zero_shifted:
  assumes "eventually_zero seq"
  shows "eventually_zero (λ i. seq (i + n))"
  by (meson assms eventually_zero_char trans_le_add1)

section‹Modular arithmetic›
text‹This section establishes a number of lemmas about modular arithmetic, including that modular
division distributes over an ``infinite'' sum whose terms are eventually zero.›

lemma pmod_int_char:
  fixes a b d :: int
  shows "[a = b] (mod d)  ((n::int). a = b + n*d)"
  by (metis cong_iff_lin cong_sym mult.commute)

lemma equiv_conj_if:
  assumes "P  Q" and "P  R" and "Q  R  P"
  shows "P  Q  R"
  using assms by auto

lemma mod_successor_char:
  fixes k k' i b :: nat
  assumes "(b::nat)  2"
  shows "[k = k'] (mod b^(Suc i))  [k div b^i = k' div b^i] (mod b)  [k = k'] (mod b^i)"
proof (rule equiv_conj_if)
  assume kk'_cong: "[k = k'] (mod b ^ Suc i)"
  then show "[k div b^i = k' div b^i] (mod b)"
    by (smt (verit, ccfv_SIG) Groups.mult_ac(2) add_diff_cancel_right' cong_def div_mult_mod_eq
        mod_mult2_eq mod_mult_self4 mult_cancel1 power_Suc2)
  from kk'_cong show "[k = k'] (mod b ^ i)"
    using Cong.cong_dvd_modulus_nat
    by (meson Suc_n_not_le_n le_imp_power_dvd nat_le_linear)
next
  assume "[k div b^i = k' div b^i] (mod b)"
  moreover assume "[k = k'] (mod b^i)"
  ultimately show "[k = k'] (mod b ^ Suc i)"
    by (metis (mono_tags, lifting) cong_def mod_mult2_eq power_Suc2)
qed

lemma mod_1:
  fixes k k' b :: nat
  shows "[k = k'] (mod b^0)"
  by simp

lemma mod_distributes:
  fixes seq :: "nat  nat" and b :: nat
  assumes "n. in. seq i = 0"
  shows "[(i. seq i) = (i. seq i mod b)] (mod b)"
proof -
  obtain n where n: "i. in  seq i = 0"
    using assms by presburger
  from n have "(i. seq i) = (i<n. seq i)"
    using sum_bounded by presburger
  moreover from n have "(i. seq i mod b) = (i<n. seq i mod b)"
    using sum_bounded by presburger
  ultimately show ?thesis
    unfolding cong_def
    by (metis mod_sum_eq)
qed

lemma another_mod_cancellation_int:
  fixes a b c d m :: int
  assumes "d > 0" and "[m = a + b] (mod c * d)" and "a div d = 0" and "d dvd b"
  shows "[m div d = b div d] (mod c)"
proof (subst pmod_int_char)
  obtain k::int where k: "m = a + b + k*c*d"
    using pmod_int_char assms(2) by (metis mult.assoc)
  have "d dvd (b + k*c*d)" using d dvd b
    by simp
  from k have "m div d = (a + b + k*c*d) div d"
    by presburger
  also have " = (b + k*c*d) div d"
    using a div d = 0 d dvd (b + k*c*d)
    by fastforce
  also have " = (b div d) + k*c"
    using d dvd b d > 0 by auto
  finally show "n. m div d = b div d + n * c"
    by blast
qed

lemma another_mod_cancellation:
  fixes a b c d m :: nat
  assumes "d > 0" and "[m = a + b] (mod c * d)" and "a div d = 0" and "d dvd b"
  shows "[m div d = b div d] (mod c)"
  by (smt (verit) another_mod_cancellation_int assms cong_int_iff of_nat_0 of_nat_0_less_iff
      of_nat_add of_nat_dvd_iff of_nat_mult zdiv_int)

section‹Digits as sequence›
text‹Rules are introduced for computing the $i^{\text{th}}$ digit of a base-$b$ representation
and the number of digits required to represent a given number. (The latter is essentially an integer
version of the base-$b$ logarithm.) It is shown that the sum of the terms $d_i b^i$ converges to
$m$ if $d_i$ is the $i^{\text{th}}$ digit $m$. It is shown that the sequence of digits defined is
the unique sequence of digits less than $b$ with this property 

Additionally, the \texttt{digits\_in\_base} locale is introduced, which specifies a single symbol
@{term b} referring to a natural number greater than one (the base of the digits). Consequently
this symbol is omitted from many of the following lemmas and definitions.
›

locale digits_in_base =
  fixes b :: nat
  assumes b_gte_2: "b  2"
begin

lemma b_facts [simp]:
  shows "b > 1" and "b > 0" and "b  1" and "b  0" and "1 mod b = 1" and "1 div b = 0"
  using b_gte_2 by force+

text‹Definition based on @{cite ThreeDivides}.›
abbreviation ith_digit :: "nat  nat  nat" where
"ith_digit m i  (m div b^i) mod b"

lemma ith_digit_lt_base:
  fixes m i :: nat
  shows "0  ith_digit m i" and "ith_digit m i < b"
  apply (rule Nat.le0)
  using b_facts(2) mod_less_divisor by presburger

definition num_digits :: "nat  nat"
  where "num_digits m = (LEAST i. m < b^i)"

lemma num_digits_works:
  shows "m < b ^ (num_digits m)"
  by (metis LeastI One_nat_def b_facts(1) num_digits_def power_gt_expt)

lemma num_digits_le:
  assumes "m < b^i"
  shows "num_digits m  i"
  using assms num_digits_works[of m] Least_le num_digits_def
  by metis

lemma num_digits_zero:
  fixes m :: nat
  assumes "num_digits m = 0"
  shows "m = 0"
  using num_digits_works[of m]
  unfolding assms
  by simp

lemma num_digits_gt:
  assumes "m  b^i"
  shows "num_digits m > i"
  by (meson assms b_facts(2) dual_order.strict_trans2 nat_power_less_imp_less num_digits_works)

lemma num_digits_eqI [intro]:
  assumes "m  b^i" and "m < b^(i+1)"
  shows "num_digits m = i + 1"
proof -
  {
    fix j :: nat
    assume "j < i + 1"
    then have "m  b^j"
      by (metis Suc_eq_plus1 assms(1) b_facts(1) less_Suc_eq_le order_trans power_increasing_iff)
  }
  then show ?thesis
    using num_digits_works
    unfolding num_digits_def
    by (meson assms(2) leD linorder_neqE_nat not_less_Least)
qed

lemma num_digits_char:
  assumes "m  1"
  shows "num_digits m = i + 1  m  b^i  m < b^(i+1)"
  by (metis add_diff_cancel_right' assms b_gte_2 ex_power_ivl1 num_digits_eqI)


text‹Statement based on @{cite ThreeDivides}.›
lemma num_digits_recurrence:
  fixes m :: nat
  assumes "m  1"
  shows "num_digits m = num_digits (m div b) + 1"
proof -
  define nd where "nd = num_digits m"
  then have lb: "m  b^(nd-1)" and ub: "m < b^nd"
    using num_digits_char[OF assms]
     apply (metis assms diff_is_0_eq le_add_diff_inverse2 nat_le_linear power_0)
    using nd_def num_digits_works by presburger
  from ub have ub2: "m div b < b^(nd-1)"
    by (metis Suc_eq_plus1 add.commute add_diff_inverse_nat assms less_mult_imp_div_less less_one
        linorder_not_less mult.commute power.simps(2) power_0)
  from lb have lb2: "m div b  b^(nd - 1) div b"
    using div_le_mono by presburger
  show ?thesis
  proof (cases "m  b")
    assume "m  b"
    then have "nd  2"
      unfolding nd_def
      by (metis One_nat_def assms less_2_cases_iff linorder_not_le nd_def power_0 power_one_right
          ub)
    then have "m div b  b^(nd-2)"
      using lb2
      by (smt (verit) One_nat_def add_le_imp_le_diff b_facts(4) diff_diff_left le_add_diff_inverse2
          nonzero_mult_div_cancel_left numeral_2_eq_2 plus_1_eq_Suc power_add power_commutes
          power_one_right)
    then show ?thesis
      using ub2 num_digits_char assms nd_def
      by (smt (verit) 2  nd add_diff_cancel_right' add_leD2 add_le_imp_le_diff diff_diff_left
          eq_diff_iff le_add2 nat_1_add_1 num_digits_eqI)
  next
    assume "¬ b  m"
    then have "m < b"
      by simp
    then have "num_digits m = 1"
      using assms
      by (metis One_nat_def Suc_eq_plus1 num_digits_char power_0 power_one_right)
    from m < b have "m div b = 0"
      using div_less by presburger
    then have "num_digits (m div b) = 0"
      using Least_eq_0 num_digits_def by presburger
    show ?thesis
      using num_digits (m div b) = 0 num_digits m = 1 by presburger
  qed
qed

lemma num_digits_zero_2 [simp]: "num_digits 0 = 0"
  by (simp add: num_digits_def)

end (* digits_in_base *)

locale base_10
begin
text‹As a sanity check, the number of digits in base ten is computed for several natural numbers.›

sublocale digits_in_base 10
  by (unfold_locales, simp)

corollary
  shows "num_digits 0 = 0"
        and "num_digits 1 = 1"
        and "num_digits 9 = 1"
        and "num_digits 10 = 2"
        and "num_digits 99 = 2"
        and "num_digits 100 = 3"
  by (simp_all add: num_digits_recurrence)

end (* base_10 *)

context digits_in_base
begin

lemma high_digits_zero_helper:
  fixes m i :: nat
  shows "i < num_digits m  ith_digit m i = 0"
proof (cases "i < num_digits m")
  case True
  then show ?thesis by meson
next
  case False
  then have "i  num_digits m" by force
  then have "m < b^i"
    by (meson b_facts(1) num_digits_works order_less_le_trans power_increasing_iff)
  then show ?thesis
    by simp
qed

lemma high_digits_zero:
  fixes m i :: nat
  assumes "i  num_digits m"
  shows "ith_digit m i = 0"
  using high_digits_zero_helper assms leD by blast

lemma digit_expansion_bound:
  fixes i :: nat and A :: "nat  nat"
  assumes "j. A j < b"
  shows "(j<i. A j * b^j) < b^i"
proof (induct i)
  case (Suc i)
  show ?case
  proof (subst Set_Interval.comm_monoid_add_class.sum.lessThan_Suc)
    have "A i * b^i  (b-1) * b^i" using assms
      by (metis One_nat_def Suc_pred b_facts(2) le_simps(2) mult_le_mono1)
    then have "(j<i. A j * b ^ j) + A i * b ^ i < b^i + (b-1) * b^i"
      using Suc add_less_le_mono by blast
    also have "  b ^ Suc i"
      using assms(1) mult_eq_if by auto
    finally show "(j<i. A j * b ^ j) + A i * b ^ i < b ^ Suc i" .
  qed
qed simp

text‹Statement and proof based on @{cite ThreeDivides}.›
lemma num_digits_suc:
  fixes n m :: nat
  assumes "Suc n = num_digits m"
  shows "n = num_digits (m div b)"
  using num_digits_recurrence assms
  by (metis One_nat_def Suc_eq_plus1 Suc_le_lessD le_add2 linorder_not_less num_digits_le
      old.nat.inject power_0)

text‹Proof (and to some extent statement) based on @{cite ThreeDivides}.›
lemma digit_expansion_bounded_seq:
  fixes m :: nat
  shows "m = (j<num_digits m. ith_digit m j * b^j)"
proof (induct "num_digits m" arbitrary: m)
  case 0
  then show "m = (j<num_digits m. ith_digit m j * b^j)"
    using lessThan_0 sum.empty num_digits_zero by metis
next
  case (Suc nd m)
  assume nd: "Suc nd = num_digits m"
  define c where "c = m mod b"
  then have mexp: "m = b * (m div b) + c" and "c < b"
    by force+
  show "m = (j<num_digits m. ith_digit m j * b^j)"
  proof -
    have "nd = num_digits (m div b)"
      using num_digits_suc[OF nd] .
    with Suc have "m div b = (j<nd. ith_digit (m div b) j * b^j)"
      by presburger
    with mexp have "m = b * (j<nd. ith_digit (m div b) j * b^j) + c"
      by presburger
    also have " = (j<nd. ith_digit (m div b) j * b^Suc j) + c"
      by (simp add: sum_distrib_left mult.assoc mult.commute)
    also have " = (j<nd. ith_digit m (Suc j) * b^Suc j) + c"
      by (simp add: div_mult2_eq)
    also have " = (j=Suc 0..<Suc nd. ith_digit m j * b^j) + ith_digit m 0"
      unfolding sum.shift_bounds_Suc_ivl c_def atLeast0LessThan
      by simp
    also have " = (j<Suc nd. ith_digit m j * b^j)"
      by (smt (verit) One_nat_def Zero_not_Suc add.commute add_diff_cancel_right' atLeast0LessThan
          calculation div_by_Suc_0 mult.commute nonzero_mult_div_cancel_left power_0
          sum.lessThan_Suc_shift sum.shift_bounds_Suc_ivl)
    also note nd
    finally show "m = (j<num_digits m. ith_digit m j * b^j)" .
  qed
qed

text‹A natural number can be obtained from knowing all its base-$b$ digits by the formula
$\sum_j d_j b^j$.›
theorem digit_expansion_seq:
  fixes m :: nat
  shows "m = (j. ith_digit m j * b^j)"
  using digit_expansion_bounded_seq[of m] high_digits_zero[of m] sum_bounded mult_0
  by (metis (no_types, lifting))

lemma lower_terms:
  fixes a c i :: nat
  assumes "c < b^i" and "a < b"
  shows "ith_digit (a * b^i + c) i = a"
  using assms by force

lemma upper_terms:
  fixes A a i :: nat
  assumes "b*b^i dvd A" and "a < b"
  shows "ith_digit (A + a * b^i) i = a"
  using assms by force

lemma current_term:
  fixes A a c i :: nat
  assumes "b*b^i dvd A" and "c < b^i" and "a < b"
  shows "ith_digit (A + a*b^i + c) i = a"
proof -
  have "(A + a*b^i + c) div b^i mod b = (a*b^i + c) div b^i mod b"
    using assms(1)
    by (metis (no_types, lifting) div_eq_0_iff add_cancel_right_right
        assms(2) assms(3) div_plus_div_distrib_dvd_left dvd_add_times_triv_right_iff
        dvd_mult_right lower_terms upper_terms)
  also have " = a"
    using assms by force
  finally show "(A + a*b^i + c) div b^i mod b = a" .
qed

text‹Given that
\begin{equation*}
m = \sum_i d_i b^i
\end{equation*}
where the $d_i$ are all natural numbers less than $b$, it follows that $d_j$ is the $j^{\text{th}}$
digit of $m$.›
theorem seq_uniqueness:
  fixes m j :: nat and D :: "nat  nat"
  assumes "eventually_zero D" and "m = (i. D i * b^i)" and "i. D i < b"
  shows "D j = ith_digit m j"
proof -
  have "eventually_zero (ith_digit m)"
    using high_digits_zero
    by (meson eventually_zero_char)
  then have term_eventually_zero: "eventually_zero (λ i. D i * b^i)"
    using product_seq_eventually_zero assms(1) by auto
  then have shifted_term_eventually_zero:
    "eventually_zero (λ i. D (i + n) * b ^ (i + n))" for n
    using eventually_zero_shifted
    by blast
  note m = (i. D i * b^i)
  then have two_sums: "m = (i<Suc j. D i * b^i) + (iSuc j. D i * b^i)"
    using split_suminf[OF term_eventually_zero] by presburger
  have "iSuc j  b*b^j dvd (D i * b^i)" for i
    by (metis dvd_mult2 le_imp_power_dvd mult.commute power_Suc)
  then have "b*b^j dvd (iSuc j. D i * b^i)"
    using dvd_suminf shifted_term_eventually_zero le_add2
    by presburger
  with two_sums have "[m = (i<Suc j. D i * b^i)] (mod b*b^j)"
    by (meson cong_def Cong.cong_dvd_modulus_nat mod_add_self2)
  then have one_sum: "[m = (i<j. D i * b^i) + D j * b^j] (mod b*b^j)"
    by simp
  have "(i<j. D i * b^i) < b^j"
    using assms(3) digit_expansion_bound by blast
  with one_sum have "[m div b^j = (D j)] (mod b)"
    using another_mod_cancellation dual_order.strict_trans1
    unfolding cong_def
    by auto
  then show "D j = ith_digit m j"
    using assms(3) mod_less unfolding cong_def by presburger
qed


end (* digits_in_base *)

section‹Little Endian notation›
text‹In this section we begin to define finite digit expansions. Ultimately we want to write digit
expansions in ``big endian'' notation, by which we mean with the highest place digit on the left
and the ones digit on the write, since this ordering is standard in informal mathematics. However,
it is easier to first define ``little endian'' expansions with the ones digit on the left since that
way the list indexing agrees with the sequence indexing used in the previous section (whenever both
are defined).

Notation, definitions, and lemmas in this section typically start with the prefix \texttt{LE} (for
``little endian'') to distinguish them from the big endian versions in the next section.
›

fun LEeval_as_base ("_⇘LEbase _" [65, 65] 70)
  where "[] ⇘LEbase b= 0"
  | "(d # d_list) ⇘LEbase b= d + b * (d_list⇘LEbase b)"

corollary shows "[2, 4] ⇘LEbase 5= (22::nat)"
  by simp

lemma LEbase_one_digit [simp]: shows "[a::nat] ⇘LEbase b= a"
  by simp

lemma LEbase_two_digits [simp]: shows "[a0::nat, a1] ⇘LEbase b= a0 + a1 * b"
  by simp

lemma LEbase_three_digits [simp]: shows "[a0::nat, a1, a2] ⇘LEbase b= a0 + a1*b + a2*b^2"
proof -
  have "[a0::nat, a1, a2] ⇘LEbase b= a0 + ([a1, a2] ⇘LEbase b) * b"
    by simp
  also have " = a0 + (a1 + a2*b) * b"
    by simp
  also have " = a0 + a1*b + a2*b^2"
    by (simp add: add_mult_distrib power2_eq_square)
  finally show ?thesis .
qed


lemma LEbase_closed_form:
shows "(A :: nat list) ⇘LEbase b= (i < length A . A!i * b^i)"
proof (induct A)
  case Nil
  show ?case
    by simp
next
  case (Cons a A)
  show ?case
  proof -
    have "(a # A)⇘LEbase b= a + b * (A⇘LEbase b)"
      by simp
    also have " = a + b * (i<length A. A!i * b ^ i)"
      using Cons by simp
    also have " = a + (i<length A. b * A!i * b^i)"
      by (smt (verit) mult.assoc sum.cong sum_distrib_left)
    also have " = a + (i<length A. A!i * b^(i+1))"
      by (simp add: mult.assoc mult.left_commute)
    also have " = a + (i<length A. (a#A)!(i+1) * b^(i+1))"
      by force
    also have " = (a#A)!0 * b^0 + (i<length A. (a#A)!(Suc i) * b^(Suc i))"
      by force
    also have " = (i<length (a # A). (a#A)!i * b^i)"
      using sum.lessThan_Suc_shift
      by (smt (verit) length_Cons sum.cong)
    finally show ?thesis .
  qed
qed

lemma LEbase_concatenate:
  fixes A D :: "nat list" and b :: nat
  shows "(A @ D)⇘LEbase b= (A⇘LEbase b) + b^(length A) * (D⇘LEbase b)"
proof (induct A)
  case Nil
  show ?case
    by simp
next
  case (Cons a A)
  show ?case
  proof -
    have "((a # A) @ D)⇘LEbase b= ((a # (A @ D)) ⇘LEbase b)"
      by simp
    also have " = a + b * ((A @ D) ⇘LEbase b)"
      by simp
    also have " = a + b * (A⇘LEbase b+ b ^ length A * (D⇘LEbase b))"
      unfolding Cons by rule
    also have " = (a + b * (A⇘LEbase b)) + b ^ (length (a#A)) * (D⇘LEbase b)"
      by (simp add: distrib_left)
    also have " = ((a # A)⇘LEbase b) + b ^ length (a # A) * (D⇘LEbase b)"
      by simp
    finally show ?thesis .
  qed
qed

context digits_in_base
begin

definition LEdigits :: "nat  nat list" where
"LEdigits m = [ith_digit m i. i  [0..<(num_digits m)]]"

lemma length_is_num_digits:
  fixes m :: nat
  shows "length (LEdigits m) = num_digits m"
  unfolding LEdigits_def by simp

lemma ith_list_element [simp]:
  assumes "(i::nat) < length (LEdigits m)"
  shows "(LEdigits m) ! i = ith_digit m i"
  using assms
  by (simp add: length_is_num_digits LEdigits_def)

lemma LEbase_infinite_sum:
  fixes m :: nat
  shows "(i. ith_digit m i  * b^i) = (LEdigits m)⇘LEbase b⇙"
proof (unfold LEdigits_def LEbase_closed_form)
  have
    "(i<length (map (ith_digit m) [0..<num_digits m]).
                                                  map (ith_digit m) [0..<num_digits m] ! i * b ^ i)
     = (i<num_digits m. map (ith_digit m) [0..<num_digits m] ! i * b ^ i)"
    using LEdigits_def length_is_num_digits by presburger
  also have "= (i<num_digits m. ith_digit m i * b^i)"
    by force
  also have "=(i. ith_digit m i * b ^ i)" 
    using sum_bounded high_digits_zero mult_0
    by (metis (no_types, lifting))
  finally show
    "(i. ith_digit m i * b ^ i) =
     (i<length (map (ith_digit m) [0..<num_digits m]). map (ith_digit m) [0..<num_digits m] ! i * b ^ i)"
    by presburger
qed

lemma digit_expansion_LElist:
  fixes m :: nat
  shows "(LEdigits m)⇘LEbase b= m"
  using digit_expansion_seq LEbase_infinite_sum
  by presburger

lemma LElist_uniqueness:
  fixes D :: "nat list"
  assumes " i < length D. D!i < b" and "D = []  last D  0"
  shows "LEdigits (D⇘LEbase b) = D"
proof -
  define seq where "seq i = (if i < length D then D!i else 0)" for i
  then have seq_bound: "i  length D  seq i = 0" for i
    by simp
  then have seq_eventually_zero: "eventually_zero seq"
    using eventually_zero_char by blast
  have ith_digit_connection: "i < num_digits m  (LEdigits m)!i = ith_digit m i" for m i
    unfolding LEdigits_def by simp
  let ?m = "D⇘LEbase b⇙"
  have length_bounded_sum: "D⇘LEbase b= (i<length D. seq i * b^i)"
    unfolding LEbase_closed_form seq_def by force
  also have " = (i. seq i * b^i)"
    using seq_bound sum_bounded by fastforce
  finally have seq_is_digits: "seq j = ith_digit ?m j" for j
    using seq_uniqueness[OF seq_eventually_zero] assms(1)
    by (metis b_facts(2) seq_def)
  then have "i < length D  ith_digit ?m i = D!i" for i
    using seq_def by presburger
  then have "i < length D  i < num_digits ?m  (LEdigits ?m)!i = D!i" for i
    using ith_digit_connection[of i ?m] by presburger
  moreover have "length D = num_digits ?m"
  proof (rule le_antisym)
    show "length D  num_digits ?m"
    proof (cases "D = []")
      assume "D  []"
      then have "last D  0" using assms(2) by auto
      then have "last D  1" by simp
      have "?m  seq (length D - 1) * b^(length D - 1)"
        using length_bounded_sum
        by (metis b_facts(2) less_eq_div_iff_mult_less_eq mod_less_eq_dividend seq_is_digits zero_less_power)
      then have "?m  (last D) * b^(length D - 1)"
        by (simp add: D  [] last_conv_nth seq_def)
      with last D  1 have "?m  b^(length D - 1)"
        by (metis le_trans mult_1 mult_le_mono1)
      then show "num_digits ?m  length D"
        using num_digits_gt not_less_eq
        by (metis One_nat_def Suc_pred D  [] bot_nat_0.extremum_uniqueI leI length_0_conv)
    qed simp
    show "num_digits ?m  length D"
      by (metis length_bounded_sum seq_is_digits digit_expansion_bound ith_digit_lt_base(2)
          num_digits_le)
  qed
  ultimately show ?thesis
    by (simp add: length_is_num_digits list_eq_iff_nth_eq)
qed

lemma LE_digits_zero [simp]: "LEdigits 0 = []"
  using LEdigits_def by auto

lemma LE_units_digit [simp]:
  assumes "(m::nat)  {1..<b}"
  shows "LEdigits m = [m]"
  using assms LEdigits_def num_digits_recurrence by auto

end (* digits_in_base *)

section‹Big Endian notation›
text‹In this section the desired representation of natural numbers, as finite lists of digits
with the highest place on the left, is finally realized.›

definition BEeval_as_base ("_⇘base _" [65, 65] 70)
  where [simp]: "D⇘base b= (rev D)⇘LEbase b⇙"

corollary shows "[4, 2]⇘base 5= (22::nat)"
  by simp

lemma BEbase_one_digit [simp]: shows "[a::nat] ⇘base b= a"
  by simp

lemma BEbase_two_digits [simp]: shows "[a1::nat, a0] ⇘base b= a1*b + a0"
  by simp

lemma BEbase_three_digits [simp]: shows "[a2::nat, a1, a0] ⇘base b= a2*b^2 + a1*b + a0"
proof -
  have "b * (a1 + b * a2) = a2 * b2 + a1 * b"
    apply (subst mult.commute)
    unfolding add_mult_distrib power2_eq_square
    by simp
  then show ?thesis by simp
qed

lemma BEbase_closed_form:
  fixes A :: "nat list" and b :: nat
  shows "A⇘base b= (i<length A. A!i * b^(length A - Suc i))"
  unfolding LEbase_closed_form BEeval_as_base_def
  apply (subst sum.nat_diff_reindex[symmetric])
  apply (subst length_rev)
  using rev_nth
  by (metis (no_types, lifting) length_rev lessThan_iff rev_rev_ident sum.cong)

lemma BEbase_concatenate:
  fixes A D :: "nat list" and b :: nat
  shows "(A @ D) ⇘base b= (A⇘base b)*b^(length D) + (D⇘base b)"
  using LEbase_concatenate by simp

context digits_in_base
begin

definition digits :: "nat  nat list" where
"digits m = rev (LEdigits m)"

lemma length_is_num_digits_2:
  fixes m :: nat
  shows "length (digits m) = num_digits m"
  using length_is_num_digits digits_def by simp

lemma LE_BE_equivalence:
  fixes m :: nat
  shows "(digits m) ⇘base b= (LEdigits m) ⇘LEbase b⇙"
  by (simp add: digits_def)

lemma BEbase_infinite_sum:
  fixes m :: nat
  shows "(i. ith_digit m i * b^i) = (digits m)⇘base b⇙"
  using LE_BE_equivalence LEbase_infinite_sum by presburger

text‹Every natural number can be represented in base $b$, specifically by the digits sequence
defined earlier.›
theorem digit_expansion_list:
  fixes m :: nat
  shows "(digits m)⇘base b= m"
  using LE_BE_equivalence digit_expansion_LElist by auto

text‹If two natural numbers have the same base-$b$ representation, then they are equal.›
lemma digits_cancellation:
  fixes k m :: nat
  assumes "digits k = digits m"
  shows "k = m"
  by (metis assms digit_expansion_list)

text‹Suppose we have a finite (possibly empty) sequence $D_1, \dotsc, D_n$ of natural numbers such
that $0 \le D_i < b$ for all $i$ and such that $D_1$, if it exists, is nonzero. Then this sequence
is the base-$b$ representation for $\sum_i D_i b^{n-i}$.›
theorem list_uniqueness:
  fixes D :: "nat list"
  assumes " d  set D. d < b" and "D = []  D!0  0"
  shows "digits (D⇘base b) = D"
  unfolding digits_def BEeval_as_base_def
  using LElist_uniqueness
  by (metis Nil_is_rev_conv One_nat_def assms last_conv_nth length_greater_0_conv
      nth_mem rev_nth rev_swap set_rev)

text‹We now prove some simplification rules (including a reccurrence relation) to make it easier for
Isabelle/HOL to compute the base-$b$ representation of a natural number.›

text‹The base-b representation of $0$ is empty, at least following the conventions of this theory
file.›
lemma digits_zero [simp]:
  shows "digits 0 = []"
  by (simp add: digits_def)

text‹If $0 < m < b$, then the base-$b$ representation of $m$ consists of a single digit, namely
$m$ itself.›
lemma single_digit_number [simp]:
  assumes "m  {0<..<b}"
  shows "digits m = [m]"
  using assms digits_def by auto

text‹For all $m \ge b$, the base-$b$ representation of $m$ consists of the base-$b$ representation
of $\lfloor m / b \rfloor$ followed by (as the last digit) the remainder of $m$ when divided by
$b$.›
lemma digits_recurrence [simp]:
  assumes "m  b"
  shows "digits m = (digits (m div b)) @ [m mod b]"
proof -
  have "num_digits m > 1"
    using assms by (simp add: num_digits_gt)
  then have "num_digits m > 0"
    by simp
  then have "num_digits (m div b) = num_digits m - 1"
    by (metis Suc_diff_1 num_digits_suc)
  have "k > 0  last (rev [0..<k]) = 0" for k::nat
    by (simp add: last_rev)
  have "[Suc 0..<Suc k] = [Suc i. i  [0..<k]]" for k::nat
    using map_Suc_upt by presburger
  then have "rev [Suc 0..<Suc k] = [Suc i. i  rev [0..<k]]" for k::nat
    by (metis rev_map)
  then have "[f i. i  rev [Suc 0..<Suc k]] = [f (Suc i). i  rev [0..<k]]" for f and k::nat
    by simp
  then have map_shift: "k > 0  [f i. i  rev [1..<k]] = [f (Suc i). i  rev [0..<(k-1)]]"
                       for f and k::nat
    by (metis One_nat_def Suc_diff_1)
  have digit_down: "ith_digit m (Suc i) = ith_digit (m div b) i" for i::nat
    by (simp add: div_mult2_eq)
  have "digits m = rev [ith_digit m i. i  [0..<num_digits m]]"
    using LEdigits_def digits_def by presburger
  also have " = [ith_digit m i. i  rev [0..<num_digits m]]"
    using rev_map by blast
  also have " = [ith_digit m i. i  butlast (rev [0..<num_digits m])] @
                  [ith_digit m (last (rev [0..<num_digits m]))]"
    by (metis (no_types, lifting) Nil_is_map_conv Nil_is_rev_conv 1 < num_digits m
        bot_nat_0.extremum_strict dual_order.strict_trans1 last_map map_butlast snoc_eq_iff_butlast
        upt_eq_Nil_conv)
  also have " = [ith_digit m i. i  rev [1..<num_digits m]] @
                  [ith_digit m 0]"
    using 1 < num_digits m k. 0 < k  last (rev [0..<k]) = 0 by fastforce
  also have " = [ith_digit m (Suc i). i  rev [0..<(num_digits m - 1)]] @
                  [ith_digit m 0]"
    using map_shift[OF num_digits m > 0] by blast
  also have " = [ith_digit (m div b) i. i  rev [0..<(num_digits m - 1)]] @
                  [ith_digit m 0]"
    using digit_down by presburger
  also have " = (digits (m div b)) @ [ith_digit m 0]"
    by (simp add: LEdigits_def num_digits (m div b) = num_digits m - 1 digits_def rev_map)
  also have " = (digits (m div b)) @ [m mod b]"
    by simp
  finally show ?thesis .
qed

end (* digits_in_base *)

section‹Exercises›
text‹This section contains demonstrations of how to denote certain facts with the notation of the
previous sections, and how to quickly prove those facts using the lemmas and theorems above.
›

text‹The base-5 representation of $22$ is $42_5$.›
corollary "digits_in_base.digits 5 22 = [4, 2]"
proof -
  interpret digits_in_base 5
    by (simp add: digits_in_base.intro)
  show "digits 22 = [4, 2]"
    by simp
qed

text‹A different proof of the same statement.›
corollary "digits_in_base.digits 5 22 = [4, 2]"
proof -
  interpret digits_in_base 5
    by (simp add: digits_in_base.intro)
  have "[4, 2]⇘base 5= (22::nat)"
    by simp
  have "d  set [4, 2]  d < 5" for d::nat
    by fastforce
  then show ?thesis
    using list_uniqueness
    by (metis [4, 2]⇘base 5= 22 nth_Cons_0 numeral_2_eq_2 zero_neq_numeral)
qed

end