src/HOL/ex/ThreeDivides.thy
 author wenzelm Wed Jun 22 10:09:20 2016 +0200 (2016-06-22) changeset 63343 fb5d8a50c641 parent 61933 cf58b5b794b2 child 63918 6bf55e6e0b75 permissions -rw-r--r--
bundle lifting_syntax;
 wenzelm@33025  1 (* Title: HOL/ex/ThreeDivides.thy  kleing@19022  2  Author: Benjamin Porter, 2005  kleing@19022  3 *)  kleing@19022  4 wenzelm@61343  5 section \Three Divides Theorem\  kleing@19022  6 kleing@19022  7 theory ThreeDivides  wenzelm@41413  8 imports Main "~~/src/HOL/Library/LaTeXsugar"  kleing@19022  9 begin  kleing@19022  10 wenzelm@61343  11 subsection \Abstract\  kleing@19022  12 wenzelm@61343  13 text \  kleing@19022  14 The following document presents a proof of the Three Divides N theorem  kleing@19022  15 formalised in the Isabelle/Isar theorem proving system.  kleing@19022  16 wenzelm@19026  17 {\em Theorem}: $3$ divides $n$ if and only if $3$ divides the sum of all  wenzelm@19026  18 digits in $n$.  kleing@19022  19 kleing@19022  20 {\em Informal Proof}:  kleing@19022  21 Take $n = \sum{n_j * 10^j}$ where $n_j$ is the $j$'th least  kleing@19022  22 significant digit of the decimal denotation of the number n and the  kleing@19022  23 sum ranges over all digits. Then $$(n - \sum{n_j}) = \sum{n_j * (10^j  kleing@19022  24 - 1)}$$ We know $\forall j\; 3|(10^j - 1)$ and hence $3|LHS$,  kleing@19022  25 therefore $$\forall n\; 3|n \Longleftrightarrow 3|\sum{n_j}$$  wenzelm@61933  26 \\\  wenzelm@61343  27 \  kleing@19022  28 kleing@19022  29 wenzelm@61343  30 subsection \Formal proof\  wenzelm@23219  31 wenzelm@61343  32 subsubsection \Miscellaneous summation lemmas\  kleing@19022  33 wenzelm@61933  34 text \If $a$ divides \A x\ for all x then $a$ divides any  wenzelm@61933  35 sum over terms of the form \(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 (\xxGeneralised Three Divides\  kleing@19022  53 wenzelm@61343  54 text \This section solves a generalised form of the three divides  kleing@19022  55 problem. Here we show that for any sequence of numbers the theorem  kleing@19022  56 holds. In the next section we specialise this theorem to apply  wenzelm@61343  57 directly to the decimal expansion of the natural numbers.\  kleing@19022  58 wenzelm@61343  59 text \Here we show that the first statement in the informal proof is  kleing@19022  60 true for all natural numbers. Note we are using @{term "D i"} to  wenzelm@61343  61 denote the $i$'th element in a sequence of numbers.\  kleing@19022  62 kleing@19022  63 lemma digit_diff_split:  kleing@19022  64  fixes n::nat and nd::nat and x::nat  wenzelm@19026  65  shows "n = (\x\{..  kleing@19022  66  (n - (\xxNow we prove that 3 always divides numbers of the form $10^x - 1$.\  wenzelm@19026  70 lemma three_divs_0:  kleing@19022  71  shows "(3::nat) dvd (10^x - 1)"  kleing@19022  72 proof (induct x)  kleing@19022  73  case 0 show ?case by simp  kleing@19022  74 next  kleing@19022  75  case (Suc n)  kleing@19022  76  let ?thr = "(3::nat)"  kleing@19022  77  have "?thr dvd 9" by simp  kleing@19022  78  moreover  wenzelm@23373  79  have "?thr dvd (10*(10^n - 1))" by (rule dvd_mult) (rule Suc)  kleing@19022  80  hence "?thr dvd (10^(n+1) - 10)" by (simp add: nat_distrib)  kleing@19022  81  ultimately  kleing@19022  82  have"?thr dvd ((10^(n+1) - 10) + 9)"  haftmann@57514  83  by (simp only: ac_simps) (rule dvd_add)  kleing@19022  84  thus ?case by simp  kleing@19022  85 qed  kleing@19022  86 wenzelm@61933  87 text \Expanding on the previous lemma and lemma \div_sum\.\  kleing@19022  88 lemma three_divs_1:  kleing@19022  89  fixes D :: "nat \ nat"  kleing@19022  90  shows "3 dvd (\xUsing lemmas \digit_diff_split\ and  wenzelm@61933  94 \three_divs_1\ we now prove the following lemma.  wenzelm@61343  95 \  kleing@19022  96 lemma three_divs_2:  kleing@19022  97  fixes nd::nat and D::"nat\nat"  kleing@19022  98  shows "3 dvd ((\xxx  kleing@19022  105 We now present the final theorem of this section. For any  kleing@19022  106 sequence of numbers (defined by a function @{term "D :: (nat\nat)"}),  kleing@19022  107 we show that 3 divides the expansive sum $\sum{(D\;x)*10^x}$ over $x$  kleing@19022  108 if and only if 3 divides the sum of the individual numbers  kleing@19022  109 $\sum{D\;x}$.  wenzelm@61343  110 \  kleing@19022  111 lemma three_div_general:  kleing@19022  112  fixes D :: "nat \ nat"  kleing@19022  113  shows "(3 dvd (\xxx (\xThis lets us form the term  wenzelm@61343  118  @{term "(\xx  kleing@19022  119 kleing@19022  120  {  kleing@19022  121  assume "3 dvd (\xxxxThree Divides Natural\  kleing@19022  136 wenzelm@61343  137 text \This section shows that for all natural numbers we can  kleing@19022  138 generate a sequence of digits less than ten that represent the decimal  wenzelm@61933  139 expansion of the number. We then use the lemma \three_div_general\ to prove our final theorem.\  kleing@19022  140 wenzelm@23219  141 wenzelm@61343  142 text \\medskip Definitions of length and digit sum.\  kleing@19022  143 wenzelm@61343  144 text \This section introduces some functions to calculate the  kleing@19022  145 required properties of natural numbers. We then proceed to prove some  kleing@19022  146 properties of these functions.  kleing@19022  147 wenzelm@61933  148 The function \nlen\ returns the number of digits in a natural  wenzelm@61343  149 number n.\  kleing@19022  150 krauss@35419  151 fun nlen :: "nat \ nat"  krauss@35419  152 where  kleing@19022  153  "nlen 0 = 0"  krauss@35419  154 | "nlen x = 1 + nlen (x div 10)"  kleing@19022  155 wenzelm@61933  156 text \The function \sumdig\ returns the sum of all digits in  wenzelm@61343  157 some number n.\  kleing@19022  158 wenzelm@19736  159 definition  wenzelm@21404  160  sumdig :: "nat \ nat" where  wenzelm@19736  161  "sumdig n = (\x < nlen n. n div 10^x mod 10)"  kleing@19022  162 wenzelm@61343  163 text \Some properties of these functions follow.\  kleing@19022  164 kleing@19022  165 lemma nlen_zero:  kleing@19022  166  "0 = nlen x \ x = 0"  kleing@19022  167  by (induct x rule: nlen.induct) auto  kleing@19022  168 kleing@19022  169 lemma nlen_suc:  kleing@19022  170  "Suc m = nlen n \ m = nlen (n div 10)"  kleing@19022  171  by (induct n rule: nlen.induct) simp_all  kleing@19022  172 kleing@19022  173 wenzelm@61343  174 text \The following lemma is the principle lemma required to prove  kleing@19022  175 our theorem. It states that an expansion of some natural number $n$  wenzelm@61343  176 into a sequence of its individual digits is always possible.\  kleing@19022  177 kleing@19022  178 lemma exp_exists:  wenzelm@19026  179  "m = (\x c < 10"  huffman@29974  185  and cdef: "c = m mod 10" by simp  wenzelm@19026  186  show "m = (\xSuc nd = nlen m\  wenzelm@19026  189  have "nd = nlen (m div 10)" by (rule nlen_suc)  berghofe@34915  190  with Suc have  wenzelm@19026  191  "m div 10 = (\xx = (\x = (\x = (\x\{Suc 0.. = (\xSuc nd = nlen m\  wenzelm@19026  208  finally  wenzelm@19026  209  show "m = (\x\medskip Final theorem.\  kleing@19022  215 wenzelm@61933  216 text \We now combine the general theorem \three_div_general\  wenzelm@61933  217 and existence result of \exp_exists\ to prove our final  wenzelm@61343  218 theorem.\  kleing@19022  219 kleing@19022  220 theorem three_divides_nat:  kleing@19022  221  shows "(3 dvd n) = (3 dvd sumdig n)"  kleing@19022  222 proof (unfold sumdig_def)  wenzelm@19026  223 ` have "n = (\xxxx