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