[STATEMENT]
lemma walk_edges_decomp_ss: "set (walk_edges (xs@[y]@zs)) \<subseteq> set (walk_edges (xs@[y]@ys@[y]@zs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (walk_edges (xs @ [y] @ zs)) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y] @ zs))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (walk_edges (xs @ [y] @ zs)) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y] @ zs))
[PROOF STEP]
have half_ss: "set (walk_edges (xs@[y])) \<subseteq> set (walk_edges (xs@[y]@ys@[y]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (walk_edges (xs @ [y])) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y]))
[PROOF STEP]
using walk_edges_append_ss2
[PROOF STATE]
proof (prove)
using this:
set (walk_edges ?xs) \<subseteq> set (walk_edges (?xs @ ?ys))

goal (1 subgoal):
 1. set (walk_edges (xs @ [y])) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y]))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
set (walk_edges (xs @ [y])) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y]))

goal (1 subgoal):
 1. set (walk_edges (xs @ [y] @ zs)) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y] @ zs))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
set (walk_edges (xs @ [y])) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y]))

goal (1 subgoal):
 1. set (walk_edges (xs @ [y] @ zs)) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y] @ zs))
[PROOF STEP]
proof (cases "zs = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>set (walk_edges (xs @ [y])) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y])); zs = []\<rbrakk> \<Longrightarrow> set (walk_edges (xs @ [y] @ zs)) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y] @ zs))
 2. \<lbrakk>set (walk_edges (xs @ [y])) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y])); zs \<noteq> []\<rbrakk> \<Longrightarrow> set (walk_edges (xs @ [y] @ zs)) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y] @ zs))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
zs = []

goal (2 subgoals):
 1. \<lbrakk>set (walk_edges (xs @ [y])) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y])); zs = []\<rbrakk> \<Longrightarrow> set (walk_edges (xs @ [y] @ zs)) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y] @ zs))
 2. \<lbrakk>set (walk_edges (xs @ [y])) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y])); zs \<noteq> []\<rbrakk> \<Longrightarrow> set (walk_edges (xs @ [y] @ zs)) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y] @ zs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
zs = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
zs = []

goal (1 subgoal):
 1. set (walk_edges (xs @ [y] @ zs)) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y] @ zs))
[PROOF STEP]
using half_ss
[PROOF STATE]
proof (prove)
using this:
zs = []
set (walk_edges (xs @ [y])) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y]))

goal (1 subgoal):
 1. set (walk_edges (xs @ [y] @ zs)) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y] @ zs))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (walk_edges (xs @ [y] @ zs)) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y] @ zs))

goal (1 subgoal):
 1. \<lbrakk>set (walk_edges (xs @ [y])) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y])); zs \<noteq> []\<rbrakk> \<Longrightarrow> set (walk_edges (xs @ [y] @ zs)) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y] @ zs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>set (walk_edges (xs @ [y])) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y])); zs \<noteq> []\<rbrakk> \<Longrightarrow> set (walk_edges (xs @ [y] @ zs)) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y] @ zs))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
zs \<noteq> []

goal (1 subgoal):
 1. \<lbrakk>set (walk_edges (xs @ [y])) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y])); zs \<noteq> []\<rbrakk> \<Longrightarrow> set (walk_edges (xs @ [y] @ zs)) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y] @ zs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
zs \<noteq> []
[PROOF STEP]
have decomp1: "set (walk_edges (xs@[y]@zs)) = set (walk_edges (xs@[y])) \<union> set (walk_edges (zs)) \<union> {{y, hd zs}}"
[PROOF STATE]
proof (prove)
using this:
zs \<noteq> []

goal (1 subgoal):
 1. set (walk_edges (xs @ [y] @ zs)) = set (walk_edges (xs @ [y])) \<union> set (walk_edges zs) \<union> {{y, hd zs}}
[PROOF STEP]
using walk_edges_append_union
[PROOF STATE]
proof (prove)
using this:
zs \<noteq> []
\<lbrakk>?xs \<noteq> []; ?ys \<noteq> []\<rbrakk> \<Longrightarrow> set (walk_edges (?xs @ ?ys)) = set (walk_edges ?xs) \<union> set (walk_edges ?ys) \<union> {{last ?xs, hd ?ys}}

goal (1 subgoal):
 1. set (walk_edges (xs @ [y] @ zs)) = set (walk_edges (xs @ [y])) \<union> set (walk_edges zs) \<union> {{y, hd zs}}
[PROOF STEP]
by (metis append_assoc append_is_Nil_conv last_snoc neq_Nil_conv)
[PROOF STATE]
proof (state)
this:
set (walk_edges (xs @ [y] @ zs)) = set (walk_edges (xs @ [y])) \<union> set (walk_edges zs) \<union> {{y, hd zs}}

goal (1 subgoal):
 1. \<lbrakk>set (walk_edges (xs @ [y])) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y])); zs \<noteq> []\<rbrakk> \<Longrightarrow> set (walk_edges (xs @ [y] @ zs)) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y] @ zs))
[PROOF STEP]
have "set (walk_edges (xs@[y]@ys@[y]@zs)) =  set (walk_edges (xs@[y]@ys@[y])) \<union> set (walk_edges (zs)) \<union> {{y, hd zs}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (walk_edges (xs @ [y] @ ys @ [y] @ zs)) = set (walk_edges (xs @ [y] @ ys @ [y])) \<union> set (walk_edges zs) \<union> {{y, hd zs}}
[PROOF STEP]
using walk_edges_append_union False
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?xs \<noteq> []; ?ys \<noteq> []\<rbrakk> \<Longrightarrow> set (walk_edges (?xs @ ?ys)) = set (walk_edges ?xs) \<union> set (walk_edges ?ys) \<union> {{last ?xs, hd ?ys}}
zs \<noteq> []

goal (1 subgoal):
 1. set (walk_edges (xs @ [y] @ ys @ [y] @ zs)) = set (walk_edges (xs @ [y] @ ys @ [y])) \<union> set (walk_edges zs) \<union> {{y, hd zs}}
[PROOF STEP]
by (metis append_assoc append_is_Nil_conv empty_iff empty_set last_snoc list.set_intros(1))
[PROOF STATE]
proof (state)
this:
set (walk_edges (xs @ [y] @ ys @ [y] @ zs)) = set (walk_edges (xs @ [y] @ ys @ [y])) \<union> set (walk_edges zs) \<union> {{y, hd zs}}

goal (1 subgoal):
 1. \<lbrakk>set (walk_edges (xs @ [y])) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y])); zs \<noteq> []\<rbrakk> \<Longrightarrow> set (walk_edges (xs @ [y] @ zs)) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y] @ zs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set (walk_edges (xs @ [y] @ ys @ [y] @ zs)) = set (walk_edges (xs @ [y] @ ys @ [y])) \<union> set (walk_edges zs) \<union> {{y, hd zs}}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set (walk_edges (xs @ [y] @ ys @ [y] @ zs)) = set (walk_edges (xs @ [y] @ ys @ [y])) \<union> set (walk_edges zs) \<union> {{y, hd zs}}

goal (1 subgoal):
 1. set (walk_edges (xs @ [y] @ zs)) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y] @ zs))
[PROOF STEP]
using decomp1 half_ss
[PROOF STATE]
proof (prove)
using this:
set (walk_edges (xs @ [y] @ ys @ [y] @ zs)) = set (walk_edges (xs @ [y] @ ys @ [y])) \<union> set (walk_edges zs) \<union> {{y, hd zs}}
set (walk_edges (xs @ [y] @ zs)) = set (walk_edges (xs @ [y])) \<union> set (walk_edges zs) \<union> {{y, hd zs}}
set (walk_edges (xs @ [y])) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y]))

goal (1 subgoal):
 1. set (walk_edges (xs @ [y] @ zs)) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y] @ zs))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (walk_edges (xs @ [y] @ zs)) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y] @ zs))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set (walk_edges (xs @ [y] @ zs)) \<subseteq> set (walk_edges (xs @ [y] @ ys @ [y] @ zs))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma walk_length_conv: "walk_length p = length p - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. walk_length p = length p - 1
[PROOF STEP]
by (induct p rule: walk_edges.induct) (auto simp: walk_length_def)


[STATEMENT]
lemma walk_length_rev: "walk_length p = walk_length (rev p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. walk_length p = walk_length (rev p)
[PROOF STEP]
using walk_edges_rev walk_length_def
[PROOF STATE]
proof (prove)
using this:
rev (walk_edges ?xs) = walk_edges (rev ?xs)
walk_length ?p \<equiv> length (walk_edges ?p)

goal (1 subgoal):
 1. walk_length p = walk_length (rev p)
[PROOF STEP]
by (metis length_rev)


