[STATEMENT]
lemma map_eq_appendE:
  assumes "map f ls = fl@fl'"
  obtains l l' where "ls=l@l'" and "map f l=fl" and  "map f l' = fl'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l l'. \<lbrakk>ls = l @ l'; map f l = fl; map f l' = fl'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using that[of "take (length fl) ls" "drop (length fl) ls"] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>ls = take (length fl) ls @ drop (length fl) ls; map f (take (length fl) ls) = fl; map f (drop (length fl) ls) = fl'\<rbrakk> \<Longrightarrow> thesis
map f ls = fl @ fl'

goal (1 subgoal):
 1. (\<And>l l'. \<lbrakk>ls = l @ l'; map f l = fl; map f l' = fl'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(simp add: take_map[symmetric] drop_map[symmetric])


[STATEMENT]
lemma (in Graph) pathVertices_fwd:
    assumes "isPath u p v"
    shows "pathVertices u p = pathVertices_fwd u p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pathVertices u p = pathVertices_fwd u p
[PROOF STEP]
unfolding pathVertices_fwd_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pathVertices u p = u # map snd p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isPath u p v

goal (1 subgoal):
 1. pathVertices u p = u # map snd p
[PROOF STEP]
apply (induction p arbitrary: u)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>u. isPath u [] v \<Longrightarrow> pathVertices u [] = u # map snd []
 2. \<And>a p u. \<lbrakk>\<And>u. isPath u p v \<Longrightarrow> pathVertices u p = u # map snd p; isPath u (a # p) v\<rbrakk> \<Longrightarrow> pathVertices u (a # p) = u # map snd (a # p)
[PROOF STEP]
by auto


[STATEMENT]
lemma V_alt: "V = fst`E \<union> snd`E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V = fst ` E \<union> snd ` E
[PROOF STEP]
unfolding V_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {u. \<exists>v. (u, v) \<in> E \<or> (v, u) \<in> E} = fst ` E \<union> snd ` E
[PROOF STEP]
by force


[STATEMENT]
lemma E_ss_VxV: "E \<subseteq> V\<times>V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E \<subseteq> V \<times> V
[PROOF STEP]
by (auto simp: V_def)


[STATEMENT]
lemma adjacent_nodes_ss_V: "adjacent_nodes u \<subseteq> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjacent_nodes u \<subseteq> V
[PROOF STEP]
unfolding adjacent_nodes_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E `` {u} \<union> E\<inverse> `` {u} \<subseteq> V
[PROOF STEP]
using E_ss_VxV
[PROOF STATE]
proof (prove)
using this:
E \<subseteq> V \<times> V

goal (1 subgoal):
 1. E `` {u} \<union> E\<inverse> `` {u} \<subseteq> V
[PROOF STEP]
by auto


[STATEMENT]
lemma Vfin_imp_Efin[simp, intro]: assumes "finite V" shows "finite E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite E
[PROOF STEP]
using E_ss_VxV assms
[PROOF STATE]
proof (prove)
using this:
E \<subseteq> V \<times> V
finite V

goal (1 subgoal):
 1. finite E
[PROOF STEP]
by (auto intro: finite_subset)


[STATEMENT]
lemma Efin_imp_Vfin: "finite E \<Longrightarrow> finite V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite E \<Longrightarrow> finite V
[PROOF STEP]
unfolding V_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite E \<Longrightarrow> finite (fst ` E \<union> snd ` E)
[PROOF STEP]
by auto


[STATEMENT]
lemma zero_cap_simp[simp]: "(u,v)\<notin>E \<Longrightarrow> c (u,v) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u, v) \<notin> E \<Longrightarrow> c (u, v) = (0::'capacity)
[PROOF STEP]
by (auto simp: E_def)


[STATEMENT]
lemma succ_ss_V: "E``{u} \<subseteq> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E `` {u} \<subseteq> V
[PROOF STEP]
by (auto simp: V_def)


[STATEMENT]
lemma pred_ss_V: "E\<inverse>``{u} \<subseteq> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E\<inverse> `` {u} \<subseteq> V
[PROOF STEP]
by (auto simp: V_def)


[STATEMENT]
lemma
  incoming_edges: "incoming u \<subseteq> E" and
  outgoing_edges: "outgoing u \<subseteq> E" and
  incoming'_edges: "incoming' U \<subseteq> E" and
  outgoing'_edges: "outgoing' U \<subseteq> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (incoming u \<subseteq> E &&& outgoing u \<subseteq> E) &&& incoming' U \<subseteq> E &&& outgoing' U \<subseteq> E
[PROOF STEP]
by (auto simp: incoming_def outgoing_def incoming'_def outgoing'_def)


[STATEMENT]
lemma
  incoming_alt: "incoming u = (\<lambda>v. (v,u))`(E\<inverse>``{u})" and
  outgoing_alt: "outgoing u = Pair u`(E``{u})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. incoming u = (\<lambda>v. (v, u)) ` E\<inverse> `` {u} &&& outgoing u = Pair u ` E `` {u}
[PROOF STEP]
by (auto simp: incoming_def outgoing_def)


[STATEMENT]
lemma
  finite_incoming[simp, intro]: "finite V \<Longrightarrow> finite (incoming u)" and
  finite_outgoing[simp, intro]: "finite V \<Longrightarrow> finite (outgoing u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (finite V \<Longrightarrow> finite (incoming u)) &&& (finite V \<Longrightarrow> finite (outgoing u))
[PROOF STEP]
by (auto simp: incoming_alt outgoing_alt intro: finite_Image)


[STATEMENT]
lemma
  finite_incoming'[simp, intro]: "finite V \<Longrightarrow> finite (incoming' U)" and
  finite_outgoing'[simp, intro]: "finite V \<Longrightarrow> finite (outgoing' U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (finite V \<Longrightarrow> finite (incoming' U)) &&& (finite V \<Longrightarrow> finite (outgoing' U))
