src/HOL/ex/ThreeDivides.thy
author kleing
Sun Feb 12 10:42:19 2006 +0100 (2006-02-12)
changeset 19022 0e6ec4fd204c
child 19026 87cd1ecae3a4
permissions -rw-r--r--
* moved ThreeDivides from Isar_examples to better suited HOL/ex
* moved 2 summation lemmas from ThreeDivides to SetInterval
kleing@19022
     1
(*  Title:      HOL/Isar_examples/ThreeDivides.thy
kleing@19022
     2
    ID:         $Id$
kleing@19022
     3
    Author:     Benjamin Porter, 2005
kleing@19022
     4
*)
kleing@19022
     5
kleing@19022
     6
header {* Three Divides Theorem *}
kleing@19022
     7
kleing@19022
     8
theory ThreeDivides
kleing@19022
     9
imports Main LaTeXsugar
kleing@19022
    10
begin
kleing@19022
    11
kleing@19022
    12
section {* Abstract *}
kleing@19022
    13
kleing@19022
    14
text {*
kleing@19022
    15
The following document presents a proof of the Three Divides N theorem
kleing@19022
    16
formalised in the Isabelle/Isar theorem proving system.
kleing@19022
    17
kleing@19022
    18
{\em Theorem}: 3 divides n if and only if 3 divides the sum of all
kleing@19022
    19
digits in n.
kleing@19022
    20
kleing@19022
    21
{\em Informal Proof}:
kleing@19022
    22
Take $n = \sum{n_j * 10^j}$ where $n_j$ is the $j$'th least
kleing@19022
    23
significant digit of the decimal denotation of the number n and the
kleing@19022
    24
sum ranges over all digits. Then $$ (n - \sum{n_j}) = \sum{n_j * (10^j
kleing@19022
    25
- 1)} $$ We know $\forall j\; 3|(10^j - 1) $ and hence $3|LHS$,
kleing@19022
    26
therefore $$\forall n\; 3|n \Longleftrightarrow 3|\sum{n_j}$$
kleing@19022
    27
@{text "\<box>"}
kleing@19022
    28
*}
kleing@19022
    29
kleing@19022
    30
section {* Formal proof *}
kleing@19022
    31
kleing@19022
    32
subsection {* Miscellaneous summation lemmas *}
kleing@19022
    33
kleing@19022
    34
text {* If $a$ divides @{text "A x"} for all x then $a$ divides any
kleing@19022
    35
sum over terms of the form @{text "(A x)*(P x)"} for arbitrary $P$. *}
kleing@19022
    36
kleing@19022
    37
lemma div_sum:
kleing@19022
    38
  fixes a::nat and n::nat
kleing@19022
    39
  shows "\<forall>x. a dvd A x \<Longrightarrow> a dvd (\<Sum>x<n. A x * D x)"
kleing@19022
    40
proof (induct n)
kleing@19022
    41
  case 0 show ?case by simp
kleing@19022
    42
next
kleing@19022
    43
  case (Suc n)
kleing@19022
    44
  from Suc
kleing@19022
    45
  have "a dvd (A n * D n)" by (simp add: dvd_mult2)
kleing@19022
    46
  with Suc
kleing@19022
    47
  have "a dvd ((\<Sum>x<n. A x * D x) + (A n * D n))" by (simp add: dvd_add)
kleing@19022
    48
  thus ?case by simp
kleing@19022
    49
qed
kleing@19022
    50
kleing@19022
    51
subsection {* Generalised Three Divides *}
kleing@19022
    52
kleing@19022
    53
text {* This section solves a generalised form of the three divides
kleing@19022
    54
problem. Here we show that for any sequence of numbers the theorem
kleing@19022
    55
holds. In the next section we specialise this theorem to apply
kleing@19022
    56
directly to the decimal expansion of the natural numbers. *}
kleing@19022
    57
kleing@19022
    58
