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