[STATEMENT]
theorem distributivity:
 assumes  "matrix_match A1 A2 B1 B2"
 shows "((A1 \<circ> A2)\<otimes>(B1\<circ>B2)) = ((A1 \<otimes> B1)\<circ>(A2 \<otimes> B2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A1 \<circ> A2 \<otimes> B1 \<circ> B2 = (A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A1 \<circ> A2 \<otimes> B1 \<circ> B2 = (A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)
[PROOF STEP]
let ?nr = " ((row_length A1)*(row_length B1))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A1 \<circ> A2 \<otimes> B1 \<circ> B2 = (A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)
[PROOF STEP]
let ?nc = "((length A2)*(length B2))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A1 \<circ> A2 \<otimes> B1 \<circ> B2 = (A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)
[PROOF STEP]
have "mat ?nr ?nc ((A1\<circ>A2)\<otimes>(B1\<circ>B2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length A1 * row_length B1) (length A2 * length B2) (A1 \<circ> A2 \<otimes> B1 \<circ> B2)
[PROOF STEP]
by (metis assms effective_tensor_compose_distribution1)
[PROOF STATE]
proof (state)
this:
mat (row_length A1 * row_length B1) (length A2 * length B2) (A1 \<circ> A2 \<otimes> B1 \<circ> B2)

goal (1 subgoal):
 1. A1 \<circ> A2 \<otimes> B1 \<circ> B2 = (A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mat (row_length A1 * row_length B1) (length A2 * length B2) (A1 \<circ> A2 \<otimes> B1 \<circ> B2)

goal (1 subgoal):
 1. A1 \<circ> A2 \<otimes> B1 \<circ> B2 = (A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)
[PROOF STEP]
have "mat ?nr ?nc ((A1 \<otimes> B1)\<circ>(A2 \<otimes> B2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length A1 * row_length B1) (length A2 * length B2) ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
matrix_match A1 A2 B1 B2

goal (1 subgoal):
 1. mat (row_length A1 * row_length B1) (length A2 * length B2) ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2))
[PROOF STEP]
by (metis effective_tensor_compose_distribution2)
[PROOF STATE]
proof (state)
this:
mat (row_length A1 * row_length B1) (length A2 * length B2) ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2))

goal (1 subgoal):
 1. A1 \<circ> A2 \<otimes> B1 \<circ> B2 = (A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mat (row_length A1 * row_length B1) (length A2 * length B2) ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2))

goal (1 subgoal):
 1. A1 \<circ> A2 \<otimes> B1 \<circ> B2 = (A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)
