src/HOL/ex/ThreeDivides.thy
author wenzelm
Wed Jun 22 10:09:20 2016 +0200 (2016-06-22)
changeset 63343 fb5d8a50c641
parent 61933 cf58b5b794b2
child 63918 6bf55e6e0b75
permissions -rw-r--r--
bundle lifting_syntax;
     1 (*  Title:      HOL/ex/ThreeDivides.thy
     2     Author:     Benjamin Porter, 2005
     3 *)
     4 
     5 section \<open>Three Divides Theorem\<close>
     6 
     7 theory ThreeDivides
     8 imports Main "~~/src/HOL/Library/LaTeXsugar"
     9 begin
    10 
    11 subsection \<open>Abstract\<close>
    12 
    13 text \<open>
    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 \<open>\<box>\<close>
    27 \<close>
    28 
    29 
    30 subsection \<open>Formal proof\<close>
    31 
    32 subsubsection \<open>Miscellaneous summation lemmas\<close>
    33 
    34 text \<open>If $a$ divides \<open>A x\<close> for all x then $a$ divides any
    35 sum over terms of the form \<open>(A x)*(P x)\<close> for arbitrary $P$.\<close>
    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 \<open>Generalised Three Divides\<close>
    53 
    54 text \<open>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.\<close>
    58 
    59 text \<open>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.\<close>
    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 \<open>Now we prove that 3 always divides numbers of the form $10^x - 1$.\<close>
    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 \<open>Expanding on the previous lemma and lemma \<open>div_sum\<close>.\<close>
    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 \<open>Using lemmas \<open>digit_diff_split\<close> and 
    94 \<open>three_divs_1\<close> we now prove the following lemma. 
    95 \<close>
    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 \<open>
   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 \<close>
   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 \<open>This lets us form the term
   118          @{term "(\<Sum>x<nd. D x * 10^x) - (\<Sum>x<nd. D x)"}\<close>
   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 \<open>Three Divides Natural\<close>
   136 
   137 text \<open>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 \<open>three_div_general\<close> to prove our final theorem.\<close>
   140 
   141 
   142 text \<open>\medskip Definitions of length and digit sum.\<close>
   143 
   144 text \<open>This section introduces some functions to calculate the
   145 required properties of natural numbers. We then proceed to prove some
   146 properties of these functions.
   147 
   148 The function \<open>nlen\<close> returns the number of digits in a natural
   149 number n.\<close>
   150 
   151 fun nlen :: "nat \<Rightarrow> nat"
   152 where
   153   "nlen 0 = 0"
   154 | "nlen x = 1 + nlen (x div 10)"
   155 
   156 text \<open>The function \<open>sumdig\<close> returns the sum of all digits in
   157 some number n.\<close>
   158 
   159 definition
   160   sumdig :: "nat \<Rightarrow> nat" where
   161   "sumdig n = (\<Sum>x < nlen n. n div 10^x mod 10)"
   162 
   163 text \<open>Some properties of these functions follow.\<close>
   164 
   165 lemma nlen_zero:
   166   "0 = nlen x \<Longrightarrow> x = 0"
   167   by (induct x rule: nlen.induct) auto
   168 
   169 lemma nlen_suc:
   170   "Suc m = nlen n \<Longrightarrow> m = nlen (n div 10)"
   171   by (induct n rule: nlen.induct) simp_all
   172 
   173 
   174 text \<open>The following lemma is the principle lemma required to prove
   175 our theorem. It states that an expansion of some natural number $n$
   176 into a sequence of its individual digits is always possible.\<close>
   177 
   178 lemma exp_exists:
   179   "m = (\<Sum>x<nlen m. (m div (10::nat)^x mod 10) * 10^x)"
   180 proof (induct "nlen m" arbitrary: m)
   181   case 0 thus ?case by (simp add: nlen_zero)
   182 next
   183   case (Suc nd)
   184   obtain c where mexp: "m = 10*(m div 10) + c \<and> c < 10"
   185     and cdef: "c = m mod 10" by simp
   186   show "m = (\<Sum>x<nlen m. m div 10^x mod 10 * 10^x)"
   187   proof -
   188     from \<open>Suc nd = nlen m\<close>
   189     have "nd = nlen (m div 10)" by (rule nlen_suc)
   190     with Suc have
   191       "m div 10 = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x)" by simp
   192     with mexp have
   193       "m = 10*(\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x) + c" by simp
   194     also have
   195       "\<dots> = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^(x+1)) + c"
   196       by (subst setsum_right_distrib) (simp add: ac_simps)
   197     also have
   198       "\<dots> = (\<Sum>x<nd. m div 10^(Suc x) mod 10 * 10^(Suc x)) + c"
   199       by (simp add: div_mult2_eq[symmetric])
   200     also have
   201       "\<dots> = (\<Sum>x\<in>{Suc 0..<Suc nd}. m div 10^x  mod 10 * 10^x) + c"
   202       by (simp only: setsum_shift_bounds_Suc_ivl)
   203          (simp add: atLeast0LessThan)
   204     also have
   205       "\<dots> = (\<Sum>x<Suc nd. m div 10^x mod 10 * 10^x)"
   206       by (simp add: atLeast0LessThan[symmetric] setsum_head_upt_Suc cdef)
   207     also note \<open>Suc nd = nlen m\<close>
   208     finally
   209     show "m = (\<Sum>x<nlen m. m div 10^x mod 10 * 10^x)" .
   210   qed
   211 qed
   212 
   213 
   214 text \<open>\medskip Final theorem.\<close>
   215 
   216 text \<open>We now combine the general theorem \<open>three_div_general\<close>
   217 and existence result of \<open>exp_exists\<close> to prove our final
   218 theorem.\<close>
   219 
   220 theorem three_divides_nat:
   221   shows "(3 dvd n) = (3 dvd sumdig n)"
   222 proof (unfold sumdig_def)
   223   have "n = (\<Sum>x<nlen n. (n div (10::nat)^x mod 10) * 10^x)"
   224     by (rule exp_exists)
   225   moreover
   226   have "3 dvd (\<Sum>x<nlen n. (n div (10::nat)^x mod 10) * 10^x) =
   227         (3 dvd (\<Sum>x<nlen n. n div 10^x mod 10))"
   228     by (rule three_div_general)
   229   ultimately 
   230   show "3 dvd n = (3 dvd (\<Sum>x<nlen n. n div 10^x mod 10))" by simp
   231 qed
   232 
   233 end