[STATEMENT]
lemma (in valid_unMultigraph) "connected \<Longrightarrow> \<forall>v\<in>V. \<forall>v'\<in>V. v\<noteq>v'\<longrightarrow>(\<exists>ps. is_trail v ps v')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.connected \<Longrightarrow> \<forall>v\<in>V. \<forall>v'\<in>V. v \<noteq> v' \<longrightarrow> (\<exists>ps. is_trail v ps v')
[PROOF STEP]
proof (rule,rule,rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v v'. \<lbrakk>local.connected; v \<in> V; v' \<in> V; v \<noteq> v'\<rbrakk> \<Longrightarrow> \<exists>ps. is_trail v ps v'
[PROOF STEP]
fix v v'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v v'. \<lbrakk>local.connected; v \<in> V; v' \<in> V; v \<noteq> v'\<rbrakk> \<Longrightarrow> \<exists>ps. is_trail v ps v'
[PROOF STEP]
assume "v\<in>V" "v'\<in>V" "v\<noteq>v'"
[PROOF STATE]
proof (state)
this:
v \<in> V
v' \<in> V
v \<noteq> v'

goal (1 subgoal):
 1. \<And>v v'. \<lbrakk>local.connected; v \<in> V; v' \<in> V; v \<noteq> v'\<rbrakk> \<Longrightarrow> \<exists>ps. is_trail v ps v'
[PROOF STEP]
assume connected
[PROOF STATE]
proof (state)
this:
local.connected

goal (1 subgoal):
 1. \<And>v v'. \<lbrakk>local.connected; v \<in> V; v' \<in> V; v \<noteq> v'\<rbrakk> \<Longrightarrow> \<exists>ps. is_trail v ps v'
[PROOF STEP]
obtain ps where "is_path v ps v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ps. is_path v ps v' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis \<open>connected\<close> \<open>v \<in> V\<close> \<open>v' \<in> V\<close> \<open>v\<noteq>v'\<close>  connected_def)
[PROOF STATE]
proof (state)
this:
is_path v ps v'

goal (1 subgoal):
 1. \<And>v v'. \<lbrakk>local.connected; v \<in> V; v' \<in> V; v \<noteq> v'\<rbrakk> \<Longrightarrow> \<exists>ps. is_trail v ps v'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_path v ps v'
[PROOF STEP]
obtain ps' where "is_trail v ps' v'"
[PROOF STATE]
proof (prove)
using this:
is_path v ps v'

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

goal (2 subgoals):
 1. \<And>v. \<lbrakk>\<And>ps'. is_trail v ps' v' \<Longrightarrow> thesis; is_path v [] v'\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>\<And>ps'. is_trail v ps' v' \<Longrightarrow> thesis; is_path v ps v'\<rbrakk> \<Longrightarrow> thesis; \<And>ps'. is_trail v ps' v' \<Longrightarrow> thesis; is_path v (a # ps) v'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
is_trail v ?ps' v' \<Longrightarrow> thesis
is_path v [] v'

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (metis is_trail.simps(1) is_path.simps(1))
[PROOF STATE]
proof (state)
this:
thesis

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

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>\<And>ps'. is_trail v ps' v' \<Longrightarrow> thesis; is_path v ps v'\<rbrakk> \<Longrightarrow> thesis; \<And>ps'. is_trail v ps' v' \<Longrightarrow> thesis; is_path v (a # ps) v'\<rbrakk> \<Longrightarrow> thesis
[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. \<lbrakk>\<And>ps'. is_trail v ps' v' \<Longrightarrow> thesis; is_path v ps v'\<rbrakk> \<Longrightarrow> thesis; \<And>ps'. is_trail v ps' v' \<Longrightarrow> thesis; is_path v (a # ps) v'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have "is_path x3 xs v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path x3 xs v'
[PROOF STEP]
by (metis Cons.prems(2) is_path.simps(2) x)
[PROOF STATE]
proof (state)
this:
is_path x3 xs v'

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

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>\<And>ps'. is_trail v ps' v' \<Longrightarrow> thesis; is_path v ps v'\<rbrakk> \<Longrightarrow> thesis; \<And>ps'. is_trail v ps' v' \<Longrightarrow> thesis; is_path v (a # ps) v'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have "\<And>ps'. is_trail x3 ps' v' \<Longrightarrow> thesis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ps'. is_trail x3 ps' v' \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ps'. is_trail x3 ps' v' \<Longrightarrow> thesis
[PROOF STEP]
fix ps'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ps'. is_trail x3 ps' v' \<Longrightarrow> thesis
[PROOF STEP]
assume "is_trail x3 ps' v'"
[PROOF STATE]
proof (state)
this:
is_trail x3 ps' v'

goal (1 subgoal):
 1. \<And>ps'. is_trail x3 ps' v' \<Longrightarrow> thesis
[PROOF STEP]
hence "(x1,x2,x3)\<notin>set ps' \<and> (x3,x2,x1)\<notin>set ps' \<Longrightarrow>is_trail v (x#ps') v'"
[PROOF STATE]
proof (prove)
using this:
is_trail x3 ps' v'

goal (1 subgoal):
 1. (x1, x2, x3) \<notin> set ps' \<and> (x3, x2, x1) \<notin> set ps' \<Longrightarrow> is_trail v (x # ps') v'
[PROOF STEP]
by (metis Cons.prems(2) is_trail.simps(2) is_path.simps(2) x)
[PROOF STATE]
proof (state)
this:
(x1, x2, x3) \<notin> set ps' \<and> (x3, x2, x1) \<notin> set ps' \<Longrightarrow> is_trail v (x # ps') v'

goal (1 subgoal):
 1. \<And>ps'. is_trail x3 ps' v' \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(x1, x2, x3) \<notin> set ps' \<and> (x3, x2, x1) \<notin> set ps' \<Longrightarrow> is_trail v (x # ps') v'

goal (1 subgoal):
 1. \<And>ps'. is_trail x3 ps' v' \<Longrightarrow> thesis
[PROOF STEP]
have "(x1,x2,x3)\<in>set ps' \<Longrightarrow> \<exists>ps1. is_trail v ps1 v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x1, x2, x3) \<in> set ps' \<Longrightarrow> \<exists>ps1. is_trail v ps1 v'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x1, x2, x3) \<in> set ps' \<Longrightarrow> \<exists>ps1. is_trail v ps1 v'
[PROOF STEP]
assume "(x1,x2,x3)\<in>set ps'"
[PROOF STATE]
proof (state)
this:
(x1, x2, x3) \<in> set ps'

goal (1 subgoal):
 1. (x1, x2, x3) \<in> set ps' \<Longrightarrow> \<exists>ps1. is_trail v ps1 v'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x1, x2, x3) \<in> set ps'
[PROOF STEP]
obtain ps1 ps2 where "ps'=ps1@(x1,x2,x3)#ps2"
[PROOF STATE]
proof (prove)
using this:
(x1, x2, x3) \<in> set ps'

goal (1 subgoal):
 1. (\<And>ps1 ps2. ps' = ps1 @ (x1, x2, x3) # ps2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis split_list)
[PROOF STATE]
proof (state)
this:
ps' = ps1 @ (x1, x2, x3) # ps2

goal (1 subgoal):
 1. (x1, x2, x3) \<in> set ps' \<Longrightarrow> \<exists>ps1. is_trail v ps1 v'
[PROOF STEP]
hence "is_trail v (x#ps2) v'"
[PROOF STATE]
proof (prove)
using this:
ps' = ps1 @ (x1, x2, x3) # ps2

goal (1 subgoal):
 1. is_trail v (x # ps2) v'
[PROOF STEP]
using \<open>is_trail x3 ps' v'\<close> x
[PROOF STATE]
proof (prove)
using this:
ps' = ps1 @ (x1, x2, x3) # ps2
is_trail x3 ps' v'
x = (x1, x2, x3)

goal (1 subgoal):
 1. is_trail v (x # ps2) v'
[PROOF STEP]
by (metis Cons.prems(2) is_trail.simps(2)
                    is_trail_split is_path.simps(2))
[PROOF STATE]
proof (state)
this:
is_trail v (x # ps2) v'

goal (1 subgoal):
 1. (x1, x2, x3) \<in> set ps' \<Longrightarrow> \<exists>ps1. is_trail v ps1 v'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
is_trail v (x # ps2) v'

goal (1 subgoal):
 1. \<exists>ps1. is_trail v ps1 v'
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
\<exists>ps1. is_trail v ps1 v'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x1, x2, x3) \<in> set ps' \<Longrightarrow> \<exists>ps1. is_trail v ps1 v'

goal (1 subgoal):
 1. \<And>ps'. is_trail x3 ps' v' \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(x1, x2, x3) \<in> set ps' \<Longrightarrow> \<exists>ps1. is_trail v ps1 v'

goal (1 subgoal):
 1. \<And>ps'. is_trail x3 ps' v' \<Longrightarrow> thesis
[PROOF STEP]
have "(x3,x2,x1)\<in>set ps' \<Longrightarrow>  \<exists>ps1. is_trail v ps1 v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x3, x2, x1) \<in> set ps' \<Longrightarrow> \<exists>ps1. is_trail v ps1 v'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x3, x2, x1) \<in> set ps' \<Longrightarrow> \<exists>ps1. is_trail v ps1 v'
[PROOF STEP]
assume "(x3,x2,x1)\<in>set ps'"
[PROOF STATE]
proof (state)
this:
(x3, x2, x1) \<in> set ps'

goal (1 subgoal):
 1. (x3, x2, x1) \<in> set ps' \<Longrightarrow> \<exists>ps1. is_trail v ps1 v'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x3, x2, x1) \<in> set ps'
[PROOF STEP]
obtain ps1 ps2 where "ps'=ps1@(x3,x2,x1)#ps2"
[PROOF STATE]
proof (prove)
using this:
(x3, x2, x1) \<in> set ps'

goal (1 subgoal):
 1. (\<And>ps1 ps2. ps' = ps1 @ (x3, x2, x1) # ps2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis split_list)
[PROOF STATE]
proof (state)
this:
ps' = ps1 @ (x3, x2, x1) # ps2

goal (1 subgoal):
 1. (x3, x2, x1) \<in> set ps' \<Longrightarrow> \<exists>ps1. is_trail v ps1 v'
[PROOF STEP]
hence "is_trail v ps2 v'"
[PROOF STATE]
proof (prove)
using this:
ps' = ps1 @ (x3, x2, x1) # ps2

goal (1 subgoal):
 1. is_trail v ps2 v'
[PROOF STEP]
using \<open>is_trail x3 ps' v'\<close> x
[PROOF STATE]
proof (prove)
using this:
ps' = ps1 @ (x3, x2, x1) # ps2
is_trail x3 ps' v'
x = (x1, x2, x3)

goal (1 subgoal):
 1. is_trail v ps2 v'
[PROOF STEP]
by (metis Cons.prems(2) is_trail.simps(2)
                    is_trail_split is_path.simps(2))
[PROOF STATE]
proof (state)
this:
is_trail v ps2 v'

goal (1 subgoal):
 1. (x3, x2, x1) \<in> set ps' \<Longrightarrow> \<exists>ps1. is_trail v ps1 v'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
is_trail v ps2 v'

goal (1 subgoal):
 1. \<exists>ps1. is_trail v ps1 v'
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
\<exists>ps1. is_trail v ps1 v'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x3, x2, x1) \<in> set ps' \<Longrightarrow> \<exists>ps1. is_trail v ps1 v'

goal (1 subgoal):
 1. \<And>ps'. is_trail x3 ps' v' \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(x1, x2, x3) \<notin> set ps' \<and> (x3, x2, x1) \<notin> set ps' \<Longrightarrow> is_trail v (x # ps') v'
(x1, x2, x3) \<in> set ps' \<Longrightarrow> \<exists>ps1. is_trail v ps1 v'
(x3, x2, x1) \<in> set ps' \<Longrightarrow> \<exists>ps1. is_trail v ps1 v'
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
(x1, x2, x3) \<notin> set ps' \<and> (x3, x2, x1) \<notin> set ps' \<Longrightarrow> is_trail v (x # ps') v'
(x1, x2, x3) \<in> set ps' \<Longrightarrow> \<exists>ps1. is_trail v ps1 v'
(x3, x2, x1) \<in> set ps' \<Longrightarrow> \<exists>ps1. is_trail v ps1 v'

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
(x1, x2, x3) \<notin> set ps' \<and> (x3, x2, x1) \<notin> set ps' \<Longrightarrow> is_trail v (x # ps') v'
(x1, x2, x3) \<in> set ps' \<Longrightarrow> \<exists>ps1. is_trail v ps1 v'
(x3, x2, x1) \<in> set ps' \<Longrightarrow> \<exists>ps1. is_trail v ps1 v'
\<lbrakk>\<And>ps'. is_trail ?v ps' v' \<Longrightarrow> thesis; is_path ?v xs v'\<rbrakk> \<Longrightarrow> thesis
is_trail v ?ps' v' \<Longrightarrow> thesis
is_path v (x # xs) v'

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_trail x3 ?ps' v' \<Longrightarrow> thesis

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. \<lbrakk>\<And>ps'. is_trail v ps' v' \<Longrightarrow> thesis; is_path v ps v'\<rbrakk> \<Longrightarrow> thesis; \<And>ps'. is_trail v ps' v' \<Longrightarrow> thesis; is_path v (a # ps) v'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_path x3 xs v'
is_trail x3 ?ps' v' \<Longrightarrow> thesis
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
is_path x3 xs v'
is_trail x3 ?ps' v' \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
is_path x3 xs v'
is_trail x3 ?ps' v' \<Longrightarrow> thesis
\<lbrakk>\<And>ps'. is_trail ?v ps' v' \<Longrightarrow> thesis; is_path ?v xs v'\<rbrakk> \<Longrightarrow> thesis
is_trail v ?ps' v' \<Longrightarrow> thesis
is_path v (x # xs) v'

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_trail v ps' v'

goal (1 subgoal):
 1. \<And>v v'. \<lbrakk>local.connected; v \<in> V; v' \<in> V; v \<noteq> v'\<rbrakk> \<Longrightarrow> \<exists>ps. is_trail v ps v'
[PROOF STEP]
thus "\<exists>ps. is_trail v ps v'"
[PROOF STATE]
proof (prove)
using this:
is_trail v ps' v'

goal (1 subgoal):
 1. \<exists>ps. is_trail v ps v'
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
\<exists>ps. is_trail v ps v'

goal:
No subgoals!
[PROOF STEP]
qed


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


[STATEMENT]
lemma (in valid_unMultigraph) path_in_edges:"is_trail v ps v' \<Longrightarrow> set ps \<subseteq> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_trail v ps v' \<Longrightarrow> set ps \<subseteq> E
[PROOF STEP]
proof (induct ps arbitrary:v)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v. is_trail v [] v' \<Longrightarrow> set [] \<subseteq> E
 2. \<And>a ps v. \<lbrakk>\<And>v. is_trail v ps v' \<Longrightarrow> set ps \<subseteq> E; is_trail v (a # ps) v'\<rbrakk> \<Longrightarrow> set (a # ps) \<subseteq> E
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
is_trail v [] v'

goal (2 subgoals):
 1. \<And>v. is_trail v [] v' \<Longrightarrow> set [] \<subseteq> E
 2. \<And>a ps v. \<lbrakk>\<And>v. is_trail v ps v' \<Longrightarrow> set ps \<subseteq> E; is_trail v (a # ps) v'\<rbrakk> \<Longrightarrow> set (a # ps) \<subseteq> E
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set [] \<subseteq> E
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set [] \<subseteq> E

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

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. is_trail v ps v' \<Longrightarrow> set ps \<subseteq> E; is_trail v (a # ps) v'\<rbrakk> \<Longrightarrow> set (a # ps) \<subseteq> E
[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. is_trail v ps v' \<Longrightarrow> set ps \<subseteq> E; is_trail v (a # ps) v'\<rbrakk> \<Longrightarrow> set (a # ps) \<subseteq> E
[PROOF STEP]
hence "is_trail x3 xs v'"
[PROOF STATE]
proof (prove)
using this:
x = (x1, x2, x3)

goal (1 subgoal):
 1. is_trail x3 xs v'
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
x = (x1, x2, x3)
is_trail ?v xs v' \<Longrightarrow> set xs \<subseteq> E
is_trail v (x # xs) v'

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

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

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

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

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

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. is_trail v ps v' \<Longrightarrow> set ps \<subseteq> E; is_trail v (a # ps) v'\<rbrakk> \<Longrightarrow> set (a # ps) \<subseteq> E
[PROOF STEP]
have "x\<in>E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> E
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
is_trail ?v xs v' \<Longrightarrow> set xs \<subseteq> E
is_trail v (x # xs) v'

goal (1 subgoal):
 1. x \<in> E
[PROOF STEP]
by (metis is_trail_intro is_path.simps(2) x)
[PROOF STATE]
proof (state)
this:
x \<in> E

goal (1 subgoal):
 1. \<And>a ps v. \<lbrakk>\<And>v. is_trail v ps v' \<Longrightarrow> set ps \<subseteq> E; is_trail v (a # ps) v'\<rbrakk> \<Longrightarrow> set (a # ps) \<subseteq> E
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set xs \<subseteq> E
x \<in> E
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set xs \<subseteq> E
x \<in> E

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in valid_unMultigraph) trail_bound:
    assumes "finite E" " is_trail v ps v'"
    shows "length ps \<le>card E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length ps \<le> card E
[PROOF STEP]
by (metis (opaque_lifting, no_types) assms(1) assms(2) card_mono no_rep_length path_in_edges)


[STATEMENT]
lemma (in valid_unMultigraph) longest_path:
  assumes "finite E" "n \<in> V"
  shows "\<exists>v. \<exists>max_path. is_trail v max_path n \<and>
        (\<forall>v'. \<forall>e\<in>E. \<not>is_trail v' (e#max_path) n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>v max_path. is_trail v max_path n \<and> (\<forall>v'. \<forall>e\<in>E. \<not> is_trail v' (e # max_path) n)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>v max_path. is_trail v max_path n \<and> (\<forall>v'. \<forall>e\<in>E. \<not> is_trail v' (e # max_path) n) \<Longrightarrow> False
[PROOF STEP]
assume  contro:"\<not> (\<exists>v max_path. is_trail v max_path n
           \<and> (\<forall>v'. \<forall>e\<in>E. \<not>is_trail v' (e#max_path) n))"
[PROOF STATE]
proof (state)
this:
\<nexists>v max_path. is_trail v max_path n \<and> (\<forall>v'. \<forall>e\<in>E. \<not> is_trail v' (e # max_path) n)

goal (1 subgoal):
 1. \<nexists>v max_path. is_trail v max_path n \<and> (\<forall>v'. \<forall>e\<in>E. \<not> is_trail v' (e # max_path) n) \<Longrightarrow> False
[PROOF STEP]
hence  induct:"(\<forall>v max_path.  is_trail v max_path n
           \<longrightarrow> (\<exists>v'. \<exists>e\<in>E. is_trail v' (e#max_path) n))"
[PROOF STATE]
proof (prove)
using this:
\<nexists>v max_path. is_trail v max_path n \<and> (\<forall>v'. \<forall>e\<in>E. \<not> is_trail v' (e # max_path) n)

goal (1 subgoal):
 1. \<forall>v max_path. is_trail v max_path n \<longrightarrow> (\<exists>v'. \<exists>e\<in>E. is_trail v' (e # max_path) n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>v max_path. is_trail v max_path n \<longrightarrow> (\<exists>v'. \<exists>e\<in>E. is_trail v' (e # max_path) n)

goal (1 subgoal):
 1. \<nexists>v max_path. is_trail v max_path n \<and> (\<forall>v'. \<forall>e\<in>E. \<not> is_trail v' (e # max_path) n) \<Longrightarrow> False
[PROOF STEP]
have "is_trail n [] n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_trail n [] n
[PROOF STEP]
using \<open>n \<in> V\<close>
[PROOF STATE]
proof (prove)
using this:
n \<in> V

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

goal (1 subgoal):
 1. \<nexists>v max_path. is_trail v max_path n \<and> (\<forall>v'. \<forall>e\<in>E. \<not> is_trail v' (e # max_path) n) \<Longrightarrow> False
[PROOF STEP]
hence "exist_path_length n 0"
[PROOF STATE]
proof (prove)
using this:
is_trail n [] n

goal (1 subgoal):
 1. exist_path_length n 0
[PROOF STEP]
unfolding exist_path_length_def
[PROOF STATE]
proof (prove)
using this:
is_trail n [] n

goal (1 subgoal):
 1. \<exists>v' ps. is_trail v' ps n \<and> length ps = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
exist_path_length n 0

goal (1 subgoal):
 1. \<nexists>v max_path. is_trail v max_path n \<and> (\<forall>v'. \<forall>e\<in>E. \<not> is_trail v' (e # max_path) n) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
exist_path_length n 0

goal (1 subgoal):
 1. \<nexists>v max_path. is_trail v max_path n \<and> (\<forall>v'. \<forall>e\<in>E. \<not> is_trail v' (e # max_path) n) \<Longrightarrow> False
[PROOF STEP]
have "\<forall>y. exist_path_length n y \<longrightarrow> y \<le> card E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y. exist_path_length n y \<longrightarrow> y \<le> card E
[PROOF STEP]
using trail_bound[OF \<open>finite E\<close>]
[PROOF STATE]
proof (prove)
using this:
is_trail ?v ?ps ?v' \<Longrightarrow> length ?ps \<le> card E

goal (1 subgoal):
 1. \<forall>y. exist_path_length n y \<longrightarrow> y \<le> card E
[PROOF STEP]
unfolding exist_path_length_def
[PROOF STATE]
proof (prove)
using this:
is_trail ?v ?ps ?v' \<Longrightarrow> length ?ps \<le> card E

goal (1 subgoal):
 1. \<forall>y. (\<exists>v' ps. is_trail v' ps n \<and> length ps = y) \<longrightarrow> y \<le> card E
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>y. exist_path_length n y \<longrightarrow> y \<le> card E

goal (1 subgoal):
 1. \<nexists>v max_path. is_trail v max_path n \<and> (\<forall>v'. \<forall>e\<in>E. \<not> is_trail v' (e # max_path) n) \<Longrightarrow> False
[PROOF STEP]
hence bound:"\<forall>y. exist_path_length n y \<longrightarrow> y \<le> card E"
[PROOF STATE]
proof (prove)
using this:
\<forall>y. exist_path_length n y \<longrightarrow> y \<le> card E

goal (1 subgoal):
 1. \<forall>y. exist_path_length n y \<longrightarrow> y \<le> card E
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>y. exist_path_length n y \<longrightarrow> y \<le> card E

goal (1 subgoal):
 1. \<nexists>v max_path. is_trail v max_path n \<and> (\<forall>v'. \<forall>e\<in>E. \<not> is_trail v' (e # max_path) n) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
exist_path_length n 0
\<forall>y. exist_path_length n y \<longrightarrow> y \<le> card E
[PROOF STEP]
have "exist_path_length n (GREATEST x. exist_path_length n x)"
[PROOF STATE]
proof (prove)
using this:
exist_path_length n 0
\<forall>y. exist_path_length n y \<longrightarrow> y \<le> card E

goal (1 subgoal):
 1. exist_path_length n (GREATEST x. exist_path_length n x)
[PROOF STEP]
using GreatestI_nat
[PROOF STATE]
proof (prove)
using this:
exist_path_length n 0
\<forall>y. exist_path_length n y \<longrightarrow> y \<le> card E
\<lbrakk>?P ?k; \<And>y. ?P y \<Longrightarrow> y \<le> ?b\<rbrakk> \<Longrightarrow> ?P (Greatest ?P)

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

goal (1 subgoal):
 1. \<nexists>v max_path. is_trail v max_path n \<and> (\<forall>v'. \<forall>e\<in>E. \<not> is_trail v' (e # max_path) n) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
exist_path_length n (GREATEST x. exist_path_length n x)
[PROOF STEP]
obtain v max_path where
    max_path:"is_trail v max_path n" "length max_path=(GREATEST x. exist_path_length n x)"
[PROOF STATE]
proof (prove)
using this:
exist_path_length n (GREATEST x. exist_path_length n x)

goal (1 subgoal):
 1. (\<And>v max_path. \<lbrakk>is_trail v max_path n; length max_path = (GREATEST x. exist_path_length n x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis exist_path_length_def)
[PROOF STATE]
proof (state)
this:
is_trail v max_path n
length max_path = (GREATEST x. exist_path_length n x)

goal (1 subgoal):
 1. \<nexists>v max_path. is_trail v max_path n \<and> (\<forall>v'. \<forall>e\<in>E. \<not> is_trail v' (e # max_path) n) \<Longrightarrow> False
[PROOF STEP]
hence "\<exists> v' e. is_trail v' (e#max_path) n"
[PROOF STATE]
proof (prove)
using this:
is_trail v max_path n
length max_path = (GREATEST x. exist_path_length n x)

goal (1 subgoal):
 1. \<exists>v' e. is_trail v' (e # max_path) n
[PROOF STEP]
using induct
[PROOF STATE]
proof (prove)
using this:
is_trail v max_path n
length max_path = (GREATEST x. exist_path_length n x)
\<forall>v max_path. is_trail v max_path n \<longrightarrow> (\<exists>v'. \<exists>e\<in>E. is_trail v' (e # max_path) n)

goal (1 subgoal):
 1. \<exists>v' e. is_trail v' (e # max_path) n
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>v' e. is_trail v' (e # max_path) n

goal (1 subgoal):
 1. \<nexists>v max_path. is_trail v max_path n \<and> (\<forall>v'. \<forall>e\<in>E. \<not> is_trail v' (e # max_path) n) \<Longrightarrow> False
[PROOF STEP]
hence "exist_path_length n (length max_path +1)"
[PROOF STATE]
proof (prove)
using this:
\<exists>v' e. is_trail v' (e # max_path) n

goal (1 subgoal):
 1. exist_path_length n (length max_path + 1)
[PROOF STEP]
by (metis One_nat_def exist_path_length_def list.size(4))
[PROOF STATE]
proof (state)
this:
exist_path_length n (length max_path + 1)

goal (1 subgoal):
 1. \<nexists>v max_path. is_trail v max_path n \<and> (\<forall>v'. \<forall>e\<in>E. \<not> is_trail v' (e # max_path) n) \<Longrightarrow> False
[PROOF STEP]
hence "length max_path + 1 \<le> (GREATEST x. exist_path_length n x)"
[PROOF STATE]
proof (prove)
using this:
exist_path_length n (length max_path + 1)

goal (1 subgoal):
 1. length max_path + 1 \<le> (GREATEST x. exist_path_length n x)
[PROOF STEP]
by (metis Greatest_le_nat bound)
[PROOF STATE]
proof (state)
this:
length max_path + 1 \<le> (GREATEST x. exist_path_length n x)

goal (1 subgoal):
 1. \<nexists>v max_path. is_trail v max_path n \<and> (\<forall>v'. \<forall>e\<in>E. \<not> is_trail v' (e # max_path) n) \<Longrightarrow> False
[PROOF STEP]
hence "length max_path + 1 \<le> length max_path"
[PROOF STATE]
proof (prove)
using this:
length max_path + 1 \<le> (GREATEST x. exist_path_length n x)

goal (1 subgoal):
 1. length max_path + 1 \<le> length max_path
[PROOF STEP]
using max_path
[PROOF STATE]
proof (prove)
using this:
length max_path + 1 \<le> (GREATEST x. exist_path_length n x)
is_trail v max_path n
length max_path = (GREATEST x. exist_path_length n x)

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

goal (1 subgoal):
 1. \<nexists>v max_path. is_trail v max_path n \<and> (\<forall>v'. \<forall>e\<in>E. \<not> is_trail v' (e # max_path) n) \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
length max_path + 1 \<le> length max_path

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma odd_card:
  assumes "finite A" "odd(card A)"
  shows "\<exists>x. x\<in>A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. x \<in> A
[PROOF STEP]
by (metis all_not_in_conv assms(2) card.empty even_zero)


[STATEMENT]
lemma (in valid_unMultigraph) extend_distinct_path:
  assumes "finite E"  "is_trail v' ps v"
  assumes parity_assms:"(even (degree v' G)\<and>v'\<noteq>v)\<or>(odd (degree v' G)\<and>v'=v)"
  shows "\<exists>e v1. is_trail v1 (e#ps) v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>e v1. is_trail v1 (e # ps) v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>e v1. is_trail v1 (e # ps) v
[PROOF STEP]
have "(even (degree v' G)\<and>v'\<noteq>v) \<Longrightarrow> odd(degree v' (rem_unPath  ps G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. even (degree v' G) \<and> v' \<noteq> v \<Longrightarrow> odd (degree v' (rem_unPath ps G))
[PROOF STEP]
by (metis assms(1) assms(2) rem_UnPath_parity_v)
[PROOF STATE]
proof (state)
this:
even (degree v' G) \<and> v' \<noteq> v \<Longrightarrow> odd (degree v' (rem_unPath ps G))

goal (1 subgoal):
 1. \<exists>e v1. is_trail v1 (e # ps) v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
even (degree v' G) \<and> v' \<noteq> v \<Longrightarrow> odd (degree v' (rem_unPath ps G))

goal (1 subgoal):
 1. \<exists>e v1. is_trail v1 (e # ps) v
[PROOF STEP]
have "(odd (degree v' G)\<and>v'=v) \<Longrightarrow> odd(degree v' (rem_unPath  ps G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd (degree v' G) \<and> v' = v \<Longrightarrow> odd (degree v' (rem_unPath ps G))
[PROOF STEP]
by (metis assms(1) assms(2) rem_UnPath_parity_v')
[PROOF STATE]
proof (state)
this:
odd (degree v' G) \<and> v' = v \<Longrightarrow> odd (degree v' (rem_unPath ps G))

goal (1 subgoal):
 1. \<exists>e v1. is_trail v1 (e # ps) v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
even (degree v' G) \<and> v' \<noteq> v \<Longrightarrow> odd (degree v' (rem_unPath ps G))
odd (degree v' G) \<and> v' = v \<Longrightarrow> odd (degree v' (rem_unPath ps G))
[PROOF STEP]
have "odd(degree v' (rem_unPath  ps G))"
[PROOF STATE]
proof (prove)
using this:
even (degree v' G) \<and> v' \<noteq> v \<Longrightarrow> odd (degree v' (rem_unPath ps G))
odd (degree v' G) \<and> v' = v \<Longrightarrow> odd (degree v' (rem_unPath ps G))

goal (1 subgoal):
 1. odd (degree v' (rem_unPath ps G))
[PROOF STEP]
using parity_assms
[PROOF STATE]
proof (prove)
using this:
even (degree v' G) \<and> v' \<noteq> v \<Longrightarrow> odd (degree v' (rem_unPath ps G))
odd (degree v' G) \<and> v' = v \<Longrightarrow> odd (degree v' (rem_unPath ps G))
even (degree v' G) \<and> v' \<noteq> v \<or> odd (degree v' G) \<and> v' = v

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

goal (1 subgoal):
 1. \<exists>e v1. is_trail v1 (e # ps) v
[PROOF STEP]
hence "odd (card {e. fst e=v' \<and> e\<in>edges G - (set ps \<union> set (rev_path ps))})"
[PROOF STATE]
proof (prove)
using this:
odd (degree v' (rem_unPath ps G))

goal (1 subgoal):
 1. odd (card {e. fst e = v' \<and> e \<in> E - (set ps \<union> set (rev_path ps))})
[PROOF STEP]
using  rem_unPath_edges
[PROOF STATE]
proof (prove)
using this:
odd (degree v' (rem_unPath ps G))
edges (rem_unPath ?ps ?G) = edges ?G - (set ?ps \<union> set (rev_path ?ps))

goal (1 subgoal):
 1. odd (card {e. fst e = v' \<and> e \<in> E - (set ps \<union> set (rev_path ps))})
[PROOF STEP]
unfolding degree_def
[PROOF STATE]
proof (prove)
using this:
odd (card {e \<in> edges (rem_unPath ps G). fst e = v'})
edges (rem_unPath ?ps ?G) = edges ?G - (set ?ps \<union> set (rev_path ?ps))

goal (1 subgoal):
 1. odd (card {e. fst e = v' \<and> e \<in> E - (set ps \<union> set (rev_path ps))})
[PROOF STEP]
by (metis (lifting, no_types) Collect_cong)
[PROOF STATE]
proof (state)
this:
odd (card {e. fst e = v' \<and> e \<in> E - (set ps \<union> set (rev_path ps))})

goal (1 subgoal):
 1. \<exists>e v1. is_trail v1 (e # ps) v
[PROOF STEP]
hence "{e. fst e=v' \<and> e\<in>E - (set ps \<union> set (rev_path ps))}\<noteq>{}"
[PROOF STATE]
proof (prove)
using this:
odd (card {e. fst e = v' \<and> e \<in> E - (set ps \<union> set (rev_path ps))})

goal (1 subgoal):
 1. {e. fst e = v' \<and> e \<in> E - (set ps \<union> set (rev_path ps))} \<noteq> {}
[PROOF STEP]
by (metis empty_iff finite.emptyI odd_card)
[PROOF STATE]
proof (state)
this:
{e. fst e = v' \<and> e \<in> E - (set ps \<union> set (rev_path ps))} \<noteq> {}

goal (1 subgoal):
 1. \<exists>e v1. is_trail v1 (e # ps) v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{e. fst e = v' \<and> e \<in> E - (set ps \<union> set (rev_path ps))} \<noteq> {}
[PROOF STEP]
obtain v0 w where v0w:  "(v',w,v0)\<in>E" "(v',w,v0)\<notin>set ps \<union> set (rev_path ps)"
[PROOF STATE]
proof (prove)
using this:
{e. fst e = v' \<and> e \<in> E - (set ps \<union> set (rev_path ps))} \<noteq> {}

goal (1 subgoal):
 1. (\<And>w v0. \<lbrakk>(v', w, v0) \<in> E; (v', w, v0) \<notin> set ps \<union> set (rev_path ps)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(v', w, v0) \<in> E
(v', w, v0) \<notin> set ps \<union> set (rev_path ps)

goal (1 subgoal):
 1. \<exists>e v1. is_trail v1 (e # ps) v
[PROOF STEP]
hence "is_trail v0 ((v0,w,v')#ps) v"
[PROOF STATE]
proof (prove)
using this:
(v', w, v0) \<in> E
(v', w, v0) \<notin> set ps \<union> set (rev_path ps)

goal (1 subgoal):
 1. is_trail v0 ((v0, w, v') # ps) v
[PROOF STEP]
by (metis (opaque_lifting, mono_tags) Un_iff assms(2) corres in_set_rev_path is_trail.simps(2))
[PROOF STATE]
proof (state)
this:
is_trail v0 ((v0, w, v') # ps) v

goal (1 subgoal):
 1. \<exists>e v1. is_trail v1 (e # ps) v
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
is_trail v0 ((v0, w, v') # ps) v

goal (1 subgoal):
 1. \<exists>e v1. is_trail v1 (e # ps) v
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>e v1. is_trail v1 (e # ps) v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in valid_unMultigraph) del_unEdge_connectivity:
  assumes "connected" "\<exists>ps. valid_graph.is_path (del_unEdge v e v' G) v ps v'"
  shows "valid_unMultigraph.connected (del_unEdge v e v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_unMultigraph.connected (del_unEdge v e v' G)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. valid_unMultigraph.connected (del_unEdge v e v' G)
[PROOF STEP]
have valid_unMulti:"valid_unMultigraph (del_unEdge v e v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_unMultigraph (del_unEdge v e v' G)
[PROOF STEP]
using valid_unMultigraph_axioms
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph G

goal (1 subgoal):
 1. valid_unMultigraph (del_unEdge v e v' G)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
valid_unMultigraph (del_unEdge v e v' G)

goal (1 subgoal):
 1. valid_unMultigraph.connected (del_unEdge v e v' G)
[PROOF STEP]
have valid_graph: "valid_graph (del_unEdge v e v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_graph (del_unEdge v e v' G)
[PROOF STEP]
using valid_graph_axioms del_undirected
[PROOF STATE]
proof (prove)
using this:
valid_graph G
del_unEdge ?v ?e ?v' ?g = delete_edge ?v' ?e ?v (delete_edge ?v ?e ?v' ?g)

goal (1 subgoal):
 1. valid_graph (del_unEdge v e v' G)
[PROOF STEP]
by (metis delete_edge_valid)
[PROOF STATE]
proof (state)
this:
valid_graph (del_unEdge v e v' G)

goal (1 subgoal):
 1. valid_unMultigraph.connected (del_unEdge v e v' G)
[PROOF STEP]
obtain ex_path where ex_path:"valid_graph.is_path (del_unEdge v e v' G) v ex_path v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ex_path. valid_graph.is_path (del_unEdge v e v' G) v ex_path v' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis assms(2))
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v e v' G) v ex_path v'

goal (1 subgoal):
 1. valid_unMultigraph.connected (del_unEdge v e v' G)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_unMultigraph.connected (del_unEdge v e v' G)
[PROOF STEP]
unfolding valid_unMultigraph.connected_def[OF valid_unMulti]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>va\<in>nodes (del_unEdge v e v' G). \<forall>v'a\<in>nodes (del_unEdge v e v' G). va \<noteq> v'a \<longrightarrow> (\<exists>ps. valid_graph.is_path (del_unEdge v e v' G) va ps v'a)
[PROOF STEP]
proof (rule,rule,rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>va v'a. \<lbrakk>va \<in> nodes (del_unEdge v e v' G); v'a \<in> nodes (del_unEdge v e v' G); va \<noteq> v'a\<rbrakk> \<Longrightarrow> \<exists>ps. valid_graph.is_path (del_unEdge v e v' G) va ps v'a
[PROOF STEP]
fix n n'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>va v'a. \<lbrakk>va \<in> nodes (del_unEdge v e v' G); v'a \<in> nodes (del_unEdge v e v' G); va \<noteq> v'a\<rbrakk> \<Longrightarrow> \<exists>ps. valid_graph.is_path (del_unEdge v e v' G) va ps v'a
[PROOF STEP]
assume  n : "n \<in>nodes (del_unEdge v e v' G)"
[PROOF STATE]
proof (state)
this:
n \<in> nodes (del_unEdge v e v' G)

goal (1 subgoal):
 1. \<And>va v'a. \<lbrakk>va \<in> nodes (del_unEdge v e v' G); v'a \<in> nodes (del_unEdge v e v' G); va \<noteq> v'a\<rbrakk> \<Longrightarrow> \<exists>ps. valid_graph.is_path (del_unEdge v e v' G) va ps v'a
[PROOF STEP]
assume  n': "n'\<in>nodes (del_unEdge v e v' G)"
[PROOF STATE]
proof (state)
this:
n' \<in> nodes (del_unEdge v e v' G)

goal (1 subgoal):
 1. \<And>va v'a. \<lbrakk>va \<in> nodes (del_unEdge v e v' G); v'a \<in> nodes (del_unEdge v e v' G); va \<noteq> v'a\<rbrakk> \<Longrightarrow> \<exists>ps. valid_graph.is_path (del_unEdge v e v' G) va ps v'a
[PROOF STEP]
assume "n\<noteq>n'"
[PROOF STATE]
proof (state)
this:
n \<noteq> n'

goal (1 subgoal):
 1. \<And>va v'a. \<lbrakk>va \<in> nodes (del_unEdge v e v' G); v'a \<in> nodes (del_unEdge v e v' G); va \<noteq> v'a\<rbrakk> \<Longrightarrow> \<exists>ps. valid_graph.is_path (del_unEdge v e v' G) va ps v'a
[PROOF STEP]
obtain ps where ps:"is_path n ps n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ps. is_path n ps n' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis \<open>n\<noteq>n'\<close> n n' \<open>connected\<close> connected_def del_UnEdge_node)
[PROOF STATE]
proof (state)
this:
is_path n ps n'

goal (1 subgoal):
 1. \<And>va v'a. \<lbrakk>va \<in> nodes (del_unEdge v e v' G); v'a \<in> nodes (del_unEdge v e v' G); va \<noteq> v'a\<rbrakk> \<Longrightarrow> \<exists>ps. valid_graph.is_path (del_unEdge v e v' G) va ps v'a
[PROOF STEP]
hence "valid_graph.is_path (del_unEdge v e v' G)
           n (replace_by_UnPath ps (v,e,v') ex_path) n'"
[PROOF STATE]
proof (prove)
using this:
is_path n ps n'

goal (1 subgoal):
 1. valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath ps (v, e, v') ex_path) n'
[PROOF STEP]
proof (induct ps arbitrary:n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. is_path n [] n' \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath [] (v, e, v') ex_path) n'
 2. \<And>a ps n. \<lbrakk>\<And>n. is_path n ps n' \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath ps (v, e, v') ex_path) n'; is_path n (a # ps) n'\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (a # ps) (v, e, v') ex_path) n'
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
is_path n [] n'

goal (2 subgoals):
 1. \<And>n. is_path n [] n' \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath [] (v, e, v') ex_path) n'
 2. \<And>a ps n. \<lbrakk>\<And>n. is_path n ps n' \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath ps (v, e, v') ex_path) n'; is_path n (a # ps) n'\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (a # ps) (v, e, v') ex_path) n'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
is_path n [] n'

goal (1 subgoal):
 1. valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath [] (v, e, v') ex_path) n'
[PROOF STEP]
by (metis is_path.simps(1) n' replace_by_UnPath.simps(1) valid_graph
          valid_graph.is_path_simps(1))
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath [] (v, e, v') ex_path) n'

goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. is_path n ps n' \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath ps (v, e, v') ex_path) n'; is_path n (a # ps) n'\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (a # ps) (v, e, v') ex_path) n'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. is_path n ps n' \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath ps (v, e, v') ex_path) n'; is_path n (a # ps) n'\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (a # ps) (v, e, v') ex_path) n'
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
is_path ?n xs n' \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) ?n (replace_by_UnPath xs (v, e, v') ex_path) n'
is_path n (x # xs) n'

goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. is_path n ps n' \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath ps (v, e, v') ex_path) n'; is_path n (a # ps) n'\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (a # ps) (v, e, v') ex_path) n'
[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 n. \<lbrakk>\<And>n. is_path n ps n' \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath ps (v, e, v') ex_path) n'; is_path n (a # ps) n'\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (a # ps) (v, e, v') ex_path) n'
[PROOF STEP]
have "x=(v,e,v') \<Longrightarrow> ?case"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = (v, e, v') \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = (v, e, v') \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n'
[PROOF STEP]
assume "x=(v,e,v')"
[PROOF STATE]
proof (state)
this:
x = (v, e, v')

goal (1 subgoal):
 1. x = (v, e, v') \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n'
[PROOF STEP]
hence "valid_graph.is_path (del_unEdge v e v' G)
                n (replace_by_UnPath (x#xs) (v,e,v') ex_path) n'
                = valid_graph.is_path (del_unEdge v e v' G)
                n (ex_path@(replace_by_UnPath xs (v,e,v') ex_path)) n'"
[PROOF STATE]
proof (prove)
using this:
x = (v, e, v')

goal (1 subgoal):
 1. valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n' = valid_graph.is_path (del_unEdge v e v' G) n (ex_path @ replace_by_UnPath xs (v, e, v') ex_path) n'
[PROOF STEP]
by (metis replace_by_UnPath.simps(2))
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n' = valid_graph.is_path (del_unEdge v e v' G) n (ex_path @ replace_by_UnPath xs (v, e, v') ex_path) n'

goal (1 subgoal):
 1. x = (v, e, v') \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n' = valid_graph.is_path (del_unEdge v e v' G) n (ex_path @ replace_by_UnPath xs (v, e, v') ex_path) n'

goal (1 subgoal):
 1. x = (v, e, v') \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n'
[PROOF STEP]
have "...=True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_graph.is_path (del_unEdge v e v' G) n (ex_path @ replace_by_UnPath xs (v, e, v') ex_path) n' = True
[PROOF STEP]
by (metis Cons.hyps Cons.prems \<open>x = (v, e, v')\<close> ex_path is_path.simps(2) valid_graph
                  valid_graph.is_path_split)
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v e v' G) n (ex_path @ replace_by_UnPath xs (v, e, v') ex_path) n' = True

goal (1 subgoal):
 1. x = (v, e, v') \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n'
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n' = True
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n' = True

goal (1 subgoal):
 1. valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x = (v, e, v') \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n'

goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. is_path n ps n' \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath ps (v, e, v') ex_path) n'; is_path n (a # ps) n'\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (a # ps) (v, e, v') ex_path) n'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x = (v, e, v') \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n'

goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. is_path n ps n' \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath ps (v, e, v') ex_path) n'; is_path n (a # ps) n'\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (a # ps) (v, e, v') ex_path) n'
[PROOF STEP]
have "x=(v',e,v) \<Longrightarrow> ?case"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = (v', e, v) \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = (v', e, v) \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n'
[PROOF STEP]
assume "x=(v',e,v)"
[PROOF STATE]
proof (state)
this:
x = (v', e, v)

goal (1 subgoal):
 1. x = (v', e, v) \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n'
[PROOF STEP]
hence "valid_graph.is_path (del_unEdge v e v' G)
                n (replace_by_UnPath (x#xs) (v,e,v') ex_path) n'
                = valid_graph.is_path (del_unEdge v e v' G)
                n ((rev_path ex_path)@(replace_by_UnPath xs (v,e,v') ex_path)) n'"
[PROOF STATE]
proof (prove)
using this:
x = (v', e, v)

goal (1 subgoal):
 1. valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n' = valid_graph.is_path (del_unEdge v e v' G) n (rev_path ex_path @ replace_by_UnPath xs (v, e, v') ex_path) n'
[PROOF STEP]
by (metis Cons.prems is_path.simps(2) no_id replace_by_UnPath.simps(2))
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n' = valid_graph.is_path (del_unEdge v e v' G) n (rev_path ex_path @ replace_by_UnPath xs (v, e, v') ex_path) n'

goal (1 subgoal):
 1. x = (v', e, v) \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n' = valid_graph.is_path (del_unEdge v e v' G) n (rev_path ex_path @ replace_by_UnPath xs (v, e, v') ex_path) n'

goal (1 subgoal):
 1. x = (v', e, v) \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n'
[PROOF STEP]
have "...=True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_graph.is_path (del_unEdge v e v' G) n (rev_path ex_path @ replace_by_UnPath xs (v, e, v') ex_path) n' = True
[PROOF STEP]
by (metis Cons.hyps Cons.prems \<open>x = (v', e, v)\<close> is_path.simps(2) ex_path valid_graph
                  valid_graph.is_path_split valid_unMulti valid_unMultigraph.is_path_rev)
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v e v' G) n (rev_path ex_path @ replace_by_UnPath xs (v, e, v') ex_path) n' = True

goal (1 subgoal):
 1. x = (v', e, v) \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n'
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n' = True
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n' = True

goal (1 subgoal):
 1. valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x = (v', e, v) \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n'

goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. is_path n ps n' \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath ps (v, e, v') ex_path) n'; is_path n (a # ps) n'\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (a # ps) (v, e, v') ex_path) n'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x = (v', e, v) \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n'

goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. is_path n ps n' \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath ps (v, e, v') ex_path) n'; is_path n (a # ps) n'\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (a # ps) (v, e, v') ex_path) n'
[PROOF STEP]
have "x\<noteq>(v,e,v')\<and>x\<noteq>(v',e,v)\<Longrightarrow>?case"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> (v, e, v') \<and> x \<noteq> (v', e, v) \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n'
[PROOF STEP]
by (metis Cons.hyps Cons.prems del_UnEdge_frame is_path.simps(2) replace_by_UnPath.simps(2)
              valid_graph valid_graph.is_path.simps(2) x)
[PROOF STATE]
proof (state)
this:
x \<noteq> (v, e, v') \<and> x \<noteq> (v', e, v) \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n'

goal (1 subgoal):
 1. \<And>a ps n. \<lbrakk>\<And>n. is_path n ps n' \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath ps (v, e, v') ex_path) n'; is_path n (a # ps) n'\<rbrakk> \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (a # ps) (v, e, v') ex_path) n'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x = (v, e, v') \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n'
x = (v', e, v) \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n'
x \<noteq> (v, e, v') \<and> x \<noteq> (v', e, v) \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x = (v, e, v') \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n'
x = (v', e, v) \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n'
x \<noteq> (v, e, v') \<and> x \<noteq> (v', e, v) \<Longrightarrow> valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n'

goal (1 subgoal):
 1. valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath (x # xs) (v, e, v') ex_path) n'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath ps (v, e, v') ex_path) n'

goal (1 subgoal):
 1. \<And>va v'a. \<lbrakk>va \<in> nodes (del_unEdge v e v' G); v'a \<in> nodes (del_unEdge v e v' G); va \<noteq> v'a\<rbrakk> \<Longrightarrow> \<exists>ps. valid_graph.is_path (del_unEdge v e v' G) va ps v'a
[PROOF STEP]
thus "\<exists>ps. valid_graph.is_path (del_unEdge v e v' G) n ps n'"
[PROOF STATE]
proof (prove)
using this:
valid_graph.is_path (del_unEdge v e v' G) n (replace_by_UnPath ps (v, e, v') ex_path) n'

goal (1 subgoal):
 1. \<exists>ps. valid_graph.is_path (del_unEdge v e v' G) n ps n'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>ps. valid_graph.is_path (del_unEdge v e v' G) n ps n'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
valid_unMultigraph.connected (del_unEdge v e v' G)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in valid_unMultigraph) path_between_odds:
  assumes "odd(degree v G)" "odd(degree v' G)" "finite E"  "v\<noteq>v'" "num_of_odd_nodes G=2"
  shows "\<exists>ps. is_trail v ps v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ps. is_trail v ps v'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>ps. is_trail v ps v'
[PROOF STEP]
have "v\<in>V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> V
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<notin> V \<Longrightarrow> False
[PROOF STEP]
assume "v\<notin>V"
[PROOF STATE]
proof (state)
this:
v \<notin> V

goal (1 subgoal):
 1. v \<notin> V \<Longrightarrow> False
[PROOF STEP]
hence "\<forall>e \<in> E. fst e \<noteq> v"
[PROOF STATE]
proof (prove)
using this:
v \<notin> V

goal (1 subgoal):
 1. \<forall>e\<in>E. fst e \<noteq> v
[PROOF STEP]
by (metis E_valid(1) imageI subsetD)
[PROOF STATE]
proof (state)
this:
\<forall>e\<in>E. fst e \<noteq> v

goal (1 subgoal):
 1. v \<notin> V \<Longrightarrow> False
[PROOF STEP]
hence "degree v G=0"
[PROOF STATE]
proof (prove)
using this:
\<forall>e\<in>E. fst e \<noteq> v

goal (1 subgoal):
 1. degree v G = 0
[PROOF STEP]
unfolding degree_def
[PROOF STATE]
proof (prove)
using this:
\<forall>e\<in>E. fst e \<noteq> v

goal (1 subgoal):
 1. card {e \<in> E. fst e = v} = 0
[PROOF STEP]
using \<open>finite E\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>e\<in>E. fst e \<noteq> v
finite E

goal (1 subgoal):
 1. card {e \<in> E. fst e = v} = 0
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
degree v G = 0

goal (1 subgoal):
 1. v \<notin> V \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
degree v G = 0

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>odd(degree v G)\<close>
[PROOF STATE]
proof (prove)
using this:
degree v G = 0
odd (degree v G)

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

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

goal (1 subgoal):
 1. \<exists>ps. is_trail v ps v'
[PROOF STEP]
have "v'\<in>V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v' \<in> V
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v' \<notin> V \<Longrightarrow> False
[PROOF STEP]
assume "v'\<notin>V"
[PROOF STATE]
proof (state)
this:
v' \<notin> V

goal (1 subgoal):
 1. v' \<notin> V \<Longrightarrow> False
[PROOF STEP]
hence "\<forall>e \<in> E. fst e \<noteq> v'"
[PROOF STATE]
proof (prove)
using this:
v' \<notin> V

goal (1 subgoal):
 1. \<forall>e\<in>E. fst e \<noteq> v'
[PROOF STEP]
by (metis E_valid(1) imageI subsetD)
[PROOF STATE]
proof (state)
this:
\<forall>e\<in>E. fst e \<noteq> v'

goal (1 subgoal):
 1. v' \<notin> V \<Longrightarrow> False
[PROOF STEP]
hence "degree v' G=0"
[PROOF STATE]
proof (prove)
using this:
\<forall>e\<in>E. fst e \<noteq> v'

goal (1 subgoal):
 1. degree v' G = 0
[PROOF STEP]
unfolding degree_def
[PROOF STATE]
proof (prove)
using this:
\<forall>e\<in>E. fst e \<noteq> v'

goal (1 subgoal):
 1. card {e \<in> E. fst e = v'} = 0
[PROOF STEP]
using \<open>finite E\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>e\<in>E. fst e \<noteq> v'
finite E

goal (1 subgoal):
 1. card {e \<in> E. fst e = v'} = 0
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
degree v' G = 0

goal (1 subgoal):
 1. v' \<notin> V \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
degree v' G = 0

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>odd(degree v' G)\<close>
[PROOF STATE]
proof (prove)
using this:
degree v' G = 0
odd (degree v' G)

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

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

goal (1 subgoal):
 1. \<exists>ps. is_trail v ps v'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v' \<in> V
[PROOF STEP]
obtain max_path v0 where max_path:
      "is_trail  v0 max_path v'"
      "(\<forall>n. \<forall>w\<in>E. \<not>is_trail n (w#max_path) v')"
[PROOF STATE]
proof (prove)
using this:
v' \<in> V

goal (1 subgoal):
 1. (\<And>v0 max_path. \<lbrakk>is_trail v0 max_path v'; \<forall>n. \<forall>w\<in>E. \<not> is_trail n (w # max_path) v'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using longest_path[of v']
[PROOF STATE]
proof (prove)
using this:
v' \<in> V
\<lbrakk>finite E; v' \<in> V\<rbrakk> \<Longrightarrow> \<exists>v max_path. is_trail v max_path v' \<and> (\<forall>v'a. \<forall>e\<in>E. \<not> is_trail v'a (e # max_path) v')

goal (1 subgoal):
 1. (\<And>v0 max_path. \<lbrakk>is_trail v0 max_path v'; \<forall>n. \<forall>w\<in>E. \<not> is_trail n (w # max_path) v'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis assms(3))
[PROOF STATE]
proof (state)
this:
is_trail v0 max_path v'
\<forall>n. \<forall>w\<in>E. \<not> is_trail n (w # max_path) v'

goal (1 subgoal):
 1. \<exists>ps. is_trail v ps v'
[PROOF STEP]
have "even(degree v0 G)\<Longrightarrow>v0=v' \<Longrightarrow> v0=v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>even (degree v0 G); v0 = v'\<rbrakk> \<Longrightarrow> v0 = v
[PROOF STEP]
by (metis assms(2))
[PROOF STATE]
proof (state)
this:
\<lbrakk>even (degree v0 G); v0 = v'\<rbrakk> \<Longrightarrow> v0 = v

goal (1 subgoal):
 1. \<exists>ps. is_trail v ps v'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>even (degree v0 G); v0 = v'\<rbrakk> \<Longrightarrow> v0 = v

goal (1 subgoal):
 1. \<exists>ps. is_trail v ps v'
[PROOF STEP]
have "even(degree v0 G)\<Longrightarrow>v0\<noteq>v' \<Longrightarrow> v0=v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>even (degree v0 G); v0 \<noteq> v'\<rbrakk> \<Longrightarrow> v0 = v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>even (degree v0 G); v0 \<noteq> v'\<rbrakk> \<Longrightarrow> v0 = v
[PROOF STEP]
assume"even(degree v0 G)" "v0\<noteq>v'"
[PROOF STATE]
proof (state)
this:
even (degree v0 G)
v0 \<noteq> v'

goal (1 subgoal):
 1. \<lbrakk>even (degree v0 G); v0 \<noteq> v'\<rbrakk> \<Longrightarrow> v0 = v
[PROOF STEP]
hence "\<exists>w v1. is_trail
            v1 (w#max_path) v'"
[PROOF STATE]
proof (prove)
using this:
even (degree v0 G)
v0 \<noteq> v'

goal (1 subgoal):
 1. \<exists>w v1. is_trail v1 (w # max_path) v'
[PROOF STEP]
by (metis assms(3) extend_distinct_path max_path(1))
[PROOF STATE]
proof (state)
this:
\<exists>w v1. is_trail v1 (w # max_path) v'

goal (1 subgoal):
 1. \<lbrakk>even (degree v0 G); v0 \<noteq> v'\<rbrakk> \<Longrightarrow> v0 = v
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>w v1. is_trail v1 (w # max_path) v'

goal (1 subgoal):
 1. v0 = v
[PROOF STEP]
by (metis (full_types) is_trail.simps(2) max_path(2) prod.exhaust)
[PROOF STATE]
proof (state)
this:
v0 = v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>even (degree v0 G); v0 \<noteq> v'\<rbrakk> \<Longrightarrow> v0 = v

goal (1 subgoal):
 1. \<exists>ps. is_trail v ps v'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>even (degree v0 G); v0 \<noteq> v'\<rbrakk> \<Longrightarrow> v0 = v

goal (1 subgoal):
 1. \<exists>ps. is_trail v ps v'
[PROOF STEP]
have "odd(degree v0 G)\<Longrightarrow>v0=v'\<Longrightarrow>v0=v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>odd (degree v0 G); v0 = v'\<rbrakk> \<Longrightarrow> v0 = v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>odd (degree v0 G); v0 = v'\<rbrakk> \<Longrightarrow> v0 = v
[PROOF STEP]
assume"odd(degree v0 G)" "v0=v'"
[PROOF STATE]
proof (state)
this:
odd (degree v0 G)
v0 = v'

goal (1 subgoal):
 1. \<lbrakk>odd (degree v0 G); v0 = v'\<rbrakk> \<Longrightarrow> v0 = v
[PROOF STEP]
hence "\<exists>w v1. is_trail v1 (w#max_path) v'"
[PROOF STATE]
proof (prove)
using this:
odd (degree v0 G)
v0 = v'

goal (1 subgoal):
 1. \<exists>w v1. is_trail v1 (w # max_path) v'
[PROOF STEP]
by (metis assms(3) extend_distinct_path max_path(1))
[PROOF STATE]
proof (state)
this:
\<exists>w v1. is_trail v1 (w # max_path) v'

goal (1 subgoal):
 1. \<lbrakk>odd (degree v0 G); v0 = v'\<rbrakk> \<Longrightarrow> v0 = v
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>w v1. is_trail v1 (w # max_path) v'

goal (1 subgoal):
 1. v0 = v
[PROOF STEP]
by (metis (full_types) List.set_simps(2) insert_subset max_path(2) path_in_edges)
[PROOF STATE]
proof (state)
this:
v0 = v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>odd (degree v0 G); v0 = v'\<rbrakk> \<Longrightarrow> v0 = v

goal (1 subgoal):
 1. \<exists>ps. is_trail v ps v'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>odd (degree v0 G); v0 = v'\<rbrakk> \<Longrightarrow> v0 = v

goal (1 subgoal):
 1. \<exists>ps. is_trail v ps v'
[PROOF STEP]
have "odd(degree v0 G)\<Longrightarrow>v0\<noteq>v'\<Longrightarrow>v0=v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>odd (degree v0 G); v0 \<noteq> v'\<rbrakk> \<Longrightarrow> v0 = v
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>odd (degree v0 G); v0 \<noteq> v'; v0 \<noteq> v\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "v0 \<noteq> v" "odd(degree v0 G)" "v0\<noteq>v'"
[PROOF STATE]
proof (state)
this:
v0 \<noteq> v
odd (degree v0 G)
v0 \<noteq> v'

goal (1 subgoal):
 1. \<lbrakk>odd (degree v0 G); v0 \<noteq> v'; v0 \<noteq> v\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v0 \<noteq> v
odd (degree v0 G)
v0 \<noteq> v'

goal (1 subgoal):
 1. \<lbrakk>odd (degree v0 G); v0 \<noteq> v'; v0 \<noteq> v\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "v\<in>odd_nodes_set G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> odd_nodes_set G
[PROOF STEP]
using \<open>v \<in> V\<close> \<open> odd (degree v G)\<close>
[PROOF STATE]
proof (prove)
using this:
v \<in> V
odd (degree v G)

goal (1 subgoal):
 1. v \<in> odd_nodes_set G
[PROOF STEP]
unfolding odd_nodes_set_def
[PROOF STATE]
proof (prove)
using this:
v \<in> V
odd (degree v G)

goal (1 subgoal):
 1. v \<in> {v \<in> V. odd (degree v G)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<in> odd_nodes_set G

goal (1 subgoal):
 1. \<lbrakk>odd (degree v0 G); v0 \<noteq> v'; v0 \<noteq> v\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v \<in> odd_nodes_set G

goal (1 subgoal):
 1. \<lbrakk>odd (degree v0 G); v0 \<noteq> v'; v0 \<noteq> v\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "v'\<in>odd_nodes_set G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v' \<in> odd_nodes_set G
[PROOF STEP]
using \<open>v' \<in> V\<close> \<open>odd (degree v' G)\<close>
[PROOF STATE]
proof (prove)
using this:
v' \<in> V
odd (degree v' G)

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

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

goal (1 subgoal):
 1. \<lbrakk>odd (degree v0 G); v0 \<noteq> v'; v0 \<noteq> v\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
v0 \<noteq> v
odd (degree v0 G)
v0 \<noteq> v'
v \<in> odd_nodes_set G
v' \<in> odd_nodes_set G
[PROOF STEP]
have "{v,v',v0} \<subseteq> odd_nodes_set G"
[PROOF STATE]
proof (prove)
using this:
v0 \<noteq> v
odd (degree v0 G)
v0 \<noteq> v'
v \<in> odd_nodes_set G
v' \<in> odd_nodes_set G

goal (1 subgoal):
 1. {v, v', v0} \<subseteq> odd_nodes_set G
[PROOF STEP]
using   is_path_memb[OF is_trail_intro[OF \<open>is_trail v0 max_path v'\<close>]] max_path(1)
[PROOF STATE]
proof (prove)
using this:
v0 \<noteq> v
odd (degree v0 G)
v0 \<noteq> v'
v \<in> odd_nodes_set G
v' \<in> odd_nodes_set G
v0 \<in> V \<and> v' \<in> V
is_trail v0 max_path v'

goal (1 subgoal):
 1. {v, v', v0} \<subseteq> odd_nodes_set G
[PROOF STEP]
unfolding odd_nodes_set_def
[PROOF STATE]
proof (prove)
using this:
v0 \<noteq> v
odd (degree v0 G)
v0 \<noteq> v'
v \<in> {v \<in> V. odd (degree v G)}
v' \<in> {v \<in> V. odd (degree v G)}
v0 \<in> V \<and> v' \<in> V
is_trail v0 max_path v'

goal (1 subgoal):
 1. {v, v', v0} \<subseteq> {v \<in> V. odd (degree v G)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{v, v', v0} \<subseteq> odd_nodes_set G

goal (1 subgoal):
 1. \<lbrakk>odd (degree v0 G); v0 \<noteq> v'; v0 \<noteq> v\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{v, v', v0} \<subseteq> odd_nodes_set G

goal (1 subgoal):
 1. \<lbrakk>odd (degree v0 G); v0 \<noteq> v'; v0 \<noteq> v\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "card {v,v',v0}=3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {v, v', v0} = 3
[PROOF STEP]
using \<open>v0\<noteq>v\<close> \<open>v\<noteq>v'\<close> \<open>v0\<noteq>v'\<close>
[PROOF STATE]
proof (prove)
using this:
v0 \<noteq> v
v \<noteq> v'
v0 \<noteq> v'

goal (1 subgoal):
 1. card {v, v', v0} = 3
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card {v, v', v0} = 3

goal (1 subgoal):
 1. \<lbrakk>odd (degree v0 G); v0 \<noteq> v'; v0 \<noteq> v\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card {v, v', v0} = 3

goal (1 subgoal):
 1. \<lbrakk>odd (degree v0 G); v0 \<noteq> v'; v0 \<noteq> v\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "finite (odd_nodes_set G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (odd_nodes_set G)
[PROOF STEP]
using assms(5) card_eq_0_iff[of "odd_nodes_set G"]
[PROOF STATE]
proof (prove)
using this:
num_of_odd_nodes G = 2
(card (odd_nodes_set G) = 0) = (odd_nodes_set G = {} \<or> infinite (odd_nodes_set G))

goal (1 subgoal):
 1. finite (odd_nodes_set G)
[PROOF STEP]
unfolding num_of_odd_nodes_def
[PROOF STATE]
proof (prove)
using this:
card (odd_nodes_set G) = 2
(card (odd_nodes_set G) = 0) = (odd_nodes_set G = {} \<or> infinite (odd_nodes_set G))

goal (1 subgoal):
 1. finite (odd_nodes_set G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (odd_nodes_set G)

goal (1 subgoal):
 1. \<lbrakk>odd (degree v0 G); v0 \<noteq> v'; v0 \<noteq> v\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{v, v', v0} \<subseteq> odd_nodes_set G
card {v, v', v0} = 3
finite (odd_nodes_set G)
[PROOF STEP]
have "3\<le>card(odd_nodes_set G)"
[PROOF STATE]
proof (prove)
using this:
{v, v', v0} \<subseteq> odd_nodes_set G
card {v, v', v0} = 3
finite (odd_nodes_set G)

goal (1 subgoal):
 1. 3 \<le> card (odd_nodes_set G)
[PROOF STEP]
by (metis card_mono)
[PROOF STATE]
proof (state)
this:
3 \<le> card (odd_nodes_set G)

goal (1 subgoal):
 1. \<lbrakk>odd (degree v0 G); v0 \<noteq> v'; v0 \<noteq> v\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
3 \<le> card (odd_nodes_set G)

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>num_of_odd_nodes G=2\<close>
[PROOF STATE]
proof (prove)
using this:
3 \<le> card (odd_nodes_set G)
num_of_odd_nodes G = 2

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding num_of_odd_nodes_def
[PROOF STATE]
proof (prove)
using this:
3 \<le> card (odd_nodes_set G)
card (odd_nodes_set G) = 2

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>odd (degree v0 G); v0 \<noteq> v'\<rbrakk> \<Longrightarrow> v0 = v

goal (1 subgoal):
 1. \<exists>ps. is_trail v ps v'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>even (degree v0 G); v0 = v'\<rbrakk> \<Longrightarrow> v0 = v
\<lbrakk>even (degree v0 G); v0 \<noteq> v'\<rbrakk> \<Longrightarrow> v0 = v
\<lbrakk>odd (degree v0 G); v0 = v'\<rbrakk> \<Longrightarrow> v0 = v
\<lbrakk>odd (degree v0 G); v0 \<noteq> v'\<rbrakk> \<Longrightarrow> v0 = v
[PROOF STEP]
have "v0=v"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>even (degree v0 G); v0 = v'\<rbrakk> \<Longrightarrow> v0 = v
\<lbrakk>even (degree v0 G); v0 \<noteq> v'\<rbrakk> \<Longrightarrow> v0 = v
\<lbrakk>odd (degree v0 G); v0 = v'\<rbrakk> \<Longrightarrow> v0 = v
\<lbrakk>odd (degree v0 G); v0 \<noteq> v'\<rbrakk> \<Longrightarrow> v0 = v

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

goal (1 subgoal):
 1. \<exists>ps. is_trail v ps v'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
v0 = v

goal (1 subgoal):
 1. \<exists>ps. is_trail v ps v'
[PROOF STEP]
by (metis max_path(1))
[PROOF STATE]
proof (state)
this:
\<exists>ps. is_trail v ps v'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in valid_unMultigraph) del_unEdge_even_connectivity:
  assumes "finite E" "finite V" "connected" "\<forall>n\<in>V. even(degree n G)" "(v,e,v')\<in>E"
  shows "valid_unMultigraph.connected (del_unEdge v e v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_unMultigraph.connected (del_unEdge v e v' G)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. valid_unMultigraph.connected (del_unEdge v e v' G)
[PROOF STEP]
have valid_unMulti:"valid_unMultigraph (del_unEdge v e v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_unMultigraph (del_unEdge v e v' G)
[PROOF STEP]
using valid_unMultigraph_axioms
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph G

goal (1 subgoal):
 1. valid_unMultigraph (del_unEdge v e v' G)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
valid_unMultigraph (del_unEdge v e v' G)

goal (1 subgoal):
 1. valid_unMultigraph.connected (del_unEdge v e v' G)
[PROOF STEP]
have valid_graph: "valid_graph (del_unEdge v e v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_graph (del_unEdge v e v' G)
[PROOF STEP]
using valid_graph_axioms del_undirected
[PROOF STATE]
proof (prove)
using this:
valid_graph G
del_unEdge ?v ?e ?v' ?g = delete_edge ?v' ?e ?v (delete_edge ?v ?e ?v' ?g)

goal (1 subgoal):
 1. valid_graph (del_unEdge v e v' G)
[PROOF STEP]
by (metis delete_edge_valid)
[PROOF STATE]
proof (state)
this:
valid_graph (del_unEdge v e v' G)

goal (1 subgoal):
 1. valid_unMultigraph.connected (del_unEdge v e v' G)
[PROOF STEP]
have fin_E': "finite(edges (del_unEdge v e v' G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (edges (del_unEdge v e v' G))
[PROOF STEP]
by (metis (opaque_lifting, no_types) assms(1) del_undirected delete_edge_def
        finite_Diff select_convs(2))
[PROOF STATE]
proof (state)
this:
finite (edges (del_unEdge v e v' G))

goal (1 subgoal):
 1. valid_unMultigraph.connected (del_unEdge v e v' G)
[PROOF STEP]
have fin_V': "finite(nodes (del_unEdge v e v' G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (nodes (del_unEdge v e v' G))
[PROOF STEP]
by (metis (mono_tags) assms(2) del_undirected delete_edge_def select_convs(1))
[PROOF STATE]
proof (state)
this:
finite (nodes (del_unEdge v e v' G))

goal (1 subgoal):
 1. valid_unMultigraph.connected (del_unEdge v e v' G)
[PROOF STEP]
have all_even: "\<forall>n\<in>nodes (del_unEdge v e v' G). n\<notin>{v,v'}
                  \<longrightarrow>even(degree n (del_unEdge v e v' G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n\<in>nodes (del_unEdge v e v' G). n \<notin> {v, v'} \<longrightarrow> even (degree n (del_unEdge v e v' G))
[PROOF STEP]
by (metis (full_types) assms(1) assms(4) degree_frame del_UnEdge_node)
[PROOF STATE]
proof (state)
this:
\<forall>n\<in>nodes (del_unEdge v e v' G). n \<notin> {v, v'} \<longrightarrow> even (degree n (del_unEdge v e v' G))

goal (1 subgoal):
 1. valid_unMultigraph.connected (del_unEdge v e v' G)
[PROOF STEP]
have "even (degree v G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. even (degree v G)
[PROOF STEP]
by (metis (full_types) E_validD(1) assms(4) assms(5))
[PROOF STATE]
proof (state)
this:
even (degree v G)

goal (1 subgoal):
 1. valid_unMultigraph.connected (del_unEdge v e v' G)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
even (degree v G)

goal (1 subgoal):
 1. valid_unMultigraph.connected (del_unEdge v e v' G)
[PROOF STEP]
have "even (degree v' G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. even (degree v' G)
[PROOF STEP]
by (metis (full_types) E_validD(2) assms(4) assms(5))
[PROOF STATE]
proof (state)
this:
even (degree v' G)

goal (1 subgoal):
 1. valid_unMultigraph.connected (del_unEdge v e v' G)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
even (degree v' G)

goal (1 subgoal):
 1. valid_unMultigraph.connected (del_unEdge v e v' G)
[PROOF STEP]
have "num_of_odd_nodes G = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_of_odd_nodes G = 0
[PROOF STEP]
using \<open>\<forall>n\<in>V. even(degree n G)\<close> \<open>finite V\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<in>V. even (degree n G)
finite V

goal (1 subgoal):
 1. num_of_odd_nodes G = 0
[PROOF STEP]
unfolding num_of_odd_nodes_def odd_nodes_set_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<in>V. even (degree n G)
finite V

goal (1 subgoal):
 1. card {v \<in> V. odd (degree v G)} = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
num_of_odd_nodes G = 0

goal (1 subgoal):
 1. valid_unMultigraph.connected (del_unEdge v e v' G)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
even (degree v G)
even (degree v' G)
num_of_odd_nodes G = 0
[PROOF STEP]
have "num_of_odd_nodes (del_unEdge v e v' G) = 2"
[PROOF STATE]
proof (prove)
using this:
even (degree v G)
even (degree v' G)
num_of_odd_nodes G = 0

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v e v' G) = 2
[PROOF STEP]
using del_UnEdge_even_even[of G v e v',OF valid_unMultigraph_axioms]
[PROOF STATE]
proof (prove)
using this:
even (degree v G)
even (degree v' G)
num_of_odd_nodes G = 0
\<lbrakk>finite E; finite V; (v, e, v') \<in> E; even (degree v G); even (degree v' G)\<rbrakk> \<Longrightarrow> num_of_odd_nodes (del_unEdge v e v' G) = num_of_odd_nodes G + 2

goal (1 subgoal):
 1. num_of_odd_nodes (del_unEdge v e v' G) = 2
[PROOF STEP]
by (metis assms(1) assms(2) assms(5) monoid_add_class.add.left_neutral)
[PROOF STATE]
proof (state)
this:
num_of_odd_nodes (del_unEdge v e v' G) = 2

goal (1 subgoal):
 1. valid_unMultigraph.connected (del_unEdge v e v' G)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
num_of_odd_nodes (del_unEdge v e v' G) = 2

goal (1 subgoal):
 1. valid_unMultigraph.connected (del_unEdge v e v' G)
[PROOF STEP]
have " odd (degree v (del_unEdge v e v' G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd (degree v (del_unEdge v e v' G))
[PROOF STEP]
using \<open>even (degree v G)\<close> del_UnEdge_even[OF \<open>(v,e,v')\<in>E\<close> \<open>finite E\<close>]
[PROOF STATE]
proof (prove)
using this:
even (degree v G)
(v \<in> odd_nodes_set (del_unEdge v e v' G)) = even (degree v G)

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

goal (1 subgoal):
 1. odd (degree v (del_unEdge v e v' G))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
odd (degree v (del_unEdge v e v' G))

goal (1 subgoal):
 1. valid_unMultigraph.connected (del_unEdge v e v' G)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
odd (degree v (del_unEdge v e v' G))

goal (1 subgoal):
 1. valid_unMultigraph.connected (del_unEdge v e v' G)
[PROOF STEP]
have "odd (degree v' (del_unEdge v e v' G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd (degree v' (del_unEdge v e v' G))
[PROOF STEP]
using \<open>even (degree v' G)\<close> del_UnEdge_even'[OF \<open>(v,e,v')\<in>E\<close> \<open>finite E\<close>]
[PROOF STATE]
proof (prove)
using this:
even (degree v' G)
(v' \<in> odd_nodes_set (del_unEdge v e v' G)) = even (degree v' G)

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

goal (1 subgoal):
 1. odd (degree v' (del_unEdge v e v' G))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
odd (degree v' (del_unEdge v e v' G))

goal (1 subgoal):
 1. valid_unMultigraph.connected (del_unEdge v e v' G)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
odd (degree v' (del_unEdge v e v' G))

goal (1 subgoal):
 1. valid_unMultigraph.connected (del_unEdge v e v' G)
[PROOF STEP]
have "finite (edges (del_unEdge v e v' G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (edges (del_unEdge v e v' G))
[PROOF STEP]
using \<open>finite E\<close>
[PROOF STATE]
proof (prove)
using this:
finite E

goal (1 subgoal):
 1. finite (edges (del_unEdge v e v' G))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (edges (del_unEdge v e v' G))

goal (1 subgoal):
 1. valid_unMultigraph.connected (del_unEdge v e v' G)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite (edges (del_unEdge v e v' G))

goal (1 subgoal):
 1. valid_unMultigraph.connected (del_unEdge v e v' G)
[PROOF STEP]
have "v\<noteq>v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<noteq> v'
[PROOF STEP]
using no_id \<open>(v,e,v')\<in>E\<close>
[PROOF STATE]
proof (prove)
using this:
(?v, ?w, ?v) \<notin> E
(v, e, v') \<in> E

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

goal (1 subgoal):
 1. valid_unMultigraph.connected (del_unEdge v e v' G)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
num_of_odd_nodes (del_unEdge v e v' G) = 2
odd (degree v (del_unEdge v e v' G))
odd (degree v' (del_unEdge v e v' G))
finite (edges (del_unEdge v e v' G))
v \<noteq> v'
[PROOF STEP]
have "\<exists>ps. valid_unMultigraph.is_trail (del_unEdge v e v' G) v ps v'"
[PROOF STATE]
proof (prove)
using this:
num_of_odd_nodes (del_unEdge v e v' G) = 2
odd (degree v (del_unEdge v e v' G))
odd (degree v' (del_unEdge v e v' G))
finite (edges (del_unEdge v e v' G))
v \<noteq> v'

goal (1 subgoal):
 1. \<exists>ps. valid_unMultigraph.is_trail (del_unEdge v e v' G) v ps v'
[PROOF STEP]
using valid_unMultigraph.path_between_odds[OF valid_unMulti,of v v']
[PROOF STATE]
proof (prove)
using this:
num_of_odd_nodes (del_unEdge v e v' G) = 2
odd (degree v (del_unEdge v e v' G))
odd (degree v' (del_unEdge v e v' G))
finite (edges (del_unEdge v e v' G))
v \<noteq> v'
\<lbrakk>odd (degree v (del_unEdge v e v' G)); odd (degree v' (del_unEdge v e v' G)); finite (edges (del_unEdge v e v' G)); v \<noteq> v'; num_of_odd_nodes (del_unEdge v e v' G) = 2\<rbrakk> \<Longrightarrow> \<exists>ps. valid_unMultigraph.is_trail (del_unEdge v e v' G) v ps v'

goal (1 subgoal):
 1. \<exists>ps. valid_unMultigraph.is_trail (del_unEdge v e v' G) v ps v'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>ps. valid_unMultigraph.is_trail (del_unEdge v e v' G) v ps v'

goal (1 subgoal):
 1. valid_unMultigraph.connected (del_unEdge v e v' G)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>ps. valid_unMultigraph.is_trail (del_unEdge v e v' G) v ps v'

goal (1 subgoal):
 1. valid_unMultigraph.connected (del_unEdge v e v' G)
[PROOF STEP]
by (metis (full_types) assms(3) del_unEdge_connectivity valid_unMulti
      valid_unMultigraph.is_trail_intro)
[PROOF STATE]
proof (state)
this:
valid_unMultigraph.connected (del_unEdge v e v' G)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in valid_graph) path_end:"ps\<noteq>[] \<Longrightarrow> is_path v ps v' \<Longrightarrow> v'=snd (snd(last ps))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ps \<noteq> []; is_path v ps v'\<rbrakk> \<Longrightarrow> v' = snd (snd (last ps))
[PROOF STEP]
by (induct ps arbitrary:v,auto)


[STATEMENT]
lemma sub_graph_degree_frame:
  assumes "valid_graph G2" "edges G1 \<union> edges G2 =edges G" "nodes G1 \<inter> nodes G2={}" "n\<in>nodes G1"
  shows "degree n G=degree n G1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree n G = degree n G1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. degree n G = degree n G1
[PROOF STEP]
have "{e \<in> edges G. fst e = n}\<subseteq>{e \<in> edges G1. fst e = n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {e \<in> edges G. fst e = n} \<subseteq> {e \<in> edges G1. fst e = n}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {e \<in> edges G. fst e = n} \<Longrightarrow> x \<in> {e \<in> edges G1. fst e = n}
[PROOF STEP]
fix e
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {e \<in> edges G. fst e = n} \<Longrightarrow> x \<in> {e \<in> edges G1. fst e = n}
[PROOF STEP]
assume  "e \<in> {e \<in> edges G. fst e = n}"
[PROOF STATE]
proof (state)
this:
e \<in> {e \<in> edges G. fst e = n}

goal (1 subgoal):
 1. \<And>x. x \<in> {e \<in> edges G. fst e = n} \<Longrightarrow> x \<in> {e \<in> edges G1. fst e = n}
[PROOF STEP]
hence "e\<in>edges G" "fst e=n"
[PROOF STATE]
proof (prove)
using this:
e \<in> {e \<in> edges G. fst e = n}

goal (1 subgoal):
 1. e \<in> edges G &&& fst e = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
e \<in> edges G
fst e = n

goal (1 subgoal):
 1. \<And>x. x \<in> {e \<in> edges G. fst e = n} \<Longrightarrow> x \<in> {e \<in> edges G1. fst e = n}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
e \<in> edges G
fst e = n

goal (1 subgoal):
 1. \<And>x. x \<in> {e \<in> edges G. fst e = n} \<Longrightarrow> x \<in> {e \<in> edges G1. fst e = n}
[PROOF STEP]
have "n\<notin>nodes G2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<notin> nodes G2
[PROOF STEP]
using \<open>nodes G1 \<inter> nodes G2={}\<close> \<open>n\<in>nodes G1\<close>
[PROOF STATE]
proof (prove)
using this:
nodes G1 \<inter> nodes G2 = {}
n \<in> nodes G1

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

goal (1 subgoal):
 1. \<And>x. x \<in> {e \<in> edges G. fst e = n} \<Longrightarrow> x \<in> {e \<in> edges G1. fst e = n}
[PROOF STEP]
hence "e\<notin>edges G2"
[PROOF STATE]
proof (prove)
using this:
n \<notin> nodes G2

goal (1 subgoal):
 1. e \<notin> edges G2
[PROOF STEP]
using valid_graph.E_validD[OF \<open>valid_graph G2\<close>] \<open>fst e=n\<close>
[PROOF STATE]
proof (prove)
using this:
n \<notin> nodes G2
(?v, ?e, ?v') \<in> edges G2 \<Longrightarrow> ?v \<in> nodes G2
(?v, ?e, ?v') \<in> edges G2 \<Longrightarrow> ?v' \<in> nodes G2
fst e = n

goal (1 subgoal):
 1. e \<notin> edges G2
[PROOF STEP]
by (metis prod.exhaust fst_conv)
[PROOF STATE]
proof (state)
this:
e \<notin> edges G2

goal (1 subgoal):
 1. \<And>x. x \<in> {e \<in> edges G. fst e = n} \<Longrightarrow> x \<in> {e \<in> edges G1. fst e = n}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
e \<in> edges G
fst e = n
e \<notin> edges G2
[PROOF STEP]
have "e\<in>edges G1"
[PROOF STATE]
proof (prove)
using this:
e \<in> edges G
fst e = n
e \<notin> edges G2

goal (1 subgoal):
 1. e \<in> edges G1
[PROOF STEP]
using \<open>edges G1 \<union> edges G2 =edges G\<close>
[PROOF STATE]
proof (prove)
using this:
e \<in> edges G
fst e = n
e \<notin> edges G2
edges G1 \<union> edges G2 = edges G

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

goal (1 subgoal):
 1. \<And>x. x \<in> {e \<in> edges G. fst e = n} \<Longrightarrow> x \<in> {e \<in> edges G1. fst e = n}
[PROOF STEP]
thus "e \<in> {e \<in> edges G1. fst e = n}"
[PROOF STATE]
proof (prove)
using this:
e \<in> edges G1

goal (1 subgoal):
 1. e \<in> {e \<in> edges G1. fst e = n}
[PROOF STEP]
using \<open>fst e=n\<close>
[PROOF STATE]
proof (prove)
using this:
e \<in> edges G1
fst e = n

goal (1 subgoal):
 1. e \<in> {e \<in> edges G1. fst e = n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
e \<in> {e \<in> edges G1. fst e = n}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{e \<in> edges G. fst e = n} \<subseteq> {e \<in> edges G1. fst e = n}

goal (1 subgoal):
 1. degree n G = degree n G1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{e \<in> edges G. fst e = n} \<subseteq> {e \<in> edges G1. fst e = n}

goal (1 subgoal):
 1. degree n G = degree n G1
[PROOF STEP]
have "{e \<in> edges G1. fst e = n}\<subseteq>{e \<in> edges G. fst e = n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {e \<in> edges G1. fst e = n} \<subseteq> {e \<in> edges G. fst e = n}
[PROOF STEP]
by (metis (lifting) Collect_mono Un_iff assms(2))
[PROOF STATE]
proof (state)
this:
{e \<in> edges G1. fst e = n} \<subseteq> {e \<in> edges G. fst e = n}

goal (1 subgoal):
 1. degree n G = degree n G1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{e \<in> edges G. fst e = n} \<subseteq> {e \<in> edges G1. fst e = n}
{e \<in> edges G1. fst e = n} \<subseteq> {e \<in> edges G. fst e = n}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{e \<in> edges G. fst e = n} \<subseteq> {e \<in> edges G1. fst e = n}
{e \<in> edges G1. fst e = n} \<subseteq> {e \<in> edges G. fst e = n}

goal (1 subgoal):
 1. degree n G = degree n G1
[PROOF STEP]
unfolding degree_def
[PROOF STATE]
proof (prove)
using this:
{e \<in> edges G. fst e = n} \<subseteq> {e \<in> edges G1. fst e = n}
{e \<in> edges G1. fst e = n} \<subseteq> {e \<in> edges G. fst e = n}

goal (1 subgoal):
 1. card {e \<in> edges G. fst e = n} = card {e \<in> edges G1. fst e = n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree n G = degree n G1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma odd_nodes_no_edge[simp]: "finite (nodes g) \<Longrightarrow> num_of_odd_nodes (g \<lparr>edges:={} \<rparr>) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (nodes g) \<Longrightarrow> num_of_odd_nodes (g\<lparr>edges := {}\<rparr>) = 0
[PROOF STEP]
unfolding  num_of_odd_nodes_def odd_nodes_set_def degree_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (nodes g) \<Longrightarrow> card {v \<in> nodes (g\<lparr>edges := {}\<rparr>). odd (card {e \<in> edges (g\<lparr>edges := {}\<rparr>). fst e = v})} = 0
[PROOF STEP]
by simp


[STATEMENT]
lemma (in valid_unMultigraph) adjacent_sym: "adjacent v v' \<longleftrightarrow> adjacent v' v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjacent v v' = adjacent v' v
[PROOF STEP]
unfolding adjacent_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>w. (v, w, v') \<in> E) = (\<exists>w. (v', w, v) \<in> E)
[PROOF STEP]
by auto


[STATEMENT]
lemma (in valid_unMultigraph) adjacent_no_loop[simp]: "adjacent v v' \<Longrightarrow> v \<noteq>v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjacent v v' \<Longrightarrow> v \<noteq> v'
[PROOF STEP]
unfolding adjacent_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>w. (v, w, v') \<in> E \<Longrightarrow> v \<noteq> v'
[PROOF STEP]
by auto


[STATEMENT]
lemma (in valid_unMultigraph) adjacent_V[simp]:
    assumes "adjacent v v'"
    shows "v\<in>V" "v'\<in>V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> V &&& v' \<in> V
[PROOF STEP]
using assms E_validD
[PROOF STATE]
proof (prove)
using this:
adjacent v v'
(?v, ?e, ?v') \<in> E \<Longrightarrow> ?v \<in> V
(?v, ?e, ?v') \<in> E \<Longrightarrow> ?v' \<in> V

goal (1 subgoal):
 1. v \<in> V &&& v' \<in> V
[PROOF STEP]
unfolding adjacent_def
[PROOF STATE]
proof (prove)
using this:
\<exists>w. (v, w, v') \<in> E
(?v, ?e, ?v') \<in> E \<Longrightarrow> ?v \<in> V
(?v, ?e, ?v') \<in> E \<Longrightarrow> ?v' \<in> V

goal (1 subgoal):
 1. v \<in> V &&& v' \<in> V
[PROOF STEP]
by auto