[STATEMENT]
lemma (in valid_unMultigraph) adjacent_finite:
  "finite E \<Longrightarrow> finite {n. adjacent v n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite E \<Longrightarrow> finite {n. adjacent v n}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite E \<Longrightarrow> finite {n. adjacent v n}
[PROOF STEP]
assume "finite E"
[PROOF STATE]
proof (state)
this:
finite E

goal (1 subgoal):
 1. finite E \<Longrightarrow> finite {n. adjacent v n}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
finite E

goal (1 subgoal):
 1. finite E \<Longrightarrow> finite {n. adjacent v n}
[PROOF STEP]
fix S v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite E \<Longrightarrow> finite {n. adjacent v n}
[PROOF STEP]
have "finite S \<Longrightarrow> finite {n. \<exists>w. (v,w,n)\<in>S}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite S \<Longrightarrow> finite {n. \<exists>w. (v, w, n) \<in> S}
[PROOF STEP]
proof (induct S rule: finite_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite {n. \<exists>w. (v, w, n) \<in> {}}
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; finite {n. \<exists>w. (v, w, n) \<in> F}\<rbrakk> \<Longrightarrow> finite {n. \<exists>w. (v, w, n) \<in> insert x F}
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. finite {n. \<exists>w. (v, w, n) \<in> {}}
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; finite {n. \<exists>w. (v, w, n) \<in> F}\<rbrakk> \<Longrightarrow> finite {n. \<exists>w. (v, w, n) \<in> insert x F}
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {n. \<exists>w. (v, w, n) \<in> {}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {n. \<exists>w. (v, w, n) \<in> {}}

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

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; finite {n. \<exists>w. (v, w, n) \<in> F}\<rbrakk> \<Longrightarrow> finite {n. \<exists>w. (v, w, n) \<in> insert x F}
[PROOF STEP]
obtain x1 x2 x3 where x: "x=(x1,x2,x3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x1 x2 x3. x = (x1, x2, x3) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod_cases3)
[PROOF STATE]
proof (state)
this:
x = (x1, x2, x3)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; finite {n. \<exists>w. (v, w, n) \<in> F}\<rbrakk> \<Longrightarrow> finite {n. \<exists>w. (v, w, n) \<in> insert x F}
[PROOF STEP]
have "x1=v \<Longrightarrow> ?case"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1 = v \<Longrightarrow> finite {n. \<exists>w. (v, w, n) \<in> insert x F}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x1 = v \<Longrightarrow> finite {n. \<exists>w. (v, w, n) \<in> insert x F}
[PROOF STEP]
assume "x1=v"
[PROOF STATE]
proof (state)
this:
x1 = v

goal (1 subgoal):
 1. x1 = v \<Longrightarrow> finite {n. \<exists>w. (v, w, n) \<in> insert x F}
[PROOF STEP]
hence "{n. \<exists>w. (v, w, n) \<in> insert x F}=insert x3 {n. \<exists>w. (v, w, n) \<in> F}"
[PROOF STATE]
proof (prove)
using this:
x1 = v

goal (1 subgoal):
 1. {n. \<exists>w. (v, w, n) \<in> insert x F} = insert x3 {n. \<exists>w. (v, w, n) \<in> F}
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
x1 = v
x = (x1, x2, x3)

goal (1 subgoal):
 1. {n. \<exists>w. (v, w, n) \<in> insert x F} = insert x3 {n. \<exists>w. (v, w, n) \<in> F}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{n. \<exists>w. (v, w, n) \<in> insert x F} = insert x3 {n. \<exists>w. (v, w, n) \<in> F}

goal (1 subgoal):
 1. x1 = v \<Longrightarrow> finite {n. \<exists>w. (v, w, n) \<in> insert x F}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{n. \<exists>w. (v, w, n) \<in> insert x F} = insert x3 {n. \<exists>w. (v, w, n) \<in> F}

goal (1 subgoal):
 1. finite {n. \<exists>w. (v, w, n) \<in> insert x F}
[PROOF STEP]
using insert
[PROOF STATE]
proof (prove)
using this:
{n. \<exists>w. (v, w, n) \<in> insert x F} = insert x3 {n. \<exists>w. (v, w, n) \<in> F}
finite F
x \<notin> F
finite {n. \<exists>w. (v, w, n) \<in> F}

goal (1 subgoal):
 1. finite {n. \<exists>w. (v, w, n) \<in> insert x F}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {n. \<exists>w. (v, w, n) \<in> insert x F}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x1 = v \<Longrightarrow> finite {n. \<exists>w. (v, w, n) \<in> insert x F}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; finite {n. \<exists>w. (v, w, n) \<in> F}\<rbrakk> \<Longrightarrow> finite {n. \<exists>w. (v, w, n) \<in> insert x F}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x1 = v \<Longrightarrow> finite {n. \<exists>w. (v, w, n) \<in> insert x F}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; finite {n. \<exists>w. (v, w, n) \<in> F}\<rbrakk> \<Longrightarrow> finite {n. \<exists>w. (v, w, n) \<in> insert x F}
[PROOF STEP]
have "x1\<noteq>v \<Longrightarrow> ?case"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1 \<noteq> v \<Longrightarrow> finite {n. \<exists>w. (v, w, n) \<in> insert x F}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x1 \<noteq> v \<Longrightarrow> finite {n. \<exists>w. (v, w, n) \<in> insert x F}
[PROOF STEP]
assume "x1\<noteq>v"
[PROOF STATE]
proof (state)
this:
x1 \<noteq> v

goal (1 subgoal):
 1. x1 \<noteq> v \<Longrightarrow> finite {n. \<exists>w. (v, w, n) \<in> insert x F}
[PROOF STEP]
hence "{n. \<exists>w. (v, w, n) \<in> insert x F}={n. \<exists>w. (v, w, n) \<in> F}"
[PROOF STATE]
proof (prove)
using this:
x1 \<noteq> v

goal (1 subgoal):
 1. {n. \<exists>w. (v, w, n) \<in> insert x F} = {n. \<exists>w. (v, w, n) \<in> F}
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
x1 \<noteq> v
x = (x1, x2, x3)

goal (1 subgoal):
 1. {n. \<exists>w. (v, w, n) \<in> insert x F} = {n. \<exists>w. (v, w, n) \<in> F}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{n. \<exists>w. (v, w, n) \<in> insert x F} = {n. \<exists>w. (v, w, n) \<in> F}

goal (1 subgoal):
 1. x1 \<noteq> v \<Longrightarrow> finite {n. \<exists>w. (v, w, n) \<in> insert x F}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{n. \<exists>w. (v, w, n) \<in> insert x F} = {n. \<exists>w. (v, w, n) \<in> F}

goal (1 subgoal):
 1. finite {n. \<exists>w. (v, w, n) \<in> insert x F}
[PROOF STEP]
using insert
[PROOF STATE]
proof (prove)
using this:
{n. \<exists>w. (v, w, n) \<in> insert x F} = {n. \<exists>w. (v, w, n) \<in> F}
finite F
x \<notin> F
finite {n. \<exists>w. (v, w, n) \<in> F}

goal (1 subgoal):
 1. finite {n. \<exists>w. (v, w, n) \<in> insert x F}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {n. \<exists>w. (v, w, n) \<in> insert x F}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x1 \<noteq> v \<Longrightarrow> finite {n. \<exists>w. (v, w, n) \<in> insert x F}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; finite {n. \<exists>w. (v, w, n) \<in> F}\<rbrakk> \<Longrightarrow> finite {n. \<exists>w. (v, w, n) \<in> insert x F}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x1 = v \<Longrightarrow> finite {n. \<exists>w. (v, w, n) \<in> insert x F}
x1 \<noteq> v \<Longrightarrow> finite {n. \<exists>w. (v, w, n) \<in> insert x F}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x1 = v \<Longrightarrow> finite {n. \<exists>w. (v, w, n) \<in> insert x F}
x1 \<noteq> v \<Longrightarrow> finite {n. \<exists>w. (v, w, n) \<in> insert x F}

goal (1 subgoal):
 1. finite {n. \<exists>w. (v, w, n) \<in> insert x F}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {n. \<exists>w. (v, w, n) \<in> insert x F}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite S \<Longrightarrow> finite {n. \<exists>w. (v, w, n) \<in> S}

goal (1 subgoal):
 1. finite E \<Longrightarrow> finite {n. adjacent v n}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
finite ?S2 \<Longrightarrow> finite {n. \<exists>w. (?va2, w, n) \<in> ?S2}

goal (1 subgoal):
 1. finite E \<Longrightarrow> finite {n. adjacent v n}
[PROOF STEP]
note aux=this
[PROOF STATE]
proof (state)
this:
finite ?S2 \<Longrightarrow> finite {n. \<exists>w. (?va2, w, n) \<in> ?S2}

goal (1 subgoal):
 1. finite E \<Longrightarrow> finite {n. adjacent v n}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {n. adjacent v n}
[PROOF STEP]
using aux[OF \<open>finite E\<close>, of v]
[PROOF STATE]
proof (prove)
using this:
finite {n. \<exists>w. (v, w, n) \<in> E}

goal (1 subgoal):
 1. finite {n. adjacent v n}
[PROOF STEP]
unfolding adjacent_def
[PROOF STATE]
proof (prove)
using this:
finite {n. \<exists>w. (v, w, n) \<in> E}

goal (1 subgoal):
 1. finite {n. \<exists>w. (v, w, n) \<in> E}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {n. adjacent v n}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in valid_unSimpGraph) finV_to_finE[simp]:
  assumes "finite V"
  shows "finite E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite E
[PROOF STEP]
proof (cases "{(v1,v2). adjacent v1 v2}={}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {(x, y). adjacent x y} = {} \<Longrightarrow> finite E
 2. {(x, y). adjacent x y} \<noteq> {} \<Longrightarrow> finite E
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
{(x, y). adjacent x y} = {}

goal (2 subgoals):
 1. {(x, y). adjacent x y} = {} \<Longrightarrow> finite E
 2. {(x, y). adjacent x y} \<noteq> {} \<Longrightarrow> finite E
[PROOF STEP]
hence "E={}"
[PROOF STATE]
proof (prove)
using this:
{(x, y). adjacent x y} = {}

goal (1 subgoal):
 1. E = {}
[PROOF STEP]
unfolding adjacent_def
[PROOF STATE]
proof (prove)
using this:
{(v1, v2). \<exists>w. (v1, w, v2) \<in> E} = {}

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

goal (2 subgoals):
 1. {(x, y). adjacent x y} = {} \<Longrightarrow> finite E
 2. {(x, y). adjacent x y} \<noteq> {} \<Longrightarrow> finite E
[PROOF STEP]
thus "finite E"
[PROOF STATE]
proof (prove)
using this:
E = {}

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

goal (1 subgoal):
 1. {(x, y). adjacent x y} \<noteq> {} \<Longrightarrow> finite E
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {(x, y). adjacent x y} \<noteq> {} \<Longrightarrow> finite E
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
{(x, y). adjacent x y} \<noteq> {}

goal (1 subgoal):
 1. {(x, y). adjacent x y} \<noteq> {} \<Longrightarrow> finite E
[PROOF STEP]
have "{(v1,v2). adjacent v1 v2} \<subseteq> V \<times> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(x, y). adjacent x y} \<subseteq> V \<times> V
[PROOF STEP]
using adjacent_V
[PROOF STATE]
proof (prove)
using this:
adjacent ?v ?v' \<Longrightarrow> ?v \<in> V
adjacent ?v ?v' \<Longrightarrow> ?v' \<in> V

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

goal (1 subgoal):
 1. {(x, y). adjacent x y} \<noteq> {} \<Longrightarrow> finite E
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{(x, y). adjacent x y} \<subseteq> V \<times> V

goal (1 subgoal):
 1. {(x, y). adjacent x y} \<noteq> {} \<Longrightarrow> finite E
[PROOF STEP]
have "finite (V \<times> V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (V \<times> V)
[PROOF STEP]
using \<open>finite V\<close>
[PROOF STATE]
proof (prove)
using this:
finite V

goal (1 subgoal):
 1. finite (V \<times> V)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (V \<times> V)

goal (1 subgoal):
 1. {(x, y). adjacent x y} \<noteq> {} \<Longrightarrow> finite E
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{(x, y). adjacent x y} \<subseteq> V \<times> V
finite (V \<times> V)
[PROOF STEP]
have "finite {(v1,v2). adjacent v1 v2}"
[PROOF STATE]
proof (prove)
using this:
{(x, y). adjacent x y} \<subseteq> V \<times> V
finite (V \<times> V)

goal (1 subgoal):
 1. finite {(x, y). adjacent x y}
[PROOF STEP]
using finite_subset
[PROOF STATE]
proof (prove)
using this:
{(x, y). adjacent x y} \<subseteq> V \<times> V
finite (V \<times> V)
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. finite {(x, y). adjacent x y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {(x, y). adjacent x y}

goal (1 subgoal):
 1. {(x, y). adjacent x y} \<noteq> {} \<Longrightarrow> finite E
[PROOF STEP]
hence "card {(v1,v2). adjacent v1 v2}\<noteq>0"
[PROOF STATE]
proof (prove)
using this:
finite {(x, y). adjacent x y}

goal (1 subgoal):
 1. card {(x, y). adjacent x y} \<noteq> 0
[PROOF STEP]
using False card_eq_0_iff
[PROOF STATE]
proof (prove)
using this:
finite {(x, y). adjacent x y}
{(x, y). adjacent x y} \<noteq> {}
(card ?A = 0) = (?A = {} \<or> infinite ?A)

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

goal (1 subgoal):
 1. {(x, y). adjacent x y} \<noteq> {} \<Longrightarrow> finite E
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card {(x, y). adjacent x y} \<noteq> 0

goal (1 subgoal):
 1. {(x, y). adjacent x y} \<noteq> {} \<Longrightarrow> finite E
[PROOF STEP]
have "card E=card {(v1,v2). adjacent v1 v2}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card E = card {(x, y). adjacent x y}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card E = card {(x, y). adjacent x y}
[PROOF STEP]
have "(\<lambda>(v1,w,v2). (v1,v2))`E = {(v1,v2). adjacent v1 v2}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>(v1, w, v2). (v1, v2)) ` E = {(x, y). adjacent x y}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>(v1, w, v2). (v1, v2)) ` E = {(x, y). adjacent x y}
[PROOF STEP]
have "\<And>x. x\<in>(\<lambda>(v1,w,v2). (v1,v2))`E \<Longrightarrow> x\<in> {(v1,v2). adjacent v1 v2}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>(v1, w, v2). (v1, v2)) ` E \<Longrightarrow> x \<in> {(x, y). adjacent x y}
[PROOF STEP]
unfolding adjacent_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>(v1, w, v2). (v1, v2)) ` E \<Longrightarrow> x \<in> {(v1, v2). \<exists>w. (v1, w, v2) \<in> E}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x \<in> (\<lambda>(v1, w, v2). (v1, v2)) ` E \<Longrightarrow> ?x \<in> {(x, y). adjacent x y}

goal (1 subgoal):
 1. (\<lambda>(v1, w, v2). (v1, v2)) ` E = {(x, y). adjacent x y}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?x \<in> (\<lambda>(v1, w, v2). (v1, v2)) ` E \<Longrightarrow> ?x \<in> {(x, y). adjacent x y}

goal (1 subgoal):
 1. (\<lambda>(v1, w, v2). (v1, v2)) ` E = {(x, y). adjacent x y}
[PROOF STEP]
have "\<And>x. x\<in>{(v1,v2). adjacent v1 v2} \<Longrightarrow> x\<in>(\<lambda>(v1,w,v2). (v1,v2))`E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {(x, y). adjacent x y} \<Longrightarrow> x \<in> (\<lambda>(v1, w, v2). (v1, v2)) ` E
[PROOF STEP]
unfolding adjacent_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {(v1, v2). \<exists>w. (v1, w, v2) \<in> E} \<Longrightarrow> x \<in> (\<lambda>(v1, w, v2). (v1, v2)) ` E
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
?x \<in> {(x, y). adjacent x y} \<Longrightarrow> ?x \<in> (\<lambda>(v1, w, v2). (v1, v2)) ` E

goal (1 subgoal):
 1. (\<lambda>(v1, w, v2). (v1, v2)) ` E = {(x, y). adjacent x y}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?x \<in> (\<lambda>(v1, w, v2). (v1, v2)) ` E \<Longrightarrow> ?x \<in> {(x, y). adjacent x y}
?x \<in> {(x, y). adjacent x y} \<Longrightarrow> ?x \<in> (\<lambda>(v1, w, v2). (v1, v2)) ` E
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?x \<in> (\<lambda>(v1, w, v2). (v1, v2)) ` E \<Longrightarrow> ?x \<in> {(x, y). adjacent x y}
?x \<in> {(x, y). adjacent x y} \<Longrightarrow> ?x \<in> (\<lambda>(v1, w, v2). (v1, v2)) ` E

goal (1 subgoal):
 1. (\<lambda>(v1, w, v2). (v1, v2)) ` E = {(x, y). adjacent x y}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<lambda>(v1, w, v2). (v1, v2)) ` E = {(x, y). adjacent x y}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>(v1, w, v2). (v1, v2)) ` E = {(x, y). adjacent x y}

goal (1 subgoal):
 1. card E = card {(x, y). adjacent x y}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>(v1, w, v2). (v1, v2)) ` E = {(x, y). adjacent x y}

goal (1 subgoal):
 1. card E = card {(x, y). adjacent x y}
[PROOF STEP]
have "inj_on (\<lambda>(v1,w,v2). (v1,v2)) E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>(v1, w, v2). (v1, v2)) E
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>E. \<forall>y\<in>E. (case x of (v1, w, xa) \<Rightarrow> (v1, xa)) = (case y of (v1, w, xa) \<Rightarrow> (v1, xa)) \<longrightarrow> x = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>(v1, w, v2). (v1, v2)) E

