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