[STATEMENT]
lemma chain_reparam_chain_line_integral:
  assumes "chain_reparam_chain one_chain1 one_chain2"
    "\<forall>(k2,\<gamma>2)\<in>one_chain2. \<gamma>2 piecewise_C1_differentiable_on {0..1}"
    "\<forall>(k2,\<gamma>2)\<in>one_chain2.\<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)"
    "finite basis"
  and bound1: "boundary_chain one_chain1"
  and bound2: "boundary_chain one_chain2"
  and line: "\<forall>(k2,\<gamma>2)\<in>one_chain2. (\<forall>b\<in>basis. line_integral_exists F {b} \<gamma>2)"
  shows "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2"
    "\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2 &&& \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
 2. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
obtain f where f: "bij f"
    "(\<forall>(k,\<gamma>)\<in>one_chain1. if k = fst (f(k,\<gamma>)) then reparam \<gamma> (snd (f(k,\<gamma>))) else reparam \<gamma> (reversepath (snd (f(k,\<gamma>)))))"
    "f ` one_chain1 = one_chain2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>bij f; \<forall>(k, \<gamma>)\<in>one_chain1. if k = fst (f (k, \<gamma>)) then reparam \<gamma> (snd (f (k, \<gamma>))) else reparam \<gamma> (reversepath (snd (f (k, \<gamma>)))); f ` one_chain1 = one_chain2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
chain_reparam_chain one_chain1 one_chain2

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>bij f; \<forall>(k, \<gamma>)\<in>one_chain1. if k = fst (f (k, \<gamma>)) then reparam \<gamma> (snd (f (k, \<gamma>))) else reparam \<gamma> (reversepath (snd (f (k, \<gamma>)))); f ` one_chain1 = one_chain2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: chain_reparam_chain_def)
[PROOF STATE]
proof (state)
this:
bij f
\<forall>(k, \<gamma>)\<in>one_chain1. if k = fst (f (k, \<gamma>)) then reparam \<gamma> (snd (f (k, \<gamma>))) else reparam \<gamma> (reversepath (snd (f (k, \<gamma>))))
f ` one_chain1 = one_chain2

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
 2. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
have integ_exist_b: "\<forall>(k1,\<gamma>1)\<in>one_chain1. \<forall>b\<in>basis. line_integral_exists F {b} (snd (f (k1, \<gamma>1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k1, \<gamma>1)\<in>one_chain1. \<forall>b\<in>basis. line_integral_exists F {b} (snd (f (k1, \<gamma>1)))
[PROOF STEP]
using line f
[PROOF STATE]
proof (prove)
using this:
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. line_integral_exists F {b} \<gamma>2
bij f
\<forall>(k, \<gamma>)\<in>one_chain1. if k = fst (f (k, \<gamma>)) then reparam \<gamma> (snd (f (k, \<gamma>))) else reparam \<gamma> (reversepath (snd (f (k, \<gamma>))))
f ` one_chain1 = one_chain2

goal (1 subgoal):
 1. \<forall>(k1, \<gamma>1)\<in>one_chain1. \<forall>b\<in>basis. line_integral_exists F {b} (snd (f (k1, \<gamma>1)))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>(k1, \<gamma>1)\<in>one_chain1. \<forall>b\<in>basis. line_integral_exists F {b} (snd (f (k1, \<gamma>1)))

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
 2. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
have valid_cubes: "\<forall>(k1,\<gamma>1)\<in>one_chain1. valid_path (snd (f (k1, \<gamma>1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k1, \<gamma>1)\<in>one_chain1. valid_path (snd (f (k1, \<gamma>1)))
[PROOF STEP]
using assms(2) f(3) valid_path_def
[PROOF STATE]
proof (prove)
using this:
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<gamma>2 piecewise_C1_differentiable_on {0..1}
f ` one_chain1 = one_chain2
valid_path ?f \<equiv> ?f piecewise_C1_differentiable_on {0..1}

goal (1 subgoal):
 1. \<forall>(k1, \<gamma>1)\<in>one_chain1. valid_path (snd (f (k1, \<gamma>1)))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>(k1, \<gamma>1)\<in>one_chain1. valid_path (snd (f (k1, \<gamma>1)))

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
 2. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
have integ_rev_exist_b: "\<forall>(k1,\<gamma>1)\<in>one_chain1. \<forall>b\<in>basis. line_integral_exists F {b} (reversepath (snd (f (k1, \<gamma>1))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k1, \<gamma>1)\<in>one_chain1. \<forall>b\<in>basis. line_integral_exists F {b} (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
using line_integral_on_reverse_path(2) integ_exist_b valid_cubes
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>valid_path ?\<gamma>; line_integral_exists ?F ?basis ?\<gamma>\<rbrakk> \<Longrightarrow> line_integral_exists ?F ?basis (reversepath ?\<gamma>)
\<forall>(k1, \<gamma>1)\<in>one_chain1. \<forall>b\<in>basis. line_integral_exists F {b} (snd (f (k1, \<gamma>1)))
\<forall>(k1, \<gamma>1)\<in>one_chain1. valid_path (snd (f (k1, \<gamma>1)))

