author | nipkow |
Fri, 21 Jun 2013 09:00:26 +0200 | |
changeset 52402 | c2f30ba4bb98 |
parent 41413 | 64cd30d6b0b8 |
child 57512 | cc97b347b301 |
permissions | -rw-r--r-- |
33025 | 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 | 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 | 17 |
{\em Theorem}: $3$ divides $n$ if and only if $3$ divides the sum of all |
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 | 30 |
subsection {* Formal proof *} |
31 |
||
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 | 51 |
|
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 | 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 | 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 | 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 | 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 | 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 | 99 |
proof - |
100 |
from three_divs_1 have "3 dvd (\<Sum>x<nd. D x * (10 ^ x - 1))" . |
|
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 | 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 | 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 | 142 |
|
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 | 152 |
fun nlen :: "nat \<Rightarrow> nat" |
153 |
where |
|
19022
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
diff
changeset
|
154 |
"nlen 0 = 0" |
35419 | 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 | 160 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20503
diff
changeset
|
161 |
sumdig :: "nat \<Rightarrow> nat" where |
19736 | 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 | 180 |
"m = (\<Sum>x<nlen m. (m div (10::nat)^x mod 10) * 10^x)" |
34915 | 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 | 185 |
obtain c where mexp: "m = 10*(m div 10) + c \<and> c < 10" |
186 |
and cdef: "c = m mod 10" by simp |
|
19026 | 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 | 189 |
from `Suc nd = nlen m` |
190 |
have "nd = nlen (m div 10)" by (rule nlen_suc) |
|
34915 | 191 |
with Suc have |
19026 | 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 | 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 | 207 |
by (simp add: atLeast0LessThan[symmetric] setsum_head_upt_Suc cdef) |
19026 | 208 |
also note `Suc nd = nlen m` |
209 |
finally |
|
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 | 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 | 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 |