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)
syntax_consts
"_from_sum" == upper_sum
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
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) + (∑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)"
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. ∀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
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
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
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) + (∑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)"
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
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"
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
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)
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
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