[STATEMENT]
lemma bad_pair_set_finite:
  assumes "finite S"
  shows "finite (bad_pair_set S T c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (bad_pair_set S T c)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (bad_pair_set S T c)
[PROOF STEP]
have "finite (S \<times> S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (S \<times> S)
[PROOF STEP]
using finite_cartesian_product assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?A; finite ?B\<rbrakk> \<Longrightarrow> finite (?A \<times> ?B)
finite S

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

goal (1 subgoal):
 1. finite (bad_pair_set S T c)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
finite (S \<times> S)

goal (1 subgoal):
 1. finite (bad_pair_set S T c)
[PROOF STEP]
using bad_pair_set_filter_alt finite_filter
[PROOF STATE]
proof (prove)
using this:
finite (S \<times> S)
bad_pair_set ?S ?T ?c = Set.filter (\<lambda>p. bad_pair (fst p) (snd p) ?T ?c) (?S \<times> ?S)
finite ?S \<Longrightarrow> finite (Set.filter ?P ?S)

goal (1 subgoal):
 1. finite (bad_pair_set S T c)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (bad_pair_set S T c)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma codegree_is_path_length_two:
  "codegree x x' = card {p . connecting_path x x' p \<and> walk_length p = 2}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. codegree x x' = card {p. connecting_path x x' p \<and> walk_length p = 2}
[PROOF STEP]
unfolding codegree_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa} = card {p. connecting_path x x' p \<and> walk_length p = 2}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa} = card {p. connecting_path x x' p \<and> walk_length p = 2}
[PROOF STEP]
define f:: "'a list \<Rightarrow> 'a" where "f = (\<lambda> p. p!1)"
[PROOF STATE]
proof (state)
this:
f = (\<lambda>p. p ! 1)

