src/HOL/ex/ThreeDivides.thy
 author wenzelm Mon Aug 31 21:28:08 2015 +0200 (2015-08-31) changeset 61070 b72a990adfe2 parent 58889 5b7a9633cfa8 child 61343 5b5656a63bd6 permissions -rw-r--r--
prefer symbols;
     1 (*  Title:      HOL/ex/ThreeDivides.thy

     2     Author:     Benjamin Porter, 2005

     3 *)

     4

     5 section {* Three Divides Theorem *}

     6

     7 theory ThreeDivides

     8 imports Main "~~/src/HOL/Library/LaTeXsugar"

     9 begin

    10

    11 subsection {* Abstract *}

    12

    13 text {*

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

    15 formalised in the Isabelle/Isar theorem proving system.

    16

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

    18 digits in $n$.

    19

    20 {\em Informal Proof}:

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

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

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

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

    26 @{text "\<box>"}

    27 *}

    28

    29

    30 subsection {* Formal proof *}

    31

    32 subsubsection {* 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

    52 subsubsection {* Generalised Three Divides *}

    53

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

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

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

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

    58

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

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

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

    62

    63 lemma digit_diff_split:

    64   fixes n::nat and nd::nat and x::nat

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

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

    67 by (simp add: sum_diff_distrib diff_mult_distrib2)

    68

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

    70 lemma three_divs_0:

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

    72 proof (induct x)

    73   case 0 show ?case by simp

    74 next

    75   case (Suc n)

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

    77   have "?thr dvd 9" by simp

    78   moreover

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

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

    81   ultimately

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

    83     by (simp only: ac_simps) (rule dvd_add)

    84   thus ?case by simp

    85 qed

    86

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

    88 lemma three_divs_1:

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

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

    91   by (subst mult.commute, rule div_sum) (simp add: three_divs_0 [simplified])

    92

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

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

    95 *}

    96 lemma three_divs_2:

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

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

    99 proof -

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

   101   thus ?thesis by (simp only: digit_diff_split)

   102 qed

   103

   104 text {*

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

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

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

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

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

   110 *}

   111 lemma three_div_general:

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

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

   114 proof

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

   116     by (rule setsum_mono) simp

   117   txt {* This lets us form the term

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

   119

   120   {

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

   122     with three_divs_2 mono

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

   124       by (blast intro: dvd_diffD)

   125   }

   126   {

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

   128     with three_divs_2 mono

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

   130       by (blast intro: dvd_diffD1)

   131   }

   132 qed

   133

   134

   135 subsubsection {* Three Divides Natural *}

   136

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

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

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

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

   141

   142

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

   144

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

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

   147 properties of these functions.

   148

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

   150 number n. *}

   151

   152 fun nlen :: "nat \<Rightarrow> nat"

   153 where

   154   "nlen 0 = 0"

   155 | "nlen x = 1 + nlen (x div 10)"

   156

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

   158 some number n. *}

   159

   160 definition

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

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

   163

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

   165

   166 lemma nlen_zero:

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

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

   169

   170 lemma nlen_suc:

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

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

   173

   174

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

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

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

   178

   179 lemma exp_exists:

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

   181 proof (induct "nlen m" arbitrary: m)

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

   183 next

   184   case (Suc nd)

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

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

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

   188   proof -

   189     from Suc nd = nlen m

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

   191     with Suc have

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

   193     with mexp have

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

   195     also have

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

   197       by (subst setsum_right_distrib) (simp add: ac_simps)

   198     also have

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

   200       by (simp add: div_mult2_eq[symmetric])

   201     also have

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

   203       by (simp only: setsum_shift_bounds_Suc_ivl)

   204          (simp add: atLeast0LessThan)

   205     also have

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

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

   208     also note Suc nd = nlen m

   209     finally

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

   211   qed

   212 qed

   213

   214

   215 text {* \medskip Final theorem. *}

   216

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

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

   219 theorem. *}

   220

   221 theorem three_divides_nat:

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

   223 proof (unfold sumdig_def)

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

   225     by (rule exp_exists)

   226   moreover

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

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

   229     by (rule three_div_general)

   230   ultimately

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

   232 qed

   233

   234 end