src/HOL/ex/ThreeDivides.thy
 author krauss Mon Mar 01 17:05:57 2010 +0100 (2010-03-01) changeset 35419 d78659d1723e parent 34915 7894c7dab132 child 41413 64cd30d6b0b8 permissions -rw-r--r--
more recdef (and old primrec) hunting
 wenzelm@33025  1 (* Title: HOL/ex/ThreeDivides.thy  kleing@19022  2  Author: Benjamin Porter, 2005  kleing@19022  3 *)  kleing@19022  4 kleing@19022  5 header {* Three Divides Theorem *}  kleing@19022  6 kleing@19022  7 theory ThreeDivides  kleing@19022  8 imports Main LaTeXsugar  kleing@19022  9 begin  kleing@19022  10 wenzelm@23219  11 subsection {* Abstract *}  kleing@19022  12 kleing@19022  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}$$  kleing@19022  26 @{text "\"}  kleing@19022  27 *}  kleing@19022  28 kleing@19022  29 wenzelm@23219  30 subsection {* Formal proof *}  wenzelm@23219  31 wenzelm@23219  32 subsubsection {* 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  66  (n - (\xx nat"  kleing@19022  90  shows "3 dvd (\xnat"  kleing@19022  98  shows "3 dvd ((\xxxnat)"}),  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}$.  kleing@19022  110 *}  kleing@19022  111 lemma three_div_general:  kleing@19022  112  fixes D :: "nat \ nat"  kleing@19022  113  shows "(3 dvd (\xxx (\xxxxxxx nat"  krauss@35419  153 where  kleing@19022  154  "nlen 0 = 0"  krauss@35419  155 | "nlen x = 1 + nlen (x div 10)"  kleing@19022  156 kleing@19022  157 text {* The function @{text "sumdig"} returns the sum of all digits in  kleing@19022  158 some number n. *}  kleing@19022  159 wenzelm@19736  160 definition  wenzelm@21404  161  sumdig :: "nat \ nat" where  wenzelm@19736  162  "sumdig n = (\x < nlen n. n div 10^x mod 10)"  kleing@19022  163 kleing@19022  164 text {* Some properties of these functions follow. *}  kleing@19022  165 kleing@19022  166 lemma nlen_zero:  kleing@19022  167  "0 = nlen x \ x = 0"  kleing@19022  168  by (induct x rule: nlen.induct) auto  kleing@19022  169 kleing@19022  170 lemma nlen_suc:  kleing@19022  171  "Suc m = nlen n \ m = nlen (n div 10)"  kleing@19022  172  by (induct n rule: nlen.induct) simp_all  kleing@19022  173 kleing@19022  174 kleing@19022  175 text {* The following lemma is the principle lemma required to prove  kleing@19022  176 our theorem. It states that an expansion of some natural number $n$  kleing@19022  177 into a sequence of its individual digits is always possible. *}  kleing@19022  178 kleing@19022  179 lemma exp_exists:  wenzelm@19026  180  "m = (\x c < 10"  huffman@29974  186  and cdef: "c = m mod 10" by simp  wenzelm@19026  187 ` show "m = (\xxx = (\x = (\x = (\x\{Suc 0.. = (\xxxxxx