[STATEMENT]
lemma
  augment_edge:
  assumes sg: "subgraph G1 G" "subgraph G2 G" and
    p: "(u, v) \<in> {(a, b) |a b. nodes_connected G1 a b}"
  and notinE2:  "(u, v) \<notin> {(a, b) |a b. nodes_connected G2 a b}"

shows "\<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a=aa \<and> b=ba \<or> a=ba \<and> b=aa)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
from sg
[PROOF STATE]
proof (chain)
picking this:
subgraph G1 G
subgraph G2 G
[PROOF STEP]
have [simp]: "nodes G1 = nodes G" "nodes G2 = nodes G"
[PROOF STATE]
proof (prove)
using this:
subgraph G1 G
subgraph G2 G

goal (1 subgoal):
 1. nodes G1 = V &&& nodes G2 = V
[PROOF STEP]
unfolding subgraph_def
[PROOF STATE]
proof (prove)
using this:
nodes G1 = V \<and> edges G1 \<subseteq> E
nodes G2 = V \<and> edges G2 \<subseteq> E

goal (1 subgoal):
 1. nodes G1 = V &&& nodes G2 = V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nodes G1 = V
nodes G2 = V

goal (1 subgoal):
 1. \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
from p
[PROOF STATE]
proof (chain)
picking this:
(u, v) \<in> {(a, b) |a b. nodes_connected G1 a b}
[PROOF STEP]
obtain p where a: "is_path_undir G1 u p v"
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> {(a, b) |a b. nodes_connected G1 a b}

