src/HOL/ex/ThreeDivides.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 41413 64cd30d6b0b8
child 57512 cc97b347b301
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
     1 (*  Title:      HOL/ex/ThreeDivides.thy
     2     Author:     Benjamin Porter, 2005
     3 *)
     4 
     5 header {* 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: add_ac) (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 nat_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: mult_ac)
   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