[STATEMENT]
lemma alphaAbs_qAbs_imp_alphaAbs_all_equal_or_qFresh:
assumes "qGood X" and "qAbs xs x X $= qAbs xs' x' X'"
shows "alphaAbs_all_equal_or_qFresh xs x X xs' x' X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_all_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. alphaAbs_all_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
have "qGoodAbs(qAbs xs x X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGoodAbs (qAbs xs x X)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
qGood X
qAbs xs x X $= qAbs xs' x' X'

goal (1 subgoal):
 1. qGoodAbs (qAbs xs x X)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
qGoodAbs (qAbs xs x X)

goal (1 subgoal):
 1. alphaAbs_all_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
hence "qGoodAbs(qAbs xs' x' X')"
[PROOF STATE]
proof (prove)
using this:
qGoodAbs (qAbs xs x X)

goal (1 subgoal):
 1. qGoodAbs (qAbs xs' x' X')
[PROOF STEP]
using assms alphaAbs_preserves_qGoodAbs
[PROOF STATE]
proof (prove)
using this:
qGoodAbs (qAbs xs x X)
qGood X
qAbs xs x X $= qAbs xs' x' X'
?A $= ?A' \<Longrightarrow> qGoodAbs ?A = qGoodAbs ?A'

goal (1 subgoal):
 1. qGoodAbs (qAbs xs' x' X')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
qGoodAbs (qAbs xs' x' X')

goal (1 subgoal):
 1. alphaAbs_all_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
hence GOOD: "qGood X \<and> qGood X'"
[PROOF STATE]
proof (prove)
using this:
qGoodAbs (qAbs xs' x' X')

goal (1 subgoal):
 1. qGood X \<and> qGood X'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
qGoodAbs (qAbs xs' x' X')
qGood X
qAbs xs x X $= qAbs xs' x' X'

goal (1 subgoal):
 1. qGood X \<and> qGood X'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
qGood X \<and> qGood X'

goal (1 subgoal):
 1. alphaAbs_all_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
have xs: "xs = xs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = xs'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
qGood X
qAbs xs x X $= qAbs xs' x' X'

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

goal (1 subgoal):
 1. alphaAbs_all_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_all_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
unfolding alphaAbs_all_equal_or_qFresh_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = xs' \<and> (\<forall>y. (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X') \<longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs)
[PROOF STEP]
using xs
[PROOF STATE]
proof (prove)
using this:
xs = xs'

goal (1 subgoal):
 1. xs = xs' \<and> (\<forall>y. (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X') \<longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs)
[PROOF STEP]
proof(intro conjI impI allI, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
assume yEqFresh: "(y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')"
[PROOF STATE]
proof (state)
this:
(y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')

goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
have "\<exists> Y. X #= Y \<and> (y = x \<or> qAFresh xs y Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Y. X #= Y \<and> (y = x \<or> qAFresh xs y Y)
[PROOF STEP]
proof(cases "y = x")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y = x \<Longrightarrow> \<exists>Y. X #= Y \<and> (y = x \<or> qAFresh xs y Y)
 2. y \<noteq> x \<Longrightarrow> \<exists>Y. X #= Y \<and> (y = x \<or> qAFresh xs y Y)
[PROOF STEP]
assume Case1: "y = x"
[PROOF STATE]
proof (state)
this:
y = x

goal (2 subgoals):
 1. y = x \<Longrightarrow> \<exists>Y. X #= Y \<and> (y = x \<or> qAFresh xs y Y)
 2. y \<noteq> x \<Longrightarrow> \<exists>Y. X #= Y \<and> (y = x \<or> qAFresh xs y Y)
[PROOF STEP]
hence "X #= X"
[PROOF STATE]
proof (prove)
using this:
y = x

goal (1 subgoal):
 1. X #= X
[PROOF STEP]
using GOOD alpha_refl
[PROOF STATE]
proof (prove)
using this:
y = x
qGood X \<and> qGood X'
qGood ?X \<Longrightarrow> ?X #= ?X

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

goal (2 subgoals):
 1. y = x \<Longrightarrow> \<exists>Y. X #= Y \<and> (y = x \<or> qAFresh xs y Y)
 2. y \<noteq> x \<Longrightarrow> \<exists>Y. X #= Y \<and> (y = x \<or> qAFresh xs y Y)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
X #= X

goal (1 subgoal):
 1. \<exists>Y. X #= Y \<and> (y = x \<or> qAFresh xs y Y)
[PROOF STEP]
using Case1
[PROOF STATE]
proof (prove)
using this:
X #= X
y = x

goal (1 subgoal):
 1. \<exists>Y. X #= Y \<and> (y = x \<or> qAFresh xs y Y)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>Y. X #= Y \<and> (y = x \<or> qAFresh xs y Y)

goal (1 subgoal):
 1. y \<noteq> x \<Longrightarrow> \<exists>Y. X #= Y \<and> (y = x \<or> qAFresh xs y Y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<noteq> x \<Longrightarrow> \<exists>Y. X #= Y \<and> (y = x \<or> qAFresh xs y Y)
[PROOF STEP]
assume Case2: "y \<noteq> x"
[PROOF STATE]
proof (state)
this:
y \<noteq> x

goal (1 subgoal):
 1. y \<noteq> x \<Longrightarrow> \<exists>Y. X #= Y \<and> (y = x \<or> qAFresh xs y Y)
[PROOF STEP]
hence "qFresh xs y X"
[PROOF STATE]
proof (prove)
using this:
y \<noteq> x

goal (1 subgoal):
 1. qFresh xs y X
[PROOF STEP]
using yEqFresh
[PROOF STATE]
proof (prove)
using this:
y \<noteq> x
(y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')

goal (1 subgoal):
 1. qFresh xs y X
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
qFresh xs y X

goal (1 subgoal):
 1. y \<noteq> x \<Longrightarrow> \<exists>Y. X #= Y \<and> (y = x \<or> qAFresh xs y Y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qFresh xs y X
[PROOF STEP]
obtain Y where "X #= Y" and "qAFresh xs y Y"
[PROOF STATE]
proof (prove)
using this:
qFresh xs y X

goal (1 subgoal):
 1. (\<And>Y. \<lbrakk>X #= Y; qAFresh xs y Y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using GOOD qFresh_imp_ex_qAFresh1
[PROOF STATE]
proof (prove)
using this:
qFresh xs y X
qGood X \<and> qGood X'
\<lbrakk>qGood ?X; qFresh ?zs ?z ?X\<rbrakk> \<Longrightarrow> \<exists>X'. qGood X' \<and> ?X #= X' \<and> qAFresh ?zs ?z X'

goal (1 subgoal):
 1. (\<And>Y. \<lbrakk>X #= Y; qAFresh xs y Y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
X #= Y
qAFresh xs y Y

goal (1 subgoal):
 1. y \<noteq> x \<Longrightarrow> \<exists>Y. X #= Y \<and> (y = x \<or> qAFresh xs y Y)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
X #= Y
qAFresh xs y Y

goal (1 subgoal):
 1. \<exists>Y. X #= Y \<and> (y = x \<or> qAFresh xs y Y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>Y. X #= Y \<and> (y = x \<or> qAFresh xs y Y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>Y. X #= Y \<and> (y = x \<or> qAFresh xs y Y)

goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>Y. X #= Y \<and> (y = x \<or> qAFresh xs y Y)
[PROOF STEP]
obtain Y where alphaXY: "X #= Y" and yEqAFresh: "y = x \<or> qAFresh xs y Y"
[PROOF STATE]
proof (prove)
using this:
\<exists>Y. X #= Y \<and> (y = x \<or> qAFresh xs y Y)

goal (1 subgoal):
 1. (\<And>Y. \<lbrakk>X #= Y; y = x \<or> qAFresh xs y Y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
X #= Y
y = x \<or> qAFresh xs y Y

goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
hence alphaXYyx: "(X #[[y \<and> x]]_xs) #= (Y #[[y \<and> x]]_xs)"
[PROOF STATE]
proof (prove)
using this:
X #= Y
y = x \<or> qAFresh xs y Y

goal (1 subgoal):
 1. X #[[y \<and> x]]_xs #= Y #[[y \<and> x]]_xs
[PROOF STEP]
using GOOD
[PROOF STATE]
proof (prove)
using this:
X #= Y
y = x \<or> qAFresh xs y Y
qGood X \<and> qGood X'

goal (1 subgoal):
 1. X #[[y \<and> x]]_xs #= Y #[[y \<and> x]]_xs
[PROOF STEP]
by (auto simp add: qSwap_preserves_alpha)
[PROOF STATE]
proof (state)
this:
X #[[y \<and> x]]_xs #= Y #[[y \<and> x]]_xs

goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
have goodY: "qGood Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGood Y
[PROOF STEP]
using GOOD alphaXY alpha_preserves_qGood
[PROOF STATE]
proof (prove)
using this:
qGood X \<and> qGood X'
X #= Y
?X #= ?X' \<Longrightarrow> qGood ?X = qGood ?X'

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

goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
(*  *)
[PROOF STATE]
proof (state)
this:
qGood Y

goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
have "\<exists> Y'. X' #= Y' \<and> (y = x' \<or> qAFresh xs y Y')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Y'. X' #= Y' \<and> (y = x' \<or> qAFresh xs y Y')
[PROOF STEP]
proof(cases "y = x'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y = x' \<Longrightarrow> \<exists>Y'. X' #= Y' \<and> (y = x' \<or> qAFresh xs y Y')
 2. y \<noteq> x' \<Longrightarrow> \<exists>Y'. X' #= Y' \<and> (y = x' \<or> qAFresh xs y Y')
[PROOF STEP]
assume Case1: "y = x'"
[PROOF STATE]
proof (state)
this:
y = x'

goal (2 subgoals):
 1. y = x' \<Longrightarrow> \<exists>Y'. X' #= Y' \<and> (y = x' \<or> qAFresh xs y Y')
 2. y \<noteq> x' \<Longrightarrow> \<exists>Y'. X' #= Y' \<and> (y = x' \<or> qAFresh xs y Y')
[PROOF STEP]
hence "X' #= X'"
[PROOF STATE]
proof (prove)
using this:
y = x'

goal (1 subgoal):
 1. X' #= X'
[PROOF STEP]
using GOOD alpha_refl
[PROOF STATE]
proof (prove)
using this:
y = x'
qGood X \<and> qGood X'
qGood ?X \<Longrightarrow> ?X #= ?X

goal (1 subgoal):
 1. X' #= X'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X' #= X'

goal (2 subgoals):
 1. y = x' \<Longrightarrow> \<exists>Y'. X' #= Y' \<and> (y = x' \<or> qAFresh xs y Y')
 2. y \<noteq> x' \<Longrightarrow> \<exists>Y'. X' #= Y' \<and> (y = x' \<or> qAFresh xs y Y')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
X' #= X'

goal (1 subgoal):
 1. \<exists>Y'. X' #= Y' \<and> (y = x' \<or> qAFresh xs y Y')
[PROOF STEP]
using Case1
[PROOF STATE]
proof (prove)
using this:
X' #= X'
y = x'

goal (1 subgoal):
 1. \<exists>Y'. X' #= Y' \<and> (y = x' \<or> qAFresh xs y Y')
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>Y'. X' #= Y' \<and> (y = x' \<or> qAFresh xs y Y')

goal (1 subgoal):
 1. y \<noteq> x' \<Longrightarrow> \<exists>Y'. X' #= Y' \<and> (y = x' \<or> qAFresh xs y Y')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<noteq> x' \<Longrightarrow> \<exists>Y'. X' #= Y' \<and> (y = x' \<or> qAFresh xs y Y')
[PROOF STEP]
assume Case2: "y \<noteq> x'"
[PROOF STATE]
proof (state)
this:
y \<noteq> x'

goal (1 subgoal):
 1. y \<noteq> x' \<Longrightarrow> \<exists>Y'. X' #= Y' \<and> (y = x' \<or> qAFresh xs y Y')
[PROOF STEP]
hence "qFresh xs y X'"
[PROOF STATE]
proof (prove)
using this:
y \<noteq> x'

goal (1 subgoal):
 1. qFresh xs y X'
[PROOF STEP]
using yEqFresh
[PROOF STATE]
proof (prove)
using this:
y \<noteq> x'
(y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')

goal (1 subgoal):
 1. qFresh xs y X'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
qFresh xs y X'

goal (1 subgoal):
 1. y \<noteq> x' \<Longrightarrow> \<exists>Y'. X' #= Y' \<and> (y = x' \<or> qAFresh xs y Y')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qFresh xs y X'
[PROOF STEP]
obtain Y' where "X' #= Y'" and "qAFresh xs y Y'"
[PROOF STATE]
proof (prove)
using this:
qFresh xs y X'

goal (1 subgoal):
 1. (\<And>Y'. \<lbrakk>X' #= Y'; qAFresh xs y Y'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using GOOD qFresh_imp_ex_qAFresh1
[PROOF STATE]
proof (prove)
using this:
qFresh xs y X'
qGood X \<and> qGood X'
\<lbrakk>qGood ?X; qFresh ?zs ?z ?X\<rbrakk> \<Longrightarrow> \<exists>X'. qGood X' \<and> ?X #= X' \<and> qAFresh ?zs ?z X'

goal (1 subgoal):
 1. (\<And>Y'. \<lbrakk>X' #= Y'; qAFresh xs y Y'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
X' #= Y'
qAFresh xs y Y'

goal (1 subgoal):
 1. y \<noteq> x' \<Longrightarrow> \<exists>Y'. X' #= Y' \<and> (y = x' \<or> qAFresh xs y Y')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
X' #= Y'
qAFresh xs y Y'

goal (1 subgoal):
 1. \<exists>Y'. X' #= Y' \<and> (y = x' \<or> qAFresh xs y Y')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>Y'. X' #= Y' \<and> (y = x' \<or> qAFresh xs y Y')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>Y'. X' #= Y' \<and> (y = x' \<or> qAFresh xs y Y')

goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>Y'. X' #= Y' \<and> (y = x' \<or> qAFresh xs y Y')
[PROOF STEP]
obtain Y' where alphaX'Y': "X' #= Y'" and
                         yEqAFresh': "y = x' \<or> qAFresh xs y Y'"
[PROOF STATE]
proof (prove)
using this:
\<exists>Y'. X' #= Y' \<and> (y = x' \<or> qAFresh xs y Y')

goal (1 subgoal):
 1. (\<And>Y'. \<lbrakk>X' #= Y'; y = x' \<or> qAFresh xs y Y'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
X' #= Y'
y = x' \<or> qAFresh xs y Y'

goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
hence "(X' #[[y \<and> x']]_xs) #= (Y' #[[y \<and> x']]_xs)"
[PROOF STATE]
proof (prove)
using this:
X' #= Y'
y = x' \<or> qAFresh xs y Y'

goal (1 subgoal):
 1. X' #[[y \<and> x']]_xs #= Y' #[[y \<and> x']]_xs
[PROOF STEP]
using GOOD
[PROOF STATE]
proof (prove)
using this:
X' #= Y'
y = x' \<or> qAFresh xs y Y'
qGood X \<and> qGood X'

goal (1 subgoal):
 1. X' #[[y \<and> x']]_xs #= Y' #[[y \<and> x']]_xs
[PROOF STEP]
by (auto simp add: qSwap_preserves_alpha)
[PROOF STATE]
proof (state)
this:
X' #[[y \<and> x']]_xs #= Y' #[[y \<and> x']]_xs

goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
hence alphaY'X'yx': "(Y' #[[y \<and> x']]_xs) #= (X' #[[y \<and> x']]_xs)"
[PROOF STATE]
proof (prove)
using this:
X' #[[y \<and> x']]_xs #= Y' #[[y \<and> x']]_xs

goal (1 subgoal):
 1. Y' #[[y \<and> x']]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
using alpha_sym
[PROOF STATE]
proof (prove)
using this:
X' #[[y \<and> x']]_xs #= Y' #[[y \<and> x']]_xs
?X #= ?X' \<Longrightarrow> ?X' #= ?X