goal (1 subgoal):
 1. (\<And>p. is_path_undir G1 u p v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_path_undir G1 u p v

goal (1 subgoal):
 1. \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
from notinE2
[PROOF STATE]
proof (chain)
picking this:
(u, v) \<notin> {(a, b) |a b. nodes_connected G2 a b}
[PROOF STEP]
have b: "~(\<exists>p. is_path_undir G2 u p v)"
[PROOF STATE]
proof (prove)
using this:
(u, v) \<notin> {(a, b) |a b. nodes_connected G2 a b}

goal (1 subgoal):
 1. \<not> nodes_connected G2 u v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> nodes_connected G2 u v

goal (1 subgoal):
 1. \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
from a b
[PROOF STATE]
proof (chain)
picking this:
is_path_undir G1 u p v
\<not> nodes_connected G2 u v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_path_undir G1 u p v
\<not> nodes_connected G2 u v

goal (1 subgoal):
 1. \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
proof (induct p arbitrary: u)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>u. \<lbrakk>is_path_undir G1 u [] v; \<not> nodes_connected G2 u v\<rbrakk> \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
 2. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>is_path_undir G1 u p v; \<not> nodes_connected G2 u v\<rbrakk> \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa); is_path_undir G1 u (a # p) v; \<not> nodes_connected G2 u v\<rbrakk> \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
is_path_undir G1 u [] v
\<not> nodes_connected G2 u v

goal (2 subgoals):
 1. \<And>u. \<lbrakk>is_path_undir G1 u [] v; \<not> nodes_connected G2 u v\<rbrakk> \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
 2. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>is_path_undir G1 u p v; \<not> nodes_connected G2 u v\<rbrakk> \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa); is_path_undir G1 u (a # p) v; \<not> nodes_connected G2 u v\<rbrakk> \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_path_undir G1 u [] v
\<not> nodes_connected G2 u v
[PROOF STEP]
have "u=v" "u\<in>nodes G1"
[PROOF STATE]
proof (prove)
using this:
is_path_undir G1 u [] v
\<not> nodes_connected G2 u v

goal (1 subgoal):
 1. u = v &&& u \<in> nodes G1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u = v
u \<in> nodes G1

goal (2 subgoals):
 1. \<And>u. \<lbrakk>is_path_undir G1 u [] v; \<not> nodes_connected G2 u v\<rbrakk> \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
 2. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>is_path_undir G1 u p v; \<not> nodes_connected G2 u v\<rbrakk> \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa); is_path_undir G1 u (a # p) v; \<not> nodes_connected G2 u v\<rbrakk> \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u = v
u \<in> nodes G1
[PROOF STEP]
have "is_path_undir G2 u [] v"
[PROOF STATE]
proof (prove)
using this:
u = v
u \<in> nodes G1

goal (1 subgoal):
 1. is_path_undir G2 u [] v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_path_undir G2 u [] v

goal (2 subgoals):
 1. \<And>u. \<lbrakk>is_path_undir G1 u [] v; \<not> nodes_connected G2 u v\<rbrakk> \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
 2. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>is_path_undir G1 u p v; \<not> nodes_connected G2 u v\<rbrakk> \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa); is_path_undir G1 u (a # p) v; \<not> nodes_connected G2 u v\<rbrakk> \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
have "(u, v) \<in> {(a, b) |a b. nodes_connected G2 a b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u, v) \<in> {(a, b) |a b. nodes_connected G2 a b}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nodes_connected G2 u v
[PROOF STEP]
apply(rule exI[where x="[]"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path_undir G2 u [] v
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
(u, v) \<in> {(a, b) |a b. nodes_connected G2 a b}

goal (2 subgoals):
 1. \<And>u. \<lbrakk>is_path_undir G1 u [] v; \<not> nodes_connected G2 u v\<rbrakk> \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
 2. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>is_path_undir G1 u p v; \<not> nodes_connected G2 u v\<rbrakk> \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa); is_path_undir G1 u (a # p) v; \<not> nodes_connected G2 u v\<rbrakk> \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
with Nil(2)
[PROOF STATE]
proof (chain)
picking this:
\<not> nodes_connected G2 u v
(u, v) \<in> {(a, b) |a b. nodes_connected G2 a b}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<not> nodes_connected G2 u v
(u, v) \<in> {(a, b) |a b. nodes_connected G2 a b}

goal (1 subgoal):
 1. \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)

goal (1 subgoal):
 1. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>is_path_undir G1 u p v; \<not> nodes_connected G2 u v\<rbrakk> \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa); is_path_undir G1 u (a # p) v; \<not> nodes_connected G2 u v\<rbrakk> \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>is_path_undir G1 u p v; \<not> nodes_connected G2 u v\<rbrakk> \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa); is_path_undir G1 u (a # p) v; \<not> nodes_connected G2 u v\<rbrakk> \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
case (Cons a p)
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_path_undir G1 ?u p v; \<not> nodes_connected G2 ?u v\<rbrakk> \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
is_path_undir G1 u (a # p) v
\<not> nodes_connected G2 u v

goal (1 subgoal):
 1. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>is_path_undir G1 u p v; \<not> nodes_connected G2 u v\<rbrakk> \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa); is_path_undir G1 u (a # p) v; \<not> nodes_connected G2 u v\<rbrakk> \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
from Cons(2)
[PROOF STATE]
proof (chain)
picking this:
is_path_undir G1 u (a # p) v
[PROOF STEP]
obtain w x y u' where axy: "a=(u,w,u')" and 2: "(x=u \<and> y=u') \<or> (x=u' \<and> y=u)" and e': "is_path_undir G1 u' p v"
      and uwE1: "(x,w,y) \<in> edges G1"
[PROOF STATE]
proof (prove)
using this:
is_path_undir G1 u (a # p) v

goal (1 subgoal):
 1. (\<And>w u' x y. \<lbrakk>a = (u, w, u'); x = u \<and> y = u' \<or> x = u' \<and> y = u; is_path_undir G1 u' p v; (x, w, y) \<in> edges G1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply(cases a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b c. \<lbrakk>\<And>w u' x y. \<lbrakk>a = (u, w, u'); x = u \<and> y = u' \<or> x = u' \<and> y = u; is_path_undir G1 u' p v; (x, w, y) \<in> edges G1\<rbrakk> \<Longrightarrow> thesis; is_path_undir G1 u (a # p) v; a = (aa, b, c)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = (u, w, u')
x = u \<and> y = u' \<or> x = u' \<and> y = u
is_path_undir G1 u' p v
(x, w, y) \<in> edges G1

goal (1 subgoal):
 1. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>is_path_undir G1 u p v; \<not> nodes_connected G2 u v\<rbrakk> \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa); is_path_undir G1 u (a # p) v; \<not> nodes_connected G2 u v\<rbrakk> \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
proof (cases "(x,w,y)\<in>edges G2 \<or> (y,w,x)\<in>edges G2")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (x, w, y) \<in> edges G2 \<or> (y, w, x) \<in> edges G2 \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
 2. \<not> ((x, w, y) \<in> edges G2 \<or> (y, w, x) \<in> edges G2) \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
(x, w, y) \<in> edges G2 \<or> (y, w, x) \<in> edges G2

goal (2 subgoals):
 1. (x, w, y) \<in> edges G2 \<or> (y, w, x) \<in> edges G2 \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
 2. \<not> ((x, w, y) \<in> edges G2 \<or> (y, w, x) \<in> edges G2) \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
have e2': "~(\<exists>p. is_path_undir G2 u' p v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> nodes_connected G2 u' v
[PROOF STEP]
proof (rule ccontr, clarsimp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. is_path_undir G2 u' p v \<Longrightarrow> False
[PROOF STEP]
fix p2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. is_path_undir G2 u' p v \<Longrightarrow> False
[PROOF STEP]
assume "is_path_undir G2 u' p2 v"
[PROOF STATE]
proof (state)
this:
is_path_undir G2 u' p2 v

goal (1 subgoal):
 1. \<And>p. is_path_undir G2 u' p v \<Longrightarrow> False
[PROOF STEP]
with True axy 2
[PROOF STATE]
proof (chain)
picking this:
(x, w, y) \<in> edges G2 \<or> (y, w, x) \<in> edges G2
a = (u, w, u')
x = u \<and> y = u' \<or> x = u' \<and> y = u
is_path_undir G2 u' p2 v
[PROOF STEP]
have "is_path_undir G2 u (a#p2) v"
[PROOF STATE]
proof (prove)
using this:
(x, w, y) \<in> edges G2 \<or> (y, w, x) \<in> edges G2
a = (u, w, u')
x = u \<and> y = u' \<or> x = u' \<and> y = u
is_path_undir G2 u' p2 v

goal (1 subgoal):
 1. is_path_undir G2 u (a # p2) v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_path_undir G2 u (a # p2) v

goal (1 subgoal):
 1. \<And>p. is_path_undir G2 u' p v \<Longrightarrow> False
[PROOF STEP]
with Cons(3)
[PROOF STATE]
proof (chain)
picking this:
\<not> nodes_connected G2 u v
is_path_undir G2 u (a # p2) v
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> nodes_connected G2 u v
is_path_undir G2 u (a # p2) v

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> nodes_connected G2 u' v

goal (2 subgoals):
 1. (x, w, y) \<in> edges G2 \<or> (y, w, x) \<in> edges G2 \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
 2. \<not> ((x, w, y) \<in> edges G2 \<or> (y, w, x) \<in> edges G2) \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
from Cons(1)[OF e' e2']
[PROOF STATE]
proof (chain)
picking this:
\<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)

goal (1 subgoal):
 1. \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)

goal (1 subgoal):
 1. \<not> ((x, w, y) \<in> edges G2 \<or> (y, w, x) \<in> edges G2) \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> ((x, w, y) \<in> edges G2 \<or> (y, w, x) \<in> edges G2) \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> ((x, w, y) \<in> edges G2 \<or> (y, w, x) \<in> edges G2)

goal (1 subgoal):
 1. \<not> ((x, w, y) \<in> edges G2 \<or> (y, w, x) \<in> edges G2) \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<not> ((x, w, y) \<in> edges G2 \<or> (y, w, x) \<in> edges G2)

goal (1 subgoal):
 1. \<not> ((x, w, y) \<in> edges G2 \<or> (y, w, x) \<in> edges G2) \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
assume e2': "~(\<exists>p. is_path_undir G2 u' p v)"
[PROOF STATE]
proof (state)
this:
\<not> nodes_connected G2 u' v

goal (1 subgoal):
 1. \<not> ((x, w, y) \<in> edges G2 \<or> (y, w, x) \<in> edges G2) \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
from Cons(1)[OF e' e2']
[PROOF STATE]
proof (chain)
picking this:
\<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
have ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)

goal (1 subgoal):
 1. \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)

goal (1 subgoal):
 1. \<not> ((x, w, y) \<in> edges G2 \<or> (y, w, x) \<in> edges G2) \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> nodes_connected G2 u' v \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)

goal (1 subgoal):
 1. \<not> ((x, w, y) \<in> edges G2 \<or> (y, w, x) \<in> edges G2) \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> nodes_connected G2 u' v \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)

goal (1 subgoal):
 1. \<not> ((x, w, y) \<in> edges G2 \<or> (y, w, x) \<in> edges G2) \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<not> nodes_connected G2 u' v \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)

goal (1 subgoal):
 1. \<not> ((x, w, y) \<in> edges G2 \<or> (y, w, x) \<in> edges G2) \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
assume e2': "\<exists>p. is_path_undir G2 u' p v"
[PROOF STATE]
proof (state)
this:
nodes_connected G2 u' v

goal (1 subgoal):
 1. \<not> ((x, w, y) \<in> edges G2 \<or> (y, w, x) \<in> edges G2) \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nodes_connected G2 u' v
[PROOF STEP]
obtain p1 where p1: "is_path_undir G2 u' p1 v"
[PROOF STATE]
proof (prove)
using this:
nodes_connected G2 u' v

goal (1 subgoal):
 1. (\<And>p1. is_path_undir G2 u' p1 v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_path_undir G2 u' p1 v

goal (1 subgoal):
 1. \<not> ((x, w, y) \<in> edges G2 \<or> (y, w, x) \<in> edges G2) \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
from False axy
[PROOF STATE]
proof (chain)
picking this:
\<not> ((x, w, y) \<in> edges G2 \<or> (y, w, x) \<in> edges G2)
a = (u, w, u')
[PROOF STEP]
have "(x, w, y)\<notin>edges G2"
[PROOF STATE]
proof (prove)
using this:
\<not> ((x, w, y) \<in> edges G2 \<or> (y, w, x) \<in> edges G2)
a = (u, w, u')

goal (1 subgoal):
 1. (x, w, y) \<notin> edges G2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, w, y) \<notin> edges G2

goal (1 subgoal):
 1. \<not> ((x, w, y) \<in> edges G2 \<or> (y, w, x) \<in> edges G2) \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(x, w, y) \<notin> edges G2

goal (1 subgoal):
 1. \<not> ((x, w, y) \<in> edges G2 \<or> (y, w, x) \<in> edges G2) \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
have "(u,u') \<notin> {(a, b) |a b. nodes_connected G2 a b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u, u') \<notin> {(a, b) |a b. nodes_connected G2 a b}
[PROOF STEP]
proof(rule ccontr, auto simp add:  )
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. is_path_undir G2 u p u' \<Longrightarrow> False
[PROOF STEP]
fix p2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. is_path_undir G2 u p u' \<Longrightarrow> False
[PROOF STEP]
assume "is_path_undir G2 u p2 u'"
[PROOF STATE]
proof (state)
this:
is_path_undir G2 u p2 u'

goal (1 subgoal):
 1. \<And>p. is_path_undir G2 u p u' \<Longrightarrow> False
[PROOF STEP]
with p1
[PROOF STATE]
proof (chain)
picking this:
is_path_undir G2 u' p1 v
is_path_undir G2 u p2 u'
[PROOF STEP]
have "is_path_undir G2 u (p2@p1) v"
[PROOF STATE]
proof (prove)
using this:
is_path_undir G2 u' p1 v
is_path_undir G2 u p2 u'

goal (1 subgoal):
 1. is_path_undir G2 u (p2 @ p1) v
[PROOF STEP]
using valid_graph.is_path_undir_append[OF valid_subgraph[OF assms(2)]]
[PROOF STATE]
proof (prove)
using this:
is_path_undir G2 u' p1 v
is_path_undir G2 u p2 u'
\<lbrakk>is_path_undir G2 ?v ?p1.0 ?u; is_path_undir G2 ?u ?p2.0 ?w\<rbrakk> \<Longrightarrow> is_path_undir G2 ?v (?p1.0 @ ?p2.0) ?w

goal (1 subgoal):
 1. is_path_undir G2 u (p2 @ p1) v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_path_undir G2 u (p2 @ p1) v

goal (1 subgoal):
 1. \<And>p. is_path_undir G2 u p u' \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_path_undir G2 u (p2 @ p1) v
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
is_path_undir G2 u (p2 @ p1) v

goal (1 subgoal):
 1. False
[PROOF STEP]
using Cons(3)
[PROOF STATE]
proof (prove)
using this:
is_path_undir G2 u (p2 @ p1) v
\<not> nodes_connected G2 u v

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(u, u') \<notin> {(a, b) |a b. nodes_connected G2 a b}

goal (1 subgoal):
 1. \<not> ((x, w, y) \<in> edges G2 \<or> (y, w, x) \<in> edges G2) \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(u, u') \<notin> {(a, b) |a b. nodes_connected G2 a b}

goal (1 subgoal):
 1. \<not> ((x, w, y) \<in> edges G2 \<or> (y, w, x) \<in> edges G2) \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
note uwE1
[PROOF STATE]
proof (state)
this:
(x, w, y) \<in> edges G1

goal (1 subgoal):
 1. \<not> ((x, w, y) \<in> edges G2 \<or> (y, w, x) \<in> edges G2) \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(x, w, y) \<notin> edges G2
(u, u') \<notin> {(a, b) |a b. nodes_connected G2 a b}
(x, w, y) \<in> edges G1
[PROOF STEP]
have ?thesis
[PROOF STATE]
proof (prove)
using this:
(x, w, y) \<notin> edges G2
(u, u') \<notin> {(a, b) |a b. nodes_connected G2 a b}
(x, w, y) \<in> edges G1

goal (1 subgoal):
 1. \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x, w, y) \<notin> edges G2; (u, u') \<notin> {(a, b) |a b. nodes_connected G2 a b}; (x, w, y) \<in> edges G1\<rbrakk> \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
apply(rule exI[where x="u"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x, w, y) \<notin> edges G2; (u, u') \<notin> {(a, b) |a b. nodes_connected G2 a b}; (x, w, y) \<in> edges G1\<rbrakk> \<Longrightarrow> \<exists>b e. (u, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> u = aa \<and> b = ba \<or> u = ba \<and> b = aa)
[PROOF STEP]
apply(rule exI[where x="u'"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x, w, y) \<notin> edges G2; (u, u') \<notin> {(a, b) |a b. nodes_connected G2 a b}; (x, w, y) \<in> edges G1\<rbrakk> \<Longrightarrow> \<exists>e. (u, u') \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> u = aa \<and> u' = ba \<or> u = ba \<and> u' = aa)
[PROOF STEP]
apply(rule exI[where x="(x,w,y)"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x, w, y) \<notin> edges G2; (u, u') \<notin> {(a, b) |a b. nodes_connected G2 a b}; (x, w, y) \<in> edges G1\<rbrakk> \<Longrightarrow> (u, u') \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> (x, w, y) \<notin> edges G2 \<and> (x, w, y) \<in> edges G1 \<and> (case (x, w, y) of (aa, w, ba) \<Rightarrow> u = aa \<and> u' = ba \<or> u = ba \<and> u' = aa)
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
x = u \<and> y = u' \<or> x = u' \<and> y = u

goal (1 subgoal):
 1. \<lbrakk>(x, w, y) \<notin> edges G2; (u, u') \<notin> {(a, b) |a b. nodes_connected G2 a b}; (x, w, y) \<in> edges G1\<rbrakk> \<Longrightarrow> (u, u') \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> (x, w, y) \<notin> edges G2 \<and> (x, w, y) \<in> edges G1 \<and> (case (x, w, y) of (aa, w, ba) \<Rightarrow> u = aa \<and> u' = ba \<or> u = ba \<and> u' = aa)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)

goal (1 subgoal):
 1. \<not> ((x, w, y) \<in> edges G2 \<or> (y, w, x) \<in> edges G2) \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
nodes_connected G2 u' v \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)

goal (1 subgoal):
 1. \<not> ((x, w, y) \<in> edges G2 \<or> (y, w, x) \<in> edges G2) \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> nodes_connected G2 u' v \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
nodes_connected G2 u' v \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> nodes_connected G2 u' v \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
nodes_connected G2 u' v \<Longrightarrow> \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)

goal (1 subgoal):
 1. \<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected G2 a b} \<and> e \<notin> edges G2 \<and> e \<in> edges G1 \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma  nodes_connected_refl: "a\<in>V \<Longrightarrow> nodes_connected G a a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> V \<Longrightarrow> nodes_connected G a a
[PROOF STEP]
apply(rule exI[where x="[]"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> V \<Longrightarrow> is_path_undir G a [] a
[PROOF STEP]
by auto


[STATEMENT]
lemma assumes sg: "subgraph H G"
  shows connected_VV: "{(x, y) |x y. nodes_connected H x y} \<subseteq> V\<times>V"
    and connected_refl: "refl_on V {(x, y) |x y. nodes_connected H x y}"
    and connected_trans: "trans {(x, y) |x y. nodes_connected H x y}"
    and connected_sym: "sym {(x, y) |x y. nodes_connected H x y}"
    and connected_equiv: "equiv V {(x, y) |x y. nodes_connected H x y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({(x, y) |x y. nodes_connected H x y} \<subseteq> V \<times> V &&& refl_on V {(x, y) |x y. nodes_connected H x y}) &&& trans {(x, y) |x y. nodes_connected H x y} &&& sym {(x, y) |x y. nodes_connected H x y} &&& equiv V {(x, y) |x y. nodes_connected H x y}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. {(x, y) |x y. nodes_connected H x y} \<subseteq> V \<times> V
 2. refl_on V {(x, y) |x y. nodes_connected H x y}
 3. trans {(x, y) |x y. nodes_connected H x y}
 4. sym {(x, y) |x y. nodes_connected H x y}
 5. equiv V {(x, y) |x y. nodes_connected H x y}
[PROOF STEP]
have *: "\<And>R S. Domain R \<subseteq> S \<Longrightarrow> Range R \<subseteq> S \<Longrightarrow> R \<subseteq> S\<times>S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>R S. \<lbrakk>Domain R \<subseteq> S; Range R \<subseteq> S\<rbrakk> \<Longrightarrow> R \<subseteq> S \<times> S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>Domain ?R \<subseteq> ?S; Range ?R \<subseteq> ?S\<rbrakk> \<Longrightarrow> ?R \<subseteq> ?S \<times> ?S

goal (5 subgoals):
 1. {(x, y) |x y. nodes_connected H x y} \<subseteq> V \<times> V
 2. refl_on V {(x, y) |x y. nodes_connected H x y}
 3. trans {(x, y) |x y. nodes_connected H x y}
 4. sym {(x, y) |x y. nodes_connected H x y}
 5. equiv V {(x, y) |x y. nodes_connected H x y}
[PROOF STEP]
from sg
[PROOF STATE]
proof (chain)
picking this:
subgraph H G
[PROOF STEP]
have [simp]: "nodes H = V"
[PROOF STATE]
proof (prove)
using this:
subgraph H G

goal (1 subgoal):
 1. nodes H = V
[PROOF STEP]
by (auto simp: subgraph_def)
[PROOF STATE]
proof (state)
this:
nodes H = V

goal (5 subgoals):
 1. {(x, y) |x y. nodes_connected H x y} \<subseteq> V \<times> V
 2. refl_on V {(x, y) |x y. nodes_connected H x y}
 3. trans {(x, y) |x y. nodes_connected H x y}
 4. sym {(x, y) |x y. nodes_connected H x y}
 5. equiv V {(x, y) |x y. nodes_connected H x y}
[PROOF STEP]
from sg valid_subgraph
[PROOF STATE]
proof (chain)
picking this:
subgraph H G
subgraph ?H G \<Longrightarrow> valid_graph ?H
[PROOF STEP]
have v: "valid_graph H"
[PROOF STATE]
proof (prove)
using this:
subgraph H G
subgraph ?H G \<Longrightarrow> valid_graph ?H

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

goal (5 subgoals):
 1. {(x, y) |x y. nodes_connected H x y} \<subseteq> V \<times> V
 2. refl_on V {(x, y) |x y. nodes_connected H x y}
 3. trans {(x, y) |x y. nodes_connected H x y}
 4. sym {(x, y) |x y. nodes_connected H x y}
 5. equiv V {(x, y) |x y. nodes_connected H x y}
[PROOF STEP]
from valid_graph.Domain_nodes_connected[OF this] valid_graph.Range_nodes_connected[OF this]
[PROOF STATE]
proof (chain)
picking this:
Domain {(x, y) |x y. nodes_connected H x y} = nodes H
Range {(x, y) |x y. nodes_connected H x y} = nodes H
[PROOF STEP]
show i: "{(x, y) |x y. nodes_connected H x y} \<subseteq> V\<times>V"
[PROOF STATE]
proof (prove)
using this:
Domain {(x, y) |x y. nodes_connected H x y} = nodes H
Range {(x, y) |x y. nodes_connected H x y} = nodes H

goal (1 subgoal):
 1. {(x, y) |x y. nodes_connected H x y} \<subseteq> V \<times> V
[PROOF STEP]
apply(intro *)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Domain {(x, y) |x y. nodes_connected H x y} = nodes H; Range {(x, y) |x y. nodes_connected H x y} = nodes H\<rbrakk> \<Longrightarrow> Domain {(x, y) |x y. nodes_connected H x y} \<subseteq> V
 2. \<lbrakk>Domain {(x, y) |x y. nodes_connected H x y} = nodes H; Range {(x, y) |x y. nodes_connected H x y} = nodes H\<rbrakk> \<Longrightarrow> Range {(x, y) |x y. nodes_connected H x y} \<subseteq> V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(x, y) |x y. nodes_connected H x y} \<subseteq> V \<times> V

goal (4 subgoals):
 1. refl_on V {(x, y) |x y. nodes_connected H x y}
 2. trans {(x, y) |x y. nodes_connected H x y}
 3. sym {(x, y) |x y. nodes_connected H x y}
 4. equiv V {(x, y) |x y. nodes_connected H x y}
[PROOF STEP]
have ii: "\<And>x. x \<in> V \<Longrightarrow> (x, x) \<in> {(x, y) |x y. nodes_connected H x y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> V \<Longrightarrow> (x, x) \<in> {(x, y) |x y. nodes_connected H x y}
[PROOF STEP]
using valid_graph.nodes_connected_refl[OF v]
[PROOF STATE]
proof (prove)
using this:
?a \<in> nodes H \<Longrightarrow> nodes_connected H ?a ?a

goal (1 subgoal):
 1. \<And>x. x \<in> V \<Longrightarrow> (x, x) \<in> {(x, y) |x y. nodes_connected H x y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x1 \<in> V \<Longrightarrow> (?x1, ?x1) \<in> {(x, y) |x y. nodes_connected H x y}

goal (4 subgoals):
 1. refl_on V {(x, y) |x y. nodes_connected H x y}
 2. trans {(x, y) |x y. nodes_connected H x y}
 3. sym {(x, y) |x y. nodes_connected H x y}
 4. equiv V {(x, y) |x y. nodes_connected H x y}
[PROOF STEP]
show "refl_on V {(x, y) |x y. nodes_connected H x y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. refl_on V {(x, y) |x y. nodes_connected H x y}
[PROOF STEP]
apply(rule refl_onI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {(x, y) |x y. nodes_connected H x y} \<subseteq> V \<times> V
 2. \<And>x. x \<in> V \<Longrightarrow> (x, x) \<in> {(x, y) |x y. nodes_connected H x y}
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
refl_on V {(x, y) |x y. nodes_connected H x y}

goal (3 subgoals):
 1. trans {(x, y) |x y. nodes_connected H x y}
 2. sym {(x, y) |x y. nodes_connected H x y}
 3. equiv V {(x, y) |x y. nodes_connected H x y}
[PROOF STEP]
from valid_graph.is_path_undir_append[OF v]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>is_path_undir H ?v ?p1.0 ?u; is_path_undir H ?u ?p2.0 ?w\<rbrakk> \<Longrightarrow> is_path_undir H ?v (?p1.0 @ ?p2.0) ?w
[PROOF STEP]
show "trans {(x, y) |x y. nodes_connected H x y}"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_path_undir H ?v ?p1.0 ?u; is_path_undir H ?u ?p2.0 ?w\<rbrakk> \<Longrightarrow> is_path_undir H ?v (?p1.0 @ ?p2.0) ?w

goal (1 subgoal):
 1. trans {(x, y) |x y. nodes_connected H x y}
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_path_undir H ?v ?p1.0 ?u; is_path_undir H ?u ?p2.0 ?w\<rbrakk> \<Longrightarrow> is_path_undir H ?v (?p1.0 @ ?p2.0) ?w

goal (1 subgoal):
 1. \<forall>x y z. (x, y) \<in> {(x, y) |x y. nodes_connected H x y} \<longrightarrow> (y, z) \<in> {(x, y) |x y. nodes_connected H x y} \<longrightarrow> (x, z) \<in> {(x, y) |x y. nodes_connected H x y}
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
trans {(x, y) |x y. nodes_connected H x y}

goal (2 subgoals):
 1. sym {(x, y) |x y. nodes_connected H x y}
 2. equiv V {(x, y) |x y. nodes_connected H x y}
[PROOF STEP]
from valid_graph.nodes_connected_sym[OF v]
[PROOF STATE]
proof (chain)
picking this:
nodes_connected H ?a ?b = nodes_connected H ?b ?a
[PROOF STEP]
show "sym {(x, y) |x y. nodes_connected H x y}"
[PROOF STATE]
proof (prove)
using this:
nodes_connected H ?a ?b = nodes_connected H ?b ?a

goal (1 subgoal):
 1. sym {(x, y) |x y. nodes_connected H x y}
[PROOF STEP]
unfolding sym_def
[PROOF STATE]
proof (prove)
using this:
nodes_connected H ?a ?b = nodes_connected H ?b ?a

goal (1 subgoal):
 1. \<forall>x y. (x, y) \<in> {(x, y) |x y. nodes_connected H x y} \<longrightarrow> (y, x) \<in> {(x, y) |x y. nodes_connected H x y}
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
sym {(x, y) |x y. nodes_connected H x y}

goal (1 subgoal):
 1. equiv V {(x, y) |x y. nodes_connected H x y}
[PROOF STEP]
show "equiv V {(x, y) |x y. nodes_connected H x y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equiv V {(x, y) |x y. nodes_connected H x y}
[PROOF STEP]
apply (rule equivI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. refl_on V {(x, y) |x y. nodes_connected H x y}
 2. sym {(x, y) |x y. nodes_connected H x y}
 3. trans {(x, y) |x y. nodes_connected H x y}
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
equiv V {(x, y) |x y. nodes_connected H x y}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma  forest_maximally_connected_incl_max1:
  assumes
    "forest H"
    "subgraph H G"
  shows "(\<forall>(a,w,b)\<in>edges G - edges H. \<not> (forest (add_edge a w b H))) \<Longrightarrow> maximally_connected H G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(a, w, b)\<in>E - edges H. \<not> forest (add_edge a w b H) \<Longrightarrow> maximally_connected H G
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>(a, w, b)\<in>E - edges H. \<not> forest (add_edge a w b H) \<Longrightarrow> maximally_connected H G
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
subgraph H G
[PROOF STEP]
have V[simp]: "nodes H = nodes G"
[PROOF STATE]
proof (prove)
using this:
subgraph H G

goal (1 subgoal):
 1. nodes H = V
[PROOF STEP]
unfolding subgraph_def
[PROOF STATE]
proof (prove)
using this:
nodes H = V \<and> edges H \<subseteq> E

goal (1 subgoal):
 1. nodes H = V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nodes H = V

goal (1 subgoal):
 1. \<forall>(a, w, b)\<in>E - edges H. \<not> forest (add_edge a w b H) \<Longrightarrow> maximally_connected H G
[PROOF STEP]
assume pff: "(\<forall>(a,w,b)\<in>E - edges H. \<not> (forest (add_edge a w b H)))"
[PROOF STATE]
proof (state)
this:
\<forall>(a, w, b)\<in>E - edges H. \<not> forest (add_edge a w b H)

goal (1 subgoal):
 1. \<forall>(a, w, b)\<in>E - edges H. \<not> forest (add_edge a w b H) \<Longrightarrow> maximally_connected H G
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>(a, w, b)\<in>E - edges H. \<not> forest (add_edge a w b H)

goal (1 subgoal):
 1. \<forall>(a, w, b)\<in>E - edges H. \<not> forest (add_edge a w b H) \<Longrightarrow> maximally_connected H G
[PROOF STEP]
fix u v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>(a, w, b)\<in>E - edges H. \<not> forest (add_edge a w b H) \<Longrightarrow> maximally_connected H G
[PROOF STEP]
assume uv: "v\<in>V" "u\<in>V"
[PROOF STATE]
proof (state)
this:
v \<in> V
u \<in> V

goal (1 subgoal):
 1. \<forall>(a, w, b)\<in>E - edges H. \<not> forest (add_edge a w b H) \<Longrightarrow> maximally_connected H G
[PROOF STEP]
assume "nodes_connected G u v"
[PROOF STATE]
proof (state)
this:
nodes_connected G u v

goal (1 subgoal):
 1. \<forall>(a, w, b)\<in>E - edges H. \<not> forest (add_edge a w b H) \<Longrightarrow> maximally_connected H G
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nodes_connected G u v
[PROOF STEP]
have i: "(u, v) \<in> {(a, b) |a b. nodes_connected G a b}"
[PROOF STATE]
proof (prove)
using this:
nodes_connected G u v

goal (1 subgoal):
 1. (u, v) \<in> {(a, b) |a b. nodes_connected G a b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(u, v) \<in> {(a, b) |a b. nodes_connected G a b}

goal (1 subgoal):
 1. \<forall>(a, w, b)\<in>E - edges H. \<not> forest (add_edge a w b H) \<Longrightarrow> maximally_connected H G
[PROOF STEP]
have "nodes_connected H u v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nodes_connected H u v
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> nodes_connected H u v \<Longrightarrow> False
[PROOF STEP]
assume "\<not>nodes_connected H u v"
[PROOF STATE]
proof (state)
this:
\<not> nodes_connected H u v

goal (1 subgoal):
 1. \<not> nodes_connected H u v \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> nodes_connected H u v
[PROOF STEP]
have ii: "(u, v) \<notin> {(a, b) |a b. nodes_connected H a b}"
[PROOF STATE]
proof (prove)
using this:
\<not> nodes_connected H u v

goal (1 subgoal):
 1. (u, v) \<notin> {(a, b) |a b. nodes_connected H a b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(u, v) \<notin> {(a, b) |a b. nodes_connected H a b}

goal (1 subgoal):
 1. \<not> nodes_connected H u v \<Longrightarrow> False
[PROOF STEP]
have "subgraph G G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgraph G G
[PROOF STEP]
by(auto simp: subgraph_def)
[PROOF STATE]
proof (state)
this:
subgraph G G

goal (1 subgoal):
 1. \<not> nodes_connected H u v \<Longrightarrow> False
[PROOF STEP]
from augment_edge[OF this assms(2) i ii]
[PROOF STATE]
proof (chain)
picking this:
\<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected H a b} \<and> e \<notin> edges H \<and> e \<in> E \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)
[PROOF STEP]
obtain e a b where
         k: "(a, b) \<notin> {(a, b) |a b. nodes_connected H a b}"
        and nn: "e \<notin> edges H" "e \<in> E" and ee: "(case e of (aa, w, ba) \<Rightarrow> a=aa \<and> b=ba \<or> a=ba \<and> b=aa) "
[PROOF STATE]
proof (prove)
using this:
\<exists>a b e. (a, b) \<notin> {(a, b) |a b. nodes_connected H a b} \<and> e \<notin> edges H \<and> e \<in> E \<and> (case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa)

goal (1 subgoal):
 1. (\<And>a b e. \<lbrakk>(a, b) \<notin> {(a, b) |a b. nodes_connected H a b}; e \<notin> edges H; e \<in> E; case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(a, b) \<notin> {(a, b) |a b. nodes_connected H a b}
e \<notin> edges H
e \<in> E
case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa

goal (1 subgoal):
 1. \<not> nodes_connected H u v \<Longrightarrow> False
[PROOF STEP]
obtain x w y where e: "e=(x,w,y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x w y. e = (x, w, y) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply(cases e)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>\<And>x w y. e = (x, w, y) \<Longrightarrow> thesis; e = (a, b, c)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
e = (x, w, y)

goal (1 subgoal):
 1. \<not> nodes_connected H u v \<Longrightarrow> False
[PROOF STEP]
from e ee
[PROOF STATE]
proof (chain)
picking this:
e = (x, w, y)
case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa
[PROOF STEP]
have "x=a \<and> y=b \<or> x=b \<and> y=a"
[PROOF STATE]
proof (prove)
using this:
e = (x, w, y)
case e of (aa, w, ba) \<Rightarrow> a = aa \<and> b = ba \<or> a = ba \<and> b = aa

goal (1 subgoal):
 1. x = a \<and> y = b \<or> x = b \<and> y = a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = a \<and> y = b \<or> x = b \<and> y = a

goal (1 subgoal):
 1. \<not> nodes_connected H u v \<Longrightarrow> False
[PROOF STEP]
with k
[PROOF STATE]
proof (chain)
picking this:
(a, b) \<notin> {(a, b) |a b. nodes_connected H a b}
x = a \<and> y = b \<or> x = b \<and> y = a
[PROOF STEP]
have k': "\<not> nodes_connected H x y"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<notin> {(a, b) |a b. nodes_connected H a b}
x = a \<and> y = b \<or> x = b \<and> y = a

goal (1 subgoal):
 1. \<not> nodes_connected H x y
[PROOF STEP]
using valid_graph.nodes_connected_sym[OF valid_subgraph[OF assms(2)]]
[PROOF STATE]
proof (prove)
using this:
(a, b) \<notin> {(a, b) |a b. nodes_connected H a b}
x = a \<and> y = b \<or> x = b \<and> y = a
nodes_connected H ?a ?b = nodes_connected H ?b ?a

goal (1 subgoal):
 1. \<not> nodes_connected H x y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> nodes_connected H x y

goal (1 subgoal):
 1. \<not> nodes_connected H u v \<Longrightarrow> False
[PROOF STEP]
have xy: "x\<in>V" "y\<in>V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> V &&& y \<in> V
[PROOF STEP]
using e nn(2)
[PROOF STATE]
proof (prove)
using this:
e = (x, w, y)
e \<in> E

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

goal (1 subgoal):
 1. \<not> nodes_connected H u v \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> V
y \<in> V
[PROOF STEP]
have nxy: "x\<in>nodes H"  "y\<in>nodes H"
[PROOF STATE]
proof (prove)
using this:
x \<in> V
y \<in> V

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

goal (1 subgoal):
 1. \<not> nodes_connected H u v \<Longrightarrow> False
[PROOF STEP]
from forest.forest_add_edge[OF assms(1) nxy k' ]
[PROOF STATE]
proof (chain)
picking this:
forest (add_edge x ?w y H)
[PROOF STEP]
have
        "forest (add_edge x w y H)"
[PROOF STATE]
proof (prove)
using this:
forest (add_edge x ?w y H)

goal (1 subgoal):
 1. forest (add_edge x w y H)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
forest (add_edge x w y H)

goal (1 subgoal):
 1. \<not> nodes_connected H u v \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
forest (add_edge x w y H)

goal (1 subgoal):
 1. \<not> nodes_connected H u v \<Longrightarrow> False
[PROOF STEP]
have "(x,w,y)\<in>E-edges H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, w, y) \<in> E - edges H
[PROOF STEP]
using nn e
[PROOF STATE]
proof (prove)
using this:
e \<notin> edges H
e \<in> E
e = (x, w, y)

goal (1 subgoal):
 1. (x, w, y) \<in> E - edges H
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, w, y) \<in> E - edges H

goal (1 subgoal):
 1. \<not> nodes_connected H u v \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
forest (add_edge x w y H)
(x, w, y) \<in> E - edges H
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
forest (add_edge x w y H)
(x, w, y) \<in> E - edges H

goal (1 subgoal):
 1. False
[PROOF STEP]
using pff
[PROOF STATE]
proof (prove)
using this:
forest (add_edge x w y H)
(x, w, y) \<in> E - edges H
\<forall>(a, w, b)\<in>E - edges H. \<not> forest (add_edge a w b H)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
nodes_connected H u v

goal (1 subgoal):
 1. \<forall>(a, w, b)\<in>E - edges H. \<not> forest (add_edge a w b H) \<Longrightarrow> maximally_connected H G
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?v2 \<in> V; ?u2 \<in> V; nodes_connected G ?u2 ?v2\<rbrakk> \<Longrightarrow> nodes_connected H ?u2 ?v2

goal (1 subgoal):
 1. \<forall>(a, w, b)\<in>E - edges H. \<not> forest (add_edge a w b H) \<Longrightarrow> maximally_connected H G
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?v2 \<in> V; ?u2 \<in> V; nodes_connected G ?u2 ?v2\<rbrakk> \<Longrightarrow> nodes_connected H ?u2 ?v2
[PROOF STEP]
show "maximally_connected H G"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?v2 \<in> V; ?u2 \<in> V; nodes_connected G ?u2 ?v2\<rbrakk> \<Longrightarrow> nodes_connected H ?u2 ?v2

goal (1 subgoal):
 1. maximally_connected H G
[PROOF STEP]
unfolding maximally_connected_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?v2 \<in> V; ?u2 \<in> V; nodes_connected G ?u2 ?v2\<rbrakk> \<Longrightarrow> nodes_connected H ?u2 ?v2

goal (1 subgoal):
 1. \<forall>v\<in>V. \<forall>v'\<in>V. nodes_connected G v v' \<longrightarrow> nodes_connected H v v'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
maximally_connected H G

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma   forest_maximally_connected_incl_max2:
  assumes
    "forest H"
    "subgraph H G"
  shows "maximally_connected H G \<Longrightarrow> (\<forall>(a,w,b)\<in>E - edges H. \<not> (forest (add_edge a w b H)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maximally_connected H G \<Longrightarrow> \<forall>(a, w, b)\<in>E - edges H. \<not> forest (add_edge a w b H)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. maximally_connected H G \<Longrightarrow> \<forall>(a, w, b)\<in>E - edges H. \<not> forest (add_edge a w b H)
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
subgraph H G
[PROOF STEP]
have V[simp]: "nodes H = nodes G"
[PROOF STATE]
proof (prove)
using this:
subgraph H G

goal (1 subgoal):
 1. nodes H = V
[PROOF STEP]
unfolding subgraph_def
[PROOF STATE]
proof (prove)
using this:
nodes H = V \<and> edges H \<subseteq> E

goal (1 subgoal):
 1. nodes H = V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nodes H = V

goal (1 subgoal):
 1. maximally_connected H G \<Longrightarrow> \<forall>(a, w, b)\<in>E - edges H. \<not> forest (add_edge a w b H)
[PROOF STEP]
assume mc: "maximally_connected H G"
[PROOF STATE]
proof (state)
this:
maximally_connected H G

goal (1 subgoal):
 1. maximally_connected H G \<Longrightarrow> \<forall>(a, w, b)\<in>E - edges H. \<not> forest (add_edge a w b H)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
maximally_connected H G
[PROOF STEP]
have k: "\<And>v v'. v\<in>V \<Longrightarrow>  v'\<in>V \<Longrightarrow>
          nodes_connected G v v' \<Longrightarrow> nodes_connected H v v'"
[PROOF STATE]
proof (prove)
using this:
maximally_connected H G

goal (1 subgoal):
 1. \<And>v v'. \<lbrakk>v \<in> V; v' \<in> V; nodes_connected G v v'\<rbrakk> \<Longrightarrow> nodes_connected H v v'
[PROOF STEP]
unfolding maximally_connected_def
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>V. \<forall>v'\<in>V. nodes_connected G v v' \<longrightarrow> nodes_connected H v v'

goal (1 subgoal):
 1. \<And>v v'. \<lbrakk>v \<in> V; v' \<in> V; nodes_connected G v v'\<rbrakk> \<Longrightarrow> nodes_connected H v v'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?v \<in> V; ?v' \<in> V; nodes_connected G ?v ?v'\<rbrakk> \<Longrightarrow> nodes_connected H ?v ?v'

goal (1 subgoal):
 1. maximally_connected H G \<Longrightarrow> \<forall>(a, w, b)\<in>E - edges H. \<not> forest (add_edge a w b H)
[PROOF STEP]
show "(\<forall>(a,w,b)\<in>E - edges H. \<not> (forest (add_edge a w b H)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(a, w, b)\<in>E - edges H. \<not> forest (add_edge a w b H)
[PROOF STEP]
proof (safe)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>(a, aa, b) \<in> E; (a, aa, b) \<notin> edges H; forest (add_edge a aa b H)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix x w y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>(a, aa, b) \<in> E; (a, aa, b) \<notin> edges H; forest (add_edge a aa b H)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume i: "(x, w, y) \<in> E" and ni: "(x, w, y) \<notin> edges H"
      and f: "forest (add_edge x w y H)"
[PROOF STATE]
proof (state)
this:
(x, w, y) \<in> E
(x, w, y) \<notin> edges H
forest (add_edge x w y H)

goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>(a, aa, b) \<in> E; (a, aa, b) \<notin> edges H; forest (add_edge a aa b H)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from i
[PROOF STATE]
proof (chain)
picking this:
(x, w, y) \<in> E
[PROOF STEP]
have xy: "x\<in>V" "y\<in>V"
[PROOF STATE]
proof (prove)
using this:
(x, w, y) \<in> E

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

goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>(a, aa, b) \<in> E; (a, aa, b) \<notin> edges H; forest (add_edge a aa b H)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from f
[PROOF STATE]
proof (chain)
picking this:
forest (add_edge x w y H)
[PROOF STEP]
have "\<forall>(a,wa,b)\<in>insert (x, w, y) (edges H). \<not> nodes_connected (delete_edge a wa b (add_edge x w y H)) a b"
[PROOF STATE]
proof (prove)
using this:
forest (add_edge x w y H)

goal (1 subgoal):
 1. \<forall>(a, wa, b)\<in>insert (x, w, y) (edges H). \<not> nodes_connected (delete_edge a wa b (add_edge x w y H)) a b
[PROOF STEP]
unfolding forest_def forest_axioms_def
[PROOF STATE]
proof (prove)
using this:
valid_graph (add_edge x w y H) \<and> (\<forall>(a, wa, b)\<in>edges (add_edge x w y H). \<not> nodes_connected (delete_edge a wa b (add_edge x w y H)) a b)

goal (1 subgoal):
 1. \<forall>(a, wa, b)\<in>insert (x, w, y) (edges H). \<not> nodes_connected (delete_edge a wa b (add_edge x w y H)) a b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>(a, wa, b)\<in>insert (x, w, y) (edges H). \<not> nodes_connected (delete_edge a wa b (add_edge x w y H)) a b

goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>(a, aa, b) \<in> E; (a, aa, b) \<notin> edges H; forest (add_edge a aa b H)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>(a, wa, b)\<in>insert (x, w, y) (edges H). \<not> nodes_connected (delete_edge a wa b (add_edge x w y H)) a b
[PROOF STEP]
have "\<not> nodes_connected (delete_edge x w y (add_edge x w y H)) x y"
[PROOF STATE]
proof (prove)
using this:
\<forall>(a, wa, b)\<in>insert (x, w, y) (edges H). \<not> nodes_connected (delete_edge a wa b (add_edge x w y H)) a b

goal (1 subgoal):
 1. \<not> nodes_connected (delete_edge x w y (add_edge x w y H)) x y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> nodes_connected (delete_edge x w y (add_edge x w y H)) x y

goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>(a, aa, b) \<in> E; (a, aa, b) \<notin> edges H; forest (add_edge a aa b H)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> nodes_connected (delete_edge x w y (add_edge x w y H)) x y

goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>(a, aa, b) \<in> E; (a, aa, b) \<notin> edges H; forest (add_edge a aa b H)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "(delete_edge x w y (add_edge x w y H)) = H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delete_edge x w y (add_edge x w y H) = H
[PROOF STEP]
using ni xy
[PROOF STATE]
proof (prove)
using this:
(x, w, y) \<notin> edges H
x \<in> V
y \<in> V

goal (1 subgoal):
 1. delete_edge x w y (add_edge x w y H) = H
[PROOF STEP]
by(auto simp: add_edge_def delete_edge_def insert_absorb)
[PROOF STATE]
proof (state)
this:
delete_edge x w y (add_edge x w y H) = H

goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>(a, aa, b) \<in> E; (a, aa, b) \<notin> edges H; forest (add_edge a aa b H)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> nodes_connected (delete_edge x w y (add_edge x w y H)) x y
delete_edge x w y (add_edge x w y H) = H
[PROOF STEP]
have "\<not> nodes_connected H x y"
[PROOF STATE]
proof (prove)
using this:
\<not> nodes_connected (delete_edge x w y (add_edge x w y H)) x y
delete_edge x w y (add_edge x w y H) = H

goal (1 subgoal):
 1. \<not> nodes_connected H x y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> nodes_connected H x y

goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>(a, aa, b) \<in> E; (a, aa, b) \<notin> edges H; forest (add_edge a aa b H)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> nodes_connected H x y

goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>(a, aa, b) \<in> E; (a, aa, b) \<notin> edges H; forest (add_edge a aa b H)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from i
[PROOF STATE]
proof (chain)
picking this:
(x, w, y) \<in> E
[PROOF STEP]
have "nodes_connected G x y"
[PROOF STATE]
proof (prove)
using this:
(x, w, y) \<in> E

goal (1 subgoal):
 1. nodes_connected G x y
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, w, y) \<in> E \<Longrightarrow> nodes_connected G x y
[PROOF STEP]
apply(rule exI[where x="[(x,w,y)]"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, w, y) \<in> E \<Longrightarrow> is_path_undir G x [(x, w, y)] y
[PROOF STEP]
by (auto dest: E_validD)
[PROOF STATE]
proof (state)
this:
nodes_connected G x y

goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>(a, aa, b) \<in> E; (a, aa, b) \<notin> edges H; forest (add_edge a aa b H)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> nodes_connected H x y
nodes_connected G x y
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
\<not> nodes_connected H x y
nodes_connected G x y

goal (1 subgoal):
 1. False
[PROOF STEP]
using k[OF xy]
[PROOF STATE]
proof (prove)
using this:
\<not> nodes_connected H x y
nodes_connected G x y
nodes_connected G x y \<Longrightarrow> nodes_connected H x y

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>(a, w, b)\<in>E - edges H. \<not> forest (add_edge a w b H)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma  forest_maximally_connected_incl_max_conv:
  assumes
    "forest H"
    "subgraph H G"
  shows "maximally_connected H G = (\<forall>(a,w,b)\<in>E - edges H. \<not> (forest (add_edge a w b H)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maximally_connected H G = (\<forall>(a, w, b)\<in>E - edges H. \<not> forest (add_edge a w b H))
[PROOF STEP]
using assms forest_maximally_connected_incl_max2 forest_maximally_connected_incl_max1
[PROOF STATE]
proof (prove)
using this:
forest H
subgraph H G
\<lbrakk>forest ?H; subgraph ?H G; maximally_connected ?H G\<rbrakk> \<Longrightarrow> \<forall>(a, w, b)\<in>E - edges ?H. \<not> forest (add_edge a w b ?H)
\<lbrakk>forest ?H; subgraph ?H G; \<forall>(a, w, b)\<in>E - edges ?H. \<not> forest (add_edge a w b ?H)\<rbrakk> \<Longrightarrow> maximally_connected ?H G

goal (1 subgoal):
 1. maximally_connected H G = (\<forall>(a, w, b)\<in>E - edges H. \<not> forest (add_edge a w b H))
[PROOF STEP]
by blast


[STATEMENT]
lemma
  rel_chain_Nil: "rel_chain [] r" and
  rel_chain_Cons: "rel_chain (x # xs) r = (if xs = [] then True else ((x, hd xs) \<in> r) \<and> rel_chain xs r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_chain [] r &&& rel_chain (x # xs) r = (if xs = [] then True else (x, hd xs) \<in> r \<and> rel_chain xs r)
[PROOF STEP]
by (auto simp add: rel_chain_def hd_conv_nth nth_Cons split: nat.split_asm nat.split)


[STATEMENT]
lemma rel_chain_drop:
  "rel_chain l R ==> rel_chain (drop n l) R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_chain l R \<Longrightarrow> rel_chain (drop n l) R
[PROOF STEP]
unfolding rel_chain_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k<length l - 1. (l ! k, l ! (k + 1)) \<in> R \<Longrightarrow> \<forall>k<length (drop n l) - 1. (drop n l ! k, drop n l ! (k + 1)) \<in> R
[PROOF STEP]
by simp


[STATEMENT]
lemma rel_chain_take:
  "rel_chain l R ==> rel_chain (take n l) R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_chain l R \<Longrightarrow> rel_chain (take n l) R
[PROOF STEP]
unfolding rel_chain_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k<length l - 1. (l ! k, l ! (k + 1)) \<in> R \<Longrightarrow> \<forall>k<length (take n l) - 1. (take n l ! k, take n l ! (k + 1)) \<in> R
[PROOF STEP]
by simp


[STATEMENT]
lemma rel_chain_butlast:
  "rel_chain l R ==> rel_chain (butlast l) R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_chain l R \<Longrightarrow> rel_chain (butlast l) R
[PROOF STEP]
unfolding rel_chain_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k<length l - 1. (l ! k, l ! (k + 1)) \<in> R \<Longrightarrow> \<forall>k<length (butlast l) - 1. (butlast l ! k, butlast l ! (k + 1)) \<in> R
[PROOF STEP]
by (auto simp add: butlast_nth)


[STATEMENT]
lemma rel_chain_tl:
  "rel_chain l R ==> rel_chain (tl l) R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_chain l R \<Longrightarrow> rel_chain (tl l) R
[PROOF STEP]
unfolding rel_chain_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k<length l - 1. (l ! k, l ! (k + 1)) \<in> R \<Longrightarrow> \<forall>k<length (tl l) - 1. (tl l ! k, tl l ! (k + 1)) \<in> R
[PROOF STEP]
by (cases "l = []") (auto simp add: tl_nth)


[STATEMENT]
lemma rel_chain_append:
  assumes "rel_chain l R" "rel_chain l' R" "(last l, hd l') \<in> R"
  shows "rel_chain (l @ l') R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_chain (l @ l') R
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
rel_chain l R
rel_chain l' R
(last l, hd l') \<in> R

goal (1 subgoal):
 1. rel_chain (l @ l') R
[PROOF STEP]
by (induct l) (auto simp add: rel_chain_Cons split: if_splits)


[STATEMENT]
lemma rel_chain_appendD:
  assumes "rel_chain (l @ l') R"
  shows "rel_chain l R" "rel_chain l' R" "l \<noteq> [] \<and> l' \<noteq> [] \<longrightarrow> (last l, hd l') \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_chain l R &&& rel_chain l' R &&& l \<noteq> [] \<and> l' \<noteq> [] \<longrightarrow> (last l, hd l') \<in> R
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
rel_chain (l @ l') R

goal (1 subgoal):
 1. rel_chain l R &&& rel_chain l' R &&& l \<noteq> [] \<and> l' \<noteq> [] \<longrightarrow> (last l, hd l') \<in> R
[PROOF STEP]
by (induct l) (auto simp add: rel_chain_Cons rel_chain_Nil split: if_splits)


[STATEMENT]
lemma rtrancl_rel_chain:
  "(x, y) \<in> R\<^sup>* \<longleftrightarrow> (\<exists> l. l \<noteq> [] \<and> hd l = x \<and> last l = y \<and> rel_chain l R)"
  (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x, y) \<in> R\<^sup>*) = (\<exists>l. l \<noteq> [] \<and> hd l = x \<and> last l = y \<and> rel_chain l R)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (x, y) \<in> R\<^sup>* \<Longrightarrow> \<exists>l. l \<noteq> [] \<and> hd l = x \<and> last l = y \<and> rel_chain l R
 2. \<exists>l. l \<noteq> [] \<and> hd l = x \<and> last l = y \<and> rel_chain l R \<Longrightarrow> (x, y) \<in> R\<^sup>*
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
(x, y) \<in> R\<^sup>*

goal (2 subgoals):
 1. (x, y) \<in> R\<^sup>* \<Longrightarrow> \<exists>l. l \<noteq> [] \<and> hd l = x \<and> last l = y \<and> rel_chain l R
 2. \<exists>l. l \<noteq> [] \<and> hd l = x \<and> last l = y \<and> rel_chain l R \<Longrightarrow> (x, y) \<in> R\<^sup>*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> R\<^sup>*
[PROOF STEP]
show ?rhs
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> R\<^sup>*

goal (1 subgoal):
 1. \<exists>l. l \<noteq> [] \<and> hd l = x \<and> last l = y \<and> rel_chain l R
[PROOF STEP]
by (induct rule: converse_rtrancl_induct) (auto simp add: rel_chain_Cons)
[PROOF STATE]
proof (state)
this:
\<exists>l. l \<noteq> [] \<and> hd l = x \<and> last l = y \<and> rel_chain l R

goal (1 subgoal):
 1. \<exists>l. l \<noteq> [] \<and> hd l = x \<and> last l = y \<and> rel_chain l R \<Longrightarrow> (x, y) \<in> R\<^sup>*
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>l. l \<noteq> [] \<and> hd l = x \<and> last l = y \<and> rel_chain l R \<Longrightarrow> (x, y) \<in> R\<^sup>*
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
\<exists>l. l \<noteq> [] \<and> hd l = x \<and> last l = y \<and> rel_chain l R

goal (1 subgoal):
 1. \<exists>l. l \<noteq> [] \<and> hd l = x \<and> last l = y \<and> rel_chain l R \<Longrightarrow> (x, y) \<in> R\<^sup>*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l. l \<noteq> [] \<and> hd l = x \<and> last l = y \<and> rel_chain l R
[PROOF STEP]
obtain l where "l \<noteq> []" "hd l = x" "last l = y" "rel_chain l R"
[PROOF STATE]
proof (prove)
using this:
\<exists>l. l \<noteq> [] \<and> hd l = x \<and> last l = y \<and> rel_chain l R

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>l \<noteq> []; hd l = x; last l = y; rel_chain l R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l \<noteq> []
hd l = x
last l = y
rel_chain l R

goal (1 subgoal):
 1. \<exists>l. l \<noteq> [] \<and> hd l = x \<and> last l = y \<and> rel_chain l R \<Longrightarrow> (x, y) \<in> R\<^sup>*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l \<noteq> []
hd l = x
last l = y
rel_chain l R
[PROOF STEP]
show ?lhs
[PROOF STATE]
proof (prove)
using this:
l \<noteq> []
hd l = x
last l = y
rel_chain l R

goal (1 subgoal):
 1. (x, y) \<in> R\<^sup>*
[PROOF STEP]
by (induct l arbitrary: x) (auto simp add: rel_chain_Cons, force)
[PROOF STATE]
proof (state)
this:
(x, y) \<in> R\<^sup>*

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma trancl_rel_chain:
  "(x, y) \<in> R\<^sup>+ \<longleftrightarrow> (\<exists> l. l \<noteq> [] \<and> length l > 1 \<and> hd l = x \<and> last l = y \<and> rel_chain l R)" (is "?lhs \<longleftrightarrow> ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x, y) \<in> R\<^sup>+) = (\<exists>l. l \<noteq> [] \<and> 1 < length l \<and> hd l = x \<and> last l = y \<and> rel_chain l R)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (x, y) \<in> R\<^sup>+ \<Longrightarrow> \<exists>l. l \<noteq> [] \<and> 1 < length l \<and> hd l = x \<and> last l = y \<and> rel_chain l R
 2. \<exists>l. l \<noteq> [] \<and> 1 < length l \<and> hd l = x \<and> last l = y \<and> rel_chain l R \<Longrightarrow> (x, y) \<in> R\<^sup>+
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
(x, y) \<in> R\<^sup>+

goal (2 subgoals):
 1. (x, y) \<in> R\<^sup>+ \<Longrightarrow> \<exists>l. l \<noteq> [] \<and> 1 < length l \<and> hd l = x \<and> last l = y \<and> rel_chain l R
 2. \<exists>l. l \<noteq> [] \<and> 1 < length l \<and> hd l = x \<and> last l = y \<and> rel_chain l R \<Longrightarrow> (x, y) \<in> R\<^sup>+
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> R\<^sup>+
[PROOF STEP]
obtain z where "(x, z) \<in> R" "(z, y) \<in> R\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> R\<^sup>+

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>(x, z) \<in> R; (z, y) \<in> R\<^sup>*\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto dest: tranclD)
[PROOF STATE]
proof (state)
this:
(x, z) \<in> R
(z, y) \<in> R\<^sup>*

goal (2 subgoals):
 1. (x, y) \<in> R\<^sup>+ \<Longrightarrow> \<exists>l. l \<noteq> [] \<and> 1 < length l \<and> hd l = x \<and> last l = y \<and> rel_chain l R
 2. \<exists>l. l \<noteq> [] \<and> 1 < length l \<and> hd l = x \<and> last l = y \<and> rel_chain l R \<Longrightarrow> (x, y) \<in> R\<^sup>+
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x, z) \<in> R
(z, y) \<in> R\<^sup>*
[PROOF STEP]
obtain l where  "l \<noteq> [] \<and> hd l = z \<and> last l = y \<and> rel_chain l R"
[PROOF STATE]
proof (prove)
using this:
(x, z) \<in> R
(z, y) \<in> R\<^sup>*

goal (1 subgoal):
 1. (\<And>l. l \<noteq> [] \<and> hd l = z \<and> last l = y \<and> rel_chain l R \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: rtrancl_rel_chain)
[PROOF STATE]
proof (state)
this:
l \<noteq> [] \<and> hd l = z \<and> last l = y \<and> rel_chain l R

goal (2 subgoals):
 1. (x, y) \<in> R\<^sup>+ \<Longrightarrow> \<exists>l. l \<noteq> [] \<and> 1 < length l \<and> hd l = x \<and> last l = y \<and> rel_chain l R
 2. \<exists>l. l \<noteq> [] \<and> 1 < length l \<and> hd l = x \<and> last l = y \<and> rel_chain l R \<Longrightarrow> (x, y) \<in> R\<^sup>+
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l \<noteq> [] \<and> hd l = z \<and> last l = y \<and> rel_chain l R
[PROOF STEP]
show ?rhs
[PROOF STATE]
proof (prove)
using this:
l \<noteq> [] \<and> hd l = z \<and> last l = y \<and> rel_chain l R

goal (1 subgoal):
 1. \<exists>l. l \<noteq> [] \<and> 1 < length l \<and> hd l = x \<and> last l = y \<and> rel_chain l R
[PROOF STEP]
using \<open>(x, z) \<in> R\<close>
[PROOF STATE]
proof (prove)
using this:
l \<noteq> [] \<and> hd l = z \<and> last l = y \<and> rel_chain l R
(x, z) \<in> R

goal (1 subgoal):
 1. \<exists>l. l \<noteq> [] \<and> 1 < length l \<and> hd l = x \<and> last l = y \<and> rel_chain l R
[PROOF STEP]
by (rule_tac x="x # l" in exI) (auto simp add: rel_chain_Cons)
[PROOF STATE]
proof (state)
this:
\<exists>l. l \<noteq> [] \<and> 1 < length l \<and> hd l = x \<and> last l = y \<and> rel_chain l R

goal (1 subgoal):
 1. \<exists>l. l \<noteq> [] \<and> 1 < length l \<and> hd l = x \<and> last l = y \<and> rel_chain l R \<Longrightarrow> (x, y) \<in> R\<^sup>+
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>l. l \<noteq> [] \<and> 1 < length l \<and> hd l = x \<and> last l = y \<and> rel_chain l R \<Longrightarrow> (x, y) \<in> R\<^sup>+
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
\<exists>l. l \<noteq> [] \<and> 1 < length l \<and> hd l = x \<and> last l = y \<and> rel_chain l R

goal (1 subgoal):
 1. \<exists>l. l \<noteq> [] \<and> 1 < length l \<and> hd l = x \<and> last l = y \<and> rel_chain l R \<Longrightarrow> (x, y) \<in> R\<^sup>+
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l. l \<noteq> [] \<and> 1 < length l \<and> hd l = x \<and> last l = y \<and> rel_chain l R
[PROOF STEP]
obtain l where "1 < length l" "l \<noteq> []" "hd l = x" "last l = y" "rel_chain l R"
[PROOF STATE]
proof (prove)
using this:
\<exists>l. l \<noteq> [] \<and> 1 < length l \<and> hd l = x \<and> last l = y \<and> rel_chain l R

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>1 < length l; l \<noteq> []; hd l = x; last l = y; rel_chain l R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 < length l
l \<noteq> []
hd l = x
last l = y
rel_chain l R

goal (1 subgoal):
 1. \<exists>l. l \<noteq> [] \<and> 1 < length l \<and> hd l = x \<and> last l = y \<and> rel_chain l R \<Longrightarrow> (x, y) \<in> R\<^sup>+
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 < length l
l \<noteq> []
hd l = x
last l = y
rel_chain l R
[PROOF STEP]
obtain l' where
    "l' \<noteq> []" "l = x # l'" "(x, hd l') \<in> R" "rel_chain l' R"
[PROOF STATE]
proof (prove)
using this:
1 < length l
l \<noteq> []
hd l = x
last l = y
rel_chain l R

goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>l' \<noteq> []; l = x # l'; (x, hd l') \<in> R; rel_chain l' R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>1 < length l\<close>
[PROOF STATE]
proof (prove)
using this:
1 < length l
l \<noteq> []
hd l = x
last l = y
rel_chain l R
1 < length l

goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>l' \<noteq> []; l = x # l'; (x, hd l') \<in> R; rel_chain l' R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases l) (auto simp add: rel_chain_Cons)
[PROOF STATE]
proof (state)
this:
l' \<noteq> []
l = x # l'
(x, hd l') \<in> R
rel_chain l' R

goal (1 subgoal):
 1. \<exists>l. l \<noteq> [] \<and> 1 < length l \<and> hd l = x \<and> last l = y \<and> rel_chain l R \<Longrightarrow> (x, y) \<in> R\<^sup>+
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l' \<noteq> []
l = x # l'
(x, hd l') \<in> R
rel_chain l' R
[PROOF STEP]
have "(x, hd l') \<in> R" "(hd l', y) \<in> R\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
l' \<noteq> []
l = x # l'
(x, hd l') \<in> R
rel_chain l' R

goal (1 subgoal):
 1. (x, hd l') \<in> R &&& (hd l', y) \<in> R\<^sup>*
[PROOF STEP]
using \<open>last l = y\<close>
[PROOF STATE]
proof (prove)
using this:
l' \<noteq> []
l = x # l'
(x, hd l') \<in> R
rel_chain l' R
last l = y

goal (1 subgoal):
 1. (x, hd l') \<in> R &&& (hd l', y) \<in> R\<^sup>*
[PROOF STEP]
by (auto simp add: rtrancl_rel_chain)
[PROOF STATE]
proof (state)
this:
(x, hd l') \<in> R
(hd l', y) \<in> R\<^sup>*

goal (1 subgoal):
 1. \<exists>l. l \<noteq> [] \<and> 1 < length l \<and> hd l = x \<and> last l = y \<and> rel_chain l R \<Longrightarrow> (x, y) \<in> R\<^sup>+
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x, hd l') \<in> R
(hd l', y) \<in> R\<^sup>*
[PROOF STEP]
show ?lhs
[PROOF STATE]
proof (prove)
using this:
(x, hd l') \<in> R
(hd l', y) \<in> R\<^sup>*

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rel_chain_elems_rtrancl:
  assumes "rel_chain l R" "i \<le> j" "j < length l"
  shows "(l ! i, l ! j) \<in> R\<^sup>*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l ! i, l ! j) \<in> R\<^sup>*
[PROOF STEP]
proof (cases "i = j")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = j \<Longrightarrow> (l ! i, l ! j) \<in> R\<^sup>*
 2. i \<noteq> j \<Longrightarrow> (l ! i, l ! j) \<in> R\<^sup>*
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i = j

goal (2 subgoals):
 1. i = j \<Longrightarrow> (l ! i, l ! j) \<in> R\<^sup>*
 2. i \<noteq> j \<Longrightarrow> (l ! i, l ! j) \<in> R\<^sup>*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i = j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i = j

goal (1 subgoal):
 1. (l ! i, l ! j) \<in> R\<^sup>*
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(l ! i, l ! j) \<in> R\<^sup>*

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (l ! i, l ! j) \<in> R\<^sup>*
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (l ! i, l ! j) \<in> R\<^sup>*
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
i \<noteq> j

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (l ! i, l ! j) \<in> R\<^sup>*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<noteq> j
[PROOF STEP]
have "i < j"
[PROOF STATE]
proof (prove)
using this:
i \<noteq> j

goal (1 subgoal):
 1. i < j
[PROOF STEP]
using \<open>i \<le> j\<close>
[PROOF STATE]
proof (prove)
using this:
i \<noteq> j
i \<le> j

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

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (l ! i, l ! j) \<in> R\<^sup>*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < j
[PROOF STEP]
have "l \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
i < j

goal (1 subgoal):
 1. l \<noteq> []
[PROOF STEP]
using \<open>j < length l\<close>
[PROOF STATE]
proof (prove)
using this:
i < j
j < length l

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

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (l ! i, l ! j) \<in> R\<^sup>*
[PROOF STEP]
let ?l = "drop i (take (j + 1) l)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (l ! i, l ! j) \<in> R\<^sup>*
[PROOF STEP]
have "?l \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop i (take (j + 1) l) \<noteq> []
[PROOF STEP]
using \<open>i < j\<close> \<open>j < length l\<close>
[PROOF STATE]
proof (prove)
using this:
i < j
j < length l

goal (1 subgoal):
 1. drop i (take (j + 1) l) \<noteq> []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
drop i (take (j + 1) l) \<noteq> []

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (l ! i, l ! j) \<in> R\<^sup>*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
drop i (take (j + 1) l) \<noteq> []

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (l ! i, l ! j) \<in> R\<^sup>*
[PROOF STEP]
have "hd ?l = l ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (drop i (take (j + 1) l)) = l ! i
[PROOF STEP]
using \<open>?l \<noteq> []\<close> \<open>i < j\<close>
[PROOF STATE]
proof (prove)
using this:
drop i (take (j + 1) l) \<noteq> []
i < j

goal (1 subgoal):
 1. hd (drop i (take (j + 1) l)) = l ! i
[PROOF STEP]
by (auto simp add: hd_conv_nth)
[PROOF STATE]
proof (state)
this:
hd (drop i (take (j + 1) l)) = l ! i

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (l ! i, l ! j) \<in> R\<^sup>*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
hd (drop i (take (j + 1) l)) = l ! i

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (l ! i, l ! j) \<in> R\<^sup>*
[PROOF STEP]
have "last ?l = l ! j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. last (drop i (take (j + 1) l)) = l ! j
[PROOF STEP]
using \<open>?l \<noteq> []\<close> \<open>l \<noteq> []\<close> \<open>i < j\<close> \<open>j < length l\<close>
[PROOF STATE]
proof (prove)
using this:
drop i (take (j + 1) l) \<noteq> []
l \<noteq> []
i < j
j < length l

goal (1 subgoal):
 1. last (drop i (take (j + 1) l)) = l ! j
[PROOF STEP]
by (cases "length l = j + 1") (auto simp add: last_conv_nth min_def)
[PROOF STATE]
proof (state)
this:
last (drop i (take (j + 1) l)) = l ! j

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (l ! i, l ! j) \<in> R\<^sup>*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
last (drop i (take (j + 1) l)) = l ! j

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (l ! i, l ! j) \<in> R\<^sup>*
[PROOF STEP]
have "rel_chain ?l R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_chain (drop i (take (j + 1) l)) R
[PROOF STEP]
using \<open>rel_chain l R\<close>
[PROOF STATE]
proof (prove)
using this:
rel_chain l R

goal (1 subgoal):
 1. rel_chain (drop i (take (j + 1) l)) R
[PROOF STEP]
by (auto intro: rel_chain_drop rel_chain_take)
[PROOF STATE]
proof (state)
this:
rel_chain (drop i (take (j + 1) l)) R

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (l ! i, l ! j) \<in> R\<^sup>*
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
drop i (take (j + 1) l) \<noteq> []
hd (drop i (take (j + 1) l)) = l ! i
last (drop i (take (j + 1) l)) = l ! j
rel_chain (drop i (take (j + 1) l)) R
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
drop i (take (j + 1) l) \<noteq> []
hd (drop i (take (j + 1) l)) = l ! i
last (drop i (take (j + 1) l)) = l ! j
rel_chain (drop i (take (j + 1) l)) R

goal (1 subgoal):
 1. (l ! i, l ! j) \<in> R\<^sup>*
[PROOF STEP]
by (subst rtrancl_rel_chain) blast
[PROOF STATE]
proof (state)
this:
(l ! i, l ! j) \<in> R\<^sup>*

goal:
No subgoals!
[PROOF STEP]
qed