src/HOL/ex/ThreeDivides.thy
 author wenzelm Mon Sep 11 21:35:19 2006 +0200 (2006-09-11) changeset 20503 503ac4c5ef91 parent 19736 d8d0f8f51d69 child 21404 eb85850d3eb7 permissions -rw-r--r--
induct method: renamed 'fixing' to 'arbitrary';
 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  kleing@19022  159  sumdig :: "nat \ nat"  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