* moved ThreeDivides from Isar_examples to better suited HOL/ex
authorkleing
Sun Feb 12 10:42:19 2006 +0100 (2006-02-12)
changeset 190220e6ec4fd204c
parent 19021 0111ecc5490e
child 19023 5652a536b7e8
* moved ThreeDivides from Isar_examples to better suited HOL/ex
* moved 2 summation lemmas from ThreeDivides to SetInterval
src/HOL/Isar_examples/ROOT.ML
src/HOL/Isar_examples/ThreeDivides.thy
src/HOL/SetInterval.thy
src/HOL/ex/ROOT.ML
src/HOL/ex/ThreeDivides.thy
     1.1 --- a/src/HOL/Isar_examples/ROOT.ML	Sun Feb 12 04:31:18 2006 +0100
     1.2 +++ b/src/HOL/Isar_examples/ROOT.ML	Sun Feb 12 10:42:19 2006 +0100
     1.3 @@ -14,7 +14,6 @@
     1.4  time_use_thy "Summation";
     1.5  time_use_thy "KnasterTarski";
     1.6  time_use_thy "MutilatedCheckerboard";
     1.7 -time_use_thy "ThreeDivides";
     1.8  with_path "../NumberTheory" (no_document time_use_thy) "Primes";
     1.9  with_path "../NumberTheory" time_use_thy "Fibonacci";
    1.10  time_use_thy "Puzzle";
     2.1 --- a/src/HOL/Isar_examples/ThreeDivides.thy	Sun Feb 12 04:31:18 2006 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,291 +0,0 @@
     2.4 -(*  Title:      HOL/Isar_examples/ThreeDivides.thy
     2.5 -    ID:         $Id$
     2.6 -    Author:     Benjamin Porter, 2005
     2.7 -*)
     2.8 -
     2.9 -header {* Three Divides Theorem *}
    2.10 -
    2.11 -theory ThreeDivides
    2.12 -imports Main LaTeXsugar
    2.13 -begin
    2.14 -
    2.15 -section {* Abstract *}
    2.16 -
    2.17 -text {*
    2.18 -The following document presents a proof of the Three Divides N theorem
    2.19 -formalised in the Isabelle/Isar theorem proving system.
    2.20 -
    2.21 -{\em Theorem}: 3 divides n if and only if 3 divides the sum of all
    2.22 -digits in n.
    2.23 -
    2.24 -{\em Informal Proof}:
    2.25 -Take $n = \sum{n_j * 10^j}$ where $n_j$ is the $j$'th least
    2.26 -significant digit of the decimal denotation of the number n and the
    2.27 -sum ranges over all digits. Then $$ (n - \sum{n_j}) = \sum{n_j * (10^j
    2.28 -- 1)} $$ We know $\forall j\; 3|(10^j - 1) $ and hence $3|LHS$,
    2.29 -therefore $$\forall n\; 3|n \Longleftrightarrow 3|\sum{n_j}$$
    2.30 -@{text "\<box>"}
    2.31 -*}
    2.32 -
    2.33 -section {* Formal proof *}
    2.34 -
    2.35 -subsection {* Miscellaneous summation lemmas *}
    2.36 -
    2.37 -text {* We can decompose a sum into an expanded form by removing
    2.38 -its first element. *}
    2.39 -
    2.40 -lemma sum_rmv_head:
    2.41 -  fixes m::nat
    2.42 -  assumes m: "0 < m"
    2.43 -  shows "(\<Sum>x<m. P x) = P 0 + (\<Sum>x\<in>{1..<m}. P x)"
    2.44 -  (is "?lhs = ?rhs")
    2.45 -proof -
    2.46 -  let ?a = "\<Sum>x\<in>({0} \<union> {0<..<m}). P x"
    2.47 -  from m
    2.48 -  have "{0..<m} = {0} \<union> {0<..<m}"
    2.49 -    by (simp only: ivl_disj_un_singleton)
    2.50 -  hence "?lhs = ?a"
    2.51 -    by (simp add: atLeast0LessThan)
    2.52 -  moreover
    2.53 -  have "?a = ?rhs"
    2.54 -    by (simp add: setsum_Un ivl_disj_int 
    2.55 -                  atLeastSucLessThan_greaterThanLessThan)
    2.56 -  ultimately 
    2.57 -  show ?thesis by simp
    2.58 -qed
    2.59 -
    2.60 -text {* This lemma states that the difference of two sums ranging over
    2.61 -the same elements is the sum of their individual differences. *}
    2.62 -
    2.63 -lemma sum_distrib [rule_format]:
    2.64 -  fixes x::nat and P::"nat\<Rightarrow>nat"
    2.65 -  shows
    2.66 -  "\<forall>x. Q x \<le> P x  \<Longrightarrow>
    2.67 -  (\<Sum>x<n. P x) - (\<Sum>x<n. Q x) = (\<Sum>x<n. P x - Q x)"
    2.68 -proof (induct n)
    2.69 -  case 0 show ?case by simp
    2.70 -next
    2.71 -  case (Suc n)
    2.72 -
    2.73 -  let ?lhs = "(\<Sum>x<n. P x) - (\<Sum>x<n. Q x)"
    2.74 -  let ?rhs = "\<Sum>x<n. P x - Q x"
    2.75 -
    2.76 -  from Suc have "?lhs = ?rhs" by simp
    2.77 -  moreover
    2.78 -  from Suc have "?lhs + P n - Q n = ?rhs + (P n - Q n)" by simp
    2.79 -  moreover
    2.80 -  from Suc have
    2.81 -    "(\<Sum>x<n. P x) + P n - ((\<Sum>x<n. Q x) + Q n) = ?rhs + (P n - Q n)"
    2.82 -    by (subst diff_diff_left[symmetric],
    2.83 -        subst diff_add_assoc2)
    2.84 -       (auto simp: diff_add_assoc2 intro: setsum_mono)
    2.85 -  ultimately
    2.86 -  show ?case by simp
    2.87 -qed
    2.88 -
    2.89 -text {* If $a$ divides @{text "A x"} for all x then $a$ divides any
    2.90 -sum over terms of the form @{text "(A x)*(P x)"} for arbitrary $P$. *}
    2.91 -
    2.92 -lemma div_sum:
    2.93 -  fixes a::nat and n::nat
    2.94 -  shows "\<forall>x. a dvd A x \<Longrightarrow> a dvd (\<Sum>x<n. A x * D x)"
    2.95 -proof (induct n)
    2.96 -  case 0 show ?case by simp
    2.97 -next
    2.98 -  case (Suc n)
    2.99 -  from Suc
   2.100 -  have "a dvd (A n * D n)" by (simp add: dvd_mult2)
   2.101 -  with Suc
   2.102 -  have "a dvd ((\<Sum>x<n. A x * D x) + (A n * D n))" by (simp add: dvd_add)
   2.103 -  thus ?case by simp
   2.104 -qed
   2.105 -
   2.106 -subsection {* Generalised Three Divides *}
   2.107 -
   2.108 -text {* This section solves a generalised form of the three divides
   2.109 -problem. Here we show that for any sequence of numbers the theorem
   2.110 -holds. In the next section we specialise this theorem to apply
   2.111 -directly to the decimal expansion of the natural numbers. *}
   2.112 -
   2.113 -text {* Here we show that the first statement in the informal proof is
   2.114 -true for all natural numbers. Note we are using @{term "D i"} to
   2.115 -denote the $i$'th element in a sequence of numbers. *}
   2.116 -
   2.117 -lemma digit_diff_split:
   2.118 -  fixes n::nat and nd::nat and x::nat
   2.119 -  shows "\<And>n. n = (\<Sum>x\<in>{..<nd}. (D x)*((10::nat)^x)) \<Longrightarrow>
   2.120 -             (n - (\<Sum>x<nd. (D x))) = (\<Sum>x<nd. (D x)*(10^x - 1))"
   2.121 -by (simp add: sum_distrib diff_mult_distrib2)
   2.122 -
   2.123 -text {* Now we prove that 3 always divides numbers of the form $10^x - 1$. *}
   2.124 -lemma three_divs_0 [rule_format, simplified]:
   2.125 -  shows "(3::nat) dvd (10^x - 1)"
   2.126 -proof (induct x)
   2.127 -  case 0 show ?case by simp
   2.128 -next
   2.129 -  case (Suc n)
   2.130 -  let ?thr = "(3::nat)"
   2.131 -  have "?thr dvd 9" by simp
   2.132 -  moreover
   2.133 -  have "?thr dvd (10*(10^n - 1))" by (rule dvd_mult)
   2.134 -  hence "?thr dvd (10^(n+1) - 10)" by (simp add: nat_distrib)
   2.135 -  ultimately
   2.136 -  have"?thr dvd ((10^(n+1) - 10) + 9)"
   2.137 -    by (simp only: add_ac) (rule dvd_add)
   2.138 -  thus ?case by simp
   2.139 -qed
   2.140 -
   2.141 -text {* Expanding on the previous lemma and lemma @{text "div_sum\<dots>"} *}
   2.142 -lemma three_divs_1:
   2.143 -  fixes D :: "nat \<Rightarrow> nat"
   2.144 -  shows "3 dvd (\<Sum>x<nd. D x * (10^x - 1))"
   2.145 -  by (subst nat_mult_commute, rule div_sum) (simp add: three_divs_0)
   2.146 -
   2.147 -text {* Using lemmas @{text "digit_diff_split"} and 
   2.148 -@{text "three_divs_1"} we now prove the following lemma. 
   2.149 -*}
   2.150 -lemma three_divs_2:
   2.151 -  fixes nd::nat and D::"nat\<Rightarrow>nat"
   2.152 -  shows "3 dvd ((\<Sum>x<nd. (D x)*(10^x)) - (\<Sum>x<nd. (D x)))"
   2.153 -proof (simp only: digit_diff_split)
   2.154 -  from three_divs_1 show "3 dvd (\<Sum>x<nd. D x * (10 ^ x - 1))" .
   2.155 -qed
   2.156 -
   2.157 -text {* 
   2.158 -We now present the final theorem of this section. For any
   2.159 -sequence of numbers (defined by a function @{term "D :: (nat\<Rightarrow>nat)"}),
   2.160 -we show that 3 divides the expansive sum $\sum{(D\;x)*10^x}$ over $x$
   2.161 -if and only if 3 divides the sum of the individual numbers
   2.162 -$\sum{D\;x}$. 
   2.163 -*}
   2.164 -lemma three_div_general:
   2.165 -  fixes D :: "nat \<Rightarrow> nat"
   2.166 -  shows "(3 dvd (\<Sum>x<nd. D x * 10^x)) = (3 dvd (\<Sum>x<nd. D x))"
   2.167 -proof
   2.168 -  have mono: "(\<Sum>x<nd. D x) \<le> (\<Sum>x<nd. D x * 10^x)"
   2.169 -    by (rule setsum_mono, simp)
   2.170 -  txt {* This lets us form the term
   2.171 -         @{term "(\<Sum>x<nd. D x * 10^x) - (\<Sum>x<nd. D x)"} *}
   2.172 -
   2.173 -  {
   2.174 -    assume "3 dvd (\<Sum>x<nd. D x)"
   2.175 -    with three_divs_2 mono
   2.176 -    show "3 dvd (\<Sum>x<nd. D x * 10^x)" 
   2.177 -      by (blast intro: dvd_diffD)
   2.178 -  }
   2.179 -  {
   2.180 -    assume "3 dvd (\<Sum>x<nd. D x * 10^x)"
   2.181 -    with three_divs_2 mono
   2.182 -    show "3 dvd (\<Sum>x<nd. D x)"
   2.183 -      by (blast intro: dvd_diffD1)
   2.184 -  }
   2.185 -qed
   2.186 -
   2.187 -
   2.188 -subsection {* Three Divides Natural *}
   2.189 -
   2.190 -text {* This section shows that for all natural numbers we can
   2.191 -generate a sequence of digits less than ten that represent the decimal
   2.192 -expansion of the number. We then use the lemma @{text
   2.193 -"three_div_general"} to prove our final theorem. *}
   2.194 -
   2.195 -subsubsection {* Definitions of length and digit sum *}
   2.196 -
   2.197 -text {* This section introduces some functions to calculate the
   2.198 -required properties of natural numbers. We then proceed to prove some
   2.199 -properties of these functions.
   2.200 -
   2.201 -The function @{text "nlen"} returns the number of digits in a natural
   2.202 -number n. *}
   2.203 -
   2.204 -consts nlen :: "nat \<Rightarrow> nat"
   2.205 -recdef nlen "measure id"
   2.206 -  "nlen 0 = 0"
   2.207 -  "nlen x = 1 + nlen (x div 10)"
   2.208 -
   2.209 -text {* The function @{text "sumdig"} returns the sum of all digits in
   2.210 -some number n. *}
   2.211 -
   2.212 -constdefs 
   2.213 -  sumdig :: "nat \<Rightarrow> nat"
   2.214 -  "sumdig n \<equiv> \<Sum>x < nlen n. n div 10^x mod 10"
   2.215 -
   2.216 -text {* Some properties of these functions follow. *}
   2.217 -
   2.218 -lemma nlen_zero:
   2.219 -  "0 = nlen x \<Longrightarrow> x = 0"
   2.220 -  by (induct x rule: nlen.induct) auto
   2.221 -
   2.222 -lemma nlen_suc:
   2.223 -  "Suc m = nlen n \<Longrightarrow> m = nlen (n div 10)"
   2.224 -  by (induct n rule: nlen.induct) simp_all
   2.225 -
   2.226 -
   2.227 -text {* The following lemma is the principle lemma required to prove
   2.228 -our theorem. It states that an expansion of some natural number $n$
   2.229 -into a sequence of its individual digits is always possible. *}
   2.230 -
   2.231 -lemma exp_exists:
   2.232 -  "\<And>m. nd = nlen m \<Longrightarrow> m = (\<Sum>x<nd. (m div (10::nat)^x mod 10) * 10^x)"
   2.233 -proof (induct nd)
   2.234 -  case 0 thus ?case by (simp add: nlen_zero)
   2.235 -next
   2.236 -  case (Suc nd)
   2.237 -  hence IH:
   2.238 -    "nd = nlen (m div 10) \<Longrightarrow>
   2.239 -    m div 10 = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x)"
   2.240 -    by blast
   2.241 -  have "\<exists>c. m = 10*(m div 10) + c \<and> c < 10" by presburger
   2.242 -  from this obtain c where mexp: "m = 10*(m div 10) + c \<and> c < 10" ..
   2.243 -  then have cdef: "c = m mod 10" by arith
   2.244 -  show "m = (\<Sum>x<Suc nd. m div 10^x mod 10 * 10^x)"
   2.245 -  proof -
   2.246 -    have "Suc nd = nlen m" .
   2.247 -    then have
   2.248 -      "nd = nlen (m div 10)" by (rule nlen_suc)
   2.249 -    with IH have
   2.250 -      "m div 10 = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x)"  by simp
   2.251 -    with mexp have
   2.252 -      "m = 10*(\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x) + c" by simp
   2.253 -    also have
   2.254 -      "\<dots> = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^(x+1)) + c"
   2.255 -      by (subst setsum_mult) (simp add: mult_ac)
   2.256 -    also have
   2.257 -      "\<dots> = (\<Sum>x<nd. m div 10^(Suc x) mod 10 * 10^(Suc x)) + c"
   2.258 -      by (simp add: div_mult2_eq[symmetric])
   2.259 -    also have
   2.260 -      "\<dots> = (\<Sum>x\<in>{Suc 0..<Suc nd}. m div 10^x  mod 10 * 10^x) + c"
   2.261 -      by (simp only: setsum_shift_bounds_Suc_ivl)
   2.262 -         (simp add: atLeast0LessThan)
   2.263 -    also have
   2.264 -      "\<dots> = (\<Sum>x<Suc nd. m div 10^x mod 10 * 10^x)"
   2.265 -      by (simp add: sum_rmv_head cdef)
   2.266 -    finally 
   2.267 -    show "m = (\<Sum>x<Suc nd. m div 10^x mod 10 * 10^x)" .
   2.268 -  qed
   2.269 -qed
   2.270 -
   2.271 -
   2.272 -subsubsection {* Final theorem *}
   2.273 -
   2.274 -text {* We now combine the general theorem @{text "three_div_general"}
   2.275 -and existence result of @{text "exp_exists"} to prove our final
   2.276 -theorem. *}
   2.277 -
   2.278 -theorem three_divides_nat:
   2.279 -  shows "(3 dvd n) = (3 dvd sumdig n)"
   2.280 -proof (unfold sumdig_def)
   2.281 -  obtain nd where "nd = nlen n" by simp
   2.282 -  moreover
   2.283 -  have "n = (\<Sum>x<nd. (n div (10::nat)^x mod 10) * 10^x)"
   2.284 -    by (rule exp_exists)
   2.285 -  moreover
   2.286 -  have "3 dvd (\<Sum>x<nlen n. (n div (10::nat)^x mod 10) * 10^x) =
   2.287 -        (3 dvd (\<Sum>x<nlen n. n div 10^x mod 10))"
   2.288 -    by (rule three_div_general)
   2.289 -  ultimately 
   2.290 -  show "3 dvd n = (3 dvd (\<Sum>x<nlen n. n div 10^x mod 10))" by simp
   2.291 -qed
   2.292 -
   2.293 -
   2.294 -end
     3.1 --- a/src/HOL/SetInterval.thy	Sun Feb 12 04:31:18 2006 +0100
     3.2 +++ b/src/HOL/SetInterval.thy	Sun Feb 12 10:42:19 2006 +0100
     3.3 @@ -715,6 +715,26 @@
     3.4    "setsum f {Suc m..<Suc n} = setsum (%i. f(Suc i)){m..<n}"
     3.5  by (simp add:setsum_shift_bounds_nat_ivl[where k=1,simplified])
     3.6  
     3.7 +lemma setsum_rmv_head:
     3.8 +  fixes m::nat
     3.9 +  assumes m: "0 < m"
    3.10 +  shows "P 0 + (\<Sum>x\<in>{1..<m}. P x) = (\<Sum>x<m. P x)"
    3.11 +  (is "?lhs = ?rhs")
    3.12 +proof -
    3.13 +  let ?a = "\<Sum>x\<in>({0} \<union> {0<..<m}). P x"
    3.14 +  from m
    3.15 +  have "{0..<m} = {0} \<union> {0<..<m}"
    3.16 +    by (simp only: ivl_disj_un_singleton)
    3.17 +  hence "?rhs = ?a"
    3.18 +    by (simp add: atLeast0LessThan)
    3.19 +  moreover
    3.20 +  have "?a = ?lhs"
    3.21 +    by (simp add: setsum_Un ivl_disj_int 
    3.22 +                  atLeastSucLessThan_greaterThanLessThan)
    3.23 +  ultimately 
    3.24 +  show ?thesis by simp
    3.25 +qed
    3.26 +
    3.27  subsection {* The formula for geometric sums *}
    3.28  
    3.29  lemma geometric_sum:
    3.30 @@ -728,6 +748,33 @@
    3.31  
    3.32  
    3.33  
    3.34 +lemma sum_diff_distrib:
    3.35 +  fixes P::"nat\<Rightarrow>nat"
    3.36 +  shows
    3.37 +  "\<forall>x. Q x \<le> P x  \<Longrightarrow>
    3.38 +  (\<Sum>x<n. P x) - (\<Sum>x<n. Q x) = (\<Sum>x<n. P x - Q x)"
    3.39 +proof (induct n)
    3.40 +  case 0 show ?case by simp
    3.41 +next
    3.42 +  case (Suc n)
    3.43 +
    3.44 +  let ?lhs = "(\<Sum>x<n. P x) - (\<Sum>x<n. Q x)"
    3.45 +  let ?rhs = "\<Sum>x<n. P x - Q x"
    3.46 +
    3.47 +  from Suc have "?lhs = ?rhs" by simp
    3.48 +  moreover
    3.49 +  from Suc have "?lhs + P n - Q n = ?rhs + (P n - Q n)" by simp
    3.50 +  moreover
    3.51 +  from Suc have
    3.52 +    "(\<Sum>x<n. P x) + P n - ((\<Sum>x<n. Q x) + Q n) = ?rhs + (P n - Q n)"
    3.53 +    by (subst diff_diff_left[symmetric],
    3.54 +        subst diff_add_assoc2)
    3.55 +       (auto simp: diff_add_assoc2 intro: setsum_mono)
    3.56 +  ultimately
    3.57 +  show ?case by simp
    3.58 +qed
    3.59 +
    3.60 +
    3.61  ML
    3.62  {*
    3.63  val Compl_atLeast = thm "Compl_atLeast";
     4.1 --- a/src/HOL/ex/ROOT.ML	Sun Feb 12 04:31:18 2006 +0100
     4.2 +++ b/src/HOL/ex/ROOT.ML	Sun Feb 12 10:42:19 2006 +0100
     4.3 @@ -19,6 +19,7 @@
     4.4  time_use_thy "Multiquote";
     4.5  
     4.6  time_use_thy "NatSum";
     4.7 +time_use_thy "ThreeDivides";
     4.8  time_use_thy "Intuitionistic";
     4.9  time_use_thy "Classical";
    4.10  time_use_thy "CTL";
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/ex/ThreeDivides.thy	Sun Feb 12 10:42:19 2006 +0100
     5.3 @@ -0,0 +1,239 @@
     5.4 +(*  Title:      HOL/Isar_examples/ThreeDivides.thy
     5.5 +    ID:         $Id$
     5.6 +    Author:     Benjamin Porter, 2005
     5.7 +*)
     5.8 +
     5.9 +header {* Three Divides Theorem *}
    5.10 +
    5.11 +theory ThreeDivides
    5.12 +imports Main LaTeXsugar
    5.13 +begin
    5.14 +
    5.15 +section {* Abstract *}
    5.16 +
    5.17 +text {*
    5.18 +The following document presents a proof of the Three Divides N theorem
    5.19 +formalised in the Isabelle/Isar theorem proving system.
    5.20 +
    5.21 +{\em Theorem}: 3 divides n if and only if 3 divides the sum of all
    5.22 +digits in n.
    5.23 +
    5.24 +{\em Informal Proof}:
    5.25 +Take $n = \sum{n_j * 10^j}$ where $n_j$ is the $j$'th least
    5.26 +significant digit of the decimal denotation of the number n and the
    5.27 +sum ranges over all digits. Then $$ (n - \sum{n_j}) = \sum{n_j * (10^j
    5.28 +- 1)} $$ We know $\forall j\; 3|(10^j - 1) $ and hence $3|LHS$,
    5.29 +therefore $$\forall n\; 3|n \Longleftrightarrow 3|\sum{n_j}$$
    5.30 +@{text "\<box>"}
    5.31 +*}
    5.32 +
    5.33 +section {* Formal proof *}
    5.34 +
    5.35 +subsection {* Miscellaneous summation lemmas *}
    5.36 +
    5.37 +text {* If $a$ divides @{text "A x"} for all x then $a$ divides any
    5.38 +sum over terms of the form @{text "(A x)*(P x)"} for arbitrary $P$. *}
    5.39 +
    5.40 +lemma div_sum:
    5.41 +  fixes a::nat and n::nat
    5.42 +  shows "\<forall>x. a dvd A x \<Longrightarrow> a dvd (\<Sum>x<n. A x * D x)"
    5.43 +proof (induct n)
    5.44 +  case 0 show ?case by simp
    5.45 +next
    5.46 +  case (Suc n)
    5.47 +  from Suc
    5.48 +  have "a dvd (A n * D n)" by (simp add: dvd_mult2)
    5.49 +  with Suc
    5.50 +  have "a dvd ((\<Sum>x<n. A x * D x) + (A n * D n))" by (simp add: dvd_add)
    5.51 +  thus ?case by simp
    5.52 +qed
    5.53 +
    5.54 +subsection {* Generalised Three Divides *}
    5.55 +
    5.56 +text {* This section solves a generalised form of the three divides
    5.57 +problem. Here we show that for any sequence of numbers the theorem
    5.58 +holds. In the next section we specialise this theorem to apply
    5.59 +directly to the decimal expansion of the natural numbers. *}
    5.60 +
    5.61 +text {* Here we show that the first statement in the informal proof is
    5.62 +true for all natural numbers. Note we are using @{term "D i"} to
    5.63 +denote the $i$'th element in a sequence of numbers. *}
    5.64 +
    5.65 +lemma digit_diff_split:
    5.66 +  fixes n::nat and nd::nat and x::nat
    5.67 +  shows "\<And>n. n = (\<Sum>x\<in>{..<nd}. (D x)*((10::nat)^x)) \<Longrightarrow>
    5.68 +             (n - (\<Sum>x<nd. (D x))) = (\<Sum>x<nd. (D x)*(10^x - 1))"
    5.69 +by (simp add: sum_diff_distrib diff_mult_distrib2)
    5.70 +
    5.71 +text {* Now we prove that 3 always divides numbers of the form $10^x - 1$. *}
    5.72 +lemma three_divs_0 [rule_format, simplified]:
    5.73 +  shows "(3::nat) dvd (10^x - 1)"
    5.74 +proof (induct x)
    5.75 +  case 0 show ?case by simp
    5.76 +next
    5.77 +  case (Suc n)
    5.78 +  let ?thr = "(3::nat)"
    5.79 +  have "?thr dvd 9" by simp
    5.80 +  moreover
    5.81 +  have "?thr dvd (10*(10^n - 1))" by (rule dvd_mult)
    5.82 +  hence "?thr dvd (10^(n+1) - 10)" by (simp add: nat_distrib)
    5.83 +  ultimately
    5.84 +  have"?thr dvd ((10^(n+1) - 10) + 9)"
    5.85 +    by (simp only: add_ac) (rule dvd_add)
    5.86 +  thus ?case by simp
    5.87 +qed
    5.88 +
    5.89 +text {* Expanding on the previous lemma and lemma @{text "div_sum\<dots>"} *}
    5.90 +lemma three_divs_1:
    5.91 +  fixes D :: "nat \<Rightarrow> nat"
    5.92 +  shows "3 dvd (\<Sum>x<nd. D x * (10^x - 1))"
    5.93 +  by (subst nat_mult_commute, rule div_sum) (simp add: three_divs_0)
    5.94 +
    5.95 +text {* Using lemmas @{text "digit_diff_split"} and 
    5.96 +@{text "three_divs_1"} we now prove the following lemma. 
    5.97 +*}
    5.98 +lemma three_divs_2:
    5.99 +  fixes nd::nat and D::"nat\<Rightarrow>nat"
   5.100 +  shows "3 dvd ((\<Sum>x<nd. (D x)*(10^x)) - (\<Sum>x<nd. (D x)))"
   5.101 +proof (simp only: digit_diff_split)
   5.102 +  from three_divs_1 show "3 dvd (\<Sum>x<nd. D x * (10 ^ x - 1))" .
   5.103 +qed
   5.104 +
   5.105 +text {* 
   5.106 +We now present the final theorem of this section. For any
   5.107 +sequence of numbers (defined by a function @{term "D :: (nat\<Rightarrow>nat)"}),
   5.108 +we show that 3 divides the expansive sum $\sum{(D\;x)*10^x}$ over $x$
   5.109 +if and only if 3 divides the sum of the individual numbers
   5.110 +$\sum{D\;x}$. 
   5.111 +*}
   5.112 +lemma three_div_general:
   5.113 +  fixes D :: "nat \<Rightarrow> nat"
   5.114 +  shows "(3 dvd (\<Sum>x<nd. D x * 10^x)) = (3 dvd (\<Sum>x<nd. D x))"
   5.115 +proof
   5.116 +  have mono: "(\<Sum>x<nd. D x) \<le> (\<Sum>x<nd. D x * 10^x)"
   5.117 +    by (rule setsum_mono, simp)
   5.118 +  txt {* This lets us form the term
   5.119 +         @{term "(\<Sum>x<nd. D x * 10^x) - (\<Sum>x<nd. D x)"} *}
   5.120 +
   5.121 +  {
   5.122 +    assume "3 dvd (\<Sum>x<nd. D x)"
   5.123 +    with three_divs_2 mono
   5.124 +    show "3 dvd (\<Sum>x<nd. D x * 10^x)" 
   5.125 +      by (blast intro: dvd_diffD)
   5.126 +  }
   5.127 +  {
   5.128 +    assume "3 dvd (\<Sum>x<nd. D x * 10^x)"
   5.129 +    with three_divs_2 mono
   5.130 +    show "3 dvd (\<Sum>x<nd. D x)"
   5.131 +      by (blast intro: dvd_diffD1)
   5.132 +  }
   5.133 +qed
   5.134 +
   5.135 +
   5.136 +subsection {* Three Divides Natural *}
   5.137 +
   5.138 +text {* This section shows that for all natural numbers we can
   5.139 +generate a sequence of digits less than ten that represent the decimal
   5.140 +expansion of the number. We then use the lemma @{text
   5.141 +"three_div_general"} to prove our final theorem. *}
   5.142 +
   5.143 +subsubsection {* Definitions of length and digit sum *}
   5.144 +
   5.145 +text {* This section introduces some functions to calculate the
   5.146 +required properties of natural numbers. We then proceed to prove some
   5.147 +properties of these functions.
   5.148 +
   5.149 +The function @{text "nlen"} returns the number of digits in a natural
   5.150 +number n. *}
   5.151 +
   5.152 +consts nlen :: "nat \<Rightarrow> nat"
   5.153 +recdef nlen "measure id"
   5.154 +  "nlen 0 = 0"
   5.155 +  "nlen x = 1 + nlen (x div 10)"
   5.156 +
   5.157 +text {* The function @{text "sumdig"} returns the sum of all digits in
   5.158 +some number n. *}
   5.159 +
   5.160 +constdefs 
   5.161 +  sumdig :: "nat \<Rightarrow> nat"
   5.162 +  "sumdig n \<equiv> \<Sum>x < nlen n. n div 10^x mod 10"
   5.163 +
   5.164 +text {* Some properties of these functions follow. *}
   5.165 +
   5.166 +lemma nlen_zero:
   5.167 +  "0 = nlen x \<Longrightarrow> x = 0"
   5.168 +  by (induct x rule: nlen.induct) auto
   5.169 +
   5.170 +lemma nlen_suc:
   5.171 +  "Suc m = nlen n \<Longrightarrow> m = nlen (n div 10)"
   5.172 +  by (induct n rule: nlen.induct) simp_all
   5.173 +
   5.174 +
   5.175 +text {* The following lemma is the principle lemma required to prove
   5.176 +our theorem. It states that an expansion of some natural number $n$
   5.177 +into a sequence of its individual digits is always possible. *}
   5.178 +
   5.179 +lemma exp_exists:
   5.180 +  "\<And>m. nd = nlen m \<Longrightarrow> m = (\<Sum>x<nd. (m div (10::nat)^x mod 10) * 10^x)"
   5.181 +proof (induct nd)
   5.182 +  case 0 thus ?case by (simp add: nlen_zero)
   5.183 +next
   5.184 +  case (Suc nd)
   5.185 +  hence IH:
   5.186 +    "nd = nlen (m div 10) \<Longrightarrow>
   5.187 +    m div 10 = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x)"
   5.188 +    by blast
   5.189 +  have "\<exists>c. m = 10*(m div 10) + c \<and> c < 10" by presburger
   5.190 +  from this obtain c where mexp: "m = 10*(m div 10) + c \<and> c < 10" ..
   5.191 +  then have cdef: "c = m mod 10" by arith
   5.192 +  show "m = (\<Sum>x<Suc nd. m div 10^x mod 10 * 10^x)"
   5.193 +  proof -
   5.194 +    have "Suc nd = nlen m" .
   5.195 +    then have
   5.196 +      "nd = nlen (m div 10)" by (rule nlen_suc)
   5.197 +    with IH have
   5.198 +      "m div 10 = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x)"  by simp
   5.199 +    with mexp have
   5.200 +      "m = 10*(\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x) + c" by simp
   5.201 +    also have
   5.202 +      "\<dots> = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^(x+1)) + c"
   5.203 +      by (subst setsum_mult) (simp add: mult_ac)
   5.204 +    also have
   5.205 +      "\<dots> = (\<Sum>x<nd. m div 10^(Suc x) mod 10 * 10^(Suc x)) + c"
   5.206 +      by (simp add: div_mult2_eq[symmetric])
   5.207 +    also have
   5.208 +      "\<dots> = (\<Sum>x\<in>{Suc 0..<Suc nd}. m div 10^x  mod 10 * 10^x) + c"
   5.209 +      by (simp only: setsum_shift_bounds_Suc_ivl)
   5.210 +         (simp add: atLeast0LessThan)
   5.211 +    also have
   5.212 +      "\<dots> = (\<Sum>x<Suc nd. m div 10^x mod 10 * 10^x)"
   5.213 +      by (simp add: setsum_rmv_head [symmetric] cdef)
   5.214 +    finally 
   5.215 +    show "m = (\<Sum>x<Suc nd. m div 10^x mod 10 * 10^x)" .
   5.216 +  qed
   5.217 +qed
   5.218 +
   5.219 +
   5.220 +subsubsection {* Final theorem *}
   5.221 +
   5.222 +text {* We now combine the general theorem @{text "three_div_general"}
   5.223 +and existence result of @{text "exp_exists"} to prove our final
   5.224 +theorem. *}
   5.225 +
   5.226 +theorem three_divides_nat:
   5.227 +  shows "(3 dvd n) = (3 dvd sumdig n)"
   5.228 +proof (unfold sumdig_def)
   5.229 +  obtain nd where "nd = nlen n" by simp
   5.230 +  moreover
   5.231 +  have "n = (\<Sum>x<nd. (n div (10::nat)^x mod 10) * 10^x)"
   5.232 +    by (rule exp_exists)
   5.233 +  moreover
   5.234 +  have "3 dvd (\<Sum>x<nlen n. (n div (10::nat)^x mod 10) * 10^x) =
   5.235 +        (3 dvd (\<Sum>x<nlen n. n div 10^x mod 10))"
   5.236 +    by (rule three_div_general)
   5.237 +  ultimately 
   5.238 +  show "3 dvd n = (3 dvd (\<Sum>x<nlen n. n div 10^x mod 10))" by simp
   5.239 +qed
   5.240 +
   5.241 +
   5.242 +end