goal (1 subgoal):
 1. Y' #[[y \<and> x']]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Y' #[[y \<and> x']]_xs #= X' #[[y \<and> x']]_xs

goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
have goodY': "qGood Y'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGood Y'
[PROOF STEP]
using GOOD alphaX'Y' alpha_preserves_qGood
[PROOF STATE]
proof (prove)
using this:
qGood X \<and> qGood X'
X' #= Y'
?X #= ?X' \<Longrightarrow> qGood ?X = qGood ?X'

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

goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
(*  *)
[PROOF STATE]
proof (state)
this:
qGood Y'

goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
have 1: "Y #= X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Y #= X
[PROOF STEP]
using alphaXY alpha_sym
[PROOF STATE]
proof (prove)
using this:
X #= Y
?X #= ?X' \<Longrightarrow> ?X' #= ?X

goal (1 subgoal):
 1. Y #= X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Y #= X

goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
hence "qGood Y"
[PROOF STATE]
proof (prove)
using this:
Y #= X

goal (1 subgoal):
 1. qGood Y
[PROOF STEP]
using GOOD alpha_preserves_qGood
[PROOF STATE]
proof (prove)
using this:
Y #= X
qGood X \<and> qGood X'
?X #= ?X' \<Longrightarrow> qGood ?X = qGood ?X'

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

goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
hence 2: "qAbs xs x Y $= qAbs xs x X"
[PROOF STATE]
proof (prove)
using this:
qGood Y

goal (1 subgoal):
 1. qAbs xs x Y $= qAbs xs x X
[PROOF STEP]
using 1 GOOD qAbs_preserves_alpha
[PROOF STATE]
proof (prove)
using this:
qGood Y
Y #= X
qGood X \<and> qGood X'
\<lbrakk>?X #= ?X'; qGood ?X \<or> qGood ?X'\<rbrakk> \<Longrightarrow> qAbs ?xs ?x ?X $= qAbs ?xs ?x ?X'

goal (1 subgoal):
 1. qAbs xs x Y $= qAbs xs x X
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
qAbs xs x Y $= qAbs xs x X

goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
qAbs xs x Y $= qAbs xs x X

goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
have "qAbs xs x' X' $= qAbs xs x' Y'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qAbs xs x' X' $= qAbs xs x' Y'
[PROOF STEP]
using alphaX'Y' GOOD qAbs_preserves_alpha
[PROOF STATE]
proof (prove)
using this:
X' #= Y'
qGood X \<and> qGood X'
\<lbrakk>?X #= ?X'; qGood ?X \<or> qGood ?X'\<rbrakk> \<Longrightarrow> qAbs ?xs ?x ?X $= qAbs ?xs ?x ?X'

goal (1 subgoal):
 1. qAbs xs x' X' $= qAbs xs x' Y'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
qAbs xs x' X' $= qAbs xs x' Y'

goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
qAbs xs x' X' $= qAbs xs x' Y'

goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
qAbs xs x' X' $= qAbs xs x' Y'

goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
have "qGoodAbs(qAbs xs x X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGoodAbs (qAbs xs x X)
[PROOF STEP]
using GOOD
[PROOF STATE]
proof (prove)
using this:
qGood X \<and> qGood X'

goal (1 subgoal):
 1. qGoodAbs (qAbs xs x X)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
qGoodAbs (qAbs xs x X)

goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
hence "qGoodAbs(qAbs xs x Y)"
[PROOF STATE]
proof (prove)
using this:
qGoodAbs (qAbs xs x X)

goal (1 subgoal):
 1. qGoodAbs (qAbs xs x Y)