goal (1 subgoal):
 1. card E = card {(x, y). adjacent x y}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>(v1, w, v2). (v1, v2)) ` E = {(x, y). adjacent x y}
inj_on (\<lambda>(v1, w, v2). (v1, v2)) E
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>(v1, w, v2). (v1, v2)) ` E = {(x, y). adjacent x y}
inj_on (\<lambda>(v1, w, v2). (v1, v2)) E

goal (1 subgoal):
 1. card E = card {(x, y). adjacent x y}
[PROOF STEP]
by (metis card_image)
[PROOF STATE]
proof (state)
this:
card E = card {(x, y). adjacent x y}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card E = card {(x, y). adjacent x y}

goal (1 subgoal):
 1. {(x, y). adjacent x y} \<noteq> {} \<Longrightarrow> finite E
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card {(x, y). adjacent x y} \<noteq> 0
card E = card {(x, y). adjacent x y}
[PROOF STEP]
show "finite E"
[PROOF STATE]
proof (prove)
using this:
card {(x, y). adjacent x y} \<noteq> 0
card E = card {(x, y). adjacent x y}

goal (1 subgoal):
 1. finite E
[PROOF STEP]
by (metis card.infinite)
[PROOF STATE]
proof (state)
this:
finite E

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma del_unEdge_valid'[simp]:"valid_unSimpGraph G\<Longrightarrow>
    valid_unSimpGraph (del_unEdge v w u G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_unSimpGraph G \<Longrightarrow> valid_unSimpGraph (del_unEdge v w u G)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. valid_unSimpGraph G \<Longrightarrow> valid_unSimpGraph (del_unEdge v w u G)
[PROOF STEP]
assume "valid_unSimpGraph G"
[PROOF STATE]
proof (state)
this:
valid_unSimpGraph G

goal (1 subgoal):
 1. valid_unSimpGraph G \<Longrightarrow> valid_unSimpGraph (del_unEdge v w u G)
[PROOF STEP]
hence "valid_unMultigraph (del_unEdge v w u G)"
[PROOF STATE]
proof (prove)
using this:
valid_unSimpGraph G

goal (1 subgoal):
 1. valid_unMultigraph (del_unEdge v w u G)
[PROOF STEP]
using valid_unSimpGraph_def[of G] del_unEdge_valid[of G]
[PROOF STATE]
proof (prove)
using this:
valid_unSimpGraph G
valid_unSimpGraph G \<equiv> valid_unMultigraph G \<and> valid_unSimpGraph_axioms G
valid_unMultigraph G \<Longrightarrow> valid_unMultigraph (del_unEdge ?v ?e ?v' G)

goal (1 subgoal):
 1. valid_unMultigraph (del_unEdge v w u G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_unMultigraph (del_unEdge v w u G)

goal (1 subgoal):
 1. valid_unSimpGraph G \<Longrightarrow> valid_unSimpGraph (del_unEdge v w u G)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
valid_unMultigraph (del_unEdge v w u G)

goal (1 subgoal):
 1. valid_unSimpGraph G \<Longrightarrow> valid_unSimpGraph (del_unEdge v w u G)
[PROOF STEP]
have "valid_unSimpGraph_axioms (del_unEdge v w u G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_unSimpGraph_axioms (del_unEdge v w u G)
[PROOF STEP]
using valid_unSimpGraph.no_multi[OF \<open>valid_unSimpGraph G\<close>]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?v, ?w, ?u) \<in> edges G; (?v, ?w', ?u) \<in> edges G\<rbrakk> \<Longrightarrow> ?w = ?w'

goal (1 subgoal):
 1. valid_unSimpGraph_axioms (del_unEdge v w u G)
[PROOF STEP]
unfolding valid_unSimpGraph_axioms_def del_unEdge_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?v, ?w, ?u) \<in> edges G; (?v, ?w', ?u) \<in> edges G\<rbrakk> \<Longrightarrow> ?w = ?w'

goal (1 subgoal):
 1. \<forall>va wa ua w'. (va, wa, ua) \<in> edges \<lparr>nodes = nodes G, edges = edges G - {(v, w, u), (u, w, v)}\<rparr> \<longrightarrow> (va, w', ua) \<in> edges \<lparr>nodes = nodes G, edges = edges G - {(v, w, u), (u, w, v)}\<rparr> \<longrightarrow> wa = w'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_unSimpGraph_axioms (del_unEdge v w u G)

goal (1 subgoal):
 1. valid_unSimpGraph G \<Longrightarrow> valid_unSimpGraph (del_unEdge v w u G)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
valid_unMultigraph (del_unEdge v w u G)
valid_unSimpGraph_axioms (del_unEdge v w u G)
[PROOF STEP]
show "valid_unSimpGraph (del_unEdge v w u G)"
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph (del_unEdge v w u G)
valid_unSimpGraph_axioms (del_unEdge v w u G)

goal (1 subgoal):
 1. valid_unSimpGraph (del_unEdge v w u G)
[PROOF STEP]
using valid_unSimpGraph_def
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph (del_unEdge v w u G)
valid_unSimpGraph_axioms (del_unEdge v w u G)
valid_unSimpGraph ?G \<equiv> valid_unMultigraph ?G \<and> valid_unSimpGraph_axioms ?G

goal (1 subgoal):
 1. valid_unSimpGraph (del_unEdge v w u G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_unSimpGraph (del_unEdge v w u G)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in valid_unSimpGraph) del_UnEdge_non_adj:
    "(v,w,u)\<in>E \<Longrightarrow> \<not>valid_unMultigraph.adjacent (del_unEdge v w u G) v u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v, w, u) \<in> E \<Longrightarrow> \<not> valid_unMultigraph.adjacent (del_unEdge v w u G) v u
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>(v, w, u) \<in> E; valid_unMultigraph.adjacent (del_unEdge v w u G) v u\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "(v, w, u) \<in> E"
      and ccontr:"valid_unMultigraph.adjacent (del_unEdge v w u G) v u"
[PROOF STATE]
proof (state)
this:
(v, w, u) \<in> E
valid_unMultigraph.adjacent (del_unEdge v w u G) v u

goal (1 subgoal):
 1. \<lbrakk>(v, w, u) \<in> E; valid_unMultigraph.adjacent (del_unEdge v w u G) v u\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have valid:"valid_unMultigraph (del_unEdge v w u G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_unMultigraph (del_unEdge v w u G)
[PROOF STEP]
using valid_unMultigraph_axioms
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph G

goal (1 subgoal):
 1. valid_unMultigraph (del_unEdge v w u G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_unMultigraph (del_unEdge v w u G)

goal (1 subgoal):
 1. \<lbrakk>(v, w, u) \<in> E; valid_unMultigraph.adjacent (del_unEdge v w u G) v u\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
valid_unMultigraph (del_unEdge v w u G)
[PROOF STEP]
obtain w' where vw'u:"(v,w',u)\<in>edges (del_unEdge v w u G)"
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph (del_unEdge v w u G)

goal (1 subgoal):
 1. (\<And>w'. (v, w', u) \<in> edges (del_unEdge v w u G) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ccontr
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph (del_unEdge v w u G)
valid_unMultigraph.adjacent (del_unEdge v w u G) v u

goal (1 subgoal):
 1. (\<And>w'. (v, w', u) \<in> edges (del_unEdge v w u G) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding valid_unMultigraph.adjacent_def[OF valid]
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph (del_unEdge v w u G)
\<exists>wa. (v, wa, u) \<in> edges (del_unEdge v w u G)

goal (1 subgoal):
 1. (\<And>w'. (v, w', u) \<in> edges (del_unEdge v w u G) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(v, w', u) \<in> edges (del_unEdge v w u G)

goal (1 subgoal):
 1. \<lbrakk>(v, w, u) \<in> E; valid_unMultigraph.adjacent (del_unEdge v w u G) v u\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "(v,w',u)\<notin>{(v,w,u),(u,w,v)}"
[PROOF STATE]
proof (prove)
using this:
(v, w', u) \<in> edges (del_unEdge v w u G)

goal (1 subgoal):
 1. (v, w', u) \<notin> {(v, w, u), (u, w, v)}
[PROOF STEP]
unfolding del_unEdge_def
[PROOF STATE]
proof (prove)
using this:
(v, w', u) \<in> edges \<lparr>nodes = V, edges = E - {(v, w, u), (u, w, v)}\<rparr>

goal (1 subgoal):
 1. (v, w', u) \<notin> {(v, w, u), (u, w, v)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(v, w', u) \<notin> {(v, w, u), (u, w, v)}

goal (1 subgoal):
 1. \<lbrakk>(v, w, u) \<in> E; valid_unMultigraph.adjacent (del_unEdge v w u G) v u\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "w'\<noteq>w"
[PROOF STATE]
proof (prove)
using this:
(v, w', u) \<notin> {(v, w, u), (u, w, v)}

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

goal (1 subgoal):
 1. \<lbrakk>(v, w, u) \<in> E; valid_unMultigraph.adjacent (del_unEdge v w u G) v u\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
w' \<noteq> w

goal (1 subgoal):
 1. \<lbrakk>(v, w, u) \<in> E; valid_unMultigraph.adjacent (del_unEdge v w u G) v u\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "(v,w',u)\<in>E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v, w', u) \<in> E
[PROOF STEP]
using vw'u
[PROOF STATE]
proof (prove)
using this:
(v, w', u) \<in> edges (del_unEdge v w u G)

goal (1 subgoal):
 1. (v, w', u) \<in> E
[PROOF STEP]
unfolding del_unEdge_def
[PROOF STATE]
proof (prove)
using this:
(v, w', u) \<in> edges \<lparr>nodes = V, edges = E - {(v, w, u), (u, w, v)}\<rparr>

goal (1 subgoal):
 1. (v, w', u) \<in> E
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(v, w', u) \<in> E

goal (1 subgoal):
 1. \<lbrakk>(v, w, u) \<in> E; valid_unMultigraph.adjacent (del_unEdge v w u G) v u\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
w' \<noteq> w
(v, w', u) \<in> E
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
w' \<noteq> w
(v, w', u) \<in> E

goal (1 subgoal):
 1. False
[PROOF STEP]
using no_multi[of v w u w'] \<open>(v, w, u) \<in> E\<close>
[PROOF STATE]
proof (prove)
using this:
w' \<noteq> w
(v, w', u) \<in> E
\<lbrakk>(v, w, u) \<in> E; (v, w', u) \<in> E\<rbrakk> \<Longrightarrow> w = w'
(v, w, u) \<in> E

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in valid_unSimpGraph) degree_adjacent: "finite E \<Longrightarrow> degree v G=card {n. adjacent v n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite E \<Longrightarrow> degree v G = card {n. adjacent v n}
[PROOF STEP]
using valid_unSimpGraph_axioms
[PROOF STATE]
proof (prove)
using this:
valid_unSimpGraph G

goal (1 subgoal):
 1. finite E \<Longrightarrow> degree v G = card {n. adjacent v n}
[PROOF STEP]
proof (induct "degree v G" arbitrary: G)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>G. \<lbrakk>0 = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v))
 2. \<And>x G. \<lbrakk>\<And>G. \<lbrakk>x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v)); Suc x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 = degree v G
finite (edges G)
valid_unSimpGraph G

goal (2 subgoals):
 1. \<And>G. \<lbrakk>0 = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v))
 2. \<And>x G. \<lbrakk>\<And>G. \<lbrakk>x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v)); Suc x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v))
[PROOF STEP]
note valid3=\<open>valid_unSimpGraph G\<close>
[PROOF STATE]
proof (state)
this:
valid_unSimpGraph G

goal (2 subgoals):
 1. \<And>G. \<lbrakk>0 = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v))
 2. \<And>x G. \<lbrakk>\<And>G. \<lbrakk>x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v)); Suc x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v))
[PROOF STEP]
hence valid2: "valid_unMultigraph G"
[PROOF STATE]
proof (prove)
using this:
valid_unSimpGraph G

goal (1 subgoal):
 1. valid_unMultigraph G
[PROOF STEP]
using valid_unSimpGraph_def
[PROOF STATE]
proof (prove)
using this:
valid_unSimpGraph G
valid_unSimpGraph ?G \<equiv> valid_unMultigraph ?G \<and> valid_unSimpGraph_axioms ?G

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

goal (2 subgoals):
 1. \<And>G. \<lbrakk>0 = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v))
 2. \<And>x G. \<lbrakk>\<And>G. \<lbrakk>x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v)); Suc x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v))