goal (1 subgoal):
 1. \<forall>(k1, \<gamma>1)\<in>one_chain1. \<forall>b\<in>basis. line_integral_exists F {b} (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>(k1, \<gamma>1)\<in>one_chain1. \<forall>b\<in>basis. line_integral_exists F {b} (reversepath (snd (f (k1, \<gamma>1))))

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
 2. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
have 0:" \<forall>x\<in>one_chain1. (case x of (k, \<gamma>) \<Rightarrow> (real_of_int k * line_integral F basis \<gamma>) = (case f x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma>) \<and>
                                                        line_integral_exists F basis \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>one_chain1. case x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma> = (case f x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma>) \<and> line_integral_exists F basis \<gamma>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> one_chain1 \<Longrightarrow> case x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma> = (case f x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma>) \<and> line_integral_exists F basis \<gamma>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> one_chain1 \<Longrightarrow> case x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma> = (case f x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma>) \<and> line_integral_exists F basis \<gamma>
[PROOF STEP]
fix k1 \<gamma>1
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> one_chain1 \<Longrightarrow> case x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma> = (case f x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma>) \<and> line_integral_exists F basis \<gamma>
[PROOF STEP]
assume ass1: "(k1,\<gamma>1) \<in>one_chain1"
[PROOF STATE]
proof (state)
this:
(k1, \<gamma>1) \<in> one_chain1

goal (1 subgoal):
 1. \<And>x. x \<in> one_chain1 \<Longrightarrow> case x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma> = (case f x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma>) \<and> line_integral_exists F basis \<gamma>
[PROOF STEP]
have "real_of_int k1 * line_integral F basis \<gamma>1 = (case (f (k1,\<gamma>1)) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and>
                      line_integral_exists F basis \<gamma>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
 2. \<not> ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
assume ass2: "k1 = 1"
[PROOF STATE]
proof (state)
this:
k1 = 1

goal (2 subgoals):
 1. ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
 2. \<not> ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
let ?k2 = "fst (f (k1, \<gamma>1))"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
 2. \<not> ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
let ?\<gamma>2 = "snd (f (k1, \<gamma>1))"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
 2. \<not> ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
have "real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int ?k2 * line_integral F basis ?\<gamma>2\<and>
                              line_integral_exists F basis \<gamma>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
 2. \<not> ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
assume ass3: "?k2 = 1"
[PROOF STATE]
proof (state)
this:
fst (f (k1, \<gamma>1)) = 1

goal (2 subgoals):
 1. ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
 2. \<not> ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst (f (k1, \<gamma>1)) = 1
[PROOF STEP]
have 0: "reparam \<gamma>1 ?\<gamma>2"
[PROOF STATE]
proof (prove)
using this:
fst (f (k1, \<gamma>1)) = 1

goal (1 subgoal):
 1. reparam \<gamma>1 (snd (f (k1, \<gamma>1)))
[PROOF STEP]
using ass1 ass2 f(2)
[PROOF STATE]
proof (prove)
using this:
fst (f (k1, \<gamma>1)) = 1
(k1, \<gamma>1) \<in> one_chain1
k1 = 1
\<forall>(k, \<gamma>)\<in>one_chain1. if k = fst (f (k, \<gamma>)) then reparam \<gamma> (snd (f (k, \<gamma>))) else reparam \<gamma> (reversepath (snd (f (k, \<gamma>))))

goal (1 subgoal):
 1. reparam \<gamma>1 (snd (f (k1, \<gamma>1)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
reparam \<gamma>1 (snd (f (k1, \<gamma>1)))

goal (2 subgoals):
 1. ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
 2. \<not> ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
have 1: "?\<gamma>2 piecewise_C1_differentiable_on {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (f (k1, \<gamma>1)) piecewise_C1_differentiable_on {0..1}
[PROOF STEP]
using f(3) assms(2) ass1
[PROOF STATE]
proof (prove)
using this:
f ` one_chain1 = one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<gamma>2 piecewise_C1_differentiable_on {0..1}
(k1, \<gamma>1) \<in> one_chain1

goal (1 subgoal):
 1. snd (f (k1, \<gamma>1)) piecewise_C1_differentiable_on {0..1}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
snd (f (k1, \<gamma>1)) piecewise_C1_differentiable_on {0..1}

goal (2 subgoals):
 1. ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
 2. \<not> ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
have 2: "\<forall>b\<in>basis. continuous_on (path_image ?\<gamma>2) (\<lambda>x. F x \<bullet> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b\<in>basis. continuous_on (path_image (snd (f (k1, \<gamma>1)))) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
using f(3) assms(3) ass1
[PROOF STATE]
proof (prove)
using this:
f ` one_chain1 = one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
(k1, \<gamma>1) \<in> one_chain1

goal (1 subgoal):
 1. \<forall>b\<in>basis. continuous_on (path_image (snd (f (k1, \<gamma>1)))) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<forall>b\<in>basis. continuous_on (path_image (snd (f (k1, \<gamma>1)))) (\<lambda>x. F x \<bullet> b)

goal (2 subgoals):
 1. ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
 2. \<not> ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
show "real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int ?k2 * line_integral F basis ?\<gamma>2 \<and>
                                     line_integral_exists F basis \<gamma>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
using assms reparam_eq_line_integrals_basis[OF 0 1 2 assms(4)] integ_exist_b
              ass1 ass2 ass3
[PROOF STATE]
proof (prove)
using this:
chain_reparam_chain one_chain1 one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<gamma>2 piecewise_C1_differentiable_on {0..1}
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
finite basis
boundary_chain one_chain1
boundary_chain one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. line_integral_exists F {b} \<gamma>2
\<forall>b\<in>basis. line_integral_exists F {b} (snd (f (k1, \<gamma>1))) \<Longrightarrow> line_integral F basis \<gamma>1 = line_integral F basis (snd (f (k1, \<gamma>1)))
\<forall>b\<in>basis. line_integral_exists F {b} (snd (f (k1, \<gamma>1))) \<Longrightarrow> line_integral_exists F basis \<gamma>1
\<forall>(k1, \<gamma>1)\<in>one_chain1. \<forall>b\<in>basis. line_integral_exists F {b} (snd (f (k1, \<gamma>1)))
(k1, \<gamma>1) \<in> one_chain1
k1 = 1
fst (f (k1, \<gamma>1)) = 1

goal (1 subgoal):
 1. real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
assume "?k2 \<noteq> 1"
[PROOF STATE]
proof (state)
this:
fst (f (k1, \<gamma>1)) \<noteq> 1

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst (f (k1, \<gamma>1)) \<noteq> 1
[PROOF STEP]
have ass3: "?k2 = -1"
[PROOF STATE]
proof (prove)
using this:
fst (f (k1, \<gamma>1)) \<noteq> 1

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) = - 1
[PROOF STEP]
using bound2 ass1 f(3)
[PROOF STATE]
proof (prove)
using this:
fst (f (k1, \<gamma>1)) \<noteq> 1
boundary_chain one_chain2
(k1, \<gamma>1) \<in> one_chain1
f ` one_chain1 = one_chain2

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) = - 1
[PROOF STEP]
unfolding boundary_chain_def
[PROOF STATE]
proof (prove)
using this:
fst (f (k1, \<gamma>1)) \<noteq> 1
\<forall>(k, \<gamma>)\<in>one_chain2. k = 1 \<or> k = - 1
(k1, \<gamma>1) \<in> one_chain1
f ` one_chain1 = one_chain2

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) = - 1
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
fst (f (k1, \<gamma>1)) = - 1

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst (f (k1, \<gamma>1)) = - 1
[PROOF STEP]
have 0: "reparam \<gamma>1 (reversepath ?\<gamma>2)"
[PROOF STATE]
proof (prove)
using this:
fst (f (k1, \<gamma>1)) = - 1

goal (1 subgoal):
 1. reparam \<gamma>1 (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
using ass1 ass2 f(2)
[PROOF STATE]
proof (prove)
using this:
fst (f (k1, \<gamma>1)) = - 1
(k1, \<gamma>1) \<in> one_chain1
k1 = 1
\<forall>(k, \<gamma>)\<in>one_chain1. if k = fst (f (k, \<gamma>)) then reparam \<gamma> (snd (f (k, \<gamma>))) else reparam \<gamma> (reversepath (snd (f (k, \<gamma>))))

goal (1 subgoal):
 1. reparam \<gamma>1 (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
reparam \<gamma>1 (reversepath (snd (f (k1, \<gamma>1))))

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
have 1: "(reversepath ?\<gamma>2) piecewise_C1_differentiable_on {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reversepath (snd (f (k1, \<gamma>1))) piecewise_C1_differentiable_on {0..1}
[PROOF STEP]
using f(3) assms(2) ass1 piecewise_smooth_path_imp_reverse
[PROOF STATE]
proof (prove)
using this:
f ` one_chain1 = one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<gamma>2 piecewise_C1_differentiable_on {0..1}
(k1, \<gamma>1) \<in> one_chain1
?g piecewise_C1_differentiable_on {0..1} \<Longrightarrow> reversepath ?g piecewise_C1_differentiable_on {0..1}

goal (1 subgoal):
 1. reversepath (snd (f (k1, \<gamma>1))) piecewise_C1_differentiable_on {0..1}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
reversepath (snd (f (k1, \<gamma>1))) piecewise_C1_differentiable_on {0..1}

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
have 2: "\<forall>b\<in>basis. continuous_on (path_image (reversepath ?\<gamma>2)) (\<lambda>x. F x \<bullet> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b\<in>basis. continuous_on (path_image (reversepath (snd (f (k1, \<gamma>1))))) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
using f(3) assms(3) ass1 path_image_reversepath
[PROOF STATE]
proof (prove)
using this:
f ` one_chain1 = one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
(k1, \<gamma>1) \<in> one_chain1
path_image (reversepath ?g) = path_image ?g

goal (1 subgoal):
 1. \<forall>b\<in>basis. continuous_on (path_image (reversepath (snd (f (k1, \<gamma>1))))) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<forall>b\<in>basis. continuous_on (path_image (reversepath (snd (f (k1, \<gamma>1))))) (\<lambda>x. F x \<bullet> b)

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
have 3: "line_integral F basis ?\<gamma>2 = - line_integral F basis (reversepath ?\<gamma>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis (snd (f (k1, \<gamma>1))) = - line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. line_integral F basis (snd (f (k1, \<gamma>1))) = - line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
have i:"valid_path (reversepath ?\<gamma>2) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
using 1 C1_differentiable_imp_piecewise
[PROOF STATE]
proof (prove)
using this:
reversepath (snd (f (k1, \<gamma>1))) piecewise_C1_differentiable_on {0..1}
?f C1_differentiable_on ?S \<Longrightarrow> ?f piecewise_C1_differentiable_on ?S

goal (1 subgoal):
 1. valid_path (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
by (auto simp add: valid_path_def)
[PROOF STATE]
proof (state)
this:
valid_path (reversepath (snd (f (k1, \<gamma>1))))

goal (1 subgoal):
 1. line_integral F basis (snd (f (k1, \<gamma>1))) = - line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
have ii: "line_integral_exists F basis (snd (f (k1, \<gamma>1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis (snd (f (k1, \<gamma>1)))
[PROOF STEP]
using assms(4) line_integral_sum_basis(2) integ_exist_b ass1
[PROOF STATE]
proof (prove)
using this:
finite basis
\<lbrakk>finite ?basis; \<forall>b\<in>?basis. line_integral_exists ?F {b} ?\<gamma>\<rbrakk> \<Longrightarrow> line_integral_exists ?F ?basis ?\<gamma>
\<forall>(k1, \<gamma>1)\<in>one_chain1. \<forall>b\<in>basis. line_integral_exists F {b} (snd (f (k1, \<gamma>1)))
(k1, \<gamma>1) \<in> one_chain1

goal (1 subgoal):
 1. line_integral_exists F basis (snd (f (k1, \<gamma>1)))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
line_integral_exists F basis (snd (f (k1, \<gamma>1)))

goal (1 subgoal):
 1. line_integral F basis (snd (f (k1, \<gamma>1))) = - line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis (snd (f (k1, \<gamma>1))) = - line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
using i ii line_integral_on_reverse_path(1) valid_path_reversepath
[PROOF STATE]
proof (prove)
using this:
valid_path (reversepath (snd (f (k1, \<gamma>1))))
line_integral_exists F basis (snd (f (k1, \<gamma>1)))
\<lbrakk>valid_path ?\<gamma>; line_integral_exists ?F ?basis ?\<gamma>\<rbrakk> \<Longrightarrow> line_integral ?F ?basis ?\<gamma> = - line_integral ?F ?basis (reversepath ?\<gamma>)
valid_path (reversepath ?g) = valid_path ?g

goal (1 subgoal):
 1. line_integral F basis (snd (f (k1, \<gamma>1))) = - line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
line_integral F basis (snd (f (k1, \<gamma>1))) = - line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
line_integral F basis (snd (f (k1, \<gamma>1))) = - line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
show "real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int ?k2 * line_integral F basis ?\<gamma>2 \<and>
                                     line_integral_exists F basis \<gamma>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
using assms reparam_eq_line_integrals_basis[OF 0 1 2 assms(4)] integ_rev_exist_b
              ass1 ass2 ass3 3
[PROOF STATE]
proof (prove)
using this:
chain_reparam_chain one_chain1 one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<gamma>2 piecewise_C1_differentiable_on {0..1}
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
finite basis
boundary_chain one_chain1
boundary_chain one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. line_integral_exists F {b} \<gamma>2
\<forall>b\<in>basis. line_integral_exists F {b} (reversepath (snd (f (k1, \<gamma>1)))) \<Longrightarrow> line_integral F basis \<gamma>1 = line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))
\<forall>b\<in>basis. line_integral_exists F {b} (reversepath (snd (f (k1, \<gamma>1)))) \<Longrightarrow> line_integral_exists F basis \<gamma>1
\<forall>(k1, \<gamma>1)\<in>one_chain1. \<forall>b\<in>basis. line_integral_exists F {b} (reversepath (snd (f (k1, \<gamma>1))))
(k1, \<gamma>1) \<in> one_chain1
k1 = 1
fst (f (k1, \<gamma>1)) = - 1
line_integral F basis (snd (f (k1, \<gamma>1))) = - line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))

