src/HOL/ex/ThreeDivides.thy
 author huffman Wed Feb 18 07:24:13 2009 -0800 (2009-02-18) changeset 29974 ca93255656a5 parent 28071 6ab5b4595f64 child 33025 cc038dc8f412 permissions -rw-r--r--
speed up proof of exp_exists
 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 wenzelm@23219  12 subsection {* 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 wenzelm@23219  31 subsection {* Formal proof *}  wenzelm@23219  32 wenzelm@23219  33 subsubsection {* Miscellaneous summation lemmas *}  kleing@19022  34 kleing@19022  35 text {* If $a$ divides @{text "A x"} for all x then $a$ divides any  kleing@19022  36 sum over terms of the form @{text "(A x)*(P x)"} for arbitrary $P$. *}  kleing@19022  37 kleing@19022  38 lemma div_sum:  kleing@19022  39  fixes a::nat and n::nat  kleing@19022  40  shows "\x. a dvd A x \ a dvd (\xxx\{..  kleing@19022  67  (n - (\xx nat"  kleing@19022  91  shows "3 dvd (\xnat"  kleing@19022  99  shows "3 dvd ((\xxxnat)"}),  kleing@19022  108 we show that 3 divides the expansive sum $\sum{(D\;x)*10^x}$ over $x$  kleing@19022  109 if and only if 3 divides the sum of the individual numbers  kleing@19022  110 $\sum{D\;x}$.  kleing@19022  111 *}  kleing@19022  112 lemma three_div_general:  kleing@19022  113  fixes D :: "nat \ nat"  kleing@19022  114  shows "(3 dvd (\xxx (\xxxxxxx nat"  kleing@19022  154 recdef nlen "measure id"  kleing@19022  155  "nlen 0 = 0"  kleing@19022  156  "nlen x = 1 + nlen (x div 10)"  kleing@19022  157 kleing@19022  158 text {* The function @{text "sumdig"} returns the sum of all digits in  kleing@19022  159 some number n. *}  kleing@19022  160 wenzelm@19736  161 definition  wenzelm@21404  162  sumdig :: "nat \ nat" where  wenzelm@19736  163  "sumdig n = (\x < nlen n. n div 10^x mod 10)"  kleing@19022  164 kleing@19022  165 text {* Some properties of these functions follow. *}  kleing@19022  166 kleing@19022  167 lemma nlen_zero:  kleing@19022  168  "0 = nlen x \ x = 0"  kleing@19022  169  by (induct x rule: nlen.induct) auto  kleing@19022  170 kleing@19022  171 lemma nlen_suc:  kleing@19022  172  "Suc m = nlen n \ m = nlen (n div 10)"  kleing@19022  173  by (induct n rule: nlen.induct) simp_all  kleing@19022  174 kleing@19022  175 kleing@19022  176 text {* The following lemma is the principle lemma required to prove  kleing@19022  177 our theorem. It states that an expansion of some natural number $n$  kleing@19022  178 into a sequence of its individual digits is always possible. *}  kleing@19022  179 kleing@19022  180 lemma exp_exists:  wenzelm@19026  181  "m = (\x "nlen m" arbitrary: m)  kleing@19022  183  case 0 thus ?case by (simp add: nlen_zero)  kleing@19022  184 next  kleing@19022  185  case (Suc nd)  kleing@19022  186  hence IH:  kleing@19022  187  "nd = nlen (m div 10) \  kleing@19022  188  m div 10 = (\x c < 10"  huffman@29974  191  and cdef: "c = m mod 10" by simp  wenzelm@19026  192 ` show "m = (\xxx = (\x = (\x = (\x\{Suc 0.. = (\xxxxxx