[PROOF STEP]
have "{a. valid_unMultigraph.adjacent G v a}={}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a. valid_unMultigraph.adjacent G v a} = {}
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {a. valid_unMultigraph.adjacent G v a} \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
assume "{a. valid_unMultigraph.adjacent G v a} \<noteq> {}"
[PROOF STATE]
proof (state)
this:
{a. valid_unMultigraph.adjacent G v a} \<noteq> {}

goal (1 subgoal):
 1. {a. valid_unMultigraph.adjacent G v a} \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{a. valid_unMultigraph.adjacent G v a} \<noteq> {}
[PROOF STEP]
obtain w u where "(v,w,u)\<in>edges G"
[PROOF STATE]
proof (prove)
using this:
{a. valid_unMultigraph.adjacent G v a} \<noteq> {}

goal (1 subgoal):
 1. (\<And>w u. (v, w, u) \<in> edges G \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding valid_unMultigraph.adjacent_def[OF valid2]
[PROOF STATE]
proof (prove)
using this:
{a. \<exists>w. (v, w, a) \<in> edges G} \<noteq> {}

goal (1 subgoal):
 1. (\<And>w u. (v, w, u) \<in> edges G \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(v, w, u) \<in> edges G

goal (1 subgoal):
 1. {a. valid_unMultigraph.adjacent G v a} \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
hence "degree v G\<noteq>0"
[PROOF STATE]
proof (prove)
using this:
(v, w, u) \<in> edges G

goal (1 subgoal):
 1. degree v G \<noteq> 0
[PROOF STEP]
using \<open>finite (edges G)\<close>
[PROOF STATE]
proof (prove)
using this:
(v, w, u) \<in> edges G
finite (edges G)

goal (1 subgoal):
 1. degree v G \<noteq> 0
[PROOF STEP]
unfolding degree_def
[PROOF STATE]
proof (prove)
using this:
(v, w, u) \<in> edges G
finite (edges G)

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

goal (1 subgoal):
 1. {a. valid_unMultigraph.adjacent G v a} \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
degree v G \<noteq> 0

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{a. valid_unMultigraph.adjacent G v a} = {}

goal (2 subgoals):
 1. \<And>G. \<lbrakk>0 = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v))
 2. \<And>x G. \<lbrakk>\<And>G. \<lbrakk>x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v)); Suc x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
{a. valid_unMultigraph.adjacent G v a} = {}

goal (1 subgoal):
 1. degree v G = card {a. valid_unMultigraph.adjacent G v a}
[PROOF STEP]
by (metis "0.hyps" card.empty)
[PROOF STATE]
proof (state)
this:
degree v G = card {a. valid_unMultigraph.adjacent G v a}

goal (1 subgoal):
 1. \<And>x G. \<lbrakk>\<And>G. \<lbrakk>x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v)); Suc x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x G. \<lbrakk>\<And>G. \<lbrakk>x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v)); Suc x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v))
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>n = degree v ?G; finite (edges ?G); valid_unSimpGraph ?G\<rbrakk> \<Longrightarrow> degree v ?G = card (Collect (valid_unMultigraph.adjacent ?G v))
Suc n = degree v G
finite (edges G)
valid_unSimpGraph G

goal (1 subgoal):
 1. \<And>x G. \<lbrakk>\<And>G. \<lbrakk>x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v)); Suc x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v))
[PROOF STEP]
hence "{e \<in> edges G. fst e = v}\<noteq>{}"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n = degree v ?G; finite (edges ?G); valid_unSimpGraph ?G\<rbrakk> \<Longrightarrow> degree v ?G = card (Collect (valid_unMultigraph.adjacent ?G v))
Suc n = degree v G
finite (edges G)
valid_unSimpGraph G

goal (1 subgoal):
 1. {e \<in> edges G. fst e = v} \<noteq> {}
[PROOF STEP]
using card.empty
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n = degree v ?G; finite (edges ?G); valid_unSimpGraph ?G\<rbrakk> \<Longrightarrow> degree v ?G = card (Collect (valid_unMultigraph.adjacent ?G v))
Suc n = degree v G
finite (edges G)
valid_unSimpGraph G
card {} = 0

goal (1 subgoal):
 1. {e \<in> edges G. fst e = v} \<noteq> {}
[PROOF STEP]
unfolding degree_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n = card {e \<in> edges ?G. fst e = v}; finite (edges ?G); valid_unSimpGraph ?G\<rbrakk> \<Longrightarrow> card {e \<in> edges ?G. fst e = v} = card (Collect (valid_unMultigraph.adjacent ?G v))
Suc n = card {e \<in> edges G. fst e = v}
finite (edges G)
valid_unSimpGraph G
card {} = 0

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

