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