text {* Here we show that the first statement in the informal proof is
kleing@19022
    59
true for all natural numbers. Note we are using @{term "D i"} to
kleing@19022
    60
denote the $i$'th element in a sequence of numbers. *}
kleing@19022
    61
kleing@19022
    62
lemma digit_diff_split:
kleing@19022
    63
  fixes n::nat and nd::nat and x::nat
kleing@19022
    64
  shows "\<And>n. n = (\<Sum>x\<in>{..<nd}. (D x)*((10::nat)^x)) \<Longrightarrow>
kleing@19022
    65
             (n - (\<Sum>x<nd. (D x))) = (\<Sum>x<nd. (D x)*(10^x - 1))"
kleing@19022
    66
by (simp add: sum_diff_distrib diff_mult_distrib2)
kleing@19022
    67
kleing@19022
    68
text {* Now we prove that 3 always divides numbers of the form $10^x - 1$. *}
kleing@19022
    69
lemma three_divs_0 [rule_format, simplified]:
kleing@19022
    70
  shows "(3::nat) dvd (10^x - 1)"
kleing@19022
    71
proof (induct x)
kleing@19022
    72
  case 0 show ?case by simp
kleing@19022
    73
next
kleing@19022
    74
  case (Suc n)
kleing@19022
    75
  let ?thr = "(3::nat)"
kleing@19022
    76
  have "?thr dvd 9" by simp
kleing@19022
    77
  moreover
kleing@19022
    78
  have "?thr dvd (10*(10^n - 1))" by (rule dvd_mult)
kleing@19022
    79
  hence "?thr dvd (10^(n+1) - 10)" by (simp add: nat_distrib)
kleing@19022
    80
  ultimately
kleing@19022
    81
  have"?thr dvd ((10^(n+1) - 10) + 9)"
kleing@19022
    82
    by (simp only: add_ac) (rule dvd_add)
kleing@19022
    83
  thus ?case by simp
kleing@19022
    84
qed
kleing@19022
    85
kleing@19022
    86
text {* Expanding on the previous lemma and lemma @{text "div_sum\<dots>"} *}
kleing@19022
    87
lemma three_divs_1:
kleing@19022
    88
  fixes D :: "nat \<Rightarrow> nat"
kleing@19022
    89
  shows "3 dvd (\<Sum>x<nd. D x * (10^x - 1))"
kleing@19022
    90
  by (subst nat_mult_commute, rule div_sum) (simp add: three_divs_0)
kleing@19022
    91
kleing@19022
    92
text {* Using lemmas @{text "digit_diff_split"} and 
kleing@19022
    93
@{text "three_divs_1"} we now prove the following lemma. 
kleing@19022
    94
*}
kleing@19022
    95
lemma three_divs_2:
kleing@19022
    96
  fixes nd::nat and D::"nat\<Rightarrow>nat"
kleing@19022
    97
  shows "3 dvd ((\<Sum>x<nd. (D x)*(10^x)) - (\<Sum>x<nd. (D x)))"
kleing@19022
    98
proof (simp only: digit_diff_split)
kleing@19022
    99
  from three_divs_1 show "3 dvd (\<Sum>x<nd. D x * (10 ^ x - 1))" .
kleing@19022
   100
qed
kleing@19022
   101
kleing@19022
   102
text {* 
kleing@19022
   103
We now present the final theorem of this section. For any
kleing@19022
   104
sequence of numbers (defined by a function @{term "D :: (nat\<Rightarrow>nat)"}),
kleing@19022
   105
we show that 3 divides the expansive sum $\sum{(D\;x)*10^x}$ over $x$
kleing@19022
   106
if and only if 3 divides the sum of the individual numbers
kleing@19022
   107
$\sum{D\;x}$. 
kleing@19022
   108
*}
kleing@19022
   109
lemma three_div_general:
kleing@19022
   110
  fixes D :: "nat \<Rightarrow> nat"
kleing@19022
   111
  shows "(3 dvd (\<Sum>x<nd. D x * 10^x)) = (3 dvd (\<Sum>x<nd. D x))"
kleing@19022
   112
proof
kleing@19022
   113
  have mono: "(\<Sum>x<nd. D x) \<le> (\<Sum>x<nd. D x * 10^x)"
kleing@19022
   114
    by (rule setsum_mono, simp)
kleing@19022
   115
  txt {* This lets us form the term
kleing@19022
   116
         @{term "(\<Sum>x<nd. D x * 10^x) - (\<Sum>x<nd. D x)"} *}
kleing@19022
   117
kleing@19022
   118
  {
kleing@19022
   119
    assume "3 dvd (\<Sum>x<nd. D x)"
kleing@19022
   120
    with three_divs_2 mono
kleing@19022
   121
    show "3 dvd (\<Sum>x<nd. D x * 10^x)" 
kleing@19022
   122
      by (blast intro: dvd_diffD)
kleing@19022
   123
  }
kleing@19022
   124
  {
kleing@19022
   125
    assume "3 dvd (\<Sum>x<nd. D x * 10^x)"
kleing@19022
   126
    with three_divs_2 mono
kleing@19022
   127
    show "3 dvd (\<Sum>x<nd. D x)"
kleing@19022
   128
      by (blast intro: dvd_diffD1)
kleing@19022
   129
  }
kleing@19022
   130
qed
kleing@19022
   131
kleing@19022
   132
kleing@19022
   133
subsection {* Three Divides Natural *}
kleing@19022
   134
kleing@19022
   135
text {* This section shows that for all natural numbers we can
kleing@19022
   136
generate a sequence of digits less than ten that represent the decimal
kleing@19022
   137
expansion of the number. We then use the lemma @{text
kleing@19022
   138
"three_div_general"} to prove our final theorem. *}
kleing@19022
   139
kleing@19022
   140
subsubsection {* Definitions of length and digit sum *}
kleing@19022
   141
kleing@19022
   142
text {* This section introduces some functions to calculate the
kleing@19022
   143
required properties of natural numbers. We then proceed to prove some
kleing@19022
   144
properties of these functions.
kleing@19022
   145
kleing@19022
   146
The function @{text "nlen"} returns the number of digits in a natural
kleing@19022
   147
number n. *}
kleing@19022
   148
kleing@19022
   149
consts nlen :: "nat \<Rightarrow> nat"
kleing@19022
   150
recdef nlen "measure id"
kleing@19022
   151
  "nlen 0 = 0"
kleing@19022
   152
  "nlen x = 1 + nlen (x div 10)"
kleing@19022
   153
kleing@19022
   154
text {* The function @{text "sumdig"} returns the sum of all digits in
kleing@19022
   155
some number n. *}
kleing@19022
   156
kleing@19022
   157
constdefs 
kleing@19022
   158
  sumdig :: "nat \<Rightarrow> nat"
kleing@19022
   159
  "sumdig n \<equiv> \<Sum>x < nlen n. n div 10^x mod 10"
kleing@19022
   160
kleing@19022
   161
text {* Some properties of these functions follow. *}
kleing@19022
   162
kleing@19022
   163
lemma nlen_zero:
kleing@19022
   164
  "0 = nlen x \<Longrightarrow> x = 0"
kleing@19022
   165
  by (induct x rule: nlen.induct) auto
kleing@19022
   166
kleing@19022
   167
lemma nlen_suc:
kleing@19022
   168
  "Suc m = nlen n \<Longrightarrow> m = nlen (n div 10)"
kleing@19022
   169
  by (induct n rule: nlen.induct) simp_all
kleing@19022
   170
kleing@19022
   171
kleing@19022
   172
text {* The following lemma is the principle lemma required to prove
kleing@19022
   173
our theorem. It states that an expansion of some natural number $n$
kleing@19022
   174
into a sequence of its individual digits is always possible. *}
kleing@19022
   175
kleing@19022
   176
lemma exp_exists:
kleing@19022
   177
  "\<And>m. nd = nlen m \<Longrightarrow> m = (\<Sum>x<nd. (m div (10::nat)^x mod 10) * 10^x)"
kleing@19022
   178
proof (induct nd)
kleing@19022
   179
  case 0 thus ?case by (simp add: nlen_zero)
kleing@19022
   180
next
kleing@19022
   181
  case (Suc nd)
kleing@19022
   182
  hence IH:
kleing@19022
   183
    "nd = nlen (m div 10) \<Longrightarrow>
kleing@19022
   184
    m div 10 = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x)"
