176 our theorem. It states that an expansion of some natural number $n$ |
176 our theorem. It states that an expansion of some natural number $n$ |
177 into a sequence of its individual digits is always possible. *} |
177 into a sequence of its individual digits is always possible. *} |
178 |
178 |
179 lemma exp_exists: |
179 lemma exp_exists: |
180 "m = (\<Sum>x<nlen m. (m div (10::nat)^x mod 10) * 10^x)" |
180 "m = (\<Sum>x<nlen m. (m div (10::nat)^x mod 10) * 10^x)" |
181 proof (induct nd \<equiv> "nlen m" arbitrary: m) |
181 proof (induct "nlen m" arbitrary: m) |
182 case 0 thus ?case by (simp add: nlen_zero) |
182 case 0 thus ?case by (simp add: nlen_zero) |
183 next |
183 next |
184 case (Suc nd) |
184 case (Suc nd) |
185 hence IH: |
|
186 "nd = nlen (m div 10) \<Longrightarrow> |
|
187 m div 10 = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x)" |
|
188 by blast |
|
189 obtain c where mexp: "m = 10*(m div 10) + c \<and> c < 10" |
185 obtain c where mexp: "m = 10*(m div 10) + c \<and> c < 10" |
190 and cdef: "c = m mod 10" by simp |
186 and cdef: "c = m mod 10" by simp |
191 show "m = (\<Sum>x<nlen m. m div 10^x mod 10 * 10^x)" |
187 show "m = (\<Sum>x<nlen m. m div 10^x mod 10 * 10^x)" |
192 proof - |
188 proof - |
193 from `Suc nd = nlen m` |
189 from `Suc nd = nlen m` |
194 have "nd = nlen (m div 10)" by (rule nlen_suc) |
190 have "nd = nlen (m div 10)" by (rule nlen_suc) |
195 with IH have |
191 with Suc have |
196 "m div 10 = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x)" by simp |
192 "m div 10 = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x)" by simp |
197 with mexp have |
193 with mexp have |
198 "m = 10*(\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x) + c" by simp |
194 "m = 10*(\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x) + c" by simp |
199 also have |
195 also have |
200 "\<dots> = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^(x+1)) + c" |
196 "\<dots> = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^(x+1)) + c" |