# 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. ∀i≥s. 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
"∑i≥n. 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 "(∑i≥0. 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 "(∑i≥0. 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 "(∑i≥n. 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 "(∑i≥n. seq i) = (∑i≤s-n. seq (i + n))"
by (meson atMost_iff finite_atMost leI suminf_finite)
also have "… = (∑i=n..s. seq i)"
proof -
have "⋀na. (∑na≤na. seq (na + n)) = sum seq {0 + n..na + n}"
by (metis (no_types) atLeast0AtMost sum.shift_bounds_cl_nat_ivl)
then show ?thesis
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) + (∑i≥n. seq i)"
proof -
obtain s where s: "⋀i. i≥s ⟶ 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) = (∑i≥n. 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)"
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))"

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. ∀i≥n. seq i = 0"
shows "[(∑i. seq i) = (∑i. seq i mod b)] (mod b)"
proof -
obtain n where n: "⋀i. i≥n ⟶ 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

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)"
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
power_one_right)
then show ?thesis
using ub2 num_digits_char assms nd_def
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"

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"

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
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"
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"
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)"
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
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) + (∑i≥Suc j. D i * b^i)"
using split_suminf[OF term_eventually_zero] by presburger
have "i≥Suc 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 (∑i≥Suc j. D i * b^i)"
by presburger
with two_sums have "[m = (∑i<Suc j. D i * b^i)] (mod b*b^j)"
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 "[a⇩0::nat, a⇩1] ⇘LEbase b⇙ = a⇩0 + a⇩1 * b"
by simp

lemma LEbase_three_digits [simp]: shows "[a⇩0::nat, a⇩1, a⇩2] ⇘LEbase b⇙ = a⇩0 + a⇩1*b + a⇩2*b^2"
proof -
have "[a⇩0::nat, a⇩1, a⇩2] ⇘LEbase b⇙ = a⇩0 + ([a⇩1, a⇩2] ⇘LEbase b⇙) * b"
by simp
also have "… = a⇩0 + (a⇩1 + a⇩2*b) * b"
by simp
also have "… = a⇩0 + a⇩1*b + a⇩2*b^2"
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))"
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⇙)"
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

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
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 "[a⇩1::nat, a⇩0] ⇘base b⇙ = a⇩1*b + a⇩0"
by simp

lemma BEbase_three_digits [simp]: shows "[a⇩2::nat, a⇩1, a⇩0] ⇘base b⇙ = a⇩2*b^2 + a⇩1*b + a⇩0"
proof -
have "b * (a⇩1 + b * a⇩2) = a⇩2 * b⇧2 + a⇩1 * b"
apply (subst mult.commute)
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⇙"

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 = []"

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
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
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
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