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