kleing@19022
   185
    by blast
kleing@19022
   186
  have "\<exists>c. m = 10*(m div 10) + c \<and> c < 10" by presburger
kleing@19022
   187
  from this obtain c where mexp: "m = 10*(m div 10) + c \<and> c < 10" ..
kleing@19022
   188
  then have cdef: "c = m mod 10" by arith
kleing@19022
   189
  show "m = (\<Sum>x<Suc nd. m div 10^x mod 10 * 10^x)"
kleing@19022
   190
  proof -
kleing@19022
   191
    have "Suc nd = nlen m" .
kleing@19022
   192
    then have
kleing@19022
   193
      "nd = nlen (m div 10)" by (rule nlen_suc)
kleing@19022
   194
    with IH have
kleing@19022
   195
      "m div 10 = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x)"  by simp
kleing@19022
   196
    with mexp have
kleing@19022
   197
      "m = 10*(\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x) + c" by simp
kleing@19022
   198
    also have
kleing@19022
   199
      "\<dots> = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^(x+1)) + c"
kleing@19022
   200
      by (subst setsum_mult) (simp add: mult_ac)
kleing@19022
   201
    also have
kleing@19022
   202
      "\<dots> = (\<Sum>x<nd. m div 10^(Suc x) mod 10 * 10^(Suc x)) + c"
