src/HOL/ex/ThreeDivides.thy
 author nipkow Fri Mar 06 17:38:47 2009 +0100 (2009-03-06) changeset 30313 b2441b0c8d38 parent 29974 ca93255656a5 child 33025 cc038dc8f412 permissions -rw-r--r--
     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 subsection {* 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

    31 subsection {* Formal proof *}

    32

    33 subsubsection {* Miscellaneous summation lemmas *}

    34

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

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

    37

    38 lemma div_sum:

    39   fixes a::nat and n::nat

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

    41 proof (induct n)

    42   case 0 show ?case by simp

    43 next

    44   case (Suc n)

    45   from Suc

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

    47   with Suc

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

    49   thus ?case by simp

    50 qed

    51

    52

    53 subsubsection {* Generalised Three Divides *}

    54

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

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

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

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

    59

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

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

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

    63

    64 lemma digit_diff_split:

    65   fixes n::nat and nd::nat and x::nat

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

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

    68 by (simp add: sum_diff_distrib diff_mult_distrib2)

    69

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

    71 lemma three_divs_0:

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

    73 proof (induct x)

    74   case 0 show ?case by simp

    75 next

    76   case (Suc n)

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

    78   have "?thr dvd 9" by simp

    79   moreover

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

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

    82   ultimately

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

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

    85   thus ?case by simp

    86 qed

    87

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

    89 lemma three_divs_1:

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

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

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

    93

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

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

    96 *}

    97 lemma three_divs_2:

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

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

   100 proof -

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

   102   thus ?thesis by (simp only: digit_diff_split)

   103 qed

   104

   105 text {*

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

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

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

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

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

   111 *}

   112 lemma three_div_general:

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

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

   115 proof

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

   117     by (rule setsum_mono) simp

   118   txt {* This lets us form the term

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

   120

   121   {

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

   123     with three_divs_2 mono

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

   125       by (blast intro: dvd_diffD)

   126   }

   127   {

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

   129     with three_divs_2 mono

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

   131       by (blast intro: dvd_diffD1)

   132   }

   133 qed

   134

   135

   136 subsubsection {* Three Divides Natural *}

   137

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

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

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

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

   142

   143

   144 text {* \medskip Definitions of length and digit sum. *}

   145

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

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

   148 properties of these functions.

   149

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

   151 number n. *}

   152

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

   154 recdef nlen "measure id"

   155   "nlen 0 = 0"

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

   157

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

   159 some number n. *}

   160

   161 definition

   162   sumdig :: "nat \<Rightarrow> nat" where

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

   164

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

   166

   167 lemma nlen_zero:

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

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

   170

   171 lemma nlen_suc:

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

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

   174

   175

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

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

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

   179

   180 lemma exp_exists:

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

   182 proof (induct nd \<equiv> "nlen m" arbitrary: m)

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

   184 next

   185   case (Suc nd)

   186   hence IH:

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

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

   189     by blast

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

   191     and cdef: "c = m mod 10" by simp

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

   193   proof -

   194     from Suc nd = nlen m

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

   196     with IH have

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

   198     with mexp have

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

   200     also have

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

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

   203     also have

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

   205       by (simp add: div_mult2_eq[symmetric])

   206     also have

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

   208       by (simp only: setsum_shift_bounds_Suc_ivl)

   209          (simp add: atLeast0LessThan)

   210     also have

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

   212       by (simp add: atLeast0LessThan[symmetric] setsum_head_upt_Suc cdef)

   213     also note Suc nd = nlen m

   214     finally

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

   216   qed

   217 qed

   218

   219

   220 text {* \medskip Final theorem. *}

   221

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

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

   224 theorem. *}

   225

   226 theorem three_divides_nat:

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

   228 proof (unfold sumdig_def)

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

   230     by (rule exp_exists)

   231   moreover

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

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

   234     by (rule three_div_general)

   235   ultimately

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

   237 qed

   238

   239 end