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