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