goal (1 subgoal):
 1. \<And>x G. \<lbrakk>\<And>G. \<lbrakk>x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v)); Suc x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{e \<in> edges G. fst e = v} \<noteq> {}
[PROOF STEP]
obtain w u where "(v,w,u)\<in>edges G"
[PROOF STATE]
proof (prove)
using this:
{e \<in> edges G. fst e = v} \<noteq> {}

goal (1 subgoal):
 1. (\<And>w u. (v, w, u) \<in> edges G \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(v, w, u) \<in> edges G

goal (1 subgoal):
 1. \<And>x G. \<lbrakk>\<And>G. \<lbrakk>x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v)); Suc x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v))
[PROOF STEP]
have valid:"valid_unMultigraph G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_unMultigraph G
[PROOF STEP]
using \<open>valid_unSimpGraph G\<close> valid_unSimpGraph_def
[PROOF STATE]
proof (prove)
using this:
valid_unSimpGraph G
valid_unSimpGraph ?G \<equiv> valid_unMultigraph ?G \<and> valid_unSimpGraph_axioms ?G

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

goal (1 subgoal):
 1. \<And>x G. \<lbrakk>\<And>G. \<lbrakk>x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v)); Suc x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v))
[PROOF STEP]
hence valid':"valid_unMultigraph (del_unEdge v w u G)"
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph G

goal (1 subgoal):
 1. valid_unMultigraph (del_unEdge v w u G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_unMultigraph (del_unEdge v w u G)

goal (1 subgoal):
 1. \<And>x G. \<lbrakk>\<And>G. \<lbrakk>x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v)); Suc x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v))
[PROOF STEP]
have "valid_unSimpGraph (del_unEdge v w u G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_unSimpGraph (del_unEdge v w u G)
[PROOF STEP]
using del_unEdge_valid' \<open>valid_unSimpGraph G\<close>
[PROOF STATE]
proof (prove)
using this:
valid_unSimpGraph ?G \<Longrightarrow> valid_unSimpGraph (del_unEdge ?v ?w ?u ?G)
valid_unSimpGraph G

goal (1 subgoal):
 1. valid_unSimpGraph (del_unEdge v w u G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_unSimpGraph (del_unEdge v w u G)

goal (1 subgoal):
 1. \<And>x G. \<lbrakk>\<And>G. \<lbrakk>x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v)); Suc x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
valid_unSimpGraph (del_unEdge v w u G)

goal (1 subgoal):
 1. \<And>x G. \<lbrakk>\<And>G. \<lbrakk>x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v)); Suc x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v))
[PROOF STEP]
have "n = degree v (del_unEdge v w u G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = degree v (del_unEdge v w u G)
[PROOF STEP]
using \<open>Suc n = degree v G\<close>\<open>(v, w, u) \<in> edges G\<close>  del_edge_undirected_degree_plus[of G v w u]
[PROOF STATE]
proof (prove)
using this:
Suc n = degree v G
(v, w, u) \<in> edges G
\<lbrakk>finite (edges G); (v, w, u) \<in> edges G; (u, w, v) \<in> edges G\<rbrakk> \<Longrightarrow> degree v (del_unEdge v w u G) + 1 = degree v G

goal (1 subgoal):
 1. n = degree v (del_unEdge v w u G)
[PROOF STEP]
by (metis Suc.prems(1) Suc_eq_plus1 diff_Suc_1 valid valid_unMultigraph.corres)
[PROOF STATE]
proof (state)
this:
n = degree v (del_unEdge v w u G)

goal (1 subgoal):
 1. \<And>x G. \<lbrakk>\<And>G. \<lbrakk>x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v)); Suc x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n = degree v (del_unEdge v w u G)

goal (1 subgoal):
 1. \<And>x G. \<lbrakk>\<And>G. \<lbrakk>x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v)); Suc x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v))
[PROOF STEP]
have "finite (edges (del_unEdge v w u G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (edges (del_unEdge v w u G))
[PROOF STEP]
using \<open>finite (edges G)\<close>
[PROOF STATE]
proof (prove)
using this:
finite (edges G)

goal (1 subgoal):
 1. finite (edges (del_unEdge v w u G))
[PROOF STEP]
unfolding del_unEdge_def
[PROOF STATE]
proof (prove)
using this:
finite (edges G)

goal (1 subgoal):
 1. finite (edges \<lparr>nodes = nodes G, edges = edges G - {(v, w, u), (u, w, v)}\<rparr>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (edges (del_unEdge v w u G))

goal (1 subgoal):
 1. \<And>x G. \<lbrakk>\<And>G. \<lbrakk>x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v)); Suc x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
valid_unSimpGraph (del_unEdge v w u G)
n = degree v (del_unEdge v w u G)
finite (edges (del_unEdge v w u G))
[PROOF STEP]
have "degree v (del_unEdge v w u G)
      = card (Collect (valid_unMultigraph.adjacent (del_unEdge v w u G) v))"
[PROOF STATE]
proof (prove)
using this:
valid_unSimpGraph (del_unEdge v w u G)
n = degree v (del_unEdge v w u G)
finite (edges (del_unEdge v w u G))

goal (1 subgoal):
 1. degree v (del_unEdge v w u G) = card (Collect (valid_unMultigraph.adjacent (del_unEdge v w u G) v))
[PROOF STEP]
using Suc.hyps
[PROOF STATE]
proof (prove)
using this:
valid_unSimpGraph (del_unEdge v w u G)
n = degree v (del_unEdge v w u G)
finite (edges (del_unEdge v w u G))
\<lbrakk>n = degree v ?G; finite (edges ?G); valid_unSimpGraph ?G\<rbrakk> \<Longrightarrow> degree v ?G = card (Collect (valid_unMultigraph.adjacent ?G v))
Suc n = degree v G

goal (1 subgoal):
 1. degree v (del_unEdge v w u G) = card (Collect (valid_unMultigraph.adjacent (del_unEdge v w u G) v))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree v (del_unEdge v w u G) = card (Collect (valid_unMultigraph.adjacent (del_unEdge v w u G) v))

goal (1 subgoal):
 1. \<And>x G. \<lbrakk>\<And>G. \<lbrakk>x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v)); Suc x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
degree v (del_unEdge v w u G) = card (Collect (valid_unMultigraph.adjacent (del_unEdge v w u G) v))

goal (1 subgoal):
 1. \<And>x G. \<lbrakk>\<And>G. \<lbrakk>x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v)); Suc x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v))
[PROOF STEP]
have "Suc(card ({n. valid_unMultigraph.adjacent (del_unEdge v w u G)
      v n})) = card ({n. valid_unMultigraph.adjacent G v n})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (card {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}) = card {n. valid_unMultigraph.adjacent G v n}
[PROOF STEP]
using valid_unMultigraph.adjacent_def[OF valid']
[PROOF STATE]
proof (prove)
using this:
valid_unMultigraph.adjacent (del_unEdge v w u G) ?v ?v' \<equiv> \<exists>wa. (?v, wa, ?v') \<in> edges (del_unEdge v w u G)

