[STATEMENT]
lemma disc_imp_back_edge_or_pending:
    "\<lbrakk>w \<in> succ v; v \<in> dom (discovered s); w \<in> dom (discovered s); \<delta> s w \<le> \<delta> s v;
      (w \<in> dom (finished s) \<Longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w)\<rbrakk>
     \<Longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w \<in> E `` {v}; v \<in> dom (discovered s); w \<in> dom (discovered s); \<delta> s w \<le> \<delta> s v; w \<in> dom (finished s) \<Longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w\<rbrakk> \<Longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s
[PROOF STEP]
using i_disc_imp_back_edge_or_pending[THEN make_invar_thm]
[PROOF STATE]
proof (prove)
using this:
\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s

goal (1 subgoal):
 1. \<lbrakk>w \<in> E `` {v}; v \<in> dom (discovered s); w \<in> dom (discovered s); \<delta> s w \<le> \<delta> s v; w \<in> dom (finished s) \<Longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w\<rbrakk> \<Longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s
[PROOF STEP]
by blast


[STATEMENT]
lemma finished_imp_back_edge:
    "\<lbrakk>w \<in> succ v; v \<in> dom (finished s); w \<in> dom (finished s);
      \<delta> s w \<le> \<delta> s v; \<phi> s v \<le> \<phi> s w\<rbrakk>
     \<Longrightarrow> (v, w) \<in> back_edges s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w \<in> E `` {v}; v \<in> dom (finished s); w \<in> dom (finished s); \<delta> s w \<le> \<delta> s v; \<phi> s v \<le> \<phi> s w\<rbrakk> \<Longrightarrow> (v, w) \<in> back_edges s
[PROOF STEP]
using disc_imp_back_edge_or_pending finished_discovered finished_no_pending
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?w \<in> E `` {?v}; ?v \<in> dom (discovered s); ?w \<in> dom (discovered s); \<delta> s ?w \<le> \<delta> s ?v; ?w \<in> dom (finished s) \<Longrightarrow> ?v \<in> dom (finished s) \<and> \<phi> s ?v \<le> \<phi> s ?w\<rbrakk> \<Longrightarrow> (?v, ?w) \<in> back_edges s \<or> (?v, ?w) \<in> pending s
dom (finished s) \<subseteq> dom (discovered s)
?v \<in> dom (finished s) \<Longrightarrow> pending s `` {?v} = {}

goal (1 subgoal):
 1. \<lbrakk>w \<in> E `` {v}; v \<in> dom (finished s); w \<in> dom (finished s); \<delta> s w \<le> \<delta> s v; \<phi> s v \<le> \<phi> s w\<rbrakk> \<Longrightarrow> (v, w) \<in> back_edges s
[PROOF STEP]
by fast


[STATEMENT]
lemma finished_not_finished_imp_back_edge:
    "\<lbrakk>w \<in> succ v; v \<in> dom (finished s); w \<in> dom (discovered s);
      w \<notin> dom (finished s);
      \<delta> s w \<le> \<delta> s v\<rbrakk>
     \<Longrightarrow> (v, w) \<in> back_edges s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w \<in> E `` {v}; v \<in> dom (finished s); w \<in> dom (discovered s); w \<notin> dom (finished s); \<delta> s w \<le> \<delta> s v\<rbrakk> \<Longrightarrow> (v, w) \<in> back_edges s
[PROOF STEP]
using disc_imp_back_edge_or_pending finished_discovered finished_no_pending
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?w \<in> E `` {?v}; ?v \<in> dom (discovered s); ?w \<in> dom (discovered s); \<delta> s ?w \<le> \<delta> s ?v; ?w \<in> dom (finished s) \<Longrightarrow> ?v \<in> dom (finished s) \<and> \<phi> s ?v \<le> \<phi> s ?w\<rbrakk> \<Longrightarrow> (?v, ?w) \<in> back_edges s \<or> (?v, ?w) \<in> pending s
dom (finished s) \<subseteq> dom (discovered s)
?v \<in> dom (finished s) \<Longrightarrow> pending s `` {?v} = {}

goal (1 subgoal):
 1. \<lbrakk>w \<in> E `` {v}; v \<in> dom (finished s); w \<in> dom (discovered s); w \<notin> dom (finished s); \<delta> s w \<le> \<delta> s v\<rbrakk> \<Longrightarrow> (v, w) \<in> back_edges s
[PROOF STEP]
by fast


[STATEMENT]
lemma finished_self_loop_in_back_edges:
    assumes "v \<in> dom (finished s)"
    and "(v,v) \<in> E"
    shows "(v,v) \<in> back_edges s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v, v) \<in> back_edges s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
v \<in> dom (finished s)
(v, v) \<in> E

goal (1 subgoal):
 1. (v, v) \<in> back_edges s
[PROOF STEP]
using finished_imp_back_edge
[PROOF STATE]
proof (prove)
using this:
v \<in> dom (finished s)
(v, v) \<in> E
\<lbrakk>?w \<in> E `` {?v}; ?v \<in> dom (finished s); ?w \<in> dom (finished s); \<delta> s ?w \<le> \<delta> s ?v; \<phi> s ?v \<le> \<phi> s ?w\<rbrakk> \<Longrightarrow> (?v, ?w) \<in> back_edges s

goal (1 subgoal):
 1. (v, v) \<in> back_edges s
[PROOF STEP]
by blast


[STATEMENT]
lemma tree_cross_acyclic:
      "acyclic (tree_edges s \<union> cross_edges s)" (is "acyclic ?E")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. acyclic (tree_edges s \<union> cross_edges s)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> acyclic (tree_edges s \<union> cross_edges s) \<Longrightarrow> False
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> acyclic (tree_edges s \<union> cross_edges s) \<Longrightarrow> False
[PROOF STEP]
fix u v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> acyclic (tree_edges s \<union> cross_edges s) \<Longrightarrow> False
[PROOF STEP]
assume *: "u \<in> dom (finished s)" and "(u,v) \<in> ?E\<^sup>+"
[PROOF STATE]
proof (state)
this:
u \<in> dom (finished s)
(u, v) \<in> (tree_edges s \<union> cross_edges s)\<^sup>+

goal (1 subgoal):
 1. \<not> acyclic (tree_edges s \<union> cross_edges s) \<Longrightarrow> False
[PROOF STEP]
from this(2)
[PROOF STATE]
proof (chain)
picking this:
(u, v) \<in> (tree_edges s \<union> cross_edges s)\<^sup>+
[PROOF STEP]
have "\<phi> s v < \<phi> s u \<and> v \<in> dom (finished s)"
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> (tree_edges s \<union> cross_edges s)\<^sup>+

goal (1 subgoal):
 1. \<phi> s v < \<phi> s u \<and> v \<in> dom (finished s)
[PROOF STEP]
proof induct
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>y. (u, y) \<in> tree_edges s \<union> cross_edges s \<Longrightarrow> \<phi> s y < \<phi> s u \<and> y \<in> dom (finished s)
 2. \<And>y z. \<lbrakk>(u, y) \<in> (tree_edges s \<union> cross_edges s)\<^sup>+; (y, z) \<in> tree_edges s \<union> cross_edges s; \<phi> s y < \<phi> s u \<and> y \<in> dom (finished s)\<rbrakk> \<Longrightarrow> \<phi> s z < \<phi> s u \<and> z \<in> dom (finished s)
[PROOF STEP]
case base
[PROOF STATE]
proof (state)
this:
(u, y_) \<in> tree_edges s \<union> cross_edges s

goal (2 subgoals):
 1. \<And>y. (u, y) \<in> tree_edges s \<union> cross_edges s \<Longrightarrow> \<phi> s y < \<phi> s u \<and> y \<in> dom (finished s)
 2. \<And>y z. \<lbrakk>(u, y) \<in> (tree_edges s \<union> cross_edges s)\<^sup>+; (y, z) \<in> tree_edges s \<union> cross_edges s; \<phi> s y < \<phi> s u \<and> y \<in> dom (finished s)\<rbrakk> \<Longrightarrow> \<phi> s z < \<phi> s u \<and> z \<in> dom (finished s)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(u, y_) \<in> tree_edges s \<union> cross_edges s

goal (1 subgoal):
 1. \<phi> s y_ < \<phi> s u \<and> y_ \<in> dom (finished s)
[PROOF STEP]
by (metis Un_iff * cross_edges_finished_decr cross_edges_target_finished tree_edge_impl_parenthesis)
[PROOF STATE]
proof (state)
this:
\<phi> s y_ < \<phi> s u \<and> y_ \<in> dom (finished s)

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(u, y) \<in> (tree_edges s \<union> cross_edges s)\<^sup>+; (y, z) \<in> tree_edges s \<union> cross_edges s; \<phi> s y < \<phi> s u \<and> y \<in> dom (finished s)\<rbrakk> \<Longrightarrow> \<phi> s z < \<phi> s u \<and> z \<in> dom (finished s)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(u, y) \<in> (tree_edges s \<union> cross_edges s)\<^sup>+; (y, z) \<in> tree_edges s \<union> cross_edges s; \<phi> s y < \<phi> s u \<and> y \<in> dom (finished s)\<rbrakk> \<Longrightarrow> \<phi> s z < \<phi> s u \<and> z \<in> dom (finished s)
[PROOF STEP]
case (step v w)
[PROOF STATE]
proof (state)
this:
(u, v) \<in> (tree_edges s \<union> cross_edges s)\<^sup>+
(v, w) \<in> tree_edges s \<union> cross_edges s
\<phi> s v < \<phi> s u \<and> v \<in> dom (finished s)

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(u, y) \<in> (tree_edges s \<union> cross_edges s)\<^sup>+; (y, z) \<in> tree_edges s \<union> cross_edges s; \<phi> s y < \<phi> s u \<and> y \<in> dom (finished s)\<rbrakk> \<Longrightarrow> \<phi> s z < \<phi> s u \<and> z \<in> dom (finished s)
[PROOF STEP]
hence "\<phi> s w < \<phi> s v \<and> w \<in> dom (finished s)"
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> (tree_edges s \<union> cross_edges s)\<^sup>+
(v, w) \<in> tree_edges s \<union> cross_edges s
\<phi> s v < \<phi> s u \<and> v \<in> dom (finished s)

goal (1 subgoal):
 1. \<phi> s w < \<phi> s v \<and> w \<in> dom (finished s)
[PROOF STEP]
by (metis Un_iff cross_edges_finished_decr cross_edges_target_finished tree_edge_impl_parenthesis)
[PROOF STATE]
proof (state)
this:
\<phi> s w < \<phi> s v \<and> w \<in> dom (finished s)

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(u, y) \<in> (tree_edges s \<union> cross_edges s)\<^sup>+; (y, z) \<in> tree_edges s \<union> cross_edges s; \<phi> s y < \<phi> s u \<and> y \<in> dom (finished s)\<rbrakk> \<Longrightarrow> \<phi> s z < \<phi> s u \<and> z \<in> dom (finished s)
[PROOF STEP]
with step
[PROOF STATE]
proof (chain)
picking this:
(u, v) \<in> (tree_edges s \<union> cross_edges s)\<^sup>+
(v, w) \<in> tree_edges s \<union> cross_edges s
\<phi> s v < \<phi> s u \<and> v \<in> dom (finished s)
\<phi> s w < \<phi> s v \<and> w \<in> dom (finished s)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> (tree_edges s \<union> cross_edges s)\<^sup>+
(v, w) \<in> tree_edges s \<union> cross_edges s
\<phi> s v < \<phi> s u \<and> v \<in> dom (finished s)
\<phi> s w < \<phi> s v \<and> w \<in> dom (finished s)

