src/HOL/ex/ThreeDivides.thy
 author wenzelm Fri Nov 17 02:20:03 2006 +0100 (2006-11-17) changeset 21404 eb85850d3eb7 parent 20503 503ac4c5ef91 child 23219 87ad6e8a5f2c permissions -rw-r--r--
more robust syntax for definition/abbreviation/notation;
 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 kleing@19022 12 section {* 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 "\"} kleing@19022 28 *} kleing@19022 29 kleing@19022 30 section {* Formal proof *} kleing@19022 31 kleing@19022 32 subsection {* Miscellaneous summation lemmas *} kleing@19022 33 kleing@19022 34 text {* If $a$ divides @{text "A x"} for all x then $a$ divides any kleing@19022 35 sum over terms of the form @{text "(A x)*(P x)"} for arbitrary $P$. *} kleing@19022 36 kleing@19022 37 lemma div_sum: kleing@19022 38 fixes a::nat and n::nat kleing@19022 39 shows "\x. a dvd A x \ a dvd (\xxx\{.. kleing@19022 65 (n - (\xx nat" kleing@19022 89 shows "3 dvd (\xnat" kleing@19022 97 shows "3 dvd ((\xxxnat)"}), kleing@19022 106 we show that 3 divides the expansive sum $\sum{(D\;x)*10^x}$ over $x$ kleing@19022 107 if and only if 3 divides the sum of the individual numbers kleing@19022 108 $\sum{D\;x}$. kleing@19022 109 *} kleing@19022 110 lemma three_div_general: kleing@19022 111 fixes D :: "nat \ nat" kleing@19022 112 shows "(3 dvd (\xxx (\xxxxxxx nat" kleing@19022 151 recdef nlen "measure id" kleing@19022 152 "nlen 0 = 0" kleing@19022 153 "nlen x = 1 + nlen (x div 10)" kleing@19022 154 kleing@19022 155 text {* The function @{text "sumdig"} returns the sum of all digits in kleing@19022 156 some number n. *} kleing@19022 157 wenzelm@19736 158 definition wenzelm@21404 159 sumdig :: "nat \ nat" where wenzelm@19736 160 "sumdig n = (\x < nlen n. n div 10^x mod 10)" kleing@19022 161 kleing@19022 162 text {* Some properties of these functions follow. *} kleing@19022 163 kleing@19022 164 lemma nlen_zero: kleing@19022 165 "0 = nlen x \ x = 0" kleing@19022 166 by (induct x rule: nlen.induct) auto kleing@19022 167 kleing@19022 168 lemma nlen_suc: kleing@19022 169 "Suc m = nlen n \ m = nlen (n div 10)" kleing@19022 170 by (induct n rule: nlen.induct) simp_all kleing@19022 171 kleing@19022 172 kleing@19022 173 text {* The following lemma is the principle lemma required to prove kleing@19022 174 our theorem. It states that an expansion of some natural number $n$ kleing@19022 175 into a sequence of its individual digits is always possible. *} kleing@19022 176 kleing@19022 177 lemma exp_exists: wenzelm@19026 178 "m = (\x "nlen m" arbitrary: m) kleing@19022 180 case 0 thus ?case by (simp add: nlen_zero) kleing@19022 181 next kleing@19022 182 case (Suc nd) kleing@19022 183 hence IH: kleing@19022 184 "nd = nlen (m div 10) \ kleing@19022 185 m div 10 = (\xc. m = 10*(m div 10) + c \ c < 10" by presburger wenzelm@19026 188 then obtain c where mexp: "m = 10*(m div 10) + c \ c < 10" .. kleing@19022 189 then have cdef: "c = m mod 10" by arith wenzelm@19026 190 show "m = (\xxx = (\x = (\x = (\x\{Suc 0.. = (\xxxxxx