[PROOF STEP]
using 2 alphaAbs_preserves_qGoodAbs
[PROOF STATE]
proof (prove)
using this:
qGoodAbs (qAbs xs x X)
qAbs xs x Y $= qAbs xs x X
?A $= ?A' \<Longrightarrow> qGoodAbs ?A = qGoodAbs ?A'

goal (1 subgoal):
 1. qGoodAbs (qAbs xs x Y)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
qGoodAbs (qAbs xs x Y)

goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
qGoodAbs (qAbs xs x Y)

goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
qAbs xs x Y $= qAbs xs x X
qAbs xs x' X' $= qAbs xs x' Y'
qGoodAbs (qAbs xs x Y)
[PROOF STEP]
have "qAbs xs x Y $= qAbs xs x' Y'"
[PROOF STATE]
proof (prove)
using this:
qAbs xs x Y $= qAbs xs x X
qAbs xs x' X' $= qAbs xs x' Y'
qGoodAbs (qAbs xs x Y)

goal (1 subgoal):
 1. qAbs xs x Y $= qAbs xs x' Y'
[PROOF STEP]
using assms xs alphaAbs_trans_twice
[PROOF STATE]
proof (prove)
using this:
qAbs xs x Y $= qAbs xs x X
qAbs xs x' X' $= qAbs xs x' Y'
qGoodAbs (qAbs xs x Y)
qGood X
qAbs xs x X $= qAbs xs' x' X'
xs = xs'
\<lbrakk>qGoodAbs ?A \<or> qGoodAbs ?A' \<or> qGoodAbs ?A'' \<or> qGoodAbs ?A'''; ?A $= ?A'; ?A' $= ?A''; ?A'' $= ?A'''\<rbrakk> \<Longrightarrow> ?A $= ?A'''

goal (1 subgoal):
 1. qAbs xs x Y $= qAbs xs x' Y'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
qAbs xs x Y $= qAbs xs x' Y'

goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
hence "alphaAbs_all_equal_or_qAFresh xs x Y xs x' Y'"
[PROOF STATE]
proof (prove)
using this:
qAbs xs x Y $= qAbs xs x' Y'

goal (1 subgoal):
 1. alphaAbs_all_equal_or_qAFresh xs x Y xs x' Y'
[PROOF STEP]
using goodY goodY' alphaAbs_qAbs_iff_alphaAbs_all_equal_or_qAFresh
[PROOF STATE]
proof (prove)
using this:
qAbs xs x Y $= qAbs xs x' Y'
qGood Y
qGood Y'
\<lbrakk>qGood ?X; qGood ?X'\<rbrakk> \<Longrightarrow> (qAbs ?xs ?x ?X $= qAbs ?xs' ?x' ?X') = alphaAbs_all_equal_or_qAFresh ?xs ?x ?X ?xs' ?x' ?X'

goal (1 subgoal):
 1. alphaAbs_all_equal_or_qAFresh xs x Y xs x' Y'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
alphaAbs_all_equal_or_qAFresh xs x Y xs x' Y'

goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
hence "(Y #[[y \<and> x]]_xs) #= (Y' #[[y \<and> x']]_xs)"
[PROOF STATE]
proof (prove)
using this:
alphaAbs_all_equal_or_qAFresh xs x Y xs x' Y'

goal (1 subgoal):
 1. Y #[[y \<and> x]]_xs #= Y' #[[y \<and> x']]_xs