goal (1 subgoal):
 1. real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1

goal (2 subgoals):
 1. ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
 2. \<not> ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
show "real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and>
                                   line_integral_exists F basis \<gamma>1"
[PROOF STATE]
proof (prove)
using this:
real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1

goal (1 subgoal):
 1. real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
by (simp add: case_prod_beta')
[PROOF STATE]
proof (state)
this:
real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1

goal (1 subgoal):
 1. k1 \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k1 \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
assume "k1 \<noteq> 1"
[PROOF STATE]
proof (state)
this:
k1 \<noteq> 1

goal (1 subgoal):
 1. k1 \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k1 \<noteq> 1
[PROOF STEP]
have ass2: "k1 = -1"
[PROOF STATE]
proof (prove)
using this:
k1 \<noteq> 1

goal (1 subgoal):
 1. k1 = - 1
[PROOF STEP]
using bound1 ass1 f(3)
[PROOF STATE]
proof (prove)
using this:
k1 \<noteq> 1
boundary_chain one_chain1
(k1, \<gamma>1) \<in> one_chain1
f ` one_chain1 = one_chain2

goal (1 subgoal):
 1. k1 = - 1
[PROOF STEP]
unfolding boundary_chain_def
[PROOF STATE]
proof (prove)
using this:
k1 \<noteq> 1
\<forall>(k, \<gamma>)\<in>one_chain1. k = 1 \<or> k = - 1
(k1, \<gamma>1) \<in> one_chain1
f ` one_chain1 = one_chain2

goal (1 subgoal):
 1. k1 = - 1
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
k1 = - 1

goal (1 subgoal):
 1. k1 \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
let ?k2 = "fst (f (k1, \<gamma>1))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k1 \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
let ?\<gamma>2 = "snd (f (k1, \<gamma>1))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k1 \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
have "real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int ?k2 * line_integral F basis ?\<gamma>2 \<and>
                              line_integral_exists F basis \<gamma>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
 2. \<not> ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
assume ass3: "?k2 = 1"
[PROOF STATE]
proof (state)
this:
fst (f (k1, \<gamma>1)) = 1

goal (2 subgoals):
 1. ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
 2. \<not> ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst (f (k1, \<gamma>1)) = 1
[PROOF STEP]
have 0: "reparam \<gamma>1 (reversepath ?\<gamma>2)"
[PROOF STATE]
proof (prove)
using this:
fst (f (k1, \<gamma>1)) = 1

goal (1 subgoal):
 1. reparam \<gamma>1 (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
using ass1 ass2 f(2)
[PROOF STATE]
proof (prove)
using this:
fst (f (k1, \<gamma>1)) = 1
(k1, \<gamma>1) \<in> one_chain1
k1 = - 1
\<forall>(k, \<gamma>)\<in>one_chain1. if k = fst (f (k, \<gamma>)) then reparam \<gamma> (snd (f (k, \<gamma>))) else reparam \<gamma> (reversepath (snd (f (k, \<gamma>))))

goal (1 subgoal):
 1. reparam \<gamma>1 (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
reparam \<gamma>1 (reversepath (snd (f (k1, \<gamma>1))))

goal (2 subgoals):
 1. ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
 2. \<not> ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
have 1: "(reversepath ?\<gamma>2) piecewise_C1_differentiable_on {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reversepath (snd (f (k1, \<gamma>1))) piecewise_C1_differentiable_on {0..1}
[PROOF STEP]
using f(3) assms(2) ass1 piecewise_smooth_path_imp_reverse
[PROOF STATE]
proof (prove)
using this:
f ` one_chain1 = one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<gamma>2 piecewise_C1_differentiable_on {0..1}
(k1, \<gamma>1) \<in> one_chain1
?g piecewise_C1_differentiable_on {0..1} \<Longrightarrow> reversepath ?g piecewise_C1_differentiable_on {0..1}

goal (1 subgoal):
 1. reversepath (snd (f (k1, \<gamma>1))) piecewise_C1_differentiable_on {0..1}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
reversepath (snd (f (k1, \<gamma>1))) piecewise_C1_differentiable_on {0..1}

goal (2 subgoals):
 1. ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
 2. \<not> ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
have 2: "\<forall>b\<in>basis. continuous_on (path_image (reversepath ?\<gamma>2)) (\<lambda>x. F x \<bullet> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b\<in>basis. continuous_on (path_image (reversepath (snd (f (k1, \<gamma>1))))) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
using f(3) assms(3) ass1 path_image_reversepath
[PROOF STATE]
proof (prove)
using this:
f ` one_chain1 = one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
(k1, \<gamma>1) \<in> one_chain1
path_image (reversepath ?g) = path_image ?g

goal (1 subgoal):
 1. \<forall>b\<in>basis. continuous_on (path_image (reversepath (snd (f (k1, \<gamma>1))))) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<forall>b\<in>basis. continuous_on (path_image (reversepath (snd (f (k1, \<gamma>1))))) (\<lambda>x. F x \<bullet> b)

goal (2 subgoals):
 1. ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
 2. \<not> ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
have 3: "line_integral F basis ?\<gamma>2 = - line_integral F basis (reversepath ?\<gamma>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis (snd (f (k1, \<gamma>1))) = - line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. line_integral F basis (snd (f (k1, \<gamma>1))) = - line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
have i:"valid_path (reversepath ?\<gamma>2) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
using 1 C1_differentiable_imp_piecewise
[PROOF STATE]
proof (prove)
using this:
reversepath (snd (f (k1, \<gamma>1))) piecewise_C1_differentiable_on {0..1}
?f C1_differentiable_on ?S \<Longrightarrow> ?f piecewise_C1_differentiable_on ?S

goal (1 subgoal):
 1. valid_path (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
by (auto simp add: valid_path_def)
[PROOF STATE]
proof (state)
this:
valid_path (reversepath (snd (f (k1, \<gamma>1))))

goal (1 subgoal):
 1. line_integral F basis (snd (f (k1, \<gamma>1))) = - line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis (snd (f (k1, \<gamma>1))) = - line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
using line_integral_on_reverse_path(1)[OF i] integ_rev_exist_b
[PROOF STATE]
proof (prove)
using this:
line_integral_exists ?F ?basis (reversepath (snd (f (k1, \<gamma>1)))) \<Longrightarrow> line_integral ?F ?basis (reversepath (snd (f (k1, \<gamma>1)))) = - line_integral ?F ?basis (reversepath (reversepath (snd (f (k1, \<gamma>1)))))
\<forall>(k1, \<gamma>1)\<in>one_chain1. \<forall>b\<in>basis. line_integral_exists F {b} (reversepath (snd (f (k1, \<gamma>1))))

goal (1 subgoal):
 1. line_integral F basis (snd (f (k1, \<gamma>1))) = - line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
using ass1 assms(4) line_integral_sum_basis(2)
[PROOF STATE]
proof (prove)
using this:
line_integral_exists ?F ?basis (reversepath (snd (f (k1, \<gamma>1)))) \<Longrightarrow> line_integral ?F ?basis (reversepath (snd (f (k1, \<gamma>1)))) = - line_integral ?F ?basis (reversepath (reversepath (snd (f (k1, \<gamma>1)))))
\<forall>(k1, \<gamma>1)\<in>one_chain1. \<forall>b\<in>basis. line_integral_exists F {b} (reversepath (snd (f (k1, \<gamma>1))))
(k1, \<gamma>1) \<in> one_chain1
finite basis
\<lbrakk>finite ?basis; \<forall>b\<in>?basis. line_integral_exists ?F {b} ?\<gamma>\<rbrakk> \<Longrightarrow> line_integral_exists ?F ?basis ?\<gamma>

goal (1 subgoal):
 1. line_integral F basis (snd (f (k1, \<gamma>1))) = - line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
line_integral F basis (snd (f (k1, \<gamma>1))) = - line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
line_integral F basis (snd (f (k1, \<gamma>1))) = - line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))

goal (2 subgoals):
 1. ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
 2. \<not> ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
show "real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int ?k2 * line_integral F basis ?\<gamma>2 \<and>
                                     line_integral_exists F basis \<gamma>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
using assms reparam_eq_line_integrals_basis[OF 0 1 2 assms(4)]
              ass2 ass3 3
[PROOF STATE]
proof (prove)
using this:
chain_reparam_chain one_chain1 one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<gamma>2 piecewise_C1_differentiable_on {0..1}
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
finite basis
boundary_chain one_chain1
boundary_chain one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. line_integral_exists F {b} \<gamma>2
\<forall>b\<in>basis. line_integral_exists F {b} (reversepath (snd (f (k1, \<gamma>1)))) \<Longrightarrow> line_integral F basis \<gamma>1 = line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))
\<forall>b\<in>basis. line_integral_exists F {b} (reversepath (snd (f (k1, \<gamma>1)))) \<Longrightarrow> line_integral_exists F basis \<gamma>1
k1 = - 1
fst (f (k1, \<gamma>1)) = 1
line_integral F basis (snd (f (k1, \<gamma>1))) = - line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))

