src/HOL/ex/ThreeDivides.thy
 author kleing Sun Feb 12 10:42:19 2006 +0100 (2006-02-12) changeset 19022 0e6ec4fd204c child 19026 87cd1ecae3a4 permissions -rw-r--r--
* moved ThreeDivides from Isar_examples to better suited HOL/ex
* moved 2 summation lemmas from ThreeDivides to SetInterval
 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 kleing@19022  18 {\em Theorem}: 3 divides n if and only if 3 divides the sum of all  kleing@19022  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 (\xxn. n = (\x\{..  kleing@19022  65  (n - (\xx"} *}  kleing@19022  87 lemma three_divs_1:  kleing@19022  88  fixes D :: "nat \ nat"  kleing@19022  89  shows "3 dvd (\xnat"  kleing@19022  97  shows "3 dvd ((\xxxnat)"}),  kleing@19022  105 we show that 3 divides the expansive sum $\sum{(D\;x)*10^x}$ over $x$  kleing@19022  106 if and only if 3 divides the sum of the individual numbers  kleing@19022  107 $\sum{D\;x}$.  kleing@19022  108 *}  kleing@19022  109 lemma three_div_general:  kleing@19022  110  fixes D :: "nat \ nat"  kleing@19022  111  shows "(3 dvd (\xxx (\xxxxxxx nat"  kleing@19022  150 recdef nlen "measure id"  kleing@19022  151  "nlen 0 = 0"  kleing@19022  152  "nlen x = 1 + nlen (x div 10)"  kleing@19022  153 kleing@19022  154 text {* The function @{text "sumdig"} returns the sum of all digits in  kleing@19022  155 some number n. *}  kleing@19022  156 kleing@19022  157 constdefs  kleing@19022  158  sumdig :: "nat \ nat"  kleing@19022  159  "sumdig n \ \x < nlen n. n div 10^x mod 10"  kleing@19022  160 kleing@19022  161 text {* Some properties of these functions follow. *}  kleing@19022  162 kleing@19022  163 lemma nlen_zero:  kleing@19022  164  "0 = nlen x \ x = 0"  kleing@19022  165  by (induct x rule: nlen.induct) auto  kleing@19022  166 kleing@19022  167 lemma nlen_suc:  kleing@19022  168  "Suc m = nlen n \ m = nlen (n div 10)"  kleing@19022  169  by (induct n rule: nlen.induct) simp_all  kleing@19022  170 kleing@19022  171 kleing@19022  172 text {* The following lemma is the principle lemma required to prove  kleing@19022  173 our theorem. It states that an expansion of some natural number $n$  kleing@19022  174 into a sequence of its individual digits is always possible. *}  kleing@19022  175 kleing@19022  176 lemma exp_exists:  kleing@19022  177  "\m. nd = nlen m \ m = (\x  kleing@19022  184  m div 10 = (\xc. m = 10*(m div 10) + c \ c < 10" by presburger  kleing@19022  187  from this obtain c where mexp: "m = 10*(m div 10) + c \ c < 10" ..  kleing@19022  188  then have cdef: "c = m mod 10" by arith  kleing@19022  189 ` show "m = (\xxx = (\x = (\x = (\x\{Suc 0.. = (\xxxxxx