author | blanchet |
Wed, 04 Mar 2009 10:45:52 +0100 | |
changeset 30240 | 5b25fee0362c |
parent 29911 | ca93255656a5 |
child 33025 | cc038dc8f412 |
permissions | -rw-r--r-- |
kleing@19022 | 1 |
(* Title: HOL/Isar_examples/ThreeDivides.thy |
kleing@19022 | 2 |
ID: $Id$ |
kleing@19022 | 3 |
Author: Benjamin Porter, 2005 |
kleing@19022 | 4 |
*) |
kleing@19022 | 5 |
|
kleing@19022 | 6 |
header {* Three Divides Theorem *} |
kleing@19022 | 7 |
|
kleing@19022 | 8 |
theory ThreeDivides |
kleing@19022 | 9 |
imports Main LaTeXsugar |
kleing@19022 | 10 |
begin |
kleing@19022 | 11 |
|
wenzelm@23219 | 12 |
subsection {* Abstract *} |
kleing@19022 | 13 |
|
kleing@19022 | 14 |
text {* |
kleing@19022 | 15 |
The following document presents a proof of the Three Divides N theorem |
kleing@19022 | 16 |
formalised in the Isabelle/Isar theorem proving system. |
kleing@19022 | 17 |
|
wenzelm@19026 | 18 |
{\em Theorem}: $3$ divides $n$ if and only if $3$ divides the sum of all |
wenzelm@19026 | 19 |
digits in $n$. |
kleing@19022 | 20 |
|
kleing@19022 | 21 |
{\em Informal Proof}: |
kleing@19022 | 22 |
Take $n = \sum{n_j * 10^j}$ where $n_j$ is the $j$'th least |
kleing@19022 | 23 |
significant digit of the decimal denotation of the number n and the |
kleing@19022 | 24 |
sum ranges over all digits. Then $$ (n - \sum{n_j}) = \sum{n_j * (10^j |
kleing@19022 | 25 |
- 1)} $$ We know $\forall j\; 3|(10^j - 1) $ and hence $3|LHS$, |
kleing@19022 | 26 |
therefore $$\forall n\; 3|n \Longleftrightarrow 3|\sum{n_j}$$ |
kleing@19022 | 27 |
@{text "\<box>"} |
kleing@19022 | 28 |
*} |
kleing@19022 | 29 |
|
kleing@19022 | 30 |
|
wenzelm@23219 | 31 |
subsection {* Formal proof *} |
wenzelm@23219 | 32 |
|
wenzelm@23219 | 33 |
subsubsection {* Miscellaneous summation lemmas *} |
kleing@19022 | 34 |
|
kleing@19022 | 35 |
text {* If $a$ divides @{text "A x"} for all x then $a$ divides any |
kleing@19022 | 36 |
sum over terms of the form @{text "(A x)*(P x)"} for arbitrary $P$. *} |
kleing@19022 | 37 |
|
kleing@19022 | 38 |
lemma div_sum: |
kleing@19022 | 39 |
fixes a::nat and n::nat |
kleing@19022 | 40 |
shows "\<forall>x. a dvd A x \<Longrightarrow> a dvd (\<Sum>x<n. A x * D x)" |
kleing@19022 | 41 |
proof (induct n) |
kleing@19022 | 42 |
case 0 show ?case by simp |
kleing@19022 | 43 |
next |
kleing@19022 | 44 |
case (Suc n) |
kleing@19022 | 45 |
from Suc |
kleing@19022 | 46 |
have "a dvd (A n * D n)" by (simp add: dvd_mult2) |
kleing@19022 | 47 |
with Suc |
kleing@19022 | 48 |
have "a dvd ((\<Sum>x<n. A x * D x) + (A n * D n))" by (simp add: dvd_add) |
kleing@19022 | 49 |
thus ?case by simp |
kleing@19022 | 50 |
qed |
kleing@19022 | 51 |
|
wenzelm@23219 | 52 |
|
wenzelm@23219 | 53 |
subsubsection {* Generalised Three Divides *} |
kleing@19022 | 54 |
|
kleing@19022 | 55 |
text {* This section solves a generalised form of the three divides |
kleing@19022 | 56 |
problem. Here we show that for any sequence of numbers the theorem |
kleing@19022 | 57 |
holds. In the next section we specialise this theorem to apply |
kleing@19022 | 58 |
directly to the decimal expansion of the natural numbers. *} |
kleing@19022 | 59 |
|
kleing@19022 | 60 |
text {* Here we show that the first statement in the informal proof is |
kleing@19022 | 61 |
true for all natural numbers. Note we are using @{term "D i"} to |
kleing@19022 | 62 |
denote the $i$'th element in a sequence of numbers. *} |
kleing@19022 | 63 |
|
kleing@19022 | 64 |
lemma digit_diff_split: |
kleing@19022 | 65 |
fixes n::nat and nd::nat and x::nat |
wenzelm@19026 | 66 |
shows "n = (\<Sum>x\<in>{..<nd}. (D x)*((10::nat)^x)) \<Longrightarrow> |
kleing@19022 | 67 |
(n - (\<Sum>x<nd. (D x))) = (\<Sum>x<nd. (D x)*(10^x - 1))" |
kleing@19022 | 68 |
by (simp add: sum_diff_distrib diff_mult_distrib2) |
kleing@19022 | 69 |
|
kleing@19022 | 70 |
text {* Now we prove that 3 always divides numbers of the form $10^x - 1$. *} |
wenzelm@19026 | 71 |
lemma three_divs_0: |
kleing@19022 | 72 |
shows "(3::nat) dvd (10^x - 1)" |
kleing@19022 | 73 |
proof (induct x) |
kleing@19022 | 74 |
case 0 show ?case by simp |
kleing@19022 | 75 |
next |
kleing@19022 | 76 |
case (Suc n) |
kleing@19022 | 77 |
let ?thr = "(3::nat)" |
kleing@19022 | 78 |
have "?thr dvd 9" by simp |
kleing@19022 | 79 |
moreover |
wenzelm@23373 | 80 |
have "?thr dvd (10*(10^n - 1))" by (rule dvd_mult) (rule Suc) |
kleing@19022 | 81 |
hence "?thr dvd (10^(n+1) - 10)" by (simp add: nat_distrib) |
kleing@19022 | 82 |
ultimately |
kleing@19022 | 83 |
have"?thr dvd ((10^(n+1) - 10) + 9)" |
kleing@19022 | 84 |
by (simp only: add_ac) (rule dvd_add) |
kleing@19022 | 85 |
thus ?case by simp |
kleing@19022 | 86 |
qed |
kleing@19022 | 87 |
|
wenzelm@19026 | 88 |
text {* Expanding on the previous lemma and lemma @{text "div_sum"}. *} |
kleing@19022 | 89 |
lemma three_divs_1: |
kleing@19022 | 90 |
fixes D :: "nat \<Rightarrow> nat" |
kleing@19022 | 91 |
shows "3 dvd (\<Sum>x<nd. D x * (10^x - 1))" |
wenzelm@19026 | 92 |
by (subst nat_mult_commute, rule div_sum) (simp add: three_divs_0 [simplified]) |
kleing@19022 | 93 |
|
kleing@19022 | 94 |
text {* Using lemmas @{text "digit_diff_split"} and |
kleing@19022 | 95 |
@{text "three_divs_1"} we now prove the following lemma. |
kleing@19022 | 96 |
*} |
kleing@19022 | 97 |
lemma three_divs_2: |
kleing@19022 | 98 |
fixes nd::nat and D::"nat\<Rightarrow>nat" |
kleing@19022 | 99 |
shows "3 dvd ((\<Sum>x<nd. (D x)*(10^x)) - (\<Sum>x<nd. (D x)))" |
wenzelm@19026 | 100 |
proof - |
wenzelm@19026 | 101 |
from three_divs_1 have "3 dvd (\<Sum>x<nd. D x * (10 ^ x - 1))" . |
wenzelm@19026 | 102 |
thus ?thesis by (simp only: digit_diff_split) |
kleing@19022 | 103 |
qed |
kleing@19022 | 104 |
|
kleing@19022 | 105 |
text {* |
kleing@19022 | 106 |
We now present the final theorem of this section. For any |
kleing@19022 | 107 |
sequence of numbers (defined by a function @{term "D :: (nat\<Rightarrow>nat)"}), |
kleing@19022 | 108 |
we show that 3 divides the expansive sum $\sum{(D\;x)*10^x}$ over $x$ |
kleing@19022 | 109 |
if and only if 3 divides the sum of the individual numbers |
kleing@19022 | 110 |
$\sum{D\;x}$. |
kleing@19022 | 111 |
*} |
kleing@19022 | 112 |
lemma three_div_general: |
kleing@19022 | 113 |
fixes D :: "nat \<Rightarrow> nat" |
kleing@19022 | 114 |
shows "(3 dvd (\<Sum>x<nd. D x * 10^x)) = (3 dvd (\<Sum>x<nd. D x))" |
kleing@19022 | 115 |
proof |
kleing@19022 | 116 |
have mono: "(\<Sum>x<nd. D x) \<le> (\<Sum>x<nd. D x * 10^x)" |
wenzelm@19026 | 117 |
by (rule setsum_mono) simp |
kleing@19022 | 118 |
txt {* This lets us form the term |
kleing@19022 | 119 |
@{term "(\<Sum>x<nd. D x * 10^x) - (\<Sum>x<nd. D x)"} *} |
kleing@19022 | 120 |
|
kleing@19022 | 121 |
{ |
kleing@19022 | 122 |
assume "3 dvd (\<Sum>x<nd. D x)" |
kleing@19022 | 123 |
with three_divs_2 mono |
kleing@19022 | 124 |
show "3 dvd (\<Sum>x<nd. D x * 10^x)" |
kleing@19022 | 125 |
by (blast intro: dvd_diffD) |
kleing@19022 | 126 |
} |
kleing@19022 | 127 |
{ |
kleing@19022 | 128 |
assume "3 dvd (\<Sum>x<nd. D x * 10^x)" |
kleing@19022 | 129 |
with three_divs_2 mono |
kleing@19022 | 130 |
show "3 dvd (\<Sum>x<nd. D x)" |
kleing@19022 | 131 |
by (blast intro: dvd_diffD1) |
kleing@19022 | 132 |
} |
kleing@19022 | 133 |
qed |
kleing@19022 | 134 |
|
kleing@19022 | 135 |
|
wenzelm@23219 | 136 |
subsubsection {* Three Divides Natural *} |
kleing@19022 | 137 |
|
kleing@19022 | 138 |
text {* This section shows that for all natural numbers we can |
kleing@19022 | 139 |
generate a sequence of digits less than ten that represent the decimal |
kleing@19022 | 140 |
expansion of the number. We then use the lemma @{text |
kleing@19022 | 141 |
"three_div_general"} to prove our final theorem. *} |
kleing@19022 | 142 |
|
wenzelm@23219 | 143 |
|
wenzelm@23219 | 144 |
text {* \medskip Definitions of length and digit sum. *} |
kleing@19022 | 145 |
|
kleing@19022 | 146 |
text {* This section introduces some functions to calculate the |
kleing@19022 | 147 |
required properties of natural numbers. We then proceed to prove some |
kleing@19022 | 148 |
properties of these functions. |
kleing@19022 | 149 |
|
kleing@19022 | 150 |
The function @{text "nlen"} returns the number of digits in a natural |
kleing@19022 | 151 |
number n. *} |
kleing@19022 | 152 |
|
kleing@19022 | 153 |
consts nlen :: "nat \<Rightarrow> nat" |
kleing@19022 | 154 |
recdef nlen "measure id" |
kleing@19022 | 155 |
"nlen 0 = 0" |
kleing@19022 | 156 |
"nlen x = 1 + nlen (x div 10)" |
kleing@19022 | 157 |
|
kleing@19022 | 158 |
text {* The function @{text "sumdig"} returns the sum of all digits in |
kleing@19022 | 159 |
some number n. *} |
kleing@19022 | 160 |
|
wenzelm@19736 | 161 |
definition |
wenzelm@21404 | 162 |
sumdig :: "nat \<Rightarrow> nat" where |
wenzelm@19736 | 163 |
"sumdig n = (\<Sum>x < nlen n. n div 10^x mod 10)" |
kleing@19022 | 164 |
|
kleing@19022 | 165 |
text {* Some properties of these functions follow. *} |
kleing@19022 | 166 |
|
kleing@19022 | 167 |
lemma nlen_zero: |
kleing@19022 | 168 |
"0 = nlen x \<Longrightarrow> x = 0" |
kleing@19022 | 169 |
by (induct x rule: nlen.induct) auto |
kleing@19022 | 170 |
|
kleing@19022 | 171 |
lemma nlen_suc: |
kleing@19022 | 172 |
"Suc m = nlen n \<Longrightarrow> m = nlen (n div 10)" |
kleing@19022 | 173 |
by (induct n rule: nlen.induct) simp_all |
kleing@19022 | 174 |
|
kleing@19022 | 175 |
|
kleing@19022 | 176 |
text {* The following lemma is the principle lemma required to prove |
kleing@19022 | 177 |
our theorem. It states that an expansion of some natural number $n$ |
kleing@19022 | 178 |
into a sequence of its individual digits is always possible. *} |
kleing@19022 | 179 |
|
kleing@19022 | 180 |
lemma exp_exists: |
wenzelm@19026 | 181 |
"m = (\<Sum>x<nlen m. (m div (10::nat)^x mod 10) * 10^x)" |
wenzelm@20503 | 182 |
proof (induct nd \<equiv> "nlen m" arbitrary: m) |
kleing@19022 | 183 |
case 0 thus ?case by (simp add: nlen_zero) |
kleing@19022 | 184 |
next |
kleing@19022 | 185 |
case (Suc nd) |
kleing@19022 | 186 |
hence IH: |
kleing@19022 | 187 |
"nd = nlen (m div 10) \<Longrightarrow> |
kleing@19022 | 188 |
m div 10 = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x)" |
kleing@19022 | 189 |
by blast |
huffman@29911 | 190 |
obtain c where mexp: "m = 10*(m div 10) + c \<and> c < 10" |
huffman@29911 | 191 |
and cdef: "c = m mod 10" by simp |
wenzelm@19026 | 192 |
show "m = (\<Sum>x<nlen m. m div 10^x mod 10 * 10^x)" |
kleing@19022 | 193 |
proof - |
wenzelm@19026 | 194 |
from `Suc nd = nlen m` |
wenzelm@19026 | 195 |
have "nd = nlen (m div 10)" by (rule nlen_suc) |
kleing@19022 | 196 |
with IH have |
wenzelm@19026 | 197 |
"m div 10 = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x)" by simp |
kleing@19022 | 198 |
with mexp have |
kleing@19022 | 199 |
"m = 10*(\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x) + c" by simp |
kleing@19022 | 200 |
also have |
kleing@19022 | 201 |
"\<dots> = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^(x+1)) + c" |
ballarin@19279 | 202 |
by (subst setsum_right_distrib) (simp add: mult_ac) |
kleing@19022 | 203 |
also have |
kleing@19022 | 204 |
"\<dots> = (\<Sum>x<nd. m div 10^(Suc x) mod 10 * 10^(Suc x)) + c" |
kleing@19022 | 205 |
by (simp add: div_mult2_eq[symmetric]) |
kleing@19022 | 206 |
also have |
kleing@19022 | 207 |
"\<dots> = (\<Sum>x\<in>{Suc 0..<Suc nd}. m div 10^x mod 10 * 10^x) + c" |
kleing@19022 | 208 |
by (simp only: setsum_shift_bounds_Suc_ivl) |
kleing@19022 | 209 |
(simp add: atLeast0LessThan) |
kleing@19022 | 210 |
also have |
kleing@19022 | 211 |
"\<dots> = (\<Sum>x<Suc nd. m div 10^x mod 10 * 10^x)" |
nipkow@28071 | 212 |
by (simp add: atLeast0LessThan[symmetric] setsum_head_upt_Suc cdef) |
wenzelm@19026 | 213 |
also note `Suc nd = nlen m` |
wenzelm@19026 | 214 |
finally |
wenzelm@19026 | 215 |
show "m = (\<Sum>x<nlen m. m div 10^x mod 10 * 10^x)" . |
kleing@19022 | 216 |
qed |
kleing@19022 | 217 |
qed |
kleing@19022 | 218 |
|
kleing@19022 | 219 |
|
wenzelm@23219 | 220 |
text {* \medskip Final theorem. *} |
kleing@19022 | 221 |
|
kleing@19022 | 222 |
text {* We now combine the general theorem @{text "three_div_general"} |
kleing@19022 | 223 |
and existence result of @{text "exp_exists"} to prove our final |
kleing@19022 | 224 |
theorem. *} |
kleing@19022 | 225 |
|
kleing@19022 | 226 |
theorem three_divides_nat: |
kleing@19022 | 227 |
shows "(3 dvd n) = (3 dvd sumdig n)" |
kleing@19022 | 228 |
proof (unfold sumdig_def) |
wenzelm@19026 | 229 |
have "n = (\<Sum>x<nlen n. (n div (10::nat)^x mod 10) * 10^x)" |
kleing@19022 | 230 |
by (rule exp_exists) |
kleing@19022 | 231 |
moreover |
kleing@19022 | 232 |
have "3 dvd (\<Sum>x<nlen n. (n div (10::nat)^x mod 10) * 10^x) = |
kleing@19022 | 233 |
(3 dvd (\<Sum>x<nlen n. n div 10^x mod 10))" |
kleing@19022 | 234 |
by (rule three_div_general) |
kleing@19022 | 235 |
ultimately |
kleing@19022 | 236 |
show "3 dvd n = (3 dvd (\<Sum>x<nlen n. n div 10^x mod 10))" by simp |
kleing@19022 | 237 |
qed |
kleing@19022 | 238 |
|
kleing@19022 | 239 |
end |