[PROOF STEP]
by (auto
    intro: finite_subset[OF incoming'_edges]
    intro: finite_subset[OF outgoing'_edges])


[STATEMENT]
lemma sum_outgoing_pointwise: "(\<Sum>e\<in>outgoing u. g e) = (\<Sum>v\<in>E``{u}. g (u,v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum g (outgoing u) = (\<Sum>v\<in>E `` {u}. g (u, v))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum g (outgoing u) = (\<Sum>v\<in>E `` {u}. g (u, v))
[PROOF STEP]
have "(\<Sum>e\<in>outgoing u. g e) = (\<Sum>e\<in>(\<lambda>v. (u,v))`(E``{u}). g e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum g (outgoing u) = sum g (Pair u ` E `` {u})
[PROOF STEP]
by (rule sum.cong) (auto simp: outgoing_def)
[PROOF STATE]
proof (state)
this:
sum g (outgoing u) = sum g (Pair u ` E `` {u})

goal (1 subgoal):
 1. sum g (outgoing u) = (\<Sum>v\<in>E `` {u}. g (u, v))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum g (outgoing u) = sum g (Pair u ` E `` {u})

goal (1 subgoal):
 1. sum g (outgoing u) = (\<Sum>v\<in>E `` {u}. g (u, v))
[PROOF STEP]
have "\<dots> = (\<Sum>v\<in>E``{u}. g (u,v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum g (Pair u ` E `` {u}) = (\<Sum>v\<in>E `` {u}. g (u, v))
[PROOF STEP]
by (subst sum.reindex)(auto simp add: inj_on_def)
[PROOF STATE]
proof (state)
this:
sum g (Pair u ` E `` {u}) = (\<Sum>v\<in>E `` {u}. g (u, v))

goal (1 subgoal):
 1. sum g (outgoing u) = (\<Sum>v\<in>E `` {u}. g (u, v))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sum g (outgoing u) = (\<Sum>v\<in>E `` {u}. g (u, v))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sum g (outgoing u) = (\<Sum>v\<in>E `` {u}. g (u, v))

goal (1 subgoal):
 1. sum g (outgoing u) = (\<Sum>v\<in>E `` {u}. g (u, v))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sum g (outgoing u) = (\<Sum>v\<in>E `` {u}. g (u, v))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum_incoming_pointwise: "(\<Sum>e\<in>incoming u. g e) = (\<Sum>v\<in>E\<inverse>``{u}. g (v,u))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum g (incoming u) = (\<Sum>v\<in>E\<inverse> `` {u}. g (v, u))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum g (incoming u) = (\<Sum>v\<in>E\<inverse> `` {u}. g (v, u))
[PROOF STEP]
have "(\<Sum>e\<in>incoming u. g e) = (\<Sum>e\<in>(\<lambda>v. (v,u))`(E\<inverse>``{u}). g e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum g (incoming u) = sum g ((\<lambda>v. (v, u)) ` E\<inverse> `` {u})
[PROOF STEP]
by (rule sum.cong) (auto simp: incoming_def)
[PROOF STATE]
proof (state)
this:
sum g (incoming u) = sum g ((\<lambda>v. (v, u)) ` E\<inverse> `` {u})

goal (1 subgoal):
 1. sum g (incoming u) = (\<Sum>v\<in>E\<inverse> `` {u}. g (v, u))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum g (incoming u) = sum g ((\<lambda>v. (v, u)) ` E\<inverse> `` {u})

goal (1 subgoal):
 1. sum g (incoming u) = (\<Sum>v\<in>E\<inverse> `` {u}. g (v, u))
[PROOF STEP]
have "\<dots> = (\<Sum>v\<in>E\<inverse>``{u}. g (v,u))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum g ((\<lambda>v. (v, u)) ` E\<inverse> `` {u}) = (\<Sum>v\<in>E\<inverse> `` {u}. g (v, u))
[PROOF STEP]
by (subst sum.reindex)(auto simp add: inj_on_def)
[PROOF STATE]
proof (state)
this:
sum g ((\<lambda>v. (v, u)) ` E\<inverse> `` {u}) = (\<Sum>v\<in>E\<inverse> `` {u}. g (v, u))

goal (1 subgoal):
 1. sum g (incoming u) = (\<Sum>v\<in>E\<inverse> `` {u}. g (v, u))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sum g (incoming u) = (\<Sum>v\<in>E\<inverse> `` {u}. g (v, u))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sum g (incoming u) = (\<Sum>v\<in>E\<inverse> `` {u}. g (v, u))

goal (1 subgoal):
 1. sum g (incoming u) = (\<Sum>v\<in>E\<inverse> `` {u}. g (v, u))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sum g (incoming u) = (\<Sum>v\<in>E\<inverse> `` {u}. g (v, u))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Finite_Graph) sum_incoming_extend:
  assumes "\<And>v. \<lbrakk> v\<in>V; (v,u)\<notin>E \<rbrakk> \<Longrightarrow> g (v,u) = 0"
  shows "(\<Sum>e\<in>incoming u. g e) = (\<Sum>v\<in>V. g (v,u))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum g (incoming u) = (\<Sum>v\<in>V. g (v, u))
[PROOF STEP]
apply (subst sum_incoming_pointwise)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>v\<in>E\<inverse> `` {u}. g (v, u)) = (\<Sum>v\<in>V. g (v, u))
[PROOF STEP]
apply (rule sum.mono_neutral_left)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. finite V
 2. E\<inverse> `` {u} \<subseteq> V
 3. \<forall>i\<in>V - E\<inverse> `` {u}. g (i, u) = (0::'b)
[PROOF STEP]
using assms pred_ss_V
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?v \<in> V; (?v, u) \<notin> E\<rbrakk> \<Longrightarrow> g (?v, u) = (0::'b)
E\<inverse> `` {?u} \<subseteq> V

goal (3 subgoals):
 1. finite V
 2. E\<inverse> `` {u} \<subseteq> V
 3. \<forall>i\<in>V - E\<inverse> `` {u}. g (i, u) = (0::'b)
[PROOF STEP]
by auto


[STATEMENT]
lemma (in Finite_Graph) sum_outgoing_extend:
  assumes "\<And>v. \<lbrakk> v\<in>V; (u,v)\<notin>E \<rbrakk> \<Longrightarrow> g (u,v) = 0"
  shows "(\<Sum>e\<in>outgoing u. g e) = (\<Sum>v\<in>V. g (u,v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum g (outgoing u) = (\<Sum>v\<in>V. g (u, v))
[PROOF STEP]
apply (subst sum_outgoing_pointwise)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>v\<in>E `` {u}. g (u, v)) = (\<Sum>v\<in>V. g (u, v))
[PROOF STEP]
apply (rule sum.mono_neutral_left)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. finite V
 2. E `` {u} \<subseteq> V
 3. \<forall>i\<in>V - E `` {u}. g (u, i) = (0::'b)
[PROOF STEP]
using assms succ_ss_V
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?v \<in> V; (u, ?v) \<notin> E\<rbrakk> \<Longrightarrow> g (u, ?v) = (0::'b)
E `` {?u} \<subseteq> V

goal (3 subgoals):
 1. finite V
 2. E `` {u} \<subseteq> V
 3. \<forall>i\<in>V - E `` {u}. g (u, i) = (0::'b)
[PROOF STEP]
by auto


[STATEMENT]
lemma (in Finite_Graph) sum_outgoing_alt: "\<lbrakk>\<forall>e. 0 \<le> g e \<and> g e \<le> c e\<rbrakk> \<Longrightarrow>
  \<forall>v \<in> V. (\<Sum>e \<in> outgoing v. g e) = (\<Sum>u \<in> V. g (v, u))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>e. (0::'a) \<le> g e \<and> g e \<le> c e \<Longrightarrow> \<forall>v\<in>V. sum g (outgoing v) = (\<Sum>u\<in>V. g (v, u))
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. \<lbrakk>\<forall>e. (0::'a) \<le> g e \<and> g e \<le> c e; v \<in> V\<rbrakk> \<Longrightarrow> sum g (outgoing v) = (\<Sum>u\<in>V. g (v, u))
[PROOF STEP]
apply (rule sum_outgoing_extend)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v u. \<lbrakk>\<forall>e. (0::'a) \<le> g e \<and> g e \<le> c e; v \<in> V; u \<in> V; (v, u) \<notin> E\<rbrakk> \<Longrightarrow> g (v, u) = (0::'a)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v u. \<lbrakk>\<forall>a b. (0::'a) \<le> g (a, b) \<and> g (a, b) \<le> c (a, b); v \<in> V; u \<in> V; (v, u) \<notin> E\<rbrakk> \<Longrightarrow> g (v, u) = (0::'a)
[PROOF STEP]
by (metis antisym zero_cap_simp)


[STATEMENT]
lemma (in Finite_Graph) sum_incoming_alt: "\<lbrakk>\<forall>e. 0 \<le> g e \<and> g e \<le> c e\<rbrakk> \<Longrightarrow>
  \<forall>v \<in> V. (\<Sum>e \<in> incoming v. g e) = (\<Sum>u \<in> V. g (u, v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>e. (0::'a) \<le> g e \<and> g e \<le> c e \<Longrightarrow> \<forall>v\<in>V. sum g (incoming v) = (\<Sum>u\<in>V. g (u, v))
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. \<lbrakk>\<forall>e. (0::'a) \<le> g e \<and> g e \<le> c e; v \<in> V\<rbrakk> \<Longrightarrow> sum g (incoming v) = (\<Sum>u\<in>V. g (u, v))
[PROOF STEP]
apply (rule sum_incoming_extend)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v u. \<lbrakk>\<forall>e. (0::'a) \<le> g e \<and> g e \<le> c e; v \<in> V; u \<in> V; (u, v) \<notin> E\<rbrakk> \<Longrightarrow> g (u, v) = (0::'a)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v u. \<lbrakk>\<forall>a b. (0::'a) \<le> g (a, b) \<and> g (a, b) \<le> c (a, b); v \<in> V; u \<in> V; (u, v) \<notin> E\<rbrakk> \<Longrightarrow> g (u, v) = (0::'a)
[PROOF STEP]
by (metis antisym zero_cap_simp)


[STATEMENT]
lemma (in Graph) Finite_Graph_EI: "finite E \<Longrightarrow> Finite_Graph c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite E \<Longrightarrow> Finite_Graph c
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite E \<Longrightarrow> finite V
[PROOF STEP]
by (rule Efin_imp_Vfin)


[STATEMENT]
lemma (in Finite_Graph) adjacent_nodes_finite[simp, intro!]: "finite (adjacent_nodes u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (adjacent_nodes u)
[PROOF STEP]
unfolding adjacent_nodes_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (E `` {u} \<union> E\<inverse> `` {u})
[PROOF STEP]
by (auto intro: finite_Image)


[STATEMENT]
lemma transfer_path:
  \<comment> \<open>Transfer path to another graph\<close>
  assumes "set p\<inter>E \<subseteq> Graph.E c'"
  assumes "isPath u p v"
  shows "Graph.isPath c' u p v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Graph.isPath c' u p v
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set p \<inter> E \<subseteq> Graph.E c'
isPath u p v

goal (1 subgoal):
 1. Graph.isPath c' u p v
[PROOF STEP]
apply (induction u p v rule: isPath.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>u v. \<lbrakk>set [] \<inter> E \<subseteq> Graph.E c'; isPath u [] v\<rbrakk> \<Longrightarrow> Graph.isPath c' u [] v
 2. \<And>u x y p v. \<lbrakk>\<lbrakk>set p \<inter> E \<subseteq> Graph.E c'; isPath y p v\<rbrakk> \<Longrightarrow> Graph.isPath c' y p v; set ((x, y) # p) \<inter> E \<subseteq> Graph.E c'; isPath u ((x, y) # p) v\<rbrakk> \<Longrightarrow> Graph.isPath c' u ((x, y) # p) v
[PROOF STEP]
apply (auto simp: Graph.isPath.simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma isPath_append[split_path_simps]:
  "isPath u (p1 @ p2) v \<longleftrightarrow> (\<exists>w. isPath u p1 w \<and> isPath w p2 v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isPath u (p1 @ p2) v = (\<exists>w. isPath u p1 w \<and> isPath w p2 v)
[PROOF STEP]
by (induction p1 arbitrary: u) auto


[STATEMENT]
lemma isPath_head[split_path_simps]:
  "isPath u (e#p) v \<longleftrightarrow> fst e = u \<and> e \<in> E \<and> isPath (snd e) p v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isPath u (e # p) v = (fst e = u \<and> e \<in> E \<and> isPath (snd e) p v)
[PROOF STEP]
by (cases e) auto


[STATEMENT]
lemma isPath_head2:
  "isPath u (e#p) v \<Longrightarrow> (p = [] \<or> (p \<noteq> [] \<and> fst (hd p) = snd e))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isPath u (e # p) v \<Longrightarrow> p = [] \<or> p \<noteq> [] \<and> fst (hd p) = snd e
[PROOF STEP]
by (metis Graph.isPath_head list.collapse)


[STATEMENT]
lemma isPath_tail:
  "isPath u (p@[e]) v \<longleftrightarrow> isPath u p (fst e) \<and> e \<in> E \<and> snd e = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isPath u (p @ [e]) v = (isPath u p (fst e) \<and> e \<in> E \<and> snd e = v)
[PROOF STEP]
by (induction p) (auto simp: isPath_append isPath_head)


[STATEMENT]
lemma isPath_tail2:
  "isPath u (p@[e]) v \<Longrightarrow> (p = [] \<or> (p \<noteq> [] \<and> snd (last p) = fst e))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isPath u (p @ [e]) v \<Longrightarrow> p = [] \<or> p \<noteq> [] \<and> snd (last p) = fst e
[PROOF STEP]
by (metis Graph.isPath_tail append_butlast_last_id)


[STATEMENT]
lemma isPath_append_edge:
  "isPath v p v' \<Longrightarrow> (v',v'')\<in>E \<Longrightarrow> isPath v (p@[(v',v'')]) v''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isPath v p v'; (v', v'') \<in> E\<rbrakk> \<Longrightarrow> isPath v (p @ [(v', v'')]) v''
[PROOF STEP]
by (auto simp: isPath_append)


[STATEMENT]
lemma isPath_edgeset: "\<lbrakk>isPath u p v; e \<in> set p\<rbrakk> \<Longrightarrow> e \<in> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isPath u p v; e \<in> set p\<rbrakk> \<Longrightarrow> e \<in> E
[PROOF STEP]
using E_def
[PROOF STATE]
proof (prove)
using this:
E \<equiv> {(u, v). c (u, v) \<noteq> (0::'capacity)}

goal (1 subgoal):
 1. \<lbrakk>isPath u p v; e \<in> set p\<rbrakk> \<Longrightarrow> e \<in> E
[PROOF STEP]
by (metis isPath_head isPath_append in_set_conv_decomp_first)


[STATEMENT]
lemma isPath_rtc: "isPath u p v \<Longrightarrow> (u, v) \<in> E\<^sup>*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isPath u p v \<Longrightarrow> (u, v) \<in> E\<^sup>*
[PROOF STEP]
proof (induction p arbitrary: u)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>u. isPath u [] v \<Longrightarrow> (u, v) \<in> E\<^sup>*
 2. \<And>a p u. \<lbrakk>\<And>u. isPath u p v \<Longrightarrow> (u, v) \<in> E\<^sup>*; isPath u (a # p) v\<rbrakk> \<Longrightarrow> (u, v) \<in> E\<^sup>*
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
isPath u [] v

goal (2 subgoals):
 1. \<And>u. isPath u [] v \<Longrightarrow> (u, v) \<in> E\<^sup>*
 2. \<And>a p u. \<lbrakk>\<And>u. isPath u p v \<Longrightarrow> (u, v) \<in> E\<^sup>*; isPath u (a # p) v\<rbrakk> \<Longrightarrow> (u, v) \<in> E\<^sup>*
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
isPath u [] v

goal (1 subgoal):
 1. (u, v) \<in> E\<^sup>*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(u, v) \<in> E\<^sup>*

goal (1 subgoal):
 1. \<And>a p u. \<lbrakk>\<And>u. isPath u p v \<Longrightarrow> (u, v) \<in> E\<^sup>*; isPath u (a # p) v\<rbrakk> \<Longrightarrow> (u, v) \<in> E\<^sup>*
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a p u. \<lbrakk>\<And>u. isPath u p v \<Longrightarrow> (u, v) \<in> E\<^sup>*; isPath u (a # p) v\<rbrakk> \<Longrightarrow> (u, v) \<in> E\<^sup>*
[PROOF STEP]
case (Cons e es)
[PROOF STATE]
proof (state)
this:
isPath ?u es v \<Longrightarrow> (?u, v) \<in> E\<^sup>*
isPath u (e # es) v

goal (1 subgoal):
 1. \<And>a p u. \<lbrakk>\<And>u. isPath u p v \<Longrightarrow> (u, v) \<in> E\<^sup>*; isPath u (a # p) v\<rbrakk> \<Longrightarrow> (u, v) \<in> E\<^sup>*
[PROOF STEP]
obtain u1 u2 where "e = (u1, u2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>u1 u2. e = (u1, u2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (cases e)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>u1 u2. e = (u1, u2) \<Longrightarrow> thesis; e = (a, b)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
e = (u1, u2)

goal (1 subgoal):
 1. \<And>a p u. \<lbrakk>\<And>u. isPath u p v \<Longrightarrow> (u, v) \<in> E\<^sup>*; isPath u (a # p) v\<rbrakk> \<Longrightarrow> (u, v) \<in> E\<^sup>*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e = (u1, u2)
[PROOF STEP]
have "u = u1 \<and> isPath u2 es v \<and> (u1, u2) \<in> E"
[PROOF STATE]
proof (prove)
using this:
e = (u1, u2)

goal (1 subgoal):
 1. u = u1 \<and> isPath u2 es v \<and> (u1, u2) \<in> E
[PROOF STEP]
using isPath.simps(2) Cons.prems
[PROOF STATE]
proof (prove)
using this:
e = (u1, u2)
isPath ?u ((?x, ?y) # ?p) ?v = (?u = ?x \<and> (?x, ?y) \<in> E \<and> isPath ?y ?p ?v)
isPath u (e # es) v

goal (1 subgoal):
 1. u = u1 \<and> isPath u2 es v \<and> (u1, u2) \<in> E
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u = u1 \<and> isPath u2 es v \<and> (u1, u2) \<in> E

goal (1 subgoal):
 1. \<And>a p u. \<lbrakk>\<And>u. isPath u p v \<Longrightarrow> (u, v) \<in> E\<^sup>*; isPath u (a # p) v\<rbrakk> \<Longrightarrow> (u, v) \<in> E\<^sup>*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u = u1 \<and> isPath u2 es v \<and> (u1, u2) \<in> E
[PROOF STEP]
have "(u, u2) \<in> E" and "(u2, v) \<in> E\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
u = u1 \<and> isPath u2 es v \<and> (u1, u2) \<in> E

goal (1 subgoal):
 1. (u, u2) \<in> E &&& (u2, v) \<in> E\<^sup>*
[PROOF STEP]
using Cons.IH
[PROOF STATE]
proof (prove)
using this:
u = u1 \<and> isPath u2 es v \<and> (u1, u2) \<in> E
isPath ?u es v \<Longrightarrow> (?u, v) \<in> E\<^sup>*

goal (1 subgoal):
 1. (u, u2) \<in> E &&& (u2, v) \<in> E\<^sup>*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(u, u2) \<in> E
(u2, v) \<in> E\<^sup>*

goal (1 subgoal):
 1. \<And>a p u. \<lbrakk>\<And>u. isPath u p v \<Longrightarrow> (u, v) \<in> E\<^sup>*; isPath u (a # p) v\<rbrakk> \<Longrightarrow> (u, v) \<in> E\<^sup>*
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(u, u2) \<in> E
(u2, v) \<in> E\<^sup>*

goal (1 subgoal):
 1. (u, v) \<in> E\<^sup>*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(u, v) \<in> E\<^sup>*

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rtc_isPath: "(u, v) \<in> E\<^sup>* \<Longrightarrow> (\<exists>p. isPath u p v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u, v) \<in> E\<^sup>* \<Longrightarrow> \<exists>p. isPath u p v
[PROOF STEP]
proof (induction rule: rtrancl.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a. \<exists>p. isPath a p a
 2. \<And>a b c. \<lbrakk>(a, b) \<in> E\<^sup>*; \<exists>p. isPath a p b; (b, c) \<in> E\<rbrakk> \<Longrightarrow> \<exists>p. isPath a p c
[PROOF STEP]
case (rtrancl_refl a)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>a. \<exists>p. isPath a p a
 2. \<And>a b c. \<lbrakk>(a, b) \<in> E\<^sup>*; \<exists>p. isPath a p b; (b, c) \<in> E\<rbrakk> \<Longrightarrow> \<exists>p. isPath a p c
[PROOF STEP]
have "isPath a [] a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isPath a [] a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
isPath a [] a

goal (2 subgoals):
 1. \<And>a. \<exists>p. isPath a p a
 2. \<And>a b c. \<lbrakk>(a, b) \<in> E\<^sup>*; \<exists>p. isPath a p b; (b, c) \<in> E\<rbrakk> \<Longrightarrow> \<exists>p. isPath a p c
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
isPath a [] a

goal (1 subgoal):
 1. \<exists>p. isPath a p a
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>p. isPath a p a

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>(a, b) \<in> E\<^sup>*; \<exists>p. isPath a p b; (b, c) \<in> E\<rbrakk> \<Longrightarrow> \<exists>p. isPath a p c
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>(a, b) \<in> E\<^sup>*; \<exists>p. isPath a p b; (b, c) \<in> E\<rbrakk> \<Longrightarrow> \<exists>p. isPath a p c
[PROOF STEP]
case (rtrancl_into_rtrancl u u' v)
[PROOF STATE]
proof (state)
this:
(u, u') \<in> E\<^sup>*
(u', v) \<in> E
\<exists>p. isPath u p u'

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>(a, b) \<in> E\<^sup>*; \<exists>p. isPath a p b; (b, c) \<in> E\<rbrakk> \<Longrightarrow> \<exists>p. isPath a p c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(u, u') \<in> E\<^sup>*
(u', v) \<in> E
\<exists>p. isPath u p u'
[PROOF STEP]
obtain p1 where "isPath u p1 u'"
[PROOF STATE]
proof (prove)
using this:
(u, u') \<in> E\<^sup>*
(u', v) \<in> E
\<exists>p. isPath u p u'

goal (1 subgoal):
 1. (\<And>p1. isPath u p1 u' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
isPath u p1 u'

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>(a, b) \<in> E\<^sup>*; \<exists>p. isPath a p b; (b, c) \<in> E\<rbrakk> \<Longrightarrow> \<exists>p. isPath a p c
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
isPath u p1 u'

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>(a, b) \<in> E\<^sup>*; \<exists>p. isPath a p b; (b, c) \<in> E\<rbrakk> \<Longrightarrow> \<exists>p. isPath a p c
[PROOF STEP]
have "(u', v) \<in> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u', v) \<in> E
[PROOF STEP]
using rtrancl_into_rtrancl.hyps(2)
[PROOF STATE]
proof (prove)
using this:
(u', v) \<in> E

goal (1 subgoal):
 1. (u', v) \<in> E
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(u', v) \<in> E

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>(a, b) \<in> E\<^sup>*; \<exists>p. isPath a p b; (b, c) \<in> E\<rbrakk> \<Longrightarrow> \<exists>p. isPath a p c
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
isPath u p1 u'
(u', v) \<in> E
[PROOF STEP]
have "isPath u (p1 @ [(u', v)]) v"
[PROOF STATE]
proof (prove)
using this:
isPath u p1 u'
(u', v) \<in> E

goal (1 subgoal):
 1. isPath u (p1 @ [(u', v)]) v
[PROOF STEP]
using isPath_tail
[PROOF STATE]
proof (prove)
using this:
isPath u p1 u'
(u', v) \<in> E
isPath ?u (?p @ [?e]) ?v = (isPath ?u ?p (fst ?e) \<and> ?e \<in> E \<and> snd ?e = ?v)

goal (1 subgoal):
 1. isPath u (p1 @ [(u', v)]) v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
isPath u (p1 @ [(u', v)]) v

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>(a, b) \<in> E\<^sup>*; \<exists>p. isPath a p b; (b, c) \<in> E\<rbrakk> \<Longrightarrow> \<exists>p. isPath a p c
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
isPath u (p1 @ [(u', v)]) v

goal (1 subgoal):
 1. \<exists>p. isPath u p v
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>p. isPath u p v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rtci_isPath: "(v, u) \<in> (E\<inverse>)\<^sup>* \<Longrightarrow> (\<exists>p. isPath u p v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v, u) \<in> (E\<inverse>)\<^sup>* \<Longrightarrow> \<exists>p. isPath u p v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (v, u) \<in> (E\<inverse>)\<^sup>* \<Longrightarrow> \<exists>p. isPath u p v
[PROOF STEP]
assume "(v,u)\<in>(E\<inverse>)\<^sup>*"
[PROOF STATE]
proof (state)
this:
(v, u) \<in> (E\<inverse>)\<^sup>*

goal (1 subgoal):
 1. (v, u) \<in> (E\<inverse>)\<^sup>* \<Longrightarrow> \<exists>p. isPath u p v
[PROOF STEP]
hence "(u,v)\<in>E\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
(v, u) \<in> (E\<inverse>)\<^sup>*

goal (1 subgoal):
 1. (u, v) \<in> E\<^sup>*
[PROOF STEP]
by (rule rtrancl_converseD)
[PROOF STATE]
proof (state)
this:
(u, v) \<in> E\<^sup>*

goal (1 subgoal):
 1. (v, u) \<in> (E\<inverse>)\<^sup>* \<Longrightarrow> \<exists>p. isPath u p v
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> E\<^sup>*

goal (1 subgoal):
 1. \<exists>p. isPath u p v
[PROOF STEP]
by (rule rtc_isPath)
[PROOF STATE]
proof (state)
this:
\<exists>p. isPath u p v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma isPath_ex_edge1:
  assumes "isPath u p v"
  assumes "(u1, v1) \<in> set p"
  assumes "u1 \<noteq> u"
  shows "\<exists>u2. (u2, u1) \<in> set p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>u2. (u2, u1) \<in> set p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>u2. (u2, u1) \<in> set p
[PROOF STEP]
obtain w1 w2 where obt1: "p = w1 @ [(u1, v1)] @ w2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>w1 w2. p = w1 @ [(u1, v1)] @ w2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
(u1, v1) \<in> set p

goal (1 subgoal):
 1. (\<And>w1 w2. p = w1 @ [(u1, v1)] @ w2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis append_Cons append_Nil in_set_conv_decomp_first)
[PROOF STATE]
proof (state)
this:
p = w1 @ [(u1, v1)] @ w2

goal (1 subgoal):
 1. \<exists>u2. (u2, u1) \<in> set p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = w1 @ [(u1, v1)] @ w2
[PROOF STEP]
have "isPath u w1 u1"
[PROOF STATE]
proof (prove)
using this:
p = w1 @ [(u1, v1)] @ w2

goal (1 subgoal):
 1. isPath u w1 u1
[PROOF STEP]
using assms(1) isPath_append
[PROOF STATE]
proof (prove)
using this:
p = w1 @ [(u1, v1)] @ w2
isPath u p v
isPath ?u (?p1.0 @ ?p2.0) ?v = (\<exists>w. isPath ?u ?p1.0 w \<and> isPath w ?p2.0 ?v)

goal (1 subgoal):
 1. isPath u w1 u1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
isPath u w1 u1

goal (1 subgoal):
 1. \<exists>u2. (u2, u1) \<in> set p
[PROOF STEP]
have "w1 \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w1 \<noteq> []
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> w1 \<noteq> [] \<Longrightarrow> False
[PROOF STEP]
assume "\<not> w1 \<noteq> []"
[PROOF STATE]
proof (state)
this:
\<not> w1 \<noteq> []

goal (1 subgoal):
 1. \<not> w1 \<noteq> [] \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> w1 \<noteq> []
[PROOF STEP]
have "u = u1"
[PROOF STATE]
proof (prove)
using this:
\<not> w1 \<noteq> []

goal (1 subgoal):
 1. u = u1
[PROOF STEP]
using \<open>isPath u w1 u1\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> w1 \<noteq> []
isPath u w1 u1

goal (1 subgoal):
 1. u = u1
[PROOF STEP]
by (metis isPath.simps(1))
[PROOF STATE]
proof (state)
this:
u = u1

goal (1 subgoal):
 1. \<not> w1 \<noteq> [] \<Longrightarrow> False
[PROOF STEP]
thus "False"
[PROOF STATE]
proof (prove)
using this:
u = u1

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
u = u1
u1 \<noteq> u

goal (1 subgoal):
 1. False
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
w1 \<noteq> []

goal (1 subgoal):
 1. \<exists>u2. (u2, u1) \<in> set p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w1 \<noteq> []
[PROOF STEP]
obtain e w1' where obt2:"w1 = w1' @ [e]"
[PROOF STATE]
proof (prove)
using this:
w1 \<noteq> []

goal (1 subgoal):
 1. (\<And>w1' e. w1 = w1' @ [e] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis append_butlast_last_id)
[PROOF STATE]
proof (state)
this:
w1 = w1' @ [e]

goal (1 subgoal):
 1. \<exists>u2. (u2, u1) \<in> set p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w1 = w1' @ [e]
[PROOF STEP]
obtain u2 where "e = (u2, u1)"
[PROOF STATE]
proof (prove)
using this:
w1 = w1' @ [e]

goal (1 subgoal):
 1. (\<And>u2. e = (u2, u1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>isPath u w1 u1\<close> isPath_tail
[PROOF STATE]
proof (prove)
using this:
w1 = w1' @ [e]
isPath u w1 u1
isPath ?u (?p @ [?e]) ?v = (isPath ?u ?p (fst ?e) \<and> ?e \<in> E \<and> snd ?e = ?v)

goal (1 subgoal):
 1. (\<And>u2. e = (u2, u1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod.collapse)
[PROOF STATE]
proof (state)
this:
e = (u2, u1)

goal (1 subgoal):
 1. \<exists>u2. (u2, u1) \<in> set p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e = (u2, u1)
[PROOF STEP]
have "p = w1' @ (u2, u1) # (u1, v1) # w2"
[PROOF STATE]
proof (prove)
using this:
e = (u2, u1)

goal (1 subgoal):
 1. p = w1' @ (u2, u1) # (u1, v1) # w2
[PROOF STEP]
using obt1 obt2
[PROOF STATE]
proof (prove)
using this:
e = (u2, u1)
p = w1 @ [(u1, v1)] @ w2
w1 = w1' @ [e]

goal (1 subgoal):
 1. p = w1' @ (u2, u1) # (u1, v1) # w2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = w1' @ (u2, u1) # (u1, v1) # w2

goal (1 subgoal):
 1. \<exists>u2. (u2, u1) \<in> set p
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p = w1' @ (u2, u1) # (u1, v1) # w2

goal (1 subgoal):
 1. \<exists>u2. (u2, u1) \<in> set p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>u2. (u2, u1) \<in> set p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma isPath_ex_edge2:
  assumes "isPath u p v"
  assumes "(u1, v1) \<in> set p"
  assumes "v1 \<noteq> v"
  shows "\<exists>v2. (v1, v2) \<in> set p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>v2. (v1, v2) \<in> set p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>v2. (v1, v2) \<in> set p
[PROOF STEP]
obtain w1 w2 where obt1: "p = w1 @ [(u1, v1)] @ w2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>w1 w2. p = w1 @ [(u1, v1)] @ w2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
(u1, v1) \<in> set p

goal (1 subgoal):
 1. (\<And>w1 w2. p = w1 @ [(u1, v1)] @ w2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis append_Cons append_Nil in_set_conv_decomp_first)
[PROOF STATE]
proof (state)
this:
p = w1 @ [(u1, v1)] @ w2

goal (1 subgoal):
 1. \<exists>v2. (v1, v2) \<in> set p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = w1 @ [(u1, v1)] @ w2
[PROOF STEP]
have "isPath v1 w2 v"
[PROOF STATE]
proof (prove)
using this:
p = w1 @ [(u1, v1)] @ w2

goal (1 subgoal):
 1. isPath v1 w2 v
[PROOF STEP]
using assms(1) isPath_append
[PROOF STATE]
proof (prove)
using this:
p = w1 @ [(u1, v1)] @ w2
isPath u p v
isPath ?u (?p1.0 @ ?p2.0) ?v = (\<exists>w. isPath ?u ?p1.0 w \<and> isPath w ?p2.0 ?v)

goal (1 subgoal):
 1. isPath v1 w2 v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
isPath v1 w2 v

goal (1 subgoal):
 1. \<exists>v2. (v1, v2) \<in> set p
[PROOF STEP]
have "w2 \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w2 \<noteq> []
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> w2 \<noteq> [] \<Longrightarrow> False
[PROOF STEP]
assume "\<not> w2 \<noteq> []"
[PROOF STATE]
proof (state)
this:
\<not> w2 \<noteq> []

goal (1 subgoal):
 1. \<not> w2 \<noteq> [] \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> w2 \<noteq> []
[PROOF STEP]
have "v = v1"
[PROOF STATE]
proof (prove)
using this:
\<not> w2 \<noteq> []

goal (1 subgoal):
 1. v = v1
[PROOF STEP]
using \<open>isPath v1 w2 v\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> w2 \<noteq> []
isPath v1 w2 v

goal (1 subgoal):
 1. v = v1
[PROOF STEP]
by (metis isPath.simps(1))
[PROOF STATE]
proof (state)
this:
v = v1

goal (1 subgoal):
 1. \<not> w2 \<noteq> [] \<Longrightarrow> False
[PROOF STEP]
thus "False"
[PROOF STATE]
proof (prove)
using this:
v = v1

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
v = v1
v1 \<noteq> v

goal (1 subgoal):
 1. False
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
w2 \<noteq> []

goal (1 subgoal):
 1. \<exists>v2. (v1, v2) \<in> set p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w2 \<noteq> []
[PROOF STEP]
obtain e w2' where obt2:"w2 =  e # w2'"
[PROOF STATE]
proof (prove)
using this:
w2 \<noteq> []

goal (1 subgoal):
 1. (\<And>e w2'. w2 = e # w2' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis neq_Nil_conv)
[PROOF STATE]
proof (state)
this:
w2 = e # w2'

goal (1 subgoal):
 1. \<exists>v2. (v1, v2) \<in> set p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w2 = e # w2'
[PROOF STEP]
obtain v2 where "e = (v1, v2)"
[PROOF STATE]
proof (prove)
using this:
w2 = e # w2'

goal (1 subgoal):
 1. (\<And>v2. e = (v1, v2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>isPath v1 w2 v\<close> isPath_head
[PROOF STATE]
proof (prove)
using this:
w2 = e # w2'
isPath v1 w2 v
isPath ?u (?e # ?p) ?v = (fst ?e = ?u \<and> ?e \<in> E \<and> isPath (snd ?e) ?p ?v)

goal (1 subgoal):
 1. (\<And>v2. e = (v1, v2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod.collapse)
[PROOF STATE]
proof (state)
this:
e = (v1, v2)

goal (1 subgoal):
 1. \<exists>v2. (v1, v2) \<in> set p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e = (v1, v2)
[PROOF STEP]
have "p = w1 @ (u1, v1) # (v1, v2) # w2'"
[PROOF STATE]
proof (prove)
using this:
e = (v1, v2)

goal (1 subgoal):
 1. p = w1 @ (u1, v1) # (v1, v2) # w2'
[PROOF STEP]
using obt1 obt2
[PROOF STATE]
proof (prove)
using this:
e = (v1, v2)
p = w1 @ [(u1, v1)] @ w2
w2 = e # w2'

goal (1 subgoal):
 1. p = w1 @ (u1, v1) # (v1, v2) # w2'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = w1 @ (u1, v1) # (v1, v2) # w2'

goal (1 subgoal):
 1. \<exists>v2. (v1, v2) \<in> set p
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p = w1 @ (u1, v1) # (v1, v2) # w2'

goal (1 subgoal):
 1. \<exists>v2. (v1, v2) \<in> set p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>v2. (v1, v2) \<in> set p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Graph) pathVertices_fwd_simps[simp]:
  "pathVertices_fwd s ([]) = [s]"
  "pathVertices_fwd s (e#p) = s#pathVertices_fwd (snd e) p"
  "pathVertices_fwd s (p@[e]) = pathVertices_fwd s p@[snd e]"
  "pathVertices_fwd s (p1@e#p2)
    = pathVertices_fwd s p1 @ pathVertices_fwd (snd e) p2"
  "s\<in>set (pathVertices_fwd s p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pathVertices_fwd s [] = [s] &&& pathVertices_fwd s (e # p) = s # pathVertices_fwd (snd e) p) &&& pathVertices_fwd s (p @ [e]) = pathVertices_fwd s p @ [snd e] &&& pathVertices_fwd s (p1 @ e # p2) = pathVertices_fwd s p1 @ pathVertices_fwd (snd e) p2 &&& s \<in> set (pathVertices_fwd s p)
[PROOF STEP]
by (auto simp: pathVertices_fwd_def)


[STATEMENT]
lemma pathVertices_alt: "p \<noteq> []
    \<Longrightarrow> pathVertices u p = map fst p @ [snd (last p)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> pathVertices u p = map fst p @ [snd (last p)]
[PROOF STEP]
by (induction p arbitrary: u) auto


[STATEMENT]
lemma pathVertices_singleton_iff[simp]: "pathVertices s p = [u] \<longleftrightarrow> (p=[] \<and> s=u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pathVertices s p = [u]) = (p = [] \<and> s = u)
[PROOF STEP]
apply (cases p rule: rev_cases)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. p = [] \<Longrightarrow> (pathVertices s p = [u]) = (p = [] \<and> s = u)
 2. \<And>ys y. p = ys @ [y] \<Longrightarrow> (pathVertices s p = [u]) = (p = [] \<and> s = u)
[PROOF STEP]
apply (auto simp: pathVertices_alt)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma length_pathVertices_eq[simp]: "length (pathVertices u p) = length p + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (pathVertices u p) = length p + 1
[PROOF STEP]
apply (cases "p=[]")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. p = [] \<Longrightarrow> length (pathVertices u p) = length p + 1
 2. p \<noteq> [] \<Longrightarrow> length (pathVertices u p) = length p + 1
[PROOF STEP]
apply (auto simp: pathVertices_alt)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma pathVertices_edgeset: "\<lbrakk>u\<in>V; isPath u p v\<rbrakk> \<Longrightarrow> set (pathVertices u p) \<subseteq> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>u \<in> V; isPath u p v\<rbrakk> \<Longrightarrow> set (pathVertices u p) \<subseteq> V
[PROOF STEP]
apply (cases p rule: rev_cases; simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ys y. \<lbrakk>u \<in> V; isPath u (ys @ [y]) v; p = ys @ [y]\<rbrakk> \<Longrightarrow> set (pathVertices u (ys @ [y])) \<subseteq> V
[PROOF STEP]
using isPath_edgeset[of u p v]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>isPath u p v; ?e \<in> set p\<rbrakk> \<Longrightarrow> ?e \<in> E

goal (1 subgoal):
 1. \<And>ys y. \<lbrakk>u \<in> V; isPath u (ys @ [y]) v; p = ys @ [y]\<rbrakk> \<Longrightarrow> set (pathVertices u (ys @ [y])) \<subseteq> V
[PROOF STEP]
apply (fastforce simp: pathVertices_alt V_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma pathVertices_append: "pathVertices u (p1 @ p2) =
butlast (pathVertices u p1) @ pathVertices (last (pathVertices u p1)) p2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pathVertices u (p1 @ p2) = butlast (pathVertices u p1) @ pathVertices (last (pathVertices u p1)) p2
[PROOF STEP]
proof (induction p1 arbitrary: u)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>u. pathVertices u ([] @ p2) = butlast (pathVertices u []) @ pathVertices (last (pathVertices u [])) p2
 2. \<And>a p1 u. (\<And>u. pathVertices u (p1 @ p2) = butlast (pathVertices u p1) @ pathVertices (last (pathVertices u p1)) p2) \<Longrightarrow> pathVertices u ((a # p1) @ p2) = butlast (pathVertices u (a # p1)) @ pathVertices (last (pathVertices u (a # p1))) p2
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>u. pathVertices u ([] @ p2) = butlast (pathVertices u []) @ pathVertices (last (pathVertices u [])) p2
 2. \<And>a p1 u. (\<And>u. pathVertices u (p1 @ p2) = butlast (pathVertices u p1) @ pathVertices (last (pathVertices u p1)) p2) \<Longrightarrow> pathVertices u ((a # p1) @ p2) = butlast (pathVertices u (a # p1)) @ pathVertices (last (pathVertices u (a # p1))) p2
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pathVertices u ([] @ p2) = butlast (pathVertices u []) @ pathVertices (last (pathVertices u [])) p2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pathVertices u ([] @ p2) = butlast (pathVertices u []) @ pathVertices (last (pathVertices u [])) p2

goal (1 subgoal):
 1. \<And>a p1 u. (\<And>u. pathVertices u (p1 @ p2) = butlast (pathVertices u p1) @ pathVertices (last (pathVertices u p1)) p2) \<Longrightarrow> pathVertices u ((a # p1) @ p2) = butlast (pathVertices u (a # p1)) @ pathVertices (last (pathVertices u (a # p1))) p2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a p1 u. (\<And>u. pathVertices u (p1 @ p2) = butlast (pathVertices u p1) @ pathVertices (last (pathVertices u p1)) p2) \<Longrightarrow> pathVertices u ((a # p1) @ p2) = butlast (pathVertices u (a # p1)) @ pathVertices (last (pathVertices u (a # p1))) p2
[PROOF STEP]
case (Cons e es)
[PROOF STATE]
proof (state)
this:
pathVertices ?u (es @ p2) = butlast (pathVertices ?u es) @ pathVertices (last (pathVertices ?u es)) p2

goal (1 subgoal):
 1. \<And>a p1 u. (\<And>u. pathVertices u (p1 @ p2) = butlast (pathVertices u p1) @ pathVertices (last (pathVertices u p1)) p2) \<Longrightarrow> pathVertices u ((a # p1) @ p2) = butlast (pathVertices u (a # p1)) @ pathVertices (last (pathVertices u (a # p1))) p2
[PROOF STEP]
have "pathVertices u ((e # es) @ p2) =  fst e # pathVertices (snd e) (es @ p2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pathVertices u ((e # es) @ p2) = fst e # pathVertices (snd e) (es @ p2)
[PROOF STEP]
by (metis Graph.pathVertices.simps(2) append_Cons)
[PROOF STATE]
proof (state)
this:
pathVertices u ((e # es) @ p2) = fst e # pathVertices (snd e) (es @ p2)

goal (1 subgoal):
 1. \<And>a p1 u. (\<And>u. pathVertices u (p1 @ p2) = butlast (pathVertices u p1) @ pathVertices (last (pathVertices u p1)) p2) \<Longrightarrow> pathVertices u ((a # p1) @ p2) = butlast (pathVertices u (a # p1)) @ pathVertices (last (pathVertices u (a # p1))) p2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
pathVertices u ((e # es) @ p2) = fst e # pathVertices (snd e) (es @ p2)

goal (1 subgoal):
 1. \<And>a p1 u. (\<And>u. pathVertices u (p1 @ p2) = butlast (pathVertices u p1) @ pathVertices (last (pathVertices u p1)) p2) \<Longrightarrow> pathVertices u ((a # p1) @ p2) = butlast (pathVertices u (a # p1)) @ pathVertices (last (pathVertices u (a # p1))) p2
[PROOF STEP]
have "pathVertices (snd e) (es @ p2)
    = butlast (pathVertices (snd e) es)
      @ pathVertices (last (pathVertices (snd e) es)) p2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pathVertices (snd e) (es @ p2) = butlast (pathVertices (snd e) es) @ pathVertices (last (pathVertices (snd e) es)) p2
[PROOF STEP]
using Cons.IH
[PROOF STATE]
proof (prove)
using this:
pathVertices ?u (es @ p2) = butlast (pathVertices ?u es) @ pathVertices (last (pathVertices ?u es)) p2

goal (1 subgoal):
 1. pathVertices (snd e) (es @ p2) = butlast (pathVertices (snd e) es) @ pathVertices (last (pathVertices (snd e) es)) p2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pathVertices (snd e) (es @ p2) = butlast (pathVertices (snd e) es) @ pathVertices (last (pathVertices (snd e) es)) p2

goal (1 subgoal):
 1. \<And>a p1 u. (\<And>u. pathVertices u (p1 @ p2) = butlast (pathVertices u p1) @ pathVertices (last (pathVertices u p1)) p2) \<Longrightarrow> pathVertices u ((a # p1) @ p2) = butlast (pathVertices u (a # p1)) @ pathVertices (last (pathVertices u (a # p1))) p2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
pathVertices (snd e) (es @ p2) = butlast (pathVertices (snd e) es) @ pathVertices (last (pathVertices (snd e) es)) p2

goal (1 subgoal):
 1. \<And>a p1 u. (\<And>u. pathVertices u (p1 @ p2) = butlast (pathVertices u p1) @ pathVertices (last (pathVertices u p1)) p2) \<Longrightarrow> pathVertices u ((a # p1) @ p2) = butlast (pathVertices u (a # p1)) @ pathVertices (last (pathVertices u (a # p1))) p2
[PROOF STEP]
have "fst e # butlast (pathVertices (snd e) es) =
    butlast (fst e # pathVertices (snd e) es)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst e # butlast (pathVertices (snd e) es) = butlast (fst e # pathVertices (snd e) es)
[PROOF STEP]
by (metis Graph.pathVertices.simps(1)
        Graph.pathVertices_alt Nil_is_append_conv butlast.simps(2)
        list.distinct(1))
[PROOF STATE]
proof (state)
this:
fst e # butlast (pathVertices (snd e) es) = butlast (fst e # pathVertices (snd e) es)

goal (1 subgoal):
 1. \<And>a p1 u. (\<And>u. pathVertices u (p1 @ p2) = butlast (pathVertices u p1) @ pathVertices (last (pathVertices u p1)) p2) \<Longrightarrow> pathVertices u ((a # p1) @ p2) = butlast (pathVertices u (a # p1)) @ pathVertices (last (pathVertices u (a # p1))) p2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
fst e # butlast (pathVertices (snd e) es) = butlast (fst e # pathVertices (snd e) es)

goal (1 subgoal):
 1. \<And>a p1 u. (\<And>u. pathVertices u (p1 @ p2) = butlast (pathVertices u p1) @ pathVertices (last (pathVertices u p1)) p2) \<Longrightarrow> pathVertices u ((a # p1) @ p2) = butlast (pathVertices u (a # p1)) @ pathVertices (last (pathVertices u (a # p1))) p2
[PROOF STEP]
have "fst e # pathVertices (snd e) es = pathVertices u (e # es)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst e # pathVertices (snd e) es = pathVertices u (e # es)
[PROOF STEP]
by (metis Graph.pathVertices.simps(2))
[PROOF STATE]
proof (state)
this:
fst e # pathVertices (snd e) es = pathVertices u (e # es)

goal (1 subgoal):
 1. \<And>a p1 u. (\<And>u. pathVertices u (p1 @ p2) = butlast (pathVertices u p1) @ pathVertices (last (pathVertices u p1)) p2) \<Longrightarrow> pathVertices u ((a # p1) @ p2) = butlast (pathVertices u (a # p1)) @ pathVertices (last (pathVertices u (a # p1))) p2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
fst e # pathVertices (snd e) es = pathVertices u (e # es)

goal (1 subgoal):
 1. \<And>a p1 u. (\<And>u. pathVertices u (p1 @ p2) = butlast (pathVertices u p1) @ pathVertices (last (pathVertices u p1)) p2) \<Longrightarrow> pathVertices u ((a # p1) @ p2) = butlast (pathVertices u (a # p1)) @ pathVertices (last (pathVertices u (a # p1))) p2
[PROOF STEP]
have "last (pathVertices (snd e) es) = last (pathVertices u (e # es))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. last (pathVertices (snd e) es) = last (pathVertices u (e # es))
[PROOF STEP]
by (metis Graph.pathVertices.simps(1) Graph.pathVertices_alt
    last.simps last_snoc list.distinct(1))
[PROOF STATE]
proof (state)
this:
last (pathVertices (snd e) es) = last (pathVertices u (e # es))

goal (1 subgoal):
 1. \<And>a p1 u. (\<And>u. pathVertices u (p1 @ p2) = butlast (pathVertices u p1) @ pathVertices (last (pathVertices u p1)) p2) \<Longrightarrow> pathVertices u ((a # p1) @ p2) = butlast (pathVertices u (a # p1)) @ pathVertices (last (pathVertices u (a # p1))) p2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
pathVertices u ((e # es) @ p2) = fst e # pathVertices (snd e) (es @ p2)
pathVertices (snd e) (es @ p2) = butlast (pathVertices (snd e) es) @ pathVertices (last (pathVertices (snd e) es)) p2
fst e # butlast (pathVertices (snd e) es) = butlast (fst e # pathVertices (snd e) es)
fst e # pathVertices (snd e) es = pathVertices u (e # es)
last (pathVertices (snd e) es) = last (pathVertices u (e # es))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
pathVertices u ((e # es) @ p2) = fst e # pathVertices (snd e) (es @ p2)
pathVertices (snd e) (es @ p2) = butlast (pathVertices (snd e) es) @ pathVertices (last (pathVertices (snd e) es)) p2
fst e # butlast (pathVertices (snd e) es) = butlast (fst e # pathVertices (snd e) es)
fst e # pathVertices (snd e) es = pathVertices u (e # es)
last (pathVertices (snd e) es) = last (pathVertices u (e # es))

goal (1 subgoal):
 1. pathVertices u ((e # es) @ p2) = butlast (pathVertices u (e # es)) @ pathVertices (last (pathVertices u (e # es))) p2
[PROOF STEP]
by (metis append_Cons)
[PROOF STATE]
proof (state)
this:
pathVertices u ((e # es) @ p2) = butlast (pathVertices u (e # es)) @ pathVertices (last (pathVertices u (e # es))) p2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma split_path_at_vertex:
  assumes "u\<in>set (pathVertices_fwd s p)"
  assumes "isPath s p t"
  obtains p1 p2 where "p=p1@p2" "isPath s p1 u" "isPath u p2 t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p1 p2. \<lbrakk>p = p1 @ p2; isPath s p1 u; isPath u p2 t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
u \<in> set (pathVertices_fwd s p)
isPath s p t

goal (1 subgoal):
 1. (\<And>p1 p2. \<lbrakk>p = p1 @ p2; isPath s p1 u; isPath u p2 t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>p1 p2. \<lbrakk>p = p1 @ p2; isPath s p1 u; isPath u p2 t\<rbrakk> \<Longrightarrow> thesis; u \<in> set (pathVertices_fwd s p); isPath s p t\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
(*unfolding pathVertices_fwd*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>p1 p2. \<lbrakk>p = p1 @ p2; isPath s p1 u; isPath u p2 t\<rbrakk> \<Longrightarrow> thesis; u \<in> set (pathVertices_fwd s p); isPath s p t\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
unfolding pathVertices_fwd_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>p1 p2. \<lbrakk>p = p1 @ p2; isPath s p1 u; isPath u p2 t\<rbrakk> \<Longrightarrow> thesis; u \<in> set (s # map snd p); isPath s p t\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (auto simp: in_set_conv_decomp isPath_append)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>p1 p2. \<lbrakk>p = p1 @ p2; isPath s p1 s; isPath s p2 t\<rbrakk> \<Longrightarrow> thesis; isPath s p t; u = s\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a ys zs. \<lbrakk>\<And>p1 p2. \<lbrakk>ys @ (a, u) # zs = p1 @ p2; isPath s p1 u; isPath u p2 t\<rbrakk> \<Longrightarrow> thesis; p = ys @ (a, u) # zs; isPath s ys a; (a, u) \<in> E; isPath u zs t\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a ys zs. \<lbrakk>\<And>p1 p2. \<lbrakk>ys @ (a, u) # zs = p1 @ p2; isPath s p1 u; isPath u p2 t\<rbrakk> \<Longrightarrow> thesis; p = ys @ (a, u) # zs; isPath s ys a; (a, u) \<in> E; isPath u zs t\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (metis Graph.isPath_append_edge append_Cons append_Nil append_assoc)


[STATEMENT]
lemma split_path_at_vertex_complete:
  assumes "isPath s p t" "pathVertices_fwd s p = pv1@u#pv2"
  obtains p1 p2 where
    "p=p1@p2"
    "isPath s p1 u" "pathVertices_fwd s p1 = pv1@[u]"
    "isPath u p2 t" "pathVertices_fwd u p2 = u#pv2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p1 p2. \<lbrakk>p = p1 @ p2; isPath s p1 u; pathVertices_fwd s p1 = pv1 @ [u]; isPath u p2 t; pathVertices_fwd u p2 = u # pv2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>p1 p2. \<lbrakk>p = p1 @ p2; isPath s p1 u; pathVertices_fwd s p1 = pv1 @ [u]; isPath u p2 t; pathVertices_fwd u p2 = u # pv2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
isPath s p t
pathVertices_fwd s p = pv1 @ u # pv2
[PROOF STEP]
have PV: "pathVertices s p = pv1@u#pv2"
[PROOF STATE]
proof (prove)
using this:
isPath s p t
pathVertices_fwd s p = pv1 @ u # pv2

goal (1 subgoal):
 1. pathVertices s p = pv1 @ u # pv2
[PROOF STEP]
by (simp add: pathVertices_fwd)
[PROOF STATE]
proof (state)
this:
pathVertices s p = pv1 @ u # pv2

goal (1 subgoal):
 1. (\<And>p1 p2. \<lbrakk>p = p1 @ p2; isPath s p1 u; pathVertices_fwd s p1 = pv1 @ [u]; isPath u p2 t; pathVertices_fwd u p2 = u # pv2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pathVertices s p = pv1 @ u # pv2
[PROOF STEP]
obtain p1 p2 where
    "p=p1@p2"
    "isPath s p1 u" "pathVertices s p1 = pv1@[u]"
    "isPath u p2 t" "pathVertices u p2 = u#pv2"
[PROOF STATE]
proof (prove)
using this:
pathVertices s p = pv1 @ u # pv2

goal (1 subgoal):
 1. (\<And>p1 p2. \<lbrakk>p = p1 @ p2; isPath s p1 u; pathVertices s p1 = pv1 @ [u]; isPath u p2 t; pathVertices u p2 = u # pv2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>p1 p2. \<lbrakk>p = p1 @ p2; isPath s p1 u; pathVertices s p1 = pv1 @ [u]; isPath u p2 t; pathVertices u p2 = u # pv2\<rbrakk> \<Longrightarrow> thesis; pathVertices s p = pv1 @ u # pv2\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
using assms(1) PV
[PROOF STATE]
proof (prove)
using this:
isPath s p t
pathVertices s p = pv1 @ u # pv2

goal (1 subgoal):
 1. thesis
[PROOF STEP]
apply (cases p rule: rev_cases; clarsimp simp: pathVertices_alt)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s = t; [t] = pv1 @ u # pv2; p = []\<rbrakk> \<Longrightarrow> thesis
 2. \<And>ys a b. \<lbrakk>isPath s (ys @ [(a, b)]) t; map fst ys @ [a, b] = pv1 @ u # pv2; p = ys @ [(a, b)]\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (rule that[of "[]" "[]"]; simp add: Cons_eq_append_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ys a b. \<lbrakk>isPath s (ys @ [(a, b)]) t; map fst ys @ [a, b] = pv1 @ u # pv2; p = ys @ [(a, b)]\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (cases pv2; clarsimp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ys a. \<lbrakk>isPath s (ys @ [(a, u)]) t; p = ys @ [(a, u)]; pv2 = []; pv1 = map fst ys @ [a]\<rbrakk> \<Longrightarrow> thesis
 2. \<And>ys a b aa list. \<lbrakk>isPath s (ys @ [(a, b)]) t; map fst ys @ [a, b] = pv1 @ u # aa # list; p = ys @ [(a, b)]; pv2 = aa # list\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (rule that[of p "[]"];
        auto simp add: isPath_append pathVertices_alt
      )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ys a b aa list. \<lbrakk>isPath s (ys @ [(a, b)]) t; map fst ys @ [a, b] = pv1 @ u # aa # list; p = ys @ [(a, b)]; pv2 = aa # list\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (clarsimp simp: append_eq_append_conv2;
        auto elim!: map_eq_appendE append_eq_Cons_conv[THEN iffD1, elim_format]
            simp: isPath_append)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>l. \<lbrakk>p = l @ [(u, t)]; pv2 = [t]; isPath s l u; (u, t) \<in> E; pv1 = map fst l\<rbrakk> \<Longrightarrow> thesis
 2. \<And>aa l. \<lbrakk>p = l @ [(u, aa), (aa, t)]; pv2 = [aa, t]; (aa, t) \<in> E; pv1 = map fst l; isPath s l u; (u, aa) \<in> E\<rbrakk> \<Longrightarrow> thesis
 3. \<And>a l b ba zsa. \<lbrakk>p = l @ (u, b) # (b, ba) # zsa @ [(a, t)]; pv2 = b # map fst zsa @ [a, t]; (a, t) \<in> E; pv1 = map fst l; isPath s l u; (u, b) \<in> E; (b, ba) \<in> E; isPath ba zsa a\<rbrakk> \<Longrightarrow> thesis
 4. \<And>ys a aa list us. \<lbrakk>p = ys @ [(a, t)]; pv2 = aa # list; isPath s ys a; (a, t) \<in> E; [a, t] = us @ u # aa # list; pv1 = map fst ys @ us\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
subgoal for \<dots> l
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p = l @ [(u, t)]; pv2 = [t]; isPath s l u; (u, t) \<in> E; pv1 = map fst l\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (erule that)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>pv2 = [t]; isPath s l u; (u, t) \<in> E; pv1 = map fst l\<rbrakk> \<Longrightarrow> isPath s l u
 2. \<lbrakk>pv2 = [t]; isPath s l u; (u, t) \<in> E; pv1 = map fst l\<rbrakk> \<Longrightarrow> pathVertices s l = pv1 @ [u]
 3. \<lbrakk>pv2 = [t]; isPath s l u; (u, t) \<in> E; pv1 = map fst l\<rbrakk> \<Longrightarrow> isPath u [(u, t)] t
 4. \<lbrakk>pv2 = [t]; isPath s l u; (u, t) \<in> E; pv1 = map fst l\<rbrakk> \<Longrightarrow> pathVertices u [(u, t)] = u # pv2
[PROOF STEP]
apply auto [4]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pv2 = [t]; isPath s l u; (u, t) \<in> E; pv1 = map fst l\<rbrakk> \<Longrightarrow> pathVertices s l = map fst l @ [u]
[PROOF STEP]
apply (case_tac l rule: rev_cases;
          auto simp add: pathVertices_alt isPath_append)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa l. \<lbrakk>p = l @ [(u, aa), (aa, t)]; pv2 = [aa, t]; (aa, t) \<in> E; pv1 = map fst l; isPath s l u; (u, aa) \<in> E\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a l b ba zsa. \<lbrakk>p = l @ (u, b) # (b, ba) # zsa @ [(a, t)]; pv2 = b # map fst zsa @ [a, t]; (a, t) \<in> E; pv1 = map fst l; isPath s l u; (u, b) \<in> E; (b, ba) \<in> E; isPath ba zsa a\<rbrakk> \<Longrightarrow> thesis
 3. \<And>ys a aa list us. \<lbrakk>p = ys @ [(a, t)]; pv2 = aa # list; isPath s ys a; (a, t) \<in> E; [a, t] = us @ u # aa # list; pv1 = map fst ys @ us\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
subgoal for \<dots> l
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p = l @ [(u, aa_), (aa_, t)]; pv2 = [aa_, t]; (aa_, t) \<in> E; pv1 = map fst l; isPath s l u; (u, aa_) \<in> E\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (erule that)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>pv2 = [aa_, t]; (aa_, t) \<in> E; pv1 = map fst l; isPath s l u; (u, aa_) \<in> E\<rbrakk> \<Longrightarrow> isPath s l u
 2. \<lbrakk>pv2 = [aa_, t]; (aa_, t) \<in> E; pv1 = map fst l; isPath s l u; (u, aa_) \<in> E\<rbrakk> \<Longrightarrow> pathVertices s l = pv1 @ [u]
 3. \<lbrakk>pv2 = [aa_, t]; (aa_, t) \<in> E; pv1 = map fst l; isPath s l u; (u, aa_) \<in> E\<rbrakk> \<Longrightarrow> isPath u [(u, aa_), (aa_, t)] t
 4. \<lbrakk>pv2 = [aa_, t]; (aa_, t) \<in> E; pv1 = map fst l; isPath s l u; (u, aa_) \<in> E\<rbrakk> \<Longrightarrow> pathVertices u [(u, aa_), (aa_, t)] = u # pv2
[PROOF STEP]
apply auto [4]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pv2 = [aa_, t]; (aa_, t) \<in> E; pv1 = map fst l; isPath s l u; (u, aa_) \<in> E\<rbrakk> \<Longrightarrow> pathVertices s l = map fst l @ [u]
[PROOF STEP]
apply (case_tac l rule: rev_cases;
          auto simp add: pathVertices_alt isPath_append)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a l b ba zsa. \<lbrakk>p = l @ (u, b) # (b, ba) # zsa @ [(a, t)]; pv2 = b # map fst zsa @ [a, t]; (a, t) \<in> E; pv1 = map fst l; isPath s l u; (u, b) \<in> E; (b, ba) \<in> E; isPath ba zsa a\<rbrakk> \<Longrightarrow> thesis
 2. \<And>ys a aa list us. \<lbrakk>p = ys @ [(a, t)]; pv2 = aa # list; isPath s ys a; (a, t) \<in> E; [a, t] = us @ u # aa # list; pv1 = map fst ys @ us\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
subgoal for \<dots> l u1 u2 u3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p = l @ (u, u1) # (u1, u2) # u3 @ [(a_, t)]; pv2 = u1 # map fst u3 @ [a_, t]; (a_, t) \<in> E; pv1 = map fst l; isPath s l u; (u, u1) \<in> E; (u1, u2) \<in> E; isPath u2 u3 a_\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (erule that)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>pv2 = u1 # map fst u3 @ [a_, t]; (a_, t) \<in> E; pv1 = map fst l; isPath s l u; (u, u1) \<in> E; (u1, u2) \<in> E; isPath u2 u3 a_\<rbrakk> \<Longrightarrow> isPath s l u
 2. \<lbrakk>pv2 = u1 # map fst u3 @ [a_, t]; (a_, t) \<in> E; pv1 = map fst l; isPath s l u; (u, u1) \<in> E; (u1, u2) \<in> E; isPath u2 u3 a_\<rbrakk> \<Longrightarrow> pathVertices s l = pv1 @ [u]
 3. \<lbrakk>pv2 = u1 # map fst u3 @ [a_, t]; (a_, t) \<in> E; pv1 = map fst l; isPath s l u; (u, u1) \<in> E; (u1, u2) \<in> E; isPath u2 u3 a_\<rbrakk> \<Longrightarrow> isPath u ((u, u1) # (u1, u2) # u3 @ [(a_, t)]) t
 4. \<lbrakk>pv2 = u1 # map fst u3 @ [a_, t]; (a_, t) \<in> E; pv1 = map fst l; isPath s l u; (u, u1) \<in> E; (u1, u2) \<in> E; isPath u2 u3 a_\<rbrakk> \<Longrightarrow> pathVertices u ((u, u1) # (u1, u2) # u3 @ [(a_, t)]) = u # pv2
[PROOF STEP]
apply auto [4]
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>pv2 = u1 # map fst u3 @ [a_, t]; (a_, t) \<in> E; pv1 = map fst l; isPath s l u; (u, u1) \<in> E; (u1, u2) \<in> E; isPath u2 u3 a_\<rbrakk> \<Longrightarrow> pathVertices s l = map fst l @ [u]
 2. \<lbrakk>pv2 = u1 # map fst u3 @ [a_, t]; (a_, t) \<in> E; pv1 = map fst l; isPath s l u; (u, u1) \<in> E; (u1, u2) \<in> E; isPath u2 u3 a_\<rbrakk> \<Longrightarrow> isPath u2 (u3 @ [(a_, t)]) t
 3. \<lbrakk>pv2 = u1 # map fst u3 @ [a_, t]; (a_, t) \<in> E; pv1 = map fst l; isPath s l u; (u, u1) \<in> E; (u1, u2) \<in> E; isPath u2 u3 a_\<rbrakk> \<Longrightarrow> pathVertices u2 (u3 @ [(a_, t)]) = map fst u3 @ [a_, t]
[PROOF STEP]
apply (case_tac l rule: rev_cases;
          auto simp add: pathVertices_alt isPath_append)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pv2 = u1 # map fst u3 @ [a_, t]; (a_, t) \<in> E; pv1 = map fst l; isPath s l u; (u, u1) \<in> E; (u1, u2) \<in> E; isPath u2 u3 a_\<rbrakk> \<Longrightarrow> isPath u2 (u3 @ [(a_, t)]) t
 2. \<lbrakk>pv2 = u1 # map fst u3 @ [a_, t]; (a_, t) \<in> E; pv1 = map fst l; isPath s l u; (u, u1) \<in> E; (u1, u2) \<in> E; isPath u2 u3 a_\<rbrakk> \<Longrightarrow> pathVertices u2 (u3 @ [(a_, t)]) = map fst u3 @ [a_, t]
[PROOF STEP]
apply (auto simp: isPath_append) []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pv2 = u1 # map fst u3 @ [a_, t]; (a_, t) \<in> E; pv1 = map fst l; isPath s l u; (u, u1) \<in> E; (u1, u2) \<in> E; isPath u2 u3 a_\<rbrakk> \<Longrightarrow> pathVertices u2 (u3 @ [(a_, t)]) = map fst u3 @ [a_, t]
[PROOF STEP]
apply (auto simp: pathVertices_alt) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ys a aa list us. \<lbrakk>p = ys @ [(a, t)]; pv2 = aa # list; isPath s ys a; (a, t) \<in> E; [a, t] = us @ u # aa # list; pv1 = map fst ys @ us\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (erule that)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>ys a aa list us. \<lbrakk>pv2 = aa # list; isPath s ys a; (a, t) \<in> E; [a, t] = us @ u # aa # list; pv1 = map fst ys @ us\<rbrakk> \<Longrightarrow> isPath s ys u
 2. \<And>ys a aa list us. \<lbrakk>pv2 = aa # list; isPath s ys a; (a, t) \<in> E; [a, t] = us @ u # aa # list; pv1 = map fst ys @ us\<rbrakk> \<Longrightarrow> pathVertices s ys = pv1 @ [u]
 3. \<And>ys a aa list us. \<lbrakk>pv2 = aa # list; isPath s ys a; (a, t) \<in> E; [a, t] = us @ u # aa # list; pv1 = map fst ys @ us\<rbrakk> \<Longrightarrow> isPath u [(a, t)] t
 4. \<And>ys a aa list us. \<lbrakk>pv2 = aa # list; isPath s ys a; (a, t) \<in> E; [a, t] = us @ u # aa # list; pv1 = map fst ys @ us\<rbrakk> \<Longrightarrow> pathVertices u [(a, t)] = u # pv2
[PROOF STEP]
apply(auto simp add: Cons_eq_append_conv) [4]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ys. \<lbrakk>pv2 = [t]; isPath s ys u; (u, t) \<in> E; pv1 = map fst ys\<rbrakk> \<Longrightarrow> pathVertices s ys = map fst ys @ [u]
[PROOF STEP]
subgoal for \<dots> l
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pv2 = [t]; isPath s l u; (u, t) \<in> E; pv1 = map fst l\<rbrakk> \<Longrightarrow> pathVertices s l = map fst l @ [u]
[PROOF STEP]
by (case_tac l rule: rev_cases;
            auto simp add: pathVertices_alt isPath_append)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
p = p1 @ p2
isPath s p1 u
pathVertices s p1 = pv1 @ [u]
isPath u p2 t
pathVertices u p2 = u # pv2

goal (1 subgoal):
 1. (\<And>p1 p2. \<lbrakk>p = p1 @ p2; isPath s p1 u; pathVertices_fwd s p1 = pv1 @ [u]; isPath u p2 t; pathVertices_fwd u p2 = u # pv2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p = p1 @ p2
isPath s p1 u
pathVertices s p1 = pv1 @ [u]
isPath u p2 t
pathVertices u p2 = u # pv2

goal (1 subgoal):
 1. thesis
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p = p1 @ p2; isPath s p1 u; pathVertices s p1 = pv1 @ [u]; isPath u p2 t; pathVertices u p2 = u # pv2\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
unfolding pathVertices_fwd
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p = p1 @ p2; isPath s p1 u; pathVertices_fwd s p1 = pv1 @ [u]; isPath u p2 t; pathVertices_fwd u p2 = u # pv2\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>p = ?p1.0 @ ?p2.0; isPath s ?p1.0 u; pathVertices_fwd s ?p1.0 = pv1 @ [u]; isPath u ?p2.0 t; pathVertices_fwd u ?p2.0 = u # pv2\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. \<lbrakk>p = p1 @ p2; isPath s p1 u; pathVertices_fwd s p1 = pv1 @ [u]; isPath u p2 t; pathVertices_fwd u p2 = u # pv2\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma isPath_fwd_cases:
  assumes "isPath s p t"
  obtains "p=[]" "t=s"
    | p' u where "p=(s,u)#p'" "(s,u)\<in>E" "isPath u p' t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>p = []; t = s\<rbrakk> \<Longrightarrow> thesis; \<And>u p'. \<lbrakk>p = (s, u) # p'; (s, u) \<in> E; isPath u p' t\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isPath s p t

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>p = []; t = s\<rbrakk> \<Longrightarrow> thesis; \<And>u p'. \<lbrakk>p = (s, u) # p'; (s, u) \<in> E; isPath u p' t\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (cases p) (auto)


[STATEMENT]
lemma isPath_bwd_cases:
  assumes "isPath s p t"
  obtains "p=[]" "t=s"
    | p' u where "p=p'@[(u,t)]" "isPath s p' u" "(u,t)\<in>E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>p = []; t = s\<rbrakk> \<Longrightarrow> thesis; \<And>p' u. \<lbrakk>p = p' @ [(u, t)]; isPath s p' u; (u, t) \<in> E\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isPath s p t

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>p = []; t = s\<rbrakk> \<Longrightarrow> thesis; \<And>p' u. \<lbrakk>p = p' @ [(u, t)]; isPath s p' u; (u, t) \<in> E\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (cases p rule: rev_cases) (auto simp: split_path_simps)


[STATEMENT]
lemma pathVertices_edge: "isPath s p t \<Longrightarrow> e \<in> set p \<Longrightarrow>
  \<exists>vs1 vs2. pathVertices_fwd s p = vs1 @ fst e # snd e # vs2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isPath s p t; e \<in> set p\<rbrakk> \<Longrightarrow> \<exists>vs1 vs2. pathVertices_fwd s p = vs1 @ fst e # snd e # vs2
[PROOF STEP]
apply (cases e)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>isPath s p t; e \<in> set p; e = (a, b)\<rbrakk> \<Longrightarrow> \<exists>vs1 vs2. pathVertices_fwd s p = vs1 @ fst e # snd e # vs2
[PROOF STEP]
apply (auto simp: in_set_conv_decomp split_path_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b ys zs. \<lbrakk>e = (a, b); p = ys @ (a, b) # zs; isPath s ys a; (a, b) \<in> E; isPath b zs t\<rbrakk> \<Longrightarrow> \<exists>vs1 vs2. pathVertices_fwd s ys @ pathVertices_fwd b zs = vs1 @ a # b # vs2
[PROOF STEP]
apply (erule isPath_bwd_cases[where s=s]; auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b zs. \<lbrakk>e = (s, b); p = (s, b) # zs; (s, b) \<in> E; isPath b zs t\<rbrakk> \<Longrightarrow> \<exists>vs1 vs2. s # pathVertices_fwd b zs = vs1 @ s # b # vs2
 2. \<And>a b zs p' u. \<lbrakk>e = (a, b); p = p' @ (u, a) # (a, b) # zs; (a, b) \<in> E; isPath b zs t; isPath s p' u; (u, a) \<in> E\<rbrakk> \<Longrightarrow> \<exists>vs1 vs2. pathVertices_fwd s p' @ a # pathVertices_fwd b zs = vs1 @ a # b # vs2
[PROOF STEP]
apply (erule isPath_fwd_cases[where t=t]; auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b zs p' u. \<lbrakk>e = (a, b); p = p' @ (u, a) # (a, b) # zs; (a, b) \<in> E; isPath b zs t; isPath s p' u; (u, a) \<in> E\<rbrakk> \<Longrightarrow> \<exists>vs1 vs2. pathVertices_fwd s p' @ a # pathVertices_fwd b zs = vs1 @ a # b # vs2
[PROOF STEP]
apply (erule isPath_fwd_cases[where t=t]; auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma pathVertices_edge_old: "isPath u p v \<Longrightarrow> e \<in> set p \<Longrightarrow>
  \<exists>vs1 vs2. pathVertices u p = vs1 @ fst e # snd e # vs2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isPath u p v; e \<in> set p\<rbrakk> \<Longrightarrow> \<exists>vs1 vs2. pathVertices u p = vs1 @ fst e # snd e # vs2
[PROOF STEP]
unfolding pathVertices_fwd
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isPath u p v; e \<in> set p\<rbrakk> \<Longrightarrow> \<exists>vs1 vs2. pathVertices_fwd u p = vs1 @ fst e # snd e # vs2
[PROOF STEP]
by (rule pathVertices_edge)


[STATEMENT]
lemma connected_refl[simp, intro!]: "connected v v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. connected v v
[PROOF STEP]
unfolding connected_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p. isPath v p v
[PROOF STEP]
by (force intro: exI[where x="[]"])


[STATEMENT]
lemma connected_append_edge: "connected u v \<Longrightarrow> (v,w)\<in>E \<Longrightarrow> connected u w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>connected u v; (v, w) \<in> E\<rbrakk> \<Longrightarrow> connected u w
[PROOF STEP]
unfolding connected_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>p. isPath u p v; (v, w) \<in> E\<rbrakk> \<Longrightarrow> \<exists>p. isPath u p w
[PROOF STEP]
by (auto intro: isPath_append_edge)


[STATEMENT]
lemma connected_inV_iff: "\<lbrakk>connected u v\<rbrakk> \<Longrightarrow> v\<in>V \<longleftrightarrow> u\<in>V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. connected u v \<Longrightarrow> (v \<in> V) = (u \<in> V)
[PROOF STEP]
apply (auto simp: connected_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>isPath u p v; v \<in> V\<rbrakk> \<Longrightarrow> u \<in> V
 2. \<And>p. \<lbrakk>isPath u p v; u \<in> V\<rbrakk> \<Longrightarrow> v \<in> V
[PROOF STEP]
apply (case_tac p; auto simp: V_def) []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>isPath u p v; u \<in> V\<rbrakk> \<Longrightarrow> v \<in> V
[PROOF STEP]
apply (case_tac p rule: rev_cases; auto simp: isPath_append V_def) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma connected_edgeRtc: "connected u v \<longleftrightarrow> (u, v) \<in> E\<^sup>*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. connected u v = ((u, v) \<in> E\<^sup>*)
[PROOF STEP]
using isPath_rtc rtc_isPath
[PROOF STATE]
proof (prove)
using this:
isPath ?u ?p ?v \<Longrightarrow> (?u, ?v) \<in> E\<^sup>*
(?u, ?v) \<in> E\<^sup>* \<Longrightarrow> \<exists>p. isPath ?u p ?v

goal (1 subgoal):
 1. connected u v = ((u, v) \<in> E\<^sup>*)
[PROOF STEP]
unfolding connected_def
[PROOF STATE]
proof (prove)
using this:
isPath ?u ?p ?v \<Longrightarrow> (?u, ?v) \<in> E\<^sup>*
(?u, ?v) \<in> E\<^sup>* \<Longrightarrow> \<exists>p. isPath ?u p ?v

goal (1 subgoal):
 1. (\<exists>p. isPath u p v) = ((u, v) \<in> E\<^sup>*)
[PROOF STEP]
by blast


[STATEMENT]
lemma reachable_ss_V: "s \<in> V \<Longrightarrow> reachableNodes s \<subseteq> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> V \<Longrightarrow> reachableNodes s \<subseteq> V
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>s \<in> V; x \<in> reachableNodes s\<rbrakk> \<Longrightarrow> x \<in> V
[PROOF STEP]
assume asm: "s \<in> V"
[PROOF STATE]
proof (state)
this:
s \<in> V

goal (1 subgoal):
 1. \<And>x. \<lbrakk>s \<in> V; x \<in> reachableNodes s\<rbrakk> \<Longrightarrow> x \<in> V
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>s \<in> V; x \<in> reachableNodes s\<rbrakk> \<Longrightarrow> x \<in> V
[PROOF STEP]
assume "x \<in> reachableNodes s"
[PROOF STATE]
proof (state)
this:
x \<in> reachableNodes s

goal (1 subgoal):
 1. \<And>x. \<lbrakk>s \<in> V; x \<in> reachableNodes s\<rbrakk> \<Longrightarrow> x \<in> V
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> reachableNodes s
[PROOF STEP]
obtain p where "x \<in> {v. isPath s p v}"
[PROOF STATE]
proof (prove)
using this:
x \<in> reachableNodes s

goal (1 subgoal):
 1. (\<And>p. x \<in> {v. isPath s p v} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding reachableNodes_def connected_def
[PROOF STATE]
proof (prove)
using this:
x \<in> {v. \<exists>p. isPath s p v}

goal (1 subgoal):
 1. (\<And>p. x \<in> {v. isPath s p v} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> {v. isPath s p v}

goal (1 subgoal):
 1. \<And>x. \<lbrakk>s \<in> V; x \<in> reachableNodes s\<rbrakk> \<Longrightarrow> x \<in> V
[PROOF STEP]
thus "x \<in> V"
[PROOF STATE]
proof (prove)
using this:
x \<in> {v. isPath s p v}

goal (1 subgoal):
 1. x \<in> V
[PROOF STEP]
using asm
[PROOF STATE]
proof (prove)
using this:
x \<in> {v. isPath s p v}
s \<in> V

goal (1 subgoal):
 1. x \<in> V
[PROOF STEP]
by (induction p arbitrary: s) (auto simp: isPath_head V_alt)
[PROOF STATE]
proof (state)
this:
x \<in> V

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reachableNodes_E_closed: "E``reachableNodes s \<subseteq> reachableNodes s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E `` reachableNodes s \<subseteq> reachableNodes s
[PROOF STEP]
unfolding reachableNodes_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E `` {v. connected s v} \<subseteq> {v. connected s v}
[PROOF STEP]
by (auto intro: connected_append_edge)


[STATEMENT]
lemma isSimplePath_fwd: "isSimplePath s p t
  \<longleftrightarrow> isPath s p t \<and> distinct (pathVertices_fwd s p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isSimplePath s p t = (isPath s p t \<and> distinct (pathVertices_fwd s p))
[PROOF STEP]
by (auto simp: isSimplePath_def pathVertices_fwd)


[STATEMENT]
lemma isSimplePath_singelton[split_path_simps]:
  "isSimplePath u [e] v \<longleftrightarrow> (e=(u,v) \<and> u\<noteq>v \<and> (u,v)\<in>E)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isSimplePath u [e] v = (e = (u, v) \<and> u \<noteq> v \<and> (u, v) \<in> E)
[PROOF STEP]
by (auto simp: isSimplePath_def isPath_head)


[STATEMENT]
lemma (in Graph) isSimplePath_append[split_path_simps]:
  "isSimplePath s (p1@p2) t
    \<longleftrightarrow> (\<exists>u.
      isSimplePath s p1 u
    \<and> isSimplePath u p2 t
    \<and> set (pathVertices_fwd s p1) \<inter> set (pathVertices_fwd u p2) = {u})"
  (is "_ \<longleftrightarrow> ?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isSimplePath s (p1 @ p2) t = (\<exists>u. isSimplePath s p1 u \<and> isSimplePath u p2 t \<and> set (pathVertices_fwd s p1) \<inter> set (pathVertices_fwd u p2) = {u})
[PROOF STEP]
unfolding isSimplePath_fwd
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (isPath s (p1 @ p2) t \<and> distinct (pathVertices_fwd s (p1 @ p2))) = (\<exists>u. (isPath s p1 u \<and> distinct (pathVertices_fwd s p1)) \<and> (isPath u p2 t \<and> distinct (pathVertices_fwd u p2)) \<and> set (pathVertices_fwd s p1) \<inter> set (pathVertices_fwd u p2) = {u})
[PROOF STEP]
apply (cases p1 rule: rev_cases; simp; cases p2; simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ys y. \<lbrakk>p1 = ys @ [y]; p2 = []\<rbrakk> \<Longrightarrow> (isPath s (ys @ [y]) t \<and> distinct (pathVertices_fwd s ys) \<and> snd y \<notin> set (pathVertices_fwd s ys)) = (isPath s (ys @ [y]) t \<and> distinct (pathVertices_fwd s ys) \<and> snd y \<notin> set (pathVertices_fwd s ys) \<and> insert (snd y) (set (pathVertices_fwd s ys)) \<inter> {t} = {t})
 2. \<And>ys y a list. \<lbrakk>p1 = ys @ [y]; p2 = a # list\<rbrakk> \<Longrightarrow> (isPath s (ys @ y # a # list) t \<and> distinct (pathVertices_fwd s ys) \<and> snd y \<notin> set (pathVertices_fwd (snd a) list) \<and> distinct (pathVertices_fwd (snd a) list) \<and> snd y \<notin> set (pathVertices_fwd s ys) \<and> set (pathVertices_fwd s ys) \<inter> set (pathVertices_fwd (snd a) list) = {}) = (\<exists>u. isPath s (ys @ [y]) u \<and> distinct (pathVertices_fwd s ys) \<and> snd y \<notin> set (pathVertices_fwd s ys) \<and> isPath u (a # list) t \<and> u \<notin> set (pathVertices_fwd (snd a) list) \<and> distinct (pathVertices_fwd (snd a) list) \<and> insert (snd y) (set (pathVertices_fwd s ys)) \<inter> insert u (set (pathVertices_fwd (snd a) list)) = {u})
[PROOF STEP]
by (auto simp: split_path_simps)


[STATEMENT]
lemma (in Graph) isSimplePath_cons[split_path_simps]:
  "isSimplePath s (e#p) t
  \<longleftrightarrow> (\<exists>u. e=(s,u) \<and> s\<noteq>u \<and> (s,u)\<in>E
        \<and> isSimplePath u p t \<and> s\<notin>set (pathVertices_fwd u p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isSimplePath s (e # p) t = (\<exists>u. e = (s, u) \<and> s \<noteq> u \<and> (s, u) \<in> E \<and> isSimplePath u p t \<and> s \<notin> set (pathVertices_fwd u p))
[PROOF STEP]
using isSimplePath_append[of s "[e]" p t, simplified]
[PROOF STATE]
proof (prove)
using this:
isSimplePath s (e # p) t = (\<exists>u. isSimplePath s [e] u \<and> isSimplePath u p t \<and> {s, snd e} \<inter> set (pathVertices_fwd u p) = {u})

goal (1 subgoal):
 1. isSimplePath s (e # p) t = (\<exists>u. e = (s, u) \<and> s \<noteq> u \<and> (s, u) \<in> E \<and> isSimplePath u p t \<and> s \<notin> set (pathVertices_fwd u p))
[PROOF STEP]
by (auto simp: split_path_simps)


[STATEMENT]
lemma (in Finite_Graph) simplePath_length_less_V:
  assumes UIV: "u\<in>V"
  assumes P: "isSimplePath u p v"
  shows "length p < card V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length p < card V
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length p < card V
[PROOF STEP]
from P
[PROOF STATE]
proof (chain)
picking this:
isSimplePath u p v
[PROOF STEP]
have 1: "isPath u p v" and 2: "distinct (pathVertices u p)"
[PROOF STATE]
proof (prove)
using this:
isSimplePath u p v

goal (1 subgoal):
 1. isPath u p v &&& distinct (pathVertices u p)
[PROOF STEP]
by (auto simp: isSimplePath_def)
[PROOF STATE]
proof (state)
this:
isPath u p v
distinct (pathVertices u p)

goal (1 subgoal):
 1. length p < card V
[PROOF STEP]
from pathVertices_edgeset[OF UIV 1]
[PROOF STATE]
proof (chain)
picking this:
set (pathVertices u p) \<subseteq> V
[PROOF STEP]
have "set (pathVertices u p) \<subseteq> V"
[PROOF STATE]
proof (prove)
using this:
set (pathVertices u p) \<subseteq> V

goal (1 subgoal):
 1. set (pathVertices u p) \<subseteq> V
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
set (pathVertices u p) \<subseteq> V

goal (1 subgoal):
 1. length p < card V
[PROOF STEP]
with 2 finite_V
[PROOF STATE]
proof (chain)
picking this:
distinct (pathVertices u p)
finite V
set (pathVertices u p) \<subseteq> V
[PROOF STEP]
have "length (pathVertices u p) \<le> card V"
[PROOF STATE]
proof (prove)
using this:
distinct (pathVertices u p)
finite V
set (pathVertices u p) \<subseteq> V

goal (1 subgoal):
 1. length (pathVertices u p) \<le> card V
[PROOF STEP]
using distinct_card card_mono
[PROOF STATE]
proof (prove)
using this:
distinct (pathVertices u p)
finite V
set (pathVertices u p) \<subseteq> V
distinct ?xs \<Longrightarrow> card (set ?xs) = length ?xs
\<lbrakk>finite ?B; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> card ?A \<le> card ?B

goal (1 subgoal):
 1. length (pathVertices u p) \<le> card V
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
length (pathVertices u p) \<le> card V

goal (1 subgoal):
 1. length p < card V
[PROOF STEP]
hence "length p + 1 \<le> card V"
[PROOF STATE]
proof (prove)
using this:
length (pathVertices u p) \<le> card V

goal (1 subgoal):
 1. length p + 1 \<le> card V
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length p + 1 \<le> card V

goal (1 subgoal):
 1. length p < card V
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
length p + 1 \<le> card V

goal (1 subgoal):
 1. length p < card V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length p < card V

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma split_simple_path: "isSimplePath u (p1@p2) v
  \<Longrightarrow> (\<exists>w. isSimplePath u p1 w \<and> isSimplePath w p2 v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isSimplePath u (p1 @ p2) v \<Longrightarrow> \<exists>w. isSimplePath u p1 w \<and> isSimplePath w p2 v
[PROOF STEP]
apply (auto simp: isSimplePath_def isPath_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>distinct (pathVertices u (p1 @ p2)); isPath u p1 w; isPath w p2 v\<rbrakk> \<Longrightarrow> \<exists>w. isPath u p1 w \<and> distinct (pathVertices u p1) \<and> isPath w p2 v \<and> distinct (pathVertices w p2)
[PROOF STEP]
apply (rule exI; intro conjI; assumption?)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>w. \<lbrakk>distinct (pathVertices u (p1 @ p2)); isPath u p1 w; isPath w p2 v\<rbrakk> \<Longrightarrow> distinct (pathVertices u p1)
 2. \<And>w. \<lbrakk>distinct (pathVertices u (p1 @ p2)); isPath u p1 w; isPath w p2 v\<rbrakk> \<Longrightarrow> distinct (pathVertices w p2)
[PROOF STEP]
apply (cases p1 rule: rev_cases) []
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>w. \<lbrakk>distinct (pathVertices u (p1 @ p2)); isPath u p1 w; isPath w p2 v; p1 = []\<rbrakk> \<Longrightarrow> distinct (pathVertices u p1)
 2. \<And>w ys y. \<lbrakk>distinct (pathVertices u (p1 @ p2)); isPath u p1 w; isPath w p2 v; p1 = ys @ [y]\<rbrakk> \<Longrightarrow> distinct (pathVertices u p1)
 3. \<And>w. \<lbrakk>distinct (pathVertices u (p1 @ p2)); isPath u p1 w; isPath w p2 v\<rbrakk> \<Longrightarrow> distinct (pathVertices w p2)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>w ys y. \<lbrakk>distinct (pathVertices u (p1 @ p2)); isPath u p1 w; isPath w p2 v; p1 = ys @ [y]\<rbrakk> \<Longrightarrow> distinct (pathVertices u p1)
 2. \<And>w. \<lbrakk>distinct (pathVertices u (p1 @ p2)); isPath u p1 w; isPath w p2 v\<rbrakk> \<Longrightarrow> distinct (pathVertices w p2)
[PROOF STEP]
apply (cases p2)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>w ys y. \<lbrakk>distinct (pathVertices u (p1 @ p2)); isPath u p1 w; isPath w p2 v; p1 = ys @ [y]; p2 = []\<rbrakk> \<Longrightarrow> distinct (pathVertices u p1)
 2. \<And>w ys y a list. \<lbrakk>distinct (pathVertices u (p1 @ p2)); isPath u p1 w; isPath w p2 v; p1 = ys @ [y]; p2 = a # list\<rbrakk> \<Longrightarrow> distinct (pathVertices u p1)
 3. \<And>w. \<lbrakk>distinct (pathVertices u (p1 @ p2)); isPath u p1 w; isPath w p2 v\<rbrakk> \<Longrightarrow> distinct (pathVertices w p2)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>w ys y a list. \<lbrakk>distinct (pathVertices u (p1 @ p2)); isPath u p1 w; isPath w p2 v; p1 = ys @ [y]; p2 = a # list\<rbrakk> \<Longrightarrow> distinct (pathVertices u p1)
 2. \<And>w. \<lbrakk>distinct (pathVertices u (p1 @ p2)); isPath u p1 w; isPath w p2 v\<rbrakk> \<Longrightarrow> distinct (pathVertices w p2)
[PROOF STEP]
apply (clarsimp simp: pathVertices_alt isPath_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>distinct (pathVertices u (p1 @ p2)); isPath u p1 w; isPath w p2 v\<rbrakk> \<Longrightarrow> distinct (pathVertices w p2)
[PROOF STEP]
apply (cases p1 rule: rev_cases) []
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>w. \<lbrakk>distinct (pathVertices u (p1 @ p2)); isPath u p1 w; isPath w p2 v; p1 = []\<rbrakk> \<Longrightarrow> distinct (pathVertices w p2)
 2. \<And>w ys y. \<lbrakk>distinct (pathVertices u (p1 @ p2)); isPath u p1 w; isPath w p2 v; p1 = ys @ [y]\<rbrakk> \<Longrightarrow> distinct (pathVertices w p2)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>w ys y. \<lbrakk>distinct (pathVertices u (p1 @ p2)); isPath u p1 w; isPath w p2 v; p1 = ys @ [y]\<rbrakk> \<Longrightarrow> distinct (pathVertices w p2)
[PROOF STEP]
apply (cases p2  rule: rev_cases)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>w ys y. \<lbrakk>distinct (pathVertices u (p1 @ p2)); isPath u p1 w; isPath w p2 v; p1 = ys @ [y]; p2 = []\<rbrakk> \<Longrightarrow> distinct (pathVertices w p2)
 2. \<And>w ys y ysa ya. \<lbrakk>distinct (pathVertices u (p1 @ p2)); isPath u p1 w; isPath w p2 v; p1 = ys @ [y]; p2 = ysa @ [ya]\<rbrakk> \<Longrightarrow> distinct (pathVertices w p2)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>w ys y ysa ya. \<lbrakk>distinct (pathVertices u (p1 @ p2)); isPath u p1 w; isPath w p2 v; p1 = ys @ [y]; p2 = ysa @ [ya]\<rbrakk> \<Longrightarrow> distinct (pathVertices w p2)
[PROOF STEP]
apply (clarsimp simp: pathVertices_alt isPath_append)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma simplePath_empty_conv[simp]: "isSimplePath s [] t \<longleftrightarrow> s=t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isSimplePath s [] t = (s = t)
[PROOF STEP]
by (auto simp: isSimplePath_def)


[STATEMENT]
lemma simplePath_same_conv[simp]: "isSimplePath s p s \<longleftrightarrow> p=[]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isSimplePath s p s = (p = [])
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. isSimplePath s p s \<Longrightarrow> p = []
 2. p = [] \<Longrightarrow> isSimplePath s p s
[PROOF STEP]
apply (cases p; simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>isSimplePath s (a # list) s; p = a # list\<rbrakk> \<Longrightarrow> False
 2. p = [] \<Longrightarrow> isSimplePath s p s
[PROOF STEP]
apply (rename_tac e pp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>e pp. \<lbrakk>isSimplePath s (e # pp) s; p = e # pp\<rbrakk> \<Longrightarrow> False
 2. p = [] \<Longrightarrow> isSimplePath s p s
[PROOF STEP]
apply (case_tac pp rule: rev_cases; simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>e pp. \<lbrakk>isSimplePath s [e] s; p = [e]; pp = []\<rbrakk> \<Longrightarrow> False
 2. \<And>e pp ys y. \<lbrakk>isSimplePath s (e # ys @ [y]) s; p = e # ys @ [y]; pp = ys @ [y]\<rbrakk> \<Longrightarrow> False
 3. p = [] \<Longrightarrow> isSimplePath s p s
[PROOF STEP]
apply (auto simp: isSimplePath_def pathVertices_alt isPath_append) [2]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = [] \<Longrightarrow> isSimplePath s p s
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma isSPath_pathLE: "isPath s p t \<Longrightarrow> \<exists>p'. isSimplePath s p' t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isPath s p t \<Longrightarrow> \<exists>p'. isSimplePath s p' t
[PROOF STEP]
proof (induction p rule: length_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> isPath s ys t \<longrightarrow> (\<exists>p'. isSimplePath s p' t); isPath s xs t\<rbrakk> \<Longrightarrow> \<exists>p'. isSimplePath s p' t
[PROOF STEP]
case (1 p)
[PROOF STATE]
proof (state)
this:
\<forall>ys. length ys < length p \<longrightarrow> isPath s ys t \<longrightarrow> (\<exists>p'. isSimplePath s p' t)
isPath s p t

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> isPath s ys t \<longrightarrow> (\<exists>p'. isSimplePath s p' t); isPath s xs t\<rbrakk> \<Longrightarrow> \<exists>p'. isSimplePath s p' t
[PROOF STEP]
hence IH: "\<And>p'. \<lbrakk>length p' < length p; isPath s p' t\<rbrakk>
    \<Longrightarrow> \<exists>p'. isSimplePath s p' t"
    and PATH: "isPath s p t"
[PROOF STATE]
proof (prove)
using this:
\<forall>ys. length ys < length p \<longrightarrow> isPath s ys t \<longrightarrow> (\<exists>p'. isSimplePath s p' t)
isPath s p t

goal (1 subgoal):
 1. (\<And>p'. \<lbrakk>length p' < length p; isPath s p' t\<rbrakk> \<Longrightarrow> \<exists>p'. isSimplePath s p' t) &&& isPath s p t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>length ?p' < length p; isPath s ?p' t\<rbrakk> \<Longrightarrow> \<exists>p'. isSimplePath s p' t
isPath s p t

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> isPath s ys t \<longrightarrow> (\<exists>p'. isSimplePath s p' t); isPath s xs t\<rbrakk> \<Longrightarrow> \<exists>p'. isSimplePath s p' t
[PROOF STEP]
show "\<exists>p. isSimplePath s p t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p. isSimplePath s p t
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>p. isSimplePath s p t
 2. \<not> ?P \<Longrightarrow> \<exists>p. isSimplePath s p t
[PROOF STEP]
assume "distinct (pathVertices_fwd s p)"
[PROOF STATE]
proof (state)
this:
distinct (pathVertices_fwd s p)

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>p. isSimplePath s p t
 2. \<not> ?P \<Longrightarrow> \<exists>p. isSimplePath s p t
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
distinct (pathVertices_fwd s p)

goal (1 subgoal):
 1. \<exists>p. isSimplePath s p t
[PROOF STEP]
using PATH
[PROOF STATE]
proof (prove)
using this:
distinct (pathVertices_fwd s p)
isPath s p t

goal (1 subgoal):
 1. \<exists>p. isSimplePath s p t
[PROOF STEP]
by (auto simp: isSimplePath_fwd)
[PROOF STATE]
proof (state)
this:
\<exists>p. isSimplePath s p t

goal (1 subgoal):
 1. \<not> distinct (pathVertices_fwd s p) \<Longrightarrow> \<exists>p. isSimplePath s p t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> distinct (pathVertices_fwd s p) \<Longrightarrow> \<exists>p. isSimplePath s p t
[PROOF STEP]
assume "\<not>(distinct (pathVertices_fwd s p))"
[PROOF STATE]
proof (state)
this:
\<not> distinct (pathVertices_fwd s p)

goal (1 subgoal):
 1. \<not> distinct (pathVertices_fwd s p) \<Longrightarrow> \<exists>p. isSimplePath s p t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> distinct (pathVertices_fwd s p)
[PROOF STEP]
obtain pv1 pv2 pv3 u where "pathVertices_fwd s p = pv1@u#pv2@u#pv3"
[PROOF STATE]
proof (prove)
using this:
\<not> distinct (pathVertices_fwd s p)

goal (1 subgoal):
 1. (\<And>pv1 u pv2 pv3. pathVertices_fwd s p = pv1 @ u # pv2 @ u # pv3 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto dest: not_distinct_decomp)
[PROOF STATE]
proof (state)
this:
pathVertices_fwd s p = pv1 @ u # pv2 @ u # pv3

goal (1 subgoal):
 1. \<not> distinct (pathVertices_fwd s p) \<Longrightarrow> \<exists>p. isSimplePath s p t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pathVertices_fwd s p = pv1 @ u # pv2 @ u # pv3
[PROOF STEP]
obtain p1 p2 p3 where
      "p = p1@p2@p3" "p2\<noteq>[]" "isPath s p1 u" "isPath u p3 t"
[PROOF STATE]
proof (prove)
using this:
pathVertices_fwd s p = pv1 @ u # pv2 @ u # pv3

goal (1 subgoal):
 1. (\<And>p1 p2 p3. \<lbrakk>p = p1 @ p2 @ p3; p2 \<noteq> []; isPath s p1 u; isPath u p3 t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using PATH
[PROOF STATE]
proof (prove)
using this:
pathVertices_fwd s p = pv1 @ u # pv2 @ u # pv3
isPath s p t

goal (1 subgoal):
 1. (\<And>p1 p2 p3. \<lbrakk>p = p1 @ p2 @ p3; p2 \<noteq> []; isPath s p1 u; isPath u p3 t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>p1 p2 p3. \<lbrakk>p = p1 @ p2 @ p3; p2 \<noteq> []; isPath s p1 u; isPath u p3 t\<rbrakk> \<Longrightarrow> thesis; pathVertices_fwd s p = pv1 @ u # pv2 @ u # pv3; isPath s p t\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (erule (1) split_path_at_vertex_complete[where s=s]; simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p1 p2. \<lbrakk>\<And>p1a p2a p3. \<lbrakk>p1 @ p2 = p1a @ p2a @ p3; p2a \<noteq> []; isPath s p1a u; isPath u p3 t\<rbrakk> \<Longrightarrow> thesis; pathVertices_fwd s (p1 @ p2) = pv1 @ u # pv2 @ u # pv3; p = p1 @ p2; isPath s p1 u; pathVertices_fwd s p1 = pv1 @ [u]; isPath u p2 t; pathVertices_fwd u p2 = u # pv2 @ u # pv3\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (erule split_path_at_vertex_complete[of _ _ t "u#pv2" u pv3]; simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p1 p2 p1a p2a. \<lbrakk>\<And>p1b p2 p3. \<lbrakk>p1 @ p1a @ p2a = p1b @ p2 @ p3; p2 \<noteq> []; isPath s p1b u; isPath u p3 t\<rbrakk> \<Longrightarrow> thesis; pathVertices_fwd s (p1 @ p1a @ p2a) = pv1 @ u # pv2 @ u # pv3; p = p1 @ p1a @ p2a; isPath s p1 u; pathVertices_fwd s p1 = pv1 @ [u]; pathVertices_fwd u (p1a @ p2a) = u # pv2 @ u # pv3; p2 = p1a @ p2a; isPath u p1a u; pathVertices_fwd u p1a = u # pv2 @ [u]; isPath u p2a t; pathVertices_fwd u p2a = u # pv3\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (auto intro: that)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
p = p1 @ p2 @ p3
p2 \<noteq> []
isPath s p1 u
isPath u p3 t

goal (1 subgoal):
 1. \<not> distinct (pathVertices_fwd s p) \<Longrightarrow> \<exists>p. isSimplePath s p t
[PROOF STEP]
hence "length (p1@p3) < length p" "isPath s (p1@p3) t"
[PROOF STATE]
proof (prove)
using this:
p = p1 @ p2 @ p3
p2 \<noteq> []
isPath s p1 u
isPath u p3 t

goal (1 subgoal):
 1. length (p1 @ p3) < length p &&& isPath s (p1 @ p3) t
[PROOF STEP]
by (auto simp: split_path_simps)
[PROOF STATE]
proof (state)
this:
length (p1 @ p3) < length p
isPath s (p1 @ p3) t

goal (1 subgoal):
 1. \<not> distinct (pathVertices_fwd s p) \<Longrightarrow> \<exists>p. isSimplePath s p t
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
length (p1 @ p3) < length p
isPath s (p1 @ p3) t

goal (1 subgoal):
 1. \<exists>p'. isSimplePath s p' t
[PROOF STEP]
by (rule IH)
[PROOF STATE]
proof (state)
this:
\<exists>p'. isSimplePath s p' t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>p. isSimplePath s p t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma isSPath_no_selfloop: "isSimplePath u p v \<Longrightarrow> (u1, u1) \<notin> set p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isSimplePath u p v \<Longrightarrow> (u1, u1) \<notin> set p
[PROOF STEP]
apply (rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isSimplePath u p v; \<not> (u1, u1) \<notin> set p\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (auto simp: in_set_conv_decomp split_path_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma isSPath_sg_outgoing: "\<lbrakk>isSimplePath u p v; (u1, v1) \<in> set p; v1 \<noteq> v2\<rbrakk>
  \<Longrightarrow> (u1, v2) \<notin> set p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isSimplePath u p v; (u1, v1) \<in> set p; v1 \<noteq> v2\<rbrakk> \<Longrightarrow> (u1, v2) \<notin> set p
[PROOF STEP]
by (auto simp: in_set_conv_decomp isSimplePath_def pathVertices_alt
      append_eq_append_conv2 Cons_eq_append_conv append_eq_Cons_conv)


[STATEMENT]
lemma isSPath_sg_incoming:
  "\<lbrakk>isSimplePath u p v; (u1, v1) \<in> set p; u1 \<noteq> u2\<rbrakk> \<Longrightarrow> (u2, v1) \<notin> set p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isSimplePath u p v; (u1, v1) \<in> set p; u1 \<noteq> u2\<rbrakk> \<Longrightarrow> (u2, v1) \<notin> set p
[PROOF STEP]
by (auto simp: in_set_conv_decomp isSimplePath_fwd pathVertices_fwd_def
      append_eq_append_conv2 append_eq_Cons_conv Cons_eq_append_conv)


[STATEMENT]
lemma isSPath_nt_parallel:
  assumes SP: "isSimplePath s p t"
  assumes EIP: "e\<in>set p"
  shows "prod.swap e \<notin> set p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod.swap e \<notin> set p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prod.swap e \<notin> set p
[PROOF STEP]
from SP
[PROOF STATE]
proof (chain)
picking this:
isSimplePath s p t
[PROOF STEP]
have P: "isPath s p t" and D: "distinct (pathVertices_fwd s p)"
[PROOF STATE]
proof (prove)
using this:
isSimplePath s p t

goal (1 subgoal):
 1. isPath s p t &&& distinct (pathVertices_fwd s p)
[PROOF STEP]
by (auto simp: isSimplePath_fwd)
[PROOF STATE]
proof (state)
this:
isPath s p t
distinct (pathVertices_fwd s p)

goal (1 subgoal):
 1. prod.swap e \<notin> set p
[PROOF STEP]
show "prod.swap e \<notin> set p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod.swap e \<notin> set p
[PROOF STEP]
apply (cases e)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. e = (a, b) \<Longrightarrow> prod.swap e \<notin> set p
[PROOF STEP]
using D EIP
[PROOF STATE]
proof (prove)
using this:
distinct (pathVertices_fwd s p)
e \<in> set p

goal (1 subgoal):
 1. \<And>a b. e = (a, b) \<Longrightarrow> prod.swap e \<notin> set p
[PROOF STEP]
by(auto dest!: pathVertices_edge[OF P] simp add: append_eq_append_conv2 Cons_eq_append_conv append_eq_Cons_conv)
[PROOF STATE]
proof (state)
this:
prod.swap e \<notin> set p

goal:
No subgoals!
[PROOF STEP]
qed