goal (1 subgoal):
 1. real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
using ass1 integ_rev_exist_b
[PROOF STATE]
proof (prove)
using this:
chain_reparam_chain one_chain1 one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<gamma>2 piecewise_C1_differentiable_on {0..1}
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
finite basis
boundary_chain one_chain1
boundary_chain one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. line_integral_exists F {b} \<gamma>2
\<forall>b\<in>basis. line_integral_exists F {b} (reversepath (snd (f (k1, \<gamma>1)))) \<Longrightarrow> line_integral F basis \<gamma>1 = line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))
\<forall>b\<in>basis. line_integral_exists F {b} (reversepath (snd (f (k1, \<gamma>1)))) \<Longrightarrow> line_integral_exists F basis \<gamma>1
k1 = - 1
fst (f (k1, \<gamma>1)) = 1
line_integral F basis (snd (f (k1, \<gamma>1))) = - line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))
(k1, \<gamma>1) \<in> one_chain1
\<forall>(k1, \<gamma>1)\<in>one_chain1. \<forall>b\<in>basis. line_integral_exists F {b} (reversepath (snd (f (k1, \<gamma>1))))

goal (1 subgoal):
 1. real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
assume "?k2 \<noteq> 1"
[PROOF STATE]
proof (state)
this:
fst (f (k1, \<gamma>1)) \<noteq> 1

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst (f (k1, \<gamma>1)) \<noteq> 1
[PROOF STEP]
have ass3: "?k2 = -1"
[PROOF STATE]
proof (prove)
using this:
fst (f (k1, \<gamma>1)) \<noteq> 1

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) = - 1
[PROOF STEP]
using bound2 ass1 f(3)
[PROOF STATE]
proof (prove)
using this:
fst (f (k1, \<gamma>1)) \<noteq> 1
boundary_chain one_chain2
(k1, \<gamma>1) \<in> one_chain1
f ` one_chain1 = one_chain2

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) = - 1
[PROOF STEP]
unfolding boundary_chain_def
[PROOF STATE]
proof (prove)
using this:
fst (f (k1, \<gamma>1)) \<noteq> 1
\<forall>(k, \<gamma>)\<in>one_chain2. k = 1 \<or> k = - 1
(k1, \<gamma>1) \<in> one_chain1
f ` one_chain1 = one_chain2

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) = - 1
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
fst (f (k1, \<gamma>1)) = - 1

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst (f (k1, \<gamma>1)) = - 1
[PROOF STEP]
have 0: "reparam \<gamma>1 ?\<gamma>2"
[PROOF STATE]
proof (prove)
using this:
fst (f (k1, \<gamma>1)) = - 1

goal (1 subgoal):
 1. reparam \<gamma>1 (snd (f (k1, \<gamma>1)))
[PROOF STEP]
using ass1 ass2 f(2)
[PROOF STATE]
proof (prove)
using this:
fst (f (k1, \<gamma>1)) = - 1
(k1, \<gamma>1) \<in> one_chain1
k1 = - 1
\<forall>(k, \<gamma>)\<in>one_chain1. if k = fst (f (k, \<gamma>)) then reparam \<gamma> (snd (f (k, \<gamma>))) else reparam \<gamma> (reversepath (snd (f (k, \<gamma>))))

