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--
added lemmas
     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