* moved ThreeDivides from Isar_examples to better suited HOL/ex
* moved 2 summation lemmas from ThreeDivides to SetInterval

--- a/src/HOL/Isar_examples/ROOT.ML	Sun Feb 12 04:31:18 2006 +0100
+++ b/src/HOL/Isar_examples/ROOT.ML	Sun Feb 12 10:42:19 2006 +0100
@@ -14,7 +14,6 @@
 time_use_thy "Summation";
 time_use_thy "KnasterTarski";
 time_use_thy "MutilatedCheckerboard";
-time_use_thy "ThreeDivides";
 with_path "../NumberTheory" (no_document time_use_thy) "Primes";
 with_path "../NumberTheory" time_use_thy "Fibonacci";
 time_use_thy "Puzzle";

--- a/src/HOL/Isar_examples/ThreeDivides.thy	Sun Feb 12 04:31:18 2006 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,291 +0,0 @@
-(*  Title:      HOL/Isar_examples/ThreeDivides.thy
-    ID:         $Id$
-    Author:     Benjamin Porter, 2005
-*)
-
-header {* Three Divides Theorem *}
-
-theory ThreeDivides
-imports Main LaTeXsugar
-begin
-
-section {* Abstract *}
-
-text {*
-The following document presents a proof of the Three Divides N theorem
-formalised in the Isabelle/Isar theorem proving system.
-
-{\em Theorem}: 3 divides n if and only if 3 divides the sum of all
-digits in n.
-
-{\em Informal Proof}:
-Take $n = \sum{n_j * 10^j}$ where $n_j$ is the $j$'th least
-significant digit of the decimal denotation of the number n and the
-sum ranges over all digits. Then $$ (n - \sum{n_j}) = \sum{n_j * (10^j
-- 1)} $$ We know $\forall j\; 3|(10^j - 1) $ and hence $3|LHS$,
-therefore $$\forall n\; 3|n \Longleftrightarrow 3|\sum{n_j}$$
-@{text "\<box>"}
-*}
-
-section {* Formal proof *}
-
-subsection {* Miscellaneous summation lemmas *}
-
-text {* We can decompose a sum into an expanded form by removing
-its first element. *}
-
-lemma sum_rmv_head:
-  fixes m::nat
-  assumes m: "0 < m"
-  shows "(\<Sum>x<m. P x) = P 0 + (\<Sum>x\<in>{1..<m}. P x)"
-  (is "?lhs = ?rhs")
-proof -
-  let ?a = "\<Sum>x\<in>({0} \<union> {0<..<m}). P x"
-  from m
-  have "{0..<m} = {0} \<union> {0<..<m}"
-    by (simp only: ivl_disj_un_singleton)
-  hence "?lhs = ?a"
-    by (simp add: atLeast0LessThan)
-  moreover
-  have "?a = ?rhs"
-    by (simp add: setsum_Un ivl_disj_int 
-                  atLeastSucLessThan_greaterThanLessThan)
-  ultimately 
-  show ?thesis by simp
-qed
-
-text {* This lemma states that the difference of two sums ranging over
-the same elements is the sum of their individual differences. *}
-
-lemma sum_distrib [rule_format]:
-  fixes x::nat and P::"nat\<Rightarrow>nat"
-  shows
-  "\<forall>x. Q x \<le> P x  \<Longrightarrow>
-  (\<Sum>x<n. P x) - (\<Sum>x<n. Q x) = (\<Sum>x<n. P x - Q x)"
-proof (induct n)
-  case 0 show ?case by simp
-next
-  case (Suc n)
-
-  let ?lhs = "(\<Sum>x<n. P x) - (\<Sum>x<n. Q x)"
-  let ?rhs = "\<Sum>x<n. P x - Q x"
-
-  from Suc have "?lhs = ?rhs" by simp
-  moreover
-  from Suc have "?lhs + P n - Q n = ?rhs + (P n - Q n)" by simp
-  moreover
-  from Suc have
-    "(\<Sum>x<n. P x) + P n - ((\<Sum>x<n. Q x) + Q n) = ?rhs + (P n - Q n)"
-    by (subst diff_diff_left[symmetric],
-        subst diff_add_assoc2)
-       (auto simp: diff_add_assoc2 intro: setsum_mono)
-  ultimately
-  show ?case by simp
-qed
-
-text {* If $a$ divides @{text "A x"} for all x then $a$ divides any
-sum over terms of the form @{text "(A x)*(P x)"} for arbitrary $P$. *}
-
-lemma div_sum:
-  fixes a::nat and n::nat
-  shows "\<forall>x. a dvd A x \<Longrightarrow> a dvd (\<Sum>x<n. A x * D x)"
-proof (induct n)
-  case 0 show ?case by simp
-next
-  case (Suc n)
-  from Suc
-  have "a dvd (A n * D n)" by (simp add: dvd_mult2)
-  with Suc
-  have "a dvd ((\<Sum>x<n. A x * D x) + (A n * D n))" by (simp add: dvd_add)
-  thus ?case by simp
-qed
-
-subsection {* Generalised Three Divides *}
-
-text {* This section solves a generalised form of the three divides
-problem. Here we show that for any sequence of numbers the theorem
-holds. In the next section we specialise this theorem to apply
-directly to the decimal expansion of the natural numbers. *}
-
-text {* Here we show that the first statement in the informal proof is
-true for all natural numbers. Note we are using @{term "D i"} to
-denote the $i$'th element in a sequence of numbers. *}
-
-lemma digit_diff_split:
-  fixes n::nat and nd::nat and x::nat
-  shows "\<And>n. n = (\<Sum>x\<in>{..<nd}. (D x)*((10::nat)^x)) \<Longrightarrow>
-             (n - (\<Sum>x<nd. (D x))) = (\<Sum>x<nd. (D x)*(10^x - 1))"
-by (simp add: sum_distrib diff_mult_distrib2)
-
-text {* Now we prove that 3 always divides numbers of the form $10^x - 1$. *}
-lemma three_divs_0 [rule_format, simplified]:
-  shows "(3::nat) dvd (10^x - 1)"
-proof (induct x)
-  case 0 show ?case by simp
-next
-  case (Suc n)
-  let ?thr = "(3::nat)"
-  have "?thr dvd 9" by simp
-  moreover
-  have "?thr dvd (10*(10^n - 1))" by (rule dvd_mult)
-  hence "?thr dvd (10^(n+1) - 10)" by (simp add: nat_distrib)
-  ultimately
-  have"?thr dvd ((10^(n+1) - 10) + 9)"
-    by (simp only: add_ac) (rule dvd_add)
-  thus ?case by simp
-qed
-
-text {* Expanding on the previous lemma and lemma @{text "div_sum\<dots>"} *}
-lemma three_divs_1:
-  fixes D :: "nat \<Rightarrow> nat"
-  shows "3 dvd (\<Sum>x<nd. D x * (10^x - 1))"
-  by (subst nat_mult_commute, rule div_sum) (simp add: three_divs_0)
-
-text {* Using lemmas @{text "digit_diff_split"} and 
-@{text "three_divs_1"} we now prove the following lemma. 
-*}
-lemma three_divs_2:
-  fixes nd::nat and D::"nat\<Rightarrow>nat"
-  shows "3 dvd ((\<Sum>x<nd. (D x)*(10^x)) - (\<Sum>x<nd. (D x)))"
-proof (simp only: digit_diff_split)
-  from three_divs_1 show "3 dvd (\<Sum>x<nd. D x * (10 ^ x - 1))" .
-qed
-
-text {* 
-We now present the final theorem of this section. For any
-sequence of numbers (defined by a function @{term "D :: (nat\<Rightarrow>nat)"}),
-we show that 3 divides the expansive sum $\sum{(D\;x)*10^x}$ over $x$
-if and only if 3 divides the sum of the individual numbers
-$\sum{D\;x}$. 
-*}
-lemma three_div_general:
-  fixes D :: "nat \<Rightarrow> nat"
-  shows "(3 dvd (\<Sum>x<nd. D x * 10^x)) = (3 dvd (\<Sum>x<nd. D x))"
-proof
-  have mono: "(\<Sum>x<nd. D x) \<le> (\<Sum>x<nd. D x * 10^x)"
-    by (rule setsum_mono, simp)
-  txt {* This lets us form the term
-         @{term "(\<Sum>x<nd. D x * 10^x) - (\<Sum>x<nd. D x)"} *}
-
-  {
-    assume "3 dvd (\<Sum>x<nd. D x)"
-    with three_divs_2 mono
-    show "3 dvd (\<Sum>x<nd. D x * 10^x)" 
-      by (blast intro: dvd_diffD)
-  }
-  {
-    assume "3 dvd (\<Sum>x<nd. D x * 10^x)"
-    with three_divs_2 mono
-    show "3 dvd (\<Sum>x<nd. D x)"
-      by (blast intro: dvd_diffD1)
-  }
-qed
-
-
-subsection {* Three Divides Natural *}
-
-text {* This section shows that for all natural numbers we can
-generate a sequence of digits less than ten that represent the decimal
-expansion of the number. We then use the lemma @{text
-"three_div_general"} to prove our final theorem. *}
-
-subsubsection {* Definitions of length and digit sum *}
-
-text {* This section introduces some functions to calculate the
-required properties of natural numbers. We then proceed to prove some
-properties of these functions.
-
-The function @{text "nlen"} returns the number of digits in a natural
-number n. *}
-
-consts nlen :: "nat \<Rightarrow> nat"
-recdef nlen "measure id"
-  "nlen 0 = 0"
-  "nlen x = 1 + nlen (x div 10)"
-
-text {* The function @{text "sumdig"} returns the sum of all digits in
-some number n. *}
-
-constdefs 
-  sumdig :: "nat \<Rightarrow> nat"
-  "sumdig n \<equiv> \<Sum>x < nlen n. n div 10^x mod 10"
-
-text {* Some properties of these functions follow. *}
-
-lemma nlen_zero:
-  "0 = nlen x \<Longrightarrow> x = 0"
-  by (induct x rule: nlen.induct) auto
-
-lemma nlen_suc:
-  "Suc m = nlen n \<Longrightarrow> m = nlen (n div 10)"
-  by (induct n rule: nlen.induct) simp_all
-
-
-text {* The following lemma is the principle lemma required to prove
-our theorem. It states that an expansion of some natural number $n$
-into a sequence of its individual digits is always possible. *}
-
-lemma exp_exists:
-  "\<And>m. nd = nlen m \<Longrightarrow> m = (\<Sum>x<nd. (m div (10::nat)^x mod 10) * 10^x)"
-proof (induct nd)
-  case 0 thus ?case by (simp add: nlen_zero)
-next
-  case (Suc nd)
-  hence IH:
-    "nd = nlen (m div 10) \<Longrightarrow>
-    m div 10 = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x)"
-    by blast
-  have "\<exists>c. m = 10*(m div 10) + c \<and> c < 10" by presburger
-  from this obtain c where mexp: "m = 10*(m div 10) + c \<and> c < 10" ..
-  then have cdef: "c = m mod 10" by arith
-  show "m = (\<Sum>x<Suc nd. m div 10^x mod 10 * 10^x)"
-  proof -
-    have "Suc nd = nlen m" .
-    then have
-      "nd = nlen (m div 10)" by (rule nlen_suc)
-    with IH have
-      "m div 10 = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x)"  by simp
-    with mexp have
-      "m = 10*(\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x) + c" by simp
-    also have
-      "\<dots> = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^(x+1)) + c"
-      by (subst setsum_mult) (simp add: mult_ac)
-    also have
-      "\<dots> = (\<Sum>x<nd. m div 10^(Suc x) mod 10 * 10^(Suc x)) + c"
-      by (simp add: div_mult2_eq[symmetric])
-    also have
-      "\<dots> = (\<Sum>x\<in>{Suc 0..<Suc nd}. m div 10^x  mod 10 * 10^x) + c"
-      by (simp only: setsum_shift_bounds_Suc_ivl)
-         (simp add: atLeast0LessThan)
-    also have
-      "\<dots> = (\<Sum>x<Suc nd. m div 10^x mod 10 * 10^x)"
-      by (simp add: sum_rmv_head cdef)
-    finally 
-    show "m = (\<Sum>x<Suc nd. m div 10^x mod 10 * 10^x)" .
-  qed
-qed
-
-
-subsubsection {* Final theorem *}
-
-text {* We now combine the general theorem @{text "three_div_general"}
-and existence result of @{text "exp_exists"} to prove our final
-theorem. *}
-
-theorem three_divides_nat:
-  shows "(3 dvd n) = (3 dvd sumdig n)"
-proof (unfold sumdig_def)
-  obtain nd where "nd = nlen n" by simp
-  moreover
-  have "n = (\<Sum>x<nd. (n div (10::nat)^x mod 10) * 10^x)"
-    by (rule exp_exists)
-  moreover
-  have "3 dvd (\<Sum>x<nlen n. (n div (10::nat)^x mod 10) * 10^x) =
-        (3 dvd (\<Sum>x<nlen n. n div 10^x mod 10))"
-    by (rule three_div_general)
-  ultimately 
-  show "3 dvd n = (3 dvd (\<Sum>x<nlen n. n div 10^x mod 10))" by simp
-qed
-
-
-end