goal (1 subgoal):
 1. \<phi> s w < \<phi> s u \<and> w \<in> dom (finished s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<phi> s w < \<phi> s u \<and> w \<in> dom (finished s)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<phi> s v < \<phi> s u \<and> v \<in> dom (finished s)

goal (1 subgoal):
 1. \<not> acyclic (tree_edges s \<union> cross_edges s) \<Longrightarrow> False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?u9 \<in> dom (finished s); (?u9, ?v9) \<in> (tree_edges s \<union> cross_edges s)\<^sup>+\<rbrakk> \<Longrightarrow> \<phi> s ?v9 < \<phi> s ?u9 \<and> ?v9 \<in> dom (finished s)

goal (1 subgoal):
 1. \<not> acyclic (tree_edges s \<union> cross_edges s) \<Longrightarrow> False
[PROOF STEP]
note aux = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?u9 \<in> dom (finished s); (?u9, ?v9) \<in> (tree_edges s \<union> cross_edges s)\<^sup>+\<rbrakk> \<Longrightarrow> \<phi> s ?v9 < \<phi> s ?u9 \<and> ?v9 \<in> dom (finished s)

goal (1 subgoal):
 1. \<not> acyclic (tree_edges s \<union> cross_edges s) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> acyclic ?E"
[PROOF STATE]
proof (state)
this:
\<not> acyclic (tree_edges s \<union> cross_edges s)

goal (1 subgoal):
 1. \<not> acyclic (tree_edges s \<union> cross_edges s) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> acyclic (tree_edges s \<union> cross_edges s)
[PROOF STEP]
obtain u where path: "(u,u) \<in> ?E\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
\<not> acyclic (tree_edges s \<union> cross_edges s)

goal (1 subgoal):
 1. (\<And>u. (u, u) \<in> (tree_edges s \<union> cross_edges s)\<^sup>+ \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: acyclic_def)
[PROOF STATE]
proof (state)
this:
(u, u) \<in> (tree_edges s \<union> cross_edges s)\<^sup>+

goal (1 subgoal):
 1. \<not> acyclic (tree_edges s \<union> cross_edges s) \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
assume "u \<in> dom (finished s)"
[PROOF STATE]
proof (state)
this:
u \<in> dom (finished s)

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
with aux path
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?u9 \<in> dom (finished s); (?u9, ?v9) \<in> (tree_edges s \<union> cross_edges s)\<^sup>+\<rbrakk> \<Longrightarrow> \<phi> s ?v9 < \<phi> s ?u9 \<and> ?v9 \<in> dom (finished s)
(u, u) \<in> (tree_edges s \<union> cross_edges s)\<^sup>+
u \<in> dom (finished s)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?u9 \<in> dom (finished s); (?u9, ?v9) \<in> (tree_edges s \<union> cross_edges s)\<^sup>+\<rbrakk> \<Longrightarrow> \<phi> s ?v9 < \<phi> s ?u9 \<and> ?v9 \<in> dom (finished s)
(u, u) \<in> (tree_edges s \<union> cross_edges s)\<^sup>+
u \<in> dom (finished s)

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

goal (1 subgoal):
 1. u \<notin> dom (finished s) \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u \<notin> dom (finished s) \<Longrightarrow> False
[PROOF STEP]
assume *: "u \<notin> dom (finished s)"
[PROOF STATE]
proof (state)
this:
u \<notin> dom (finished s)

goal (1 subgoal):
 1. u \<notin> dom (finished s) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
u \<notin> dom (finished s)

goal (1 subgoal):
 1. u \<notin> dom (finished s) \<Longrightarrow> False
[PROOF STEP]
from no_loop_in_tree
[PROOF STATE]
proof (chain)
picking this:
(?v, ?v) \<notin> (tree_edges s)\<^sup>+
[PROOF STEP]
have "(u,u) \<notin> (tree_edges s)\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
(?v, ?v) \<notin> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. (u, u) \<notin> (tree_edges s)\<^sup>+
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(u, u) \<notin> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. u \<notin> dom (finished s) \<Longrightarrow> False
[PROOF STEP]
with trancl_union_outside[OF path]
[PROOF STATE]
proof (chain)
picking this:
(u, u) \<notin> (tree_edges s)\<^sup>+ \<Longrightarrow> \<exists>x y. (u, x) \<in> (tree_edges s \<union> cross_edges s)\<^sup>* \<and> (x, y) \<in> cross_edges s \<and> (y, u) \<in> (tree_edges s \<union> cross_edges s)\<^sup>*
(u, u) \<notin> (tree_edges s)\<^sup>+
[PROOF STEP]
obtain x y where "(u,x) \<in> ?E\<^sup>*" "(x,y) \<in> cross_edges s" "(y,u) \<in> ?E\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
(u, u) \<notin> (tree_edges s)\<^sup>+ \<Longrightarrow> \<exists>x y. (u, x) \<in> (tree_edges s \<union> cross_edges s)\<^sup>* \<and> (x, y) \<in> cross_edges s \<and> (y, u) \<in> (tree_edges s \<union> cross_edges s)\<^sup>*
(u, u) \<notin> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>(u, x) \<in> (tree_edges s \<union> cross_edges s)\<^sup>*; (x, y) \<in> cross_edges s; (y, u) \<in> (tree_edges s \<union> cross_edges s)\<^sup>*\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(u, x) \<in> (tree_edges s \<union> cross_edges s)\<^sup>*
(x, y) \<in> cross_edges s
(y, u) \<in> (tree_edges s \<union> cross_edges s)\<^sup>*

goal (1 subgoal):
 1. u \<notin> dom (finished s) \<Longrightarrow> False
[PROOF STEP]
with cross_edges_target_finished
[PROOF STATE]
proof (chain)
picking this:
(?u, ?v) \<in> cross_edges s \<Longrightarrow> ?v \<in> dom (finished s)
(u, x) \<in> (tree_edges s \<union> cross_edges s)\<^sup>*
(x, y) \<in> cross_edges s
(y, u) \<in> (tree_edges s \<union> cross_edges s)\<^sup>*
[PROOF STEP]
have "y \<in> dom (finished s)"
[PROOF STATE]
proof (prove)
using this:
(?u, ?v) \<in> cross_edges s \<Longrightarrow> ?v \<in> dom (finished s)
(u, x) \<in> (tree_edges s \<union> cross_edges s)\<^sup>*
(x, y) \<in> cross_edges s
(y, u) \<in> (tree_edges s \<union> cross_edges s)\<^sup>*

goal (1 subgoal):
 1. y \<in> dom (finished s)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y \<in> dom (finished s)

goal (1 subgoal):
 1. u \<notin> dom (finished s) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
y \<in> dom (finished s)

goal (1 subgoal):
 1. u \<notin> dom (finished s) \<Longrightarrow> False
[PROOF STEP]
with * \<open>(y,u) \<in> ?E\<^sup>*\<close>
[PROOF STATE]
proof (chain)
picking this:
u \<notin> dom (finished s)
(y, u) \<in> (tree_edges s \<union> cross_edges s)\<^sup>*
y \<in> dom (finished s)
[PROOF STEP]
have "(y,u) \<in> ?E\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
u \<notin> dom (finished s)
(y, u) \<in> (tree_edges s \<union> cross_edges s)\<^sup>*
y \<in> dom (finished s)

goal (1 subgoal):
 1. (y, u) \<in> (tree_edges s \<union> cross_edges s)\<^sup>+
[PROOF STEP]
by (auto simp add: rtrancl_eq_or_trancl)
[PROOF STATE]
proof (state)
this:
(y, u) \<in> (tree_edges s \<union> cross_edges s)\<^sup>+

goal (1 subgoal):
 1. u \<notin> dom (finished s) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
u \<notin> dom (finished s)
y \<in> dom (finished s)
(y, u) \<in> (tree_edges s \<union> cross_edges s)\<^sup>+
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
u \<notin> dom (finished s)
y \<in> dom (finished s)
(y, u) \<in> (tree_edges s \<union> cross_edges s)\<^sup>+

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cycle_contains_back_edge:
    assumes cycle: "(u,u) \<in> (edges s)\<^sup>+"
    shows "\<exists>v w. (u,v) \<in> (edges s)\<^sup>* \<and> (v,w) \<in> back_edges s \<and> (w,u) \<in> (edges s)\<^sup>*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>v w. (u, v) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>* \<and> (v, w) \<in> back_edges s \<and> (w, u) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>*
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>v w. (u, v) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>* \<and> (v, w) \<in> back_edges s \<and> (w, u) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>*
[PROOF STEP]
from tree_cross_acyclic
[PROOF STATE]
proof (chain)
picking this:
acyclic (tree_edges s \<union> cross_edges s)
[PROOF STEP]
have "(u,u) \<notin> (tree_edges s \<union> cross_edges s)\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
acyclic (tree_edges s \<union> cross_edges s)

goal (1 subgoal):
 1. (u, u) \<notin> (tree_edges s \<union> cross_edges s)\<^sup>+
[PROOF STEP]
by (simp add: acyclic_def)
[PROOF STATE]
proof (state)
this:
(u, u) \<notin> (tree_edges s \<union> cross_edges s)\<^sup>+

goal (1 subgoal):
 1. \<exists>v w. (u, v) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>* \<and> (v, w) \<in> back_edges s \<and> (w, u) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>*
[PROOF STEP]
with trancl_union_outside[OF cycle]
[PROOF STATE]
proof (chain)
picking this:
(u, u) \<notin> (tree_edges s \<union> cross_edges s)\<^sup>+ \<Longrightarrow> \<exists>x y. (u, x) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>* \<and> (x, y) \<in> back_edges s \<and> (y, u) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>*
(u, u) \<notin> (tree_edges s \<union> cross_edges s)\<^sup>+
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(u, u) \<notin> (tree_edges s \<union> cross_edges s)\<^sup>+ \<Longrightarrow> \<exists>x y. (u, x) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>* \<and> (x, y) \<in> back_edges s \<and> (y, u) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>*
(u, u) \<notin> (tree_edges s \<union> cross_edges s)\<^sup>+

goal (1 subgoal):
 1. \<exists>v w. (u, v) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>* \<and> (v, w) \<in> back_edges s \<and> (w, u) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>*
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<exists>v w. (u, v) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>* \<and> (v, w) \<in> back_edges s \<and> (w, u) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>*

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cycle_needs_back_edge:
    assumes "back_edges s = {}"
    shows "acyclic (edges s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. acyclic (tree_edges s \<union> cross_edges s \<union> back_edges s)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> acyclic (tree_edges s \<union> cross_edges s \<union> back_edges s) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> acyclic (edges s)"
[PROOF STATE]
proof (state)
this:
\<not> acyclic (tree_edges s \<union> cross_edges s \<union> back_edges s)

goal (1 subgoal):
 1. \<not> acyclic (tree_edges s \<union> cross_edges s \<union> back_edges s) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> acyclic (tree_edges s \<union> cross_edges s \<union> back_edges s)
[PROOF STEP]
obtain u where "(u,u) \<in> (edges s)\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
\<not> acyclic (tree_edges s \<union> cross_edges s \<union> back_edges s)

goal (1 subgoal):
 1. (\<And>u. (u, u) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>+ \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: acyclic_def)
[PROOF STATE]
proof (state)
this:
(u, u) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>+

goal (1 subgoal):
 1. \<not> acyclic (tree_edges s \<union> cross_edges s \<union> back_edges s) \<Longrightarrow> False
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
back_edges s = {}
(u, u) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>+
[PROOF STEP]
have "(u,u) \<in> (tree_edges s \<union> cross_edges s)\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
back_edges s = {}
(u, u) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>+

goal (1 subgoal):
 1. (u, u) \<in> (tree_edges s \<union> cross_edges s)\<^sup>+
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(u, u) \<in> (tree_edges s \<union> cross_edges s)\<^sup>+

goal (1 subgoal):
 1. \<not> acyclic (tree_edges s \<union> cross_edges s \<union> back_edges s) \<Longrightarrow> False
[PROOF STEP]
with tree_cross_acyclic
[PROOF STATE]
proof (chain)
picking this:
acyclic (tree_edges s \<union> cross_edges s)
(u, u) \<in> (tree_edges s \<union> cross_edges s)\<^sup>+
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
acyclic (tree_edges s \<union> cross_edges s)
(u, u) \<in> (tree_edges s \<union> cross_edges s)\<^sup>+

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma back_edge_closes_cycle:
    assumes "back_edges s \<noteq> {}"
    shows "\<not> acyclic (edges s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> acyclic (tree_edges s \<union> cross_edges s \<union> back_edges s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> acyclic (tree_edges s \<union> cross_edges s \<union> back_edges s)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
back_edges s \<noteq> {}
[PROOF STEP]
obtain v w where be: "(v,w) \<in> back_edges s"
[PROOF STATE]
proof (prove)
using this:
back_edges s \<noteq> {}

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

goal (1 subgoal):
 1. \<not> acyclic (tree_edges s \<union> cross_edges s \<union> back_edges s)
[PROOF STEP]
hence "(w,w) \<in> (edges s)\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
(v, w) \<in> back_edges s

goal (1 subgoal):
 1. (w, w) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>+
[PROOF STEP]
proof (cases "v=w")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>(v, w) \<in> back_edges s; v = w\<rbrakk> \<Longrightarrow> (w, w) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>+
 2. \<lbrakk>(v, w) \<in> back_edges s; v \<noteq> w\<rbrakk> \<Longrightarrow> (w, w) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>+
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
v \<noteq> w

goal (2 subgoals):
 1. \<lbrakk>(v, w) \<in> back_edges s; v = w\<rbrakk> \<Longrightarrow> (w, w) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>+
 2. \<lbrakk>(v, w) \<in> back_edges s; v \<noteq> w\<rbrakk> \<Longrightarrow> (w, w) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>+
[PROOF STEP]
with be back_edge_impl_tree_path
[PROOF STATE]
proof (chain)
picking this:
(v, w) \<in> back_edges s
\<lbrakk>(?v, ?w) \<in> back_edges s; ?v \<noteq> ?w\<rbrakk> \<Longrightarrow> (?w, ?v) \<in> (tree_edges s)\<^sup>+
v \<noteq> w
[PROOF STEP]
have "(w,v) \<in> (tree_edges s)\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
(v, w) \<in> back_edges s
\<lbrakk>(?v, ?w) \<in> back_edges s; ?v \<noteq> ?w\<rbrakk> \<Longrightarrow> (?w, ?v) \<in> (tree_edges s)\<^sup>+
v \<noteq> w

goal (1 subgoal):
 1. (w, v) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(w, v) \<in> (tree_edges s)\<^sup>+

goal (2 subgoals):
 1. \<lbrakk>(v, w) \<in> back_edges s; v = w\<rbrakk> \<Longrightarrow> (w, w) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>+
 2. \<lbrakk>(v, w) \<in> back_edges s; v \<noteq> w\<rbrakk> \<Longrightarrow> (w, w) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>+
[PROOF STEP]
hence "(w,v) \<in> (edges s)\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
(w, v) \<in> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. (w, v) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>+
[PROOF STEP]
by (blast intro: trancl_mono_mp)
[PROOF STATE]
proof (state)
this:
(w, v) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>+

goal (2 subgoals):
 1. \<lbrakk>(v, w) \<in> back_edges s; v = w\<rbrakk> \<Longrightarrow> (w, w) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>+
 2. \<lbrakk>(v, w) \<in> back_edges s; v \<noteq> w\<rbrakk> \<Longrightarrow> (w, w) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>+
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(w, v) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>+

goal (2 subgoals):
 1. \<lbrakk>(v, w) \<in> back_edges s; v = w\<rbrakk> \<Longrightarrow> (w, w) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>+
 2. \<lbrakk>(v, w) \<in> back_edges s; v \<noteq> w\<rbrakk> \<Longrightarrow> (w, w) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>+
[PROOF STEP]
from be
[PROOF STATE]
proof (chain)
picking this:
(v, w) \<in> back_edges s
[PROOF STEP]
have "(v,w) \<in> edges s"
[PROOF STATE]
proof (prove)
using this:
(v, w) \<in> back_edges s

goal (1 subgoal):
 1. (v, w) \<in> tree_edges s \<union> cross_edges s \<union> back_edges s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(v, w) \<in> tree_edges s \<union> cross_edges s \<union> back_edges s

goal (2 subgoals):
 1. \<lbrakk>(v, w) \<in> back_edges s; v = w\<rbrakk> \<Longrightarrow> (w, w) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>+
 2. \<lbrakk>(v, w) \<in> back_edges s; v \<noteq> w\<rbrakk> \<Longrightarrow> (w, w) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>+
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(w, w) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>+
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(w, w) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>+

goal (1 subgoal):
 1. (w, w) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>+
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(w, w) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>+

goal (1 subgoal):
 1. \<lbrakk>(v, w) \<in> back_edges s; v = w\<rbrakk> \<Longrightarrow> (w, w) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>+
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
(w, w) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>+

goal (1 subgoal):
 1. \<not> acyclic (tree_edges s \<union> cross_edges s \<union> back_edges s)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(w, w) \<in> (tree_edges s \<union> cross_edges s \<union> back_edges s)\<^sup>+

goal (1 subgoal):
 1. \<not> acyclic (tree_edges s \<union> cross_edges s \<union> back_edges s)
[PROOF STEP]
by (auto simp add: acyclic_def)
[PROOF STATE]
proof (state)
this:
\<not> acyclic (tree_edges s \<union> cross_edges s \<union> back_edges s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma back_edge_closes_reachable_cycle:
    "back_edges s \<noteq> {} \<Longrightarrow> \<not> acyclic (E \<inter> reachable \<times> UNIV)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. back_edges s \<noteq> {} \<Longrightarrow> \<not> acyclic (E \<inter> reachable \<times> UNIV)
[PROOF STEP]
by (metis back_edge_closes_cycle edges_ss_reachable_edges cyclic_subset)


[STATEMENT]
lemma cycle_iff_back_edges:
    "acyclic (edges s) \<longleftrightarrow> back_edges s = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. acyclic (tree_edges s \<union> cross_edges s \<union> back_edges s) = (back_edges s = {})
[PROOF STEP]
by (metis back_edge_closes_cycle cycle_needs_back_edge)


[STATEMENT]
lemma white_path:
    "it_dfs \<le> SPEC(\<lambda>s. \<forall>x \<in> reachable. \<forall>y \<in> reachable. \<not> is_break param s \<longrightarrow>
            white_path s x y \<longleftrightarrow> (x,y) \<in> (tree_edges s)\<^sup>*)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it_dfs \<le> SPEC (\<lambda>s. \<forall>x\<in>reachable. \<forall>y\<in>reachable. \<not> is_break param s \<longrightarrow> white_path s x y = ((x, y) \<in> (tree_edges s)\<^sup>*))
[PROOF STEP]
proof (rule it_dfs_SPEC, intro ballI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s x y. \<lbrakk>DFS_invar G param s; \<not> cond s; x \<in> reachable; y \<in> reachable; \<not> is_break param s\<rbrakk> \<Longrightarrow> white_path s x y = ((x, y) \<in> (tree_edges s)\<^sup>*)
[PROOF STEP]
fix s x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s x y. \<lbrakk>DFS_invar G param s; \<not> cond s; x \<in> reachable; y \<in> reachable; \<not> is_break param s\<rbrakk> \<Longrightarrow> white_path s x y = ((x, y) \<in> (tree_edges s)\<^sup>*)
[PROOF STEP]
assume DI: "DFS_invar G param s"
      and C: "\<not> cond s" "\<not> is_break param s"
      and reach: "x \<in> reachable" "y \<in> reachable"
[PROOF STATE]
proof (state)
this:
DFS_invar G param s
\<not> cond s
\<not> is_break param s
x \<in> reachable
y \<in> reachable

goal (1 subgoal):
 1. \<And>s x y. \<lbrakk>DFS_invar G param s; \<not> cond s; x \<in> reachable; y \<in> reachable; \<not> is_break param s\<rbrakk> \<Longrightarrow> white_path s x y = ((x, y) \<in> (tree_edges s)\<^sup>*)
[PROOF STEP]
from DI
[PROOF STATE]
proof (chain)
picking this:
DFS_invar G param s
[PROOF STEP]
interpret DFS_invar where s=s
[PROOF STATE]
proof (prove)
using this:
DFS_invar G param s

goal (1 subgoal):
 1. DFS_invar G param s
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s x y. \<lbrakk>DFS_invar G param s; \<not> cond s; x \<in> reachable; y \<in> reachable; \<not> is_break param s\<rbrakk> \<Longrightarrow> white_path s x y = ((x, y) \<in> (tree_edges s)\<^sup>*)
[PROOF STEP]
note fin_eq_reach = nc_finished_eq_reachable[OF C]
[PROOF STATE]
proof (state)
this:
dom (finished s) = reachable

goal (1 subgoal):
 1. \<And>s x y. \<lbrakk>DFS_invar G param s; \<not> cond s; x \<in> reachable; y \<in> reachable; \<not> is_break param s\<rbrakk> \<Longrightarrow> white_path s x y = ((x, y) \<in> (tree_edges s)\<^sup>*)
[PROOF STEP]
show "white_path s x y \<longleftrightarrow> (x,y) \<in> (tree_edges s)\<^sup>*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. white_path s x y = ((x, y) \<in> (tree_edges s)\<^sup>*)
[PROOF STEP]
proof (cases "x=y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = y \<Longrightarrow> white_path s x y = ((x, y) \<in> (tree_edges s)\<^sup>*)
 2. x \<noteq> y \<Longrightarrow> white_path s x y = ((x, y) \<in> (tree_edges s)\<^sup>*)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = y

goal (2 subgoals):
 1. x = y \<Longrightarrow> white_path s x y = ((x, y) \<in> (tree_edges s)\<^sup>*)
 2. x \<noteq> y \<Longrightarrow> white_path s x y = ((x, y) \<in> (tree_edges s)\<^sup>*)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x = y

goal (1 subgoal):
 1. white_path s x y = ((x, y) \<in> (tree_edges s)\<^sup>*)
[PROOF STEP]
by (simp add: white_path_def)
[PROOF STATE]
proof (state)
this:
white_path s x y = ((x, y) \<in> (tree_edges s)\<^sup>*)

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> white_path s x y = ((x, y) \<in> (tree_edges s)\<^sup>*)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> white_path s x y = ((x, y) \<in> (tree_edges s)\<^sup>*)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> y

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> white_path s x y = ((x, y) \<in> (tree_edges s)\<^sup>*)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. white_path s x y = ((x, y) \<in> (tree_edges s)\<^sup>*)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. white_path s x y \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
 2. (x, y) \<in> (tree_edges s)\<^sup>* \<Longrightarrow> white_path s x y
[PROOF STEP]
assume "(x,y) \<in> (tree_edges s)\<^sup>*"
[PROOF STATE]
proof (state)
this:
(x, y) \<in> (tree_edges s)\<^sup>*

goal (2 subgoals):
 1. white_path s x y \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
 2. (x, y) \<in> (tree_edges s)\<^sup>* \<Longrightarrow> white_path s x y
[PROOF STEP]
with \<open>x\<noteq>y\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> y
(x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
have T: "(x,y) \<in> (tree_edges s)\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
(x, y) \<in> (tree_edges s)\<^sup>*

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
by (metis rtranclD)
[PROOF STATE]
proof (state)
this:
(x, y) \<in> (tree_edges s)\<^sup>+

goal (2 subgoals):
 1. white_path s x y \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
 2. (x, y) \<in> (tree_edges s)\<^sup>* \<Longrightarrow> white_path s x y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
obtain p where P: "path (tree_edges s) x p y"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. (\<And>p. path (tree_edges s) x p y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis trancl_is_path)
[PROOF STATE]
proof (state)
this:
path (tree_edges s) x p y

goal (2 subgoals):
 1. white_path s x y \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
 2. (x, y) \<in> (tree_edges s)\<^sup>* \<Longrightarrow> white_path s x y
[PROOF STEP]
with tree_edges_ssE
[PROOF STATE]
proof (chain)
picking this:
tree_edges s \<subseteq> E
path (tree_edges s) x p y
[PROOF STEP]
have "path E x p y"
[PROOF STATE]
proof (prove)
using this:
tree_edges s \<subseteq> E
path (tree_edges s) x p y

goal (1 subgoal):
 1. path E x p y
[PROOF STEP]
using path_mono[where E="tree_edges s"]
[PROOF STATE]
proof (prove)
using this:
tree_edges s \<subseteq> E
path (tree_edges s) x p y
\<lbrakk>tree_edges s \<subseteq> ?E'; path (tree_edges s) ?u ?p ?v\<rbrakk> \<Longrightarrow> path ?E' ?u ?p ?v

goal (1 subgoal):
 1. path E x p y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
path E x p y

goal (2 subgoals):
 1. white_path s x y \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
 2. (x, y) \<in> (tree_edges s)\<^sup>* \<Longrightarrow> white_path s x y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
path E x p y

goal (2 subgoals):
 1. white_path s x y \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
 2. (x, y) \<in> (tree_edges s)\<^sup>* \<Longrightarrow> white_path s x y
[PROOF STEP]
from P
[PROOF STATE]
proof (chain)
picking this:
path (tree_edges s) x p y
[PROOF STEP]
have "\<delta> s x < \<delta> s y \<and> (\<forall> v \<in> set (tl p). \<delta> s x < \<delta> s v)"
[PROOF STATE]
proof (prove)
using this:
path (tree_edges s) x p y

goal (1 subgoal):
 1. \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl p). \<delta> s x < \<delta> s v)
[PROOF STEP]
using \<open>x\<noteq>y\<close>
[PROOF STATE]
proof (prove)
using this:
path (tree_edges s) x p y
x \<noteq> y

goal (1 subgoal):
 1. \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl p). \<delta> s x < \<delta> s v)
