[STATEMENT]
lemma line_integral_rec_join_cons_2:
  assumes "line_integral_exists F basis \<gamma>"
    "line_integral_exists F basis (rec_join ((l)))"
    "(\<And>k' \<gamma>'. (k', \<gamma>') \<in> set ((-1,\<gamma>) # l) \<Longrightarrow> valid_path \<gamma>')"
    "finite basis"
  shows "line_integral F basis (rec_join ((-1,\<gamma>) # l)) = line_integral F basis ((reversepath \<gamma>) +++ (rec_join l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis (rec_join ((- 1, \<gamma>) # l)) = line_integral F basis (reversepath \<gamma> +++ rec_join l)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> line_integral F basis (rec_join ((- 1, \<gamma>) # l)) = line_integral F basis (reversepath \<gamma> +++ rec_join l)
 2. \<not> ?P \<Longrightarrow> line_integral F basis (rec_join ((- 1, \<gamma>) # l)) = line_integral F basis (reversepath \<gamma> +++ rec_join l)
[PROOF STEP]
assume l_empty: "l = []"
[PROOF STATE]
proof (state)
this:
l = []

goal (2 subgoals):
 1. ?P \<Longrightarrow> line_integral F basis (rec_join ((- 1, \<gamma>) # l)) = line_integral F basis (reversepath \<gamma> +++ rec_join l)
 2. \<not> ?P \<Longrightarrow> line_integral F basis (rec_join ((- 1, \<gamma>) # l)) = line_integral F basis (reversepath \<gamma> +++ rec_join l)
[PROOF STEP]
have 0: "line_integral_exists F basis (reversepath \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis (reversepath \<gamma>)
[PROOF STEP]
using assms line_integral_on_reverse_path(2)
[PROOF STATE]
proof (prove)
using this:
line_integral_exists F basis \<gamma>
line_integral_exists F basis (rec_join l)
(?k', ?\<gamma>') \<in> set ((- 1, \<gamma>) # l) \<Longrightarrow> valid_path ?\<gamma>'
finite basis
\<lbrakk>valid_path ?\<gamma>; line_integral_exists ?F ?basis ?\<gamma>\<rbrakk> \<Longrightarrow> line_integral_exists ?F ?basis (reversepath ?\<gamma>)

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> line_integral F basis (rec_join ((- 1, \<gamma>) # l)) = line_integral F basis (reversepath \<gamma> +++ rec_join l)
 2. \<not> ?P \<Longrightarrow> line_integral F basis (rec_join ((- 1, \<gamma>) # l)) = line_integral F basis (reversepath \<gamma> +++ rec_join l)
[PROOF STEP]
have 1: "valid_path (reversepath \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path (reversepath \<gamma>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
line_integral_exists F basis \<gamma>
line_integral_exists F basis (rec_join l)
(?k', ?\<gamma>') \<in> set ((- 1, \<gamma>) # l) \<Longrightarrow> valid_path ?\<gamma>'
finite basis

goal (1 subgoal):
 1. valid_path (reversepath \<gamma>)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
valid_path (reversepath \<gamma>)

goal (2 subgoals):
 1. ?P \<Longrightarrow> line_integral F basis (rec_join ((- 1, \<gamma>) # l)) = line_integral F basis (reversepath \<gamma> +++ rec_join l)
 2. \<not> ?P \<Longrightarrow> line_integral F basis (rec_join ((- 1, \<gamma>) # l)) = line_integral F basis (reversepath \<gamma> +++ rec_join l)
[PROOF STEP]
show "line_integral F basis (rec_join ((-1,\<gamma>) # l)) = line_integral F basis ((reversepath \<gamma>) +++ (rec_join l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis (rec_join ((- 1, \<gamma>) # l)) = line_integral F basis (reversepath \<gamma> +++ rec_join l)
[PROOF STEP]
using assms line_integral_distrib(1)[OF 0 line_integral_exists_on_degenerate_path[OF assms(4)], of "0"]
[PROOF STATE]
proof (prove)
using this:
line_integral_exists F basis \<gamma>
line_integral_exists F basis (rec_join l)
(?k', ?\<gamma>') \<in> set ((- 1, \<gamma>) # l) \<Longrightarrow> valid_path ?\<gamma>'
finite basis
\<lbrakk>valid_path (reversepath \<gamma>); valid_path (\<lambda>x. 0)\<rbrakk> \<Longrightarrow> line_integral F basis (reversepath \<gamma> +++ (\<lambda>x. 0)) = line_integral F basis (reversepath \<gamma>) + line_integral F basis (\<lambda>x. 0)

goal (1 subgoal):
 1. line_integral F basis (rec_join ((- 1, \<gamma>) # l)) = line_integral F basis (reversepath \<gamma> +++ rec_join l)
[PROOF STEP]
apply (auto simp add: l_empty)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>line_integral_exists F basis \<gamma>; line_integral_exists F basis (\<lambda>x. 0); valid_path \<gamma>; finite basis; valid_path (\<lambda>x. 0) \<Longrightarrow> line_integral F basis (reversepath \<gamma> +++ (\<lambda>x. 0)) = line_integral F basis (reversepath \<gamma>) + line_integral F basis (\<lambda>x. 0)\<rbrakk> \<Longrightarrow> line_integral F basis (reversepath \<gamma>) = line_integral F basis (reversepath \<gamma> +++ (\<lambda>x. 0))
[PROOF STEP]
using degenerate_path_is_valid_path line_integral_degenerate_path
[PROOF STATE]
proof (prove)
using this:
valid_path (\<lambda>x. ?c)
finite ?basis \<Longrightarrow> line_integral ?F ?basis (\<lambda>x. ?c) = 0

goal (1 subgoal):
 1. \<lbrakk>line_integral_exists F basis \<gamma>; line_integral_exists F basis (\<lambda>x. 0); valid_path \<gamma>; finite basis; valid_path (\<lambda>x. 0) \<Longrightarrow> line_integral F basis (reversepath \<gamma> +++ (\<lambda>x. 0)) = line_integral F basis (reversepath \<gamma>) + line_integral F basis (\<lambda>x. 0)\<rbrakk> \<Longrightarrow> line_integral F basis (reversepath \<gamma>) = line_integral F basis (reversepath \<gamma> +++ (\<lambda>x. 0))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
line_integral F basis (rec_join ((- 1, \<gamma>) # l)) = line_integral F basis (reversepath \<gamma> +++ rec_join l)

goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> line_integral F basis (rec_join ((- 1, \<gamma>) # l)) = line_integral F basis (reversepath \<gamma> +++ rec_join l)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> line_integral F basis (rec_join ((- 1, \<gamma>) # l)) = line_integral F basis (reversepath \<gamma> +++ rec_join l)
[PROOF STEP]
assume "l \<noteq> []"
[PROOF STATE]
proof (state)
this:
l \<noteq> []

goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> line_integral F basis (rec_join ((- 1, \<gamma>) # l)) = line_integral F basis (reversepath \<gamma> +++ rec_join l)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l \<noteq> []
[PROOF STEP]
obtain h l' where l_nempty: "l = h#l'"
[PROOF STATE]
proof (prove)
using this:
l \<noteq> []

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

goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> line_integral F basis (rec_join ((- 1, \<gamma>) # l)) = line_integral F basis (reversepath \<gamma> +++ rec_join l)
[PROOF STEP]
show "line_integral F basis (rec_join ((-1,\<gamma>) # l)) = line_integral F basis ((reversepath \<gamma>) +++ (rec_join l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis (rec_join ((- 1, \<gamma>) # l)) = line_integral F basis (reversepath \<gamma> +++ rec_join l)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
line_integral_exists F basis \<gamma>
line_integral_exists F basis (rec_join l)
(?k', ?\<gamma>') \<in> set ((- 1, \<gamma>) # l) \<Longrightarrow> valid_path ?\<gamma>'
finite basis

goal (1 subgoal):
 1. line_integral F basis (rec_join ((- 1, \<gamma>) # l)) = line_integral F basis (reversepath \<gamma> +++ rec_join l)
[PROOF STEP]
by (auto simp add: l_nempty)
[PROOF STATE]
proof (state)
this:
line_integral F basis (rec_join ((- 1, \<gamma>) # l)) = line_integral F basis (reversepath \<gamma> +++ rec_join l)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma one_chain_line_integral_rec_join:
  assumes l_props: "set l = one_chain" "distinct l" "valid_chain_list l" and
    boundary_chain: "boundary_chain one_chain" and
    line_integral_exists: "\<forall>(k::int, \<gamma>) \<in> one_chain. line_integral_exists F basis \<gamma>" and
    valid_path: "\<forall>(k::int, \<gamma>) \<in> one_chain. valid_path \<gamma>" and
    finite_basis: "finite basis"
  shows "line_integral F basis (rec_join l) = one_chain_line_integral F basis one_chain"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis (rec_join l) = one_chain_line_integral F basis one_chain
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. line_integral F basis (rec_join l) = one_chain_line_integral F basis one_chain
[PROOF STEP]
have 0: "sum_list (map (\<lambda>((k::int), \<gamma>). (k::int) * (line_integral F basis \<gamma>)) l) = one_chain_line_integral F basis one_chain"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(k, \<gamma>)\<leftarrow>l. real_of_int k * line_integral F basis \<gamma>) = one_chain_line_integral F basis one_chain
[PROOF STEP]
unfolding one_chain_line_integral_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(k, \<gamma>)\<leftarrow>l. real_of_int k * line_integral F basis \<gamma>) = (\<Sum>(k, g)\<in>one_chain. real_of_int k * line_integral F basis g)
[PROOF STEP]
using l_props Groups_List.comm_monoid_add_class.sum.distinct_set_conv_list[OF l_props(2), of "(\<lambda>(k, \<gamma>). (k::int) * (line_integral F basis \<gamma>))"]
[PROOF STATE]
proof (prove)
using this:
set l = one_chain
distinct l
valid_chain_list l
(\<Sum>(k, \<gamma>)\<in>set l. real_of_int k * line_integral F basis \<gamma>) = (\<Sum>(k, \<gamma>)\<leftarrow>l. real_of_int k * line_integral F basis \<gamma>)

goal (1 subgoal):
 1. (\<Sum>(k, \<gamma>)\<leftarrow>l. real_of_int k * line_integral F basis \<gamma>) = (\<Sum>(k, g)\<in>one_chain. real_of_int k * line_integral F basis g)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>(k, \<gamma>)\<leftarrow>l. real_of_int k * line_integral F basis \<gamma>) = one_chain_line_integral F basis one_chain

goal (1 subgoal):
 1. line_integral F basis (rec_join l) = one_chain_line_integral F basis one_chain
[PROOF STEP]
have "valid_chain_list l \<Longrightarrow>
                    boundary_chain (set l) \<Longrightarrow>
                    (\<forall>(k::int, \<gamma>) \<in> set l. line_integral_exists F basis \<gamma>) \<Longrightarrow>
                    (\<forall>(k::int, \<gamma>) \<in> set l. valid_path \<gamma>) \<Longrightarrow>
                    line_integral F basis (rec_join l) = sum_list (map (\<lambda>(k::int, \<gamma>). k * (line_integral F basis \<gamma>)) l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_chain_list l; boundary_chain (set l); \<forall>(k, \<gamma>)\<in>set l. line_integral_exists F basis \<gamma>; \<forall>(k, \<gamma>)\<in>set l. valid_path \<gamma>\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join l) = (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
proof (induction l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>valid_chain_list []; boundary_chain (set []); \<forall>(k, y)\<in>set []. line_integral_exists F basis y; \<forall>(k, y)\<in>set []. valid_path y\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join []) = (\<Sum>(x, \<gamma>)\<leftarrow>[]. real_of_int x * line_integral F basis \<gamma>)
 2. \<And>a l. \<lbrakk>\<lbrakk>valid_chain_list l; boundary_chain (set l); \<forall>(k, y)\<in>set l. line_integral_exists F basis y; \<forall>(k, y)\<in>set l. valid_path y\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join l) = (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>); valid_chain_list (a # l); boundary_chain (set (a # l)); \<forall>(k, y)\<in>set (a # l). line_integral_exists F basis y; \<forall>(k, y)\<in>set (a # l). valid_path y\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join (a # l)) = (\<Sum>(x, \<gamma>)\<leftarrow>a # l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
valid_chain_list []
boundary_chain (set [])
\<forall>a\<in>set []. case a of (k, a) \<Rightarrow> line_integral_exists F basis a
\<forall>a\<in>set []. case a of (k, a) \<Rightarrow> valid_path a

goal (2 subgoals):
 1. \<lbrakk>valid_chain_list []; boundary_chain (set []); \<forall>(k, y)\<in>set []. line_integral_exists F basis y; \<forall>(k, y)\<in>set []. valid_path y\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join []) = (\<Sum>(x, \<gamma>)\<leftarrow>[]. real_of_int x * line_integral F basis \<gamma>)
 2. \<And>a l. \<lbrakk>\<lbrakk>valid_chain_list l; boundary_chain (set l); \<forall>(k, y)\<in>set l. line_integral_exists F basis y; \<forall>(k, y)\<in>set l. valid_path y\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join l) = (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>); valid_chain_list (a # l); boundary_chain (set (a # l)); \<forall>(k, y)\<in>set (a # l). line_integral_exists F basis y; \<forall>(k, y)\<in>set (a # l). valid_path y\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join (a # l)) = (\<Sum>(x, \<gamma>)\<leftarrow>a # l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis (rec_join []) = (\<Sum>a\<leftarrow>[]. case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
unfolding line_integral_def boundary_chain_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. \<Sum>b\<in>basis. F (rec_join [] x) \<bullet> b * (vector_derivative (rec_join []) (at x within {0..1}) \<bullet> b)) = (\<Sum>a\<leftarrow>[]. case a of (x, \<gamma>) \<Rightarrow> real_of_int x * integral {0..1} (\<lambda>x. \<Sum>b\<in>basis. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)))
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. \<Sum>b\<in>basis. F 0 \<bullet> b * (vector_derivative (\<lambda>x. 0) (at x within {0..1}) \<bullet> b)) = 0
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>x. \<Sum>b\<in>basis. F 0 \<bullet> b * (vector_derivative (\<lambda>x. 0) (at x within {0..1}) \<bullet> b)) has_integral 0) {0..1}
[PROOF STEP]
have "\<forall>x. (vector_derivative (\<lambda>x. 0) (at x)) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. vector_derivative (\<lambda>x. 0::'a) (at x) = (0::'a)
[PROOF STEP]
using Derivative.vector_derivative_const_at
[PROOF STATE]
proof (prove)
using this:
vector_derivative (\<lambda>x. ?c) (at ?a) = (0::?'a)

goal (1 subgoal):
 1. \<forall>x. vector_derivative (\<lambda>x. 0::'a) (at x) = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x. vector_derivative (\<lambda>x. 0::?'a1) (at x) = (0::?'a1)

goal (1 subgoal):
 1. ((\<lambda>x. \<Sum>b\<in>basis. F 0 \<bullet> b * (vector_derivative (\<lambda>x. 0) (at x within {0..1}) \<bullet> b)) has_integral 0) {0..1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. vector_derivative (\<lambda>x. 0::?'a1) (at x) = (0::?'a1)
[PROOF STEP]
have "\<forall>x. ((\<lambda>x. 0) has_vector_derivative 0) (at x)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. vector_derivative (\<lambda>x. 0::?'a1) (at x) = (0::?'a1)

goal (1 subgoal):
 1. \<forall>x. ((\<lambda>x. 0::'a) has_vector_derivative (0::'a)) (at x)
[PROOF STEP]
using Derivative.vector_derivative_const_at
[PROOF STATE]
proof (prove)
using this:
\<forall>x. vector_derivative (\<lambda>x. 0::?'a1) (at x) = (0::?'a1)
vector_derivative (\<lambda>x. ?c) (at ?a) = (0::?'a)

goal (1 subgoal):
 1. \<forall>x. ((\<lambda>x. 0::'a) has_vector_derivative (0::'a)) (at x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x. ((\<lambda>x. 0::?'a2) has_vector_derivative (0::?'a2)) (at x)

goal (1 subgoal):
 1. ((\<lambda>x. \<Sum>b\<in>basis. F 0 \<bullet> b * (vector_derivative (\<lambda>x. 0) (at x within {0..1}) \<bullet> b)) has_integral 0) {0..1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. ((\<lambda>x. 0::?'a2) has_vector_derivative (0::?'a2)) (at x)
[PROOF STEP]
have "\<forall>x. ((\<lambda>x. 0) has_vector_derivative 0) (at x within {0..1})"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. ((\<lambda>x. 0::?'a2) has_vector_derivative (0::?'a2)) (at x)

goal (1 subgoal):
 1. \<forall>x. ((\<lambda>x. 0::'a) has_vector_derivative (0::'a)) (at x within {0..1})
[PROOF STEP]
using Derivative.vector_derivative_const_at
[PROOF STATE]
proof (prove)
using this:
\<forall>x. ((\<lambda>x. 0::?'a2) has_vector_derivative (0::?'a2)) (at x)
vector_derivative (\<lambda>x. ?c) (at ?a) = (0::?'a)

goal (1 subgoal):
 1. \<forall>x. ((\<lambda>x. 0::'a) has_vector_derivative (0::'a)) (at x within {0..1})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x. ((\<lambda>x. 0::?'a3) has_vector_derivative (0::?'a3)) (at x within {0..1})

goal (1 subgoal):
 1. ((\<lambda>x. \<Sum>b\<in>basis. F 0 \<bullet> b * (vector_derivative (\<lambda>x. 0) (at x within {0..1}) \<bullet> b)) has_integral 0) {0..1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. ((\<lambda>x. 0::?'a3) has_vector_derivative (0::?'a3)) (at x within {0..1})
[PROOF STEP]
have 0: "\<forall>x\<in>{0..1}. (vector_derivative (\<lambda>x. 0) (at x within{0..1})) = 0"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. ((\<lambda>x. 0::?'a3) has_vector_derivative (0::?'a3)) (at x within {0..1})

goal (1 subgoal):
 1. \<forall>x\<in>{0..1}. vector_derivative (\<lambda>x. 0::'a) (at x within {0..1}) = (0::'a)
[PROOF STEP]
by (metis (no_types) box_real(2) vector_derivative_within_cbox zero_less_one)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{0..1}. vector_derivative (\<lambda>x. 0::?'a4) (at x within {0..1}) = (0::?'a4)

goal (1 subgoal):
 1. ((\<lambda>x. \<Sum>b\<in>basis. F 0 \<bullet> b * (vector_derivative (\<lambda>x. 0) (at x within {0..1}) \<bullet> b)) has_integral 0) {0..1}
[PROOF STEP]
have "(\<forall>x\<in>{0..1}. (\<Sum>b\<in>basis. F 0 \<bullet> b * (vector_derivative (\<lambda>x. 0) (at x within {0..1}) \<bullet> b)) = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{0..1}. (\<Sum>b\<in>basis. F 0 \<bullet> b * (vector_derivative (\<lambda>x. 0) (at x within {0..1}) \<bullet> b)) = 0
[PROOF STEP]
by (simp add: 0)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{0..1}. (\<Sum>b\<in>basis. F 0 \<bullet> b * (vector_derivative (\<lambda>x. 0) (at x within {0..1}) \<bullet> b)) = 0

goal (1 subgoal):
 1. ((\<lambda>x. \<Sum>b\<in>basis. F 0 \<bullet> b * (vector_derivative (\<lambda>x. 0) (at x within {0..1}) \<bullet> b)) has_integral 0) {0..1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>{0..1}. (\<Sum>b\<in>basis. F 0 \<bullet> b * (vector_derivative (\<lambda>x. 0) (at x within {0..1}) \<bullet> b)) = 0
[PROOF STEP]
show "((\<lambda>x. \<Sum>b\<in>basis. F 0 \<bullet> b * (vector_derivative (\<lambda>x. 0) (at x within {0..1}) \<bullet> b)) has_integral 0) {0..1}"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0..1}. (\<Sum>b\<in>basis. F 0 \<bullet> b * (vector_derivative (\<lambda>x. 0) (at x within {0..1}) \<bullet> b)) = 0

goal (1 subgoal):
 1. ((\<lambda>x. \<Sum>b\<in>basis. F 0 \<bullet> b * (vector_derivative (\<lambda>x. 0) (at x within {0..1}) \<bullet> b)) has_integral 0) {0..1}
[PROOF STEP]
by (meson has_integral_is_0)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. \<Sum>b\<in>basis. F 0 \<bullet> b * (vector_derivative (\<lambda>x. 0) (at x within {0..1}) \<bullet> b)) has_integral 0) {0..1}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
line_integral F basis (rec_join []) = (\<Sum>a\<leftarrow>[]. case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>)

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>\<lbrakk>valid_chain_list l; boundary_chain (set l); \<forall>(k, y)\<in>set l. line_integral_exists F basis y; \<forall>(k, y)\<in>set l. valid_path y\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join l) = (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>); valid_chain_list (a # l); boundary_chain (set (a # l)); \<forall>(k, y)\<in>set (a # l). line_integral_exists F basis y; \<forall>(k, y)\<in>set (a # l). valid_path y\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join (a # l)) = (\<Sum>(x, \<gamma>)\<leftarrow>a # l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l. \<lbrakk>\<lbrakk>valid_chain_list l; boundary_chain (set l); \<forall>(k, y)\<in>set l. line_integral_exists F basis y; \<forall>(k, y)\<in>set l. valid_path y\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join l) = (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>); valid_chain_list (a # l); boundary_chain (set (a # l)); \<forall>(k, y)\<in>set (a # l). line_integral_exists F basis y; \<forall>(k, y)\<in>set (a # l). valid_path y\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join (a # l)) = (\<Sum>(x, \<gamma>)\<leftarrow>a # l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
case ass: (Cons a l)
[PROOF STATE]
proof (state)
this:
\<lbrakk>valid_chain_list l; boundary_chain (set l); \<forall>a\<in>set l. case a of (k, a) \<Rightarrow> line_integral_exists F basis a; \<forall>a\<in>set l. case a of (k, a) \<Rightarrow> valid_path a\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join l) = (\<Sum>a\<leftarrow>l. case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>)
valid_chain_list (a # l)
boundary_chain (set (a # l))
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> line_integral_exists F basis a
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> valid_path a

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>\<lbrakk>valid_chain_list l; boundary_chain (set l); \<forall>(k, y)\<in>set l. line_integral_exists F basis y; \<forall>(k, y)\<in>set l. valid_path y\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join l) = (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>); valid_chain_list (a # l); boundary_chain (set (a # l)); \<forall>(k, y)\<in>set (a # l). line_integral_exists F basis y; \<forall>(k, y)\<in>set (a # l). valid_path y\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join (a # l)) = (\<Sum>(x, \<gamma>)\<leftarrow>a # l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
obtain k::"int" and
      \<gamma>::"one_cube" where props: "a = (k,\<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k \<gamma>. a = (k, \<gamma>) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>k \<gamma>. a = (k, \<gamma>) \<Longrightarrow> thesis) \<Longrightarrow> a = (?k2, ?\<gamma>2)
[PROOF STEP]
let ?k2 = "fst a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>k \<gamma>. a = (k, \<gamma>) \<Longrightarrow> thesis) \<Longrightarrow> a = (?k2, ?\<gamma>2)
[PROOF STEP]
let ?\<gamma>2 = "snd a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>k \<gamma>. a = (k, \<gamma>) \<Longrightarrow> thesis) \<Longrightarrow> a = (?k2, ?\<gamma>2)
[PROOF STEP]
show "a = (?k2, ?\<gamma>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = (fst a, snd a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = (fst a, snd a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
a = (k, \<gamma>)

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>\<lbrakk>valid_chain_list l; boundary_chain (set l); \<forall>(k, y)\<in>set l. line_integral_exists F basis y; \<forall>(k, y)\<in>set l. valid_path y\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join l) = (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>); valid_chain_list (a # l); boundary_chain (set (a # l)); \<forall>(k, y)\<in>set (a # l). line_integral_exists F basis y; \<forall>(k, y)\<in>set (a # l). valid_path y\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join (a # l)) = (\<Sum>(x, \<gamma>)\<leftarrow>a # l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
have "line_integral_exists F basis (rec_join (a # l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis (rec_join (a # l))
[PROOF STEP]
using line_integral_exists_on_rec_join[OF ass(3) ass(2)] ass(5) ass(4)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>k \<gamma>. (k, \<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path \<gamma>; \<forall>(k, \<gamma>)\<in>set (a # l). line_integral_exists ?F ?basis \<gamma>\<rbrakk> \<Longrightarrow> line_integral_exists ?F ?basis (rec_join (a # l))
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> valid_path a
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> line_integral_exists F basis a

goal (1 subgoal):
 1. line_integral_exists F basis (rec_join (a # l))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
line_integral_exists F basis (rec_join (a # l))

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>\<lbrakk>valid_chain_list l; boundary_chain (set l); \<forall>(k, y)\<in>set l. line_integral_exists F basis y; \<forall>(k, y)\<in>set l. valid_path y\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join l) = (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>); valid_chain_list (a # l); boundary_chain (set (a # l)); \<forall>(k, y)\<in>set (a # l). line_integral_exists F basis y; \<forall>(k, y)\<in>set (a # l). valid_path y\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join (a # l)) = (\<Sum>(x, \<gamma>)\<leftarrow>a # l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
have "boundary_chain (set l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. boundary_chain (set l)
[PROOF STEP]
by (meson ass.prems(2) boundary_chain_def list.set_intros(2))
[PROOF STATE]
proof (state)
this:
boundary_chain (set l)

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>\<lbrakk>valid_chain_list l; boundary_chain (set l); \<forall>(k, y)\<in>set l. line_integral_exists F basis y; \<forall>(k, y)\<in>set l. valid_path y\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join l) = (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>); valid_chain_list (a # l); boundary_chain (set (a # l)); \<forall>(k, y)\<in>set (a # l). line_integral_exists F basis y; \<forall>(k, y)\<in>set (a # l). valid_path y\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join (a # l)) = (\<Sum>(x, \<gamma>)\<leftarrow>a # l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
have val_l: "\<And>f i. (i,f) \<in> set l \<Longrightarrow> valid_path f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f i. (i, f) \<in> set l \<Longrightarrow> valid_path f
[PROOF STEP]
using ass.prems(4)
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> valid_path a

goal (1 subgoal):
 1. \<And>f i. (i, f) \<in> set l \<Longrightarrow> valid_path f
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(?i, ?f) \<in> set l \<Longrightarrow> valid_path ?f

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>\<lbrakk>valid_chain_list l; boundary_chain (set l); \<forall>(k, y)\<in>set l. line_integral_exists F basis y; \<forall>(k, y)\<in>set l. valid_path y\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join l) = (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>); valid_chain_list (a # l); boundary_chain (set (a # l)); \<forall>(k, y)\<in>set (a # l). line_integral_exists F basis y; \<forall>(k, y)\<in>set (a # l). valid_path y\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join (a # l)) = (\<Sum>(x, \<gamma>)\<leftarrow>a # l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
have vcl_l: "valid_chain_list l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_chain_list l
[PROOF STEP]
by (metis (no_types) ass.prems(1) valid_chain_list.elims(3) valid_chain_list.simps(3))
[PROOF STATE]
proof (state)
this:
valid_chain_list l

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>\<lbrakk>valid_chain_list l; boundary_chain (set l); \<forall>(k, y)\<in>set l. line_integral_exists F basis y; \<forall>(k, y)\<in>set l. valid_path y\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join l) = (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>); valid_chain_list (a # l); boundary_chain (set (a # l)); \<forall>(k, y)\<in>set (a # l). line_integral_exists F basis y; \<forall>(k, y)\<in>set (a # l). valid_path y\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join (a # l)) = (\<Sum>(x, \<gamma>)\<leftarrow>a # l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
have line_integral_exists_on_joined:
      "line_integral_exists F basis (rec_join l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis (rec_join l)
[PROOF STEP]
by (metis \<open>boundary_chain (set l)\<close> \<open>line_integral_exists F basis (rec_join (a # l))\<close> emptyE val_l vcl_l joined_is_valid line_integral_exists_joinD2 line_integral_exists_on_rec_join list.set(1) neq_Nil_conv rec_join.simps(3))
[PROOF STATE]
proof (state)
this:
line_integral_exists F basis (rec_join l)

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>\<lbrakk>valid_chain_list l; boundary_chain (set l); \<forall>(k, y)\<in>set l. line_integral_exists F basis y; \<forall>(k, y)\<in>set l. valid_path y\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join l) = (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>); valid_chain_list (a # l); boundary_chain (set (a # l)); \<forall>(k, y)\<in>set (a # l). line_integral_exists F basis y; \<forall>(k, y)\<in>set (a # l). valid_path y\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join (a # l)) = (\<Sum>(x, \<gamma>)\<leftarrow>a # l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
have "valid_path (rec_join (a # l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path (rec_join (a # l))
[PROOF STEP]
using joined_is_valid ass(5) ass(3) ass(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>boundary_chain (set ?l); \<And>k \<gamma>. (k, \<gamma>) \<in> set ?l \<Longrightarrow> valid_path \<gamma>; valid_chain_list ?l\<rbrakk> \<Longrightarrow> valid_path (rec_join ?l)
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> valid_path a
boundary_chain (set (a # l))
valid_chain_list (a # l)

goal (1 subgoal):
 1. valid_path (rec_join (a # l))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
valid_path (rec_join (a # l))

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>\<lbrakk>valid_chain_list l; boundary_chain (set l); \<forall>(k, y)\<in>set l. line_integral_exists F basis y; \<forall>(k, y)\<in>set l. valid_path y\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join l) = (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>); valid_chain_list (a # l); boundary_chain (set (a # l)); \<forall>(k, y)\<in>set (a # l). line_integral_exists F basis y; \<forall>(k, y)\<in>set (a # l). valid_path y\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join (a # l)) = (\<Sum>(x, \<gamma>)\<leftarrow>a # l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
valid_path (rec_join (a # l))
[PROOF STEP]
have joined_is_valid: "valid_path (rec_join l)"
[PROOF STATE]
proof (prove)
using this:
valid_path (rec_join (a # l))

goal (1 subgoal):
 1. valid_path (rec_join l)
[PROOF STEP]
using \<open>boundary_chain (set l)\<close> val_l vcl_l joined_is_valid
[PROOF STATE]
proof (prove)
using this:
valid_path (rec_join (a # l))
boundary_chain (set l)
(?i, ?f) \<in> set l \<Longrightarrow> valid_path ?f
valid_chain_list l
\<lbrakk>boundary_chain (set ?l); \<And>k \<gamma>. (k, \<gamma>) \<in> set ?l \<Longrightarrow> valid_path \<gamma>; valid_chain_list ?l\<rbrakk> \<Longrightarrow> valid_path (rec_join ?l)

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

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>\<lbrakk>valid_chain_list l; boundary_chain (set l); \<forall>(k, y)\<in>set l. line_integral_exists F basis y; \<forall>(k, y)\<in>set l. valid_path y\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join l) = (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>); valid_chain_list (a # l); boundary_chain (set (a # l)); \<forall>(k, y)\<in>set (a # l). line_integral_exists F basis y; \<forall>(k, y)\<in>set (a # l). valid_path y\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join (a # l)) = (\<Sum>(x, \<gamma>)\<leftarrow>a # l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis (rec_join (a # l)) = (\<Sum>a\<leftarrow>a # l. case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
proof (clarsimp, cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> line_integral F basis (rec_join (a # l)) = (case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>) + (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)
 2. \<not> ?P \<Longrightarrow> line_integral F basis (rec_join (a # l)) = (case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>) + (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
assume k_eq_1: "(k::int) = 1"
[PROOF STATE]
proof (state)
this:
k = 1

goal (2 subgoals):
 1. ?P \<Longrightarrow> line_integral F basis (rec_join (a # l)) = (case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>) + (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)
 2. \<not> ?P \<Longrightarrow> line_integral F basis (rec_join (a # l)) = (case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>) + (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
have line_integral_exists_on_gamma: "line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis \<gamma>
[PROOF STEP]
using ass props
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>valid_chain_list l; boundary_chain (set l); \<forall>a\<in>set l. case a of (k, a) \<Rightarrow> line_integral_exists F basis a; \<forall>a\<in>set l. case a of (k, a) \<Rightarrow> valid_path a\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join l) = (\<Sum>a\<leftarrow>l. case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>)
valid_chain_list (a # l)
boundary_chain (set (a # l))
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> line_integral_exists F basis a
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> valid_path a
a = (k, \<gamma>)

goal (1 subgoal):
 1. line_integral_exists F basis \<gamma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
line_integral_exists F basis \<gamma>

goal (2 subgoals):
 1. ?P \<Longrightarrow> line_integral F basis (rec_join (a # l)) = (case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>) + (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)
 2. \<not> ?P \<Longrightarrow> line_integral F basis (rec_join (a # l)) = (case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>) + (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
have gamma_is_valid: "valid_path \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path \<gamma>
[PROOF STEP]
using ass props
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>valid_chain_list l; boundary_chain (set l); \<forall>a\<in>set l. case a of (k, a) \<Rightarrow> line_integral_exists F basis a; \<forall>a\<in>set l. case a of (k, a) \<Rightarrow> valid_path a\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join l) = (\<Sum>a\<leftarrow>l. case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>)
valid_chain_list (a # l)
boundary_chain (set (a # l))
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> line_integral_exists F basis a
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> valid_path a
a = (k, \<gamma>)

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> line_integral F basis (rec_join (a # l)) = (case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>) + (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)
 2. \<not> ?P \<Longrightarrow> line_integral F basis (rec_join (a # l)) = (case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>) + (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
have line_int_rw: "line_integral F basis (rec_join ((k, \<gamma>) # l)) = line_integral F basis (\<gamma> +++ rec_join l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis (rec_join ((k, \<gamma>) # l)) = line_integral F basis (\<gamma> +++ rec_join l)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. line_integral F basis (rec_join ((k, \<gamma>) # l)) = line_integral F basis (\<gamma> +++ rec_join l)
[PROOF STEP]
have gam_int: "line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis \<gamma>
[PROOF STEP]
using ass props
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>valid_chain_list l; boundary_chain (set l); \<forall>a\<in>set l. case a of (k, a) \<Rightarrow> line_integral_exists F basis a; \<forall>a\<in>set l. case a of (k, a) \<Rightarrow> valid_path a\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join l) = (\<Sum>a\<leftarrow>l. case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>)
valid_chain_list (a # l)
boundary_chain (set (a # l))
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> line_integral_exists F basis a
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> valid_path a
a = (k, \<gamma>)

goal (1 subgoal):
 1. line_integral_exists F basis \<gamma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
line_integral_exists F basis \<gamma>

goal (1 subgoal):
 1. line_integral F basis (rec_join ((k, \<gamma>) # l)) = line_integral F basis (\<gamma> +++ rec_join l)
[PROOF STEP]
have rec_join_int: "line_integral_exists F basis (rec_join l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis (rec_join l)
[PROOF STEP]
using line_integral_exists_on_rec_join
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>boundary_chain (set ?l); valid_chain_list ?l; \<And>k \<gamma>. (k, \<gamma>) \<in> set ?l \<Longrightarrow> valid_path \<gamma>; \<forall>(k, \<gamma>)\<in>set ?l. line_integral_exists ?F ?basis \<gamma>\<rbrakk> \<Longrightarrow> line_integral_exists ?F ?basis (rec_join ?l)

goal (1 subgoal):
 1. line_integral_exists F basis (rec_join l)
[PROOF STEP]
using line_integral_exists_on_joined
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>boundary_chain (set ?l); valid_chain_list ?l; \<And>k \<gamma>. (k, \<gamma>) \<in> set ?l \<Longrightarrow> valid_path \<gamma>; \<forall>(k, \<gamma>)\<in>set ?l. line_integral_exists ?F ?basis \<gamma>\<rbrakk> \<Longrightarrow> line_integral_exists ?F ?basis (rec_join ?l)
line_integral_exists F basis (rec_join l)

goal (1 subgoal):
 1. line_integral_exists F basis (rec_join l)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
line_integral_exists F basis (rec_join l)

goal (1 subgoal):
 1. line_integral F basis (rec_join ((k, \<gamma>) # l)) = line_integral F basis (\<gamma> +++ rec_join l)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis (rec_join ((k, \<gamma>) # l)) = line_integral F basis (\<gamma> +++ rec_join l)
[PROOF STEP]
using line_integral_rec_join_cons[OF gam_int rec_join_int] ass k_eq_1 finite_basis props
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>k' \<gamma>'. (k', \<gamma>') \<in> set ((1, \<gamma>) # l) \<Longrightarrow> valid_path \<gamma>'; finite basis\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join ((1, \<gamma>) # l)) = line_integral F basis (\<gamma> +++ rec_join l)
\<lbrakk>valid_chain_list l; boundary_chain (set l); \<forall>a\<in>set l. case a of (k, a) \<Rightarrow> line_integral_exists F basis a; \<forall>a\<in>set l. case a of (k, a) \<Rightarrow> valid_path a\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join l) = (\<Sum>a\<leftarrow>l. case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>)
valid_chain_list (a # l)
boundary_chain (set (a # l))
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> line_integral_exists F basis a
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> valid_path a
k = 1
finite basis
a = (k, \<gamma>)

goal (1 subgoal):
 1. line_integral F basis (rec_join ((k, \<gamma>) # l)) = line_integral F basis (\<gamma> +++ rec_join l)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
line_integral F basis (rec_join ((k, \<gamma>) # l)) = line_integral F basis (\<gamma> +++ rec_join l)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
line_integral F basis (rec_join ((k, \<gamma>) # l)) = line_integral F basis (\<gamma> +++ rec_join l)

goal (2 subgoals):
 1. ?P \<Longrightarrow> line_integral F basis (rec_join (a # l)) = (case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>) + (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)
 2. \<not> ?P \<Longrightarrow> line_integral F basis (rec_join (a # l)) = (case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>) + (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
show "line_integral F basis (rec_join (a # l)) =
            (case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>) + (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis (rec_join (a # l)) = (case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>) + (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
apply (simp add: props line_int_rw)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis (\<gamma> +++ rec_join l) = real_of_int k * line_integral F basis \<gamma> + (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
using line_integral_distrib[OF line_integral_exists_on_gamma line_integral_exists_on_joined gamma_is_valid joined_is_valid]
          ass k_eq_1 vcl_l
[PROOF STATE]
proof (prove)
using this:
line_integral F basis (\<gamma> +++ rec_join l) = line_integral F basis \<gamma> + line_integral F basis (rec_join l)
line_integral_exists F basis (\<gamma> +++ rec_join l)
\<lbrakk>valid_chain_list l; boundary_chain (set l); \<forall>a\<in>set l. case a of (k, a) \<Rightarrow> line_integral_exists F basis a; \<forall>a\<in>set l. case a of (k, a) \<Rightarrow> valid_path a\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join l) = (\<Sum>a\<leftarrow>l. case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>)
valid_chain_list (a # l)
boundary_chain (set (a # l))
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> line_integral_exists F basis a
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> valid_path a
k = 1
valid_chain_list l

goal (1 subgoal):
 1. line_integral F basis (\<gamma> +++ rec_join l) = real_of_int k * line_integral F basis \<gamma> + (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
by (auto simp: boundary_chain_def props)
[PROOF STATE]
proof (state)
this:
line_integral F basis (rec_join (a # l)) = (case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>) + (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> line_integral F basis (rec_join (a # l)) = (case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>) + (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> line_integral F basis (rec_join (a # l)) = (case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>) + (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
assume "k \<noteq> 1"
[PROOF STATE]
proof (state)
this:
k \<noteq> 1

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> line_integral F basis (rec_join (a # l)) = (case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>) + (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k \<noteq> 1
[PROOF STEP]
have k_eq_neg_1: "k = -1"
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 1

goal (1 subgoal):
 1. k = - 1
[PROOF STEP]
using ass props
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 1
\<lbrakk>valid_chain_list l; boundary_chain (set l); \<forall>a\<in>set l. case a of (k, a) \<Rightarrow> line_integral_exists F basis a; \<forall>a\<in>set l. case a of (k, a) \<Rightarrow> valid_path a\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join l) = (\<Sum>a\<leftarrow>l. case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>)
valid_chain_list (a # l)
boundary_chain (set (a # l))
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> line_integral_exists F basis a
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> valid_path a
a = (k, \<gamma>)

goal (1 subgoal):
 1. k = - 1
[PROOF STEP]
by (auto simp add: boundary_chain_def)
[PROOF STATE]
proof (state)
this:
k = - 1

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> line_integral F basis (rec_join (a # l)) = (case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>) + (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
have line_integral_exists_on_gamma:
        "line_integral_exists F basis (reversepath \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis (reversepath \<gamma>)
[PROOF STEP]
using line_integral_on_reverse_path ass props
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>valid_path ?\<gamma>; line_integral_exists ?F ?basis ?\<gamma>\<rbrakk> \<Longrightarrow> line_integral ?F ?basis ?\<gamma> = - line_integral ?F ?basis (reversepath ?\<gamma>)
\<lbrakk>valid_path ?\<gamma>; line_integral_exists ?F ?basis ?\<gamma>\<rbrakk> \<Longrightarrow> line_integral_exists ?F ?basis (reversepath ?\<gamma>)
\<lbrakk>valid_chain_list l; boundary_chain (set l); \<forall>a\<in>set l. case a of (k, a) \<Rightarrow> line_integral_exists F basis a; \<forall>a\<in>set l. case a of (k, a) \<Rightarrow> valid_path a\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join l) = (\<Sum>a\<leftarrow>l. case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>)
valid_chain_list (a # l)
boundary_chain (set (a # l))
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> line_integral_exists F basis a
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> valid_path a
a = (k, \<gamma>)

goal (1 subgoal):
 1. line_integral_exists F basis (reversepath \<gamma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
line_integral_exists F basis (reversepath \<gamma>)

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> line_integral F basis (rec_join (a # l)) = (case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>) + (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
have gamma_is_valid: "valid_path (reversepath \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path (reversepath \<gamma>)
[PROOF STEP]
using valid_path_imp_reverse ass props
[PROOF STATE]
proof (prove)
using this:
valid_path ?g \<Longrightarrow> valid_path (reversepath ?g)
\<lbrakk>valid_chain_list l; boundary_chain (set l); \<forall>a\<in>set l. case a of (k, a) \<Rightarrow> line_integral_exists F basis a; \<forall>a\<in>set l. case a of (k, a) \<Rightarrow> valid_path a\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join l) = (\<Sum>a\<leftarrow>l. case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>)
valid_chain_list (a # l)
boundary_chain (set (a # l))
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> line_integral_exists F basis a
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> valid_path a
a = (k, \<gamma>)

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

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> line_integral F basis (rec_join (a # l)) = (case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>) + (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
have line_int_rw: "line_integral F basis (rec_join ((k, \<gamma>) # l)) = line_integral F basis ((reversepath \<gamma>) +++ rec_join l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis (rec_join ((k, \<gamma>) # l)) = line_integral F basis (reversepath \<gamma> +++ rec_join l)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. line_integral F basis (rec_join ((k, \<gamma>) # l)) = line_integral F basis (reversepath \<gamma> +++ rec_join l)
[PROOF STEP]
have gam_int: "line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis \<gamma>
[PROOF STEP]
using ass props
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>valid_chain_list l; boundary_chain (set l); \<forall>a\<in>set l. case a of (k, a) \<Rightarrow> line_integral_exists F basis a; \<forall>a\<in>set l. case a of (k, a) \<Rightarrow> valid_path a\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join l) = (\<Sum>a\<leftarrow>l. case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>)
valid_chain_list (a # l)
boundary_chain (set (a # l))
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> line_integral_exists F basis a
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> valid_path a
a = (k, \<gamma>)

goal (1 subgoal):
 1. line_integral_exists F basis \<gamma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
line_integral_exists F basis \<gamma>

goal (1 subgoal):
 1. line_integral F basis (rec_join ((k, \<gamma>) # l)) = line_integral F basis (reversepath \<gamma> +++ rec_join l)
[PROOF STEP]
have rec_join_int: "line_integral_exists F basis (rec_join l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis (rec_join l)
[PROOF STEP]
using line_integral_exists_on_rec_join
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>boundary_chain (set ?l); valid_chain_list ?l; \<And>k \<gamma>. (k, \<gamma>) \<in> set ?l \<Longrightarrow> valid_path \<gamma>; \<forall>(k, \<gamma>)\<in>set ?l. line_integral_exists ?F ?basis \<gamma>\<rbrakk> \<Longrightarrow> line_integral_exists ?F ?basis (rec_join ?l)

goal (1 subgoal):
 1. line_integral_exists F basis (rec_join l)
[PROOF STEP]
using line_integral_exists_on_joined
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>boundary_chain (set ?l); valid_chain_list ?l; \<And>k \<gamma>. (k, \<gamma>) \<in> set ?l \<Longrightarrow> valid_path \<gamma>; \<forall>(k, \<gamma>)\<in>set ?l. line_integral_exists ?F ?basis \<gamma>\<rbrakk> \<Longrightarrow> line_integral_exists ?F ?basis (rec_join ?l)
line_integral_exists F basis (rec_join l)

goal (1 subgoal):
 1. line_integral_exists F basis (rec_join l)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
line_integral_exists F basis (rec_join l)

goal (1 subgoal):
 1. line_integral F basis (rec_join ((k, \<gamma>) # l)) = line_integral F basis (reversepath \<gamma> +++ rec_join l)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis (rec_join ((k, \<gamma>) # l)) = line_integral F basis (reversepath \<gamma> +++ rec_join l)
[PROOF STEP]
using line_integral_rec_join_cons_2[OF gam_int rec_join_int]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>k' \<gamma>'. (k', \<gamma>') \<in> set ((- 1, \<gamma>) # l) \<Longrightarrow> valid_path \<gamma>'; finite basis\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join ((- 1, \<gamma>) # l)) = line_integral F basis (reversepath \<gamma> +++ rec_join l)

goal (1 subgoal):
 1. line_integral F basis (rec_join ((k, \<gamma>) # l)) = line_integral F basis (reversepath \<gamma> +++ rec_join l)
[PROOF STEP]
using ass k_eq_neg_1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>k' \<gamma>'. (k', \<gamma>') \<in> set ((- 1, \<gamma>) # l) \<Longrightarrow> valid_path \<gamma>'; finite basis\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join ((- 1, \<gamma>) # l)) = line_integral F basis (reversepath \<gamma> +++ rec_join l)
\<lbrakk>valid_chain_list l; boundary_chain (set l); \<forall>a\<in>set l. case a of (k, a) \<Rightarrow> line_integral_exists F basis a; \<forall>a\<in>set l. case a of (k, a) \<Rightarrow> valid_path a\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join l) = (\<Sum>a\<leftarrow>l. case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>)
valid_chain_list (a # l)
boundary_chain (set (a # l))
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> line_integral_exists F basis a
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> valid_path a
k = - 1

goal (1 subgoal):
 1. line_integral F basis (rec_join ((k, \<gamma>) # l)) = line_integral F basis (reversepath \<gamma> +++ rec_join l)
[PROOF STEP]
using finite_basis props
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>k' \<gamma>'. (k', \<gamma>') \<in> set ((- 1, \<gamma>) # l) \<Longrightarrow> valid_path \<gamma>'; finite basis\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join ((- 1, \<gamma>) # l)) = line_integral F basis (reversepath \<gamma> +++ rec_join l)
\<lbrakk>valid_chain_list l; boundary_chain (set l); \<forall>a\<in>set l. case a of (k, a) \<Rightarrow> line_integral_exists F basis a; \<forall>a\<in>set l. case a of (k, a) \<Rightarrow> valid_path a\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join l) = (\<Sum>a\<leftarrow>l. case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>)
valid_chain_list (a # l)
boundary_chain (set (a # l))
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> line_integral_exists F basis a
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> valid_path a
k = - 1
finite basis
a = (k, \<gamma>)

goal (1 subgoal):
 1. line_integral F basis (rec_join ((k, \<gamma>) # l)) = line_integral F basis (reversepath \<gamma> +++ rec_join l)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
line_integral F basis (rec_join ((k, \<gamma>) # l)) = line_integral F basis (reversepath \<gamma> +++ rec_join l)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
line_integral F basis (rec_join ((k, \<gamma>) # l)) = line_integral F basis (reversepath \<gamma> +++ rec_join l)

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> line_integral F basis (rec_join (a # l)) = (case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>) + (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
show "line_integral F basis (rec_join (a # l)) =
            (case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>) + (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis (rec_join (a # l)) = (case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>) + (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
apply (simp add: props line_int_rw)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis (reversepath \<gamma> +++ rec_join l) = real_of_int k * line_integral F basis \<gamma> + (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
using line_integral_distrib[OF line_integral_exists_on_gamma line_integral_exists_on_joined gamma_is_valid joined_is_valid]
          props ass line_integral_on_reverse_path(1)[of "\<gamma>" "F" "basis"] k_eq_neg_1
[PROOF STATE]
proof (prove)
using this:
line_integral F basis (reversepath \<gamma> +++ rec_join l) = line_integral F basis (reversepath \<gamma>) + line_integral F basis (rec_join l)
line_integral_exists F basis (reversepath \<gamma> +++ rec_join l)
a = (k, \<gamma>)
\<lbrakk>valid_chain_list l; boundary_chain (set l); \<forall>a\<in>set l. case a of (k, a) \<Rightarrow> line_integral_exists F basis a; \<forall>a\<in>set l. case a of (k, a) \<Rightarrow> valid_path a\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join l) = (\<Sum>a\<leftarrow>l. case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>)
valid_chain_list (a # l)
boundary_chain (set (a # l))
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> line_integral_exists F basis a
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> valid_path a
\<lbrakk>valid_path \<gamma>; line_integral_exists F basis \<gamma>\<rbrakk> \<Longrightarrow> line_integral F basis \<gamma> = - line_integral F basis (reversepath \<gamma>)
k = - 1

goal (1 subgoal):
 1. line_integral F basis (reversepath \<gamma> +++ rec_join l) = real_of_int k * line_integral F basis \<gamma> + (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
using \<open>boundary_chain (set l)\<close> vcl_l
[PROOF STATE]
proof (prove)
using this:
line_integral F basis (reversepath \<gamma> +++ rec_join l) = line_integral F basis (reversepath \<gamma>) + line_integral F basis (rec_join l)
line_integral_exists F basis (reversepath \<gamma> +++ rec_join l)
a = (k, \<gamma>)
\<lbrakk>valid_chain_list l; boundary_chain (set l); \<forall>a\<in>set l. case a of (k, a) \<Rightarrow> line_integral_exists F basis a; \<forall>a\<in>set l. case a of (k, a) \<Rightarrow> valid_path a\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join l) = (\<Sum>a\<leftarrow>l. case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>)
valid_chain_list (a # l)
boundary_chain (set (a # l))
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> line_integral_exists F basis a
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> valid_path a
\<lbrakk>valid_path \<gamma>; line_integral_exists F basis \<gamma>\<rbrakk> \<Longrightarrow> line_integral F basis \<gamma> = - line_integral F basis (reversepath \<gamma>)
k = - 1
boundary_chain (set l)
valid_chain_list l

goal (1 subgoal):
 1. line_integral F basis (reversepath \<gamma> +++ rec_join l) = real_of_int k * line_integral F basis \<gamma> + (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
line_integral F basis (rec_join (a # l)) = (case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>) + (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
line_integral F basis (rec_join (a # l)) = (\<Sum>a\<leftarrow>a # l. case a of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>valid_chain_list l; boundary_chain (set l); \<forall>(k, \<gamma>)\<in>set l. line_integral_exists F basis \<gamma>; \<forall>(k, \<gamma>)\<in>set l. valid_path \<gamma>\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join l) = (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)

goal (1 subgoal):
 1. line_integral F basis (rec_join l) = one_chain_line_integral F basis one_chain
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>valid_chain_list l; boundary_chain (set l); \<forall>(k, \<gamma>)\<in>set l. line_integral_exists F basis \<gamma>; \<forall>(k, \<gamma>)\<in>set l. valid_path \<gamma>\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join l) = (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
have 1:"line_integral F basis (rec_join l) = sum_list (map (\<lambda>(k::int, \<gamma>). k * (line_integral F basis \<gamma>)) l)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>valid_chain_list l; boundary_chain (set l); \<forall>(k, \<gamma>)\<in>set l. line_integral_exists F basis \<gamma>; \<forall>(k, \<gamma>)\<in>set l. valid_path \<gamma>\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join l) = (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)

goal (1 subgoal):
 1. line_integral F basis (rec_join l) = (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
using l_props assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>valid_chain_list l; boundary_chain (set l); \<forall>(k, \<gamma>)\<in>set l. line_integral_exists F basis \<gamma>; \<forall>(k, \<gamma>)\<in>set l. valid_path \<gamma>\<rbrakk> \<Longrightarrow> line_integral F basis (rec_join l) = (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)
set l = one_chain
distinct l
valid_chain_list l
set l = one_chain
distinct l
valid_chain_list l
boundary_chain one_chain
\<forall>(k, \<gamma>)\<in>one_chain. line_integral_exists F basis \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain. valid_path \<gamma>
finite basis

goal (1 subgoal):
 1. line_integral F basis (rec_join l) = (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
line_integral F basis (rec_join l) = (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)

goal (1 subgoal):
 1. line_integral F basis (rec_join l) = one_chain_line_integral F basis one_chain
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
line_integral F basis (rec_join l) = (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
line_integral F basis (rec_join l) = (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)

goal (1 subgoal):
 1. line_integral F basis (rec_join l) = one_chain_line_integral F basis one_chain
[PROOF STEP]
using 0 1
[PROOF STATE]
proof (prove)
using this:
line_integral F basis (rec_join l) = (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)
(\<Sum>(k, \<gamma>)\<leftarrow>l. real_of_int k * line_integral F basis \<gamma>) = one_chain_line_integral F basis one_chain
line_integral F basis (rec_join l) = (\<Sum>(x, \<gamma>)\<leftarrow>l. real_of_int x * line_integral F basis \<gamma>)

goal (1 subgoal):
 1. line_integral F basis (rec_join l) = one_chain_line_integral F basis one_chain
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
line_integral F basis (rec_join l) = one_chain_line_integral F basis one_chain

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma line_integral_on_path_eq_line_integral_on_equiv_chain:
  assumes path_eq_chain: "chain_subdiv_path \<gamma> one_chain" and
    boundary_chain: "boundary_chain one_chain" and
    line_integral_exists: "\<forall>(k::int, \<gamma>) \<in> one_chain. line_integral_exists F basis \<gamma>" and
    valid_path: "\<forall>(k::int, \<gamma>) \<in> one_chain. valid_path \<gamma>" and
    finite_basis: "finite basis"
  shows "one_chain_line_integral F basis one_chain = line_integral F basis \<gamma>"
    "line_integral_exists F basis \<gamma>"
    "valid_path \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain = line_integral F basis \<gamma> &&& line_integral_exists F basis \<gamma> &&& valid_path \<gamma>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. one_chain_line_integral F basis one_chain = line_integral F basis \<gamma>
 2. line_integral_exists F basis \<gamma>
 3. valid_path \<gamma>
[PROOF STEP]
obtain l where l_props: "set l = one_chain" "distinct l" "rec_join l = \<gamma>" "valid_chain_list l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l. \<lbrakk>set l = one_chain; distinct l; rec_join l = \<gamma>; valid_chain_list l\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using chain_subdiv_path.cases path_eq_chain
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>chain_subdiv_path ?a1.0 ?a2.0; \<And>l \<gamma>. \<lbrakk>?a1.0 = \<gamma>; ?a2.0 = set l; distinct l; rec_join l = \<gamma>; valid_chain_list l\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
chain_subdiv_path \<gamma> one_chain

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>set l = one_chain; distinct l; rec_join l = \<gamma>; valid_chain_list l\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
set l = one_chain
distinct l
rec_join l = \<gamma>
valid_chain_list l

goal (3 subgoals):
 1. one_chain_line_integral F basis one_chain = line_integral F basis \<gamma>
 2. line_integral_exists F basis \<gamma>
 3. valid_path \<gamma>
[PROOF STEP]
show "line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis \<gamma>
[PROOF STEP]
using line_integral_exists_on_rec_join assms l_props
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>boundary_chain (set ?l); valid_chain_list ?l; \<And>k \<gamma>. (k, \<gamma>) \<in> set ?l \<Longrightarrow> valid_path \<gamma>; \<forall>(k, \<gamma>)\<in>set ?l. line_integral_exists ?F ?basis \<gamma>\<rbrakk> \<Longrightarrow> line_integral_exists ?F ?basis (rec_join ?l)
chain_subdiv_path \<gamma> one_chain
boundary_chain one_chain
\<forall>(k, \<gamma>)\<in>one_chain. line_integral_exists F basis \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain. valid_path \<gamma>
finite basis
set l = one_chain
distinct l
rec_join l = \<gamma>
valid_chain_list l

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

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain = line_integral F basis \<gamma>
 2. valid_path \<gamma>
[PROOF STEP]
show "valid_path \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path \<gamma>
[PROOF STEP]
using joined_is_valid assms l_props
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>boundary_chain (set ?l); \<And>k \<gamma>. (k, \<gamma>) \<in> set ?l \<Longrightarrow> valid_path \<gamma>; valid_chain_list ?l\<rbrakk> \<Longrightarrow> valid_path (rec_join ?l)
chain_subdiv_path \<gamma> one_chain
boundary_chain one_chain
\<forall>(k, \<gamma>)\<in>one_chain. line_integral_exists F basis \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain. valid_path \<gamma>
finite basis
set l = one_chain
distinct l
rec_join l = \<gamma>
valid_chain_list l

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

goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain = line_integral F basis \<gamma>
[PROOF STEP]
have "line_integral F basis (rec_join l) = one_chain_line_integral F basis one_chain"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis (rec_join l) = one_chain_line_integral F basis one_chain
[PROOF STEP]
using one_chain_line_integral_rec_join l_props assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set ?l = ?one_chain; distinct ?l; valid_chain_list ?l; boundary_chain ?one_chain; \<forall>(k, \<gamma>)\<in>?one_chain. line_integral_exists ?F ?basis \<gamma>; \<forall>(k, \<gamma>)\<in>?one_chain. valid_path \<gamma>; finite ?basis\<rbrakk> \<Longrightarrow> line_integral ?F ?basis (rec_join ?l) = one_chain_line_integral ?F ?basis ?one_chain
set l = one_chain
distinct l
rec_join l = \<gamma>
valid_chain_list l
chain_subdiv_path \<gamma> one_chain
boundary_chain one_chain
\<forall>(k, \<gamma>)\<in>one_chain. line_integral_exists F basis \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain. valid_path \<gamma>
finite basis

goal (1 subgoal):
 1. line_integral F basis (rec_join l) = one_chain_line_integral F basis one_chain
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
line_integral F basis (rec_join l) = one_chain_line_integral F basis one_chain

goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain = line_integral F basis \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
line_integral F basis (rec_join l) = one_chain_line_integral F basis one_chain
[PROOF STEP]
show "one_chain_line_integral F basis one_chain = line_integral F basis \<gamma>"
[PROOF STATE]
proof (prove)
using this:
line_integral F basis (rec_join l) = one_chain_line_integral F basis one_chain

goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain = line_integral F basis \<gamma>
[PROOF STEP]
using l_props
[PROOF STATE]
proof (prove)
using this:
line_integral F basis (rec_join l) = one_chain_line_integral F basis one_chain
set l = one_chain
distinct l
rec_join l = \<gamma>
valid_chain_list l

goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain = line_integral F basis \<gamma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
one_chain_line_integral F basis one_chain = line_integral F basis \<gamma>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma line_integral_on_path_eq_line_integral_on_equiv_chain':
  assumes path_eq_chain: "chain_subdiv_path \<gamma> one_chain" and
    boundary_chain: "boundary_chain one_chain" and
    line_integral_exists: "line_integral_exists F basis \<gamma>" and
    valid_path: "\<forall>(k, \<gamma>) \<in> one_chain. valid_path \<gamma>" and
    finite_basis: "finite basis"
  shows "one_chain_line_integral F basis one_chain = line_integral F basis \<gamma>"
    "\<forall>(k, \<gamma>) \<in> one_chain. line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain = line_integral F basis \<gamma> &&& \<forall>(k, \<gamma>)\<in>one_chain. line_integral_exists F basis \<gamma>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain = line_integral F basis \<gamma>
 2. \<forall>(k, \<gamma>)\<in>one_chain. line_integral_exists F basis \<gamma>
[PROOF STEP]
obtain l where l_props: "set l = one_chain" "distinct l" "rec_join l = \<gamma>" "valid_chain_list l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l. \<lbrakk>set l = one_chain; distinct l; rec_join l = \<gamma>; valid_chain_list l\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using chain_subdiv_path.cases path_eq_chain
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>chain_subdiv_path ?a1.0 ?a2.0; \<And>l \<gamma>. \<lbrakk>?a1.0 = \<gamma>; ?a2.0 = set l; distinct l; rec_join l = \<gamma>; valid_chain_list l\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
chain_subdiv_path \<gamma> one_chain

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>set l = one_chain; distinct l; rec_join l = \<gamma>; valid_chain_list l\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
set l = one_chain
distinct l
rec_join l = \<gamma>
valid_chain_list l

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain = line_integral F basis \<gamma>
 2. \<forall>(k, \<gamma>)\<in>one_chain. line_integral_exists F basis \<gamma>
[PROOF STEP]
show 0: "\<forall>(k, \<gamma>) \<in> one_chain. line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain. line_integral_exists F basis \<gamma>
[PROOF STEP]
using line_integral_exists_on_rec_join' assms l_props
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>boundary_chain (set ?l); valid_chain_list ?l; \<And>k \<gamma>. (k, \<gamma>) \<in> set ?l \<Longrightarrow> valid_path \<gamma>; line_integral_exists ?F ?basis (rec_join ?l); finite ?basis\<rbrakk> \<Longrightarrow> \<forall>(k, \<gamma>)\<in>set ?l. line_integral_exists ?F ?basis \<gamma>
chain_subdiv_path \<gamma> one_chain
boundary_chain one_chain
line_integral_exists F basis \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain. valid_path \<gamma>
finite basis
set l = one_chain
distinct l
rec_join l = \<gamma>
valid_chain_list l

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

goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain = line_integral F basis \<gamma>
[PROOF STEP]
show "one_chain_line_integral F basis one_chain = line_integral F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain = line_integral F basis \<gamma>
[PROOF STEP]
using line_integral_on_path_eq_line_integral_on_equiv_chain(1)[OF assms(1) assms(2) 0 assms(4) assms(5)]
[PROOF STATE]
proof (prove)
using this:
one_chain_line_integral F basis one_chain = line_integral F basis \<gamma>

goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain = line_integral F basis \<gamma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
one_chain_line_integral F basis one_chain = line_integral F basis \<gamma>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma chain_subdiv_chain_character:
  shows "chain_subdiv_chain one_chain1 subdiv \<longleftrightarrow>
        (\<exists>f. \<Union>(f ` one_chain1) = subdiv \<and>
             (\<forall>(k, \<gamma>)\<in>one_chain1.
                 if k = 1
                 then chain_subdiv_path \<gamma> (f (k, \<gamma>))
                 else chain_subdiv_path (reversepath \<gamma>) (f (k, \<gamma>))) \<and>
             (\<forall>p\<in>one_chain1.
                 \<forall>p'\<in>one_chain1. p \<noteq> p' \<longrightarrow> f p \<inter> f p' = {}) \<and>
             (\<forall>x\<in>one_chain1. finite (f x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chain_subdiv_chain one_chain1 subdiv = (\<exists>f. \<Union> (f ` one_chain1) = subdiv \<and> (\<forall>(k, \<gamma>)\<in>one_chain1. if k = 1 then chain_subdiv_path \<gamma> (f (k, \<gamma>)) else chain_subdiv_path (reversepath \<gamma>) (f (k, \<gamma>))) \<and> (\<forall>p\<in>one_chain1. \<forall>p'\<in>one_chain1. p \<noteq> p' \<longrightarrow> f p \<inter> f p' = {}) \<and> (\<forall>x\<in>one_chain1. finite (f x)))
[PROOF STEP]
unfolding chain_subdiv_chain_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>f. \<Union> (f ` one_chain1) = subdiv \<and> (\<forall>c\<in>one_chain1. chain_subdiv_path (coeff_cube_to_path c) (f c)) \<and> pairwise (\<lambda>p p'. f p \<inter> f p' = {}) one_chain1 \<and> (\<forall>x\<in>one_chain1. finite (f x))) = (\<exists>f. \<Union> (f ` one_chain1) = subdiv \<and> (\<forall>(k, \<gamma>)\<in>one_chain1. if k = 1 then chain_subdiv_path \<gamma> (f (k, \<gamma>)) else chain_subdiv_path (reversepath \<gamma>) (f (k, \<gamma>))) \<and> (\<forall>p\<in>one_chain1. \<forall>p'\<in>one_chain1. p \<noteq> p' \<longrightarrow> f p \<inter> f p' = {}) \<and> (\<forall>x\<in>one_chain1. finite (f x)))
[PROOF STEP]
by (safe; intro exI conjI iffI; fastforce simp add: pairwise_def)


[STATEMENT]
lemma chain_subdiv_chain_imp_finite_subdiv:
  assumes "finite one_chain1"
    "chain_subdiv_chain one_chain1 subdiv"
  shows "finite subdiv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite subdiv
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite one_chain1
chain_subdiv_chain one_chain1 subdiv

goal (1 subgoal):
 1. finite subdiv
[PROOF STEP]
by(auto simp add: chain_subdiv_chain_def)


[STATEMENT]
lemma valid_subdiv_imp_valid_one_chain:
  assumes chain1_eq_chain2: "chain_subdiv_chain one_chain1 subdiv" and
    boundary_chain1: "boundary_chain one_chain1" and
    boundary_chain2: "boundary_chain subdiv" and
    valid_path: "\<forall>(k, \<gamma>) \<in> subdiv. valid_path \<gamma>"
  shows "\<forall>(k, \<gamma>) \<in> one_chain1. valid_path \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>
[PROOF STEP]
obtain f where f_props:
    "((\<Union>(f ` one_chain1)) = subdiv)"
    "(\<forall>(k,\<gamma>)\<in>one_chain1. if k = 1 then chain_subdiv_path \<gamma> (f(k,\<gamma>)) else chain_subdiv_path (reversepath \<gamma>) (f(k,\<gamma>)))"
    "(\<forall>p\<in>one_chain1. \<forall>p'\<in>one_chain1. p \<noteq> p' \<longrightarrow> f p \<inter> f p' = {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>\<Union> (f ` one_chain1) = subdiv; \<forall>(k, \<gamma>)\<in>one_chain1. if k = 1 then chain_subdiv_path \<gamma> (f (k, \<gamma>)) else chain_subdiv_path (reversepath \<gamma>) (f (k, \<gamma>)); \<forall>p\<in>one_chain1. \<forall>p'\<in>one_chain1. p \<noteq> p' \<longrightarrow> f p \<inter> f p' = {}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using chain1_eq_chain2 chain_subdiv_chain_character
[PROOF STATE]
proof (prove)
using this:
chain_subdiv_chain one_chain1 subdiv
chain_subdiv_chain ?one_chain1.0 ?subdiv = (\<exists>f. \<Union> (f ` ?one_chain1.0) = ?subdiv \<and> (\<forall>(k, \<gamma>)\<in>?one_chain1.0. if k = 1 then chain_subdiv_path \<gamma> (f (k, \<gamma>)) else chain_subdiv_path (reversepath \<gamma>) (f (k, \<gamma>))) \<and> (\<forall>p\<in>?one_chain1.0. \<forall>p'\<in>?one_chain1.0. p \<noteq> p' \<longrightarrow> f p \<inter> f p' = {}) \<and> (\<forall>x\<in>?one_chain1.0. finite (f x)))

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>\<Union> (f ` one_chain1) = subdiv; \<forall>(k, \<gamma>)\<in>one_chain1. if k = 1 then chain_subdiv_path \<gamma> (f (k, \<gamma>)) else chain_subdiv_path (reversepath \<gamma>) (f (k, \<gamma>)); \<forall>p\<in>one_chain1. \<forall>p'\<in>one_chain1. p \<noteq> p' \<longrightarrow> f p \<inter> f p' = {}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Union> (f ` one_chain1) = subdiv
\<forall>(k, \<gamma>)\<in>one_chain1. if k = 1 then chain_subdiv_path \<gamma> (f (k, \<gamma>)) else chain_subdiv_path (reversepath \<gamma>) (f (k, \<gamma>))
\<forall>p\<in>one_chain1. \<forall>p'\<in>one_chain1. p \<noteq> p' \<longrightarrow> f p \<inter> f p' = {}

goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>
[PROOF STEP]
have "\<And> k \<gamma>. (k,\<gamma>) \<in> one_chain1\<Longrightarrow> valid_path \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k \<gamma>. (k, \<gamma>) \<in> one_chain1 \<Longrightarrow> valid_path \<gamma>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k \<gamma>. (k, \<gamma>) \<in> one_chain1 \<Longrightarrow> valid_path \<gamma>
[PROOF STEP]
fix k \<gamma>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k \<gamma>. (k, \<gamma>) \<in> one_chain1 \<Longrightarrow> valid_path \<gamma>
[PROOF STEP]
assume ass: "(k,\<gamma>) \<in> one_chain1"
[PROOF STATE]
proof (state)
this:
(k, \<gamma>) \<in> one_chain1

goal (1 subgoal):
 1. \<And>k \<gamma>. (k, \<gamma>) \<in> one_chain1 \<Longrightarrow> valid_path \<gamma>
[PROOF STEP]
show "valid_path \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path \<gamma>
[PROOF STEP]
proof (cases "k = 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k = 1 \<Longrightarrow> valid_path \<gamma>
 2. k \<noteq> 1 \<Longrightarrow> valid_path \<gamma>
[PROOF STEP]
assume k_eq_1: "k = 1"
[PROOF STATE]
proof (state)
this:
k = 1

goal (2 subgoals):
 1. k = 1 \<Longrightarrow> valid_path \<gamma>
 2. k \<noteq> 1 \<Longrightarrow> valid_path \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k = 1
[PROOF STEP]
have i:"chain_subdiv_path \<gamma> (f(k,\<gamma>))"
[PROOF STATE]
proof (prove)
using this:
k = 1

goal (1 subgoal):
 1. chain_subdiv_path \<gamma> (f (k, \<gamma>))
[PROOF STEP]
using f_props(2) ass
[PROOF STATE]
proof (prove)
using this:
k = 1
\<forall>(k, \<gamma>)\<in>one_chain1. if k = 1 then chain_subdiv_path \<gamma> (f (k, \<gamma>)) else chain_subdiv_path (reversepath \<gamma>) (f (k, \<gamma>))
(k, \<gamma>) \<in> one_chain1

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

goal (2 subgoals):
 1. k = 1 \<Longrightarrow> valid_path \<gamma>
 2. k \<noteq> 1 \<Longrightarrow> valid_path \<gamma>
[PROOF STEP]
have ii:"boundary_chain (f(k,\<gamma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. boundary_chain (f (k, \<gamma>))
[PROOF STEP]
using f_props(1) ass assms
[PROOF STATE]
proof (prove)
using this:
\<Union> (f ` one_chain1) = subdiv
(k, \<gamma>) \<in> one_chain1
chain_subdiv_chain one_chain1 subdiv
boundary_chain one_chain1
boundary_chain subdiv
\<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>

goal (1 subgoal):
 1. boundary_chain (f (k, \<gamma>))
[PROOF STEP]
apply (simp add: boundary_chain_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Union> (f ` one_chain1) = subdiv; (k, \<gamma>) \<in> one_chain1; chain_subdiv_chain one_chain1 subdiv; \<forall>x\<in>one_chain1. case x of (k, \<gamma>) \<Rightarrow> k = 1 \<or> k = - 1; \<forall>x\<in>subdiv. case x of (k, \<gamma>) \<Rightarrow> k = 1 \<or> k = - 1; \<forall>x\<in>subdiv. case x of (k, \<gamma>) \<Rightarrow> valid_path \<gamma>\<rbrakk> \<Longrightarrow> \<forall>x\<in>f (k, \<gamma>). case x of (k, \<gamma>) \<Rightarrow> k = 1 \<or> k = - 1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
boundary_chain (f (k, \<gamma>))

goal (2 subgoals):
 1. k = 1 \<Longrightarrow> valid_path \<gamma>
 2. k \<noteq> 1 \<Longrightarrow> valid_path \<gamma>
[PROOF STEP]
have "iv": " \<forall>(k, \<gamma>)\<in>f (k, \<gamma>). valid_path \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>f (k, \<gamma>). valid_path \<gamma>
[PROOF STEP]
using f_props(1) ass assms
[PROOF STATE]
proof (prove)
using this:
\<Union> (f ` one_chain1) = subdiv
(k, \<gamma>) \<in> one_chain1
chain_subdiv_chain one_chain1 subdiv
boundary_chain one_chain1
boundary_chain subdiv
\<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>

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

goal (2 subgoals):
 1. k = 1 \<Longrightarrow> valid_path \<gamma>
 2. k \<noteq> 1 \<Longrightarrow> valid_path \<gamma>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path \<gamma>
[PROOF STEP]
using valid_path_equiv_valid_chain_list[OF i ii iv]
[PROOF STATE]
proof (prove)
using this:
valid_path \<gamma>

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

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> valid_path \<gamma>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> valid_path \<gamma>
[PROOF STEP]
assume "k \<noteq> 1"
[PROOF STATE]
proof (state)
this:
k \<noteq> 1

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> valid_path \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k \<noteq> 1
[PROOF STEP]
have k_eq_neg1: "k = -1"
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 1

goal (1 subgoal):
 1. k = - 1
[PROOF STEP]
using ass boundary_chain1
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 1
(k, \<gamma>) \<in> one_chain1
boundary_chain one_chain1

goal (1 subgoal):
 1. k = - 1
[PROOF STEP]
by (auto simp add: boundary_chain_def)
[PROOF STATE]
proof (state)
this:
k = - 1

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> valid_path \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k = - 1
[PROOF STEP]
have i:"chain_subdiv_path (reversepath \<gamma>) (f(k,\<gamma>))"
[PROOF STATE]
proof (prove)
using this:
k = - 1

goal (1 subgoal):
 1. chain_subdiv_path (reversepath \<gamma>) (f (k, \<gamma>))
[PROOF STEP]
using f_props(2) ass
[PROOF STATE]
proof (prove)
using this:
k = - 1
\<forall>(k, \<gamma>)\<in>one_chain1. if k = 1 then chain_subdiv_path \<gamma> (f (k, \<gamma>)) else chain_subdiv_path (reversepath \<gamma>) (f (k, \<gamma>))
(k, \<gamma>) \<in> one_chain1

goal (1 subgoal):
 1. chain_subdiv_path (reversepath \<gamma>) (f (k, \<gamma>))
[PROOF STEP]
using \<open>k \<noteq> 1\<close>
[PROOF STATE]
proof (prove)
using this:
k = - 1
\<forall>(k, \<gamma>)\<in>one_chain1. if k = 1 then chain_subdiv_path \<gamma> (f (k, \<gamma>)) else chain_subdiv_path (reversepath \<gamma>) (f (k, \<gamma>))
(k, \<gamma>) \<in> one_chain1
k \<noteq> 1

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

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> valid_path \<gamma>
[PROOF STEP]
have ii:"boundary_chain (f(k,\<gamma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. boundary_chain (f (k, \<gamma>))
[PROOF STEP]
using f_props(1) ass assms
[PROOF STATE]
proof (prove)
using this:
\<Union> (f ` one_chain1) = subdiv
(k, \<gamma>) \<in> one_chain1
chain_subdiv_chain one_chain1 subdiv
boundary_chain one_chain1
boundary_chain subdiv
\<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>

goal (1 subgoal):
 1. boundary_chain (f (k, \<gamma>))
[PROOF STEP]
by (auto simp add: boundary_chain_def)
[PROOF STATE]
proof (state)
this:
boundary_chain (f (k, \<gamma>))

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> valid_path \<gamma>
[PROOF STEP]
have "iv": " \<forall>(k, \<gamma>)\<in>f (k, \<gamma>). valid_path \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>f (k, \<gamma>). valid_path \<gamma>
[PROOF STEP]
using f_props(1) ass assms
[PROOF STATE]
proof (prove)
using this:
\<Union> (f ` one_chain1) = subdiv
(k, \<gamma>) \<in> one_chain1
chain_subdiv_chain one_chain1 subdiv
boundary_chain one_chain1
boundary_chain subdiv
\<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>

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

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> valid_path \<gamma>
[PROOF STEP]
have "valid_path (reversepath \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path (reversepath \<gamma>)
[PROOF STEP]
using valid_path_equiv_valid_chain_list[OF i ii iv]
[PROOF STATE]
proof (prove)
using this:
valid_path (reversepath \<gamma>)

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

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> valid_path \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
valid_path (reversepath \<gamma>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
valid_path (reversepath \<gamma>)

goal (1 subgoal):
 1. valid_path \<gamma>
[PROOF STEP]
using  reversepath_reversepath valid_path_imp_reverse
[PROOF STATE]
proof (prove)
using this:
valid_path (reversepath \<gamma>)
reversepath (reversepath ?g) = ?g
valid_path ?g \<Longrightarrow> valid_path (reversepath ?g)

goal (1 subgoal):
 1. valid_path \<gamma>
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
valid_path \<gamma>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
valid_path \<gamma>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(?k, ?\<gamma>) \<in> one_chain1 \<Longrightarrow> valid_path ?\<gamma>

goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(?k, ?\<gamma>) \<in> one_chain1 \<Longrightarrow> valid_path ?\<gamma>
[PROOF STEP]
show valid_path1: "\<forall>(k, \<gamma>) \<in> one_chain1. valid_path \<gamma>"
[PROOF STATE]
proof (prove)
using this:
(?k, ?\<gamma>) \<in> one_chain1 \<Longrightarrow> valid_path ?\<gamma>

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

goal:
No subgoals!
[PROOF STEP]
qed