goal (1 subgoal):
 1. Suc (card {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}) = card {n. valid_unMultigraph.adjacent G v n}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>va v'. valid_unMultigraph.adjacent (del_unEdge v w u G) va v' \<equiv> \<exists>wa. (va, wa, v') \<in> edges (del_unEdge v w u G)) \<Longrightarrow> Suc (card {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}) = card {n. valid_unMultigraph.adjacent G v n}
[PROOF STEP]
have "{n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n} \<subseteq>
          {n. valid_unMultigraph.adjacent G v n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n} \<subseteq> {n. valid_unMultigraph.adjacent G v n}
[PROOF STEP]
using del_unEdge_def[of v w u G]
[PROOF STATE]
proof (prove)
using this:
del_unEdge v w u G \<equiv> \<lparr>nodes = nodes G, edges = edges G - {(v, w, u), (u, w, v)}\<rparr>

goal (1 subgoal):
 1. {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n} \<subseteq> {n. valid_unMultigraph.adjacent G v n}
[PROOF STEP]
unfolding valid_unMultigraph.adjacent_def[OF valid']
          valid_unMultigraph.adjacent_def[OF valid]
[PROOF STATE]
proof (prove)
using this:
del_unEdge v w u G \<equiv> \<lparr>nodes = nodes G, edges = edges G - {(v, w, u), (u, w, v)}\<rparr>

goal (1 subgoal):
 1. {n. \<exists>wa. (v, wa, n) \<in> edges (del_unEdge v w u G)} \<subseteq> {n. \<exists>w. (v, w, n) \<in> edges G}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n} \<subseteq> {n. valid_unMultigraph.adjacent G v n}

goal (1 subgoal):
 1. (\<And>va v'. valid_unMultigraph.adjacent (del_unEdge v w u G) va v' \<equiv> \<exists>wa. (va, wa, v') \<in> edges (del_unEdge v w u G)) \<Longrightarrow> Suc (card {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}) = card {n. valid_unMultigraph.adjacent G v n}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n} \<subseteq> {n. valid_unMultigraph.adjacent G v n}

goal (1 subgoal):
 1. (\<And>va v'. valid_unMultigraph.adjacent (del_unEdge v w u G) va v' \<equiv> \<exists>wa. (va, wa, v') \<in> edges (del_unEdge v w u G)) \<Longrightarrow> Suc (card {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}) = card {n. valid_unMultigraph.adjacent G v n}
[PROOF STEP]
have "u\<in>{n. valid_unMultigraph.adjacent G v n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<in> {n. valid_unMultigraph.adjacent G v n}
[PROOF STEP]
using \<open>(v,w,u)\<in>edges G\<close>
[PROOF STATE]
proof (prove)
using this:
(v, w, u) \<in> edges G

goal (1 subgoal):
 1. u \<in> {n. valid_unMultigraph.adjacent G v n}
[PROOF STEP]
unfolding valid_unMultigraph.adjacent_def[OF valid]
[PROOF STATE]
proof (prove)
using this:
(v, w, u) \<in> edges G

goal (1 subgoal):
 1. u \<in> {n. \<exists>w. (v, w, n) \<in> edges G}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<in> {n. valid_unMultigraph.adjacent G v n}

goal (1 subgoal):
 1. (\<And>va v'. valid_unMultigraph.adjacent (del_unEdge v w u G) va v' \<equiv> \<exists>wa. (va, wa, v') \<in> edges (del_unEdge v w u G)) \<Longrightarrow> Suc (card {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}) = card {n. valid_unMultigraph.adjacent G v n}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n} \<subseteq> {n. valid_unMultigraph.adjacent G v n}
u \<in> {n. valid_unMultigraph.adjacent G v n}
[PROOF STEP]
have "{n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n} \<union> {u}
          \<subseteq> {n. valid_unMultigraph.adjacent G v n}"
[PROOF STATE]
proof (prove)
using this:
{n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n} \<subseteq> {n. valid_unMultigraph.adjacent G v n}
u \<in> {n. valid_unMultigraph.adjacent G v n}

goal (1 subgoal):
 1. {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n} \<union> {u} \<subseteq> {n. valid_unMultigraph.adjacent G v n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n} \<union> {u} \<subseteq> {n. valid_unMultigraph.adjacent G v n}

goal (1 subgoal):
 1. (\<And>va v'. valid_unMultigraph.adjacent (del_unEdge v w u G) va v' \<equiv> \<exists>wa. (va, wa, v') \<in> edges (del_unEdge v w u G)) \<Longrightarrow> Suc (card {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}) = card {n. valid_unMultigraph.adjacent G v n}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n} \<union> {u} \<subseteq> {n. valid_unMultigraph.adjacent G v n}

goal (1 subgoal):
 1. (\<And>va v'. valid_unMultigraph.adjacent (del_unEdge v w u G) va v' \<equiv> \<exists>wa. (va, wa, v') \<in> edges (del_unEdge v w u G)) \<Longrightarrow> Suc (card {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}) = card {n. valid_unMultigraph.adjacent G v n}
[PROOF STEP]
have "{n. valid_unMultigraph.adjacent G v n} - {u}
          \<subseteq> {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {n. valid_unMultigraph.adjacent G v n} - {u} \<subseteq> {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}
[PROOF STEP]
using del_unEdge_def[of v w u G]
[PROOF STATE]
proof (prove)
using this:
del_unEdge v w u G \<equiv> \<lparr>nodes = nodes G, edges = edges G - {(v, w, u), (u, w, v)}\<rparr>

goal (1 subgoal):
 1. {n. valid_unMultigraph.adjacent G v n} - {u} \<subseteq> {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}
[PROOF STEP]
unfolding valid_unMultigraph.adjacent_def[OF valid']
          valid_unMultigraph.adjacent_def[OF valid]
[PROOF STATE]
proof (prove)
using this:
del_unEdge v w u G \<equiv> \<lparr>nodes = nodes G, edges = edges G - {(v, w, u), (u, w, v)}\<rparr>

goal (1 subgoal):
 1. {n. \<exists>w. (v, w, n) \<in> edges G} - {u} \<subseteq> {n. \<exists>wa. (v, wa, n) \<in> edges (del_unEdge v w u G)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{n. valid_unMultigraph.adjacent G v n} - {u} \<subseteq> {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}

goal (1 subgoal):
 1. (\<And>va v'. valid_unMultigraph.adjacent (del_unEdge v w u G) va v' \<equiv> \<exists>wa. (va, wa, v') \<in> edges (del_unEdge v w u G)) \<Longrightarrow> Suc (card {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}) = card {n. valid_unMultigraph.adjacent G v n}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n} \<union> {u} \<subseteq> {n. valid_unMultigraph.adjacent G v n}
{n. valid_unMultigraph.adjacent G v n} - {u} \<subseteq> {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}
[PROOF STEP]
have "{n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n} \<union> {u}
          = {n. valid_unMultigraph.adjacent G v n}"
[PROOF STATE]
proof (prove)
using this:
{n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n} \<union> {u} \<subseteq> {n. valid_unMultigraph.adjacent G v n}
{n. valid_unMultigraph.adjacent G v n} - {u} \<subseteq> {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}

goal (1 subgoal):
 1. {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n} \<union> {u} = {n. valid_unMultigraph.adjacent G v n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n} \<union> {u} = {n. valid_unMultigraph.adjacent G v n}

goal (1 subgoal):
 1. (\<And>va v'. valid_unMultigraph.adjacent (del_unEdge v w u G) va v' \<equiv> \<exists>wa. (va, wa, v') \<in> edges (del_unEdge v w u G)) \<Longrightarrow> Suc (card {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}) = card {n. valid_unMultigraph.adjacent G v n}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n} \<union> {u} = {n. valid_unMultigraph.adjacent G v n}

goal (1 subgoal):
 1. (\<And>va v'. valid_unMultigraph.adjacent (del_unEdge v w u G) va v' \<equiv> \<exists>wa. (va, wa, v') \<in> edges (del_unEdge v w u G)) \<Longrightarrow> Suc (card {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}) = card {n. valid_unMultigraph.adjacent G v n}
[PROOF STEP]
have "u\<notin>{n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<notin> {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}
[PROOF STEP]
using valid_unSimpGraph.del_UnEdge_non_adj[OF \<open>valid_unSimpGraph G\<close> \<open>(v,w,u)\<in>edges G\<close>]
[PROOF STATE]
proof (prove)
using this:
\<not> valid_unMultigraph.adjacent (del_unEdge v w u G) v u

goal (1 subgoal):
 1. u \<notin> {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<notin> {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}

goal (1 subgoal):
 1. (\<And>va v'. valid_unMultigraph.adjacent (del_unEdge v w u G) va v' \<equiv> \<exists>wa. (va, wa, v') \<in> edges (del_unEdge v w u G)) \<Longrightarrow> Suc (card {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}) = card {n. valid_unMultigraph.adjacent G v n}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
u \<notin> {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}

goal (1 subgoal):
 1. (\<And>va v'. valid_unMultigraph.adjacent (del_unEdge v w u G) va v' \<equiv> \<exists>wa. (va, wa, v') \<in> edges (del_unEdge v w u G)) \<Longrightarrow> Suc (card {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}) = card {n. valid_unMultigraph.adjacent G v n}
[PROOF STEP]
have "finite {n. valid_unMultigraph.adjacent G v n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {n. valid_unMultigraph.adjacent G v n}
[PROOF STEP]
using valid_unMultigraph.adjacent_finite[OF valid \<open>finite (edges G)\<close>]
[PROOF STATE]
proof (prove)
using this:
finite {n. valid_unMultigraph.adjacent G ?v n}

goal (1 subgoal):
 1. finite {n. valid_unMultigraph.adjacent G v n}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite {n. valid_unMultigraph.adjacent G v n}

goal (1 subgoal):
 1. (\<And>va v'. valid_unMultigraph.adjacent (del_unEdge v w u G) va v' \<equiv> \<exists>wa. (va, wa, v') \<in> edges (del_unEdge v w u G)) \<Longrightarrow> Suc (card {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}) = card {n. valid_unMultigraph.adjacent G v n}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n} \<union> {u} = {n. valid_unMultigraph.adjacent G v n}
u \<notin> {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}
finite {n. valid_unMultigraph.adjacent G v n}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n} \<union> {u} = {n. valid_unMultigraph.adjacent G v n}
u \<notin> {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}
finite {n. valid_unMultigraph.adjacent G v n}

goal (1 subgoal):
 1. Suc (card {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}) = card {n. valid_unMultigraph.adjacent G v n}
[PROOF STEP]
by (metis Un_insert_right card_insert_disjoint finite_Un sup_bot_right)
[PROOF STATE]
proof (state)
this:
Suc (card {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}) = card {n. valid_unMultigraph.adjacent G v n}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Suc (card {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}) = card {n. valid_unMultigraph.adjacent G v n}

goal (1 subgoal):
 1. \<And>x G. \<lbrakk>\<And>G. \<lbrakk>x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v)); Suc x = degree v G; finite (edges G); valid_unSimpGraph G\<rbrakk> \<Longrightarrow> degree v G = card (Collect (valid_unMultigraph.adjacent G v))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
degree v (del_unEdge v w u G) = card (Collect (valid_unMultigraph.adjacent (del_unEdge v w u G) v))
Suc (card {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}) = card {n. valid_unMultigraph.adjacent G v n}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
degree v (del_unEdge v w u G) = card (Collect (valid_unMultigraph.adjacent (del_unEdge v w u G) v))
Suc (card {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}) = card {n. valid_unMultigraph.adjacent G v n}

goal (1 subgoal):
 1. degree v G = card (Collect (valid_unMultigraph.adjacent G v))
[PROOF STEP]
by (metis Suc.hyps(2) \<open>n = degree v (del_unEdge v w u G)\<close>)
[PROOF STATE]
proof (state)
this:
degree v G = card (Collect (valid_unMultigraph.adjacent G v))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in AC) left_commute[simp]: "f x (f y z) = f y (f x z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x (f y z) = f y (f x z)
[PROOF STEP]
by (simp only: assoc[symmetric]) simp


[STATEMENT]
lemma (in su_rel_fun) repr1: "(A,f A)\<in>F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A, f A) \<in> F
[PROOF STEP]
proof (unfold f_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (A, THE B. (A, B) \<in> F) \<in> F
[PROOF STEP]
obtain B where "(A,B)\<in>F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>B. (A, B) \<in> F \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule surjective)
[PROOF STATE]
proof (state)
this:
(A, B) \<in> F

goal (1 subgoal):
 1. (A, THE B. (A, B) \<in> F) \<in> F
[PROOF STEP]
with theI[where P="\<lambda>B. (A,B)\<in>F", OF this]
[PROOF STATE]
proof (chain)
picking this:
(\<And>x. (A, x) \<in> F \<Longrightarrow> x = B) \<Longrightarrow> (A, THE x. (A, x) \<in> F) \<in> F
(A, B) \<in> F
[PROOF STEP]
show "(A, THE x. (A, x) \<in> F) \<in> F"
[PROOF STATE]
proof (prove)
using this:
(\<And>x. (A, x) \<in> F \<Longrightarrow> x = B) \<Longrightarrow> (A, THE x. (A, x) \<in> F) \<in> F
(A, B) \<in> F

goal (1 subgoal):
 1. (A, THE x. (A, x) \<in> F) \<in> F
[PROOF STEP]
by (blast intro: unique)
[PROOF STATE]
proof (state)
this:
(A, THE x. (A, x) \<in> F) \<in> F

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in su_rel_fun) repr2: "(A,B)\<in>F \<Longrightarrow> B=f A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A, B) \<in> F \<Longrightarrow> B = f A
[PROOF STEP]
using repr1
[PROOF STATE]
proof (prove)
using this:
(?A, f ?A) \<in> F

goal (1 subgoal):
 1. (A, B) \<in> F \<Longrightarrow> B = f A
[PROOF STEP]
by (blast intro: unique)


[STATEMENT]
lemma (in su_rel_fun) repr: "(f A = B) = ((A,B)\<in>F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f A = B) = ((A, B) \<in> F)
[PROOF STEP]
using repr1 repr2
[PROOF STATE]
proof (prove)
using this:
(?A, f ?A) \<in> F
(?A, ?B) \<in> F \<Longrightarrow> ?B = f ?A

goal (1 subgoal):
 1. (f A = B) = ((A, B) \<in> F)
[PROOF STEP]
by (blast)


[STATEMENT]
lemma multiset_induct'[case_names empty add]: "\<lbrakk>P {#}; \<And>M x. P M \<Longrightarrow> P ({#x#}+M)\<rbrakk> \<Longrightarrow> P M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P {#}; \<And>M x. P M \<Longrightarrow> P ({#x#} + M)\<rbrakk> \<Longrightarrow> P M
[PROOF STEP]
by (induct rule: multiset_induct) (auto simp add: union_commute)


[STATEMENT]
lemma count_ne_remove: "\<lbrakk> x ~= t\<rbrakk> \<Longrightarrow> count S x = count (S-{#t#}) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> t \<Longrightarrow> count S x = count (S - {#t#}) x
[PROOF STEP]
by (auto)


[STATEMENT]
lemma mset_empty_count[simp]: "(\<forall>p. count M p = 0) = (M={#})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>p. count M p = 0) = (M = {#})
[PROOF STEP]
by (auto simp add: multiset_eq_iff)


[STATEMENT]
lemma size_diff_se: "\<lbrakk>t \<in># S\<rbrakk> \<Longrightarrow> size S = size (S - {#t#}) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> size S = size (S - {#t#}) + 1
[PROOF STEP]
proof (unfold size_multiset_overloaded_eq)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
[PROOF STEP]
let ?SIZE = "sum (count S) (set_mset S)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
[PROOF STEP]
assume A: "t \<in># S"
[PROOF STATE]
proof (state)
this:
t \<in># S

goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
t \<in># S
[PROOF STEP]
have SPLITPRE: "finite (set_mset S) & {t}\<subseteq>(set_mset S)"
[PROOF STATE]
proof (prove)
using this:
t \<in># S

goal (1 subgoal):
 1. finite (set_mset S) \<and> {t} \<subseteq> set_mset S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (set_mset S) \<and> {t} \<subseteq> set_mset S

goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
[PROOF STEP]
hence "?SIZE = sum (count S) (set_mset S - {t}) + sum (count S) {t}"
[PROOF STATE]
proof (prove)
using this:
finite (set_mset S) \<and> {t} \<subseteq> set_mset S

goal (1 subgoal):
 1. sum (count S) (set_mset S) = sum (count S) (set_mset S - {t}) + sum (count S) {t}
[PROOF STEP]
by (blast dest: sum.subset_diff)
[PROOF STATE]
proof (state)
this:
sum (count S) (set_mset S) = sum (count S) (set_mset S - {t}) + sum (count S) {t}

goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
[PROOF STEP]
hence "?SIZE = sum (count S) (set_mset S - {t}) + count (S) t"
[PROOF STATE]
proof (prove)
using this:
sum (count S) (set_mset S) = sum (count S) (set_mset S - {t}) + sum (count S) {t}

goal (1 subgoal):
 1. sum (count S) (set_mset S) = sum (count S) (set_mset S - {t}) + count S t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum (count S) (set_mset S) = sum (count S) (set_mset S - {t}) + count S t

goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sum (count S) (set_mset S) = sum (count S) (set_mset S - {t}) + count S t

goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
[PROOF STEP]
with A
[PROOF STATE]
proof (chain)
picking this:
t \<in># S
sum (count S) (set_mset S) = sum (count S) (set_mset S - {t}) + count S t
[PROOF STEP]
have "count S t = count (S-{#t#}) t + 1"
[PROOF STATE]
proof (prove)
using this:
t \<in># S
sum (count S) (set_mset S) = sum (count S) (set_mset S - {t}) + count S t

goal (1 subgoal):
 1. count S t = count (S - {#t#}) t + 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
count S t = count (S - {#t#}) t + 1

goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sum (count S) (set_mset S) = sum (count S) (set_mset S - {t}) + count S t
count S t = count (S - {#t#}) t + 1
[PROOF STEP]
have D: "?SIZE = sum (count S) (set_mset S - {t}) + count (S-{#t#}) t + 1"
[PROOF STATE]
proof (prove)
using this:
sum (count S) (set_mset S) = sum (count S) (set_mset S - {t}) + count S t
count S t = count (S - {#t#}) t + 1

goal (1 subgoal):
 1. sum (count S) (set_mset S) = sum (count S) (set_mset S - {t}) + count (S - {#t#}) t + 1
[PROOF STEP]
by (arith)
[PROOF STATE]
proof (state)
this:
sum (count S) (set_mset S) = sum (count S) (set_mset S - {t}) + count (S - {#t#}) t + 1

goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sum (count S) (set_mset S) = sum (count S) (set_mset S - {t}) + count (S - {#t#}) t + 1

goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
[PROOF STEP]
have "sum (count S) (set_mset S - {t}) = sum (count (S-{#t#})) (set_mset S - {t})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (count S) (set_mset S - {t}) = sum (count (S - {#t#})) (set_mset S - {t})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum (count S) (set_mset S - {t}) = sum (count (S - {#t#})) (set_mset S - {t})
[PROOF STEP]
have "ALL x:(set_mset S - {t}) . count S x = count (S-{#t#}) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set_mset S - {t}. count S x = count (S - {#t#}) x
[PROOF STEP]
by (auto iff add: count_ne_remove)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set_mset S - {t}. count S x = count (S - {#t#}) x

goal (1 subgoal):
 1. sum (count S) (set_mset S - {t}) = sum (count (S - {#t#})) (set_mset S - {t})
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set_mset S - {t}. count S x = count (S - {#t#}) x

goal (1 subgoal):
 1. sum (count S) (set_mset S - {t}) = sum (count (S - {#t#})) (set_mset S - {t})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum (count S) (set_mset S - {t}) = sum (count (S - {#t#})) (set_mset S - {t})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sum (count S) (set_mset S - {t}) = sum (count (S - {#t#})) (set_mset S - {t})

goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sum (count S) (set_mset S) = sum (count S) (set_mset S - {t}) + count (S - {#t#}) t + 1
sum (count S) (set_mset S - {t}) = sum (count (S - {#t#})) (set_mset S - {t})
[PROOF STEP]
have D: "?SIZE = sum (count (S-{#t#})) (set_mset S - {t}) + count (S-{#t#}) t + 1"
[PROOF STATE]
proof (prove)
using this:
sum (count S) (set_mset S) = sum (count S) (set_mset S - {t}) + count (S - {#t#}) t + 1
sum (count S) (set_mset S - {t}) = sum (count (S - {#t#})) (set_mset S - {t})

goal (1 subgoal):
 1. sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset S - {t}) + count (S - {#t#}) t + 1
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset S - {t}) + count (S - {#t#}) t + 1

goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset S - {t}) + count (S - {#t#}) t + 1

goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset S - {t}) + count (S - {#t#}) t + 1

goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
[PROOF STEP]
assume CASE: "t \<notin># S - {#t#}"
[PROOF STATE]
proof (state)
this:
t \<notin># S - {#t#}

goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
[PROOF STEP]
from CASE
[PROOF STATE]
proof (chain)
picking this:
t \<notin># S - {#t#}
[PROOF STEP]
have "set_mset S - {t} = set_mset (S - {#t#})"
[PROOF STATE]
proof (prove)
using this:
t \<notin># S - {#t#}

goal (1 subgoal):
 1. set_mset S - {t} = set_mset (S - {#t#})
[PROOF STEP]
by (simp add: at_most_one_mset_mset_diff)
[PROOF STATE]
proof (state)
this:
set_mset S - {t} = set_mset (S - {#t#})

goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
[PROOF STEP]
with CASE D
[PROOF STATE]
proof (chain)
picking this:
t \<notin># S - {#t#}
sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset S - {t}) + count (S - {#t#}) t + 1
set_mset S - {t} = set_mset (S - {#t#})
[PROOF STEP]
have "?SIZE = sum (count (S-{#t#})) (set_mset (S - {#t#})) + 1"
[PROOF STATE]
proof (prove)
using this:
t \<notin># S - {#t#}
sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset S - {t}) + count (S - {#t#}) t + 1
set_mset S - {t} = set_mset (S - {#t#})

goal (1 subgoal):
 1. sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
[PROOF STEP]
by (simp add: not_in_iff)
[PROOF STATE]
proof (state)
this:
sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1

goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
t \<notin># S - {#t#} \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1

goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
t \<notin># S - {#t#} \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1

goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
t \<notin># S - {#t#} \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1

goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
[PROOF STEP]
assume CASE: "t \<in># S - {#t#}"
[PROOF STATE]
proof (state)
this:
t \<in># S - {#t#}

goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
[PROOF STEP]
from CASE
[PROOF STATE]
proof (chain)
picking this:
t \<in># S - {#t#}
[PROOF STEP]
have 1: "set_mset S = set_mset (S-{#t#})"
[PROOF STATE]
proof (prove)
using this:
t \<in># S - {#t#}

goal (1 subgoal):
 1. set_mset S = set_mset (S - {#t#})
[PROOF STEP]
by (rule more_than_one_mset_mset_diff [symmetric])
[PROOF STATE]
proof (state)
this:
set_mset S = set_mset (S - {#t#})

goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set_mset S = set_mset (S - {#t#})

goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
[PROOF STEP]
from D
[PROOF STATE]
proof (chain)
picking this:
sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset S - {t}) + count (S - {#t#}) t + 1
[PROOF STEP]
have "?SIZE = sum (count (S-{#t#})) (set_mset S - {t}) + sum (count (S-{#t#})) {t} + 1"
[PROOF STATE]
proof (prove)
using this:
sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset S - {t}) + count (S - {#t#}) t + 1

goal (1 subgoal):
 1. sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset S - {t}) + sum (count (S - {#t#})) {t} + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset S - {t}) + sum (count (S - {#t#})) {t} + 1

goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset S - {t}) + sum (count (S - {#t#})) {t} + 1

goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
[PROOF STEP]
from SPLITPRE sum.subset_diff
[PROOF STATE]
proof (chain)
picking this:
finite (set_mset S) \<and> {t} \<subseteq> set_mset S
\<lbrakk>?B \<subseteq> ?A; finite ?A\<rbrakk> \<Longrightarrow> sum ?g ?A = sum ?g (?A - ?B) + sum ?g ?B
[PROOF STEP]
have "sum (count (S-{#t#})) (set_mset S) = sum (count (S-{#t#})) (set_mset S - {t}) + sum (count (S-{#t#})) {t}"
[PROOF STATE]
proof (prove)
using this:
finite (set_mset S) \<and> {t} \<subseteq> set_mset S
\<lbrakk>?B \<subseteq> ?A; finite ?A\<rbrakk> \<Longrightarrow> sum ?g ?A = sum ?g (?A - ?B) + sum ?g ?B

goal (1 subgoal):
 1. sum (count (S - {#t#})) (set_mset S) = sum (count (S - {#t#})) (set_mset S - {t}) + sum (count (S - {#t#})) {t}
[PROOF STEP]
by (blast)
[PROOF STATE]
proof (state)
this:
sum (count (S - {#t#})) (set_mset S) = sum (count (S - {#t#})) (set_mset S - {t}) + sum (count (S - {#t#})) {t}

goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set_mset S = set_mset (S - {#t#})
sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset S - {t}) + sum (count (S - {#t#})) {t} + 1
sum (count (S - {#t#})) (set_mset S) = sum (count (S - {#t#})) (set_mset S - {t}) + sum (count (S - {#t#})) {t}
[PROOF STEP]
have "?SIZE = sum (count (S-{#t#})) (set_mset (S-{#t#})) + 1"
[PROOF STATE]
proof (prove)
using this:
set_mset S = set_mset (S - {#t#})
sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset S - {t}) + sum (count (S - {#t#})) {t} + 1
sum (count (S - {#t#})) (set_mset S) = sum (count (S - {#t#})) (set_mset S - {t}) + sum (count (S - {#t#})) {t}

goal (1 subgoal):
 1. sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1

goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
t \<in># S - {#t#} \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1

goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset S - {t}) + count (S - {#t#}) t + 1
t \<notin># S - {#t#} \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
t \<in># S - {#t#} \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
[PROOF STEP]
show "?SIZE = sum (count (S-{#t#})) (set_mset (S - {#t#})) + 1"
[PROOF STATE]
proof (prove)
using this:
sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset S - {t}) + count (S - {#t#}) t + 1
t \<notin># S - {#t#} \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
t \<in># S - {#t#} \<Longrightarrow> sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1

goal (1 subgoal):
 1. sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
sum (count S) (set_mset S) = sum (count (S - {#t#})) (set_mset (S - {#t#})) + 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mset_union_diff_comm: "t \<in># S \<Longrightarrow> T + (S - {#t#}) = (T + S) - {#t#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> T + (S - {#t#}) = T + S - {#t#}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> T + (S - {#t#}) = T + S - {#t#}
[PROOF STEP]
assume "t \<in># S"
[PROOF STATE]
proof (state)
this:
t \<in># S

goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> T + (S - {#t#}) = T + S - {#t#}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<in># S
[PROOF STEP]
obtain S' where S: "S = add_mset t S'"
[PROOF STATE]
proof (prove)
using this:
t \<in># S

goal (1 subgoal):
 1. (\<And>S'. S = add_mset t S' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis insert_DiffM)
[PROOF STATE]
proof (state)
this:
S = add_mset t S'

goal (1 subgoal):
 1. t \<in># S \<Longrightarrow> T + (S - {#t#}) = T + S - {#t#}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S = add_mset t S'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
S = add_mset t S'

goal (1 subgoal):
 1. T + (S - {#t#}) = T + S - {#t#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
T + (S - {#t#}) = T + S - {#t#}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mset_right_cancel_union: "\<lbrakk>a \<in># A+B; ~(a \<in># B)\<rbrakk> \<Longrightarrow> a\<in>#A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in># A + B; a \<notin># B\<rbrakk> \<Longrightarrow> a \<in># A
[PROOF STEP]
by (simp)


[STATEMENT]
lemma mset_left_cancel_union: "\<lbrakk>a \<in># A+B; ~(a \<in># A)\<rbrakk> \<Longrightarrow> a\<in>#B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in># A + B; a \<notin># A\<rbrakk> \<Longrightarrow> a \<in># B
[PROOF STEP]
by (simp)


[STATEMENT]
lemma mset_right_cancel_elem: "\<lbrakk>a \<in># A+{#b#}; a~=b\<rbrakk> \<Longrightarrow> a\<in>#A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in># A + {#b#}; a \<noteq> b\<rbrakk> \<Longrightarrow> a \<in># A
[PROOF STEP]
apply(subgoal_tac "~(a \<in># {#b#})")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in># A + {#b#}; a \<noteq> b; a \<notin># {#b#}\<rbrakk> \<Longrightarrow> a \<in># A
 2. \<lbrakk>a \<in># A + {#b#}; a \<noteq> b\<rbrakk> \<Longrightarrow> a \<notin># {#b#}
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mset_left_cancel_elem: "\<lbrakk>a \<in># {#b#}+A; a~=b\<rbrakk> \<Longrightarrow> a\<in>#A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in># {#b#} + A; a \<noteq> b\<rbrakk> \<Longrightarrow> a \<in># A
[PROOF STEP]
apply(subgoal_tac "~(a \<in># {#b#})")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in># {#b#} + A; a \<noteq> b; a \<notin># {#b#}\<rbrakk> \<Longrightarrow> a \<in># A
 2. \<lbrakk>a \<in># {#b#} + A; a \<noteq> b\<rbrakk> \<Longrightarrow> a \<notin># {#b#}
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mset_diff_cancel1elem[simp]: "~(a \<in># B) \<Longrightarrow> {#a#}-B = {#a#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<notin># B \<Longrightarrow> {#a#} - B = {#a#}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<notin># B \<Longrightarrow> {#a#} - B = {#a#}
[PROOF STEP]
assume A: "~(a \<in># B)"
[PROOF STATE]
proof (state)
this:
a \<notin># B

goal (1 subgoal):
 1. a \<notin># B \<Longrightarrow> {#a#} - B = {#a#}
[PROOF STEP]
hence "count ({#a#}-B) a = count ({#a#}) a"
[PROOF STATE]
proof (prove)
using this:
a \<notin># B

goal (1 subgoal):
 1. count ({#a#} - B) a = count {#a#} a
[PROOF STEP]
by (auto simp add: not_in_iff)
[PROOF STATE]
proof (state)
this:
count ({#a#} - B) a = count {#a#} a

goal (1 subgoal):
 1. a \<notin># B \<Longrightarrow> {#a#} - B = {#a#}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
count ({#a#} - B) a = count {#a#} a

goal (1 subgoal):
 1. a \<notin># B \<Longrightarrow> {#a#} - B = {#a#}
[PROOF STEP]
have "ALL e . e~=a \<longrightarrow> count ({#a#}-B) e = count ({#a#}) e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>e. e \<noteq> a \<longrightarrow> count ({#a#} - B) e = count {#a#} e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>e. e \<noteq> a \<longrightarrow> count ({#a#} - B) e = count {#a#} e

goal (1 subgoal):
 1. a \<notin># B \<Longrightarrow> {#a#} - B = {#a#}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
count ({#a#} - B) a = count {#a#} a
\<forall>e. e \<noteq> a \<longrightarrow> count ({#a#} - B) e = count {#a#} e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
count ({#a#} - B) a = count {#a#} a
\<forall>e. e \<noteq> a \<longrightarrow> count ({#a#} - B) e = count {#a#} e

goal (1 subgoal):
 1. {#a#} - B = {#a#}
[PROOF STEP]
by (auto simp add: multiset_eq_iff)
[PROOF STATE]
proof (state)
this:
{#a#} - B = {#a#}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma union_diff_assoc: "C-B={#} \<Longrightarrow> (A+B)-C = A + (B-C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C - B = {#} \<Longrightarrow> A + B - C = A + (B - C)
[PROOF STEP]
by (simp add: multiset_eq_iff)


[STATEMENT]
lemma mset_union_2_elem: "{#a#}+{#b#} = M + {#c#} \<Longrightarrow> {#a#}=M & b=c | a=c & {#b#}=M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#a#} + {#b#} = M + {#c#} \<Longrightarrow> {#a#} = M \<and> b = c \<or> a = c \<and> {#b#} = M
[PROOF STEP]
by (auto simp: add_eq_conv_diff)


[STATEMENT]
lemma mset_un_cases[cases set, case_names left right]:
    "\<lbrakk>a \<in># A + B; a\<in>#A \<Longrightarrow> P; a\<in>#B \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in># A + B; a \<in># A \<Longrightarrow> P; a \<in># B \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (auto)


[STATEMENT]
lemma mset_unplusm_dist_cases[cases set, case_names left right]:
    assumes A: "add_mset s A = B+C"
    assumes L: "\<lbrakk>B=add_mset s (B-{#s#}); A=(B-{#s#})+C\<rbrakk> \<Longrightarrow> P"
    assumes R: "\<lbrakk>C=add_mset s (C-{#s#}); A=B+(C-{#s#})\<rbrakk> \<Longrightarrow> P"
    shows P
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P
[PROOF STEP]
from A[symmetric]
[PROOF STATE]
proof (chain)
picking this:
B + C = add_mset s A
[PROOF STEP]
have "s \<in># B+C"
[PROOF STATE]
proof (prove)
using this:
B + C = add_mset s A

goal (1 subgoal):
 1. s \<in># B + C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s \<in># B + C

goal (1 subgoal):
 1. P
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
s \<in># B + C

goal (1 subgoal):
 1. P
[PROOF STEP]
proof (cases rule: mset_un_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s \<in># B \<Longrightarrow> P
 2. s \<in># C \<Longrightarrow> P
[PROOF STEP]
case left
[PROOF STATE]
proof (state)
this:
s \<in># B

goal (2 subgoals):
 1. s \<in># B \<Longrightarrow> P
 2. s \<in># C \<Longrightarrow> P
[PROOF STEP]
hence 1: "B=add_mset s (B-{#s#})"
[PROOF STATE]
proof (prove)
using this:
s \<in># B

goal (1 subgoal):
 1. B = add_mset s (B - {#s#})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
B = add_mset s (B - {#s#})

goal (2 subgoals):
 1. s \<in># B \<Longrightarrow> P
 2. s \<in># C \<Longrightarrow> P
[PROOF STEP]
with A
[PROOF STATE]
proof (chain)
picking this:
add_mset s A = B + C
B = add_mset s (B - {#s#})
[PROOF STEP]
have "add_mset s A = add_mset s ((B-{#s#})+C)"
[PROOF STATE]
proof (prove)
using this:
add_mset s A = B + C
B = add_mset s (B - {#s#})

goal (1 subgoal):
 1. add_mset s A = add_mset s (B - {#s#} + C)
[PROOF STEP]
by (simp add: union_ac)
[PROOF STATE]
proof (state)
this:
add_mset s A = add_mset s (B - {#s#} + C)

goal (2 subgoals):
 1. s \<in># B \<Longrightarrow> P
 2. s \<in># C \<Longrightarrow> P
[PROOF STEP]
hence 2: "A = (B-{#s#})+C"
[PROOF STATE]
proof (prove)
using this:
add_mset s A = add_mset s (B - {#s#} + C)

goal (1 subgoal):
 1. A = B - {#s#} + C
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
A = B - {#s#} + C

goal (2 subgoals):
 1. s \<in># B \<Longrightarrow> P
 2. s \<in># C \<Longrightarrow> P
[PROOF STEP]
from L[OF 1 2]
[PROOF STATE]
proof (chain)
picking this:
P
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P

goal (1 subgoal):
 1. P
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
P

goal (1 subgoal):
 1. s \<in># C \<Longrightarrow> P
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<in># C \<Longrightarrow> P
[PROOF STEP]
case right
[PROOF STATE]
proof (state)
this:
s \<in># C

goal (1 subgoal):
 1. s \<in># C \<Longrightarrow> P
[PROOF STEP]
hence 1: "C=add_mset s (C-{#s#})"
[PROOF STATE]
proof (prove)
using this:
s \<in># C

goal (1 subgoal):
 1. C = add_mset s (C - {#s#})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
C = add_mset s (C - {#s#})

goal (1 subgoal):
 1. s \<in># C \<Longrightarrow> P
[PROOF STEP]
with A
[PROOF STATE]
proof (chain)
picking this:
add_mset s A = B + C
C = add_mset s (C - {#s#})
[PROOF STEP]
have "add_mset s A = add_mset s (B+(C-{#s#}))"
[PROOF STATE]
proof (prove)
using this:
add_mset s A = B + C
C = add_mset s (C - {#s#})

goal (1 subgoal):
 1. add_mset s A = add_mset s (B + (C - {#s#}))
[PROOF STEP]
by (simp add: union_ac)
[PROOF STATE]
proof (state)
this:
add_mset s A = add_mset s (B + (C - {#s#}))

goal (1 subgoal):
 1. s \<in># C \<Longrightarrow> P
[PROOF STEP]
hence 2: "A = B+(C-{#s#})"
[PROOF STATE]
proof (prove)
using this:
add_mset s A = add_mset s (B + (C - {#s#}))

goal (1 subgoal):
 1. A = B + (C - {#s#})
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
A = B + (C - {#s#})

goal (1 subgoal):
 1. s \<in># C \<Longrightarrow> P
[PROOF STEP]
from R[OF 1 2]
[PROOF STATE]
proof (chain)
picking this:
P
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P

goal (1 subgoal):
 1. P
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
P

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mset_unplusm_dist_cases2[cases set, case_names left right]:
    assumes A: "B+C = add_mset s A"
    assumes L: "\<lbrakk>B=add_mset s (B-{#s#}); A=(B-{#s#})+C\<rbrakk> \<Longrightarrow> P"
    assumes R: "\<lbrakk>C=add_mset s (C-{#s#}); A=B+(C-{#s#})\<rbrakk> \<Longrightarrow> P"
    shows P
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
using mset_unplusm_dist_cases[OF A[symmetric]] L R
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<lbrakk>B = add_mset s (B - {#s#}); A = B - {#s#} + C\<rbrakk> \<Longrightarrow> ?P; \<lbrakk>C = add_mset s (C - {#s#}); A = B + (C - {#s#})\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>B = add_mset s (B - {#s#}); A = B - {#s#} + C\<rbrakk> \<Longrightarrow> P
\<lbrakk>C = add_mset s (C - {#s#}); A = B + (C - {#s#})\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
by blast


[STATEMENT]
lemma mset_single_cases[cases set, case_names loc env]:
    assumes A: "add_mset s c = add_mset r' c'"
    assumes CASES: "\<lbrakk>s=r'; c=c'\<rbrakk> \<Longrightarrow> P" "\<lbrakk>c'={#s#}+(c'-{#s#}); c={#r'#}+(c-{#r'#}); c-{#r'#} = c'-{#s#} \<rbrakk> \<Longrightarrow> P"
    shows "P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P
[PROOF STEP]
assume CASE: "s=r'"
[PROOF STATE]
proof (state)
this:
s = r'

goal (1 subgoal):
 1. P
[PROOF STEP]
with A
[PROOF STATE]
proof (chain)
picking this:
add_mset s c = add_mset r' c'
s = r'
[PROOF STEP]
have "c=c'"
[PROOF STATE]
proof (prove)
using this:
add_mset s c = add_mset r' c'
s = r'

goal (1 subgoal):
 1. c = c'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
c = c'

goal (1 subgoal):
 1. P
[PROOF STEP]
with CASE CASES
[PROOF STATE]
proof (chain)
picking this:
s = r'
\<lbrakk>s = r'; c = c'\<rbrakk> \<Longrightarrow> P
\<lbrakk>c' = {#s#} + (c' - {#s#}); c = {#r'#} + (c - {#r'#}); c - {#r'#} = c' - {#s#}\<rbrakk> \<Longrightarrow> P
c = c'
[PROOF STEP]
have ?thesis
[PROOF STATE]
proof (prove)
using this:
s = r'
\<lbrakk>s = r'; c = c'\<rbrakk> \<Longrightarrow> P
\<lbrakk>c' = {#s#} + (c' - {#s#}); c = {#r'#} + (c - {#r'#}); c - {#r'#} = c' - {#s#}\<rbrakk> \<Longrightarrow> P
c = c'

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

goal (1 subgoal):
 1. P
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
s = r' \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s = r' \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
s = r' \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
assume CASE: "s\<noteq>r'"
[PROOF STATE]
proof (state)
this:
s \<noteq> r'

goal (1 subgoal):
 1. P
[PROOF STEP]
have "s\<in>#{#s#}+c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in># {#s#} + c
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s \<in># {#s#} + c

goal (1 subgoal):
 1. P
[PROOF STEP]
with A
[PROOF STATE]
proof (chain)
picking this:
add_mset s c = add_mset r' c'
s \<in># {#s#} + c
[PROOF STEP]
have "s \<in># {#r'#} + c'"
[PROOF STATE]
proof (prove)
using this:
add_mset s c = add_mset r' c'
s \<in># {#s#} + c

goal (1 subgoal):
 1. s \<in># {#r'#} + c'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s \<in># {#r'#} + c'

goal (1 subgoal):
 1. P
[PROOF STEP]
with CASE
[PROOF STATE]
proof (chain)
picking this:
s \<noteq> r'
s \<in># {#r'#} + c'
[PROOF STEP]
have "s \<in># c'"
[PROOF STATE]
proof (prove)
using this:
s \<noteq> r'
s \<in># {#r'#} + c'

goal (1 subgoal):
 1. s \<in># c'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s \<in># c'

goal (1 subgoal):
 1. P
[PROOF STEP]
from insert_DiffM[OF this, symmetric]
[PROOF STATE]
proof (chain)
picking this:
c' = add_mset s (c' - {#s#})
[PROOF STEP]
have 1: "c' = add_mset s (c' - {#s#})"
[PROOF STATE]
proof (prove)
using this:
c' = add_mset s (c' - {#s#})

goal (1 subgoal):
 1. c' = add_mset s (c' - {#s#})
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
c' = add_mset s (c' - {#s#})

goal (1 subgoal):
 1. P
[PROOF STEP]
with A
[PROOF STATE]
proof (chain)
picking this:
add_mset s c = add_mset r' c'
c' = add_mset s (c' - {#s#})
[PROOF STEP]
have "{#s#}+c = {#s#}+({#r'#}+(c' - {#s#}))"
[PROOF STATE]
proof (prove)
using this:
add_mset s c = add_mset r' c'
c' = add_mset s (c' - {#s#})

goal (1 subgoal):
 1. {#s#} + c = {#s#} + ({#r'#} + (c' - {#s#}))
[PROOF STEP]
by (auto simp add: union_ac)
[PROOF STATE]
proof (state)
this:
{#s#} + c = {#s#} + ({#r'#} + (c' - {#s#}))

goal (1 subgoal):
 1. P
[PROOF STEP]
hence 2: "c={#r'#}+(c' - {#s#})"
[PROOF STATE]
proof (prove)
using this:
{#s#} + c = {#s#} + ({#r'#} + (c' - {#s#}))

goal (1 subgoal):
 1. c = {#r'#} + (c' - {#s#})
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
c = {#r'#} + (c' - {#s#})

goal (1 subgoal):
 1. P
[PROOF STEP]
hence 3: "c-{#r'#} = (c' - {#s#})"
[PROOF STATE]
proof (prove)
using this:
c = {#r'#} + (c' - {#s#})

goal (1 subgoal):
 1. c - {#r'#} = c' - {#s#}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c - {#r'#} = c' - {#s#}

goal (1 subgoal):
 1. P
[PROOF STEP]
from 1 2 3 CASES
[PROOF STATE]
proof (chain)
picking this:
c' = add_mset s (c' - {#s#})
c = {#r'#} + (c' - {#s#})
c - {#r'#} = c' - {#s#}
\<lbrakk>s = r'; c = c'\<rbrakk> \<Longrightarrow> P
\<lbrakk>c' = {#s#} + (c' - {#s#}); c = {#r'#} + (c - {#r'#}); c - {#r'#} = c' - {#s#}\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
have ?thesis
[PROOF STATE]
proof (prove)
using this:
c' = add_mset s (c' - {#s#})
c = {#r'#} + (c' - {#s#})
c - {#r'#} = c' - {#s#}
\<lbrakk>s = r'; c = c'\<rbrakk> \<Longrightarrow> P
\<lbrakk>c' = {#s#} + (c' - {#s#}); c = {#r'#} + (c - {#r'#}); c - {#r'#} = c' - {#s#}\<rbrakk> \<Longrightarrow> P

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

goal (1 subgoal):
 1. P
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
s \<noteq> r' \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
s = r' \<Longrightarrow> P
s \<noteq> r' \<Longrightarrow> P
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s = r' \<Longrightarrow> P
s \<noteq> r' \<Longrightarrow> P

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mset_single_cases'[cases set, case_names loc env]:
    assumes A: "add_mset s c = add_mset r' c'"
    assumes CASES: "\<lbrakk>s=r'; c=c'\<rbrakk> \<Longrightarrow> P" "!!cc. \<lbrakk>c'={#s#}+cc; c={#r'#}+cc; c'-{#s#}=cc; c-{#r'#}=cc\<rbrakk> \<Longrightarrow> P"
    shows "P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
using A  CASES
[PROOF STATE]
proof (prove)
using this:
add_mset s c = add_mset r' c'
\<lbrakk>s = r'; c = c'\<rbrakk> \<Longrightarrow> P
\<lbrakk>c' = {#s#} + ?cc; c = {#r'#} + ?cc; c' - {#s#} = ?cc; c - {#r'#} = ?cc\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
by (auto elim!: mset_single_cases)


[STATEMENT]
lemma mset_single_cases2[cases set, case_names loc env]:
    assumes A: "add_mset s c = add_mset r' c'"
    assumes CASES: "\<lbrakk>s=r'; c=c'\<rbrakk> \<Longrightarrow> P" "\<lbrakk>c'=(c'-{#s#})+{#s#}; c=(c-{#r'#})+{#r'#}; c-{#r'#} = c'-{#s#} \<rbrakk> \<Longrightarrow> P"
    shows "P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
add_mset s c = add_mset r' c'
[PROOF STEP]
have "add_mset s c = add_mset r' c'"
[PROOF STATE]
proof (prove)
using this:
add_mset s c = add_mset r' c'

goal (1 subgoal):
 1. add_mset s c = add_mset r' c'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
add_mset s c = add_mset r' c'

goal (1 subgoal):
 1. P
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
add_mset s c = add_mset r' c'

goal (1 subgoal):
 1. P
[PROOF STEP]
proof (cases rule: mset_single_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>s = r'; c = c'\<rbrakk> \<Longrightarrow> P
 2. \<lbrakk>c' = {#s#} + (c' - {#s#}); c = {#r'#} + (c - {#r'#}); c - {#r'#} = c' - {#s#}\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
case loc
[PROOF STATE]
proof (state)
this:
s = r'
c = c'

goal (2 subgoals):
 1. \<lbrakk>s = r'; c = c'\<rbrakk> \<Longrightarrow> P
 2. \<lbrakk>c' = {#s#} + (c' - {#s#}); c = {#r'#} + (c - {#r'#}); c - {#r'#} = c' - {#s#}\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
with CASES
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>s = r'; c = c'\<rbrakk> \<Longrightarrow> P
\<lbrakk>c' = c' - {#s#} + {#s#}; c = c - {#r'#} + {#r'#}; c - {#r'#} = c' - {#s#}\<rbrakk> \<Longrightarrow> P
s = r'
c = c'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>s = r'; c = c'\<rbrakk> \<Longrightarrow> P
\<lbrakk>c' = c' - {#s#} + {#s#}; c = c - {#r'#} + {#r'#}; c - {#r'#} = c' - {#s#}\<rbrakk> \<Longrightarrow> P
s = r'
c = c'

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

goal (1 subgoal):
 1. \<lbrakk>c' = {#s#} + (c' - {#s#}); c = {#r'#} + (c - {#r'#}); c - {#r'#} = c' - {#s#}\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>c' = {#s#} + (c' - {#s#}); c = {#r'#} + (c - {#r'#}); c - {#r'#} = c' - {#s#}\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
case env
[PROOF STATE]
proof (state)
this:
c' = {#s#} + (c' - {#s#})
c = {#r'#} + (c - {#r'#})
c - {#r'#} = c' - {#s#}

goal (1 subgoal):
 1. \<lbrakk>c' = {#s#} + (c' - {#s#}); c = {#r'#} + (c - {#r'#}); c - {#r'#} = c' - {#s#}\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
with CASES
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>s = r'; c = c'\<rbrakk> \<Longrightarrow> P
\<lbrakk>c' = c' - {#s#} + {#s#}; c = c - {#r'#} + {#r'#}; c - {#r'#} = c' - {#s#}\<rbrakk> \<Longrightarrow> P
c' = {#s#} + (c' - {#s#})
c = {#r'#} + (c - {#r'#})
c - {#r'#} = c' - {#s#}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>s = r'; c = c'\<rbrakk> \<Longrightarrow> P
\<lbrakk>c' = c' - {#s#} + {#s#}; c = c - {#r'#} + {#r'#}; c - {#r'#} = c' - {#s#}\<rbrakk> \<Longrightarrow> P
c' = {#s#} + (c' - {#s#})
c = {#r'#} + (c - {#r'#})
c - {#r'#} = c' - {#s#}

goal (1 subgoal):
 1. P
[PROOF STEP]
by (simp add: union_ac)
[PROOF STATE]
proof (state)
this:
P

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mset_single_cases2'[cases set, case_names loc env]:
    assumes A: "add_mset s c = add_mset r' c'"
    assumes CASES: "\<lbrakk>s=r'; c=c'\<rbrakk> \<Longrightarrow> P" "!!cc. \<lbrakk>c'=cc+{#s#}; c=cc+{#r'#}; c'-{#s#}=cc; c-{#r'#}=cc\<rbrakk> \<Longrightarrow> P"
    shows "P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
using A  CASES
[PROOF STATE]
proof (prove)
using this:
add_mset s c = add_mset r' c'
\<lbrakk>s = r'; c = c'\<rbrakk> \<Longrightarrow> P
\<lbrakk>c' = ?cc + {#s#}; c = ?cc + {#r'#}; c' - {#s#} = ?cc; c - {#r'#} = ?cc\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
by (auto elim!: mset_single_cases2)