[PROOF STEP]
unfolding alphaAbs_all_equal_or_qAFresh_def
[PROOF STATE]
proof (prove)
using this:
xs = xs \<and> (\<forall>y. (y = x \<or> qAFresh xs y Y) \<and> (y = x' \<or> qAFresh xs y Y') \<longrightarrow> Y #[[y \<and> x]]_xs #= Y' #[[y \<and> x']]_xs)

goal (1 subgoal):
 1. Y #[[y \<and> x]]_xs #= Y' #[[y \<and> x']]_xs
[PROOF STEP]
using yEqAFresh yEqAFresh'
[PROOF STATE]
proof (prove)
using this:
xs = xs \<and> (\<forall>y. (y = x \<or> qAFresh xs y Y) \<and> (y = x' \<or> qAFresh xs y Y') \<longrightarrow> Y #[[y \<and> x]]_xs #= Y' #[[y \<and> x']]_xs)
y = x \<or> qAFresh xs y Y
y = x' \<or> qAFresh xs y Y'

goal (1 subgoal):
 1. Y #[[y \<and> x]]_xs #= Y' #[[y \<and> x']]_xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Y #[[y \<and> x]]_xs #= Y' #[[y \<and> x']]_xs

goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Y #[[y \<and> x]]_xs #= Y' #[[y \<and> x']]_xs

goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
have "qGood (X #[[y \<and> x]]_xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGood (X #[[y \<and> x]]_xs)
[PROOF STEP]
using GOOD qSwap_preserves_qGood
[PROOF STATE]
proof (prove)
using this:
qGood X \<and> qGood X'
qGood (?X #[[?x \<and> ?y]]_?zs) = qGood ?X

goal (1 subgoal):
 1. qGood (X #[[y \<and> x]]_xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
qGood (X #[[y \<and> x]]_xs)

goal (1 subgoal):
 1. \<And>y. \<lbrakk>xs = xs'; (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X')\<rbrakk> \<Longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Y #[[y \<and> x]]_xs #= Y' #[[y \<and> x']]_xs
qGood (X #[[y \<and> x]]_xs)
[PROOF STEP]
show "(X #[[y \<and> x]]_xs) #= (X' #[[y \<and> x']]_xs)"
[PROOF STATE]
proof (prove)
using this:
Y #[[y \<and> x]]_xs #= Y' #[[y \<and> x']]_xs
qGood (X #[[y \<and> x]]_xs)

goal (1 subgoal):
 1. X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
using alphaXYyx alphaY'X'yx' alpha_trans_twice
[PROOF STATE]
proof (prove)
using this:
Y #[[y \<and> x]]_xs #= Y' #[[y \<and> x']]_xs
qGood (X #[[y \<and> x]]_xs)
X #[[y \<and> x]]_xs #= Y #[[y \<and> x]]_xs
Y' #[[y \<and> x']]_xs #= X' #[[y \<and> x']]_xs
\<lbrakk>qGood ?X \<or> qGood ?X' \<or> qGood ?X'' \<or> qGood ?X'''; ?X #= ?X'; ?X' #= ?X''; ?X'' #= ?X'''\<rbrakk> \<Longrightarrow> ?X #= ?X'''

goal (1 subgoal):
 1. X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
alphaAbs_all_equal_or_qFresh xs x X xs' x' X'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alphaAbs_qAbs_iff_alphaAbs_all_equal_or_qFresh:
assumes "qGood X" and "qGood X'"
shows "(qAbs xs x X $= qAbs xs' x' X') =
       alphaAbs_all_equal_or_qFresh xs x X xs' x' X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
let ?Left = "(qAbs xs x X $= qAbs xs' x' X')"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
let ?Middle = "alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
let ?Right = "alphaAbs_all_equal_or_qFresh xs x X xs' x' X'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
have "?Left \<Longrightarrow> ?Right"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs' x' X' \<Longrightarrow> alphaAbs_all_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
using assms alphaAbs_qAbs_imp_alphaAbs_all_equal_or_qFresh
[PROOF STATE]
proof (prove)
using this:
qGood X
qGood X'
\<lbrakk>qGood ?X; qAbs ?xs ?x ?X $= qAbs ?xs' ?x' ?X'\<rbrakk> \<Longrightarrow> alphaAbs_all_equal_or_qFresh ?xs ?x ?X ?xs' ?x' ?X'

goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs' x' X' \<Longrightarrow> alphaAbs_all_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
qAbs xs x X $= qAbs xs' x' X' \<Longrightarrow> alphaAbs_all_equal_or_qFresh xs x X xs' x' X'

goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
qAbs xs x X $= qAbs xs' x' X' \<Longrightarrow> alphaAbs_all_equal_or_qFresh xs x X xs' x' X'

goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
have "?Right \<Longrightarrow> ?Middle"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_all_equal_or_qFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
using alphaAbs_all_equal_or_qFresh_imp_qAFresh
[PROOF STATE]
proof (prove)
using this:
alphaAbs_all_equal_or_qFresh ?xs ?x ?X ?xs' ?x' ?X' \<Longrightarrow> alphaAbs_all_equal_or_qAFresh ?xs ?x ?X ?xs' ?x' ?X'

goal (1 subgoal):
 1. alphaAbs_all_equal_or_qFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
alphaAbs_all_equal_or_qFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'

goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
alphaAbs_all_equal_or_qFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'

goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
have "?Middle ==> ?Left"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_all_equal_or_qAFresh xs x X xs' x' X' \<Longrightarrow> qAbs xs x X $= qAbs xs' x' X'
[PROOF STEP]
using assms alphaAbs_qAbs_iff_alphaAbs_all_equal_or_qAFresh
[PROOF STATE]
proof (prove)
using this:
qGood X
qGood X'
\<lbrakk>qGood ?X; qGood ?X'\<rbrakk> \<Longrightarrow> (qAbs ?xs ?x ?X $= qAbs ?xs' ?x' ?X') = alphaAbs_all_equal_or_qAFresh ?xs ?x ?X ?xs' ?x' ?X'

goal (1 subgoal):
 1. alphaAbs_all_equal_or_qAFresh xs x X xs' x' X' \<Longrightarrow> qAbs xs x X $= qAbs xs' x' X'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
alphaAbs_all_equal_or_qAFresh xs x X xs' x' X' \<Longrightarrow> qAbs xs x X $= qAbs xs' x' X'

goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
qAbs xs x X $= qAbs xs' x' X' \<Longrightarrow> alphaAbs_all_equal_or_qFresh xs x X xs' x' X'
alphaAbs_all_equal_or_qFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'
alphaAbs_all_equal_or_qAFresh xs x X xs' x' X' \<Longrightarrow> qAbs xs x X $= qAbs xs' x' X'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
qAbs xs x X $= qAbs xs' x' X' \<Longrightarrow> alphaAbs_all_equal_or_qFresh xs x X xs' x' X'
alphaAbs_all_equal_or_qFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_all_equal_or_qAFresh xs x X xs' x' X'
alphaAbs_all_equal_or_qAFresh xs x X xs' x' X' \<Longrightarrow> qAbs xs x X $= qAbs xs' x' X'

goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_equal_or_qFresh xs x X xs' x' X'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alphaAbs_qAbs_imp_alphaAbs_all_qFresh:
assumes "qGood X" and "qAbs xs x X $= qAbs xs' x' X'"
shows "alphaAbs_all_qFresh xs x X xs' x' X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_all_qFresh xs x X xs' x' X'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. alphaAbs_all_qFresh xs x X xs' x' X'
[PROOF STEP]
let ?Left = "(qAbs xs x X $= qAbs xs' x' X')"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. alphaAbs_all_qFresh xs x X xs' x' X'
[PROOF STEP]
let ?Middle = "alphaAbs_all_equal_or_qFresh xs x X xs' x' X'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. alphaAbs_all_qFresh xs x X xs' x' X'
[PROOF STEP]
let ?Right = "alphaAbs_all_qFresh xs x X xs' x' X'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. alphaAbs_all_qFresh xs x X xs' x' X'
[PROOF STEP]
have "?Left \<Longrightarrow> ?Middle"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs' x' X' \<Longrightarrow> alphaAbs_all_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
using assms alphaAbs_qAbs_imp_alphaAbs_all_equal_or_qFresh
[PROOF STATE]
proof (prove)
using this:
qGood X
qAbs xs x X $= qAbs xs' x' X'
\<lbrakk>qGood ?X; qAbs ?xs ?x ?X $= qAbs ?xs' ?x' ?X'\<rbrakk> \<Longrightarrow> alphaAbs_all_equal_or_qFresh ?xs ?x ?X ?xs' ?x' ?X'

goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs' x' X' \<Longrightarrow> alphaAbs_all_equal_or_qFresh xs x X xs' x' X'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
qAbs xs x X $= qAbs xs' x' X' \<Longrightarrow> alphaAbs_all_equal_or_qFresh xs x X xs' x' X'

goal (1 subgoal):
 1. alphaAbs_all_qFresh xs x X xs' x' X'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
qAbs xs x X $= qAbs xs' x' X' \<Longrightarrow> alphaAbs_all_equal_or_qFresh xs x X xs' x' X'

goal (1 subgoal):
 1. alphaAbs_all_qFresh xs x X xs' x' X'
[PROOF STEP]
have "?Middle \<Longrightarrow> ?Right"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_all_equal_or_qFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_all_qFresh xs x X xs' x' X'
[PROOF STEP]
unfolding alphaAbs_all_equal_or_qFresh_def alphaAbs_all_qFresh_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = xs' \<and> (\<forall>y. (y = x \<or> qFresh xs y X) \<and> (y = x' \<or> qFresh xs y X') \<longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs) \<Longrightarrow> xs = xs' \<and> (\<forall>y. qFresh xs y X \<and> qFresh xs y X' \<longrightarrow> X #[[y \<and> x]]_xs #= X' #[[y \<and> x']]_xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
alphaAbs_all_equal_or_qFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_all_qFresh xs x X xs' x' X'

goal (1 subgoal):
 1. alphaAbs_all_qFresh xs x X xs' x' X'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
qAbs xs x X $= qAbs xs' x' X' \<Longrightarrow> alphaAbs_all_equal_or_qFresh xs x X xs' x' X'
alphaAbs_all_equal_or_qFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_all_qFresh xs x X xs' x' X'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
qAbs xs x X $= qAbs xs' x' X' \<Longrightarrow> alphaAbs_all_equal_or_qFresh xs x X xs' x' X'
alphaAbs_all_equal_or_qFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_all_qFresh xs x X xs' x' X'

goal (1 subgoal):
 1. alphaAbs_all_qFresh xs x X xs' x' X'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
qAbs xs x X $= qAbs xs' x' X' \<Longrightarrow> alphaAbs_all_equal_or_qFresh xs x X xs' x' X'
alphaAbs_all_equal_or_qFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_all_qFresh xs x X xs' x' X'
qGood X
qAbs xs x X $= qAbs xs' x' X'

goal (1 subgoal):
 1. alphaAbs_all_qFresh xs x X xs' x' X'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
alphaAbs_all_qFresh xs x X xs' x' X'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alphaAbs_qAbs_iff_alphaAbs_all_qFresh:
assumes "qGood X" and "qGood X'"
shows "(qAbs xs x X $= qAbs xs' x' X') =
       alphaAbs_all_qFresh xs x X xs' x' X'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_qFresh xs x X xs' x' X'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_qFresh xs x X xs' x' X'
[PROOF STEP]
let ?Left = "(qAbs xs x X $= qAbs xs' x' X')"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_qFresh xs x X xs' x' X'
[PROOF STEP]
let ?Middle = "alphaAbs_all_qAFresh xs x X xs' x' X'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_qFresh xs x X xs' x' X'
[PROOF STEP]
let ?Right = "alphaAbs_all_qFresh xs x X xs' x' X'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_qFresh xs x X xs' x' X'
[PROOF STEP]
have "?Left \<Longrightarrow> ?Right"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs' x' X' \<Longrightarrow> alphaAbs_all_qFresh xs x X xs' x' X'
[PROOF STEP]
using assms alphaAbs_qAbs_imp_alphaAbs_all_qFresh
[PROOF STATE]
proof (prove)
using this:
qGood X
qGood X'
\<lbrakk>qGood ?X; qAbs ?xs ?x ?X $= qAbs ?xs' ?x' ?X'\<rbrakk> \<Longrightarrow> alphaAbs_all_qFresh ?xs ?x ?X ?xs' ?x' ?X'

goal (1 subgoal):
 1. qAbs xs x X $= qAbs xs' x' X' \<Longrightarrow> alphaAbs_all_qFresh xs x X xs' x' X'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
qAbs xs x X $= qAbs xs' x' X' \<Longrightarrow> alphaAbs_all_qFresh xs x X xs' x' X'

goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_qFresh xs x X xs' x' X'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
qAbs xs x X $= qAbs xs' x' X' \<Longrightarrow> alphaAbs_all_qFresh xs x X xs' x' X'

goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_qFresh xs x X xs' x' X'
[PROOF STEP]
have "?Right \<Longrightarrow> ?Middle"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_all_qFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_all_qAFresh xs x X xs' x' X'
[PROOF STEP]
using alphaAbs_all_qFresh_imp_qAFresh
[PROOF STATE]
proof (prove)
using this:
alphaAbs_all_qFresh ?xs ?x ?X ?xs' ?x' ?X' \<Longrightarrow> alphaAbs_all_qAFresh ?xs ?x ?X ?xs' ?x' ?X'

goal (1 subgoal):
 1. alphaAbs_all_qFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_all_qAFresh xs x X xs' x' X'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
alphaAbs_all_qFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_all_qAFresh xs x X xs' x' X'

goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_qFresh xs x X xs' x' X'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
alphaAbs_all_qFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_all_qAFresh xs x X xs' x' X'

goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_qFresh xs x X xs' x' X'
[PROOF STEP]
have "?Middle \<Longrightarrow> ?Left"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alphaAbs_all_qAFresh xs x X xs' x' X' \<Longrightarrow> qAbs xs x X $= qAbs xs' x' X'
[PROOF STEP]
using assms alphaAbs_qAbs_iff_alphaAbs_all_qAFresh
[PROOF STATE]
proof (prove)
using this:
qGood X
qGood X'
\<lbrakk>qGood ?X; qGood ?X'\<rbrakk> \<Longrightarrow> (qAbs ?xs ?x ?X $= qAbs ?xs' ?x' ?X') = alphaAbs_all_qAFresh ?xs ?x ?X ?xs' ?x' ?X'

goal (1 subgoal):
 1. alphaAbs_all_qAFresh xs x X xs' x' X' \<Longrightarrow> qAbs xs x X $= qAbs xs' x' X'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
alphaAbs_all_qAFresh xs x X xs' x' X' \<Longrightarrow> qAbs xs x X $= qAbs xs' x' X'

goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_qFresh xs x X xs' x' X'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
qAbs xs x X $= qAbs xs' x' X' \<Longrightarrow> alphaAbs_all_qFresh xs x X xs' x' X'
alphaAbs_all_qFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_all_qAFresh xs x X xs' x' X'
alphaAbs_all_qAFresh xs x X xs' x' X' \<Longrightarrow> qAbs xs x X $= qAbs xs' x' X'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
qAbs xs x X $= qAbs xs' x' X' \<Longrightarrow> alphaAbs_all_qFresh xs x X xs' x' X'
alphaAbs_all_qFresh xs x X xs' x' X' \<Longrightarrow> alphaAbs_all_qAFresh xs x X xs' x' X'
alphaAbs_all_qAFresh xs x X xs' x' X' \<Longrightarrow> qAbs xs x X $= qAbs xs' x' X'

goal (1 subgoal):
 1. (qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_qFresh xs x X xs' x' X'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(qAbs xs x X $= qAbs xs' x' X') = alphaAbs_all_qFresh xs x X xs' x' X'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reverse_subpaths_join:
  shows " subpath 1 (1 / 2) p +++ subpath (1 / 2) 0 p = reversepath p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subpath 1 (1 / 2) p +++ subpath (1 / 2) 0 p = reversepath p
[PROOF STEP]
using reversepath_subpath join_subpaths_middle pathfinish_subpath pathstart_subpath reversepath_joinpaths
[PROOF STATE]
proof (prove)
using this:
reversepath (subpath ?u ?v ?g) = subpath ?v ?u ?g
subpath 0 (1 / 2) ?p +++ subpath (1 / 2) 1 ?p = ?p
pathfinish (subpath ?u ?v ?g) = ?g ?v
pathstart (subpath ?u ?v ?g) = ?g ?u
pathfinish ?g1.0 = pathstart ?g2.0 \<Longrightarrow> reversepath (?g1.0 +++ ?g2.0) = reversepath ?g2.0 +++ reversepath ?g1.0

goal (1 subgoal):
 1. subpath 1 (1 / 2) p +++ subpath (1 / 2) 0 p = reversepath p
[PROOF STEP]
by (metis (no_types, lifting))


[STATEMENT]
lemma line_integral_on_pair_straight_path:
  fixes F::"('a::euclidean_space) \<Rightarrow> 'a" and g :: "real \<Rightarrow> real" and \<gamma>
  assumes gamma_const: "\<forall>x. \<gamma>(x)\<bullet> i = a"
      and gamma_smooth: "\<forall>x \<in> {0 .. 1}. \<gamma> differentiable at x"
  shows "(line_integral F {i} \<gamma>) = 0" "(line_integral_exists F {i} \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F {i} \<gamma> = 0 &&& line_integral_exists F {i} \<gamma>
[PROOF STEP]
proof (simp add: line_integral_def)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = 0
 2. line_integral_exists F {i} \<gamma>
[PROOF STEP]
have *: "F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i) = 0"
    if "0 \<le> x \<and> x \<le> 1" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i) = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i) = 0
[PROOF STEP]
have "((\<lambda>x. \<gamma>(x)\<bullet> i) has_vector_derivative 0) (at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative 0) (at x)
[PROOF STEP]
using vector_derivative_const_at[of "a" "x"] and gamma_const
[PROOF STATE]
proof (prove)
using this:
vector_derivative (\<lambda>x. a) (at x) = 0
\<forall>x. \<gamma> x \<bullet> i = a

goal (1 subgoal):
 1. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative 0) (at x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative 0) (at x)

goal (1 subgoal):
 1. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i) = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative 0) (at x)
