|
1 (* Title: HOL/Library/SCT_Theorem.thy |
|
2 ID: $Id$ |
|
3 Author: Alexander Krauss, TU Muenchen |
|
4 *) |
|
5 |
|
6 header "Proof of the Size-Change Principle" |
|
7 |
|
8 theory Correctness |
|
9 imports Main Ramsey Misc_Tools Criterion |
|
10 begin |
|
11 |
|
12 subsection {* Auxiliary definitions *} |
|
13 |
|
14 definition is_thread :: "nat \<Rightarrow> 'a sequence \<Rightarrow> ('a, 'a scg) ipath \<Rightarrow> bool" |
|
15 where |
|
16 "is_thread n \<theta> p = (\<forall>i\<ge>n. eqlat p \<theta> i)" |
|
17 |
|
18 definition is_fthread :: |
|
19 "'a sequence \<Rightarrow> ('a, 'a scg) ipath \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" |
|
20 where |
|
21 "is_fthread \<theta> mp i j = (\<forall>k\<in>{i..<j}. eqlat mp \<theta> k)" |
|
22 |
|
23 definition is_desc_fthread :: |
|
24 "'a sequence \<Rightarrow> ('a, 'a scg) ipath \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" |
|
25 where |
|
26 "is_desc_fthread \<theta> mp i j = |
|
27 (is_fthread \<theta> mp i j \<and> |
|
28 (\<exists>k\<in>{i..<j}. descat mp \<theta> k))" |
|
29 |
|
30 definition |
|
31 "has_fth p i j n m = |
|
32 (\<exists>\<theta>. is_fthread \<theta> p i j \<and> \<theta> i = n \<and> \<theta> j = m)" |
|
33 |
|
34 definition |
|
35 "has_desc_fth p i j n m = |
|
36 (\<exists>\<theta>. is_desc_fthread \<theta> p i j \<and> \<theta> i = n \<and> \<theta> j = m)" |
|
37 |
|
38 |
|
39 subsection {* Everything is finite *} |
|
40 |
|
41 lemma finite_range: |
|
42 fixes f :: "nat \<Rightarrow> 'a" |
|
43 assumes fin: "finite (range f)" |
|
44 shows "\<exists>x. \<exists>\<^sub>\<infinity>i. f i = x" |
|
45 proof (rule classical) |
|
46 assume "\<not>(\<exists>x. \<exists>\<^sub>\<infinity>i. f i = x)" |
|
47 hence "\<forall>x. \<exists>j. \<forall>i>j. f i \<noteq> x" |
|
48 unfolding INF_nat by blast |
|
49 with choice |
|
50 have "\<exists>j. \<forall>x. \<forall>i>(j x). f i \<noteq> x" . |
|
51 then obtain j where |
|
52 neq: "\<And>x i. j x < i \<Longrightarrow> f i \<noteq> x" by blast |
|
53 |
|
54 from fin have "finite (range (j o f))" |
|
55 by (auto simp:comp_def) |
|
56 with finite_nat_bounded |
|
57 obtain m where "range (j o f) \<subseteq> {..<m}" by blast |
|
58 hence "j (f m) < m" unfolding comp_def by auto |
|
59 |
|
60 with neq[of "f m" m] show ?thesis by blast |
|
61 qed |
|
62 |
|
63 lemma finite_range_ignore_prefix: |
|
64 fixes f :: "nat \<Rightarrow> 'a" |
|
65 assumes fA: "finite A" |
|
66 assumes inA: "\<forall>x\<ge>n. f x \<in> A" |
|
67 shows "finite (range f)" |
|
68 proof - |
|
69 have a: "UNIV = {0 ..< (n::nat)} \<union> { x. n \<le> x }" by auto |
|
70 have b: "range f = f ` {0 ..< n} \<union> f ` { x. n \<le> x }" |
|
71 (is "\<dots> = ?A \<union> ?B") |
|
72 by (unfold a) (simp add:image_Un) |
|
73 |
|
74 have "finite ?A" by (rule finite_imageI) simp |
|
75 moreover |
|
76 from inA have "?B \<subseteq> A" by auto |
|
77 from this fA have "finite ?B" by (rule finite_subset) |
|
78 ultimately show ?thesis using b by simp |
|
79 qed |
|
80 |
|
81 |
|
82 |
|
83 |
|
84 definition |
|
85 "finite_graph G = finite (dest_graph G)" |
|
86 definition |
|
87 "all_finite G = (\<forall>n H m. has_edge G n H m \<longrightarrow> finite_graph H)" |
|
88 definition |
|
89 "finite_acg A = (finite_graph A \<and> all_finite A)" |
|
90 definition |
|
91 "nodes G = fst ` dest_graph G \<union> snd ` snd ` dest_graph G" |
|
92 definition |
|
93 "edges G = fst ` snd ` dest_graph G" |
|
94 definition |
|
95 "smallnodes G = \<Union>(nodes ` edges G)" |
|
96 |
|
97 lemma thread_image_nodes: |
|
98 assumes th: "is_thread n \<theta> p" |
|
99 shows "\<forall>i\<ge>n. \<theta> i \<in> nodes (snd (p i))" |
|
100 using prems |
|
101 unfolding is_thread_def has_edge_def nodes_def |
|
102 by force |
|
103 |
|
104 lemma finite_nodes: "finite_graph G \<Longrightarrow> finite (nodes G)" |
|
105 unfolding finite_graph_def nodes_def |
|
106 by auto |
|
107 |
|
108 lemma nodes_subgraph: "A \<le> B \<Longrightarrow> nodes A \<subseteq> nodes B" |
|
109 unfolding graph_leq_def nodes_def |
|
110 by auto |
|
111 |
|
112 lemma finite_edges: "finite_graph G \<Longrightarrow> finite (edges G)" |
|
113 unfolding finite_graph_def edges_def |
|
114 by auto |
|
115 |
|
116 lemma edges_sum[simp]: "edges (A + B) = edges A \<union> edges B" |
|
117 unfolding edges_def graph_plus_def |
|
118 by auto |
|
119 |
|
120 lemma nodes_sum[simp]: "nodes (A + B) = nodes A \<union> nodes B" |
|
121 unfolding nodes_def graph_plus_def |
|
122 by auto |
|
123 |
|
124 lemma finite_acg_subset: |
|
125 "A \<le> B \<Longrightarrow> finite_acg B \<Longrightarrow> finite_acg A" |
|
126 unfolding finite_acg_def finite_graph_def all_finite_def |
|
127 has_edge_def graph_leq_def |
|
128 by (auto elim:finite_subset) |
|
129 |
|
130 lemma scg_finite: |
|
131 fixes G :: "'a scg" |
|
132 assumes fin: "finite (nodes G)" |
|
133 shows "finite_graph G" |
|
134 unfolding finite_graph_def |
|
135 proof (rule finite_subset) |
|
136 show "dest_graph G \<subseteq> nodes G \<times> UNIV \<times> nodes G" (is "_ \<subseteq> ?P") |
|
137 unfolding nodes_def |
|
138 by force |
|
139 show "finite ?P" |
|
140 by (intro finite_cartesian_product fin finite) |
|
141 qed |
|
142 |
|
143 lemma smallnodes_sum[simp]: |
|
144 "smallnodes (A + B) = smallnodes A \<union> smallnodes B" |
|
145 unfolding smallnodes_def |
|
146 by auto |
|
147 |
|
148 lemma in_smallnodes: |
|
149 fixes A :: "'a acg" |
|
150 assumes e: "has_edge A x G y" |
|
151 shows "nodes G \<subseteq> smallnodes A" |
|
152 proof - |
|
153 have "fst (snd (x, G, y)) \<in> fst ` snd ` dest_graph A" |
|
154 unfolding has_edge_def |
|
155 by (rule imageI)+ (rule e[unfolded has_edge_def]) |
|
156 then have "G \<in> edges A" |
|
157 unfolding edges_def by simp |
|
158 thus ?thesis |
|
159 unfolding smallnodes_def |
|
160 by blast |
|
161 qed |
|
162 |
|
163 lemma finite_smallnodes: |
|
164 assumes fA: "finite_acg A" |
|
165 shows "finite (smallnodes A)" |
|
166 unfolding smallnodes_def edges_def |
|
167 proof |
|
168 from fA |
|
169 show "finite (nodes ` fst ` snd ` dest_graph A)" |
|
170 unfolding finite_acg_def finite_graph_def |
|
171 by simp |
|
172 |
|
173 fix M assume "M \<in> nodes ` fst ` snd ` dest_graph A" |
|
174 then obtain n G m |
|
175 where M: "M = nodes G" and nGm: "(n,G,m) \<in> dest_graph A" |
|
176 by auto |
|
177 |
|
178 from fA |
|
179 have "all_finite A" unfolding finite_acg_def by simp |
|
180 with nGm have "finite_graph G" |
|
181 unfolding all_finite_def has_edge_def by auto |
|
182 with finite_nodes |
|
183 show "finite M" |
|
184 unfolding finite_graph_def M . |
|
185 qed |
|
186 |
|
187 lemma nodes_tcl: |
|
188 "nodes (tcl A) = nodes A" |
|
189 proof |
|
190 show "nodes A \<subseteq> nodes (tcl A)" |
|
191 apply (rule nodes_subgraph) |
|
192 by (subst tcl_unfold_right) simp |
|
193 |
|
194 show "nodes (tcl A) \<subseteq> nodes A" |
|
195 proof |
|
196 fix x assume "x \<in> nodes (tcl A)" |
|
197 then obtain z G y |
|
198 where z: "z \<in> dest_graph (tcl A)" |
|
199 and dis: "z = (x, G, y) \<or> z = (y, G, x)" |
|
200 unfolding nodes_def |
|
201 by auto force+ |
|
202 |
|
203 from dis |
|
204 show "x \<in> nodes A" |
|
205 proof |
|
206 assume "z = (x, G, y)" |
|
207 with z have "has_edge (tcl A) x G y" unfolding has_edge_def by simp |
|
208 then obtain n where "n > 0 " and An: "has_edge (A ^ n) x G y" |
|
209 unfolding in_tcl by auto |
|
210 then obtain n' where "n = Suc n'" by (cases n, auto) |
|
211 hence "A ^ n = A * A ^ n'" by (simp add:power_Suc) |
|
212 with An obtain e k |
|
213 where "has_edge A x e k" by (auto simp:in_grcomp) |
|
214 thus "x \<in> nodes A" unfolding has_edge_def nodes_def |
|
215 by force |
|
216 next |
|
217 assume "z = (y, G, x)" |
|
218 with z have "has_edge (tcl A) y G x" unfolding has_edge_def by simp |
|
219 then obtain n where "n > 0 " and An: "has_edge (A ^ n) y G x" |
|
220 unfolding in_tcl by auto |
|
221 then obtain n' where "n = Suc n'" by (cases n, auto) |
|
222 hence "A ^ n = A ^ n' * A" by (simp add:power_Suc power_commutes) |
|
223 with An obtain e k |
|
224 where "has_edge A k e x" by (auto simp:in_grcomp) |
|
225 thus "x \<in> nodes A" unfolding has_edge_def nodes_def |
|
226 by force |
|
227 qed |
|
228 qed |
|
229 qed |
|
230 |
|
231 lemma smallnodes_tcl: |
|
232 fixes A :: "'a acg" |
|
233 shows "smallnodes (tcl A) = smallnodes A" |
|
234 proof (intro equalityI subsetI) |
|
235 fix n assume "n \<in> smallnodes (tcl A)" |
|
236 then obtain x G y where edge: "has_edge (tcl A) x G y" |
|
237 and "n \<in> nodes G" |
|
238 unfolding smallnodes_def edges_def has_edge_def |
|
239 by auto |
|
240 |
|
241 from `n \<in> nodes G` |
|
242 have "n \<in> fst ` dest_graph G \<or> n \<in> snd ` snd ` dest_graph G" |
|
243 (is "?A \<or> ?B") |
|
244 unfolding nodes_def by blast |
|
245 thus "n \<in> smallnodes A" |
|
246 proof |
|
247 assume ?A |
|
248 then obtain m e where A: "has_edge G n e m" |
|
249 unfolding has_edge_def by auto |
|
250 |
|
251 have "tcl A = A * star A" |
|
252 unfolding tcl_def |
|
253 by (simp add: star_commute[of A A A, simplified]) |
|
254 |
|
255 with edge |
|
256 have "has_edge (A * star A) x G y" by simp |
|
257 then obtain H H' z |
|
258 where AH: "has_edge A x H z" and G: "G = H * H'" |
|
259 by (auto simp:in_grcomp) |
|
260 from A |
|
261 obtain m' e' where "has_edge H n e' m'" |
|
262 by (auto simp:G in_grcomp) |
|
263 hence "n \<in> nodes H" unfolding nodes_def has_edge_def |
|
264 by force |
|
265 with in_smallnodes[OF AH] show "n \<in> smallnodes A" .. |
|
266 next |
|
267 assume ?B |
|
268 then obtain m e where B: "has_edge G m e n" |
|
269 unfolding has_edge_def by auto |
|
270 |
|
271 with edge |
|
272 have "has_edge (star A * A) x G y" by (simp add:tcl_def) |
|
273 then obtain H H' z |
|
274 where AH': "has_edge A z H' y" and G: "G = H * H'" |
|
275 by (auto simp:in_grcomp) |
|
276 from B |
|
277 obtain m' e' where "has_edge H' m' e' n" |
|
278 by (auto simp:G in_grcomp) |
|
279 hence "n \<in> nodes H'" unfolding nodes_def has_edge_def |
|
280 by force |
|
281 with in_smallnodes[OF AH'] show "n \<in> smallnodes A" .. |
|
282 qed |
|
283 next |
|
284 fix x assume "x \<in> smallnodes A" |
|
285 then show "x \<in> smallnodes (tcl A)" |
|
286 by (subst tcl_unfold_right) simp |
|
287 qed |
|
288 |
|
289 lemma finite_nodegraphs: |
|
290 assumes F: "finite F" |
|
291 shows "finite { G::'a scg. nodes G \<subseteq> F }" (is "finite ?P") |
|
292 proof (rule finite_subset) |
|
293 show "?P \<subseteq> Graph ` (Pow (F \<times> UNIV \<times> F))" (is "?P \<subseteq> ?Q") |
|
294 proof |
|
295 fix x assume xP: "x \<in> ?P" |
|
296 obtain S where x[simp]: "x = Graph S" |
|
297 by (cases x) auto |
|
298 from xP |
|
299 show "x \<in> ?Q" |
|
300 apply (simp add:nodes_def) |
|
301 apply (rule imageI) |
|
302 apply (rule PowI) |
|
303 apply force |
|
304 done |
|
305 qed |
|
306 show "finite ?Q" |
|
307 by (auto intro:finite_imageI finite_cartesian_product F finite) |
|
308 qed |
|
309 |
|
310 lemma finite_graphI: |
|
311 fixes A :: "'a acg" |
|
312 assumes fin: "finite (nodes A)" "finite (smallnodes A)" |
|
313 shows "finite_graph A" |
|
314 proof - |
|
315 obtain S where A[simp]: "A = Graph S" |
|
316 by (cases A) auto |
|
317 |
|
318 have "finite S" |
|
319 proof (rule finite_subset) |
|
320 show "S \<subseteq> nodes A \<times> { G::'a scg. nodes G \<subseteq> smallnodes A } \<times> nodes A" |
|
321 (is "S \<subseteq> ?T") |
|
322 proof |
|
323 fix x assume xS: "x \<in> S" |
|
324 obtain a b c where x[simp]: "x = (a, b, c)" |
|
325 by (cases x) auto |
|
326 |
|
327 then have edg: "has_edge A a b c" |
|
328 unfolding has_edge_def using xS |
|
329 by simp |
|
330 |
|
331 hence "a \<in> nodes A" "c \<in> nodes A" |
|
332 unfolding nodes_def has_edge_def by force+ |
|
333 moreover |
|
334 from edg have "nodes b \<subseteq> smallnodes A" by (rule in_smallnodes) |
|
335 hence "b \<in> { G :: 'a scg. nodes G \<subseteq> smallnodes A }" by simp |
|
336 ultimately show "x \<in> ?T" by simp |
|
337 qed |
|
338 |
|
339 show "finite ?T" |
|
340 by (intro finite_cartesian_product fin finite_nodegraphs) |
|
341 qed |
|
342 thus ?thesis |
|
343 unfolding finite_graph_def by simp |
|
344 qed |
|
345 |
|
346 |
|
347 lemma smallnodes_allfinite: |
|
348 fixes A :: "'a acg" |
|
349 assumes fin: "finite (smallnodes A)" |
|
350 shows "all_finite A" |
|
351 unfolding all_finite_def |
|
352 proof (intro allI impI) |
|
353 fix n H m assume "has_edge A n H m" |
|
354 then have "nodes H \<subseteq> smallnodes A" |
|
355 by (rule in_smallnodes) |
|
356 then have "finite (nodes H)" |
|
357 by (rule finite_subset) (rule fin) |
|
358 thus "finite_graph H" by (rule scg_finite) |
|
359 qed |
|
360 |
|
361 lemma finite_tcl: |
|
362 fixes A :: "'a acg" |
|
363 shows "finite_acg (tcl A) \<longleftrightarrow> finite_acg A" |
|
364 proof |
|
365 assume f: "finite_acg A" |
|
366 from f have g: "finite_graph A" and "all_finite A" |
|
367 unfolding finite_acg_def by auto |
|
368 |
|
369 from g have "finite (nodes A)" by (rule finite_nodes) |
|
370 then have "finite (nodes (tcl A))" unfolding nodes_tcl . |
|
371 moreover |
|
372 from f have "finite (smallnodes A)" by (rule finite_smallnodes) |
|
373 then have fs: "finite (smallnodes (tcl A))" unfolding smallnodes_tcl . |
|
374 ultimately |
|
375 have "finite_graph (tcl A)" by (rule finite_graphI) |
|
376 |
|
377 moreover from fs have "all_finite (tcl A)" |
|
378 by (rule smallnodes_allfinite) |
|
379 ultimately show "finite_acg (tcl A)" unfolding finite_acg_def .. |
|
380 next |
|
381 assume a: "finite_acg (tcl A)" |
|
382 have "A \<le> tcl A" by (rule less_tcl) |
|
383 thus "finite_acg A" using a |
|
384 by (rule finite_acg_subset) |
|
385 qed |
|
386 |
|
387 lemma finite_acg_empty: "finite_acg (Graph {})" |
|
388 unfolding finite_acg_def finite_graph_def all_finite_def |
|
389 has_edge_def |
|
390 by simp |
|
391 |
|
392 lemma finite_acg_ins: |
|
393 assumes fA: "finite_acg (Graph A)" |
|
394 assumes fG: "finite G" |
|
395 shows "finite_acg (Graph (insert (a, Graph G, b) A))" |
|
396 using fA fG |
|
397 unfolding finite_acg_def finite_graph_def all_finite_def |
|
398 has_edge_def |
|
399 by auto |
|
400 |
|
401 lemmas finite_acg_simps = finite_acg_empty finite_acg_ins finite_graph_def |
|
402 |
|
403 subsection {* Contraction and more *} |
|
404 |
|
405 abbreviation |
|
406 "pdesc P == (fst P, prod P, end_node P)" |
|
407 |
|
408 lemma pdesc_acgplus: |
|
409 assumes "has_ipath \<A> p" |
|
410 and "i < j" |
|
411 shows "has_edge (tcl \<A>) (fst (p\<langle>i,j\<rangle>)) (prod (p\<langle>i,j\<rangle>)) (end_node (p\<langle>i,j\<rangle>))" |
|
412 unfolding plus_paths |
|
413 apply (rule exI) |
|
414 apply (insert prems) |
|
415 by (auto intro:sub_path_is_path[of "\<A>" p i j] simp:sub_path_def) |
|
416 |
|
417 |
|
418 lemma combine_fthreads: |
|
419 assumes range: "i < j" "j \<le> k" |
|
420 shows |
|
421 "has_fth p i k m r = |
|
422 (\<exists>n. has_fth p i j m n \<and> has_fth p j k n r)" (is "?L = ?R") |
|
423 proof (intro iffI) |
|
424 assume "?L" |
|
425 then obtain \<theta> |
|
426 where "is_fthread \<theta> p i k" |
|
427 and [simp]: "\<theta> i = m" "\<theta> k = r" |
|
428 by (auto simp:has_fth_def) |
|
429 |
|
430 with range |
|
431 have "is_fthread \<theta> p i j" and "is_fthread \<theta> p j k" |
|
432 by (auto simp:is_fthread_def) |
|
433 hence "has_fth p i j m (\<theta> j)" and "has_fth p j k (\<theta> j) r" |
|
434 by (auto simp:has_fth_def) |
|
435 thus "?R" by auto |
|
436 next |
|
437 assume "?R" |
|
438 then obtain n \<theta>1 \<theta>2 |
|
439 where ths: "is_fthread \<theta>1 p i j" "is_fthread \<theta>2 p j k" |
|
440 and [simp]: "\<theta>1 i = m" "\<theta>1 j = n" "\<theta>2 j = n" "\<theta>2 k = r" |
|
441 by (auto simp:has_fth_def) |
|
442 |
|
443 let ?\<theta> = "(\<lambda>i. if i < j then \<theta>1 i else \<theta>2 i)" |
|
444 have "is_fthread ?\<theta> p i k" |
|
445 unfolding is_fthread_def |
|
446 proof |
|
447 fix l assume range: "l \<in> {i..<k}" |
|
448 |
|
449 show "eqlat p ?\<theta> l" |
|
450 proof (cases rule:three_cases) |
|
451 assume "Suc l < j" |
|
452 with ths range show ?thesis |
|
453 unfolding is_fthread_def Ball_def |
|
454 by simp |
|
455 next |
|
456 assume "Suc l = j" |
|
457 hence "l < j" "\<theta>2 (Suc l) = \<theta>1 (Suc l)" by auto |
|
458 with ths range show ?thesis |
|
459 unfolding is_fthread_def Ball_def |
|
460 by simp |
|
461 next |
|
462 assume "j \<le> l" |
|
463 with ths range show ?thesis |
|
464 unfolding is_fthread_def Ball_def |
|
465 by simp |
|
466 qed arith |
|
467 qed |
|
468 moreover |
|
469 have "?\<theta> i = m" "?\<theta> k = r" using range by auto |
|
470 ultimately show "has_fth p i k m r" |
|
471 by (auto simp:has_fth_def) |
|
472 qed |
|
473 |
|
474 |
|
475 lemma desc_is_fthread: |
|
476 "is_desc_fthread \<theta> p i k \<Longrightarrow> is_fthread \<theta> p i k" |
|
477 unfolding is_desc_fthread_def |
|
478 by simp |
|
479 |
|
480 |
|
481 lemma combine_dfthreads: |
|
482 assumes range: "i < j" "j \<le> k" |
|
483 shows |
|
484 "has_desc_fth p i k m r = |
|
485 (\<exists>n. (has_desc_fth p i j m n \<and> has_fth p j k n r) |
|
486 \<or> (has_fth p i j m n \<and> has_desc_fth p j k n r))" (is "?L = ?R") |
|
487 proof |
|
488 assume "?L" |
|
489 then obtain \<theta> |
|
490 where desc: "is_desc_fthread \<theta> p i k" |
|
491 and [simp]: "\<theta> i = m" "\<theta> k = r" |
|
492 by (auto simp:has_desc_fth_def) |
|
493 |
|
494 hence "is_fthread \<theta> p i k" |
|
495 by (simp add: desc_is_fthread) |
|
496 with range have fths: "is_fthread \<theta> p i j" "is_fthread \<theta> p j k" |
|
497 unfolding is_fthread_def |
|
498 by auto |
|
499 hence hfths: "has_fth p i j m (\<theta> j)" "has_fth p j k (\<theta> j) r" |
|
500 by (auto simp:has_fth_def) |
|
501 |
|
502 from desc obtain l |
|
503 where "i \<le> l" "l < k" |
|
504 and "descat p \<theta> l" |
|
505 by (auto simp:is_desc_fthread_def) |
|
506 |
|
507 with fths |
|
508 have "is_desc_fthread \<theta> p i j \<or> is_desc_fthread \<theta> p j k" |
|
509 unfolding is_desc_fthread_def |
|
510 by (cases "l < j") auto |
|
511 hence "has_desc_fth p i j m (\<theta> j) \<or> has_desc_fth p j k (\<theta> j) r" |
|
512 by (auto simp:has_desc_fth_def) |
|
513 with hfths show ?R |
|
514 by auto |
|
515 next |
|
516 assume "?R" |
|
517 then obtain n \<theta>1 \<theta>2 |
|
518 where "(is_desc_fthread \<theta>1 p i j \<and> is_fthread \<theta>2 p j k) |
|
519 \<or> (is_fthread \<theta>1 p i j \<and> is_desc_fthread \<theta>2 p j k)" |
|
520 and [simp]: "\<theta>1 i = m" "\<theta>1 j = n" "\<theta>2 j = n" "\<theta>2 k = r" |
|
521 by (auto simp:has_fth_def has_desc_fth_def) |
|
522 |
|
523 hence ths2: "is_fthread \<theta>1 p i j" "is_fthread \<theta>2 p j k" |
|
524 and dths: "is_desc_fthread \<theta>1 p i j \<or> is_desc_fthread \<theta>2 p j k" |
|
525 by (auto simp:desc_is_fthread) |
|
526 |
|
527 let ?\<theta> = "(\<lambda>i. if i < j then \<theta>1 i else \<theta>2 i)" |
|
528 have "is_fthread ?\<theta> p i k" |
|
529 unfolding is_fthread_def |
|
530 proof |
|
531 fix l assume range: "l \<in> {i..<k}" |
|
532 |
|
533 show "eqlat p ?\<theta> l" |
|
534 proof (cases rule:three_cases) |
|
535 assume "Suc l < j" |
|
536 with ths2 range show ?thesis |
|
537 unfolding is_fthread_def Ball_def |
|
538 by simp |
|
539 next |
|
540 assume "Suc l = j" |
|
541 hence "l < j" "\<theta>2 (Suc l) = \<theta>1 (Suc l)" by auto |
|
542 with ths2 range show ?thesis |
|
543 unfolding is_fthread_def Ball_def |
|
544 by simp |
|
545 next |
|
546 assume "j \<le> l" |
|
547 with ths2 range show ?thesis |
|
548 unfolding is_fthread_def Ball_def |
|
549 by simp |
|
550 qed arith |
|
551 qed |
|
552 moreover |
|
553 from dths |
|
554 have "\<exists>l. i \<le> l \<and> l < k \<and> descat p ?\<theta> l" |
|
555 proof |
|
556 assume "is_desc_fthread \<theta>1 p i j" |
|
557 |
|
558 then obtain l where range: "i \<le> l" "l < j" and "descat p \<theta>1 l" |
|
559 unfolding is_desc_fthread_def Bex_def by auto |
|
560 hence "descat p ?\<theta> l" |
|
561 by (cases "Suc l = j", auto) |
|
562 with `j \<le> k` and range show ?thesis |
|
563 by (rule_tac x="l" in exI, auto) |
|
564 next |
|
565 assume "is_desc_fthread \<theta>2 p j k" |
|
566 then obtain l where range: "j \<le> l" "l < k" and "descat p \<theta>2 l" |
|
567 unfolding is_desc_fthread_def Bex_def by auto |
|
568 with `i < j` have "descat p ?\<theta> l" "i \<le> l" |
|
569 by auto |
|
570 with range show ?thesis |
|
571 by (rule_tac x="l" in exI, auto) |
|
572 qed |
|
573 ultimately have "is_desc_fthread ?\<theta> p i k" |
|
574 by (simp add: is_desc_fthread_def Bex_def) |
|
575 |
|
576 moreover |
|
577 have "?\<theta> i = m" "?\<theta> k = r" using range by auto |
|
578 |
|
579 ultimately show "has_desc_fth p i k m r" |
|
580 by (auto simp:has_desc_fth_def) |
|
581 qed |
|
582 |
|
583 |
|
584 |
|
585 lemma fth_single: |
|
586 "has_fth p i (Suc i) m n = eql (snd (p i)) m n" (is "?L = ?R") |
|
587 proof |
|
588 assume "?L" thus "?R" |
|
589 unfolding is_fthread_def Ball_def has_fth_def |
|
590 by auto |
|
591 next |
|
592 let ?\<theta> = "\<lambda>k. if k = i then m else n" |
|
593 assume edge: "?R" |
|
594 hence "is_fthread ?\<theta> p i (Suc i) \<and> ?\<theta> i = m \<and> ?\<theta> (Suc i) = n" |
|
595 unfolding is_fthread_def Ball_def |
|
596 by auto |
|
597 |
|
598 thus "?L" |
|
599 unfolding has_fth_def |
|
600 by auto |
|
601 qed |
|
602 |
|
603 lemma desc_fth_single: |
|
604 "has_desc_fth p i (Suc i) m n = |
|
605 dsc (snd (p i)) m n" (is "?L = ?R") |
|
606 proof |
|
607 assume "?L" thus "?R" |
|
608 unfolding is_desc_fthread_def has_desc_fth_def is_fthread_def |
|
609 Bex_def |
|
610 by (elim exE conjE) (case_tac "k = i", auto) |
|
611 next |
|
612 let ?\<theta> = "\<lambda>k. if k = i then m else n" |
|
613 assume edge: "?R" |
|
614 hence "is_desc_fthread ?\<theta> p i (Suc i) \<and> ?\<theta> i = m \<and> ?\<theta> (Suc i) = n" |
|
615 unfolding is_desc_fthread_def is_fthread_def Ball_def Bex_def |
|
616 by auto |
|
617 thus "?L" |
|
618 unfolding has_desc_fth_def |
|
619 by auto |
|
620 qed |
|
621 |
|
622 lemma mk_eql: "(G \<turnstile> m \<leadsto>\<^bsup>e\<^esup> n) \<Longrightarrow> eql G m n" |
|
623 by (cases e, auto) |
|
624 |
|
625 lemma eql_scgcomp: |
|
626 "eql (G * H) m r = |
|
627 (\<exists>n. eql G m n \<and> eql H n r)" (is "?L = ?R") |
|
628 proof |
|
629 show "?L \<Longrightarrow> ?R" |
|
630 by (auto simp:in_grcomp intro!:mk_eql) |
|
631 |
|
632 assume "?R" |
|
633 then obtain n where l: "eql G m n" and r:"eql H n r" by auto |
|
634 thus ?L |
|
635 by (cases "dsc G m n") (auto simp:in_grcomp mult_sedge_def) |
|
636 qed |
|
637 |
|
638 lemma desc_scgcomp: |
|
639 "dsc (G * H) m r = |
|
640 (\<exists>n. (dsc G m n \<and> eql H n r) \<or> (eq G m n \<and> dsc H n r))" (is "?L = ?R") |
|
641 proof |
|
642 show "?R \<Longrightarrow> ?L" by (auto simp:in_grcomp mult_sedge_def) |
|
643 |
|
644 assume "?L" |
|
645 thus ?R |
|
646 by (auto simp:in_grcomp mult_sedge_def) |
|
647 (case_tac "e", auto, case_tac "e'", auto) |
|
648 qed |
|
649 |
|
650 |
|
651 lemma has_fth_unfold: |
|
652 assumes "i < j" |
|
653 shows "has_fth p i j m n = |
|
654 (\<exists>r. has_fth p i (Suc i) m r \<and> has_fth p (Suc i) j r n)" |
|
655 by (rule combine_fthreads) (insert `i < j`, auto) |
|
656 |
|
657 lemma has_dfth_unfold: |
|
658 assumes range: "i < j" |
|
659 shows |
|
660 "has_desc_fth p i j m r = |
|
661 (\<exists>n. (has_desc_fth p i (Suc i) m n \<and> has_fth p (Suc i) j n r) |
|
662 \<or> (has_fth p i (Suc i) m n \<and> has_desc_fth p (Suc i) j n r))" |
|
663 by (rule combine_dfthreads) (insert `i < j`, auto) |
|
664 |
|
665 |
|
666 lemma Lemma7a: |
|
667 "i \<le> j \<Longrightarrow> has_fth p i j m n = eql (prod (p\<langle>i,j\<rangle>)) m n" |
|
668 proof (induct i arbitrary: m rule:inc_induct) |
|
669 case base show ?case |
|
670 unfolding has_fth_def is_fthread_def sub_path_def |
|
671 by (auto simp:in_grunit one_sedge_def) |
|
672 next |
|
673 case (step i) |
|
674 note IH = `\<And>m. has_fth p (Suc i) j m n = |
|
675 eql (prod (p\<langle>Suc i,j\<rangle>)) m n` |
|
676 |
|
677 have "has_fth p i j m n |
|
678 = (\<exists>r. has_fth p i (Suc i) m r \<and> has_fth p (Suc i) j r n)" |
|
679 by (rule has_fth_unfold[OF `i < j`]) |
|
680 also have "\<dots> = (\<exists>r. has_fth p i (Suc i) m r |
|
681 \<and> eql (prod (p\<langle>Suc i,j\<rangle>)) r n)" |
|
682 by (simp only:IH) |
|
683 also have "\<dots> = (\<exists>r. eql (snd (p i)) m r |
|
684 \<and> eql (prod (p\<langle>Suc i,j\<rangle>)) r n)" |
|
685 by (simp only:fth_single) |
|
686 also have "\<dots> = eql (snd (p i) * prod (p\<langle>Suc i,j\<rangle>)) m n" |
|
687 by (simp only:eql_scgcomp) |
|
688 also have "\<dots> = eql (prod (p\<langle>i,j\<rangle>)) m n" |
|
689 by (simp only:prod_unfold[OF `i < j`]) |
|
690 finally show ?case . |
|
691 qed |
|
692 |
|
693 |
|
694 lemma Lemma7b: |
|
695 assumes "i \<le> j" |
|
696 shows |
|
697 "has_desc_fth p i j m n = |
|
698 dsc (prod (p\<langle>i,j\<rangle>)) m n" |
|
699 using prems |
|
700 proof (induct i arbitrary: m rule:inc_induct) |
|
701 case base show ?case |
|
702 unfolding has_desc_fth_def is_desc_fthread_def sub_path_def |
|
703 by (auto simp:in_grunit one_sedge_def) |
|
704 next |
|
705 case (step i) |
|
706 thus ?case |
|
707 by (simp only:prod_unfold desc_scgcomp desc_fth_single |
|
708 has_dfth_unfold fth_single Lemma7a) auto |
|
709 qed |
|
710 |
|
711 |
|
712 lemma descat_contract: |
|
713 assumes [simp]: "increasing s" |
|
714 shows |
|
715 "descat (contract s p) \<theta> i = |
|
716 has_desc_fth p (s i) (s (Suc i)) (\<theta> i) (\<theta> (Suc i))" |
|
717 by (simp add:Lemma7b increasing_weak contract_def) |
|
718 |
|
719 lemma eqlat_contract: |
|
720 assumes [simp]: "increasing s" |
|
721 shows |
|
722 "eqlat (contract s p) \<theta> i = |
|
723 has_fth p (s i) (s (Suc i)) (\<theta> i) (\<theta> (Suc i))" |
|
724 by (auto simp:Lemma7a increasing_weak contract_def) |
|
725 |
|
726 |
|
727 subsubsection {* Connecting threads *} |
|
728 |
|
729 definition |
|
730 "connect s \<theta>s = (\<lambda>k. \<theta>s (section_of s k) k)" |
|
731 |
|
732 |
|
733 lemma next_in_range: |
|
734 assumes [simp]: "increasing s" |
|
735 assumes a: "k \<in> section s i" |
|
736 shows "(Suc k \<in> section s i) \<or> (Suc k \<in> section s (Suc i))" |
|
737 proof - |
|
738 from a have "k < s (Suc i)" by simp |
|
739 |
|
740 hence "Suc k < s (Suc i) \<or> Suc k = s (Suc i)" by arith |
|
741 thus ?thesis |
|
742 proof |
|
743 assume "Suc k < s (Suc i)" |
|
744 with a have "Suc k \<in> section s i" by simp |
|
745 thus ?thesis .. |
|
746 next |
|
747 assume eq: "Suc k = s (Suc i)" |
|
748 with increasing_strict have "Suc k < s (Suc (Suc i))" by simp |
|
749 with eq have "Suc k \<in> section s (Suc i)" by simp |
|
750 thus ?thesis .. |
|
751 qed |
|
752 qed |
|
753 |
|
754 |
|
755 lemma connect_threads: |
|
756 assumes [simp]: "increasing s" |
|
757 assumes connected: "\<theta>s i (s (Suc i)) = \<theta>s (Suc i) (s (Suc i))" |
|
758 assumes fth: "is_fthread (\<theta>s i) p (s i) (s (Suc i))" |
|
759 |
|
760 shows |
|
761 "is_fthread (connect s \<theta>s) p (s i) (s (Suc i))" |
|
762 unfolding is_fthread_def |
|
763 proof |
|
764 fix k assume krng: "k \<in> section s i" |
|
765 |
|
766 with fth have eqlat: "eqlat p (\<theta>s i) k" |
|
767 unfolding is_fthread_def by simp |
|
768 |
|
769 from krng and next_in_range |
|
770 have "(Suc k \<in> section s i) \<or> (Suc k \<in> section s (Suc i))" |
|
771 by simp |
|
772 thus "eqlat p (connect s \<theta>s) k" |
|
773 proof |
|
774 assume "Suc k \<in> section s i" |
|
775 with krng eqlat show ?thesis |
|
776 unfolding connect_def |
|
777 by (simp only:section_of_known `increasing s`) |
|
778 next |
|
779 assume skrng: "Suc k \<in> section s (Suc i)" |
|
780 with krng have "Suc k = s (Suc i)" by auto |
|
781 |
|
782 with krng skrng eqlat show ?thesis |
|
783 unfolding connect_def |
|
784 by (simp only:section_of_known connected[symmetric] `increasing s`) |
|
785 qed |
|
786 qed |
|
787 |
|
788 |
|
789 lemma connect_dthreads: |
|
790 assumes inc[simp]: "increasing s" |
|
791 assumes connected: "\<theta>s i (s (Suc i)) = \<theta>s (Suc i) (s (Suc i))" |
|
792 assumes fth: "is_desc_fthread (\<theta>s i) p (s i) (s (Suc i))" |
|
793 |
|
794 shows |
|
795 "is_desc_fthread (connect s \<theta>s) p (s i) (s (Suc i))" |
|
796 unfolding is_desc_fthread_def |
|
797 proof |
|
798 show "is_fthread (connect s \<theta>s) p (s i) (s (Suc i))" |
|
799 apply (rule connect_threads) |
|
800 apply (insert fth) |
|
801 by (auto simp:connected is_desc_fthread_def) |
|
802 |
|
803 from fth |
|
804 obtain k where dsc: "descat p (\<theta>s i) k" and krng: "k \<in> section s i" |
|
805 unfolding is_desc_fthread_def by blast |
|
806 |
|
807 from krng and next_in_range |
|
808 have "(Suc k \<in> section s i) \<or> (Suc k \<in> section s (Suc i))" |
|
809 by simp |
|
810 hence "descat p (connect s \<theta>s) k" |
|
811 proof |
|
812 assume "Suc k \<in> section s i" |
|
813 with krng dsc show ?thesis unfolding connect_def |
|
814 by (simp only:section_of_known inc) |
|
815 next |
|
816 assume skrng: "Suc k \<in> section s (Suc i)" |
|
817 with krng have "Suc k = s (Suc i)" by auto |
|
818 |
|
819 with krng skrng dsc show ?thesis unfolding connect_def |
|
820 by (simp only:section_of_known connected[symmetric] inc) |
|
821 qed |
|
822 with krng show "\<exists>k\<in>section s i. descat p (connect s \<theta>s) k" .. |
|
823 qed |
|
824 |
|
825 lemma mk_inf_thread: |
|
826 assumes [simp]: "increasing s" |
|
827 assumes fths: "\<And>i. i > n \<Longrightarrow> is_fthread \<theta> p (s i) (s (Suc i))" |
|
828 shows "is_thread (s (Suc n)) \<theta> p" |
|
829 unfolding is_thread_def |
|
830 proof (intro allI impI) |
|
831 fix j assume st: "s (Suc n) \<le> j" |
|
832 |
|
833 let ?k = "section_of s j" |
|
834 from in_section_of st |
|
835 have rs: "j \<in> section s ?k" by simp |
|
836 |
|
837 with st have "s (Suc n) < s (Suc ?k)" by simp |
|
838 with increasing_bij have "n < ?k" by simp |
|
839 with rs and fths[of ?k] |
|
840 show "eqlat p \<theta> j" by (simp add:is_fthread_def) |
|
841 qed |
|
842 |
|
843 |
|
844 lemma mk_inf_desc_thread: |
|
845 assumes [simp]: "increasing s" |
|
846 assumes fths: "\<And>i. i > n \<Longrightarrow> is_fthread \<theta> p (s i) (s (Suc i))" |
|
847 assumes fdths: "\<exists>\<^sub>\<infinity>i. is_desc_fthread \<theta> p (s i) (s (Suc i))" |
|
848 shows "is_desc_thread \<theta> p" |
|
849 unfolding is_desc_thread_def |
|
850 proof (intro exI conjI) |
|
851 |
|
852 from mk_inf_thread[of s n \<theta> p] fths |
|
853 show "\<forall>i\<ge>s (Suc n). eqlat p \<theta> i" |
|
854 by (fold is_thread_def) simp |
|
855 |
|
856 show "\<exists>\<^sub>\<infinity>l. descat p \<theta> l" |
|
857 unfolding INF_nat |
|
858 proof |
|
859 fix i |
|
860 |
|
861 let ?k = "section_of s i" |
|
862 from fdths obtain j |
|
863 where "?k < j" "is_desc_fthread \<theta> p (s j) (s (Suc j))" |
|
864 unfolding INF_nat by auto |
|
865 then obtain l where "s j \<le> l" and desc: "descat p \<theta> l" |
|
866 unfolding is_desc_fthread_def |
|
867 by auto |
|
868 |
|
869 have "i < s (Suc ?k)" by (rule section_of2) simp |
|
870 also have "\<dots> \<le> s j" |
|
871 by (rule increasing_weak [OF `increasing s`]) (insert `?k < j`, arith) |
|
872 also note `\<dots> \<le> l` |
|
873 finally have "i < l" . |
|
874 with desc |
|
875 show "\<exists>l. i < l \<and> descat p \<theta> l" by blast |
|
876 qed |
|
877 qed |
|
878 |
|
879 |
|
880 lemma desc_ex_choice: |
|
881 assumes A: "((\<exists>n.\<forall>i\<ge>n. \<exists>x. P x i) \<and> (\<exists>\<^sub>\<infinity>i. \<exists>x. Q x i))" |
|
882 and imp: "\<And>x i. Q x i \<Longrightarrow> P x i" |
|
883 shows "\<exists>xs. ((\<exists>n.\<forall>i\<ge>n. P (xs i) i) \<and> (\<exists>\<^sub>\<infinity>i. Q (xs i) i))" |
|
884 (is "\<exists>xs. ?Ps xs \<and> ?Qs xs") |
|
885 proof |
|
886 let ?w = "\<lambda>i. (if (\<exists>x. Q x i) then (SOME x. Q x i) |
|
887 else (SOME x. P x i))" |
|
888 |
|
889 from A |
|
890 obtain n where P: "\<And>i. n \<le> i \<Longrightarrow> \<exists>x. P x i" |
|
891 by auto |
|
892 { |
|
893 fix i::'a assume "n \<le> i" |
|
894 |
|
895 have "P (?w i) i" |
|
896 proof (cases "\<exists>x. Q x i") |
|
897 case True |
|
898 hence "Q (?w i) i" by (auto intro:someI) |
|
899 with imp show "P (?w i) i" . |
|
900 next |
|
901 case False |
|
902 with P[OF `n \<le> i`] show "P (?w i) i" |
|
903 by (auto intro:someI) |
|
904 qed |
|
905 } |
|
906 |
|
907 hence "?Ps ?w" by (rule_tac x=n in exI) auto |
|
908 |
|
909 moreover |
|
910 from A have "\<exists>\<^sub>\<infinity>i. (\<exists>x. Q x i)" .. |
|
911 hence "?Qs ?w" by (rule INF_mono) (auto intro:someI) |
|
912 ultimately |
|
913 show "?Ps ?w \<and> ?Qs ?w" .. |
|
914 qed |
|
915 |
|
916 |
|
917 |
|
918 lemma dthreads_join: |
|
919 assumes [simp]: "increasing s" |
|
920 assumes dthread: "is_desc_thread \<theta> (contract s p)" |
|
921 shows "\<exists>\<theta>s. desc (\<lambda>i. is_fthread (\<theta>s i) p (s i) (s (Suc i)) |
|
922 \<and> \<theta>s i (s i) = \<theta> i |
|
923 \<and> \<theta>s i (s (Suc i)) = \<theta> (Suc i)) |
|
924 (\<lambda>i. is_desc_fthread (\<theta>s i) p (s i) (s (Suc i)) |
|
925 \<and> \<theta>s i (s i) = \<theta> i |
|
926 \<and> \<theta>s i (s (Suc i)) = \<theta> (Suc i))" |
|
927 apply (rule desc_ex_choice) |
|
928 apply (insert dthread) |
|
929 apply (simp only:is_desc_thread_def) |
|
930 apply (simp add:eqlat_contract) |
|
931 apply (simp add:descat_contract) |
|
932 apply (simp only:has_fth_def has_desc_fth_def) |
|
933 by (auto simp:is_desc_fthread_def) |
|
934 |
|
935 |
|
936 |
|
937 lemma INF_drop_prefix: |
|
938 "(\<exists>\<^sub>\<infinity>i::nat. i > n \<and> P i) = (\<exists>\<^sub>\<infinity>i. P i)" |
|
939 apply (auto simp:INF_nat) |
|
940 apply (drule_tac x = "max m n" in spec) |
|
941 apply (elim exE conjE) |
|
942 apply (rule_tac x = "na" in exI) |
|
943 by auto |
|
944 |
|
945 |
|
946 |
|
947 lemma contract_keeps_threads: |
|
948 assumes inc[simp]: "increasing s" |
|
949 shows "(\<exists>\<theta>. is_desc_thread \<theta> p) |
|
950 \<longleftrightarrow> (\<exists>\<theta>. is_desc_thread \<theta> (contract s p))" |
|
951 (is "?A \<longleftrightarrow> ?B") |
|
952 proof |
|
953 assume "?A" |
|
954 then obtain \<theta> n |
|
955 where fr: "\<forall>i\<ge>n. eqlat p \<theta> i" |
|
956 and ds: "\<exists>\<^sub>\<infinity>i. descat p \<theta> i" |
|
957 unfolding is_desc_thread_def |
|
958 by auto |
|
959 |
|
960 let ?c\<theta> = "\<lambda>i. \<theta> (s i)" |
|
961 |
|
962 have "is_desc_thread ?c\<theta> (contract s p)" |
|
963 unfolding is_desc_thread_def |
|
964 proof (intro exI conjI) |
|
965 |
|
966 show "\<forall>i\<ge>n. eqlat (contract s p) ?c\<theta> i" |
|
967 proof (intro allI impI) |
|
968 fix i assume "n \<le> i" |
|
969 also have "i \<le> s i" |
|
970 using increasing_inc by auto |
|
971 finally have "n \<le> s i" . |
|
972 |
|
973 with fr have "is_fthread \<theta> p (s i) (s (Suc i))" |
|
974 unfolding is_fthread_def by auto |
|
975 hence "has_fth p (s i) (s (Suc i)) (\<theta> (s i)) (\<theta> (s (Suc i)))" |
|
976 unfolding has_fth_def by auto |
|
977 with less_imp_le[OF increasing_strict] |
|
978 have "eql (prod (p\<langle>s i,s (Suc i)\<rangle>)) (\<theta> (s i)) (\<theta> (s (Suc i)))" |
|
979 by (simp add:Lemma7a) |
|
980 thus "eqlat (contract s p) ?c\<theta> i" unfolding contract_def |
|
981 by auto |
|
982 qed |
|
983 |
|
984 show "\<exists>\<^sub>\<infinity>i. descat (contract s p) ?c\<theta> i" |
|
985 unfolding INF_nat |
|
986 proof |
|
987 fix i |
|
988 |
|
989 let ?K = "section_of s (max (s (Suc i)) n)" |
|
990 from `\<exists>\<^sub>\<infinity>i. descat p \<theta> i` obtain j |
|
991 where "s (Suc ?K) < j" "descat p \<theta> j" |
|
992 unfolding INF_nat by blast |
|
993 |
|
994 let ?L = "section_of s j" |
|
995 { |
|
996 fix x assume r: "x \<in> section s ?L" |
|
997 |
|
998 have e1: "max (s (Suc i)) n < s (Suc ?K)" by (rule section_of2) simp |
|
999 note `s (Suc ?K) < j` |
|
1000 also have "j < s (Suc ?L)" |
|
1001 by (rule section_of2) simp |
|
1002 finally have "Suc ?K \<le> ?L" |
|
1003 by (simp add:increasing_bij) |
|
1004 with increasing_weak have "s (Suc ?K) \<le> s ?L" by simp |
|
1005 with e1 r have "max (s (Suc i)) n < x" by simp |
|
1006 |
|
1007 hence "(s (Suc i)) < x" "n < x" by auto |
|
1008 } |
|
1009 note range_est = this |
|
1010 |
|
1011 have "is_desc_fthread \<theta> p (s ?L) (s (Suc ?L))" |
|
1012 unfolding is_desc_fthread_def is_fthread_def |
|
1013 proof |
|
1014 show "\<forall>m\<in>section s ?L. eqlat p \<theta> m" |
|
1015 proof |
|
1016 fix m assume "m\<in>section s ?L" |
|
1017 with range_est(2) have "n < m" . |
|
1018 with fr show "eqlat p \<theta> m" by simp |
|
1019 qed |
|
1020 |
|
1021 from in_section_of inc less_imp_le[OF `s (Suc ?K) < j`] |
|
1022 have "j \<in> section s ?L" . |
|
1023 |
|
1024 with `descat p \<theta> j` |
|
1025 show "\<exists>m\<in>section s ?L. descat p \<theta> m" .. |
|
1026 qed |
|
1027 |
|
1028 with less_imp_le[OF increasing_strict] |
|
1029 have a: "descat (contract s p) ?c\<theta> ?L" |
|
1030 unfolding contract_def Lemma7b[symmetric] |
|
1031 by (auto simp:Lemma7b[symmetric] has_desc_fth_def) |
|
1032 |
|
1033 have "i < ?L" |
|
1034 proof (rule classical) |
|
1035 assume "\<not> i < ?L" |
|
1036 hence "s ?L < s (Suc i)" |
|
1037 by (simp add:increasing_bij) |
|
1038 also have "\<dots> < s ?L" |
|
1039 by (rule range_est(1)) (simp add:increasing_strict) |
|
1040 finally show ?thesis . |
|
1041 qed |
|
1042 with a show "\<exists>l. i < l \<and> descat (contract s p) ?c\<theta> l" |
|
1043 by blast |
|
1044 qed |
|
1045 qed |
|
1046 with exI show "?B" . |
|
1047 next |
|
1048 assume "?B" |
|
1049 then obtain \<theta> |
|
1050 where dthread: "is_desc_thread \<theta> (contract s p)" .. |
|
1051 |
|
1052 with dthreads_join inc |
|
1053 obtain \<theta>s where ths_spec: |
|
1054 "desc (\<lambda>i. is_fthread (\<theta>s i) p (s i) (s (Suc i)) |
|
1055 \<and> \<theta>s i (s i) = \<theta> i |
|
1056 \<and> \<theta>s i (s (Suc i)) = \<theta> (Suc i)) |
|
1057 (\<lambda>i. is_desc_fthread (\<theta>s i) p (s i) (s (Suc i)) |
|
1058 \<and> \<theta>s i (s i) = \<theta> i |
|
1059 \<and> \<theta>s i (s (Suc i)) = \<theta> (Suc i))" |
|
1060 (is "desc ?alw ?inf") |
|
1061 by blast |
|
1062 |
|
1063 then obtain n where fr: "\<forall>i\<ge>n. ?alw i" by blast |
|
1064 hence connected: "\<And>i. n < i \<Longrightarrow> \<theta>s i (s (Suc i)) = \<theta>s (Suc i) (s (Suc i))" |
|
1065 by auto |
|
1066 |
|
1067 let ?j\<theta> = "connect s \<theta>s" |
|
1068 |
|
1069 from fr ths_spec have ths_spec2: |
|
1070 "\<And>i. i > n \<Longrightarrow> is_fthread (\<theta>s i) p (s i) (s (Suc i))" |
|
1071 "\<exists>\<^sub>\<infinity>i. is_desc_fthread (\<theta>s i) p (s i) (s (Suc i))" |
|
1072 by (auto intro:INF_mono) |
|
1073 |
|
1074 have p1: "\<And>i. i > n \<Longrightarrow> is_fthread ?j\<theta> p (s i) (s (Suc i))" |
|
1075 by (rule connect_threads) (auto simp:connected ths_spec2) |
|
1076 |
|
1077 from ths_spec2(2) |
|
1078 have "\<exists>\<^sub>\<infinity>i. n < i \<and> is_desc_fthread (\<theta>s i) p (s i) (s (Suc i))" |
|
1079 unfolding INF_drop_prefix . |
|
1080 |
|
1081 hence p2: "\<exists>\<^sub>\<infinity>i. is_desc_fthread ?j\<theta> p (s i) (s (Suc i))" |
|
1082 apply (rule INF_mono) |
|
1083 apply (rule connect_dthreads) |
|
1084 by (auto simp:connected) |
|
1085 |
|
1086 with `increasing s` p1 |
|
1087 have "is_desc_thread ?j\<theta> p" |
|
1088 by (rule mk_inf_desc_thread) |
|
1089 with exI show "?A" . |
|
1090 qed |
|
1091 |
|
1092 |
|
1093 lemma repeated_edge: |
|
1094 assumes "\<And>i. i > n \<Longrightarrow> dsc (snd (p i)) k k" |
|
1095 shows "is_desc_thread (\<lambda>i. k) p" |
|
1096 proof- |
|
1097 have th: "\<forall> m. \<exists>na>m. n < na" by arith |
|
1098 show ?thesis using prems |
|
1099 unfolding is_desc_thread_def |
|
1100 apply (auto) |
|
1101 apply (rule_tac x="Suc n" in exI, auto) |
|
1102 apply (rule INF_mono[where P="\<lambda>i. n < i"]) |
|
1103 apply (simp only:INF_nat) |
|
1104 by (auto simp add: th) |
|
1105 qed |
|
1106 |
|
1107 lemma fin_from_inf: |
|
1108 assumes "is_thread n \<theta> p" |
|
1109 assumes "n < i" |
|
1110 assumes "i < j" |
|
1111 shows "is_fthread \<theta> p i j" |
|
1112 using prems |
|
1113 unfolding is_thread_def is_fthread_def |
|
1114 by auto |
|
1115 |
|
1116 |
|
1117 subsection {* Ramsey's Theorem *} |
|
1118 |
|
1119 definition |
|
1120 "set2pair S = (THE (x,y). x < y \<and> S = {x,y})" |
|
1121 |
|
1122 lemma set2pair_conv: |
|
1123 fixes x y :: nat |
|
1124 assumes "x < y" |
|
1125 shows "set2pair {x, y} = (x, y)" |
|
1126 unfolding set2pair_def |
|
1127 proof (rule the_equality, simp_all only:split_conv split_paired_all) |
|
1128 from `x < y` show "x < y \<and> {x,y}={x,y}" by simp |
|
1129 next |
|
1130 fix a b |
|
1131 assume a: "a < b \<and> {x, y} = {a, b}" |
|
1132 hence "{a, b} = {x, y}" by simp_all |
|
1133 hence "(a, b) = (x, y) \<or> (a, b) = (y, x)" |
|
1134 by (cases "x = y") auto |
|
1135 thus "(a, b) = (x, y)" |
|
1136 proof |
|
1137 assume "(a, b) = (y, x)" |
|
1138 with a and `x < y` |
|
1139 show ?thesis by auto (* contradiction *) |
|
1140 qed |
|
1141 qed |
|
1142 |
|
1143 definition |
|
1144 "set2list = inv set" |
|
1145 |
|
1146 lemma finite_set2list: |
|
1147 assumes "finite S" |
|
1148 shows "set (set2list S) = S" |
|
1149 unfolding set2list_def |
|
1150 proof (rule f_inv_f) |
|
1151 from `finite S` have "\<exists>l. set l = S" |
|
1152 by (rule finite_list) |
|
1153 thus "S \<in> range set" |
|
1154 unfolding image_def |
|
1155 by auto |
|
1156 qed |
|
1157 |
|
1158 |
|
1159 corollary RamseyNatpairs: |
|
1160 fixes S :: "'a set" |
|
1161 and f :: "nat \<times> nat \<Rightarrow> 'a" |
|
1162 |
|
1163 assumes "finite S" |
|
1164 and inS: "\<And>x y. x < y \<Longrightarrow> f (x, y) \<in> S" |
|
1165 |
|
1166 obtains T :: "nat set" and s :: "'a" |
|
1167 where "infinite T" |
|
1168 and "s \<in> S" |
|
1169 and "\<And>x y. \<lbrakk>x \<in> T; y \<in> T; x < y\<rbrakk> \<Longrightarrow> f (x, y) = s" |
|
1170 proof - |
|
1171 from `finite S` |
|
1172 have "set (set2list S) = S" by (rule finite_set2list) |
|
1173 then |
|
1174 obtain l where S: "S = set l" by auto |
|
1175 also from set_conv_nth have "\<dots> = {l ! i |i. i < length l}" . |
|
1176 finally have "S = {l ! i |i. i < length l}" . |
|
1177 |
|
1178 let ?s = "length l" |
|
1179 |
|
1180 from inS |
|
1181 have index_less: "\<And>x y. x \<noteq> y \<Longrightarrow> index_of l (f (set2pair {x, y})) < ?s" |
|
1182 proof - |
|
1183 fix x y :: nat |
|
1184 assume neq: "x \<noteq> y" |
|
1185 have "f (set2pair {x, y}) \<in> S" |
|
1186 proof (cases "x < y") |
|
1187 case True hence "set2pair {x, y} = (x, y)" |
|
1188 by (rule set2pair_conv) |
|
1189 with True inS |
|
1190 show ?thesis by simp |
|
1191 next |
|
1192 case False |
|
1193 with neq have y_less: "y < x" by simp |
|
1194 have x:"{x,y} = {y,x}" by auto |
|
1195 with y_less have "set2pair {x, y} = (y, x)" |
|
1196 by (simp add:set2pair_conv) |
|
1197 with y_less inS |
|
1198 show ?thesis by simp |
|
1199 qed |
|
1200 |
|
1201 thus "index_of l (f (set2pair {x, y})) < length l" |
|
1202 by (simp add: S index_of_length) |
|
1203 qed |
|
1204 |
|
1205 have "\<exists>Y. infinite Y \<and> |
|
1206 (\<exists>t. t < ?s \<and> |
|
1207 (\<forall>x\<in>Y. \<forall>y\<in>Y. x \<noteq> y \<longrightarrow> |
|
1208 index_of l (f (set2pair {x, y})) = t))" |
|
1209 by (rule Ramsey2[of "UNIV::nat set", simplified]) |
|
1210 (auto simp:index_less) |
|
1211 then obtain T i |
|
1212 where inf: "infinite T" |
|
1213 and i: "i < length l" |
|
1214 and d: "\<And>x y. \<lbrakk>x \<in> T; y\<in>T; x \<noteq> y\<rbrakk> |
|
1215 \<Longrightarrow> index_of l (f (set2pair {x, y})) = i" |
|
1216 by auto |
|
1217 |
|
1218 have "l ! i \<in> S" unfolding S using i |
|
1219 by (rule nth_mem) |
|
1220 moreover |
|
1221 have "\<And>x y. x \<in> T \<Longrightarrow> y\<in>T \<Longrightarrow> x < y |
|
1222 \<Longrightarrow> f (x, y) = l ! i" |
|
1223 proof - |
|
1224 fix x y assume "x \<in> T" "y \<in> T" "x < y" |
|
1225 with d have |
|
1226 "index_of l (f (set2pair {x, y})) = i" by auto |
|
1227 with `x < y` |
|
1228 have "i = index_of l (f (x, y))" |
|
1229 by (simp add:set2pair_conv) |
|
1230 with `i < length l` |
|
1231 show "f (x, y) = l ! i" |
|
1232 by (auto intro:index_of_member[symmetric] iff:index_of_length) |
|
1233 qed |
|
1234 moreover note inf |
|
1235 ultimately |
|
1236 show ?thesis using prems |
|
1237 by blast |
|
1238 qed |
|
1239 |
|
1240 |
|
1241 subsection {* Main Result *} |
|
1242 |
|
1243 |
|
1244 theorem LJA_Theorem4: |
|
1245 assumes "finite_acg A" |
|
1246 shows "SCT A \<longleftrightarrow> SCT' A" |
|
1247 proof |
|
1248 assume "SCT A" |
|
1249 |
|
1250 show "SCT' A" |
|
1251 proof (rule classical) |
|
1252 assume "\<not> SCT' A" |
|
1253 |
|
1254 then obtain n G |
|
1255 where in_closure: "(tcl A) \<turnstile> n \<leadsto>\<^bsup>G\<^esup> n" |
|
1256 and idemp: "G * G = G" |
|
1257 and no_strict_arc: "\<forall>p. \<not>(G \<turnstile> p \<leadsto>\<^bsup>\<down>\<^esup> p)" |
|
1258 unfolding SCT'_def no_bad_graphs_def by auto |
|
1259 |
|
1260 from in_closure obtain k |
|
1261 where k_pow: "A ^ k \<turnstile> n \<leadsto>\<^bsup>G\<^esup> n" |
|
1262 and "0 < k" |
|
1263 unfolding in_tcl by auto |
|
1264 |
|
1265 from power_induces_path k_pow |
|
1266 obtain loop where loop_props: |
|
1267 "has_fpath A loop" |
|
1268 "n = fst loop" "n = end_node loop" |
|
1269 "G = prod loop" "k = length (snd loop)" . |
|
1270 |
|
1271 with `0 < k` and path_loop_graph |
|
1272 have "has_ipath A (omega loop)" by blast |
|
1273 with `SCT A` |
|
1274 have thread: "\<exists>\<theta>. is_desc_thread \<theta> (omega loop)" by (auto simp:SCT_def) |
|
1275 |
|
1276 let ?s = "\<lambda>i. k * i" |
|
1277 let ?cp = "\<lambda>i::nat. (n, G)" |
|
1278 |
|
1279 from loop_props have "fst loop = end_node loop" by auto |
|
1280 with `0 < k` `k = length (snd loop)` |
|
1281 have "\<And>i. (omega loop)\<langle>?s i,?s (Suc i)\<rangle> = loop" |
|
1282 by (rule sub_path_loop) |
|
1283 |
|
1284 with `n = fst loop` `G = prod loop` `k = length (snd loop)` |
|
1285 have a: "contract ?s (omega loop) = ?cp" |
|
1286 unfolding contract_def |
|
1287 by (simp add:path_loop_def split_def fst_p0) |
|
1288 |
|
1289 from `0 < k` have "increasing ?s" |
|
1290 by (auto simp:increasing_def) |
|
1291 with thread have "\<exists>\<theta>. is_desc_thread \<theta> ?cp" |
|
1292 unfolding a[symmetric] |
|
1293 by (unfold contract_keeps_threads[symmetric]) |
|
1294 |
|
1295 then obtain \<theta> where desc: "is_desc_thread \<theta> ?cp" by auto |
|
1296 |
|
1297 then obtain n where thr: "is_thread n \<theta> ?cp" |
|
1298 unfolding is_desc_thread_def is_thread_def |
|
1299 by auto |
|
1300 |
|
1301 have "finite (range \<theta>)" |
|
1302 proof (rule finite_range_ignore_prefix) |
|
1303 |
|
1304 from `finite_acg A` |
|
1305 have "finite_acg (tcl A)" by (simp add:finite_tcl) |
|
1306 with in_closure have "finite_graph G" |
|
1307 unfolding finite_acg_def all_finite_def by blast |
|
1308 thus "finite (nodes G)" by (rule finite_nodes) |
|
1309 |
|
1310 from thread_image_nodes[OF thr] |
|
1311 show "\<forall>i\<ge>n. \<theta> i \<in> nodes G" by simp |
|
1312 qed |
|
1313 with finite_range |
|
1314 obtain p where inf_visit: "\<exists>\<^sub>\<infinity>i. \<theta> i = p" by auto |
|
1315 |
|
1316 then obtain i where "n < i" "\<theta> i = p" |
|
1317 by (auto simp:INF_nat) |
|
1318 |
|
1319 from desc |
|
1320 have "\<exists>\<^sub>\<infinity>i. descat ?cp \<theta> i" |
|
1321 unfolding is_desc_thread_def by auto |
|
1322 then obtain j |
|
1323 where "i < j" and "descat ?cp \<theta> j" |
|
1324 unfolding INF_nat by auto |
|
1325 from inf_visit obtain k where "j < k" "\<theta> k = p" |
|
1326 by (auto simp:INF_nat) |
|
1327 |
|
1328 from `i < j` `j < k` `n < i` thr |
|
1329 fin_from_inf[of n \<theta> ?cp] |
|
1330 `descat ?cp \<theta> j` |
|
1331 have "is_desc_fthread \<theta> ?cp i k" |
|
1332 unfolding is_desc_fthread_def |
|
1333 by auto |
|
1334 |
|
1335 with `\<theta> k = p` `\<theta> i = p` |
|
1336 have dfth: "has_desc_fth ?cp i k p p" |
|
1337 unfolding has_desc_fth_def |
|
1338 by auto |
|
1339 |
|
1340 from `i < j` `j < k` have "i < k" by auto |
|
1341 hence "prod (?cp\<langle>i, k\<rangle>) = G" |
|
1342 proof (induct i rule:strict_inc_induct) |
|
1343 case base thus ?case by (simp add:sub_path_def) |
|
1344 next |
|
1345 case (step i) thus ?case |
|
1346 by (simp add:sub_path_def upt_rec[of i k] idemp) |
|
1347 qed |
|
1348 |
|
1349 with `i < j` `j < k` dfth Lemma7b[of i k ?cp p p] |
|
1350 have "dsc G p p" by auto |
|
1351 with no_strict_arc have False by auto |
|
1352 thus ?thesis .. |
|
1353 qed |
|
1354 next |
|
1355 assume "SCT' A" |
|
1356 |
|
1357 show "SCT A" |
|
1358 proof (rule classical) |
|
1359 assume "\<not> SCT A" |
|
1360 |
|
1361 with SCT_def |
|
1362 obtain p |
|
1363 where ipath: "has_ipath A p" |
|
1364 and no_desc_th: "\<not> (\<exists>\<theta>. is_desc_thread \<theta> p)" |
|
1365 by blast |
|
1366 |
|
1367 from `finite_acg A` |
|
1368 have "finite_acg (tcl A)" by (simp add: finite_tcl) |
|
1369 hence "finite (dest_graph (tcl A))" (is "finite ?AG") |
|
1370 by (simp add: finite_acg_def finite_graph_def) |
|
1371 |
|
1372 from pdesc_acgplus[OF ipath] |
|
1373 have a: "\<And>x y. x<y \<Longrightarrow> pdesc p\<langle>x,y\<rangle> \<in> dest_graph (tcl A)" |
|
1374 unfolding has_edge_def . |
|
1375 |
|
1376 obtain S G |
|
1377 where "infinite S" "G \<in> dest_graph (tcl A)" |
|
1378 and all_G: "\<And>x y. \<lbrakk> x \<in> S; y \<in> S; x < y\<rbrakk> \<Longrightarrow> |
|
1379 pdesc (p\<langle>x,y\<rangle>) = G" |
|
1380 apply (rule RamseyNatpairs[of ?AG "\<lambda>(x,y). pdesc p\<langle>x, y\<rangle>"]) |
|
1381 apply (rule `finite ?AG`) |
|
1382 by (simp only:split_conv, rule a, auto) |
|
1383 |
|
1384 obtain n H m where |
|
1385 G_struct: "G = (n, H, m)" by (cases G) |
|
1386 |
|
1387 let ?s = "enumerate S" |
|
1388 let ?q = "contract ?s p" |
|
1389 |
|
1390 note all_in_S[simp] = enumerate_in_set[OF `infinite S`] |
|
1391 from `infinite S` |
|
1392 have inc[simp]: "increasing ?s" |
|
1393 unfolding increasing_def by (simp add:enumerate_mono) |
|
1394 note increasing_bij[OF this, simp] |
|
1395 |
|
1396 from ipath_contract inc ipath |
|
1397 have "has_ipath (tcl A) ?q" . |
|
1398 |
|
1399 from all_G G_struct |
|
1400 have all_H: "\<And>i. (snd (?q i)) = H" |
|
1401 unfolding contract_def |
|
1402 by simp |
|
1403 |
|
1404 have loop: "(tcl A) \<turnstile> n \<leadsto>\<^bsup>H\<^esup> n" |
|
1405 and idemp: "H * H = H" |
|
1406 proof - |
|
1407 let ?i = "?s 0" and ?j = "?s (Suc 0)" and ?k = "?s (Suc (Suc 0))" |
|
1408 |
|
1409 have "pdesc (p\<langle>?i,?j\<rangle>) = G" |
|
1410 and "pdesc (p\<langle>?j,?k\<rangle>) = G" |
|
1411 and "pdesc (p\<langle>?i,?k\<rangle>) = G" |
|
1412 using all_G |
|
1413 by auto |
|
1414 |
|
1415 with G_struct |
|
1416 have "m = end_node (p\<langle>?i,?j\<rangle>)" |
|
1417 "n = fst (p\<langle>?j,?k\<rangle>)" |
|
1418 and Hs: "prod (p\<langle>?i,?j\<rangle>) = H" |
|
1419 "prod (p\<langle>?j,?k\<rangle>) = H" |
|
1420 "prod (p\<langle>?i,?k\<rangle>) = H" |
|
1421 by auto |
|
1422 |
|
1423 hence "m = n" by simp |
|
1424 thus "tcl A \<turnstile> n \<leadsto>\<^bsup>H\<^esup> n" |
|
1425 using G_struct `G \<in> dest_graph (tcl A)` |
|
1426 by (simp add:has_edge_def) |
|
1427 |
|
1428 from sub_path_prod[of ?i ?j ?k p] |
|
1429 show "H * H = H" |
|
1430 unfolding Hs by simp |
|
1431 qed |
|
1432 moreover have "\<And>k. \<not>dsc H k k" |
|
1433 proof |
|
1434 fix k :: 'a assume "dsc H k k" |
|
1435 |
|
1436 with all_H repeated_edge |
|
1437 have "\<exists>\<theta>. is_desc_thread \<theta> ?q" by fast |
|
1438 with inc have "\<exists>\<theta>. is_desc_thread \<theta> p" |
|
1439 by (subst contract_keeps_threads) |
|
1440 with no_desc_th |
|
1441 show False .. |
|
1442 qed |
|
1443 ultimately |
|
1444 have False |
|
1445 using `SCT' A`[unfolded SCT'_def no_bad_graphs_def] |
|
1446 by blast |
|
1447 thus ?thesis .. |
|
1448 qed |
|
1449 qed |
|
1450 |
|
1451 end |