(* Title: HOL/ex/ThreeDivides.thy Author: Benjamin Porter, 2005 *)
section‹Three Divides Theorem›
theory ThreeDivides imports Main "HOL-Library.LaTeXsugar" begin
subsection‹Abstract›
text‹ The following document presents a proof of the Three Divides N theorem formalised in the Isabelle/Isar theorem proving system. {\em Theorem}: $3$ divides $n$ if and only if $3$ divides the sum of all digits in $n$. {\em Informal Proof}: Take $n = \sum{n_j * 10^j}$ where $n_j$ is the $j$'th least significant digit of the decimal denotation of the number n and the sum ranges over all digits. Then $$ (n - \sum{n_j}) = \sum{n_j * (10^j - 1)} $$ We know $\forall j\; 3|(10^j - 1) $ and hence $3|LHS$, therefore $$\forall n\; 3|n \Longleftrightarrow 3|\sum{n_j}$$ ‹◻› ›
subsection‹Formal proof›
subsubsection ‹Miscellaneous summation lemmas›
text‹If $a$ divides ‹A x›for all x then $a$ divides any sum over terms of the form ‹(A x)*(P x)›for arbitrary $P$.›
lemma div_sum: fixes a::nat and n::nat shows"∀x. a dvd A x ==> a dvd (∑x proof (induct n) case 0 show ?caseby simp next case (Suc n) from Suc have"a dvd (A n * D n)"by (simp add: dvd_mult2) with Suc have"a dvd ((∑xby (simp add: dvd_add) thus ?caseby simp qed
subsubsection ‹Generalised Three Divides›
text‹This section solves a generalised form of the three divides problem. Here we show that for any sequence of numbers the theorem holds. In the next section we specialise this theorem to apply directly to the decimal expansion of the natural numbers.›
text‹Here we show that the first statement in the informal proof is true for all natural numbers. Note we are using 🍋‹D i›to denote the $i$'th element in a sequence of numbers.›
lemma digit_diff_split: fixes n::nat and nd::nat and x::nat shows"n = (∑x∈{..==> (n - (∑x∑x by (simp add: sum_diff_distrib diff_mult_distrib2)
text‹Now we prove that 3 always divides numbers of the form $10^x - 1$.› lemma three_divs_0: shows"(3::nat) dvd (10^x - 1)" proof (induct x) case 0 show ?caseby simp next case (Suc n) let ?thr = "(3::nat)" have"?thr dvd 9"by simp moreover have"?thr dvd (10*(10^n - 1))"by (rule dvd_mult) (rule Suc) hence"?thr dvd (10^(n+1) - 10)"by (simp add: nat_distrib) ultimately have"?thr dvd ((10^(n+1) - 10) + 9)" by (simp only: ac_simps) (rule dvd_add) thus ?caseby simp qed
text‹Expanding on the previous lemma and lemma ‹div_sum›.› lemma three_divs_1: fixes D :: "nat ==> nat" shows"3 dvd (∑x by (subst mult.commute, rule div_sum) (simp add: three_divs_0 [simplified])
text‹Using lemmas ‹digit_diff_split›and ‹three_divs_1›we now prove the following lemma. › lemma three_divs_2: fixes nd::nat and D::"nat==>nat" shows"3 dvd ((∑x∑x proof - from three_divs_1 have"3 dvd (∑x . thus ?thesis by (simp only: digit_diff_split) qed
text‹ We now present the final theorem of this section. For any sequence of numbers (defined by a function 🍋‹D :: (nat==>nat)›), we show that 3 divides the expansive sum $\sum{(D\;x)*10^x}$ over $x$ if and only if 3 divides the sum of the individual numbers $\sum{D\;x}$. › lemma three_div_general: fixes D :: "nat ==> nat" shows"(3 dvd (∑x∑x proof have mono: "(∑x≤ (∑x by (rule sum_mono) simp txt‹This lets us form the term 🍋‹(∑x🚫 D x * 10^x) - (∑x🚫 D x)›\›
{ assume"3 dvd (∑x with three_divs_2 mono show"3 dvd (∑x by (blast intro: dvd_diffD)
}
{ assume"3 dvd (∑x with three_divs_2 mono show"3 dvd (∑x by (blast intro: dvd_diffD1)
} qed
subsubsection ‹Three Divides Natural›
text‹This section shows that for all natural numbers we can generate a sequence of digits less than ten that represent the decimal expansion of the number. We then use the lemma ‹three_div_general›to prove our final theorem.›
text‹\medskip Definitions of length and digit sum.›
text‹This section introduces some functions to calculate the required properties of natural numbers. We then proceed to prove some properties of these functions. The function ‹nlen›returns the number of digits in a natural number n.›
fun nlen :: "nat ==> nat" where "nlen 0 = 0"
| "nlen x = 1 + nlen (x div 10)"
text‹The function ‹sumdig›returns the sum of all digits in some number n.›
definition
sumdig :: "nat ==> nat"where "sumdig n = (∑x < nlen n. n div 10^x mod 10)"
text‹Some properties of these functions follow.›
lemma nlen_zero: "0 = nlen x ==> x = 0" by (induct x rule: nlen.induct) auto
lemma nlen_suc: "Suc m = nlen n ==> m = nlen (n div 10)" by (induct n rule: nlen.induct) simp_all
text‹The following lemma is the principle lemma required to prove our theorem. It states that an expansion of some natural number $n$ into a sequence of its individual digits is always possible.›
lemma exp_exists: "m = (∑x proof (induct "nlen m" arbitrary: m) case 0 thus ?caseby (simp add: nlen_zero) next case (Suc nd) obtain c where mexp: "m = 10*(m div 10) + c ∧ c < 10" and cdef: "c = m mod 10"by simp show"m = (∑x proof - from‹Suc nd = nlen m› have"nd = nlen (m div 10)"by (rule nlen_suc) with Suc have "m div 10 = (∑xby simp with mexp have "m = 10*(∑xby simp alsohave "… = (∑x by (subst sum_distrib_left) (simp add: ac_simps) alsohave "… = (∑x by (simp add: div_mult2_eq[symmetric]) alsohave "… = (∑x∈{Suc 0.. by (simp only: sum.shift_bounds_Suc_ivl)
(simp add: atLeast0LessThan) alsohave "… = (∑x by (simp add: atLeast0LessThan[symmetric] sum.atLeast_Suc_lessThan cdef) alsonote‹Suc nd = nlen m› finally show"m = (∑x . qed qed
text‹\medskip Final theorem.›
text‹We now combine the general theorem ‹three_div_general› and existence result of ‹exp_exists›to prove our final theorem.›
theorem three_divides_nat: shows"(3 dvd n) = (3 dvd sumdig n)" proof (unfold sumdig_def) have"n = (∑x by (rule exp_exists) moreover have"3 dvd (∑x (3 dvd (∑x by (rule three_div_general) ultimately show"3 dvd n = (3 dvd (∑xby simp qed
end
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet am 2026-04-26)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