[PROOF STEP]
have "(vector_derivative \<gamma> (at x) \<bullet> i) = 0"
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative 0) (at x)

goal (1 subgoal):
 1. vector_derivative \<gamma> (at x) \<bullet> i = 0
[PROOF STEP]
using derivative_component_fun_component[ of "\<gamma>" "x" "i"]
        and gamma_smooth and that
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative 0) (at x)
\<gamma> differentiable at x \<Longrightarrow> vector_derivative \<gamma> (at x) \<bullet> i = vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x)
\<forall>x\<in>{0..1}. \<gamma> differentiable at x
0 \<le> x \<and> x \<le> 1

goal (1 subgoal):
 1. vector_derivative \<gamma> (at x) \<bullet> i = 0
[PROOF STEP]
by (simp add: vector_derivative_at)
[PROOF STATE]
proof (state)
this:
vector_derivative \<gamma> (at x) \<bullet> i = 0

goal (1 subgoal):
 1. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i) = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vector_derivative \<gamma> (at x) \<bullet> i = 0
[PROOF STEP]
have "(vector_derivative \<gamma> (at x within {0 .. 1}) \<bullet> i) = 0"
[PROOF STATE]
proof (prove)
using this:
vector_derivative \<gamma> (at x) \<bullet> i = 0

goal (1 subgoal):
 1. vector_derivative \<gamma> (at x within {0..1}) \<bullet> i = 0
[PROOF STEP]
using has_vector_derivative_at_within vector_derivative_at_within_ivl that
[PROOF STATE]
proof (prove)
using this:
vector_derivative \<gamma> (at x) \<bullet> i = 0
(?f has_vector_derivative ?f') (at ?x) \<Longrightarrow> (?f has_vector_derivative ?f') (at ?x within ?S)
\<lbrakk>(?f has_vector_derivative ?f') (at ?x); ?a \<le> ?x; ?x \<le> ?b; ?a < ?b\<rbrakk> \<Longrightarrow> vector_derivative ?f (at ?x within {?a..?b}) = ?f'
0 \<le> x \<and> x \<le> 1

goal (1 subgoal):
 1. vector_derivative \<gamma> (at x within {0..1}) \<bullet> i = 0
[PROOF STEP]
by (metis atLeastAtMost_iff gamma_smooth vector_derivative_works zero_less_one)
[PROOF STATE]
proof (state)
this:
vector_derivative \<gamma> (at x within {0..1}) \<bullet> i = 0

goal (1 subgoal):
 1. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i) = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vector_derivative \<gamma> (at x within {0..1}) \<bullet> i = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vector_derivative \<gamma> (at x within {0..1}) \<bullet> i = 0

goal (1 subgoal):
 1. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i) = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 \<le> ?x \<and> ?x \<le> 1 \<Longrightarrow> F (\<gamma> ?x) \<bullet> i * (vector_derivative \<gamma> (at ?x within {0..1}) \<bullet> i) = 0

goal (2 subgoals):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = 0
 2. line_integral_exists F {i} \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 \<le> ?x \<and> ?x \<le> 1 \<Longrightarrow> F (\<gamma> ?x) \<bullet> i * (vector_derivative \<gamma> (at ?x within {0..1}) \<bullet> i) = 0
[PROOF STEP]
have "((\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) has_integral 0) {0..1}"
[PROOF STATE]
proof (prove)
using this:
0 \<le> ?x \<and> ?x \<le> 1 \<Longrightarrow> F (\<gamma> ?x) \<bullet> i * (vector_derivative \<gamma> (at ?x within {0..1}) \<bullet> i) = 0

goal (1 subgoal):
 1. ((\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) has_integral 0) {0..1}
[PROOF STEP]
using has_integral_is_0[of "{0 .. 1}" "(\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i))"]
[PROOF STATE]
proof (prove)
using this:
0 \<le> ?x \<and> ?x \<le> 1 \<Longrightarrow> F (\<gamma> ?x) \<bullet> i * (vector_derivative \<gamma> (at ?x within {0..1}) \<bullet> i) = 0
(\<And>x. x \<in> {0..1} \<Longrightarrow> F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i) = 0) \<Longrightarrow> ((\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) has_integral 0) {0..1}

goal (1 subgoal):
 1. ((\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) has_integral 0) {0..1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) has_integral 0) {0..1}

goal (2 subgoals):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = 0
 2. line_integral_exists F {i} \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) has_integral 0) {0..1}
[PROOF STEP]
have "((\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) integrable_on {0..1})"
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) has_integral 0) {0..1}

goal (1 subgoal):
 1. (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) integrable_on {0..1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) integrable_on {0..1}

goal (2 subgoals):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = 0
 2. line_integral_exists F {i} \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) integrable_on {0..1}
[PROOF STEP]
show "line_integral_exists F {i} \<gamma>"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) integrable_on {0..1}

goal (1 subgoal):
 1. line_integral_exists F {i} \<gamma>
[PROOF STEP]
by (auto simp add:line_integral_exists_def)
[PROOF STATE]
proof (state)
this:
line_integral_exists F {i} \<gamma>

goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = 0
[PROOF STEP]
show "integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = 0
[PROOF STEP]
using * has_integral_is_0[of "{0 .. 1}" "(\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i))"]
[PROOF STATE]
proof (prove)
using this:
0 \<le> ?x \<and> ?x \<le> 1 \<Longrightarrow> F (\<gamma> ?x) \<bullet> i * (vector_derivative \<gamma> (at ?x within {0..1}) \<bullet> i) = 0
(\<And>x. x \<in> {0..1} \<Longrightarrow> F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i) = 0) \<Longrightarrow> ((\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) has_integral 0) {0..1}

goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma line_integral_on_pair_path_strong:
  fixes F::"('a::euclidean_space) \<Rightarrow> ('a)" and
    g::"real \<Rightarrow> 'a" and
    \<gamma>::"(real \<Rightarrow> 'a)" and
    i::'a
  assumes i_norm_1: "norm i = 1" and
    g_orthogonal_to_i: "\<forall>x. g(x) \<bullet> i = 0" and
    gamma_is_in_terms_of_i: "\<gamma> = (\<lambda>x. f(x) *\<^sub>R i + g(f(x)))" and
    gamma_smooth: "\<gamma> piecewise_C1_differentiable_on {0 .. 1}" and
    g_continuous_on_f: "continuous_on (f ` {0..1}) g" and
    path_start_le_path_end: "(pathstart \<gamma>) \<bullet> i \<le> (pathfinish \<gamma>) \<bullet> i" and
    field_i_comp_cont: "continuous_on (path_image \<gamma>) (\<lambda>x. F x \<bullet> i)"
  shows "line_integral F {i} \<gamma>
         = integral (cbox ((pathstart \<gamma>) \<bullet> i) ((pathfinish \<gamma>) \<bullet> i)) (\<lambda>f_var. (F (f_var *\<^sub>R i + g(f_var)) \<bullet> i))"
    "line_integral_exists F {i} \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F {i} \<gamma> = integral (cbox (pathstart \<gamma> \<bullet> i) (pathfinish \<gamma> \<bullet> i)) (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i) &&& line_integral_exists F {i} \<gamma>
[PROOF STEP]
proof (simp add: line_integral_def)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
 2. line_integral_exists F {i} \<gamma>
[PROOF STEP]
obtain s where gamma_differentiable: "finite s" "(\<forall>x \<in> {0 .. 1} - s. \<gamma> differentiable at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. \<lbrakk>finite s; \<forall>x\<in>{0..1} - s. \<gamma> differentiable at x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using gamma_smooth
[PROOF STATE]
proof (prove)
using this:
\<gamma> piecewise_C1_differentiable_on {0..1}

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>finite s; \<forall>x\<in>{0..1} - s. \<gamma> differentiable at x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: C1_differentiable_on_eq piecewise_C1_differentiable_on_def)
[PROOF STATE]
proof (state)
this:
finite s
\<forall>x\<in>{0..1} - s. \<gamma> differentiable at x

goal (2 subgoals):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
 2. line_integral_exists F {i} \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite s