goal (1 subgoal):
 1. reparam \<gamma>1 (snd (f (k1, \<gamma>1)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
reparam \<gamma>1 (snd (f (k1, \<gamma>1)))

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
have 1: "?\<gamma>2 piecewise_C1_differentiable_on {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (f (k1, \<gamma>1)) piecewise_C1_differentiable_on {0..1}
[PROOF STEP]
using f(3) assms(2) ass1
[PROOF STATE]
proof (prove)
using this:
f ` one_chain1 = one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<gamma>2 piecewise_C1_differentiable_on {0..1}
(k1, \<gamma>1) \<in> one_chain1

goal (1 subgoal):
 1. snd (f (k1, \<gamma>1)) piecewise_C1_differentiable_on {0..1}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
snd (f (k1, \<gamma>1)) piecewise_C1_differentiable_on {0..1}

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
have 2: "\<forall>b\<in>basis. continuous_on (path_image ?\<gamma>2) (\<lambda>x. F x \<bullet> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b\<in>basis. continuous_on (path_image (snd (f (k1, \<gamma>1)))) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
using f(3) assms(3) ass1
[PROOF STATE]
proof (prove)
using this:
f ` one_chain1 = one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
(k1, \<gamma>1) \<in> one_chain1

goal (1 subgoal):
 1. \<forall>b\<in>basis. continuous_on (path_image (snd (f (k1, \<gamma>1)))) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<forall>b\<in>basis. continuous_on (path_image (snd (f (k1, \<gamma>1)))) (\<lambda>x. F x \<bullet> b)

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
show "real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int ?k2 * line_integral F basis ?\<gamma>2 \<and>
                                     line_integral_exists F basis \<gamma>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
using assms reparam_eq_line_integrals_basis[OF 0 1 2 assms(4)]
              ass2 ass3
[PROOF STATE]
proof (prove)
using this:
chain_reparam_chain one_chain1 one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<gamma>2 piecewise_C1_differentiable_on {0..1}
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
finite basis
boundary_chain one_chain1
boundary_chain one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. line_integral_exists F {b} \<gamma>2
\<forall>b\<in>basis. line_integral_exists F {b} (snd (f (k1, \<gamma>1))) \<Longrightarrow> line_integral F basis \<gamma>1 = line_integral F basis (snd (f (k1, \<gamma>1)))
\<forall>b\<in>basis. line_integral_exists F {b} (snd (f (k1, \<gamma>1))) \<Longrightarrow> line_integral_exists F basis \<gamma>1
k1 = - 1
fst (f (k1, \<gamma>1)) = - 1

goal (1 subgoal):
 1. real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
using ass1 integ_exist_b
[PROOF STATE]
proof (prove)
using this:
chain_reparam_chain one_chain1 one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<gamma>2 piecewise_C1_differentiable_on {0..1}
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
finite basis
boundary_chain one_chain1
boundary_chain one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. line_integral_exists F {b} \<gamma>2
\<forall>b\<in>basis. line_integral_exists F {b} (snd (f (k1, \<gamma>1))) \<Longrightarrow> line_integral F basis \<gamma>1 = line_integral F basis (snd (f (k1, \<gamma>1)))
\<forall>b\<in>basis. line_integral_exists F {b} (snd (f (k1, \<gamma>1))) \<Longrightarrow> line_integral_exists F basis \<gamma>1
k1 = - 1
fst (f (k1, \<gamma>1)) = - 1
(k1, \<gamma>1) \<in> one_chain1
\<forall>(k1, \<gamma>1)\<in>one_chain1. \<forall>b\<in>basis. line_integral_exists F {b} (snd (f (k1, \<gamma>1)))

goal (1 subgoal):
 1. real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1

goal (1 subgoal):
 1. k1 \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
show "real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and>
                                   line_integral_exists F basis \<gamma>1"
[PROOF STATE]
proof (prove)
using this:
real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1

goal (1 subgoal):
 1. real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
by (simp add: case_prod_beta')
[PROOF STATE]
proof (state)
this:
real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1

goal (1 subgoal):
 1. \<And>x. x \<in> one_chain1 \<Longrightarrow> case x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma> = (case f x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma>) \<and> line_integral_exists F basis \<gamma>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?k1.2, ?\<gamma>1.2) \<in> one_chain1 \<Longrightarrow> real_of_int ?k1.2 * line_integral F basis ?\<gamma>1.2 = (case f (?k1.2, ?\<gamma>1.2) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis ?\<gamma>1.2

goal (1 subgoal):
 1. \<And>x. x \<in> one_chain1 \<Longrightarrow> case x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma> = (case f x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma>) \<and> line_integral_exists F basis \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(?k1.2, ?\<gamma>1.2) \<in> one_chain1 \<Longrightarrow> real_of_int ?k1.2 * line_integral F basis ?\<gamma>1.2 = (case f (?k1.2, ?\<gamma>1.2) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis ?\<gamma>1.2
[PROOF STEP]
show "\<And>x. x \<in> one_chain1 \<Longrightarrow>
                                (case x of (k, \<gamma>) \<Rightarrow> (real_of_int k * line_integral F basis \<gamma>) = (case f x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma>) \<and>
                                                        line_integral_exists F basis \<gamma>)"
[PROOF STATE]
proof (prove)
using this:
(?k1.2, ?\<gamma>1.2) \<in> one_chain1 \<Longrightarrow> real_of_int ?k1.2 * line_integral F basis ?\<gamma>1.2 = (case f (?k1.2, ?\<gamma>1.2) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis ?\<gamma>1.2

goal (1 subgoal):
 1. \<And>x. x \<in> one_chain1 \<Longrightarrow> case x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma> = (case f x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma>) \<and> line_integral_exists F basis \<gamma>
[PROOF STEP]
by (auto simp add: case_prod_beta')
[PROOF STATE]
proof (state)
this:
?x \<in> one_chain1 \<Longrightarrow> case ?x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma> = (case f ?x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma>) \<and> line_integral_exists F basis \<gamma>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>one_chain1. case x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma> = (case f x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma>) \<and> line_integral_exists F basis \<gamma>

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
 2. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
show "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>one_chain1. case x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma> = (case f x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma>) \<and> line_integral_exists F basis \<gamma>

goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
[PROOF STEP]
by (simp add: one_chain_line_integral_def sum_bij[OF f(1) _ f(3)] prod.case_eq_if)
[PROOF STATE]
proof (state)
this:
one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2

goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
show "\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>one_chain1. case x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma> = (case f x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma>) \<and> line_integral_exists F basis \<gamma>

goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma path_image_rec_join:
  fixes \<gamma>::"real \<Rightarrow> (real \<times> real)"
  fixes k::int
  fixes l
  shows "\<And>k \<gamma>. (k, \<gamma>) \<in> set l \<Longrightarrow> valid_chain_list l \<Longrightarrow> path_image \<gamma> \<subseteq> path_image (rec_join l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k \<gamma>. \<lbrakk>(k, \<gamma>) \<in> set l; valid_chain_list l\<rbrakk> \<Longrightarrow> path_image \<gamma> \<subseteq> path_image (rec_join l)
[PROOF STEP]
proof(induction l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>k \<gamma>. \<lbrakk>(k, \<gamma>) \<in> set []; valid_chain_list []\<rbrakk> \<Longrightarrow> path_image \<gamma> \<subseteq> path_image (rec_join [])
 2. \<And>a l k \<gamma>. \<lbrakk>\<And>k \<gamma>. \<lbrakk>(k, \<gamma>) \<in> set l; valid_chain_list l\<rbrakk> \<Longrightarrow> path_image \<gamma> \<subseteq> path_image (rec_join l); (k, \<gamma>) \<in> set (a # l); valid_chain_list (a # l)\<rbrakk> \<Longrightarrow> path_image \<gamma> \<subseteq> path_image (rec_join (a # l))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
(k, \<gamma>) \<in> set []
valid_chain_list []

goal (2 subgoals):
 1. \<And>k \<gamma>. \<lbrakk>(k, \<gamma>) \<in> set []; valid_chain_list []\<rbrakk> \<Longrightarrow> path_image \<gamma> \<subseteq> path_image (rec_join [])
 2. \<And>a l k \<gamma>. \<lbrakk>\<And>k \<gamma>. \<lbrakk>(k, \<gamma>) \<in> set l; valid_chain_list l\<rbrakk> \<Longrightarrow> path_image \<gamma> \<subseteq> path_image (rec_join l); (k, \<gamma>) \<in> set (a # l); valid_chain_list (a # l)\<rbrakk> \<Longrightarrow> path_image \<gamma> \<subseteq> path_image (rec_join (a # l))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(k, \<gamma>) \<in> set []
valid_chain_list []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(k, \<gamma>) \<in> set []
valid_chain_list []

goal (1 subgoal):
 1. path_image \<gamma> \<subseteq> path_image (rec_join [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path_image \<gamma> \<subseteq> path_image (rec_join [])

goal (1 subgoal):
 1. \<And>a l k \<gamma>. \<lbrakk>\<And>k \<gamma>. \<lbrakk>(k, \<gamma>) \<in> set l; valid_chain_list l\<rbrakk> \<Longrightarrow> path_image \<gamma> \<subseteq> path_image (rec_join l); (k, \<gamma>) \<in> set (a # l); valid_chain_list (a # l)\<rbrakk> \<Longrightarrow> path_image \<gamma> \<subseteq> path_image (rec_join (a # l))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l k \<gamma>. \<lbrakk>\<And>k \<gamma>. \<lbrakk>(k, \<gamma>) \<in> set l; valid_chain_list l\<rbrakk> \<Longrightarrow> path_image \<gamma> \<subseteq> path_image (rec_join l); (k, \<gamma>) \<in> set (a # l); valid_chain_list (a # l)\<rbrakk> \<Longrightarrow> path_image \<gamma> \<subseteq> path_image (rec_join (a # l))
[PROOF STEP]
case ass: (Cons a l)
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?k, ?\<gamma>) \<in> set l; valid_chain_list l\<rbrakk> \<Longrightarrow> path_image ?\<gamma> \<subseteq> path_image (rec_join l)
(k, \<gamma>) \<in> set (a # l)
valid_chain_list (a # l)

goal (1 subgoal):
 1. \<And>a l k \<gamma>. \<lbrakk>\<And>k \<gamma>. \<lbrakk>(k, \<gamma>) \<in> set l; valid_chain_list l\<rbrakk> \<Longrightarrow> path_image \<gamma> \<subseteq> path_image (rec_join l); (k, \<gamma>) \<in> set (a # l); valid_chain_list (a # l)\<rbrakk> \<Longrightarrow> path_image \<gamma> \<subseteq> path_image (rec_join (a # l))
[PROOF STEP]
obtain k' \<gamma>' where a: "a = (k',\<gamma>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k' \<gamma>'. a = (k', \<gamma>') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
a = (k', \<gamma>')

goal (1 subgoal):
 1. \<And>a l k \<gamma>. \<lbrakk>\<And>k \<gamma>. \<lbrakk>(k, \<gamma>) \<in> set l; valid_chain_list l\<rbrakk> \<Longrightarrow> path_image \<gamma> \<subseteq> path_image (rec_join l); (k, \<gamma>) \<in> set (a # l); valid_chain_list (a # l)\<rbrakk> \<Longrightarrow> path_image \<gamma> \<subseteq> path_image (rec_join (a # l))
[PROOF STEP]
have "path_image \<gamma> \<subseteq> path_image (rec_join ((k',\<gamma>') # l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path_image \<gamma> \<subseteq> path_image (rec_join ((k', \<gamma>') # l))
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> path_image \<gamma> \<subseteq> path_image (rec_join ((k', \<gamma>') # l))
 2. \<not> ?P \<Longrightarrow> path_image \<gamma> \<subseteq> path_image (rec_join ((k', \<gamma>') # l))
[PROOF STEP]
assume "l=[]"
[PROOF STATE]
proof (state)
this:
l = []

goal (2 subgoals):
 1. ?P \<Longrightarrow> path_image \<gamma> \<subseteq> path_image (rec_join ((k', \<gamma>') # l))
 2. \<not> ?P \<Longrightarrow> path_image \<gamma> \<subseteq> path_image (rec_join ((k', \<gamma>') # l))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l = []
[PROOF STEP]
show "path_image \<gamma> \<subseteq> path_image (rec_join ((k',\<gamma>') # l))"
[PROOF STATE]
proof (prove)
using this:
l = []

goal (1 subgoal):
 1. path_image \<gamma> \<subseteq> path_image (rec_join ((k', \<gamma>') # l))
[PROOF STEP]
using ass(2-3) a
[PROOF STATE]
proof (prove)
using this:
l = []
(k, \<gamma>) \<in> set (a # l)
valid_chain_list (a # l)
a = (k', \<gamma>')

goal (1 subgoal):
 1. path_image \<gamma> \<subseteq> path_image (rec_join ((k', \<gamma>') # l))
[PROOF STEP]
by(auto simp add:)
[PROOF STATE]
proof (state)
this:
path_image \<gamma> \<subseteq> path_image (rec_join ((k', \<gamma>') # l))

goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> path_image \<gamma> \<subseteq> path_image (rec_join ((k', \<gamma>') # l))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> path_image \<gamma> \<subseteq> path_image (rec_join ((k', \<gamma>') # l))
[PROOF STEP]
assume "l\<noteq>[]"
[PROOF STATE]
proof (state)
this:
l \<noteq> []

goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> path_image \<gamma> \<subseteq> path_image (rec_join ((k', \<gamma>') # l))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l \<noteq> []
[PROOF STEP]
obtain b l' where b_l: "l = b # l'"
[PROOF STATE]
proof (prove)
using this:
l \<noteq> []

goal (1 subgoal):
 1. (\<And>b l'. l = b # l' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson rec_join.elims)
[PROOF STATE]
proof (state)
this:
l = b # l'

goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> path_image \<gamma> \<subseteq> path_image (rec_join ((k', \<gamma>') # l))
[PROOF STEP]
obtain k'' \<gamma>'' where b: "b = (k'',\<gamma>'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k'' \<gamma>''. b = (k'', \<gamma>'') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
b = (k'', \<gamma>'')

goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> path_image \<gamma> \<subseteq> path_image (rec_join ((k', \<gamma>') # l))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path_image \<gamma> \<subseteq> path_image (rec_join ((k', \<gamma>') # l))
[PROOF STEP]
using ass path_image_reversepath b_l path_image_join
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?k, ?\<gamma>) \<in> set l; valid_chain_list l\<rbrakk> \<Longrightarrow> path_image ?\<gamma> \<subseteq> path_image (rec_join l)
(k, \<gamma>) \<in> set (a # l)
valid_chain_list (a # l)
path_image (reversepath ?g) = path_image ?g
l = b # l'
pathfinish ?g1.0 = pathstart ?g2.0 \<Longrightarrow> path_image (?g1.0 +++ ?g2.0) = path_image ?g1.0 \<union> path_image ?g2.0

goal (1 subgoal):
 1. path_image \<gamma> \<subseteq> path_image (rec_join ((k', \<gamma>') # l))
[PROOF STEP]
by(fastforce simp add: a)
[PROOF STATE]
proof (state)
this:
path_image \<gamma> \<subseteq> path_image (rec_join ((k', \<gamma>') # l))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
path_image \<gamma> \<subseteq> path_image (rec_join ((k', \<gamma>') # l))

goal (1 subgoal):
 1. \<And>a l k \<gamma>. \<lbrakk>\<And>k \<gamma>. \<lbrakk>(k, \<gamma>) \<in> set l; valid_chain_list l\<rbrakk> \<Longrightarrow> path_image \<gamma> \<subseteq> path_image (rec_join l); (k, \<gamma>) \<in> set (a # l); valid_chain_list (a # l)\<rbrakk> \<Longrightarrow> path_image \<gamma> \<subseteq> path_image (rec_join (a # l))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path_image \<gamma> \<subseteq> path_image (rec_join ((k', \<gamma>') # l))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
path_image \<gamma> \<subseteq> path_image (rec_join ((k', \<gamma>') # l))

goal (1 subgoal):
 1. path_image \<gamma> \<subseteq> path_image (rec_join (a # l))
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
path_image \<gamma> \<subseteq> path_image (rec_join ((k', \<gamma>') # l))
a = (k', \<gamma>')

goal (1 subgoal):
 1. path_image \<gamma> \<subseteq> path_image (rec_join (a # l))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path_image \<gamma> \<subseteq> path_image (rec_join (a # l))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma path_image_rec_join_2:
  fixes l
  shows "l \<noteq> [] \<Longrightarrow> valid_chain_list l \<Longrightarrow> path_image (rec_join l) \<subseteq> (\<Union>(k, \<gamma>) \<in> set l. path_image \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>l \<noteq> []; valid_chain_list l\<rbrakk> \<Longrightarrow> path_image (rec_join l) \<subseteq> (\<Union>(k, \<gamma>)\<in>set l. path_image \<gamma>)
[PROOF STEP]
proof(induction l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>[] \<noteq> []; valid_chain_list []\<rbrakk> \<Longrightarrow> path_image (rec_join []) \<subseteq> (\<Union>(k, y)\<in>set []. path_image y)
 2. \<And>a l. \<lbrakk>\<lbrakk>l \<noteq> []; valid_chain_list l\<rbrakk> \<Longrightarrow> path_image (rec_join l) \<subseteq> (\<Union>(k, y)\<in>set l. path_image y); a # l \<noteq> []; valid_chain_list (a # l)\<rbrakk> \<Longrightarrow> path_image (rec_join (a # l)) \<subseteq> (\<Union>(k, y)\<in>set (a # l). path_image y)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
[] \<noteq> []
valid_chain_list []

goal (2 subgoals):
 1. \<lbrakk>[] \<noteq> []; valid_chain_list []\<rbrakk> \<Longrightarrow> path_image (rec_join []) \<subseteq> (\<Union>(k, y)\<in>set []. path_image y)
 2. \<And>a l. \<lbrakk>\<lbrakk>l \<noteq> []; valid_chain_list l\<rbrakk> \<Longrightarrow> path_image (rec_join l) \<subseteq> (\<Union>(k, y)\<in>set l. path_image y); a # l \<noteq> []; valid_chain_list (a # l)\<rbrakk> \<Longrightarrow> path_image (rec_join (a # l)) \<subseteq> (\<Union>(k, y)\<in>set (a # l). path_image y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[] \<noteq> []
valid_chain_list []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
[] \<noteq> []
valid_chain_list []

goal (1 subgoal):
 1. path_image (rec_join []) \<subseteq> (\<Union>a\<in>set []. case a of (k, a) \<Rightarrow> path_image a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path_image (rec_join []) \<subseteq> (\<Union>a\<in>set []. case a of (k, a) \<Rightarrow> path_image a)

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>\<lbrakk>l \<noteq> []; valid_chain_list l\<rbrakk> \<Longrightarrow> path_image (rec_join l) \<subseteq> (\<Union>(k, y)\<in>set l. path_image y); a # l \<noteq> []; valid_chain_list (a # l)\<rbrakk> \<Longrightarrow> path_image (rec_join (a # l)) \<subseteq> (\<Union>(k, y)\<in>set (a # l). path_image y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l. \<lbrakk>\<lbrakk>l \<noteq> []; valid_chain_list l\<rbrakk> \<Longrightarrow> path_image (rec_join l) \<subseteq> (\<Union>(k, y)\<in>set l. path_image y); a # l \<noteq> []; valid_chain_list (a # l)\<rbrakk> \<Longrightarrow> path_image (rec_join (a # l)) \<subseteq> (\<Union>(k, y)\<in>set (a # l). path_image y)
[PROOF STEP]
case ass: (Cons a l)
[PROOF STATE]
proof (state)
this:
\<lbrakk>l \<noteq> []; valid_chain_list l\<rbrakk> \<Longrightarrow> path_image (rec_join l) \<subseteq> (\<Union>a\<in>set l. case a of (k, a) \<Rightarrow> path_image a)
a # l \<noteq> []
valid_chain_list (a # l)

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>\<lbrakk>l \<noteq> []; valid_chain_list l\<rbrakk> \<Longrightarrow> path_image (rec_join l) \<subseteq> (\<Union>(k, y)\<in>set l. path_image y); a # l \<noteq> []; valid_chain_list (a # l)\<rbrakk> \<Longrightarrow> path_image (rec_join (a # l)) \<subseteq> (\<Union>(k, y)\<in>set (a # l). path_image y)
[PROOF STEP]
obtain k' \<gamma>' where a: "a = (k',\<gamma>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k' \<gamma>'. a = (k', \<gamma>') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
a = (k', \<gamma>')

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>\<lbrakk>l \<noteq> []; valid_chain_list l\<rbrakk> \<Longrightarrow> path_image (rec_join l) \<subseteq> (\<Union>(k, y)\<in>set l. path_image y); a # l \<noteq> []; valid_chain_list (a # l)\<rbrakk> \<Longrightarrow> path_image (rec_join (a # l)) \<subseteq> (\<Union>(k, y)\<in>set (a # l). path_image y)
[PROOF STEP]
have "path_image (rec_join (a # l)) \<subseteq> (\<Union>(k, y)\<in>set (a # l). path_image y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path_image (rec_join (a # l)) \<subseteq> (\<Union>(k, y)\<in>set (a # l). path_image y)
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> path_image (rec_join (a # l)) \<subseteq> (\<Union>(k, y)\<in>set (a # l). path_image y)
 2. \<not> ?P \<Longrightarrow> path_image (rec_join (a # l)) \<subseteq> (\<Union>(k, y)\<in>set (a # l). path_image y)
[PROOF STEP]
assume "l=[]"
[PROOF STATE]
proof (state)
this:
l = []

goal (2 subgoals):
 1. ?P \<Longrightarrow> path_image (rec_join (a # l)) \<subseteq> (\<Union>(k, y)\<in>set (a # l). path_image y)
 2. \<not> ?P \<Longrightarrow> path_image (rec_join (a # l)) \<subseteq> (\<Union>(k, y)\<in>set (a # l). path_image y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l = []
[PROOF STEP]
show "path_image (rec_join (a # l)) \<subseteq> (\<Union>(k, y)\<in>set (a # l). path_image y)"
[PROOF STATE]
proof (prove)
using this:
l = []

goal (1 subgoal):
 1. path_image (rec_join (a # l)) \<subseteq> (\<Union>(k, y)\<in>set (a # l). path_image y)
[PROOF STEP]
using step a
[PROOF STATE]
proof (prove)
using this:
l = []
?x \<in> ccpo_class.iterates ?f \<Longrightarrow> ?f ?x \<in> ccpo_class.iterates ?f
a = (k', \<gamma>')

goal (1 subgoal):
 1. path_image (rec_join (a # l)) \<subseteq> (\<Union>(k, y)\<in>set (a # l). path_image y)
[PROOF STEP]
by(auto simp add:)
[PROOF STATE]
proof (state)
this:
path_image (rec_join (a # l)) \<subseteq> (\<Union>(k, y)\<in>set (a # l). path_image y)

goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> path_image (rec_join (a # l)) \<subseteq> (\<Union>(k, y)\<in>set (a # l). path_image y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> path_image (rec_join (a # l)) \<subseteq> (\<Union>(k, y)\<in>set (a # l). path_image y)
[PROOF STEP]
assume "l\<noteq>[]"
[PROOF STATE]
proof (state)
this:
l \<noteq> []

goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> path_image (rec_join (a # l)) \<subseteq> (\<Union>(k, y)\<in>set (a # l). path_image y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l \<noteq> []
[PROOF STEP]
obtain b l' where b_l: "l = b # l'"
[PROOF STATE]
proof (prove)
using this:
l \<noteq> []

goal (1 subgoal):
 1. (\<And>b l'. l = b # l' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson rec_join.elims)
[PROOF STATE]
proof (state)
this:
l = b # l'

goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> path_image (rec_join (a # l)) \<subseteq> (\<Union>(k, y)\<in>set (a # l). path_image y)
[PROOF STEP]
obtain k'' \<gamma>'' where b: "b = (k'',\<gamma>'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k'' \<gamma>''. b = (k'', \<gamma>'') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
b = (k'', \<gamma>'')

goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> path_image (rec_join (a # l)) \<subseteq> (\<Union>(k, y)\<in>set (a # l). path_image y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path_image (rec_join (a # l)) \<subseteq> (\<Union>(k, y)\<in>set (a # l). path_image y)
[PROOF STEP]
using ass
        path_image_reversepath b_l path_image_join
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>l \<noteq> []; valid_chain_list l\<rbrakk> \<Longrightarrow> path_image (rec_join l) \<subseteq> (\<Union>a\<in>set l. case a of (k, a) \<Rightarrow> path_image a)
a # l \<noteq> []
valid_chain_list (a # l)
path_image (reversepath ?g) = path_image ?g
l = b # l'
pathfinish ?g1.0 = pathstart ?g2.0 \<Longrightarrow> path_image (?g1.0 +++ ?g2.0) = path_image ?g1.0 \<union> path_image ?g2.0

goal (1 subgoal):
 1. path_image (rec_join (a # l)) \<subseteq> (\<Union>(k, y)\<in>set (a # l). path_image y)
[PROOF STEP]
apply(auto simp add: a)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a ba k baa. \<lbrakk>path_image (rec_join ((k, baa) # l')) \<subseteq> path_image baa \<union> (\<Union>x\<in>set l'. case x of (k, x) \<Rightarrow> path_image x); l = (k, baa) # l'; \<And>g1 g2. pathfinish g1 = pathstart g2 \<Longrightarrow> path_image (g1 +++ g2) = path_image g1 \<union> path_image g2; pathfinish \<gamma>' = pathstart (rec_join ((k, baa) # l')); valid_chain_list ((k, baa) # l'); k' = 1; (a, ba) \<in> path_image (\<gamma>' +++ rec_join ((k, baa) # l')); (a, ba) \<notin> path_image \<gamma>'; \<forall>x\<in>set l'. (a, ba) \<notin> (case x of (k, x) \<Rightarrow> path_image x); b = (k, baa)\<rbrakk> \<Longrightarrow> (a, ba) \<in> path_image baa
 2. \<And>a ba k baa. \<lbrakk>path_image (rec_join ((k, baa) # l')) \<subseteq> path_image baa \<union> (\<Union>x\<in>set l'. case x of (k, x) \<Rightarrow> path_image x); l = (k, baa) # l'; \<And>g1 g2. pathfinish g1 = pathstart g2 \<Longrightarrow> path_image (g1 +++ g2) = path_image g1 \<union> path_image g2; pathstart \<gamma>' = pathstart (rec_join ((k, baa) # l')); valid_chain_list ((k, baa) # l'); k' \<noteq> 1; (a, ba) \<in> path_image (reversepath \<gamma>' +++ rec_join ((k, baa) # l')); (a, ba) \<notin> path_image \<gamma>'; \<forall>x\<in>set l'. (a, ba) \<notin> (case x of (k, x) \<Rightarrow> path_image x); b = (k, baa)\<rbrakk> \<Longrightarrow> (a, ba) \<in> path_image baa
[PROOF STEP]
(*Excuse the ugliness of the next script*)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a ba k baa. \<lbrakk>path_image (rec_join ((k, baa) # l')) \<subseteq> path_image baa \<union> (\<Union>x\<in>set l'. case x of (k, x) \<Rightarrow> path_image x); l = (k, baa) # l'; \<And>g1 g2. pathfinish g1 = pathstart g2 \<Longrightarrow> path_image (g1 +++ g2) = path_image g1 \<union> path_image g2; pathfinish \<gamma>' = pathstart (rec_join ((k, baa) # l')); valid_chain_list ((k, baa) # l'); k' = 1; (a, ba) \<in> path_image (\<gamma>' +++ rec_join ((k, baa) # l')); (a, ba) \<notin> path_image \<gamma>'; \<forall>x\<in>set l'. (a, ba) \<notin> (case x of (k, x) \<Rightarrow> path_image x); b = (k, baa)\<rbrakk> \<Longrightarrow> (a, ba) \<in> path_image baa
 2. \<And>a ba k baa. \<lbrakk>path_image (rec_join ((k, baa) # l')) \<subseteq> path_image baa \<union> (\<Union>x\<in>set l'. case x of (k, x) \<Rightarrow> path_image x); l = (k, baa) # l'; \<And>g1 g2. pathfinish g1 = pathstart g2 \<Longrightarrow> path_image (g1 +++ g2) = path_image g1 \<union> path_image g2; pathstart \<gamma>' = pathstart (rec_join ((k, baa) # l')); valid_chain_list ((k, baa) # l'); k' \<noteq> 1; (a, ba) \<in> path_image (reversepath \<gamma>' +++ rec_join ((k, baa) # l')); (a, ba) \<notin> path_image \<gamma>'; \<forall>x\<in>set l'. (a, ba) \<notin> (case x of (k, x) \<Rightarrow> path_image x); b = (k, baa)\<rbrakk> \<Longrightarrow> (a, ba) \<in> path_image baa
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a ba k baa. \<lbrakk>path_image (rec_join ((k, baa) # l')) \<subseteq> path_image baa \<union> (\<Union>x\<in>set l'. case x of (k, x) \<Rightarrow> path_image x); l = (k, baa) # l'; \<And>g1 g2. pathfinish g1 = pathstart g2 \<Longrightarrow> path_image (g1 +++ g2) = path_image g1 \<union> path_image g2; pathstart \<gamma>' = pathstart (rec_join ((k, baa) # l')); valid_chain_list ((k, baa) # l'); k' \<noteq> 1; (a, ba) \<in> path_image (reversepath \<gamma>' +++ rec_join ((k, baa) # l')); (a, ba) \<notin> path_image \<gamma>'; \<forall>x\<in>set l'. (a, ba) \<notin> (case x of (k, x) \<Rightarrow> path_image x); b = (k, baa)\<rbrakk> \<Longrightarrow> (a, ba) \<in> path_image baa
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
path_image (rec_join (a # l)) \<subseteq> (\<Union>(k, y)\<in>set (a # l). path_image y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
path_image (rec_join (a # l)) \<subseteq> (\<Union>(k, y)\<in>set (a # l). path_image y)

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>\<lbrakk>l \<noteq> []; valid_chain_list l\<rbrakk> \<Longrightarrow> path_image (rec_join l) \<subseteq> (\<Union>(k, y)\<in>set l. path_image y); a # l \<noteq> []; valid_chain_list (a # l)\<rbrakk> \<Longrightarrow> path_image (rec_join (a # l)) \<subseteq> (\<Union>(k, y)\<in>set (a # l). path_image y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path_image (rec_join (a # l)) \<subseteq> (\<Union>(k, y)\<in>set (a # l). path_image y)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
path_image (rec_join (a # l)) \<subseteq> (\<Union>(k, y)\<in>set (a # l). path_image y)

goal (1 subgoal):
 1. path_image (rec_join (a # l)) \<subseteq> (\<Union>a\<in>set (a # l). case a of (k, a) \<Rightarrow> path_image a)
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
path_image (rec_join (a # l)) \<subseteq> (\<Union>(k, y)\<in>set (a # l). path_image y)
a = (k', \<gamma>')

goal (1 subgoal):
 1. path_image (rec_join (a # l)) \<subseteq> (\<Union>a\<in>set (a # l). case a of (k, a) \<Rightarrow> path_image a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path_image (rec_join (a # l)) \<subseteq> (\<Union>a\<in>set (a # l). case a of (k, a) \<Rightarrow> path_image a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma continuous_on_closed_UN:
  assumes "finite S"
  shows "((\<And>s. s \<in> S \<Longrightarrow> closed s) \<Longrightarrow> (\<And>s. s \<in> S \<Longrightarrow> continuous_on s f) \<Longrightarrow> continuous_on (\<Union>S) f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. s \<in> S \<Longrightarrow> closed s; \<And>s. s \<in> S \<Longrightarrow> continuous_on s f\<rbrakk> \<Longrightarrow> continuous_on (\<Union> S) f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite S

goal (1 subgoal):
 1. \<lbrakk>\<And>s. s \<in> S \<Longrightarrow> closed s; \<And>s. s \<in> S \<Longrightarrow> continuous_on s f\<rbrakk> \<Longrightarrow> continuous_on (\<Union> S) f
[PROOF STEP]
proof(induction S)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>s. s \<in> {} \<Longrightarrow> closed s; \<And>s. s \<in> {} \<Longrightarrow> continuous_on s f\<rbrakk> \<Longrightarrow> continuous_on (\<Union> {}) f
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>\<And>s. s \<in> F \<Longrightarrow> closed s; \<And>s. s \<in> F \<Longrightarrow> continuous_on s f\<rbrakk> \<Longrightarrow> continuous_on (\<Union> F) f; \<And>s. s \<in> insert x F \<Longrightarrow> closed s; \<And>s. s \<in> insert x F \<Longrightarrow> continuous_on s f\<rbrakk> \<Longrightarrow> continuous_on (\<Union> (insert x F)) f
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
?s \<in> {} \<Longrightarrow> closed ?s
?s \<in> {} \<Longrightarrow> continuous_on ?s f

goal (2 subgoals):
 1. \<lbrakk>\<And>s. s \<in> {} \<Longrightarrow> closed s; \<And>s. s \<in> {} \<Longrightarrow> continuous_on s f\<rbrakk> \<Longrightarrow> continuous_on (\<Union> {}) f
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>\<And>s. s \<in> F \<Longrightarrow> closed s; \<And>s. s \<in> F \<Longrightarrow> continuous_on s f\<rbrakk> \<Longrightarrow> continuous_on (\<Union> F) f; \<And>s. s \<in> insert x F \<Longrightarrow> closed s; \<And>s. s \<in> insert x F \<Longrightarrow> continuous_on s f\<rbrakk> \<Longrightarrow> continuous_on (\<Union> (insert x F)) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?s \<in> {} \<Longrightarrow> closed ?s
?s \<in> {} \<Longrightarrow> continuous_on ?s f
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?s \<in> {} \<Longrightarrow> closed ?s
?s \<in> {} \<Longrightarrow> continuous_on ?s f

goal (1 subgoal):
 1. continuous_on (\<Union> {}) f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
continuous_on (\<Union> {}) f

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>\<And>s. s \<in> F \<Longrightarrow> closed s; \<And>s. s \<in> F \<Longrightarrow> continuous_on s f\<rbrakk> \<Longrightarrow> continuous_on (\<Union> F) f; \<And>s. s \<in> insert x F \<Longrightarrow> closed s; \<And>s. s \<in> insert x F \<Longrightarrow> continuous_on s f\<rbrakk> \<Longrightarrow> continuous_on (\<Union> (insert x F)) f
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>\<And>s. s \<in> F \<Longrightarrow> closed s; \<And>s. s \<in> F \<Longrightarrow> continuous_on s f\<rbrakk> \<Longrightarrow> continuous_on (\<Union> F) f; \<And>s. s \<in> insert x F \<Longrightarrow> closed s; \<And>s. s \<in> insert x F \<Longrightarrow> continuous_on s f\<rbrakk> \<Longrightarrow> continuous_on (\<Union> (insert x F)) f
[PROOF STEP]
case (insert x F)
[PROOF STATE]
proof (state)
this:
finite F
x \<notin> F
\<lbrakk>\<And>s. s \<in> F \<Longrightarrow> closed s; \<And>s. s \<in> F \<Longrightarrow> continuous_on s f\<rbrakk> \<Longrightarrow> continuous_on (\<Union> F) f
?s \<in> insert x F \<Longrightarrow> closed ?s
?s \<in> insert x F \<Longrightarrow> continuous_on ?s f

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>\<And>s. s \<in> F \<Longrightarrow> closed s; \<And>s. s \<in> F \<Longrightarrow> continuous_on s f\<rbrakk> \<Longrightarrow> continuous_on (\<Union> F) f; \<And>s. s \<in> insert x F \<Longrightarrow> closed s; \<And>s. s \<in> insert x F \<Longrightarrow> continuous_on s f\<rbrakk> \<Longrightarrow> continuous_on (\<Union> (insert x F)) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite F
x \<notin> F
\<lbrakk>\<And>s. s \<in> F \<Longrightarrow> closed s; \<And>s. s \<in> F \<Longrightarrow> continuous_on s f\<rbrakk> \<Longrightarrow> continuous_on (\<Union> F) f
?s \<in> insert x F \<Longrightarrow> closed ?s
?s \<in> insert x F \<Longrightarrow> continuous_on ?s f
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
finite F
x \<notin> F
\<lbrakk>\<And>s. s \<in> F \<Longrightarrow> closed s; \<And>s. s \<in> F \<Longrightarrow> continuous_on s f\<rbrakk> \<Longrightarrow> continuous_on (\<Union> F) f
?s \<in> insert x F \<Longrightarrow> closed ?s
?s \<in> insert x F \<Longrightarrow> continuous_on ?s f

goal (1 subgoal):
 1. continuous_on (\<Union> (insert x F)) f
[PROOF STEP]
using continuous_on_closed_Un closed_Union
[PROOF STATE]
proof (prove)
using this:
finite F
x \<notin> F
\<lbrakk>\<And>s. s \<in> F \<Longrightarrow> closed s; \<And>s. s \<in> F \<Longrightarrow> continuous_on s f\<rbrakk> \<Longrightarrow> continuous_on (\<Union> F) f
?s \<in> insert x F \<Longrightarrow> closed ?s
?s \<in> insert x F \<Longrightarrow> continuous_on ?s f
\<lbrakk>closed ?s; closed ?t; continuous_on ?s ?f; continuous_on ?t ?f\<rbrakk> \<Longrightarrow> continuous_on (?s \<union> ?t) ?f
\<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk> \<Longrightarrow> closed (\<Union> ?S)

goal (1 subgoal):
 1. continuous_on (\<Union> (insert x F)) f
[PROOF STEP]
by (simp add: closed_Union continuous_on_closed_Un)
[PROOF STATE]
proof (state)
this:
continuous_on (\<Union> (insert x F)) f

goal:
No subgoals!
[PROOF STEP]
qed