equal
deleted
inserted
replaced
174 our theorem. It states that an expansion of some natural number $n$ |
174 our theorem. It states that an expansion of some natural number $n$ |
175 into a sequence of its individual digits is always possible. *} |
175 into a sequence of its individual digits is always possible. *} |
176 |
176 |
177 lemma exp_exists: |
177 lemma exp_exists: |
178 "m = (\<Sum>x<nlen m. (m div (10::nat)^x mod 10) * 10^x)" |
178 "m = (\<Sum>x<nlen m. (m div (10::nat)^x mod 10) * 10^x)" |
179 proof (induct nd \<equiv> "nlen m" fixing: m) |
179 proof (induct nd \<equiv> "nlen m" arbitrary: m) |
180 case 0 thus ?case by (simp add: nlen_zero) |
180 case 0 thus ?case by (simp add: nlen_zero) |
181 next |
181 next |
182 case (Suc nd) |
182 case (Suc nd) |
183 hence IH: |
183 hence IH: |
184 "nd = nlen (m div 10) \<Longrightarrow> |
184 "nd = nlen (m div 10) \<Longrightarrow> |