[STATEMENT]
lemma euler_imp_connected:
  assumes "euler_trail u p v" shows "connected G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Digraph_Component.connected G
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Digraph_Component.connected G
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Digraph_Component.connected G
[PROOF STEP]
have "verts G \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. verts G \<noteq> {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
euler_trail u p v

goal (1 subgoal):
 1. verts G \<noteq> {}
[PROOF STEP]
unfolding euler_trail_def trail_def
[PROOF STATE]
proof (prove)
using this:
(awalk u p v \<and> distinct p) \<and> set p = arcs G \<and> set (awalk_verts u p) = verts G

goal (1 subgoal):
 1. verts G \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
verts G \<noteq> {}

goal (1 subgoal):
 1. Digraph_Component.connected G
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
verts G \<noteq> {}

goal (1 subgoal):
 1. Digraph_Component.connected G
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
verts G \<noteq> {}

goal (1 subgoal):
 1. Digraph_Component.connected G
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
verts G \<noteq> {}

goal (1 subgoal):
 1. Digraph_Component.connected G
[PROOF STEP]
fix w1 w2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Digraph_Component.connected G
[PROOF STEP]
assume "w1 \<in> verts G" "w2 \<in> verts G"
[PROOF STATE]
proof (state)
this:
w1 \<in> verts G
w2 \<in> verts G

goal (1 subgoal):
 1. Digraph_Component.connected G
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w1 \<in> verts G
w2 \<in> verts G
[PROOF STEP]
have "awalk u p v " "w1 \<in> set (awalk_verts u p)" "w2 \<in> set (awalk_verts u p)"
[PROOF STATE]
proof (prove)
using this:
w1 \<in> verts G
w2 \<in> verts G

goal (1 subgoal):
 1. awalk u p v &&& w1 \<in> set (awalk_verts u p) &&& w2 \<in> set (awalk_verts u p)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
w1 \<in> verts G
w2 \<in> verts G
euler_trail u p v

goal (1 subgoal):
 1. awalk u p v &&& w1 \<in> set (awalk_verts u p) &&& w2 \<in> set (awalk_verts u p)
[PROOF STEP]
by (auto simp: euler_trail_def trail_def)
[PROOF STATE]
proof (state)
this:
awalk u p v
w1 \<in> set (awalk_verts u p)
w2 \<in> set (awalk_verts u p)

goal (1 subgoal):
 1. Digraph_Component.connected G
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
awalk u p v
w1 \<in> set (awalk_verts u p)
w2 \<in> set (awalk_verts u p)
[PROOF STEP]
have "w1 \<rightarrow>\<^sup>*\<^bsub>mk_symmetric G\<^esub> w2"
[PROOF STATE]
proof (prove)
using this:
awalk u p v
w1 \<in> set (awalk_verts u p)
w2 \<in> set (awalk_verts u p)

goal (1 subgoal):
 1. w1 \<rightarrow>\<^sup>*\<^bsub>with_proj (mk_symmetric G)\<^esub> w2
[PROOF STEP]
by (rule sym_reachableI_in_awalk)
[PROOF STATE]
proof (state)
this:
w1 \<rightarrow>\<^sup>*\<^bsub>with_proj (mk_symmetric G)\<^esub> w2

goal (1 subgoal):
 1. Digraph_Component.connected G
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?w1.4 \<in> verts G; ?w2.4 \<in> verts G\<rbrakk> \<Longrightarrow> ?w1.4 \<rightarrow>\<^sup>*\<^bsub>with_proj (mk_symmetric G)\<^esub> ?w2.4

goal (1 subgoal):
 1. Digraph_Component.connected G
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
verts G \<noteq> {}
\<lbrakk>?w1.4 \<in> verts G; ?w2.4 \<in> verts G\<rbrakk> \<Longrightarrow> ?w1.4 \<rightarrow>\<^sup>*\<^bsub>with_proj (mk_symmetric G)\<^esub> ?w2.4
[PROOF STEP]
show "connected G"
[PROOF STATE]
proof (prove)
using this:
verts G \<noteq> {}
\<lbrakk>?w1.4 \<in> verts G; ?w2.4 \<in> verts G\<rbrakk> \<Longrightarrow> ?w1.4 \<rightarrow>\<^sup>*\<^bsub>with_proj (mk_symmetric G)\<^esub> ?w2.4

goal (1 subgoal):
 1. Digraph_Component.connected G
[PROOF STEP]
by (rule connectedI)
[PROOF STATE]
proof (state)
this:
Digraph_Component.connected G

goal:
No subgoals!
[PROOF STEP]
qed