[PROOF STEP]
proof (induct rule: path_tl_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>u. (x, u) \<in> tree_edges s \<Longrightarrow> \<delta> s x < \<delta> s u
 2. \<And>u v. \<lbrakk>(x, u) \<in> (tree_edges s)\<^sup>+; (u, v) \<in> tree_edges s; \<delta> s x < \<delta> s u\<rbrakk> \<Longrightarrow> \<delta> s x < \<delta> s v
[PROOF STEP]
case (single u)
[PROOF STATE]
proof (state)
this:
(x, u) \<in> tree_edges s

goal (2 subgoals):
 1. \<And>u. (x, u) \<in> tree_edges s \<Longrightarrow> \<delta> s x < \<delta> s u
 2. \<And>u v. \<lbrakk>(x, u) \<in> (tree_edges s)\<^sup>+; (u, v) \<in> tree_edges s; \<delta> s x < \<delta> s u\<rbrakk> \<Longrightarrow> \<delta> s x < \<delta> s v
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(x, u) \<in> tree_edges s

goal (1 subgoal):
 1. \<delta> s x < \<delta> s u
[PROOF STEP]
by (fact tree_edge_disc)
[PROOF STATE]
proof (state)
this:
\<delta> s x < \<delta> s u

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>(x, u) \<in> (tree_edges s)\<^sup>+; (u, v) \<in> tree_edges s; \<delta> s x < \<delta> s u\<rbrakk> \<Longrightarrow> \<delta> s x < \<delta> s v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u v. \<lbrakk>(x, u) \<in> (tree_edges s)\<^sup>+; (u, v) \<in> tree_edges s; \<delta> s x < \<delta> s u\<rbrakk> \<Longrightarrow> \<delta> s x < \<delta> s v
[PROOF STEP]
case (step u v)
[PROOF STATE]
proof (state)
this:
(x, u) \<in> (tree_edges s)\<^sup>+
(u, v) \<in> tree_edges s
\<delta> s x < \<delta> s u

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>(x, u) \<in> (tree_edges s)\<^sup>+; (u, v) \<in> tree_edges s; \<delta> s x < \<delta> s u\<rbrakk> \<Longrightarrow> \<delta> s x < \<delta> s v
[PROOF STEP]
note \<open>\<delta> s x < \<delta> s u\<close>
[PROOF STATE]
proof (state)
this:
\<delta> s x < \<delta> s u

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>(x, u) \<in> (tree_edges s)\<^sup>+; (u, v) \<in> tree_edges s; \<delta> s x < \<delta> s u\<rbrakk> \<Longrightarrow> \<delta> s x < \<delta> s v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<delta> s x < \<delta> s u

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>(x, u) \<in> (tree_edges s)\<^sup>+; (u, v) \<in> tree_edges s; \<delta> s x < \<delta> s u\<rbrakk> \<Longrightarrow> \<delta> s x < \<delta> s v
[PROOF STEP]
from step
[PROOF STATE]
proof (chain)
picking this:
(x, u) \<in> (tree_edges s)\<^sup>+
(u, v) \<in> tree_edges s
\<delta> s x < \<delta> s u
[PROOF STEP]
have "\<delta> s u < \<delta> s v"
[PROOF STATE]
proof (prove)
using this:
(x, u) \<in> (tree_edges s)\<^sup>+
(u, v) \<in> tree_edges s
\<delta> s x < \<delta> s u

goal (1 subgoal):
 1. \<delta> s u < \<delta> s v
[PROOF STEP]
by (metis tree_edge_disc)
[PROOF STATE]
proof (state)
this:
\<delta> s u < \<delta> s v

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>(x, u) \<in> (tree_edges s)\<^sup>+; (u, v) \<in> tree_edges s; \<delta> s x < \<delta> s u\<rbrakk> \<Longrightarrow> \<delta> s x < \<delta> s v
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<delta> s x < \<delta> s v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<delta> s x < \<delta> s v

goal (1 subgoal):
 1. \<delta> s x < \<delta> s v
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<delta> s x < \<delta> s v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl p). \<delta> s x < \<delta> s v)

