src/HOL/ex/ThreeDivides.thy

 
 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 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

 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>
+  shows "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]:
+lemma three_divs_0:
   shows "(3::nat) dvd (10^x - 1)"
 proof (induct x)
   case 0 show ?case by simp
 next
   case (Suc n)

   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>"} *}
+text {* Expanding on the previous lemma and lemma @{text "div_sum"}. *}
 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)
+  by (subst nat_mult_commute, rule div_sum) (simp add: three_divs_0 [simplified])
 
 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))" .
+proof -
+  from three_divs_1 have "3 dvd (\<Sum>x<nd. D x * (10 ^ x - 1))" .
+  thus ?thesis by (simp only: digit_diff_split)
 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)"}),

 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)
+    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)"

 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)
+  "m = (\<Sum>x<nlen m. (m div (10::nat)^x mod 10) * 10^x)"
+proof (induct nd \<equiv> "nlen m" fixing: m)
   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 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)"
+  show "m = (\<Sum>x<nlen m. 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)
+    from `Suc nd = nlen m`
+    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
+      "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)

       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)" .
+    also note `Suc nd = nlen m`
+    finally
+    show "m = (\<Sum>x<nlen m. m div 10^x mod 10 * 10^x)" .
   qed
 qed
 
 
 subsubsection {* Final theorem *}

 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)"
+  have "n = (\<Sum>x<nlen n. (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)