--- a/src/HOL/SetInterval.thy	Sun Feb 12 04:31:18 2006 +0100
+++ b/src/HOL/SetInterval.thy	Sun Feb 12 10:42:19 2006 +0100
@@ -715,6 +715,26 @@
   "setsum f {Suc m..<Suc n} = setsum (%i. f(Suc i)){m..<n}"
 by (simp add:setsum_shift_bounds_nat_ivl[where k=1,simplified])
 
+lemma setsum_rmv_head:
+  fixes m::nat
+  assumes m: "0 < m"
+  shows "P 0 + (\<Sum>x\<in>{1..<m}. P x) = (\<Sum>x<m. P x)"
+  (is "?lhs = ?rhs")
+proof -
+  let ?a = "\<Sum>x\<in>({0} \<union> {0<..<m}). P x"
+  from m
+  have "{0..<m} = {0} \<union> {0<..<m}"
+    by (simp only: ivl_disj_un_singleton)
+  hence "?rhs = ?a"
+    by (simp add: atLeast0LessThan)
+  moreover
+  have "?a = ?lhs"
+    by (simp add: setsum_Un ivl_disj_int 
+                  atLeastSucLessThan_greaterThanLessThan)
+  ultimately 
+  show ?thesis by simp
+qed
+
 subsection {* The formula for geometric sums *}
 
 lemma geometric_sum:
@@ -728,6 +748,33 @@
 
 
 
+lemma sum_diff_distrib:
+  fixes P::"nat\<Rightarrow>nat"
+  shows
+  "\<forall>x. Q x \<le> P x  \<Longrightarrow>
+  (\<Sum>x<n. P x) - (\<Sum>x<n. Q x) = (\<Sum>x<n. P x - Q x)"
+proof (induct n)
+  case 0 show ?case by simp
+next
+  case (Suc n)
+
+  let ?lhs = "(\<Sum>x<n. P x) - (\<Sum>x<n. Q x)"
+  let ?rhs = "\<Sum>x<n. P x - Q x"
+
+  from Suc have "?lhs = ?rhs" by simp
+  moreover
+  from Suc have "?lhs + P n - Q n = ?rhs + (P n - Q n)" by simp
+  moreover
+  from Suc have
+    "(\<Sum>x<n. P x) + P n - ((\<Sum>x<n. Q x) + Q n) = ?rhs + (P n - Q n)"
+    by (subst diff_diff_left[symmetric],
+        subst diff_add_assoc2)
+       (auto simp: diff_add_assoc2 intro: setsum_mono)
+  ultimately
+  show ?case by simp
+qed
+
+
 ML
 {*
 val Compl_atLeast = thm "Compl_atLeast";

--- a/src/HOL/ex/ROOT.ML	Sun Feb 12 04:31:18 2006 +0100
+++ b/src/HOL/ex/ROOT.ML	Sun Feb 12 10:42:19 2006 +0100
@@ -19,6 +19,7 @@
 time_use_thy "Multiquote";
 
 time_use_thy "NatSum";
+time_use_thy "ThreeDivides";
 time_use_thy "Intuitionistic";
 time_use_thy "Classical";
 time_use_thy "CTL";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/ThreeDivides.thy	Sun Feb 12 10:42:19 2006 +0100
@@ -0,0 +1,239 @@
+(*  Title:      HOL/Isar_examples/ThreeDivides.thy
+    ID:         $Id$
+    Author:     Benjamin Porter, 2005
+*)
+
+header {* Three Divides Theorem *}
+
+theory ThreeDivides
+imports Main LaTeXsugar
+begin
+
+section {* Abstract *}
+
+text {*
+The following document presents a proof of the Three Divides N theorem
+formalised in the Isabelle/Isar theorem proving system.
+
+{\em Theorem}: 3 divides n if and only if 3 divides the sum of all
+digits in n.
+
+{\em Informal Proof}:
+Take $n = \sum{n_j * 10^j}$ where $n_j$ is the $j$'th least
+significant digit of the decimal denotation of the number n and the
+sum ranges over all digits. Then $$ (n - \sum{n_j}) = \sum{n_j * (10^j
+- 1)} $$ We know $\forall j\; 3|(10^j - 1) $ and hence $3|LHS$,
+therefore $$\forall n\; 3|n \Longleftrightarrow 3|\sum{n_j}$$
+@{text "\<box>"}
+*}
+
+section {* Formal proof *}
+
+subsection {* Miscellaneous summation lemmas *}
+
+text {* If $a$ divides @{text "A x"} for all x then $a$ divides any
+sum over terms of the form @{text "(A x)*(P x)"} for arbitrary $P$. *}
+
+lemma div_sum:
+  fixes a::nat and n::nat
+  shows "\<forall>x. a dvd A x \<Longrightarrow> a dvd (\<Sum>x<n. A x * D x)"
+proof (induct n)
+  case 0 show ?case by simp
+next
+  case (Suc n)
+  from Suc
+  have "a dvd (A n * D n)" by (simp add: dvd_mult2)
+  with Suc
+  have "a dvd ((\<Sum>x<n. A x * D x) + (A n * D n))" by (simp add: dvd_add)
+  thus ?case by simp
+qed
+
+subsection {* Generalised Three Divides *}
+
+text {* This section solves a generalised form of the three divides
+problem. Here we show that for any sequence of numbers the theorem
+holds. In the next section we specialise this theorem to apply
+directly to the decimal expansion of the natural numbers. *}
+
+text {* Here we show that the first statement in the informal proof is
+true for all natural numbers. Note we are using @{term "D i"} to
+denote the $i$'th element in a sequence of numbers. *}
+
+lemma digit_diff_split:
+  fixes n::nat and nd::nat and x::nat
+  shows "\<And>n. n = (\<Sum>x\<in>{..<nd}. (D x)*((10::nat)^x)) \<Longrightarrow>
+             (n - (\<Sum>x<nd. (D x))) = (\<Sum>x<nd. (D x)*(10^x - 1))"
+by (simp add: sum_diff_distrib diff_mult_distrib2)
+
+text {* Now we prove that 3 always divides numbers of the form $10^x - 1$. *}
+lemma three_divs_0 [rule_format, simplified]:
+  shows "(3::nat) dvd (10^x - 1)"
+proof (induct x)
+  case 0 show ?case by simp
+next
+  case (Suc n)
+  let ?thr = "(3::nat)"
+  have "?thr dvd 9" by simp
+  moreover
+  have "?thr dvd (10*(10^n - 1))" by (rule dvd_mult)
+  hence "?thr dvd (10^(n+1) - 10)" by (simp add: nat_distrib)
+  ultimately
+  have"?thr dvd ((10^(n+1) - 10) + 9)"
+    by (simp only: add_ac) (rule dvd_add)
+  thus ?case by simp
+qed
+
+text {* Expanding on the previous lemma and lemma @{text "div_sum\<dots>"} *}
+lemma three_divs_1:
+  fixes D :: "nat \<Rightarrow> nat"
+  shows "3 dvd (\<Sum>x<nd. D x * (10^x - 1))"
+  by (subst nat_mult_commute, rule div_sum) (simp add: three_divs_0)
+
+text {* Using lemmas @{text "digit_diff_split"} and 
+@{text "three_divs_1"} we now prove the following lemma. 
+*}
+lemma three_divs_2:
+  fixes nd::nat and D::"nat\<Rightarrow>nat"
+  shows "3 dvd ((\<Sum>x<nd. (D x)*(10^x)) - (\<Sum>x<nd. (D x)))"
+proof (simp only: digit_diff_split)
+  from three_divs_1 show "3 dvd (\<Sum>x<nd. D x * (10 ^ x - 1))" .
+qed
+
+text {* 
+We now present the final theorem of this section. For any
+sequence of numbers (defined by a function @{term "D :: (nat\<Rightarrow>nat)"}),
+we show that 3 divides the expansive sum $\sum{(D\;x)*10^x}$ over $x$
+if and only if 3 divides the sum of the individual numbers
+$\sum{D\;x}$. 
+*}
+lemma three_div_general:
+  fixes D :: "nat \<Rightarrow> nat"
+  shows "(3 dvd (\<Sum>x<nd. D x * 10^x)) = (3 dvd (\<Sum>x<nd. D x))"
+proof
+  have mono: "(\<Sum>x<nd. D x) \<le> (\<Sum>x<nd. D x * 10^x)"
+    by (rule setsum_mono, simp)
+  txt {* This lets us form the term
+         @{term "(\<Sum>x<nd. D x * 10^x) - (\<Sum>x<nd. D x)"} *}
+
+  {
+    assume "3 dvd (\<Sum>x<nd. D x)"
+    with three_divs_2 mono
+    show "3 dvd (\<Sum>x<nd. D x * 10^x)" 
+      by (blast intro: dvd_diffD)
+  }
+  {
+    assume "3 dvd (\<Sum>x<nd. D x * 10^x)"
+    with three_divs_2 mono
+    show "3 dvd (\<Sum>x<nd. D x)"
+      by (blast intro: dvd_diffD1)
+  }
+qed
+
+
+subsection {* Three Divides Natural *}
+
+text {* This section shows that for all natural numbers we can
+generate a sequence of digits less than ten that represent the decimal
+expansion of the number. We then use the lemma @{text
+"three_div_general"} to prove our final theorem. *}
+
+subsubsection {* Definitions of length and digit sum *}
+
+text {* This section introduces some functions to calculate the
+required properties of natural numbers. We then proceed to prove some
+properties of these functions.
+
+The function @{text "nlen"} returns the number of digits in a natural
+number n. *}
+
+consts nlen :: "nat \<Rightarrow> nat"
+recdef nlen "measure id"
+  "nlen 0 = 0"
+  "nlen x = 1 + nlen (x div 10)"
+
+text {* The function @{text "sumdig"} returns the sum of all digits in
+some number n. *}
+
+constdefs 
+  sumdig :: "nat \<Rightarrow> nat"
+  "sumdig n \<equiv> \<Sum>x < nlen n. n div 10^x mod 10"
+
+text {* Some properties of these functions follow. *}
+
+lemma nlen_zero:
+  "0 = nlen x \<Longrightarrow> x = 0"
+  by (induct x rule: nlen.induct) auto
+
+lemma nlen_suc:
+  "Suc m = nlen n \<Longrightarrow> m = nlen (n div 10)"
+  by (induct n rule: nlen.induct) simp_all
+
+
+text {* The following lemma is the principle lemma required to prove
+our theorem. It states that an expansion of some natural number $n$
+into a sequence of its individual digits is always possible. *}
+
+lemma exp_exists:
+  "\<And>m. nd = nlen m \<Longrightarrow> m = (\<Sum>x<nd. (m div (10::nat)^x mod 10) * 10^x)"
+proof (induct nd)
+  case 0 thus ?case by (simp add: nlen_zero)
+next
+  case (Suc nd)
+  hence IH:
+    "nd = nlen (m div 10) \<Longrightarrow>
+    m div 10 = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x)"
+    by blast
+  have "\<exists>c. m = 10*(m div 10) + c \<and> c < 10" by presburger
+  from this obtain c where mexp: "m = 10*(m div 10) + c \<and> c < 10" ..
+  then have cdef: "c = m mod 10" by arith
+  show "m = (\<Sum>x<Suc nd. m div 10^x mod 10 * 10^x)"
+  proof -
+    have "Suc nd = nlen m" .
+    then have
+      "nd = nlen (m div 10)" by (rule nlen_suc)
+    with IH have
+      "m div 10 = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x)"  by simp
+    with mexp have
+      "m = 10*(\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x) + c" by simp
+    also have
+      "\<dots> = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^(x+1)) + c"
+      by (subst setsum_mult) (simp add: mult_ac)
+    also have
+      "\<dots> = (\<Sum>x<nd. m div 10^(Suc x) mod 10 * 10^(Suc x)) + c"
+      by (simp add: div_mult2_eq[symmetric])
+    also have
+      "\<dots> = (\<Sum>x\<in>{Suc 0..<Suc nd}. m div 10^x  mod 10 * 10^x) + c"
+      by (simp only: setsum_shift_bounds_Suc_ivl)
+         (simp add: atLeast0LessThan)
+    also have
+      "\<dots> = (\<Sum>x<Suc nd. m div 10^x mod 10 * 10^x)"
+      by (simp add: setsum_rmv_head [symmetric] cdef)
+    finally 
+    show "m = (\<Sum>x<Suc nd. m div 10^x mod 10 * 10^x)" .
+  qed
+qed
+
+
+subsubsection {* Final theorem *}
+
+text {* We now combine the general theorem @{text "three_div_general"}
+and existence result of @{text "exp_exists"} to prove our final
+theorem. *}
+
+theorem three_divides_nat:
+  shows "(3 dvd n) = (3 dvd sumdig n)"
+proof (unfold sumdig_def)
+  obtain nd where "nd = nlen n" by simp
+  moreover
+  have "n = (\<Sum>x<nd. (n div (10::nat)^x mod 10) * 10^x)"
+    by (rule exp_exists)
+  moreover
+  have "3 dvd (\<Sum>x<nlen n. (n div (10::nat)^x mod 10) * 10^x) =
+        (3 dvd (\<Sum>x<nlen n. n div 10^x mod 10))"
+    by (rule three_div_general)
+  ultimately 
+  show "3 dvd n = (3 dvd (\<Sum>x<nlen n. n div 10^x mod 10))" by simp
+qed
+
+
+end