\<forall>x\<in>{0..1} - s. \<gamma> differentiable at x
[PROOF STEP]
have gamma_i_component_smooth: "\<forall>x \<in> {0 .. 1} - s. (\<lambda>x. \<gamma> x \<bullet> i) differentiable at x"
[PROOF STATE]
proof (prove)
using this:
finite s
\<forall>x\<in>{0..1} - s. \<gamma> differentiable at x

goal (1 subgoal):
 1. \<forall>x\<in>{0..1} - s. (\<lambda>x. \<gamma> x \<bullet> i) differentiable at x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{0..1} - s. (\<lambda>x. \<gamma> x \<bullet> i) differentiable at x

goal (2 subgoals):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
 2. line_integral_exists F {i} \<gamma>
[PROOF STEP]
have field_cont_on_path: "continuous_on ((\<lambda>x. \<gamma> x \<bullet> i) ` {0..1}) (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on ((\<lambda>x. \<gamma> x \<bullet> i) ` {0..1}) (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. continuous_on ((\<lambda>x. \<gamma> x \<bullet> i) ` {0..1}) (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
[PROOF STEP]
have 0: "(\<lambda>x. \<gamma> x \<bullet> i) = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<gamma> x \<bullet> i) = f
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<gamma> x \<bullet> i = f x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<gamma> x \<bullet> i = f x
[PROOF STEP]
show "\<gamma> x \<bullet> i = f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma> x \<bullet> i = f x
[PROOF STEP]
using g_orthogonal_to_i i_norm_1
[PROOF STATE]
proof (prove)
using this:
\<forall>x. g x \<bullet> i = 0
norm i = 1

goal (1 subgoal):
 1. \<gamma> x \<bullet> i = f x
[PROOF STEP]
by (simp only: gamma_is_in_terms_of_i  real_inner_class.inner_add_left g_orthogonal_to_i inner_scaleR_left inner_same_Basis norm_eq_1)
[PROOF STATE]
proof (state)
this:
\<gamma> x \<bullet> i = f x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<gamma> x \<bullet> i) = f

goal (1 subgoal):
 1. continuous_on ((\<lambda>x. \<gamma> x \<bullet> i) ` {0..1}) (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on ((\<lambda>x. \<gamma> x \<bullet> i) ` {0..1}) (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
[PROOF STEP]
unfolding 0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on (f ` {0..1}) (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
[PROOF STEP]
apply (rule continuous_on_compose2 [of _ "(\<lambda>x. F(x)  \<bullet> i)" "f ` { 0..1}" "(\<lambda>x. x *\<^sub>R i + g x)"]
          field_i_comp_cont g_continuous_on_f field_i_comp_cont continuous_intros)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>f_var. f_var *\<^sub>R i + g f_var) ` f ` {0..1} \<subseteq> path_image \<gamma>
[PROOF STEP]
by (auto simp add: gamma_is_in_terms_of_i path_image_def)
[PROOF STATE]
proof (state)
this:
continuous_on ((\<lambda>x. \<gamma> x \<bullet> i) ` {0..1}) (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
continuous_on ((\<lambda>x. \<gamma> x \<bullet> i) ` {0..1}) (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)

goal (2 subgoals):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
 2. line_integral_exists F {i} \<gamma>
[PROOF STEP]
have path_start_le_path_end': "\<gamma> 0 \<bullet> i \<le> \<gamma> 1 \<bullet> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma> 0 \<bullet> i \<le> \<gamma> 1 \<bullet> i
[PROOF STEP]
using path_start_le_path_end
[PROOF STATE]
proof (prove)
using this:
pathstart \<gamma> \<bullet> i \<le> pathfinish \<gamma> \<bullet> i

goal (1 subgoal):
 1. \<gamma> 0 \<bullet> i \<le> \<gamma> 1 \<bullet> i
[PROOF STEP]
by (auto simp add: pathstart_def pathfinish_def)
[PROOF STATE]
proof (state)
this:
\<gamma> 0 \<bullet> i \<le> \<gamma> 1 \<bullet> i

goal (2 subgoals):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
 2. line_integral_exists F {i} \<gamma>
[PROOF STEP]
have gamm_cont: "continuous_on {0..1} (\<lambda>a. \<gamma> a \<bullet> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>a. \<gamma> a \<bullet> i)
[PROOF STEP]
apply(rule continuous_on_inner)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. continuous_on {0..1} \<gamma>
 2. continuous_on {0..1} (\<lambda>x. i)
[PROOF STEP]
using gamma_smooth
[PROOF STATE]
proof (prove)
using this:
\<gamma> piecewise_C1_differentiable_on {0..1}

goal (2 subgoals):
 1. continuous_on {0..1} \<gamma>
 2. continuous_on {0..1} (\<lambda>x. i)
[PROOF STEP]
apply (simp add: piecewise_C1_differentiable_on_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. i)
[PROOF STEP]
using continuous_on_const
[PROOF STATE]
proof (prove)
using this:
continuous_on ?s (\<lambda>x. ?c)

goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
continuous_on {0..1} (\<lambda>a. \<gamma> a \<bullet> i)

goal (2 subgoals):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
 2. line_integral_exists F {i} \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
continuous_on {0..1} (\<lambda>a. \<gamma> a \<bullet> i)
[PROOF STEP]
obtain c d where cd: "c \<le> d" "(\<lambda>a. \<gamma> a \<bullet> i) ` {0..1} = {c..d}"
[PROOF STATE]
proof (prove)
using this:
continuous_on {0..1} (\<lambda>a. \<gamma> a \<bullet> i)

