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