[STATEMENT]
lemma walk_length_app: "xs \<noteq> [] \<Longrightarrow> ys \<noteq> [] \<Longrightarrow> walk_length (xs @ ys) = walk_length xs + walk_length ys + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs \<noteq> []; ys \<noteq> []\<rbrakk> \<Longrightarrow> walk_length (xs @ ys) = walk_length xs + walk_length ys + 1
[PROOF STEP]
apply (induct xs rule: walk_edges.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>[] \<noteq> []; ys \<noteq> []\<rbrakk> \<Longrightarrow> walk_length ([] @ ys) = walk_length [] + walk_length ys + 1
 2. \<And>x. \<lbrakk>[x] \<noteq> []; ys \<noteq> []\<rbrakk> \<Longrightarrow> walk_length ([x] @ ys) = walk_length [x] + walk_length ys + 1
 3. \<And>x y ysa. \<lbrakk>\<lbrakk>y # ysa \<noteq> []; ys \<noteq> []\<rbrakk> \<Longrightarrow> walk_length ((y # ysa) @ ys) = walk_length (y # ysa) + walk_length ys + 1; x # y # ysa \<noteq> []; ys \<noteq> []\<rbrakk> \<Longrightarrow> walk_length ((x # y # ysa) @ ys) = walk_length (x # y # ysa) + walk_length ys + 1
[PROOF STEP]
apply (simp_all add: walk_length_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. ys \<noteq> [] \<Longrightarrow> length (walk_edges (x # ys)) = Suc (length (walk_edges ys))
[PROOF STEP]
using walk_edges_singleton_app
[PROOF STATE]
proof (prove)
using this:
?ys \<noteq> [] \<Longrightarrow> walk_edges ([?x] @ ?ys) = {?x, hd ?ys} # walk_edges ?ys

goal (1 subgoal):
 1. \<And>x. ys \<noteq> [] \<Longrightarrow> length (walk_edges (x # ys)) = Suc (length (walk_edges ys))
[PROOF STEP]
by force


[STATEMENT]
lemma walk_length_app_ineq: "walk_length (xs @ ys) \<ge> walk_length xs + walk_length ys \<and>
  walk_length (xs @ ys) \<le> walk_length xs + walk_length ys + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. walk_length xs + walk_length ys \<le> walk_length (xs @ ys) \<and> walk_length (xs @ ys) \<le> walk_length xs + walk_length ys + 1
[PROOF STEP]
proof (cases "xs = [] \<or> ys = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. xs = [] \<or> ys = [] \<Longrightarrow> walk_length xs + walk_length ys \<le> walk_length (xs @ ys) \<and> walk_length (xs @ ys) \<le> walk_length xs + walk_length ys + 1
 2. \<not> (xs = [] \<or> ys = []) \<Longrightarrow> walk_length xs + walk_length ys \<le> walk_length (xs @ ys) \<and> walk_length (xs @ ys) \<le> walk_length xs + walk_length ys + 1
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
xs = [] \<or> ys = []

goal (2 subgoals):
 1. xs = [] \<or> ys = [] \<Longrightarrow> walk_length xs + walk_length ys \<le> walk_length (xs @ ys) \<and> walk_length (xs @ ys) \<le> walk_length xs + walk_length ys + 1
 2. \<not> (xs = [] \<or> ys = []) \<Longrightarrow> walk_length xs + walk_length ys \<le> walk_length (xs @ ys) \<and> walk_length (xs @ ys) \<le> walk_length xs + walk_length ys + 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs = [] \<or> ys = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xs = [] \<or> ys = []

goal (1 subgoal):
 1. walk_length xs + walk_length ys \<le> walk_length (xs @ ys) \<and> walk_length (xs @ ys) \<le> walk_length xs + walk_length ys + 1
[PROOF STEP]
using walk_length_def
[PROOF STATE]
proof (prove)
using this:
xs = [] \<or> ys = []
walk_length ?p \<equiv> length (walk_edges ?p)

goal (1 subgoal):
 1. walk_length xs + walk_length ys \<le> walk_length (xs @ ys) \<and> walk_length (xs @ ys) \<le> walk_length xs + walk_length ys + 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
walk_length xs + walk_length ys \<le> walk_length (xs @ ys) \<and> walk_length (xs @ ys) \<le> walk_length xs + walk_length ys + 1

goal (1 subgoal):
 1. \<not> (xs = [] \<or> ys = []) \<Longrightarrow> walk_length xs + walk_length ys \<le> walk_length (xs @ ys) \<and> walk_length (xs @ ys) \<le> walk_length xs + walk_length ys + 1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (xs = [] \<or> ys = []) \<Longrightarrow> walk_length xs + walk_length ys \<le> walk_length (xs @ ys) \<and> walk_length (xs @ ys) \<le> walk_length xs + walk_length ys + 1
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (xs = [] \<or> ys = [])

goal (1 subgoal):
 1. \<not> (xs = [] \<or> ys = []) \<Longrightarrow> walk_length xs + walk_length ys \<le> walk_length (xs @ ys) \<and> walk_length (xs @ ys) \<le> walk_length xs + walk_length ys + 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (xs = [] \<or> ys = [])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> (xs = [] \<or> ys = [])

goal (1 subgoal):
 1. walk_length xs + walk_length ys \<le> walk_length (xs @ ys) \<and> walk_length (xs @ ys) \<le> walk_length xs + walk_length ys + 1
[PROOF STEP]
by (simp add: walk_length_app)
[PROOF STATE]
proof (state)
this:
walk_length xs + walk_length ys \<le> walk_length (xs @ ys) \<and> walk_length (xs @ ys) \<le> walk_length xs + walk_length ys + 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_walkI: "set xs \<subseteq> V \<Longrightarrow> set (walk_edges xs) \<subseteq> E \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> is_walk xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set xs \<subseteq> V; set (walk_edges xs) \<subseteq> E; xs \<noteq> []\<rbrakk> \<Longrightarrow> is_walk xs
[PROOF STEP]
using is_walk_def
[PROOF STATE]
proof (prove)
using this:
is_walk ?xs \<equiv> set ?xs \<subseteq> V \<and> set (walk_edges ?xs) \<subseteq> E \<and> ?xs \<noteq> []

goal (1 subgoal):
 1. \<lbrakk>set xs \<subseteq> V; set (walk_edges xs) \<subseteq> E; xs \<noteq> []\<rbrakk> \<Longrightarrow> is_walk xs
[PROOF STEP]
by simp


[STATEMENT]
lemma is_walk_wf: "is_walk xs \<Longrightarrow> set xs \<subseteq> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_walk xs \<Longrightarrow> set xs \<subseteq> V
[PROOF STEP]
by (simp add: is_walk_def)


[STATEMENT]
lemma is_walk_wf_hd: "is_walk xs \<Longrightarrow> hd xs \<in> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_walk xs \<Longrightarrow> hd xs \<in> V
[PROOF STEP]
using is_walk_wf hd_in_set is_walk_def
[PROOF STATE]
proof (prove)
using this:
is_walk ?xs \<Longrightarrow> set ?xs \<subseteq> V
?xs \<noteq> [] \<Longrightarrow> hd ?xs \<in> set ?xs
is_walk ?xs \<equiv> set ?xs \<subseteq> V \<and> set (walk_edges ?xs) \<subseteq> E \<and> ?xs \<noteq> []

goal (1 subgoal):
 1. is_walk xs \<Longrightarrow> hd xs \<in> V
[PROOF STEP]
by blast


[STATEMENT]
lemma is_walk_wf_last: "is_walk xs \<Longrightarrow> last xs \<in> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_walk xs \<Longrightarrow> last xs \<in> V
[PROOF STEP]
using is_walk_wf last_in_set is_walk_def
[PROOF STATE]
proof (prove)
using this:
is_walk ?xs \<Longrightarrow> set ?xs \<subseteq> V
?as \<noteq> [] \<Longrightarrow> last ?as \<in> set ?as
is_walk ?xs \<equiv> set ?xs \<subseteq> V \<and> set (walk_edges ?xs) \<subseteq> E \<and> ?xs \<noteq> []

goal (1 subgoal):
 1. is_walk xs \<Longrightarrow> last xs \<in> V
[PROOF STEP]
by blast


[STATEMENT]
lemma is_walk_singleton: "u \<in> V \<Longrightarrow> is_walk [u]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<in> V \<Longrightarrow> is_walk [u]
[PROOF STEP]
unfolding is_walk_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<in> V \<Longrightarrow> set [u] \<subseteq> V \<and> set (walk_edges [u]) \<subseteq> E \<and> [u] \<noteq> []
[PROOF STEP]
using walk_edges.simps
[PROOF STATE]
proof (prove)
using this:
walk_edges [] = []
walk_edges [?x] = []
walk_edges (?x # ?y # ?ys) = {?x, ?y} # walk_edges (?y # ?ys)

goal (1 subgoal):
 1. u \<in> V \<Longrightarrow> set [u] \<subseteq> V \<and> set (walk_edges [u]) \<subseteq> E \<and> [u] \<noteq> []
[PROOF STEP]
by simp


[STATEMENT]
lemma is_walk_not_empty: "is_walk xs \<Longrightarrow> xs \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_walk xs \<Longrightarrow> xs \<noteq> []
[PROOF STEP]
unfolding is_walk_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set xs \<subseteq> V \<and> set (walk_edges xs) \<subseteq> E \<and> xs \<noteq> [] \<Longrightarrow> xs \<noteq> []
[PROOF STEP]
by simp


[STATEMENT]
lemma is_walk_not_empty2: "is_walk [] = False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_walk [] = False
[PROOF STEP]
unfolding is_walk_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (set [] \<subseteq> V \<and> set (walk_edges []) \<subseteq> E \<and> [] \<noteq> []) = False
[PROOF STEP]
by simp


[STATEMENT]
lemma is_walk_rev: "is_walk xs \<longleftrightarrow> is_walk (rev xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_walk xs = is_walk (rev xs)
[PROOF STEP]
unfolding is_walk_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (set xs \<subseteq> V \<and> set (walk_edges xs) \<subseteq> E \<and> xs \<noteq> []) = (set (rev xs) \<subseteq> V \<and> set (walk_edges (rev xs)) \<subseteq> E \<and> rev xs \<noteq> [])
[PROOF STEP]
using walk_edges_rev
[PROOF STATE]
proof (prove)
using this:
rev (walk_edges ?xs) = walk_edges (rev ?xs)

goal (1 subgoal):
 1. (set xs \<subseteq> V \<and> set (walk_edges xs) \<subseteq> E \<and> xs \<noteq> []) = (set (rev xs) \<subseteq> V \<and> set (walk_edges (rev xs)) \<subseteq> E \<and> rev xs \<noteq> [])
[PROOF STEP]
by (metis rev_is_Nil_conv set_rev)


[STATEMENT]
lemma is_walk_tl: "length xs \<ge> 2 \<Longrightarrow> is_walk xs \<Longrightarrow> is_walk (tl xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 \<le> length xs; is_walk xs\<rbrakk> \<Longrightarrow> is_walk (tl xs)
[PROOF STEP]
using walk_edges_tl_ss is_walk_def in_mono list.set_sel(2) tl_Nil
[PROOF STATE]
proof (prove)
using this:
set (walk_edges (tl ?xs)) \<subseteq> set (walk_edges ?xs)
is_walk ?xs \<equiv> set ?xs \<subseteq> V \<and> set (walk_edges ?xs) \<subseteq> E \<and> ?xs \<noteq> []
?A \<subseteq> ?B \<Longrightarrow> ?x \<in> ?A \<longrightarrow> ?x \<in> ?B
\<lbrakk>?a \<noteq> []; ?x \<in> set (tl ?a)\<rbrakk> \<Longrightarrow> ?x \<in> set ?a
(tl ?xs = []) = (?xs = [] \<or> (\<exists>x. ?xs = [x]))

goal (1 subgoal):
 1. \<lbrakk>2 \<le> length xs; is_walk xs\<rbrakk> \<Longrightarrow> is_walk (tl xs)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma is_walk_append:
  assumes "is_walk xs"
  assumes "is_walk ys"
  assumes "last xs = hd ys"
  shows "is_walk (xs @ (tl ys))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_walk (xs @ tl ys)
[PROOF STEP]
proof (intro is_walkI subsetI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. x \<in> set (xs @ tl ys) \<Longrightarrow> x \<in> V
 2. \<And>x. x \<in> set (walk_edges (xs @ tl ys)) \<Longrightarrow> x \<in> E
 3. xs @ tl ys \<noteq> []
[PROOF STEP]
show "xs @ tl ys \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs @ tl ys \<noteq> []
[PROOF STEP]
using is_walk_def assms
[PROOF STATE]
proof (prove)
using this:
is_walk ?xs \<equiv> set ?xs \<subseteq> V \<and> set (walk_edges ?xs) \<subseteq> E \<and> ?xs \<noteq> []
is_walk xs
is_walk ys
last xs = hd ys

goal (1 subgoal):
 1. xs @ tl ys \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xs @ tl ys \<noteq> []

goal (2 subgoals):
 1. \<And>x. x \<in> set (xs @ tl ys) \<Longrightarrow> x \<in> V
 2. \<And>x. x \<in> set (walk_edges (xs @ tl ys)) \<Longrightarrow> x \<in> E
[PROOF STEP]
show "\<And>x. x \<in> set (xs @ tl ys) \<Longrightarrow> x \<in> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set (xs @ tl ys) \<Longrightarrow> x \<in> V
[PROOF STEP]
using assms is_walk_def is_walk_wf
[PROOF STATE]
proof (prove)
using this:
is_walk xs
is_walk ys
last xs = hd ys
is_walk ?xs \<equiv> set ?xs \<subseteq> V \<and> set (walk_edges ?xs) \<subseteq> E \<and> ?xs \<noteq> []
is_walk ?xs \<Longrightarrow> set ?xs \<subseteq> V

goal (1 subgoal):
 1. \<And>x. x \<in> set (xs @ tl ys) \<Longrightarrow> x \<in> V
[PROOF STEP]
by (metis Un_iff in_mono list_set_tl set_append)
[PROOF STATE]
proof (state)
this:
?x \<in> set (xs @ tl ys) \<Longrightarrow> ?x \<in> V

goal (1 subgoal):
 1. \<And>x. x \<in> set (walk_edges (xs @ tl ys)) \<Longrightarrow> x \<in> E
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set (walk_edges (xs @ tl ys)) \<Longrightarrow> x \<in> E
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set (walk_edges (xs @ tl ys)) \<Longrightarrow> x \<in> E
[PROOF STEP]
assume xin: "x \<in> set (walk_edges (xs @ tl ys))"
[PROOF STATE]
proof (state)
this:
x \<in> set (walk_edges (xs @ tl ys))

goal (1 subgoal):
 1. \<And>x. x \<in> set (walk_edges (xs @ tl ys)) \<Longrightarrow> x \<in> E
[PROOF STEP]
show "x \<in> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> E
[PROOF STEP]
proof (cases "tl ys = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. tl ys = [] \<Longrightarrow> x \<in> E
 2. tl ys \<noteq> [] \<Longrightarrow> x \<in> E
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
tl ys = []

goal (2 subgoals):
 1. tl ys = [] \<Longrightarrow> x \<in> E
 2. tl ys \<noteq> [] \<Longrightarrow> x \<in> E
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
tl ys = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
tl ys = []

goal (1 subgoal):
 1. x \<in> E
[PROOF STEP]
using assms(1) is_walk_def xin
[PROOF STATE]
proof (prove)
using this:
tl ys = []
is_walk xs
is_walk ?xs \<equiv> set ?xs \<subseteq> V \<and> set (walk_edges ?xs) \<subseteq> E \<and> ?xs \<noteq> []
x \<in> set (walk_edges (xs @ tl ys))

goal (1 subgoal):
 1. x \<in> E
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> E

goal (1 subgoal):
 1. tl ys \<noteq> [] \<Longrightarrow> x \<in> E
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. tl ys \<noteq> [] \<Longrightarrow> x \<in> E
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
tl ys \<noteq> []

goal (1 subgoal):
 1. tl ys \<noteq> [] \<Longrightarrow> x \<in> E
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
tl ys \<noteq> []
[PROOF STEP]
have xin2: "x \<in> (set (walk_edges xs) \<union> set (walk_edges (tl ys)) \<union> {{last xs, hd (tl ys)}})"
[PROOF STATE]
proof (prove)
using this:
tl ys \<noteq> []

goal (1 subgoal):
 1. x \<in> set (walk_edges xs) \<union> set (walk_edges (tl ys)) \<union> {{last xs, hd (tl ys)}}
[PROOF STEP]
using walk_edges_append_union is_walk_not_empty assms xin
[PROOF STATE]
proof (prove)
using this:
tl ys \<noteq> []
\<lbrakk>?xs \<noteq> []; ?ys \<noteq> []\<rbrakk> \<Longrightarrow> set (walk_edges (?xs @ ?ys)) = set (walk_edges ?xs) \<union> set (walk_edges ?ys) \<union> {{last ?xs, hd ?ys}}
is_walk ?xs \<Longrightarrow> ?xs \<noteq> []
is_walk xs
is_walk ys
last xs = hd ys
x \<in> set (walk_edges (xs @ tl ys))

goal (1 subgoal):
 1. x \<in> set (walk_edges xs) \<union> set (walk_edges (tl ys)) \<union> {{last xs, hd (tl ys)}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> set (walk_edges xs) \<union> set (walk_edges (tl ys)) \<union> {{last xs, hd (tl ys)}}

goal (1 subgoal):
 1. tl ys \<noteq> [] \<Longrightarrow> x \<in> E
[PROOF STEP]
have 1: "set (walk_edges xs) \<subseteq> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (walk_edges xs) \<subseteq> E
[PROOF STEP]
using assms(1) is_walk_def
[PROOF STATE]
proof (prove)
using this:
is_walk xs
is_walk ?xs \<equiv> set ?xs \<subseteq> V \<and> set (walk_edges ?xs) \<subseteq> E \<and> ?xs \<noteq> []

goal (1 subgoal):
 1. set (walk_edges xs) \<subseteq> E
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (walk_edges xs) \<subseteq> E

goal (1 subgoal):
 1. tl ys \<noteq> [] \<Longrightarrow> x \<in> E
[PROOF STEP]
have 2: "set (walk_edges (tl ys)) \<subseteq> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (walk_edges (tl ys)) \<subseteq> E
[PROOF STEP]
using assms(2) is_walk_def
[PROOF STATE]
proof (prove)
using this:
is_walk ys
is_walk ?xs \<equiv> set ?xs \<subseteq> V \<and> set (walk_edges ?xs) \<subseteq> E \<and> ?xs \<noteq> []

goal (1 subgoal):
 1. set (walk_edges (tl ys)) \<subseteq> E
[PROOF STEP]
by (meson dual_order.trans walk_edges_tl_ss)
[PROOF STATE]
proof (state)
this:
set (walk_edges (tl ys)) \<subseteq> E

goal (1 subgoal):
 1. tl ys \<noteq> [] \<Longrightarrow> x \<in> E
[PROOF STEP]
have "{last xs, hd (tl ys)} \<in> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {last xs, hd (tl ys)} \<in> E
[PROOF STEP]
using is_walk_def assms(2) assms(3)
[PROOF STATE]
proof (prove)
using this:
is_walk ?xs \<equiv> set ?xs \<subseteq> V \<and> set (walk_edges ?xs) \<subseteq> E \<and> ?xs \<noteq> []
is_walk ys
last xs = hd ys

goal (1 subgoal):
 1. {last xs, hd (tl ys)} \<in> E
[PROOF STEP]
by (metis False hd_Cons_tl insert_subset list.simps(15) walk_edges.simps(3))
[PROOF STATE]
proof (state)
this:
{last xs, hd (tl ys)} \<in> E

goal (1 subgoal):
 1. tl ys \<noteq> [] \<Longrightarrow> x \<in> E
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{last xs, hd (tl ys)} \<in> E
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{last xs, hd (tl ys)} \<in> E

goal (1 subgoal):
 1. x \<in> E
[PROOF STEP]
using 1 2 xin2
[PROOF STATE]
proof (prove)
using this:
{last xs, hd (tl ys)} \<in> E
set (walk_edges xs) \<subseteq> E
set (walk_edges (tl ys)) \<subseteq> E
x \<in> set (walk_edges xs) \<union> set (walk_edges (tl ys)) \<union> {{last xs, hd (tl ys)}}

goal (1 subgoal):
 1. x \<in> E
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> E

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> E

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_walk_decomp:
  assumes "is_walk (xs@[y]@ys@[y]@zs)" (is "is_walk ?w")
  shows "is_walk (xs@[y]@zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_walk (xs @ [y] @ zs)
[PROOF STEP]
proof (intro is_walkI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. set (xs @ [y] @ zs) \<subseteq> V
 2. set (walk_edges (xs @ [y] @ zs)) \<subseteq> E
 3. xs @ [y] @ zs \<noteq> []
[PROOF STEP]
show "set (xs @ [y] @ zs) \<subseteq> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (xs @ [y] @ zs) \<subseteq> V
[PROOF STEP]
using assms is_walk_def
[PROOF STATE]
proof (prove)
using this:
is_walk (xs @ [y] @ ys @ [y] @ zs)
is_walk ?xs \<equiv> set ?xs \<subseteq> V \<and> set (walk_edges ?xs) \<subseteq> E \<and> ?xs \<noteq> []

goal (1 subgoal):
 1. set (xs @ [y] @ zs) \<subseteq> V
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (xs @ [y] @ zs) \<subseteq> V

goal (2 subgoals):
 1. set (walk_edges (xs @ [y] @ zs)) \<subseteq> E
 2. xs @ [y] @ zs \<noteq> []
[PROOF STEP]
show "xs @ [y] @ zs \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs @ [y] @ zs \<noteq> []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
xs @ [y] @ zs \<noteq> []

goal (1 subgoal):
 1. set (walk_edges (xs @ [y] @ zs)) \<subseteq> E
[PROOF STEP]
show "set (walk_edges (xs @ [y] @ zs)) \<subseteq> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (walk_edges (xs @ [y] @ zs)) \<subseteq> E
[PROOF STEP]
using walk_edges_decomp_ss assms(1) is_walk_def
[PROOF STATE]
proof (prove)
using this:
set (walk_edges (?xs @ [?y] @ ?zs)) \<subseteq> set (walk_edges (?xs @ [?y] @ ?ys @ [?y] @ ?zs))
is_walk (xs @ [y] @ ys @ [y] @ zs)
is_walk ?xs \<equiv> set ?xs \<subseteq> V \<and> set (walk_edges ?xs) \<subseteq> E \<and> ?xs \<noteq> []

goal (1 subgoal):
 1. set (walk_edges (xs @ [y] @ zs)) \<subseteq> E
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set (walk_edges (xs @ [y] @ zs)) \<subseteq> E

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_walk_hd_tl:
  assumes "is_walk (y # ys)"
  assumes "{x, y} \<in> E"
  shows "is_walk (x # y # ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_walk (x # y # ys)
[PROOF STEP]
proof (intro is_walkI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. set (x # y # ys) \<subseteq> V
 2. set (walk_edges (x # y # ys)) \<subseteq> E
 3. x # y # ys \<noteq> []
[PROOF STEP]
show "set (x # y # ys) \<subseteq> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (x # y # ys) \<subseteq> V
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_walk (y # ys)
{x, y} \<in> E

goal (1 subgoal):
 1. set (x # y # ys) \<subseteq> V
[PROOF STEP]
by (simp add: is_walk_def wellformed_alt_fst)
[PROOF STATE]
proof (state)
this:
set (x # y # ys) \<subseteq> V

goal (2 subgoals):
 1. set (walk_edges (x # y # ys)) \<subseteq> E
 2. x # y # ys \<noteq> []
[PROOF STEP]
show "set (walk_edges (x # y # ys)) \<subseteq> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (walk_edges (x # y # ys)) \<subseteq> E
[PROOF STEP]
using walk_edges.simps assms is_walk_def
[PROOF STATE]
proof (prove)
using this:
walk_edges [] = []
walk_edges [?x] = []
walk_edges (?x # ?y # ?ys) = {?x, ?y} # walk_edges (?y # ?ys)
is_walk (y # ys)
{x, y} \<in> E
is_walk ?xs \<equiv> set ?xs \<subseteq> V \<and> set (walk_edges ?xs) \<subseteq> E \<and> ?xs \<noteq> []

goal (1 subgoal):
 1. set (walk_edges (x # y # ys)) \<subseteq> E
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (walk_edges (x # y # ys)) \<subseteq> E

goal (1 subgoal):
 1. x # y # ys \<noteq> []
[PROOF STEP]
show "x # y # ys \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x # y # ys \<noteq> []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x # y # ys \<noteq> []

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_walk_drop_hd:
  assumes "ys \<noteq> []"
  assumes "is_walk (y # ys)"
  shows "is_walk ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_walk ys
[PROOF STEP]
proof (intro is_walkI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. set ys \<subseteq> V
 2. set (walk_edges ys) \<subseteq> E
 3. ys \<noteq> []
[PROOF STEP]
show "set ys \<subseteq> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set ys \<subseteq> V
[PROOF STEP]
using assms is_walk_wf
[PROOF STATE]
proof (prove)
using this:
ys \<noteq> []
is_walk (y # ys)
is_walk ?xs \<Longrightarrow> set ?xs \<subseteq> V

goal (1 subgoal):
 1. set ys \<subseteq> V
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
set ys \<subseteq> V

goal (2 subgoals):
 1. set (walk_edges ys) \<subseteq> E
 2. ys \<noteq> []
[PROOF STEP]
show "set (walk_edges ys) \<subseteq> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (walk_edges ys) \<subseteq> E
[PROOF STEP]
using assms is_walk_def walk_edges_tl_ss
[PROOF STATE]
proof (prove)
using this:
ys \<noteq> []
is_walk (y # ys)
is_walk ?xs \<equiv> set ?xs \<subseteq> V \<and> set (walk_edges ?xs) \<subseteq> E \<and> ?xs \<noteq> []
set (walk_edges (tl ?xs)) \<subseteq> set (walk_edges ?xs)

goal (1 subgoal):
 1. set (walk_edges ys) \<subseteq> E
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
set (walk_edges ys) \<subseteq> E

goal (1 subgoal):
 1. ys \<noteq> []
[PROOF STEP]
show "ys \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ys \<noteq> []
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ys \<noteq> []
is_walk (y # ys)

goal (1 subgoal):
 1. ys \<noteq> []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ys \<noteq> []

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma walk_edges_index:
  assumes "i \<ge> 0" "i < walk_length w"
  assumes "is_walk w"
  shows "(walk_edges w) ! i \<in> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. walk_edges w ! i \<in> E
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 \<le> i
i < walk_length w
is_walk w

goal (1 subgoal):
 1. walk_edges w ! i \<in> E
[PROOF STEP]
proof (induct w arbitrary: i rule: walk_edges.induct, simp add: is_walk_not_empty2,
    simp add: walk_length_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y ys i. \<lbrakk>\<And>i. \<lbrakk>0 \<le> i; i < walk_length (y # ys); is_walk (y # ys)\<rbrakk> \<Longrightarrow> walk_edges (y # ys) ! i \<in> E; 0 \<le> i; i < walk_length (x # y # ys); is_walk (x # y # ys)\<rbrakk> \<Longrightarrow> walk_edges (x # y # ys) ! i \<in> E
[PROOF STEP]
case (3 x y ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 \<le> ?i; ?i < walk_length (y # ys); is_walk (y # ys)\<rbrakk> \<Longrightarrow> walk_edges (y # ys) ! ?i \<in> E
0 \<le> i
i < walk_length (x # y # ys)
is_walk (x # y # ys)

goal (1 subgoal):
 1. \<And>x y ys i. \<lbrakk>\<And>i. \<lbrakk>0 \<le> i; i < walk_length (y # ys); is_walk (y # ys)\<rbrakk> \<Longrightarrow> walk_edges (y # ys) ! i \<in> E; 0 \<le> i; i < walk_length (x # y # ys); is_walk (x # y # ys)\<rbrakk> \<Longrightarrow> walk_edges (x # y # ys) ! i \<in> E
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>0 \<le> ?i; ?i < walk_length (y # ys); is_walk (y # ys)\<rbrakk> \<Longrightarrow> walk_edges (y # ys) ! ?i \<in> E
0 \<le> i
i < walk_length (x # y # ys)
is_walk (x # y # ys)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<le> ?i; ?i < walk_length (y # ys); is_walk (y # ys)\<rbrakk> \<Longrightarrow> walk_edges (y # ys) ! ?i \<in> E
0 \<le> i
i < walk_length (x # y # ys)
is_walk (x # y # ys)

goal (1 subgoal):
 1. walk_edges (x # y # ys) ! i \<in> E
[PROOF STEP]
proof (cases "i = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>i. \<lbrakk>0 \<le> i; i < walk_length (y # ys); is_walk (y # ys)\<rbrakk> \<Longrightarrow> walk_edges (y # ys) ! i \<in> E; 0 \<le> i; i < walk_length (x # y # ys); is_walk (x # y # ys); i = 0\<rbrakk> \<Longrightarrow> walk_edges (x # y # ys) ! i \<in> E
 2. \<lbrakk>\<And>i. \<lbrakk>0 \<le> i; i < walk_length (y # ys); is_walk (y # ys)\<rbrakk> \<Longrightarrow> walk_edges (y # ys) ! i \<in> E; 0 \<le> i; i < walk_length (x # y # ys); is_walk (x # y # ys); i \<noteq> 0\<rbrakk> \<Longrightarrow> walk_edges (x # y # ys) ! i \<in> E
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i = 0

goal (2 subgoals):
 1. \<lbrakk>\<And>i. \<lbrakk>0 \<le> i; i < walk_length (y # ys); is_walk (y # ys)\<rbrakk> \<Longrightarrow> walk_edges (y # ys) ! i \<in> E; 0 \<le> i; i < walk_length (x # y # ys); is_walk (x # y # ys); i = 0\<rbrakk> \<Longrightarrow> walk_edges (x # y # ys) ! i \<in> E
 2. \<lbrakk>\<And>i. \<lbrakk>0 \<le> i; i < walk_length (y # ys); is_walk (y # ys)\<rbrakk> \<Longrightarrow> walk_edges (y # ys) ! i \<in> E; 0 \<le> i; i < walk_length (x # y # ys); is_walk (x # y # ys); i \<noteq> 0\<rbrakk> \<Longrightarrow> walk_edges (x # y # ys) ! i \<in> E
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i = 0

goal (1 subgoal):
 1. walk_edges (x # y # ys) ! i \<in> E
[PROOF STEP]
using "3.prems"(3) is_walk_def
[PROOF STATE]
proof (prove)
using this:
i = 0
is_walk (x # y # ys)
is_walk ?xs \<equiv> set ?xs \<subseteq> V \<and> set (walk_edges ?xs) \<subseteq> E \<and> ?xs \<noteq> []

goal (1 subgoal):
 1. walk_edges (x # y # ys) ! i \<in> E
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
walk_edges (x # y # ys) ! i \<in> E

goal (1 subgoal):
 1. \<lbrakk>\<And>i. \<lbrakk>0 \<le> i; i < walk_length (y # ys); is_walk (y # ys)\<rbrakk> \<Longrightarrow> walk_edges (y # ys) ! i \<in> E; 0 \<le> i; i < walk_length (x # y # ys); is_walk (x # y # ys); i \<noteq> 0\<rbrakk> \<Longrightarrow> walk_edges (x # y # ys) ! i \<in> E
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>i. \<lbrakk>0 \<le> i; i < walk_length (y # ys); is_walk (y # ys)\<rbrakk> \<Longrightarrow> walk_edges (y # ys) ! i \<in> E; 0 \<le> i; i < walk_length (x # y # ys); is_walk (x # y # ys); i \<noteq> 0\<rbrakk> \<Longrightarrow> walk_edges (x # y # ys) ! i \<in> E
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
i \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>\<And>i. \<lbrakk>0 \<le> i; i < walk_length (y # ys); is_walk (y # ys)\<rbrakk> \<Longrightarrow> walk_edges (y # ys) ! i \<in> E; 0 \<le> i; i < walk_length (x # y # ys); is_walk (x # y # ys); i \<noteq> 0\<rbrakk> \<Longrightarrow> walk_edges (x # y # ys) ! i \<in> E
[PROOF STEP]
have gt: "0 \<le> i -1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> i - 1
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
i \<noteq> 0

goal (1 subgoal):
 1. 0 \<le> i - 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> i - 1

goal (1 subgoal):
 1. \<lbrakk>\<And>i. \<lbrakk>0 \<le> i; i < walk_length (y # ys); is_walk (y # ys)\<rbrakk> \<Longrightarrow> walk_edges (y # ys) ! i \<in> E; 0 \<le> i; i < walk_length (x # y # ys); is_walk (x # y # ys); i \<noteq> 0\<rbrakk> \<Longrightarrow> walk_edges (x # y # ys) ! i \<in> E
[PROOF STEP]
have lt: "i - 1 < walk_length (y # ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i - 1 < walk_length (y # ys)
[PROOF STEP]
using "3.prems"(2) False walk_length_conv
[PROOF STATE]
proof (prove)
using this:
i < walk_length (x # y # ys)
i \<noteq> 0
walk_length ?p = length ?p - 1

goal (1 subgoal):
 1. i - 1 < walk_length (y # ys)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i - 1 < walk_length (y # ys)

goal (1 subgoal):
 1. \<lbrakk>\<And>i. \<lbrakk>0 \<le> i; i < walk_length (y # ys); is_walk (y # ys)\<rbrakk> \<Longrightarrow> walk_edges (y # ys) ! i \<in> E; 0 \<le> i; i < walk_length (x # y # ys); is_walk (x # y # ys); i \<noteq> 0\<rbrakk> \<Longrightarrow> walk_edges (x # y # ys) ! i \<in> E
[PROOF STEP]
have "is_walk (y # ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_walk (y # ys)
[PROOF STEP]
using "3.prems"(3) is_walk_def
[PROOF STATE]
proof (prove)
using this:
is_walk (x # y # ys)
is_walk ?xs \<equiv> set ?xs \<subseteq> V \<and> set (walk_edges ?xs) \<subseteq> E \<and> ?xs \<noteq> []

goal (1 subgoal):
 1. is_walk (y # ys)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
is_walk (y # ys)

goal (1 subgoal):
 1. \<lbrakk>\<And>i. \<lbrakk>0 \<le> i; i < walk_length (y # ys); is_walk (y # ys)\<rbrakk> \<Longrightarrow> walk_edges (y # ys) ! i \<in> E; 0 \<le> i; i < walk_length (x # y # ys); is_walk (x # y # ys); i \<noteq> 0\<rbrakk> \<Longrightarrow> walk_edges (x # y # ys) ! i \<in> E
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_walk (y # ys)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_walk (y # ys)

goal (1 subgoal):
 1. walk_edges (x # y # ys) ! i \<in> E
[PROOF STEP]
using "3.hyps"[of "i -1"]
[PROOF STATE]
proof (prove)
using this:
is_walk (y # ys)
\<lbrakk>0 \<le> i - 1; i - 1 < walk_length (y # ys); is_walk (y # ys)\<rbrakk> \<Longrightarrow> walk_edges (y # ys) ! (i - 1) \<in> E

goal (1 subgoal):
 1. walk_edges (x # y # ys) ! i \<in> E
[PROOF STEP]
by (metis "3.prems"(1) False gt lt le_neq_implies_less nth_Cons_pos walk_edges.simps(3))
[PROOF STATE]
proof (state)
this:
walk_edges (x # y # ys) ! i \<in> E

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
walk_edges (x # y # ys) ! i \<in> E

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_walk_index:
  assumes "i \<ge> 0" "Suc i < (length w)"
  assumes "is_walk w"
  shows "{w ! i, w ! (i + 1)} \<in> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {w ! i, w ! (i + 1)} \<in> E
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 \<le> i
Suc i < length w
is_walk w

goal (1 subgoal):
 1. {w ! i, w ! (i + 1)} \<in> E
[PROOF STEP]
proof (induct w arbitrary: i rule: walk_edges.induct, simp, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y ys i. \<lbrakk>\<And>i. \<lbrakk>0 \<le> i; Suc i < length (y # ys); is_walk (y # ys)\<rbrakk> \<Longrightarrow> {(y # ys) ! i, (y # ys) ! (i + 1)} \<in> E; 0 \<le> i; Suc i < length (x # y # ys); is_walk (x # y # ys)\<rbrakk> \<Longrightarrow> {(x # y # ys) ! i, (x # y # ys) ! (i + 1)} \<in> E
[PROOF STEP]
fix x y ys i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y ys i. \<lbrakk>\<And>i. \<lbrakk>0 \<le> i; Suc i < length (y # ys); is_walk (y # ys)\<rbrakk> \<Longrightarrow> {(y # ys) ! i, (y # ys) ! (i + 1)} \<in> E; 0 \<le> i; Suc i < length (x # y # ys); is_walk (x # y # ys)\<rbrakk> \<Longrightarrow> {(x # y # ys) ! i, (x # y # ys) ! (i + 1)} \<in> E
[PROOF STEP]
assume IH: "\<And>j. 0 \<le> j \<Longrightarrow> Suc j < length (y # ys) \<Longrightarrow> is_walk (y # ys) \<Longrightarrow> {(y # ys) ! j, (y # ys) ! (j + 1)} \<in> E"
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 \<le> ?j; Suc ?j < length (y # ys); is_walk (y # ys)\<rbrakk> \<Longrightarrow> {(y # ys) ! ?j, (y # ys) ! (?j + 1)} \<in> E

goal (1 subgoal):
 1. \<And>x y ys i. \<lbrakk>\<And>i. \<lbrakk>0 \<le> i; Suc i < length (y # ys); is_walk (y # ys)\<rbrakk> \<Longrightarrow> {(y # ys) ! i, (y # ys) ! (i + 1)} \<in> E; 0 \<le> i; Suc i < length (x # y # ys); is_walk (x # y # ys)\<rbrakk> \<Longrightarrow> {(x # y # ys) ! i, (x # y # ys) ! (i + 1)} \<in> E
[PROOF STEP]
assume 1: " 0 \<le> i" and 2: "Suc i < length (x # y # ys)" and 3: "is_walk (x # y # ys)"
[PROOF STATE]
proof (state)
this:
0 \<le> i
Suc i < length (x # y # ys)
is_walk (x # y # ys)

goal (1 subgoal):
 1. \<And>x y ys i. \<lbrakk>\<And>i. \<lbrakk>0 \<le> i; Suc i < length (y # ys); is_walk (y # ys)\<rbrakk> \<Longrightarrow> {(y # ys) ! i, (y # ys) ! (i + 1)} \<in> E; 0 \<le> i; Suc i < length (x # y # ys); is_walk (x # y # ys)\<rbrakk> \<Longrightarrow> {(x # y # ys) ! i, (x # y # ys) ! (i + 1)} \<in> E
[PROOF STEP]
show "{(x # y # ys) ! i, (x # y # ys) ! (i + 1)} \<in> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(x # y # ys) ! i, (x # y # ys) ! (i + 1)} \<in> E
[PROOF STEP]
proof (cases "i = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = 0 \<Longrightarrow> {(x # y # ys) ! i, (x # y # ys) ! (i + 1)} \<in> E
 2. i \<noteq> 0 \<Longrightarrow> {(x # y # ys) ! i, (x # y # ys) ! (i + 1)} \<in> E
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i = 0

goal (2 subgoals):
 1. i = 0 \<Longrightarrow> {(x # y # ys) ! i, (x # y # ys) ! (i + 1)} \<in> E
 2. i \<noteq> 0 \<Longrightarrow> {(x # y # ys) ! i, (x # y # ys) ! (i + 1)} \<in> E
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i = 0

goal (1 subgoal):
 1. {(x # y # ys) ! i, (x # y # ys) ! (i + 1)} \<in> E
[PROOF STEP]
using 3 is_walk_def
[PROOF STATE]
proof (prove)
using this:
i = 0
is_walk (x # y # ys)
is_walk ?xs \<equiv> set ?xs \<subseteq> V \<and> set (walk_edges ?xs) \<subseteq> E \<and> ?xs \<noteq> []

goal (1 subgoal):
 1. {(x # y # ys) ! i, (x # y # ys) ! (i + 1)} \<in> E
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{(x # y # ys) ! i, (x # y # ys) ! (i + 1)} \<in> E

goal (1 subgoal):
 1. i \<noteq> 0 \<Longrightarrow> {(x # y # ys) ! i, (x # y # ys) ! (i + 1)} \<in> E
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<noteq> 0 \<Longrightarrow> {(x # y # ys) ! i, (x # y # ys) ! (i + 1)} \<in> E
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
i \<noteq> 0

goal (1 subgoal):
 1. i \<noteq> 0 \<Longrightarrow> {(x # y # ys) ! i, (x # y # ys) ! (i + 1)} \<in> E
[PROOF STEP]
have "is_walk (y # ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_walk (y # ys)
[PROOF STEP]
using is_walk_def 3
[PROOF STATE]
proof (prove)
using this:
is_walk ?xs \<equiv> set ?xs \<subseteq> V \<and> set (walk_edges ?xs) \<subseteq> E \<and> ?xs \<noteq> []
is_walk (x # y # ys)

goal (1 subgoal):
 1. is_walk (y # ys)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
is_walk (y # ys)

goal (1 subgoal):
 1. i \<noteq> 0 \<Longrightarrow> {(x # y # ys) ! i, (x # y # ys) ! (i + 1)} \<in> E
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_walk (y # ys)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_walk (y # ys)

goal (1 subgoal):
 1. {(x # y # ys) ! i, (x # y # ys) ! (i + 1)} \<in> E
[PROOF STEP]
using 2 IH[of "i - 1"]
[PROOF STATE]
proof (prove)
using this:
is_walk (y # ys)
Suc i < length (x # y # ys)
\<lbrakk>0 \<le> i - 1; Suc (i - 1) < length (y # ys); is_walk (y # ys)\<rbrakk> \<Longrightarrow> {(y # ys) ! (i - 1), (y # ys) ! (i - 1 + 1)} \<in> E

goal (1 subgoal):
 1. {(x # y # ys) ! i, (x # y # ys) ! (i + 1)} \<in> E
[PROOF STEP]
by (simp add: False nat_less_le)
[PROOF STATE]
proof (state)
this:
{(x # y # ys) ! i, (x # y # ys) ! (i + 1)} \<in> E

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{(x # y # ys) ! i, (x # y # ys) ! (i + 1)} \<in> E

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_walk_take:
  assumes "is_walk w"
  assumes "n > 0"
  assumes "n \<le> length w"
  shows "is_walk (take n w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_walk (take n w)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_walk w
0 < n
n \<le> length w

goal (1 subgoal):
 1. is_walk (take n w)
[PROOF STEP]
proof (induct w arbitrary: n rule: walk_edges.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>is_walk []; 0 < n; n \<le> length []\<rbrakk> \<Longrightarrow> is_walk (take n [])
 2. \<And>x n. \<lbrakk>is_walk [x]; 0 < n; n \<le> length [x]\<rbrakk> \<Longrightarrow> is_walk (take n [x])
 3. \<And>x y ys n. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); 0 < n; n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (y # ys)); is_walk (x # y # ys); 0 < n; n \<le> length (x # y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (x # y # ys))
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
is_walk []
0 < n
n \<le> length []

goal (3 subgoals):
 1. \<And>n. \<lbrakk>is_walk []; 0 < n; n \<le> length []\<rbrakk> \<Longrightarrow> is_walk (take n [])
 2. \<And>x n. \<lbrakk>is_walk [x]; 0 < n; n \<le> length [x]\<rbrakk> \<Longrightarrow> is_walk (take n [x])
 3. \<And>x y ys n. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); 0 < n; n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (y # ys)); is_walk (x # y # ys); 0 < n; n \<le> length (x # y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (x # y # ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_walk []
0 < n
n \<le> length []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
is_walk []
0 < n
n \<le> length []

goal (1 subgoal):
 1. is_walk (take n [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_walk (take n [])

goal (2 subgoals):
 1. \<And>x n. \<lbrakk>is_walk [x]; 0 < n; n \<le> length [x]\<rbrakk> \<Longrightarrow> is_walk (take n [x])
 2. \<And>x y ys n. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); 0 < n; n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (y # ys)); is_walk (x # y # ys); 0 < n; n \<le> length (x # y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (x # y # ys))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x n. \<lbrakk>is_walk [x]; 0 < n; n \<le> length [x]\<rbrakk> \<Longrightarrow> is_walk (take n [x])
 2. \<And>x y ys n. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); 0 < n; n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (y # ys)); is_walk (x # y # ys); 0 < n; n \<le> length (x # y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (x # y # ys))
[PROOF STEP]
case (2 x)
[PROOF STATE]
proof (state)
this:
is_walk [x]
0 < n
n \<le> length [x]

goal (2 subgoals):
 1. \<And>x n. \<lbrakk>is_walk [x]; 0 < n; n \<le> length [x]\<rbrakk> \<Longrightarrow> is_walk (take n [x])
 2. \<And>x y ys n. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); 0 < n; n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (y # ys)); is_walk (x # y # ys); 0 < n; n \<le> length (x # y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (x # y # ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_walk [x]
0 < n
n \<le> length [x]
[PROOF STEP]
have "n = 1"
[PROOF STATE]
proof (prove)
using this:
is_walk [x]
0 < n
n \<le> length [x]

goal (1 subgoal):
 1. n = 1
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
is_walk [x]
0 < n
n \<le> length [x]
is_walk [x]
0 < n
n \<le> length [x]

goal (1 subgoal):
 1. n = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n = 1

goal (2 subgoals):
 1. \<And>x n. \<lbrakk>is_walk [x]; 0 < n; n \<le> length [x]\<rbrakk> \<Longrightarrow> is_walk (take n [x])
 2. \<And>x y ys n. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); 0 < n; n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (y # ys)); is_walk (x # y # ys); 0 < n; n \<le> length (x # y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (x # y # ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = 1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
n = 1

goal (1 subgoal):
 1. is_walk (take n [x])
[PROOF STEP]
by (simp add: "2.prems"(1))
[PROOF STATE]
proof (state)
this:
is_walk (take n [x])

goal (1 subgoal):
 1. \<And>x y ys n. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); 0 < n; n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (y # ys)); is_walk (x # y # ys); 0 < n; n \<le> length (x # y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (x # y # ys))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y ys n. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); 0 < n; n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (y # ys)); is_walk (x # y # ys); 0 < n; n \<le> length (x # y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (x # y # ys))
[PROOF STEP]
case (3 x y ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_walk (y # ys); 0 < ?n; ?n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (take ?n (y # ys))
is_walk (x # y # ys)
0 < n
n \<le> length (x # y # ys)

goal (1 subgoal):
 1. \<And>x y ys n. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); 0 < n; n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (y # ys)); is_walk (x # y # ys); 0 < n; n \<le> length (x # y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (x # y # ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>is_walk (y # ys); 0 < ?n; ?n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (take ?n (y # ys))
is_walk (x # y # ys)
0 < n
n \<le> length (x # y # ys)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_walk (y # ys); 0 < ?n; ?n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (take ?n (y # ys))
is_walk (x # y # ys)
0 < n
n \<le> length (x # y # ys)

goal (1 subgoal):
 1. is_walk (take n (x # y # ys))
[PROOF STEP]
proof (cases "n = 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); 0 < n; n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (y # ys)); is_walk (x # y # ys); 0 < n; n \<le> length (x # y # ys); n = 1\<rbrakk> \<Longrightarrow> is_walk (take n (x # y # ys))
 2. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); 0 < n; n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (y # ys)); is_walk (x # y # ys); 0 < n; n \<le> length (x # y # ys); n \<noteq> 1\<rbrakk> \<Longrightarrow> is_walk (take n (x # y # ys))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n = 1

goal (2 subgoals):
 1. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); 0 < n; n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (y # ys)); is_walk (x # y # ys); 0 < n; n \<le> length (x # y # ys); n = 1\<rbrakk> \<Longrightarrow> is_walk (take n (x # y # ys))
 2. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); 0 < n; n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (y # ys)); is_walk (x # y # ys); 0 < n; n \<le> length (x # y # ys); n \<noteq> 1\<rbrakk> \<Longrightarrow> is_walk (take n (x # y # ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = 1
[PROOF STEP]
have "take n (x # y # ys) = [x]"
[PROOF STATE]
proof (prove)
using this:
n = 1

goal (1 subgoal):
 1. take n (x # y # ys) = [x]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
take n (x # y # ys) = [x]

goal (2 subgoals):
 1. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); 0 < n; n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (y # ys)); is_walk (x # y # ys); 0 < n; n \<le> length (x # y # ys); n = 1\<rbrakk> \<Longrightarrow> is_walk (take n (x # y # ys))
 2. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); 0 < n; n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (y # ys)); is_walk (x # y # ys); 0 < n; n \<le> length (x # y # ys); n \<noteq> 1\<rbrakk> \<Longrightarrow> is_walk (take n (x # y # ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
take n (x # y # ys) = [x]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
take n (x # y # ys) = [x]

goal (1 subgoal):
 1. is_walk (take n (x # y # ys))
[PROOF STEP]
using is_walk_def "3.prems"(1)
[PROOF STATE]
proof (prove)
using this:
take n (x # y # ys) = [x]
is_walk ?xs \<equiv> set ?xs \<subseteq> V \<and> set (walk_edges ?xs) \<subseteq> E \<and> ?xs \<noteq> []
is_walk (x # y # ys)

goal (1 subgoal):
 1. is_walk (take n (x # y # ys))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_walk (take n (x # y # ys))

goal (1 subgoal):
 1. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); 0 < n; n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (y # ys)); is_walk (x # y # ys); 0 < n; n \<le> length (x # y # ys); n \<noteq> 1\<rbrakk> \<Longrightarrow> is_walk (take n (x # y # ys))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); 0 < n; n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (y # ys)); is_walk (x # y # ys); 0 < n; n \<le> length (x # y # ys); n \<noteq> 1\<rbrakk> \<Longrightarrow> is_walk (take n (x # y # ys))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> 1

goal (1 subgoal):
 1. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); 0 < n; n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (y # ys)); is_walk (x # y # ys); 0 < n; n \<le> length (x # y # ys); n \<noteq> 1\<rbrakk> \<Longrightarrow> is_walk (take n (x # y # ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<noteq> 1
[PROOF STEP]
have ngt: "n \<ge> 2"
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 1

goal (1 subgoal):
 1. 2 \<le> n
[PROOF STEP]
using "3.prems"(2)
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 1
0 < n

goal (1 subgoal):
 1. 2 \<le> n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 \<le> n

goal (1 subgoal):
 1. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); 0 < n; n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (y # ys)); is_walk (x # y # ys); 0 < n; n \<le> length (x # y # ys); n \<noteq> 1\<rbrakk> \<Longrightarrow> is_walk (take n (x # y # ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 \<le> n
[PROOF STEP]
have tk_split1: "take n (x # y # ys) = x # take (n - 1) (y # ys)"
[PROOF STATE]
proof (prove)
using this:
2 \<le> n

goal (1 subgoal):
 1. take n (x # y # ys) = x # take (n - 1) (y # ys)
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
2 \<le> n
\<lbrakk>is_walk (y # ys); 0 < ?n; ?n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (take ?n (y # ys))
is_walk (x # y # ys)
0 < n
n \<le> length (x # y # ys)

goal (1 subgoal):
 1. take n (x # y # ys) = x # take (n - 1) (y # ys)
[PROOF STEP]
by (simp add: take_Cons')
[PROOF STATE]
proof (state)
this:
take n (x # y # ys) = x # take (n - 1) (y # ys)

goal (1 subgoal):
 1. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); 0 < n; n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (y # ys)); is_walk (x # y # ys); 0 < n; n \<le> length (x # y # ys); n \<noteq> 1\<rbrakk> \<Longrightarrow> is_walk (take n (x # y # ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
take n (x # y # ys) = x # take (n - 1) (y # ys)
[PROOF STEP]
have tk_split: "take n (x # y # ys) = x # y # (take (n - 2) ys)"
[PROOF STATE]
proof (prove)
using this:
take n (x # y # ys) = x # take (n - 1) (y # ys)

goal (1 subgoal):
 1. take n (x # y # ys) = x # y # take (n - 2) ys
[PROOF STEP]
using 3 ngt take_Cons'[of "n -1" "y" "ys"]
[PROOF STATE]
proof (prove)
using this:
take n (x # y # ys) = x # take (n - 1) (y # ys)
\<lbrakk>is_walk (y # ys); 0 < ?n; ?n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (take ?n (y # ys))
is_walk (x # y # ys)
0 < n
n \<le> length (x # y # ys)
2 \<le> n
take (n - 1) (y # ys) = (if n - 1 = 0 then [] else y # take (n - 1 - 1) ys)

goal (1 subgoal):
 1. take n (x # y # ys) = x # y # take (n - 2) ys
[PROOF STEP]
by (metis False diff_diff_left less_one nat_neq_iff one_add_one zero_less_diff)
[PROOF STATE]
proof (state)
this:
take n (x # y # ys) = x # y # take (n - 2) ys

goal (1 subgoal):
 1. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); 0 < n; n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (y # ys)); is_walk (x # y # ys); 0 < n; n \<le> length (x # y # ys); n \<noteq> 1\<rbrakk> \<Longrightarrow> is_walk (take n (x # y # ys))
[PROOF STEP]
have w: "is_walk (y # ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_walk (y # ys)
[PROOF STEP]
using is_walk_tl
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>2 \<le> length ?xs; is_walk ?xs\<rbrakk> \<Longrightarrow> is_walk (tl ?xs)

goal (1 subgoal):
 1. is_walk (y # ys)
[PROOF STEP]
using "3.prems"(1) is_walk_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>2 \<le> length ?xs; is_walk ?xs\<rbrakk> \<Longrightarrow> is_walk (tl ?xs)
is_walk (x # y # ys)
is_walk ?xs \<equiv> set ?xs \<subseteq> V \<and> set (walk_edges ?xs) \<subseteq> E \<and> ?xs \<noteq> []

goal (1 subgoal):
 1. is_walk (y # ys)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
is_walk (y # ys)

goal (1 subgoal):
 1. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); 0 < n; n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (y # ys)); is_walk (x # y # ys); 0 < n; n \<le> length (x # y # ys); n \<noteq> 1\<rbrakk> \<Longrightarrow> is_walk (take n (x # y # ys))
[PROOF STEP]
have "n - 1 \<le> length (y # ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n - 1 \<le> length (y # ys)
[PROOF STEP]
using "3.prems"(3)
[PROOF STATE]
proof (prove)
using this:
n \<le> length (x # y # ys)

goal (1 subgoal):
 1. n - 1 \<le> length (y # ys)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n - 1 \<le> length (y # ys)

goal (1 subgoal):
 1. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); 0 < n; n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (y # ys)); is_walk (x # y # ys); 0 < n; n \<le> length (x # y # ys); n \<noteq> 1\<rbrakk> \<Longrightarrow> is_walk (take n (x # y # ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n - 1 \<le> length (y # ys)
[PROOF STEP]
have w_tl: "is_walk (take (n - 1) (y # ys))"
[PROOF STATE]
proof (prove)
using this:
n - 1 \<le> length (y # ys)

goal (1 subgoal):
 1. is_walk (take (n - 1) (y # ys))
[PROOF STEP]
using "3.hyps"[of "n - 1"] w "3.prems" ngt
[PROOF STATE]
proof (prove)
using this:
n - 1 \<le> length (y # ys)
\<lbrakk>is_walk (y # ys); 0 < n - 1; n - 1 \<le> length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (take (n - 1) (y # ys))
is_walk (y # ys)
is_walk (x # y # ys)
0 < n
n \<le> length (x # y # ys)
2 \<le> n

goal (1 subgoal):
 1. is_walk (take (n - 1) (y # ys))
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
is_walk (take (n - 1) (y # ys))

goal (1 subgoal):
 1. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); 0 < n; n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (y # ys)); is_walk (x # y # ys); 0 < n; n \<le> length (x # y # ys); n \<noteq> 1\<rbrakk> \<Longrightarrow> is_walk (take n (x # y # ys))
[PROOF STEP]
have "{x, y} \<in> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x, y} \<in> E
[PROOF STEP]
using is_walk_def walk_edges.simps "3.prems"(1)
[PROOF STATE]
proof (prove)
using this:
is_walk ?xs \<equiv> set ?xs \<subseteq> V \<and> set (walk_edges ?xs) \<subseteq> E \<and> ?xs \<noteq> []
walk_edges [] = []
walk_edges [?x] = []
walk_edges (?x # ?y # ?ys) = {?x, ?y} # walk_edges (?y # ?ys)
is_walk (x # y # ys)

goal (1 subgoal):
 1. {x, y} \<in> E
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x, y} \<in> E

goal (1 subgoal):
 1. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); 0 < n; n \<le> length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (take n (y # ys)); is_walk (x # y # ys); 0 < n; n \<le> length (x # y # ys); n \<noteq> 1\<rbrakk> \<Longrightarrow> is_walk (take n (x # y # ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{x, y} \<in> E
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{x, y} \<in> E

goal (1 subgoal):
 1. is_walk (take n (x # y # ys))
[PROOF STEP]
using is_walk_hd_tl[of y "(take (n - 2) ys)" x] tk_split
[PROOF STATE]
proof (prove)
using this:
{x, y} \<in> E
\<lbrakk>is_walk (y # take (n - 2) ys); {x, y} \<in> E\<rbrakk> \<Longrightarrow> is_walk (x # y # take (n - 2) ys)
take n (x # y # ys) = x # y # take (n - 2) ys

goal (1 subgoal):
 1. is_walk (take n (x # y # ys))
[PROOF STEP]
using tk_split1 w_tl
[PROOF STATE]
proof (prove)
using this:
{x, y} \<in> E
\<lbrakk>is_walk (y # take (n - 2) ys); {x, y} \<in> E\<rbrakk> \<Longrightarrow> is_walk (x # y # take (n - 2) ys)
take n (x # y # ys) = x # y # take (n - 2) ys
take n (x # y # ys) = x # take (n - 1) (y # ys)
is_walk (take (n - 1) (y # ys))

goal (1 subgoal):
 1. is_walk (take n (x # y # ys))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
is_walk (take n (x # y # ys))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_walk (take n (x # y # ys))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_walk_drop:
  assumes "is_walk w"
  assumes "n < length w"
  shows "is_walk (drop n w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_walk (drop n w)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_walk w
n < length w

goal (1 subgoal):
 1. is_walk (drop n w)
[PROOF STEP]
proof (induct w arbitrary: n rule: walk_edges.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>is_walk []; n < length []\<rbrakk> \<Longrightarrow> is_walk (drop n [])
 2. \<And>x n. \<lbrakk>is_walk [x]; n < length [x]\<rbrakk> \<Longrightarrow> is_walk (drop n [x])
 3. \<And>x y ys n. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
is_walk []
n < length []

goal (3 subgoals):
 1. \<And>n. \<lbrakk>is_walk []; n < length []\<rbrakk> \<Longrightarrow> is_walk (drop n [])
 2. \<And>x n. \<lbrakk>is_walk [x]; n < length [x]\<rbrakk> \<Longrightarrow> is_walk (drop n [x])
 3. \<And>x y ys n. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_walk []
n < length []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
is_walk []
n < length []

goal (1 subgoal):
 1. is_walk (drop n [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_walk (drop n [])

goal (2 subgoals):
 1. \<And>x n. \<lbrakk>is_walk [x]; n < length [x]\<rbrakk> \<Longrightarrow> is_walk (drop n [x])
 2. \<And>x y ys n. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x n. \<lbrakk>is_walk [x]; n < length [x]\<rbrakk> \<Longrightarrow> is_walk (drop n [x])
 2. \<And>x y ys n. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
[PROOF STEP]
case (2 x)
[PROOF STATE]
proof (state)
this:
is_walk [x]
n < length [x]

goal (2 subgoals):
 1. \<And>x n. \<lbrakk>is_walk [x]; n < length [x]\<rbrakk> \<Longrightarrow> is_walk (drop n [x])
 2. \<And>x y ys n. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_walk [x]
n < length [x]
[PROOF STEP]
have "n = 0"
[PROOF STATE]
proof (prove)
using this:
is_walk [x]
n < length [x]

goal (1 subgoal):
 1. n = 0
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
is_walk [x]
n < length [x]
is_walk [x]
n < length [x]

goal (1 subgoal):
 1. n = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n = 0

goal (2 subgoals):
 1. \<And>x n. \<lbrakk>is_walk [x]; n < length [x]\<rbrakk> \<Longrightarrow> is_walk (drop n [x])
 2. \<And>x y ys n. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = 0
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
n = 0

goal (1 subgoal):
 1. is_walk (drop n [x])
[PROOF STEP]
by (simp add: "2.prems"(1))
[PROOF STATE]
proof (state)
this:
is_walk (drop n [x])

goal (1 subgoal):
 1. \<And>x y ys n. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y ys n. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
[PROOF STEP]
case (3 x y ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_walk (y # ys); ?n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop ?n (y # ys))
is_walk (x # y # ys)
n < length (x # y # ys)

goal (1 subgoal):
 1. \<And>x y ys n. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>is_walk (y # ys); ?n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop ?n (y # ys))
is_walk (x # y # ys)
n < length (x # y # ys)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_walk (y # ys); ?n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop ?n (y # ys))
is_walk (x # y # ys)
n < length (x # y # ys)

goal (1 subgoal):
 1. is_walk (drop n (x # y # ys))
[PROOF STEP]
proof (cases "n \<ge> 2")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys); 2 \<le> n\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
 2. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys); \<not> 2 \<le> n\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
2 \<le> n

goal (2 subgoals):
 1. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys); 2 \<le> n\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
 2. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys); \<not> 2 \<le> n\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 \<le> n
[PROOF STEP]
have ngt: "n \<ge> 2"
[PROOF STATE]
proof (prove)
using this:
2 \<le> n

goal (1 subgoal):
 1. 2 \<le> n
[PROOF STEP]
using "3.prems"(2)
[PROOF STATE]
proof (prove)
using this:
2 \<le> n
n < length (x # y # ys)

goal (1 subgoal):
 1. 2 \<le> n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 \<le> n

goal (2 subgoals):
 1. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys); 2 \<le> n\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
 2. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys); \<not> 2 \<le> n\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 \<le> n
[PROOF STEP]
have tk_split1: "drop n (x # y # ys) = drop (n - 1) (y # ys)"
[PROOF STATE]
proof (prove)
using this:
2 \<le> n

goal (1 subgoal):
 1. drop n (x # y # ys) = drop (n - 1) (y # ys)
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
2 \<le> n
\<lbrakk>is_walk (y # ys); ?n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop ?n (y # ys))
is_walk (x # y # ys)
n < length (x # y # ys)

goal (1 subgoal):
 1. drop n (x # y # ys) = drop (n - 1) (y # ys)
[PROOF STEP]
by (simp add: drop_Cons')
[PROOF STATE]
proof (state)
this:
drop n (x # y # ys) = drop (n - 1) (y # ys)

goal (2 subgoals):
 1. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys); 2 \<le> n\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
 2. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys); \<not> 2 \<le> n\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
drop n (x # y # ys) = drop (n - 1) (y # ys)
[PROOF STEP]
have tk_split: "drop n (x # y # ys) = (drop (n - 2) ys)"
[PROOF STATE]
proof (prove)
using this:
drop n (x # y # ys) = drop (n - 1) (y # ys)

goal (1 subgoal):
 1. drop n (x # y # ys) = drop (n - 2) ys
[PROOF STEP]
using 3 ngt drop_Cons'[of "n -1" "y" "ys"] True
[PROOF STATE]
proof (prove)
using this:
drop n (x # y # ys) = drop (n - 1) (y # ys)
\<lbrakk>is_walk (y # ys); ?n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop ?n (y # ys))
is_walk (x # y # ys)
n < length (x # y # ys)
2 \<le> n
drop (n - 1) (y # ys) = (if n - 1 = 0 then y # ys else drop (n - 1 - 1) ys)
2 \<le> n

goal (1 subgoal):
 1. drop n (x # y # ys) = drop (n - 2) ys
[PROOF STEP]
by (metis Suc_1 Suc_le_eq diff_diff_left less_not_refl nat_1_add_1 zero_less_diff)
[PROOF STATE]
proof (state)
this:
drop n (x # y # ys) = drop (n - 2) ys

goal (2 subgoals):
 1. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys); 2 \<le> n\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
 2. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys); \<not> 2 \<le> n\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
[PROOF STEP]
have w: "is_walk (y # ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_walk (y # ys)
[PROOF STEP]
using is_walk_tl
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>2 \<le> length ?xs; is_walk ?xs\<rbrakk> \<Longrightarrow> is_walk (tl ?xs)

goal (1 subgoal):
 1. is_walk (y # ys)
[PROOF STEP]
using "3.prems"(1) is_walk_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>2 \<le> length ?xs; is_walk ?xs\<rbrakk> \<Longrightarrow> is_walk (tl ?xs)
is_walk (x # y # ys)
is_walk ?xs \<equiv> set ?xs \<subseteq> V \<and> set (walk_edges ?xs) \<subseteq> E \<and> ?xs \<noteq> []

goal (1 subgoal):
 1. is_walk (y # ys)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
is_walk (y # ys)

goal (2 subgoals):
 1. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys); 2 \<le> n\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
 2. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys); \<not> 2 \<le> n\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
[PROOF STEP]
have "n - 1 < length (y # ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n - 1 < length (y # ys)
[PROOF STEP]
using "3.prems"(2)
[PROOF STATE]
proof (prove)
using this:
n < length (x # y # ys)

goal (1 subgoal):
 1. n - 1 < length (y # ys)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n - 1 < length (y # ys)

goal (2 subgoals):
 1. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys); 2 \<le> n\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
 2. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys); \<not> 2 \<le> n\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n - 1 < length (y # ys)
[PROOF STEP]
have w_tl: "is_walk (drop (n - 1) (y # ys))"
[PROOF STATE]
proof (prove)
using this:
n - 1 < length (y # ys)

goal (1 subgoal):
 1. is_walk (drop (n - 1) (y # ys))
[PROOF STEP]
using "3.hyps"[of "n - 1"] w "3.prems" ngt
[PROOF STATE]
proof (prove)
using this:
n - 1 < length (y # ys)
\<lbrakk>is_walk (y # ys); n - 1 < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop (n - 1) (y # ys))
is_walk (y # ys)
is_walk (x # y # ys)
n < length (x # y # ys)
2 \<le> n

goal (1 subgoal):
 1. is_walk (drop (n - 1) (y # ys))
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
is_walk (drop (n - 1) (y # ys))

goal (2 subgoals):
 1. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys); 2 \<le> n\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
 2. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys); \<not> 2 \<le> n\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
[PROOF STEP]
have "{x, y} \<in> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x, y} \<in> E
[PROOF STEP]
using is_walk_def walk_edges.simps "3.prems"(1)
[PROOF STATE]
proof (prove)
using this:
is_walk ?xs \<equiv> set ?xs \<subseteq> V \<and> set (walk_edges ?xs) \<subseteq> E \<and> ?xs \<noteq> []
walk_edges [] = []
walk_edges [?x] = []
walk_edges (?x # ?y # ?ys) = {?x, ?y} # walk_edges (?y # ?ys)
is_walk (x # y # ys)

goal (1 subgoal):
 1. {x, y} \<in> E
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x, y} \<in> E

goal (2 subgoals):
 1. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys); 2 \<le> n\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
 2. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys); \<not> 2 \<le> n\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{x, y} \<in> E
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{x, y} \<in> E

goal (1 subgoal):
 1. is_walk (drop n (x # y # ys))
[PROOF STEP]
using is_walk_hd_tl[of y "(take (n - 2) ys)" x] tk_split
[PROOF STATE]
proof (prove)
using this:
{x, y} \<in> E
\<lbrakk>is_walk (y # take (n - 2) ys); {x, y} \<in> E\<rbrakk> \<Longrightarrow> is_walk (x # y # take (n - 2) ys)
drop n (x # y # ys) = drop (n - 2) ys

goal (1 subgoal):
 1. is_walk (drop n (x # y # ys))
[PROOF STEP]
using tk_split1 w_tl
[PROOF STATE]
proof (prove)
using this:
{x, y} \<in> E
\<lbrakk>is_walk (y # take (n - 2) ys); {x, y} \<in> E\<rbrakk> \<Longrightarrow> is_walk (x # y # take (n - 2) ys)
drop n (x # y # ys) = drop (n - 2) ys
drop n (x # y # ys) = drop (n - 1) (y # ys)
is_walk (drop (n - 1) (y # ys))

goal (1 subgoal):
 1. is_walk (drop n (x # y # ys))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
is_walk (drop n (x # y # ys))

goal (1 subgoal):
 1. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys); \<not> 2 \<le> n\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys); \<not> 2 \<le> n\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 2 \<le> n

goal (1 subgoal):
 1. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys); \<not> 2 \<le> n\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> 2 \<le> n
[PROOF STEP]
have or: "n = 0 \<or> n = 1"
[PROOF STATE]
proof (prove)
using this:
\<not> 2 \<le> n

goal (1 subgoal):
 1. n = 0 \<or> n = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n = 0 \<or> n = 1

goal (1 subgoal):
 1. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys); \<not> 2 \<le> n\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
[PROOF STEP]
have walk: "is_walk (y # ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_walk (y # ys)
[PROOF STEP]
using is_walk_drop_hd 3
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?ys \<noteq> []; is_walk (?y # ?ys)\<rbrakk> \<Longrightarrow> is_walk ?ys
\<lbrakk>is_walk (y # ys); ?n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop ?n (y # ys))
is_walk (x # y # ys)
n < length (x # y # ys)

goal (1 subgoal):
 1. is_walk (y # ys)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_walk (y # ys)

goal (1 subgoal):
 1. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys); \<not> 2 \<le> n\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
[PROOF STEP]
have n0: "n = 0 \<Longrightarrow> (drop n (x # y # ys)) = (x # y # ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = 0 \<Longrightarrow> drop n (x # y # ys) = x # y # ys
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n = 0 \<Longrightarrow> drop n (x # y # ys) = x # y # ys

goal (1 subgoal):
 1. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys); \<not> 2 \<le> n\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
[PROOF STEP]
have "n = 1 \<Longrightarrow> (drop n (x # y # ys)) = y # ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = 1 \<Longrightarrow> drop n (x # y # ys) = y # ys
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n = 1 \<Longrightarrow> drop n (x # y # ys) = y # ys

goal (1 subgoal):
 1. \<lbrakk>\<And>n. \<lbrakk>is_walk (y # ys); n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop n (y # ys)); is_walk (x # y # ys); n < length (x # y # ys); \<not> 2 \<le> n\<rbrakk> \<Longrightarrow> is_walk (drop n (x # y # ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = 1 \<Longrightarrow> drop n (x # y # ys) = y # ys
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n = 1 \<Longrightarrow> drop n (x # y # ys) = y # ys

goal (1 subgoal):
 1. is_walk (drop n (x # y # ys))
[PROOF STEP]
using n0 3 walk or
[PROOF STATE]
proof (prove)
using this:
n = 1 \<Longrightarrow> drop n (x # y # ys) = y # ys
n = 0 \<Longrightarrow> drop n (x # y # ys) = x # y # ys
\<lbrakk>is_walk (y # ys); ?n < length (y # ys)\<rbrakk> \<Longrightarrow> is_walk (drop ?n (y # ys))
is_walk (x # y # ys)
n < length (x # y # ys)
is_walk (y # ys)
n = 0 \<or> n = 1

goal (1 subgoal):
 1. is_walk (drop n (x # y # ys))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_walk (drop n (x # y # ys))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_walk (drop n (x # y # ys))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_open_walk_rev: "is_open_walk xs \<longleftrightarrow> is_open_walk (rev xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_open_walk xs = is_open_walk (rev xs)
[PROOF STEP]
unfolding is_open_walk_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (is_walk xs \<and> hd xs \<noteq> last xs) = (is_walk (rev xs) \<and> hd (rev xs) \<noteq> last (rev xs))
[PROOF STEP]
using is_walk_rev
[PROOF STATE]
proof (prove)
using this:
is_walk ?xs = is_walk (rev ?xs)

goal (1 subgoal):
 1. (is_walk xs \<and> hd xs \<noteq> last xs) = (is_walk (rev xs) \<and> hd (rev xs) \<noteq> last (rev xs))
[PROOF STEP]
by (metis hd_rev last_rev)


[STATEMENT]
lemma is_closed_walk_rev: "is_closed_walk xs \<longleftrightarrow> is_closed_walk (rev xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_closed_walk xs = is_closed_walk (rev xs)
[PROOF STEP]
unfolding is_closed_walk_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (is_walk xs \<and> hd xs = last xs) = (is_walk (rev xs) \<and> hd (rev xs) = last (rev xs))
[PROOF STEP]
using is_walk_rev
[PROOF STATE]
proof (prove)
using this:
is_walk ?xs = is_walk (rev ?xs)

goal (1 subgoal):
 1. (is_walk xs \<and> hd xs = last xs) = (is_walk (rev xs) \<and> hd (rev xs) = last (rev xs))
[PROOF STEP]
by (metis hd_rev last_rev)


[STATEMENT]
lemma is_trail_rev: "is_trail xs \<longleftrightarrow> is_trail (rev xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_trail xs = is_trail (rev xs)
[PROOF STEP]
unfolding is_trail_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (is_walk xs \<and> distinct (walk_edges xs)) = (is_walk (rev xs) \<and> distinct (walk_edges (rev xs)))
[PROOF STEP]
using is_walk_rev
[PROOF STATE]
proof (prove)
using this:
is_walk ?xs = is_walk (rev ?xs)

goal (1 subgoal):
 1. (is_walk xs \<and> distinct (walk_edges xs)) = (is_walk (rev xs) \<and> distinct (walk_edges (rev xs)))
[PROOF STEP]
by (metis distinct_rev walk_edges_rev)


[STATEMENT]
lemma is_path_rev: "is_path xs \<longleftrightarrow> is_path (rev xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path xs = is_path (rev xs)
[PROOF STEP]
unfolding is_path_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (is_open_walk xs \<and> distinct xs) = (is_open_walk (rev xs) \<and> distinct (rev xs))
[PROOF STEP]
using is_open_walk_rev
[PROOF STATE]
proof (prove)
using this:
is_open_walk ?xs = is_open_walk (rev ?xs)

goal (1 subgoal):
 1. (is_open_walk xs \<and> distinct xs) = (is_open_walk (rev xs) \<and> distinct (rev xs))
[PROOF STEP]
by (metis distinct_rev)


[STATEMENT]
lemma is_path_walk: "is_path xs \<Longrightarrow> is_walk xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path xs \<Longrightarrow> is_walk xs
[PROOF STEP]
unfolding is_path_def is_open_walk_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (is_walk xs \<and> hd xs \<noteq> last xs) \<and> distinct xs \<Longrightarrow> is_walk xs
[PROOF STEP]
by auto


[STATEMENT]
lemma paths_ss_walk: "paths \<subseteq> walks"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paths \<subseteq> walks
[PROOF STEP]
unfolding paths_def walks_def is_path_def is_open_walk_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {p. (is_walk p \<and> hd p \<noteq> last p) \<and> distinct p} \<subseteq> Collect is_walk
[PROOF STEP]
by auto


[STATEMENT]
lemma is_path_gen_path: "is_path p \<Longrightarrow> is_gen_path p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path p \<Longrightarrow> is_gen_path p
[PROOF STEP]
unfolding is_path_def is_gen_path_def is_open_walk_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (is_walk p \<and> hd p \<noteq> last p) \<and> distinct p \<Longrightarrow> is_walk p \<and> (distinct (tl p) \<and> hd p = last p \<or> distinct p)
[PROOF STEP]
by (auto simp add: distinct_tl)


[STATEMENT]
lemma is_gen_path_rev: "is_gen_path p \<longleftrightarrow> is_gen_path (rev p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_gen_path p = is_gen_path (rev p)
[PROOF STEP]
unfolding is_gen_path_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (is_walk p \<and> (distinct (tl p) \<and> hd p = last p \<or> distinct p)) = (is_walk (rev p) \<and> (distinct (tl (rev p)) \<and> hd (rev p) = last (rev p) \<or> distinct (rev p)))
[PROOF STEP]
using is_walk_rev distinct_tl_rev
[PROOF STATE]
proof (prove)
using this:
is_walk ?xs = is_walk (rev ?xs)
hd ?xs = last ?xs \<Longrightarrow> distinct (tl ?xs) = distinct (tl (rev ?xs))

goal (1 subgoal):
 1. (is_walk p \<and> (distinct (tl p) \<and> hd p = last p \<or> distinct p)) = (is_walk (rev p) \<and> (distinct (tl (rev p)) \<and> hd (rev p) = last (rev p) \<or> distinct (rev p)))
[PROOF STEP]
by (metis distinct_rev hd_rev last_rev)


[STATEMENT]
lemma is_gen_path_distinct: "is_gen_path p \<Longrightarrow> hd p \<noteq> last p \<Longrightarrow> distinct p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_gen_path p; hd p \<noteq> last p\<rbrakk> \<Longrightarrow> distinct p
[PROOF STEP]
unfolding is_gen_path_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_walk p \<and> (distinct (tl p) \<and> hd p = last p \<or> distinct p); hd p \<noteq> last p\<rbrakk> \<Longrightarrow> distinct p
[PROOF STEP]
by auto


[STATEMENT]
lemma is_gen_path_distinct_tl:
  assumes "is_gen_path p" and "hd p = last p"
  shows "distinct (tl p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (tl p)
[PROOF STEP]
proof (cases "length p > 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 1 < length p \<Longrightarrow> distinct (tl p)
 2. \<not> 1 < length p \<Longrightarrow> distinct (tl p)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
1 < length p

goal (2 subgoals):
 1. 1 < length p \<Longrightarrow> distinct (tl p)
 2. \<not> 1 < length p \<Longrightarrow> distinct (tl p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 < length p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
1 < length p

goal (1 subgoal):
 1. distinct (tl p)
[PROOF STEP]
using assms(1) distinct_tl is_gen_path_def
[PROOF STATE]
proof (prove)
using this:
1 < length p
is_gen_path p
distinct ?xs \<Longrightarrow> distinct (tl ?xs)
is_gen_path ?p \<equiv> is_walk ?p \<and> (distinct (tl ?p) \<and> hd ?p = last ?p \<or> distinct ?p)

goal (1 subgoal):
 1. distinct (tl p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct (tl p)

goal (1 subgoal):
 1. \<not> 1 < length p \<Longrightarrow> distinct (tl p)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 1 < length p \<Longrightarrow> distinct (tl p)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 1 < length p

goal (1 subgoal):
 1. \<not> 1 < length p \<Longrightarrow> distinct (tl p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> 1 < length p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> 1 < length p

goal (1 subgoal):
 1. distinct (tl p)
[PROOF STEP]
using assms(1) distinct_tl is_gen_path_def
[PROOF STATE]
proof (prove)
using this:
\<not> 1 < length p
is_gen_path p
distinct ?xs \<Longrightarrow> distinct (tl ?xs)
is_gen_path ?p \<equiv> is_walk ?p \<and> (distinct (tl ?p) \<and> hd ?p = last ?p \<or> distinct ?p)

goal (1 subgoal):
 1. distinct (tl p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct (tl p)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_gen_path_trivial: "x \<in> V \<Longrightarrow> is_gen_path [x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> V \<Longrightarrow> is_gen_path [x]
[PROOF STEP]
unfolding is_gen_path_def is_walk_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> V \<Longrightarrow> (set [x] \<subseteq> V \<and> set (walk_edges [x]) \<subseteq> E \<and> [x] \<noteq> []) \<and> (distinct (tl [x]) \<and> hd [x] = last [x] \<or> distinct [x])
[PROOF STEP]
by simp


[STATEMENT]
lemma gen_paths_ss_walks: "gen_paths \<subseteq> walks"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gen_paths \<subseteq> walks
[PROOF STEP]
unfolding gen_paths_def walks_def is_gen_path_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {p. is_walk p \<and> (distinct (tl p) \<and> hd p = last p \<or> distinct p)} \<subseteq> Collect is_walk
[PROOF STEP]
by auto


[STATEMENT]
lemma is_gen_path_cycle: "is_cycle p \<Longrightarrow> is_gen_path p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_cycle p \<Longrightarrow> is_gen_path p
[PROOF STEP]
unfolding is_cycle_def is_gen_path_def is_closed_walk_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (is_walk p \<and> hd p = last p) \<and> 1 \<le> walk_length p \<and> distinct (tl p) \<Longrightarrow> is_walk p \<and> (distinct (tl p) \<and> hd p = last p \<or> distinct p)
[PROOF STEP]
by auto


[STATEMENT]
lemma is_cycle_alt_gen_path: "is_cycle xs \<longleftrightarrow> is_gen_path xs \<and> walk_length xs \<ge> 1 \<and> hd xs = last xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_cycle xs = (is_gen_path xs \<and> 1 \<le> walk_length xs \<and> hd xs = last xs)
[PROOF STEP]
proof (intro iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_cycle xs \<Longrightarrow> is_gen_path xs \<and> 1 \<le> walk_length xs \<and> hd xs = last xs
 2. is_gen_path xs \<and> 1 \<le> walk_length xs \<and> hd xs = last xs \<Longrightarrow> is_cycle xs
[PROOF STEP]
show "is_cycle xs \<Longrightarrow> is_gen_path xs \<and> 1 \<le> walk_length xs \<and> hd xs = last xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_cycle xs \<Longrightarrow> is_gen_path xs \<and> 1 \<le> walk_length xs \<and> hd xs = last xs
[PROOF STEP]
using is_gen_path_cycle is_cycle_def is_closed_walk_def
[PROOF STATE]
proof (prove)
using this:
is_cycle ?p \<Longrightarrow> is_gen_path ?p
is_cycle ?xs \<equiv> is_closed_walk ?xs \<and> 1 \<le> walk_length ?xs \<and> distinct (tl ?xs)
is_closed_walk ?xs \<equiv> is_walk ?xs \<and> hd ?xs = last ?xs

goal (1 subgoal):
 1. is_cycle xs \<Longrightarrow> is_gen_path xs \<and> 1 \<le> walk_length xs \<and> hd xs = last xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_cycle xs \<Longrightarrow> is_gen_path xs \<and> 1 \<le> walk_length xs \<and> hd xs = last xs

goal (1 subgoal):
 1. is_gen_path xs \<and> 1 \<le> walk_length xs \<and> hd xs = last xs \<Longrightarrow> is_cycle xs
[PROOF STEP]
show "is_gen_path xs \<and> 1 \<le> walk_length xs \<and> hd xs = last xs \<Longrightarrow> is_cycle xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_gen_path xs \<and> 1 \<le> walk_length xs \<and> hd xs = last xs \<Longrightarrow> is_cycle xs
[PROOF STEP]
using distinct_tl is_closed_walk_def is_cycle_def is_gen_path_def
[PROOF STATE]
proof (prove)
using this:
distinct ?xs \<Longrightarrow> distinct (tl ?xs)
is_closed_walk ?xs \<equiv> is_walk ?xs \<and> hd ?xs = last ?xs
is_cycle ?xs \<equiv> is_closed_walk ?xs \<and> 1 \<le> walk_length ?xs \<and> distinct (tl ?xs)
is_gen_path ?p \<equiv> is_walk ?p \<and> (distinct (tl ?p) \<and> hd ?p = last ?p \<or> distinct ?p)

goal (1 subgoal):
 1. is_gen_path xs \<and> 1 \<le> walk_length xs \<and> hd xs = last xs \<Longrightarrow> is_cycle xs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_gen_path xs \<and> 1 \<le> walk_length xs \<and> hd xs = last xs \<Longrightarrow> is_cycle xs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_cycle_alt: "is_cycle xs \<longleftrightarrow> is_walk xs \<and> distinct (tl xs) \<and> walk_length xs \<ge> 1 \<and> hd xs = last xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_cycle xs = (is_walk xs \<and> distinct (tl xs) \<and> 1 \<le> walk_length xs \<and> hd xs = last xs)
[PROOF STEP]
proof (intro iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_cycle xs \<Longrightarrow> is_walk xs \<and> distinct (tl xs) \<and> 1 \<le> walk_length xs \<and> hd xs = last xs
 2. is_walk xs \<and> distinct (tl xs) \<and> 1 \<le> walk_length xs \<and> hd xs = last xs \<Longrightarrow> is_cycle xs
[PROOF STEP]
show "is_cycle xs \<Longrightarrow> is_walk xs \<and> distinct (tl xs) \<and> 1 \<le> walk_length xs \<and> hd xs = last xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_cycle xs \<Longrightarrow> is_walk xs \<and> distinct (tl xs) \<and> 1 \<le> walk_length xs \<and> hd xs = last xs
[PROOF STEP]
using is_cycle_alt_gen_path is_cycle_def is_gen_path_def
[PROOF STATE]
proof (prove)
using this:
is_cycle ?xs = (is_gen_path ?xs \<and> 1 \<le> walk_length ?xs \<and> hd ?xs = last ?xs)
is_cycle ?xs \<equiv> is_closed_walk ?xs \<and> 1 \<le> walk_length ?xs \<and> distinct (tl ?xs)
is_gen_path ?p \<equiv> is_walk ?p \<and> (distinct (tl ?p) \<and> hd ?p = last ?p \<or> distinct ?p)

goal (1 subgoal):
 1. is_cycle xs \<Longrightarrow> is_walk xs \<and> distinct (tl xs) \<and> 1 \<le> walk_length xs \<and> hd xs = last xs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_cycle xs \<Longrightarrow> is_walk xs \<and> distinct (tl xs) \<and> 1 \<le> walk_length xs \<and> hd xs = last xs

goal (1 subgoal):
 1. is_walk xs \<and> distinct (tl xs) \<and> 1 \<le> walk_length xs \<and> hd xs = last xs \<Longrightarrow> is_cycle xs
[PROOF STEP]
show "is_walk xs \<and> distinct (tl xs) \<and> 1 \<le> walk_length xs \<and> hd xs = last xs \<Longrightarrow> is_cycle xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_walk xs \<and> distinct (tl xs) \<and> 1 \<le> walk_length xs \<and> hd xs = last xs \<Longrightarrow> is_cycle xs
[PROOF STEP]
by (simp add: is_cycle_alt_gen_path is_gen_path_def)
[PROOF STATE]
proof (state)
this:
is_walk xs \<and> distinct (tl xs) \<and> 1 \<le> walk_length xs \<and> hd xs = last xs \<Longrightarrow> is_cycle xs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_cycle_rev: "is_cycle xs \<longleftrightarrow> is_cycle (rev xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_cycle xs = is_cycle (rev xs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_cycle xs = is_cycle (rev xs)
[PROOF STEP]
have len: "1 \<le> walk_length xs \<longleftrightarrow> 1 \<le> walk_length (rev xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 \<le> walk_length xs) = (1 \<le> walk_length (rev xs))
[PROOF STEP]
by (metis length_rev walk_edges_rev walk_length_def)
[PROOF STATE]
proof (state)
this:
(1 \<le> walk_length xs) = (1 \<le> walk_length (rev xs))

goal (1 subgoal):
 1. is_cycle xs = is_cycle (rev xs)
[PROOF STEP]
have "hd xs = last xs \<Longrightarrow> distinct (tl xs) \<longleftrightarrow> distinct (tl (rev xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd xs = last xs \<Longrightarrow> distinct (tl xs) = distinct (tl (rev xs))
[PROOF STEP]
using distinct_tl_rev
[PROOF STATE]
proof (prove)
using this:
hd ?xs = last ?xs \<Longrightarrow> distinct (tl ?xs) = distinct (tl (rev ?xs))

goal (1 subgoal):
 1. hd xs = last xs \<Longrightarrow> distinct (tl xs) = distinct (tl (rev xs))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
hd xs = last xs \<Longrightarrow> distinct (tl xs) = distinct (tl (rev xs))

goal (1 subgoal):
 1. is_cycle xs = is_cycle (rev xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hd xs = last xs \<Longrightarrow> distinct (tl xs) = distinct (tl (rev xs))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
hd xs = last xs \<Longrightarrow> distinct (tl xs) = distinct (tl (rev xs))

goal (1 subgoal):
 1. is_cycle xs = is_cycle (rev xs)
[PROOF STEP]
using len is_cycle_def
[PROOF STATE]
proof (prove)
using this:
hd xs = last xs \<Longrightarrow> distinct (tl xs) = distinct (tl (rev xs))
(1 \<le> walk_length xs) = (1 \<le> walk_length (rev xs))
is_cycle ?xs \<equiv> is_closed_walk ?xs \<and> 1 \<le> walk_length ?xs \<and> distinct (tl ?xs)

goal (1 subgoal):
 1. is_cycle xs = is_cycle (rev xs)
[PROOF STEP]
using is_closed_walk_def is_closed_walk_rev
[PROOF STATE]
proof (prove)
using this:
hd xs = last xs \<Longrightarrow> distinct (tl xs) = distinct (tl (rev xs))
(1 \<le> walk_length xs) = (1 \<le> walk_length (rev xs))
is_cycle ?xs \<equiv> is_closed_walk ?xs \<and> 1 \<le> walk_length ?xs \<and> distinct (tl ?xs)
is_closed_walk ?xs \<equiv> is_walk ?xs \<and> hd ?xs = last ?xs
is_closed_walk ?xs = is_closed_walk (rev ?xs)

goal (1 subgoal):
 1. is_cycle xs = is_cycle (rev xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_cycle xs = is_cycle (rev xs)

goal:
No subgoals!
[PROOF STEP]
qed