[PROOF STEP]
have "\<forall>j<?nc.\<forall>i<?nr.
                   (((A1 \<circ> A2)\<otimes>(B1 \<circ>B2))!j!i
                                = ((A1 \<otimes> B1)\<circ>(A2 \<otimes> B2))!j!i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j<length A2 * length B2. \<forall>i<row_length A1 * row_length B1. (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i
[PROOF STEP]
using element_match assms
[PROOF STATE]
proof (prove)
using this:
matrix_match ?A1.0 ?A2.0 ?B1.0 ?B2.0 \<Longrightarrow> \<forall>i<row_length ?A1.0 * row_length ?B1.0. \<forall>j<length ?A2.0 * length ?B2.0. (?A1.0 \<circ> ?A2.0 \<otimes> ?B1.0 \<circ> ?B2.0) ! j ! i = ((?A1.0 \<otimes> ?B1.0) \<circ> (?A2.0 \<otimes> ?B2.0)) ! j ! i
matrix_match A1 A2 B1 B2

goal (1 subgoal):
 1. \<forall>j<length A2 * length B2. \<forall>i<row_length A1 * row_length B1. (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>j<length A2 * length B2. \<forall>i<row_length A1 * row_length B1. (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i

goal (1 subgoal):
 1. A1 \<circ> A2 \<otimes> B1 \<circ> B2 = (A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
mat (row_length A1 * row_length B1) (length A2 * length B2) (A1 \<circ> A2 \<otimes> B1 \<circ> B2)
mat (row_length A1 * row_length B1) (length A2 * length B2) ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2))
\<forall>j<length A2 * length B2. \<forall>i<row_length A1 * row_length B1. (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mat (row_length A1 * row_length B1) (length A2 * length B2) (A1 \<circ> A2 \<otimes> B1 \<circ> B2)
mat (row_length A1 * row_length B1) (length A2 * length B2) ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2))
\<forall>j<length A2 * length B2. \<forall>i<row_length A1 * row_length B1. (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i

goal (1 subgoal):
 1. A1 \<circ> A2 \<otimes> B1 \<circ> B2 = (A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)
[PROOF STEP]
using application
[PROOF STATE]
proof (prove)
using this:
mat (row_length A1 * row_length B1) (length A2 * length B2) (A1 \<circ> A2 \<otimes> B1 \<circ> B2)
mat (row_length A1 * row_length B1) (length A2 * length B2) ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2))
\<forall>j<length A2 * length B2. \<forall>i<row_length A1 * row_length B1. (A1 \<circ> A2 \<otimes> B1 \<circ> B2) ! j ! i = ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i
\<forall>m1 m2. mat ?nr ?nc m1 \<and> mat ?nr ?nc m2 \<and> (\<forall>j<?nc. \<forall>i<?nr. m1 ! j ! i = m2 ! j ! i) \<longrightarrow> m1 = m2

goal (1 subgoal):
 1. A1 \<circ> A2 \<otimes> B1 \<circ> B2 = (A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A1 \<circ> A2 \<otimes> B1 \<circ> B2 = (A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma distinct_tl_rev:
  assumes "hd xs = last xs"
  shows "distinct (tl xs) \<longleftrightarrow> distinct (tl (rev xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (tl xs) = distinct (tl (rev xs))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
hd xs = last xs

goal (1 subgoal):
 1. distinct (tl xs) = distinct (tl (rev xs))
[PROOF STEP]
proof (induct xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. hd [] = last [] \<Longrightarrow> distinct (tl []) = distinct (tl (rev []))
 2. \<And>a xs. \<lbrakk>hd xs = last xs \<Longrightarrow> distinct (tl xs) = distinct (tl (rev xs)); hd (a # xs) = last (a # xs)\<rbrakk> \<Longrightarrow> distinct (tl (a # xs)) = distinct (tl (rev (a # xs)))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
hd [] = last []

goal (2 subgoals):
 1. hd [] = last [] \<Longrightarrow> distinct (tl []) = distinct (tl (rev []))
 2. \<And>a xs. \<lbrakk>hd xs = last xs \<Longrightarrow> distinct (tl xs) = distinct (tl (rev xs)); hd (a # xs) = last (a # xs)\<rbrakk> \<Longrightarrow> distinct (tl (a # xs)) = distinct (tl (rev (a # xs)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hd [] = last []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
hd [] = last []

goal (1 subgoal):
 1. distinct (tl []) = distinct (tl (rev []))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct (tl []) = distinct (tl (rev []))

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>hd xs = last xs \<Longrightarrow> distinct (tl xs) = distinct (tl (rev xs)); hd (a # xs) = last (a # xs)\<rbrakk> \<Longrightarrow> distinct (tl (a # xs)) = distinct (tl (rev (a # xs)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>hd xs = last xs \<Longrightarrow> distinct (tl xs) = distinct (tl (rev xs)); hd (a # xs) = last (a # xs)\<rbrakk> \<Longrightarrow> distinct (tl (a # xs)) = distinct (tl (rev (a # xs)))
[PROOF STEP]
case (Cons a xs)
[PROOF STATE]
proof (state)
this:
hd xs = last xs \<Longrightarrow> distinct (tl xs) = distinct (tl (rev xs))
hd (a # xs) = last (a # xs)

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>hd xs = last xs \<Longrightarrow> distinct (tl xs) = distinct (tl (rev xs)); hd (a # xs) = last (a # xs)\<rbrakk> \<Longrightarrow> distinct (tl (a # xs)) = distinct (tl (rev (a # xs)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hd xs = last xs \<Longrightarrow> distinct (tl xs) = distinct (tl (rev xs))
hd (a # xs) = last (a # xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
hd xs = last xs \<Longrightarrow> distinct (tl xs) = distinct (tl (rev xs))
hd (a # xs) = last (a # xs)

goal (1 subgoal):
 1. distinct (tl (a # xs)) = distinct (tl (rev (a # xs)))
[PROOF STEP]
proof (cases "xs = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>hd xs = last xs \<Longrightarrow> distinct (tl xs) = distinct (tl (rev xs)); hd (a # xs) = last (a # xs); xs = []\<rbrakk> \<Longrightarrow> distinct (tl (a # xs)) = distinct (tl (rev (a # xs)))
 2. \<lbrakk>hd xs = last xs \<Longrightarrow> distinct (tl xs) = distinct (tl (rev xs)); hd (a # xs) = last (a # xs); xs \<noteq> []\<rbrakk> \<Longrightarrow> distinct (tl (a # xs)) = distinct (tl (rev (a # xs)))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
xs = []

goal (2 subgoals):
 1. \<lbrakk>hd xs = last xs \<Longrightarrow> distinct (tl xs) = distinct (tl (rev xs)); hd (a # xs) = last (a # xs); xs = []\<rbrakk> \<Longrightarrow> distinct (tl (a # xs)) = distinct (tl (rev (a # xs)))
 2. \<lbrakk>hd xs = last xs \<Longrightarrow> distinct (tl xs) = distinct (tl (rev xs)); hd (a # xs) = last (a # xs); xs \<noteq> []\<rbrakk> \<Longrightarrow> distinct (tl (a # xs)) = distinct (tl (rev (a # xs)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xs = []

goal (1 subgoal):
 1. distinct (tl (a # xs)) = distinct (tl (rev (a # xs)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct (tl (a # xs)) = distinct (tl (rev (a # xs)))

goal (1 subgoal):
 1. \<lbrakk>hd xs = last xs \<Longrightarrow> distinct (tl xs) = distinct (tl (rev xs)); hd (a # xs) = last (a # xs); xs \<noteq> []\<rbrakk> \<Longrightarrow> distinct (tl (a # xs)) = distinct (tl (rev (a # xs)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>hd xs = last xs \<Longrightarrow> distinct (tl xs) = distinct (tl (rev xs)); hd (a # xs) = last (a # xs); xs \<noteq> []\<rbrakk> \<Longrightarrow> distinct (tl (a # xs)) = distinct (tl (rev (a # xs)))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
xs \<noteq> []

goal (1 subgoal):
 1. \<lbrakk>hd xs = last xs \<Longrightarrow> distinct (tl xs) = distinct (tl (rev xs)); hd (a # xs) = last (a # xs); xs \<noteq> []\<rbrakk> \<Longrightarrow> distinct (tl (a # xs)) = distinct (tl (rev (a # xs)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs \<noteq> []
[PROOF STEP]
have "a = last xs"
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> []

goal (1 subgoal):
 1. a = last xs
[PROOF STEP]
using Cons.prems
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> []
hd (a # xs) = last (a # xs)

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

goal (1 subgoal):
 1. \<lbrakk>hd xs = last xs \<Longrightarrow> distinct (tl xs) = distinct (tl (rev xs)); hd (a # xs) = last (a # xs); xs \<noteq> []\<rbrakk> \<Longrightarrow> distinct (tl (a # xs)) = distinct (tl (rev (a # xs)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = last xs
[PROOF STEP]
obtain xs' where "xs = xs' @ [last xs]"
[PROOF STATE]
proof (prove)
using this:
a = last xs

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

goal (1 subgoal):
 1. \<lbrakk>hd xs = last xs \<Longrightarrow> distinct (tl xs) = distinct (tl (rev xs)); hd (a # xs) = last (a # xs); xs \<noteq> []\<rbrakk> \<Longrightarrow> distinct (tl (a # xs)) = distinct (tl (rev (a # xs)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs = xs' @ [last xs]
[PROOF STEP]
have tleq: "tl (rev xs) = rev (xs')"
[PROOF STATE]
proof (prove)
using this:
xs = xs' @ [last xs]

goal (1 subgoal):
 1. tl (rev xs) = rev xs'
[PROOF STEP]
by (metis butlast_rev butlast_snoc rev_rev_ident)
[PROOF STATE]
proof (state)
this:
tl (rev xs) = rev xs'

goal (1 subgoal):
 1. \<lbrakk>hd xs = last xs \<Longrightarrow> distinct (tl xs) = distinct (tl (rev xs)); hd (a # xs) = last (a # xs); xs \<noteq> []\<rbrakk> \<Longrightarrow> distinct (tl (a # xs)) = distinct (tl (rev (a # xs)))
[PROOF STEP]
have "distinct (tl (a # xs)) \<longleftrightarrow> distinct xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (tl (a # xs)) = distinct xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct (tl (a # xs)) = distinct xs

goal (1 subgoal):
 1. \<lbrakk>hd xs = last xs \<Longrightarrow> distinct (tl xs) = distinct (tl (rev xs)); hd (a # xs) = last (a # xs); xs \<noteq> []\<rbrakk> \<Longrightarrow> distinct (tl (a # xs)) = distinct (tl (rev (a # xs)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
distinct (tl (a # xs)) = distinct xs

goal (1 subgoal):
 1. \<lbrakk>hd xs = last xs \<Longrightarrow> distinct (tl xs) = distinct (tl (rev xs)); hd (a # xs) = last (a # xs); xs \<noteq> []\<rbrakk> \<Longrightarrow> distinct (tl (a # xs)) = distinct (tl (rev (a # xs)))
[PROOF STEP]
have "... \<longleftrightarrow> distinct (rev xs') \<and> a \<notin> set (rev xs')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct xs = (distinct (rev xs') \<and> a \<notin> set (rev xs'))
[PROOF STEP]
by (metis False Nil_is_rev_conv \<open>a = last xs\<close> distinct.simps(2) distinct_rev hd_rev list.exhaust_sel tleq)
[PROOF STATE]
proof (state)
this:
distinct xs = (distinct (rev xs') \<and> a \<notin> set (rev xs'))

goal (1 subgoal):
 1. \<lbrakk>hd xs = last xs \<Longrightarrow> distinct (tl xs) = distinct (tl (rev xs)); hd (a # xs) = last (a # xs); xs \<noteq> []\<rbrakk> \<Longrightarrow> distinct (tl (a # xs)) = distinct (tl (rev (a # xs)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
distinct (tl (a # xs)) = (distinct (rev xs') \<and> a \<notin> set (rev xs'))
[PROOF STEP]
show "distinct (tl (a # xs)) \<longleftrightarrow> distinct (tl (rev (a # xs)))"
[PROOF STATE]
proof (prove)
using this:
distinct (tl (a # xs)) = (distinct (rev xs') \<and> a \<notin> set (rev xs'))

goal (1 subgoal):
 1. distinct (tl (a # xs)) = distinct (tl (rev (a # xs)))
[PROOF STEP]
using tleq
[PROOF STATE]
proof (prove)
using this:
distinct (tl (a # xs)) = (distinct (rev xs') \<and> a \<notin> set (rev xs'))
tl (rev xs) = rev xs'

goal (1 subgoal):
 1. distinct (tl (a # xs)) = distinct (tl (rev (a # xs)))
[PROOF STEP]
by (simp add: False)
[PROOF STATE]
proof (state)
this:
distinct (tl (a # xs)) = distinct (tl (rev (a # xs)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
distinct (tl (a # xs)) = distinct (tl (rev (a # xs)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma last_in_list_set:  "length xs \<ge> 1 \<Longrightarrow> last xs \<in> set (xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> length xs \<Longrightarrow> last xs \<in> set xs
[PROOF STEP]
using dual_order.strict_trans1 last_in_set
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?b \<le> ?a; ?c < ?b\<rbrakk> \<Longrightarrow> ?c < ?a
?as \<noteq> [] \<Longrightarrow> last ?as \<in> set ?as

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


[STATEMENT]
lemma last_in_list_tl_set:
  assumes "length xs \<ge> 2"
  shows "last xs \<in> set (tl xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. last xs \<in> set (tl xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
2 \<le> length xs

goal (1 subgoal):
 1. last xs \<in> set (tl xs)
[PROOF STEP]
by (induct xs) auto


[STATEMENT]
lemma length_list_decomp_lt: "ys \<noteq> [] \<Longrightarrow> length (xs @zs) < length (xs@ys@zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ys \<noteq> [] \<Longrightarrow> length (xs @ zs) < length (xs @ ys @ zs)
[PROOF STEP]
using length_append
[PROOF STATE]
proof (prove)
using this:
length (?xs @ ?ys) = length ?xs + length ?ys

goal (1 subgoal):
 1. ys \<noteq> [] \<Longrightarrow> length (xs @ zs) < length (xs @ ys @ zs)
[PROOF STEP]
by simp


[STATEMENT]
lemma obtains_Max:
  assumes "finite A" and "A \<noteq> {}"
  obtains x where "x \<in> A" and "Max A = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> A; Max A = x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms Max_in
[PROOF STATE]
proof (prove)
using this:
finite A
A \<noteq> {}
\<lbrakk>finite ?A; ?A \<noteq> {}\<rbrakk> \<Longrightarrow> Max ?A \<in> ?A

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> A; Max A = x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast


[STATEMENT]
lemma obtains_MAX:
  assumes "finite A" and "A \<noteq> {}"
  obtains x where "x \<in> A" and "Max (f ` A) = f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> A; Max (f ` A) = f x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using obtains_Max
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?A; ?A \<noteq> {}; \<And>x. \<lbrakk>x \<in> ?A; Max ?A = x\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> A; Max (f ` A) = f x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis (mono_tags, opaque_lifting) assms(1) assms(2) empty_is_image finite_imageI image_iff)


[STATEMENT]
lemma obtains_Min:
  assumes "finite A" and "A \<noteq> {}"
  obtains x where "x \<in> A" and "Min A = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> A; Min A = x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms Min_in
[PROOF STATE]
proof (prove)
using this:
finite A
A \<noteq> {}
\<lbrakk>finite ?A; ?A \<noteq> {}\<rbrakk> \<Longrightarrow> Min ?A \<in> ?A

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> A; Min A = x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast


[STATEMENT]
lemma obtains_MIN:
  assumes "finite A" and "A \<noteq> {}"
  obtains x where "x \<in> A" and "Min (f ` A) = f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> A; Min (f ` A) = f x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using obtains_Min assms empty_is_image finite_imageI image_iff
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?A; ?A \<noteq> {}; \<And>x. \<lbrakk>x \<in> ?A; Min ?A = x\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
finite A
A \<noteq> {}
({} = ?f ` ?A) = (?A = {})
finite ?F \<Longrightarrow> finite (?h ` ?F)
(?z \<in> ?f ` ?A) = (\<exists>x\<in>?A. ?z = ?f x)

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> A; Min (f ` A) = f x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis (mono_tags, opaque_lifting))


[STATEMENT]
lemma all_edges_mono:
  "vs \<subseteq> ws \<Longrightarrow> all_edges vs \<subseteq> all_edges ws"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vs \<subseteq> ws \<Longrightarrow> all_edges vs \<subseteq> all_edges ws
[PROOF STEP]
unfolding all_edges_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vs \<subseteq> ws \<Longrightarrow> {e. e \<subseteq> vs \<and> card e = 2} \<subseteq> {e. e \<subseteq> ws \<and> card e = 2}
[PROOF STEP]
by auto


[STATEMENT]
lemma all_edges_alt: "all_edges S = {{x, y} | x y . x \<in> S \<and> y \<in> S \<and> x \<noteq> y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_edges S = {{x, y} |x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y}
[PROOF STEP]
unfolding all_edges_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {e. e \<subseteq> S \<and> card e = 2} = {{x, y} |x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y}
[PROOF STEP]
proof (intro subset_antisym subsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> {e. e \<subseteq> S \<and> card e = 2} \<Longrightarrow> x \<in> {{x, y} |x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y}
 2. \<And>x. x \<in> {{x, y} |x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y} \<Longrightarrow> x \<in> {e. e \<subseteq> S \<and> card e = 2}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> {e. e \<subseteq> S \<and> card e = 2} \<Longrightarrow> x \<in> {{x, y} |x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y}
 2. \<And>x. x \<in> {{x, y} |x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y} \<Longrightarrow> x \<in> {e. e \<subseteq> S \<and> card e = 2}
[PROOF STEP]
assume "x \<in> {e. e \<subseteq> S \<and> card e = 2}"
[PROOF STATE]
proof (state)
this:
x \<in> {e. e \<subseteq> S \<and> card e = 2}

goal (2 subgoals):
 1. \<And>x. x \<in> {e. e \<subseteq> S \<and> card e = 2} \<Longrightarrow> x \<in> {{x, y} |x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y}
 2. \<And>x. x \<in> {{x, y} |x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y} \<Longrightarrow> x \<in> {e. e \<subseteq> S \<and> card e = 2}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> {e. e \<subseteq> S \<and> card e = 2}
[PROOF STEP]
obtain u v where "x = {u, v}" and "card {u, v} = 2" and "{u, v} \<subseteq> S"
[PROOF STATE]
proof (prove)
using this:
x \<in> {e. e \<subseteq> S \<and> card e = 2}

goal (1 subgoal):
 1. (\<And>u v. \<lbrakk>x = {u, v}; card {u, v} = 2; {u, v} \<subseteq> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis (mono_tags, lifting) card_2_iff mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
x = {u, v}
card {u, v} = 2
{u, v} \<subseteq> S

goal (2 subgoals):
 1. \<And>x. x \<in> {e. e \<subseteq> S \<and> card e = 2} \<Longrightarrow> x \<in> {{x, y} |x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y}
 2. \<And>x. x \<in> {{x, y} |x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y} \<Longrightarrow> x \<in> {e. e \<subseteq> S \<and> card e = 2}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = {u, v}
card {u, v} = 2
{u, v} \<subseteq> S
[PROOF STEP]
show "x \<in> {{x, y} |x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y}"
[PROOF STATE]
proof (prove)
using this:
x = {u, v}
card {u, v} = 2
{u, v} \<subseteq> S

goal (1 subgoal):
 1. x \<in> {{x, y} |x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x \<in> {{x, y} |x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y}

goal (1 subgoal):
 1. \<And>x. x \<in> {{x, y} |x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y} \<Longrightarrow> x \<in> {e. e \<subseteq> S \<and> card e = 2}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {{x, y} |x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y} \<Longrightarrow> x \<in> {e. e \<subseteq> S \<and> card e = 2}
[PROOF STEP]
show "\<And>x. x \<in> {{x, y} |x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y} \<Longrightarrow> x \<in> {e. e \<subseteq> S \<and> card e = 2}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {{x, y} |x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y} \<Longrightarrow> x \<in> {e. e \<subseteq> S \<and> card e = 2}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x \<in> {{x, y} |x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y} \<Longrightarrow> ?x \<in> {e. e \<subseteq> S \<and> card e = 2}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma all_edges_alt_pairs: "all_edges S = mk_edge ` {uv \<in> S \<times> S. fst uv \<noteq> snd uv}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_edges S = mk_edge ` {uv \<in> S \<times> S. fst uv \<noteq> snd uv}
[PROOF STEP]
unfolding all_edges_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {{x, y} |x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y} = mk_edge ` {uv \<in> S \<times> S. fst uv \<noteq> snd uv}
[PROOF STEP]
proof (intro subset_antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {{x, y} |x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y} \<subseteq> mk_edge ` {uv \<in> S \<times> S. fst uv \<noteq> snd uv}
 2. mk_edge ` {uv \<in> S \<times> S. fst uv \<noteq> snd uv} \<subseteq> {{x, y} |x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y}
[PROOF STEP]
have img: "mk_edge ` {uv \<in> S \<times> S. fst uv \<noteq> snd uv} = {mk_edge (u, v) | u v. (u, v) \<in> S \<times> S \<and> u \<noteq>v}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_edge ` {uv \<in> S \<times> S. fst uv \<noteq> snd uv} = {mk_edge (u, v) |u v. (u, v) \<in> S \<times> S \<and> u \<noteq> v}
[PROOF STEP]
by (smt (z3) Collect_cong fst_conv prod.collapse setcompr_eq_image snd_conv)
[PROOF STATE]
proof (state)
this:
mk_edge ` {uv \<in> S \<times> S. fst uv \<noteq> snd uv} = {mk_edge (u, v) |u v. (u, v) \<in> S \<times> S \<and> u \<noteq> v}

goal (2 subgoals):
 1. {{x, y} |x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y} \<subseteq> mk_edge ` {uv \<in> S \<times> S. fst uv \<noteq> snd uv}
 2. mk_edge ` {uv \<in> S \<times> S. fst uv \<noteq> snd uv} \<subseteq> {{x, y} |x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mk_edge ` {uv \<in> S \<times> S. fst uv \<noteq> snd uv} = {mk_edge (u, v) |u v. (u, v) \<in> S \<times> S \<and> u \<noteq> v}
[PROOF STEP]
show " mk_edge ` {uv \<in> S \<times> S. fst uv \<noteq> snd uv} \<subseteq> {{x, y} |x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y}"
[PROOF STATE]
proof (prove)
using this:
mk_edge ` {uv \<in> S \<times> S. fst uv \<noteq> snd uv} = {mk_edge (u, v) |u v. (u, v) \<in> S \<times> S \<and> u \<noteq> v}

goal (1 subgoal):
 1. mk_edge ` {uv \<in> S \<times> S. fst uv \<noteq> snd uv} \<subseteq> {{x, y} |x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mk_edge ` {uv \<in> S \<times> S. fst uv \<noteq> snd uv} \<subseteq> {{x, y} |x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y}

goal (1 subgoal):
 1. {{x, y} |x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y} \<subseteq> mk_edge ` {uv \<in> S \<times> S. fst uv \<noteq> snd uv}
[PROOF STEP]
show  "{{x, y} |x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y} \<subseteq> mk_edge ` {uv \<in> S \<times> S. fst uv \<noteq> snd uv}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {{x, y} |x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y} \<subseteq> mk_edge ` {uv \<in> S \<times> S. fst uv \<noteq> snd uv}
[PROOF STEP]
using img
[PROOF STATE]
proof (prove)
using this:
mk_edge ` {uv \<in> S \<times> S. fst uv \<noteq> snd uv} = {mk_edge (u, v) |u v. (u, v) \<in> S \<times> S \<and> u \<noteq> v}

goal (1 subgoal):
 1. {{x, y} |x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y} \<subseteq> mk_edge ` {uv \<in> S \<times> S. fst uv \<noteq> snd uv}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{{x, y} |x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y} \<subseteq> mk_edge ` {uv \<in> S \<times> S. fst uv \<noteq> snd uv}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma all_edges_subset_Pow: "all_edges A \<subseteq> Pow A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_edges A \<subseteq> Pow A
[PROOF STEP]
by (auto simp: all_edges_def)


[STATEMENT]
lemma all_edges_disjoint:  "S \<inter> T = {} \<Longrightarrow> all_edges S \<inter> all_edges T = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<inter> T = {} \<Longrightarrow> all_edges S \<inter> all_edges T = {}
[PROOF STEP]
by (auto simp add: all_edges_def disjoint_iff subset_eq)


[STATEMENT]
lemma card_all_edges: "finite A \<Longrightarrow> card (all_edges A) = card A choose 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite A \<Longrightarrow> card (all_edges A) = card A choose 2
[PROOF STEP]
using all_edges_def
[PROOF STATE]
proof (prove)
using this:
all_edges ?S \<equiv> {e. e \<subseteq> ?S \<and> card e = 2}

goal (1 subgoal):
 1. finite A \<Longrightarrow> card (all_edges A) = card A choose 2
[PROOF STEP]
by (metis (full_types) n_subsets)


[STATEMENT]
lemma finite_all_edges: "finite S \<Longrightarrow> finite (all_edges S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite S \<Longrightarrow> finite (all_edges S)
[PROOF STEP]
by (meson all_edges_subset_Pow finite_Pow_iff finite_subset)


[STATEMENT]
lemma in_mk_edge_img: "(a,b) \<in> A \<or> (b,a) \<in> A \<Longrightarrow> {a,b} \<in> mk_edge ` A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a, b) \<in> A \<or> (b, a) \<in> A \<Longrightarrow> {a, b} \<in> mk_edge ` A
[PROOF STEP]
by (auto intro: rev_image_eqI)


[STATEMENT]
lemma in_mk_uedge_img_iff: "{a,b} \<in> mk_edge ` A \<longleftrightarrow> (a,b) \<in> A \<or> (b,a) \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({a, b} \<in> mk_edge ` A) = ((a, b) \<in> A \<or> (b, a) \<in> A)
[PROOF STEP]
by (auto simp: doubleton_eq_iff intro: rev_image_eqI)


[STATEMENT]
lemma inj_on_mk_edge: "X \<inter> Y = {} \<Longrightarrow> inj_on mk_edge (X \<times> Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<inter> Y = {} \<Longrightarrow> inj_on mk_edge (X \<times> Y)
[PROOF STEP]
by (auto simp: inj_on_def doubleton_eq_iff)


[STATEMENT]
lemma all_edges_loops_alt: "all_edges_loops S = {e . e \<subseteq> S \<and> (card e = 2 \<or> card e = 1)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_edges_loops S = {e. e \<subseteq> S \<and> (card e = 2 \<or> card e = 1)}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. all_edges_loops S = {e. e \<subseteq> S \<and> (card e = 2 \<or> card e = 1)}
[PROOF STEP]
have 1: " {{v} | v. v \<in> S} = {e . e \<subseteq> S \<and> card e = 1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {{v} |v. v \<in> S} = {e. e \<subseteq> S \<and> card e = 1}
[PROOF STEP]
by (metis One_nat_def card.empty card_Suc_eq empty_iff empty_subsetI insert_subset is_singleton_altdef is_singleton_the_elem )
[PROOF STATE]
proof (state)
this:
{{v} |v. v \<in> S} = {e. e \<subseteq> S \<and> card e = 1}

goal (1 subgoal):
 1. all_edges_loops S = {e. e \<subseteq> S \<and> (card e = 2 \<or> card e = 1)}
[PROOF STEP]
have "{e . e \<subseteq> S \<and> (card e = 2 \<or> card e = 1)} = {e . e \<subseteq> S \<and> card e = 2} \<union> {e . e \<subseteq> S \<and> card e = 1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {e. e \<subseteq> S \<and> (card e = 2 \<or> card e = 1)} = {e. e \<subseteq> S \<and> card e = 2} \<union> {e. e \<subseteq> S \<and> card e = 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{e. e \<subseteq> S \<and> (card e = 2 \<or> card e = 1)} = {e. e \<subseteq> S \<and> card e = 2} \<union> {e. e \<subseteq> S \<and> card e = 1}

goal (1 subgoal):
 1. all_edges_loops S = {e. e \<subseteq> S \<and> (card e = 2 \<or> card e = 1)}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{e. e \<subseteq> S \<and> (card e = 2 \<or> card e = 1)} = {e. e \<subseteq> S \<and> card e = 2} \<union> {e. e \<subseteq> S \<and> card e = 1}
[PROOF STEP]
have "{e . e \<subseteq> S \<and> (card e = 2 \<or> card e = 1)} = all_edges S \<union> {{v} | v. v \<in> S}"
[PROOF STATE]
proof (prove)
using this:
{e. e \<subseteq> S \<and> (card e = 2 \<or> card e = 1)} = {e. e \<subseteq> S \<and> card e = 2} \<union> {e. e \<subseteq> S \<and> card e = 1}

goal (1 subgoal):
 1. {e. e \<subseteq> S \<and> (card e = 2 \<or> card e = 1)} = all_edges S \<union> {{v} |v. v \<in> S}
[PROOF STEP]
by (simp add: all_edges_def 1)
[PROOF STATE]
proof (state)
this:
{e. e \<subseteq> S \<and> (card e = 2 \<or> card e = 1)} = all_edges S \<union> {{v} |v. v \<in> S}

goal (1 subgoal):
 1. all_edges_loops S = {e. e \<subseteq> S \<and> (card e = 2 \<or> card e = 1)}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{e. e \<subseteq> S \<and> (card e = 2 \<or> card e = 1)} = all_edges S \<union> {{v} |v. v \<in> S}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{e. e \<subseteq> S \<and> (card e = 2 \<or> card e = 1)} = all_edges S \<union> {{v} |v. v \<in> S}

goal (1 subgoal):
 1. all_edges_loops S = {e. e \<subseteq> S \<and> (card e = 2 \<or> card e = 1)}
[PROOF STEP]
unfolding all_edges_loops_def
[PROOF STATE]
proof (prove)
using this:
{e. e \<subseteq> S \<and> (card e = 2 \<or> card e = 1)} = all_edges S \<union> {{v} |v. v \<in> S}

goal (1 subgoal):
 1. all_edges S \<union> {{v} |v. v \<in> S} = {e. e \<subseteq> S \<and> (card e = 2 \<or> card e = 1)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
all_edges_loops S = {e. e \<subseteq> S \<and> (card e = 2 \<or> card e = 1)}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma loops_disjoint: "all_edges S \<inter> {{v} | v. v \<in> S} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_edges S \<inter> {{v} |v. v \<in> S} = {}
[PROOF STEP]
unfolding all_edges_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {e. e \<subseteq> S \<and> card e = 2} \<inter> {{v} |v. v \<in> S} = {}
[PROOF STEP]
using card_2_iff
[PROOF STATE]
proof (prove)
using this:
(card ?S = 2) = (\<exists>x y. ?S = {x, y} \<and> x \<noteq> y)

goal (1 subgoal):
 1. {e. e \<subseteq> S \<and> card e = 2} \<inter> {{v} |v. v \<in> S} = {}
[PROOF STEP]
by fastforce


[STATEMENT]
lemma all_edges_loops_ss: "all_edges S \<subseteq> all_edges_loops S" "{{v} | v. v \<in> S} \<subseteq> all_edges_loops S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_edges S \<subseteq> all_edges_loops S &&& {{v} |v. v \<in> S} \<subseteq> all_edges_loops S
[PROOF STEP]
by (simp_all add: all_edges_loops_def)


[STATEMENT]
lemma finite_singletons: "finite S \<Longrightarrow> finite ({{v} | v. v \<in> S})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite S \<Longrightarrow> finite {{v} |v. v \<in> S}
[PROOF STEP]
by (auto)


[STATEMENT]
lemma card_singletons:
  assumes "finite S" shows "card {{v} | v. v \<in> S} = card S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {{v} |v. v \<in> S} = card S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite S

goal (1 subgoal):
 1. card {{v} |v. v \<in> S} = card S
[PROOF STEP]
proof (induct S rule: finite_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. card {{v} |v. v \<in> {}} = card {}
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; card {{v} |v. v \<in> F} = card F\<rbrakk> \<Longrightarrow> card {{v} |v. v \<in> insert x F} = card (insert x F)
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. card {{v} |v. v \<in> {}} = card {}
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; card {{v} |v. v \<in> F} = card F\<rbrakk> \<Longrightarrow> card {{v} |v. v \<in> insert x F} = card (insert x F)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {{v} |v. v \<in> {}} = card {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {{v} |v. v \<in> {}} = card {}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; card {{v} |v. v \<in> F} = card F\<rbrakk> \<Longrightarrow> card {{v} |v. v \<in> insert x F} = card (insert x F)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; card {{v} |v. v \<in> F} = card F\<rbrakk> \<Longrightarrow> card {{v} |v. v \<in> insert x F} = card (insert x F)
[PROOF STEP]
case (insert x F)
[PROOF STATE]
proof (state)
this:
finite F
x \<notin> F
card {{v} |v. v \<in> F} = card F

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; card {{v} |v. v \<in> F} = card F\<rbrakk> \<Longrightarrow> card {{v} |v. v \<in> insert x F} = card (insert x F)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite F
x \<notin> F
card {{v} |v. v \<in> F} = card F
[PROOF STEP]
have disj: "{{x}} \<inter> {{v} |v. v \<in> F} = {}"
[PROOF STATE]
proof (prove)
using this:
finite F
x \<notin> F
card {{v} |v. v \<in> F} = card F

goal (1 subgoal):
 1. {{x}} \<inter> {{v} |v. v \<in> F} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{{x}} \<inter> {{v} |v. v \<in> F} = {}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; card {{v} |v. v \<in> F} = card F\<rbrakk> \<Longrightarrow> card {{v} |v. v \<in> insert x F} = card (insert x F)
[PROOF STEP]
have "{{v} |v. v \<in> insert x F} = ({{x}} \<union> {{v} |v. v \<in> F})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {{v} |v. v \<in> insert x F} = {{x}} \<union> {{v} |v. v \<in> F}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{{v} |v. v \<in> insert x F} = {{x}} \<union> {{v} |v. v \<in> F}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; card {{v} |v. v \<in> F} = card F\<rbrakk> \<Longrightarrow> card {{v} |v. v \<in> insert x F} = card (insert x F)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{{v} |v. v \<in> insert x F} = {{x}} \<union> {{v} |v. v \<in> F}
[PROOF STEP]
have "card {{v} |v. v \<in> insert x F} = card ({{x}} \<union> {{v} |v. v \<in> F})"
[PROOF STATE]
proof (prove)
using this:
{{v} |v. v \<in> insert x F} = {{x}} \<union> {{v} |v. v \<in> F}

goal (1 subgoal):
 1. card {{v} |v. v \<in> insert x F} = card ({{x}} \<union> {{v} |v. v \<in> F})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {{v} |v. v \<in> insert x F} = card ({{x}} \<union> {{v} |v. v \<in> F})

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; card {{v} |v. v \<in> F} = card F\<rbrakk> \<Longrightarrow> card {{v} |v. v \<in> insert x F} = card (insert x F)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card {{v} |v. v \<in> insert x F} = card ({{x}} \<union> {{v} |v. v \<in> F})

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; card {{v} |v. v \<in> F} = card F\<rbrakk> \<Longrightarrow> card {{v} |v. v \<in> insert x F} = card (insert x F)
[PROOF STEP]
have "... = card {{x}} + card {{v} |v. v \<in> F}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ({{x}} \<union> {{v} |v. v \<in> F}) = card {{x}} + card {{v} |v. v \<in> F}
[PROOF STEP]
using card_Un_disjoint disj assms finite_subset
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?A; finite ?B; ?A \<inter> ?B = {}\<rbrakk> \<Longrightarrow> card (?A \<union> ?B) = card ?A + card ?B
{{x}} \<inter> {{v} |v. v \<in> F} = {}
finite S
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. card ({{x}} \<union> {{v} |v. v \<in> F}) = card {{x}} + card {{v} |v. v \<in> F}
[PROOF STEP]
using insert.hyps(1)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?A; finite ?B; ?A \<inter> ?B = {}\<rbrakk> \<Longrightarrow> card (?A \<union> ?B) = card ?A + card ?B
{{x}} \<inter> {{v} |v. v \<in> F} = {}
finite S
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A
finite F

goal (1 subgoal):
 1. card ({{x}} \<union> {{v} |v. v \<in> F}) = card {{x}} + card {{v} |v. v \<in> F}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
card ({{x}} \<union> {{v} |v. v \<in> F}) = card {{x}} + card {{v} |v. v \<in> F}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; card {{v} |v. v \<in> F} = card F\<rbrakk> \<Longrightarrow> card {{v} |v. v \<in> insert x F} = card (insert x F)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card ({{x}} \<union> {{v} |v. v \<in> F}) = card {{x}} + card {{v} |v. v \<in> F}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; card {{v} |v. v \<in> F} = card F\<rbrakk> \<Longrightarrow> card {{v} |v. v \<in> insert x F} = card (insert x F)
[PROOF STEP]
have "... = 1 + card {{v} |v. v \<in> F}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {{x}} + card {{v} |v. v \<in> F} = 1 + card {{v} |v. v \<in> F}
[PROOF STEP]
using is_singleton_altdef
[PROOF STATE]
proof (prove)
using this:
is_singleton ?A = (card ?A = 1)

goal (1 subgoal):
 1. card {{x}} + card {{v} |v. v \<in> F} = 1 + card {{v} |v. v \<in> F}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {{x}} + card {{v} |v. v \<in> F} = 1 + card {{v} |v. v \<in> F}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; card {{v} |v. v \<in> F} = card F\<rbrakk> \<Longrightarrow> card {{v} |v. v \<in> insert x F} = card (insert x F)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card {{x}} + card {{v} |v. v \<in> F} = 1 + card {{v} |v. v \<in> F}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; card {{v} |v. v \<in> F} = card F\<rbrakk> \<Longrightarrow> card {{v} |v. v \<in> insert x F} = card (insert x F)
[PROOF STEP]
have "... = 1 + card F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + card {{v} |v. v \<in> F} = 1 + card F
[PROOF STEP]
using insert.hyps
[PROOF STATE]
proof (prove)
using this:
finite F
x \<notin> F
card {{v} |v. v \<in> F} = card F

goal (1 subgoal):
 1. 1 + card {{v} |v. v \<in> F} = 1 + card F
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 + card {{v} |v. v \<in> F} = 1 + card F

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; card {{v} |v. v \<in> F} = card F\<rbrakk> \<Longrightarrow> card {{v} |v. v \<in> insert x F} = card (insert x F)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card {{v} |v. v \<in> insert x F} = 1 + card F
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
card {{v} |v. v \<in> insert x F} = 1 + card F

goal (1 subgoal):
 1. card {{v} |v. v \<in> insert x F} = card (insert x F)
[PROOF STEP]
using insert.hyps(1) insert.hyps(2)
[PROOF STATE]
proof (prove)
using this:
card {{v} |v. v \<in> insert x F} = 1 + card F
finite F
x \<notin> F

goal (1 subgoal):
 1. card {{v} |v. v \<in> insert x F} = card (insert x F)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
card {{v} |v. v \<in> insert x F} = card (insert x F)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_all_edges_loops: "finite S \<Longrightarrow> finite (all_edges_loops S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite S \<Longrightarrow> finite (all_edges_loops S)
[PROOF STEP]
unfolding all_edges_loops_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite S \<Longrightarrow> finite (all_edges S \<union> {{v} |v. v \<in> S})
[PROOF STEP]
using finite_all_edges finite_singletons
[PROOF STATE]
proof (prove)
using this:
finite ?S \<Longrightarrow> finite (all_edges ?S)
finite ?S \<Longrightarrow> finite {{v} |v. v \<in> ?S}

goal (1 subgoal):
 1. finite S \<Longrightarrow> finite (all_edges S \<union> {{v} |v. v \<in> S})
[PROOF STEP]
by auto


[STATEMENT]
lemma card_all_edges_loops:
  assumes "finite S"
  shows "card (all_edges_loops S) = (card S) choose 2 + card S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (all_edges_loops S) = card S choose 2 + card S
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (all_edges_loops S) = card S choose 2 + card S
[PROOF STEP]
have "card (all_edges_loops S) = card (all_edges S \<union> {{v} | v. v \<in> S})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (all_edges_loops S) = card (all_edges S \<union> {{v} |v. v \<in> S})
[PROOF STEP]
by (simp add: all_edges_loops_def)
[PROOF STATE]
proof (state)
this:
card (all_edges_loops S) = card (all_edges S \<union> {{v} |v. v \<in> S})

goal (1 subgoal):
 1. card (all_edges_loops S) = card S choose 2 + card S
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (all_edges_loops S) = card (all_edges S \<union> {{v} |v. v \<in> S})

goal (1 subgoal):
 1. card (all_edges_loops S) = card S choose 2 + card S
[PROOF STEP]
have "... = card (all_edges S) + card {{v} | v. v \<in> S}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (all_edges S \<union> {{v} |v. v \<in> S}) = card (all_edges S) + card {{v} |v. v \<in> S}
[PROOF STEP]
using loops_disjoint assms card_Un_disjoint[of "all_edges S" "{{v} | v. v \<in> S}"]
      all_edges_loops_ss finite_all_edges_loops finite_subset
[PROOF STATE]
proof (prove)
using this:
all_edges ?S \<inter> {{v} |v. v \<in> ?S} = {}
finite S
\<lbrakk>finite (all_edges S); finite {{v} |v. v \<in> S}; all_edges S \<inter> {{v} |v. v \<in> S} = {}\<rbrakk> \<Longrightarrow> card (all_edges S \<union> {{v} |v. v \<in> S}) = card (all_edges S) + card {{v} |v. v \<in> S}
all_edges ?S \<subseteq> all_edges_loops ?S
{{v} |v. v \<in> ?S} \<subseteq> all_edges_loops ?S
finite ?S \<Longrightarrow> finite (all_edges_loops ?S)
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. card (all_edges S \<union> {{v} |v. v \<in> S}) = card (all_edges S) + card {{v} |v. v \<in> S}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
card (all_edges S \<union> {{v} |v. v \<in> S}) = card (all_edges S) + card {{v} |v. v \<in> S}

goal (1 subgoal):
 1. card (all_edges_loops S) = card S choose 2 + card S
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (all_edges S \<union> {{v} |v. v \<in> S}) = card (all_edges S) + card {{v} |v. v \<in> S}

goal (1 subgoal):
 1. card (all_edges_loops S) = card S choose 2 + card S
[PROOF STEP]
have "... = (card S) choose 2 + card {{v} | v. v \<in> S}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (all_edges S) + card {{v} |v. v \<in> S} = card S choose 2 + card {{v} |v. v \<in> S}
[PROOF STEP]
by(simp add: card_all_edges assms)
[PROOF STATE]
proof (state)
this:
card (all_edges S) + card {{v} |v. v \<in> S} = card S choose 2 + card {{v} |v. v \<in> S}

goal (1 subgoal):
 1. card (all_edges_loops S) = card S choose 2 + card S
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card (all_edges_loops S) = card S choose 2 + card {{v} |v. v \<in> S}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card (all_edges_loops S) = card S choose 2 + card {{v} |v. v \<in> S}

goal (1 subgoal):
 1. card (all_edges_loops S) = card S choose 2 + card S
[PROOF STEP]
using assms card_singletons
[PROOF STATE]
proof (prove)
using this:
card (all_edges_loops S) = card S choose 2 + card {{v} |v. v \<in> S}
finite S
finite ?S \<Longrightarrow> card {{v} |v. v \<in> ?S} = card ?S

goal (1 subgoal):
 1. card (all_edges_loops S) = card S choose 2 + card S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (all_edges_loops S) = card S choose 2 + card S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma incident_edge_in_wf: "e \<in> E \<Longrightarrow> incident v e \<Longrightarrow> v \<in> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>e \<in> E; incident v e\<rbrakk> \<Longrightarrow> v \<in> V
[PROOF STEP]
using wellformed incident_def
[PROOF STATE]
proof (prove)
using this:
?e \<in> E \<Longrightarrow> ?e \<subseteq> V
incident ?v ?e \<equiv> ?v \<in> ?e

goal (1 subgoal):
 1. \<lbrakk>e \<in> E; incident v e\<rbrakk> \<Longrightarrow> v \<in> V
[PROOF STEP]
by auto


[STATEMENT]
lemma incident_edges_empty: "\<not> (v \<in> V) \<Longrightarrow> incident_edges v = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<notin> V \<Longrightarrow> incident_edges v = {}
[PROOF STEP]
using incident_edges_def incident_edge_in_wf
[PROOF STATE]
proof (prove)
using this:
incident_edges ?v \<equiv> {e \<in> E. incident ?v e}
\<lbrakk>?e \<in> E; incident ?v ?e\<rbrakk> \<Longrightarrow> ?v \<in> V

goal (1 subgoal):
 1. v \<notin> V \<Longrightarrow> incident_edges v = {}
[PROOF STEP]
by auto


[STATEMENT]
lemma finite_incident_edges: "finite E \<Longrightarrow> finite (incident_edges v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite E \<Longrightarrow> finite (incident_edges v)
[PROOF STEP]
by (simp add: incident_edges_def)


[STATEMENT]
lemma edge_adj_inE: "edge_adj e1 e2 \<Longrightarrow> e1 \<in> E \<and> e2 \<in> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. edge_adj e1 e2 \<Longrightarrow> e1 \<in> E \<and> e2 \<in> E
[PROOF STEP]
using edge_adj_def
[PROOF STATE]
proof (prove)
using this:
edge_adj ?e1.0 ?e2.0 \<equiv> ?e1.0 \<inter> ?e2.0 \<noteq> {} \<and> ?e1.0 \<in> E \<and> ?e2.0 \<in> E

goal (1 subgoal):
 1. edge_adj e1 e2 \<Longrightarrow> e1 \<in> E \<and> e2 \<in> E
[PROOF STEP]
by auto


[STATEMENT]
lemma edge_adjacent_alt_def: "e1 \<in> E \<Longrightarrow> e2 \<in> E \<Longrightarrow> \<exists> x . x \<in> V \<and> x \<in> e1 \<and> x \<in> e2 \<Longrightarrow> edge_adj e1 e2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>e1 \<in> E; e2 \<in> E; \<exists>x. x \<in> V \<and> x \<in> e1 \<and> x \<in> e2\<rbrakk> \<Longrightarrow> edge_adj e1 e2
[PROOF STEP]
unfolding edge_adj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>e1 \<in> E; e2 \<in> E; \<exists>x. x \<in> V \<and> x \<in> e1 \<and> x \<in> e2\<rbrakk> \<Longrightarrow> e1 \<inter> e2 \<noteq> {} \<and> e1 \<in> E \<and> e2 \<in> E
[PROOF STEP]
by auto


[STATEMENT]
lemma wellformed_alt_fst:  "{x, y} \<in> E \<Longrightarrow> x \<in> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x, y} \<in> E \<Longrightarrow> x \<in> V
[PROOF STEP]
using wellformed
[PROOF STATE]
proof (prove)
using this:
?e \<in> E \<Longrightarrow> ?e \<subseteq> V

goal (1 subgoal):
 1. {x, y} \<in> E \<Longrightarrow> x \<in> V
[PROOF STEP]
by auto


[STATEMENT]
lemma wellformed_alt_snd:  "{x, y} \<in> E \<Longrightarrow> y \<in> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x, y} \<in> E \<Longrightarrow> y \<in> V
[PROOF STEP]
using wellformed
[PROOF STATE]
proof (prove)
using this:
?e \<in> E \<Longrightarrow> ?e \<subseteq> V

goal (1 subgoal):
 1. {x, y} \<in> E \<Longrightarrow> y \<in> V
[PROOF STEP]
by auto


[STATEMENT]
lemma fin_edges: "finite E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite E
[PROOF STEP]
using wellformed finV
[PROOF STATE]
proof (prove)
using this:
?e \<in> E \<Longrightarrow> ?e \<subseteq> V
finite V

goal (1 subgoal):
 1. finite E
[PROOF STEP]
by (meson PowI finite_Pow_iff finite_subset subsetI)


[STATEMENT]
lemma alt_edge_size: "e \<in> E \<Longrightarrow> card e = 1 \<or> card e = 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e \<in> E \<Longrightarrow> card e = 1 \<or> card e = 2
[PROOF STEP]
using edge_size
[PROOF STATE]
proof (prove)
using this:
?e \<in> E \<Longrightarrow> 0 < card ?e \<and> card ?e \<le> 2

goal (1 subgoal):
 1. e \<in> E \<Longrightarrow> card e = 1 \<or> card e = 2
[PROOF STEP]
by fastforce


[STATEMENT]
lemma is_edge_or_loop: "e \<in> E \<Longrightarrow> is_loop e \<or> is_sedge e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e \<in> E \<Longrightarrow> is_loop e \<or> is_sedge e
[PROOF STEP]
using alt_edge_size is_loop_def is_sedge_def
[PROOF STATE]
proof (prove)
using this:
?e \<in> E \<Longrightarrow> card ?e = 1 \<or> card ?e = 2
is_loop ?e \<equiv> card ?e = 1
is_sedge ?e \<equiv> card ?e = 2

goal (1 subgoal):
 1. e \<in> E \<Longrightarrow> is_loop e \<or> is_sedge e
[PROOF STEP]
by simp


[STATEMENT]
lemma edges_split_loop: "E = {e \<in> E . is_loop e } \<union> {e \<in> E . is_sedge e}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E = {e \<in> E. is_loop e} \<union> {e \<in> E. is_sedge e}
[PROOF STEP]
using is_edge_or_loop
[PROOF STATE]
proof (prove)
using this:
?e \<in> E \<Longrightarrow> is_loop ?e \<or> is_sedge ?e

goal (1 subgoal):
 1. E = {e \<in> E. is_loop e} \<union> {e \<in> E. is_sedge e}
[PROOF STEP]
by auto


[STATEMENT]
lemma edges_split_loop_inter_empty: "{} = {e \<in> E . is_loop e } \<inter> {e \<in> E . is_sedge e}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} = {e \<in> E. is_loop e} \<inter> {e \<in> E. is_sedge e}
[PROOF STEP]
unfolding is_loop_def is_sedge_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} = {e \<in> E. card e = 1} \<inter> {e \<in> E. card e = 2}
[PROOF STEP]
by auto


[STATEMENT]
lemma vert_adj_sym: "vert_adj v1 v2 \<longleftrightarrow> vert_adj v2 v1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vert_adj v1 v2 = vert_adj v2 v1
[PROOF STEP]
unfolding vert_adj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({v1, v2} \<in> E) = ({v2, v1} \<in> E)
[PROOF STEP]
by (simp_all add: insert_commute)


[STATEMENT]
lemma vert_adj_imp_inV: "vert_adj v1 v2 \<Longrightarrow> v1 \<in> V \<and> v2 \<in> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vert_adj v1 v2 \<Longrightarrow> v1 \<in> V \<and> v2 \<in> V
[PROOF STEP]
using vert_adj_def wellformed
[PROOF STATE]
proof (prove)
using this:
vert_adj ?v1.0 ?v2.0 \<equiv> {?v1.0, ?v2.0} \<in> E
?e \<in> E \<Longrightarrow> ?e \<subseteq> V

goal (1 subgoal):
 1. vert_adj v1 v2 \<Longrightarrow> v1 \<in> V \<and> v2 \<in> V
[PROOF STEP]
by auto


[STATEMENT]
lemma vert_adj_inc_edge_iff: "vert_adj v1 v2 \<longleftrightarrow> incident v1 {v1, v2} \<and> incident v2 {v1, v2} \<and> {v1, v2} \<in> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vert_adj v1 v2 = (incident v1 {v1, v2} \<and> incident v2 {v1, v2} \<and> {v1, v2} \<in> E)
[PROOF STEP]
unfolding vert_adj_def incident_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({v1, v2} \<in> E) = (v1 \<in> {v1, v2} \<and> v2 \<in> {v1, v2} \<and> {v1, v2} \<in> E)
[PROOF STEP]
by auto


[STATEMENT]
lemma not_vert_adj[simp]: "\<not> vert_adj v u \<Longrightarrow> {v, u} \<notin> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> vert_adj v u \<Longrightarrow> {v, u} \<notin> E
[PROOF STEP]
by (simp add: vert_adj_def)


[STATEMENT]
lemma neighborhood_incident: "u \<in> neighborhood v \<longleftrightarrow> {u, v} \<in> incident_edges v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u \<in> neighborhood v) = ({u, v} \<in> incident_edges v)
[PROOF STEP]
unfolding neighborhood_def incident_edges_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u \<in> {va \<in> V. vert_adj v va}) = ({u, v} \<in> {e \<in> E. incident v e})
[PROOF STEP]
by (smt (verit) incident_def insert_commute insert_subset mem_Collect_eq subset_insertI vert_adj_def wellformed)


[STATEMENT]
lemma vert_adj_edge_iff2:
  assumes "v1 \<noteq> v2"
  shows "vert_adj v1 v2 \<longleftrightarrow> (\<exists> e \<in> E . incident v1 e \<and> incident v2 e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vert_adj v1 v2 = (\<exists>e\<in>E. incident v1 e \<and> incident v2 e)
[PROOF STEP]
proof (intro iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vert_adj v1 v2 \<Longrightarrow> \<exists>e\<in>E. incident v1 e \<and> incident v2 e
 2. \<exists>e\<in>E. incident v1 e \<and> incident v2 e \<Longrightarrow> vert_adj v1 v2
[PROOF STEP]
show "vert_adj v1 v2 \<Longrightarrow> \<exists>e\<in>E. incident v1 e \<and> incident v2 e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vert_adj v1 v2 \<Longrightarrow> \<exists>e\<in>E. incident v1 e \<and> incident v2 e
[PROOF STEP]
using vert_adj_inc_edge_iff
[PROOF STATE]
proof (prove)
using this:
vert_adj ?v1.0 ?v2.0 = (incident ?v1.0 {?v1.0, ?v2.0} \<and> incident ?v2.0 {?v1.0, ?v2.0} \<and> {?v1.0, ?v2.0} \<in> E)

goal (1 subgoal):
 1. vert_adj v1 v2 \<Longrightarrow> \<exists>e\<in>E. incident v1 e \<and> incident v2 e
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vert_adj v1 v2 \<Longrightarrow> \<exists>e\<in>E. incident v1 e \<and> incident v2 e

goal (1 subgoal):
 1. \<exists>e\<in>E. incident v1 e \<and> incident v2 e \<Longrightarrow> vert_adj v1 v2
[PROOF STEP]
assume "\<exists>e\<in>E. incident v1 e \<and> incident v2 e"
[PROOF STATE]
proof (state)
this:
\<exists>e\<in>E. incident v1 e \<and> incident v2 e

goal (1 subgoal):
 1. \<exists>e\<in>E. incident v1 e \<and> incident v2 e \<Longrightarrow> vert_adj v1 v2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>e\<in>E. incident v1 e \<and> incident v2 e
[PROOF STEP]
obtain e where ein: "e \<in> E" and "incident v1 e" and "incident v2 e"
[PROOF STATE]
proof (prove)
using this:
\<exists>e\<in>E. incident v1 e \<and> incident v2 e

goal (1 subgoal):
 1. (\<And>e. \<lbrakk>e \<in> E; incident v1 e; incident v2 e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using vert_adj_inc_edge_iff assms alt_edge_size
[PROOF STATE]
proof (prove)
using this:
\<exists>e\<in>E. incident v1 e \<and> incident v2 e
vert_adj ?v1.0 ?v2.0 = (incident ?v1.0 {?v1.0, ?v2.0} \<and> incident ?v2.0 {?v1.0, ?v2.0} \<and> {?v1.0, ?v2.0} \<in> E)
v1 \<noteq> v2
?e \<in> E \<Longrightarrow> card ?e = 1 \<or> card ?e = 2

goal (1 subgoal):
 1. (\<And>e. \<lbrakk>e \<in> E; incident v1 e; incident v2 e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
e \<in> E
incident v1 e
incident v2 e

goal (1 subgoal):
 1. \<exists>e\<in>E. incident v1 e \<and> incident v2 e \<Longrightarrow> vert_adj v1 v2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e \<in> E
incident v1 e
incident v2 e
[PROOF STEP]
have "e = {v1, v2}"
[PROOF STATE]
proof (prove)
using this:
e \<in> E
incident v1 e
incident v2 e

goal (1 subgoal):
 1. e = {v1, v2}
[PROOF STEP]
using alt_edge_size assms
[PROOF STATE]
proof (prove)
using this:
e \<in> E
incident v1 e
incident v2 e
?e \<in> E \<Longrightarrow> card ?e = 1 \<or> card ?e = 2
v1 \<noteq> v2

goal (1 subgoal):
 1. e = {v1, v2}
[PROOF STEP]
by (smt (verit) card_1_singletonE card_2_iff incident_def insertE insert_commute singletonD)
[PROOF STATE]
proof (state)
this:
e = {v1, v2}

goal (1 subgoal):
 1. \<exists>e\<in>E. incident v1 e \<and> incident v2 e \<Longrightarrow> vert_adj v1 v2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e = {v1, v2}
[PROOF STEP]
show "vert_adj v1 v2"
[PROOF STATE]
proof (prove)
using this:
e = {v1, v2}

goal (1 subgoal):
 1. vert_adj v1 v2
[PROOF STEP]
using ein vert_adj_def
[PROOF STATE]
proof (prove)
using this:
e = {v1, v2}
e \<in> E
vert_adj ?v1.0 ?v2.0 \<equiv> {?v1.0, ?v2.0} \<in> E

goal (1 subgoal):
 1. vert_adj v1 v2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vert_adj v1 v2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_inc_sedges: "finite E \<Longrightarrow> finite (incident_sedges v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite E \<Longrightarrow> finite (incident_sedges v)
[PROOF STEP]
by (simp add: incident_sedges_def)


[STATEMENT]
lemma incident_sedges_empty[simp]: "v \<notin> V \<Longrightarrow> incident_sedges v = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<notin> V \<Longrightarrow> incident_sedges v = {}
[PROOF STEP]
unfolding incident_sedges_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<notin> V \<Longrightarrow> {e \<in> E. incident v e \<and> card e = 2} = {}
[PROOF STEP]
using incident_def wellformed
[PROOF STATE]
proof (prove)
using this:
incident ?v ?e \<equiv> ?v \<in> ?e
?e \<in> E \<Longrightarrow> ?e \<subseteq> V

goal (1 subgoal):
 1. v \<notin> V \<Longrightarrow> {e \<in> E. incident v e \<and> card e = 2} = {}
[PROOF STEP]
by fastforce


[STATEMENT]
lemma has_loop_in_verts: "has_loop v \<Longrightarrow> v \<in> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_loop v \<Longrightarrow> v \<in> V
[PROOF STEP]
using has_loop_def wellformed
[PROOF STATE]
proof (prove)
using this:
has_loop ?v \<equiv> {?v} \<in> E
?e \<in> E \<Longrightarrow> ?e \<subseteq> V

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


[STATEMENT]
lemma is_loop_set_alt: "{{v} | v . has_loop v} = {e \<in> E . is_loop e}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {{v} |v. has_loop v} = {e \<in> E. is_loop e}
[PROOF STEP]
proof (intro subset_antisym subsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> {{v} |v. has_loop v} \<Longrightarrow> x \<in> {e \<in> E. is_loop e}
 2. \<And>x. x \<in> {e \<in> E. is_loop e} \<Longrightarrow> x \<in> {{v} |v. has_loop v}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> {{v} |v. has_loop v} \<Longrightarrow> x \<in> {e \<in> E. is_loop e}
 2. \<And>x. x \<in> {e \<in> E. is_loop e} \<Longrightarrow> x \<in> {{v} |v. has_loop v}
[PROOF STEP]
assume "x \<in> {{v} |v. has_loop v}"
[PROOF STATE]
proof (state)
this:
x \<in> {{v} |v. has_loop v}

goal (2 subgoals):
 1. \<And>x. x \<in> {{v} |v. has_loop v} \<Longrightarrow> x \<in> {e \<in> E. is_loop e}
 2. \<And>x. x \<in> {e \<in> E. is_loop e} \<Longrightarrow> x \<in> {{v} |v. has_loop v}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> {{v} |v. has_loop v}
[PROOF STEP]
obtain v where "x = {v}" and "has_loop v"
[PROOF STATE]
proof (prove)
using this:
x \<in> {{v} |v. has_loop v}

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>x = {v}; has_loop v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x = {v}
has_loop v

goal (2 subgoals):
 1. \<And>x. x \<in> {{v} |v. has_loop v} \<Longrightarrow> x \<in> {e \<in> E. is_loop e}
 2. \<And>x. x \<in> {e \<in> E. is_loop e} \<Longrightarrow> x \<in> {{v} |v. has_loop v}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = {v}
has_loop v
[PROOF STEP]
show "x \<in> {e \<in> E. is_loop e}"
[PROOF STATE]
proof (prove)
using this:
x = {v}
has_loop v

goal (1 subgoal):
 1. x \<in> {e \<in> E. is_loop e}
[PROOF STEP]
using has_loop_def is_loop_def
[PROOF STATE]
proof (prove)
using this:
x = {v}
has_loop v
has_loop ?v \<equiv> {?v} \<in> E
is_loop ?e \<equiv> card ?e = 1

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

goal (1 subgoal):
 1. \<And>x. x \<in> {e \<in> E. is_loop e} \<Longrightarrow> x \<in> {{v} |v. has_loop v}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {e \<in> E. is_loop e} \<Longrightarrow> x \<in> {{v} |v. has_loop v}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {e \<in> E. is_loop e} \<Longrightarrow> x \<in> {{v} |v. has_loop v}
[PROOF STEP]
assume a: "x \<in>{e \<in> E. is_loop e}"
[PROOF STATE]
proof (state)
this:
x \<in> {e \<in> E. is_loop e}

goal (1 subgoal):
 1. \<And>x. x \<in> {e \<in> E. is_loop e} \<Longrightarrow> x \<in> {{v} |v. has_loop v}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> {e \<in> E. is_loop e}
[PROOF STEP]
have "is_loop x"
[PROOF STATE]
proof (prove)
using this:
x \<in> {e \<in> E. is_loop e}

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

goal (1 subgoal):
 1. \<And>x. x \<in> {e \<in> E. is_loop e} \<Longrightarrow> x \<in> {{v} |v. has_loop v}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_loop x
[PROOF STEP]
obtain v where "x = {v}" and "{v} \<in> E"
[PROOF STATE]
proof (prove)
using this:
is_loop x

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>x = {v}; {v} \<in> E\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using is_loop_def a
[PROOF STATE]
proof (prove)
using this:
is_loop x
is_loop ?e \<equiv> card ?e = 1
x \<in> {e \<in> E. is_loop e}

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>x = {v}; {v} \<in> E\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis card_1_singletonE mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
x = {v}
{v} \<in> E

goal (1 subgoal):
 1. \<And>x. x \<in> {e \<in> E. is_loop e} \<Longrightarrow> x \<in> {{v} |v. has_loop v}
[PROOF STEP]
thus "x \<in> {{v} |v. has_loop v}"
[PROOF STATE]
proof (prove)
using this:
x = {v}
{v} \<in> E

goal (1 subgoal):
 1. x \<in> {{v} |v. has_loop v}
[PROOF STEP]
using has_loop_def
[PROOF STATE]
proof (prove)
using this:
x = {v}
{v} \<in> E
has_loop ?v \<equiv> {?v} \<in> E

goal (1 subgoal):
 1. x \<in> {{v} |v. has_loop v}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> {{v} |v. has_loop v}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma card1_incident_imp_vert: "incident v e \<and> card e = 1 \<Longrightarrow> e = {v}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. incident v e \<and> card e = 1 \<Longrightarrow> e = {v}
[PROOF STEP]
by (metis card_1_singletonE incident_def singleton_iff)


[STATEMENT]
lemma incident_loops_alt: "incident_loops v = {e \<in> E. incident v e \<and> card e = 1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. incident_loops v = {e \<in> E. incident v e \<and> card e = 1}
[PROOF STEP]
unfolding incident_loops_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {e \<in> E. e = {v}} = {e \<in> E. incident v e \<and> card e = 1}
[PROOF STEP]
using card1_incident_imp_vert incident_def
[PROOF STATE]
proof (prove)
using this:
incident ?v ?e \<and> card ?e = 1 \<Longrightarrow> ?e = {?v}
incident ?v ?e \<equiv> ?v \<in> ?e

goal (1 subgoal):
 1. {e \<in> E. e = {v}} = {e \<in> E. incident v e \<and> card e = 1}
[PROOF STEP]
by auto


[STATEMENT]
lemma incident_loops_simp: "has_loop v \<Longrightarrow> incident_loops v = {{v}}" "\<not> has_loop v \<Longrightarrow> incident_loops v = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (has_loop v \<Longrightarrow> incident_loops v = {{v}}) &&& (\<not> has_loop v \<Longrightarrow> incident_loops v = {})
[PROOF STEP]
unfolding incident_loops_def has_loop_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({v} \<in> E \<Longrightarrow> {e \<in> E. e = {v}} = {{v}}) &&& ({v} \<notin> E \<Longrightarrow> {e \<in> E. e = {v}} = {})
[PROOF STEP]
by auto


[STATEMENT]
lemma incident_loops_union: "\<Union> (incident_loops ` V) = {e \<in> E . is_loop e}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (incident_loops ` V) = {e \<in> E. is_loop e}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union> (incident_loops ` V) = {e \<in> E. is_loop e}
[PROOF STEP]
have "V = {v \<in> V. has_loop v} \<union> {v \<in> V . \<not> has_loop v}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V = {v \<in> V. has_loop v} \<union> {v \<in> V. \<not> has_loop v}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V = {v \<in> V. has_loop v} \<union> {v \<in> V. \<not> has_loop v}

goal (1 subgoal):
 1. \<Union> (incident_loops ` V) = {e \<in> E. is_loop e}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
V = {v \<in> V. has_loop v} \<union> {v \<in> V. \<not> has_loop v}
[PROOF STEP]
have "\<Union> (incident_loops ` V) = \<Union> (incident_loops ` {v \<in> V. has_loop v}) \<union>
      \<Union> (incident_loops ` {v \<in> V. \<not> has_loop v})"
[PROOF STATE]
proof (prove)
using this:
V = {v \<in> V. has_loop v} \<union> {v \<in> V. \<not> has_loop v}

goal (1 subgoal):
 1. \<Union> (incident_loops ` V) = \<Union> (incident_loops ` {v \<in> V. has_loop v}) \<union> \<Union> (incident_loops ` {v \<in> V. \<not> has_loop v})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Union> (incident_loops ` V) = \<Union> (incident_loops ` {v \<in> V. has_loop v}) \<union> \<Union> (incident_loops ` {v \<in> V. \<not> has_loop v})

goal (1 subgoal):
 1. \<Union> (incident_loops ` V) = {e \<in> E. is_loop e}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Union> (incident_loops ` V) = \<Union> (incident_loops ` {v \<in> V. has_loop v}) \<union> \<Union> (incident_loops ` {v \<in> V. \<not> has_loop v})

goal (1 subgoal):
 1. \<Union> (incident_loops ` V) = {e \<in> E. is_loop e}
[PROOF STEP]
have "... = \<Union> (incident_loops ` {v \<in> V. has_loop v})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (incident_loops ` {v \<in> V. has_loop v}) \<union> \<Union> (incident_loops ` {v \<in> V. \<not> has_loop v}) = \<Union> (incident_loops ` {v \<in> V. has_loop v})
[PROOF STEP]
using incident_loops_simp(2)
[PROOF STATE]
proof (prove)
using this:
\<not> has_loop ?v \<Longrightarrow> incident_loops ?v = {}

goal (1 subgoal):
 1. \<Union> (incident_loops ` {v \<in> V. has_loop v}) \<union> \<Union> (incident_loops ` {v \<in> V. \<not> has_loop v}) = \<Union> (incident_loops ` {v \<in> V. has_loop v})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Union> (incident_loops ` {v \<in> V. has_loop v}) \<union> \<Union> (incident_loops ` {v \<in> V. \<not> has_loop v}) = \<Union> (incident_loops ` {v \<in> V. has_loop v})

goal (1 subgoal):
 1. \<Union> (incident_loops ` V) = {e \<in> E. is_loop e}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Union> (incident_loops ` {v \<in> V. has_loop v}) \<union> \<Union> (incident_loops ` {v \<in> V. \<not> has_loop v}) = \<Union> (incident_loops ` {v \<in> V. has_loop v})

goal (1 subgoal):
 1. \<Union> (incident_loops ` V) = {e \<in> E. is_loop e}
[PROOF STEP]
have "... = \<Union> ({{{v}} | v . has_loop v})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (incident_loops ` {v \<in> V. has_loop v}) = \<Union> {{{v}} |v. has_loop v}
[PROOF STEP]
using has_loop_in_verts incident_loops_simp(1)
[PROOF STATE]
proof (prove)
using this:
has_loop ?v \<Longrightarrow> ?v \<in> V
has_loop ?v \<Longrightarrow> incident_loops ?v = {{?v}}

goal (1 subgoal):
 1. \<Union> (incident_loops ` {v \<in> V. has_loop v}) = \<Union> {{{v}} |v. has_loop v}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Union> (incident_loops ` {v \<in> V. has_loop v}) = \<Union> {{{v}} |v. has_loop v}

goal (1 subgoal):
 1. \<Union> (incident_loops ` V) = {e \<in> E. is_loop e}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Union> (incident_loops ` {v \<in> V. has_loop v}) = \<Union> {{{v}} |v. has_loop v}

goal (1 subgoal):
 1. \<Union> (incident_loops ` V) = {e \<in> E. is_loop e}
[PROOF STEP]
have "... = ({{v} | v . has_loop v})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> {{{v}} |v. has_loop v} = {{v} |v. has_loop v}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Union> {{{v}} |v. has_loop v} = {{v} |v. has_loop v}

goal (1 subgoal):
 1. \<Union> (incident_loops ` V) = {e \<in> E. is_loop e}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Union> (incident_loops ` V) = {{v} |v. has_loop v}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Union> (incident_loops ` V) = {{v} |v. has_loop v}

goal (1 subgoal):
 1. \<Union> (incident_loops ` V) = {e \<in> E. is_loop e}
[PROOF STEP]
using is_loop_set_alt
[PROOF STATE]
proof (prove)
using this:
\<Union> (incident_loops ` V) = {{v} |v. has_loop v}
{{v} |v. has_loop v} = {e \<in> E. is_loop e}

goal (1 subgoal):
 1. \<Union> (incident_loops ` V) = {e \<in> E. is_loop e}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Union> (incident_loops ` V) = {e \<in> E. is_loop e}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_incident_loops: "finite (incident_loops v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (incident_loops v)
[PROOF STEP]
using incident_loops_simp
[PROOF STATE]
proof (prove)
using this:
has_loop ?v \<Longrightarrow> incident_loops ?v = {{?v}}
\<not> has_loop ?v \<Longrightarrow> incident_loops ?v = {}

goal (1 subgoal):
 1. finite (incident_loops v)
[PROOF STEP]
by (cases "has_loop v") auto


[STATEMENT]
lemma incident_loops_card: "card (incident_loops v) \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (incident_loops v) \<le> 1
[PROOF STEP]
by (cases "has_loop v") (simp_all add: incident_loops_simp)


[STATEMENT]
lemma incident_edges_union: "incident_edges v = incident_sedges v \<union> incident_loops v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. incident_edges v = incident_sedges v \<union> incident_loops v
[PROOF STEP]
unfolding incident_edges_def incident_sedges_def incident_loops_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {e \<in> E. incident v e} = {e \<in> E. incident v e \<and> card e = 2} \<union> {e \<in> E. incident v e \<and> card e = 1}
[PROOF STEP]
using alt_edge_size
[PROOF STATE]
proof (prove)
using this:
?e \<in> E \<Longrightarrow> card ?e = 1 \<or> card ?e = 2

goal (1 subgoal):
 1. {e \<in> E. incident v e} = {e \<in> E. incident v e \<and> card e = 2} \<union> {e \<in> E. incident v e \<and> card e = 1}
[PROOF STEP]
by auto


[STATEMENT]
lemma incident_edges_sedges[simp]: "\<not> has_loop v \<Longrightarrow> incident_edges v = incident_sedges v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> has_loop v \<Longrightarrow> incident_edges v = incident_sedges v
[PROOF STEP]
using incident_edges_union incident_loops_simp
[PROOF STATE]
proof (prove)
using this:
incident_edges ?v = incident_sedges ?v \<union> incident_loops ?v
has_loop ?v \<Longrightarrow> incident_loops ?v = {{?v}}
\<not> has_loop ?v \<Longrightarrow> incident_loops ?v = {}

goal (1 subgoal):
 1. \<not> has_loop v \<Longrightarrow> incident_edges v = incident_sedges v
[PROOF STEP]
by auto


[STATEMENT]
lemma incident_sedges_union: "\<Union> (incident_sedges ` V) = {e \<in> E . is_sedge e}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (incident_sedges ` V) = {e \<in> E. is_sedge e}
[PROOF STEP]
proof (intro subset_antisym subsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> \<Union> (incident_sedges ` V) \<Longrightarrow> x \<in> {e \<in> E. is_sedge e}
 2. \<And>x. x \<in> {e \<in> E. is_sedge e} \<Longrightarrow> x \<in> \<Union> (incident_sedges ` V)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> \<Union> (incident_sedges ` V) \<Longrightarrow> x \<in> {e \<in> E. is_sedge e}
 2. \<And>x. x \<in> {e \<in> E. is_sedge e} \<Longrightarrow> x \<in> \<Union> (incident_sedges ` V)
[PROOF STEP]
assume "x \<in> \<Union> (incident_sedges ` V)"
[PROOF STATE]
proof (state)
this:
x \<in> \<Union> (incident_sedges ` V)

goal (2 subgoals):
 1. \<And>x. x \<in> \<Union> (incident_sedges ` V) \<Longrightarrow> x \<in> {e \<in> E. is_sedge e}
 2. \<And>x. x \<in> {e \<in> E. is_sedge e} \<Longrightarrow> x \<in> \<Union> (incident_sedges ` V)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> \<Union> (incident_sedges ` V)
[PROOF STEP]
obtain v where "x \<in> incident_sedges v"
[PROOF STATE]
proof (prove)
using this:
x \<in> \<Union> (incident_sedges ` V)

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

goal (2 subgoals):
 1. \<And>x. x \<in> \<Union> (incident_sedges ` V) \<Longrightarrow> x \<in> {e \<in> E. is_sedge e}
 2. \<And>x. x \<in> {e \<in> E. is_sedge e} \<Longrightarrow> x \<in> \<Union> (incident_sedges ` V)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> incident_sedges v
[PROOF STEP]
show "x \<in> {e \<in> E. is_sedge e}"
[PROOF STATE]
proof (prove)
using this:
x \<in> incident_sedges v

goal (1 subgoal):
 1. x \<in> {e \<in> E. is_sedge e}
[PROOF STEP]
using incident_sedges_def is_sedge_def
[PROOF STATE]
proof (prove)
using this:
x \<in> incident_sedges v
incident_sedges ?v \<equiv> {e \<in> E. incident ?v e \<and> card e = 2}
is_sedge ?e \<equiv> card ?e = 2

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

goal (1 subgoal):
 1. \<And>x. x \<in> {e \<in> E. is_sedge e} \<Longrightarrow> x \<in> \<Union> (incident_sedges ` V)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {e \<in> E. is_sedge e} \<Longrightarrow> x \<in> \<Union> (incident_sedges ` V)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {e \<in> E. is_sedge e} \<Longrightarrow> x \<in> \<Union> (incident_sedges ` V)
[PROOF STEP]
assume "x \<in> {e \<in> E. is_sedge e}"
[PROOF STATE]
proof (state)
this:
x \<in> {e \<in> E. is_sedge e}

goal (1 subgoal):
 1. \<And>x. x \<in> {e \<in> E. is_sedge e} \<Longrightarrow> x \<in> \<Union> (incident_sedges ` V)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> {e \<in> E. is_sedge e}
[PROOF STEP]
have xin: "x \<in> E" and c2: "card x = 2"
[PROOF STATE]
proof (prove)
using this:
x \<in> {e \<in> E. is_sedge e}

goal (1 subgoal):
 1. x \<in> E &&& card x = 2
[PROOF STEP]
using is_sedge_def
[PROOF STATE]
proof (prove)
using this:
x \<in> {e \<in> E. is_sedge e}
is_sedge ?e \<equiv> card ?e = 2

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

goal (1 subgoal):
 1. \<And>x. x \<in> {e \<in> E. is_sedge e} \<Longrightarrow> x \<in> \<Union> (incident_sedges ` V)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> E
card x = 2
[PROOF STEP]
obtain v where "v \<in> x" and vin: "v \<in> V"
[PROOF STATE]
proof (prove)
using this:
x \<in> E
card x = 2

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<in> x; v \<in> V\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wellformed
[PROOF STATE]
proof (prove)
using this:
x \<in> E
card x = 2
?e \<in> E \<Longrightarrow> ?e \<subseteq> V

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<in> x; v \<in> V\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson card_2_iff' subsetD)
[PROOF STATE]
proof (state)
this:
v \<in> x
v \<in> V

goal (1 subgoal):
 1. \<And>x. x \<in> {e \<in> E. is_sedge e} \<Longrightarrow> x \<in> \<Union> (incident_sedges ` V)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> x
v \<in> V
[PROOF STEP]
have "x \<in> incident_sedges v"
[PROOF STATE]
proof (prove)
using this:
v \<in> x
v \<in> V

goal (1 subgoal):
 1. x \<in> incident_sedges v
[PROOF STEP]
unfolding incident_sedges_def incident_def
[PROOF STATE]
proof (prove)
using this:
v \<in> x
v \<in> V

goal (1 subgoal):
 1. x \<in> {e \<in> E. v \<in> e \<and> card e = 2}
[PROOF STEP]
using xin c2
[PROOF STATE]
proof (prove)
using this:
v \<in> x
v \<in> V
x \<in> E
card x = 2

goal (1 subgoal):
 1. x \<in> {e \<in> E. v \<in> e \<and> card e = 2}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> incident_sedges v

goal (1 subgoal):
 1. \<And>x. x \<in> {e \<in> E. is_sedge e} \<Longrightarrow> x \<in> \<Union> (incident_sedges ` V)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> incident_sedges v
[PROOF STEP]
show "x \<in> \<Union> (incident_sedges ` V)"
[PROOF STATE]
proof (prove)
using this:
x \<in> incident_sedges v

goal (1 subgoal):
 1. x \<in> \<Union> (incident_sedges ` V)
[PROOF STEP]
using vin
[PROOF STATE]
proof (prove)
using this:
x \<in> incident_sedges v
v \<in> V

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma empty_not_edge: "{} \<notin> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<notin> E
[PROOF STEP]
using edge_size
[PROOF STATE]
proof (prove)
using this:
?e \<in> E \<Longrightarrow> 0 < card ?e \<and> card ?e \<le> 2

goal (1 subgoal):
 1. {} \<notin> E
[PROOF STEP]
by fastforce


[STATEMENT]
lemma degree_no_loops[simp]: "\<not> has_loop v \<Longrightarrow> degree v = card (incident_edges v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> has_loop v \<Longrightarrow> degree v = card (incident_edges v)
[PROOF STEP]
using incident_edges_sedges degree_def incident_loops_simp(2)
[PROOF STATE]
proof (prove)
using this:
\<not> has_loop ?v \<Longrightarrow> incident_edges ?v = incident_sedges ?v
degree ?v \<equiv> card (incident_sedges ?v) + 2 * card (incident_loops ?v)
\<not> has_loop ?v \<Longrightarrow> incident_loops ?v = {}

goal (1 subgoal):
 1. \<not> has_loop v \<Longrightarrow> degree v = card (incident_edges v)
[PROOF STEP]
by auto


[STATEMENT]
lemma degree_none[simp]: "\<not> v  \<in> V \<Longrightarrow> degree v = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<notin> V \<Longrightarrow> degree v = 0
[PROOF STEP]
using degree_def degree_no_loops has_loop_in_verts incident_edges_sedges incident_sedges_empty
[PROOF STATE]
proof (prove)
using this:
degree ?v \<equiv> card (incident_sedges ?v) + 2 * card (incident_loops ?v)
\<not> has_loop ?v \<Longrightarrow> degree ?v = card (incident_edges ?v)
has_loop ?v \<Longrightarrow> ?v \<in> V
\<not> has_loop ?v \<Longrightarrow> incident_edges ?v = incident_sedges ?v
?v \<notin> V \<Longrightarrow> incident_sedges ?v = {}

goal (1 subgoal):
 1. v \<notin> V \<Longrightarrow> degree v = 0
[PROOF STEP]
by auto


[STATEMENT]
lemma degree0_inc_edges_empt_iff:
  assumes "finite E"
  shows "degree v = 0 \<longleftrightarrow> incident_edges v = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (degree v = 0) = (incident_edges v = {})
[PROOF STEP]
proof (intro iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. degree v = 0 \<Longrightarrow> incident_edges v = {}
 2. incident_edges v = {} \<Longrightarrow> degree v = 0
[PROOF STEP]
assume "degree v = 0"
[PROOF STATE]
proof (state)
this:
degree v = 0

goal (2 subgoals):
 1. degree v = 0 \<Longrightarrow> incident_edges v = {}
 2. incident_edges v = {} \<Longrightarrow> degree v = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
degree v = 0
[PROOF STEP]
have "card (incident_sedges v) + 2 * (card (incident_loops v)) = 0"
[PROOF STATE]
proof (prove)
using this:
degree v = 0

goal (1 subgoal):
 1. card (incident_sedges v) + 2 * card (incident_loops v) = 0
[PROOF STEP]
using degree_def
[PROOF STATE]
proof (prove)
using this:
degree v = 0
degree ?v \<equiv> card (incident_sedges ?v) + 2 * card (incident_loops ?v)

goal (1 subgoal):
 1. card (incident_sedges v) + 2 * card (incident_loops v) = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card (incident_sedges v) + 2 * card (incident_loops v) = 0

goal (2 subgoals):
 1. degree v = 0 \<Longrightarrow> incident_edges v = {}
 2. incident_edges v = {} \<Longrightarrow> degree v = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card (incident_sedges v) + 2 * card (incident_loops v) = 0
[PROOF STEP]
have "incident_sedges v = {}" and "incident_loops v = {}"
[PROOF STATE]
proof (prove)
using this:
card (incident_sedges v) + 2 * card (incident_loops v) = 0

goal (1 subgoal):
 1. incident_sedges v = {} &&& incident_loops v = {}
[PROOF STEP]
using degree_def incident_edges_union assms finite_incident_edges finite_incident_loops
[PROOF STATE]
proof (prove)
using this:
card (incident_sedges v) + 2 * card (incident_loops v) = 0
degree ?v \<equiv> card (incident_sedges ?v) + 2 * card (incident_loops ?v)
incident_edges ?v = incident_sedges ?v \<union> incident_loops ?v
finite E
finite E \<Longrightarrow> finite (incident_edges ?v)
finite (incident_loops ?v)

goal (1 subgoal):
 1. incident_sedges v = {} &&& incident_loops v = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
incident_sedges v = {}
incident_loops v = {}

goal (2 subgoals):
 1. degree v = 0 \<Longrightarrow> incident_edges v = {}
 2. incident_edges v = {} \<Longrightarrow> degree v = 0
[PROOF STEP]
thus "incident_edges v = {}"
[PROOF STATE]
proof (prove)
using this:
incident_sedges v = {}
incident_loops v = {}

goal (1 subgoal):
 1. incident_edges v = {}
[PROOF STEP]
using incident_edges_union
[PROOF STATE]
proof (prove)
using this:
incident_sedges v = {}
incident_loops v = {}
incident_edges ?v = incident_sedges ?v \<union> incident_loops ?v

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

goal (1 subgoal):
 1. incident_edges v = {} \<Longrightarrow> degree v = 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. incident_edges v = {} \<Longrightarrow> degree v = 0
[PROOF STEP]
show "incident_edges v = {} \<Longrightarrow> degree v = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. incident_edges v = {} \<Longrightarrow> degree v = 0
[PROOF STEP]
using incident_edges_union degree_def
[PROOF STATE]
proof (prove)
using this:
incident_edges ?v = incident_sedges ?v \<union> incident_loops ?v
degree ?v \<equiv> card (incident_sedges ?v) + 2 * card (incident_loops ?v)

goal (1 subgoal):
 1. incident_edges v = {} \<Longrightarrow> degree v = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
incident_edges v = {} \<Longrightarrow> degree v = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma incident_edges_neighbors_img: "incident_edges v = (\<lambda> u . {v, u}) ` (neighborhood v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. incident_edges v = (\<lambda>u. {v, u}) ` neighborhood v
[PROOF STEP]
proof (intro subset_antisym subsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> incident_edges v \<Longrightarrow> x \<in> (\<lambda>u. {v, u}) ` neighborhood v
 2. \<And>x. x \<in> (\<lambda>u. {v, u}) ` neighborhood v \<Longrightarrow> x \<in> incident_edges v
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> incident_edges v \<Longrightarrow> x \<in> (\<lambda>u. {v, u}) ` neighborhood v
 2. \<And>x. x \<in> (\<lambda>u. {v, u}) ` neighborhood v \<Longrightarrow> x \<in> incident_edges v
[PROOF STEP]
assume a: "x \<in> incident_edges v"
[PROOF STATE]
proof (state)
this:
x \<in> incident_edges v

goal (2 subgoals):
 1. \<And>x. x \<in> incident_edges v \<Longrightarrow> x \<in> (\<lambda>u. {v, u}) ` neighborhood v
 2. \<And>x. x \<in> (\<lambda>u. {v, u}) ` neighborhood v \<Longrightarrow> x \<in> incident_edges v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> incident_edges v
[PROOF STEP]
have xE: "x \<in> E" and vx: "v \<in> x"
[PROOF STATE]
proof (prove)
using this:
x \<in> incident_edges v

goal (1 subgoal):
 1. x \<in> E &&& v \<in> x
[PROOF STEP]
using incident_edges_def incident_def
[PROOF STATE]
proof (prove)
using this:
x \<in> incident_edges v
incident_edges ?v \<equiv> {e \<in> E. incident ?v e}
incident ?v ?e \<equiv> ?v \<in> ?e

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

goal (2 subgoals):
 1. \<And>x. x \<in> incident_edges v \<Longrightarrow> x \<in> (\<lambda>u. {v, u}) ` neighborhood v
 2. \<And>x. x \<in> (\<lambda>u. {v, u}) ` neighborhood v \<Longrightarrow> x \<in> incident_edges v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> E
v \<in> x
[PROOF STEP]
obtain u where "x = {u, v}"
[PROOF STATE]
proof (prove)
using this:
x \<in> E
v \<in> x

goal (1 subgoal):
 1. (\<And>u. x = {u, v} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using alt_edge_size
[PROOF STATE]
proof (prove)
using this:
x \<in> E
v \<in> x
?e \<in> E \<Longrightarrow> card ?e = 1 \<or> card ?e = 2

goal (1 subgoal):
 1. (\<And>u. x = {u, v} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (smt (verit, best) card_1_singletonE card_2_iff insertE insert_absorb2 insert_commute singletonD)
[PROOF STATE]
proof (state)
this:
x = {u, v}

goal (2 subgoals):
 1. \<And>x. x \<in> incident_edges v \<Longrightarrow> x \<in> (\<lambda>u. {v, u}) ` neighborhood v
 2. \<And>x. x \<in> (\<lambda>u. {v, u}) ` neighborhood v \<Longrightarrow> x \<in> incident_edges v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = {u, v}
[PROOF STEP]
have "u \<in> neighborhood v"
[PROOF STATE]
proof (prove)
using this:
x = {u, v}

goal (1 subgoal):
 1. u \<in> neighborhood v
[PROOF STEP]
using a neighborhood_incident
[PROOF STATE]
proof (prove)
using this:
x = {u, v}
x \<in> incident_edges v
(?u \<in> neighborhood ?v) = ({?u, ?v} \<in> incident_edges ?v)

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

goal (2 subgoals):
 1. \<And>x. x \<in> incident_edges v \<Longrightarrow> x \<in> (\<lambda>u. {v, u}) ` neighborhood v
 2. \<And>x. x \<in> (\<lambda>u. {v, u}) ` neighborhood v \<Longrightarrow> x \<in> incident_edges v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u \<in> neighborhood v
[PROOF STEP]
show "x \<in> (\<lambda>u. {v, u}) ` neighborhood v"
[PROOF STATE]
proof (prove)
using this:
u \<in> neighborhood v

goal (1 subgoal):
 1. x \<in> (\<lambda>u. {v, u}) ` neighborhood v
[PROOF STEP]
using \<open>x = {u, v}\<close>
[PROOF STATE]
proof (prove)
using this:
u \<in> neighborhood v
x = {u, v}

goal (1 subgoal):
 1. x \<in> (\<lambda>u. {v, u}) ` neighborhood v
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> (\<lambda>u. {v, u}) ` neighborhood v

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>u. {v, u}) ` neighborhood v \<Longrightarrow> x \<in> incident_edges v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>u. {v, u}) ` neighborhood v \<Longrightarrow> x \<in> incident_edges v
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>u. {v, u}) ` neighborhood v \<Longrightarrow> x \<in> incident_edges v
[PROOF STEP]
assume "x \<in> (\<lambda>u. {v, u}) ` neighborhood v"
[PROOF STATE]
proof (state)
this:
x \<in> (\<lambda>u. {v, u}) ` neighborhood v

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>u. {v, u}) ` neighborhood v \<Longrightarrow> x \<in> incident_edges v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> (\<lambda>u. {v, u}) ` neighborhood v
[PROOF STEP]
obtain u' where "x = {v, u'}" and "u' \<in> neighborhood v"
[PROOF STATE]
proof (prove)
using this:
x \<in> (\<lambda>u. {v, u}) ` neighborhood v

goal (1 subgoal):
 1. (\<And>u'. \<lbrakk>x = {v, u'}; u' \<in> neighborhood v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x = {v, u'}
u' \<in> neighborhood v

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>u. {v, u}) ` neighborhood v \<Longrightarrow> x \<in> incident_edges v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = {v, u'}
u' \<in> neighborhood v
[PROOF STEP]
show "x \<in> incident_edges v"
[PROOF STATE]
proof (prove)
using this:
x = {v, u'}
u' \<in> neighborhood v

goal (1 subgoal):
 1. x \<in> incident_edges v
[PROOF STEP]
by (simp add: insert_commute neighborhood_incident)
[PROOF STATE]
proof (state)
this:
x \<in> incident_edges v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma card_incident_sedges_neighborhood: "card (incident_edges v) = card (neighborhood v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (incident_edges v) = card (neighborhood v)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (incident_edges v) = card (neighborhood v)
[PROOF STEP]
have "bij_betw (\<lambda> u . {v, u}) (neighborhood v) (incident_edges v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (\<lambda>u. {v, u}) (neighborhood v) (incident_edges v)
[PROOF STEP]
by(intro bij_betw_imageI inj_onI, simp_all add:incident_edges_neighbors_img)(metis doubleton_eq_iff)
[PROOF STATE]
proof (state)
this:
bij_betw (\<lambda>u. {v, u}) (neighborhood v) (incident_edges v)

goal (1 subgoal):
 1. card (incident_edges v) = card (neighborhood v)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
bij_betw (\<lambda>u. {v, u}) (neighborhood v) (incident_edges v)

goal (1 subgoal):
 1. card (incident_edges v) = card (neighborhood v)
[PROOF STEP]
by (metis bij_betw_same_card)
[PROOF STATE]
proof (state)
this:
card (incident_edges v) = card (neighborhood v)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma degree0_neighborhood_empt_iff:
  assumes "finite E"
  shows "degree v = 0 \<longleftrightarrow> neighborhood v = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (degree v = 0) = (neighborhood v = {})
[PROOF STEP]
using degree0_inc_edges_empt_iff incident_edges_neighbors_img
[PROOF STATE]
proof (prove)
using this:
finite E \<Longrightarrow> (degree ?v = 0) = (incident_edges ?v = {})
incident_edges ?v = (\<lambda>u. {?v, u}) ` neighborhood ?v

goal (1 subgoal):
 1. (degree v = 0) = (neighborhood v = {})
[PROOF STEP]
by (simp add: assms)


[STATEMENT]
lemma is_isolated_vertex_edge: "is_isolated_vertex v \<Longrightarrow> (\<And> e. e \<in> E \<Longrightarrow> \<not> (incident v e))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_isolated_vertex v \<Longrightarrow> (\<And>e. e \<in> E \<Longrightarrow> \<not> incident v e)
[PROOF STEP]
unfolding is_isolated_vertex_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> V \<and> (\<forall>u\<in>V. \<not> vert_adj u v) \<Longrightarrow> (\<And>e. e \<in> E \<Longrightarrow> \<not> incident v e)
[PROOF STEP]
by (metis (full_types) all_not_in_conv incident_def insert_absorb insert_iff mk_disjoint_insert
      vert_adj_def vert_adj_edge_iff2 vert_adj_imp_inV)


[STATEMENT]
lemma is_isolated_vertex_no_loop: "is_isolated_vertex v \<Longrightarrow> \<not> has_loop v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_isolated_vertex v \<Longrightarrow> \<not> has_loop v
[PROOF STEP]
unfolding has_loop_def is_isolated_vertex_def vert_adj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> V \<and> (\<forall>u\<in>V. {u, v} \<notin> E) \<Longrightarrow> {v} \<notin> E
[PROOF STEP]
by auto


[STATEMENT]
lemma is_isolated_vertex_degree0: "is_isolated_vertex v \<Longrightarrow> degree v = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_isolated_vertex v \<Longrightarrow> degree v = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_isolated_vertex v \<Longrightarrow> degree v = 0
[PROOF STEP]
assume assm: "is_isolated_vertex v"
[PROOF STATE]
proof (state)
this:
is_isolated_vertex v

goal (1 subgoal):
 1. is_isolated_vertex v \<Longrightarrow> degree v = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_isolated_vertex v
[PROOF STEP]
have "\<not> has_loop v"
[PROOF STATE]
proof (prove)
using this:
is_isolated_vertex v

goal (1 subgoal):
 1. \<not> has_loop v
[PROOF STEP]
using is_isolated_vertex_no_loop
[PROOF STATE]
proof (prove)
using this:
is_isolated_vertex v
is_isolated_vertex ?v \<Longrightarrow> \<not> has_loop ?v

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

goal (1 subgoal):
 1. is_isolated_vertex v \<Longrightarrow> degree v = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> has_loop v
[PROOF STEP]
have "degree v = card (incident_edges v)"
[PROOF STATE]
proof (prove)
using this:
\<not> has_loop v

goal (1 subgoal):
 1. degree v = card (incident_edges v)
[PROOF STEP]
using degree_no_loops
[PROOF STATE]
proof (prove)
using this:
\<not> has_loop v
\<not> has_loop ?v \<Longrightarrow> degree ?v = card (incident_edges ?v)

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

goal (1 subgoal):
 1. is_isolated_vertex v \<Longrightarrow> degree v = 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
degree v = card (incident_edges v)

goal (1 subgoal):
 1. is_isolated_vertex v \<Longrightarrow> degree v = 0
[PROOF STEP]
have "\<And> e. e \<in> E \<Longrightarrow> \<not> (incident v e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e. e \<in> E \<Longrightarrow> \<not> incident v e
[PROOF STEP]
using is_isolated_vertex_edge assm
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_isolated_vertex ?v; ?e \<in> E\<rbrakk> \<Longrightarrow> \<not> incident ?v ?e
is_isolated_vertex v

goal (1 subgoal):
 1. \<And>e. e \<in> E \<Longrightarrow> \<not> incident v e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?e \<in> E \<Longrightarrow> \<not> incident v ?e

goal (1 subgoal):
 1. is_isolated_vertex v \<Longrightarrow> degree v = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?e \<in> E \<Longrightarrow> \<not> incident v ?e
[PROOF STEP]
have "(incident_edges v) = {}"
[PROOF STATE]
proof (prove)
using this:
?e \<in> E \<Longrightarrow> \<not> incident v ?e

goal (1 subgoal):
 1. incident_edges v = {}
[PROOF STEP]
unfolding incident_edges_def
[PROOF STATE]
proof (prove)
using this:
?e \<in> E \<Longrightarrow> \<not> incident v ?e

goal (1 subgoal):
 1. {e \<in> E. incident v e} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
incident_edges v = {}

goal (1 subgoal):
 1. is_isolated_vertex v \<Longrightarrow> degree v = 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
degree v = card (incident_edges v)
incident_edges v = {}
[PROOF STEP]
show "degree v = 0"
[PROOF STATE]
proof (prove)
using this:
degree v = card (incident_edges v)
incident_edges v = {}

goal (1 subgoal):
 1. degree v = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
degree v = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iso_vertex_empty_neighborhood: "is_isolated_vertex v \<Longrightarrow> neighborhood v = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_isolated_vertex v \<Longrightarrow> neighborhood v = {}
[PROOF STEP]
using is_isolated_vertex_def neighborhood_def
[PROOF STATE]
proof (prove)
using this:
is_isolated_vertex ?v \<equiv> ?v \<in> V \<and> (\<forall>u\<in>V. \<not> vert_adj u ?v)
neighborhood ?x \<equiv> {v \<in> V. vert_adj ?x v}

goal (1 subgoal):
 1. is_isolated_vertex v \<Longrightarrow> neighborhood v = {}
[PROOF STEP]
by (metis (mono_tags, lifting) Collect_empty_eq is_isolated_vertex_edge vert_adj_inc_edge_iff)


[STATEMENT]
lemma all_edges_betw_D3: "(x, y) \<in> all_edges_between X Y \<Longrightarrow> {x, y} \<in> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> all_edges_between X Y \<Longrightarrow> {x, y} \<in> E
[PROOF STEP]
by (simp add: all_edges_between_def)


[STATEMENT]
lemma all_edges_betw_I: "x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> {x, y} \<in> E \<Longrightarrow> (x, y) \<in> all_edges_between X Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> X; y \<in> Y; {x, y} \<in> E\<rbrakk> \<Longrightarrow> (x, y) \<in> all_edges_between X Y
[PROOF STEP]
by (simp add: all_edges_between_def)


[STATEMENT]
lemma all_edges_between_subset: "all_edges_between X Y \<subseteq> X\<times>Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_edges_between X Y \<subseteq> X \<times> Y
[PROOF STEP]
by (auto simp: all_edges_between_def)


[STATEMENT]
lemma all_edges_between_E_ss: "mk_edge ` all_edges_between X Y \<subseteq> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_edge ` all_edges_between X Y \<subseteq> E
[PROOF STEP]
by (auto simp add: all_edges_between_def)


[STATEMENT]
lemma all_edges_between_rem_wf: "all_edges_between X Y = all_edges_between (X \<inter> V) (Y \<inter> V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_edges_between X Y = all_edges_between (X \<inter> V) (Y \<inter> V)
[PROOF STEP]
using wellformed
[PROOF STATE]
proof (prove)
using this:
?e \<in> E \<Longrightarrow> ?e \<subseteq> V

goal (1 subgoal):
 1. all_edges_between X Y = all_edges_between (X \<inter> V) (Y \<inter> V)
[PROOF STEP]
by (simp add: all_edges_between_def) blast


[STATEMENT]
lemma all_edges_between_empty [simp]:
  "all_edges_between {} Z = {}" "all_edges_between Z {} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_edges_between {} Z = {} &&& all_edges_between Z {} = {}
[PROOF STEP]
by (auto simp: all_edges_between_def)


[STATEMENT]
lemma all_edges_between_disjnt1: "disjnt X Y \<Longrightarrow> disjnt (all_edges_between X Z) (all_edges_between Y Z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. disjnt X Y \<Longrightarrow> disjnt (all_edges_between X Z) (all_edges_between Y Z)
[PROOF STEP]
by (auto simp: all_edges_between_def disjnt_iff)


[STATEMENT]
lemma all_edges_between_disjnt2: "disjnt Y Z \<Longrightarrow> disjnt (all_edges_between X Y) (all_edges_between X Z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. disjnt Y Z \<Longrightarrow> disjnt (all_edges_between X Y) (all_edges_between X Z)
[PROOF STEP]
by (auto simp: all_edges_between_def disjnt_iff)