src/HOL/ex/ThreeDivides.thy
 author wenzelm Sat May 27 17:42:02 2006 +0200 (2006-05-27) changeset 19736 d8d0f8f51d69 parent 19279 48b527d0331b child 20503 503ac4c5ef91 permissions -rw-r--r--
tuned;
     1 (*  Title:      HOL/Isar_examples/ThreeDivides.thy

     2     ID:         $Id$

     3     Author:     Benjamin Porter, 2005

     4 *)

     5

     6 header {* Three Divides Theorem *}

     7

     8 theory ThreeDivides

     9 imports Main LaTeXsugar

    10 begin

    11

    12 section {* Abstract *}

    13

    14 text {*

    15 The following document presents a proof of the Three Divides N theorem

    16 formalised in the Isabelle/Isar theorem proving system.

    17

    18 {\em Theorem}: $3$ divides $n$ if and only if $3$ divides the sum of all

    19 digits in $n$.

    20

    21 {\em Informal Proof}:

    22 Take $n = \sum{n_j * 10^j}$ where $n_j$ is the $j$'th least

    23 significant digit of the decimal denotation of the number n and the

    24 sum ranges over all digits. Then $$(n - \sum{n_j}) = \sum{n_j * (10^j   25 - 1)}$$ We know $\forall j\; 3|(10^j - 1)$ and hence $3|LHS$,

    26 therefore $$\forall n\; 3|n \Longleftrightarrow 3|\sum{n_j}$$

    27 @{text "\<box>"}

    28 *}

    29

    30 section {* Formal proof *}

    31

    32 subsection {* Miscellaneous summation lemmas *}

    33

    34 text {* If $a$ divides @{text "A x"} for all x then $a$ divides any

    35 sum over terms of the form @{text "(A x)*(P x)"} for arbitrary $P$. *}

    36

    37 lemma div_sum:

    38   fixes a::nat and n::nat

    39   shows "\<forall>x. a dvd A x \<Longrightarrow> a dvd (\<Sum>x<n. A x * D x)"

    40 proof (induct n)

    41   case 0 show ?case by simp

    42 next

    43   case (Suc n)

    44   from Suc

    45   have "a dvd (A n * D n)" by (simp add: dvd_mult2)

    46   with Suc

    47   have "a dvd ((\<Sum>x<n. A x * D x) + (A n * D n))" by (simp add: dvd_add)

    48   thus ?case by simp

    49 qed

    50

    51 subsection {* Generalised Three Divides *}

    52

    53 text {* This section solves a generalised form of the three divides

    54 problem. Here we show that for any sequence of numbers the theorem

    55 holds. In the next section we specialise this theorem to apply

    56 directly to the decimal expansion of the natural numbers. *}

    57

    58 text {* Here we show that the first statement in the informal proof is

    59 true for all natural numbers. Note we are using @{term "D i"} to

    60 denote the $i$'th element in a sequence of numbers. *}

    61

    62 lemma digit_diff_split:

    63   fixes n::nat and nd::nat and x::nat

    64   shows "n = (\<Sum>x\<in>{..<nd}. (D x)*((10::nat)^x)) \<Longrightarrow>

    65              (n - (\<Sum>x<nd. (D x))) = (\<Sum>x<nd. (D x)*(10^x - 1))"

    66 by (simp add: sum_diff_distrib diff_mult_distrib2)

    67

    68 text {* Now we prove that 3 always divides numbers of the form $10^x - 1$. *}

    69 lemma three_divs_0:

    70   shows "(3::nat) dvd (10^x - 1)"

    71 proof (induct x)

    72   case 0 show ?case by simp

    73 next

    74   case (Suc n)

    75   let ?thr = "(3::nat)"

    76   have "?thr dvd 9" by simp

    77   moreover

    78   have "?thr dvd (10*(10^n - 1))" by (rule dvd_mult)

    79   hence "?thr dvd (10^(n+1) - 10)" by (simp add: nat_distrib)

    80   ultimately

    81   have"?thr dvd ((10^(n+1) - 10) + 9)"

    82     by (simp only: add_ac) (rule dvd_add)

    83   thus ?case by simp

    84 qed

    85

    86 text {* Expanding on the previous lemma and lemma @{text "div_sum"}. *}

    87 lemma three_divs_1:

    88   fixes D :: "nat \<Rightarrow> nat"

    89   shows "3 dvd (\<Sum>x<nd. D x * (10^x - 1))"

    90   by (subst nat_mult_commute, rule div_sum) (simp add: three_divs_0 [simplified])

    91

    92 text {* Using lemmas @{text "digit_diff_split"} and

    93 @{text "three_divs_1"} we now prove the following lemma.

    94 *}

    95 lemma three_divs_2:

    96   fixes nd::nat and D::"nat\<Rightarrow>nat"

    97   shows "3 dvd ((\<Sum>x<nd. (D x)*(10^x)) - (\<Sum>x<nd. (D x)))"

    98 proof -

    99   from three_divs_1 have "3 dvd (\<Sum>x<nd. D x * (10 ^ x - 1))" .

   100   thus ?thesis by (simp only: digit_diff_split)

   101 qed

   102

   103 text {*

   104 We now present the final theorem of this section. For any

   105 sequence of numbers (defined by a function @{term "D :: (nat\<Rightarrow>nat)"}),

   106 we show that 3 divides the expansive sum $\sum{(D\;x)*10^x}$ over $x$

   107 if and only if 3 divides the sum of the individual numbers

   108 $\sum{D\;x}$.

   109 *}

   110 lemma three_div_general:

   111   fixes D :: "nat \<Rightarrow> nat"

   112   shows "(3 dvd (\<Sum>x<nd. D x * 10^x)) = (3 dvd (\<Sum>x<nd. D x))"

   113 proof

   114   have mono: "(\<Sum>x<nd. D x) \<le> (\<Sum>x<nd. D x * 10^x)"

   115     by (rule setsum_mono) simp

   116   txt {* This lets us form the term

   117          @{term "(\<Sum>x<nd. D x * 10^x) - (\<Sum>x<nd. D x)"} *}

   118

   119   {

   120     assume "3 dvd (\<Sum>x<nd. D x)"

   121     with three_divs_2 mono

   122     show "3 dvd (\<Sum>x<nd. D x * 10^x)"

   123       by (blast intro: dvd_diffD)

   124   }

   125   {

   126     assume "3 dvd (\<Sum>x<nd. D x * 10^x)"

   127     with three_divs_2 mono

   128     show "3 dvd (\<Sum>x<nd. D x)"

   129       by (blast intro: dvd_diffD1)

   130   }

   131 qed

   132

   133

   134 subsection {* Three Divides Natural *}

   135

   136 text {* This section shows that for all natural numbers we can

   137 generate a sequence of digits less than ten that represent the decimal

   138 expansion of the number. We then use the lemma @{text

   139 "three_div_general"} to prove our final theorem. *}

   140

   141 subsubsection {* Definitions of length and digit sum *}

   142

   143 text {* This section introduces some functions to calculate the

   144 required properties of natural numbers. We then proceed to prove some

   145 properties of these functions.

   146

   147 The function @{text "nlen"} returns the number of digits in a natural

   148 number n. *}

   149

   150 consts nlen :: "nat \<Rightarrow> nat"

   151 recdef nlen "measure id"

   152   "nlen 0 = 0"

   153   "nlen x = 1 + nlen (x div 10)"

   154

   155 text {* The function @{text "sumdig"} returns the sum of all digits in

   156 some number n. *}

   157

   158 definition

   159   sumdig :: "nat \<Rightarrow> nat"

   160   "sumdig n = (\<Sum>x < nlen n. n div 10^x mod 10)"

   161

   162 text {* Some properties of these functions follow. *}

   163

   164 lemma nlen_zero:

   165   "0 = nlen x \<Longrightarrow> x = 0"

   166   by (induct x rule: nlen.induct) auto

   167

   168 lemma nlen_suc:

   169   "Suc m = nlen n \<Longrightarrow> m = nlen (n div 10)"

   170   by (induct n rule: nlen.induct) simp_all

   171

   172

   173 text {* The following lemma is the principle lemma required to prove

   174 our theorem. It states that an expansion of some natural number $n$

   175 into a sequence of its individual digits is always possible. *}

   176

   177 lemma exp_exists:

   178   "m = (\<Sum>x<nlen m. (m div (10::nat)^x mod 10) * 10^x)"

   179 proof (induct nd \<equiv> "nlen m" fixing: m)

   180   case 0 thus ?case by (simp add: nlen_zero)

   181 next

   182   case (Suc nd)

   183   hence IH:

   184     "nd = nlen (m div 10) \<Longrightarrow>

   185     m div 10 = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x)"

   186     by blast

   187   have "\<exists>c. m = 10*(m div 10) + c \<and> c < 10" by presburger

   188   then obtain c where mexp: "m = 10*(m div 10) + c \<and> c < 10" ..

   189   then have cdef: "c = m mod 10" by arith

   190   show "m = (\<Sum>x<nlen m. m div 10^x mod 10 * 10^x)"

   191   proof -

   192     from Suc nd = nlen m

   193     have "nd = nlen (m div 10)" by (rule nlen_suc)

   194     with IH have

   195       "m div 10 = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x)" by simp

   196     with mexp have

   197       "m = 10*(\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x) + c" by simp

   198     also have

   199       "\<dots> = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^(x+1)) + c"

   200       by (subst setsum_right_distrib) (simp add: mult_ac)

   201     also have

   202       "\<dots> = (\<Sum>x<nd. m div 10^(Suc x) mod 10 * 10^(Suc x)) + c"

   203       by (simp add: div_mult2_eq[symmetric])

   204     also have

   205       "\<dots> = (\<Sum>x\<in>{Suc 0..<Suc nd}. m div 10^x  mod 10 * 10^x) + c"

   206       by (simp only: setsum_shift_bounds_Suc_ivl)

   207          (simp add: atLeast0LessThan)

   208     also have

   209       "\<dots> = (\<Sum>x<Suc nd. m div 10^x mod 10 * 10^x)"

   210       by (simp add: setsum_head_upt cdef)

   211     also note Suc nd = nlen m

   212     finally

   213     show "m = (\<Sum>x<nlen m. m div 10^x mod 10 * 10^x)" .

   214   qed

   215 qed

   216

   217

   218 subsubsection {* Final theorem *}

   219

   220 text {* We now combine the general theorem @{text "three_div_general"}

   221 and existence result of @{text "exp_exists"} to prove our final

   222 theorem. *}

   223

   224 theorem three_divides_nat:

   225   shows "(3 dvd n) = (3 dvd sumdig n)"

   226 proof (unfold sumdig_def)

   227   have "n = (\<Sum>x<nlen n. (n div (10::nat)^x mod 10) * 10^x)"

   228     by (rule exp_exists)

   229   moreover

   230   have "3 dvd (\<Sum>x<nlen n. (n div (10::nat)^x mod 10) * 10^x) =

   231         (3 dvd (\<Sum>x<nlen n. n div 10^x mod 10))"

   232     by (rule three_div_general)

   233   ultimately

   234   show "3 dvd n = (3 dvd (\<Sum>x<nlen n. n div 10^x mod 10))" by simp

   235 qed

   236

   237

   238 end