goal (2 subgoals):
 1. white_path s x y \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
 2. (x, y) \<in> (tree_edges s)\<^sup>* \<Longrightarrow> white_path s x y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
path E x p y
\<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl p). \<delta> s x < \<delta> s v)
[PROOF STEP]
show "white_path s x y"
[PROOF STATE]
proof (prove)
using this:
path E x p y
\<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl p). \<delta> s x < \<delta> s v)

goal (1 subgoal):
 1. white_path s x y
[PROOF STEP]
by (auto simp add: \<open>x\<noteq>y\<close> white_path_def)
[PROOF STATE]
proof (state)
this:
white_path s x y

goal (1 subgoal):
 1. white_path s x y \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. white_path s x y \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
assume "white_path s x y"
[PROOF STATE]
proof (state)
this:
white_path s x y

goal (1 subgoal):
 1. white_path s x y \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
with \<open>x\<noteq>y\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> y
white_path s x y
[PROOF STEP]
obtain p where
            P:"path E x p y" and
            white: "\<delta> s x < \<delta> s y \<and> (\<forall> v \<in> set (tl p). \<delta> s x < \<delta> s v)"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
white_path s x y

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>path E x p y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl p). \<delta> s x < \<delta> s v)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding white_path_def
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
x \<noteq> y \<longrightarrow> (\<exists>p. path E x p y \<and> \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl p). \<delta> s x < \<delta> s v))

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>path E x p y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl p). \<delta> s x < \<delta> s v)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
path E x p y
\<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl p). \<delta> s x < \<delta> s v)

goal (1 subgoal):
 1. white_path s x y \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
hence "p \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
path E x p y
\<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl p). \<delta> s x < \<delta> s v)

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

goal (1 subgoal):
 1. white_path s x y \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
thus "(x,y) \<in> (tree_edges s)\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> []

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
using P white reach(2)
[PROOF STATE]
proof (prove)
using this:
p \<noteq> []
path E x p y
\<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl p). \<delta> s x < \<delta> s v)
y \<in> reachable

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
proof (induction p arbitrary: y rule: rev_nonempty_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xa y. \<lbrakk>path E x [xa] y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl [xa]). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
 2. \<And>xa xs y. \<lbrakk>xs \<noteq> []; \<And>y. \<lbrakk>path E x xs y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl xs). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*; path E x (xs @ [xa]) y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl (xs @ [xa])). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
case single
[PROOF STATE]
proof (state)
this:
path E x [x_] y
\<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl [x_]). \<delta> s x < \<delta> s v)
y \<in> reachable

goal (2 subgoals):
 1. \<And>xa y. \<lbrakk>path E x [xa] y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl [xa]). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
 2. \<And>xa xs y. \<lbrakk>xs \<noteq> []; \<And>y. \<lbrakk>path E x xs y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl xs). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*; path E x (xs @ [xa]) y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl (xs @ [xa])). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
hence "y \<in> succ x"
[PROOF STATE]
proof (prove)
using this:
path E x [x_] y
\<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl [x_]). \<delta> s x < \<delta> s v)
y \<in> reachable

goal (1 subgoal):
 1. y \<in> E `` {x}
[PROOF STEP]
by (simp add: path_cons_conv)
[PROOF STATE]
proof (state)
this:
y \<in> E `` {x}

goal (2 subgoals):
 1. \<And>xa y. \<lbrakk>path E x [xa] y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl [xa]). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
 2. \<And>xa xs y. \<lbrakk>xs \<noteq> []; \<And>y. \<lbrakk>path E x xs y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl xs). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*; path E x (xs @ [xa]) y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl (xs @ [xa])). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
with reach single
[PROOF STATE]
proof (chain)
picking this:
x \<in> reachable
y__ \<in> reachable
path E x [x_] y
\<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl [x_]). \<delta> s x < \<delta> s v)
y \<in> reachable
y \<in> E `` {x}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<in> reachable
y__ \<in> reachable
path E x [x_] y
\<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl [x_]). \<delta> s x < \<delta> s v)
y \<in> reachable
y \<in> E `` {x}

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
using fin_eq_reach finished_succ_impl_path_in_tree[of x y]
[PROOF STATE]
proof (prove)
using this:
x \<in> reachable
y__ \<in> reachable
path E x [x_] y
\<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl [x_]). \<delta> s x < \<delta> s v)
y \<in> reachable
y \<in> E `` {x}
dom (finished s) = reachable
\<lbrakk>x \<in> dom (finished s); y \<in> E `` {x}; \<delta> s x < \<delta> s y\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x, y) \<in> (tree_edges s)\<^sup>*

goal (1 subgoal):
 1. \<And>xa xs y. \<lbrakk>xs \<noteq> []; \<And>y. \<lbrakk>path E x xs y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl xs). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*; path E x (xs @ [xa]) y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl (xs @ [xa])). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa xs y. \<lbrakk>xs \<noteq> []; \<And>y. \<lbrakk>path E x xs y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl xs). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*; path E x (xs @ [xa]) y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl (xs @ [xa])). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
case (snoc u us)
[PROOF STATE]
proof (state)
this:
us \<noteq> []
\<lbrakk>path E x us ?y8; \<delta> s x < \<delta> s ?y8 \<and> (\<forall>v\<in>set (tl us). \<delta> s x < \<delta> s v); ?y8 \<in> reachable\<rbrakk> \<Longrightarrow> (x, ?y8) \<in> (tree_edges s)\<^sup>*
path E x (us @ [u]) y
\<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl (us @ [u])). \<delta> s x < \<delta> s v)
y \<in> reachable

goal (1 subgoal):
 1. \<And>xa xs y. \<lbrakk>xs \<noteq> []; \<And>y. \<lbrakk>path E x xs y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl xs). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*; path E x (xs @ [xa]) y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl (xs @ [xa])). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
hence "path E x us u"
[PROOF STATE]
proof (prove)
using this:
us \<noteq> []
\<lbrakk>path E x us ?y8; \<delta> s x < \<delta> s ?y8 \<and> (\<forall>v\<in>set (tl us). \<delta> s x < \<delta> s v); ?y8 \<in> reachable\<rbrakk> \<Longrightarrow> (x, ?y8) \<in> (tree_edges s)\<^sup>*
path E x (us @ [u]) y
\<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl (us @ [u])). \<delta> s x < \<delta> s v)
y \<in> reachable

goal (1 subgoal):
 1. path E x us u
[PROOF STEP]
by (simp add: path_append_conv)
[PROOF STATE]
proof (state)
this:
path E x us u

goal (1 subgoal):
 1. \<And>xa xs y. \<lbrakk>xs \<noteq> []; \<And>y. \<lbrakk>path E x xs y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl xs). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*; path E x (xs @ [xa]) y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl (xs @ [xa])). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
path E x us u

goal (1 subgoal):
 1. \<And>xa xs y. \<lbrakk>xs \<noteq> []; \<And>y. \<lbrakk>path E x xs y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl xs). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*; path E x (xs @ [xa]) y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl (xs @ [xa])). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
hence "(x,u) \<in> E\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
path E x us u

goal (1 subgoal):
 1. (x, u) \<in> E\<^sup>*
[PROOF STEP]
by (simp add: path_is_rtrancl)
[PROOF STATE]
proof (state)
this:
(x, u) \<in> E\<^sup>*

goal (1 subgoal):
 1. \<And>xa xs y. \<lbrakk>xs \<noteq> []; \<And>y. \<lbrakk>path E x xs y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl xs). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*; path E x (xs @ [xa]) y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl (xs @ [xa])). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
