[STATEMENT]
lemma quadratic_change_coefficients:
  fixes x y :: complex
  assumes "A1 \<noteq> 0"
  assumes "qf = (\<lambda> x y. A1*x\<^sup>2 + A1*y\<^sup>2 + b1*x + b2*y + c)"
          "qf x y = 0"
          "qf_1 = (\<lambda> x y. x\<^sup>2 + y\<^sup>2 + (b1/A1)*x + (b2/A1)*y + c/A1)"
  shows "qf_1 x y = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qf_1 x y = 0
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. qf_1 x y = 0
[PROOF STEP]
have "0 = A1*x\<^sup>2 + A1*y\<^sup>2 + b1*x + b2*y + c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 = A1 * x\<^sup>2 + A1 * y\<^sup>2 + b1 * x + b2 * y + c
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A1 \<noteq> 0
qf = (\<lambda>x y. A1 * x\<^sup>2 + A1 * y\<^sup>2 + b1 * x + b2 * y + c)
qf x y = 0
qf_1 = (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + b1 / A1 * x + b2 / A1 * y + c / A1)

goal (1 subgoal):
 1. 0 = A1 * x\<^sup>2 + A1 * y\<^sup>2 + b1 * x + b2 * y + c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 = A1 * x\<^sup>2 + A1 * y\<^sup>2 + b1 * x + b2 * y + c

goal (1 subgoal):
 1. qf_1 x y = 0
[PROOF STEP]
hence "0/A1 = (A1*x\<^sup>2 + A1*y\<^sup>2 + b1*x + b2*y + c)/A1"
[PROOF STATE]
proof (prove)
using this:
0 = A1 * x\<^sup>2 + A1 * y\<^sup>2 + b1 * x + b2 * y + c

goal (1 subgoal):
 1. 0 / A1 = (A1 * x\<^sup>2 + A1 * y\<^sup>2 + b1 * x + b2 * y + c) / A1
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
0 = A1 * x\<^sup>2 + A1 * y\<^sup>2 + b1 * x + b2 * y + c
A1 \<noteq> 0

goal (1 subgoal):
 1. 0 / A1 = (A1 * x\<^sup>2 + A1 * y\<^sup>2 + b1 * x + b2 * y + c) / A1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 / A1 = (A1 * x\<^sup>2 + A1 * y\<^sup>2 + b1 * x + b2 * y + c) / A1

goal (1 subgoal):
 1. qf_1 x y = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 / A1 = (A1 * x\<^sup>2 + A1 * y\<^sup>2 + b1 * x + b2 * y + c) / A1

goal (1 subgoal):
 1. qf_1 x y = 0
[PROOF STEP]
have "... = A1*x\<^sup>2/A1 + A1*y\<^sup>2/A1 + b1*x/A1 + b2*y/A1 + c/A1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A1 * x\<^sup>2 + A1 * y\<^sup>2 + b1 * x + b2 * y + c) / A1 = A1 * x\<^sup>2 / A1 + A1 * y\<^sup>2 / A1 + b1 * x / A1 + b2 * y / A1 + c / A1
[PROOF STEP]
by (simp add: add_divide_distrib)
[PROOF STATE]
proof (state)
this:
(A1 * x\<^sup>2 + A1 * y\<^sup>2 + b1 * x + b2 * y + c) / A1 = A1 * x\<^sup>2 / A1 + A1 * y\<^sup>2 / A1 + b1 * x / A1 + b2 * y / A1 + c / A1

goal (1 subgoal):
 1. qf_1 x y = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(A1 * x\<^sup>2 + A1 * y\<^sup>2 + b1 * x + b2 * y + c) / A1 = A1 * x\<^sup>2 / A1 + A1 * y\<^sup>2 / A1 + b1 * x / A1 + b2 * y / A1 + c / A1

goal (1 subgoal):
 1. qf_1 x y = 0
[PROOF STEP]
have "... = x\<^sup>2 + y\<^sup>2 + (b1/A1)*x + (b2/A1)*y + c/A1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A1 * x\<^sup>2 / A1 + A1 * y\<^sup>2 / A1 + b1 * x / A1 + b2 * y / A1 + c / A1 = x\<^sup>2 + y\<^sup>2 + b1 / A1 * x + b2 / A1 * y + c / A1
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
A1 \<noteq> 0

goal (1 subgoal):
 1. A1 * x\<^sup>2 / A1 + A1 * y\<^sup>2 / A1 + b1 * x / A1 + b2 * y / A1 + c / A1 = x\<^sup>2 + y\<^sup>2 + b1 / A1 * x + b2 / A1 * y + c / A1
[PROOF STEP]
by (simp add:field_simps)
[PROOF STATE]
proof (state)
this:
A1 * x\<^sup>2 / A1 + A1 * y\<^sup>2 / A1 + b1 * x / A1 + b2 * y / A1 + c / A1 = x\<^sup>2 + y\<^sup>2 + b1 / A1 * x + b2 / A1 * y + c / A1

goal (1 subgoal):
 1. qf_1 x y = 0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
0 / A1 = x\<^sup>2 + y\<^sup>2 + b1 / A1 * x + b2 / A1 * y + c / A1
[PROOF STEP]
have "0 = x\<^sup>2 + y\<^sup>2 + (b1/A1)*x + (b2/A1)*y + c/A1"
[PROOF STATE]
proof (prove)
using this:
0 / A1 = x\<^sup>2 + y\<^sup>2 + b1 / A1 * x + b2 / A1 * y + c / A1

goal (1 subgoal):
 1. 0 = x\<^sup>2 + y\<^sup>2 + b1 / A1 * x + b2 / A1 * y + c / A1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 = x\<^sup>2 + y\<^sup>2 + b1 / A1 * x + b2 / A1 * y + c / A1

goal (1 subgoal):
 1. qf_1 x y = 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
0 = x\<^sup>2 + y\<^sup>2 + b1 / A1 * x + b2 / A1 * y + c / A1

goal (1 subgoal):
 1. qf_1 x y = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 = x\<^sup>2 + y\<^sup>2 + b1 / A1 * x + b2 / A1 * y + c / A1
A1 \<noteq> 0
qf = (\<lambda>x y. A1 * x\<^sup>2 + A1 * y\<^sup>2 + b1 * x + b2 * y + c)
qf x y = 0
qf_1 = (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + b1 / A1 * x + b2 / A1 * y + c / A1)

goal (1 subgoal):
 1. qf_1 x y = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
qf_1 x y = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma quadratic_quadratic_at_most_2_intersections:
  fixes x y x1 y1 x2 y2 :: complex
  assumes "A1 \<noteq> 0" and "A2 \<noteq> 0"
  assumes "qf1 = (\<lambda> x y. A1*x\<^sup>2 + A1*y\<^sup>2 + b1*x + b2*y + c)" and
          "qf2 = (\<lambda> x y. A2*x\<^sup>2 + A2*y\<^sup>2 + B1*x + B2*y + C)" and
          "qf1 x1 y1 = 0" and "qf2 x1 y1 = 0" and
          "qf1 x2 y2 = 0" and "qf2 x2 y2 = 0" and
          "(x1, y1) \<noteq> (x2, y2)" and
          "qf1 x y = 0" and "qf2 x y = 0"
  assumes "(b2*A2 - B2*A1)\<^sup>2 + (b1*A2 - B1*A1)\<^sup>2 \<noteq> 0" and
          "b2*A2 \<noteq> B2*A1 \<or> b1*A2 \<noteq> B1*A1"
  shows "(x, y) = (x1, y1) \<or> (x, y) = (x2, y2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
have *: "b2 / A1 \<noteq> B2 / A2 \<or> b1 / A1 \<noteq> B1 / A2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b2 / A1 \<noteq> B2 / A2 \<or> b1 / A1 \<noteq> B1 / A2
[PROOF STEP]
using assms(1, 2) assms(13)
[PROOF STATE]
proof (prove)
using this:
A1 \<noteq> 0
A2 \<noteq> 0
b2 * A2 \<noteq> B2 * A1 \<or> b1 * A2 \<noteq> B1 * A1

goal (1 subgoal):
 1. b2 / A1 \<noteq> B2 / A2 \<or> b1 / A1 \<noteq> B1 / A2
[PROOF STEP]
by (simp add:field_simps)
[PROOF STATE]
proof (state)
this:
b2 / A1 \<noteq> B2 / A2 \<or> b1 / A1 \<noteq> B1 / A2

goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
have **: "(b2 / A1 - B2 / A2)\<^sup>2 + (b1 / A1 - B1 / A2)\<^sup>2 \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b2 / A1 - B2 / A2)\<^sup>2 + (b1 / A1 - B1 / A2)\<^sup>2 \<noteq> 0
[PROOF STEP]
using assms(1, 2) assms(12)
[PROOF STATE]
proof (prove)
using this:
A1 \<noteq> 0
A2 \<noteq> 0
(b2 * A2 - B2 * A1)\<^sup>2 + (b1 * A2 - B1 * A1)\<^sup>2 \<noteq> 0

goal (1 subgoal):
 1. (b2 / A1 - B2 / A2)\<^sup>2 + (b1 / A1 - B1 / A2)\<^sup>2 \<noteq> 0
[PROOF STEP]
by (simp add:field_simps)
[PROOF STATE]
proof (state)
this:
(b2 / A1 - B2 / A2)\<^sup>2 + (b1 / A1 - B1 / A2)\<^sup>2 \<noteq> 0

goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
let ?qf_1 = "(\<lambda> x y. x\<^sup>2 + y\<^sup>2 + (b1/A1)*x + (b2/A1)*y + c/A1)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
let ?qf_2 = "(\<lambda> x y. x\<^sup>2 + y\<^sup>2 + (B1/A2)*x + (B2/A2)*y + C/A2)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
have "?qf_1 x1 y1 = 0" "?qf_1 x2 y2 = 0" "?qf_1 x y = 0"
       "?qf_2 x1 y1 = 0" "?qf_2 x2 y2 = 0" "?qf_2 x y = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x1\<^sup>2 + y1\<^sup>2 + b1 / A1 * x1 + b2 / A1 * y1 + c / A1 = 0 &&& x2\<^sup>2 + y2\<^sup>2 + b1 / A1 * x2 + b2 / A1 * y2 + c / A1 = 0 &&& x\<^sup>2 + y\<^sup>2 + b1 / A1 * x + b2 / A1 * y + c / A1 = 0) &&& x1\<^sup>2 + y1\<^sup>2 + B1 / A2 * x1 + B2 / A2 * y1 + C / A2 = 0 &&& x2\<^sup>2 + y2\<^sup>2 + B1 / A2 * x2 + B2 / A2 * y2 + C / A2 = 0 &&& x\<^sup>2 + y\<^sup>2 + B1 / A2 * x + B2 / A2 * y + C / A2 = 0
[PROOF STEP]
using assms quadratic_change_coefficients[of A1 qf1 b1 b2 c x2 y2 ?qf_1]
          quadratic_change_coefficients[of A1 qf1 b1 b2 c x1 y1 ?qf_1]
          quadratic_change_coefficients[of A2 qf2 B1 B2 C x1 y1 ?qf_2]
          quadratic_change_coefficients[of A2 qf2 B1 B2 C x2 y2 ?qf_2]
          quadratic_change_coefficients[of A1 qf1 b1 b2 c x y ?qf_1]
          quadratic_change_coefficients[of A2 qf2 B1 B2 C x y ?qf_2]
[PROOF STATE]
proof (prove)
using this:
A1 \<noteq> 0
A2 \<noteq> 0
qf1 = (\<lambda>x y. A1 * x\<^sup>2 + A1 * y\<^sup>2 + b1 * x + b2 * y + c)
qf2 = (\<lambda>x y. A2 * x\<^sup>2 + A2 * y\<^sup>2 + B1 * x + B2 * y + C)
qf1 x1 y1 = 0
qf2 x1 y1 = 0
qf1 x2 y2 = 0
qf2 x2 y2 = 0
(x1, y1) \<noteq> (x2, y2)
qf1 x y = 0
qf2 x y = 0
(b2 * A2 - B2 * A1)\<^sup>2 + (b1 * A2 - B1 * A1)\<^sup>2 \<noteq> 0
b2 * A2 \<noteq> B2 * A1 \<or> b1 * A2 \<noteq> B1 * A1
\<lbrakk>A1 \<noteq> 0; qf1 = (\<lambda>x y. A1 * x\<^sup>2 + A1 * y\<^sup>2 + b1 * x + b2 * y + c); qf1 x2 y2 = 0; (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + b1 / A1 * x + b2 / A1 * y + c / A1) = (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + b1 / A1 * x + b2 / A1 * y + c / A1)\<rbrakk> \<Longrightarrow> x2\<^sup>2 + y2\<^sup>2 + b1 / A1 * x2 + b2 / A1 * y2 + c / A1 = 0
\<lbrakk>A1 \<noteq> 0; qf1 = (\<lambda>x y. A1 * x\<^sup>2 + A1 * y\<^sup>2 + b1 * x + b2 * y + c); qf1 x1 y1 = 0; (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + b1 / A1 * x + b2 / A1 * y + c / A1) = (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + b1 / A1 * x + b2 / A1 * y + c / A1)\<rbrakk> \<Longrightarrow> x1\<^sup>2 + y1\<^sup>2 + b1 / A1 * x1 + b2 / A1 * y1 + c / A1 = 0
\<lbrakk>A2 \<noteq> 0; qf2 = (\<lambda>x y. A2 * x\<^sup>2 + A2 * y\<^sup>2 + B1 * x + B2 * y + C); qf2 x1 y1 = 0; (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + B1 / A2 * x + B2 / A2 * y + C / A2) = (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + B1 / A2 * x + B2 / A2 * y + C / A2)\<rbrakk> \<Longrightarrow> x1\<^sup>2 + y1\<^sup>2 + B1 / A2 * x1 + B2 / A2 * y1 + C / A2 = 0
\<lbrakk>A2 \<noteq> 0; qf2 = (\<lambda>x y. A2 * x\<^sup>2 + A2 * y\<^sup>2 + B1 * x + B2 * y + C); qf2 x2 y2 = 0; (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + B1 / A2 * x + B2 / A2 * y + C / A2) = (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + B1 / A2 * x + B2 / A2 * y + C / A2)\<rbrakk> \<Longrightarrow> x2\<^sup>2 + y2\<^sup>2 + B1 / A2 * x2 + B2 / A2 * y2 + C / A2 = 0
\<lbrakk>A1 \<noteq> 0; qf1 = (\<lambda>x y. A1 * x\<^sup>2 + A1 * y\<^sup>2 + b1 * x + b2 * y + c); qf1 x y = 0; (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + b1 / A1 * x + b2 / A1 * y + c / A1) = (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + b1 / A1 * x + b2 / A1 * y + c / A1)\<rbrakk> \<Longrightarrow> x\<^sup>2 + y\<^sup>2 + b1 / A1 * x + b2 / A1 * y + c / A1 = 0
\<lbrakk>A2 \<noteq> 0; qf2 = (\<lambda>x y. A2 * x\<^sup>2 + A2 * y\<^sup>2 + B1 * x + B2 * y + C); qf2 x y = 0; (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + B1 / A2 * x + B2 / A2 * y + C / A2) = (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + B1 / A2 * x + B2 / A2 * y + C / A2)\<rbrakk> \<Longrightarrow> x\<^sup>2 + y\<^sup>2 + B1 / A2 * x + B2 / A2 * y + C / A2 = 0

