|
1 (* Title: Infinite Sequences |
|
2 Author: Christian Sternagel <c-sterna@jaist.ac.jp> |
|
3 René Thiemann <rene.thiemann@uibk.ac.at> |
|
4 Maintainer: Christian Sternagel and René Thiemann |
|
5 License: LGPL |
|
6 *) |
|
7 |
|
8 (* |
|
9 Copyright 2012 Christian Sternagel, René Thiemann |
|
10 |
|
11 This file is part of IsaFoR/CeTA. |
|
12 |
|
13 IsaFoR/CeTA is free software: you can redistribute it and/or modify it under the |
|
14 terms of the GNU Lesser General Public License as published by the Free Software |
|
15 Foundation, either version 3 of the License, or (at your option) any later |
|
16 version. |
|
17 |
|
18 IsaFoR/CeTA is distributed in the hope that it will be useful, but WITHOUT ANY |
|
19 WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A |
|
20 PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details. |
|
21 |
|
22 You should have received a copy of the GNU Lesser General Public License along |
|
23 with IsaFoR/CeTA. If not, see <http://www.gnu.org/licenses/>. |
|
24 *) |
|
25 header {* Infinite Sequences *} |
|
26 theory Seq |
|
27 imports |
|
28 Main |
|
29 "~~/src/HOL/Library/Infinite_Set" |
|
30 begin |
|
31 |
|
32 text {*Infinite sequences are represented by functions of type @{typ "nat \<Rightarrow> 'a"}.*} |
|
33 type_synonym 'a seq = "nat \<Rightarrow> 'a" |
|
34 |
|
35 subsection {*Operations on Infinite Sequences*} |
|
36 |
|
37 text {*Adding a new element at the front.*} |
|
38 abbreviation cons :: "'a \<Rightarrow> 'a seq \<Rightarrow> 'a seq" (infixr "#s" 65) where (*FIXME: find better infix symbol*) |
|
39 "x #s S \<equiv> (\<lambda>i. case i of 0 \<Rightarrow> x | Suc n \<Rightarrow> S n)" |
|
40 |
|
41 text {*An infinite sequence is \emph{linked} by a binary predicate @{term P} if every two |
|
42 consecutive elements satisfy it. Such a sequence is called a \emph{@{term P}-chain}. *} |
|
43 abbreviation (input) chainp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow>'a seq \<Rightarrow> bool" where |
|
44 "chainp P S \<equiv> \<forall>i. P (S i) (S (Suc i))" |
|
45 |
|
46 text {*Special version for relations.*} |
|
47 abbreviation (input) chain :: "'a rel \<Rightarrow> 'a seq \<Rightarrow> bool" where |
|
48 "chain r S \<equiv> chainp (\<lambda>x y. (x, y) \<in> r) S" |
|
49 |
|
50 text {*Extending a chain at the front.*} |
|
51 lemma cons_chainp: |
|
52 assumes "P x (S 0)" and "chainp P S" |
|
53 shows "chainp P (x #s S)" (is "chainp P ?S") |
|
54 proof |
|
55 fix i show "P (?S i) (?S (Suc i))" using assms by (cases i) simp_all |
|
56 qed |
|
57 |
|
58 text {*Special version for relations.*} |
|
59 lemma cons_chain: |
|
60 assumes "(x, S 0) \<in> r" and "chain r S" shows "chain r (x #s S)" |
|
61 using cons_chainp[of "\<lambda>x y. (x, y) \<in> r", OF assms] . |
|
62 |
|
63 text {*A chain admits arbitrary transitive steps.*} |
|
64 lemma chainp_imp_relpowp: |
|
65 assumes "chainp P S" shows "(P^^j) (S i) (S (i + j))" |
|
66 proof (induct "i + j" arbitrary: j) |
|
67 case (Suc n) thus ?case using assms by (cases j) auto |
|
68 qed simp |
|
69 |
|
70 lemma chain_imp_relpow: |
|
71 assumes "chain r S" shows "(S i, S (i + j)) \<in> r^^j" |
|
72 proof (induct "i + j" arbitrary: j) |
|
73 case (Suc n) thus ?case using assms by (cases j) auto |
|
74 qed simp |
|
75 |
|
76 lemma chainp_imp_tranclp: |
|
77 assumes "chainp P S" and "i < j" shows "P^++ (S i) (S j)" |
|
78 proof - |
|
79 from less_imp_Suc_add[OF assms(2)] obtain n where "j = i + Suc n" by auto |
|
80 with chainp_imp_relpowp[of P S "Suc n" i, OF assms(1)] |
|
81 show ?thesis |
|
82 unfolding trancl_power[of "(S i, S j)", to_pred] |
|
83 by force |
|
84 qed |
|
85 |
|
86 lemma chain_imp_trancl: |
|
87 assumes "chain r S" and "i < j" shows "(S i, S j) \<in> r^+" |
|
88 proof - |
|
89 from less_imp_Suc_add[OF assms(2)] obtain n where "j = i + Suc n" by auto |
|
90 with chain_imp_relpow[OF assms(1), of i "Suc n"] |
|
91 show ?thesis unfolding trancl_power by force |
|
92 qed |
|
93 |
|
94 text {*A chain admits arbitrary reflexive and transitive steps.*} |
|
95 lemma chainp_imp_rtranclp: |
|
96 assumes "chainp P S" and "i \<le> j" shows "P^** (S i) (S j)" |
|
97 proof - |
|
98 from assms(2) obtain n where "j = i + n" by (induct "j - i" arbitrary: j) force+ |
|
99 with chainp_imp_relpowp[of P S, OF assms(1), of n i] show ?thesis |
|
100 by (simp add: relpow_imp_rtrancl[of "(S i, S (i + n))", to_pred]) |
|
101 qed |
|
102 |
|
103 lemma chain_imp_rtrancl: |
|
104 assumes "chain r S" and "i \<le> j" shows "(S i, S j) \<in> r^*" |
|
105 proof - |
|
106 from assms(2) obtain n where "j = i + n" by (induct "j - i" arbitrary: j) force+ |
|
107 with chain_imp_relpow[OF assms(1), of i n] show ?thesis by (simp add: relpow_imp_rtrancl) |
|
108 qed |
|
109 |
|
110 text {*If for every @{term i} there is a later index @{term "f i"} such that the |
|
111 corresponding elements satisfy the predicate @{term P}, then there is a @{term P}-chain.*} |
|
112 lemma stepfun_imp_chainp: |
|
113 assumes "\<forall>i\<ge>n::nat. f i > i \<and> P (S i) (S (f i))" |
|
114 shows "chainp P (\<lambda>i. S ((f ^^ i) n))" (is "chainp P ?T") |
|
115 proof |
|
116 fix i |
|
117 from assms have "(f ^^ i) n \<ge> n" by (induct i) auto |
|
118 with assms[THEN spec[of _ "(f ^^ i) n"]] |
|
119 show "P (?T i) (?T (Suc i))" by simp |
|
120 qed |
|
121 |
|
122 text {*If for every @{term i} there is a later index @{term j} such that the |
|
123 corresponding elements satisfy the predicate @{term P}, then there is a @{term P}-chain.*} |
|
124 lemma steps_imp_chainp: |
|
125 assumes "\<forall>i\<ge>n::nat. \<exists>j>i. P (S i) (S j)" shows "\<exists>T. chainp P T" |
|
126 proof - |
|
127 from assms have "\<forall>i\<in>{i. i \<ge> n}. \<exists>j>i. P (S i) (S j)" by auto |
|
128 from bchoice[OF this] |
|
129 obtain f where seq: "\<forall>i\<ge>n. f i > i \<and> P (S i) (S (f i))" by auto |
|
130 from stepfun_imp_chainp[of n f P S, OF this] show ?thesis by fast |
|
131 qed |
|
132 |
|
133 |
|
134 subsection {* Predicates on Natural Numbers *} |
|
135 |
|
136 text {*If some property holds for infinitely many natural numbers, obtain |
|
137 an index function that points to these numbers in increasing order.*} |
|
138 |
|
139 locale infinitely_many = |
|
140 fixes p :: "nat \<Rightarrow> bool" |
|
141 assumes infinite: "INFM j. p j" |
|
142 begin |
|
143 |
|
144 lemma inf: "\<exists>j\<ge>i. p j" using infinite[unfolded INFM_nat_le] by auto |
|
145 |
|
146 fun index :: "nat seq" where |
|
147 "index 0 = (LEAST n. p n)" |
|
148 | "index (Suc n) = (LEAST k. p k \<and> k > index n)" |
|
149 |
|
150 lemma index_p: "p (index n)" |
|
151 proof (induct n) |
|
152 case 0 |
|
153 from inf obtain j where "p j" by auto |
|
154 with LeastI[of p j] show ?case by auto |
|
155 next |
|
156 case (Suc n) |
|
157 from inf obtain k where "k \<ge> Suc (index n) \<and> p k" by auto |
|
158 with LeastI[of "\<lambda> k. p k \<and> k > index n" k] show ?case by auto |
|
159 qed |
|
160 |
|
161 lemma index_ordered: "index n < index (Suc n)" |
|
162 proof - |
|
163 from inf obtain k where "k \<ge> Suc (index n) \<and> p k" by auto |
|
164 with LeastI[of "\<lambda> k. p k \<and> k > index n" k] show ?thesis by auto |
|
165 qed |
|
166 |
|
167 lemma index_not_p_between: |
|
168 assumes i1: "index n < i" |
|
169 and i2: "i < index (Suc n)" |
|
170 shows "\<not> p i" |
|
171 proof - |
|
172 from not_less_Least[OF i2[simplified]] i1 show ?thesis by auto |
|
173 qed |
|
174 |
|
175 lemma index_ordered_le: |
|
176 assumes "i \<le> j" shows "index i \<le> index j" |
|
177 proof - |
|
178 from assms have "j = i + (j - i)" by auto |
|
179 then obtain k where j: "j = i + k" by auto |
|
180 have "index i \<le> index (i + k)" |
|
181 proof (induct k) |
|
182 case (Suc k) |
|
183 with index_ordered[of "i + k"] |
|
184 show ?case by auto |
|
185 qed simp |
|
186 thus ?thesis unfolding j . |
|
187 qed |
|
188 |
|
189 lemma index_surj: |
|
190 assumes "k \<ge> index l" |
|
191 shows "\<exists>i j. k = index i + j \<and> index i + j < index (Suc i)" |
|
192 proof - |
|
193 from assms have "k = index l + (k - index l)" by auto |
|
194 then obtain u where k: "k = index l + u" by auto |
|
195 show ?thesis unfolding k |
|
196 proof (induct u) |
|
197 case 0 |
|
198 show ?case |
|
199 by (intro exI conjI, rule refl, insert index_ordered[of l], simp) |
|
200 next |
|
201 case (Suc u) |
|
202 then obtain i j |
|
203 where lu: "index l + u = index i + j" and lt: "index i + j < index (Suc i)" by auto |
|
204 hence "index l + u < index (Suc i)" by auto |
|
205 show ?case |
|
206 proof (cases "index l + (Suc u) = index (Suc i)") |
|
207 case False |
|
208 show ?thesis |
|
209 by (rule exI[of _ i], rule exI[of _ "Suc j"], insert lu lt False, auto) |
|
210 next |
|
211 case True |
|
212 show ?thesis |
|
213 by (rule exI[of _ "Suc i"], rule exI[of _ 0], insert True index_ordered[of "Suc i"], auto) |
|
214 qed |
|
215 qed |
|
216 qed |
|
217 |
|
218 lemma index_ordered_less: |
|
219 assumes "i < j" shows "index i < index j" |
|
220 proof - |
|
221 from assms have "Suc i \<le> j" by auto |
|
222 from index_ordered_le[OF this] |
|
223 have "index (Suc i) \<le> index j" . |
|
224 with index_ordered[of i] show ?thesis by auto |
|
225 qed |
|
226 |
|
227 lemma index_not_p_start: assumes i: "i < index 0" shows "\<not> p i" |
|
228 proof - |
|
229 from i[simplified index.simps] have "i < Least p" . |
|
230 from not_less_Least[OF this] show ?thesis . |
|
231 qed |
|
232 |
|
233 end |
|
234 |
|
235 |
|
236 subsection {* Assembling Infinite Words from Finite Words *} |
|
237 |
|
238 text {*Concatenate infinitely many non-empty words to an infinite word.*} |
|
239 |
|
240 fun inf_concat_simple :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> (nat \<times> nat)" where |
|
241 "inf_concat_simple f 0 = (0, 0)" |
|
242 | "inf_concat_simple f (Suc n) = ( |
|
243 let (i, j) = inf_concat_simple f n in |
|
244 if Suc j < f i then (i, Suc j) |
|
245 else (Suc i, 0))" |
|
246 |
|
247 lemma inf_concat_simple_add: |
|
248 assumes ck: "inf_concat_simple f k = (i, j)" |
|
249 and jl: "j + l < f i" |
|
250 shows "inf_concat_simple f (k + l) = (i,j + l)" |
|
251 using jl |
|
252 proof (induct l) |
|
253 case 0 |
|
254 thus ?case using ck by simp |
|
255 next |
|
256 case (Suc l) |
|
257 hence c: "inf_concat_simple f (k + l) = (i, j+ l)" by auto |
|
258 show ?case |
|
259 by (simp add: c, insert Suc(2), auto) |
|
260 qed |
|
261 |
|
262 lemma inf_concat_simple_surj_zero: "\<exists> k. inf_concat_simple f k = (i,0)" |
|
263 proof (induct i) |
|
264 case 0 |
|
265 show ?case |
|
266 by (rule exI[of _ 0], simp) |
|
267 next |
|
268 case (Suc i) |
|
269 then obtain k where ck: "inf_concat_simple f k = (i,0)" by auto |
|
270 show ?case |
|
271 proof (cases "f i") |
|
272 case 0 |
|
273 show ?thesis |
|
274 by (rule exI[of _ "Suc k"], simp add: ck 0) |
|
275 next |
|
276 case (Suc n) |
|
277 hence "0 + n < f i" by auto |
|
278 from inf_concat_simple_add[OF ck, OF this] Suc |
|
279 show ?thesis |
|
280 by (intro exI[of _ "k + Suc n"], auto) |
|
281 qed |
|
282 qed |
|
283 |
|
284 lemma inf_concat_simple_surj: |
|
285 assumes "j < f i" |
|
286 shows "\<exists> k. inf_concat_simple f k = (i,j)" |
|
287 proof - |
|
288 from assms have j: "0 + j < f i" by auto |
|
289 from inf_concat_simple_surj_zero obtain k where "inf_concat_simple f k = (i,0)" by auto |
|
290 from inf_concat_simple_add[OF this, OF j] show ?thesis by auto |
|
291 qed |
|
292 |
|
293 lemma inf_concat_simple_mono: |
|
294 assumes "k \<le> k'" shows "fst (inf_concat_simple f k) \<le> fst (inf_concat_simple f k')" |
|
295 proof - |
|
296 from assms have "k' = k + (k' - k)" by auto |
|
297 then obtain l where k': "k' = k + l" by auto |
|
298 show ?thesis unfolding k' |
|
299 proof (induct l) |
|
300 case (Suc l) |
|
301 obtain i j where ckl: "inf_concat_simple f (k+l) = (i,j)" by (cases "inf_concat_simple f (k+l)", auto) |
|
302 with Suc have "fst (inf_concat_simple f k) \<le> i" by auto |
|
303 also have "... \<le> fst (inf_concat_simple f (k + Suc l))" |
|
304 by (simp add: ckl) |
|
305 finally show ?case . |
|
306 qed simp |
|
307 qed |
|
308 |
|
309 |
|
310 (* inf_concat assembles infinitely many (possibly empty) words to an infinite word *) |
|
311 fun inf_concat :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where |
|
312 "inf_concat n 0 = (LEAST j. n j > 0, 0)" |
|
313 | "inf_concat n (Suc k) = (let (i, j) = inf_concat n k in (if Suc j < n i then (i, Suc j) else (LEAST i'. i' > i \<and> n i' > 0, 0)))" |
|
314 |
|
315 lemma inf_concat_bounds: |
|
316 assumes inf: "INFM i. n i > 0" |
|
317 and res: "inf_concat n k = (i,j)" |
|
318 shows "j < n i" |
|
319 proof (cases k) |
|
320 case 0 |
|
321 with res have i: "i = (LEAST i. n i > 0)" and j: "j = 0" by auto |
|
322 from inf[unfolded INFM_nat_le] obtain i' where i': "0 < n i'" by auto |
|
323 have "0 < n (LEAST i. n i > 0)" |
|
324 by (rule LeastI, rule i') |
|
325 with i j show ?thesis by auto |
|
326 next |
|
327 case (Suc k') |
|
328 obtain i' j' where res': "inf_concat n k' = (i',j')" by force |
|
329 note res = res[unfolded Suc inf_concat.simps res' Let_def split] |
|
330 show ?thesis |
|
331 proof (cases "Suc j' < n i'") |
|
332 case True |
|
333 with res show ?thesis by auto |
|
334 next |
|
335 case False |
|
336 with res have i: "i = (LEAST f. i' < f \<and> 0 < n f)" and j: "j = 0" by auto |
|
337 from inf[unfolded INFM_nat] obtain f where f: "i' < f \<and> 0 < n f" by auto |
|
338 have "0 < n (LEAST f. i' < f \<and> 0 < n f)" |
|
339 using LeastI[of "\<lambda> f. i' < f \<and> 0 < n f", OF f] |
|
340 by auto |
|
341 with i j show ?thesis by auto |
|
342 qed |
|
343 qed |
|
344 |
|
345 lemma inf_concat_add: |
|
346 assumes res: "inf_concat n k = (i,j)" |
|
347 and j: "j + m < n i" |
|
348 shows "inf_concat n (k + m) = (i,j+m)" |
|
349 using j |
|
350 proof (induct m) |
|
351 case 0 show ?case using res by auto |
|
352 next |
|
353 case (Suc m) |
|
354 hence "inf_concat n (k + m) = (i, j+m)" by auto |
|
355 with Suc(2) |
|
356 show ?case by auto |
|
357 qed |
|
358 |
|
359 lemma inf_concat_step: |
|
360 assumes res: "inf_concat n k = (i,j)" |
|
361 and j: "Suc (j + m) = n i" |
|
362 shows "inf_concat n (k + Suc m) = (LEAST i'. i' > i \<and> 0 < n i', 0)" |
|
363 proof - |
|
364 from j have "j + m < n i" by auto |
|
365 note res = inf_concat_add[OF res, OF this] |
|
366 show ?thesis by (simp add: res j) |
|
367 qed |
|
368 |
|
369 lemma inf_concat_surj_zero: |
|
370 assumes "0 < n i" |
|
371 shows "\<exists>k. inf_concat n k = (i, 0)" |
|
372 proof - |
|
373 { |
|
374 fix l |
|
375 have "\<forall> j. j < l \<and> 0 < n j \<longrightarrow> (\<exists> k. inf_concat n k = (j,0))" |
|
376 proof (induct l) |
|
377 case 0 |
|
378 thus ?case by auto |
|
379 next |
|
380 case (Suc l) |
|
381 show ?case |
|
382 proof (intro allI impI, elim conjE) |
|
383 fix j |
|
384 assume j: "j < Suc l" and nj: "0 < n j" |
|
385 show "\<exists> k. inf_concat n k = (j, 0)" |
|
386 proof (cases "j < l") |
|
387 case True |
|
388 from Suc[THEN spec[of _ j]] True nj show ?thesis by auto |
|
389 next |
|
390 case False |
|
391 with j have j: "j = l" by auto |
|
392 show ?thesis |
|
393 proof (cases "\<exists> j'. j' < l \<and> 0 < n j'") |
|
394 case False |
|
395 have l: "(LEAST i. 0 < n i) = l" |
|
396 proof (rule Least_equality, rule nj[unfolded j]) |
|
397 fix l' |
|
398 assume "0 < n l'" |
|
399 with False have "\<not> l' < l" by auto |
|
400 thus "l \<le> l'" by auto |
|
401 qed |
|
402 show ?thesis |
|
403 by (rule exI[of _ 0], simp add: l j) |
|
404 next |
|
405 case True |
|
406 then obtain lll where lll: "lll < l" and nlll: "0 < n lll" by auto |
|
407 then obtain ll where l: "l = Suc ll" by (cases l, auto) |
|
408 from lll l have lll: "lll = ll - (ll - lll)" by auto |
|
409 let ?l' = "LEAST d. 0 < n (ll - d)" |
|
410 have nl': "0 < n (ll - ?l')" |
|
411 proof (rule LeastI) |
|
412 show "0 < n (ll - (ll - lll))" using lll nlll by auto |
|
413 qed |
|
414 with Suc[THEN spec[of _ "ll - ?l'"]] obtain k where k: |
|
415 "inf_concat n k = (ll - ?l',0)" unfolding l by auto |
|
416 from nl' obtain off where off: "Suc (0 + off) = n (ll - ?l')" by (cases "n (ll - ?l')", auto) |
|
417 from inf_concat_step[OF k, OF off] |
|
418 have id: "inf_concat n (k + Suc off) = (LEAST i'. ll - ?l' < i' \<and> 0 < n i',0)" (is "_ = (?l,0)") . |
|
419 have ll: "?l = l" unfolding l |
|
420 proof (rule Least_equality) |
|
421 show "ll - ?l' < Suc ll \<and> 0 < n (Suc ll)" using nj[unfolded j l] by simp |
|
422 next |
|
423 fix l' |
|
424 assume ass: "ll - ?l' < l' \<and> 0 < n l'" |
|
425 show "Suc ll \<le> l'" |
|
426 proof (rule ccontr) |
|
427 assume not: "\<not> ?thesis" |
|
428 hence "l' \<le> ll" by auto |
|
429 hence "ll = l' + (ll - l')" by auto |
|
430 then obtain k where ll: "ll = l' + k" by auto |
|
431 from ass have "l' + k - ?l' < l'" unfolding ll by auto |
|
432 hence kl': "k < ?l'" by auto |
|
433 have "0 < n (ll - k)" using ass unfolding ll by simp |
|
434 from Least_le[of "\<lambda> k. 0 < n (ll - k)", OF this] kl' |
|
435 show False by auto |
|
436 qed |
|
437 qed |
|
438 show ?thesis unfolding j |
|
439 by (rule exI[of _ "k + Suc off"], unfold id ll, simp) |
|
440 qed |
|
441 qed |
|
442 qed |
|
443 qed |
|
444 } |
|
445 with assms show ?thesis by auto |
|
446 qed |
|
447 |
|
448 lemma inf_concat_surj: |
|
449 assumes j: "j < n i" |
|
450 shows "\<exists>k. inf_concat n k = (i, j)" |
|
451 proof - |
|
452 from j have "0 < n i" by auto |
|
453 from inf_concat_surj_zero[of n, OF this] |
|
454 obtain k where "inf_concat n k = (i,0)" by auto |
|
455 from inf_concat_add[OF this, of j] j |
|
456 show ?thesis by auto |
|
457 qed |
|
458 |
|
459 lemma inf_concat_mono: |
|
460 assumes inf: "INFM i. n i > 0" |
|
461 and resk: "inf_concat n k = (i, j)" |
|
462 and reskp: "inf_concat n k' = (i', j')" |
|
463 and lt: "i < i'" |
|
464 shows "k < k'" |
|
465 proof - |
|
466 note bounds = inf_concat_bounds[OF inf] |
|
467 { |
|
468 assume "k' \<le> k" |
|
469 hence "k = k' + (k - k')" by auto |
|
470 then obtain l where k: "k = k' + l" by auto |
|
471 have "i' \<le> fst (inf_concat n (k' + l))" |
|
472 proof (induct l) |
|
473 case 0 |
|
474 with reskp show ?case by auto |
|
475 next |
|
476 case (Suc l) |
|
477 obtain i'' j'' where l: "inf_concat n (k' + l) = (i'',j'')" by force |
|
478 with Suc have one: "i' \<le> i''" by auto |
|
479 from bounds[OF l] have j'': "j'' < n i''" by auto |
|
480 show ?case |
|
481 proof (cases "Suc j'' < n i''") |
|
482 case True |
|
483 show ?thesis by (simp add: l True one) |
|
484 next |
|
485 case False |
|
486 let ?i = "LEAST i'. i'' < i' \<and> 0 < n i'" |
|
487 from inf[unfolded INFM_nat] obtain k where "i'' < k \<and> 0 < n k" by auto |
|
488 from LeastI[of "\<lambda> k. i'' < k \<and> 0 < n k", OF this] |
|
489 have "i'' < ?i" by auto |
|
490 with one show ?thesis by (simp add: l False) |
|
491 qed |
|
492 qed |
|
493 with resk k lt have False by auto |
|
494 } |
|
495 thus ?thesis by arith |
|
496 qed |
|
497 |
|
498 lemma inf_concat_Suc: |
|
499 assumes inf: "INFM i. n i > 0" |
|
500 and f: "\<And> i. f i (n i) = f (Suc i) 0" |
|
501 and resk: "inf_concat n k = (i, j)" |
|
502 and ressk: "inf_concat n (Suc k) = (i', j')" |
|
503 shows "f i' j' = f i (Suc j)" |
|
504 proof - |
|
505 note bounds = inf_concat_bounds[OF inf] |
|
506 from bounds[OF resk] have j: "j < n i" . |
|
507 show ?thesis |
|
508 proof (cases "Suc j < n i") |
|
509 case True |
|
510 with ressk resk |
|
511 show ?thesis by simp |
|
512 next |
|
513 case False |
|
514 let ?p = "\<lambda> i'. i < i' \<and> 0 < n i'" |
|
515 let ?i' = "LEAST i'. ?p i'" |
|
516 from False j have id: "Suc (j + 0) = n i" by auto |
|
517 from inf_concat_step[OF resk, OF id] ressk |
|
518 have i': "i' = ?i'" and j': "j' = 0" by auto |
|
519 from id have j: "Suc j = n i" by simp |
|
520 from inf[unfolded INFM_nat] obtain k where "?p k" by auto |
|
521 from LeastI[of ?p, OF this] have "?p ?i'" . |
|
522 hence "?i' = Suc i + (?i' - Suc i)" by simp |
|
523 then obtain d where ii': "?i' = Suc i + d" by auto |
|
524 from not_less_Least[of _ ?p, unfolded ii'] have d': "\<And> d'. d' < d \<Longrightarrow> n (Suc i + d') = 0" by auto |
|
525 have "f (Suc i) 0 = f ?i' 0" unfolding ii' using d' |
|
526 proof (induct d) |
|
527 case 0 |
|
528 show ?case by simp |
|
529 next |
|
530 case (Suc d) |
|
531 hence "f (Suc i) 0 = f (Suc i + d) 0" by auto |
|
532 also have "... = f (Suc (Suc i + d)) 0" |
|
533 unfolding f[symmetric] |
|
534 using Suc(2)[of d] by simp |
|
535 finally show ?case by simp |
|
536 qed |
|
537 thus ?thesis unfolding i' j' j f by simp |
|
538 qed |
|
539 qed |
|
540 |
|
541 end |