with reach
[PROOF STATE]
proof (chain)
picking this:
x \<in> reachable
y__ \<in> reachable
(x, u) \<in> E\<^sup>*
[PROOF STEP]
have ureach: "u \<in> reachable"
[PROOF STATE]
proof (prove)
using this:
x \<in> reachable
y__ \<in> reachable
(x, u) \<in> E\<^sup>*

goal (1 subgoal):
 1. u \<in> reachable
[PROOF STEP]
by (metis rtrancl_image_advance_rtrancl)
[PROOF STATE]
proof (state)
this:
u \<in> reachable

goal (1 subgoal):
 1. \<And>xa xs y. \<lbrakk>xs \<noteq> []; \<And>y. \<lbrakk>path E x xs y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl xs). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*; path E x (xs @ [xa]) y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl (xs @ [xa])). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
u \<in> reachable

goal (1 subgoal):
 1. \<And>xa xs y. \<lbrakk>xs \<noteq> []; \<And>y. \<lbrakk>path E x xs y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl xs). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*; path E x (xs @ [xa]) y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl (xs @ [xa])). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
from snoc
[PROOF STATE]
proof (chain)
picking this:
us \<noteq> []
\<lbrakk>path E x us ?y8; \<delta> s x < \<delta> s ?y8 \<and> (\<forall>v\<in>set (tl us). \<delta> s x < \<delta> s v); ?y8 \<in> reachable\<rbrakk> \<Longrightarrow> (x, ?y8) \<in> (tree_edges s)\<^sup>*
path E x (us @ [u]) y
\<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl (us @ [u])). \<delta> s x < \<delta> s v)
y \<in> reachable
[PROOF STEP]
have "\<delta> s x < \<delta> s u" "(\<forall>v\<in>set (tl us). \<delta> s x < \<delta> s v)"
[PROOF STATE]
proof (prove)
using this:
us \<noteq> []
\<lbrakk>path E x us ?y8; \<delta> s x < \<delta> s ?y8 \<and> (\<forall>v\<in>set (tl us). \<delta> s x < \<delta> s v); ?y8 \<in> reachable\<rbrakk> \<Longrightarrow> (x, ?y8) \<in> (tree_edges s)\<^sup>*
path E x (us @ [u]) y
\<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl (us @ [u])). \<delta> s x < \<delta> s v)
y \<in> reachable

goal (1 subgoal):
 1. \<delta> s x < \<delta> s u &&& \<forall>v\<in>set (tl us). \<delta> s x < \<delta> s v
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
\<delta> s x < \<delta> s u
\<forall>v\<in>set (tl us). \<delta> s x < \<delta> s v

goal (1 subgoal):
 1. \<And>xa xs y. \<lbrakk>xs \<noteq> []; \<And>y. \<lbrakk>path E x xs y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl xs). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*; path E x (xs @ [xa]) y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl (xs @ [xa])). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
path E x us u
u \<in> reachable
\<delta> s x < \<delta> s u
\<forall>v\<in>set (tl us). \<delta> s x < \<delta> s v
[PROOF STEP]
have x_u: "(x,u) \<in> (tree_edges s)\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
path E x us u
u \<in> reachable
\<delta> s x < \<delta> s u
\<forall>v\<in>set (tl us). \<delta> s x < \<delta> s v

goal (1 subgoal):
 1. (x, u) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
by (metis snoc.IH)
[PROOF STATE]
proof (state)
this:
(x, u) \<in> (tree_edges s)\<^sup>*

goal (1 subgoal):
 1. \<And>xa xs y. \<lbrakk>xs \<noteq> []; \<And>y. \<lbrakk>path E x xs y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl xs). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*; path E x (xs @ [xa]) y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl (xs @ [xa])). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
from snoc
[PROOF STATE]
proof (chain)
picking this:
us \<noteq> []
\<lbrakk>path E x us ?y8; \<delta> s x < \<delta> s ?y8 \<and> (\<forall>v\<in>set (tl us). \<delta> s x < \<delta> s v); ?y8 \<in> reachable\<rbrakk> \<Longrightarrow> (x, ?y8) \<in> (tree_edges s)\<^sup>*
path E x (us @ [u]) y
\<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl (us @ [u])). \<delta> s x < \<delta> s v)
y \<in> reachable
[PROOF STEP]
have "y \<in> succ u"
[PROOF STATE]
proof (prove)
using this:
us \<noteq> []
\<lbrakk>path E x us ?y8; \<delta> s x < \<delta> s ?y8 \<and> (\<forall>v\<in>set (tl us). \<delta> s x < \<delta> s v); ?y8 \<in> reachable\<rbrakk> \<Longrightarrow> (x, ?y8) \<in> (tree_edges s)\<^sup>*
path E x (us @ [u]) y
\<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl (us @ [u])). \<delta> s x < \<delta> s v)
y \<in> reachable

goal (1 subgoal):
 1. y \<in> E `` {u}
[PROOF STEP]
by (simp add: path_append_conv)
[PROOF STATE]
proof (state)
this:
y \<in> E `` {u}

goal (1 subgoal):
 1. \<And>xa xs y. \<lbrakk>xs \<noteq> []; \<And>y. \<lbrakk>path E x xs y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl xs). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*; path E x (xs @ [xa]) y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl (xs @ [xa])). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
from snoc(5) fin_eq_reach finished_discovered
[PROOF STATE]
proof (chain)
picking this:
y \<in> reachable
dom (finished s) = reachable
dom (finished s) \<subseteq> dom (discovered s)
[PROOF STEP]
have
            y_f_d: "y \<in> dom (finished s)" "y \<in> dom (discovered s)"
[PROOF STATE]
proof (prove)
using this:
y \<in> reachable
dom (finished s) = reachable
dom (finished s) \<subseteq> dom (discovered s)

goal (1 subgoal):
 1. y \<in> dom (finished s) &&& y \<in> dom (discovered s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> dom (finished s)
y \<in> dom (discovered s)

goal (1 subgoal):
 1. \<And>xa xs y. \<lbrakk>xs \<noteq> []; \<And>y. \<lbrakk>path E x xs y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl xs). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*; path E x (xs @ [xa]) y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl (xs @ [xa])). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
from \<open>y \<in> succ u\<close> ureach fin_eq_reach
[PROOF STATE]
proof (chain)
picking this:
y \<in> E `` {u}
u \<in> reachable
dom (finished s) = reachable
[PROOF STEP]
have "\<delta> s y < \<phi> s u"
[PROOF STATE]
proof (prove)
using this:
y \<in> E `` {u}
u \<in> reachable
dom (finished s) = reachable

goal (1 subgoal):
 1. \<delta> s y < \<phi> s u
[PROOF STEP]
using finished_succ_fin
[PROOF STATE]
proof (prove)
using this:
y \<in> E `` {u}
u \<in> reachable
dom (finished s) = reachable
\<lbrakk>?v \<in> dom (finished s); ?w \<in> E `` {?v}\<rbrakk> \<Longrightarrow> \<delta> s ?w < \<phi> s ?v

goal (1 subgoal):
 1. \<delta> s y < \<phi> s u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<delta> s y < \<phi> s u

goal (1 subgoal):
 1. \<And>xa xs y. \<lbrakk>xs \<noteq> []; \<And>y. \<lbrakk>path E x xs y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl xs). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*; path E x (xs @ [xa]) y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl (xs @ [xa])). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<delta> s y < \<phi> s u

goal (1 subgoal):
 1. \<And>xa xs y. \<lbrakk>xs \<noteq> []; \<And>y. \<lbrakk>path E x xs y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl xs). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*; path E x (xs @ [xa]) y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl (xs @ [xa])). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
from \<open>\<delta> s x < \<delta> s u\<close>
[PROOF STATE]
proof (chain)
picking this:
\<delta> s x < \<delta> s u
[PROOF STEP]
have "x \<noteq> u"
[PROOF STATE]
proof (prove)
using this:
\<delta> s x < \<delta> s u

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

goal (1 subgoal):
 1. \<And>xa xs y. \<lbrakk>xs \<noteq> []; \<And>y. \<lbrakk>path E x xs y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl xs). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*; path E x (xs @ [xa]) y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl (xs @ [xa])). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
with x_u
[PROOF STATE]
proof (chain)
picking this:
(x, u) \<in> (tree_edges s)\<^sup>*
x \<noteq> u
[PROOF STEP]
have "(x,u) \<in> (tree_edges s)\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
(x, u) \<in> (tree_edges s)\<^sup>*
x \<noteq> u

goal (1 subgoal):
 1. (x, u) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
by (metis rtrancl_eq_or_trancl)
[PROOF STATE]
proof (state)
this:
(x, u) \<in> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. \<And>xa xs y. \<lbrakk>xs \<noteq> []; \<And>y. \<lbrakk>path E x xs y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl xs). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*; path E x (xs @ [xa]) y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl (xs @ [xa])). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
with fin_eq_reach reach
[PROOF STATE]
proof (chain)
picking this:
dom (finished s) = reachable
x \<in> reachable
y__ \<in> reachable
(x, u) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
have "\<phi> s u < \<phi> s x"
[PROOF STATE]
proof (prove)
using this:
dom (finished s) = reachable
x \<in> reachable
y__ \<in> reachable
(x, u) \<in> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. \<phi> s u < \<phi> s x
[PROOF STEP]
using tree_path_impl_parenthesis
[PROOF STATE]
proof (prove)
using this:
dom (finished s) = reachable
x \<in> reachable
y__ \<in> reachable
(x, u) \<in> (tree_edges s)\<^sup>+
\<lbrakk>(?v, ?w) \<in> (tree_edges s)\<^sup>+; ?v \<in> dom (finished s)\<rbrakk> \<Longrightarrow> ?w \<in> dom (finished s) \<and> \<delta> s ?v < \<delta> s ?w \<and> \<phi> s ?w < \<phi> s ?v

goal (1 subgoal):
 1. \<phi> s u < \<phi> s x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<phi> s u < \<phi> s x

goal (1 subgoal):
 1. \<And>xa xs y. \<lbrakk>xs \<noteq> []; \<And>y. \<lbrakk>path E x xs y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl xs). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*; path E x (xs @ [xa]) y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl (xs @ [xa])). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<delta> s y < \<phi> s x
[PROOF STEP]
have "\<phi> s y < \<phi> s x"
[PROOF STATE]
proof (prove)
using this:
\<delta> s y < \<phi> s x

goal (1 subgoal):
 1. \<phi> s y < \<phi> s x
[PROOF STEP]
using reach fin_eq_reach y_f_d snoc
[PROOF STATE]
proof (prove)
using this:
\<delta> s y < \<phi> s x
x \<in> reachable
y__ \<in> reachable
dom (finished s) = reachable
y \<in> dom (finished s)
y \<in> dom (discovered s)
us \<noteq> []
\<lbrakk>path E x us ?y8; \<delta> s x < \<delta> s ?y8 \<and> (\<forall>v\<in>set (tl us). \<delta> s x < \<delta> s v); ?y8 \<in> reachable\<rbrakk> \<Longrightarrow> (x, ?y8) \<in> (tree_edges s)\<^sup>*
path E x (us @ [u]) y
\<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl (us @ [u])). \<delta> s x < \<delta> s v)
y \<in> reachable

goal (1 subgoal):
 1. \<phi> s y < \<phi> s x
[PROOF STEP]
using parenthesis_contained
[PROOF STATE]
proof (prove)
using this:
\<delta> s y < \<phi> s x
x \<in> reachable
y__ \<in> reachable
dom (finished s) = reachable
y \<in> dom (finished s)
y \<in> dom (discovered s)
us \<noteq> []
\<lbrakk>path E x us ?y8; \<delta> s x < \<delta> s ?y8 \<and> (\<forall>v\<in>set (tl us). \<delta> s x < \<delta> s v); ?y8 \<in> reachable\<rbrakk> \<Longrightarrow> (x, ?y8) \<in> (tree_edges s)\<^sup>*
path E x (us @ [u]) y
\<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl (us @ [u])). \<delta> s x < \<delta> s v)
y \<in> reachable
\<lbrakk>?v \<in> dom (finished s); ?w \<in> dom (discovered s); \<delta> s ?v < \<delta> s ?w; \<delta> s ?w < \<phi> s ?v\<rbrakk> \<Longrightarrow> ?w \<in> dom (finished s) \<and> \<phi> s ?w < \<phi> s ?v