goal (1 subgoal):
 1. card {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa} = card {p. connecting_path x x' p \<and> walk_length p = 2}
[PROOF STEP]
have f_inj: "inj_on f {p . connecting_path x x' p \<and> walk_length p = 2}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on f {p. connecting_path x x' p \<and> walk_length p = 2}
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>p. p ! 1) {p. connecting_path x x' p \<and> walk_length p = 2}
[PROOF STEP]
proof (intro inj_onI, simp del: One_nat_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa y. \<lbrakk>connecting_path x x' xa \<and> walk_length xa = 2; connecting_path x x' y \<and> walk_length y = 2; xa ! 1 = y ! 1\<rbrakk> \<Longrightarrow> xa = y
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa y. \<lbrakk>connecting_path x x' xa \<and> walk_length xa = 2; connecting_path x x' y \<and> walk_length y = 2; xa ! 1 = y ! 1\<rbrakk> \<Longrightarrow> xa = y
[PROOF STEP]
assume ha: "connecting_path x x' a \<and> walk_length a = 2" and
      hb: "connecting_path x x' b \<and> walk_length b = 2" and 1: "a!1 = b!1"
[PROOF STATE]
proof (state)
this:
connecting_path x x' a \<and> walk_length a = 2
connecting_path x x' b \<and> walk_length b = 2
a ! 1 = b ! 1

goal (1 subgoal):
 1. \<And>xa y. \<lbrakk>connecting_path x x' xa \<and> walk_length xa = 2; connecting_path x x' y \<and> walk_length y = 2; xa ! 1 = y ! 1\<rbrakk> \<Longrightarrow> xa = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
connecting_path x x' a \<and> walk_length a = 2
connecting_path x x' b \<and> walk_length b = 2
a ! 1 = b ! 1
[PROOF STEP]
have len: "length a = 3" "length b = 3"
[PROOF STATE]
proof (prove)
using this:
connecting_path x x' a \<and> walk_length a = 2
connecting_path x x' b \<and> walk_length b = 2
a ! 1 = b ! 1

goal (1 subgoal):
 1. length a = 3 &&& length b = 3
[PROOF STEP]
using walk_length_conv
[PROOF STATE]
proof (prove)
using this:
connecting_path x x' a \<and> walk_length a = 2
connecting_path x x' b \<and> walk_length b = 2
a ! 1 = b ! 1
walk_length ?p = length ?p - 1

goal (1 subgoal):
 1. length a = 3 &&& length b = 3
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length a = 3
length b = 3

goal (1 subgoal):
 1. \<And>xa y. \<lbrakk>connecting_path x x' xa \<and> walk_length xa = 2; connecting_path x x' y \<and> walk_length y = 2; xa ! 1 = y ! 1\<rbrakk> \<Longrightarrow> xa = y
[PROOF STEP]
show "a = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = b
[PROOF STEP]
using list2_middle_singleton 1 len list_middle_eq ha hb connecting_path_def len
[PROOF STATE]
proof (prove)
using this:
length ?xs = 3 \<Longrightarrow> butlast (tl ?xs) = [?xs ! 1]
a ! 1 = b ! 1
length a = 3
length b = 3
\<lbrakk>length ?xs = length ?ys; hd ?xs = hd ?ys; last ?xs = last ?ys; butlast (tl ?xs) = butlast (tl ?ys)\<rbrakk> \<Longrightarrow> ?xs = ?ys
connecting_path x x' a \<and> walk_length a = 2
connecting_path x x' b \<and> walk_length b = 2
connecting_path ?u ?v ?xs \<equiv> is_gen_path ?xs \<and> hd ?xs = ?u \<and> last ?xs = ?v
length a = 3
length b = 3

goal (1 subgoal):
 1. a = b
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
a = b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inj_on f {p. connecting_path x x' p \<and> walk_length p = 2}

goal (1 subgoal):
 1. card {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa} = card {p. connecting_path x x' p \<and> walk_length p = 2}
[PROOF STEP]
have f_image: "f ` {p . connecting_path x x' p \<and> walk_length p = 2} =
    {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` {p. connecting_path x x' p \<and> walk_length p = 2} = {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa}
[PROOF STEP]
proof(intro subset_antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f ` {p. connecting_path x x' p \<and> walk_length p = 2} \<subseteq> {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa}
 2. {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa} \<subseteq> f ` {p. connecting_path x x' p \<and> walk_length p = 2}
[PROOF STEP]
show "f ` {p. connecting_path x x' p \<and> walk_length p = 2}
    \<subseteq> {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` {p. connecting_path x x' p \<and> walk_length p = 2} \<subseteq> {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa}
[PROOF STEP]
proof (intro subsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> f ` {p. connecting_path x x' p \<and> walk_length p = 2} \<Longrightarrow> xa \<in> {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa}
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> f ` {p. connecting_path x x' p \<and> walk_length p = 2} \<Longrightarrow> xa \<in> {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa}
[PROOF STEP]
assume "a \<in> f ` {p. connecting_path x x' p \<and> walk_length p = 2}"
[PROOF STATE]
proof (state)
this:
a \<in> f ` {p. connecting_path x x' p \<and> walk_length p = 2}

goal (1 subgoal):
 1. \<And>xa. xa \<in> f ` {p. connecting_path x x' p \<and> walk_length p = 2} \<Longrightarrow> xa \<in> {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> f ` {p. connecting_path x x' p \<and> walk_length p = 2}
[PROOF STEP]
obtain p where ha: "p!1 = a" and hp: "connecting_path x x' p" and hpl: "length p = 3"
[PROOF STATE]
proof (prove)
using this:
a \<in> f ` {p. connecting_path x x' p \<and> walk_length p = 2}

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p ! 1 = a; connecting_path x x' p; length p = 3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using f_def walk_length_conv
[PROOF STATE]
proof (prove)
using this:
a \<in> f ` {p. connecting_path x x' p \<and> walk_length p = 2}
f = (\<lambda>p. p ! 1)
walk_length ?p = length ?p - 1

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p ! 1 = a; connecting_path x x' p; length p = 3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p ! 1 = a
connecting_path x x' p
length p = 3

goal (1 subgoal):
 1. \<And>xa. xa \<in> f ` {p. connecting_path x x' p \<and> walk_length p = 2} \<Longrightarrow> xa \<in> {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa}
[PROOF STEP]
have "p ! 0 = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p ! 0 = x
[PROOF STEP]
using hd_conv_nth[of p] hpl hp connecting_path_def
[PROOF STATE]
proof (prove)
using this:
p \<noteq> [] \<Longrightarrow> hd p = p ! 0
length p = 3
connecting_path x x' p
connecting_path ?u ?v ?xs \<equiv> is_gen_path ?xs \<and> hd ?xs = ?u \<and> last ?xs = ?v

goal (1 subgoal):
 1. p ! 0 = x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
p ! 0 = x

goal (1 subgoal):
 1. \<And>xa. xa \<in> f ` {p. connecting_path x x' p \<and> walk_length p = 2} \<Longrightarrow> xa \<in> {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p ! 0 = x
[PROOF STEP]
have va1: "vert_adj x a"
[PROOF STATE]
proof (prove)
using this:
p ! 0 = x

goal (1 subgoal):
 1. vert_adj x a
[PROOF STEP]
using is_walk_index[of 0 p] hp connecting_path_def is_gen_path_def
          vert_adj_def ha hpl
[PROOF STATE]
proof (prove)
using this:
p ! 0 = x
\<lbrakk>0 \<le> 0; Suc 0 < length p; is_walk p\<rbrakk> \<Longrightarrow> {p ! 0, p ! (0 + 1)} \<in> E
connecting_path x x' p
connecting_path ?u ?v ?xs \<equiv> is_gen_path ?xs \<and> hd ?xs = ?u \<and> last ?xs = ?v
is_gen_path ?p \<equiv> is_walk ?p \<and> (distinct (tl ?p) \<and> hd ?p = last ?p \<or> distinct ?p)
vert_adj ?v1.0 ?v2.0 \<equiv> {?v1.0, ?v2.0} \<in> E
p ! 1 = a
length p = 3

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

goal (1 subgoal):
 1. \<And>xa. xa \<in> f ` {p. connecting_path x x' p \<and> walk_length p = 2} \<Longrightarrow> xa \<in> {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa}
[PROOF STEP]
have "p ! 2 = x'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p ! 2 = x'
[PROOF STEP]
using last_conv_nth[of p] hpl hp connecting_path_def
[PROOF STATE]
proof (prove)
using this:
p \<noteq> [] \<Longrightarrow> last p = p ! (length p - 1)
length p = 3
connecting_path x x' p
connecting_path ?u ?v ?xs \<equiv> is_gen_path ?xs \<and> hd ?xs = ?u \<and> last ?xs = ?v

goal (1 subgoal):
 1. p ! 2 = x'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
p ! 2 = x'

goal (1 subgoal):
 1. \<And>xa. xa \<in> f ` {p. connecting_path x x' p \<and> walk_length p = 2} \<Longrightarrow> xa \<in> {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p ! 2 = x'
[PROOF STEP]
have "vert_adj a x'"
[PROOF STATE]
proof (prove)
using this:
p ! 2 = x'

goal (1 subgoal):
 1. vert_adj a x'
[PROOF STEP]
using is_walk_index[of 1 p] hp connecting_path_def is_gen_path_def
          vert_adj_def ha hpl
[PROOF STATE]
proof (prove)
using this:
p ! 2 = x'
\<lbrakk>0 \<le> 1; Suc 1 < length p; is_walk p\<rbrakk> \<Longrightarrow> {p ! 1, p ! (1 + 1)} \<in> E
connecting_path x x' p
connecting_path ?u ?v ?xs \<equiv> is_gen_path ?xs \<and> hd ?xs = ?u \<and> last ?xs = ?v
is_gen_path ?p \<equiv> is_walk ?p \<and> (distinct (tl ?p) \<and> hd ?p = last ?p \<or> distinct ?p)
vert_adj ?v1.0 ?v2.0 \<equiv> {?v1.0, ?v2.0} \<in> E
p ! 1 = a
length p = 3

goal (1 subgoal):
 1. vert_adj a x'
[PROOF STEP]
by (metis One_nat_def le0 lessI numeral_3_eq_3 one_add_one)
[PROOF STATE]
proof (state)
this:
vert_adj a x'

goal (1 subgoal):
 1. \<And>xa. xa \<in> f ` {p. connecting_path x x' p \<and> walk_length p = 2} \<Longrightarrow> xa \<in> {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vert_adj a x'
[PROOF STEP]
show "a \<in> {a \<in> V. vert_adj x a \<and> vert_adj x' a}"
[PROOF STATE]
proof (prove)
using this:
vert_adj a x'

goal (1 subgoal):
 1. a \<in> {a \<in> V. vert_adj x a \<and> vert_adj x' a}
[PROOF STEP]
using va1 vert_adj_sym
[PROOF STATE]
proof (prove)
using this:
vert_adj a x'
vert_adj x a
vert_adj ?v1.0 ?v2.0 = vert_adj ?v2.0 ?v1.0

goal (1 subgoal):
 1. a \<in> {a \<in> V. vert_adj x a \<and> vert_adj x' a}
[PROOF STEP]
by (simp add: vert_adj_imp_inV)
[PROOF STATE]
proof (state)
this:
a \<in> {a \<in> V. vert_adj x a \<and> vert_adj x' a}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f ` {p. connecting_path x x' p \<and> walk_length p = 2} \<subseteq> {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa}

goal (1 subgoal):
 1. {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa} \<subseteq> f ` {p. connecting_path x x' p \<and> walk_length p = 2}
[PROOF STEP]
show "{xa \<in> V. vert_adj x xa \<and> vert_adj x' xa}
      \<subseteq> f ` {p. connecting_path x x' p \<and> walk_length p = 2}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa} \<subseteq> f ` {p. connecting_path x x' p \<and> walk_length p = 2}
[PROOF STEP]
proof (intro subsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa} \<Longrightarrow> xa \<in> f ` {p. connecting_path x x' p \<and> walk_length p = 2}
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa} \<Longrightarrow> xa \<in> f ` {p. connecting_path x x' p \<and> walk_length p = 2}
[PROOF STEP]
assume ha: "a \<in> {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa}"
[PROOF STATE]
proof (state)
this:
a \<in> {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa}

goal (1 subgoal):
 1. \<And>xa. xa \<in> {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa} \<Longrightarrow> xa \<in> f ` {p. connecting_path x x' p \<and> walk_length p = 2}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa}
[PROOF STEP]
have "a \<in> V" and "x \<in> V" and "x' \<in> V" and "vert_adj x a" and "vert_adj x' a"
[PROOF STATE]
proof (prove)
using this:
a \<in> {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa}

goal (1 subgoal):
 1. (a \<in> V &&& x \<in> V) &&& x' \<in> V &&& vert_adj x a &&& vert_adj x' a
[PROOF STEP]
using vert_adj_imp_inV
[PROOF STATE]
proof (prove)
using this:
a \<in> {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa}
vert_adj ?v1.0 ?v2.0 \<Longrightarrow> ?v1.0 \<in> V \<and> ?v2.0 \<in> V

goal (1 subgoal):
 1. (a \<in> V &&& x \<in> V) &&& x' \<in> V &&& vert_adj x a &&& vert_adj x' a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in> V
x \<in> V
x' \<in> V
vert_adj x a
vert_adj x' a

goal (1 subgoal):
 1. \<And>xa. xa \<in> {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa} \<Longrightarrow> xa \<in> f ` {p. connecting_path x x' p \<and> walk_length p = 2}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> V
x \<in> V
x' \<in> V
vert_adj x a
vert_adj x' a
[PROOF STEP]
have "is_gen_path [x, a, x']"
[PROOF STATE]
proof (prove)
using this:
a \<in> V
x \<in> V
x' \<in> V
vert_adj x a
vert_adj x' a

goal (1 subgoal):
 1. is_gen_path [x, a, x']
[PROOF STEP]
using is_walk_def vert_adj_def vert_adj_sym ha singleton_not_edge is_gen_path_def
[PROOF STATE]
proof (prove)
using this:
a \<in> V
x \<in> V
x' \<in> V
vert_adj x a
vert_adj x' a
is_walk ?xs \<equiv> set ?xs \<subseteq> V \<and> set (walk_edges ?xs) \<subseteq> E \<and> ?xs \<noteq> []
vert_adj ?v1.0 ?v2.0 \<equiv> {?v1.0, ?v2.0} \<in> E
vert_adj ?v1.0 ?v2.0 = vert_adj ?v2.0 ?v1.0
a \<in> {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa}
{?x} \<notin> E
is_gen_path ?p \<equiv> is_walk ?p \<and> (distinct (tl ?p) \<and> hd ?p = last ?p \<or> distinct ?p)

goal (1 subgoal):
 1. is_gen_path [x, a, x']
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_gen_path [x, a, x']

goal (1 subgoal):
 1. \<And>xa. xa \<in> {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa} \<Longrightarrow> xa \<in> f ` {p. connecting_path x x' p \<and> walk_length p = 2}
[PROOF STEP]
(* Slow *)
[PROOF STATE]
proof (state)
this:
is_gen_path [x, a, x']

goal (1 subgoal):
 1. \<And>xa. xa \<in> {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa} \<Longrightarrow> xa \<in> f ` {p. connecting_path x x' p \<and> walk_length p = 2}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_gen_path [x, a, x']
[PROOF STEP]
have "connecting_path x x' [x, a, x']"
[PROOF STATE]
proof (prove)
using this:
is_gen_path [x, a, x']

goal (1 subgoal):
 1. connecting_path x x' [x, a, x']
[PROOF STEP]
unfolding connecting_path_def vert_adj_def hd_conv_nth last_conv_nth
[PROOF STATE]
proof (prove)
using this:
is_gen_path [x, a, x']

goal (1 subgoal):
 1. is_gen_path [x, a, x'] \<and> hd [x, a, x'] = x \<and> last [x, a, x'] = x'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
connecting_path x x' [x, a, x']

goal (1 subgoal):
 1. \<And>xa. xa \<in> {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa} \<Longrightarrow> xa \<in> f ` {p. connecting_path x x' p \<and> walk_length p = 2}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
connecting_path x x' [x, a, x']

goal (1 subgoal):
 1. \<And>xa. xa \<in> {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa} \<Longrightarrow> xa \<in> f ` {p. connecting_path x x' p \<and> walk_length p = 2}
[PROOF STEP]
have "walk_length [x, a, x'] = 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. walk_length [x, a, x'] = 2
[PROOF STEP]
using walk_length_conv
[PROOF STATE]
proof (prove)
using this:
walk_length ?p = length ?p - 1

goal (1 subgoal):
 1. walk_length [x, a, x'] = 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
walk_length [x, a, x'] = 2

goal (1 subgoal):
 1. \<And>xa. xa \<in> {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa} \<Longrightarrow> xa \<in> f ` {p. connecting_path x x' p \<and> walk_length p = 2}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
connecting_path x x' [x, a, x']
walk_length [x, a, x'] = 2
[PROOF STEP]
show "a \<in> f ` {p. connecting_path x x' p \<and> walk_length p = 2}"
[PROOF STATE]
proof (prove)
using this:
connecting_path x x' [x, a, x']
walk_length [x, a, x'] = 2

goal (1 subgoal):
 1. a \<in> f ` {p. connecting_path x x' p \<and> walk_length p = 2}
[PROOF STEP]
using f_def
[PROOF STATE]
proof (prove)
using this:
connecting_path x x' [x, a, x']
walk_length [x, a, x'] = 2
f = (\<lambda>p. p ! 1)

goal (1 subgoal):
 1. a \<in> f ` {p. connecting_path x x' p \<and> walk_length p = 2}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
a \<in> f ` {p. connecting_path x x' p \<and> walk_length p = 2}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{xa \<in> V. vert_adj x xa \<and> vert_adj x' xa} \<subseteq> f ` {p. connecting_path x x' p \<and> walk_length p = 2}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f ` {p. connecting_path x x' p \<and> walk_length p = 2} = {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa}

goal (1 subgoal):
 1. card {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa} = card {p. connecting_path x x' p \<and> walk_length p = 2}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f ` {p. connecting_path x x' p \<and> walk_length p = 2} = {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa}
[PROOF STEP]
show "card {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa} =
    card {p. connecting_path x x' p \<and> walk_length p = 2}"
[PROOF STATE]
proof (prove)
using this:
f ` {p. connecting_path x x' p \<and> walk_length p = 2} = {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa}

goal (1 subgoal):
 1. card {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa} = card {p. connecting_path x x' p \<and> walk_length p = 2}
[PROOF STEP]
using f_inj card_image
[PROOF STATE]
proof (prove)
using this:
f ` {p. connecting_path x x' p \<and> walk_length p = 2} = {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa}
inj_on f {p. connecting_path x x' p \<and> walk_length p = 2}
inj_on ?f ?A \<Longrightarrow> card (?f ` ?A) = card ?A

goal (1 subgoal):
 1. card {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa} = card {p. connecting_path x x' p \<and> walk_length p = 2}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
card {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa} = card {p. connecting_path x x' p \<and> walk_length p = 2}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma codegree_bipartite_eq:
  "\<forall> x \<in> X. \<forall> x' \<in> X. codegree x x' = card {y \<in> Y. vert_adj x y \<and> vert_adj x' y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>X. \<forall>x'\<in>X. codegree x x' = card {y \<in> Y. vert_adj x y \<and> vert_adj x' y}
[PROOF STEP]
unfolding codegree_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>X. \<forall>x'\<in>X. card {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa} = card {y \<in> Y. vert_adj x y \<and> vert_adj x' y}
[PROOF STEP]
using vert_adj_imp_inV X_vert_adj_Y
[PROOF STATE]
proof (prove)
using this:
vert_adj ?v1.0 ?v2.0 \<Longrightarrow> ?v1.0 \<in> V \<and> ?v2.0 \<in> V
\<lbrakk>?x \<in> X; vert_adj ?x ?y\<rbrakk> \<Longrightarrow> ?y \<in> Y

goal (1 subgoal):
 1. \<forall>x\<in>X. \<forall>x'\<in>X. card {xa \<in> V. vert_adj x xa \<and> vert_adj x' xa} = card {y \<in> Y. vert_adj x y \<and> vert_adj x' y}
[PROOF STEP]
by (metis (no_types, lifting) Collect_cong)


[STATEMENT]
lemma (in fin_bipartite_graph) bipartite_deg_square_eq:
  "\<forall> y \<in> Y. (\<Sum> x' \<in> X. \<Sum> x \<in> X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (degree y)^2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y\<in>Y. (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (degree y)\<^sup>2
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. y \<in> Y \<Longrightarrow> (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (degree y)\<^sup>2
[PROOF STEP]
have hX: "finite X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite X
[PROOF STEP]
by (simp add: partitions_finite(1))
[PROOF STATE]
proof (state)
this:
finite X

goal (1 subgoal):
 1. \<And>y. y \<in> Y \<Longrightarrow> (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (degree y)\<^sup>2
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. y \<in> Y \<Longrightarrow> (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (degree y)\<^sup>2
[PROOF STEP]
assume hy: "y \<in> Y"
[PROOF STATE]
proof (state)
this:
y \<in> Y

goal (1 subgoal):
 1. \<And>y. y \<in> Y \<Longrightarrow> (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (degree y)\<^sup>2
[PROOF STEP]
have 1: "\<forall> x' \<in> X. \<forall> x \<in> X. indicator {z. vert_adj x z \<and> vert_adj x' z} y =
    indicator ({z. vert_adj x' z} \<inter> {z. vert_adj x z}) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x'\<in>X. \<forall>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y = indicator ({z. vert_adj x' z} \<inter> {z. vert_adj x z}) y
[PROOF STEP]
by (metis (mono_tags, lifting) Int_Collect indicator_simps(1) indicator_simps(2) mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
\<forall>x'\<in>X. \<forall>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y = indicator ({z. vert_adj x' z} \<inter> {z. vert_adj x z}) y

goal (1 subgoal):
 1. \<And>y. y \<in> Y \<Longrightarrow> (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (degree y)\<^sup>2
[PROOF STEP]
have 2: "\<forall> x' \<in> X. \<forall> x \<in> X. (indicator ({z. vert_adj x' z} \<inter> {z. vert_adj x z}) y:: nat) =
    indicator {z. vert_adj x' z} y * indicator {z. vert_adj x z} y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x'\<in>X. \<forall>x\<in>X. indicator ({z. vert_adj x' z} \<inter> {z. vert_adj x z}) y = indicator {z. vert_adj x' z} y * indicator {z. vert_adj x z} y
[PROOF STEP]
using indicator_inter_arith
[PROOF STATE]
proof (prove)
using this:
indicator (?A \<inter> ?B) ?x = indicator ?A ?x * indicator ?B ?x

goal (1 subgoal):
 1. \<forall>x'\<in>X. \<forall>x\<in>X. indicator ({z. vert_adj x' z} \<inter> {z. vert_adj x z}) y = indicator {z. vert_adj x' z} y * indicator {z. vert_adj x z} y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x'\<in>X. \<forall>x\<in>X. indicator ({z. vert_adj x' z} \<inter> {z. vert_adj x z}) y = indicator {z. vert_adj x' z} y * indicator {z. vert_adj x z} y

goal (1 subgoal):
 1. \<And>y. y \<in> Y \<Longrightarrow> (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (degree y)\<^sup>2
[PROOF STEP]
have "(\<Sum> x' \<in> X. \<Sum> x \<in> X. (indicator {z. vert_adj x z \<and> vert_adj x' z} y:: nat)) =
    (\<Sum> x' \<in> X. \<Sum> x \<in> X. indicator ({z. vert_adj x' z} \<inter> {z. vert_adj x z}) y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator ({z. vert_adj x' z} \<inter> {z. vert_adj x z}) y)
[PROOF STEP]
using 1 sum.cong
[PROOF STATE]
proof (prove)
using this:
\<forall>x'\<in>X. \<forall>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y = indicator ({z. vert_adj x' z} \<inter> {z. vert_adj x z}) y
\<lbrakk>?A = ?B; \<And>x. x \<in> ?B \<Longrightarrow> ?g x = ?h x\<rbrakk> \<Longrightarrow> sum ?g ?A = sum ?h ?B

goal (1 subgoal):
 1. (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator ({z. vert_adj x' z} \<inter> {z. vert_adj x z}) y)
[PROOF STEP]
by (metis (no_types, lifting))
[PROOF STATE]
proof (state)
this:
(\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator ({z. vert_adj x' z} \<inter> {z. vert_adj x z}) y)

goal (1 subgoal):
 1. \<And>y. y \<in> Y \<Longrightarrow> (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (degree y)\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator ({z. vert_adj x' z} \<inter> {z. vert_adj x z}) y)

goal (1 subgoal):
 1. \<And>y. y \<in> Y \<Longrightarrow> (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (degree y)\<^sup>2
[PROOF STEP]
have "... = (\<Sum> x' \<in> X. \<Sum> x \<in> X. indicator {z. vert_adj x' z} y *
    indicator {z. vert_adj x z} y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator ({z. vert_adj x' z} \<inter> {z. vert_adj x z}) y) = (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x' z} y * indicator {z. vert_adj x z} y)
[PROOF STEP]
using 2 sum.cong
[PROOF STATE]
proof (prove)
using this:
\<forall>x'\<in>X. \<forall>x\<in>X. indicator ({z. vert_adj x' z} \<inter> {z. vert_adj x z}) y = indicator {z. vert_adj x' z} y * indicator {z. vert_adj x z} y
\<lbrakk>?A = ?B; \<And>x. x \<in> ?B \<Longrightarrow> ?g x = ?h x\<rbrakk> \<Longrightarrow> sum ?g ?A = sum ?h ?B

goal (1 subgoal):
 1. (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator ({z. vert_adj x' z} \<inter> {z. vert_adj x z}) y) = (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x' z} y * indicator {z. vert_adj x z} y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator ({z. vert_adj x' z} \<inter> {z. vert_adj x z}) y) = (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x' z} y * indicator {z. vert_adj x z} y)

goal (1 subgoal):
 1. \<And>y. y \<in> Y \<Longrightarrow> (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (degree y)\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator ({z. vert_adj x' z} \<inter> {z. vert_adj x z}) y) = (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x' z} y * indicator {z. vert_adj x z} y)

goal (1 subgoal):
 1. \<And>y. y \<in> Y \<Longrightarrow> (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (degree y)\<^sup>2
[PROOF STEP]
have "... = sum (\<lambda> x. indicator {z. vert_adj x z} y) X * sum (\<lambda> x. indicator {z. vert_adj x z} y) X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x' z} y * indicator {z. vert_adj x z} y) = (\<Sum>x\<in>X. indicator {z. vert_adj x z} y) * (\<Sum>x\<in>X. indicator {z. vert_adj x z} y)
[PROOF STEP]
using sum_product[of "(\<lambda> x. (indicator {z. vert_adj x z} y:: nat))" "X"
      "(\<lambda> x. indicator {z. vert_adj x z} y)" "X"]
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x\<in>X. indicator {z. vert_adj x z} y) * (\<Sum>x\<in>X. indicator {z. vert_adj x z} y) = (\<Sum>i\<in>X. \<Sum>j\<in>X. indicator {z. vert_adj i z} y * indicator {z. vert_adj j z} y)

goal (1 subgoal):
 1. (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x' z} y * indicator {z. vert_adj x z} y) = (\<Sum>x\<in>X. indicator {z. vert_adj x z} y) * (\<Sum>x\<in>X. indicator {z. vert_adj x z} y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x' z} y * indicator {z. vert_adj x z} y) = (\<Sum>x\<in>X. indicator {z. vert_adj x z} y) * (\<Sum>x\<in>X. indicator {z. vert_adj x z} y)

goal (1 subgoal):
 1. \<And>y. y \<in> Y \<Longrightarrow> (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (degree y)\<^sup>2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (\<Sum>x\<in>X. indicator {z. vert_adj x z} y) * (\<Sum>x\<in>X. indicator {z. vert_adj x z} y)
[PROOF STEP]
have 3: "(\<Sum> x' \<in> X. \<Sum> x \<in> X. (indicator {z. vert_adj x z \<and> vert_adj x' z} y:: nat)) =
    (sum (\<lambda> x. indicator {z. vert_adj x z} y) X) ^ 2"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (\<Sum>x\<in>X. indicator {z. vert_adj x z} y) * (\<Sum>x\<in>X. indicator {z. vert_adj x z} y)

goal (1 subgoal):
 1. (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (\<Sum>x\<in>X. indicator {z. vert_adj x z} y)\<^sup>2
[PROOF STEP]
using power2_eq_square
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (\<Sum>x\<in>X. indicator {z. vert_adj x z} y) * (\<Sum>x\<in>X. indicator {z. vert_adj x z} y)
?a\<^sup>2 = ?a * ?a

goal (1 subgoal):
 1. (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (\<Sum>x\<in>X. indicator {z. vert_adj x z} y)\<^sup>2
[PROOF STEP]
by (metis (no_types, lifting))
[PROOF STATE]
proof (state)
this:
(\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (\<Sum>x\<in>X. indicator {z. vert_adj x z} y)\<^sup>2

goal (1 subgoal):
 1. \<And>y. y \<in> Y \<Longrightarrow> (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (degree y)\<^sup>2
[PROOF STEP]
have "\<forall> x \<in> X. indicator {z. vert_adj x z} y = indicator {x. vert_adj x y} x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>X. indicator {z. vert_adj x z} y = indicator {x. vert_adj x y} x
[PROOF STEP]
by (simp add: indicator_def)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>X. indicator {z. vert_adj x z} y = indicator {x. vert_adj x y} x

goal (1 subgoal):
 1. \<And>y. y \<in> Y \<Longrightarrow> (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (degree y)\<^sup>2
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>X. indicator {z. vert_adj x z} y = indicator {x. vert_adj x y} x
[PROOF STEP]
have "(sum (\<lambda> x. indicator {z. vert_adj x z} y) X) = sum (\<lambda> x. indicator {x. vert_adj x y} x) X"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>X. indicator {z. vert_adj x z} y = indicator {x. vert_adj x y} x

goal (1 subgoal):
 1. (\<Sum>x\<in>X. indicator {z. vert_adj x z} y) = sum (indicator {x. vert_adj x y}) X
[PROOF STEP]
using sum.cong
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>X. indicator {z. vert_adj x z} y = indicator {x. vert_adj x y} x
\<lbrakk>?A = ?B; \<And>x. x \<in> ?B \<Longrightarrow> ?g x = ?h x\<rbrakk> \<Longrightarrow> sum ?g ?A = sum ?h ?B

goal (1 subgoal):
 1. (\<Sum>x\<in>X. indicator {z. vert_adj x z} y) = sum (indicator {x. vert_adj x y}) X
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>X. indicator {z. vert_adj x z} y) = sum (indicator {x. vert_adj x y}) X

goal (1 subgoal):
 1. \<And>y. y \<in> Y \<Longrightarrow> (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (degree y)\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>X. indicator {z. vert_adj x z} y) = sum (indicator {x. vert_adj x y}) X

goal (1 subgoal):
 1. \<And>y. y \<in> Y \<Longrightarrow> (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (degree y)\<^sup>2
[PROOF STEP]
have "... = card ({x \<in> X. vert_adj x y})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (indicator {x. vert_adj x y}) X = card {x \<in> X. vert_adj x y}
[PROOF STEP]
using sum_indicator_eq_card hX
[PROOF STATE]
proof (prove)
using this:
finite ?A \<Longrightarrow> sum (indicator ?B) ?A = card (?A \<inter> ?B)
finite X

goal (1 subgoal):
 1. sum (indicator {x. vert_adj x y}) X = card {x \<in> X. vert_adj x y}
[PROOF STEP]
by (metis Collect_conj_eq Collect_mem_eq)
[PROOF STATE]
proof (state)
this:
sum (indicator {x. vert_adj x y}) X = card {x \<in> X. vert_adj x y}

goal (1 subgoal):
 1. \<And>y. y \<in> Y \<Longrightarrow> (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (degree y)\<^sup>2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>x\<in>X. indicator {z. vert_adj x z} y) = card {x \<in> X. vert_adj x y}
[PROOF STEP]
show "(\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (degree y)^2"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x\<in>X. indicator {z. vert_adj x z} y) = card {x \<in> X. vert_adj x y}

goal (1 subgoal):
 1. (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (degree y)\<^sup>2
[PROOF STEP]
using 3 hy degree_neighbors_ssY neighbors_ss_def vert_adj_sym
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x\<in>X. indicator {z. vert_adj x z} y) = card {x \<in> X. vert_adj x y}
(\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (\<Sum>x\<in>X. indicator {z. vert_adj x z} y)\<^sup>2
y \<in> Y
?v \<in> Y \<Longrightarrow> degree ?v = card (neighbors_ss ?v X)
neighbors_ss ?x ?Y \<equiv> {y \<in> ?Y. vert_adj ?x y}
vert_adj ?v1.0 ?v2.0 = vert_adj ?v2.0 ?v1.0

goal (1 subgoal):
 1. (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (degree y)\<^sup>2
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
(\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (degree y)\<^sup>2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in fin_bipartite_graph) codegree_degree:
  "(\<Sum> x' \<in> X. \<Sum> x \<in> X. (codegree x x')) = (\<Sum> y \<in> Y. (degree y)^2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x'\<in>X. \<Sum>x\<in>X. codegree x x') = (\<Sum>y\<in>Y. (degree y)\<^sup>2)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>x'\<in>X. \<Sum>x\<in>X. codegree x x') = (\<Sum>y\<in>Y. (degree y)\<^sup>2)
[PROOF STEP]
have hX: "finite X" and hY: "finite Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite X &&& finite Y
[PROOF STEP]
by (simp_all add: partitions_finite)
[PROOF STATE]
proof (state)
this:
finite X
finite Y

goal (1 subgoal):
 1. (\<Sum>x'\<in>X. \<Sum>x\<in>X. codegree x x') = (\<Sum>y\<in>Y. (degree y)\<^sup>2)
[PROOF STEP]
have "\<forall> x' \<in> X. \<forall> x \<in> X. {z \<in> V. vert_adj x z \<and> vert_adj x' z} = Y \<inter> {z. vert_adj x z \<and> vert_adj x' z}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x'\<in>X. \<forall>x\<in>X. {z \<in> V. vert_adj x z \<and> vert_adj x' z} = Y \<inter> {z. vert_adj x z \<and> vert_adj x' z}
[PROOF STEP]
using XY_union X_vert_adj_Y
[PROOF STATE]
proof (prove)
using this:
X \<union> Y = V
\<lbrakk>?x \<in> X; vert_adj ?x ?y\<rbrakk> \<Longrightarrow> ?y \<in> Y

goal (1 subgoal):
 1. \<forall>x'\<in>X. \<forall>x\<in>X. {z \<in> V. vert_adj x z \<and> vert_adj x' z} = Y \<inter> {z. vert_adj x z \<and> vert_adj x' z}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>x'\<in>X. \<forall>x\<in>X. {z \<in> V. vert_adj x z \<and> vert_adj x' z} = Y \<inter> {z. vert_adj x z \<and> vert_adj x' z}

goal (1 subgoal):
 1. (\<Sum>x'\<in>X. \<Sum>x\<in>X. codegree x x') = (\<Sum>y\<in>Y. (degree y)\<^sup>2)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<forall>x'\<in>X. \<forall>x\<in>X. {z \<in> V. vert_adj x z \<and> vert_adj x' z} = Y \<inter> {z. vert_adj x z \<and> vert_adj x' z}
[PROOF STEP]
have "(\<Sum> x' \<in> X. \<Sum> x \<in> X. (codegree x x')) = (\<Sum> x' \<in> X. \<Sum> x \<in> X. card (Y \<inter> {z. vert_adj x z \<and> vert_adj x' z}))"
[PROOF STATE]
proof (prove)
using this:
\<forall>x'\<in>X. \<forall>x\<in>X. {z \<in> V. vert_adj x z \<and> vert_adj x' z} = Y \<inter> {z. vert_adj x z \<and> vert_adj x' z}

goal (1 subgoal):
 1. (\<Sum>x'\<in>X. \<Sum>x\<in>X. codegree x x') = (\<Sum>x'\<in>X. \<Sum>x\<in>X. card (Y \<inter> {z. vert_adj x z \<and> vert_adj x' z}))
[PROOF STEP]
using codegree_def sum.cong
[PROOF STATE]
proof (prove)
using this:
\<forall>x'\<in>X. \<forall>x\<in>X. {z \<in> V. vert_adj x z \<and> vert_adj x' z} = Y \<inter> {z. vert_adj x z \<and> vert_adj x' z}
codegree ?v ?u \<equiv> card {x \<in> V. vert_adj ?v x \<and> vert_adj ?u x}
\<lbrakk>?A = ?B; \<And>x. x \<in> ?B \<Longrightarrow> ?g x = ?h x\<rbrakk> \<Longrightarrow> sum ?g ?A = sum ?h ?B

goal (1 subgoal):
 1. (\<Sum>x'\<in>X. \<Sum>x\<in>X. codegree x x') = (\<Sum>x'\<in>X. \<Sum>x\<in>X. card (Y \<inter> {z. vert_adj x z \<and> vert_adj x' z}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x'\<in>X. \<Sum>x\<in>X. codegree x x') = (\<Sum>x'\<in>X. \<Sum>x\<in>X. card (Y \<inter> {z. vert_adj x z \<and> vert_adj x' z}))

goal (1 subgoal):
 1. (\<Sum>x'\<in>X. \<Sum>x\<in>X. codegree x x') = (\<Sum>y\<in>Y. (degree y)\<^sup>2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x'\<in>X. \<Sum>x\<in>X. codegree x x') = (\<Sum>x'\<in>X. \<Sum>x\<in>X. card (Y \<inter> {z. vert_adj x z \<and> vert_adj x' z}))

goal (1 subgoal):
 1. (\<Sum>x'\<in>X. \<Sum>x\<in>X. codegree x x') = (\<Sum>y\<in>Y. (degree y)\<^sup>2)
[PROOF STEP]
have "... = (\<Sum> x' \<in> X. \<Sum> x \<in> X. \<Sum> y \<in> Y. indicator {z. vert_adj x z \<and> vert_adj x' z} y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x'\<in>X. \<Sum>x\<in>X. card (Y \<inter> {z. vert_adj x z \<and> vert_adj x' z})) = (\<Sum>x'\<in>X. \<Sum>x\<in>X. sum (indicator {z. vert_adj x z \<and> vert_adj x' z}) Y)
[PROOF STEP]
using sum_indicator_eq_card hY
[PROOF STATE]
proof (prove)
using this:
finite ?A \<Longrightarrow> sum (indicator ?B) ?A = card (?A \<inter> ?B)
finite Y

goal (1 subgoal):
 1. (\<Sum>x'\<in>X. \<Sum>x\<in>X. card (Y \<inter> {z. vert_adj x z \<and> vert_adj x' z})) = (\<Sum>x'\<in>X. \<Sum>x\<in>X. sum (indicator {z. vert_adj x z \<and> vert_adj x' z}) Y)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(\<Sum>x'\<in>X. \<Sum>x\<in>X. card (Y \<inter> {z. vert_adj x z \<and> vert_adj x' z})) = (\<Sum>x'\<in>X. \<Sum>x\<in>X. sum (indicator {z. vert_adj x z \<and> vert_adj x' z}) Y)

goal (1 subgoal):
 1. (\<Sum>x'\<in>X. \<Sum>x\<in>X. codegree x x') = (\<Sum>y\<in>Y. (degree y)\<^sup>2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x'\<in>X. \<Sum>x\<in>X. card (Y \<inter> {z. vert_adj x z \<and> vert_adj x' z})) = (\<Sum>x'\<in>X. \<Sum>x\<in>X. sum (indicator {z. vert_adj x z \<and> vert_adj x' z}) Y)

goal (1 subgoal):
 1. (\<Sum>x'\<in>X. \<Sum>x\<in>X. codegree x x') = (\<Sum>y\<in>Y. (degree y)\<^sup>2)
[PROOF STEP]
have "... =  (\<Sum> x' \<in> X. \<Sum> y \<in> Y. (\<Sum> x \<in> X. indicator {z. vert_adj x z \<and> vert_adj x' z} y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x'\<in>X. \<Sum>x\<in>X. sum (indicator {z. vert_adj x z \<and> vert_adj x' z}) Y) = (\<Sum>x'\<in>X. \<Sum>y\<in>Y. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y)
[PROOF STEP]
using sum.swap
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>?A. sum (?g i) ?B) = (\<Sum>j\<in>?B. \<Sum>i\<in>?A. ?g i j)

goal (1 subgoal):
 1. (\<Sum>x'\<in>X. \<Sum>x\<in>X. sum (indicator {z. vert_adj x z \<and> vert_adj x' z}) Y) = (\<Sum>x'\<in>X. \<Sum>y\<in>Y. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y)
[PROOF STEP]
by (metis (no_types))
[PROOF STATE]
proof (state)
this:
(\<Sum>x'\<in>X. \<Sum>x\<in>X. sum (indicator {z. vert_adj x z \<and> vert_adj x' z}) Y) = (\<Sum>x'\<in>X. \<Sum>y\<in>Y. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y)

goal (1 subgoal):
 1. (\<Sum>x'\<in>X. \<Sum>x\<in>X. codegree x x') = (\<Sum>y\<in>Y. (degree y)\<^sup>2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x'\<in>X. \<Sum>x\<in>X. sum (indicator {z. vert_adj x z \<and> vert_adj x' z}) Y) = (\<Sum>x'\<in>X. \<Sum>y\<in>Y. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y)

goal (1 subgoal):
 1. (\<Sum>x'\<in>X. \<Sum>x\<in>X. codegree x x') = (\<Sum>y\<in>Y. (degree y)\<^sup>2)
[PROOF STEP]
have "... = (\<Sum> y \<in> Y. \<Sum> x' \<in> X. (\<Sum> x \<in> X. indicator {z. vert_adj x z \<and> vert_adj x' z} y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x'\<in>X. \<Sum>y\<in>Y. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (\<Sum>y\<in>Y. \<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y)
[PROOF STEP]
using sum.swap
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>?A. sum (?g i) ?B) = (\<Sum>j\<in>?B. \<Sum>i\<in>?A. ?g i j)

goal (1 subgoal):
 1. (\<Sum>x'\<in>X. \<Sum>y\<in>Y. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (\<Sum>y\<in>Y. \<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(\<Sum>x'\<in>X. \<Sum>y\<in>Y. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (\<Sum>y\<in>Y. \<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y)

goal (1 subgoal):
 1. (\<Sum>x'\<in>X. \<Sum>x\<in>X. codegree x x') = (\<Sum>y\<in>Y. (degree y)\<^sup>2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x'\<in>X. \<Sum>y\<in>Y. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (\<Sum>y\<in>Y. \<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y)

goal (1 subgoal):
 1. (\<Sum>x'\<in>X. \<Sum>x\<in>X. codegree x x') = (\<Sum>y\<in>Y. (degree y)\<^sup>2)
[PROOF STEP]
have "... = (\<Sum> y \<in> Y. (degree y)^2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>y\<in>Y. \<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (\<Sum>y\<in>Y. (degree y)\<^sup>2)
[PROOF STEP]
using bipartite_deg_square_eq sum.cong
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<in>Y. (\<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (degree y)\<^sup>2
\<lbrakk>?A = ?B; \<And>x. x \<in> ?B \<Longrightarrow> ?g x = ?h x\<rbrakk> \<Longrightarrow> sum ?g ?A = sum ?h ?B

goal (1 subgoal):
 1. (\<Sum>y\<in>Y. \<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (\<Sum>y\<in>Y. (degree y)\<^sup>2)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<Sum>y\<in>Y. \<Sum>x'\<in>X. \<Sum>x\<in>X. indicator {z. vert_adj x z \<and> vert_adj x' z} y) = (\<Sum>y\<in>Y. (degree y)\<^sup>2)

goal (1 subgoal):
 1. (\<Sum>x'\<in>X. \<Sum>x\<in>X. codegree x x') = (\<Sum>y\<in>Y. (degree y)\<^sup>2)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>x'\<in>X. \<Sum>x\<in>X. codegree x x') = (\<Sum>y\<in>Y. (degree y)\<^sup>2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x'\<in>X. \<Sum>x\<in>X. codegree x x') = (\<Sum>y\<in>Y. (degree y)\<^sup>2)

goal (1 subgoal):
 1. (\<Sum>x'\<in>X. \<Sum>x\<in>X. codegree x x') = (\<Sum>y\<in>Y. (degree y)\<^sup>2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>x'\<in>X. \<Sum>x\<in>X. codegree x x') = (\<Sum>y\<in>Y. (degree y)\<^sup>2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in fin_bipartite_graph) sum_degree_normalized_X_density:
  "(\<Sum> x \<in> X. degree_normalized x Y) / card X = edge_density X Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>X. degree_normalized x Y) / real (card X) = local.density
[PROOF STEP]
by (smt (z3) card_all_edges_betw_neighbor card_edges_between_set degree_normalized_def
    divide_divide_eq_left' density_simp of_nat_mult of_nat_sum partitions_finite(1)
    partitions_finite(2) sum.cong sum_left_div_distrib)


[STATEMENT]
lemma (in fin_bipartite_graph) sum_degree_normalized_Y_density:
  "(\<Sum> y \<in> Y. degree_normalized y X) / card Y = edge_density X Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>y\<in>Y. degree_normalized y X) / real (card Y) = local.density
[PROOF STEP]
using bipartite_sym fin_bipartite_graph.sum_degree_normalized_X_density fin_bipartite_graph_def
    fin_graph_system_axioms edge_density_commute
[PROOF STATE]
proof (prove)
using this:
bipartite_graph V E Y X
fin_bipartite_graph ?vertices ?edges ?X ?Y \<Longrightarrow> (\<Sum>x\<in>?X. ulgraph.degree_normalized ?edges x ?Y) / real (card ?X) = ulgraph.edge_density ?edges ?X ?Y
fin_bipartite_graph ?vertices ?edges ?X ?Y \<equiv> bipartite_graph ?vertices ?edges ?X ?Y \<and> fin_graph_system ?vertices ?edges
fin_graph_system V E
edge_density ?X ?Y = edge_density ?Y ?X

goal (1 subgoal):
 1. (\<Sum>y\<in>Y. degree_normalized y X) / real (card Y) = local.density
[PROOF STEP]
by fastforce


[STATEMENT]
lemma find_path_ex_rule:
    assumes "finite U0"
    assumes "finite (E\<^sup>*``U0)"
    assumes "\<exists>v\<in>E\<^sup>*``U0. P v"
    shows "find_path E U0 P \<le> SPEC (\<lambda>r.
      \<exists>p v. r = Some (p,v) \<and> P v \<and> (\<forall>v\<in>set p. \<not>P v) \<and> (\<exists>u0\<in>U0. path E u0 p v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_path E U0 P \<le> SPEC (\<lambda>r. \<exists>p v. r = Some (p, v) \<and> P v \<and> (\<forall>v\<in>set p. \<not> P v) \<and> (\<exists>u0\<in>U0. path E u0 p v))
[PROOF STEP]
unfolding find_path_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ASSERT (finite U0) \<bind> (\<lambda>_. ASSERT (finite (E\<^sup>* `` U0)) \<bind> (\<lambda>_. SPEC (\<lambda>p. case p of None \<Rightarrow> \<forall>u0\<in>U0. \<forall>v\<in>E\<^sup>* `` {u0}. \<not> P v | Some (p, v) \<Rightarrow> \<exists>u0\<in>U0. path E u0 p v \<and> P v \<and> (\<forall>v\<in>set p. \<not> P v)))) \<le> SPEC (\<lambda>r. \<exists>p v. r = Some (p, v) \<and> P v \<and> (\<forall>v\<in>set p. \<not> P v) \<and> (\<exists>u0\<in>U0. path E u0 p v))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite U0
finite (E\<^sup>* `` U0)
\<exists>v\<in>E\<^sup>* `` U0. P v

goal (1 subgoal):
 1. ASSERT (finite U0) \<bind> (\<lambda>_. ASSERT (finite (E\<^sup>* `` U0)) \<bind> (\<lambda>_. SPEC (\<lambda>p. case p of None \<Rightarrow> \<forall>u0\<in>U0. \<forall>v\<in>E\<^sup>* `` {u0}. \<not> P v | Some (p, v) \<Rightarrow> \<exists>u0\<in>U0. path E u0 p v \<and> P v \<and> (\<forall>v\<in>set p. \<not> P v)))) \<le> SPEC (\<lambda>r. \<exists>p v. r = Some (p, v) \<and> P v \<and> (\<forall>v\<in>set p. \<not> P v) \<and> (\<exists>u0\<in>U0. path E u0 p v))
[PROOF STEP]
by (fastforce split: option.splits)


[STATEMENT]
lemma (in -) find_path1_ex_rule:
    assumes "finite (E\<^sup>*``{u0})"
    assumes "\<exists>v\<in>E\<^sup>+``{u0}. P v"
    shows "find_path1 E u0 P \<le> SPEC (\<lambda>r.
      \<exists>p v. r = Some (p,v) \<and> p\<noteq>[] \<and> P v \<and> path E u0 p v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_path1 E u0 P \<le> SPEC (\<lambda>r. \<exists>p v. r = Some (p, v) \<and> p \<noteq> [] \<and> P v \<and> path E u0 p v)
[PROOF STEP]
unfolding find_path1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ASSERT (finite (E\<^sup>* `` {u0})) \<bind> (\<lambda>_. SPEC (\<lambda>p. case p of None \<Rightarrow> \<forall>v\<in>E\<^sup>+ `` {u0}. \<not> P v | Some (p, v) \<Rightarrow> path E u0 p v \<and> P v \<and> p \<noteq> [])) \<le> SPEC (\<lambda>r. \<exists>p v. r = Some (p, v) \<and> p \<noteq> [] \<and> P v \<and> path E u0 p v)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite (E\<^sup>* `` {u0})
\<exists>v\<in>E\<^sup>+ `` {u0}. P v

goal (1 subgoal):
 1. ASSERT (finite (E\<^sup>* `` {u0})) \<bind> (\<lambda>_. SPEC (\<lambda>p. case p of None \<Rightarrow> \<forall>v\<in>E\<^sup>+ `` {u0}. \<not> P v | Some (p, v) \<Rightarrow> path E u0 p v \<and> P v \<and> p \<noteq> [])) \<le> SPEC (\<lambda>r. \<exists>p v. r = Some (p, v) \<and> p \<noteq> [] \<and> P v \<and> path E u0 p v)
[PROOF STEP]
by (fastforce split: option.splits)


[STATEMENT]
lemma list_reversal:
  "PRE (\<lambda>s :: 'a state. List (projr (s ''h'')) (projl (s ''p'')) Ps
        \<and> List (projr (s ''h'')) (projl (s ''q'')) Qs
        \<and> set Ps \<inter> set Qs = {})
    (WHILE (\<lambda>s. projl (s ''p'') \<noteq> Null)
     INV (\<lambda>s. \<exists>ps qs. List (projr (s ''h'')) (projl (s ''p'')) ps
              \<and> List (projr (s ''h'')) (projl (s ''q'')) qs
              \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs)
     DO
      (''r'' ::= (\<lambda>s. s ''p''));
      (''p'' ::= (\<lambda>s. Inl (projr (s ''h'') (addr (projl (s ''p''))))) );
      (''h'' ::= (\<lambda>s. Inr ((projr (s ''h''))(addr (projl (s ''r'')) := projl (s ''q''))) ));
      (''q'' ::= (\<lambda>s. s ''r''))
     OD)
  POST (\<lambda>s. List (projr (s ''h'')) (projl (s ''q'')) (rev Ps @ Qs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rdom \<lceil>\<lambda>s. List (projr (s ''h'')) (projl (s ''p'')) Ps \<and> List (projr (s ''h'')) (projl (s ''q'')) Qs \<and> set Ps \<inter> set Qs = {}\<rceil> \<subseteq> wp (WHILE (\<lambda>s. projl (s ''p'') \<noteq> Null) INV (\<lambda>s. \<exists>ps qs. List (projr (s ''h'')) (projl (s ''p'')) ps \<and> List (projr (s ''h'')) (projl (s ''q'')) qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs) DO (''r'' ::= (\<lambda>s. s ''p'')) ; (''p'' ::= (\<lambda>s. Inl (projr (s ''h'') (addr (projl (s ''p'')))))) ; (''h'' ::= (\<lambda>s. Inr ((projr (s ''h''))(addr (projl (s ''r'')) := projl (s ''q''))))) ; (''q'' ::= (\<lambda>s. s ''r'')) OD) \<lceil>\<lambda>s. List (projr (s ''h'')) (projl (s ''q'')) (rev Ps @ Qs)\<rceil>
[PROOF STEP]
apply hoare
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. rdom \<lceil>\<lambda>s. List (projr (s ''h'')) (projl (s ''p'')) Ps \<and> List (projr (s ''h'')) (projl (s ''q'')) Qs \<and> set Ps \<inter> set Qs = {}\<rceil> \<subseteq> rdom \<lceil>\<lambda>s. \<exists>ps qs. List (projr (s ''h'')) (projl (s ''p'')) ps \<and> List (projr (s ''h'')) (projl (s ''q'')) qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs\<rceil>
 2. rdom \<lceil>\<lambda>s. \<exists>ps qs. List (projr (s ''h'')) (projl (s ''p'')) ps \<and> List (projr (s ''h'')) (projl (s ''q'')) qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs\<rceil> ; rel_ad \<lceil>\<lambda>s. projl (s ''p'') \<noteq> Null\<rceil> \<subseteq> rdom \<lceil>\<lambda>s. List (projr (s ''h'')) (projl (s ''q'')) (rev Ps @ Qs)\<rceil>
 3. rdom \<lceil>\<lambda>s. \<exists>ps qs. List (projr (s ''h'')) (projl (s ''p'')) ps \<and> List (projr (s ''h'')) (projl (s ''q'')) qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs\<rceil> ; rdom \<lceil>\<lambda>s. projl (s ''p'') \<noteq> Null\<rceil> \<subseteq> wp (''r'' ::= (\<lambda>s. s ''p'')) (wp (''p'' ::= (\<lambda>s. Inl (projr (s ''h'') (addr (projl (s ''p'')))))) (wp (''h'' ::= (\<lambda>s. Inr ((projr (s ''h''))(addr (projl (s ''r'')) := projl (s ''q''))))) (wp (''q'' ::= (\<lambda>s. s ''r'')) \<lceil>\<lambda>s. \<exists>ps qs. List (projr (s ''h'')) (projl (s ''p'')) ps \<and> List (projr (s ''h'')) (projl (s ''q'')) qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs\<rceil>)))
[PROOF STEP]
apply auto[2]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rdom \<lceil>\<lambda>s. \<exists>ps qs. List (projr (s ''h'')) (projl (s ''p'')) ps \<and> List (projr (s ''h'')) (projl (s ''q'')) qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs\<rceil> ; rdom \<lceil>\<lambda>s. projl (s ''p'') \<noteq> Null\<rceil> \<subseteq> wp (''r'' ::= (\<lambda>s. s ''p'')) (wp (''p'' ::= (\<lambda>s. Inl (projr (s ''h'') (addr (projl (s ''p'')))))) (wp (''h'' ::= (\<lambda>s. Inr ((projr (s ''h''))(addr (projl (s ''r'')) := projl (s ''q''))))) (wp (''q'' ::= (\<lambda>s. s ''r'')) \<lceil>\<lambda>s. \<exists>ps qs. List (projr (s ''h'')) (projl (s ''p'')) ps \<and> List (projr (s ''h'')) (projl (s ''q'')) qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs\<rceil>)))
[PROOF STEP]
by (clarsimp, fastforce intro: notin_List_update[THEN iffD2])


[STATEMENT]
lemma projection_on_union:
  "l \<upharpoonleft> Y = [] \<Longrightarrow> l \<upharpoonleft> (X \<union> Y) = l \<upharpoonleft> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<upharpoonleft> Y = [] \<Longrightarrow> l \<upharpoonleft> (X \<union> Y) = l \<upharpoonleft> X
[PROOF STEP]
proof (induct l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. [] \<upharpoonleft> Y = [] \<Longrightarrow> [] \<upharpoonleft> (X \<union> Y) = [] \<upharpoonleft> X
 2. \<And>a l. \<lbrakk>l \<upharpoonleft> Y = [] \<Longrightarrow> l \<upharpoonleft> (X \<union> Y) = l \<upharpoonleft> X; (a # l) \<upharpoonleft> Y = []\<rbrakk> \<Longrightarrow> (a # l) \<upharpoonleft> (X \<union> Y) = (a # l) \<upharpoonleft> X
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
[] \<upharpoonleft> Y = []

goal (2 subgoals):
 1. [] \<upharpoonleft> Y = [] \<Longrightarrow> [] \<upharpoonleft> (X \<union> Y) = [] \<upharpoonleft> X
 2. \<And>a l. \<lbrakk>l \<upharpoonleft> Y = [] \<Longrightarrow> l \<upharpoonleft> (X \<union> Y) = l \<upharpoonleft> X; (a # l) \<upharpoonleft> Y = []\<rbrakk> \<Longrightarrow> (a # l) \<upharpoonleft> (X \<union> Y) = (a # l) \<upharpoonleft> X
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] \<upharpoonleft> (X \<union> Y) = [] \<upharpoonleft> X
[PROOF STEP]
by (simp add: projection_def)
[PROOF STATE]
proof (state)
this:
[] \<upharpoonleft> (X \<union> Y) = [] \<upharpoonleft> X

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<upharpoonleft> Y = [] \<Longrightarrow> l \<upharpoonleft> (X \<union> Y) = l \<upharpoonleft> X; (a # l) \<upharpoonleft> Y = []\<rbrakk> \<Longrightarrow> (a # l) \<upharpoonleft> (X \<union> Y) = (a # l) \<upharpoonleft> X
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<upharpoonleft> Y = [] \<Longrightarrow> l \<upharpoonleft> (X \<union> Y) = l \<upharpoonleft> X; (a # l) \<upharpoonleft> Y = []\<rbrakk> \<Longrightarrow> (a # l) \<upharpoonleft> (X \<union> Y) = (a # l) \<upharpoonleft> X
[PROOF STEP]
case (Cons a b)
[PROOF STATE]
proof (state)
this:
b \<upharpoonleft> Y = [] \<Longrightarrow> b \<upharpoonleft> (X \<union> Y) = b \<upharpoonleft> X
(a # b) \<upharpoonleft> Y = []

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<upharpoonleft> Y = [] \<Longrightarrow> l \<upharpoonleft> (X \<union> Y) = l \<upharpoonleft> X; (a # l) \<upharpoonleft> Y = []\<rbrakk> \<Longrightarrow> (a # l) \<upharpoonleft> (X \<union> Y) = (a # l) \<upharpoonleft> X
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a # b) \<upharpoonleft> (X \<union> Y) = (a # b) \<upharpoonleft> X
[PROOF STEP]
proof (cases "a \<in> Y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<in> Y \<Longrightarrow> (a # b) \<upharpoonleft> (X \<union> Y) = (a # b) \<upharpoonleft> X
 2. a \<notin> Y \<Longrightarrow> (a # b) \<upharpoonleft> (X \<union> Y) = (a # b) \<upharpoonleft> X
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a \<in> Y

goal (2 subgoals):
 1. a \<in> Y \<Longrightarrow> (a # b) \<upharpoonleft> (X \<union> Y) = (a # b) \<upharpoonleft> X
 2. a \<notin> Y \<Longrightarrow> (a # b) \<upharpoonleft> (X \<union> Y) = (a # b) \<upharpoonleft> X
[PROOF STEP]
from Cons
[PROOF STATE]
proof (chain)
picking this:
b \<upharpoonleft> Y = [] \<Longrightarrow> b \<upharpoonleft> (X \<union> Y) = b \<upharpoonleft> X
(a # b) \<upharpoonleft> Y = []
[PROOF STEP]
show "a \<in> Y \<Longrightarrow> (a # b) \<upharpoonleft> (X \<union> Y) = (a # b) \<upharpoonleft> X"
[PROOF STATE]
proof (prove)
using this:
b \<upharpoonleft> Y = [] \<Longrightarrow> b \<upharpoonleft> (X \<union> Y) = b \<upharpoonleft> X
(a # b) \<upharpoonleft> Y = []

goal (1 subgoal):
 1. a \<in> Y \<Longrightarrow> (a # b) \<upharpoonleft> (X \<union> Y) = (a # b) \<upharpoonleft> X
[PROOF STEP]
by (simp add: projection_def)
[PROOF STATE]
proof (state)
this:
a \<in> Y \<Longrightarrow> (a # b) \<upharpoonleft> (X \<union> Y) = (a # b) \<upharpoonleft> X

goal (1 subgoal):
 1. a \<notin> Y \<Longrightarrow> (a # b) \<upharpoonleft> (X \<union> Y) = (a # b) \<upharpoonleft> X
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<notin> Y \<Longrightarrow> (a # b) \<upharpoonleft> (X \<union> Y) = (a # b) \<upharpoonleft> X
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<notin> Y

goal (1 subgoal):
 1. a \<notin> Y \<Longrightarrow> (a # b) \<upharpoonleft> (X \<union> Y) = (a # b) \<upharpoonleft> X
[PROOF STEP]
from Cons
[PROOF STATE]
proof (chain)
picking this:
b \<upharpoonleft> Y = [] \<Longrightarrow> b \<upharpoonleft> (X \<union> Y) = b \<upharpoonleft> X
(a # b) \<upharpoonleft> Y = []
[PROOF STEP]
show "a \<notin> Y \<Longrightarrow> (a # b) \<upharpoonleft> (X \<union> Y) = (a # b) \<upharpoonleft> X"
[PROOF STATE]
proof (prove)
using this:
b \<upharpoonleft> Y = [] \<Longrightarrow> b \<upharpoonleft> (X \<union> Y) = b \<upharpoonleft> X
(a # b) \<upharpoonleft> Y = []

goal (1 subgoal):
 1. a \<notin> Y \<Longrightarrow> (a # b) \<upharpoonleft> (X \<union> Y) = (a # b) \<upharpoonleft> X
[PROOF STEP]
by (simp add: projection_def)
[PROOF STATE]
proof (state)
this:
a \<notin> Y \<Longrightarrow> (a # b) \<upharpoonleft> (X \<union> Y) = (a # b) \<upharpoonleft> X

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(a # b) \<upharpoonleft> (X \<union> Y) = (a # b) \<upharpoonleft> X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma projection_on_empty_trace: "[] \<upharpoonleft> X =[]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] \<upharpoonleft> X = []
[PROOF STEP]
by (simp add: projection_def)


[STATEMENT]
lemma projection_to_emptyset_is_empty_trace: "l \<upharpoonleft>{} = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<upharpoonleft> {} = []
[PROOF STEP]
by (simp add: projection_def)


[STATEMENT]
lemma projection_idempotent: "l \<upharpoonleft> X= (l \<upharpoonleft>X) \<upharpoonleft>X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<upharpoonleft> X = l \<upharpoonleft> X \<upharpoonleft> X
[PROOF STEP]
by (simp add: projection_def)


[STATEMENT]
lemma projection_empty_implies_absence_of_events: "l \<upharpoonleft> X = [] \<Longrightarrow>  X \<inter> (set l) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<upharpoonleft> X = [] \<Longrightarrow> X \<inter> set l = {}
[PROOF STEP]
by (metis empty_set inter_set_filter projection_def)


[STATEMENT]
lemma disjoint_projection: "X \<inter> Y = {} \<Longrightarrow> (l \<upharpoonleft> X) \<upharpoonleft> Y = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<inter> Y = {} \<Longrightarrow> l \<upharpoonleft> X \<upharpoonleft> Y = []
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. X \<inter> Y = {} \<Longrightarrow> l \<upharpoonleft> X \<upharpoonleft> Y = []
[PROOF STEP]
assume X_Y_disjoint: "X \<inter> Y = {}"
[PROOF STATE]
proof (state)
this:
X \<inter> Y = {}

goal (1 subgoal):
 1. X \<inter> Y = {} \<Longrightarrow> l \<upharpoonleft> X \<upharpoonleft> Y = []
[PROOF STEP]
show "(l \<upharpoonleft> X) \<upharpoonleft> Y = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<upharpoonleft> X \<upharpoonleft> Y = []
[PROOF STEP]
unfolding projection_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) l) = []
[PROOF STEP]
proof (induct l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) []) = []
 2. \<And>a l. filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) l) = [] \<Longrightarrow> filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) (a # l)) = []
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) []) = []
 2. \<And>a l. filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) l) = [] \<Longrightarrow> filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) (a # l)) = []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) []) = []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) []) = []

goal (1 subgoal):
 1. \<And>a l. filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) l) = [] \<Longrightarrow> filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) (a # l)) = []
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l. filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) l) = [] \<Longrightarrow> filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) (a # l)) = []
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) xs) = []

goal (1 subgoal):
 1. \<And>a l. filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) l) = [] \<Longrightarrow> filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) (a # l)) = []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) (x # xs)) = []
[PROOF STEP]
proof (cases "x \<in> X")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> X \<Longrightarrow> filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) (x # xs)) = []
 2. x \<notin> X \<Longrightarrow> filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) (x # xs)) = []
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x \<in> X

goal (2 subgoals):
 1. x \<in> X \<Longrightarrow> filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) (x # xs)) = []
 2. x \<notin> X \<Longrightarrow> filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) (x # xs)) = []
[PROOF STEP]
with X_Y_disjoint
[PROOF STATE]
proof (chain)
picking this:
X \<inter> Y = {}
x \<in> X
[PROOF STEP]
have "x \<notin> Y"
[PROOF STATE]
proof (prove)
using this:
X \<inter> Y = {}
x \<in> X

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

goal (2 subgoals):
 1. x \<in> X \<Longrightarrow> filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) (x # xs)) = []
 2. x \<notin> X \<Longrightarrow> filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) (x # xs)) = []
[PROOF STEP]
thus "[x\<leftarrow>[x\<leftarrow>x # xs . x \<in> X] . x \<in> Y] = []"
[PROOF STATE]
proof (prove)
using this:
x \<notin> Y

goal (1 subgoal):
 1. filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) (x # xs)) = []
[PROOF STEP]
using Cons.hyps
[PROOF STATE]
proof (prove)
using this:
x \<notin> Y
filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) xs) = []

goal (1 subgoal):
 1. filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) (x # xs)) = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) (x # xs)) = []

goal (1 subgoal):
 1. x \<notin> X \<Longrightarrow> filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) (x # xs)) = []
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<notin> X \<Longrightarrow> filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) (x # xs)) = []
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<notin> X

goal (1 subgoal):
 1. x \<notin> X \<Longrightarrow> filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) (x # xs)) = []
[PROOF STEP]
show "[x\<leftarrow>[x\<leftarrow>x # xs . x \<in> X] . x \<in> Y] = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) (x # xs)) = []
[PROOF STEP]
using Cons.hyps False
[PROOF STATE]
proof (prove)
using this:
filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) xs) = []
x \<notin> X

goal (1 subgoal):
 1. filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) (x # xs)) = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) (x # xs)) = []

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
filter (\<lambda>x. x \<in> Y) (filter (\<lambda>x. x \<in> X) (x # xs)) = []

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
l \<upharpoonleft> X \<upharpoonleft> Y = []

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma projection_concatenation_commute:
  "(l1 @ l2) \<upharpoonleft> X = (l1 \<upharpoonleft> X) @ (l2 \<upharpoonleft> X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l1 @ l2) \<upharpoonleft> X = l1 \<upharpoonleft> X @ l2 \<upharpoonleft> X
[PROOF STEP]
by (unfold projection_def, auto)


[STATEMENT]
lemma projection_subset_eq_from_superset_eq:
"((xs \<upharpoonleft> (X \<union> Y)) = (ys \<upharpoonleft> (X \<union> Y))) \<Longrightarrow> ((xs \<upharpoonleft> X) = (ys \<upharpoonleft> X))"
(is "(?L1 = ?L2) \<Longrightarrow> (?L3 = ?L4)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<upharpoonleft> (X \<union> Y) = ys \<upharpoonleft> (X \<union> Y) \<Longrightarrow> xs \<upharpoonleft> X = ys \<upharpoonleft> X
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. xs \<upharpoonleft> (X \<union> Y) = ys \<upharpoonleft> (X \<union> Y) \<Longrightarrow> xs \<upharpoonleft> X = ys \<upharpoonleft> X
[PROOF STEP]
assume prem: "?L1 = ?L2"
[PROOF STATE]
proof (state)
this:
xs \<upharpoonleft> (X \<union> Y) = ys \<upharpoonleft> (X \<union> Y)

goal (1 subgoal):
 1. xs \<upharpoonleft> (X \<union> Y) = ys \<upharpoonleft> (X \<union> Y) \<Longrightarrow> xs \<upharpoonleft> X = ys \<upharpoonleft> X
[PROOF STEP]
have "?L1 \<upharpoonleft> X = ?L3 \<and> ?L2 \<upharpoonleft> X = ?L4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<upharpoonleft> (X \<union> Y) \<upharpoonleft> X = xs \<upharpoonleft> X \<and> ys \<upharpoonleft> (X \<union> Y) \<upharpoonleft> X = ys \<upharpoonleft> X
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. xs \<upharpoonleft> (X \<union> Y) \<upharpoonleft> X = xs \<upharpoonleft> X \<and> ys \<upharpoonleft> (X \<union> Y) \<upharpoonleft> X = ys \<upharpoonleft> X
[PROOF STEP]
have "\<And> a. ((a \<in> X \<or> a \<in> Y) \<and> a \<in> X) = (a \<in> X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. ((a \<in> X \<or> a \<in> Y) \<and> a \<in> X) = (a \<in> X)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((?a \<in> X \<or> ?a \<in> Y) \<and> ?a \<in> X) = (?a \<in> X)

goal (1 subgoal):
 1. xs \<upharpoonleft> (X \<union> Y) \<upharpoonleft> X = xs \<upharpoonleft> X \<and> ys \<upharpoonleft> (X \<union> Y) \<upharpoonleft> X = ys \<upharpoonleft> X
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
((?a \<in> X \<or> ?a \<in> Y) \<and> ?a \<in> X) = (?a \<in> X)

goal (1 subgoal):
 1. xs \<upharpoonleft> (X \<union> Y) \<upharpoonleft> X = xs \<upharpoonleft> X \<and> ys \<upharpoonleft> (X \<union> Y) \<upharpoonleft> X = ys \<upharpoonleft> X
[PROOF STEP]
by (simp add: projection_def)
[PROOF STATE]
proof (state)
this:
xs \<upharpoonleft> (X \<union> Y) \<upharpoonleft> X = xs \<upharpoonleft> X \<and> ys \<upharpoonleft> (X \<union> Y) \<upharpoonleft> X = ys \<upharpoonleft> X

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
xs \<upharpoonleft> (X \<union> Y) \<upharpoonleft> X = xs \<upharpoonleft> X \<and> ys \<upharpoonleft> (X \<union> Y) \<upharpoonleft> X = ys \<upharpoonleft> X

goal (1 subgoal):
 1. xs \<upharpoonleft> (X \<union> Y) = ys \<upharpoonleft> (X \<union> Y) \<Longrightarrow> xs \<upharpoonleft> X = ys \<upharpoonleft> X
[PROOF STEP]
with prem
[PROOF STATE]
proof (chain)
picking this:
xs \<upharpoonleft> (X \<union> Y) = ys \<upharpoonleft> (X \<union> Y)
xs \<upharpoonleft> (X \<union> Y) \<upharpoonleft> X = xs \<upharpoonleft> X \<and> ys \<upharpoonleft> (X \<union> Y) \<upharpoonleft> X = ys \<upharpoonleft> X
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xs \<upharpoonleft> (X \<union> Y) = ys \<upharpoonleft> (X \<union> Y)
xs \<upharpoonleft> (X \<union> Y) \<upharpoonleft> X = xs \<upharpoonleft> X \<and> ys \<upharpoonleft> (X \<union> Y) \<upharpoonleft> X = ys \<upharpoonleft> X

goal (1 subgoal):
 1. xs \<upharpoonleft> X = ys \<upharpoonleft> X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xs \<upharpoonleft> X = ys \<upharpoonleft> X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_subset_iff_projection_neutral: "(set l \<subseteq> X) = ((l \<upharpoonleft> X) = l)"
(is "?A = ?B")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (set l \<subseteq> X) = (l \<upharpoonleft> X = l)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (set l \<subseteq> X) = (l \<upharpoonleft> X = l)
[PROOF STEP]
have "?A \<Longrightarrow> ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set l \<subseteq> X \<Longrightarrow> l \<upharpoonleft> X = l
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set l \<subseteq> X \<Longrightarrow> l \<upharpoonleft> X = l
[PROOF STEP]
assume "?A"
[PROOF STATE]
proof (state)
this:
set l \<subseteq> X

goal (1 subgoal):
 1. set l \<subseteq> X \<Longrightarrow> l \<upharpoonleft> X = l
[PROOF STEP]
hence "\<And>x. x \<in> (set l) \<Longrightarrow> x \<in> X"
[PROOF STATE]
proof (prove)
using this:
set l \<subseteq> X

goal (1 subgoal):
 1. \<And>x. x \<in> set l \<Longrightarrow> x \<in> X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x \<in> set l \<Longrightarrow> ?x \<in> X

goal (1 subgoal):
 1. set l \<subseteq> X \<Longrightarrow> l \<upharpoonleft> X = l
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?x \<in> set l \<Longrightarrow> ?x \<in> X

goal (1 subgoal):
 1. l \<upharpoonleft> X = l
[PROOF STEP]
by (simp add: projection_def)
[PROOF STATE]
proof (state)
this:
l \<upharpoonleft> X = l

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set l \<subseteq> X \<Longrightarrow> l \<upharpoonleft> X = l

goal (1 subgoal):
 1. (set l \<subseteq> X) = (l \<upharpoonleft> X = l)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set l \<subseteq> X \<Longrightarrow> l \<upharpoonleft> X = l

goal (1 subgoal):
 1. (set l \<subseteq> X) = (l \<upharpoonleft> X = l)
[PROOF STEP]
have "?B \<Longrightarrow> ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<upharpoonleft> X = l \<Longrightarrow> set l \<subseteq> X
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l \<upharpoonleft> X = l \<Longrightarrow> set l \<subseteq> X
[PROOF STEP]
assume "?B"
[PROOF STATE]
proof (state)
this:
l \<upharpoonleft> X = l

goal (1 subgoal):
 1. l \<upharpoonleft> X = l \<Longrightarrow> set l \<subseteq> X
[PROOF STEP]
hence "(set (l \<upharpoonleft> X)) = set l"
[PROOF STATE]
proof (prove)
using this:
l \<upharpoonleft> X = l

goal (1 subgoal):
 1. set (l \<upharpoonleft> X) = set l
[PROOF STEP]
by (simp add: projection_def)
[PROOF STATE]
proof (state)
this:
set (l \<upharpoonleft> X) = set l

goal (1 subgoal):
 1. l \<upharpoonleft> X = l \<Longrightarrow> set l \<subseteq> X
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
set (l \<upharpoonleft> X) = set l

goal (1 subgoal):
 1. set l \<subseteq> X
[PROOF STEP]
by (simp add: projection_def, auto)
[PROOF STATE]
proof (state)
this:
set l \<subseteq> X

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
l \<upharpoonleft> X = l \<Longrightarrow> set l \<subseteq> X

goal (1 subgoal):
 1. (set l \<subseteq> X) = (l \<upharpoonleft> X = l)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set l \<subseteq> X \<Longrightarrow> l \<upharpoonleft> X = l
l \<upharpoonleft> X = l \<Longrightarrow> set l \<subseteq> X
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set l \<subseteq> X \<Longrightarrow> l \<upharpoonleft> X = l
l \<upharpoonleft> X = l \<Longrightarrow> set l \<subseteq> X

goal (1 subgoal):
 1. (set l \<subseteq> X) = (l \<upharpoonleft> X = l)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(set l \<subseteq> X) = (l \<upharpoonleft> X = l)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma projection_split_last: "Suc n = length (\<tau> \<upharpoonleft> X) \<Longrightarrow>
\<exists> \<beta> x \<alpha>. (x \<in> X \<and> \<tau> = \<beta> @ [x] @ \<alpha> \<and> \<alpha> \<upharpoonleft> X = [] \<and> n = length ((\<beta> @ \<alpha>) \<upharpoonleft> X))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc n = length (\<tau> \<upharpoonleft> X) \<Longrightarrow> \<exists>\<beta> x \<alpha>. x \<in> X \<and> \<tau> = \<beta> @ [x] @ \<alpha> \<and> \<alpha> \<upharpoonleft> X = [] \<and> n = length ((\<beta> @ \<alpha>) \<upharpoonleft> X)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Suc n = length (\<tau> \<upharpoonleft> X) \<Longrightarrow> \<exists>\<beta> x \<alpha>. x \<in> X \<and> \<tau> = \<beta> @ [x] @ \<alpha> \<and> \<alpha> \<upharpoonleft> X = [] \<and> n = length ((\<beta> @ \<alpha>) \<upharpoonleft> X)
[PROOF STEP]
assume Suc_n_is_len_\<tau>X: "Suc n = length (\<tau> \<upharpoonleft> X)"
[PROOF STATE]
proof (state)
this:
Suc n = length (\<tau> \<upharpoonleft> X)

goal (1 subgoal):
 1. Suc n = length (\<tau> \<upharpoonleft> X) \<Longrightarrow> \<exists>\<beta> x \<alpha>. x \<in> X \<and> \<tau> = \<beta> @ [x] @ \<alpha> \<and> \<alpha> \<upharpoonleft> X = [] \<and> n = length ((\<beta> @ \<alpha>) \<upharpoonleft> X)
[PROOF STEP]
let ?L = "\<tau> \<upharpoonleft> X"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Suc n = length (\<tau> \<upharpoonleft> X) \<Longrightarrow> \<exists>\<beta> x \<alpha>. x \<in> X \<and> \<tau> = \<beta> @ [x] @ \<alpha> \<and> \<alpha> \<upharpoonleft> X = [] \<and> n = length ((\<beta> @ \<alpha>) \<upharpoonleft> X)
[PROOF STEP]
let ?RL = "filter (\<lambda>x . x \<in> X) (rev \<tau>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Suc n = length (\<tau> \<upharpoonleft> X) \<Longrightarrow> \<exists>\<beta> x \<alpha>. x \<in> X \<and> \<tau> = \<beta> @ [x] @ \<alpha> \<and> \<alpha> \<upharpoonleft> X = [] \<and> n = length ((\<beta> @ \<alpha>) \<upharpoonleft> X)
[PROOF STEP]
have "Suc n = length ?RL"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc n = length (filter (\<lambda>x. x \<in> X) (rev \<tau>))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Suc n = length (filter (\<lambda>x. x \<in> X) (rev \<tau>))
[PROOF STEP]
have "rev ?L = ?RL"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev (\<tau> \<upharpoonleft> X) = filter (\<lambda>x. x \<in> X) (rev \<tau>)
[PROOF STEP]
by (simp add: projection_def, rule rev_filter)
[PROOF STATE]
proof (state)
this:
rev (\<tau> \<upharpoonleft> X) = filter (\<lambda>x. x \<in> X) (rev \<tau>)

goal (1 subgoal):
 1. Suc n = length (filter (\<lambda>x. x \<in> X) (rev \<tau>))
[PROOF STEP]
hence "rev (rev ?L) = rev ?RL"
[PROOF STATE]
proof (prove)
using this:
rev (\<tau> \<upharpoonleft> X) = filter (\<lambda>x. x \<in> X) (rev \<tau>)

goal (1 subgoal):
 1. rev (rev (\<tau> \<upharpoonleft> X)) = rev (filter (\<lambda>x. x \<in> X) (rev \<tau>))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
rev (rev (\<tau> \<upharpoonleft> X)) = rev (filter (\<lambda>x. x \<in> X) (rev \<tau>))

goal (1 subgoal):
 1. Suc n = length (filter (\<lambda>x. x \<in> X) (rev \<tau>))
[PROOF STEP]
hence "?L = rev ?RL"
[PROOF STATE]
proof (prove)
using this:
rev (rev (\<tau> \<upharpoonleft> X)) = rev (filter (\<lambda>x. x \<in> X) (rev \<tau>))

goal (1 subgoal):
 1. \<tau> \<upharpoonleft> X = rev (filter (\<lambda>x. x \<in> X) (rev \<tau>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<tau> \<upharpoonleft> X = rev (filter (\<lambda>x. x \<in> X) (rev \<tau>))

goal (1 subgoal):
 1. Suc n = length (filter (\<lambda>x. x \<in> X) (rev \<tau>))
[PROOF STEP]
with Suc_n_is_len_\<tau>X
[PROOF STATE]
proof (chain)
picking this:
Suc n = length (\<tau> \<upharpoonleft> X)
\<tau> \<upharpoonleft> X = rev (filter (\<lambda>x. x \<in> X) (rev \<tau>))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Suc n = length (\<tau> \<upharpoonleft> X)
\<tau> \<upharpoonleft> X = rev (filter (\<lambda>x. x \<in> X) (rev \<tau>))

goal (1 subgoal):
 1. Suc n = length (filter (\<lambda>x. x \<in> X) (rev \<tau>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc n = length (filter (\<lambda>x. x \<in> X) (rev \<tau>))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Suc n = length (filter (\<lambda>x. x \<in> X) (rev \<tau>))

goal (1 subgoal):
 1. Suc n = length (\<tau> \<upharpoonleft> X) \<Longrightarrow> \<exists>\<beta> x \<alpha>. x \<in> X \<and> \<tau> = \<beta> @ [x] @ \<alpha> \<and> \<alpha> \<upharpoonleft> X = [] \<and> n = length ((\<beta> @ \<alpha>) \<upharpoonleft> X)
[PROOF STEP]
with Suc_length_conv[of n ?RL]
[PROOF STATE]
proof (chain)
picking this:
(Suc n = length (filter (\<lambda>x. x \<in> X) (rev \<tau>))) = (\<exists>y ys. filter (\<lambda>x. x \<in> X) (rev \<tau>) = y # ys \<and> length ys = n)
Suc n = length (filter (\<lambda>x. x \<in> X) (rev \<tau>))
[PROOF STEP]
obtain x xs
    where "?RL = x # xs"
[PROOF STATE]
proof (prove)
using this:
(Suc n = length (filter (\<lambda>x. x \<in> X) (rev \<tau>))) = (\<exists>y ys. filter (\<lambda>x. x \<in> X) (rev \<tau>) = y # ys \<and> length ys = n)
Suc n = length (filter (\<lambda>x. x \<in> X) (rev \<tau>))

goal (1 subgoal):
 1. (\<And>x xs. filter (\<lambda>x. x \<in> X) (rev \<tau>) = x # xs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
filter (\<lambda>x. x \<in> X) (rev \<tau>) = x # xs

goal (1 subgoal):
 1. Suc n = length (\<tau> \<upharpoonleft> X) \<Longrightarrow> \<exists>\<beta> x \<alpha>. x \<in> X \<and> \<tau> = \<beta> @ [x] @ \<alpha> \<and> \<alpha> \<upharpoonleft> X = [] \<and> n = length ((\<beta> @ \<alpha>) \<upharpoonleft> X)
[PROOF STEP]
hence "x # xs = ?RL"
[PROOF STATE]
proof (prove)
using this:
filter (\<lambda>x. x \<in> X) (rev \<tau>) = x # xs

goal (1 subgoal):
 1. x # xs = filter (\<lambda>x. x \<in> X) (rev \<tau>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x # xs = filter (\<lambda>x. x \<in> X) (rev \<tau>)

goal (1 subgoal):
 1. Suc n = length (\<tau> \<upharpoonleft> X) \<Longrightarrow> \<exists>\<beta> x \<alpha>. x \<in> X \<and> \<tau> = \<beta> @ [x] @ \<alpha> \<and> \<alpha> \<upharpoonleft> X = [] \<and> n = length ((\<beta> @ \<alpha>) \<upharpoonleft> X)
[PROOF STEP]
from Cons_eq_filterD[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>us vs. rev \<tau> = us @ x # vs \<and> (\<forall>u\<in>set us. u \<notin> X) \<and> x \<in> X \<and> xs = filter (\<lambda>x. x \<in> X) vs
[PROOF STEP]
obtain rev\<alpha> rev\<beta>
    where "(rev \<tau>) = rev\<alpha> @ x # rev\<beta>"
    and rev\<alpha>_no_x: "\<forall>a \<in> set rev\<alpha>. a \<notin> X"
    and x_in_X: "x \<in> X"
[PROOF STATE]
proof (prove)
using this:
\<exists>us vs. rev \<tau> = us @ x # vs \<and> (\<forall>u\<in>set us. u \<notin> X) \<and> x \<in> X \<and> xs = filter (\<lambda>x. x \<in> X) vs

goal (1 subgoal):
 1. (\<And>rev\<alpha> rev\<beta>. \<lbrakk>rev \<tau> = rev\<alpha> @ x # rev\<beta>; \<forall>a\<in>set rev\<alpha>. a \<notin> X; x \<in> X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rev \<tau> = rev\<alpha> @ x # rev\<beta>
\<forall>a\<in>set rev\<alpha>. a \<notin> X
x \<in> X

goal (1 subgoal):
 1. Suc n = length (\<tau> \<upharpoonleft> X) \<Longrightarrow> \<exists>\<beta> x \<alpha>. x \<in> X \<and> \<tau> = \<beta> @ [x] @ \<alpha> \<and> \<alpha> \<upharpoonleft> X = [] \<and> n = length ((\<beta> @ \<alpha>) \<upharpoonleft> X)
[PROOF STEP]
hence "rev (rev \<tau>) = rev (rev\<alpha> @ x # rev\<beta>)"
[PROOF STATE]
proof (prove)
using this:
rev \<tau> = rev\<alpha> @ x # rev\<beta>
\<forall>a\<in>set rev\<alpha>. a \<notin> X
x \<in> X

goal (1 subgoal):
 1. rev (rev \<tau>) = rev (rev\<alpha> @ x # rev\<beta>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rev (rev \<tau>) = rev (rev\<alpha> @ x # rev\<beta>)

goal (1 subgoal):
 1. Suc n = length (\<tau> \<upharpoonleft> X) \<Longrightarrow> \<exists>\<beta> x \<alpha>. x \<in> X \<and> \<tau> = \<beta> @ [x] @ \<alpha> \<and> \<alpha> \<upharpoonleft> X = [] \<and> n = length ((\<beta> @ \<alpha>) \<upharpoonleft> X)
[PROOF STEP]
hence "\<tau> = (rev rev\<beta>) @ [x] @ (rev rev\<alpha>)"
[PROOF STATE]
proof (prove)
using this:
rev (rev \<tau>) = rev (rev\<alpha> @ x # rev\<beta>)

goal (1 subgoal):
 1. \<tau> = rev rev\<beta> @ [x] @ rev rev\<alpha>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<tau> = rev rev\<beta> @ [x] @ rev rev\<alpha>

goal (1 subgoal):
 1. Suc n = length (\<tau> \<upharpoonleft> X) \<Longrightarrow> \<exists>\<beta> x \<alpha>. x \<in> X \<and> \<tau> = \<beta> @ [x] @ \<alpha> \<and> \<alpha> \<upharpoonleft> X = [] \<and> n = length ((\<beta> @ \<alpha>) \<upharpoonleft> X)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<tau> = rev rev\<beta> @ [x] @ rev rev\<alpha>
[PROOF STEP]
obtain \<beta> \<alpha>
    where \<tau>_is_\<beta>x\<alpha>: "\<tau> = \<beta> @ [x] @ \<alpha>"
    and \<alpha>_is_revrev\<alpha>: "\<alpha> = (rev rev\<alpha>)"
    and \<beta>_is_revrev\<beta>: "\<beta> = (rev rev\<beta>)"
[PROOF STATE]
proof (prove)
using this:
\<tau> = rev rev\<beta> @ [x] @ rev rev\<alpha>

goal (1 subgoal):
 1. (\<And>\<beta> \<alpha>. \<lbrakk>\<tau> = \<beta> @ [x] @ \<alpha>; \<alpha> = rev rev\<alpha>; \<beta> = rev rev\<beta>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<tau> = \<beta> @ [x] @ \<alpha>
\<alpha> = rev rev\<alpha>
\<beta> = rev rev\<beta>

goal (1 subgoal):
 1. Suc n = length (\<tau> \<upharpoonleft> X) \<Longrightarrow> \<exists>\<beta> x \<alpha>. x \<in> X \<and> \<tau> = \<beta> @ [x] @ \<alpha> \<and> \<alpha> \<upharpoonleft> X = [] \<and> n = length ((\<beta> @ \<alpha>) \<upharpoonleft> X)
[PROOF STEP]
hence \<alpha>_no_x: "\<alpha> \<upharpoonleft> X = []"
[PROOF STATE]
proof (prove)
using this:
\<tau> = \<beta> @ [x] @ \<alpha>
\<alpha> = rev rev\<alpha>
\<beta> = rev rev\<beta>

goal (1 subgoal):
 1. \<alpha> \<upharpoonleft> X = []
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<tau> = \<beta> @ [x] @ \<alpha>; \<alpha> = rev rev\<alpha>; \<beta> = rev rev\<beta>\<rbrakk> \<Longrightarrow> \<alpha> \<upharpoonleft> X = []
[PROOF STEP]
from \<alpha>_is_revrev\<alpha> rev\<alpha>_no_x
[PROOF STATE]
proof (chain)
picking this:
\<alpha> = rev rev\<alpha>
\<forall>a\<in>set rev\<alpha>. a \<notin> X
[PROOF STEP]
have "\<forall>a \<in> set \<alpha>. a \<notin> X"
[PROOF STATE]
proof (prove)
using this:
\<alpha> = rev rev\<alpha>
\<forall>a\<in>set rev\<alpha>. a \<notin> X

goal (1 subgoal):
 1. \<forall>a\<in>set \<alpha>. a \<notin> X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>set \<alpha>. a \<notin> X

goal (1 subgoal):
 1. \<lbrakk>\<tau> = \<beta> @ [x] @ \<alpha>; \<alpha> = rev rev\<alpha>; \<beta> = rev rev\<beta>\<rbrakk> \<Longrightarrow> \<alpha> \<upharpoonleft> X = []
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set \<alpha>. a \<notin> X

goal (1 subgoal):
 1. \<alpha> \<upharpoonleft> X = []
[PROOF STEP]
by (simp add: projection_def)
[PROOF STATE]
proof (state)
this:
\<alpha> \<upharpoonleft> X = []

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<alpha> \<upharpoonleft> X = []

goal (1 subgoal):
 1. Suc n = length (\<tau> \<upharpoonleft> X) \<Longrightarrow> \<exists>\<beta> x \<alpha>. x \<in> X \<and> \<tau> = \<beta> @ [x] @ \<alpha> \<and> \<alpha> \<upharpoonleft> X = [] \<and> n = length ((\<beta> @ \<alpha>) \<upharpoonleft> X)
[PROOF STEP]
have "n = length ((\<beta> @ \<alpha>) \<upharpoonleft> X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = length ((\<beta> @ \<alpha>) \<upharpoonleft> X)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n = length ((\<beta> @ \<alpha>) \<upharpoonleft> X)
[PROOF STEP]
from \<alpha>_no_x
[PROOF STATE]
proof (chain)
picking this:
\<alpha> \<upharpoonleft> X = []
[PROOF STEP]
have \<alpha>X_zero_len: "length (\<alpha> \<upharpoonleft> X) = 0"
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<upharpoonleft> X = []

goal (1 subgoal):
 1. length (\<alpha> \<upharpoonleft> X) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (\<alpha> \<upharpoonleft> X) = 0

goal (1 subgoal):
 1. n = length ((\<beta> @ \<alpha>) \<upharpoonleft> X)
[PROOF STEP]
from x_in_X
[PROOF STATE]
proof (chain)
picking this:
x \<in> X
[PROOF STEP]
have xX_one_len: "length ([x] \<upharpoonleft> X) = 1"
[PROOF STATE]
proof (prove)
using this:
x \<in> X

goal (1 subgoal):
 1. length ([x] \<upharpoonleft> X) = 1
[PROOF STEP]
by (simp add: projection_def)
[PROOF STATE]
proof (state)
this:
length ([x] \<upharpoonleft> X) = 1

goal (1 subgoal):
 1. n = length ((\<beta> @ \<alpha>) \<upharpoonleft> X)
[PROOF STEP]
from \<tau>_is_\<beta>x\<alpha>
[PROOF STATE]
proof (chain)
picking this:
\<tau> = \<beta> @ [x] @ \<alpha>
[PROOF STEP]
have "length ?L = length (\<beta> \<upharpoonleft> X) + length ([x] \<upharpoonleft> X) + length (\<alpha> \<upharpoonleft> X)"
[PROOF STATE]
proof (prove)
using this:
\<tau> = \<beta> @ [x] @ \<alpha>

goal (1 subgoal):
 1. length (\<tau> \<upharpoonleft> X) = length (\<beta> \<upharpoonleft> X) + length ([x] \<upharpoonleft> X) + length (\<alpha> \<upharpoonleft> X)
[PROOF STEP]
by (simp add: projection_def)
[PROOF STATE]
proof (state)
this:
length (\<tau> \<upharpoonleft> X) = length (\<beta> \<upharpoonleft> X) + length ([x] \<upharpoonleft> X) + length (\<alpha> \<upharpoonleft> X)

goal (1 subgoal):
 1. n = length ((\<beta> @ \<alpha>) \<upharpoonleft> X)
[PROOF STEP]
with \<alpha>X_zero_len
[PROOF STATE]
proof (chain)
picking this:
length (\<alpha> \<upharpoonleft> X) = 0
length (\<tau> \<upharpoonleft> X) = length (\<beta> \<upharpoonleft> X) + length ([x] \<upharpoonleft> X) + length (\<alpha> \<upharpoonleft> X)
[PROOF STEP]
have "length ?L = length (\<beta> \<upharpoonleft> X) + length ([x] \<upharpoonleft> X)"
[PROOF STATE]
proof (prove)
using this:
length (\<alpha> \<upharpoonleft> X) = 0
length (\<tau> \<upharpoonleft> X) = length (\<beta> \<upharpoonleft> X) + length ([x] \<upharpoonleft> X) + length (\<alpha> \<upharpoonleft> X)

goal (1 subgoal):
 1. length (\<tau> \<upharpoonleft> X) = length (\<beta> \<upharpoonleft> X) + length ([x] \<upharpoonleft> X)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (\<tau> \<upharpoonleft> X) = length (\<beta> \<upharpoonleft> X) + length ([x] \<upharpoonleft> X)

goal (1 subgoal):
 1. n = length ((\<beta> @ \<alpha>) \<upharpoonleft> X)
[PROOF STEP]
with xX_one_len Suc_n_is_len_\<tau>X
[PROOF STATE]
proof (chain)
picking this:
length ([x] \<upharpoonleft> X) = 1
Suc n = length (\<tau> \<upharpoonleft> X)
length (\<tau> \<upharpoonleft> X) = length (\<beta> \<upharpoonleft> X) + length ([x] \<upharpoonleft> X)
[PROOF STEP]
have "n = length (\<beta> \<upharpoonleft> X)"
[PROOF STATE]
proof (prove)
using this:
length ([x] \<upharpoonleft> X) = 1
Suc n = length (\<tau> \<upharpoonleft> X)
length (\<tau> \<upharpoonleft> X) = length (\<beta> \<upharpoonleft> X) + length ([x] \<upharpoonleft> X)

goal (1 subgoal):
 1. n = length (\<beta> \<upharpoonleft> X)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n = length (\<beta> \<upharpoonleft> X)

goal (1 subgoal):
 1. n = length ((\<beta> @ \<alpha>) \<upharpoonleft> X)
[PROOF STEP]
with \<alpha>X_zero_len
[PROOF STATE]
proof (chain)
picking this:
length (\<alpha> \<upharpoonleft> X) = 0
n = length (\<beta> \<upharpoonleft> X)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length (\<alpha> \<upharpoonleft> X) = 0
n = length (\<beta> \<upharpoonleft> X)

goal (1 subgoal):
 1. n = length ((\<beta> @ \<alpha>) \<upharpoonleft> X)
[PROOF STEP]
by (simp add: projection_def)
[PROOF STATE]
proof (state)
this:
n = length ((\<beta> @ \<alpha>) \<upharpoonleft> X)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n = length ((\<beta> @ \<alpha>) \<upharpoonleft> X)

goal (1 subgoal):
 1. Suc n = length (\<tau> \<upharpoonleft> X) \<Longrightarrow> \<exists>\<beta> x \<alpha>. x \<in> X \<and> \<tau> = \<beta> @ [x] @ \<alpha> \<and> \<alpha> \<upharpoonleft> X = [] \<and> n = length ((\<beta> @ \<alpha>) \<upharpoonleft> X)
[PROOF STEP]
with x_in_X \<tau>_is_\<beta>x\<alpha> \<alpha>_no_x
[PROOF STATE]
proof (chain)
picking this:
x \<in> X
\<tau> = \<beta> @ [x] @ \<alpha>
\<alpha> \<upharpoonleft> X = []
n = length ((\<beta> @ \<alpha>) \<upharpoonleft> X)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> X
\<tau> = \<beta> @ [x] @ \<alpha>
\<alpha> \<upharpoonleft> X = []
n = length ((\<beta> @ \<alpha>) \<upharpoonleft> X)

goal (1 subgoal):
 1. \<exists>\<beta> x \<alpha>. x \<in> X \<and> \<tau> = \<beta> @ [x] @ \<alpha> \<and> \<alpha> \<upharpoonleft> X = [] \<and> n = length ((\<beta> @ \<alpha>) \<upharpoonleft> X)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>\<beta> x \<alpha>. x \<in> X \<and> \<tau> = \<beta> @ [x] @ \<alpha> \<and> \<alpha> \<upharpoonleft> X = [] \<and> n = length ((\<beta> @ \<alpha>) \<upharpoonleft> X)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma projection_rev_commute:
  "rev (l \<upharpoonleft> X) = (rev l) \<upharpoonleft> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev (l \<upharpoonleft> X) = rev l \<upharpoonleft> X
[PROOF STEP]
by (induct l, simp add: projection_def, simp add: projection_def)


[STATEMENT]
lemma projection_split_first_with_suffix:
  "\<lbrakk> (\<tau> \<upharpoonleft> X) = x # xs \<rbrakk> \<Longrightarrow> \<exists> \<alpha> \<beta>. (\<tau> = \<alpha> @ [x] @ \<beta> \<and> \<alpha> \<upharpoonleft> X = [] \<and> \<beta> \<upharpoonleft> X = xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> \<upharpoonleft> X = x # xs \<Longrightarrow> \<exists>\<alpha> \<beta>. \<tau> = \<alpha> @ [x] @ \<beta> \<and> \<alpha> \<upharpoonleft> X = [] \<and> \<beta> \<upharpoonleft> X = xs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<tau> \<upharpoonleft> X = x # xs \<Longrightarrow> \<exists>\<alpha> \<beta>. \<tau> = \<alpha> @ [x] @ \<beta> \<and> \<alpha> \<upharpoonleft> X = [] \<and> \<beta> \<upharpoonleft> X = xs
[PROOF STEP]
assume tau_proj_X: "(\<tau> \<upharpoonleft> X) = x # xs"
[PROOF STATE]
proof (state)
this:
\<tau> \<upharpoonleft> X = x # xs

goal (1 subgoal):
 1. \<tau> \<upharpoonleft> X = x # xs \<Longrightarrow> \<exists>\<alpha> \<beta>. \<tau> = \<alpha> @ [x] @ \<beta> \<and> \<alpha> \<upharpoonleft> X = [] \<and> \<beta> \<upharpoonleft> X = xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<alpha> \<beta>. \<tau> = \<alpha> @ [x] @ \<beta> \<and> \<alpha> \<upharpoonleft> X = [] \<and> \<beta> \<upharpoonleft> X = xs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>\<alpha> \<beta>. \<tau> = \<alpha> @ [x] @ \<beta> \<and> \<alpha> \<upharpoonleft> X = [] \<and> \<beta> \<upharpoonleft> X = xs
[PROOF STEP]
from   tau_proj_X
[PROOF STATE]
proof (chain)
picking this:
\<tau> \<upharpoonleft> X = x # xs
[PROOF STEP]
have x_in_X: "x \<in> X"
[PROOF STATE]
proof (prove)
using this:
\<tau> \<upharpoonleft> X = x # xs

goal (1 subgoal):
 1. x \<in> X
[PROOF STEP]
by (metis IntE inter_set_filter list.set_intros(1) projection_def)
[PROOF STATE]
proof (state)
this:
x \<in> X

goal (1 subgoal):
 1. \<exists>\<alpha> \<beta>. \<tau> = \<alpha> @ [x] @ \<beta> \<and> \<alpha> \<upharpoonleft> X = [] \<and> \<beta> \<upharpoonleft> X = xs
[PROOF STEP]
from  tau_proj_X
[PROOF STATE]
proof (chain)
picking this:
\<tau> \<upharpoonleft> X = x # xs
[PROOF STEP]
have  "\<exists> \<alpha> \<beta>. \<tau> = \<alpha> @ [x] @ \<beta> \<and> \<alpha> \<upharpoonleft> X = []"
[PROOF STATE]
proof (prove)
using this:
\<tau> \<upharpoonleft> X = x # xs

goal (1 subgoal):
 1. \<exists>\<alpha> \<beta>. \<tau> = \<alpha> @ [x] @ \<beta> \<and> \<alpha> \<upharpoonleft> X = []
[PROOF STEP]
using projection_split_first
[PROOF STATE]
proof (prove)
using this:
\<tau> \<upharpoonleft> X = x # xs
?\<tau> \<upharpoonleft> ?X = ?x # ?xs \<Longrightarrow> \<exists>\<alpha> \<beta>. ?\<tau> = \<alpha> @ [?x] @ \<beta> \<and> \<alpha> \<upharpoonleft> ?X = []

goal (1 subgoal):
 1. \<exists>\<alpha> \<beta>. \<tau> = \<alpha> @ [x] @ \<beta> \<and> \<alpha> \<upharpoonleft> X = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>\<alpha> \<beta>. \<tau> = \<alpha> @ [x] @ \<beta> \<and> \<alpha> \<upharpoonleft> X = []

goal (1 subgoal):
 1. \<exists>\<alpha> \<beta>. \<tau> = \<alpha> @ [x] @ \<beta> \<and> \<alpha> \<upharpoonleft> X = [] \<and> \<beta> \<upharpoonleft> X = xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>\<alpha> \<beta>. \<tau> = \<alpha> @ [x] @ \<beta> \<and> \<alpha> \<upharpoonleft> X = []
[PROOF STEP]
obtain \<alpha> \<beta> where tau_split: "\<tau> = \<alpha> @ [x] @ \<beta>"
                      and X_empty_prefix:"\<alpha> \<upharpoonleft> X = []"
[PROOF STATE]
proof (prove)
using this:
\<exists>\<alpha> \<beta>. \<tau> = \<alpha> @ [x] @ \<beta> \<and> \<alpha> \<upharpoonleft> X = []

goal (1 subgoal):
 1. (\<And>\<alpha> \<beta>. \<lbrakk>\<tau> = \<alpha> @ [x] @ \<beta>; \<alpha> \<upharpoonleft> X = []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<tau> = \<alpha> @ [x] @ \<beta>
\<alpha> \<upharpoonleft> X = []

goal (1 subgoal):
 1. \<exists>\<alpha> \<beta>. \<tau> = \<alpha> @ [x] @ \<beta> \<and> \<alpha> \<upharpoonleft> X = [] \<and> \<beta> \<upharpoonleft> X = xs
[PROOF STEP]
from tau_split tau_proj_X
[PROOF STATE]
proof (chain)
picking this:
\<tau> = \<alpha> @ [x] @ \<beta>
\<tau> \<upharpoonleft> X = x # xs
[PROOF STEP]
have  "(\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X =x # xs"
[PROOF STATE]
proof (prove)
using this:
\<tau> = \<alpha> @ [x] @ \<beta>
\<tau> \<upharpoonleft> X = x # xs

goal (1 subgoal):
 1. (\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X = x # xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X = x # xs

goal (1 subgoal):
 1. \<exists>\<alpha> \<beta>. \<tau> = \<alpha> @ [x] @ \<beta> \<and> \<alpha> \<upharpoonleft> X = [] \<and> \<beta> \<upharpoonleft> X = xs
[PROOF STEP]
with  X_empty_prefix
[PROOF STATE]
proof (chain)
picking this:
\<alpha> \<upharpoonleft> X = []
(\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X = x # xs
[PROOF STEP]
have  "([x] @ \<beta>) \<upharpoonleft> X =x # xs"
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<upharpoonleft> X = []
(\<alpha> @ [x] @ \<beta>) \<upharpoonleft> X = x # xs

goal (1 subgoal):
 1. ([x] @ \<beta>) \<upharpoonleft> X = x # xs
[PROOF STEP]
by (simp add: projection_concatenation_commute)
[PROOF STATE]
proof (state)
this:
([x] @ \<beta>) \<upharpoonleft> X = x # xs

goal (1 subgoal):
 1. \<exists>\<alpha> \<beta>. \<tau> = \<alpha> @ [x] @ \<beta> \<and> \<alpha> \<upharpoonleft> X = [] \<and> \<beta> \<upharpoonleft> X = xs
[PROOF STEP]
hence "(x # \<beta>) \<upharpoonleft> X =x # xs"
[PROOF STATE]
proof (prove)
using this:
([x] @ \<beta>) \<upharpoonleft> X = x # xs

goal (1 subgoal):
 1. (x # \<beta>) \<upharpoonleft> X = x # xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x # \<beta>) \<upharpoonleft> X = x # xs

goal (1 subgoal):
 1. \<exists>\<alpha> \<beta>. \<tau> = \<alpha> @ [x] @ \<beta> \<and> \<alpha> \<upharpoonleft> X = [] \<and> \<beta> \<upharpoonleft> X = xs
[PROOF STEP]
with  x_in_X
[PROOF STATE]
proof (chain)
picking this:
x \<in> X
(x # \<beta>) \<upharpoonleft> X = x # xs
[PROOF STEP]
have "\<beta> \<upharpoonleft> X = xs"
[PROOF STATE]
proof (prove)
using this:
x \<in> X
(x # \<beta>) \<upharpoonleft> X = x # xs

goal (1 subgoal):
 1. \<beta> \<upharpoonleft> X = xs
[PROOF STEP]
unfolding projection_def
[PROOF STATE]
proof (prove)
using this:
x \<in> X
filter (\<lambda>x. x \<in> X) (x # \<beta>) = x # xs

goal (1 subgoal):
 1. filter (\<lambda>x. x \<in> X) \<beta> = xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<beta> \<upharpoonleft> X = xs

goal (1 subgoal):
 1. \<exists>\<alpha> \<beta>. \<tau> = \<alpha> @ [x] @ \<beta> \<and> \<alpha> \<upharpoonleft> X = [] \<and> \<beta> \<upharpoonleft> X = xs
[PROOF STEP]
with  tau_split X_empty_prefix
[PROOF STATE]
proof (chain)
picking this:
\<tau> = \<alpha> @ [x] @ \<beta>
\<alpha> \<upharpoonleft> X = []
\<beta> \<upharpoonleft> X = xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<tau> = \<alpha> @ [x] @ \<beta>
\<alpha> \<upharpoonleft> X = []
\<beta> \<upharpoonleft> X = xs

goal (1 subgoal):
 1. \<exists>\<alpha> \<beta>. \<tau> = \<alpha> @ [x] @ \<beta> \<and> \<alpha> \<upharpoonleft> X = [] \<and> \<beta> \<upharpoonleft> X = xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>\<alpha> \<beta>. \<tau> = \<alpha> @ [x] @ \<beta> \<and> \<alpha> \<upharpoonleft> X = [] \<and> \<beta> \<upharpoonleft> X = xs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>\<alpha> \<beta>. \<tau> = \<alpha> @ [x] @ \<beta> \<and> \<alpha> \<upharpoonleft> X = [] \<and> \<beta> \<upharpoonleft> X = xs

goal:
No subgoals!
[PROOF STEP]
qed