kleing@19022: (* Title: HOL/Isar_examples/ThreeDivides.thy kleing@19022: ID: $Id$ kleing@19022: Author: Benjamin Porter, 2005 kleing@19022: *) kleing@19022: kleing@19022: header {* Three Divides Theorem *} kleing@19022: kleing@19022: theory ThreeDivides kleing@19022: imports Main LaTeXsugar kleing@19022: begin kleing@19022: kleing@19022: section {* Abstract *} kleing@19022: kleing@19022: text {* kleing@19022: The following document presents a proof of the Three Divides N theorem kleing@19022: formalised in the Isabelle/Isar theorem proving system. kleing@19022: wenzelm@19026: {\em Theorem}: $3$ divides $n$ if and only if $3$ divides the sum of all wenzelm@19026: digits in $n$. kleing@19022: kleing@19022: {\em Informal Proof}: kleing@19022: Take $n = \sum{n_j * 10^j}$ where $n_j$ is the $j$'th least kleing@19022: significant digit of the decimal denotation of the number n and the kleing@19022: sum ranges over all digits. Then $$ (n - \sum{n_j}) = \sum{n_j * (10^j kleing@19022: - 1)} $$ We know $\forall j\; 3|(10^j - 1) $ and hence $3|LHS$, kleing@19022: therefore $$\forall n\; 3|n \Longleftrightarrow 3|\sum{n_j}$$ kleing@19022: @{text "\"} kleing@19022: *} kleing@19022: kleing@19022: section {* Formal proof *} kleing@19022: kleing@19022: subsection {* Miscellaneous summation lemmas *} kleing@19022: kleing@19022: text {* If $a$ divides @{text "A x"} for all x then $a$ divides any kleing@19022: sum over terms of the form @{text "(A x)*(P x)"} for arbitrary $P$. *} kleing@19022: kleing@19022: lemma div_sum: kleing@19022: fixes a::nat and n::nat kleing@19022: shows "\x. a dvd A x \ a dvd (\xxx\{.. kleing@19022: (n - (\xx nat" kleing@19022: shows "3 dvd (\xnat" kleing@19022: shows "3 dvd ((\xxxnat)"}), kleing@19022: we show that 3 divides the expansive sum $\sum{(D\;x)*10^x}$ over $x$ kleing@19022: if and only if 3 divides the sum of the individual numbers kleing@19022: $\sum{D\;x}$. kleing@19022: *} kleing@19022: lemma three_div_general: kleing@19022: fixes D :: "nat \ nat" kleing@19022: shows "(3 dvd (\xxx (\xxxxxxx nat" kleing@19022: recdef nlen "measure id" kleing@19022: "nlen 0 = 0" kleing@19022: "nlen x = 1 + nlen (x div 10)" kleing@19022: kleing@19022: text {* The function @{text "sumdig"} returns the sum of all digits in kleing@19022: some number n. *} kleing@19022: kleing@19022: constdefs kleing@19022: sumdig :: "nat \ nat" kleing@19022: "sumdig n \ \x < nlen n. n div 10^x mod 10" kleing@19022: kleing@19022: text {* Some properties of these functions follow. *} kleing@19022: kleing@19022: lemma nlen_zero: kleing@19022: "0 = nlen x \ x = 0" kleing@19022: by (induct x rule: nlen.induct) auto kleing@19022: kleing@19022: lemma nlen_suc: kleing@19022: "Suc m = nlen n \ m = nlen (n div 10)" kleing@19022: by (induct n rule: nlen.induct) simp_all kleing@19022: kleing@19022: kleing@19022: text {* The following lemma is the principle lemma required to prove kleing@19022: our theorem. It states that an expansion of some natural number $n$ kleing@19022: into a sequence of its individual digits is always possible. *} kleing@19022: kleing@19022: lemma exp_exists: wenzelm@19026: "m = (\x "nlen m" fixing: m) kleing@19022: case 0 thus ?case by (simp add: nlen_zero) kleing@19022: next kleing@19022: case (Suc nd) kleing@19022: hence IH: kleing@19022: "nd = nlen (m div 10) \ kleing@19022: m div 10 = (\xc. m = 10*(m div 10) + c \ c < 10" by presburger wenzelm@19026: then obtain c where mexp: "m = 10*(m div 10) + c \ c < 10" .. kleing@19022: then have cdef: "c = m mod 10" by arith wenzelm@19026: show "m = (\xxx = (\x = (\x = (\x\{Suc 0.. = (\xxxxxx