[STATEMENT]
lemma list_sel_aux'1_if_tree_sel_nfwd:
  "\<lbrakk>tree_sel sel; \<not>forward_arcs (y#xs); forward_arcs (y#ys@xs)\<rbrakk>
    \<Longrightarrow> list_sel_aux' sel xs y = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tree_sel sel; \<not> forward_arcs (y # xs); forward_arcs (y # ys @ xs)\<rbrakk> \<Longrightarrow> list_sel_aux' sel xs y = 1
[PROOF STEP]
proof(induction xs arbitrary: ys rule: forward_arcs.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>ys. \<lbrakk>tree_sel sel; \<not> forward_arcs [y]; forward_arcs (y # ys @ [])\<rbrakk> \<Longrightarrow> list_sel_aux' sel [] y = 1
 2. \<And>x ys. \<lbrakk>tree_sel sel; \<not> forward_arcs [y, x]; forward_arcs (y # ys @ [x])\<rbrakk> \<Longrightarrow> list_sel_aux' sel [x] y = 1
 3. \<And>x v va ys. \<lbrakk>\<And>ys. \<lbrakk>tree_sel sel; \<not> forward_arcs (y # v # va); forward_arcs (y # ys @ v # va)\<rbrakk> \<Longrightarrow> list_sel_aux' sel (v # va) y = 1; tree_sel sel; \<not> forward_arcs (y # x # v # va); forward_arcs (y # ys @ x # v # va)\<rbrakk> \<Longrightarrow> list_sel_aux' sel (x # v # va) y = 1
[PROOF STEP]
case (2 x)
[PROOF STATE]
proof (state)
this:
tree_sel sel
\<not> forward_arcs [y, x]
forward_arcs (y # ys @ [x])

goal (3 subgoals):
 1. \<And>ys. \<lbrakk>tree_sel sel; \<not> forward_arcs [y]; forward_arcs (y # ys @ [])\<rbrakk> \<Longrightarrow> list_sel_aux' sel [] y = 1
 2. \<And>x ys. \<lbrakk>tree_sel sel; \<not> forward_arcs [y, x]; forward_arcs (y # ys @ [x])\<rbrakk> \<Longrightarrow> list_sel_aux' sel [x] y = 1
 3. \<And>x v va ys. \<lbrakk>\<And>ys. \<lbrakk>tree_sel sel; \<not> forward_arcs (y # v # va); forward_arcs (y # ys @ v # va)\<rbrakk> \<Longrightarrow> list_sel_aux' sel (v # va) y = 1; tree_sel sel; \<not> forward_arcs (y # x # v # va); forward_arcs (y # ys @ x # v # va)\<rbrakk> \<Longrightarrow> list_sel_aux' sel (x # v # va) y = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
tree_sel sel
\<not> forward_arcs [y, x]
forward_arcs (y # ys @ [x])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
tree_sel sel
\<not> forward_arcs [y, x]
forward_arcs (y # ys @ [x])

goal (1 subgoal):
 1. list_sel_aux' sel [x] y = 1
[PROOF STEP]
using not_y_dom_if_nfwd_app_fwd[OF 2(2,3)]
[PROOF STATE]
proof (prove)
using this:
tree_sel sel
\<not> forward_arcs [y, x]
forward_arcs (y # ys @ [x])
?x \<in> set [x] \<Longrightarrow> (y, ?x) \<notin> arcs_ends T

goal (1 subgoal):
 1. list_sel_aux' sel [x] y = 1
[PROOF STEP]
by (auto simp: tree_sel_def)
[PROOF STATE]
proof (state)
this:
list_sel_aux' sel [x] y = 1

goal (2 subgoals):
 1. \<And>ys. \<lbrakk>tree_sel sel; \<not> forward_arcs [y]; forward_arcs (y # ys @ [])\<rbrakk> \<Longrightarrow> list_sel_aux' sel [] y = 1
 2. \<And>x v va ys. \<lbrakk>\<And>ys. \<lbrakk>tree_sel sel; \<not> forward_arcs (y # v # va); forward_arcs (y # ys @ v # va)\<rbrakk> \<Longrightarrow> list_sel_aux' sel (v # va) y = 1; tree_sel sel; \<not> forward_arcs (y # x # v # va); forward_arcs (y # ys @ x # v # va)\<rbrakk> \<Longrightarrow> list_sel_aux' sel (x # v # va) y = 1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ys. \<lbrakk>tree_sel sel; \<not> forward_arcs [y]; forward_arcs (y # ys @ [])\<rbrakk> \<Longrightarrow> list_sel_aux' sel [] y = 1
 2. \<And>x v va ys. \<lbrakk>\<And>ys. \<lbrakk>tree_sel sel; \<not> forward_arcs (y # v # va); forward_arcs (y # ys @ v # va)\<rbrakk> \<Longrightarrow> list_sel_aux' sel (v # va) y = 1; tree_sel sel; \<not> forward_arcs (y # x # v # va); forward_arcs (y # ys @ x # v # va)\<rbrakk> \<Longrightarrow> list_sel_aux' sel (x # v # va) y = 1
[PROOF STEP]
case (3 x x' xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>tree_sel sel; \<not> forward_arcs (y # x' # xs); forward_arcs (y # ?ys2 @ x' # xs)\<rbrakk> \<Longrightarrow> list_sel_aux' sel (x' # xs) y = 1
tree_sel sel
\<not> forward_arcs (y # x # x' # xs)
forward_arcs (y # ys @ x # x' # xs)

goal (2 subgoals):
 1. \<And>ys. \<lbrakk>tree_sel sel; \<not> forward_arcs [y]; forward_arcs (y # ys @ [])\<rbrakk> \<Longrightarrow> list_sel_aux' sel [] y = 1
 2. \<And>x v va ys. \<lbrakk>\<And>ys. \<lbrakk>tree_sel sel; \<not> forward_arcs (y # v # va); forward_arcs (y # ys @ v # va)\<rbrakk> \<Longrightarrow> list_sel_aux' sel (v # va) y = 1; tree_sel sel; \<not> forward_arcs (y # x # v # va); forward_arcs (y # ys @ x # v # va)\<rbrakk> \<Longrightarrow> list_sel_aux' sel (x # v # va) y = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>tree_sel sel; \<not> forward_arcs (y # x' # xs); forward_arcs (y # ?ys2 @ x' # xs)\<rbrakk> \<Longrightarrow> list_sel_aux' sel (x' # xs) y = 1
tree_sel sel
\<not> forward_arcs (y # x # x' # xs)
forward_arcs (y # ys @ x # x' # xs)
[PROOF STEP]
have "forward_arcs (x # x' # xs)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>tree_sel sel; \<not> forward_arcs (y # x' # xs); forward_arcs (y # ?ys2 @ x' # xs)\<rbrakk> \<Longrightarrow> list_sel_aux' sel (x' # xs) y = 1
tree_sel sel
\<not> forward_arcs (y # x # x' # xs)
forward_arcs (y # ys @ x # x' # xs)

goal (1 subgoal):
 1. forward_arcs (x # x' # xs)
[PROOF STEP]
using forward_arcs_split[of "y#ys" "x#x'#xs"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>tree_sel sel; \<not> forward_arcs (y # x' # xs); forward_arcs (y # ?ys2 @ x' # xs)\<rbrakk> \<Longrightarrow> list_sel_aux' sel (x' # xs) y = 1
tree_sel sel
\<not> forward_arcs (y # x # x' # xs)
forward_arcs (y # ys @ x # x' # xs)
forward_arcs ((y # ys) @ x # x' # xs) \<Longrightarrow> forward_arcs (x # x' # xs)

goal (1 subgoal):
 1. forward_arcs (x # x' # xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
forward_arcs (x # x' # xs)

goal (2 subgoals):
 1. \<And>ys. \<lbrakk>tree_sel sel; \<not> forward_arcs [y]; forward_arcs (y # ys @ [])\<rbrakk> \<Longrightarrow> list_sel_aux' sel [] y = 1
 2. \<And>x v va ys. \<lbrakk>\<And>ys. \<lbrakk>tree_sel sel; \<not> forward_arcs (y # v # va); forward_arcs (y # ys @ v # va)\<rbrakk> \<Longrightarrow> list_sel_aux' sel (v # va) y = 1; tree_sel sel; \<not> forward_arcs (y # x # v # va); forward_arcs (y # ys @ x # v # va)\<rbrakk> \<Longrightarrow> list_sel_aux' sel (x # v # va) y = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
forward_arcs (x # x' # xs)
[PROOF STEP]
have "\<not> forward_arcs (y # x' # xs)"
[PROOF STATE]
proof (prove)
using this:
forward_arcs (x # x' # xs)

goal (1 subgoal):
 1. \<not> forward_arcs (y # x' # xs)
[PROOF STEP]
using not_fwd_if_skip1 "3.prems"(2)
[PROOF STATE]
proof (prove)
using this:
forward_arcs (x # x' # xs)
\<lbrakk>\<not> forward_arcs (?y # ?x # ?x' # ?xs); forward_arcs (?x # ?x' # ?xs)\<rbrakk> \<Longrightarrow> \<not> forward_arcs (?y # ?x' # ?xs)
\<not> forward_arcs (y # x # x' # xs)

goal (1 subgoal):
 1. \<not> forward_arcs (y # x' # xs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> forward_arcs (y # x' # xs)

goal (2 subgoals):
 1. \<And>ys. \<lbrakk>tree_sel sel; \<not> forward_arcs [y]; forward_arcs (y # ys @ [])\<rbrakk> \<Longrightarrow> list_sel_aux' sel [] y = 1
 2. \<And>x v va ys. \<lbrakk>\<And>ys. \<lbrakk>tree_sel sel; \<not> forward_arcs (y # v # va); forward_arcs (y # ys @ v # va)\<rbrakk> \<Longrightarrow> list_sel_aux' sel (v # va) y = 1; tree_sel sel; \<not> forward_arcs (y # x # v # va); forward_arcs (y # ys @ x # v # va)\<rbrakk> \<Longrightarrow> list_sel_aux' sel (x # v # va) y = 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> forward_arcs (y # x' # xs)

goal (2 subgoals):
 1. \<And>ys. \<lbrakk>tree_sel sel; \<not> forward_arcs [y]; forward_arcs (y # ys @ [])\<rbrakk> \<Longrightarrow> list_sel_aux' sel [] y = 1
 2. \<And>x v va ys. \<lbrakk>\<And>ys. \<lbrakk>tree_sel sel; \<not> forward_arcs (y # v # va); forward_arcs (y # ys @ v # va)\<rbrakk> \<Longrightarrow> list_sel_aux' sel (v # va) y = 1; tree_sel sel; \<not> forward_arcs (y # x # v # va); forward_arcs (y # ys @ x # v # va)\<rbrakk> \<Longrightarrow> list_sel_aux' sel (x # v # va) y = 1
[PROOF STEP]
have "forward_arcs (y # (ys@[x]) @ x' # xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. forward_arcs (y # (ys @ [x]) @ x' # xs)
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>tree_sel sel; \<not> forward_arcs (y # x' # xs); forward_arcs (y # ?ys2 @ x' # xs)\<rbrakk> \<Longrightarrow> list_sel_aux' sel (x' # xs) y = 1
tree_sel sel
\<not> forward_arcs (y # x # x' # xs)
forward_arcs (y # ys @ x # x' # xs)

goal (1 subgoal):
 1. forward_arcs (y # (ys @ [x]) @ x' # xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
forward_arcs (y # (ys @ [x]) @ x' # xs)

goal (2 subgoals):
 1. \<And>ys. \<lbrakk>tree_sel sel; \<not> forward_arcs [y]; forward_arcs (y # ys @ [])\<rbrakk> \<Longrightarrow> list_sel_aux' sel [] y = 1
 2. \<And>x v va ys. \<lbrakk>\<And>ys. \<lbrakk>tree_sel sel; \<not> forward_arcs (y # v # va); forward_arcs (y # ys @ v # va)\<rbrakk> \<Longrightarrow> list_sel_aux' sel (v # va) y = 1; tree_sel sel; \<not> forward_arcs (y # x # v # va); forward_arcs (y # ys @ x # v # va)\<rbrakk> \<Longrightarrow> list_sel_aux' sel (x # v # va) y = 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> forward_arcs (y # x' # xs)
forward_arcs (y # (ys @ [x]) @ x' # xs)
[PROOF STEP]
have "list_sel_aux' sel (x' # xs) y = 1"
[PROOF STATE]
proof (prove)
using this:
\<not> forward_arcs (y # x' # xs)
forward_arcs (y # (ys @ [x]) @ x' # xs)

goal (1 subgoal):
 1. list_sel_aux' sel (x' # xs) y = 1
[PROOF STEP]
using "3.IH"[OF "3.prems"(1)]
[PROOF STATE]
proof (prove)
using this:
\<not> forward_arcs (y # x' # xs)
forward_arcs (y # (ys @ [x]) @ x' # xs)
\<lbrakk>\<not> forward_arcs (y # x' # xs); forward_arcs (y # ?ys2 @ x' # xs)\<rbrakk> \<Longrightarrow> list_sel_aux' sel (x' # xs) y = 1

goal (1 subgoal):
 1. list_sel_aux' sel (x' # xs) y = 1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
list_sel_aux' sel (x' # xs) y = 1

goal (2 subgoals):
 1. \<And>ys. \<lbrakk>tree_sel sel; \<not> forward_arcs [y]; forward_arcs (y # ys @ [])\<rbrakk> \<Longrightarrow> list_sel_aux' sel [] y = 1
 2. \<And>x v va ys. \<lbrakk>\<And>ys. \<lbrakk>tree_sel sel; \<not> forward_arcs (y # v # va); forward_arcs (y # ys @ v # va)\<rbrakk> \<Longrightarrow> list_sel_aux' sel (v # va) y = 1; tree_sel sel; \<not> forward_arcs (y # x # v # va); forward_arcs (y # ys @ x # v # va)\<rbrakk> \<Longrightarrow> list_sel_aux' sel (x # v # va) y = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
list_sel_aux' sel (x' # xs) y = 1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
list_sel_aux' sel (x' # xs) y = 1

goal (1 subgoal):
 1. list_sel_aux' sel (x # x' # xs) y = 1
[PROOF STEP]
using "3.prems"(1) y_not_dom_if_nfwd_app_fwd[OF "3.prems"(2,3)]
      not_y_dom_if_nfwd_app_fwd[OF "3.prems"(2,3)]
[PROOF STATE]
proof (prove)
using this:
list_sel_aux' sel (x' # xs) y = 1
tree_sel sel
?x \<in> set (x # x' # xs) \<Longrightarrow> (?x, y) \<notin> arcs_ends T
?x \<in> set (x # x' # xs) \<Longrightarrow> (y, ?x) \<notin> arcs_ends T

goal (1 subgoal):
 1. list_sel_aux' sel (x # x' # xs) y = 1
[PROOF STEP]
by (simp add: tree_sel_def)
[PROOF STATE]
proof (state)
this:
list_sel_aux' sel (x # x' # xs) y = 1

goal (1 subgoal):
 1. \<And>ys. \<lbrakk>tree_sel sel; \<not> forward_arcs [y]; forward_arcs (y # ys @ [])\<rbrakk> \<Longrightarrow> list_sel_aux' sel [] y = 1
[PROOF STEP]
qed(simp)


[STATEMENT]
lemma contr_sel_eq_list_sel_aux'_if_tree_sel:
  "\<lbrakk>tree_sel sel; distinct (y#xs); forward_arcs (y#xs); xs \<noteq> []\<rbrakk>
    \<Longrightarrow> contr_sel sel y = list_sel_aux' sel xs y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tree_sel sel; distinct (y # xs); forward_arcs (y # xs); xs \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel xs y
[PROOF STEP]
proof(induction xs rule: forward_arcs.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>tree_sel sel; distinct [y]; forward_arcs [y]; [] \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel [] y
 2. \<And>x. \<lbrakk>tree_sel sel; distinct [y, x]; forward_arcs [y, x]; [x] \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel [x] y
 3. \<And>x v va. \<lbrakk>\<lbrakk>tree_sel sel; distinct (y # v # va); forward_arcs (y # v # va); v # va \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (v # va) y; tree_sel sel; distinct (y # x # v # va); forward_arcs (y # x # v # va); x # v # va \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x # v # va) y
[PROOF STEP]
case (2 x)
[PROOF STATE]
proof (state)
this:
tree_sel sel
distinct [y, x]
forward_arcs [y, x]
[x] \<noteq> []

goal (3 subgoals):
 1. \<lbrakk>tree_sel sel; distinct [y]; forward_arcs [y]; [] \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel [] y
 2. \<And>x. \<lbrakk>tree_sel sel; distinct [y, x]; forward_arcs [y, x]; [x] \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel [x] y
 3. \<And>x v va. \<lbrakk>\<lbrakk>tree_sel sel; distinct (y # v # va); forward_arcs (y # v # va); v # va \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (v # va) y; tree_sel sel; distinct (y # x # v # va); forward_arcs (y # x # v # va); x # v # va \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x # v # va) y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
tree_sel sel
distinct [y, x]
forward_arcs [y, x]
[x] \<noteq> []
[PROOF STEP]
have "x \<rightarrow>\<^bsub>T\<^esub> y"
[PROOF STATE]
proof (prove)
using this:
tree_sel sel
distinct [y, x]
forward_arcs [y, x]
[x] \<noteq> []

goal (1 subgoal):
 1. x \<rightarrow>\<^bsub>T\<^esub> y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<rightarrow>\<^bsub>T\<^esub> y

goal (3 subgoals):
 1. \<lbrakk>tree_sel sel; distinct [y]; forward_arcs [y]; [] \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel [] y
 2. \<And>x. \<lbrakk>tree_sel sel; distinct [y, x]; forward_arcs [y, x]; [x] \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel [x] y
 3. \<And>x v va. \<lbrakk>\<lbrakk>tree_sel sel; distinct (y # v # va); forward_arcs (y # v # va); v # va \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (v # va) y; tree_sel sel; distinct (y # x # v # va); forward_arcs (y # x # v # va); x # v # va \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x # v # va) y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<rightarrow>\<^bsub>T\<^esub> y
[PROOF STEP]
have "(THE x. x \<rightarrow>\<^bsub>T\<^esub> y) = x"
[PROOF STATE]
proof (prove)
using this:
x \<rightarrow>\<^bsub>T\<^esub> y

goal (1 subgoal):
 1. (THE x. x \<rightarrow>\<^bsub>T\<^esub> y) = x
[PROOF STEP]
using two_in_arcs_contr
[PROOF STATE]
proof (prove)
using this:
x \<rightarrow>\<^bsub>T\<^esub> y
\<lbrakk>?e1.0 \<in> arcs T; ?e2.0 \<in> arcs T; ?e1.0 \<noteq> ?e2.0; head T ?e1.0 = head T ?e2.0\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. (THE x. x \<rightarrow>\<^bsub>T\<^esub> y) = x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(THE x. x \<rightarrow>\<^bsub>T\<^esub> y) = x

goal (3 subgoals):
 1. \<lbrakk>tree_sel sel; distinct [y]; forward_arcs [y]; [] \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel [] y
 2. \<And>x. \<lbrakk>tree_sel sel; distinct [y, x]; forward_arcs [y, x]; [x] \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel [x] y
 3. \<And>x v va. \<lbrakk>\<lbrakk>tree_sel sel; distinct (y # v # va); forward_arcs (y # v # va); v # va \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (v # va) y; tree_sel sel; distinct (y # x # v # va); forward_arcs (y # x # v # va); x # v # va \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x # v # va) y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(THE x. x \<rightarrow>\<^bsub>T\<^esub> y) = x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(THE x. x \<rightarrow>\<^bsub>T\<^esub> y) = x

goal (1 subgoal):
 1. contr_sel sel y = list_sel_aux' sel [x] y
[PROOF STEP]
using \<open>x \<rightarrow>\<^bsub>T\<^esub> y\<close>
[PROOF STATE]
proof (prove)
using this:
(THE x. x \<rightarrow>\<^bsub>T\<^esub> y) = x
x \<rightarrow>\<^bsub>T\<^esub> y

goal (1 subgoal):
 1. contr_sel sel y = list_sel_aux' sel [x] y
[PROOF STEP]
unfolding contr_sel_def
[PROOF STATE]
proof (prove)
using this:
(THE x. x \<rightarrow>\<^bsub>T\<^esub> y) = x
x \<rightarrow>\<^bsub>T\<^esub> y

goal (1 subgoal):
 1. (if \<exists>x. x \<rightarrow>\<^bsub>T\<^esub> y then sel (THE x. x \<rightarrow>\<^bsub>T\<^esub> y) y else 1) = list_sel_aux' sel [x] y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
contr_sel sel y = list_sel_aux' sel [x] y

goal (2 subgoals):
 1. \<lbrakk>tree_sel sel; distinct [y]; forward_arcs [y]; [] \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel [] y
 2. \<And>x v va. \<lbrakk>\<lbrakk>tree_sel sel; distinct (y # v # va); forward_arcs (y # v # va); v # va \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (v # va) y; tree_sel sel; distinct (y # x # v # va); forward_arcs (y # x # v # va); x # v # va \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x # v # va) y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>tree_sel sel; distinct [y]; forward_arcs [y]; [] \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel [] y
 2. \<And>x v va. \<lbrakk>\<lbrakk>tree_sel sel; distinct (y # v # va); forward_arcs (y # v # va); v # va \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (v # va) y; tree_sel sel; distinct (y # x # v # va); forward_arcs (y # x # v # va); x # v # va \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x # v # va) y
[PROOF STEP]
case (3 x x' xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>tree_sel sel; distinct (y # x' # xs); forward_arcs (y # x' # xs); x' # xs \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x' # xs) y
tree_sel sel
distinct (y # x # x' # xs)
forward_arcs (y # x # x' # xs)
x # x' # xs \<noteq> []

goal (2 subgoals):
 1. \<lbrakk>tree_sel sel; distinct [y]; forward_arcs [y]; [] \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel [] y
 2. \<And>x v va. \<lbrakk>\<lbrakk>tree_sel sel; distinct (y # v # va); forward_arcs (y # v # va); v # va \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (v # va) y; tree_sel sel; distinct (y # x # v # va); forward_arcs (y # x # v # va); x # v # va \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x # v # va) y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>tree_sel sel; distinct (y # x' # xs); forward_arcs (y # x' # xs); x' # xs \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x' # xs) y
tree_sel sel
distinct (y # x # x' # xs)
forward_arcs (y # x # x' # xs)
x # x' # xs \<noteq> []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>tree_sel sel; distinct (y # x' # xs); forward_arcs (y # x' # xs); x' # xs \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x' # xs) y
tree_sel sel
distinct (y # x # x' # xs)
forward_arcs (y # x # x' # xs)
x # x' # xs \<noteq> []

goal (1 subgoal):
 1. contr_sel sel y = list_sel_aux' sel (x # x' # xs) y
[PROOF STEP]
proof(cases "x \<rightarrow>\<^bsub>T\<^esub> y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>tree_sel sel; distinct (y # x' # xs); forward_arcs (y # x' # xs); x' # xs \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x' # xs) y; tree_sel sel; distinct (y # x # x' # xs); forward_arcs (y # x # x' # xs); x # x' # xs \<noteq> []; x \<rightarrow>\<^bsub>T\<^esub> y\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x # x' # xs) y
 2. \<lbrakk>\<lbrakk>tree_sel sel; distinct (y # x' # xs); forward_arcs (y # x' # xs); x' # xs \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x' # xs) y; tree_sel sel; distinct (y # x # x' # xs); forward_arcs (y # x # x' # xs); x # x' # xs \<noteq> []; (x, y) \<notin> arcs_ends T\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x # x' # xs) y
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x \<rightarrow>\<^bsub>T\<^esub> y

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>tree_sel sel; distinct (y # x' # xs); forward_arcs (y # x' # xs); x' # xs \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x' # xs) y; tree_sel sel; distinct (y # x # x' # xs); forward_arcs (y # x # x' # xs); x # x' # xs \<noteq> []; x \<rightarrow>\<^bsub>T\<^esub> y\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x # x' # xs) y
 2. \<lbrakk>\<lbrakk>tree_sel sel; distinct (y # x' # xs); forward_arcs (y # x' # xs); x' # xs \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x' # xs) y; tree_sel sel; distinct (y # x # x' # xs); forward_arcs (y # x # x' # xs); x # x' # xs \<noteq> []; (x, y) \<notin> arcs_ends T\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x # x' # xs) y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<rightarrow>\<^bsub>T\<^esub> y
[PROOF STEP]
have "(THE x. x \<rightarrow>\<^bsub>T\<^esub> y) = x"
[PROOF STATE]
proof (prove)
using this:
x \<rightarrow>\<^bsub>T\<^esub> y

goal (1 subgoal):
 1. (THE x. x \<rightarrow>\<^bsub>T\<^esub> y) = x
[PROOF STEP]
using two_in_arcs_contr
[PROOF STATE]
proof (prove)
using this:
x \<rightarrow>\<^bsub>T\<^esub> y
\<lbrakk>?e1.0 \<in> arcs T; ?e2.0 \<in> arcs T; ?e1.0 \<noteq> ?e2.0; head T ?e1.0 = head T ?e2.0\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. (THE x. x \<rightarrow>\<^bsub>T\<^esub> y) = x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(THE x. x \<rightarrow>\<^bsub>T\<^esub> y) = x

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>tree_sel sel; distinct (y # x' # xs); forward_arcs (y # x' # xs); x' # xs \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x' # xs) y; tree_sel sel; distinct (y # x # x' # xs); forward_arcs (y # x # x' # xs); x # x' # xs \<noteq> []; x \<rightarrow>\<^bsub>T\<^esub> y\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x # x' # xs) y
 2. \<lbrakk>\<lbrakk>tree_sel sel; distinct (y # x' # xs); forward_arcs (y # x' # xs); x' # xs \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x' # xs) y; tree_sel sel; distinct (y # x # x' # xs); forward_arcs (y # x # x' # xs); x # x' # xs \<noteq> []; (x, y) \<notin> arcs_ends T\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x # x' # xs) y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(THE x. x \<rightarrow>\<^bsub>T\<^esub> y) = x
[PROOF STEP]
have contr_sel: "contr_sel sel y = sel x y"
[PROOF STATE]
proof (prove)
using this:
(THE x. x \<rightarrow>\<^bsub>T\<^esub> y) = x

goal (1 subgoal):
 1. contr_sel sel y = sel x y
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
(THE x. x \<rightarrow>\<^bsub>T\<^esub> y) = x
x \<rightarrow>\<^bsub>T\<^esub> y

goal (1 subgoal):
 1. contr_sel sel y = sel x y
[PROOF STEP]
unfolding contr_sel_def
[PROOF STATE]
proof (prove)
using this:
(THE x. x \<rightarrow>\<^bsub>T\<^esub> y) = x
x \<rightarrow>\<^bsub>T\<^esub> y

goal (1 subgoal):
 1. (if \<exists>x. x \<rightarrow>\<^bsub>T\<^esub> y then sel (THE x. x \<rightarrow>\<^bsub>T\<^esub> y) y else 1) = sel x y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
contr_sel sel y = sel x y

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>tree_sel sel; distinct (y # x' # xs); forward_arcs (y # x' # xs); x' # xs \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x' # xs) y; tree_sel sel; distinct (y # x # x' # xs); forward_arcs (y # x # x' # xs); x # x' # xs \<noteq> []; x \<rightarrow>\<^bsub>T\<^esub> y\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x # x' # xs) y
 2. \<lbrakk>\<lbrakk>tree_sel sel; distinct (y # x' # xs); forward_arcs (y # x' # xs); x' # xs \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x' # xs) y; tree_sel sel; distinct (y # x # x' # xs); forward_arcs (y # x # x' # xs); x # x' # xs \<noteq> []; (x, y) \<notin> arcs_ends T\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x # x' # xs) y
[PROOF STEP]
have "\<not>forward_arcs (y#x'#xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> forward_arcs (y # x' # xs)
[PROOF STEP]
using True "3.prems"(2) two_in_arcs_contr
[PROOF STATE]
proof (prove)
using this:
x \<rightarrow>\<^bsub>T\<^esub> y
distinct (y # x # x' # xs)
\<lbrakk>?e1.0 \<in> arcs T; ?e2.0 \<in> arcs T; ?e1.0 \<noteq> ?e2.0; head T ?e1.0 = head T ?e2.0\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. \<not> forward_arcs (y # x' # xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> forward_arcs (y # x' # xs)

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>tree_sel sel; distinct (y # x' # xs); forward_arcs (y # x' # xs); x' # xs \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x' # xs) y; tree_sel sel; distinct (y # x # x' # xs); forward_arcs (y # x # x' # xs); x # x' # xs \<noteq> []; x \<rightarrow>\<^bsub>T\<^esub> y\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x # x' # xs) y
 2. \<lbrakk>\<lbrakk>tree_sel sel; distinct (y # x' # xs); forward_arcs (y # x' # xs); x' # xs \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x' # xs) y; tree_sel sel; distinct (y # x # x' # xs); forward_arcs (y # x # x' # xs); x # x' # xs \<noteq> []; (x, y) \<notin> arcs_ends T\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x # x' # xs) y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> forward_arcs (y # x' # xs)
[PROOF STEP]
have "list_sel_aux' sel (x'#xs) y = 1"
[PROOF STATE]
proof (prove)
using this:
\<not> forward_arcs (y # x' # xs)

goal (1 subgoal):
 1. list_sel_aux' sel (x' # xs) y = 1
[PROOF STEP]
using list_sel_aux'1_if_tree_sel_nfwd[of sel y "x'#xs" "[x]"] "3.prems"(1,3)
[PROOF STATE]
proof (prove)
using this:
\<not> forward_arcs (y # x' # xs)
\<lbrakk>tree_sel sel; \<not> forward_arcs (y # x' # xs); forward_arcs (y # [x] @ x' # xs)\<rbrakk> \<Longrightarrow> list_sel_aux' sel (x' # xs) y = 1
tree_sel sel
forward_arcs (y # x # x' # xs)

goal (1 subgoal):
 1. list_sel_aux' sel (x' # xs) y = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
list_sel_aux' sel (x' # xs) y = 1

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>tree_sel sel; distinct (y # x' # xs); forward_arcs (y # x' # xs); x' # xs \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x' # xs) y; tree_sel sel; distinct (y # x # x' # xs); forward_arcs (y # x # x' # xs); x # x' # xs \<noteq> []; x \<rightarrow>\<^bsub>T\<^esub> y\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x # x' # xs) y
 2. \<lbrakk>\<lbrakk>tree_sel sel; distinct (y # x' # xs); forward_arcs (y # x' # xs); x' # xs \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x' # xs) y; tree_sel sel; distinct (y # x # x' # xs); forward_arcs (y # x # x' # xs); x # x' # xs \<noteq> []; (x, y) \<notin> arcs_ends T\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x # x' # xs) y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
list_sel_aux' sel (x' # xs) y = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
list_sel_aux' sel (x' # xs) y = 1

goal (1 subgoal):
 1. contr_sel sel y = list_sel_aux' sel (x # x' # xs) y
[PROOF STEP]
using contr_sel
[PROOF STATE]
proof (prove)
using this:
list_sel_aux' sel (x' # xs) y = 1
contr_sel sel y = sel x y

goal (1 subgoal):
 1. contr_sel sel y = list_sel_aux' sel (x # x' # xs) y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
contr_sel sel y = list_sel_aux' sel (x # x' # xs) y

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>tree_sel sel; distinct (y # x' # xs); forward_arcs (y # x' # xs); x' # xs \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x' # xs) y; tree_sel sel; distinct (y # x # x' # xs); forward_arcs (y # x # x' # xs); x # x' # xs \<noteq> []; (x, y) \<notin> arcs_ends T\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x # x' # xs) y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>tree_sel sel; distinct (y # x' # xs); forward_arcs (y # x' # xs); x' # xs \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x' # xs) y; tree_sel sel; distinct (y # x # x' # xs); forward_arcs (y # x # x' # xs); x # x' # xs \<noteq> []; (x, y) \<notin> arcs_ends T\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x # x' # xs) y
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
(x, y) \<notin> arcs_ends T

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>tree_sel sel; distinct (y # x' # xs); forward_arcs (y # x' # xs); x' # xs \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x' # xs) y; tree_sel sel; distinct (y # x # x' # xs); forward_arcs (y # x # x' # xs); x # x' # xs \<noteq> []; (x, y) \<notin> arcs_ends T\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x # x' # xs) y
[PROOF STEP]
have "\<not>y \<rightarrow>\<^bsub>T\<^esub> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y, x) \<notin> arcs_ends T
[PROOF STEP]
using "3.prems"(2,3) forward_arcs_alt' no_back_arc_if_fwd_dstct
[PROOF STATE]
proof (prove)
using this:
distinct (y # x # x' # xs)
forward_arcs (y # x # x' # xs)
forward (rev ?xs) = forward_arcs ?xs
\<lbrakk>forward (?as @ ?bs); distinct (?as @ ?bs)\<rbrakk> \<Longrightarrow> \<not> (\<exists>x\<in>set ?bs. \<exists>y\<in>set ?as. x \<rightarrow>\<^bsub>T\<^esub> y)

goal (1 subgoal):
 1. (y, x) \<notin> arcs_ends T
[PROOF STEP]
by (metis distinct_rev list.set_intros(1) rev.simps(2) set_rev)
[PROOF STATE]
proof (state)
this:
(y, x) \<notin> arcs_ends T

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>tree_sel sel; distinct (y # x' # xs); forward_arcs (y # x' # xs); x' # xs \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x' # xs) y; tree_sel sel; distinct (y # x # x' # xs); forward_arcs (y # x # x' # xs); x # x' # xs \<noteq> []; (x, y) \<notin> arcs_ends T\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x # x' # xs) y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(y, x) \<notin> arcs_ends T
[PROOF STEP]
have "sel x y = 1"
[PROOF STATE]
proof (prove)
using this:
(y, x) \<notin> arcs_ends T

goal (1 subgoal):
 1. sel x y = 1
[PROOF STEP]
using "3.prems"(1) False
[PROOF STATE]
proof (prove)
using this:
(y, x) \<notin> arcs_ends T
tree_sel sel
(x, y) \<notin> arcs_ends T

goal (1 subgoal):
 1. sel x y = 1
[PROOF STEP]
unfolding tree_sel_def
[PROOF STATE]
proof (prove)
using this:
(y, x) \<notin> arcs_ends T
\<forall>x y. \<not> (x \<rightarrow>\<^bsub>T\<^esub> y \<or> y \<rightarrow>\<^bsub>T\<^esub> x) \<longrightarrow> sel x y = 1
(x, y) \<notin> arcs_ends T

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

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>tree_sel sel; distinct (y # x' # xs); forward_arcs (y # x' # xs); x' # xs \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x' # xs) y; tree_sel sel; distinct (y # x # x' # xs); forward_arcs (y # x # x' # xs); x # x' # xs \<noteq> []; (x, y) \<notin> arcs_ends T\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x # x' # xs) y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sel x y = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sel x y = 1

goal (1 subgoal):
 1. contr_sel sel y = list_sel_aux' sel (x # x' # xs) y
[PROOF STEP]
using 3 False
[PROOF STATE]
proof (prove)
using this:
sel x y = 1
\<lbrakk>tree_sel sel; distinct (y # x' # xs); forward_arcs (y # x' # xs); x' # xs \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel (x' # xs) y
tree_sel sel
distinct (y # x # x' # xs)
forward_arcs (y # x # x' # xs)
x # x' # xs \<noteq> []
(x, y) \<notin> arcs_ends T

goal (1 subgoal):
 1. contr_sel sel y = list_sel_aux' sel (x # x' # xs) y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
contr_sel sel y = list_sel_aux' sel (x # x' # xs) y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
contr_sel sel y = list_sel_aux' sel (x # x' # xs) y

goal (1 subgoal):
 1. \<lbrakk>tree_sel sel; distinct [y]; forward_arcs [y]; [] \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel y = list_sel_aux' sel [] y
[PROOF STEP]
qed(simp)


[STATEMENT]
lemma contr_sel_root[simp]: "contr_sel sel root = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. contr_sel sel root = 1
[PROOF STEP]
by (auto simp: contr_sel_def dest: dominated_not_root)


[STATEMENT]
lemma contr_sel_notvert[simp]: "v \<notin> verts T \<Longrightarrow> contr_sel sel v = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<notin> verts T \<Longrightarrow> contr_sel sel v = 1
[PROOF STEP]
by (auto simp: contr_sel_def)


[STATEMENT]
lemma hd_reach_all_forward_verts:
  "\<lbrakk>forward xs; set xs = verts T; v \<in> verts T\<rbrakk> \<Longrightarrow> hd xs \<rightarrow>\<^sup>*\<^bsub>T\<^esub> v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>forward xs; set xs = verts T; v \<in> verts T\<rbrakk> \<Longrightarrow> hd xs \<rightarrow>\<^sup>*\<^bsub>T\<^esub> v
[PROOF STEP]
using hd_reach_all_forward list.set_sel(1)[of xs]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>hd ?xs \<in> verts T; forward ?xs; ?x \<in> set ?xs\<rbrakk> \<Longrightarrow> hd ?xs \<rightarrow>\<^sup>*\<^bsub>T\<^esub> ?x
xs \<noteq> [] \<Longrightarrow> hd xs \<in> set xs

goal (1 subgoal):
 1. \<lbrakk>forward xs; set xs = verts T; v \<in> verts T\<rbrakk> \<Longrightarrow> hd xs \<rightarrow>\<^sup>*\<^bsub>T\<^esub> v
[PROOF STEP]
by force


[STATEMENT]
lemma hd_eq_root_if_forward_verts: "\<lbrakk>forward xs; set xs = verts T\<rbrakk> \<Longrightarrow> hd xs = root"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>forward xs; set xs = verts T\<rbrakk> \<Longrightarrow> hd xs = root
[PROOF STEP]
using hd_reach_all_forward_verts root_if_all_reach
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>forward ?xs; set ?xs = verts T; ?v \<in> verts T\<rbrakk> \<Longrightarrow> hd ?xs \<rightarrow>\<^sup>*\<^bsub>T\<^esub> ?v
\<forall>v\<in>verts T. ?x \<rightarrow>\<^sup>*\<^bsub>T\<^esub> v \<Longrightarrow> ?x = root

goal (1 subgoal):
 1. \<lbrakk>forward xs; set xs = verts T\<rbrakk> \<Longrightarrow> hd xs = root
[PROOF STEP]
by simp


[STATEMENT]
lemma contr_sel_eq_ldeep_s_if_tree_dst_fwd_verts:
  assumes "tree_sel sel" and "distinct xs" and "forward xs" and "set xs = verts T"
  shows "contr_sel sel y = ldeep_s sel (rev xs) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. contr_sel sel y = ldeep_s sel (rev xs) y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. contr_sel sel y = ldeep_s sel (rev xs) y
[PROOF STEP]
have hd_root: "hd xs = root"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd xs = root
[PROOF STEP]
using hd_eq_root_if_forward_verts assms(3,4)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>forward ?xs; set ?xs = verts T\<rbrakk> \<Longrightarrow> hd ?xs = root
forward xs
set xs = verts T

goal (1 subgoal):
 1. hd xs = root
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
hd xs = root

goal (1 subgoal):
 1. contr_sel sel y = ldeep_s sel (rev xs) y
[PROOF STEP]
consider "y \<in> set xs" "y = root" | "y \<in> set xs" "y \<noteq> root" | "y \<notin> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>y \<in> set xs; y = root\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>y \<in> set xs; y \<noteq> root\<rbrakk> \<Longrightarrow> thesis; y \<notin> set xs \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>y \<in> set xs; y = root\<rbrakk> \<Longrightarrow> ?thesis2; \<lbrakk>y \<in> set xs; y \<noteq> root\<rbrakk> \<Longrightarrow> ?thesis2; y \<notin> set xs \<Longrightarrow> ?thesis2\<rbrakk> \<Longrightarrow> ?thesis2

goal (1 subgoal):
 1. contr_sel sel y = ldeep_s sel (rev xs) y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<lbrakk>y \<in> set xs; y = root\<rbrakk> \<Longrightarrow> ?thesis2; \<lbrakk>y \<in> set xs; y \<noteq> root\<rbrakk> \<Longrightarrow> ?thesis2; y \<notin> set xs \<Longrightarrow> ?thesis2\<rbrakk> \<Longrightarrow> ?thesis2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<lbrakk>y \<in> set xs; y = root\<rbrakk> \<Longrightarrow> ?thesis2; \<lbrakk>y \<in> set xs; y \<noteq> root\<rbrakk> \<Longrightarrow> ?thesis2; y \<notin> set xs \<Longrightarrow> ?thesis2\<rbrakk> \<Longrightarrow> ?thesis2

goal (1 subgoal):
 1. contr_sel sel y = ldeep_s sel (rev xs) y
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>y \<in> set xs; y = root\<rbrakk> \<Longrightarrow> contr_sel sel y = ldeep_s sel (rev xs) y
 2. \<lbrakk>y \<in> set xs; y \<noteq> root\<rbrakk> \<Longrightarrow> contr_sel sel y = ldeep_s sel (rev xs) y
 3. y \<notin> set xs \<Longrightarrow> contr_sel sel y = ldeep_s sel (rev xs) y
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
y \<in> set xs
y = root

goal (3 subgoals):
 1. \<lbrakk>y \<in> set xs; y = root\<rbrakk> \<Longrightarrow> contr_sel sel y = ldeep_s sel (rev xs) y
 2. \<lbrakk>y \<in> set xs; y \<noteq> root\<rbrakk> \<Longrightarrow> contr_sel sel y = ldeep_s sel (rev xs) y
 3. y \<notin> set xs \<Longrightarrow> contr_sel sel y = ldeep_s sel (rev xs) y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> set xs
y = root
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
y \<in> set xs
y = root

goal (1 subgoal):
 1. contr_sel sel y = ldeep_s sel (rev xs) y
[PROOF STEP]
using hd_root ldeep_s_revhd1_if_distinct assms(2)
[PROOF STATE]
proof (prove)
using this:
y \<in> set xs
y = root
hd xs = root
distinct ?xs \<Longrightarrow> ldeep_s ?sel (rev ?xs) (hd ?xs) = 1
distinct xs

goal (1 subgoal):
 1. contr_sel sel y = ldeep_s sel (rev xs) y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
contr_sel sel y = ldeep_s sel (rev xs) y

goal (2 subgoals):
 1. \<lbrakk>y \<in> set xs; y \<noteq> root\<rbrakk> \<Longrightarrow> contr_sel sel y = ldeep_s sel (rev xs) y
 2. y \<notin> set xs \<Longrightarrow> contr_sel sel y = ldeep_s sel (rev xs) y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>y \<in> set xs; y \<noteq> root\<rbrakk> \<Longrightarrow> contr_sel sel y = ldeep_s sel (rev xs) y
 2. y \<notin> set xs \<Longrightarrow> contr_sel sel y = ldeep_s sel (rev xs) y
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
y \<in> set xs
y \<noteq> root

goal (2 subgoals):
 1. \<lbrakk>y \<in> set xs; y \<noteq> root\<rbrakk> \<Longrightarrow> contr_sel sel y = ldeep_s sel (rev xs) y
 2. y \<notin> set xs \<Longrightarrow> contr_sel sel y = ldeep_s sel (rev xs) y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> set xs
y \<noteq> root
[PROOF STEP]
obtain as bs where as_def: "as @ y # bs = xs"
[PROOF STATE]
proof (prove)
using this:
y \<in> set xs
y \<noteq> root

goal (1 subgoal):
 1. (\<And>as bs. as @ y # bs = xs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using split_list[of y]
[PROOF STATE]
proof (prove)
using this:
y \<in> set xs
y \<noteq> root
y \<in> set ?xs \<Longrightarrow> \<exists>ys zs. ?xs = ys @ y # zs

goal (1 subgoal):
 1. (\<And>as bs. as @ y # bs = xs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
as @ y # bs = xs

goal (2 subgoals):
 1. \<lbrakk>y \<in> set xs; y \<noteq> root\<rbrakk> \<Longrightarrow> contr_sel sel y = ldeep_s sel (rev xs) y
 2. y \<notin> set xs \<Longrightarrow> contr_sel sel y = ldeep_s sel (rev xs) y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
as @ y # bs = xs
[PROOF STEP]
have "forward (as@[y])"
[PROOF STATE]
proof (prove)
using this:
as @ y # bs = xs

goal (1 subgoal):
 1. forward (as @ [y])
[PROOF STEP]
using assms(3) forward_split[of "as@[y]"]
[PROOF STATE]
proof (prove)
using this:
as @ y # bs = xs
forward xs
forward ((as @ [y]) @ ?ys) \<Longrightarrow> forward (as @ [y])

goal (1 subgoal):
 1. forward (as @ [y])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
forward (as @ [y])

goal (2 subgoals):
 1. \<lbrakk>y \<in> set xs; y \<noteq> root\<rbrakk> \<Longrightarrow> contr_sel sel y = ldeep_s sel (rev xs) y
 2. y \<notin> set xs \<Longrightarrow> contr_sel sel y = ldeep_s sel (rev xs) y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
forward (as @ [y])

goal (2 subgoals):
 1. \<lbrakk>y \<in> set xs; y \<noteq> root\<rbrakk> \<Longrightarrow> contr_sel sel y = ldeep_s sel (rev xs) y
 2. y \<notin> set xs \<Longrightarrow> contr_sel sel y = ldeep_s sel (rev xs) y
[PROOF STEP]
have "distinct (as@[y])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (as @ [y])
[PROOF STEP]
using assms(2) as_def
[PROOF STATE]
proof (prove)
using this:
distinct xs
as @ y # bs = xs

goal (1 subgoal):
 1. distinct (as @ [y])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct (as @ [y])

goal (2 subgoals):
 1. \<lbrakk>y \<in> set xs; y \<noteq> root\<rbrakk> \<Longrightarrow> contr_sel sel y = ldeep_s sel (rev xs) y
 2. y \<notin> set xs \<Longrightarrow> contr_sel sel y = ldeep_s sel (rev xs) y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distinct (as @ [y])

goal (2 subgoals):
 1. \<lbrakk>y \<in> set xs; y \<noteq> root\<rbrakk> \<Longrightarrow> contr_sel sel y = ldeep_s sel (rev xs) y
 2. y \<notin> set xs \<Longrightarrow> contr_sel sel y = ldeep_s sel (rev xs) y
[PROOF STEP]
have "as \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. as \<noteq> []
[PROOF STEP]
using 2 hd_root as_def
[PROOF STATE]
proof (prove)
using this:
y \<in> set xs
y \<noteq> root
hd xs = root
as @ y # bs = xs

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

goal (2 subgoals):
 1. \<lbrakk>y \<in> set xs; y \<noteq> root\<rbrakk> \<Longrightarrow> contr_sel sel y = ldeep_s sel (rev xs) y
 2. y \<notin> set xs \<Longrightarrow> contr_sel sel y = ldeep_s sel (rev xs) y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
forward (as @ [y])
distinct (as @ [y])
as \<noteq> []
[PROOF STEP]
have "contr_sel sel y = list_sel_aux' sel (rev as) y"
[PROOF STATE]
proof (prove)
using this:
forward (as @ [y])
distinct (as @ [y])
as \<noteq> []

goal (1 subgoal):
 1. contr_sel sel y = list_sel_aux' sel (rev as) y
[PROOF STEP]
using contr_sel_eq_list_sel_aux'_if_tree_sel'[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
forward (as @ [y])
distinct (as @ [y])
as \<noteq> []
\<lbrakk>distinct (?xs @ [?y]); forward (?xs @ [?y]); ?xs \<noteq> []\<rbrakk> \<Longrightarrow> contr_sel sel ?y = list_sel_aux' sel (rev ?xs) ?y

goal (1 subgoal):
 1. contr_sel sel y = list_sel_aux' sel (rev as) y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
contr_sel sel y = list_sel_aux' sel (rev as) y

goal (2 subgoals):
 1. \<lbrakk>y \<in> set xs; y \<noteq> root\<rbrakk> \<Longrightarrow> contr_sel sel y = ldeep_s sel (rev xs) y
 2. y \<notin> set xs \<Longrightarrow> contr_sel sel y = ldeep_s sel (rev xs) y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
contr_sel sel y = list_sel_aux' sel (rev as) y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
contr_sel sel y = list_sel_aux' sel (rev as) y

goal (1 subgoal):
 1. contr_sel sel y = ldeep_s sel (rev xs) y
[PROOF STEP]
using as_def distinct_ldeep_s_eq_aux'[of "rev xs"] assms(2)
[PROOF STATE]
proof (prove)
using this:
contr_sel sel y = list_sel_aux' sel (rev as) y
as @ y # bs = xs
\<lbrakk>distinct (rev xs); ?as @ ?y # ?bs = rev xs\<rbrakk> \<Longrightarrow> ldeep_s ?sel (rev xs) ?y = list_sel_aux' ?sel ?bs ?y
distinct xs

goal (1 subgoal):
 1. contr_sel sel y = ldeep_s sel (rev xs) y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
contr_sel sel y = ldeep_s sel (rev xs) y

goal (1 subgoal):
 1. y \<notin> set xs \<Longrightarrow> contr_sel sel y = ldeep_s sel (rev xs) y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<notin> set xs \<Longrightarrow> contr_sel sel y = ldeep_s sel (rev xs) y
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
y \<notin> set xs

goal (1 subgoal):
 1. y \<notin> set xs \<Longrightarrow> contr_sel sel y = ldeep_s sel (rev xs) y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<notin> set xs
[PROOF STEP]
have "contr_sel sel y = 1"
[PROOF STATE]
proof (prove)
using this:
y \<notin> set xs

goal (1 subgoal):
 1. contr_sel sel y = 1
[PROOF STEP]
using assms(4)
[PROOF STATE]
proof (prove)
using this:
y \<notin> set xs
set xs = verts T

goal (1 subgoal):
 1. contr_sel sel y = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
contr_sel sel y = 1

goal (1 subgoal):
 1. y \<notin> set xs \<Longrightarrow> contr_sel sel y = ldeep_s sel (rev xs) y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
contr_sel sel y = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
contr_sel sel y = 1

goal (1 subgoal):
 1. contr_sel sel y = ldeep_s sel (rev xs) y
[PROOF STEP]
using 3 ldeep_s_1_if_nelem set_rev
[PROOF STATE]
proof (prove)
using this:
contr_sel sel y = 1
y \<notin> set xs
?x \<notin> set ?xs \<Longrightarrow> ldeep_s ?sel ?xs ?x = 1
set (rev ?xs) = set ?xs

goal (1 subgoal):
 1. contr_sel sel y = ldeep_s sel (rev xs) y
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
contr_sel sel y = ldeep_s sel (rev xs) y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
contr_sel sel y = ldeep_s sel (rev xs) y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma add_leaf_forward_arcs_preserv:
  "\<lbrakk>a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs xs\<rbrakk>
    \<Longrightarrow> directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a},
              tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs xs\<rbrakk> \<Longrightarrow> directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> xs
[PROOF STEP]
proof(induction xs rule: forward_arcs.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs []\<rbrakk> \<Longrightarrow> directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> []
 2. \<And>x. \<lbrakk>a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs [x]\<rbrakk> \<Longrightarrow> directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> [x]
 3. \<And>x va vaa. \<lbrakk>\<lbrakk>a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs (va # vaa)\<rbrakk> \<Longrightarrow> directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> (va # vaa); a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs (x # va # vaa)\<rbrakk> \<Longrightarrow> directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> (x # va # vaa)
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
a \<notin> arcs T
u \<in> verts T
v \<notin> verts T
forward_arcs []

goal (3 subgoals):
 1. \<lbrakk>a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs []\<rbrakk> \<Longrightarrow> directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> []
 2. \<And>x. \<lbrakk>a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs [x]\<rbrakk> \<Longrightarrow> directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> [x]
 3. \<And>x va vaa. \<lbrakk>\<lbrakk>a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs (va # vaa)\<rbrakk> \<Longrightarrow> directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> (va # vaa); a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs (x # va # vaa)\<rbrakk> \<Longrightarrow> directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> (x # va # vaa)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<notin> arcs T
u \<in> verts T
v \<notin> verts T
forward_arcs []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
a \<notin> arcs T
u \<in> verts T
v \<notin> verts T
forward_arcs []

goal (1 subgoal):
 1. directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> []
[PROOF STEP]
using directed_tree.forward_arcs.simps(1) add_leaf_dir_tree
[PROOF STATE]
proof (prove)
using this:
a \<notin> arcs T
u \<in> verts T
v \<notin> verts T
forward_arcs []
directed_tree ?T ?root \<Longrightarrow> directed_tree.forward_arcs ?T [] = True
\<lbrakk>?a \<notin> arcs T; ?u \<in> verts T; ?v \<notin> verts T\<rbrakk> \<Longrightarrow> directed_tree \<lparr>verts = verts T \<union> {?v}, arcs = arcs T \<union> {?a}, tail = (tail T)(?a := ?u), head = (head T)(?a := ?v)\<rparr> root

goal (1 subgoal):
 1. directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> []
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> []

goal (2 subgoals):
 1. \<And>x. \<lbrakk>a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs [x]\<rbrakk> \<Longrightarrow> directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> [x]
 2. \<And>x va vaa. \<lbrakk>\<lbrakk>a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs (va # vaa)\<rbrakk> \<Longrightarrow> directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> (va # vaa); a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs (x # va # vaa)\<rbrakk> \<Longrightarrow> directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> (x # va # vaa)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs [x]\<rbrakk> \<Longrightarrow> directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> [x]
 2. \<And>x va vaa. \<lbrakk>\<lbrakk>a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs (va # vaa)\<rbrakk> \<Longrightarrow> directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> (va # vaa); a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs (x # va # vaa)\<rbrakk> \<Longrightarrow> directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> (x # va # vaa)
[PROOF STEP]
case (2 x)
[PROOF STATE]
proof (state)
this:
a \<notin> arcs T
u \<in> verts T
v \<notin> verts T
forward_arcs [x]

goal (2 subgoals):
 1. \<And>x. \<lbrakk>a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs [x]\<rbrakk> \<Longrightarrow> directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> [x]
 2. \<And>x va vaa. \<lbrakk>\<lbrakk>a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs (va # vaa)\<rbrakk> \<Longrightarrow> directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> (va # vaa); a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs (x # va # vaa)\<rbrakk> \<Longrightarrow> directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> (x # va # vaa)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<notin> arcs T
u \<in> verts T
v \<notin> verts T
forward_arcs [x]
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
a \<notin> arcs T
u \<in> verts T
v \<notin> verts T
forward_arcs [x]

goal (1 subgoal):
 1. directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> [x]
[PROOF STEP]
using directed_tree.forward_arcs.simps(2) add_leaf_dir_tree
[PROOF STATE]
proof (prove)
using this:
a \<notin> arcs T
u \<in> verts T
v \<notin> verts T
forward_arcs [x]
directed_tree ?T ?root \<Longrightarrow> directed_tree.forward_arcs ?T [?x] = True
\<lbrakk>?a \<notin> arcs T; ?u \<in> verts T; ?v \<notin> verts T\<rbrakk> \<Longrightarrow> directed_tree \<lparr>verts = verts T \<union> {?v}, arcs = arcs T \<union> {?a}, tail = (tail T)(?a := ?u), head = (head T)(?a := ?v)\<rparr> root

goal (1 subgoal):
 1. directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> [x]
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> [x]

goal (1 subgoal):
 1. \<And>x va vaa. \<lbrakk>\<lbrakk>a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs (va # vaa)\<rbrakk> \<Longrightarrow> directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> (va # vaa); a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs (x # va # vaa)\<rbrakk> \<Longrightarrow> directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> (x # va # vaa)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x va vaa. \<lbrakk>\<lbrakk>a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs (va # vaa)\<rbrakk> \<Longrightarrow> directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> (va # vaa); a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs (x # va # vaa)\<rbrakk> \<Longrightarrow> directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> (x # va # vaa)
[PROOF STEP]
case (3 x y xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs (y # xs)\<rbrakk> \<Longrightarrow> directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> (y # xs)
a \<notin> arcs T
u \<in> verts T
v \<notin> verts T
forward_arcs (x # y # xs)

goal (1 subgoal):
 1. \<And>x va vaa. \<lbrakk>\<lbrakk>a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs (va # vaa)\<rbrakk> \<Longrightarrow> directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> (va # vaa); a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs (x # va # vaa)\<rbrakk> \<Longrightarrow> directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> (x # va # vaa)
[PROOF STEP]
let ?T = "\<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a},
            tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x va vaa. \<lbrakk>\<lbrakk>a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs (va # vaa)\<rbrakk> \<Longrightarrow> directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> (va # vaa); a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs (x # va # vaa)\<rbrakk> \<Longrightarrow> directed_tree.forward_arcs \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> (x # va # vaa)
[PROOF STEP]
interpret T: directed_tree ?T root
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. directed_tree \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> root
[PROOF STEP]
using add_leaf_dir_tree[OF "3.prems"(1-3)]
[PROOF STATE]
proof (prove)
using this:
directed_tree \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> root

goal (1 subgoal):
 1. directed_tree \<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr> root
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x va vaa. \<lbrakk>\<lbrakk>a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs (va # vaa)\<rbrakk> \<Longrightarrow> T.forward_arcs (va # vaa); a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs (x # va # vaa)\<rbrakk> \<Longrightarrow> T.forward_arcs (x # va # vaa)
[PROOF STEP]
have "T.forward_arcs (y # xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T.forward_arcs (y # xs)
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs (y # xs)\<rbrakk> \<Longrightarrow> T.forward_arcs (y # xs)
a \<notin> arcs T
u \<in> verts T
v \<notin> verts T
forward_arcs (x # y # xs)

goal (1 subgoal):
 1. T.forward_arcs (y # xs)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
T.forward_arcs (y # xs)

goal (1 subgoal):
 1. \<And>x va vaa. \<lbrakk>\<lbrakk>a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs (va # vaa)\<rbrakk> \<Longrightarrow> T.forward_arcs (va # vaa); a \<notin> arcs T; u \<in> verts T; v \<notin> verts T; forward_arcs (x # va # vaa)\<rbrakk> \<Longrightarrow> T.forward_arcs (x # va # vaa)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
T.forward_arcs (y # xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
T.forward_arcs (y # xs)

goal (1 subgoal):
 1. T.forward_arcs (x # y # xs)
[PROOF STEP]
using T.forward_arcs.simps(3)[of x y xs] add_leaf_dom_preserv "3.prems"(1,4)
[PROOF STATE]
proof (prove)
using this:
T.forward_arcs (y # xs)
T.forward_arcs (x # y # xs) = ((\<exists>y\<in>set (y # xs). y \<rightarrow>\<^bsub>\<lparr>verts = verts T \<union> {v}, arcs = arcs T \<union> {a}, tail = (tail T)(a := u), head = (head T)(a := v)\<rparr>\<^esub> x) \<and> T.forward_arcs (y # xs))
\<lbrakk>?a \<notin> arcs T; ?x \<rightarrow>\<^bsub>T\<^esub> ?y\<rbrakk> \<Longrightarrow> ?x \<rightarrow>\<^bsub>\<lparr>verts = verts T \<union> {?v}, arcs = arcs T \<union> {?a}, tail = (tail T)(?a := ?u), head = (head T)(?a := ?v)\<rparr>\<^esub> ?y
a \<notin> arcs T
forward_arcs (x # y # xs)

goal (1 subgoal):
 1. T.forward_arcs (x # y # xs)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
T.forward_arcs (x # y # xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dst_fwd_arcs_all_verts_ex: "\<exists>xs. forward_arcs xs \<and> distinct xs \<and> set xs = verts T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>xs. forward_arcs xs \<and> distinct xs \<and> set xs = verts T
[PROOF STEP]
using finite_verts
[PROOF STATE]
proof (prove)
using this:
finite (verts T)

goal (1 subgoal):
 1. \<exists>xs. forward_arcs xs \<and> distinct xs \<and> set xs = verts T
[PROOF STEP]
proof(induction rule: finite_directed_tree_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t h root. \<exists>xs. directed_tree.forward_arcs \<lparr>verts = {root}, arcs = {}, tail = t, head = h\<rparr> xs \<and> distinct xs \<and> set xs = verts \<lparr>verts = {root}, arcs = {}, tail = t, head = h\<rparr>
 2. \<And>T' V A t h u root a v. \<lbrakk>T' = \<lparr>verts = V, arcs = A, tail = t, head = h\<rparr>; finite (verts T'); directed_tree T' root; \<exists>xs. directed_tree.forward_arcs T' xs \<and> distinct xs \<and> set xs = verts T'; u \<in> V; v \<notin> V; a \<notin> A\<rbrakk> \<Longrightarrow> \<exists>xs. directed_tree.forward_arcs \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr> xs \<and> distinct xs \<and> set xs = verts \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr>
[PROOF STEP]
case (single_vert t h root)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>t h root. \<exists>xs. directed_tree.forward_arcs \<lparr>verts = {root}, arcs = {}, tail = t, head = h\<rparr> xs \<and> distinct xs \<and> set xs = verts \<lparr>verts = {root}, arcs = {}, tail = t, head = h\<rparr>
 2. \<And>T' V A t h u root a v. \<lbrakk>T' = \<lparr>verts = V, arcs = A, tail = t, head = h\<rparr>; finite (verts T'); directed_tree T' root; \<exists>xs. directed_tree.forward_arcs T' xs \<and> distinct xs \<and> set xs = verts T'; u \<in> V; v \<notin> V; a \<notin> A\<rbrakk> \<Longrightarrow> \<exists>xs. directed_tree.forward_arcs \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr> xs \<and> distinct xs \<and> set xs = verts \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>xs. directed_tree.forward_arcs \<lparr>verts = {root}, arcs = {}, tail = t, head = h\<rparr> xs \<and> distinct xs \<and> set xs = verts \<lparr>verts = {root}, arcs = {}, tail = t, head = h\<rparr>
[PROOF STEP]
using directed_tree.forward_arcs.simps(2)[OF dir_tree_single]
[PROOF STATE]
proof (prove)
using this:
directed_tree.forward_arcs \<lparr>verts = {?root}, arcs = {}, tail = ?t1, head = ?h1\<rparr> [?x] = True

goal (1 subgoal):
 1. \<exists>xs. directed_tree.forward_arcs \<lparr>verts = {root}, arcs = {}, tail = t, head = h\<rparr> xs \<and> distinct xs \<and> set xs = verts \<lparr>verts = {root}, arcs = {}, tail = t, head = h\<rparr>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>xs. directed_tree.forward_arcs \<lparr>verts = {root}, arcs = {}, tail = t, head = h\<rparr> xs \<and> distinct xs \<and> set xs = verts \<lparr>verts = {root}, arcs = {}, tail = t, head = h\<rparr>

goal (1 subgoal):
 1. \<And>T' V A t h u root a v. \<lbrakk>T' = \<lparr>verts = V, arcs = A, tail = t, head = h\<rparr>; finite (verts T'); directed_tree T' root; \<exists>xs. directed_tree.forward_arcs T' xs \<and> distinct xs \<and> set xs = verts T'; u \<in> V; v \<notin> V; a \<notin> A\<rbrakk> \<Longrightarrow> \<exists>xs. directed_tree.forward_arcs \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr> xs \<and> distinct xs \<and> set xs = verts \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>T' V A t h u root a v. \<lbrakk>T' = \<lparr>verts = V, arcs = A, tail = t, head = h\<rparr>; finite (verts T'); directed_tree T' root; \<exists>xs. directed_tree.forward_arcs T' xs \<and> distinct xs \<and> set xs = verts T'; u \<in> V; v \<notin> V; a \<notin> A\<rbrakk> \<Longrightarrow> \<exists>xs. directed_tree.forward_arcs \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr> xs \<and> distinct xs \<and> set xs = verts \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr>
[PROOF STEP]
case (add_leaf T' V A t h u root a v)
[PROOF STATE]
proof (state)
this:
T' = \<lparr>verts = V, arcs = A, tail = t, head = h\<rparr>
finite (verts T')
directed_tree T' root
u \<in> V
v \<notin> V
a \<notin> A
\<exists>xs. directed_tree.forward_arcs T' xs \<and> distinct xs \<and> set xs = verts T'

goal (1 subgoal):
 1. \<And>T' V A t h u root a v. \<lbrakk>T' = \<lparr>verts = V, arcs = A, tail = t, head = h\<rparr>; finite (verts T'); directed_tree T' root; \<exists>xs. directed_tree.forward_arcs T' xs \<and> distinct xs \<and> set xs = verts T'; u \<in> V; v \<notin> V; a \<notin> A\<rbrakk> \<Longrightarrow> \<exists>xs. directed_tree.forward_arcs \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr> xs \<and> distinct xs \<and> set xs = verts \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr>
[PROOF STEP]
define T where "T \<equiv> \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr>"
[PROOF STATE]
proof (state)
this:
T \<equiv> \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr>

goal (1 subgoal):
 1. \<And>T' V A t h u root a v. \<lbrakk>T' = \<lparr>verts = V, arcs = A, tail = t, head = h\<rparr>; finite (verts T'); directed_tree T' root; \<exists>xs. directed_tree.forward_arcs T' xs \<and> distinct xs \<and> set xs = verts T'; u \<in> V; v \<notin> V; a \<notin> A\<rbrakk> \<Longrightarrow> \<exists>xs. directed_tree.forward_arcs \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr> xs \<and> distinct xs \<and> set xs = verts \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr>
[PROOF STEP]
interpret T': directed_tree T' root
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. directed_tree T' root
[PROOF STEP]
using add_leaf.hyps(3)
[PROOF STATE]
proof (prove)
using this:
directed_tree T' root

goal (1 subgoal):
 1. directed_tree T' root
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>T' V A t h u root a v. \<lbrakk>T' = \<lparr>verts = V, arcs = A, tail = t, head = h\<rparr>; finite (verts T'); directed_tree T' root; \<exists>xs. directed_tree.forward_arcs T' xs \<and> distinct xs \<and> set xs = verts T'; u \<in> V; v \<notin> V; a \<notin> A\<rbrakk> \<Longrightarrow> \<exists>xs. directed_tree.forward_arcs \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr> xs \<and> distinct xs \<and> set xs = verts \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr>
[PROOF STEP]
interpret T: directed_tree T root
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. directed_tree T root
[PROOF STEP]
using add_leaf.hyps(1,4-6) T'.add_leaf_dir_tree T_def
[PROOF STATE]
proof (prove)
using this:
T' = \<lparr>verts = V, arcs = A, tail = t, head = h\<rparr>
u \<in> V
v \<notin> V
a \<notin> A
\<lbrakk>?a \<notin> arcs T'; ?u \<in> verts T'; ?v \<notin> verts T'\<rbrakk> \<Longrightarrow> directed_tree \<lparr>verts = verts T' \<union> {?v}, arcs = arcs T' \<union> {?a}, tail = (tail T')(?a := ?u), head = (head T')(?a := ?v)\<rparr> root
T \<equiv> \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr>

goal (1 subgoal):
 1. directed_tree T root
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>T' V A t h u root a v. \<lbrakk>T' = \<lparr>verts = V, arcs = A, tail = t, head = h\<rparr>; finite (verts T'); directed_tree T' root; \<exists>xs. directed_tree.forward_arcs T' xs \<and> distinct xs \<and> set xs = verts T'; u \<in> V; v \<notin> V; a \<notin> A\<rbrakk> \<Longrightarrow> \<exists>xs. directed_tree.forward_arcs \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr> xs \<and> distinct xs \<and> set xs = verts \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr>
[PROOF STEP]
obtain xs where xs_def: "T'.forward_arcs xs" "distinct xs" "set xs = verts T'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xs. \<lbrakk>T'.forward_arcs xs; distinct xs; set xs = verts T'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using add_leaf.IH
[PROOF STATE]
proof (prove)
using this:
\<exists>xs. T'.forward_arcs xs \<and> distinct xs \<and> set xs = verts T'

goal (1 subgoal):
 1. (\<And>xs. \<lbrakk>T'.forward_arcs xs; distinct xs; set xs = verts T'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
T'.forward_arcs xs
distinct xs
set xs = verts T'

goal (1 subgoal):
 1. \<And>T' V A t h u root a v. \<lbrakk>T' = \<lparr>verts = V, arcs = A, tail = t, head = h\<rparr>; finite (verts T'); directed_tree T' root; \<exists>xs. directed_tree.forward_arcs T' xs \<and> distinct xs \<and> set xs = verts T'; u \<in> V; v \<notin> V; a \<notin> A\<rbrakk> \<Longrightarrow> \<exists>xs. directed_tree.forward_arcs \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr> xs \<and> distinct xs \<and> set xs = verts \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
T'.forward_arcs xs
distinct xs
set xs = verts T'
[PROOF STEP]
have "T.forward_arcs xs"
[PROOF STATE]
proof (prove)
using this:
T'.forward_arcs xs
distinct xs
set xs = verts T'

goal (1 subgoal):
 1. T.forward_arcs xs
[PROOF STEP]
using T'.add_leaf_forward_arcs_preserv add_leaf.hyps(1,4,5,6) T_def
[PROOF STATE]
proof (prove)
using this:
T'.forward_arcs xs
distinct xs
set xs = verts T'
\<lbrakk>?a \<notin> arcs T'; ?u \<in> verts T'; ?v \<notin> verts T'; T'.forward_arcs ?xs\<rbrakk> \<Longrightarrow> directed_tree.forward_arcs \<lparr>verts = verts T' \<union> {?v}, arcs = arcs T' \<union> {?a}, tail = (tail T')(?a := ?u), head = (head T')(?a := ?v)\<rparr> ?xs
T' = \<lparr>verts = V, arcs = A, tail = t, head = h\<rparr>
u \<in> V
v \<notin> V
a \<notin> A
T \<equiv> \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr>

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

goal (1 subgoal):
 1. \<And>T' V A t h u root a v. \<lbrakk>T' = \<lparr>verts = V, arcs = A, tail = t, head = h\<rparr>; finite (verts T'); directed_tree T' root; \<exists>xs. directed_tree.forward_arcs T' xs \<and> distinct xs \<and> set xs = verts T'; u \<in> V; v \<notin> V; a \<notin> A\<rbrakk> \<Longrightarrow> \<exists>xs. directed_tree.forward_arcs \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr> xs \<and> distinct xs \<and> set xs = verts \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
T.forward_arcs xs

goal (1 subgoal):
 1. \<And>T' V A t h u root a v. \<lbrakk>T' = \<lparr>verts = V, arcs = A, tail = t, head = h\<rparr>; finite (verts T'); directed_tree T' root; \<exists>xs. directed_tree.forward_arcs T' xs \<and> distinct xs \<and> set xs = verts T'; u \<in> V; v \<notin> V; a \<notin> A\<rbrakk> \<Longrightarrow> \<exists>xs. directed_tree.forward_arcs \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr> xs \<and> distinct xs \<and> set xs = verts \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr>
[PROOF STEP]
have "\<exists>y\<in>set xs. y \<rightarrow>\<^bsub>T\<^esub> v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y\<in>set xs. y \<rightarrow>\<^bsub>T\<^esub> v
[PROOF STEP]
using add_leaf.hyps(1,4) T_def xs_def(3)
[PROOF STATE]
proof (prove)
using this:
T' = \<lparr>verts = V, arcs = A, tail = t, head = h\<rparr>
u \<in> V
T \<equiv> \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr>
set xs = verts T'

goal (1 subgoal):
 1. \<exists>y\<in>set xs. y \<rightarrow>\<^bsub>T\<^esub> v
[PROOF STEP]
unfolding arcs_ends_def arc_to_ends_def
[PROOF STATE]
proof (prove)
using this:
T' = \<lparr>verts = V, arcs = A, tail = t, head = h\<rparr>
u \<in> V
T \<equiv> \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr>
set xs = verts T'

goal (1 subgoal):
 1. \<exists>y\<in>set xs. (y, v) \<in> (\<lambda>e. (tail T e, head T e)) ` arcs T
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>set xs. y \<rightarrow>\<^bsub>T\<^esub> v

goal (1 subgoal):
 1. \<And>T' V A t h u root a v. \<lbrakk>T' = \<lparr>verts = V, arcs = A, tail = t, head = h\<rparr>; finite (verts T'); directed_tree T' root; \<exists>xs. directed_tree.forward_arcs T' xs \<and> distinct xs \<and> set xs = verts T'; u \<in> V; v \<notin> V; a \<notin> A\<rbrakk> \<Longrightarrow> \<exists>xs. directed_tree.forward_arcs \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr> xs \<and> distinct xs \<and> set xs = verts \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
T.forward_arcs xs
\<exists>y\<in>set xs. y \<rightarrow>\<^bsub>T\<^esub> v
[PROOF STEP]
have "T.forward_arcs (v#xs)"
[PROOF STATE]
proof (prove)
using this:
T.forward_arcs xs
\<exists>y\<in>set xs. y \<rightarrow>\<^bsub>T\<^esub> v

goal (1 subgoal):
 1. T.forward_arcs (v # xs)
[PROOF STEP]
using T.forward_arcs.elims(3)
[PROOF STATE]
proof (prove)
using this:
T.forward_arcs xs
\<exists>y\<in>set xs. y \<rightarrow>\<^bsub>T\<^esub> v
\<lbrakk>\<not> T.forward_arcs ?x; \<And>x v va. \<lbrakk>?x = x # v # va; \<not> ((\<exists>y\<in>set (v # va). y \<rightarrow>\<^bsub>T\<^esub> x) \<and> T.forward_arcs (v # va))\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. T.forward_arcs (v # xs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
T.forward_arcs (v # xs)

goal (1 subgoal):
 1. \<And>T' V A t h u root a v. \<lbrakk>T' = \<lparr>verts = V, arcs = A, tail = t, head = h\<rparr>; finite (verts T'); directed_tree T' root; \<exists>xs. directed_tree.forward_arcs T' xs \<and> distinct xs \<and> set xs = verts T'; u \<in> V; v \<notin> V; a \<notin> A\<rbrakk> \<Longrightarrow> \<exists>xs. directed_tree.forward_arcs \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr> xs \<and> distinct xs \<and> set xs = verts \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
T.forward_arcs (v # xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
T.forward_arcs (v # xs)

goal (1 subgoal):
 1. \<exists>xs. directed_tree.forward_arcs \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr> xs \<and> distinct xs \<and> set xs = verts \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr>
[PROOF STEP]
using xs_def(2,3) add_leaf.hyps(1,5) T_def
[PROOF STATE]
proof (prove)
using this:
T.forward_arcs (v # xs)
distinct xs
set xs = verts T'
T' = \<lparr>verts = V, arcs = A, tail = t, head = h\<rparr>
v \<notin> V
T \<equiv> \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr>

goal (1 subgoal):
 1. \<exists>xs. directed_tree.forward_arcs \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr> xs \<and> distinct xs \<and> set xs = verts \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>xs. directed_tree.forward_arcs \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr> xs \<and> distinct xs \<and> set xs = verts \<lparr>verts = V \<union> {v}, arcs = A \<union> {a}, tail = t(a := u), head = h(a := v)\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dst_fwd_all_verts_ex: "\<exists>xs. forward xs \<and> distinct xs \<and> set xs = verts T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>xs. forward xs \<and> distinct xs \<and> set xs = verts T
[PROOF STEP]
using dst_fwd_arcs_all_verts_ex forward_arcs_alt'[symmetric]
[PROOF STATE]
proof (prove)
using this:
\<exists>xs. forward_arcs xs \<and> distinct xs \<and> set xs = verts T
forward_arcs ?xs = forward (rev ?xs)

goal (1 subgoal):
 1. \<exists>xs. forward xs \<and> distinct xs \<and> set xs = verts T
[PROOF STEP]
by auto


[STATEMENT]
lemma c_list_asi_if_tree_sel:
  fixes sf cf h r
  defines "rank \<equiv> (\<lambda>l. (ldeep_T (contr_sel sf) cf l - 1) / c_list (contr_sel sf) cf h r l)"
  assumes "tree_sel sf"
      and "sel_reasonable sf"
      and "\<forall>x. cf x > 0"
      and "\<forall>x. h x > 0"
    shows "asi rank r (c_list (contr_sel sf) cf h r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. asi rank r (c_list (contr_sel sf) cf h r)
[PROOF STEP]
using c_list_asi assms contr_sel_eq_ldeep_s_if_tree_dst_fwd_verts' dst_fwd_all_verts_ex
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>sel_reasonable ?sf; \<forall>x. 0 < ?cf x; \<forall>x. 0 < ?h x\<rbrakk> \<Longrightarrow> asi (\<lambda>l. (ldeep_T (ldeep_s ?sf ?xs) ?cf l - 1) / c_list (ldeep_s ?sf ?xs) ?cf ?h ?r l) ?r (c_list (ldeep_s ?sf ?xs) ?cf ?h ?r)
rank \<equiv> \<lambda>l. (ldeep_T (contr_sel sf) cf l - 1) / c_list (contr_sel sf) cf h r l
tree_sel sf
sel_reasonable sf
\<forall>x. 0 < cf x
\<forall>x. 0 < h x
\<lbrakk>tree_sel ?sel; distinct ?xs; forward ?xs; set ?xs = verts T\<rbrakk> \<Longrightarrow> contr_sel ?sel = ldeep_s ?sel (rev ?xs)
\<exists>xs. forward xs \<and> distinct xs \<and> set xs = verts T

goal (1 subgoal):
 1. asi rank r (c_list (contr_sel sf) cf h r)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma dom_in_dir_tree_r:
  assumes "r \<in> verts G" and "x \<rightarrow>\<^bsub>G\<^esub> y"
  shows "x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x
[PROOF STEP]
obtain e1 where e1_def: "e1 \<in> arcs G" "tail G e1 = x" "head G e1 = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>e1. \<lbrakk>e1 \<in> arcs G; tail G e1 = x; head G e1 = y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
x \<rightarrow>\<^bsub>G\<^esub> y

goal (1 subgoal):
 1. (\<And>e1. \<lbrakk>e1 \<in> arcs G; tail G e1 = x; head G e1 = y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding arcs_ends_def arc_to_ends_def
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> (\<lambda>e. (tail G e, head G e)) ` arcs G

goal (1 subgoal):
 1. (\<And>e1. \<lbrakk>e1 \<in> arcs G; tail G e1 = x; head G e1 = y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
e1 \<in> arcs G
tail G e1 = x
head G e1 = y

goal (1 subgoal):
 1. x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e1 \<in> arcs G
tail G e1 = x
head G e1 = y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
e1 \<in> arcs G
tail G e1 = x
head G e1 = y

goal (1 subgoal):
 1. x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x
[PROOF STEP]
proof(cases "e1 \<in> arcs (dir_tree_r r)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>e1 \<in> arcs G; tail G e1 = x; head G e1 = y; e1 \<in> arcs (dir_tree_r r)\<rbrakk> \<Longrightarrow> x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x
 2. \<lbrakk>e1 \<in> arcs G; tail G e1 = x; head G e1 = y; e1 \<notin> arcs (dir_tree_r r)\<rbrakk> \<Longrightarrow> x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
e1 \<in> arcs (dir_tree_r r)

goal (2 subgoals):
 1. \<lbrakk>e1 \<in> arcs G; tail G e1 = x; head G e1 = y; e1 \<in> arcs (dir_tree_r r)\<rbrakk> \<Longrightarrow> x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x
 2. \<lbrakk>e1 \<in> arcs G; tail G e1 = x; head G e1 = y; e1 \<notin> arcs (dir_tree_r r)\<rbrakk> \<Longrightarrow> x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
e1 \<in> arcs (dir_tree_r r)

goal (2 subgoals):
 1. \<lbrakk>e1 \<in> arcs G; tail G e1 = x; head G e1 = y; e1 \<in> arcs (dir_tree_r r)\<rbrakk> \<Longrightarrow> x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x
 2. \<lbrakk>e1 \<in> arcs G; tail G e1 = x; head G e1 = y; e1 \<notin> arcs (dir_tree_r r)\<rbrakk> \<Longrightarrow> x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x
[PROOF STEP]
have "tail (dir_tree_r r) e1 = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tail (dir_tree_r r) e1 = x
[PROOF STEP]
using e1_def(2) tail_dir_tree_r_eq[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
tail G e1 = x
tail (dir_tree_r r) ?e = tail G ?e

goal (1 subgoal):
 1. tail (dir_tree_r r) e1 = x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
tail (dir_tree_r r) e1 = x

goal (2 subgoals):
 1. \<lbrakk>e1 \<in> arcs G; tail G e1 = x; head G e1 = y; e1 \<in> arcs (dir_tree_r r)\<rbrakk> \<Longrightarrow> x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x
 2. \<lbrakk>e1 \<in> arcs G; tail G e1 = x; head G e1 = y; e1 \<notin> arcs (dir_tree_r r)\<rbrakk> \<Longrightarrow> x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
tail (dir_tree_r r) e1 = x

goal (2 subgoals):
 1. \<lbrakk>e1 \<in> arcs G; tail G e1 = x; head G e1 = y; e1 \<in> arcs (dir_tree_r r)\<rbrakk> \<Longrightarrow> x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x
 2. \<lbrakk>e1 \<in> arcs G; tail G e1 = x; head G e1 = y; e1 \<notin> arcs (dir_tree_r r)\<rbrakk> \<Longrightarrow> x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x
[PROOF STEP]
have "head (dir_tree_r r) e1 = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. head (dir_tree_r r) e1 = y
[PROOF STEP]
using e1_def(3) head_dir_tree_r_eq[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
head G e1 = y
head (dir_tree_r r) ?e = head G ?e

goal (1 subgoal):
 1. head (dir_tree_r r) e1 = y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
head (dir_tree_r r) e1 = y

goal (2 subgoals):
 1. \<lbrakk>e1 \<in> arcs G; tail G e1 = x; head G e1 = y; e1 \<in> arcs (dir_tree_r r)\<rbrakk> \<Longrightarrow> x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x
 2. \<lbrakk>e1 \<in> arcs G; tail G e1 = x; head G e1 = y; e1 \<notin> arcs (dir_tree_r r)\<rbrakk> \<Longrightarrow> x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
e1 \<in> arcs (dir_tree_r r)
tail (dir_tree_r r) e1 = x
head (dir_tree_r r) e1 = y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
e1 \<in> arcs (dir_tree_r r)
tail (dir_tree_r r) e1 = x
head (dir_tree_r r) e1 = y

goal (1 subgoal):
 1. x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x
[PROOF STEP]
using e1_def(1)
[PROOF STATE]
proof (prove)
using this:
e1 \<in> arcs (dir_tree_r r)
tail (dir_tree_r r) e1 = x
head (dir_tree_r r) e1 = y
e1 \<in> arcs G

goal (1 subgoal):
 1. x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x
[PROOF STEP]
unfolding arcs_ends_def arc_to_ends_def
[PROOF STATE]
proof (prove)
using this:
e1 \<in> arcs (dir_tree_r r)
tail (dir_tree_r r) e1 = x
head (dir_tree_r r) e1 = y
e1 \<in> arcs G

goal (1 subgoal):
 1. (x, y) \<in> (\<lambda>e. (tail (dir_tree_r r) e, head (dir_tree_r r) e)) ` arcs (dir_tree_r r) \<or> (y, x) \<in> (\<lambda>e. (tail (dir_tree_r r) e, head (dir_tree_r r) e)) ` arcs (dir_tree_r r)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x

goal (1 subgoal):
 1. \<lbrakk>e1 \<in> arcs G; tail G e1 = x; head G e1 = y; e1 \<notin> arcs (dir_tree_r r)\<rbrakk> \<Longrightarrow> x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>e1 \<in> arcs G; tail G e1 = x; head G e1 = y; e1 \<notin> arcs (dir_tree_r r)\<rbrakk> \<Longrightarrow> x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
e1 \<notin> arcs (dir_tree_r r)

goal (1 subgoal):
 1. \<lbrakk>e1 \<in> arcs G; tail G e1 = x; head G e1 = y; e1 \<notin> arcs (dir_tree_r r)\<rbrakk> \<Longrightarrow> x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e1 \<notin> arcs (dir_tree_r r)
[PROOF STEP]
obtain e2 where e2_def: "e2 \<in> arcs (dir_tree_r r)" "tail G e2 = y" "head G e2 = x"
[PROOF STATE]
proof (prove)
using this:
e1 \<notin> arcs (dir_tree_r r)

goal (1 subgoal):
 1. (\<And>e2. \<lbrakk>e2 \<in> arcs (dir_tree_r r); tail G e2 = y; head G e2 = x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using arcs_compl_un_eq_arcs[OF assms(1)] e1_def
[PROOF STATE]
proof (prove)
using this:
e1 \<notin> arcs (dir_tree_r r)
{e2 \<in> arcs G. \<exists>e1\<in>arcs (dir_tree_r r). head G e2 = tail G e1 \<and> head G e1 = tail G e2} \<union> arcs (dir_tree_r r) = arcs G
e1 \<in> arcs G
tail G e1 = x
head G e1 = y

goal (1 subgoal):
 1. (\<And>e2. \<lbrakk>e2 \<in> arcs (dir_tree_r r); tail G e2 = y; head G e2 = x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
e2 \<in> arcs (dir_tree_r r)
tail G e2 = y
head G e2 = x

goal (1 subgoal):
 1. \<lbrakk>e1 \<in> arcs G; tail G e1 = x; head G e1 = y; e1 \<notin> arcs (dir_tree_r r)\<rbrakk> \<Longrightarrow> x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x
[PROOF STEP]
have "tail (dir_tree_r r) e2 = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tail (dir_tree_r r) e2 = y
[PROOF STEP]
using e2_def(2) tail_dir_tree_r_eq[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
tail G e2 = y
tail (dir_tree_r r) ?e = tail G ?e

goal (1 subgoal):
 1. tail (dir_tree_r r) e2 = y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
tail (dir_tree_r r) e2 = y

goal (1 subgoal):
 1. \<lbrakk>e1 \<in> arcs G; tail G e1 = x; head G e1 = y; e1 \<notin> arcs (dir_tree_r r)\<rbrakk> \<Longrightarrow> x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
tail (dir_tree_r r) e2 = y

goal (1 subgoal):
 1. \<lbrakk>e1 \<in> arcs G; tail G e1 = x; head G e1 = y; e1 \<notin> arcs (dir_tree_r r)\<rbrakk> \<Longrightarrow> x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x
[PROOF STEP]
have "head (dir_tree_r r) e2 = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. head (dir_tree_r r) e2 = x
[PROOF STEP]
using e2_def(3) head_dir_tree_r_eq[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
head G e2 = x
head (dir_tree_r r) ?e = head G ?e

goal (1 subgoal):
 1. head (dir_tree_r r) e2 = x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
head (dir_tree_r r) e2 = x

goal (1 subgoal):
 1. \<lbrakk>e1 \<in> arcs G; tail G e1 = x; head G e1 = y; e1 \<notin> arcs (dir_tree_r r)\<rbrakk> \<Longrightarrow> x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
tail (dir_tree_r r) e2 = y
head (dir_tree_r r) e2 = x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
tail (dir_tree_r r) e2 = y
head (dir_tree_r r) e2 = x

goal (1 subgoal):
 1. x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x
[PROOF STEP]
using e2_def(1)
[PROOF STATE]
proof (prove)
using this:
tail (dir_tree_r r) e2 = y
head (dir_tree_r r) e2 = x
e2 \<in> arcs (dir_tree_r r)

goal (1 subgoal):
 1. x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x
[PROOF STEP]
unfolding arcs_ends_def arc_to_ends_def
[PROOF STATE]
proof (prove)
using this:
tail (dir_tree_r r) e2 = y
head (dir_tree_r r) e2 = x
e2 \<in> arcs (dir_tree_r r)

goal (1 subgoal):
 1. (x, y) \<in> (\<lambda>e. (tail (dir_tree_r r) e, head (dir_tree_r r) e)) ` arcs (dir_tree_r r) \<or> (y, x) \<in> (\<lambda>e. (tail (dir_tree_r r) e, head (dir_tree_r r) e)) ` arcs (dir_tree_r r)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dom_in_dir_tree_r_iff_aux:
  "r \<in> verts G \<Longrightarrow> (x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x) \<longleftrightarrow> (x \<rightarrow>\<^bsub>G\<^esub> y \<or> y \<rightarrow>\<^bsub>G\<^esub> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> verts G \<Longrightarrow> (x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x) = (x \<rightarrow>\<^bsub>G\<^esub> y \<or> y \<rightarrow>\<^bsub>G\<^esub> x)
[PROOF STEP]
using dir_tree_r_dom_in_G dom_in_dir_tree_r
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?r \<in> verts G; ?u \<rightarrow>\<^bsub>dir_tree_r ?r\<^esub> ?v\<rbrakk> \<Longrightarrow> ?u \<rightarrow>\<^bsub>G\<^esub> ?v
\<lbrakk>?r \<in> verts G; ?x \<rightarrow>\<^bsub>G\<^esub> ?y\<rbrakk> \<Longrightarrow> ?x \<rightarrow>\<^bsub>dir_tree_r ?r\<^esub> ?y \<or> ?y \<rightarrow>\<^bsub>dir_tree_r ?r\<^esub> ?x

goal (1 subgoal):
 1. r \<in> verts G \<Longrightarrow> (x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x) = (x \<rightarrow>\<^bsub>G\<^esub> y \<or> y \<rightarrow>\<^bsub>G\<^esub> x)
[PROOF STEP]
by blast


[STATEMENT]
lemma dom_in_dir_tree_r_iff:
  "r \<in> verts G \<Longrightarrow> (x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x) \<longleftrightarrow> x \<rightarrow>\<^bsub>G\<^esub> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> verts G \<Longrightarrow> (x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x) = (x \<rightarrow>\<^bsub>G\<^esub> y)
[PROOF STEP]
using dom_in_dir_tree_r_iff_aux dominates_sym
[PROOF STATE]
proof (prove)
using this:
?r \<in> verts G \<Longrightarrow> (?x \<rightarrow>\<^bsub>dir_tree_r ?r\<^esub> ?y \<or> ?y \<rightarrow>\<^bsub>dir_tree_r ?r\<^esub> ?x) = (?x \<rightarrow>\<^bsub>G\<^esub> ?y \<or> ?y \<rightarrow>\<^bsub>G\<^esub> ?x)
(?x \<rightarrow>\<^bsub>G\<^esub> ?y) = (?y \<rightarrow>\<^bsub>G\<^esub> ?x)

goal (1 subgoal):
 1. r \<in> verts G \<Longrightarrow> (x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x) = (x \<rightarrow>\<^bsub>G\<^esub> y)
[PROOF STEP]
by blast


[STATEMENT]
lemma dir_tree_sel[intro]: "r \<in> verts G \<Longrightarrow> directed_tree.tree_sel (dir_tree_r r) match_sel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> verts G \<Longrightarrow> directed_tree.tree_sel (dir_tree_r r) match_sel
[PROOF STEP]
unfolding directed_tree.tree_sel_def[OF directed_tree_r]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> verts G \<Longrightarrow> \<forall>x y. \<not> (x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x) \<longrightarrow> match_sel x y = 1
[PROOF STEP]
using match_sel1_if_no_arc dom_in_dir_tree_r_iff
[PROOF STATE]
proof (prove)
using this:
\<not> (?x \<rightarrow>\<^bsub>G\<^esub> ?y \<or> ?y \<rightarrow>\<^bsub>G\<^esub> ?x) \<Longrightarrow> match_sel ?x ?y = 1
?r \<in> verts G \<Longrightarrow> (?x \<rightarrow>\<^bsub>dir_tree_r ?r\<^esub> ?y \<or> ?y \<rightarrow>\<^bsub>dir_tree_r ?r\<^esub> ?x) = (?x \<rightarrow>\<^bsub>G\<^esub> ?y)

goal (1 subgoal):
 1. r \<in> verts G \<Longrightarrow> \<forall>x y. \<not> (x \<rightarrow>\<^bsub>dir_tree_r r\<^esub> y \<or> y \<rightarrow>\<^bsub>dir_tree_r r\<^esub> x) \<longrightarrow> match_sel x y = 1
[PROOF STEP]
by blast


[STATEMENT]
lemma pos_cards'[intro!]: "\<forall>x. cf' x > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. 0 < cf' x
[PROOF STEP]
unfolding cf'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. 0 < (if x \<in> verts G then cf x else 1)
[PROOF STEP]
using pos_cards
[PROOF STATE]
proof (prove)
using this:
?x \<in> verts G \<Longrightarrow> 0 < cf ?x

goal (1 subgoal):
 1. \<forall>x. 0 < (if x \<in> verts G then cf x else 1)
[PROOF STEP]
by simp


[STATEMENT]
theorem c_list_asi: "\<lbrakk>r \<in> verts G; \<forall>x. h x > 0\<rbrakk> \<Longrightarrow> asi (rank_r h r) r (c_list_r h r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<in> verts G; \<forall>x. 0 < h x\<rbrakk> \<Longrightarrow> asi (rank_r h r) r (c_list_r h r)
[PROOF STEP]
using finite_directed_tree.c_list_asi_if_tree_sel[OF fin_directed_tree_r]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?root \<in> verts G; directed_tree.tree_sel (dir_tree_r ?root) ?sf; sel_reasonable ?sf; \<forall>x. 0 < ?cf x; \<forall>x. 0 < ?h x\<rbrakk> \<Longrightarrow> asi (\<lambda>l. (ldeep_T (directed_tree.contr_sel (dir_tree_r ?root) ?sf) ?cf l - 1) / c_list (directed_tree.contr_sel (dir_tree_r ?root) ?sf) ?cf ?h ?r l) ?r (c_list (directed_tree.contr_sel (dir_tree_r ?root) ?sf) ?cf ?h ?r)

goal (1 subgoal):
 1. \<lbrakk>r \<in> verts G; \<forall>x. 0 < h x\<rbrakk> \<Longrightarrow> asi (rank_r h r) r (c_list_r h r)
[PROOF STEP]
unfolding c_list_r_def rank_r_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?root \<in> verts G; directed_tree.tree_sel (dir_tree_r ?root) ?sf; sel_reasonable ?sf; \<forall>x. 0 < ?cf x; \<forall>x. 0 < ?h x\<rbrakk> \<Longrightarrow> asi (\<lambda>l. (ldeep_T (directed_tree.contr_sel (dir_tree_r ?root) ?sf) ?cf l - 1) / c_list (directed_tree.contr_sel (dir_tree_r ?root) ?sf) ?cf ?h ?r l) ?r (c_list (directed_tree.contr_sel (dir_tree_r ?root) ?sf) ?cf ?h ?r)

goal (1 subgoal):
 1. \<lbrakk>r \<in> verts G; \<forall>x. 0 < h x\<rbrakk> \<Longrightarrow> asi (\<lambda>xs. (ldeep_T (sel_r r) cf' xs - 1) / c_list (sel_r r) cf' h r xs) r (c_list (sel_r r) cf' h r)
[PROOF STEP]
by blast


[STATEMENT]
lemma cf'_simp: "x \<in> verts G \<Longrightarrow> cf' x = cf x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> verts G \<Longrightarrow> cf' x = cf x
[PROOF STEP]
unfolding cf'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> verts G \<Longrightarrow> (if x \<in> verts G then cf x else 1) = cf x
[PROOF STEP]
by simp


[STATEMENT]
lemma ldeep_T_cf'_eq: "set xs \<subseteq> verts G \<Longrightarrow> ldeep_T sf cf' xs = ldeep_T sf cf xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set xs \<subseteq> verts G \<Longrightarrow> ldeep_T sf cf' xs = ldeep_T sf cf xs
[PROOF STEP]
using ldeep_T_eq_if_cf_eq[of xs] cf'_simp
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set xs. ?f x = ?g x \<Longrightarrow> ldeep_T ?sf ?f xs = ldeep_T ?sf ?g xs
?x \<in> verts G \<Longrightarrow> cf' ?x = cf ?x

goal (1 subgoal):
 1. set xs \<subseteq> verts G \<Longrightarrow> ldeep_T sf cf' xs = ldeep_T sf cf xs
[PROOF STEP]
by blast


[STATEMENT]
lemma clist_cf'_eq: "set xs \<subseteq> verts G \<Longrightarrow> c_list sf cf' h r xs = c_list sf cf h r xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set xs \<subseteq> verts G \<Longrightarrow> c_list sf cf' h r xs = c_list sf cf h r xs
[PROOF STEP]
by (simp add: clist_eq_if_cf_eq ldeep_T_cf'_eq)


[STATEMENT]
lemma card_cf'_eq: "matching_rels t \<Longrightarrow> card cf' f t = card cf f t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matching_rels t \<Longrightarrow> JoinTree.card cf' f t = JoinTree.card cf f t
[PROOF STEP]
by (induction cf' f t rule: card.induct) (auto simp: matching_rels_def cf'_simp)


[STATEMENT]
lemma c_IKKBZ_cf'_eq: "matching_rels t \<Longrightarrow> c_IKKBZ h cf' sf t = c_IKKBZ h cf sf t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matching_rels t \<Longrightarrow> c_IKKBZ h cf' sf t = c_IKKBZ h cf sf t
[PROOF STEP]
by (induction h cf' sf t rule: c_IKKBZ.induct) (auto simp: card_cf'_eq cf'_simp matching_rels_def)


[STATEMENT]
lemma c_IKKBZ_cf'_eq': "valid_tree t \<Longrightarrow> c_IKKBZ h cf' sf t = c_IKKBZ h cf sf t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_tree t \<Longrightarrow> c_IKKBZ h cf' sf t = c_IKKBZ h cf sf t
[PROOF STEP]
by (simp add: c_IKKBZ_cf'_eq matching_rels_def valid_tree_def)


[STATEMENT]
lemma c_out_cf'_eq: "matching_rels t \<Longrightarrow> c_out cf' sf t = c_out cf sf t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matching_rels t \<Longrightarrow> c_out cf' sf t = c_out cf sf t
[PROOF STEP]
by (induction cf' sf t rule: c_out.induct) (auto simp: card_cf'_eq cf'_simp matching_rels_def)