src/HOL/ex/ThreeDivides.thy
author kleing
Mon Feb 20 21:51:50 2006 +0100 (2006-02-20)
changeset 19114 dfe6ace301c3
parent 19106 6e6b5b1fdc06
child 19279 48b527d0331b
permissions -rw-r--r--
fixed
     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 constdefs 
   159   sumdig :: "nat \<Rightarrow> nat"
   160   "sumdig n \<equiv> \<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_mult) (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