kleing@19022
   203
      by (simp add: div_mult2_eq[symmetric])
kleing@19022
   204
    also have
kleing@19022
   205
      "\<dots> = (\<Sum>x\<in>{Suc 0..<Suc nd}. m div 10^x  mod 10 * 10^x) + c"
kleing@19022
   206
      by (simp only: setsum_shift_bounds_Suc_ivl)
kleing@19022
   207
         (simp add: atLeast0LessThan)
kleing@19022
   208
    also have
kleing@19022
   209
      "\<dots> = (\<Sum>x<Suc nd. m div 10^x mod 10 * 10^x)"
kleing@19022
   210
      by (simp add: setsum_rmv_head [symmetric] cdef)
kleing@19022
   211
    finally 
kleing@19022
   212
    show "m = (\<Sum>x<Suc nd. m div 10^x mod 10 * 10^x)" .
kleing@19022
   213
  qed
kleing@19022
   214
qed
kleing@19022
   215
kleing@19022
   216
kleing@19022
   217
subsubsection {* Final theorem *}
kleing@19022
   218
kleing@19022
   219
text {* We now combine the general theorem @{text "three_div_general"}
kleing@19022
   220
and existence result of @{text "exp_exists"} to prove our final
kleing@19022
   221
theorem. *}
kleing@19022
   222
kleing@19022
   223
theorem three_divides_nat:
kleing@19022
   224
  shows "(3 dvd n) = (3 dvd sumdig n)"
kleing@19022
   225
proof (unfold sumdig_def)
kleing@19022
   226
  obtain nd where "nd = nlen n" by simp
kleing@19022
   227
  moreover
kleing@19022
   228
  have "n = (\<Sum>x<nd. (n div (10::nat)^x mod 10) * 10^x)"
kleing@19022
   229
    by (rule exp_exists)
kleing@19022
   230
  moreover
kleing@19022
   231
  have "3 dvd (\<Sum>x<nlen n. (n div (10::nat)^x mod 10) * 10^x) =
kleing@19022
   232
        (3 dvd (\<Sum>x<nlen n. n div 10^x mod 10))"
kleing@19022
   233
    by (rule three_div_general)
kleing@19022
   234
  ultimately 
kleing@19022
   235
  show "3 dvd n = (3 dvd (\<Sum>x<nlen n. n div 10^x mod 10))" by simp
kleing@19022
   236
qed
kleing@19022
   237
kleing@19022
   238
kleing@19022
   239
end