goal (1 subgoal):
 1. (\<And>c d. \<lbrakk>c \<le> d; (\<lambda>a. \<gamma> a \<bullet> i) ` {0..1} = {c..d}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson continuous_image_closed_interval zero_le_one)
[PROOF STATE]
proof (state)
this:
c \<le> d
(\<lambda>a. \<gamma> a \<bullet> i) ` {0..1} = {c..d}

goal (2 subgoals):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
 2. line_integral_exists F {i} \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c \<le> d
(\<lambda>a. \<gamma> a \<bullet> i) ` {0..1} = {c..d}
[PROOF STEP]
have subset_cd: "(\<lambda>a. \<gamma> a \<bullet> i) ` {0..1} \<subseteq> {c..d}"
[PROOF STATE]
proof (prove)
using this:
c \<le> d
(\<lambda>a. \<gamma> a \<bullet> i) ` {0..1} = {c..d}

goal (1 subgoal):
 1. (\<lambda>a. \<gamma> a \<bullet> i) ` {0..1} \<subseteq> {c..d}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>a. \<gamma> a \<bullet> i) ` {0..1} \<subseteq> {c..d}

goal (2 subgoals):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
 2. line_integral_exists F {i} \<gamma>
[PROOF STEP]
have field_cont_on_path_cd:
    "continuous_on {c..d} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on {c..d} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
[PROOF STEP]
using field_cont_on_path cd
[PROOF STATE]
proof (prove)
using this:
continuous_on ((\<lambda>x. \<gamma> x \<bullet> i) ` {0..1}) (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
c \<le> d
(\<lambda>a. \<gamma> a \<bullet> i) ` {0..1} = {c..d}

goal (1 subgoal):
 1. continuous_on {c..d} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
continuous_on {c..d} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)

goal (2 subgoals):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
 2. line_integral_exists F {i} \<gamma>
[PROOF STEP]
have path_vector_deriv_line_integrals:
    "\<forall>x\<in>{0..1} - s. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative
                                          vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x))
                                                  (at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{0..1} - s. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x)) (at x)
[PROOF STEP]
using gamma_i_component_smooth and derivative_component_fun_component and
      vector_derivative_works
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0..1} - s. (\<lambda>x. \<gamma> x \<bullet> i) differentiable at x
?f differentiable at ?x \<Longrightarrow> vector_derivative ?f (at ?x) \<bullet> ?i = vector_derivative (\<lambda>x. ?f x \<bullet> ?i) (at ?x)
(?f differentiable ?net) = (?f has_vector_derivative vector_derivative ?f ?net) ?net

goal (1 subgoal):
 1. \<forall>x\<in>{0..1} - s. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x)) (at x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{0..1} - s. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x)) (at x)

goal (2 subgoals):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
 2. line_integral_exists F {i} \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>{0..1} - s. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x)) (at x)
[PROOF STEP]
have "\<forall>x\<in>{0..1} - s. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative
                                          vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within ({0..1})))
                                                  (at x within ({0..1}))"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0..1} - s. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x)) (at x)

goal (1 subgoal):
 1. \<forall>x\<in>{0..1} - s. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})) (at x within {0..1})
[PROOF STEP]
using has_vector_derivative_at_within vector_derivative_at_within_ivl
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0..1} - s. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x)) (at x)
(?f has_vector_derivative ?f') (at ?x) \<Longrightarrow> (?f has_vector_derivative ?f') (at ?x within ?S)
\<lbrakk>(?f has_vector_derivative ?f') (at ?x); ?a \<le> ?x; ?x \<le> ?b; ?a < ?b\<rbrakk> \<Longrightarrow> vector_derivative ?f (at ?x within {?a..?b}) = ?f'

goal (1 subgoal):
 1. \<forall>x\<in>{0..1} - s. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})) (at x within {0..1})
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{0..1} - s. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})) (at x within {0..1})

goal (2 subgoals):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
 2. line_integral_exists F {i} \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>{0..1} - s. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})) (at x within {0..1})
[PROOF STEP]
have has_int:"((\<lambda>x. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) *\<^sub>R (F ((\<gamma> x \<bullet> i) *\<^sub>R i + g (\<gamma> x \<bullet> i)) \<bullet> i)) has_integral
           integral {\<gamma> 0 \<bullet> i..\<gamma> 1 \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)) {0..1}"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0..1} - s. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})) (at x within {0..1})

goal (1 subgoal):
 1. ((\<lambda>x. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) *\<^sub>R (F ((\<gamma> x \<bullet> i) *\<^sub>R i + g (\<gamma> x \<bullet> i)) \<bullet> i)) has_integral integral {\<gamma> 0 \<bullet> i..\<gamma> 1 \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)) {0..1}
[PROOF STEP]
using has_integral_substitution_strong[OF gamma_differentiable(1) rel_simps(44)
        path_start_le_path_end' subset_cd field_cont_on_path_cd gamm_cont,
        of "(\<lambda>x. vector_derivative (\<lambda>x. \<gamma>(x) \<bullet> i) (at x within ({0..1})))"]
      gamma_is_in_terms_of_i
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0..1} - s. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})) (at x within {0..1})
(\<And>x. x \<in> {0..1} - s \<Longrightarrow> ((\<lambda>a. \<gamma> a \<bullet> i) has_real_derivative vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})) (at x within {0..1})) \<Longrightarrow> ((\<lambda>x. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) *\<^sub>R (F ((\<gamma> x \<bullet> i) *\<^sub>R i + g (\<gamma> x \<bullet> i)) \<bullet> i)) has_integral integral {\<gamma> 0 \<bullet> i..\<gamma> 1 \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)) {0..1}
\<gamma> = (\<lambda>x. f x *\<^sub>R i + g (f x))

goal (1 subgoal):
 1. ((\<lambda>x. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) *\<^sub>R (F ((\<gamma> x \<bullet> i) *\<^sub>R i + g (\<gamma> x \<bullet> i)) \<bullet> i)) has_integral integral {\<gamma> 0 \<bullet> i..\<gamma> 1 \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)) {0..1}
[PROOF STEP]
by (auto simp only: has_real_derivative_iff_has_vector_derivative)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) *\<^sub>R (F ((\<gamma> x \<bullet> i) *\<^sub>R i + g (\<gamma> x \<bullet> i)) \<bullet> i)) has_integral integral {\<gamma> 0 \<bullet> i..\<gamma> 1 \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)) {0..1}

goal (2 subgoals):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
 2. line_integral_exists F {i} \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>x. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) *\<^sub>R (F ((\<gamma> x \<bullet> i) *\<^sub>R i + g (\<gamma> x \<bullet> i)) \<bullet> i)) has_integral integral {\<gamma> 0 \<bullet> i..\<gamma> 1 \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)) {0..1}
[PROOF STEP]
have has_int':"((\<lambda>x. (F(\<gamma>(x)) \<bullet> i)*(vector_derivative (\<lambda>x. \<gamma>(x) \<bullet> i) (at x within ({0..1})))) has_integral
           integral {((pathstart \<gamma>) \<bullet> i)..((pathfinish \<gamma>) \<bullet> i)} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)) {0..1}"
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) *\<^sub>R (F ((\<gamma> x \<bullet> i) *\<^sub>R i + g (\<gamma> x \<bullet> i)) \<bullet> i)) has_integral integral {\<gamma> 0 \<bullet> i..\<gamma> 1 \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)) {0..1}

goal (1 subgoal):
 1. ((\<lambda>x. F (\<gamma> x) \<bullet> i * vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})) has_integral integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)) {0..1}
[PROOF STEP]
using  gamma_is_in_terms_of_i i_norm_1
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) *\<^sub>R (F ((\<gamma> x \<bullet> i) *\<^sub>R i + g (\<gamma> x \<bullet> i)) \<bullet> i)) has_integral integral {\<gamma> 0 \<bullet> i..\<gamma> 1 \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)) {0..1}
\<gamma> = (\<lambda>x. f x *\<^sub>R i + g (f x))
norm i = 1

goal (1 subgoal):
 1. ((\<lambda>x. F (\<gamma> x) \<bullet> i * vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})) has_integral integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)) {0..1}
[PROOF STEP]
apply (auto simp add: pathstart_def pathfinish_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((\<lambda>x. vector_derivative (\<lambda>x. (f x *\<^sub>R i + g (f x)) \<bullet> i) (at x within {0..1}) * (F (((f x *\<^sub>R i + g (f x)) \<bullet> i) *\<^sub>R i + g ((f x *\<^sub>R i + g (f x)) \<bullet> i)) \<bullet> i)) has_integral integral {(f 0 *\<^sub>R i + g (f 0)) \<bullet> i..(f 1 *\<^sub>R i + g (f 1)) \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)) {0..1}; \<gamma> = (\<lambda>x. f x *\<^sub>R i + g (f x)); norm i = 1\<rbrakk> \<Longrightarrow> ((\<lambda>x. F (f x *\<^sub>R i + g (f x)) \<bullet> i * vector_derivative (\<lambda>x. (f x *\<^sub>R i + g (f x)) \<bullet> i) (at x within {0..1})) has_integral integral {(f 0 *\<^sub>R i + g (f 0)) \<bullet> i..(f 1 *\<^sub>R i + g (f 1)) \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)) {0..1}
[PROOF STEP]
apply (simp only:  real_inner_class.inner_add_left inner_not_same_Basis g_orthogonal_to_i inner_scaleR_left norm_eq_1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((\<lambda>x. vector_derivative (\<lambda>x. f x * 1 + 0) (at x within {0..1}) * (F ((f x * 1 + 0) *\<^sub>R i + g (f x * 1 + 0)) \<bullet> i)) has_integral integral {f 0 * 1 + 0..f 1 * 1 + 0} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)) {0..1}; \<gamma> = (\<lambda>x. f x *\<^sub>R i + g (f x)); i \<bullet> i = 1\<rbrakk> \<Longrightarrow> ((\<lambda>x. F (f x *\<^sub>R i + g (f x)) \<bullet> i * vector_derivative (\<lambda>x. f x * 1 + 0) (at x within {0..1})) has_integral integral {f 0 * 1 + 0..f 1 * 1 + 0} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)) {0..1}
[PROOF STEP]
by (auto simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. F (\<gamma> x) \<bullet> i * vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})) has_integral integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)) {0..1}

goal (2 subgoals):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
 2. line_integral_exists F {i} \<gamma>
[PROOF STEP]
have substitute:
    "integral ({((pathstart \<gamma>) \<bullet> i)..((pathfinish \<gamma>) \<bullet> i)}) (\<lambda>f_var. (F (f_var *\<^sub>R i + g(f_var)) \<bullet> i))
                 = integral ({0..1}) (\<lambda>x. (F(\<gamma>(x)) \<bullet> i)*(vector_derivative (\<lambda>x. \<gamma>(x) \<bullet> i) (at x within ({0..1}))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i) = integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}))
[PROOF STEP]
using gamma_is_in_terms_of_i integral_unique[OF has_int] i_norm_1
[PROOF STATE]
proof (prove)
using this:
\<gamma> = (\<lambda>x. f x *\<^sub>R i + g (f x))
integral {0..1} (\<lambda>x. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) *\<^sub>R (F ((\<gamma> x \<bullet> i) *\<^sub>R i + g (\<gamma> x \<bullet> i)) \<bullet> i)) = integral {\<gamma> 0 \<bullet> i..\<gamma> 1 \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
norm i = 1

goal (1 subgoal):
 1. integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i) = integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}))
[PROOF STEP]
apply (auto simp add: pathstart_def pathfinish_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<gamma> = (\<lambda>x. f x *\<^sub>R i + g (f x)); integral {0..1} (\<lambda>x. vector_derivative (\<lambda>x. (f x *\<^sub>R i + g (f x)) \<bullet> i) (at x within {0..1}) * (F (((f x *\<^sub>R i + g (f x)) \<bullet> i) *\<^sub>R i + g ((f x *\<^sub>R i + g (f x)) \<bullet> i)) \<bullet> i)) = integral {(f 0 *\<^sub>R i + g (f 0)) \<bullet> i..(f 1 *\<^sub>R i + g (f 1)) \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i); norm i = 1\<rbrakk> \<Longrightarrow> integral {(f 0 *\<^sub>R i + g (f 0)) \<bullet> i..(f 1 *\<^sub>R i + g (f 1)) \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i) = integral {0..1} (\<lambda>x. F (f x *\<^sub>R i + g (f x)) \<bullet> i * vector_derivative (\<lambda>x. (f x *\<^sub>R i + g (f x)) \<bullet> i) (at x within {0..1}))
[PROOF STEP]
apply (simp only:  real_inner_class.inner_add_left inner_not_same_Basis g_orthogonal_to_i inner_scaleR_left norm_eq_1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<gamma> = (\<lambda>x. f x *\<^sub>R i + g (f x)); integral {0..1} (\<lambda>x. vector_derivative (\<lambda>x. f x * 1 + 0) (at x within {0..1}) * (F ((f x * 1 + 0) *\<^sub>R i + g (f x * 1 + 0)) \<bullet> i)) = integral {f 0 * 1 + 0..f 1 * 1 + 0} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i); i \<bullet> i = 1\<rbrakk> \<Longrightarrow> integral {f 0 * 1 + 0..f 1 * 1 + 0} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i) = integral {0..1} (\<lambda>x. F (f x *\<^sub>R i + g (f x)) \<bullet> i * vector_derivative (\<lambda>x. f x * 1 + 0) (at x within {0..1}))
[PROOF STEP]
by (auto simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i) = integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}))

goal (2 subgoals):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
 2. line_integral_exists F {i} \<gamma>
[PROOF STEP]
have comp_in_eq_comp_out: "\<forall>x \<in> {0..1} - s.
            (vector_derivative (\<lambda>x. \<gamma>(x) \<bullet> i) (at x within {0..1}))
                = (vector_derivative \<gamma> (at x within {0..1})) \<bullet> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{0..1} - s. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - s \<Longrightarrow> vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
[PROOF STEP]
fix x:: real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - s \<Longrightarrow> vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
[PROOF STEP]
assume ass:"x \<in> {0..1} -s"
[PROOF STATE]
proof (state)
this:
x \<in> {0..1} - s

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - s \<Longrightarrow> vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> {0..1} - s
[PROOF STEP]
have x_bounds:"x \<in> {0..1}"
[PROOF STATE]
proof (prove)
using this:
x \<in> {0..1} - s

goal (1 subgoal):
 1. x \<in> {0..1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> {0..1}

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - s \<Longrightarrow> vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
[PROOF STEP]
have "\<gamma> differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma> differentiable at x
[PROOF STEP]
using ass gamma_differentiable
[PROOF STATE]
proof (prove)
using this:
x \<in> {0..1} - s
finite s
\<forall>x\<in>{0..1} - s. \<gamma> differentiable at x

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

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - s \<Longrightarrow> vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<gamma> differentiable at x
[PROOF STEP]
have dotprod_in_is_out:
      "vector_derivative (\<lambda>x. \<gamma>(x) \<bullet> i) (at x)
                         = (vector_derivative \<gamma> (at x)) \<bullet> i"
[PROOF STATE]
proof (prove)
using this:
\<gamma> differentiable at x

goal (1 subgoal):
 1. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x) = vector_derivative \<gamma> (at x) \<bullet> i
[PROOF STEP]
using derivative_component_fun_component
[PROOF STATE]
proof (prove)
using this:
\<gamma> differentiable at x
?f differentiable at ?x \<Longrightarrow> vector_derivative ?f (at ?x) \<bullet> ?i = vector_derivative (\<lambda>x. ?f x \<bullet> ?i) (at ?x)

goal (1 subgoal):
 1. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x) = vector_derivative \<gamma> (at x) \<bullet> i
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x) = vector_derivative \<gamma> (at x) \<bullet> i

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - s \<Longrightarrow> vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x) = vector_derivative \<gamma> (at x) \<bullet> i
[PROOF STEP]
have 0: "(vector_derivative \<gamma> (at x)) \<bullet> i = (vector_derivative \<gamma> (at x within {0..1})) \<bullet> i"
[PROOF STATE]
proof (prove)
using this:
vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x) = vector_derivative \<gamma> (at x) \<bullet> i

goal (1 subgoal):
 1. vector_derivative \<gamma> (at x) \<bullet> i = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x) = vector_derivative \<gamma> (at x) \<bullet> i \<Longrightarrow> vector_derivative \<gamma> (at x) \<bullet> i = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
[PROOF STEP]
have "(\<gamma> has_vector_derivative vector_derivative \<gamma> (at x)) (at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<gamma> has_vector_derivative vector_derivative \<gamma> (at x)) (at x)
[PROOF STEP]
using \<open>\<gamma> differentiable at x\<close> vector_derivative_works
[PROOF STATE]
proof (prove)
using this:
\<gamma> differentiable at x
(?f differentiable ?net) = (?f has_vector_derivative vector_derivative ?f ?net) ?net

goal (1 subgoal):
 1. (\<gamma> has_vector_derivative vector_derivative \<gamma> (at x)) (at x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<gamma> has_vector_derivative vector_derivative \<gamma> (at x)) (at x)

goal (1 subgoal):
 1. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x) = vector_derivative \<gamma> (at x) \<bullet> i \<Longrightarrow> vector_derivative \<gamma> (at x) \<bullet> i = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<gamma> has_vector_derivative vector_derivative \<gamma> (at x)) (at x)

goal (1 subgoal):
 1. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x) = vector_derivative \<gamma> (at x) \<bullet> i \<Longrightarrow> vector_derivative \<gamma> (at x) \<bullet> i = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
[PROOF STEP]
have "0 \<le> x \<and> x \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> x \<and> x \<le> 1
[PROOF STEP]
using x_bounds
[PROOF STATE]
proof (prove)
using this:
x \<in> {0..1}

goal (1 subgoal):
 1. 0 \<le> x \<and> x \<le> 1
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
0 \<le> x \<and> x \<le> 1

goal (1 subgoal):
 1. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x) = vector_derivative \<gamma> (at x) \<bullet> i \<Longrightarrow> vector_derivative \<gamma> (at x) \<bullet> i = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<gamma> has_vector_derivative vector_derivative \<gamma> (at x)) (at x)
0 \<le> x \<and> x \<le> 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<gamma> has_vector_derivative vector_derivative \<gamma> (at x)) (at x)
0 \<le> x \<and> x \<le> 1

goal (1 subgoal):
 1. vector_derivative \<gamma> (at x) \<bullet> i = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
[PROOF STEP]
by (simp add: vector_derivative_at_within_ivl)
[PROOF STATE]
proof (state)
this:
vector_derivative \<gamma> (at x) \<bullet> i = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
vector_derivative \<gamma> (at x) \<bullet> i = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - s \<Longrightarrow> vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
[PROOF STEP]
have 1: "vector_derivative (\<lambda>x. \<gamma>(x) \<bullet> i) (at x) = vector_derivative (\<lambda>x. \<gamma>(x) \<bullet> i) (at x within {0..1})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x) = vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})
[PROOF STEP]
using path_vector_deriv_line_integrals and vector_derivative_at_within_ivl and
        x_bounds
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0..1} - s. ((\<lambda>x. \<gamma> x \<bullet> i) has_vector_derivative vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x)) (at x)
\<lbrakk>(?f has_vector_derivative ?f') (at ?x); ?a \<le> ?x; ?x \<le> ?b; ?a < ?b\<rbrakk> \<Longrightarrow> vector_derivative ?f (at ?x within {?a..?b}) = ?f'
x \<in> {0..1}

goal (1 subgoal):
 1. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x) = vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})
[PROOF STEP]
by (metis ass atLeastAtMost_iff zero_less_one)
[PROOF STATE]
proof (state)
this:
vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x) = vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - s \<Longrightarrow> vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
[PROOF STEP]
show "vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
[PROOF STEP]
using 0 and 1 and dotprod_in_is_out
[PROOF STATE]
proof (prove)
using this:
vector_derivative \<gamma> (at x) \<bullet> i = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x) = vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})
vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x) = vector_derivative \<gamma> (at x) \<bullet> i

goal (1 subgoal):
 1. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{0..1} - s. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i

goal (2 subgoals):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
 2. line_integral_exists F {i} \<gamma>
[PROOF STEP]
show "integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) =
                   integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
[PROOF STEP]
using substitute and comp_in_eq_comp_out and negligible_finite
      Henstock_Kurzweil_Integration.integral_spike
      [of "s" "{0..1}" "(\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i))"
        "(\<lambda>x. F (\<gamma> x) \<bullet> i * vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}))"]
[PROOF STATE]
proof (prove)
using this:
integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i) = integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}))
\<forall>x\<in>{0..1} - s. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
finite ?s \<Longrightarrow> negligible ?s
\<lbrakk>negligible s; \<And>x. x \<in> {0..1} - s \<Longrightarrow> F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i) = F (\<gamma> x) \<bullet> i * vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})\<rbrakk> \<Longrightarrow> integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})) = integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i))

goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)
[PROOF STEP]
by (metis (no_types, lifting) gamma_differentiable(1))
[PROOF STATE]
proof (state)
this:
integral {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) = integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)

goal (1 subgoal):
 1. line_integral_exists F {i} \<gamma>
[PROOF STEP]
have "((\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) has_integral
                   integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)) {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) has_integral integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)) {0..1}
[PROOF STEP]
using has_int' and comp_in_eq_comp_out and negligible_finite
      Henstock_Kurzweil_Integration.has_integral_spike
      [of "s" "{0..1}" "(\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i))"
        "(\<lambda>x. F (\<gamma> x) \<bullet> i * vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}))"
        "integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)"]
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. F (\<gamma> x) \<bullet> i * vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})) has_integral integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)) {0..1}
\<forall>x\<in>{0..1} - s. vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}) = vector_derivative \<gamma> (at x within {0..1}) \<bullet> i
finite ?s \<Longrightarrow> negligible ?s
\<lbrakk>negligible s; \<And>x. x \<in> {0..1} - s \<Longrightarrow> F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i) = F (\<gamma> x) \<bullet> i * vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1}); ((\<lambda>x. F (\<gamma> x) \<bullet> i * vector_derivative (\<lambda>x. \<gamma> x \<bullet> i) (at x within {0..1})) has_integral integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)) {0..1}\<rbrakk> \<Longrightarrow> ((\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) has_integral integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)) {0..1}

goal (1 subgoal):
 1. ((\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) has_integral integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)) {0..1}
[PROOF STEP]
by (metis (no_types, lifting) gamma_differentiable(1))
[PROOF STATE]
proof (state)
this:
((\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) has_integral integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)) {0..1}

goal (1 subgoal):
 1. line_integral_exists F {i} \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) has_integral integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)) {0..1}
[PROOF STEP]
have "(\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) integrable_on {0..1}"
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) has_integral integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)) {0..1}

goal (1 subgoal):
 1. (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) integrable_on {0..1}
[PROOF STEP]
using integrable_on_def
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) has_integral integral {pathstart \<gamma> \<bullet> i..pathfinish \<gamma> \<bullet> i} (\<lambda>f_var. F (f_var *\<^sub>R i + g f_var) \<bullet> i)) {0..1}
(?f integrable_on ?i) = (\<exists>y. (?f has_integral y) ?i)

goal (1 subgoal):
 1. (\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) integrable_on {0..1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) integrable_on {0..1}

goal (1 subgoal):
 1. line_integral_exists F {i} \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) integrable_on {0..1}
[PROOF STEP]
show "line_integral_exists F {i} \<gamma>"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. F (\<gamma> x) \<bullet> i * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> i)) integrable_on {0..1}

goal (1 subgoal):
 1. line_integral_exists F {i} \<gamma>
[PROOF STEP]
by (auto simp add: line_integral_exists_def)
[PROOF STATE]
proof (state)
this:
line_integral_exists F {i} \<gamma>

goal:
No subgoals!
[PROOF STEP]
qed