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