goal (1 subgoal):
 1. \<phi> s y < \<phi> s x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<phi> s y < \<phi> s x

goal (1 subgoal):
 1. \<And>xa xs y. \<lbrakk>xs \<noteq> []; \<And>y. \<lbrakk>path E x xs y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl xs). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*; path E x (xs @ [xa]) y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl (xs @ [xa])). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
hence "(x,y) \<in> (tree_edges s)\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
\<phi> s y < \<phi> s x

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
using reach fin_eq_reach y_f_d snoc
[PROOF STATE]
proof (prove)
using this:
\<phi> s y < \<phi> s x
x \<in> reachable
y__ \<in> reachable
dom (finished s) = reachable
y \<in> dom (finished s)
y \<in> dom (discovered s)
us \<noteq> []
\<lbrakk>path E x us ?y8; \<delta> s x < \<delta> s ?y8 \<and> (\<forall>v\<in>set (tl us). \<delta> s x < \<delta> s v); ?y8 \<in> reachable\<rbrakk> \<Longrightarrow> (x, ?y8) \<in> (tree_edges s)\<^sup>*
path E x (us @ [u]) y
\<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl (us @ [u])). \<delta> s x < \<delta> s v)
y \<in> reachable

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
using parenthesis_impl_tree_path
[PROOF STATE]
proof (prove)
using this:
\<phi> s y < \<phi> s x
x \<in> reachable
y__ \<in> reachable
dom (finished s) = reachable
y \<in> dom (finished s)
y \<in> dom (discovered s)
us \<noteq> []
\<lbrakk>path E x us ?y8; \<delta> s x < \<delta> s ?y8 \<and> (\<forall>v\<in>set (tl us). \<delta> s x < \<delta> s v); ?y8 \<in> reachable\<rbrakk> \<Longrightarrow> (x, ?y8) \<in> (tree_edges s)\<^sup>*
path E x (us @ [u]) y
\<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl (us @ [u])). \<delta> s x < \<delta> s v)
y \<in> reachable
\<lbrakk>?v \<in> dom (finished s); ?w \<in> dom (finished s); \<delta> s ?v < \<delta> s ?w; \<phi> s ?w < \<phi> s ?v\<rbrakk> \<Longrightarrow> (?v, ?w) \<in> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(x, y) \<in> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. \<And>xa xs y. \<lbrakk>xs \<noteq> []; \<And>y. \<lbrakk>path E x xs y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl xs). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*; path E x (xs @ [xa]) y; \<delta> s x < \<delta> s y \<and> (\<forall>v\<in>set (tl (xs @ [xa])). \<delta> s x < \<delta> s v); y \<in> reachable\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, y) \<in> (tree_edges s)\<^sup>*

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x, y) \<in> (tree_edges s)\<^sup>*

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
white_path s x y = ((x, y) \<in> (tree_edges s)\<^sup>*)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
white_path s x y = ((x, y) \<in> (tree_edges s)\<^sup>*)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma uncurry_fun_rel_conv:
    "(uncurry f, uncurry g) \<in> A\<times>\<^sub>rB \<rightarrow> R \<longleftrightarrow> (f,g)\<in>A\<rightarrow>B\<rightarrow>R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((uncurry f, uncurry g) \<in> A \<times>\<^sub>r B \<rightarrow> R) = ((f, g) \<in> A \<rightarrow> B \<rightarrow> R)
[PROOF STEP]
by (auto simp: uncurry_def dest!: fun_relD intro: prod_relI)


[STATEMENT]
lemma uncurry0_fun_rel_conv:
    "(uncurry0 f, uncurry0 g) \<in> unit_rel \<rightarrow> R \<longleftrightarrow> (f,g)\<in>R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((uncurry0 f, uncurry0 g) \<in> unit_rel \<rightarrow> R) = ((f, g) \<in> R)
[PROOF STEP]
by (auto dest!: fun_relD)


[STATEMENT]
lemma RETURN_rel_conv0: "(RETURN f, RETURN g)\<in>\<langle>A\<rangle>nres_rel \<longleftrightarrow> (f,g)\<in>A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((RETURN f, RETURN g) \<in> \<langle>A\<rangle>nres_rel) = ((f, g) \<in> A)
[PROOF STEP]
by (auto simp: nres_rel_def)


[STATEMENT]
lemma RETURN_rel_conv1: "(RETURN o f, RETURN o g)\<in>A \<rightarrow> \<langle>B\<rangle>nres_rel \<longleftrightarrow> (f,g)\<in>A\<rightarrow>B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((RETURN \<circ> f, RETURN \<circ> g) \<in> A \<rightarrow> \<langle>B\<rangle>nres_rel) = ((f, g) \<in> A \<rightarrow> B)
[PROOF STEP]
by (auto simp: nres_rel_def dest!: fun_relD)


[STATEMENT]
lemma RETURN_rel_conv2: "(RETURN oo f, RETURN oo g)\<in>A \<rightarrow> B \<rightarrow> \<langle>R\<rangle>nres_rel \<longleftrightarrow> (f,g)\<in>A\<rightarrow>B\<rightarrow>R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((RETURN \<circ>\<circ> f, RETURN \<circ>\<circ> g) \<in> A \<rightarrow> B \<rightarrow> \<langle>R\<rangle>nres_rel) = ((f, g) \<in> A \<rightarrow> B \<rightarrow> R)
[PROOF STEP]
by (auto simp: nres_rel_def dest!: fun_relD)


[STATEMENT]
lemma RETURN_rel_conv3: "(RETURN ooo f, RETURN ooo g)\<in>A\<rightarrow>B\<rightarrow>C \<rightarrow> \<langle>R\<rangle>nres_rel \<longleftrightarrow> (f,g)\<in>A\<rightarrow>B\<rightarrow>C\<rightarrow>R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((RETURN \<circ>\<circ>\<circ> f, RETURN \<circ>\<circ>\<circ> g) \<in> A \<rightarrow> B \<rightarrow> C \<rightarrow> \<langle>R\<rangle>nres_rel) = ((f, g) \<in> A \<rightarrow> B \<rightarrow> C \<rightarrow> R)
[PROOF STEP]
by (auto simp: nres_rel_def dest!: fun_relD)


[STATEMENT]
lemma IS_BELOW_ID_D: "(a,b)\<in>R \<Longrightarrow> IS_BELOW_ID R \<Longrightarrow> a=b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(a, b) \<in> R; IS_BELOW_ID R\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
by (auto simp: IS_BELOW_ID_def)


[STATEMENT]
lemma nnf_semantics: "\<A> \<Turnstile> nnf F \<longleftrightarrow> \<A> \<Turnstile> F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<A> \<Turnstile> nnf F = \<A> \<Turnstile> F
[PROOF STEP]
by(induction F rule: nnf.induct; simp)


[STATEMENT]
lemma cnf_semantics: "is_nnf F \<Longrightarrow> cnf_semantics \<A> (cnf F) \<longleftrightarrow> \<A> \<Turnstile> F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_nnf F \<Longrightarrow> cnf_semantics \<A> (cnf F) = \<A> \<Turnstile> F
[PROOF STEP]
by(induction F rule: cnf.induct; simp add: cnf_semantics_def clause_semantics_def ball_Un; metis Un_iff)


[STATEMENT]
lemma cnf_form_semantics:
  fixes F :: "'a formula"
  assumes nnf: "is_nnf F"
  shows "\<A> \<Turnstile> cnf_form_of F \<longleftrightarrow> \<A> \<Turnstile> F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<A> \<Turnstile> cnf_form_of F = \<A> \<Turnstile> F
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<A> \<Turnstile> cnf_form_of F = \<A> \<Turnstile> F
[PROOF STEP]
define cnf_semantics_list
    where "cnf_semantics_list \<A> S \<longleftrightarrow> (\<forall>s \<in> set S. \<exists>l \<in> set s. lit_semantics \<A> (l :: 'a literal))"
    for \<A> S
[PROOF STATE]
proof (state)
this:
cnf_semantics_list ?\<A> ?S = (\<forall>s\<in>set ?S. \<exists>l\<in>set s. lit_semantics ?\<A> l)

goal (1 subgoal):
 1. \<A> \<Turnstile> cnf_form_of F = \<A> \<Turnstile> F
[PROOF STEP]
have tcn: "cnf F = set (map set (cnf_lists F))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnf F = set (map set (cnf_lists F))
[PROOF STEP]
using nnf
[PROOF STATE]
proof (prove)
using this:
is_nnf F

goal (1 subgoal):
 1. cnf F = set (map set (cnf_lists F))
[PROOF STEP]
by(induction F rule: cnf.induct) (auto simp add: image_UN image_comp comp_def )
[PROOF STATE]
proof (state)
this:
cnf F = set (map set (cnf_lists F))

goal (1 subgoal):
 1. \<A> \<Turnstile> cnf_form_of F = \<A> \<Turnstile> F
[PROOF STEP]
have "\<A> \<Turnstile> F \<longleftrightarrow> cnf_semantics \<A> (cnf F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<A> \<Turnstile> F = cnf_semantics \<A> (cnf F)
[PROOF STEP]
using cnf_semantics[OF nnf]
[PROOF STATE]
proof (prove)
using this:
cnf_semantics ?\<A> (cnf F) = ?\<A> \<Turnstile> F

goal (1 subgoal):
 1. \<A> \<Turnstile> F = cnf_semantics \<A> (cnf F)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<A> \<Turnstile> F = cnf_semantics \<A> (cnf F)

goal (1 subgoal):
 1. \<A> \<Turnstile> cnf_form_of F = \<A> \<Turnstile> F
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<A> \<Turnstile> F = cnf_semantics \<A> (cnf F)

goal (1 subgoal):
 1. \<A> \<Turnstile> cnf_form_of F = \<A> \<Turnstile> F
[PROOF STEP]
have "\<dots> = cnf_semantics \<A> (set (map set (cnf_lists F)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnf_semantics \<A> (cnf F) = cnf_semantics \<A> (set (map set (cnf_lists F)))
[PROOF STEP]
unfolding tcn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnf_semantics \<A> (set (map set (cnf_lists F))) = cnf_semantics \<A> (set (map set (cnf_lists F)))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
cnf_semantics \<A> (cnf F) = cnf_semantics \<A> (set (map set (cnf_lists F)))

goal (1 subgoal):
 1. \<A> \<Turnstile> cnf_form_of F = \<A> \<Turnstile> F
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cnf_semantics \<A> (cnf F) = cnf_semantics \<A> (set (map set (cnf_lists F)))

goal (1 subgoal):
 1. \<A> \<Turnstile> cnf_form_of F = \<A> \<Turnstile> F
[PROOF STEP]
have "\<dots> = cnf_semantics_list \<A> (cnf_lists F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnf_semantics \<A> (set (map set (cnf_lists F))) = cnf_semantics_list \<A> (cnf_lists F)
[PROOF STEP]
unfolding cnf_semantics_def clause_semantics_def cnf_semantics_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>C\<in>set (map set (cnf_lists F)). \<exists>L\<in>C. lit_semantics \<A> L) = (\<forall>s\<in>set (cnf_lists F). Bex (set s) (lit_semantics \<A>))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
cnf_semantics \<A> (set (map set (cnf_lists F))) = cnf_semantics_list \<A> (cnf_lists F)

goal (1 subgoal):
 1. \<A> \<Turnstile> cnf_form_of F = \<A> \<Turnstile> F
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cnf_semantics \<A> (set (map set (cnf_lists F))) = cnf_semantics_list \<A> (cnf_lists F)

goal (1 subgoal):
 1. \<A> \<Turnstile> cnf_form_of F = \<A> \<Turnstile> F
[PROOF STEP]
have "\<dots> = \<A> \<Turnstile> (cnf_form_of F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnf_semantics_list \<A> (cnf_lists F) = \<A> \<Turnstile> cnf_form_of F
[PROOF STEP]
using nnf
[PROOF STATE]
proof (prove)
using this:
is_nnf F

goal (1 subgoal):
 1. cnf_semantics_list \<A> (cnf_lists F) = \<A> \<Turnstile> cnf_form_of F
[PROOF STEP]
by(induction F rule: cnf_lists.induct;
       simp add: cnf_semantics_list_def cnf_form_of_defs  ball_Un bex_Un)
