1 (* Title: HOL/Library/Graphs.thy |
|
2 ID: $Id$ |
|
3 Author: Alexander Krauss, TU Muenchen |
|
4 *) |
|
5 |
|
6 header {* General Graphs as Sets *} |
|
7 |
|
8 theory Graphs |
|
9 imports Main SCT_Misc Kleene_Algebras |
|
10 begin |
|
11 |
|
12 subsection {* Basic types, Size Change Graphs *} |
|
13 |
|
14 datatype ('a, 'b) graph = |
|
15 Graph "('a \<times> 'b \<times> 'a) set" |
|
16 |
|
17 fun dest_graph :: "('a, 'b) graph \<Rightarrow> ('a \<times> 'b \<times> 'a) set" |
|
18 where "dest_graph (Graph G) = G" |
|
19 |
|
20 lemma graph_dest_graph[simp]: |
|
21 "Graph (dest_graph G) = G" |
|
22 by (cases G) simp |
|
23 |
|
24 lemma split_graph_all: |
|
25 "(\<And>gr. PROP P gr) \<equiv> (\<And>set. PROP P (Graph set))" |
|
26 proof |
|
27 fix set |
|
28 assume "\<And>gr. PROP P gr" |
|
29 then show "PROP P (Graph set)" . |
|
30 next |
|
31 fix gr |
|
32 assume "\<And>set. PROP P (Graph set)" |
|
33 then have "PROP P (Graph (dest_graph gr))" . |
|
34 then show "PROP P gr" by simp |
|
35 qed |
|
36 |
|
37 definition |
|
38 has_edge :: "('n,'e) graph \<Rightarrow> 'n \<Rightarrow> 'e \<Rightarrow> 'n \<Rightarrow> bool" |
|
39 ("_ \<turnstile> _ \<leadsto>\<^bsup>_\<^esup> _") |
|
40 where |
|
41 "has_edge G n e n' = ((n, e, n') \<in> dest_graph G)" |
|
42 |
|
43 |
|
44 subsection {* Graph composition *} |
|
45 |
|
46 fun grcomp :: "('n, 'e::times) graph \<Rightarrow> ('n, 'e) graph \<Rightarrow> ('n, 'e) graph" |
|
47 where |
|
48 "grcomp (Graph G) (Graph H) = |
|
49 Graph {(p,b,q) | p b q. |
|
50 (\<exists>k e e'. (p,e,k)\<in>G \<and> (k,e',q)\<in>H \<and> b = e * e')}" |
|
51 |
|
52 |
|
53 declare grcomp.simps[code del] |
|
54 |
|
55 |
|
56 lemma graph_ext: |
|
57 assumes "\<And>n e n'. has_edge G n e n' = has_edge H n e n'" |
|
58 shows "G = H" |
|
59 using assms |
|
60 by (cases G, cases H) (auto simp:split_paired_all has_edge_def) |
|
61 |
|
62 |
|
63 instance graph :: (type, type) "{comm_monoid_add}" |
|
64 graph_zero_def: "0 == Graph {}" |
|
65 graph_plus_def: "G + H == Graph (dest_graph G \<union> dest_graph H)" |
|
66 proof |
|
67 fix x y z :: "('a,'b) graph" |
|
68 |
|
69 show "x + y + z = x + (y + z)" |
|
70 and "x + y = y + x" |
|
71 and "0 + x = x" |
|
72 unfolding graph_plus_def graph_zero_def |
|
73 by auto |
|
74 qed |
|
75 |
|
76 lemmas [code func del] = graph_plus_def |
|
77 |
|
78 instance graph :: (type, type) "{distrib_lattice, complete_lattice}" |
|
79 graph_leq_def: "G \<le> H \<equiv> dest_graph G \<subseteq> dest_graph H" |
|
80 graph_less_def: "G < H \<equiv> dest_graph G \<subset> dest_graph H" |
|
81 "inf G H \<equiv> Graph (dest_graph G \<inter> dest_graph H)" |
|
82 "sup G H \<equiv> G + H" |
|
83 Inf_graph_def: "Inf \<equiv> \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))" |
|
84 Sup_graph_def: "Sup \<equiv> \<lambda>Gs. Graph (\<Union>(dest_graph ` Gs))" |
|
85 proof |
|
86 fix x y z :: "('a,'b) graph" |
|
87 fix A :: "('a, 'b) graph set" |
|
88 |
|
89 show "(x < y) = (x \<le> y \<and> x \<noteq> y)" |
|
90 unfolding graph_leq_def graph_less_def |
|
91 by (cases x, cases y) auto |
|
92 |
|
93 show "x \<le> x" unfolding graph_leq_def .. |
|
94 |
|
95 { assume "x \<le> y" "y \<le> z" |
|
96 with order_trans show "x \<le> z" |
|
97 unfolding graph_leq_def . } |
|
98 |
|
99 { assume "x \<le> y" "y \<le> x" thus "x = y" |
|
100 unfolding graph_leq_def |
|
101 by (cases x, cases y) simp } |
|
102 |
|
103 show "inf x y \<le> x" "inf x y \<le> y" |
|
104 unfolding inf_graph_def graph_leq_def |
|
105 by auto |
|
106 |
|
107 { assume "x \<le> y" "x \<le> z" thus "x \<le> inf y z" |
|
108 unfolding inf_graph_def graph_leq_def |
|
109 by auto } |
|
110 |
|
111 show "x \<le> sup x y" "y \<le> sup x y" |
|
112 unfolding sup_graph_def graph_leq_def graph_plus_def by auto |
|
113 |
|
114 { assume "y \<le> x" "z \<le> x" thus "sup y z \<le> x" |
|
115 unfolding sup_graph_def graph_leq_def graph_plus_def by auto } |
|
116 |
|
117 show "sup x (inf y z) = inf (sup x y) (sup x z)" |
|
118 unfolding inf_graph_def sup_graph_def graph_leq_def graph_plus_def by auto |
|
119 |
|
120 { assume "x \<in> A" thus "Inf A \<le> x" |
|
121 unfolding Inf_graph_def graph_leq_def by auto } |
|
122 |
|
123 { assume "\<And>x. x \<in> A \<Longrightarrow> z \<le> x" thus "z \<le> Inf A" |
|
124 unfolding Inf_graph_def graph_leq_def by auto } |
|
125 |
|
126 { assume "x \<in> A" thus "x \<le> Sup A" |
|
127 unfolding Sup_graph_def graph_leq_def by auto } |
|
128 |
|
129 { assume "\<And>x. x \<in> A \<Longrightarrow> x \<le> z" thus "Sup A \<le> z" |
|
130 unfolding Sup_graph_def graph_leq_def by auto } |
|
131 qed |
|
132 |
|
133 lemmas [code func del] = graph_leq_def graph_less_def |
|
134 inf_graph_def sup_graph_def Inf_graph_def Sup_graph_def |
|
135 |
|
136 lemma in_grplus: |
|
137 "has_edge (G + H) p b q = (has_edge G p b q \<or> has_edge H p b q)" |
|
138 by (cases G, cases H, auto simp:has_edge_def graph_plus_def) |
|
139 |
|
140 lemma in_grzero: |
|
141 "has_edge 0 p b q = False" |
|
142 by (simp add:graph_zero_def has_edge_def) |
|
143 |
|
144 |
|
145 subsubsection {* Multiplicative Structure *} |
|
146 |
|
147 instance graph :: (type, times) mult_zero |
|
148 graph_mult_def: "G * H == grcomp G H" |
|
149 proof |
|
150 fix a :: "('a, 'b) graph" |
|
151 |
|
152 show "0 * a = 0" |
|
153 unfolding graph_mult_def graph_zero_def |
|
154 by (cases a) (simp add:grcomp.simps) |
|
155 show "a * 0 = 0" |
|
156 unfolding graph_mult_def graph_zero_def |
|
157 by (cases a) (simp add:grcomp.simps) |
|
158 qed |
|
159 |
|
160 lemmas [code func del] = graph_mult_def |
|
161 |
|
162 instance graph :: (type, one) one |
|
163 graph_one_def: "1 == Graph { (x, 1, x) |x. True}" .. |
|
164 |
|
165 lemma in_grcomp: |
|
166 "has_edge (G * H) p b q |
|
167 = (\<exists>k e e'. has_edge G p e k \<and> has_edge H k e' q \<and> b = e * e')" |
|
168 by (cases G, cases H) (auto simp:graph_mult_def has_edge_def image_def) |
|
169 |
|
170 lemma in_grunit: |
|
171 "has_edge 1 p b q = (p = q \<and> b = 1)" |
|
172 by (auto simp:graph_one_def has_edge_def) |
|
173 |
|
174 instance graph :: (type, semigroup_mult) semigroup_mult |
|
175 proof |
|
176 fix G1 G2 G3 :: "('a,'b) graph" |
|
177 |
|
178 show "G1 * G2 * G3 = G1 * (G2 * G3)" |
|
179 proof (rule graph_ext, rule trans) |
|
180 fix p J q |
|
181 show "has_edge ((G1 * G2) * G3) p J q = |
|
182 (\<exists>G i H j I. |
|
183 has_edge G1 p G i |
|
184 \<and> has_edge G2 i H j |
|
185 \<and> has_edge G3 j I q |
|
186 \<and> J = (G * H) * I)" |
|
187 by (simp only:in_grcomp) blast |
|
188 show "\<dots> = has_edge (G1 * (G2 * G3)) p J q" |
|
189 by (simp only:in_grcomp mult_assoc) blast |
|
190 qed |
|
191 qed |
|
192 |
|
193 fun grpow :: "nat \<Rightarrow> ('a::type, 'b::monoid_mult) graph \<Rightarrow> ('a, 'b) graph" |
|
194 where |
|
195 "grpow 0 A = 1" |
|
196 | "grpow (Suc n) A = A * (grpow n A)" |
|
197 |
|
198 instance graph :: (type, monoid_mult) |
|
199 "{semiring_1,idem_add,recpower,star}" |
|
200 graph_pow_def: "A ^ n == grpow n A" |
|
201 graph_star_def: "star G == (SUP n. G ^ n)" |
|
202 proof |
|
203 fix a b c :: "('a, 'b) graph" |
|
204 |
|
205 show "1 * a = a" |
|
206 by (rule graph_ext) (auto simp:in_grcomp in_grunit) |
|
207 show "a * 1 = a" |
|
208 by (rule graph_ext) (auto simp:in_grcomp in_grunit) |
|
209 |
|
210 show "(a + b) * c = a * c + b * c" |
|
211 by (rule graph_ext, simp add:in_grcomp in_grplus) blast |
|
212 |
|
213 show "a * (b + c) = a * b + a * c" |
|
214 by (rule graph_ext, simp add:in_grcomp in_grplus) blast |
|
215 |
|
216 show "(0::('a,'b) graph) \<noteq> 1" unfolding graph_zero_def graph_one_def |
|
217 by simp |
|
218 |
|
219 show "a + a = a" unfolding graph_plus_def by simp |
|
220 |
|
221 show "a ^ 0 = 1" "\<And>n. a ^ (Suc n) = a * a ^ n" |
|
222 unfolding graph_pow_def by simp_all |
|
223 qed |
|
224 |
|
225 lemma graph_leqI: |
|
226 assumes "\<And>n e n'. has_edge G n e n' \<Longrightarrow> has_edge H n e n'" |
|
227 shows "G \<le> H" |
|
228 using assms |
|
229 unfolding graph_leq_def has_edge_def |
|
230 by auto |
|
231 |
|
232 lemma in_graph_plusE: |
|
233 assumes "has_edge (G + H) n e n'" |
|
234 assumes "has_edge G n e n' \<Longrightarrow> P" |
|
235 assumes "has_edge H n e n' \<Longrightarrow> P" |
|
236 shows P |
|
237 using assms |
|
238 by (auto simp: in_grplus) |
|
239 |
|
240 lemma in_graph_compE: |
|
241 assumes GH: "has_edge (G * H) n e n'" |
|
242 obtains e1 k e2 |
|
243 where "has_edge G n e1 k" "has_edge H k e2 n'" "e = e1 * e2" |
|
244 using GH |
|
245 by (auto simp: in_grcomp) |
|
246 |
|
247 lemma |
|
248 assumes "x \<in> S k" |
|
249 shows "x \<in> (\<Union>k. S k)" |
|
250 using assms by blast |
|
251 |
|
252 lemma graph_union_least: |
|
253 assumes "\<And>n. Graph (G n) \<le> C" |
|
254 shows "Graph (\<Union>n. G n) \<le> C" |
|
255 using assms unfolding graph_leq_def |
|
256 by auto |
|
257 |
|
258 lemma Sup_graph_eq: |
|
259 "(SUP n. Graph (G n)) = Graph (\<Union>n. G n)" |
|
260 proof (rule order_antisym) |
|
261 show "(SUP n. Graph (G n)) \<le> Graph (\<Union>n. G n)" |
|
262 by (rule SUP_leI) (auto simp add: graph_leq_def) |
|
263 |
|
264 show "Graph (\<Union>n. G n) \<le> (SUP n. Graph (G n))" |
|
265 by (rule graph_union_least, rule le_SUPI', rule) |
|
266 qed |
|
267 |
|
268 lemma has_edge_leq: "has_edge G p b q = (Graph {(p,b,q)} \<le> G)" |
|
269 unfolding has_edge_def graph_leq_def |
|
270 by (cases G) simp |
|
271 |
|
272 |
|
273 lemma Sup_graph_eq2: |
|
274 "(SUP n. G n) = Graph (\<Union>n. dest_graph (G n))" |
|
275 using Sup_graph_eq[of "\<lambda>n. dest_graph (G n)", simplified] |
|
276 by simp |
|
277 |
|
278 lemma in_SUP: |
|
279 "has_edge (SUP x. Gs x) p b q = (\<exists>x. has_edge (Gs x) p b q)" |
|
280 unfolding Sup_graph_eq2 has_edge_leq graph_leq_def |
|
281 by simp |
|
282 |
|
283 instance graph :: (type, monoid_mult) kleene_by_complete_lattice |
|
284 proof |
|
285 fix a b c :: "('a, 'b) graph" |
|
286 |
|
287 show "a \<le> b \<longleftrightarrow> a + b = b" unfolding graph_leq_def graph_plus_def |
|
288 by (cases a, cases b) auto |
|
289 |
|
290 from order_less_le show "a < b \<longleftrightarrow> a \<le> b \<and> a \<noteq> b" . |
|
291 |
|
292 show "a * star b * c = (SUP n. a * b ^ n * c)" |
|
293 unfolding graph_star_def |
|
294 by (rule graph_ext) (force simp:in_SUP in_grcomp) |
|
295 qed |
|
296 |
|
297 |
|
298 lemma in_star: |
|
299 "has_edge (star G) a x b = (\<exists>n. has_edge (G ^ n) a x b)" |
|
300 by (auto simp:graph_star_def in_SUP) |
|
301 |
|
302 lemma tcl_is_SUP: |
|
303 "tcl (G::('a::type, 'b::monoid_mult) graph) = |
|
304 (SUP n. G ^ (Suc n))" |
|
305 unfolding tcl_def |
|
306 using star_cont[of 1 G G] |
|
307 by (simp add:power_Suc power_commutes) |
|
308 |
|
309 |
|
310 lemma in_tcl: |
|
311 "has_edge (tcl G) a x b = (\<exists>n>0. has_edge (G ^ n) a x b)" |
|
312 apply (auto simp: tcl_is_SUP in_SUP) |
|
313 apply (rule_tac x = "n - 1" in exI, auto) |
|
314 done |
|
315 |
|
316 |
|
317 subsection {* Infinite Paths *} |
|
318 |
|
319 types ('n, 'e) ipath = "('n \<times> 'e) sequence" |
|
320 |
|
321 definition has_ipath :: "('n, 'e) graph \<Rightarrow> ('n, 'e) ipath \<Rightarrow> bool" |
|
322 where |
|
323 "has_ipath G p = |
|
324 (\<forall>i. has_edge G (fst (p i)) (snd (p i)) (fst (p (Suc i))))" |
|
325 |
|
326 |
|
327 subsection {* Finite Paths *} |
|
328 |
|
329 types ('n, 'e) fpath = "('n \<times> ('e \<times> 'n) list)" |
|
330 |
|
331 inductive has_fpath :: "('n, 'e) graph \<Rightarrow> ('n, 'e) fpath \<Rightarrow> bool" |
|
332 for G :: "('n, 'e) graph" |
|
333 where |
|
334 has_fpath_empty: "has_fpath G (n, [])" |
|
335 | has_fpath_join: "\<lbrakk>G \<turnstile> n \<leadsto>\<^bsup>e\<^esup> n'; has_fpath G (n', es)\<rbrakk> \<Longrightarrow> has_fpath G (n, (e, n')#es)" |
|
336 |
|
337 definition |
|
338 "end_node p = |
|
339 (if snd p = [] then fst p else snd (snd p ! (length (snd p) - 1)))" |
|
340 |
|
341 definition path_nth :: "('n, 'e) fpath \<Rightarrow> nat \<Rightarrow> ('n \<times> 'e \<times> 'n)" |
|
342 where |
|
343 "path_nth p k = (if k = 0 then fst p else snd (snd p ! (k - 1)), snd p ! k)" |
|
344 |
|
345 lemma endnode_nth: |
|
346 assumes "length (snd p) = Suc k" |
|
347 shows "end_node p = snd (snd (path_nth p k))" |
|
348 using assms unfolding end_node_def path_nth_def |
|
349 by auto |
|
350 |
|
351 lemma path_nth_graph: |
|
352 assumes "k < length (snd p)" |
|
353 assumes "has_fpath G p" |
|
354 shows "(\<lambda>(n,e,n'). has_edge G n e n') (path_nth p k)" |
|
355 using assms |
|
356 proof (induct k arbitrary: p) |
|
357 case 0 thus ?case |
|
358 unfolding path_nth_def by (auto elim:has_fpath.cases) |
|
359 next |
|
360 case (Suc k p) |
|
361 |
|
362 from `has_fpath G p` show ?case |
|
363 proof (rule has_fpath.cases) |
|
364 case goal1 with Suc show ?case by simp |
|
365 next |
|
366 fix n e n' es |
|
367 assume st: "p = (n, (e, n') # es)" |
|
368 "G \<turnstile> n \<leadsto>\<^bsup>e\<^esup> n'" |
|
369 "has_fpath G (n', es)" |
|
370 with Suc |
|
371 have "(\<lambda>(n, b, a). G \<turnstile> n \<leadsto>\<^bsup>b\<^esup> a) (path_nth (n', es) k)" by simp |
|
372 with st show ?thesis by (cases k, auto simp:path_nth_def) |
|
373 qed |
|
374 qed |
|
375 |
|
376 lemma path_nth_connected: |
|
377 assumes "Suc k < length (snd p)" |
|
378 shows "fst (path_nth p (Suc k)) = snd (snd (path_nth p k))" |
|
379 using assms |
|
380 unfolding path_nth_def |
|
381 by auto |
|
382 |
|
383 definition path_loop :: "('n, 'e) fpath \<Rightarrow> ('n, 'e) ipath" ("omega") |
|
384 where |
|
385 "omega p \<equiv> (\<lambda>i. (\<lambda>(n,e,n'). (n,e)) (path_nth p (i mod (length (snd p)))))" |
|
386 |
|
387 lemma fst_p0: "fst (path_nth p 0) = fst p" |
|
388 unfolding path_nth_def by simp |
|
389 |
|
390 lemma path_loop_connect: |
|
391 assumes "fst p = end_node p" |
|
392 and "0 < length (snd p)" (is "0 < ?l") |
|
393 shows "fst (path_nth p (Suc i mod (length (snd p)))) |
|
394 = snd (snd (path_nth p (i mod length (snd p))))" |
|
395 (is "\<dots> = snd (snd (path_nth p ?k))") |
|
396 proof - |
|
397 from `0 < ?l` have "i mod ?l < ?l" (is "?k < ?l") |
|
398 by simp |
|
399 |
|
400 show ?thesis |
|
401 proof (cases "Suc ?k < ?l") |
|
402 case True |
|
403 hence "Suc ?k \<noteq> ?l" by simp |
|
404 with path_nth_connected[OF True] |
|
405 show ?thesis |
|
406 by (simp add:mod_Suc) |
|
407 next |
|
408 case False |
|
409 with `?k < ?l` have wrap: "Suc ?k = ?l" by simp |
|
410 |
|
411 hence "fst (path_nth p (Suc i mod ?l)) = fst (path_nth p 0)" |
|
412 by (simp add: mod_Suc) |
|
413 also from fst_p0 have "\<dots> = fst p" . |
|
414 also have "\<dots> = end_node p" by fact |
|
415 also have "\<dots> = snd (snd (path_nth p ?k))" |
|
416 by (auto simp: endnode_nth wrap) |
|
417 finally show ?thesis . |
|
418 qed |
|
419 qed |
|
420 |
|
421 lemma path_loop_graph: |
|
422 assumes "has_fpath G p" |
|
423 and loop: "fst p = end_node p" |
|
424 and nonempty: "0 < length (snd p)" (is "0 < ?l") |
|
425 shows "has_ipath G (omega p)" |
|
426 proof - |
|
427 { |
|
428 fix i |
|
429 from `0 < ?l` have "i mod ?l < ?l" (is "?k < ?l") |
|
430 by simp |
|
431 from this and `has_fpath G p` |
|
432 have pk_G: "(\<lambda>(n,e,n'). has_edge G n e n') (path_nth p ?k)" |
|
433 by (rule path_nth_graph) |
|
434 |
|
435 from path_loop_connect[OF loop nonempty] pk_G |
|
436 have "has_edge G (fst (omega p i)) (snd (omega p i)) (fst (omega p (Suc i)))" |
|
437 unfolding path_loop_def has_edge_def split_def |
|
438 by simp |
|
439 } |
|
440 then show ?thesis by (auto simp:has_ipath_def) |
|
441 qed |
|
442 |
|
443 definition prod :: "('n, 'e::monoid_mult) fpath \<Rightarrow> 'e" |
|
444 where |
|
445 "prod p = foldr (op *) (map fst (snd p)) 1" |
|
446 |
|
447 lemma prod_simps[simp]: |
|
448 "prod (n, []) = 1" |
|
449 "prod (n, (e,n')#es) = e * (prod (n',es))" |
|
450 unfolding prod_def |
|
451 by simp_all |
|
452 |
|
453 lemma power_induces_path: |
|
454 assumes a: "has_edge (A ^ k) n G m" |
|
455 obtains p |
|
456 where "has_fpath A p" |
|
457 and "n = fst p" "m = end_node p" |
|
458 and "G = prod p" |
|
459 and "k = length (snd p)" |
|
460 using a |
|
461 proof (induct k arbitrary:m n G thesis) |
|
462 case (0 m n G) |
|
463 let ?p = "(n, [])" |
|
464 from 0 have "has_fpath A ?p" "m = end_node ?p" "G = prod ?p" |
|
465 by (auto simp:in_grunit end_node_def intro:has_fpath.intros) |
|
466 thus ?case using 0 by (auto simp:end_node_def) |
|
467 next |
|
468 case (Suc k m n G) |
|
469 hence "has_edge (A * A ^ k) n G m" |
|
470 by (simp add:power_Suc power_commutes) |
|
471 then obtain G' H j where |
|
472 a_A: "has_edge A n G' j" |
|
473 and H_pow: "has_edge (A ^ k) j H m" |
|
474 and [simp]: "G = G' * H" |
|
475 by (auto simp:in_grcomp) |
|
476 |
|
477 from H_pow and Suc |
|
478 obtain p |
|
479 where p_path: "has_fpath A p" |
|
480 and [simp]: "j = fst p" "m = end_node p" "H = prod p" |
|
481 "k = length (snd p)" |
|
482 by blast |
|
483 |
|
484 let ?p' = "(n, (G', j)#snd p)" |
|
485 from a_A and p_path |
|
486 have "has_fpath A ?p'" "m = end_node ?p'" "G = prod ?p'" |
|
487 by (auto simp:end_node_def nth.simps intro:has_fpath.intros split:nat.split) |
|
488 thus ?case using Suc by auto |
|
489 qed |
|
490 |
|
491 |
|
492 subsection {* Sub-Paths *} |
|
493 |
|
494 definition sub_path :: "('n, 'e) ipath \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ('n, 'e) fpath" |
|
495 ("(_\<langle>_,_\<rangle>)") |
|
496 where |
|
497 "p\<langle>i,j\<rangle> = |
|
498 (fst (p i), map (\<lambda>k. (snd (p k), fst (p (Suc k)))) [i ..< j])" |
|
499 |
|
500 |
|
501 lemma sub_path_is_path: |
|
502 assumes ipath: "has_ipath G p" |
|
503 assumes l: "i \<le> j" |
|
504 shows "has_fpath G (p\<langle>i,j\<rangle>)" |
|
505 using l |
|
506 proof (induct i rule:inc_induct) |
|
507 case base show ?case by (auto simp:sub_path_def intro:has_fpath.intros) |
|
508 next |
|
509 case (step i) |
|
510 with ipath upt_rec[of i j] |
|
511 show ?case |
|
512 by (auto simp:sub_path_def has_ipath_def intro:has_fpath.intros) |
|
513 qed |
|
514 |
|
515 |
|
516 lemma sub_path_start[simp]: |
|
517 "fst (p\<langle>i,j\<rangle>) = fst (p i)" |
|
518 by (simp add:sub_path_def) |
|
519 |
|
520 lemma nth_upto[simp]: "k < j - i \<Longrightarrow> [i ..< j] ! k = i + k" |
|
521 by (induct k) auto |
|
522 |
|
523 lemma sub_path_end[simp]: |
|
524 "i < j \<Longrightarrow> end_node (p\<langle>i,j\<rangle>) = fst (p j)" |
|
525 by (auto simp:sub_path_def end_node_def) |
|
526 |
|
527 lemma foldr_map: "foldr f (map g xs) = foldr (f o g) xs" |
|
528 by (induct xs) auto |
|
529 |
|
530 lemma upto_append[simp]: |
|
531 assumes "i \<le> j" "j \<le> k" |
|
532 shows "[ i ..< j ] @ [j ..< k] = [i ..< k]" |
|
533 using assms and upt_add_eq_append[of i j "k - j"] |
|
534 by simp |
|
535 |
|
536 lemma foldr_monoid: "foldr (op *) xs 1 * foldr (op *) ys 1 |
|
537 = foldr (op *) (xs @ ys) (1::'a::monoid_mult)" |
|
538 by (induct xs) (auto simp:mult_assoc) |
|
539 |
|
540 lemma sub_path_prod: |
|
541 assumes "i < j" |
|
542 assumes "j < k" |
|
543 shows "prod (p\<langle>i,k\<rangle>) = prod (p\<langle>i,j\<rangle>) * prod (p\<langle>j,k\<rangle>)" |
|
544 using assms |
|
545 unfolding prod_def sub_path_def |
|
546 by (simp add:map_compose[symmetric] comp_def) |
|
547 (simp only:foldr_monoid map_append[symmetric] upto_append) |
|
548 |
|
549 |
|
550 lemma path_acgpow_aux: |
|
551 assumes "length es = l" |
|
552 assumes "has_fpath G (n,es)" |
|
553 shows "has_edge (G ^ l) n (prod (n,es)) (end_node (n,es))" |
|
554 using assms |
|
555 proof (induct l arbitrary:n es) |
|
556 case 0 thus ?case |
|
557 by (simp add:in_grunit end_node_def) |
|
558 next |
|
559 case (Suc l n es) |
|
560 hence "es \<noteq> []" by auto |
|
561 let ?n' = "snd (hd es)" |
|
562 let ?es' = "tl es" |
|
563 let ?e = "fst (hd es)" |
|
564 |
|
565 from Suc have len: "length ?es' = l" by auto |
|
566 |
|
567 from Suc |
|
568 have [simp]: "end_node (n, es) = end_node (?n', ?es')" |
|
569 by (cases es) (auto simp:end_node_def nth.simps split:nat.split) |
|
570 |
|
571 from `has_fpath G (n,es)` |
|
572 have "has_fpath G (?n', ?es')" |
|
573 by (rule has_fpath.cases) (auto intro:has_fpath.intros) |
|
574 with Suc len |
|
575 have "has_edge (G ^ l) ?n' (prod (?n', ?es')) (end_node (?n', ?es'))" |
|
576 by auto |
|
577 moreover |
|
578 from `es \<noteq> []` |
|
579 have "prod (n, es) = ?e * (prod (?n', ?es'))" |
|
580 by (cases es) auto |
|
581 moreover |
|
582 from `has_fpath G (n,es)` have c:"has_edge G n ?e ?n'" |
|
583 by (rule has_fpath.cases) (insert `es \<noteq> []`, auto) |
|
584 |
|
585 ultimately |
|
586 show ?case |
|
587 unfolding power_Suc |
|
588 by (auto simp:in_grcomp) |
|
589 qed |
|
590 |
|
591 |
|
592 lemma path_acgpow: |
|
593 "has_fpath G p |
|
594 \<Longrightarrow> has_edge (G ^ length (snd p)) (fst p) (prod p) (end_node p)" |
|
595 by (cases p) |
|
596 (rule path_acgpow_aux[of "snd p" "length (snd p)" _ "fst p", simplified]) |
|
597 |
|
598 |
|
599 lemma star_paths: |
|
600 "has_edge (star G) a x b = |
|
601 (\<exists>p. has_fpath G p \<and> a = fst p \<and> b = end_node p \<and> x = prod p)" |
|
602 proof |
|
603 assume "has_edge (star G) a x b" |
|
604 then obtain n where pow: "has_edge (G ^ n) a x b" |
|
605 by (auto simp:in_star) |
|
606 |
|
607 then obtain p where |
|
608 "has_fpath G p" "a = fst p" "b = end_node p" "x = prod p" |
|
609 by (rule power_induces_path) |
|
610 |
|
611 thus "\<exists>p. has_fpath G p \<and> a = fst p \<and> b = end_node p \<and> x = prod p" |
|
612 by blast |
|
613 next |
|
614 assume "\<exists>p. has_fpath G p \<and> a = fst p \<and> b = end_node p \<and> x = prod p" |
|
615 then obtain p where |
|
616 "has_fpath G p" "a = fst p" "b = end_node p" "x = prod p" |
|
617 by blast |
|
618 |
|
619 hence "has_edge (G ^ length (snd p)) a x b" |
|
620 by (auto intro:path_acgpow) |
|
621 |
|
622 thus "has_edge (star G) a x b" |
|
623 by (auto simp:in_star) |
|
624 qed |
|
625 |
|
626 |
|
627 lemma plus_paths: |
|
628 "has_edge (tcl G) a x b = |
|
629 (\<exists>p. has_fpath G p \<and> a = fst p \<and> b = end_node p \<and> x = prod p \<and> 0 < length (snd p))" |
|
630 proof |
|
631 assume "has_edge (tcl G) a x b" |
|
632 |
|
633 then obtain n where pow: "has_edge (G ^ n) a x b" and "0 < n" |
|
634 by (auto simp:in_tcl) |
|
635 |
|
636 from pow obtain p where |
|
637 "has_fpath G p" "a = fst p" "b = end_node p" "x = prod p" |
|
638 "n = length (snd p)" |
|
639 by (rule power_induces_path) |
|
640 |
|
641 with `0 < n` |
|
642 show "\<exists>p. has_fpath G p \<and> a = fst p \<and> b = end_node p \<and> x = prod p \<and> 0 < length (snd p) " |
|
643 by blast |
|
644 next |
|
645 assume "\<exists>p. has_fpath G p \<and> a = fst p \<and> b = end_node p \<and> x = prod p |
|
646 \<and> 0 < length (snd p)" |
|
647 then obtain p where |
|
648 "has_fpath G p" "a = fst p" "b = end_node p" "x = prod p" |
|
649 "0 < length (snd p)" |
|
650 by blast |
|
651 |
|
652 hence "has_edge (G ^ length (snd p)) a x b" |
|
653 by (auto intro:path_acgpow) |
|
654 |
|
655 with `0 < length (snd p)` |
|
656 show "has_edge (tcl G) a x b" |
|
657 by (auto simp:in_tcl) |
|
658 qed |
|
659 |
|
660 |
|
661 definition |
|
662 "contract s p = |
|
663 (\<lambda>i. (fst (p (s i)), prod (p\<langle>s i,s (Suc i)\<rangle>)))" |
|
664 |
|
665 lemma ipath_contract: |
|
666 assumes [simp]: "increasing s" |
|
667 assumes ipath: "has_ipath G p" |
|
668 shows "has_ipath (tcl G) (contract s p)" |
|
669 unfolding has_ipath_def |
|
670 proof |
|
671 fix i |
|
672 let ?p = "p\<langle>s i,s (Suc i)\<rangle>" |
|
673 |
|
674 from increasing_strict |
|
675 have "fst (p (s (Suc i))) = end_node ?p" by simp |
|
676 moreover |
|
677 from increasing_strict[of s i "Suc i"] have "snd ?p \<noteq> []" |
|
678 by (simp add:sub_path_def) |
|
679 moreover |
|
680 from ipath increasing_weak[of s] have "has_fpath G ?p" |
|
681 by (rule sub_path_is_path) auto |
|
682 ultimately |
|
683 show "has_edge (tcl G) |
|
684 (fst (contract s p i)) (snd (contract s p i)) (fst (contract s p (Suc i)))" |
|
685 unfolding contract_def plus_paths |
|
686 by (intro exI) auto |
|
687 qed |
|
688 |
|
689 lemma prod_unfold: |
|
690 "i < j \<Longrightarrow> prod (p\<langle>i,j\<rangle>) |
|
691 = snd (p i) * prod (p\<langle>Suc i, j\<rangle>)" |
|
692 unfolding prod_def |
|
693 by (simp add:sub_path_def upt_rec[of "i" j]) |
|
694 |
|
695 |
|
696 lemma sub_path_loop: |
|
697 assumes "0 < k" |
|
698 assumes k: "k = length (snd loop)" |
|
699 assumes loop: "fst loop = end_node loop" |
|
700 shows "(omega loop)\<langle>k * i,k * Suc i\<rangle> = loop" (is "?\<omega> = loop") |
|
701 proof (rule prod_eqI) |
|
702 show "fst ?\<omega> = fst loop" |
|
703 by (auto simp:path_loop_def path_nth_def split_def k) |
|
704 |
|
705 show "snd ?\<omega> = snd loop" |
|
706 proof (rule nth_equalityI[rule_format]) |
|
707 show leneq: "length (snd ?\<omega>) = length (snd loop)" |
|
708 unfolding sub_path_def k by simp |
|
709 |
|
710 fix j assume "j < length (snd (?\<omega>))" |
|
711 with leneq and k have "j < k" by simp |
|
712 |
|
713 have a: "\<And>i. fst (path_nth loop (Suc i mod k)) |
|
714 = snd (snd (path_nth loop (i mod k)))" |
|
715 unfolding k |
|
716 apply (rule path_loop_connect[OF loop]) |
|
717 using `0 < k` and k |
|
718 apply auto |
|
719 done |
|
720 |
|
721 from `j < k` |
|
722 show "snd ?\<omega> ! j = snd loop ! j" |
|
723 unfolding sub_path_def |
|
724 apply (simp add:path_loop_def split_def add_ac) |
|
725 apply (simp add:a k[symmetric]) |
|
726 apply (simp add:path_nth_def) |
|
727 done |
|
728 qed |
|
729 qed |
|
730 |
|
731 end |
|