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