[PROOF STATE]
proof (state)
this:
cnf_semantics_list \<A> (cnf_lists F) = \<A> \<Turnstile> cnf_form_of F

goal (1 subgoal):
 1. \<A> \<Turnstile> cnf_form_of F = \<A> \<Turnstile> F
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<A> \<Turnstile> F = \<A> \<Turnstile> cnf_form_of F
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<A> \<Turnstile> F = \<A> \<Turnstile> cnf_form_of F

goal (1 subgoal):
 1. \<A> \<Turnstile> cnf_form_of F = \<A> \<Turnstile> F
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<A> \<Turnstile> cnf_form_of F = \<A> \<Turnstile> F

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma JVM_states_unfold:
  "states P mxs mxl \<equiv> err(opt((Union {list n (types P) |n. n <= mxs}) \<times>
                                 list mxl (err(types P))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. states P mxs mxl \<equiv> err (opt (\<Union> {list n (types P) |n. n \<le> mxs} \<times> list mxl (err (types P))))
[PROOF STEP]
apply (unfold states_def sl_def Opt.esl_def Err.sl_def
         stk_esl_def loc_sl_def Product.esl_def
         Listn.sl_def upto_esl_def SemiType.esl_def Err.esl_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (case case (case case (types P, widen P, SemiType.sup P) of (A, r, f) \<Rightarrow> (\<Union> {list n A |n. n \<le> mxs}, Listn.le r, Listn.sup f) of (A, r\<^sub>A, f\<^sub>A) \<Rightarrow> \<lambda>(B, r\<^sub>B, f\<^sub>B). (A \<times> B, Product.le r\<^sub>A r\<^sub>B, Product.sup f\<^sub>A f\<^sub>B)) (case case case (types P, widen P, SemiType.sup P) of (A, r, f) \<Rightarrow> (err A, Err.le r, lift2 f) of (A, r, f) \<Rightarrow> (list mxl A, Listn.le r, map2 f) of (A, r, f) \<Rightarrow> (A, r, \<lambda>x y. OK (f x y))) of (A, r, f) \<Rightarrow> (opt A, Opt.le r, Opt.sup f) of (A, r, f) \<Rightarrow> (err A, Err.le r, lift2 f)) \<equiv> err (opt (\<Union> {list n (types P) |n. n \<le> mxs} \<times> list mxl (err (types P))))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma JVM_le_unfold:
 "le P m n \<equiv>
  Err.le(Opt.le(Product.le(Listn.le(widen P))(Listn.le(Err.le(widen P)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. JVM_SemiType.le P m n \<equiv> Err.le (Opt.le (Product.le (Listn.le (widen P)) (Listn.le (Err.le (widen P)))))
[PROOF STEP]
apply (unfold le_def sl_def Opt.esl_def Err.sl_def
         stk_esl_def loc_sl_def Product.esl_def
         Listn.sl_def upto_esl_def SemiType.esl_def Err.esl_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (case case (case case (types P, widen P, SemiType.sup P) of (A, r, f) \<Rightarrow> (\<Union> {list n A |n. n \<le> m}, Listn.le r, Listn.sup f) of (A, r\<^sub>A, f\<^sub>A) \<Rightarrow> \<lambda>(B, r\<^sub>B, f\<^sub>B). (A \<times> B, Product.le r\<^sub>A r\<^sub>B, Product.sup f\<^sub>A f\<^sub>B)) (case case case (types P, widen P, SemiType.sup P) of (A, r, f) \<Rightarrow> (err A, Err.le r, lift2 f) of (A, r, f) \<Rightarrow> (list n A, Listn.le r, map2 f) of (A, r, f) \<Rightarrow> (A, r, \<lambda>x y. OK (f x y))) of (A, r, f) \<Rightarrow> (opt A, Opt.le r, Opt.sup f) of (A, r, f) \<Rightarrow> (err A, Err.le r, lift2 f))) \<equiv> Err.le (Opt.le (Product.le (Listn.le (widen P)) (Listn.le (Err.le (widen P)))))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sl_def2:
  "JVM_SemiType.sl P mxs mxl \<equiv>
  (states P mxs mxl, JVM_SemiType.le P mxs mxl, JVM_SemiType.sup P mxs mxl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. JVM_SemiType.sl P mxs mxl \<equiv> (states P mxs mxl, JVM_SemiType.le P mxs mxl, JVM_SemiType.sup P mxs mxl)
[PROOF STEP]
by (unfold JVM_SemiType.sup_def states_def JVM_SemiType.le_def) simp


[STATEMENT]
lemma JVM_le_conv:
  "le P m n (OK t1) (OK t2) = P \<turnstile> t1 \<le>' t2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. JVM_SemiType.le P m n (OK t1) (OK t2) = P \<turnstile> t1 \<le>' t2
[PROOF STEP]
by (simp add: JVM_le_unfold Err.le_def lesub_def sup_state_opt_def
                sup_state_def sup_ty_opt_def)


[STATEMENT]
lemma JVM_le_Err_conv:
  "le P m n = Err.le (sup_state_opt P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. JVM_SemiType.le P m n = Err.le (sup_state_opt P)
[PROOF STEP]
by (unfold sup_state_opt_def sup_state_def
             sup_ty_opt_def JVM_le_unfold) simp


[STATEMENT]
lemma err_le_unfold [iff]:
  "Err.le r (OK a) (OK b) = r a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Err.le r (OK a) (OK b) = r a b
[PROOF STEP]
by (simp add: Err.le_def lesub_def)


[STATEMENT]
lemma order_sup_state_opt [intro, simp]:
  "wf_prog wf_mb P \<Longrightarrow> order (sup_state_opt P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog wf_mb P \<Longrightarrow> order (sup_state_opt P)
[PROOF STEP]
by (unfold sup_state_opt_def sup_state_def sup_ty_opt_def) blast


[STATEMENT]
lemma semilat_JVM [intro?]:
  "wf_prog wf_mb P \<Longrightarrow> semilat (JVM_SemiType.sl P mxs mxl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog wf_mb P \<Longrightarrow> semilat (JVM_SemiType.sl P mxs mxl)
[PROOF STEP]
apply (unfold JVM_SemiType.sl_def stk_esl_def loc_sl_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog wf_mb P \<Longrightarrow> err_semilat (Opt.esl (Product.esl (upto_esl mxs (SemiType.esl P)) (Err.esl (Listn.sl mxl (Err.sl (SemiType.esl P))))))
[PROOF STEP]
apply (blast intro: err_semilat_Product_esl err_semilat_upto_esl
                      Listn_sl err_semilat_JType_esl)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma acc_JVM [intro]:
  "wf_prog wf_mb P \<Longrightarrow> acc (JVM_SemiType.states P mxs mxl) (JVM_SemiType.le P mxs mxl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog wf_mb P \<Longrightarrow> acc (states P mxs mxl) (JVM_SemiType.le P mxs mxl)
[PROOF STEP]
by(unfold JVM_le_unfold JVM_states_unfold) blast


[STATEMENT]
lemma widen_refl[iff]: "widen P t t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> t \<le> t
[PROOF STEP]
by (simp add: fun_of_def)


[STATEMENT]
lemma sup_ty_opt_refl [iff]: "P \<turnstile> T \<le>\<^sub>\<top> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> T \<le>\<^sub>\<top> T
[PROOF STEP]
apply (unfold sup_ty_opt_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Err.le (widen P) T T
[PROOF STEP]
apply (fold lesub_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T \<sqsubseteq>\<^bsub>Err.le (widen P)\<^esub> T
[PROOF STEP]
apply (rule le_err_refl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. x \<sqsubseteq>\<^bsub>widen P\<^esub> x
[PROOF STEP]
apply (simp add: lesub_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Err_any_conv [iff]: "P \<turnstile> Err \<le>\<^sub>\<top> T = (T = Err)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> Err \<le>\<^sub>\<top> T = (T = Err)
[PROOF STEP]
by (unfold sup_ty_opt_def) (rule Err_le_conv [simplified lesub_def])


[STATEMENT]
lemma any_Err [iff]: "P \<turnstile> T \<le>\<^sub>\<top> Err"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> T \<le>\<^sub>\<top> Err
[PROOF STEP]
by (unfold sup_ty_opt_def) (rule le_Err [simplified lesub_def])


[STATEMENT]
lemma OK_OK_conv [iff]:
  "P \<turnstile> OK T \<le>\<^sub>\<top> OK T' = P \<turnstile> T \<le> T'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> OK T \<le>\<^sub>\<top> OK T' = P \<turnstile> T \<le> T'
[PROOF STEP]
by (simp add: sup_ty_opt_def fun_of_def)


[STATEMENT]
lemma any_OK_conv [iff]:
  "P \<turnstile> X \<le>\<^sub>\<top> OK T' = (\<exists>T. X = OK T \<and> P \<turnstile> T \<le> T')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> X \<le>\<^sub>\<top> OK T' = (\<exists>T. X = OK T \<and> P \<turnstile> T \<le> T')
[PROOF STEP]
apply (unfold sup_ty_opt_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Err.le (widen P) X (OK T') = (\<exists>T. X = OK T \<and> P \<turnstile> T \<le> T')
[PROOF STEP]
apply (rule le_OK_conv [simplified lesub_def])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma OK_any_conv:
 "P \<turnstile> OK T \<le>\<^sub>\<top> X = (X = Err \<or> (\<exists>T'. X = OK T' \<and> P \<turnstile> T \<le> T'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> OK T \<le>\<^sub>\<top> X = (X = Err \<or> (\<exists>T'. X = OK T' \<and> P \<turnstile> T \<le> T'))
[PROOF STEP]
apply (unfold sup_ty_opt_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Err.le (widen P) (OK T) X = (X = Err \<or> (\<exists>T'. X = OK T' \<and> P \<turnstile> T \<le> T'))
[PROOF STEP]
apply (rule OK_le_conv [simplified lesub_def])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sup_ty_opt_trans [intro?, trans]:
  "\<lbrakk>P \<turnstile> a \<le>\<^sub>\<top> b; P \<turnstile> b \<le>\<^sub>\<top> c\<rbrakk> \<Longrightarrow> P \<turnstile> a \<le>\<^sub>\<top> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> a \<le>\<^sub>\<top> b; P \<turnstile> b \<le>\<^sub>\<top> c\<rbrakk> \<Longrightarrow> P \<turnstile> a \<le>\<^sub>\<top> c
[PROOF STEP]
by (auto intro: widen_trans
           simp add: sup_ty_opt_def Err.le_def lesub_def fun_of_def
           split: err.splits)


[STATEMENT]
lemma stk_convert:
  "P \<turnstile> ST [\<le>] ST' = Listn.le (widen P) ST ST'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> ST [\<le>] ST' = Listn.le (widen P) ST ST'
[PROOF STEP]
by (simp add: Listn.le_def lesub_def)


[STATEMENT]
lemma sup_loc_refl [iff]: "P \<turnstile> LT [\<le>\<^sub>\<top>] LT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> LT [\<le>\<^sub>\<top>] LT
[PROOF STEP]
by (rule list_all2_refl) simp


[STATEMENT]
lemma sup_loc_def:
  "P \<turnstile> LT [\<le>\<^sub>\<top>] LT' \<equiv> Listn.le (sup_ty_opt P) LT LT'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> LT [\<le>\<^sub>\<top>] LT' \<equiv> Listn.le (sup_ty_opt P) LT LT'
[PROOF STEP]
by (simp add: Listn.le_def lesub_def)


[STATEMENT]
lemma sup_loc_widens_conv [iff]:
  "P \<turnstile> map OK Ts [\<le>\<^sub>\<top>] map OK Ts' = P \<turnstile> Ts [\<le>] Ts'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> map OK Ts [\<le>\<^sub>\<top>] map OK Ts' = P \<turnstile> Ts [\<le>] Ts'
[PROOF STEP]
by (simp add: list_all2_map1 list_all2_map2)


[STATEMENT]
lemma sup_loc_trans [intro?, trans]:
  "\<lbrakk>P \<turnstile> a [\<le>\<^sub>\<top>] b; P \<turnstile> b [\<le>\<^sub>\<top>] c\<rbrakk> \<Longrightarrow> P \<turnstile> a [\<le>\<^sub>\<top>] c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> a [\<le>\<^sub>\<top>] b; P \<turnstile> b [\<le>\<^sub>\<top>] c\<rbrakk> \<Longrightarrow> P \<turnstile> a [\<le>\<^sub>\<top>] c
[PROOF STEP]
by (rule list_all2_trans, rule sup_ty_opt_trans)


[STATEMENT]
lemma sup_state_conv [iff]:
  "P \<turnstile> (ST,LT) \<le>\<^sub>i (ST',LT') = (P \<turnstile> ST [\<le>] ST' \<and> P \<turnstile> LT [\<le>\<^sub>\<top>] LT')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> (ST, LT) \<le>\<^sub>i (ST', LT') = (P \<turnstile> ST [\<le>] ST' \<and> P \<turnstile> LT [\<le>\<^sub>\<top>] LT')
[PROOF STEP]
by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def sup_loc_def)


[STATEMENT]
lemma sup_state_conv2:
  "P \<turnstile> s1 \<le>\<^sub>i s2 = (P \<turnstile> fst s1 [\<le>] fst s2 \<and> P \<turnstile> snd s1 [\<le>\<^sub>\<top>] snd s2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> s1 \<le>\<^sub>i s2 = (P \<turnstile> fst s1 [\<le>] fst s2 \<and> P \<turnstile> snd s1 [\<le>\<^sub>\<top>] snd s2)
[PROOF STEP]
by (cases s1, cases s2) simp


[STATEMENT]
lemma sup_state_refl [iff]: "P \<turnstile> s \<le>\<^sub>i s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> s \<le>\<^sub>i s
[PROOF STEP]
by (auto simp add: sup_state_conv2 intro: list_all2_refl)


[STATEMENT]
lemma sup_state_trans [intro?, trans]:
  "\<lbrakk>P \<turnstile> a \<le>\<^sub>i b; P \<turnstile> b \<le>\<^sub>i c\<rbrakk> \<Longrightarrow> P \<turnstile> a \<le>\<^sub>i c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> a \<le>\<^sub>i b; P \<turnstile> b \<le>\<^sub>i c\<rbrakk> \<Longrightarrow> P \<turnstile> a \<le>\<^sub>i c
[PROOF STEP]
by (auto intro: sup_loc_trans widens_trans simp add: sup_state_conv2)


[STATEMENT]
lemma sup_state_opt_None_any [iff]:
  "P \<turnstile> None \<le>' s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> None \<le>' s
[PROOF STEP]
by (simp add: sup_state_opt_def Opt.le_def)


[STATEMENT]
lemma sup_state_opt_any_None [iff]:
  "P \<turnstile> s \<le>' None = (s = None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> s \<le>' None = (s = None)
[PROOF STEP]
by (simp add: sup_state_opt_def Opt.le_def)


[STATEMENT]
lemma sup_state_opt_Some_Some [iff]:
  "P \<turnstile> Some a \<le>' Some b = P \<turnstile> a \<le>\<^sub>i b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> \<lfloor>a\<rfloor> \<le>' \<lfloor>b\<rfloor> = P \<turnstile> a \<le>\<^sub>i b
[PROOF STEP]
by (simp add: sup_state_opt_def Opt.le_def lesub_def)


[STATEMENT]
lemma sup_state_opt_refl [iff]: "P \<turnstile> s \<le>' s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> s \<le>' s
[PROOF STEP]
by (simp add: sup_state_opt_def Opt.le_def lesub_def)


[STATEMENT]
lemma sup_state_opt_trans [intro?, trans]:
  "\<lbrakk>P \<turnstile> a \<le>' b; P \<turnstile> b \<le>' c\<rbrakk> \<Longrightarrow> P \<turnstile> a \<le>' c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> a \<le>' b; P \<turnstile> b \<le>' c\<rbrakk> \<Longrightarrow> P \<turnstile> a \<le>' c
[PROOF STEP]
apply (unfold sup_state_opt_def Opt.le_def lesub_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>case b of None \<Rightarrow> a = None | \<lfloor>y\<rfloor> \<Rightarrow> case a of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> P \<turnstile> x \<le>\<^sub>i y; case c of None \<Rightarrow> b = None | \<lfloor>y\<rfloor> \<Rightarrow> case b of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> P \<turnstile> x \<le>\<^sub>i y\<rbrakk> \<Longrightarrow> case c of None \<Rightarrow> a = None | \<lfloor>y\<rfloor> \<Rightarrow> case a of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> P \<turnstile> x \<le>\<^sub>i y
[PROOF STEP]
apply (simp del: split_paired_All)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x2 x2a x2b. \<lbrakk>c = \<lfloor>x2a\<rfloor>; P \<turnstile> x2 \<le>\<^sub>i x2a; b = \<lfloor>x2\<rfloor>; a = \<lfloor>x2b\<rfloor>; P \<turnstile> x2b \<le>\<^sub>i x2\<rbrakk> \<Longrightarrow> P \<turnstile> x2b \<le>\<^sub>i x2a
[PROOF STEP]
apply (rule sup_state_trans, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Lp_cases_1_PInf:
  assumes "p \<ge> (1::ennreal)"
  obtains (gr) p2 where "p = ennreal p2" "p2 > 1" "p > 1"
    | (one) "p = 1"
    | (PInf) "p = \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>p2. \<lbrakk>p = ennreal p2; 1 < p2; 1 < p\<rbrakk> \<Longrightarrow> thesis; p = 1 \<Longrightarrow> thesis; p = \<infinity> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
1 \<le> p

goal (1 subgoal):
 1. \<lbrakk>\<And>p2. \<lbrakk>p = ennreal p2; 1 < p2; 1 < p\<rbrakk> \<Longrightarrow> thesis; p = 1 \<Longrightarrow> thesis; p = \<infinity> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (metis (full_types) antisym_conv ennreal_cases ennreal_le_1 infinity_ennreal_def not_le)


[STATEMENT]
lemma Lp_cases:
  obtains (real_pos) p2 where "p = ennreal p2" "p2 > 0" "p > 0"
    | (zero) "p = 0"
    | (PInf) "p = \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>p2. \<lbrakk>p = ennreal p2; 0 < p2; 0 < p\<rbrakk> \<Longrightarrow> thesis; p = 0 \<Longrightarrow> thesis; p = \<infinity> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (metis enn2real_positive_iff ennreal_enn2real_if infinity_ennreal_def not_gr_zero top.not_eq_extremum)


[STATEMENT]
lemma conjugate_exponent_real:
  assumes "p > (1::real)"
  shows "1/p + 1/(conjugate_exponent p) = 1"
        "conjugate_exponent p > 1"
        "conjugate_exponent(conjugate_exponent p) = p"
        "(p-1) * conjugate_exponent p = p"
        "p - p / conjugate_exponent p = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 / p + 1 / conjugate_exponent p = 1 &&& 1 < conjugate_exponent p) &&& conjugate_exponent (conjugate_exponent p) = p &&& (p - 1) * conjugate_exponent p = p &&& p - p / conjugate_exponent p = 1
[PROOF STEP]
unfolding conjugate_exponent_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 / p + 1 / (1 + 1 / (p - 1)) = 1 &&& 1 < 1 + 1 / (p - 1)) &&& 1 + 1 / (1 + 1 / (p - 1) - 1) = p &&& (p - 1) * (1 + 1 / (p - 1)) = p &&& p - p / (1 + 1 / (p - 1)) = 1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
1 < p

goal (1 subgoal):
 1. (1 / p + 1 / (1 + 1 / (p - 1)) = 1 &&& 1 < 1 + 1 / (p - 1)) &&& 1 + 1 / (1 + 1 / (p - 1) - 1) = p &&& (p - 1) * (1 + 1 / (p - 1)) = p &&& p - p / (1 + 1 / (p - 1)) = 1
[PROOF STEP]
by (auto simp add: algebra_simps divide_simps)


[STATEMENT]
lemma conjugate_exponent_real_iff:
  assumes "p > (1::real)"
  shows "q = conjugate_exponent p \<longleftrightarrow> (1/p + 1/q = 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (q = conjugate_exponent p) = (1 / p + 1 / q = 1)
[PROOF STEP]
unfolding conjugate_exponent_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (q = 1 + 1 / (p - 1)) = (1 / p + 1 / q = 1)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
1 < p

goal (1 subgoal):
 1. (q = 1 + 1 / (p - 1)) = (1 / p + 1 / q = 1)
[PROOF STEP]
by (auto simp add: algebra_simps divide_simps)


[STATEMENT]
lemma conjugate_exponent_real_2 [simp]:
  "conjugate_exponent (2::real) = 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conjugate_exponent 2 = 2
[PROOF STEP]
unfolding conjugate_exponent_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + 1 / (2 - 1) = 2
[PROOF STEP]
by (auto simp add: algebra_simps divide_simps)


[STATEMENT]
lemma conjugate_exponent_realI:
  assumes "p > (0::real)" "q > 0" "1/p + 1/q = 1"
  shows "p > 1" "q = conjugate_exponent p" "q > 1" "p = conjugate_exponent q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 < p &&& q = conjugate_exponent p) &&& 1 < q &&& p = conjugate_exponent q
[PROOF STEP]
unfolding conjugate_exponent_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 < p &&& q = 1 + 1 / (p - 1)) &&& 1 < q &&& p = 1 + 1 / (q - 1)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < p
0 < q
1 / p + 1 / q = 1

goal (1 subgoal):
 1. (1 < p &&& q = 1 + 1 / (p - 1)) &&& 1 < q &&& p = 1 + 1 / (q - 1)
[PROOF STEP]
apply (auto simp add: algebra_simps divide_simps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < p; 0 < q; p + q = p * q\<rbrakk> \<Longrightarrow> 1 < p
 2. \<lbrakk>0 < p; 0 < q; p + q = p * q\<rbrakk> \<Longrightarrow> 1 < q
[PROOF STEP]
apply (metis assms(3) divide_less_eq_1_pos less_add_same_cancel1 zero_less_divide_1_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < p; 0 < q; p + q = p * q\<rbrakk> \<Longrightarrow> 1 < q
[PROOF STEP]
using mult_less_cancel_left_pos
[PROOF STATE]
proof (prove)
using this:
(0::?'a) < ?c \<Longrightarrow> (?c * ?a < ?c * ?b) = (?a < ?b)

goal (1 subgoal):
 1. \<lbrakk>0 < p; 0 < q; p + q = p * q\<rbrakk> \<Longrightarrow> 1 < q
[PROOF STEP]
by fastforce


[STATEMENT]
lemma conjugate_exponent_real_ennreal:
  assumes "p> (1::real)"
  shows "conjugate_exponent(ennreal p) = ennreal(conjugate_exponent p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conjugate_exponent (ennreal p) = ennreal (conjugate_exponent p)
[PROOF STEP]
unfolding conjugate_exponent_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + 1 / (ennreal p - 1) = ennreal (1 + 1 / (p - 1))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
1 < p

goal (1 subgoal):
 1. 1 + 1 / (ennreal p - 1) = ennreal (1 + 1 / (p - 1))
[PROOF STEP]
by (auto, metis diff_gt_0_iff_gt divide_ennreal ennreal_1 ennreal_minus zero_le_one)


[STATEMENT]
lemma conjugate_exponent_ennreal_1_2_PInf [simp]:
  "conjugate_exponent (1::ennreal) = \<infinity>"
  "conjugate_exponent (\<infinity>::ennreal) = 1"
  "conjugate_exponent (\<top>::ennreal) = 1"
  "conjugate_exponent (2::ennreal) = 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (conjugate_exponent 1 = \<infinity> &&& conjugate_exponent \<infinity> = 1) &&& conjugate_exponent \<top> = 1 &&& conjugate_exponent 2 = 2
[PROOF STEP]
using conjugate_exponent_real_ennreal[of 2]
[PROOF STATE]
proof (prove)
using this:
1 < 2 \<Longrightarrow> conjugate_exponent (ennreal 2) = ennreal (conjugate_exponent 2)

goal (1 subgoal):
 1. (conjugate_exponent 1 = \<infinity> &&& conjugate_exponent \<infinity> = 1) &&& conjugate_exponent \<top> = 1 &&& conjugate_exponent 2 = 2
[PROOF STEP]
by (auto simp add: conjugate_exponent_def)