goal (1 subgoal):
 1. (x1\<^sup>2 + y1\<^sup>2 + b1 / A1 * x1 + b2 / A1 * y1 + c / A1 = 0 &&& x2\<^sup>2 + y2\<^sup>2 + b1 / A1 * x2 + b2 / A1 * y2 + c / A1 = 0 &&& x\<^sup>2 + y\<^sup>2 + b1 / A1 * x + b2 / A1 * y + c / A1 = 0) &&& x1\<^sup>2 + y1\<^sup>2 + B1 / A2 * x1 + B2 / A2 * y1 + C / A2 = 0 &&& x2\<^sup>2 + y2\<^sup>2 + B1 / A2 * x2 + B2 / A2 * y2 + C / A2 = 0 &&& x\<^sup>2 + y\<^sup>2 + B1 / A2 * x + B2 / A2 * y + C / A2 = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x1\<^sup>2 + y1\<^sup>2 + b1 / A1 * x1 + b2 / A1 * y1 + c / A1 = 0
x2\<^sup>2 + y2\<^sup>2 + b1 / A1 * x2 + b2 / A1 * y2 + c / A1 = 0
x\<^sup>2 + y\<^sup>2 + b1 / A1 * x + b2 / A1 * y + c / A1 = 0
x1\<^sup>2 + y1\<^sup>2 + B1 / A2 * x1 + B2 / A2 * y1 + C / A2 = 0
x2\<^sup>2 + y2\<^sup>2 + B1 / A2 * x2 + B2 / A2 * y2 + C / A2 = 0
x\<^sup>2 + y\<^sup>2 + B1 / A2 * x + B2 / A2 * y + C / A2 = 0

goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x1\<^sup>2 + y1\<^sup>2 + b1 / A1 * x1 + b2 / A1 * y1 + c / A1 = 0
x2\<^sup>2 + y2\<^sup>2 + b1 / A1 * x2 + b2 / A1 * y2 + c / A1 = 0
x\<^sup>2 + y\<^sup>2 + b1 / A1 * x + b2 / A1 * y + c / A1 = 0
x1\<^sup>2 + y1\<^sup>2 + B1 / A2 * x1 + B2 / A2 * y1 + C / A2 = 0
x2\<^sup>2 + y2\<^sup>2 + B1 / A2 * x2 + B2 / A2 * y2 + C / A2 = 0
x\<^sup>2 + y\<^sup>2 + B1 / A2 * x + B2 / A2 * y + C / A2 = 0

goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
using quadratic_quadratic_at_most_2_intersections'
              [of "b2 / A1" "B2 / A2" "b1 / A1" "B1 / A2" ?qf_1 "c / A1" ?qf_2 "C / A2" x1 y1 x2 y2 x y]
[PROOF STATE]
proof (prove)
using this:
x1\<^sup>2 + y1\<^sup>2 + b1 / A1 * x1 + b2 / A1 * y1 + c / A1 = 0
x2\<^sup>2 + y2\<^sup>2 + b1 / A1 * x2 + b2 / A1 * y2 + c / A1 = 0
x\<^sup>2 + y\<^sup>2 + b1 / A1 * x + b2 / A1 * y + c / A1 = 0
x1\<^sup>2 + y1\<^sup>2 + B1 / A2 * x1 + B2 / A2 * y1 + C / A2 = 0
x2\<^sup>2 + y2\<^sup>2 + B1 / A2 * x2 + B2 / A2 * y2 + C / A2 = 0
x\<^sup>2 + y\<^sup>2 + B1 / A2 * x + B2 / A2 * y + C / A2 = 0
\<lbrakk>b2 / A1 \<noteq> B2 / A2 \<or> b1 / A1 \<noteq> B1 / A2; (b2 / A1 - B2 / A2)\<^sup>2 + (b1 / A1 - B1 / A2)\<^sup>2 \<noteq> 0; (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + b1 / A1 * x + b2 / A1 * y + c / A1) = (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + b1 / A1 * x + b2 / A1 * y + c / A1); (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + B1 / A2 * x + B2 / A2 * y + C / A2) = (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + B1 / A2 * x + B2 / A2 * y + C / A2); x1\<^sup>2 + y1\<^sup>2 + b1 / A1 * x1 + b2 / A1 * y1 + c / A1 = 0; x1\<^sup>2 + y1\<^sup>2 + B1 / A2 * x1 + B2 / A2 * y1 + C / A2 = 0; x2\<^sup>2 + y2\<^sup>2 + b1 / A1 * x2 + b2 / A1 * y2 + c / A1 = 0; x2\<^sup>2 + y2\<^sup>2 + B1 / A2 * x2 + B2 / A2 * y2 + C / A2 = 0; (x1, y1) \<noteq> (x2, y2); x\<^sup>2 + y\<^sup>2 + b1 / A1 * x + b2 / A1 * y + c / A1 = 0; x\<^sup>2 + y\<^sup>2 + B1 / A2 * x + B2 / A2 * y + C / A2 = 0\<rbrakk> \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)

goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
using * ** \<open>(x1, y1) \<noteq> (x2, y2)\<close>
[PROOF STATE]
proof (prove)
using this:
x1\<^sup>2 + y1\<^sup>2 + b1 / A1 * x1 + b2 / A1 * y1 + c / A1 = 0
x2\<^sup>2 + y2\<^sup>2 + b1 / A1 * x2 + b2 / A1 * y2 + c / A1 = 0
x\<^sup>2 + y\<^sup>2 + b1 / A1 * x + b2 / A1 * y + c / A1 = 0
x1\<^sup>2 + y1\<^sup>2 + B1 / A2 * x1 + B2 / A2 * y1 + C / A2 = 0
x2\<^sup>2 + y2\<^sup>2 + B1 / A2 * x2 + B2 / A2 * y2 + C / A2 = 0
x\<^sup>2 + y\<^sup>2 + B1 / A2 * x + B2 / A2 * y + C / A2 = 0
\<lbrakk>b2 / A1 \<noteq> B2 / A2 \<or> b1 / A1 \<noteq> B1 / A2; (b2 / A1 - B2 / A2)\<^sup>2 + (b1 / A1 - B1 / A2)\<^sup>2 \<noteq> 0; (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + b1 / A1 * x + b2 / A1 * y + c / A1) = (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + b1 / A1 * x + b2 / A1 * y + c / A1); (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + B1 / A2 * x + B2 / A2 * y + C / A2) = (\<lambda>x y. x\<^sup>2 + y\<^sup>2 + B1 / A2 * x + B2 / A2 * y + C / A2); x1\<^sup>2 + y1\<^sup>2 + b1 / A1 * x1 + b2 / A1 * y1 + c / A1 = 0; x1\<^sup>2 + y1\<^sup>2 + B1 / A2 * x1 + B2 / A2 * y1 + C / A2 = 0; x2\<^sup>2 + y2\<^sup>2 + b1 / A1 * x2 + b2 / A1 * y2 + c / A1 = 0; x2\<^sup>2 + y2\<^sup>2 + B1 / A2 * x2 + B2 / A2 * y2 + C / A2 = 0; (x1, y1) \<noteq> (x2, y2); x\<^sup>2 + y\<^sup>2 + b1 / A1 * x + b2 / A1 * y + c / A1 = 0; x\<^sup>2 + y\<^sup>2 + B1 / A2 * x + B2 / A2 * y + C / A2 = 0\<rbrakk> \<Longrightarrow> (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
b2 / A1 \<noteq> B2 / A2 \<or> b1 / A1 \<noteq> B1 / A2
(b2 / A1 - B2 / A2)\<^sup>2 + (b1 / A1 - B1 / A2)\<^sup>2 \<noteq> 0
(x1, y1) \<noteq> (x2, y2)

goal (1 subgoal):
 1. (x, y) = (x1, y1) \<or> (x, y) = (x2, y2)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(x, y) = (x1, y1) \<or> (x, y) = (x2, y2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma edge_begin_tup: "edge_begin x = fst (fst x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. edge_begin x = fst (fst x)
[PROOF STEP]
by (metis edge_begin.simps prod.collapse)


[STATEMENT]
lemma edge_end_tup: "edge_end x = fst (snd x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. edge_end x = fst (snd x)
[PROOF STEP]
by (metis edge_end.simps prod.collapse)


[STATEMENT]
lemma path_cons_simp: "path v v' (e # pth) \<longleftrightarrow> fst (fst e) = v \<and> e \<in> edges \<and> path (fst (snd e)) v' pth"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path v v' (e # pth) = (fst (fst e) = v \<and> e \<in> edges \<and> path (fst (snd e)) v' pth)
[PROOF STEP]
by(auto simp add: path_cons_simp', metis prod.collapse)


[STATEMENT]
lemma path_appendI: "path v v' pth1 \<Longrightarrow> path v' v'' pth2 \<Longrightarrow> path v v'' (pth1@pth2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>path v v' pth1; path v' v'' pth2\<rbrakk> \<Longrightarrow> path v v'' (pth1 @ pth2)
[PROOF STEP]
by (induction pth1 arbitrary: v) (auto simp add: path_cons_simp )


[STATEMENT]
lemma path_split: "path v v' (pth1@[e]@pth2) \<longleftrightarrow> path v (edge_end e) (pth1@[e]) \<and> path (edge_end e) v' pth2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path v v' (pth1 @ [e] @ pth2) = (path v (edge_end e) (pth1 @ [e]) \<and> path (edge_end e) v' pth2)
[PROOF STEP]
by (induction pth1 arbitrary: v) (auto simp add: path_cons_simp edge_end_tup intro: path_empty)


[STATEMENT]
lemma path_split2: "path v v' (pth1@(e#pth2)) \<longleftrightarrow> path v (edge_begin e) pth1 \<and> path (edge_begin e) v' (e#pth2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path v v' (pth1 @ e # pth2) = (path v (edge_begin e) pth1 \<and> path (edge_begin e) v' (e # pth2))
[PROOF STEP]
by (induction pth1 arbitrary: v) (auto simp add: path_cons_simp edge_begin_tup intro: path_empty)


[STATEMENT]
lemma path_snoc: "path v v' (pth1@[e]) \<longleftrightarrow> e \<in> edges \<and> path v (edge_begin e) pth1 \<and> edge_end e = v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path v v' (pth1 @ [e]) = (e \<in> edges \<and> path v (edge_begin e) pth1 \<and> edge_end e = v')
[PROOF STEP]
by (auto simp add: path_split2 path_cons_simp edge_end_tup edge_begin_tup)


[STATEMENT]
lemma scope_find:
    assumes "v \<in> scope ps"
    assumes "terminal_vertex v'"
    assumes "path v v' pth"
    shows "ps \<in> snd ` set pth"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ps \<in> snd ` set pth
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
v \<in> scope ps
terminal_vertex v'
path v v' pth

goal (1 subgoal):
 1. ps \<in> snd ` set pth
[PROOF STEP]
by (auto simp add: scope.simps)


[STATEMENT]
lemma snd_set_split:
    assumes "ps \<in> snd ` set pth"
    obtains pth1 pth2 e  where "pth = pth1@[e]@pth2" and "snd e = ps" and "ps \<notin> snd ` set pth1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pth1 e pth2. \<lbrakk>pth = pth1 @ [e] @ pth2; snd e = ps; ps \<notin> snd ` set pth1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ps \<in> snd ` set pth

goal (1 subgoal):
 1. (\<And>pth1 e pth2. \<lbrakk>pth = pth1 @ [e] @ pth2; snd e = ps; ps \<notin> snd ` set pth1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof (atomize_elim, induction pth)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>ps \<in> snd ` set []; ps \<in> snd ` set []\<rbrakk> \<Longrightarrow> \<exists>pth1 e pth2. [] = pth1 @ [e] @ pth2 \<and> snd e = ps \<and> ps \<notin> snd ` set pth1
 2. \<And>a pth. \<lbrakk>\<lbrakk>ps \<in> snd ` set pth; ps \<in> snd ` set pth\<rbrakk> \<Longrightarrow> \<exists>pth1 e pth2. pth = pth1 @ [e] @ pth2 \<and> snd e = ps \<and> ps \<notin> snd ` set pth1; ps \<in> snd ` set (a # pth); ps \<in> snd ` set (a # pth)\<rbrakk> \<Longrightarrow> \<exists>pth1 e pth2. a # pth = pth1 @ [e] @ pth2 \<and> snd e = ps \<and> ps \<notin> snd ` set pth1
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
ps \<in> snd ` set []
ps \<in> snd ` set []

goal (2 subgoals):
 1. \<lbrakk>ps \<in> snd ` set []; ps \<in> snd ` set []\<rbrakk> \<Longrightarrow> \<exists>pth1 e pth2. [] = pth1 @ [e] @ pth2 \<and> snd e = ps \<and> ps \<notin> snd ` set pth1
 2. \<And>a pth. \<lbrakk>\<lbrakk>ps \<in> snd ` set pth; ps \<in> snd ` set pth\<rbrakk> \<Longrightarrow> \<exists>pth1 e pth2. pth = pth1 @ [e] @ pth2 \<and> snd e = ps \<and> ps \<notin> snd ` set pth1; ps \<in> snd ` set (a # pth); ps \<in> snd ` set (a # pth)\<rbrakk> \<Longrightarrow> \<exists>pth1 e pth2. a # pth = pth1 @ [e] @ pth2 \<and> snd e = ps \<and> ps \<notin> snd ` set pth1
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
ps \<in> snd ` set []
ps \<in> snd ` set []

goal (1 subgoal):
 1. \<exists>pth1 e pth2. [] = pth1 @ [e] @ pth2 \<and> snd e = ps \<and> ps \<notin> snd ` set pth1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>pth1 e pth2. [] = pth1 @ [e] @ pth2 \<and> snd e = ps \<and> ps \<notin> snd ` set pth1

goal (1 subgoal):
 1. \<And>a pth. \<lbrakk>\<lbrakk>ps \<in> snd ` set pth; ps \<in> snd ` set pth\<rbrakk> \<Longrightarrow> \<exists>pth1 e pth2. pth = pth1 @ [e] @ pth2 \<and> snd e = ps \<and> ps \<notin> snd ` set pth1; ps \<in> snd ` set (a # pth); ps \<in> snd ` set (a # pth)\<rbrakk> \<Longrightarrow> \<exists>pth1 e pth2. a # pth = pth1 @ [e] @ pth2 \<and> snd e = ps \<and> ps \<notin> snd ` set pth1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a pth. \<lbrakk>\<lbrakk>ps \<in> snd ` set pth; ps \<in> snd ` set pth\<rbrakk> \<Longrightarrow> \<exists>pth1 e pth2. pth = pth1 @ [e] @ pth2 \<and> snd e = ps \<and> ps \<notin> snd ` set pth1; ps \<in> snd ` set (a # pth); ps \<in> snd ` set (a # pth)\<rbrakk> \<Longrightarrow> \<exists>pth1 e pth2. a # pth = pth1 @ [e] @ pth2 \<and> snd e = ps \<and> ps \<notin> snd ` set pth1
[PROOF STEP]
case (Cons e pth)
[PROOF STATE]
proof (state)
this:
\<lbrakk>ps \<in> snd ` set pth; ps \<in> snd ` set pth\<rbrakk> \<Longrightarrow> \<exists>pth1 e pth2. pth = pth1 @ [e] @ pth2 \<and> snd e = ps \<and> ps \<notin> snd ` set pth1
ps \<in> snd ` set (e # pth)
ps \<in> snd ` set (e # pth)

goal (1 subgoal):
 1. \<And>a pth. \<lbrakk>\<lbrakk>ps \<in> snd ` set pth; ps \<in> snd ` set pth\<rbrakk> \<Longrightarrow> \<exists>pth1 e pth2. pth = pth1 @ [e] @ pth2 \<and> snd e = ps \<and> ps \<notin> snd ` set pth1; ps \<in> snd ` set (a # pth); ps \<in> snd ` set (a # pth)\<rbrakk> \<Longrightarrow> \<exists>pth1 e pth2. a # pth = pth1 @ [e] @ pth2 \<and> snd e = ps \<and> ps \<notin> snd ` set pth1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>pth1 ea pth2. e # pth = pth1 @ [ea] @ pth2 \<and> snd ea = ps \<and> ps \<notin> snd ` set pth1
[PROOF STEP]
proof(cases "snd e = ps")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. snd e = ps \<Longrightarrow> \<exists>pth1 ea pth2. e # pth = pth1 @ [ea] @ pth2 \<and> snd ea = ps \<and> ps \<notin> snd ` set pth1
 2. snd e \<noteq> ps \<Longrightarrow> \<exists>pth1 ea pth2. e # pth = pth1 @ [ea] @ pth2 \<and> snd ea = ps \<and> ps \<notin> snd ` set pth1
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
snd e = ps

goal (2 subgoals):
 1. snd e = ps \<Longrightarrow> \<exists>pth1 ea pth2. e # pth = pth1 @ [ea] @ pth2 \<and> snd ea = ps \<and> ps \<notin> snd ` set pth1
 2. snd e \<noteq> ps \<Longrightarrow> \<exists>pth1 ea pth2. e # pth = pth1 @ [ea] @ pth2 \<and> snd ea = ps \<and> ps \<notin> snd ` set pth1
[PROOF STEP]
hence "e # pth = [] @ [e] @ pth \<and> snd e = ps \<and> ps \<notin> snd ` set []"
[PROOF STATE]
proof (prove)
using this:
snd e = ps

goal (1 subgoal):
 1. e # pth = [] @ [e] @ pth \<and> snd e = ps \<and> ps \<notin> snd ` set []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
e # pth = [] @ [e] @ pth \<and> snd e = ps \<and> ps \<notin> snd ` set []

goal (2 subgoals):
 1. snd e = ps \<Longrightarrow> \<exists>pth1 ea pth2. e # pth = pth1 @ [ea] @ pth2 \<and> snd ea = ps \<and> ps \<notin> snd ` set pth1
 2. snd e \<noteq> ps \<Longrightarrow> \<exists>pth1 ea pth2. e # pth = pth1 @ [ea] @ pth2 \<and> snd ea = ps \<and> ps \<notin> snd ` set pth1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
e # pth = [] @ [e] @ pth \<and> snd e = ps \<and> ps \<notin> snd ` set []

goal (1 subgoal):
 1. \<exists>pth1 ea pth2. e # pth = pth1 @ [ea] @ pth2 \<and> snd ea = ps \<and> ps \<notin> snd ` set pth1
[PROOF STEP]
by (intro exI)
[PROOF STATE]
proof (state)
this:
\<exists>pth1 ea pth2. e # pth = pth1 @ [ea] @ pth2 \<and> snd ea = ps \<and> ps \<notin> snd ` set pth1

goal (1 subgoal):
 1. snd e \<noteq> ps \<Longrightarrow> \<exists>pth1 ea pth2. e # pth = pth1 @ [ea] @ pth2 \<and> snd ea = ps \<and> ps \<notin> snd ` set pth1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. snd e \<noteq> ps \<Longrightarrow> \<exists>pth1 ea pth2. e # pth = pth1 @ [ea] @ pth2 \<and> snd ea = ps \<and> ps \<notin> snd ` set pth1
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
snd e \<noteq> ps

goal (1 subgoal):
 1. snd e \<noteq> ps \<Longrightarrow> \<exists>pth1 ea pth2. e # pth = pth1 @ [ea] @ pth2 \<and> snd ea = ps \<and> ps \<notin> snd ` set pth1
[PROOF STEP]
with Cons(2)
[PROOF STATE]
proof (chain)
picking this:
ps \<in> snd ` set (e # pth)
snd e \<noteq> ps
[PROOF STEP]
have "ps \<in> snd ` set pth"
[PROOF STATE]
proof (prove)
using this:
ps \<in> snd ` set (e # pth)
snd e \<noteq> ps

goal (1 subgoal):
 1. ps \<in> snd ` set pth
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ps \<in> snd ` set pth

goal (1 subgoal):
 1. snd e \<noteq> ps \<Longrightarrow> \<exists>pth1 ea pth2. e # pth = pth1 @ [ea] @ pth2 \<and> snd ea = ps \<and> ps \<notin> snd ` set pth1
[PROOF STEP]
from Cons.IH[OF this this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>pth1 e pth2. pth = pth1 @ [e] @ pth2 \<and> snd e = ps \<and> ps \<notin> snd ` set pth1
[PROOF STEP]
obtain pth1 e' pth2 where "pth = pth1 @ [e'] @ pth2 \<and> snd e' = ps \<and> ps \<notin> snd ` set pth1"
[PROOF STATE]
proof (prove)
using this:
\<exists>pth1 e pth2. pth = pth1 @ [e] @ pth2 \<and> snd e = ps \<and> ps \<notin> snd ` set pth1

goal (1 subgoal):
 1. (\<And>pth1 e' pth2. pth = pth1 @ [e'] @ pth2 \<and> snd e' = ps \<and> ps \<notin> snd ` set pth1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pth = pth1 @ [e'] @ pth2 \<and> snd e' = ps \<and> ps \<notin> snd ` set pth1

goal (1 subgoal):
 1. snd e \<noteq> ps \<Longrightarrow> \<exists>pth1 ea pth2. e # pth = pth1 @ [ea] @ pth2 \<and> snd ea = ps \<and> ps \<notin> snd ` set pth1
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
snd e \<noteq> ps
pth = pth1 @ [e'] @ pth2 \<and> snd e' = ps \<and> ps \<notin> snd ` set pth1
[PROOF STEP]
have "e#pth = (e# pth1) @ [e'] @ pth2 \<and> snd e' = ps \<and> ps \<notin> snd ` set (e#pth1)"
[PROOF STATE]
proof (prove)
using this:
snd e \<noteq> ps
pth = pth1 @ [e'] @ pth2 \<and> snd e' = ps \<and> ps \<notin> snd ` set pth1

goal (1 subgoal):
 1. e # pth = (e # pth1) @ [e'] @ pth2 \<and> snd e' = ps \<and> ps \<notin> snd ` set (e # pth1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
e # pth = (e # pth1) @ [e'] @ pth2 \<and> snd e' = ps \<and> ps \<notin> snd ` set (e # pth1)

goal (1 subgoal):
 1. snd e \<noteq> ps \<Longrightarrow> \<exists>pth1 ea pth2. e # pth = pth1 @ [ea] @ pth2 \<and> snd ea = ps \<and> ps \<notin> snd ` set pth1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
e # pth = (e # pth1) @ [e'] @ pth2 \<and> snd e' = ps \<and> ps \<notin> snd ` set (e # pth1)

goal (1 subgoal):
 1. \<exists>pth1 ea pth2. e # pth = pth1 @ [ea] @ pth2 \<and> snd ea = ps \<and> ps \<notin> snd ` set pth1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>pth1 ea pth2. e # pth = pth1 @ [ea] @ pth2 \<and> snd ea = ps \<and> ps \<notin> snd ` set pth1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>pth1 ea pth2. e # pth = pth1 @ [ea] @ pth2 \<and> snd ea = ps \<and> ps \<notin> snd ` set pth1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma scope_split:
    assumes "v \<in> scope ps"
    assumes "path v v' pth"
    assumes "terminal_vertex v'"
    obtains pth1 e pth2
    where "pth = (pth1@[e])@pth2" and "path v (fst ps) (pth1@[e])" and "path (fst ps) v' pth2" and "snd e = ps" and "ps \<notin> snd ` set pth1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pth1 e pth2. \<lbrakk>pth = (pth1 @ [e]) @ pth2; path v (fst ps) (pth1 @ [e]); path (fst ps) v' pth2; snd e = ps; ps \<notin> snd ` set pth1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>pth1 e pth2. \<lbrakk>pth = (pth1 @ [e]) @ pth2; path v (fst ps) (pth1 @ [e]); path (fst ps) v' pth2; snd e = ps; ps \<notin> snd ` set pth1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
v \<in> scope ps
path v v' pth
terminal_vertex v'
[PROOF STEP]
have "ps \<in> snd ` set pth"
[PROOF STATE]
proof (prove)
using this:
v \<in> scope ps
path v v' pth
terminal_vertex v'

goal (1 subgoal):
 1. ps \<in> snd ` set pth
[PROOF STEP]
by (auto simp add: scope.simps)
[PROOF STATE]
proof (state)
this:
ps \<in> snd ` set pth

goal (1 subgoal):
 1. (\<And>pth1 e pth2. \<lbrakk>pth = (pth1 @ [e]) @ pth2; path v (fst ps) (pth1 @ [e]); path (fst ps) v' pth2; snd e = ps; ps \<notin> snd ` set pth1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ps \<in> snd ` set pth
[PROOF STEP]
obtain pth1 pth2 e  where "pth = pth1@[e]@pth2" and "snd e = ps" and "ps \<notin> snd ` set pth1"
[PROOF STATE]
proof (prove)
using this:
ps \<in> snd ` set pth

goal (1 subgoal):
 1. (\<And>pth1 e pth2. \<lbrakk>pth = pth1 @ [e] @ pth2; snd e = ps; ps \<notin> snd ` set pth1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule snd_set_split)
[PROOF STATE]
proof (state)
this:
pth = pth1 @ [e] @ pth2
snd e = ps
ps \<notin> snd ` set pth1

goal (1 subgoal):
 1. (\<And>pth1 e pth2. \<lbrakk>pth = (pth1 @ [e]) @ pth2; path v (fst ps) (pth1 @ [e]); path (fst ps) v' pth2; snd e = ps; ps \<notin> snd ` set pth1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from \<open>path _ _ _\<close> and \<open>pth = pth1@[e]@pth2\<close>
[PROOF STATE]
proof (chain)
picking this:
path v v' pth
pth = pth1 @ [e] @ pth2
[PROOF STEP]
have "path v (edge_end e) (pth1@[e])" and "path (edge_end e) v' pth2"
[PROOF STATE]
proof (prove)
using this:
path v v' pth
pth = pth1 @ [e] @ pth2

goal (1 subgoal):
 1. path v (edge_end e) (pth1 @ [e]) &&& path (edge_end e) v' pth2
[PROOF STEP]
by (metis path_split)+
[PROOF STATE]
proof (state)
this:
path v (edge_end e) (pth1 @ [e])
path (edge_end e) v' pth2

goal (1 subgoal):
 1. (\<And>pth1 e pth2. \<lbrakk>pth = (pth1 @ [e]) @ pth2; path v (fst ps) (pth1 @ [e]); path (fst ps) v' pth2; snd e = ps; ps \<notin> snd ` set pth1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof(rule that)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. pth = (?pth1.0 @ [?e]) @ ?pth2.0
 2. path v (fst ps) (?pth1.0 @ [?e])
 3. path (fst ps) v' ?pth2.0
 4. snd ?e = ps
 5. ps \<notin> snd ` set ?pth1.0
[PROOF STEP]
show "pth = (pth1@[e])@pth2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pth = (pth1 @ [e]) @ pth2
[PROOF STEP]
using \<open>pth= _\<close>
[PROOF STATE]
proof (prove)
using this:
pth = pth1 @ [e] @ pth2

goal (1 subgoal):
 1. pth = (pth1 @ [e]) @ pth2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pth = (pth1 @ [e]) @ pth2

goal (4 subgoals):
 1. path v (fst ps) (pth1 @ [e])
 2. path (fst ps) v' pth2
 3. snd e = ps
 4. ps \<notin> snd ` set pth1
[PROOF STEP]
show "path v (fst ps) (pth1@[e])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path v (fst ps) (pth1 @ [e])
[PROOF STEP]
using \<open>path v (edge_end e) (pth1@[e])\<close>  \<open>snd e = ps\<close>
[PROOF STATE]
proof (prove)
using this:
path v (edge_end e) (pth1 @ [e])
snd e = ps

goal (1 subgoal):
 1. path v (fst ps) (pth1 @ [e])
[PROOF STEP]
by (simp add: edge_end_tup)
[PROOF STATE]
proof (state)
this:
path v (fst ps) (pth1 @ [e])

goal (3 subgoals):
 1. path (fst ps) v' pth2
 2. snd e = ps
 3. ps \<notin> snd ` set pth1
[PROOF STEP]
show "path (fst ps) v' pth2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (fst ps) v' pth2
[PROOF STEP]
using \<open>path (edge_end e) v' pth2\<close>  \<open>snd e = ps\<close>
[PROOF STATE]
proof (prove)
using this:
path (edge_end e) v' pth2
snd e = ps

goal (1 subgoal):
 1. path (fst ps) v' pth2
[PROOF STEP]
by (simp add: edge_end_tup)
[PROOF STATE]
proof (state)
this:
path (fst ps) v' pth2

goal (2 subgoals):
 1. snd e = ps
 2. ps \<notin> snd ` set pth1
[PROOF STEP]
show "ps \<notin> snd ` set pth1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ps \<notin> snd ` set pth1
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
ps \<notin> snd ` set pth1

goal (1 subgoal):
 1. snd e = ps
[PROOF STEP]
show "snd e = ps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd e = ps
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
snd e = ps

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma snd_set_path_verties: "path v v' pth \<Longrightarrow> fst ` snd ` set pth \<subseteq> fset vertices"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path v v' pth \<Longrightarrow> fst ` snd ` set pth \<subseteq> fset vertices
[PROOF STEP]
apply (induction rule: path.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>v. fst ` snd ` set [] \<subseteq> fset vertices
 2. \<And>e v' pth. \<lbrakk>e \<in> edges; path (edge_end e) v' pth; fst ` snd ` set pth \<subseteq> fset vertices\<rbrakk> \<Longrightarrow> fst ` snd ` set (e # pth) \<subseteq> fset vertices
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba v' pth. \<lbrakk>((a, b), aa, ba) \<in> edges; path aa v' pth; fst ` snd ` set pth \<subseteq> fset vertices\<rbrakk> \<Longrightarrow> aa \<in> fset vertices
[PROOF STEP]
apply (metis valid_in_port.elims(2) edge_end.simps notin_fset case_prodD valid_edges)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fst_set_path_verties: "path v v' pth \<Longrightarrow> fst ` fst ` set pth \<subseteq> fset vertices"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path v v' pth \<Longrightarrow> fst ` fst ` set pth \<subseteq> fset vertices
[PROOF STEP]
apply (induction rule: path.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>v. fst ` fst ` set [] \<subseteq> fset vertices
 2. \<And>e v' pth. \<lbrakk>e \<in> edges; path (edge_end e) v' pth; fst ` fst ` set pth \<subseteq> fset vertices\<rbrakk> \<Longrightarrow> fst ` fst ` set (e # pth) \<subseteq> fset vertices
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba v' pth. \<lbrakk>((a, b), aa, ba) \<in> edges; path aa v' pth; fst ` fst ` set pth \<subseteq> fset vertices\<rbrakk> \<Longrightarrow> a \<in> fset vertices
[PROOF STEP]
apply (metis valid_out_port.elims(2) edge_begin.simps notin_fset case_prodD valid_edges)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma scopes_not_refl:
    assumes "v |\<in>| vertices"
    shows "v \<notin> scope (v,p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<notin> scope (v, p)
[PROOF STEP]
proof(rule notI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<in> scope (v, p) \<Longrightarrow> False
[PROOF STEP]
assume "v \<in> scope (v,p)"
[PROOF STATE]
proof (state)
this:
v \<in> scope (v, p)

goal (1 subgoal):
 1. v \<in> scope (v, p) \<Longrightarrow> False
[PROOF STEP]
from pruned[OF assms]
[PROOF STATE]
proof (chain)
picking this:
\<exists>pth v'. path v v' pth \<and> terminal_vertex v'
[PROOF STEP]
obtain pth t where "terminal_vertex t" and "path v t pth" and least: "\<forall> pth'. path v t pth' \<longrightarrow> length pth \<le> length pth'"
[PROOF STATE]
proof (prove)
using this:
\<exists>pth v'. path v v' pth \<and> terminal_vertex v'

goal (1 subgoal):
 1. (\<And>t pth. \<lbrakk>terminal_vertex t; path v t pth; \<forall>pth'. path v t pth' \<longrightarrow> length pth \<le> length pth'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by atomize_elim (auto simp del: terminal_vertex.simps elim: ex_has_least_nat)
[PROOF STATE]
proof (state)
this:
terminal_vertex t
path v t pth
\<forall>pth'. path v t pth' \<longrightarrow> length pth \<le> length pth'

goal (1 subgoal):
 1. v \<in> scope (v, p) \<Longrightarrow> False
[PROOF STEP]
from scope_split[OF \<open>v \<in> scope (v,p)\<close> \<open>path v t pth\<close> \<open>terminal_vertex t\<close>]
[PROOF STATE]
proof (chain)
picking this:
(\<And>pth1 e pth2. \<lbrakk>pth = (pth1 @ [e]) @ pth2; path v (fst (v, p)) (pth1 @ [e]); path (fst (v, p)) t pth2; snd e = (v, p); (v, p) \<notin> snd ` set pth1\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain pth1 e pth2 where "pth = (pth1 @ [e]) @ pth2" "path v t pth2"
[PROOF STATE]
proof (prove)
using this:
(\<And>pth1 e pth2. \<lbrakk>pth = (pth1 @ [e]) @ pth2; path v (fst (v, p)) (pth1 @ [e]); path (fst (v, p)) t pth2; snd e = (v, p); (v, p) \<notin> snd ` set pth1\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>pth1 e pth2. \<lbrakk>pth = (pth1 @ [e]) @ pth2; path v t pth2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis fst_conv)
[PROOF STATE]
proof (state)
this:
pth = (pth1 @ [e]) @ pth2
path v t pth2

goal (1 subgoal):
 1. v \<in> scope (v, p) \<Longrightarrow> False
[PROOF STEP]
from this(2) least
[PROOF STATE]
proof (chain)
picking this:
path v t pth2
\<forall>pth'. path v t pth' \<longrightarrow> length pth \<le> length pth'
[PROOF STEP]
have "length pth \<le> length pth2"
[PROOF STATE]
proof (prove)
using this:
path v t pth2
\<forall>pth'. path v t pth' \<longrightarrow> length pth \<le> length pth'

goal (1 subgoal):
 1. length pth \<le> length pth2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length pth \<le> length pth2

goal (1 subgoal):
 1. v \<in> scope (v, p) \<Longrightarrow> False
[PROOF STEP]
with \<open>pth = _\<close>
[PROOF STATE]
proof (chain)
picking this:
pth = (pth1 @ [e]) @ pth2
length pth \<le> length pth2
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
pth = (pth1 @ [e]) @ pth2
length pth \<le> length pth2

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma scopes_nest:
    fixes ps1 ps2
    shows "scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1 \<or> scope ps1 \<inter> scope ps2 = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1 \<or> scope ps1 \<inter> scope ps2 = {}
[PROOF STEP]
proof(cases "ps1 = ps2")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ps1 = ps2 \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1 \<or> scope ps1 \<inter> scope ps2 = {}
 2. ps1 \<noteq> ps2 \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1 \<or> scope ps1 \<inter> scope ps2 = {}
[PROOF STEP]
assume "ps1 \<noteq> ps2"
[PROOF STATE]
proof (state)
this:
ps1 \<noteq> ps2

goal (2 subgoals):
 1. ps1 = ps2 \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1 \<or> scope ps1 \<inter> scope ps2 = {}
 2. ps1 \<noteq> ps2 \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1 \<or> scope ps1 \<inter> scope ps2 = {}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
ps1 \<noteq> ps2

goal (2 subgoals):
 1. ps1 = ps2 \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1 \<or> scope ps1 \<inter> scope ps2 = {}
 2. ps1 \<noteq> ps2 \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1 \<or> scope ps1 \<inter> scope ps2 = {}
[PROOF STEP]
fix v
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ps1 = ps2 \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1 \<or> scope ps1 \<inter> scope ps2 = {}
 2. ps1 \<noteq> ps2 \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1 \<or> scope ps1 \<inter> scope ps2 = {}
[PROOF STEP]
assume "v \<in> scope ps1 \<inter> scope ps2"
[PROOF STATE]
proof (state)
this:
v \<in> scope ps1 \<inter> scope ps2

goal (2 subgoals):
 1. ps1 = ps2 \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1 \<or> scope ps1 \<inter> scope ps2 = {}
 2. ps1 \<noteq> ps2 \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1 \<or> scope ps1 \<inter> scope ps2 = {}
[PROOF STEP]
hence "v |\<in>| vertices"
[PROOF STATE]
proof (prove)
using this:
v \<in> scope ps1 \<inter> scope ps2

goal (1 subgoal):
 1. v |\<in>| vertices
[PROOF STEP]
using scope.simps
[PROOF STATE]
proof (prove)
using this:
v \<in> scope ps1 \<inter> scope ps2
(?a \<in> scope ?ps) = (\<exists>v. ?a = v \<and> v |\<in>| vertices \<and> (\<forall>x xa. path v xa x \<longrightarrow> terminal_vertex xa \<longrightarrow> ?ps \<in> snd ` set x))

goal (1 subgoal):
 1. v |\<in>| vertices
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v |\<in>| vertices

goal (2 subgoals):
 1. ps1 = ps2 \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1 \<or> scope ps1 \<inter> scope ps2 = {}
 2. ps1 \<noteq> ps2 \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1 \<or> scope ps1 \<inter> scope ps2 = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v |\<in>| vertices
[PROOF STEP]
obtain pth t where "path v t pth" and "terminal_vertex t"
[PROOF STATE]
proof (prove)
using this:
v |\<in>| vertices

goal (1 subgoal):
 1. (\<And>t pth. \<lbrakk>path v t pth; terminal_vertex t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using pruned
[PROOF STATE]
proof (prove)
using this:
v |\<in>| vertices
?v |\<in>| vertices \<Longrightarrow> \<exists>pth v'. path ?v v' pth \<and> terminal_vertex v'

goal (1 subgoal):
 1. (\<And>t pth. \<lbrakk>path v t pth; terminal_vertex t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
path v t pth
terminal_vertex t

goal (2 subgoals):
 1. ps1 = ps2 \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1 \<or> scope ps1 \<inter> scope ps2 = {}
 2. ps1 \<noteq> ps2 \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1 \<or> scope ps1 \<inter> scope ps2 = {}
[PROOF STEP]
from \<open>path v t pth\<close> and \<open>terminal_vertex t\<close> and \<open>v \<in> scope ps1 \<inter> scope ps2\<close>
[PROOF STATE]
proof (chain)
picking this:
path v t pth
terminal_vertex t
v \<in> scope ps1 \<inter> scope ps2
[PROOF STEP]
obtain pth1a e1 pth1b  where "pth = (pth1a@[e1])@pth1b" and "path v (fst ps1) (pth1a@[e1])" and "snd e1 = ps1" and "ps1 \<notin> snd ` set pth1a"
[PROOF STATE]
proof (prove)
using this:
path v t pth
terminal_vertex t
v \<in> scope ps1 \<inter> scope ps2

goal (1 subgoal):
 1. (\<And>pth1a e1 pth1b. \<lbrakk>pth = (pth1a @ [e1]) @ pth1b; path v (fst ps1) (pth1a @ [e1]); snd e1 = ps1; ps1 \<notin> snd ` set pth1a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: scope_split)
[PROOF STATE]
proof (state)
this:
pth = (pth1a @ [e1]) @ pth1b
path v (fst ps1) (pth1a @ [e1])
snd e1 = ps1
ps1 \<notin> snd ` set pth1a

goal (2 subgoals):
 1. ps1 = ps2 \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1 \<or> scope ps1 \<inter> scope ps2 = {}
 2. ps1 \<noteq> ps2 \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1 \<or> scope ps1 \<inter> scope ps2 = {}
[PROOF STEP]
from \<open>path v t pth\<close> and \<open>terminal_vertex t\<close> and \<open>v \<in> scope ps1 \<inter> scope ps2\<close>
[PROOF STATE]
proof (chain)
picking this:
path v t pth
terminal_vertex t
v \<in> scope ps1 \<inter> scope ps2
[PROOF STEP]
obtain pth2a e2 pth2b  where "pth = (pth2a@[e2])@pth2b" and "path v (fst ps2) (pth2a@[e2])" and "snd e2 = ps2" and "ps2 \<notin> snd ` set pth2a"
[PROOF STATE]
proof (prove)
using this:
path v t pth
terminal_vertex t
v \<in> scope ps1 \<inter> scope ps2

goal (1 subgoal):
 1. (\<And>pth2a e2 pth2b. \<lbrakk>pth = (pth2a @ [e2]) @ pth2b; path v (fst ps2) (pth2a @ [e2]); snd e2 = ps2; ps2 \<notin> snd ` set pth2a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: scope_split)
[PROOF STATE]
proof (state)
this:
pth = (pth2a @ [e2]) @ pth2b
path v (fst ps2) (pth2a @ [e2])
snd e2 = ps2
ps2 \<notin> snd ` set pth2a

goal (2 subgoals):
 1. ps1 = ps2 \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1 \<or> scope ps1 \<inter> scope ps2 = {}
 2. ps1 \<noteq> ps2 \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1 \<or> scope ps1 \<inter> scope ps2 = {}
[PROOF STEP]
from \<open>pth = (pth1a@[e1])@pth1b\<close> \<open>pth = (pth2a@[e2])@pth2b\<close>
[PROOF STATE]
proof (chain)
picking this:
pth = (pth1a @ [e1]) @ pth1b
pth = (pth2a @ [e2]) @ pth2b
[PROOF STEP]
have "set pth1a \<subseteq> set pth2a \<or> set pth2a \<subseteq> set pth1a"
[PROOF STATE]
proof (prove)
using this:
pth = (pth1a @ [e1]) @ pth1b
pth = (pth2a @ [e2]) @ pth2b

goal (1 subgoal):
 1. set pth1a \<subseteq> set pth2a \<or> set pth2a \<subseteq> set pth1a
[PROOF STEP]
by (auto simp add: append_eq_append_conv2)
[PROOF STATE]
proof (state)
this:
set pth1a \<subseteq> set pth2a \<or> set pth2a \<subseteq> set pth1a

goal (2 subgoals):
 1. ps1 = ps2 \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1 \<or> scope ps1 \<inter> scope ps2 = {}
 2. ps1 \<noteq> ps2 \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1 \<or> scope ps1 \<inter> scope ps2 = {}
[PROOF STEP]
hence "scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1"
[PROOF STATE]
proof (prove)
using this:
set pth1a \<subseteq> set pth2a \<or> set pth2a \<subseteq> set pth1a

goal (1 subgoal):
 1. scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. set pth1a \<subseteq> set pth2a \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1
 2. set pth2a \<subseteq> set pth1a \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1
[PROOF STEP]
assume "set pth1a \<subseteq> set pth2a"
[PROOF STATE]
proof (state)
this:
set pth1a \<subseteq> set pth2a

goal (2 subgoals):
 1. set pth1a \<subseteq> set pth2a \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1
 2. set pth2a \<subseteq> set pth1a \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1
[PROOF STEP]
with \<open>ps2 \<notin> _\<close>
[PROOF STATE]
proof (chain)
picking this:
ps2 \<notin> snd ` set pth2a
set pth1a \<subseteq> set pth2a
[PROOF STEP]
have "ps2 \<notin> snd ` set (pth1a@[e1])"
[PROOF STATE]
proof (prove)
using this:
ps2 \<notin> snd ` set pth2a
set pth1a \<subseteq> set pth2a

goal (1 subgoal):
 1. ps2 \<notin> snd ` set (pth1a @ [e1])
[PROOF STEP]
using \<open>ps1 \<noteq> ps2\<close> \<open>snd e1 = ps1\<close>
[PROOF STATE]
proof (prove)
using this:
ps2 \<notin> snd ` set pth2a
set pth1a \<subseteq> set pth2a
ps1 \<noteq> ps2
snd e1 = ps1

goal (1 subgoal):
 1. ps2 \<notin> snd ` set (pth1a @ [e1])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ps2 \<notin> snd ` set (pth1a @ [e1])

goal (2 subgoals):
 1. set pth1a \<subseteq> set pth2a \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1
 2. set pth2a \<subseteq> set pth1a \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1
[PROOF STEP]
have "scope ps1 \<subseteq> scope ps2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. scope ps1 \<subseteq> scope ps2
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> scope ps1 \<Longrightarrow> x \<in> scope ps2
[PROOF STEP]
fix v'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> scope ps1 \<Longrightarrow> x \<in> scope ps2
[PROOF STEP]
assume "v' \<in> scope ps1"
[PROOF STATE]
proof (state)
this:
v' \<in> scope ps1

goal (1 subgoal):
 1. \<And>x. x \<in> scope ps1 \<Longrightarrow> x \<in> scope ps2
[PROOF STEP]
hence "v' |\<in>| vertices"
[PROOF STATE]
proof (prove)
using this:
v' \<in> scope ps1

goal (1 subgoal):
 1. v' |\<in>| vertices
[PROOF STEP]
using scope.simps
[PROOF STATE]
proof (prove)
using this:
v' \<in> scope ps1
(?a \<in> scope ?ps) = (\<exists>v. ?a = v \<and> v |\<in>| vertices \<and> (\<forall>x xa. path v xa x \<longrightarrow> terminal_vertex xa \<longrightarrow> ?ps \<in> snd ` set x))

goal (1 subgoal):
 1. v' |\<in>| vertices
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v' |\<in>| vertices

goal (1 subgoal):
 1. \<And>x. x \<in> scope ps1 \<Longrightarrow> x \<in> scope ps2
[PROOF STEP]
thus "v' \<in> scope ps2"
[PROOF STATE]
proof (prove)
using this:
v' |\<in>| vertices

goal (1 subgoal):
 1. v' \<in> scope ps2
[PROOF STEP]
proof(rule scope.intros)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pth v'a. \<lbrakk>path v' v'a pth; terminal_vertex v'a\<rbrakk> \<Longrightarrow> ps2 \<in> snd ` set pth
[PROOF STEP]
fix pth' t'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pth v'a. \<lbrakk>path v' v'a pth; terminal_vertex v'a\<rbrakk> \<Longrightarrow> ps2 \<in> snd ` set pth
[PROOF STEP]
assume "path v' t' pth'" and "terminal_vertex t'"
[PROOF STATE]
proof (state)
this:
path v' t' pth'
terminal_vertex t'

goal (1 subgoal):
 1. \<And>pth v'a. \<lbrakk>path v' v'a pth; terminal_vertex v'a\<rbrakk> \<Longrightarrow> ps2 \<in> snd ` set pth
[PROOF STEP]
with \<open>v' \<in> scope ps1\<close>
[PROOF STATE]
proof (chain)
picking this:
v' \<in> scope ps1
path v' t' pth'
terminal_vertex t'
[PROOF STEP]
obtain pth3a e3 pth3b where "pth' = (pth3a@[e3])@pth3b" and "path (fst ps1) t' pth3b"
[PROOF STATE]
proof (prove)
using this:
v' \<in> scope ps1
path v' t' pth'
terminal_vertex t'

goal (1 subgoal):
 1. (\<And>pth3a e3 pth3b. \<lbrakk>pth' = (pth3a @ [e3]) @ pth3b; path (fst ps1) t' pth3b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: scope_split)
[PROOF STATE]
proof (state)
this:
pth' = (pth3a @ [e3]) @ pth3b
path (fst ps1) t' pth3b

goal (1 subgoal):
 1. \<And>pth v'a. \<lbrakk>path v' v'a pth; terminal_vertex v'a\<rbrakk> \<Longrightarrow> ps2 \<in> snd ` set pth
[PROOF STEP]
have "path v t' ((pth1a@[e1]) @ pth3b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path v t' ((pth1a @ [e1]) @ pth3b)
[PROOF STEP]
using \<open>path v (fst ps1) (pth1a@[e1])\<close> and \<open>path (fst ps1) t' pth3b\<close>
[PROOF STATE]
proof (prove)
using this:
path v (fst ps1) (pth1a @ [e1])
path (fst ps1) t' pth3b

goal (1 subgoal):
 1. path v t' ((pth1a @ [e1]) @ pth3b)
[PROOF STEP]
by (rule path_appendI)
[PROOF STATE]
proof (state)
this:
path v t' ((pth1a @ [e1]) @ pth3b)

goal (1 subgoal):
 1. \<And>pth v'a. \<lbrakk>path v' v'a pth; terminal_vertex v'a\<rbrakk> \<Longrightarrow> ps2 \<in> snd ` set pth
[PROOF STEP]
with \<open>terminal_vertex t'\<close> \<open>v \<in> _\<close>
[PROOF STATE]
proof (chain)
picking this:
terminal_vertex t'
v \<in> scope ps1 \<inter> scope ps2
path v t' ((pth1a @ [e1]) @ pth3b)
[PROOF STEP]
have "ps2 \<in> snd ` set ((pth1a@[e1]) @ pth3b)"
[PROOF STATE]
proof (prove)
using this:
terminal_vertex t'
v \<in> scope ps1 \<inter> scope ps2
path v t' ((pth1a @ [e1]) @ pth3b)

goal (1 subgoal):
 1. ps2 \<in> snd ` set ((pth1a @ [e1]) @ pth3b)
[PROOF STEP]
by (meson IntD2 scope.cases)
[PROOF STATE]
proof (state)
this:
ps2 \<in> snd ` set ((pth1a @ [e1]) @ pth3b)

goal (1 subgoal):
 1. \<And>pth v'a. \<lbrakk>path v' v'a pth; terminal_vertex v'a\<rbrakk> \<Longrightarrow> ps2 \<in> snd ` set pth
[PROOF STEP]
hence "ps2 \<in> snd ` set pth3b"
[PROOF STATE]
proof (prove)
using this:
ps2 \<in> snd ` set ((pth1a @ [e1]) @ pth3b)

goal (1 subgoal):
 1. ps2 \<in> snd ` set pth3b
[PROOF STEP]
using \<open>ps2 \<notin> snd ` set (pth1a@[e1])\<close>
[PROOF STATE]
proof (prove)
using this:
ps2 \<in> snd ` set ((pth1a @ [e1]) @ pth3b)
ps2 \<notin> snd ` set (pth1a @ [e1])

goal (1 subgoal):
 1. ps2 \<in> snd ` set pth3b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ps2 \<in> snd ` set pth3b

goal (1 subgoal):
 1. \<And>pth v'a. \<lbrakk>path v' v'a pth; terminal_vertex v'a\<rbrakk> \<Longrightarrow> ps2 \<in> snd ` set pth
[PROOF STEP]
thus "ps2 \<in> snd ` set pth'"
[PROOF STATE]
proof (prove)
using this:
ps2 \<in> snd ` set pth3b

goal (1 subgoal):
 1. ps2 \<in> snd ` set pth'
[PROOF STEP]
using \<open>pth'=_\<close>
[PROOF STATE]
proof (prove)
using this:
ps2 \<in> snd ` set pth3b
pth' = (pth3a @ [e3]) @ pth3b

goal (1 subgoal):
 1. ps2 \<in> snd ` set pth'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ps2 \<in> snd ` set pth'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
v' \<in> scope ps2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
scope ps1 \<subseteq> scope ps2

goal (2 subgoals):
 1. set pth1a \<subseteq> set pth2a \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1
 2. set pth2a \<subseteq> set pth1a \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
scope ps1 \<subseteq> scope ps2

goal (1 subgoal):
 1. scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1

goal (1 subgoal):
 1. set pth2a \<subseteq> set pth1a \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set pth2a \<subseteq> set pth1a \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1
[PROOF STEP]
assume "set pth2a \<subseteq> set pth1a"
[PROOF STATE]
proof (state)
this:
set pth2a \<subseteq> set pth1a

goal (1 subgoal):
 1. set pth2a \<subseteq> set pth1a \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1
[PROOF STEP]
with \<open>ps1 \<notin> _\<close>
[PROOF STATE]
proof (chain)
picking this:
ps1 \<notin> snd ` set pth1a
set pth2a \<subseteq> set pth1a
[PROOF STEP]
have "ps1 \<notin> snd ` set (pth2a@[e2])"
[PROOF STATE]
proof (prove)
using this:
ps1 \<notin> snd ` set pth1a
set pth2a \<subseteq> set pth1a

goal (1 subgoal):
 1. ps1 \<notin> snd ` set (pth2a @ [e2])
[PROOF STEP]
using \<open>ps1 \<noteq> ps2\<close> \<open>snd e2 = ps2\<close>
[PROOF STATE]
proof (prove)
using this:
ps1 \<notin> snd ` set pth1a
set pth2a \<subseteq> set pth1a
ps1 \<noteq> ps2
snd e2 = ps2

goal (1 subgoal):
 1. ps1 \<notin> snd ` set (pth2a @ [e2])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ps1 \<notin> snd ` set (pth2a @ [e2])

goal (1 subgoal):
 1. set pth2a \<subseteq> set pth1a \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1
[PROOF STEP]
have "scope ps2 \<subseteq> scope ps1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. scope ps2 \<subseteq> scope ps1
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> scope ps2 \<Longrightarrow> x \<in> scope ps1
[PROOF STEP]
fix v'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> scope ps2 \<Longrightarrow> x \<in> scope ps1
[PROOF STEP]
assume "v' \<in> scope ps2"
[PROOF STATE]
proof (state)
this:
v' \<in> scope ps2

goal (1 subgoal):
 1. \<And>x. x \<in> scope ps2 \<Longrightarrow> x \<in> scope ps1
[PROOF STEP]
hence "v' |\<in>| vertices"
[PROOF STATE]
proof (prove)
using this:
v' \<in> scope ps2

goal (1 subgoal):
 1. v' |\<in>| vertices
[PROOF STEP]
using scope.simps
[PROOF STATE]
proof (prove)
using this:
v' \<in> scope ps2
(?a \<in> scope ?ps) = (\<exists>v. ?a = v \<and> v |\<in>| vertices \<and> (\<forall>x xa. path v xa x \<longrightarrow> terminal_vertex xa \<longrightarrow> ?ps \<in> snd ` set x))

goal (1 subgoal):
 1. v' |\<in>| vertices
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v' |\<in>| vertices

goal (1 subgoal):
 1. \<And>x. x \<in> scope ps2 \<Longrightarrow> x \<in> scope ps1
[PROOF STEP]
thus "v' \<in> scope ps1"
[PROOF STATE]
proof (prove)
using this:
v' |\<in>| vertices

goal (1 subgoal):
 1. v' \<in> scope ps1
[PROOF STEP]
proof(rule scope.intros)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pth v'a. \<lbrakk>path v' v'a pth; terminal_vertex v'a\<rbrakk> \<Longrightarrow> ps1 \<in> snd ` set pth
[PROOF STEP]
fix pth' t'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pth v'a. \<lbrakk>path v' v'a pth; terminal_vertex v'a\<rbrakk> \<Longrightarrow> ps1 \<in> snd ` set pth
[PROOF STEP]
assume "path v' t' pth'" and "terminal_vertex t'"
[PROOF STATE]
proof (state)
this:
path v' t' pth'
terminal_vertex t'

goal (1 subgoal):
 1. \<And>pth v'a. \<lbrakk>path v' v'a pth; terminal_vertex v'a\<rbrakk> \<Longrightarrow> ps1 \<in> snd ` set pth
[PROOF STEP]
with \<open>v' \<in> scope ps2\<close>
[PROOF STATE]
proof (chain)
picking this:
v' \<in> scope ps2
path v' t' pth'
terminal_vertex t'
[PROOF STEP]
obtain pth3a e3 pth3b where "pth' = (pth3a@[e3])@pth3b" and "path (fst ps2) t' pth3b"
[PROOF STATE]
proof (prove)
using this:
v' \<in> scope ps2
path v' t' pth'
terminal_vertex t'

goal (1 subgoal):
 1. (\<And>pth3a e3 pth3b. \<lbrakk>pth' = (pth3a @ [e3]) @ pth3b; path (fst ps2) t' pth3b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: scope_split)
[PROOF STATE]
proof (state)
this:
pth' = (pth3a @ [e3]) @ pth3b
path (fst ps2) t' pth3b

goal (1 subgoal):
 1. \<And>pth v'a. \<lbrakk>path v' v'a pth; terminal_vertex v'a\<rbrakk> \<Longrightarrow> ps1 \<in> snd ` set pth
[PROOF STEP]
have "path v t' ((pth2a@[e2]) @ pth3b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path v t' ((pth2a @ [e2]) @ pth3b)
[PROOF STEP]
using \<open>path v (fst ps2) (pth2a@[e2])\<close> and \<open>path (fst ps2) t' pth3b\<close>
[PROOF STATE]
proof (prove)
using this:
path v (fst ps2) (pth2a @ [e2])
path (fst ps2) t' pth3b

goal (1 subgoal):
 1. path v t' ((pth2a @ [e2]) @ pth3b)
[PROOF STEP]
by (rule path_appendI)
[PROOF STATE]
proof (state)
this:
path v t' ((pth2a @ [e2]) @ pth3b)

goal (1 subgoal):
 1. \<And>pth v'a. \<lbrakk>path v' v'a pth; terminal_vertex v'a\<rbrakk> \<Longrightarrow> ps1 \<in> snd ` set pth
[PROOF STEP]
with \<open>terminal_vertex t'\<close> \<open>v \<in> _\<close>
[PROOF STATE]
proof (chain)
picking this:
terminal_vertex t'
v \<in> scope ps1 \<inter> scope ps2
path v t' ((pth2a @ [e2]) @ pth3b)
[PROOF STEP]
have "ps1 \<in> snd ` set ((pth2a@[e2]) @ pth3b)"
[PROOF STATE]
proof (prove)
using this:
terminal_vertex t'
v \<in> scope ps1 \<inter> scope ps2
path v t' ((pth2a @ [e2]) @ pth3b)

goal (1 subgoal):
 1. ps1 \<in> snd ` set ((pth2a @ [e2]) @ pth3b)
[PROOF STEP]
by (meson IntD1 scope.cases)
[PROOF STATE]
proof (state)
this:
ps1 \<in> snd ` set ((pth2a @ [e2]) @ pth3b)

goal (1 subgoal):
 1. \<And>pth v'a. \<lbrakk>path v' v'a pth; terminal_vertex v'a\<rbrakk> \<Longrightarrow> ps1 \<in> snd ` set pth
[PROOF STEP]
hence "ps1 \<in> snd ` set pth3b"
[PROOF STATE]
proof (prove)
using this:
ps1 \<in> snd ` set ((pth2a @ [e2]) @ pth3b)

goal (1 subgoal):
 1. ps1 \<in> snd ` set pth3b
[PROOF STEP]
using \<open>ps1 \<notin> snd ` set (pth2a@[e2])\<close>
[PROOF STATE]
proof (prove)
using this:
ps1 \<in> snd ` set ((pth2a @ [e2]) @ pth3b)
ps1 \<notin> snd ` set (pth2a @ [e2])

goal (1 subgoal):
 1. ps1 \<in> snd ` set pth3b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ps1 \<in> snd ` set pth3b

goal (1 subgoal):
 1. \<And>pth v'a. \<lbrakk>path v' v'a pth; terminal_vertex v'a\<rbrakk> \<Longrightarrow> ps1 \<in> snd ` set pth
[PROOF STEP]
thus "ps1 \<in> snd ` set pth'"
[PROOF STATE]
proof (prove)
using this:
ps1 \<in> snd ` set pth3b

goal (1 subgoal):
 1. ps1 \<in> snd ` set pth'
[PROOF STEP]
using \<open>pth'=_\<close>
[PROOF STATE]
proof (prove)
using this:
ps1 \<in> snd ` set pth3b
pth' = (pth3a @ [e3]) @ pth3b

goal (1 subgoal):
 1. ps1 \<in> snd ` set pth'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ps1 \<in> snd ` set pth'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
v' \<in> scope ps1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
scope ps2 \<subseteq> scope ps1

goal (1 subgoal):
 1. set pth2a \<subseteq> set pth1a \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
scope ps2 \<subseteq> scope ps1

goal (1 subgoal):
 1. scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1

goal (2 subgoals):
 1. ps1 = ps2 \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1 \<or> scope ps1 \<inter> scope ps2 = {}
 2. ps1 \<noteq> ps2 \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1 \<or> scope ps1 \<inter> scope ps2 = {}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?v2 \<in> scope ps1 \<inter> scope ps2 \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1

goal (2 subgoals):
 1. ps1 = ps2 \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1 \<or> scope ps1 \<inter> scope ps2 = {}
 2. ps1 \<noteq> ps2 \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1 \<or> scope ps1 \<inter> scope ps2 = {}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?v2 \<in> scope ps1 \<inter> scope ps2 \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1

goal (1 subgoal):
 1. scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1 \<or> scope ps1 \<inter> scope ps2 = {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1 \<or> scope ps1 \<inter> scope ps2 = {}

goal (1 subgoal):
 1. ps1 = ps2 \<Longrightarrow> scope ps1 \<subseteq> scope ps2 \<or> scope ps2 \<subseteq> scope ps1 \<or> scope ps1 \<inter> scope ps2 = {}
[PROOF STEP]
qed simp


[STATEMENT]
lemma hyps_free_Nil[simp]: "hyps_free []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hyps_free []
[PROOF STEP]
by (simp add: hyps_free_def)


[STATEMENT]
lemma hyps_free_Cons[simp]: "hyps_free (e#pth) \<longleftrightarrow> hyps_free pth \<and> hyps (nodeOf (fst (fst e))) (snd (fst e)) = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hyps_free (e # pth) = (hyps_free pth \<and> hyps (nodeOf (fst (fst e))) (snd (fst e)) = None)
[PROOF STEP]
by (auto simp add: hyps_free_def) (metis prod.collapse)


[STATEMENT]
lemma path_vertices_shift:
  assumes "path v v' pth"
  shows "map fst (map fst pth)@[v'] = v#map fst (map snd pth)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map fst (map fst pth) @ [v'] = v # map fst (map snd pth)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
path v v' pth

goal (1 subgoal):
 1. map fst (map fst pth) @ [v'] = v # map fst (map snd pth)
[PROOF STEP]
by induction auto


[STATEMENT]
lemma terminal_path_is_path:
  assumes "terminal_path v v' pth"
  shows "path v v' pth"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path v v' pth
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
terminal_path v v' pth

goal (1 subgoal):
 1. path v v' pth
[PROOF STEP]
by induction (auto simp add: path_cons_simp)


[STATEMENT]
lemma terminal_path_is_hyps_free:
  assumes "terminal_path v v' pth"
  shows "hyps_free pth"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hyps_free pth
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
terminal_path v v' pth

goal (1 subgoal):
 1. hyps_free pth
[PROOF STEP]
by induction (auto simp add: hyps_free_def)


[STATEMENT]
lemma terminal_path_end_is_terminal:
  assumes "terminal_path v v' pth"
  shows "terminal_vertex v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. terminal_vertex v'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
terminal_path v v' pth

goal (1 subgoal):
 1. terminal_vertex v'
[PROOF STEP]
by induction


[STATEMENT]
lemma terminal_pathI:
  assumes "path v v' pth"
  assumes "hyps_free pth"
  assumes "terminal_vertex v'"
  shows "terminal_path v v' pth"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. terminal_path v v' pth
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
path v v' pth
hyps_free pth
terminal_vertex v'

goal (1 subgoal):
 1. terminal_path v v' pth
[PROOF STEP]
by induction (auto intro: terminal_path.intros)


[STATEMENT]
lemma hyps_free_vertices_distinct:
  assumes "terminal_path v v' pth"
  shows "distinct (map fst (map fst pth)@[v'])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map fst (map fst pth) @ [v'])
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
terminal_path v v' pth

goal (1 subgoal):
 1. distinct (map fst (map fst pth) @ [v'])
[PROOF STEP]
proof(induction v v' pth)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v. terminal_vertex v \<Longrightarrow> distinct (map fst (map fst []) @ [v])
 2. \<And>v\<^sub>1 p\<^sub>1 v\<^sub>2 p\<^sub>2 v' pth. \<lbrakk>((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) \<in> edges; terminal_path v\<^sub>2 v' pth; distinct (map fst (map fst pth) @ [v']); hyps (nodeOf v\<^sub>1) p\<^sub>1 = None\<rbrakk> \<Longrightarrow> distinct (map fst (map fst (((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) # pth)) @ [v'])
[PROOF STEP]
case terminal_path_empty
[PROOF STATE]
proof (state)
this:
terminal_vertex v_

goal (2 subgoals):
 1. \<And>v. terminal_vertex v \<Longrightarrow> distinct (map fst (map fst []) @ [v])
 2. \<And>v\<^sub>1 p\<^sub>1 v\<^sub>2 p\<^sub>2 v' pth. \<lbrakk>((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) \<in> edges; terminal_path v\<^sub>2 v' pth; distinct (map fst (map fst pth) @ [v']); hyps (nodeOf v\<^sub>1) p\<^sub>1 = None\<rbrakk> \<Longrightarrow> distinct (map fst (map fst (((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) # pth)) @ [v'])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map fst (map fst []) @ [v_])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct (map fst (map fst []) @ [v_])

goal (1 subgoal):
 1. \<And>v\<^sub>1 p\<^sub>1 v\<^sub>2 p\<^sub>2 v' pth. \<lbrakk>((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) \<in> edges; terminal_path v\<^sub>2 v' pth; distinct (map fst (map fst pth) @ [v']); hyps (nodeOf v\<^sub>1) p\<^sub>1 = None\<rbrakk> \<Longrightarrow> distinct (map fst (map fst (((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) # pth)) @ [v'])
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v\<^sub>1 p\<^sub>1 v\<^sub>2 p\<^sub>2 v' pth. \<lbrakk>((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) \<in> edges; terminal_path v\<^sub>2 v' pth; distinct (map fst (map fst pth) @ [v']); hyps (nodeOf v\<^sub>1) p\<^sub>1 = None\<rbrakk> \<Longrightarrow> distinct (map fst (map fst (((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) # pth)) @ [v'])
[PROOF STEP]
case (terminal_path_cons v\<^sub>1 p\<^sub>1 v\<^sub>2 p\<^sub>2 v' pth)
[PROOF STATE]
proof (state)
this:
((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) \<in> edges
terminal_path v\<^sub>2 v' pth
hyps (nodeOf v\<^sub>1) p\<^sub>1 = None
distinct (map fst (map fst pth) @ [v'])

goal (1 subgoal):
 1. \<And>v\<^sub>1 p\<^sub>1 v\<^sub>2 p\<^sub>2 v' pth. \<lbrakk>((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) \<in> edges; terminal_path v\<^sub>2 v' pth; distinct (map fst (map fst pth) @ [v']); hyps (nodeOf v\<^sub>1) p\<^sub>1 = None\<rbrakk> \<Longrightarrow> distinct (map fst (map fst (((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) # pth)) @ [v'])
[PROOF STEP]
note terminal_path_cons.IH
[PROOF STATE]
proof (state)
this:
distinct (map fst (map fst pth) @ [v'])

goal (1 subgoal):
 1. \<And>v\<^sub>1 p\<^sub>1 v\<^sub>2 p\<^sub>2 v' pth. \<lbrakk>((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) \<in> edges; terminal_path v\<^sub>2 v' pth; distinct (map fst (map fst pth) @ [v']); hyps (nodeOf v\<^sub>1) p\<^sub>1 = None\<rbrakk> \<Longrightarrow> distinct (map fst (map fst (((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) # pth)) @ [v'])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distinct (map fst (map fst pth) @ [v'])

goal (1 subgoal):
 1. \<And>v\<^sub>1 p\<^sub>1 v\<^sub>2 p\<^sub>2 v' pth. \<lbrakk>((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) \<in> edges; terminal_path v\<^sub>2 v' pth; distinct (map fst (map fst pth) @ [v']); hyps (nodeOf v\<^sub>1) p\<^sub>1 = None\<rbrakk> \<Longrightarrow> distinct (map fst (map fst (((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) # pth)) @ [v'])
[PROOF STEP]
have "v\<^sub>1 \<notin> fst ` fst ` set pth"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v\<^sub>1 \<notin> fst ` fst ` set pth
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v\<^sub>1 \<in> fst ` fst ` set pth \<Longrightarrow> False
[PROOF STEP]
assume "v\<^sub>1 \<in> fst ` fst ` set pth"
[PROOF STATE]
proof (state)
this:
v\<^sub>1 \<in> fst ` fst ` set pth

goal (1 subgoal):
 1. v\<^sub>1 \<in> fst ` fst ` set pth \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v\<^sub>1 \<in> fst ` fst ` set pth
[PROOF STEP]
obtain pth1 e' pth2 where "pth = pth1@[e']@pth2" and "v\<^sub>1 = fst (fst e')"
[PROOF STATE]
proof (prove)
using this:
v\<^sub>1 \<in> fst ` fst ` set pth

goal (1 subgoal):
 1. (\<And>pth1 e' pth2. \<lbrakk>pth = pth1 @ [e'] @ pth2; v\<^sub>1 = fst (fst e')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (atomize_elim)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v\<^sub>1 \<in> fst ` fst ` set pth \<Longrightarrow> \<exists>pth1 e' pth2. pth = pth1 @ [e'] @ pth2 \<and> v\<^sub>1 = fst (fst e')
[PROOF STEP]
apply (induction pth)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. v\<^sub>1 \<in> fst ` fst ` set [] \<Longrightarrow> \<exists>pth1 e' pth2. [] = pth1 @ [e'] @ pth2 \<and> v\<^sub>1 = fst (fst e')
 2. \<And>a pth. \<lbrakk>v\<^sub>1 \<in> fst ` fst ` set pth \<Longrightarrow> \<exists>pth1 e' pth2. pth = pth1 @ [e'] @ pth2 \<and> v\<^sub>1 = fst (fst e'); v\<^sub>1 \<in> fst ` fst ` set (a # pth)\<rbrakk> \<Longrightarrow> \<exists>pth1 e' pth2. a # pth = pth1 @ [e'] @ pth2 \<and> v\<^sub>1 = fst (fst e')
[PROOF STEP]
apply (solves simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a pth. \<lbrakk>v\<^sub>1 \<in> fst ` fst ` set pth \<Longrightarrow> \<exists>pth1 e' pth2. pth = pth1 @ [e'] @ pth2 \<and> v\<^sub>1 = fst (fst e'); v\<^sub>1 \<in> fst ` fst ` set (a # pth)\<rbrakk> \<Longrightarrow> \<exists>pth1 e' pth2. a # pth = pth1 @ [e'] @ pth2 \<and> v\<^sub>1 = fst (fst e')
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b aa ba pth. (v\<^sub>1 \<in> fst ` fst ` set pth \<Longrightarrow> \<exists>pth1 b a ba pth2. pth = pth1 @ ((v\<^sub>1, b), a, ba) # pth2) \<Longrightarrow> \<exists>pth1 bb a bc pth2. ((v\<^sub>1, b), aa, ba) # pth = pth1 @ ((v\<^sub>1, bb), a, bc) # pth2
 2. \<And>a b aa ba pth bb ad bc. \<lbrakk>v\<^sub>1 \<in> fst ` fst ` set pth \<Longrightarrow> \<exists>pth1 b a ba pth2. pth = pth1 @ ((v\<^sub>1, b), a, ba) # pth2; ((v\<^sub>1, bb), ad, bc) \<in> set pth\<rbrakk> \<Longrightarrow> \<exists>pth1 bb ab bc pth2. ((a, b), aa, ba) # pth = pth1 @ ((v\<^sub>1, bb), ab, bc) # pth2
[PROOF STEP]
apply (solves \<open>rule exI[where x = "[]"]; simp\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba pth bb ad bc. \<lbrakk>v\<^sub>1 \<in> fst ` fst ` set pth \<Longrightarrow> \<exists>pth1 b a ba pth2. pth = pth1 @ ((v\<^sub>1, b), a, ba) # pth2; ((v\<^sub>1, bb), ad, bc) \<in> set pth\<rbrakk> \<Longrightarrow> \<exists>pth1 bb ab bc pth2. ((a, b), aa, ba) # pth = pth1 @ ((v\<^sub>1, bb), ab, bc) # pth2
[PROOF STEP]
apply (metis Cons_eq_appendI image_eqI prod.sel(1))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
pth = pth1 @ [e'] @ pth2
v\<^sub>1 = fst (fst e')

goal (1 subgoal):
 1. v\<^sub>1 \<in> fst ` fst ` set pth \<Longrightarrow> False
[PROOF STEP]
with terminal_path_is_path[OF \<open>terminal_path v\<^sub>2 v' pth\<close>]
[PROOF STATE]
proof (chain)
picking this:
path v\<^sub>2 v' pth
pth = pth1 @ [e'] @ pth2
v\<^sub>1 = fst (fst e')
[PROOF STEP]
have "path v\<^sub>2 v\<^sub>1 pth1"
[PROOF STATE]
proof (prove)
using this:
path v\<^sub>2 v' pth
pth = pth1 @ [e'] @ pth2
v\<^sub>1 = fst (fst e')

goal (1 subgoal):
 1. path v\<^sub>2 v\<^sub>1 pth1
[PROOF STEP]
by (simp add:  path_split2 edge_begin_tup)
[PROOF STATE]
proof (state)
this:
path v\<^sub>2 v\<^sub>1 pth1

goal (1 subgoal):
 1. v\<^sub>1 \<in> fst ` fst ` set pth \<Longrightarrow> False
[PROOF STEP]
with \<open>((v\<^sub>1, p\<^sub>1), (v\<^sub>2, p\<^sub>2)) \<in> _\<close>
[PROOF STATE]
proof (chain)
picking this:
((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) \<in> edges
path v\<^sub>2 v\<^sub>1 pth1
[PROOF STEP]
have "path v\<^sub>1 v\<^sub>1 (((v\<^sub>1, p\<^sub>1), (v\<^sub>2, p\<^sub>2)) # pth1)"
[PROOF STATE]
proof (prove)
using this:
((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) \<in> edges
path v\<^sub>2 v\<^sub>1 pth1

goal (1 subgoal):
 1. path v\<^sub>1 v\<^sub>1 (((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) # pth1)
[PROOF STEP]
by (simp add: path_cons_simp)
[PROOF STATE]
proof (state)
this:
path v\<^sub>1 v\<^sub>1 (((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) # pth1)

goal (1 subgoal):
 1. v\<^sub>1 \<in> fst ` fst ` set pth \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
path v\<^sub>1 v\<^sub>1 (((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) # pth1)

goal (1 subgoal):
 1. v\<^sub>1 \<in> fst ` fst ` set pth \<Longrightarrow> False
[PROOF STEP]
from terminal_path_is_hyps_free[OF \<open>terminal_path v\<^sub>2 v' pth\<close>]
         \<open>hyps (nodeOf v\<^sub>1) p\<^sub>1 = None\<close>
         \<open>pth = pth1@[e']@pth2\<close>
[PROOF STATE]
proof (chain)
picking this:
hyps_free pth
hyps (nodeOf v\<^sub>1) p\<^sub>1 = None
pth = pth1 @ [e'] @ pth2
[PROOF STEP]
have "hyps_free(((v\<^sub>1, p\<^sub>1), (v\<^sub>2, p\<^sub>2)) # pth1)"
[PROOF STATE]
proof (prove)
using this:
hyps_free pth
hyps (nodeOf v\<^sub>1) p\<^sub>1 = None
pth = pth1 @ [e'] @ pth2

goal (1 subgoal):
 1. hyps_free (((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) # pth1)
[PROOF STEP]
by (auto simp add: hyps_free_def)
[PROOF STATE]
proof (state)
this:
hyps_free (((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) # pth1)

goal (1 subgoal):
 1. v\<^sub>1 \<in> fst ` fst ` set pth \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
path v\<^sub>1 v\<^sub>1 (((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) # pth1)
hyps_free (((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) # pth1)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
path v\<^sub>1 v\<^sub>1 (((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) # pth1)
hyps_free (((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) # pth1)

goal (1 subgoal):
 1. False
[PROOF STEP]
using hyps_free_acyclic
[PROOF STATE]
proof (prove)
using this:
path v\<^sub>1 v\<^sub>1 (((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) # pth1)
hyps_free (((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) # pth1)
\<lbrakk>path ?v ?v ?pth; hyps_free ?pth\<rbrakk> \<Longrightarrow> ?pth = []

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:
v\<^sub>1 \<notin> fst ` fst ` set pth

goal (1 subgoal):
 1. \<And>v\<^sub>1 p\<^sub>1 v\<^sub>2 p\<^sub>2 v' pth. \<lbrakk>((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) \<in> edges; terminal_path v\<^sub>2 v' pth; distinct (map fst (map fst pth) @ [v']); hyps (nodeOf v\<^sub>1) p\<^sub>1 = None\<rbrakk> \<Longrightarrow> distinct (map fst (map fst (((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) # pth)) @ [v'])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v\<^sub>1 \<notin> fst ` fst ` set pth

goal (1 subgoal):
 1. \<And>v\<^sub>1 p\<^sub>1 v\<^sub>2 p\<^sub>2 v' pth. \<lbrakk>((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) \<in> edges; terminal_path v\<^sub>2 v' pth; distinct (map fst (map fst pth) @ [v']); hyps (nodeOf v\<^sub>1) p\<^sub>1 = None\<rbrakk> \<Longrightarrow> distinct (map fst (map fst (((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) # pth)) @ [v'])
[PROOF STEP]
have "v\<^sub>1 \<noteq> v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v\<^sub>1 \<noteq> v'
[PROOF STEP]
using hyps_free_acyclic path_cons terminal_path_cons.hyps(1) terminal_path_cons.hyps(2) terminal_path_cons.hyps(3) terminal_path_is_hyps_free terminal_path_is_path
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>path ?v ?v ?pth; hyps_free ?pth\<rbrakk> \<Longrightarrow> ?pth = []
\<lbrakk>?e \<in> edges; path (edge_end ?e) ?v' ?pth\<rbrakk> \<Longrightarrow> path (edge_begin ?e) ?v' (?e # ?pth)
((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) \<in> edges
terminal_path v\<^sub>2 v' pth
hyps (nodeOf v\<^sub>1) p\<^sub>1 = None
terminal_path ?v ?v' ?pth \<Longrightarrow> hyps_free ?pth
terminal_path ?v ?v' ?pth \<Longrightarrow> path ?v ?v' ?pth

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

goal (1 subgoal):
 1. \<And>v\<^sub>1 p\<^sub>1 v\<^sub>2 p\<^sub>2 v' pth. \<lbrakk>((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) \<in> edges; terminal_path v\<^sub>2 v' pth; distinct (map fst (map fst pth) @ [v']); hyps (nodeOf v\<^sub>1) p\<^sub>1 = None\<rbrakk> \<Longrightarrow> distinct (map fst (map fst (((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) # pth)) @ [v'])
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
distinct (map fst (map fst pth) @ [v'])
v\<^sub>1 \<notin> fst ` fst ` set pth
v\<^sub>1 \<noteq> v'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
distinct (map fst (map fst pth) @ [v'])
v\<^sub>1 \<notin> fst ` fst ` set pth
v\<^sub>1 \<noteq> v'

goal (1 subgoal):
 1. distinct (map fst (map fst (((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) # pth)) @ [v'])
[PROOF STEP]
by (auto simp add: comp_def)
[PROOF STATE]
proof (state)
this:
distinct (map fst (map fst (((v\<^sub>1, p\<^sub>1), v\<^sub>2, p\<^sub>2) # pth)) @ [v'])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hyps_free_vertices_distinct':
  assumes "terminal_path v v' pth"
  shows "distinct (v # map fst (map snd pth))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (v # map fst (map snd pth))
[PROOF STEP]
using hyps_free_vertices_distinct[OF assms]
[PROOF STATE]
proof (prove)
using this:
distinct (map fst (map fst pth) @ [v'])

goal (1 subgoal):
 1. distinct (v # map fst (map snd pth))
[PROOF STEP]
unfolding path_vertices_shift[OF terminal_path_is_path[OF assms]]
[PROOF STATE]
proof (prove)
using this:
distinct (v # map fst (map snd pth))

goal (1 subgoal):
 1. distinct (v # map fst (map snd pth))
[PROOF STEP]
.


[STATEMENT]
lemma hyps_free_limited:
  assumes "terminal_path v v' pth"
  shows "length pth \<le> fcard vertices"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length pth \<le> fcard vertices
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length pth \<le> fcard vertices
[PROOF STEP]
have "length pth = length (map fst (map fst pth))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length pth = length (map fst (map fst pth))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length pth = length (map fst (map fst pth))

goal (1 subgoal):
 1. length pth \<le> fcard vertices
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
length pth = length (map fst (map fst pth))

goal (1 subgoal):
 1. length pth \<le> fcard vertices
[PROOF STEP]
from hyps_free_vertices_distinct[OF assms]
[PROOF STATE]
proof (chain)
picking this:
distinct (map fst (map fst pth) @ [v'])
[PROOF STEP]
have "distinct (map fst (map fst pth))"
[PROOF STATE]
proof (prove)
using this:
distinct (map fst (map fst pth) @ [v'])

goal (1 subgoal):
 1. distinct (map fst (map fst pth))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct (map fst (map fst pth))

goal (1 subgoal):
 1. length pth \<le> fcard vertices
[PROOF STEP]
hence "length (map fst (map fst pth)) = card (set (map fst (map fst pth)))"
[PROOF STATE]
proof (prove)
using this:
distinct (map fst (map fst pth))

goal (1 subgoal):
 1. length (map fst (map fst pth)) = card (set (map fst (map fst pth)))
[PROOF STEP]
by (rule distinct_card[symmetric])
[PROOF STATE]
proof (state)
this:
length (map fst (map fst pth)) = card (set (map fst (map fst pth)))

goal (1 subgoal):
 1. length pth \<le> fcard vertices
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
length (map fst (map fst pth)) = card (set (map fst (map fst pth)))

goal (1 subgoal):
 1. length pth \<le> fcard vertices
[PROOF STEP]
have "\<dots> \<le> card (fset vertices)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (set (map fst (map fst pth))) \<le> card (fset vertices)
[PROOF STEP]
proof (rule card_mono[OF finite_fset])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (map fst (map fst pth)) \<subseteq> fset vertices
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
terminal_path v v' pth
[PROOF STEP]
show "set (map fst (map fst pth)) \<subseteq> fset vertices"
[PROOF STATE]
proof (prove)
using this:
terminal_path v v' pth

goal (1 subgoal):
 1. set (map fst (map fst pth)) \<subseteq> fset vertices
[PROOF STEP]
by (induction v v' pth) (auto, metis valid_edges notin_fset case_prodD valid_out_port.simps)
[PROOF STATE]
proof (state)
this:
set (map fst (map fst pth)) \<subseteq> fset vertices

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card (set (map fst (map fst pth))) \<le> card (fset vertices)

goal (1 subgoal):
 1. length pth \<le> fcard vertices
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (set (map fst (map fst pth))) \<le> card (fset vertices)

goal (1 subgoal):
 1. length pth \<le> fcard vertices
[PROOF STEP]
have "\<dots> = fcard vertices"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (fset vertices) = fcard vertices
[PROOF STEP]
by (simp add: fcard.rep_eq)
[PROOF STATE]
proof (state)
this:
card (fset vertices) = fcard vertices

goal (1 subgoal):
 1. length pth \<le> fcard vertices
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
length pth \<le> fcard vertices
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length pth \<le> fcard vertices

goal (1 subgoal):
 1. length pth \<le> fcard vertices
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
length pth \<le> fcard vertices

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hyps_free_path_not_in_scope:
  assumes "terminal_path v t pth"
  assumes "(v',p') \<in> snd ` set pth"
  shows   "v' \<notin> scope (v, p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v' \<notin> scope (v, p)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v' \<in> scope (v, p) \<Longrightarrow> False
[PROOF STEP]
assume "v' \<in> scope (v,p)"
[PROOF STATE]
proof (state)
this:
v' \<in> scope (v, p)

goal (1 subgoal):
 1. v' \<in> scope (v, p) \<Longrightarrow> False
[PROOF STEP]
from \<open>(v',p') \<in> snd ` set pth\<close>
[PROOF STATE]
proof (chain)
picking this:
(v', p') \<in> snd ` set pth
[PROOF STEP]
obtain pth1 pth2 e  where "pth = pth1@[e]@pth2" and "snd e = (v',p')"
[PROOF STATE]
proof (prove)
using this:
(v', p') \<in> snd ` set pth

goal (1 subgoal):
 1. (\<And>pth1 e pth2. \<lbrakk>pth = pth1 @ [e] @ pth2; snd e = (v', p')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule snd_set_split)
[PROOF STATE]
proof (state)
this:
pth = pth1 @ [e] @ pth2
snd e = (v', p')

goal (1 subgoal):
 1. v' \<in> scope (v, p) \<Longrightarrow> False
[PROOF STEP]
from terminal_path_is_path[OF assms(1), unfolded \<open>pth = _ \<close>] \<open>snd e = _\<close>
[PROOF STATE]
proof (chain)
picking this:
path v t (pth1 @ [e] @ pth2)
snd e = (v', p')
[PROOF STEP]
have "path v v' (pth1@[e])" and "path v' t pth2"
[PROOF STATE]
proof (prove)
using this:
path v t (pth1 @ [e] @ pth2)
snd e = (v', p')

goal (1 subgoal):
 1. path v v' (pth1 @ [e]) &&& path v' t pth2
[PROOF STEP]
unfolding path_split
[PROOF STATE]
proof (prove)
using this:
path v (edge_end e) (pth1 @ [e]) \<and> path (edge_end e) t pth2
snd e = (v', p')

goal (1 subgoal):
 1. path v v' (pth1 @ [e]) &&& path v' t pth2
[PROOF STEP]
by (auto simp add: edge_end_tup)
[PROOF STATE]
proof (state)
this:
path v v' (pth1 @ [e])
path v' t pth2

goal (1 subgoal):
 1. v' \<in> scope (v, p) \<Longrightarrow> False
[PROOF STEP]
from \<open>v' \<in> scope (v,p)\<close> terminal_path_end_is_terminal[OF assms(1)] \<open>path v' t pth2\<close>
[PROOF STATE]
proof (chain)
picking this:
v' \<in> scope (v, p)
terminal_vertex t
path v' t pth2
[PROOF STEP]
have "(v,p) \<in> snd ` set pth2"
[PROOF STATE]
proof (prove)
using this:
v' \<in> scope (v, p)
terminal_vertex t
path v' t pth2

goal (1 subgoal):
 1. (v, p) \<in> snd ` set pth2
[PROOF STEP]
by (rule scope_find)
[PROOF STATE]
proof (state)
this:
(v, p) \<in> snd ` set pth2

goal (1 subgoal):
 1. v' \<in> scope (v, p) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(v, p) \<in> snd ` set pth2
[PROOF STEP]
obtain pth2a e' pth2b  where "pth2 = pth2a@[e']@pth2b" and "snd e' = (v,p)"
[PROOF STATE]
proof (prove)
using this:
(v, p) \<in> snd ` set pth2

goal (1 subgoal):
 1. (\<And>pth2a e' pth2b. \<lbrakk>pth2 = pth2a @ [e'] @ pth2b; snd e' = (v, p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule snd_set_split)
[PROOF STATE]
proof (state)
this:
pth2 = pth2a @ [e'] @ pth2b
snd e' = (v, p)

goal (1 subgoal):
 1. v' \<in> scope (v, p) \<Longrightarrow> False
[PROOF STEP]
from \<open>path v' t pth2\<close>[unfolded \<open>pth2 = _ \<close>] \<open>snd e' = _\<close>
[PROOF STATE]
proof (chain)
picking this:
path v' t (pth2a @ [e'] @ pth2b)
snd e' = (v, p)
[PROOF STEP]
have "path v' v (pth2a@[e'])" and "path v t pth2b"
[PROOF STATE]
proof (prove)
using this:
path v' t (pth2a @ [e'] @ pth2b)
snd e' = (v, p)

goal (1 subgoal):
 1. path v' v (pth2a @ [e']) &&& path v t pth2b
[PROOF STEP]
unfolding path_split
[PROOF STATE]
proof (prove)
using this:
path v' (edge_end e') (pth2a @ [e']) \<and> path (edge_end e') t pth2b
snd e' = (v, p)

goal (1 subgoal):
 1. path v' v (pth2a @ [e']) &&& path v t pth2b
[PROOF STEP]
by (auto simp add: edge_end_tup)
[PROOF STATE]
proof (state)
this:
path v' v (pth2a @ [e'])
path v t pth2b

goal (1 subgoal):
 1. v' \<in> scope (v, p) \<Longrightarrow> False
[PROOF STEP]
from \<open>path v v' (pth1@[e])\<close> \<open>path v' v (pth2a@[e'])\<close>
[PROOF STATE]
proof (chain)
picking this:
path v v' (pth1 @ [e])
path v' v (pth2a @ [e'])
[PROOF STEP]
have "path v v ((pth1@[e])@(pth2a@[e']))"
[PROOF STATE]
proof (prove)
using this:
path v v' (pth1 @ [e])
path v' v (pth2a @ [e'])

goal (1 subgoal):
 1. path v v ((pth1 @ [e]) @ pth2a @ [e'])
[PROOF STEP]
by (rule path_appendI)
[PROOF STATE]
proof (state)
this:
path v v ((pth1 @ [e]) @ pth2a @ [e'])

goal (1 subgoal):
 1. v' \<in> scope (v, p) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
path v v ((pth1 @ [e]) @ pth2a @ [e'])

goal (1 subgoal):
 1. v' \<in> scope (v, p) \<Longrightarrow> False
[PROOF STEP]
from terminal_path_is_hyps_free[OF assms(1)] \<open>pth = _\<close> \<open>pth2 = _\<close>
[PROOF STATE]
proof (chain)
picking this:
hyps_free pth
pth = pth1 @ [e] @ pth2
pth2 = pth2a @ [e'] @ pth2b
[PROOF STEP]
have "hyps_free ((pth1@[e])@(pth2a@[e']))"
[PROOF STATE]
proof (prove)
using this:
hyps_free pth
pth = pth1 @ [e] @ pth2
pth2 = pth2a @ [e'] @ pth2b

goal (1 subgoal):
 1. hyps_free ((pth1 @ [e]) @ pth2a @ [e'])
[PROOF STEP]
by (auto simp add: hyps_free_def)
[PROOF STATE]
proof (state)
this:
hyps_free ((pth1 @ [e]) @ pth2a @ [e'])

goal (1 subgoal):
 1. v' \<in> scope (v, p) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
path v v ((pth1 @ [e]) @ pth2a @ [e'])
hyps_free ((pth1 @ [e]) @ pth2a @ [e'])
[PROOF STEP]
have "((pth1@[e])@(pth2a@[e'])) = []"
[PROOF STATE]
proof (prove)
using this:
path v v ((pth1 @ [e]) @ pth2a @ [e'])
hyps_free ((pth1 @ [e]) @ pth2a @ [e'])

goal (1 subgoal):
 1. (pth1 @ [e]) @ pth2a @ [e'] = []
[PROOF STEP]
by (rule hyps_free_acyclic)
[PROOF STATE]
proof (state)
this:
(pth1 @ [e]) @ pth2a @ [e'] = []

goal (1 subgoal):
 1. v' \<in> scope (v, p) \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
(pth1 @ [e]) @ pth2a @ [e'] = []

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma out_of_scope: "valid_in_port (v,p) \<Longrightarrow> v' |\<in>| vertices \<Longrightarrow> v' \<notin> scope (v,p) \<Longrightarrow> freshenLC (vidx v) ` local_vars (nodeOf v) p \<inter> subst_lconsts (inst v') = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_in_port (v, p); v' |\<in>| vertices; v' \<notin> scope (v, p)\<rbrakk> \<Longrightarrow> freshenLC (vidx v) ` local_vars (nodeOf v) p \<inter> subst_lconsts (inst v') = {}
[PROOF STEP]
using well_scoped_inst
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>valid_in_port (?v, ?p); ?var \<in> local_vars (nodeOf ?v) ?p; ?v' |\<in>| vertices; freshenLC (vidx ?v) ?var \<in> subst_lconsts (inst ?v')\<rbrakk> \<Longrightarrow> ?v' \<in> scope (?v, ?p)

goal (1 subgoal):
 1. \<lbrakk>valid_in_port (v, p); v' |\<in>| vertices; v' \<notin> scope (v, p)\<rbrakk> \<Longrightarrow> freshenLC (vidx v) ` local_vars (nodeOf v) p \<inter> subst_lconsts (inst v') = {}
[PROOF STEP]
by auto


[STATEMENT]
lemma walk_edges_app: "walk_edges (xs @ [y, x]) = walk_edges (xs @ [y]) @ [{y, x}]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. walk_edges (xs @ [y, x]) = walk_edges (xs @ [y]) @ [{y, x}]
[PROOF STEP]
by (induct xs rule: walk_edges.induct, simp_all)


[STATEMENT]
lemma walk_edges_tl_ss: "set (walk_edges (tl xs)) \<subseteq> set (walk_edges xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (walk_edges (tl xs)) \<subseteq> set (walk_edges xs)
[PROOF STEP]
by (induct xs rule: walk_edges.induct)  auto


[STATEMENT]
lemma walk_edges_rev: "rev (walk_edges xs) = walk_edges (rev xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev (walk_edges xs) = walk_edges (rev xs)
[PROOF STEP]
proof (induct xs rule: walk_edges.induct, simp_all)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y ys. rev (walk_edges (y # ys)) = walk_edges (rev ys @ [y]) \<Longrightarrow> walk_edges (rev ys @ [y]) @ [{x, y}] = walk_edges (rev ys @ [y, x])
[PROOF STEP]
fix x y ys
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y ys. rev (walk_edges (y # ys)) = walk_edges (rev ys @ [y]) \<Longrightarrow> walk_edges (rev ys @ [y]) @ [{x, y}] = walk_edges (rev ys @ [y, x])
[PROOF STEP]
assume assm: "rev (walk_edges (y # ys)) = walk_edges (rev ys @ [y])"
[PROOF STATE]
proof (state)
this:
rev (walk_edges (y # ys)) = walk_edges (rev ys @ [y])

goal (1 subgoal):
 1. \<And>x y ys. rev (walk_edges (y # ys)) = walk_edges (rev ys @ [y]) \<Longrightarrow> walk_edges (rev ys @ [y]) @ [{x, y}] = walk_edges (rev ys @ [y, x])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rev (walk_edges (y # ys)) = walk_edges (rev ys @ [y])
[PROOF STEP]
show "walk_edges (rev ys @ [y]) @ [{x, y}] = walk_edges (rev ys @ [y, x])"
[PROOF STATE]
proof (prove)
using this:
rev (walk_edges (y # ys)) = walk_edges (rev ys @ [y])

goal (1 subgoal):
 1. walk_edges (rev ys @ [y]) @ [{x, y}] = walk_edges (rev ys @ [y, x])
[PROOF STEP]
using walk_edges_app
[PROOF STATE]
proof (prove)
using this:
rev (walk_edges (y # ys)) = walk_edges (rev ys @ [y])
walk_edges (?xs @ [?y, ?x]) = walk_edges (?xs @ [?y]) @ [{?y, ?x}]

goal (1 subgoal):
 1. walk_edges (rev ys @ [y]) @ [{x, y}] = walk_edges (rev ys @ [y, x])
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
walk_edges (rev ys @ [y]) @ [{x, y}] = walk_edges (rev ys @ [y, x])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma walk_edges_append_ss1: "set (walk_edges (ys)) \<subseteq> set (walk_edges (xs@ys))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (walk_edges ys) \<subseteq> set (walk_edges (xs @ ys))
[PROOF STEP]
proof (induct xs rule: walk_edges.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. set (walk_edges ys) \<subseteq> set (walk_edges ([] @ ys))
 2. \<And>x. set (walk_edges ys) \<subseteq> set (walk_edges ([x] @ ys))
 3. \<And>x y ysa. set (walk_edges ys) \<subseteq> set (walk_edges ((y # ysa) @ ys)) \<Longrightarrow> set (walk_edges ys) \<subseteq> set (walk_edges ((x # y # ysa) @ ys))
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. set (walk_edges ys) \<subseteq> set (walk_edges ([] @ ys))
 2. \<And>x. set (walk_edges ys) \<subseteq> set (walk_edges ([x] @ ys))
 3. \<And>x y ysa. set (walk_edges ys) \<subseteq> set (walk_edges ((y # ysa) @ ys)) \<Longrightarrow> set (walk_edges ys) \<subseteq> set (walk_edges ((x # y # ysa) @ ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (walk_edges ys) \<subseteq> set (walk_edges ([] @ ys))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (walk_edges ys) \<subseteq> set (walk_edges ([] @ ys))

goal (2 subgoals):
 1. \<And>x. set (walk_edges ys) \<subseteq> set (walk_edges ([x] @ ys))
 2. \<And>x y ysa. set (walk_edges ys) \<subseteq> set (walk_edges ((y # ysa) @ ys)) \<Longrightarrow> set (walk_edges ys) \<subseteq> set (walk_edges ((x # y # ysa) @ ys))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. set (walk_edges ys) \<subseteq> set (walk_edges ([x] @ ys))
 2. \<And>x y ysa. set (walk_edges ys) \<subseteq> set (walk_edges ((y # ysa) @ ys)) \<Longrightarrow> set (walk_edges ys) \<subseteq> set (walk_edges ((x # y # ysa) @ ys))
[PROOF STEP]
case (2 x)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>x. set (walk_edges ys) \<subseteq> set (walk_edges ([x] @ ys))
 2. \<And>x y ysa. set (walk_edges ys) \<subseteq> set (walk_edges ((y # ysa) @ ys)) \<Longrightarrow> set (walk_edges ys) \<subseteq> set (walk_edges ((x # y # ysa) @ ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (walk_edges ys) \<subseteq> set (walk_edges ([x] @ ys))
[PROOF STEP]
using walk_edges_tl_ss
[PROOF STATE]
proof (prove)
using this:
set (walk_edges (tl ?xs)) \<subseteq> set (walk_edges ?xs)

goal (1 subgoal):
 1. set (walk_edges ys) \<subseteq> set (walk_edges ([x] @ ys))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
set (walk_edges ys) \<subseteq> set (walk_edges ([x] @ ys))

goal (1 subgoal):
 1. \<And>x y ysa. set (walk_edges ys) \<subseteq> set (walk_edges ((y # ysa) @ ys)) \<Longrightarrow> set (walk_edges ys) \<subseteq> set (walk_edges ((x # y # ysa) @ ys))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y ysa. set (walk_edges ys) \<subseteq> set (walk_edges ((y # ysa) @ ys)) \<Longrightarrow> set (walk_edges ys) \<subseteq> set (walk_edges ((x # y # ysa) @ ys))
[PROOF STEP]
case (3 x y ys)
[PROOF STATE]
proof (state)
this:
set (walk_edges ys) \<subseteq> set (walk_edges ((y # ys) @ ys))

goal (1 subgoal):
 1. \<And>x y ysa. set (walk_edges ys) \<subseteq> set (walk_edges ((y # ysa) @ ys)) \<Longrightarrow> set (walk_edges ys) \<subseteq> set (walk_edges ((x # y # ysa) @ ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set (walk_edges ys) \<subseteq> set (walk_edges ((y # ys) @ ys))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set (walk_edges ys) \<subseteq> set (walk_edges ((y # ys) @ ys))

goal (1 subgoal):
 1. set (walk_edges ys) \<subseteq> set (walk_edges ((x # y # ys) @ ys))
[PROOF STEP]
by (simp add: subset_iff)
[PROOF STATE]
proof (state)
this:
set (walk_edges ys) \<subseteq> set (walk_edges ((x # y # ys) @ ys))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma walk_edges_append_ss2: "set (walk_edges (xs)) \<subseteq> set (walk_edges (xs@ys))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (walk_edges xs) \<subseteq> set (walk_edges (xs @ ys))
[PROOF STEP]
by (induct xs rule: walk_edges.induct) auto


[STATEMENT]
lemma walk_edges_singleton_app: "ys \<noteq> [] \<Longrightarrow> walk_edges ([x]@ys) = {x, hd ys} # walk_edges ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ys \<noteq> [] \<Longrightarrow> walk_edges ([x] @ ys) = {x, hd ys} # walk_edges ys
[PROOF STEP]
using list.exhaust_sel walk_edges.simps(3)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?list = [] \<Longrightarrow> ?P; ?list = hd ?list # tl ?list \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
walk_edges (?x # ?y # ?ys) = {?x, ?y} # walk_edges (?y # ?ys)

goal (1 subgoal):
 1. ys \<noteq> [] \<Longrightarrow> walk_edges ([x] @ ys) = {x, hd ys} # walk_edges ys
[PROOF STEP]
by (metis Cons_eq_appendI eq_Nil_appendI)


[STATEMENT]
lemma walk_edges_append_union: "xs \<noteq> [] \<Longrightarrow> ys \<noteq> [] \<Longrightarrow>
    set (walk_edges (xs@ys)) = set (walk_edges (xs)) \<union> set (walk_edges ys) \<union> {{last xs, hd ys}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs \<noteq> []; ys \<noteq> []\<rbrakk> \<Longrightarrow> set (walk_edges (xs @ ys)) = set (walk_edges xs) \<union> set (walk_edges ys) \<union> {{last xs, hd ys}}
[PROOF STEP]
using walk_edges_singleton_app
[PROOF STATE]
proof (prove)
using this:
?ys \<noteq> [] \<Longrightarrow> walk_edges ([?x] @ ?ys) = {?x, hd ?ys} # walk_edges ?ys

goal (1 subgoal):
 1. \<lbrakk>xs \<noteq> []; ys \<noteq> []\<rbrakk> \<Longrightarrow> set (walk_edges (xs @ ys)) = set (walk_edges xs) \<union> set (walk_edges ys) \<union> {{last xs, hd ys}}
[PROOF STEP]
by (induct xs rule: walk_edges.induct) auto