[STATEMENT]
lemma [intro!]: "finite (edges G) \<Longrightarrow> finite (edges (rem_unPath ps G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (edges G) \<Longrightarrow> finite (edges (rem_unPath ps G))
[PROOF STEP]
proof (induct ps arbitrary:G)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>G. finite (edges G) \<Longrightarrow> finite (edges (rem_unPath [] G))
 2. \<And>a ps G. \<lbrakk>\<And>G. finite (edges G) \<Longrightarrow> finite (edges (rem_unPath ps G)); finite (edges G)\<rbrakk> \<Longrightarrow> finite (edges (rem_unPath (a # ps) G))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
finite (edges G)

goal (2 subgoals):
 1. \<And>G. finite (edges G) \<Longrightarrow> finite (edges (rem_unPath [] G))
 2. \<And>a ps G. \<lbrakk>\<And>G. finite (edges G) \<Longrightarrow> finite (edges (rem_unPath ps G)); finite (edges G)\<rbrakk> \<Longrightarrow> finite (edges (rem_unPath (a # ps) G))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
finite (edges G)

goal (1 subgoal):
 1. finite (edges (rem_unPath [] G))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (edges (rem_unPath [] G))

goal (1 subgoal):
 1. \<And>a ps G. \<lbrakk>\<And>G. finite (edges G) \<Longrightarrow> finite (edges (rem_unPath ps G)); finite (edges G)\<rbrakk> \<Longrightarrow> finite (edges (rem_unPath (a # ps) G))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ps G. \<lbrakk>\<And>G. finite (edges G) \<Longrightarrow> finite (edges (rem_unPath ps G)); finite (edges G)\<rbrakk> \<Longrightarrow> finite (edges (rem_unPath (a # ps) G))
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
finite (edges ?G) \<Longrightarrow> finite (edges (rem_unPath xs ?G))
finite (edges G)

goal (1 subgoal):
 1. \<And>a ps G. \<lbrakk>\<And>G. finite (edges G) \<Longrightarrow> finite (edges (rem_unPath ps G)); finite (edges G)\<rbrakk> \<Longrightarrow> finite (edges (rem_unPath (a # ps) G))
[PROOF STEP]
hence "finite (edges (rem_unPath (x # xs) G)) = finite (edges (del_unEdge
          (fst x) (fst (snd x)) (snd (snd x)) (rem_unPath xs G)))"
[PROOF STATE]
proof (prove)
using this:
finite (edges ?G) \<Longrightarrow> finite (edges (rem_unPath xs ?G))
finite (edges G)

goal (1 subgoal):
 1. finite (edges (rem_unPath (x # xs) G)) = finite (edges (del_unEdge (fst x) (fst (snd x)) (snd (snd x)) (rem_unPath xs G)))
[PROOF STEP]
by (metis rem_unPath.simps(2) rem_unPath_com surjective_pairing)
[PROOF STATE]
proof (state)
this:
finite (edges (rem_unPath (x # xs) G)) = finite (edges (del_unEdge (fst x) (fst (snd x)) (snd (snd x)) (rem_unPath xs G)))

goal (1 subgoal):
 1. \<And>a ps G. \<lbrakk>\<And>G. finite (edges G) \<Longrightarrow> finite (edges (rem_unPath ps G)); finite (edges G)\<rbrakk> \<Longrightarrow> finite (edges (rem_unPath (a # ps) G))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
finite (edges (rem_unPath (x # xs) G)) = finite (edges (del_unEdge (fst x) (fst (snd x)) (snd (snd x)) (rem_unPath xs G)))

goal (1 subgoal):
 1. \<And>a ps G. \<lbrakk>\<And>G. finite (edges G) \<Longrightarrow> finite (edges (rem_unPath ps G)); finite (edges G)\<rbrakk> \<Longrightarrow> finite (edges (rem_unPath (a # ps) G))
[PROOF STEP]
have "...=finite (edges (rem_unPath xs G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (edges (del_unEdge (fst x) (fst (snd x)) (snd (snd x)) (rem_unPath xs G))) = finite (edges (rem_unPath xs G))
[PROOF STEP]
using del_unEdge_def
[PROOF STATE]
proof (prove)
using this:
del_unEdge ?v ?e ?v' ?g \<equiv> \<lparr>nodes = nodes ?g, edges = edges ?g - {(?v, ?e, ?v'), (?v', ?e, ?v)}\<rparr>

goal (1 subgoal):
 1. finite (edges (del_unEdge (fst x) (fst (snd x)) (snd (snd x)) (rem_unPath xs G))) = finite (edges (rem_unPath xs G))
[PROOF STEP]
by (metis  finite.emptyI finite_Diff2 finite_Diff_insert select_convs(2))
[PROOF STATE]
proof (state)
this:
finite (edges (del_unEdge (fst x) (fst (snd x)) (snd (snd x)) (rem_unPath xs G))) = finite (edges (rem_unPath xs G))

goal (1 subgoal):
 1. \<And>a ps G. \<lbrakk>\<And>G. finite (edges G) \<Longrightarrow> finite (edges (rem_unPath ps G)); finite (edges G)\<rbrakk> \<Longrightarrow> finite (edges (rem_unPath (a # ps) G))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
finite (edges (del_unEdge (fst x) (fst (snd x)) (snd (snd x)) (rem_unPath xs G))) = finite (edges (rem_unPath xs G))

goal (1 subgoal):
 1. \<And>a ps G. \<lbrakk>\<And>G. finite (edges G) \<Longrightarrow> finite (edges (rem_unPath ps G)); finite (edges G)\<rbrakk> \<Longrightarrow> finite (edges (rem_unPath (a # ps) G))
[PROOF STEP]
have "...=True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (edges (rem_unPath xs G)) = True
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
finite (edges ?G) \<Longrightarrow> finite (edges (rem_unPath xs ?G))
finite (edges G)

goal (1 subgoal):
 1. finite (edges (rem_unPath xs G)) = True
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (edges (rem_unPath xs G)) = True

goal (1 subgoal):
 1. \<And>a ps G. \<lbrakk>\<And>G. finite (edges G) \<Longrightarrow> finite (edges (rem_unPath ps G)); finite (edges G)\<rbrakk> \<Longrightarrow> finite (edges (rem_unPath (a # ps) G))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
finite (edges (rem_unPath (x # xs) G)) = True
[PROOF STEP]
have "?case = True"
[PROOF STATE]
proof (prove)
using this:
finite (edges (rem_unPath (x # xs) G)) = True

goal (1 subgoal):
 1. finite (edges (rem_unPath (x # xs) G)) = True
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
finite (edges (rem_unPath (x # xs) G)) = True

goal (1 subgoal):
 1. \<And>a ps G. \<lbrakk>\<And>G. finite (edges G) \<Longrightarrow> finite (edges (rem_unPath ps G)); finite (edges G)\<rbrakk> \<Longrightarrow> finite (edges (rem_unPath (a # ps) G))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
finite (edges (rem_unPath (x # xs) G)) = True

goal (1 subgoal):
 1. finite (edges (rem_unPath (x # xs) G))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (edges (rem_unPath (x # xs) G))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma del_UnEdge_frame[intro]:
  "x\<in>edges g \<Longrightarrow> x\<noteq>(v,e,v') \<Longrightarrow>x\<noteq>(v',e,v) \<Longrightarrow> x\<in>edges (del_unEdge v e v' g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> edges g; x \<noteq> (v, e, v'); x \<noteq> (v', e, v)\<rbrakk> \<Longrightarrow> x \<in> edges (del_unEdge v e v' g)
[PROOF STEP]
unfolding del_unEdge_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> edges g; x \<noteq> (v, e, v'); x \<noteq> (v', e, v)\<rbrakk> \<Longrightarrow> x \<in> edges \<lparr>nodes = nodes g, edges = edges g - {(v, e, v'), (v', e, v)}\<rparr>
[PROOF STEP]
by auto


[STATEMENT]
lemma [intro!]: "finite (nodes G) \<Longrightarrow> finite (odd_nodes_set G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (nodes G) \<Longrightarrow> finite (odd_nodes_set G)
[PROOF STEP]
by (metis (lifting) mem_Collect_eq odd_nodes_set_def rev_finite_subset subsetI)


[STATEMENT]
lemma [simp]: "nodes (del_unEdge u e u' G)=nodes G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nodes (del_unEdge u e u' G) = nodes G
[PROOF STEP]
by (metis del_unEdge_def select_convs(1))


[STATEMENT]
lemma [simp]: "nodes (rem_unPath ps G) = nodes G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nodes (rem_unPath ps G) = nodes G
[PROOF STEP]
proof (induct ps)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. nodes (rem_unPath [] G) = nodes G
 2. \<And>a ps. nodes (rem_unPath ps G) = nodes G \<Longrightarrow> nodes (rem_unPath (a # ps) G) = nodes G
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. nodes (rem_unPath [] G) = nodes G
 2. \<And>a ps. nodes (rem_unPath ps G) = nodes G \<Longrightarrow> nodes (rem_unPath (a # ps) G) = nodes G
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nodes (rem_unPath [] G) = nodes G
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
nodes (rem_unPath [] G) = nodes G

goal (1 subgoal):
 1. \<And>a ps. nodes (rem_unPath ps G) = nodes G \<Longrightarrow> nodes (rem_unPath (a # ps) G) = nodes G
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ps. nodes (rem_unPath ps G) = nodes G \<Longrightarrow> nodes (rem_unPath (a # ps) G) = nodes G
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
nodes (rem_unPath xs G) = nodes G

goal (1 subgoal):
 1. \<And>a ps. nodes (rem_unPath ps G) = nodes G \<Longrightarrow> nodes (rem_unPath (a # ps) G) = nodes G
[PROOF STEP]
have "nodes (rem_unPath (x # xs) G)=nodes (del_unEdge
        (fst x) (fst (snd x)) (snd (snd x)) (rem_unPath xs G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nodes (rem_unPath (x # xs) G) = nodes (del_unEdge (fst x) (fst (snd x)) (snd (snd x)) (rem_unPath xs G))
[PROOF STEP]
by (metis rem_unPath.simps(2) rem_unPath_com surjective_pairing)
[PROOF STATE]
proof (state)
this:
nodes (rem_unPath (x # xs) G) = nodes (del_unEdge (fst x) (fst (snd x)) (snd (snd x)) (rem_unPath xs G))

goal (1 subgoal):
 1. \<And>a ps. nodes (rem_unPath ps G) = nodes G \<Longrightarrow> nodes (rem_unPath (a # ps) G) = nodes G
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
nodes (rem_unPath (x # xs) G) = nodes (del_unEdge (fst x) (fst (snd x)) (snd (snd x)) (rem_unPath xs G))

goal (1 subgoal):
 1. \<And>a ps. nodes (rem_unPath ps G) = nodes G \<Longrightarrow> nodes (rem_unPath (a # ps) G) = nodes G
[PROOF STEP]
have "...=nodes (rem_unPath xs G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nodes (del_unEdge (fst x) (fst (snd x)) (snd (snd x)) (rem_unPath xs G)) = nodes (rem_unPath xs G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nodes (del_unEdge (fst x) (fst (snd x)) (snd (snd x)) (rem_unPath xs G)) = nodes (rem_unPath xs G)

goal (1 subgoal):
 1. \<And>a ps. nodes (rem_unPath ps G) = nodes G \<Longrightarrow> nodes (rem_unPath (a # ps) G) = nodes G
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
nodes (del_unEdge (fst x) (fst (snd x)) (snd (snd x)) (rem_unPath xs G)) = nodes (rem_unPath xs G)

goal (1 subgoal):
 1. \<And>a ps. nodes (rem_unPath ps G) = nodes G \<Longrightarrow> nodes (rem_unPath (a # ps) G) = nodes G
[PROOF STEP]
have "...=nodes G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nodes (rem_unPath xs G) = nodes G
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
nodes (rem_unPath xs G) = nodes G

goal (1 subgoal):
 1. nodes (rem_unPath xs G) = nodes G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nodes (rem_unPath xs G) = nodes G

goal (1 subgoal):
 1. \<And>a ps. nodes (rem_unPath ps G) = nodes G \<Longrightarrow> nodes (rem_unPath (a # ps) G) = nodes G
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
nodes (rem_unPath (x # xs) G) = nodes G
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
nodes (rem_unPath (x # xs) G) = nodes G

goal (1 subgoal):
 1. nodes (rem_unPath (x # xs) G) = nodes G
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
nodes (rem_unPath (x # xs) G) = nodes G

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma [intro!]: "finite (nodes G) \<Longrightarrow> finite (nodes (rem_unPath ps G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (nodes G) \<Longrightarrow> finite (nodes (rem_unPath ps G))
[PROOF STEP]
by auto


[STATEMENT]
lemma in_set_rev_path[simp]: "(v',w,v )\<in>set (rev_path ps) \<longleftrightarrow> (v,w,v')\<in>set ps "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((v', w, v) \<in> set (rev_path ps)) = ((v, w, v') \<in> set ps)
[PROOF STEP]
proof (induct ps)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ((v', w, v) \<in> set (rev_path [])) = ((v, w, v') \<in> set [])
 2. \<And>a ps. ((v', w, v) \<in> set (rev_path ps)) = ((v, w, v') \<in> set ps) \<Longrightarrow> ((v', w, v) \<in> set (rev_path (a # ps))) = ((v, w, v') \<in> set (a # ps))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. ((v', w, v) \<in> set (rev_path [])) = ((v, w, v') \<in> set [])
 2. \<And>a ps. ((v', w, v) \<in> set (rev_path ps)) = ((v, w, v') \<in> set ps) \<Longrightarrow> ((v', w, v) \<in> set (rev_path (a # ps))) = ((v, w, v') \<in> set (a # ps))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((v', w, v) \<in> set (rev_path [])) = ((v, w, v') \<in> set [])
[PROOF STEP]
unfolding rev_path_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((v', w, v) \<in> set (map (\<lambda>(a, b, c). (c, b, a)) (rev []))) = ((v, w, v') \<in> set [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((v', w, v) \<in> set (rev_path [])) = ((v, w, v') \<in> set [])

goal (1 subgoal):
 1. \<And>a ps. ((v', w, v) \<in> set (rev_path ps)) = ((v, w, v') \<in> set ps) \<Longrightarrow> ((v', w, v) \<in> set (rev_path (a # ps))) = ((v, w, v') \<in> set (a # ps))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ps. ((v', w, v) \<in> set (rev_path ps)) = ((v, w, v') \<in> set ps) \<Longrightarrow> ((v', w, v) \<in> set (rev_path (a # ps))) = ((v, w, v') \<in> set (a # ps))
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
((v', w, v) \<in> set (rev_path xs)) = ((v, w, v') \<in> set xs)

goal (1 subgoal):
 1. \<And>a ps. ((v', w, v) \<in> set (rev_path ps)) = ((v, w, v') \<in> set ps) \<Longrightarrow> ((v', w, v) \<in> set (rev_path (a # ps))) = ((v, w, v') \<in> set (a # ps))
[PROOF STEP]
obtain x1 x2 x3 where x:"x=(x1,x2,x3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x1 x2 x3. x = (x1, x2, x3) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod_cases3)
[PROOF STATE]
proof (state)
this:
x = (x1, x2, x3)

goal (1 subgoal):
 1. \<And>a ps. ((v', w, v) \<in> set (rev_path ps)) = ((v, w, v') \<in> set ps) \<Longrightarrow> ((v', w, v) \<in> set (rev_path (a # ps))) = ((v, w, v') \<in> set (a # ps))
[PROOF STEP]
have "set (rev_path (x # xs))=set ((rev_path xs)@[(x3,x2,x1)])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (rev_path (x # xs)) = set (rev_path xs @ [(x3, x2, x1)])
[PROOF STEP]
unfolding rev_path_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map (\<lambda>(a, b, c). (c, b, a)) (rev (x # xs))) = set (map (\<lambda>(a, b, c). (c, b, a)) (rev xs) @ [(x3, x2, x1)])
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
x = (x1, x2, x3)

goal (1 subgoal):
 1. set (map (\<lambda>(a, b, c). (c, b, a)) (rev (x # xs))) = set (map (\<lambda>(a, b, c). (c, b, a)) (rev xs) @ [(x3, x2, x1)])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (rev_path (x # xs)) = set (rev_path xs @ [(x3, x2, x1)])

goal (1 subgoal):
 1. \<And>a ps. ((v', w, v) \<in> set (rev_path ps)) = ((v, w, v') \<in> set ps) \<Longrightarrow> ((v', w, v) \<in> set (rev_path (a # ps))) = ((v, w, v') \<in> set (a # ps))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set (rev_path (x # xs)) = set (rev_path xs @ [(x3, x2, x1)])

goal (1 subgoal):
 1. \<And>a ps. ((v', w, v) \<in> set (rev_path ps)) = ((v, w, v') \<in> set ps) \<Longrightarrow> ((v', w, v) \<in> set (rev_path (a # ps))) = ((v, w, v') \<in> set (a # ps))
[PROOF STEP]
have "...=set (rev_path xs) \<union> {(x3,x2,x1)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (rev_path xs @ [(x3, x2, x1)]) = set (rev_path xs) \<union> {(x3, x2, x1)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (rev_path xs @ [(x3, x2, x1)]) = set (rev_path xs) \<union> {(x3, x2, x1)}

goal (1 subgoal):
 1. \<And>a ps. ((v', w, v) \<in> set (rev_path ps)) = ((v, w, v') \<in> set ps) \<Longrightarrow> ((v', w, v) \<in> set (rev_path (a # ps))) = ((v, w, v') \<in> set (a # ps))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
set (rev_path (x # xs)) = set (rev_path xs) \<union> {(x3, x2, x1)}
[PROOF STEP]
have "set (rev_path (x # xs)) =set (rev_path xs) \<union> {(x3,x2,x1)}"
[PROOF STATE]
proof (prove)
using this:
set (rev_path (x # xs)) = set (rev_path xs) \<union> {(x3, x2, x1)}

goal (1 subgoal):
 1. set (rev_path (x # xs)) = set (rev_path xs) \<union> {(x3, x2, x1)}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
set (rev_path (x # xs)) = set (rev_path xs) \<union> {(x3, x2, x1)}

goal (1 subgoal):
 1. \<And>a ps. ((v', w, v) \<in> set (rev_path ps)) = ((v, w, v') \<in> set ps) \<Longrightarrow> ((v', w, v) \<in> set (rev_path (a # ps))) = ((v, w, v') \<in> set (a # ps))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (rev_path (x # xs)) = set (rev_path xs) \<union> {(x3, x2, x1)}

goal (1 subgoal):
 1. \<And>a ps. ((v', w, v) \<in> set (rev_path ps)) = ((v, w, v') \<in> set ps) \<Longrightarrow> ((v', w, v) \<in> set (rev_path (a # ps))) = ((v, w, v') \<in> set (a # ps))
[PROOF STEP]
have "set (x#xs)= set xs \<union> {(x1,x2,x3)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (x # xs) = set xs \<union> {(x1, x2, x3)}
[PROOF STEP]
by (metis List.set_simps(2) insert_is_Un sup_commute x)
[PROOF STATE]
proof (state)
this:
set (x # xs) = set xs \<union> {(x1, x2, x3)}

goal (1 subgoal):
 1. \<And>a ps. ((v', w, v) \<in> set (rev_path ps)) = ((v, w, v') \<in> set ps) \<Longrightarrow> ((v', w, v) \<in> set (rev_path (a # ps))) = ((v, w, v') \<in> set (a # ps))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set (rev_path (x # xs)) = set (rev_path xs) \<union> {(x3, x2, x1)}
set (x # xs) = set xs \<union> {(x1, x2, x3)}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set (rev_path (x # xs)) = set (rev_path xs) \<union> {(x3, x2, x1)}
set (x # xs) = set xs \<union> {(x1, x2, x3)}

goal (1 subgoal):
 1. ((v', w, v) \<in> set (rev_path (x # xs))) = ((v, w, v') \<in> set (x # xs))
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
set (rev_path (x # xs)) = set (rev_path xs) \<union> {(x3, x2, x1)}
set (x # xs) = set xs \<union> {(x1, x2, x3)}
((v', w, v) \<in> set (rev_path xs)) = ((v, w, v') \<in> set xs)

goal (1 subgoal):
 1. ((v', w, v) \<in> set (rev_path (x # xs))) = ((v, w, v') \<in> set (x # xs))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((v', w, v) \<in> set (rev_path (x # xs))) = ((v, w, v') \<in> set (x # xs))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rem_unPath_edges:
    "edges(rem_unPath ps G) = edges G - (set ps \<union> set (rev_path ps))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. edges (rem_unPath ps G) = edges G - (set ps \<union> set (rev_path ps))
[PROOF STEP]
proof (induct ps)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. edges (rem_unPath [] G) = edges G - (set [] \<union> set (rev_path []))
 2. \<And>a ps. edges (rem_unPath ps G) = edges G - (set ps \<union> set (rev_path ps)) \<Longrightarrow> edges (rem_unPath (a # ps) G) = edges G - (set (a # ps) \<union> set (rev_path (a # ps)))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. edges (rem_unPath [] G) = edges G - (set [] \<union> set (rev_path []))
 2. \<And>a ps. edges (rem_unPath ps G) = edges G - (set ps \<union> set (rev_path ps)) \<Longrightarrow> edges (rem_unPath (a # ps) G) = edges G - (set (a # ps) \<union> set (rev_path (a # ps)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. edges (rem_unPath [] G) = edges G - (set [] \<union> set (rev_path []))
[PROOF STEP]
unfolding rev_path_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. edges (rem_unPath [] G) = edges G - (set [] \<union> set (map (\<lambda>(a, b, c). (c, b, a)) (rev [])))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
edges (rem_unPath [] G) = edges G - (set [] \<union> set (rev_path []))

goal (1 subgoal):
 1. \<And>a ps. edges (rem_unPath ps G) = edges G - (set ps \<union> set (rev_path ps)) \<Longrightarrow> edges (rem_unPath (a # ps) G) = edges G - (set (a # ps) \<union> set (rev_path (a # ps)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ps. edges (rem_unPath ps G) = edges G - (set ps \<union> set (rev_path ps)) \<Longrightarrow> edges (rem_unPath (a # ps) G) = edges G - (set (a # ps) \<union> set (rev_path (a # ps)))
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
edges (rem_unPath xs G) = edges G - (set xs \<union> set (rev_path xs))

goal (1 subgoal):
 1. \<And>a ps. edges (rem_unPath ps G) = edges G - (set ps \<union> set (rev_path ps)) \<Longrightarrow> edges (rem_unPath (a # ps) G) = edges G - (set (a # ps) \<union> set (rev_path (a # ps)))
[PROOF STEP]
obtain x1 x2 x3 where x: "x=(x1,x2,x3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x1 x2 x3. x = (x1, x2, x3) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod_cases3)
[PROOF STATE]
proof (state)
this:
x = (x1, x2, x3)

goal (1 subgoal):
 1. \<And>a ps. edges (rem_unPath ps G) = edges G - (set ps \<union> set (rev_path ps)) \<Longrightarrow> edges (rem_unPath (a # ps) G) = edges G - (set (a # ps) \<union> set (rev_path (a # ps)))
[PROOF STEP]
hence "edges(rem_unPath (x#xs) G)= edges(del_unEdge x1 x2 x3 (rem_unPath xs G))"
[PROOF STATE]
proof (prove)
using this:
x = (x1, x2, x3)

goal (1 subgoal):
 1. edges (rem_unPath (x # xs) G) = edges (del_unEdge x1 x2 x3 (rem_unPath xs G))
[PROOF STEP]
by (metis rem_unPath.simps(2) rem_unPath_com)
[PROOF STATE]
proof (state)
this:
edges (rem_unPath (x # xs) G) = edges (del_unEdge x1 x2 x3 (rem_unPath xs G))

goal (1 subgoal):
 1. \<And>a ps. edges (rem_unPath ps G) = edges G - (set ps \<union> set (rev_path ps)) \<Longrightarrow> edges (rem_unPath (a # ps) G) = edges G - (set (a # ps) \<union> set (rev_path (a # ps)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
edges (rem_unPath (x # xs) G) = edges (del_unEdge x1 x2 x3 (rem_unPath xs G))

goal (1 subgoal):
 1. \<And>a ps. edges (rem_unPath ps G) = edges G - (set ps \<union> set (rev_path ps)) \<Longrightarrow> edges (rem_unPath (a # ps) G) = edges G - (set (a # ps) \<union> set (rev_path (a # ps)))
[PROOF STEP]
have "...=edges(rem_unPath xs G)-{(x1,x2,x3),(x3,x2,x1)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. edges (del_unEdge x1 x2 x3 (rem_unPath xs G)) = edges (rem_unPath xs G) - {(x1, x2, x3), (x3, x2, x1)}
[PROOF STEP]
by (metis del_unEdge_def select_convs(2))
[PROOF STATE]
proof (state)
this:
edges (del_unEdge x1 x2 x3 (rem_unPath xs G)) = edges (rem_unPath xs G) - {(x1, x2, x3), (x3, x2, x1)}

goal (1 subgoal):
 1. \<And>a ps. edges (rem_unPath ps G) = edges G - (set ps \<union> set (rev_path ps)) \<Longrightarrow> edges (rem_unPath (a # ps) G) = edges G - (set (a # ps) \<union> set (rev_path (a # ps)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
edges (del_unEdge x1 x2 x3 (rem_unPath xs G)) = edges (rem_unPath xs G) - {(x1, x2, x3), (x3, x2, x1)}

goal (1 subgoal):
 1. \<And>a ps. edges (rem_unPath ps G) = edges G - (set ps \<union> set (rev_path ps)) \<Longrightarrow> edges (rem_unPath (a # ps) G) = edges G - (set (a # ps) \<union> set (rev_path (a # ps)))
[PROOF STEP]
have "...= edges G - (set xs \<union> set (rev_path xs))-{(x1,x2,x3),(x3,x2,x1)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. edges (rem_unPath xs G) - {(x1, x2, x3), (x3, x2, x1)} = edges G - (set xs \<union> set (rev_path xs)) - {(x1, x2, x3), (x3, x2, x1)}
[PROOF STEP]
by (metis Cons.hyps)
[PROOF STATE]
proof (state)
this:
edges (rem_unPath xs G) - {(x1, x2, x3), (x3, x2, x1)} = edges G - (set xs \<union> set (rev_path xs)) - {(x1, x2, x3), (x3, x2, x1)}

goal (1 subgoal):
 1. \<And>a ps. edges (rem_unPath ps G) = edges G - (set ps \<union> set (rev_path ps)) \<Longrightarrow> edges (rem_unPath (a # ps) G) = edges G - (set (a # ps) \<union> set (rev_path (a # ps)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
edges (rem_unPath xs G) - {(x1, x2, x3), (x3, x2, x1)} = edges G - (set xs \<union> set (rev_path xs)) - {(x1, x2, x3), (x3, x2, x1)}

goal (1 subgoal):
 1. \<And>a ps. edges (rem_unPath ps G) = edges G - (set ps \<union> set (rev_path ps)) \<Longrightarrow> edges (rem_unPath (a # ps) G) = edges G - (set (a # ps) \<union> set (rev_path (a # ps)))
[PROOF STEP]
have "...=edges G - (set (x#xs) \<union> set (rev_path (x#xs)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. edges G - (set xs \<union> set (rev_path xs)) - {(x1, x2, x3), (x3, x2, x1)} = edges G - (set (x # xs) \<union> set (rev_path (x # xs)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. edges G - (set xs \<union> set (rev_path xs)) - {(x1, x2, x3), (x3, x2, x1)} = edges G - (set (x # xs) \<union> set (rev_path (x # xs)))
[PROOF STEP]
have "set (rev_path xs) \<union> {(x3,x2,x1)}=set ((rev_path xs)@[(x3,x2,x1)])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (rev_path xs) \<union> {(x3, x2, x1)} = set (rev_path xs @ [(x3, x2, x1)])
[PROOF STEP]
by (metis List.set_simps(2) empty_set set_append)
[PROOF STATE]
proof (state)
this:
set (rev_path xs) \<union> {(x3, x2, x1)} = set (rev_path xs @ [(x3, x2, x1)])

goal (1 subgoal):
 1. edges G - (set xs \<union> set (rev_path xs)) - {(x1, x2, x3), (x3, x2, x1)} = edges G - (set (x # xs) \<union> set (rev_path (x # xs)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set (rev_path xs) \<union> {(x3, x2, x1)} = set (rev_path xs @ [(x3, x2, x1)])

goal (1 subgoal):
 1. edges G - (set xs \<union> set (rev_path xs)) - {(x1, x2, x3), (x3, x2, x1)} = edges G - (set (x # xs) \<union> set (rev_path (x # xs)))
[PROOF STEP]
have "...=set (rev_path (x#xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (rev_path xs @ [(x3, x2, x1)]) = set (rev_path (x # xs))
[PROOF STEP]
unfolding rev_path_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map (\<lambda>(a, b, c). (c, b, a)) (rev xs) @ [(x3, x2, x1)]) = set (map (\<lambda>(a, b, c). (c, b, a)) (rev (x # xs)))
[PROOF STEP]
using  x
[PROOF STATE]
proof (prove)
using this:
x = (x1, x2, x3)

goal (1 subgoal):
 1. set (map (\<lambda>(a, b, c). (c, b, a)) (rev xs) @ [(x3, x2, x1)]) = set (map (\<lambda>(a, b, c). (c, b, a)) (rev (x # xs)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (rev_path xs @ [(x3, x2, x1)]) = set (rev_path (x # xs))

goal (1 subgoal):
 1. edges G - (set xs \<union> set (rev_path xs)) - {(x1, x2, x3), (x3, x2, x1)} = edges G - (set (x # xs) \<union> set (rev_path (x # xs)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
set (rev_path xs) \<union> {(x3, x2, x1)} = set (rev_path (x # xs))
[PROOF STEP]
have "set (rev_path xs) \<union> {(x3,x2,x1)}=set (rev_path (x#xs))"
[PROOF STATE]
proof (prove)
using this:
set (rev_path xs) \<union> {(x3, x2, x1)} = set (rev_path (x # xs))

goal (1 subgoal):
 1. set (rev_path xs) \<union> {(x3, x2, x1)} = set (rev_path (x # xs))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
set (rev_path xs) \<union> {(x3, x2, x1)} = set (rev_path (x # xs))

goal (1 subgoal):
 1. edges G - (set xs \<union> set (rev_path xs)) - {(x1, x2, x3), (x3, x2, x1)} = edges G - (set (x # xs) \<union> set (rev_path (x # xs)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (rev_path xs) \<union> {(x3, x2, x1)} = set (rev_path (x # xs))

goal (1 subgoal):
 1. edges G - (set xs \<union> set (rev_path xs)) - {(x1, x2, x3), (x3, x2, x1)} = edges G - (set (x # xs) \<union> set (rev_path (x # xs)))
[PROOF STEP]
have "set xs \<union> {(x1,x2,x3)}=set (x#xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set xs \<union> {(x1, x2, x3)} = set (x # xs)
[PROOF STEP]
by (metis List.set_simps(2) insert_is_Un sup_commute x)
[PROOF STATE]
proof (state)
this:
set xs \<union> {(x1, x2, x3)} = set (x # xs)

goal (1 subgoal):
 1. edges G - (set xs \<union> set (rev_path xs)) - {(x1, x2, x3), (x3, x2, x1)} = edges G - (set (x # xs) \<union> set (rev_path (x # xs)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set xs \<union> {(x1, x2, x3)} = set (x # xs)

goal (1 subgoal):
 1. edges G - (set xs \<union> set (rev_path xs)) - {(x1, x2, x3), (x3, x2, x1)} = edges G - (set (x # xs) \<union> set (rev_path (x # xs)))
[PROOF STEP]
have "edges G - (set xs \<union> set (rev_path xs))-{(x1,x2,x3),(x3,x2,x1)} =
                      edges G - ((set xs \<union> {(x1,x2,x3)}) \<union> (set (rev_path xs) \<union> {(x3,x2,x1)}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. edges G - (set xs \<union> set (rev_path xs)) - {(x1, x2, x3), (x3, x2, x1)} = edges G - (set xs \<union> {(x1, x2, x3)} \<union> (set (rev_path xs) \<union> {(x3, x2, x1)}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
edges G - (set xs \<union> set (rev_path xs)) - {(x1, x2, x3), (x3, x2, x1)} = edges G - (set xs \<union> {(x1, x2, x3)} \<union> (set (rev_path xs) \<union> {(x3, x2, x1)}))

goal (1 subgoal):
 1. edges G - (set xs \<union> set (rev_path xs)) - {(x1, x2, x3), (x3, x2, x1)} = edges G - (set (x # xs) \<union> set (rev_path (x # xs)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set (rev_path xs) \<union> {(x3, x2, x1)} = set (rev_path (x # xs))
set xs \<union> {(x1, x2, x3)} = set (x # xs)
edges G - (set xs \<union> set (rev_path xs)) - {(x1, x2, x3), (x3, x2, x1)} = edges G - (set xs \<union> {(x1, x2, x3)} \<union> (set (rev_path xs) \<union> {(x3, x2, x1)}))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set (rev_path xs) \<union> {(x3, x2, x1)} = set (rev_path (x # xs))
set xs \<union> {(x1, x2, x3)} = set (x # xs)
edges G - (set xs \<union> set (rev_path xs)) - {(x1, x2, x3), (x3, x2, x1)} = edges G - (set xs \<union> {(x1, x2, x3)} \<union> (set (rev_path xs) \<union> {(x3, x2, x1)}))

goal (1 subgoal):
 1. edges G - (set xs \<union> set (rev_path xs)) - {(x1, x2, x3), (x3, x2, x1)} = edges G - (set (x # xs) \<union> set (rev_path (x # xs)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
edges G - (set xs \<union> set (rev_path xs)) - {(x1, x2, x3), (x3, x2, x1)} = edges G - (set (x # xs) \<union> set (rev_path (x # xs)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
edges G - (set xs \<union> set (rev_path xs)) - {(x1, x2, x3), (x3, x2, x1)} = edges G - (set (x # xs) \<union> set (rev_path (x # xs)))

goal (1 subgoal):
 1. \<And>a ps. edges (rem_unPath ps G) = edges G - (set ps \<union> set (rev_path ps)) \<Longrightarrow> edges (rem_unPath (a # ps) G) = edges G - (set (a # ps) \<union> set (rev_path (a # ps)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
edges (rem_unPath (x # xs) G) = edges G - (set (x # xs) \<union> set (rev_path (x # xs)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
edges (rem_unPath (x # xs) G) = edges G - (set (x # xs) \<union> set (rev_path (x # xs)))

goal (1 subgoal):
 1. edges (rem_unPath (x # xs) G) = edges G - (set (x # xs) \<union> set (rev_path (x # xs)))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
edges (rem_unPath (x # xs) G) = edges G - (set (x # xs) \<union> set (rev_path (x # xs)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rem_unPath_graph [simp]:
    "rem_unPath (rev_path ps) G=rem_unPath ps G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rem_unPath (rev_path ps) G = rem_unPath ps G
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rem_unPath (rev_path ps) G = rem_unPath ps G
[PROOF STEP]
have "nodes(rem_unPath (rev_path ps) G)=nodes(rem_unPath ps G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nodes (rem_unPath (rev_path ps) G) = nodes (rem_unPath ps G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nodes (rem_unPath (rev_path ps) G) = nodes (rem_unPath ps G)

goal (1 subgoal):
 1. rem_unPath (rev_path ps) G = rem_unPath ps G
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nodes (rem_unPath (rev_path ps) G) = nodes (rem_unPath ps G)

goal (1 subgoal):
 1. rem_unPath (rev_path ps) G = rem_unPath ps G
[PROOF STEP]
have "edges(rem_unPath (rev_path ps) G)=edges(rem_unPath ps G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. edges (rem_unPath (rev_path ps) G) = edges (rem_unPath ps G)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. edges (rem_unPath (rev_path ps) G) = edges (rem_unPath ps G)
[PROOF STEP]
have "set (rev_path ps) \<union> set (rev_path (rev_path ps)) = set ps \<union>  set (rev_path ps) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (rev_path ps) \<union> set (rev_path (rev_path ps)) = set ps \<union> set (rev_path ps)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (rev_path ps) \<union> set (rev_path (rev_path ps)) = set ps \<union> set (rev_path ps)

goal (1 subgoal):
 1. edges (rem_unPath (rev_path ps) G) = edges (rem_unPath ps G)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
set (rev_path ps) \<union> set (rev_path (rev_path ps)) = set ps \<union> set (rev_path ps)

goal (1 subgoal):
 1. edges (rem_unPath (rev_path ps) G) = edges (rem_unPath ps G)
[PROOF STEP]
by (metis rem_unPath_edges)
[PROOF STATE]
proof (state)
this:
edges (rem_unPath (rev_path ps) G) = edges (rem_unPath ps G)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
edges (rem_unPath (rev_path ps) G) = edges (rem_unPath ps G)

goal (1 subgoal):
 1. rem_unPath (rev_path ps) G = rem_unPath ps G
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
nodes (rem_unPath (rev_path ps) G) = nodes (rem_unPath ps G)
edges (rem_unPath (rev_path ps) G) = edges (rem_unPath ps G)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
nodes (rem_unPath (rev_path ps) G) = nodes (rem_unPath ps G)
edges (rem_unPath (rev_path ps) G) = edges (rem_unPath ps G)

goal (1 subgoal):
 1. rem_unPath (rev_path ps) G = rem_unPath ps G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rem_unPath (rev_path ps) G = rem_unPath ps G

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma distinct_rev_path[simp]: "distinct (rev_path ps) \<longleftrightarrow>distinct ps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (rev_path ps) = distinct ps
[PROOF STEP]
proof (induct ps)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. distinct (rev_path []) = distinct []
 2. \<And>a ps. distinct (rev_path ps) = distinct ps \<Longrightarrow> distinct (rev_path (a # ps)) = distinct (a # ps)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. distinct (rev_path []) = distinct []
 2. \<And>a ps. distinct (rev_path ps) = distinct ps \<Longrightarrow> distinct (rev_path (a # ps)) = distinct (a # ps)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (rev_path []) = distinct []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct (rev_path []) = distinct []

goal (1 subgoal):
 1. \<And>a ps. distinct (rev_path ps) = distinct ps \<Longrightarrow> distinct (rev_path (a # ps)) = distinct (a # ps)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ps. distinct (rev_path ps) = distinct ps \<Longrightarrow> distinct (rev_path (a # ps)) = distinct (a # ps)
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
distinct (rev_path xs) = distinct xs

goal (1 subgoal):
 1. \<And>a ps. distinct (rev_path ps) = distinct ps \<Longrightarrow> distinct (rev_path (a # ps)) = distinct (a # ps)
[PROOF STEP]
obtain x1 x2 x3 where x: "x=(x1,x2,x3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x1 x2 x3. x = (x1, x2, x3) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod_cases3)
[PROOF STATE]
proof (state)
this:
x = (x1, x2, x3)

goal (1 subgoal):
 1. \<And>a ps. distinct (rev_path ps) = distinct ps \<Longrightarrow> distinct (rev_path (a # ps)) = distinct (a # ps)
[PROOF STEP]
hence "distinct (rev_path (x # xs))=distinct ((rev_path xs)@[(x3,x2,x1)])"
[PROOF STATE]
proof (prove)
using this:
x = (x1, x2, x3)

goal (1 subgoal):
 1. distinct (rev_path (x # xs)) = distinct (rev_path xs @ [(x3, x2, x1)])
[PROOF STEP]
unfolding rev_path_def
[PROOF STATE]
proof (prove)
using this:
x = (x1, x2, x3)

goal (1 subgoal):
 1. distinct (map (\<lambda>(a, b, c). (c, b, a)) (rev (x # xs))) = distinct (map (\<lambda>(a, b, c). (c, b, a)) (rev xs) @ [(x3, x2, x1)])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct (rev_path (x # xs)) = distinct (rev_path xs @ [(x3, x2, x1)])

goal (1 subgoal):
 1. \<And>a ps. distinct (rev_path ps) = distinct ps \<Longrightarrow> distinct (rev_path (a # ps)) = distinct (a # ps)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
distinct (rev_path (x # xs)) = distinct (rev_path xs @ [(x3, x2, x1)])

goal (1 subgoal):
 1. \<And>a ps. distinct (rev_path ps) = distinct ps \<Longrightarrow> distinct (rev_path (a # ps)) = distinct (a # ps)
[PROOF STEP]
have "...= (distinct (rev_path xs) \<and> (x3,x2,x1)\<notin>set (rev_path xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (rev_path xs @ [(x3, x2, x1)]) = (distinct (rev_path xs) \<and> (x3, x2, x1) \<notin> set (rev_path xs))
[PROOF STEP]
by (metis distinct.simps(2) distinct1_rotate rotate1.simps(2))
[PROOF STATE]
proof (state)
this:
distinct (rev_path xs @ [(x3, x2, x1)]) = (distinct (rev_path xs) \<and> (x3, x2, x1) \<notin> set (rev_path xs))

goal (1 subgoal):
 1. \<And>a ps. distinct (rev_path ps) = distinct ps \<Longrightarrow> distinct (rev_path (a # ps)) = distinct (a # ps)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
distinct (rev_path xs @ [(x3, x2, x1)]) = (distinct (rev_path xs) \<and> (x3, x2, x1) \<notin> set (rev_path xs))

goal (1 subgoal):
 1. \<And>a ps. distinct (rev_path ps) = distinct ps \<Longrightarrow> distinct (rev_path (a # ps)) = distinct (a # ps)
[PROOF STEP]
have "...=distinct (x#xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (distinct (rev_path xs) \<and> (x3, x2, x1) \<notin> set (rev_path xs)) = distinct (x # xs)
[PROOF STEP]
by (metis Cons.hyps distinct.simps(2) in_set_rev_path x)
[PROOF STATE]
proof (state)
this:
(distinct (rev_path xs) \<and> (x3, x2, x1) \<notin> set (rev_path xs)) = distinct (x # xs)

goal (1 subgoal):
 1. \<And>a ps. distinct (rev_path ps) = distinct ps \<Longrightarrow> distinct (rev_path (a # ps)) = distinct (a # ps)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
distinct (rev_path (x # xs)) = distinct (x # xs)
[PROOF STEP]
have "distinct (rev_path (x # xs))=distinct (x#xs)"
[PROOF STATE]
proof (prove)
using this:
distinct (rev_path (x # xs)) = distinct (x # xs)

goal (1 subgoal):
 1. distinct (rev_path (x # xs)) = distinct (x # xs)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
distinct (rev_path (x # xs)) = distinct (x # xs)

goal (1 subgoal):
 1. \<And>a ps. distinct (rev_path ps) = distinct ps \<Longrightarrow> distinct (rev_path (a # ps)) = distinct (a # ps)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
distinct (rev_path (x # xs)) = distinct (x # xs)

goal (1 subgoal):
 1. distinct (rev_path (x # xs)) = distinct (x # xs)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
distinct (rev_path (x # xs)) = distinct (x # xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in valid_unMultigraph) is_path_rev: "is_path v' (rev_path ps) v \<longleftrightarrow> is_path v ps v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path v' (rev_path ps) v = is_path v ps v'
[PROOF STEP]
proof (induct ps arbitrary: v)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v. is_path v' (rev_path []) v = is_path v [] v'
 2. \<And>a ps v. (\<And>v. is_path v' (rev_path ps) v = is_path v ps v') \<Longrightarrow> is_path v' (rev_path (a # ps)) v = is_path v (a # ps) v'
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>v. is_path v' (rev_path []) v = is_path v [] v'
 2. \<And>a ps v. (\<And>v. is_path v' (rev_path ps) v = is_path v ps v') \<Longrightarrow> is_path v' (rev_path (a # ps)) v = is_path v (a # ps) v'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path v' (rev_path []) v = is_path v [] v'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_path v' (rev_path []) v = is_path v [] v'

goal (1 subgoal):
 1. \<And>a ps v. (\<And>v. is_path v' (rev_path ps) v = is_path v ps v') \<Longrightarrow> is_path v' (rev_path (a # ps)) v = is_path v (a # ps) v'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ps v. (\<And>v. is_path v' (rev_path ps) v = is_path v ps v') \<Longrightarrow> is_path v' (rev_path (a # ps)) v = is_path v (a # ps) v'
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
is_path v' (rev_path xs) ?v = is_path ?v xs v'

goal (1 subgoal):
 1. \<And>a ps v. (\<And>v. is_path v' (rev_path ps) v = is_path v ps v') \<Longrightarrow> is_path v' (rev_path (a # ps)) v = is_path v (a # ps) v'
[PROOF STEP]
obtain x1 x2 x3 where x: "x=(x1,x2,x3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x1 x2 x3. x = (x1, x2, x3) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod_cases3)
[PROOF STATE]
proof (state)
this:
x = (x1, x2, x3)

goal (1 subgoal):
 1. \<And>a ps v. (\<And>v. is_path v' (rev_path ps) v = is_path v ps v') \<Longrightarrow> is_path v' (rev_path (a # ps)) v = is_path v (a # ps) v'
[PROOF STEP]
hence "is_path v' (rev_path (x # xs)) v=is_path v' ((rev_path xs) @[(x3,x2,x1)]) v"
[PROOF STATE]
proof (prove)
using this:
x = (x1, x2, x3)

goal (1 subgoal):
 1. is_path v' (rev_path (x # xs)) v = is_path v' (rev_path xs @ [(x3, x2, x1)]) v
[PROOF STEP]
unfolding rev_path_def
[PROOF STATE]
proof (prove)
using this:
x = (x1, x2, x3)

goal (1 subgoal):
 1. is_path v' (map (\<lambda>(a, b, c). (c, b, a)) (rev (x # xs))) v = is_path v' (map (\<lambda>(a, b, c). (c, b, a)) (rev xs) @ [(x3, x2, x1)]) v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_path v' (rev_path (x # xs)) v = is_path v' (rev_path xs @ [(x3, x2, x1)]) v

goal (1 subgoal):
 1. \<And>a ps v. (\<And>v. is_path v' (rev_path ps) v = is_path v ps v') \<Longrightarrow> is_path v' (rev_path (a # ps)) v = is_path v (a # ps) v'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
is_path v' (rev_path (x # xs)) v = is_path v' (rev_path xs @ [(x3, x2, x1)]) v

goal (1 subgoal):
 1. \<And>a ps v. (\<And>v. is_path v' (rev_path ps) v = is_path v ps v') \<Longrightarrow> is_path v' (rev_path (a # ps)) v = is_path v (a # ps) v'
[PROOF STEP]
have "...=(is_path v' (rev_path xs) x3 \<and> (x3,x2,x1)\<in>E \<and> is_path x1 [] v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path v' (rev_path xs @ [(x3, x2, x1)]) v = (is_path v' (rev_path xs) x3 \<and> (x3, x2, x1) \<in> E \<and> is_path x1 [] v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_path v' (rev_path xs @ [(x3, x2, x1)]) v = (is_path v' (rev_path xs) x3 \<and> (x3, x2, x1) \<in> E \<and> is_path x1 [] v)

goal (1 subgoal):
 1. \<And>a ps v. (\<And>v. is_path v' (rev_path ps) v = is_path v ps v') \<Longrightarrow> is_path v' (rev_path (a # ps)) v = is_path v (a # ps) v'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
is_path v' (rev_path xs @ [(x3, x2, x1)]) v = (is_path v' (rev_path xs) x3 \<and> (x3, x2, x1) \<in> E \<and> is_path x1 [] v)

goal (1 subgoal):
 1. \<And>a ps v. (\<And>v. is_path v' (rev_path ps) v = is_path v ps v') \<Longrightarrow> is_path v' (rev_path (a # ps)) v = is_path v (a # ps) v'
[PROOF STEP]
have "...=(is_path x3 xs v' \<and> (x3,x2,x1)\<in>E \<and> is_path x1 [] v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (is_path v' (rev_path xs) x3 \<and> (x3, x2, x1) \<in> E \<and> is_path x1 [] v) = (is_path x3 xs v' \<and> (x3, x2, x1) \<in> E \<and> is_path x1 [] v)
[PROOF STEP]
using Cons.hyps
[PROOF STATE]
proof (prove)
using this:
is_path v' (rev_path xs) ?v = is_path ?v xs v'

goal (1 subgoal):
 1. (is_path v' (rev_path xs) x3 \<and> (x3, x2, x1) \<in> E \<and> is_path x1 [] v) = (is_path x3 xs v' \<and> (x3, x2, x1) \<in> E \<and> is_path x1 [] v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(is_path v' (rev_path xs) x3 \<and> (x3, x2, x1) \<in> E \<and> is_path x1 [] v) = (is_path x3 xs v' \<and> (x3, x2, x1) \<in> E \<and> is_path x1 [] v)

goal (1 subgoal):
 1. \<And>a ps v. (\<And>v. is_path v' (rev_path ps) v = is_path v ps v') \<Longrightarrow> is_path v' (rev_path (a # ps)) v = is_path v (a # ps) v'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(is_path v' (rev_path xs) x3 \<and> (x3, x2, x1) \<in> E \<and> is_path x1 [] v) = (is_path x3 xs v' \<and> (x3, x2, x1) \<in> E \<and> is_path x1 [] v)

goal (1 subgoal):
 1. \<And>a ps v. (\<And>v. is_path v' (rev_path ps) v = is_path v ps v') \<Longrightarrow> is_path v' (rev_path (a # ps)) v = is_path v (a # ps) v'
[PROOF STEP]
have "...=is_path v (x#xs) v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (is_path x3 xs v' \<and> (x3, x2, x1) \<in> E \<and> is_path x1 [] v) = is_path v (x # xs) v'
[PROOF STEP]
by (metis corres is_path.simps(1) is_path.simps(2) is_path_memb x)
[PROOF STATE]
proof (state)
this:
(is_path x3 xs v' \<and> (x3, x2, x1) \<in> E \<and> is_path x1 [] v) = is_path v (x # xs) v'

goal (1 subgoal):
 1. \<And>a ps v. (\<And>v. is_path v' (rev_path ps) v = is_path v ps v') \<Longrightarrow> is_path v' (rev_path (a # ps)) v = is_path v (a # ps) v'
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
is_path v' (rev_path (x # xs)) v = is_path v (x # xs) v'
[PROOF STEP]
have "is_path v' (rev_path (x # xs)) v=is_path v (x#xs) v'"
[PROOF STATE]
proof (prove)
using this:
is_path v' (rev_path (x # xs)) v = is_path v (x # xs) v'

goal (1 subgoal):
 1. is_path v' (rev_path (x # xs)) v = is_path v (x # xs) v'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
is_path v' (rev_path (x # xs)) v = is_path v (x # xs) v'

goal (1 subgoal):
 1. \<And>a ps v. (\<And>v. is_path v' (rev_path ps) v = is_path v ps v') \<Longrightarrow> is_path v' (rev_path (a # ps)) v = is_path v (a # ps) v'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
is_path v' (rev_path (x # xs)) v = is_path v (x # xs) v'

goal (1 subgoal):
 1. is_path v' (rev_path (x # xs)) v = is_path v (x # xs) v'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
is_path v' (rev_path (x # xs)) v = is_path v (x # xs) v'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in valid_unMultigraph) singleton_distinct_path [intro]:
   "(v,w,v')\<in>E \<Longrightarrow> is_trail v [(v,w,v')] v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v, w, v') \<in> E \<Longrightarrow> is_trail v [(v, w, v')] v'
[PROOF STEP]
by (metis E_validD(2) all_not_in_conv is_trail.simps set_empty)


[STATEMENT]
lemma (in valid_unMultigraph) is_trail_path:
  "is_trail v ps v' \<longleftrightarrow> is_path v ps v' \<and> distinct ps \<and> (set ps \<inter> set (rev_path ps) = {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_trail v ps v' = (is_path v ps v' \<and> distinct ps \<and> set ps \<inter> set (rev_path ps) = {})
[PROOF STEP]
proof (induct ps arbitrary:v)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v. is_trail v [] v' = (is_path v [] v' \<and> distinct [] \<and> set [] \<inter> set (rev_path []) = {})
 2. \<And>a ps v. (\<And>v. is_trail v ps v' = (is_path v ps v' \<and> distinct ps \<and> set ps \<inter> set (rev_path ps) = {})) \<Longrightarrow> is_trail v (a # ps) v' = (is_path v (a # ps) v' \<and> distinct (a # ps) \<and> set (a # ps) \<inter> set (rev_path (a # ps)) = {})
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>v. is_trail v [] v' = (is_path v [] v' \<and> distinct [] \<and> set [] \<inter> set (rev_path []) = {})
 2. \<And>a ps v. (\<And>v. is_trail v ps v' = (is_path v ps v' \<and> distinct ps \<and> set ps \<inter> set (rev_path ps) = {})) \<Longrightarrow> is_trail v (a # ps) v' = (is_path v (a # ps) v' \<and> distinct (a # ps) \<and> set (a # ps) \<inter> set (rev_path (a # ps)) = {})
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_trail v [] v' = (is_path v [] v' \<and> distinct [] \<and> set [] \<inter> set (rev_path []) = {})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_trail v [] v' = (is_path v [] v' \<and> distinct [] \<and> set [] \<inter> set (rev_path []) = {})

goal (1 subgoal):
 1. \<And>a ps v. (\<And>v. is_trail v ps v' = (is_path v ps v' \<and> distinct ps \<and> set ps \<inter> set (rev_path ps) = {})) \<Longrightarrow> is_trail v (a # ps) v' = (is_path v (a # ps) v' \<and> distinct (a # ps) \<and> set (a # ps) \<inter> set (rev_path (a # ps)) = {})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ps v. (\<And>v. is_trail v ps v' = (is_path v ps v' \<and> distinct ps \<and> set ps \<inter> set (rev_path ps) = {})) \<Longrightarrow> is_trail v (a # ps) v' = (is_path v (a # ps) v' \<and> distinct (a # ps) \<and> set (a # ps) \<inter> set (rev_path (a # ps)) = {})
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
is_trail ?v xs v' = (is_path ?v xs v' \<and> distinct xs \<and> set xs \<inter> set (rev_path xs) = {})

goal (1 subgoal):
 1. \<And>a ps v. (\<And>v. is_trail v ps v' = (is_path v ps v' \<and> distinct ps \<and> set ps \<inter> set (rev_path ps) = {})) \<Longrightarrow> is_trail v (a # ps) v' = (is_path v (a # ps) v' \<and> distinct (a # ps) \<and> set (a # ps) \<inter> set (rev_path (a # ps)) = {})
[PROOF STEP]
obtain x1 x2 x3 where x: "x=(x1,x2,x3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x1 x2 x3. x = (x1, x2, x3) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod_cases3)
[PROOF STATE]
proof (state)
this:
x = (x1, x2, x3)

goal (1 subgoal):
 1. \<And>a ps v. (\<And>v. is_trail v ps v' = (is_path v ps v' \<and> distinct ps \<and> set ps \<inter> set (rev_path ps) = {})) \<Longrightarrow> is_trail v (a # ps) v' = (is_path v (a # ps) v' \<and> distinct (a # ps) \<and> set (a # ps) \<inter> set (rev_path (a # ps)) = {})
[PROOF STEP]
hence "is_trail v (x#xs) v'= (v=x1 \<and> (x1,x2,x3)\<in>E \<and>
                (x1,x2,x3)\<notin>set xs \<and>(x3,x2,x1)\<notin>set xs \<and> is_trail x3 xs v')"
[PROOF STATE]
proof (prove)
using this:
x = (x1, x2, x3)

goal (1 subgoal):
 1. is_trail v (x # xs) v' = (v = x1 \<and> (x1, x2, x3) \<in> E \<and> (x1, x2, x3) \<notin> set xs \<and> (x3, x2, x1) \<notin> set xs \<and> is_trail x3 xs v')
[PROOF STEP]
by (metis is_trail.simps(2))
[PROOF STATE]
proof (state)
this:
is_trail v (x # xs) v' = (v = x1 \<and> (x1, x2, x3) \<in> E \<and> (x1, x2, x3) \<notin> set xs \<and> (x3, x2, x1) \<notin> set xs \<and> is_trail x3 xs v')

goal (1 subgoal):
 1. \<And>a ps v. (\<And>v. is_trail v ps v' = (is_path v ps v' \<and> distinct ps \<and> set ps \<inter> set (rev_path ps) = {})) \<Longrightarrow> is_trail v (a # ps) v' = (is_path v (a # ps) v' \<and> distinct (a # ps) \<and> set (a # ps) \<inter> set (rev_path (a # ps)) = {})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
is_trail v (x # xs) v' = (v = x1 \<and> (x1, x2, x3) \<in> E \<and> (x1, x2, x3) \<notin> set xs \<and> (x3, x2, x1) \<notin> set xs \<and> is_trail x3 xs v')

goal (1 subgoal):
 1. \<And>a ps v. (\<And>v. is_trail v ps v' = (is_path v ps v' \<and> distinct ps \<and> set ps \<inter> set (rev_path ps) = {})) \<Longrightarrow> is_trail v (a # ps) v' = (is_path v (a # ps) v' \<and> distinct (a # ps) \<and> set (a # ps) \<inter> set (rev_path (a # ps)) = {})
[PROOF STEP]
have "...=(v=x1 \<and> (x1,x2,x3)\<in>E \<and>  (x1,x2,x3)\<notin>set xs \<and>(x3,x2,x1)\<notin>set xs \<and> is_path x3 xs v'
                  \<and> distinct xs \<and> (set xs \<inter> set (rev_path xs)={}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v = x1 \<and> (x1, x2, x3) \<in> E \<and> (x1, x2, x3) \<notin> set xs \<and> (x3, x2, x1) \<notin> set xs \<and> is_trail x3 xs v') = (v = x1 \<and> (x1, x2, x3) \<in> E \<and> (x1, x2, x3) \<notin> set xs \<and> (x3, x2, x1) \<notin> set xs \<and> is_path x3 xs v' \<and> distinct xs \<and> set xs \<inter> set (rev_path xs) = {})
[PROOF STEP]
using Cons.hyps
[PROOF STATE]
proof (prove)
using this:
is_trail ?v xs v' = (is_path ?v xs v' \<and> distinct xs \<and> set xs \<inter> set (rev_path xs) = {})

goal (1 subgoal):
 1. (v = x1 \<and> (x1, x2, x3) \<in> E \<and> (x1, x2, x3) \<notin> set xs \<and> (x3, x2, x1) \<notin> set xs \<and> is_trail x3 xs v') = (v = x1 \<and> (x1, x2, x3) \<in> E \<and> (x1, x2, x3) \<notin> set xs \<and> (x3, x2, x1) \<notin> set xs \<and> is_path x3 xs v' \<and> distinct xs \<and> set xs \<inter> set (rev_path xs) = {})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(v = x1 \<and> (x1, x2, x3) \<in> E \<and> (x1, x2, x3) \<notin> set xs \<and> (x3, x2, x1) \<notin> set xs \<and> is_trail x3 xs v') = (v = x1 \<and> (x1, x2, x3) \<in> E \<and> (x1, x2, x3) \<notin> set xs \<and> (x3, x2, x1) \<notin> set xs \<and> is_path x3 xs v' \<and> distinct xs \<and> set xs \<inter> set (rev_path xs) = {})

goal (1 subgoal):
 1. \<And>a ps v. (\<And>v. is_trail v ps v' = (is_path v ps v' \<and> distinct ps \<and> set ps \<inter> set (rev_path ps) = {})) \<Longrightarrow> is_trail v (a # ps) v' = (is_path v (a # ps) v' \<and> distinct (a # ps) \<and> set (a # ps) \<inter> set (rev_path (a # ps)) = {})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(v = x1 \<and> (x1, x2, x3) \<in> E \<and> (x1, x2, x3) \<notin> set xs \<and> (x3, x2, x1) \<notin> set xs \<and> is_trail x3 xs v') = (v = x1 \<and> (x1, x2, x3) \<in> E \<and> (x1, x2, x3) \<notin> set xs \<and> (x3, x2, x1) \<notin> set xs \<and> is_path x3 xs v' \<and> distinct xs \<and> set xs \<inter> set (rev_path xs) = {})

goal (1 subgoal):
 1. \<And>a ps v. (\<And>v. is_trail v ps v' = (is_path v ps v' \<and> distinct ps \<and> set ps \<inter> set (rev_path ps) = {})) \<Longrightarrow> is_trail v (a # ps) v' = (is_path v (a # ps) v' \<and> distinct (a # ps) \<and> set (a # ps) \<inter> set (rev_path (a # ps)) = {})
[PROOF STEP]
have "...=(is_path v (x#xs) v' \<and> (x1,x2,x3) \<noteq> (x3,x2,x1) \<and> (x1,x2,x3)\<notin>set xs
                  \<and>(x3,x2,x1)\<notin>set xs \<and> distinct xs \<and> (set xs \<inter> set (rev_path xs)={}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v = x1 \<and> (x1, x2, x3) \<in> E \<and> (x1, x2, x3) \<notin> set xs \<and> (x3, x2, x1) \<notin> set xs \<and> is_path x3 xs v' \<and> distinct xs \<and> set xs \<inter> set (rev_path xs) = {}) = (is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> (x1, x2, x3) \<notin> set xs \<and> (x3, x2, x1) \<notin> set xs \<and> distinct xs \<and> set xs \<inter> set (rev_path xs) = {})
[PROOF STEP]
by (metis append_Nil is_path.simps(1) is_path_simps(2) is_path_split' no_id x)
[PROOF STATE]
proof (state)
this:
(v = x1 \<and> (x1, x2, x3) \<in> E \<and> (x1, x2, x3) \<notin> set xs \<and> (x3, x2, x1) \<notin> set xs \<and> is_path x3 xs v' \<and> distinct xs \<and> set xs \<inter> set (rev_path xs) = {}) = (is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> (x1, x2, x3) \<notin> set xs \<and> (x3, x2, x1) \<notin> set xs \<and> distinct xs \<and> set xs \<inter> set (rev_path xs) = {})

goal (1 subgoal):
 1. \<And>a ps v. (\<And>v. is_trail v ps v' = (is_path v ps v' \<and> distinct ps \<and> set ps \<inter> set (rev_path ps) = {})) \<Longrightarrow> is_trail v (a # ps) v' = (is_path v (a # ps) v' \<and> distinct (a # ps) \<and> set (a # ps) \<inter> set (rev_path (a # ps)) = {})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(v = x1 \<and> (x1, x2, x3) \<in> E \<and> (x1, x2, x3) \<notin> set xs \<and> (x3, x2, x1) \<notin> set xs \<and> is_path x3 xs v' \<and> distinct xs \<and> set xs \<inter> set (rev_path xs) = {}) = (is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> (x1, x2, x3) \<notin> set xs \<and> (x3, x2, x1) \<notin> set xs \<and> distinct xs \<and> set xs \<inter> set (rev_path xs) = {})

goal (1 subgoal):
 1. \<And>a ps v. (\<And>v. is_trail v ps v' = (is_path v ps v' \<and> distinct ps \<and> set ps \<inter> set (rev_path ps) = {})) \<Longrightarrow> is_trail v (a # ps) v' = (is_path v (a # ps) v' \<and> distinct (a # ps) \<and> set (a # ps) \<inter> set (rev_path (a # ps)) = {})
[PROOF STEP]
have "...=(is_path v (x#xs) v' \<and> (x1,x2,x3) \<noteq> (x3,x2,x1) \<and>(x3,x2,x1)\<notin>set xs
                  \<and> distinct (x#xs) \<and> (set xs \<inter> set (rev_path xs)={}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> (x1, x2, x3) \<notin> set xs \<and> (x3, x2, x1) \<notin> set xs \<and> distinct xs \<and> set xs \<inter> set (rev_path xs) = {}) = (is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> (x3, x2, x1) \<notin> set xs \<and> distinct (x # xs) \<and> set xs \<inter> set (rev_path xs) = {})
[PROOF STEP]
by (metis (full_types) distinct.simps(2) x)
[PROOF STATE]
proof (state)
this:
(is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> (x1, x2, x3) \<notin> set xs \<and> (x3, x2, x1) \<notin> set xs \<and> distinct xs \<and> set xs \<inter> set (rev_path xs) = {}) = (is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> (x3, x2, x1) \<notin> set xs \<and> distinct (x # xs) \<and> set xs \<inter> set (rev_path xs) = {})

goal (1 subgoal):
 1. \<And>a ps v. (\<And>v. is_trail v ps v' = (is_path v ps v' \<and> distinct ps \<and> set ps \<inter> set (rev_path ps) = {})) \<Longrightarrow> is_trail v (a # ps) v' = (is_path v (a # ps) v' \<and> distinct (a # ps) \<and> set (a # ps) \<inter> set (rev_path (a # ps)) = {})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> (x1, x2, x3) \<notin> set xs \<and> (x3, x2, x1) \<notin> set xs \<and> distinct xs \<and> set xs \<inter> set (rev_path xs) = {}) = (is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> (x3, x2, x1) \<notin> set xs \<and> distinct (x # xs) \<and> set xs \<inter> set (rev_path xs) = {})

goal (1 subgoal):
 1. \<And>a ps v. (\<And>v. is_trail v ps v' = (is_path v ps v' \<and> distinct ps \<and> set ps \<inter> set (rev_path ps) = {})) \<Longrightarrow> is_trail v (a # ps) v' = (is_path v (a # ps) v' \<and> distinct (a # ps) \<and> set (a # ps) \<inter> set (rev_path (a # ps)) = {})
[PROOF STEP]
have "...=(is_path v (x#xs) v' \<and> (x1,x2,x3) \<noteq> (x3,x2,x1) \<and> distinct (x#xs)
                  \<and> (x3,x2,x1)\<notin>set xs \<and> set xs \<inter> set (rev_path (x#xs))={})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> (x3, x2, x1) \<notin> set xs \<and> distinct (x # xs) \<and> set xs \<inter> set (rev_path xs) = {}) = (is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> distinct (x # xs) \<and> (x3, x2, x1) \<notin> set xs \<and> set xs \<inter> set (rev_path (x # xs)) = {})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> (x3, x2, x1) \<notin> set xs \<and> distinct (x # xs) \<and> set xs \<inter> set (rev_path xs) = {}) = (is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> distinct (x # xs) \<and> (x3, x2, x1) \<notin> set xs \<and> set xs \<inter> set (rev_path (x # xs)) = {})
[PROOF STEP]
have "set (rev_path (x#xs)) = set ((rev_path xs)@[(x3,x2,x1)])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (rev_path (x # xs)) = set (rev_path xs @ [(x3, x2, x1)])
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
x = (x1, x2, x3)

goal (1 subgoal):
 1. set (rev_path (x # xs)) = set (rev_path xs @ [(x3, x2, x1)])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (rev_path (x # xs)) = set (rev_path xs @ [(x3, x2, x1)])

goal (1 subgoal):
 1. (is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> (x3, x2, x1) \<notin> set xs \<and> distinct (x # xs) \<and> set xs \<inter> set (rev_path xs) = {}) = (is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> distinct (x # xs) \<and> (x3, x2, x1) \<notin> set xs \<and> set xs \<inter> set (rev_path (x # xs)) = {})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set (rev_path (x # xs)) = set (rev_path xs @ [(x3, x2, x1)])

goal (1 subgoal):
 1. (is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> (x3, x2, x1) \<notin> set xs \<and> distinct (x # xs) \<and> set xs \<inter> set (rev_path xs) = {}) = (is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> distinct (x # xs) \<and> (x3, x2, x1) \<notin> set xs \<and> set xs \<inter> set (rev_path (x # xs)) = {})
[PROOF STEP]
have "... = set (rev_path xs) \<union> {(x3,x2,x1)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (rev_path xs @ [(x3, x2, x1)]) = set (rev_path xs) \<union> {(x3, x2, x1)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (rev_path xs @ [(x3, x2, x1)]) = set (rev_path xs) \<union> {(x3, x2, x1)}

goal (1 subgoal):
 1. (is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> (x3, x2, x1) \<notin> set xs \<and> distinct (x # xs) \<and> set xs \<inter> set (rev_path xs) = {}) = (is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> distinct (x # xs) \<and> (x3, x2, x1) \<notin> set xs \<and> set xs \<inter> set (rev_path (x # xs)) = {})
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
set (rev_path (x # xs)) = set (rev_path xs) \<union> {(x3, x2, x1)}
[PROOF STEP]
have "set (rev_path (x#xs))=set (rev_path xs) \<union> {(x3,x2,x1)}"
[PROOF STATE]
proof (prove)
using this:
set (rev_path (x # xs)) = set (rev_path xs) \<union> {(x3, x2, x1)}

goal (1 subgoal):
 1. set (rev_path (x # xs)) = set (rev_path xs) \<union> {(x3, x2, x1)}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
set (rev_path (x # xs)) = set (rev_path xs) \<union> {(x3, x2, x1)}

goal (1 subgoal):
 1. (is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> (x3, x2, x1) \<notin> set xs \<and> distinct (x # xs) \<and> set xs \<inter> set (rev_path xs) = {}) = (is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> distinct (x # xs) \<and> (x3, x2, x1) \<notin> set xs \<and> set xs \<inter> set (rev_path (x # xs)) = {})
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
set (rev_path (x # xs)) = set (rev_path xs) \<union> {(x3, x2, x1)}

goal (1 subgoal):
 1. (is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> (x3, x2, x1) \<notin> set xs \<and> distinct (x # xs) \<and> set xs \<inter> set (rev_path xs) = {}) = (is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> distinct (x # xs) \<and> (x3, x2, x1) \<notin> set xs \<and> set xs \<inter> set (rev_path (x # xs)) = {})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> (x3, x2, x1) \<notin> set xs \<and> distinct (x # xs) \<and> set xs \<inter> set (rev_path xs) = {}) = (is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> distinct (x # xs) \<and> (x3, x2, x1) \<notin> set xs \<and> set xs \<inter> set (rev_path (x # xs)) = {})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> (x3, x2, x1) \<notin> set xs \<and> distinct (x # xs) \<and> set xs \<inter> set (rev_path xs) = {}) = (is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> distinct (x # xs) \<and> (x3, x2, x1) \<notin> set xs \<and> set xs \<inter> set (rev_path (x # xs)) = {})

goal (1 subgoal):
 1. \<And>a ps v. (\<And>v. is_trail v ps v' = (is_path v ps v' \<and> distinct ps \<and> set ps \<inter> set (rev_path ps) = {})) \<Longrightarrow> is_trail v (a # ps) v' = (is_path v (a # ps) v' \<and> distinct (a # ps) \<and> set (a # ps) \<inter> set (rev_path (a # ps)) = {})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> (x3, x2, x1) \<notin> set xs \<and> distinct (x # xs) \<and> set xs \<inter> set (rev_path xs) = {}) = (is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> distinct (x # xs) \<and> (x3, x2, x1) \<notin> set xs \<and> set xs \<inter> set (rev_path (x # xs)) = {})

goal (1 subgoal):
 1. \<And>a ps v. (\<And>v. is_trail v ps v' = (is_path v ps v' \<and> distinct ps \<and> set ps \<inter> set (rev_path ps) = {})) \<Longrightarrow> is_trail v (a # ps) v' = (is_path v (a # ps) v' \<and> distinct (a # ps) \<and> set (a # ps) \<inter> set (rev_path (a # ps)) = {})
[PROOF STEP]
have "...=(is_path v (x#xs) v'\<and> distinct (x#xs) \<and> (set (x#xs) \<inter> set (rev_path (x#xs))={}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> distinct (x # xs) \<and> (x3, x2, x1) \<notin> set xs \<and> set xs \<inter> set (rev_path (x # xs)) = {}) = (is_path v (x # xs) v' \<and> distinct (x # xs) \<and> set (x # xs) \<inter> set (rev_path (x # xs)) = {})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> distinct (x # xs) \<and> (x3, x2, x1) \<notin> set xs \<and> set xs \<inter> set (rev_path (x # xs)) = {}) = (is_path v (x # xs) v' \<and> distinct (x # xs) \<and> set (x # xs) \<inter> set (rev_path (x # xs)) = {})
[PROOF STEP]
have "(x3,x2,x1)\<notin>set xs \<longleftrightarrow> (x1,x2,x3)\<notin> set (rev_path xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x3, x2, x1) \<notin> set xs) = ((x1, x2, x3) \<notin> set (rev_path xs))
[PROOF STEP]
using in_set_rev_path
[PROOF STATE]
proof (prove)
using this:
((?v', ?w, ?v) \<in> set (rev_path ?ps)) = ((?v, ?w, ?v') \<in> set ?ps)

goal (1 subgoal):
 1. ((x3, x2, x1) \<notin> set xs) = ((x1, x2, x3) \<notin> set (rev_path xs))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((x3, x2, x1) \<notin> set xs) = ((x1, x2, x3) \<notin> set (rev_path xs))

goal (1 subgoal):
 1. (is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> distinct (x # xs) \<and> (x3, x2, x1) \<notin> set xs \<and> set xs \<inter> set (rev_path (x # xs)) = {}) = (is_path v (x # xs) v' \<and> distinct (x # xs) \<and> set (x # xs) \<inter> set (rev_path (x # xs)) = {})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
((x3, x2, x1) \<notin> set xs) = ((x1, x2, x3) \<notin> set (rev_path xs))

goal (1 subgoal):
 1. (is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> distinct (x # xs) \<and> (x3, x2, x1) \<notin> set xs \<and> set xs \<inter> set (rev_path (x # xs)) = {}) = (is_path v (x # xs) v' \<and> distinct (x # xs) \<and> set (x # xs) \<inter> set (rev_path (x # xs)) = {})
[PROOF STEP]
have  "set (rev_path (x#xs))=set (rev_path xs) \<union> {(x3,x2,x1)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (rev_path (x # xs)) = set (rev_path xs) \<union> {(x3, x2, x1)}
[PROOF STEP]
unfolding rev_path_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map (\<lambda>(a, b, c). (c, b, a)) (rev (x # xs))) = set (map (\<lambda>(a, b, c). (c, b, a)) (rev xs)) \<union> {(x3, x2, x1)}
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
x = (x1, x2, x3)

goal (1 subgoal):
 1. set (map (\<lambda>(a, b, c). (c, b, a)) (rev (x # xs))) = set (map (\<lambda>(a, b, c). (c, b, a)) (rev xs)) \<union> {(x3, x2, x1)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (rev_path (x # xs)) = set (rev_path xs) \<union> {(x3, x2, x1)}

goal (1 subgoal):
 1. (is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> distinct (x # xs) \<and> (x3, x2, x1) \<notin> set xs \<and> set xs \<inter> set (rev_path (x # xs)) = {}) = (is_path v (x # xs) v' \<and> distinct (x # xs) \<and> set (x # xs) \<inter> set (rev_path (x # xs)) = {})
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
((x3, x2, x1) \<notin> set xs) = ((x1, x2, x3) \<notin> set (rev_path xs))
set (rev_path (x # xs)) = set (rev_path xs) \<union> {(x3, x2, x1)}
[PROOF STEP]
have " (x1,x2,x3) \<noteq> (x3,x2,x1)\<and> (x3,x2,x1)\<notin>set xs
                        \<longleftrightarrow> (x1,x2,x3)\<notin> set (rev_path (x#xs))"
[PROOF STATE]
proof (prove)
using this:
((x3, x2, x1) \<notin> set xs) = ((x1, x2, x3) \<notin> set (rev_path xs))
set (rev_path (x # xs)) = set (rev_path xs) \<union> {(x3, x2, x1)}

goal (1 subgoal):
 1. ((x1, x2, x3) \<noteq> (x3, x2, x1) \<and> (x3, x2, x1) \<notin> set xs) = ((x1, x2, x3) \<notin> set (rev_path (x # xs)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
((x1, x2, x3) \<noteq> (x3, x2, x1) \<and> (x3, x2, x1) \<notin> set xs) = ((x1, x2, x3) \<notin> set (rev_path (x # xs)))

goal (1 subgoal):
 1. (is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> distinct (x # xs) \<and> (x3, x2, x1) \<notin> set xs \<and> set xs \<inter> set (rev_path (x # xs)) = {}) = (is_path v (x # xs) v' \<and> distinct (x # xs) \<and> set (x # xs) \<inter> set (rev_path (x # xs)) = {})
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
((x1, x2, x3) \<noteq> (x3, x2, x1) \<and> (x3, x2, x1) \<notin> set xs) = ((x1, x2, x3) \<notin> set (rev_path (x # xs)))

goal (1 subgoal):
 1. (is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> distinct (x # xs) \<and> (x3, x2, x1) \<notin> set xs \<and> set xs \<inter> set (rev_path (x # xs)) = {}) = (is_path v (x # xs) v' \<and> distinct (x # xs) \<and> set (x # xs) \<inter> set (rev_path (x # xs)) = {})
[PROOF STEP]
by (metis (mono_tags) Int_iff Int_insert_left_if0 List.set_simps(2) empty_iff insertI1 x)
[PROOF STATE]
proof (state)
this:
(is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> distinct (x # xs) \<and> (x3, x2, x1) \<notin> set xs \<and> set xs \<inter> set (rev_path (x # xs)) = {}) = (is_path v (x # xs) v' \<and> distinct (x # xs) \<and> set (x # xs) \<inter> set (rev_path (x # xs)) = {})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(is_path v (x # xs) v' \<and> (x1, x2, x3) \<noteq> (x3, x2, x1) \<and> distinct (x # xs) \<and> (x3, x2, x1) \<notin> set xs \<and> set xs \<inter> set (rev_path (x # xs)) = {}) = (is_path v (x # xs) v' \<and> distinct (x # xs) \<and> set (x # xs) \<inter> set (rev_path (x # xs)) = {})

goal (1 subgoal):
 1. \<And>a ps v. (\<And>v. is_trail v ps v' = (is_path v ps v' \<and> distinct ps \<and> set ps \<inter> set (rev_path ps) = {})) \<Longrightarrow> is_trail v (a # ps) v' = (is_path v (a # ps) v' \<and> distinct (a # ps) \<and> set (a # ps) \<inter> set (rev_path (a # ps)) = {})
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
is_trail v (x # xs) v' = (is_path v (x # xs) v' \<and> distinct (x # xs) \<and> set (x # xs) \<inter> set (rev_path (x # xs)) = {})
[PROOF STEP]
have "is_trail v (x#xs) v'\<longleftrightarrow>(is_path v (x#xs) v'\<and> distinct (x#xs)
                  \<and> (set (x#xs) \<inter> set (rev_path (x#xs))={}))"
[PROOF STATE]
proof (prove)
using this:
is_trail v (x # xs) v' = (is_path v (x # xs) v' \<and> distinct (x # xs) \<and> set (x # xs) \<inter> set (rev_path (x # xs)) = {})

goal (1 subgoal):
 1. is_trail v (x # xs) v' = (is_path v (x # xs) v' \<and> distinct (x # xs) \<and> set (x # xs) \<inter> set (rev_path (x # xs)) = {})
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
is_trail v (x # xs) v' = (is_path v (x # xs) v' \<and> distinct (x # xs) \<and> set (x # xs) \<inter> set (rev_path (x # xs)) = {})

goal (1 subgoal):
 1. \<And>a ps v. (\<And>v. is_trail v ps v' = (is_path v ps v' \<and> distinct ps \<and> set ps \<inter> set (rev_path ps) = {})) \<Longrightarrow> is_trail v (a # ps) v' = (is_path v (a # ps) v' \<and> distinct (a # ps) \<and> set (a # ps) \<inter> set (rev_path (a # ps)) = {})
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
is_trail v (x # xs) v' = (is_path v (x # xs) v' \<and> distinct (x # xs) \<and> set (x # xs) \<inter> set (rev_path (x # xs)) = {})

goal (1 subgoal):
 1. is_trail v (x # xs) v' = (is_path v (x # xs) v' \<and> distinct (x # xs) \<and> set (x # xs) \<inter> set (rev_path (x # xs)) = {})
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
is_trail v (x # xs) v' = (is_path v (x # xs) v' \<and> distinct (x # xs) \<and> set (x # xs) \<inter> set (rev_path (x # xs)) = {})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma  (in valid_unMultigraph) is_trail_rev:
    "is_trail v' (rev_path ps) v \<longleftrightarrow> is_trail v ps v' "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_trail v' (rev_path ps) v = is_trail v ps v'
[PROOF STEP]
using rev_path_append is_trail_path  is_path_rev distinct_rev_path
[PROOF STATE]
proof (prove)
using this:
rev_path (?xs @ ?ys) = rev_path ?ys @ rev_path ?xs
is_trail ?v ?ps ?v' = (is_path ?v ?ps ?v' \<and> distinct ?ps \<and> set ?ps \<inter> set (rev_path ?ps) = {})
is_path ?v' (rev_path ?ps) ?v = is_path ?v ?ps ?v'
distinct (rev_path ?ps) = distinct ?ps

goal (1 subgoal):
 1. is_trail v' (rev_path ps) v = is_trail v ps v'
[PROOF STEP]
by (metis Int_commute distinct_append)


[STATEMENT]
lemma (in valid_unMultigraph) is_trail_intro[intro]:
  "is_trail v' ps v \<Longrightarrow> is_path v' ps v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_trail v' ps v \<Longrightarrow> is_path v' ps v
[PROOF STEP]
by (induct ps arbitrary:v',auto)


[STATEMENT]
lemma (in valid_unMultigraph) is_trail_split:
      "is_trail v (p1@p2) v' \<Longrightarrow> (\<exists>u. is_trail v p1 u \<and> is_trail u p2 v')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_trail v (p1 @ p2) v' \<Longrightarrow> \<exists>u. is_trail v p1 u \<and> is_trail u p2 v'
[PROOF STEP]
apply (induct p1 arbitrary: v,auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. is_trail v p2 v' \<Longrightarrow> v \<in> V
[PROOF STEP]
apply (metis is_trail_intro is_path_memb)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in valid_unMultigraph) is_trail_split':"is_trail v (p1@(u,w,u')#p2) v'
    \<Longrightarrow> is_trail v p1 u \<and> (u,w,u')\<in>E \<and> is_trail u' p2 v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_trail v (p1 @ (u, w, u') # p2) v' \<Longrightarrow> is_trail v p1 u \<and> (u, w, u') \<in> E \<and> is_trail u' p2 v'
[PROOF STEP]
by (metis is_trail.simps(2) is_trail_split)


[STATEMENT]
lemma (in valid_unMultigraph) distinct_elim[simp]:
  assumes "is_trail v ((v1,w,v2)#ps) v'"
  shows "(v1,w,v2)\<in>edges(rem_unPath ps G) \<longleftrightarrow> (v1,w,v2)\<in>E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((v1, w, v2) \<in> edges (rem_unPath ps G)) = ((v1, w, v2) \<in> E)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (v1, w, v2) \<in> edges (rem_unPath ps G) \<Longrightarrow> (v1, w, v2) \<in> E
 2. (v1, w, v2) \<in> E \<Longrightarrow> (v1, w, v2) \<in> edges (rem_unPath ps G)
[PROOF STEP]
assume "(v1, w, v2) \<in> edges (rem_unPath ps G)"
[PROOF STATE]
proof (state)
this:
(v1, w, v2) \<in> edges (rem_unPath ps G)

goal (2 subgoals):
 1. (v1, w, v2) \<in> edges (rem_unPath ps G) \<Longrightarrow> (v1, w, v2) \<in> E
 2. (v1, w, v2) \<in> E \<Longrightarrow> (v1, w, v2) \<in> edges (rem_unPath ps G)
[PROOF STEP]
thus "(v1, w, v2) \<in> E"
[PROOF STATE]
proof (prove)
using this:
(v1, w, v2) \<in> edges (rem_unPath ps G)

goal (1 subgoal):
 1. (v1, w, v2) \<in> E
[PROOF STEP]
by (metis assms is_trail.simps(2))
[PROOF STATE]
proof (state)
this:
(v1, w, v2) \<in> E

goal (1 subgoal):
 1. (v1, w, v2) \<in> E \<Longrightarrow> (v1, w, v2) \<in> edges (rem_unPath ps G)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (v1, w, v2) \<in> E \<Longrightarrow> (v1, w, v2) \<in> edges (rem_unPath ps G)
[PROOF STEP]
assume "(v1, w, v2) \<in> E"
[PROOF STATE]
proof (state)
this:
(v1, w, v2) \<in> E

goal (1 subgoal):
 1. (v1, w, v2) \<in> E \<Longrightarrow> (v1, w, v2) \<in> edges (rem_unPath ps G)
[PROOF STEP]
have "(v1,w,v2)\<notin>set ps \<and> (v2,w,v1)\<notin>set ps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v1, w, v2) \<notin> set ps \<and> (v2, w, v1) \<notin> set ps
[PROOF STEP]
by (metis assms is_trail.simps(2))
[PROOF STATE]
proof (state)
this:
(v1, w, v2) \<notin> set ps \<and> (v2, w, v1) \<notin> set ps

goal (1 subgoal):
 1. (v1, w, v2) \<in> E \<Longrightarrow> (v1, w, v2) \<in> edges (rem_unPath ps G)
[PROOF STEP]
hence "(v1,w,v2)\<notin>set ps \<and> (v1,w,v2)\<notin>set (rev_path ps)"
[PROOF STATE]
proof (prove)
using this:
(v1, w, v2) \<notin> set ps \<and> (v2, w, v1) \<notin> set ps

goal (1 subgoal):
 1. (v1, w, v2) \<notin> set ps \<and> (v1, w, v2) \<notin> set (rev_path ps)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(v1, w, v2) \<notin> set ps \<and> (v1, w, v2) \<notin> set (rev_path ps)

goal (1 subgoal):
 1. (v1, w, v2) \<in> E \<Longrightarrow> (v1, w, v2) \<in> edges (rem_unPath ps G)
[PROOF STEP]
hence "(v1,w,v2)\<notin>set ps \<union> set (rev_path ps)"
[PROOF STATE]
proof (prove)
using this:
(v1, w, v2) \<notin> set ps \<and> (v1, w, v2) \<notin> set (rev_path ps)

goal (1 subgoal):
 1. (v1, w, v2) \<notin> set ps \<union> set (rev_path ps)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(v1, w, v2) \<notin> set ps \<union> set (rev_path ps)

goal (1 subgoal):
 1. (v1, w, v2) \<in> E \<Longrightarrow> (v1, w, v2) \<in> edges (rem_unPath ps G)
[PROOF STEP]
hence "(v1,w,v2)\<in>edges G - (set ps \<union> set (rev_path ps))"
[PROOF STATE]
proof (prove)
using this:
(v1, w, v2) \<notin> set ps \<union> set (rev_path ps)

goal (1 subgoal):
 1. (v1, w, v2) \<in> E - (set ps \<union> set (rev_path ps))
[PROOF STEP]
using \<open>(v1, w, v2) \<in> E\<close>
[PROOF STATE]
proof (prove)
using this:
(v1, w, v2) \<notin> set ps \<union> set (rev_path ps)
(v1, w, v2) \<in> E

goal (1 subgoal):
 1. (v1, w, v2) \<in> E - (set ps \<union> set (rev_path ps))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(v1, w, v2) \<in> E - (set ps \<union> set (rev_path ps))

goal (1 subgoal):
 1. (v1, w, v2) \<in> E \<Longrightarrow> (v1, w, v2) \<in> edges (rem_unPath ps G)
[PROOF STEP]
thus "(v1,w,v2)\<in>edges(rem_unPath ps G)"
[PROOF STATE]
proof (prove)
using this:
(v1, w, v2) \<in> E - (set ps \<union> set (rev_path ps))

goal (1 subgoal):
 1. (v1, w, v2) \<in> edges (rem_unPath ps G)
[PROOF STEP]
by (metis rem_unPath_edges)
[PROOF STATE]
proof (state)
this:
(v1, w, v2) \<in> edges (rem_unPath ps G)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma distinct_path_subset:
  assumes "valid_unMultigraph G1" "valid_unMultigraph G2" "edges G1 \<subseteq>edges G2" "nodes G1 \<subseteq>nodes G2"
  assumes distinct_G1:"valid_unMultigraph.is_trail G1 v ps v'"
  shows "valid_unMultigraph.is_trail G2 v ps v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_unMultigraph.is_trail G2 v ps v'
[PROOF STEP]
using distinct_G1
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph.is_trail G1 v ps v'

goal (1 subgoal):
 1. valid_unMultigraph.is_trail G2 v ps v'
[PROOF STEP]
proof (induct ps arbitrary:v)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v. valid_unMultigraph.is_trail G1 v [] v' \<Longrightarrow> valid_unMultigraph.is_trail G2 v [] v'
 2. \<And>a ps v. \<lbrakk>\<And>v. valid_unMultigraph.is_trail G1 v ps v' \<Longrightarrow> valid_unMultigraph.is_trail G2 v ps v'; valid_unMultigraph.is_trail G1 v (a # ps) v'\<rbrakk> \<Longrightarrow> valid_unMultigraph.is_trail G2 v (a # ps) v'
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
valid_unMultigraph.is_trail G1 v [] v'

goal (2 subgoals):
 1. \<And>v. valid_unMultigraph.is_trail G1 v [] v' \<Longrightarrow> valid_unMultigraph.is_trail G2 v [] v'
 2. \<And>a ps v. \<lbrakk>\<And>v. valid_unMultigraph.is_trail G1 v ps v' \<Longrightarrow> valid_unMultigraph.is_trail G2 v ps v'; valid_unMultigraph.is_trail G1 v (a # ps) v'\<rbrakk> \<Longrightarrow> valid_unMultigraph.is_trail G2 v (a # ps) v'
[PROOF STEP]
hence "v=v'\<and>v'\<in>nodes G1"
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph.is_trail G1 v [] v'

goal (1 subgoal):
 1. v = v' \<and> v' \<in> nodes G1
[PROOF STEP]
by (metis (full_types) assms(1) valid_unMultigraph.is_trail.simps(1))
[PROOF STATE]
proof (state)
this:
v = v' \<and> v' \<in> nodes G1

goal (2 subgoals):
 1. \<And>v. valid_unMultigraph.is_trail G1 v [] v' \<Longrightarrow> valid_unMultigraph.is_trail G2 v [] v'
 2. \<And>a ps v. \<lbrakk>\<And>v. valid_unMultigraph.is_trail G1 v ps v' \<Longrightarrow> valid_unMultigraph.is_trail G2 v ps v'; valid_unMultigraph.is_trail G1 v (a # ps) v'\<rbrakk> \<Longrightarrow> valid_unMultigraph.is_trail G2 v (a # ps) v'
[PROOF STEP]
hence "v=v'\<and>v'\<in>nodes G2"
[PROOF STATE]
proof (prove)
using this:
v = v' \<and> v' \<in> nodes G1

goal (1 subgoal):
 1. v = v' \<and> v' \<in> nodes G2
[PROOF STEP]
using \<open>nodes G1 \<subseteq> nodes G2\<close>
[PROOF STATE]
proof (prove)
using this:
v = v' \<and> v' \<in> nodes G1
nodes G1 \<subseteq> nodes G2

goal (1 subgoal):
 1. v = v' \<and> v' \<in> nodes G2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v = v' \<and> v' \<in> nodes G2

goal (2 subgoals):
 1. \<And>v. valid_unMultigraph.is_trail G1 v [] v' \<Longrightarrow> valid_unMultigraph.is_trail G2 v [] v'
 2. \<And>a ps v. \<lbrakk>\<And>v. valid_unMultigraph.is_trail G1 v ps v' \<Longrightarrow> valid_unMultigraph.is_trail G2 v ps v'; valid_unMultigraph.is_trail G1 v (a # ps) v'\<rbrakk> \<Longrightarrow> valid_unMultigraph.is_trail G2 v (a # ps) v'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
v = v' \<and> v' \<in> nodes G2

goal (1 subgoal):
 1. valid_unMultigraph.is_trail G2 v [] v'
[PROOF STEP]
by (metis assms(2) valid_unMultigraph.is_trail.simps(1))
[PROOF STATE]
proof (state)
this:
valid_unMultigraph.is_trail G2 v [] v'

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. valid_unMultigraph.is_trail G1 v ps v' \<Longrightarrow> valid_unMultigraph.is_trail G2 v ps v'; valid_unMultigraph.is_trail G1 v (a # ps) v'\<rbrakk> \<Longrightarrow> valid_unMultigraph.is_trail G2 v (a # ps) v'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. valid_unMultigraph.is_trail G1 v ps v' \<Longrightarrow> valid_unMultigraph.is_trail G2 v ps v'; valid_unMultigraph.is_trail G1 v (a # ps) v'\<rbrakk> \<Longrightarrow> valid_unMultigraph.is_trail G2 v (a # ps) v'
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
valid_unMultigraph.is_trail G1 ?v xs v' \<Longrightarrow> valid_unMultigraph.is_trail G2 ?v xs v'
valid_unMultigraph.is_trail G1 v (x # xs) v'

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. valid_unMultigraph.is_trail G1 v ps v' \<Longrightarrow> valid_unMultigraph.is_trail G2 v ps v'; valid_unMultigraph.is_trail G1 v (a # ps) v'\<rbrakk> \<Longrightarrow> valid_unMultigraph.is_trail G2 v (a # ps) v'
[PROOF STEP]
obtain x1 x2 x3 where x:"x=(x1,x2,x3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x1 x2 x3. x = (x1, x2, x3) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod_cases3)
[PROOF STATE]
proof (state)
this:
x = (x1, x2, x3)

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. valid_unMultigraph.is_trail G1 v ps v' \<Longrightarrow> valid_unMultigraph.is_trail G2 v ps v'; valid_unMultigraph.is_trail G1 v (a # ps) v'\<rbrakk> \<Longrightarrow> valid_unMultigraph.is_trail G2 v (a # ps) v'
[PROOF STEP]
hence "valid_unMultigraph.is_trail G1 x3 xs v'"
[PROOF STATE]
proof (prove)
using this:
x = (x1, x2, x3)

goal (1 subgoal):
 1. valid_unMultigraph.is_trail G1 x3 xs v'
[PROOF STEP]
by (metis Cons.prems assms(1) valid_unMultigraph.is_trail.simps(2))
[PROOF STATE]
proof (state)
this:
valid_unMultigraph.is_trail G1 x3 xs v'

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. valid_unMultigraph.is_trail G1 v ps v' \<Longrightarrow> valid_unMultigraph.is_trail G2 v ps v'; valid_unMultigraph.is_trail G1 v (a # ps) v'\<rbrakk> \<Longrightarrow> valid_unMultigraph.is_trail G2 v (a # ps) v'
[PROOF STEP]
hence "valid_unMultigraph.is_trail G2 x3 xs v'"
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph.is_trail G1 x3 xs v'

goal (1 subgoal):
 1. valid_unMultigraph.is_trail G2 x3 xs v'
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph.is_trail G1 x3 xs v'
valid_unMultigraph.is_trail G1 ?v xs v' \<Longrightarrow> valid_unMultigraph.is_trail G2 ?v xs v'
valid_unMultigraph.is_trail G1 v (x # xs) v'

goal (1 subgoal):
 1. valid_unMultigraph.is_trail G2 x3 xs v'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_unMultigraph.is_trail G2 x3 xs v'

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. valid_unMultigraph.is_trail G1 v ps v' \<Longrightarrow> valid_unMultigraph.is_trail G2 v ps v'; valid_unMultigraph.is_trail G1 v (a # ps) v'\<rbrakk> \<Longrightarrow> valid_unMultigraph.is_trail G2 v (a # ps) v'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
valid_unMultigraph.is_trail G2 x3 xs v'

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. valid_unMultigraph.is_trail G1 v ps v' \<Longrightarrow> valid_unMultigraph.is_trail G2 v ps v'; valid_unMultigraph.is_trail G1 v (a # ps) v'\<rbrakk> \<Longrightarrow> valid_unMultigraph.is_trail G2 v (a # ps) v'
[PROOF STEP]
have "x\<in>edges G1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> edges G1
[PROOF STEP]
by (metis Cons.prems assms(1) valid_unMultigraph.is_trail.simps(2) x)
[PROOF STATE]
proof (state)
this:
x \<in> edges G1

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. valid_unMultigraph.is_trail G1 v ps v' \<Longrightarrow> valid_unMultigraph.is_trail G2 v ps v'; valid_unMultigraph.is_trail G1 v (a # ps) v'\<rbrakk> \<Longrightarrow> valid_unMultigraph.is_trail G2 v (a # ps) v'
[PROOF STEP]
hence "x\<in>edges G2"
[PROOF STATE]
proof (prove)
using this:
x \<in> edges G1

goal (1 subgoal):
 1. x \<in> edges G2
[PROOF STEP]
using \<open>edges G1 \<subseteq> edges G2\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> edges G1
edges G1 \<subseteq> edges G2

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

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. valid_unMultigraph.is_trail G1 v ps v' \<Longrightarrow> valid_unMultigraph.is_trail G2 v ps v'; valid_unMultigraph.is_trail G1 v (a # ps) v'\<rbrakk> \<Longrightarrow> valid_unMultigraph.is_trail G2 v (a # ps) v'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> edges G2

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. valid_unMultigraph.is_trail G1 v ps v' \<Longrightarrow> valid_unMultigraph.is_trail G2 v ps v'; valid_unMultigraph.is_trail G1 v (a # ps) v'\<rbrakk> \<Longrightarrow> valid_unMultigraph.is_trail G2 v (a # ps) v'
[PROOF STEP]
have "v=x1\<and>(x1,x2,x3)\<notin>set xs\<and>(x3,x2,x1)\<notin>set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v = x1 \<and> (x1, x2, x3) \<notin> set xs \<and> (x3, x2, x1) \<notin> set xs
[PROOF STEP]
by (metis Cons.prems assms(1) valid_unMultigraph.is_trail.simps(2) x)
[PROOF STATE]
proof (state)
this:
v = x1 \<and> (x1, x2, x3) \<notin> set xs \<and> (x3, x2, x1) \<notin> set xs

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. valid_unMultigraph.is_trail G1 v ps v' \<Longrightarrow> valid_unMultigraph.is_trail G2 v ps v'; valid_unMultigraph.is_trail G1 v (a # ps) v'\<rbrakk> \<Longrightarrow> valid_unMultigraph.is_trail G2 v (a # ps) v'
[PROOF STEP]
hence "v=x1" "(x1,x2,x3)\<notin>set xs" "(x3,x2,x1)\<notin>set xs"
[PROOF STATE]
proof (prove)
using this:
v = x1 \<and> (x1, x2, x3) \<notin> set xs \<and> (x3, x2, x1) \<notin> set xs

goal (1 subgoal):
 1. v = x1 &&& (x1, x2, x3) \<notin> set xs &&& (x3, x2, x1) \<notin> set xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v = x1
(x1, x2, x3) \<notin> set xs
(x3, x2, x1) \<notin> set xs

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. valid_unMultigraph.is_trail G1 v ps v' \<Longrightarrow> valid_unMultigraph.is_trail G2 v ps v'; valid_unMultigraph.is_trail G1 v (a # ps) v'\<rbrakk> \<Longrightarrow> valid_unMultigraph.is_trail G2 v (a # ps) v'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
valid_unMultigraph.is_trail G2 x3 xs v'
x \<in> edges G2
v = x1
(x1, x2, x3) \<notin> set xs
(x3, x2, x1) \<notin> set xs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph.is_trail G2 x3 xs v'
x \<in> edges G2
v = x1
(x1, x2, x3) \<notin> set xs
(x3, x2, x1) \<notin> set xs

goal (1 subgoal):
 1. valid_unMultigraph.is_trail G2 v (x # xs) v'
[PROOF STEP]
by (metis assms(2) valid_unMultigraph.is_trail.simps(2) x)
[PROOF STATE]
proof (state)
this:
valid_unMultigraph.is_trail G2 v (x # xs) v'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in valid_unMultigraph) distinct_path_intro':
  assumes "valid_unMultigraph.is_trail (rem_unPath p G) v ps v'"
  shows "is_trail  v ps v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_trail v ps v'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_trail v ps v'
[PROOF STEP]
have valid:"valid_unMultigraph (rem_unPath p G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_unMultigraph (rem_unPath p G)
[PROOF STEP]
using rem_unPath_valid[OF valid_unMultigraph_axioms,of p]
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph (rem_unPath p G)

goal (1 subgoal):
 1. valid_unMultigraph (rem_unPath p G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_unMultigraph (rem_unPath p G)

goal (1 subgoal):
 1. is_trail v ps v'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
valid_unMultigraph (rem_unPath p G)

goal (1 subgoal):
 1. is_trail v ps v'
[PROOF STEP]
have "nodes (rem_unPath p G) \<subseteq> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nodes (rem_unPath p G) \<subseteq> V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nodes (rem_unPath p G) \<subseteq> V

goal (1 subgoal):
 1. is_trail v ps v'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nodes (rem_unPath p G) \<subseteq> V

goal (1 subgoal):
 1. is_trail v ps v'
[PROOF STEP]
have "edges (rem_unPath p G) \<subseteq> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. edges (rem_unPath p G) \<subseteq> E
[PROOF STEP]
using rem_unPath_edges
[PROOF STATE]
proof (prove)
using this:
edges (rem_unPath ?ps ?G) = edges ?G - (set ?ps \<union> set (rev_path ?ps))

goal (1 subgoal):
 1. edges (rem_unPath p G) \<subseteq> E
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
edges (rem_unPath p G) \<subseteq> E

goal (1 subgoal):
 1. is_trail v ps v'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
valid_unMultigraph (rem_unPath p G)
nodes (rem_unPath p G) \<subseteq> V
edges (rem_unPath p G) \<subseteq> E
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph (rem_unPath p G)
nodes (rem_unPath p G) \<subseteq> V
edges (rem_unPath p G) \<subseteq> E

goal (1 subgoal):
 1. is_trail v ps v'
[PROOF STEP]
using distinct_path_subset[of "rem_unPath p G" G] valid_unMultigraph_axioms assms
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph (rem_unPath p G)
nodes (rem_unPath p G) \<subseteq> V
edges (rem_unPath p G) \<subseteq> E
\<lbrakk>valid_unMultigraph (rem_unPath p G); valid_unMultigraph G; edges (rem_unPath p G) \<subseteq> E; nodes (rem_unPath p G) \<subseteq> V; valid_unMultigraph.is_trail (rem_unPath p G) ?v ?ps ?v'\<rbrakk> \<Longrightarrow> is_trail ?v ?ps ?v'
valid_unMultigraph G
valid_unMultigraph.is_trail (rem_unPath p G) v ps v'

goal (1 subgoal):
 1. is_trail v ps v'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_trail v ps v'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in valid_unMultigraph) distinct_path_intro:
  assumes "valid_unMultigraph.is_trail (del_unEdge x1 x2 x3 G) v ps v'"
  shows "is_trail  v ps v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_trail v ps v'
[PROOF STEP]
by (metis (full_types) assms distinct_path_intro' rem_unPath.simps(1)
    rem_unPath.simps(2))


[STATEMENT]
lemma (in valid_unMultigraph) distinct_elim_rev[simp]:
  assumes "is_trail v ((v1,w,v2)#ps) v'"
  shows "(v2,w,v1)\<in>edges(rem_unPath ps G) \<longleftrightarrow> (v2,w,v1)\<in>E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((v2, w, v1) \<in> edges (rem_unPath ps G)) = ((v2, w, v1) \<in> E)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((v2, w, v1) \<in> edges (rem_unPath ps G)) = ((v2, w, v1) \<in> E)
[PROOF STEP]
have  "valid_unMultigraph (rem_unPath ps G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_unMultigraph (rem_unPath ps G)
[PROOF STEP]
using valid_unMultigraph_axioms
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph G

goal (1 subgoal):
 1. valid_unMultigraph (rem_unPath ps G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_unMultigraph (rem_unPath ps G)

goal (1 subgoal):
 1. ((v2, w, v1) \<in> edges (rem_unPath ps G)) = ((v2, w, v1) \<in> E)
[PROOF STEP]
hence "(v2,w,v1)\<in>edges(rem_unPath ps G)\<longleftrightarrow>(v1,w,v2)\<in>edges(rem_unPath ps G)"
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph (rem_unPath ps G)

goal (1 subgoal):
 1. ((v2, w, v1) \<in> edges (rem_unPath ps G)) = ((v1, w, v2) \<in> edges (rem_unPath ps G))
[PROOF STEP]
by (metis valid_unMultigraph.corres)
[PROOF STATE]
proof (state)
this:
((v2, w, v1) \<in> edges (rem_unPath ps G)) = ((v1, w, v2) \<in> edges (rem_unPath ps G))

goal (1 subgoal):
 1. ((v2, w, v1) \<in> edges (rem_unPath ps G)) = ((v2, w, v1) \<in> E)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
((v2, w, v1) \<in> edges (rem_unPath ps G)) = ((v1, w, v2) \<in> edges (rem_unPath ps G))

goal (1 subgoal):
 1. ((v2, w, v1) \<in> edges (rem_unPath ps G)) = ((v2, w, v1) \<in> E)
[PROOF STEP]
have "(v2,w,v1)\<in>E\<longleftrightarrow>(v1,w,v2)\<in>E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((v2, w, v1) \<in> E) = ((v1, w, v2) \<in> E)
[PROOF STEP]
using corres
[PROOF STATE]
proof (prove)
using this:
((?v, ?w, ?u') \<in> E) = ((?u', ?w, ?v) \<in> E)

goal (1 subgoal):
 1. ((v2, w, v1) \<in> E) = ((v1, w, v2) \<in> E)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((v2, w, v1) \<in> E) = ((v1, w, v2) \<in> E)

goal (1 subgoal):
 1. ((v2, w, v1) \<in> edges (rem_unPath ps G)) = ((v2, w, v1) \<in> E)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
((v2, w, v1) \<in> edges (rem_unPath ps G)) = ((v1, w, v2) \<in> edges (rem_unPath ps G))
((v2, w, v1) \<in> E) = ((v1, w, v2) \<in> E)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((v2, w, v1) \<in> edges (rem_unPath ps G)) = ((v1, w, v2) \<in> edges (rem_unPath ps G))
((v2, w, v1) \<in> E) = ((v1, w, v2) \<in> E)

goal (1 subgoal):
 1. ((v2, w, v1) \<in> edges (rem_unPath ps G)) = ((v2, w, v1) \<in> E)
[PROOF STEP]
using distinct_elim
[PROOF STATE]
proof (prove)
using this:
((v2, w, v1) \<in> edges (rem_unPath ps G)) = ((v1, w, v2) \<in> edges (rem_unPath ps G))
((v2, w, v1) \<in> E) = ((v1, w, v2) \<in> E)
is_trail ?v ((?v1.0, ?w, ?v2.0) # ?ps) ?v' \<Longrightarrow> ((?v1.0, ?w, ?v2.0) \<in> edges (rem_unPath ?ps G)) = ((?v1.0, ?w, ?v2.0) \<in> E)

goal (1 subgoal):
 1. ((v2, w, v1) \<in> edges (rem_unPath ps G)) = ((v2, w, v1) \<in> E)
[PROOF STEP]
by (metis assms)
[PROOF STATE]
proof (state)
this:
((v2, w, v1) \<in> edges (rem_unPath ps G)) = ((v2, w, v1) \<in> E)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in valid_unMultigraph) del_UnEdge_even:
  assumes "(v,w,v') \<in> E" "finite E"
  shows "v\<in>odd_nodes_set(del_unEdge v w v' G) \<longleftrightarrow> even (degree v G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v \<in> odd_nodes_set (del_unEdge v w v' G)) = even (degree v G)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (v \<in> odd_nodes_set (del_unEdge v w v' G)) = even (degree v G)
[PROOF STEP]
have "degree v (del_unEdge v w v' G) + 1=degree v G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree v (del_unEdge v w v' G) + 1 = degree v G
[PROOF STEP]
using del_edge_undirected_degree_plus corres
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite (edges ?g); (?v, ?e, ?v') \<in> edges ?g; (?v', ?e, ?v) \<in> edges ?g\<rbrakk> \<Longrightarrow> degree ?v (del_unEdge ?v ?e ?v' ?g) + 1 = degree ?v ?g
((?v, ?w, ?u') \<in> E) = ((?u', ?w, ?v) \<in> E)

goal (1 subgoal):
 1. degree v (del_unEdge v w v' G) + 1 = degree v G
[PROOF STEP]
by (metis assms)
[PROOF STATE]
proof (state)
this:
degree v (del_unEdge v w v' G) + 1 = degree v G

goal (1 subgoal):
 1. (v \<in> odd_nodes_set (del_unEdge v w v' G)) = even (degree v G)
[PROOF STEP]
from this [symmetric]
[PROOF STATE]
proof (chain)
picking this:
degree v G = degree v (del_unEdge v w v' G) + 1
[PROOF STEP]
have "odd (degree v (del_unEdge v w v' G)) = even (degree v G)"
[PROOF STATE]
proof (prove)
using this:
degree v G = degree v (del_unEdge v w v' G) + 1

goal (1 subgoal):
 1. odd (degree v (del_unEdge v w v' G)) = even (degree v G)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
odd (degree v (del_unEdge v w v' G)) = even (degree v G)

goal (1 subgoal):
 1. (v \<in> odd_nodes_set (del_unEdge v w v' G)) = even (degree v G)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
odd (degree v (del_unEdge v w v' G)) = even (degree v G)

goal (1 subgoal):
 1. (v \<in> odd_nodes_set (del_unEdge v w v' G)) = even (degree v G)
[PROOF STEP]
have "v\<in>nodes (del_unEdge v w v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> nodes (del_unEdge v w v' G)
[PROOF STEP]
by (metis E_validD(1) assms(1) del_UnEdge_node)
[PROOF STATE]
proof (state)
this:
v \<in> nodes (del_unEdge v w v' G)

goal (1 subgoal):
 1. (v \<in> odd_nodes_set (del_unEdge v w v' G)) = even (degree v G)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
odd (degree v (del_unEdge v w v' G)) = even (degree v G)
v \<in> nodes (del_unEdge v w v' G)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
odd (degree v (del_unEdge v w v' G)) = even (degree v G)
v \<in> nodes (del_unEdge v w v' G)

goal (1 subgoal):
 1. (v \<in> odd_nodes_set (del_unEdge v w v' G)) = even (degree v G)
[PROOF STEP]
unfolding odd_nodes_set_def
[PROOF STATE]
proof (prove)
using this:
odd (degree v (del_unEdge v w v' G)) = even (degree v G)
v \<in> nodes (del_unEdge v w v' G)

goal (1 subgoal):
 1. (v \<in> {va \<in> nodes (del_unEdge v w v' G). odd (degree va (del_unEdge v w v' G))}) = even (degree v G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(v \<in> odd_nodes_set (del_unEdge v w v' G)) = even (degree v G)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in valid_unMultigraph) del_UnEdge_even':
  assumes "(v,w,v') \<in> E" "finite E"
  shows "v'\<in>odd_nodes_set(del_unEdge v w v' G) \<longleftrightarrow> even (degree v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v' \<in> odd_nodes_set (del_unEdge v w v' G)) = even (degree v' G)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (v' \<in> odd_nodes_set (del_unEdge v w v' G)) = even (degree v' G)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v' \<in> odd_nodes_set (del_unEdge v w v' G)) = even (degree v' G)
[PROOF STEP]
by (metis (full_types) assms corres del_UnEdge_even delete_edge_sym)
[PROOF STATE]
proof (state)
this:
(v' \<in> odd_nodes_set (del_unEdge v w v' G)) = even (degree v' G)

goal:
No subgoals!
[PROOF STEP]
qed