[STATEMENT]
lemma joined_is_valid:
  assumes boundary_chain: "boundary_chain (set l)" and
    valid_path: "\<And>k \<gamma>. (k, \<gamma>) \<in> set l \<Longrightarrow> valid_path \<gamma>" and
    valid_chain_list_ass: "valid_chain_list l"
  shows "valid_path (rec_join l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path (rec_join l)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
boundary_chain (set l)
(?k, ?\<gamma>) \<in> set l \<Longrightarrow> valid_path ?\<gamma>
valid_chain_list l

goal (1 subgoal):
 1. valid_path (rec_join l)
[PROOF STEP]
proof(induction l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>boundary_chain (set []); \<And>k \<gamma>. (k, \<gamma>) \<in> set [] \<Longrightarrow> valid_path \<gamma>; valid_chain_list []\<rbrakk> \<Longrightarrow> valid_path (rec_join [])
 2. \<And>a l. \<lbrakk>\<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); boundary_chain (set (a # l)); \<And>k \<gamma>. (k, \<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path \<gamma>; valid_chain_list (a # l)\<rbrakk> \<Longrightarrow> valid_path (rec_join (a # l))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
boundary_chain (set [])
(?k, ?\<gamma>) \<in> set [] \<Longrightarrow> valid_path ?\<gamma>
valid_chain_list []

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

goal (1 subgoal):
 1. valid_path (rec_join [])
[PROOF STEP]
using C1_differentiable_imp_piecewise[OF C1_differentiable_on_const[of "0" "{0..1}"]]
[PROOF STATE]
proof (prove)
using this:
boundary_chain (set [])
(?k, ?\<gamma>) \<in> set [] \<Longrightarrow> valid_path ?\<gamma>
valid_chain_list []
(\<lambda>z. 0::?'a) piecewise_C1_differentiable_on {0..1}

goal (1 subgoal):
 1. valid_path (rec_join [])
[PROOF STEP]
by (auto simp add: valid_path_def)
[PROOF STATE]
proof (state)
this:
valid_path (rec_join [])

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>\<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); boundary_chain (set (a # l)); \<And>k \<gamma>. (k, \<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path \<gamma>; valid_chain_list (a # l)\<rbrakk> \<Longrightarrow> valid_path (rec_join (a # l))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l. \<lbrakk>\<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); boundary_chain (set (a # l)); \<And>k \<gamma>. (k, \<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path \<gamma>; valid_chain_list (a # l)\<rbrakk> \<Longrightarrow> valid_path (rec_join (a # l))
[PROOF STEP]
case (Cons a l)
[PROOF STATE]
proof (state)
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)
boundary_chain (set (a # l))
(?k, ?\<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path ?\<gamma>
valid_chain_list (a # l)

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>\<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); boundary_chain (set (a # l)); \<And>k \<gamma>. (k, \<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path \<gamma>; valid_chain_list (a # l)\<rbrakk> \<Longrightarrow> valid_path (rec_join (a # l))
[PROOF STEP]
have *: "valid_path (rec_join ((k::int, \<gamma>) # l))"
    if "boundary_chain (set (l))"
      "(\<And>k' \<gamma>'. (k', \<gamma>') \<in> set l \<Longrightarrow> valid_path \<gamma>')"
      "valid_chain_list l"
      "valid_path (rec_join l) "
      "(\<And>k' \<gamma>'. (k', \<gamma>') \<in> set ((k, \<gamma>) # l) \<Longrightarrow> valid_path \<gamma>')"
      "valid_chain_list ((k, \<gamma>) # l)"
      "boundary_chain (set ((k,\<gamma>) # l))" for k \<gamma> l
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path (rec_join ((k, \<gamma>) # l))
[PROOF STEP]
proof (cases "l = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. l = [] \<Longrightarrow> valid_path (rec_join ((k, \<gamma>) # l))
 2. l \<noteq> [] \<Longrightarrow> valid_path (rec_join ((k, \<gamma>) # l))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
l = []

goal (2 subgoals):
 1. l = [] \<Longrightarrow> valid_path (rec_join ((k, \<gamma>) # l))
 2. l \<noteq> [] \<Longrightarrow> valid_path (rec_join ((k, \<gamma>) # l))
[PROOF STEP]
with that
[PROOF STATE]
proof (chain)
picking this:
boundary_chain (set l)
(?k', ?\<gamma>') \<in> set l \<Longrightarrow> valid_path ?\<gamma>'
valid_chain_list l
valid_path (rec_join l)
(?k', ?\<gamma>') \<in> set ((k, \<gamma>) # l) \<Longrightarrow> valid_path ?\<gamma>'
valid_chain_list ((k, \<gamma>) # l)
boundary_chain (set ((k, \<gamma>) # l))
l = []
[PROOF STEP]
show "valid_path (rec_join ((k, \<gamma>) # l))"
[PROOF STATE]
proof (prove)
using this:
boundary_chain (set l)
(?k', ?\<gamma>') \<in> set l \<Longrightarrow> valid_path ?\<gamma>'
valid_chain_list l
valid_path (rec_join l)
(?k', ?\<gamma>') \<in> set ((k, \<gamma>) # l) \<Longrightarrow> valid_path ?\<gamma>'
valid_chain_list ((k, \<gamma>) # l)
boundary_chain (set ((k, \<gamma>) # l))
l = []

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

goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> valid_path (rec_join ((k, \<gamma>) # l))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> valid_path (rec_join ((k, \<gamma>) # l))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
l \<noteq> []

goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> valid_path (rec_join ((k, \<gamma>) # 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> valid_path (rec_join ((k, \<gamma>) # l))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l = h # l'
[PROOF STEP]
show "valid_path (rec_join ((k, \<gamma>) # l))"
[PROOF STATE]
proof (prove)
using this:
l = h # l'

goal (1 subgoal):
 1. valid_path (rec_join ((k, \<gamma>) # l))
[PROOF STEP]
proof (simp, intro conjI impI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>l = h # l'; l = h # l'; k = 1\<rbrakk> \<Longrightarrow> valid_path (\<gamma> +++ rec_join (h # l'))
 2. \<lbrakk>l = h # l'; l = h # l'; k \<noteq> 1\<rbrakk> \<Longrightarrow> valid_path (reversepath \<gamma> +++ rec_join (h # l'))
[PROOF STEP]
assume k_eq_1: "k = 1"
[PROOF STATE]
proof (state)
this:
k = 1

goal (2 subgoals):
 1. \<lbrakk>l = h # l'; l = h # l'; k = 1\<rbrakk> \<Longrightarrow> valid_path (\<gamma> +++ rec_join (h # l'))
 2. \<lbrakk>l = h # l'; l = h # l'; k \<noteq> 1\<rbrakk> \<Longrightarrow> valid_path (reversepath \<gamma> +++ rec_join (h # l'))
[PROOF STEP]
have 0:"valid_path \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path \<gamma>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
boundary_chain (set l)
(?k', ?\<gamma>') \<in> set l \<Longrightarrow> valid_path ?\<gamma>'
valid_chain_list l
valid_path (rec_join l)
(?k', ?\<gamma>') \<in> set ((k, \<gamma>) # l) \<Longrightarrow> valid_path ?\<gamma>'
valid_chain_list ((k, \<gamma>) # l)
boundary_chain (set ((k, \<gamma>) # l))

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

goal (2 subgoals):
 1. \<lbrakk>l = h # l'; l = h # l'; k = 1\<rbrakk> \<Longrightarrow> valid_path (\<gamma> +++ rec_join (h # l'))
 2. \<lbrakk>l = h # l'; l = h # l'; k \<noteq> 1\<rbrakk> \<Longrightarrow> valid_path (reversepath \<gamma> +++ rec_join (h # l'))
[PROOF STEP]
have 1:"pathfinish \<gamma> = pathstart (rec_join (h#l'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pathfinish \<gamma> = pathstart (rec_join (h # l'))
[PROOF STEP]
using that(6) k_eq_1 l_nempty
[PROOF STATE]
proof (prove)
using this:
valid_chain_list ((k, \<gamma>) # l)
k = 1
l = h # l'

goal (1 subgoal):
 1. pathfinish \<gamma> = pathstart (rec_join (h # l'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pathfinish \<gamma> = pathstart (rec_join (h # l'))

goal (2 subgoals):
 1. \<lbrakk>l = h # l'; l = h # l'; k = 1\<rbrakk> \<Longrightarrow> valid_path (\<gamma> +++ rec_join (h # l'))
 2. \<lbrakk>l = h # l'; l = h # l'; k \<noteq> 1\<rbrakk> \<Longrightarrow> valid_path (reversepath \<gamma> +++ rec_join (h # l'))
[PROOF STEP]
show "valid_path (\<gamma> +++ rec_join (h#l'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path (\<gamma> +++ rec_join (h # l'))
[PROOF STEP]
using 0 1 valid_path_join that(4) l_nempty
[PROOF STATE]
proof (prove)
using this:
valid_path \<gamma>
pathfinish \<gamma> = pathstart (rec_join (h # l'))
\<lbrakk>valid_path ?g1.0; valid_path ?g2.0; pathfinish ?g1.0 = pathstart ?g2.0\<rbrakk> \<Longrightarrow> valid_path (?g1.0 +++ ?g2.0)
valid_path (rec_join l)
l = h # l'

goal (1 subgoal):
 1. valid_path (\<gamma> +++ rec_join (h # l'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_path (\<gamma> +++ rec_join (h # l'))

goal (1 subgoal):
 1. \<lbrakk>l = h # l'; l = h # l'; k \<noteq> 1\<rbrakk> \<Longrightarrow> valid_path (reversepath \<gamma> +++ rec_join (h # l'))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>l = h # l'; l = h # l'; k \<noteq> 1\<rbrakk> \<Longrightarrow> valid_path (reversepath \<gamma> +++ rec_join (h # l'))
[PROOF STEP]
assume "k \<noteq> 1"
[PROOF STATE]
proof (state)
this:
k \<noteq> 1

goal (1 subgoal):
 1. \<lbrakk>l = h # l'; l = h # l'; k \<noteq> 1\<rbrakk> \<Longrightarrow> valid_path (reversepath \<gamma> +++ rec_join (h # l'))
[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 that(7)
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 1
boundary_chain (set ((k, \<gamma>) # l))

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. \<lbrakk>l = h # l'; l = h # l'; k \<noteq> 1\<rbrakk> \<Longrightarrow> valid_path (reversepath \<gamma> +++ rec_join (h # l'))
[PROOF STEP]
have "valid_path \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path \<gamma>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
boundary_chain (set l)
(?k', ?\<gamma>') \<in> set l \<Longrightarrow> valid_path ?\<gamma>'
valid_chain_list l
valid_path (rec_join l)
(?k', ?\<gamma>') \<in> set ((k, \<gamma>) # l) \<Longrightarrow> valid_path ?\<gamma>'
valid_chain_list ((k, \<gamma>) # l)
boundary_chain (set ((k, \<gamma>) # l))

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

goal (1 subgoal):
 1. \<lbrakk>l = h # l'; l = h # l'; k \<noteq> 1\<rbrakk> \<Longrightarrow> valid_path (reversepath \<gamma> +++ rec_join (h # l'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
valid_path \<gamma>
[PROOF STEP]
have 0: "valid_path (reversepath \<gamma>)"
[PROOF STATE]
proof (prove)
using this:
valid_path \<gamma>

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

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. \<lbrakk>l = h # l'; l = h # l'; k \<noteq> 1\<rbrakk> \<Longrightarrow> valid_path (reversepath \<gamma> +++ rec_join (h # l'))
[PROOF STEP]
have 1: "pathfinish (reversepath \<gamma>) = pathstart (rec_join (h#l'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pathfinish (reversepath \<gamma>) = pathstart (rec_join (h # l'))
[PROOF STEP]
using that(6) k_eq_neg_1 l_nempty
[PROOF STATE]
proof (prove)
using this:
valid_chain_list ((k, \<gamma>) # l)
k = - 1
l = h # l'

goal (1 subgoal):
 1. pathfinish (reversepath \<gamma>) = pathstart (rec_join (h # l'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pathfinish (reversepath \<gamma>) = pathstart (rec_join (h # l'))

goal (1 subgoal):
 1. \<lbrakk>l = h # l'; l = h # l'; k \<noteq> 1\<rbrakk> \<Longrightarrow> valid_path (reversepath \<gamma> +++ rec_join (h # l'))
[PROOF STEP]
show "valid_path ((reversepath \<gamma>) +++ rec_join (h#l'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path (reversepath \<gamma> +++ rec_join (h # l'))
[PROOF STEP]
using 0 1 valid_path_join that(4) l_nempty
[PROOF STATE]
proof (prove)
using this:
valid_path (reversepath \<gamma>)
pathfinish (reversepath \<gamma>) = pathstart (rec_join (h # l'))
\<lbrakk>valid_path ?g1.0; valid_path ?g2.0; pathfinish ?g1.0 = pathstart ?g2.0\<rbrakk> \<Longrightarrow> valid_path (?g1.0 +++ ?g2.0)
valid_path (rec_join l)
l = h # l'

goal (1 subgoal):
 1. valid_path (reversepath \<gamma> +++ rec_join (h # l'))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
valid_path (reversepath \<gamma> +++ rec_join (h # l'))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>boundary_chain (set ?l); \<And>k' \<gamma>'. (k', \<gamma>') \<in> set ?l \<Longrightarrow> valid_path \<gamma>'; valid_chain_list ?l; valid_path (rec_join ?l); \<And>k' \<gamma>'. (k', \<gamma>') \<in> set ((?k, ?\<gamma>) # ?l) \<Longrightarrow> valid_path \<gamma>'; valid_chain_list ((?k, ?\<gamma>) # ?l); boundary_chain (set ((?k, ?\<gamma>) # ?l))\<rbrakk> \<Longrightarrow> valid_path (rec_join ((?k, ?\<gamma>) # ?l))

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>\<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); boundary_chain (set (a # l)); \<And>k \<gamma>. (k, \<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path \<gamma>; valid_chain_list (a # l)\<rbrakk> \<Longrightarrow> valid_path (rec_join (a # l))
[PROOF STEP]
have "\<forall>ps. valid_chain_list ps \<or> (\<exists>i f p psa. ps = (i, f) # p # psa \<and> ((i = 1 \<and> pathfinish f \<noteq> pathstart (rec_join (p # psa)) \<or> i \<noteq> 1 \<and> pathfinish (reversepath f) \<noteq> pathstart (rec_join (p # psa))) \<or> \<not> valid_chain_list (p # psa)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>ps. valid_chain_list ps \<or> (\<exists>i f p psa. ps = (i, f) # p # psa \<and> ((i = 1 \<and> pathfinish f \<noteq> pathstart (rec_join (p # psa)) \<or> i \<noteq> 1 \<and> pathfinish (reversepath f) \<noteq> pathstart (rec_join (p # psa))) \<or> \<not> valid_chain_list (p # psa)))
[PROOF STEP]
by (smt coeff_cube_to_path.elims valid_chain_list.elims(3))
[PROOF STATE]
proof (state)
this:
\<forall>ps. valid_chain_list ps \<or> (\<exists>i f p psa. ps = (i, f) # p # psa \<and> ((i = 1 \<and> pathfinish f \<noteq> pathstart (rec_join (p # psa)) \<or> i \<noteq> 1 \<and> pathfinish (reversepath f) \<noteq> pathstart (rec_join (p # psa))) \<or> \<not> valid_chain_list (p # psa)))

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>\<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); boundary_chain (set (a # l)); \<And>k \<gamma>. (k, \<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path \<gamma>; valid_chain_list (a # l)\<rbrakk> \<Longrightarrow> valid_path (rec_join (a # l))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>ps. valid_chain_list ps \<or> (\<exists>i f p psa. ps = (i, f) # p # psa \<and> ((i = 1 \<and> pathfinish f \<noteq> pathstart (rec_join (p # psa)) \<or> i \<noteq> 1 \<and> pathfinish (reversepath f) \<noteq> pathstart (rec_join (p # psa))) \<or> \<not> valid_chain_list (p # psa)))

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>\<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); boundary_chain (set (a # l)); \<And>k \<gamma>. (k, \<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path \<gamma>; valid_chain_list (a # l)\<rbrakk> \<Longrightarrow> valid_path (rec_join (a # l))
[PROOF STEP]
have "boundary_chain (set l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. boundary_chain (set l)
[PROOF STEP]
by (meson Cons.prems(1) boundary_chain_def set_subset_Cons subset_eq)
[PROOF STATE]
proof (state)
this:
boundary_chain (set l)

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>\<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); boundary_chain (set (a # l)); \<And>k \<gamma>. (k, \<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path \<gamma>; valid_chain_list (a # l)\<rbrakk> \<Longrightarrow> valid_path (rec_join (a # l))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>ps. valid_chain_list ps \<or> (\<exists>i f p psa. ps = (i, f) # p # psa \<and> ((i = 1 \<and> pathfinish f \<noteq> pathstart (rec_join (p # psa)) \<or> i \<noteq> 1 \<and> pathfinish (reversepath f) \<noteq> pathstart (rec_join (p # psa))) \<or> \<not> valid_chain_list (p # psa)))
boundary_chain (set l)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>ps. valid_chain_list ps \<or> (\<exists>i f p psa. ps = (i, f) # p # psa \<and> ((i = 1 \<and> pathfinish f \<noteq> pathstart (rec_join (p # psa)) \<or> i \<noteq> 1 \<and> pathfinish (reversepath f) \<noteq> pathstart (rec_join (p # psa))) \<or> \<not> valid_chain_list (p # psa)))
boundary_chain (set l)

goal (1 subgoal):
 1. valid_path (rec_join (a # l))
[PROOF STEP]
using * Cons
[PROOF STATE]
proof (prove)
using this:
\<forall>ps. valid_chain_list ps \<or> (\<exists>i f p psa. ps = (i, f) # p # psa \<and> ((i = 1 \<and> pathfinish f \<noteq> pathstart (rec_join (p # psa)) \<or> i \<noteq> 1 \<and> pathfinish (reversepath f) \<noteq> pathstart (rec_join (p # psa))) \<or> \<not> valid_chain_list (p # psa)))
boundary_chain (set l)
\<lbrakk>boundary_chain (set ?l); \<And>k' \<gamma>'. (k', \<gamma>') \<in> set ?l \<Longrightarrow> valid_path \<gamma>'; valid_chain_list ?l; valid_path (rec_join ?l); \<And>k' \<gamma>'. (k', \<gamma>') \<in> set ((?k, ?\<gamma>) # ?l) \<Longrightarrow> valid_path \<gamma>'; valid_chain_list ((?k, ?\<gamma>) # ?l); boundary_chain (set ((?k, ?\<gamma>) # ?l))\<rbrakk> \<Longrightarrow> valid_path (rec_join ((?k, ?\<gamma>) # ?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)
boundary_chain (set (a # l))
(?k, ?\<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path ?\<gamma>
valid_chain_list (a # l)

goal (1 subgoal):
 1. valid_path (rec_join (a # l))
[PROOF STEP]
by (metis (no_types) list.set_intros(2) prod.collapse valid_chain_list.simps(3))
[PROOF STATE]
proof (state)
this:
valid_path (rec_join (a # l))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pathstart_rec_join_1:
  "pathstart (rec_join ((1, \<gamma>) # l)) = pathstart \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pathstart (rec_join ((1, \<gamma>) # l)) = pathstart \<gamma>
[PROOF STEP]
proof (cases "l = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. l = [] \<Longrightarrow> pathstart (rec_join ((1, \<gamma>) # l)) = pathstart \<gamma>
 2. l \<noteq> [] \<Longrightarrow> pathstart (rec_join ((1, \<gamma>) # l)) = pathstart \<gamma>
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
l = []

goal (2 subgoals):
 1. l = [] \<Longrightarrow> pathstart (rec_join ((1, \<gamma>) # l)) = pathstart \<gamma>
 2. l \<noteq> [] \<Longrightarrow> pathstart (rec_join ((1, \<gamma>) # l)) = pathstart \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l = []
[PROOF STEP]
show "pathstart (rec_join ((1, \<gamma>) # l)) = pathstart \<gamma>"
[PROOF STATE]
proof (prove)
using this:
l = []

goal (1 subgoal):
 1. pathstart (rec_join ((1, \<gamma>) # l)) = pathstart \<gamma>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pathstart (rec_join ((1, \<gamma>) # l)) = pathstart \<gamma>

goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> pathstart (rec_join ((1, \<gamma>) # l)) = pathstart \<gamma>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> pathstart (rec_join ((1, \<gamma>) # l)) = pathstart \<gamma>
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
l \<noteq> []

goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> pathstart (rec_join ((1, \<gamma>) # l)) = pathstart \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l \<noteq> []
[PROOF STEP]
obtain h l' where "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> pathstart (rec_join ((1, \<gamma>) # l)) = pathstart \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l = h # l'
[PROOF STEP]
show "pathstart (rec_join ((1, \<gamma>) # l)) = pathstart \<gamma>"
[PROOF STATE]
proof (prove)
using this:
l = h # l'

goal (1 subgoal):
 1. pathstart (rec_join ((1, \<gamma>) # l)) = pathstart \<gamma>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pathstart (rec_join ((1, \<gamma>) # l)) = pathstart \<gamma>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pathstart_rec_join_2:
  "pathstart (rec_join ((-1, \<gamma>) # l)) = pathstart (reversepath \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pathstart (rec_join ((- 1, \<gamma>) # l)) = pathstart (reversepath \<gamma>)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> pathstart (rec_join ((- 1, \<gamma>) # l)) = pathstart (reversepath \<gamma>)
 2. \<not> ?P \<Longrightarrow> pathstart (rec_join ((- 1, \<gamma>) # l)) = pathstart (reversepath \<gamma>)
[PROOF STEP]
assume "l = []"
[PROOF STATE]
proof (state)
this:
l = []

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

goal (1 subgoal):
 1. pathstart (rec_join ((- 1, \<gamma>) # l)) = pathstart (reversepath \<gamma>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pathstart (rec_join ((- 1, \<gamma>) # l)) = pathstart (reversepath \<gamma>)

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

goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> pathstart (rec_join ((- 1, \<gamma>) # l)) = pathstart (reversepath \<gamma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l \<noteq> []
[PROOF STEP]
obtain h l' where "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> pathstart (rec_join ((- 1, \<gamma>) # l)) = pathstart (reversepath \<gamma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l = h # l'
[PROOF STEP]
show "pathstart (rec_join ((- 1, \<gamma>) # l)) = pathstart (reversepath \<gamma>)"
[PROOF STATE]
proof (prove)
using this:
l = h # l'

goal (1 subgoal):
 1. pathstart (rec_join ((- 1, \<gamma>) # l)) = pathstart (reversepath \<gamma>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pathstart (rec_join ((- 1, \<gamma>) # l)) = pathstart (reversepath \<gamma>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pathstart_rec_join:
  "pathstart (rec_join ((1, \<gamma>) # l)) = pathstart \<gamma>"
  "pathstart (rec_join ((-1, \<gamma>) # l)) = pathstart (reversepath \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pathstart (rec_join ((1, \<gamma>) # l)) = pathstart \<gamma> &&& pathstart (rec_join ((- 1, \<gamma>) # l)) = pathstart (reversepath \<gamma>)
[PROOF STEP]
using pathstart_rec_join_1 pathstart_rec_join_2
[PROOF STATE]
proof (prove)
using this:
pathstart (rec_join ((1, ?\<gamma>) # ?l)) = pathstart ?\<gamma>
pathstart (rec_join ((- 1, ?\<gamma>) # ?l)) = pathstart (reversepath ?\<gamma>)

goal (1 subgoal):
 1. pathstart (rec_join ((1, \<gamma>) # l)) = pathstart \<gamma> &&& pathstart (rec_join ((- 1, \<gamma>) # l)) = pathstart (reversepath \<gamma>)
[PROOF STEP]
by auto


[STATEMENT]
lemma line_integral_exists_on_rec_join:
  assumes boundary_chain: "boundary_chain (set l)" and
    valid_chain_list: "valid_chain_list l" and
    valid_path: "\<And>k \<gamma>. (k, \<gamma>) \<in> set l \<Longrightarrow> valid_path \<gamma>" and
    line_integral_exists: "\<forall>(k, \<gamma>) \<in> set l. line_integral_exists F basis \<gamma>"
  shows "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 assms
[PROOF STATE]
proof (prove)
using this:
boundary_chain (set l)
valid_chain_list l
(?k, ?\<gamma>) \<in> set l \<Longrightarrow> valid_path ?\<gamma>
\<forall>(k, \<gamma>)\<in>set l. line_integral_exists F basis \<gamma>

goal (1 subgoal):
 1. line_integral_exists F basis (rec_join l)
[PROOF STEP]
proof (induction l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>boundary_chain (set []); valid_chain_list []; \<And>k \<gamma>. (k, \<gamma>) \<in> set [] \<Longrightarrow> valid_path \<gamma>; \<forall>(k, y)\<in>set []. line_integral_exists F basis y\<rbrakk> \<Longrightarrow> line_integral_exists F basis (rec_join [])
 2. \<And>a l. \<lbrakk>\<lbrakk>boundary_chain (set l); valid_chain_list l; \<And>k \<gamma>. (k, \<gamma>) \<in> set l \<Longrightarrow> valid_path \<gamma>; \<forall>(k, y)\<in>set l. line_integral_exists F basis y\<rbrakk> \<Longrightarrow> line_integral_exists F basis (rec_join l); boundary_chain (set (a # l)); valid_chain_list (a # l); \<And>k \<gamma>. (k, \<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path \<gamma>; \<forall>(k, y)\<in>set (a # l). line_integral_exists F basis y\<rbrakk> \<Longrightarrow> line_integral_exists F basis (rec_join (a # l))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
boundary_chain (set [])
valid_chain_list []
(?k, ?\<gamma>) \<in> set [] \<Longrightarrow> valid_path ?\<gamma>
\<forall>a\<in>set []. case a of (k, a) \<Rightarrow> line_integral_exists F basis a

goal (2 subgoals):
 1. \<lbrakk>boundary_chain (set []); valid_chain_list []; \<And>k \<gamma>. (k, \<gamma>) \<in> set [] \<Longrightarrow> valid_path \<gamma>; \<forall>(k, y)\<in>set []. line_integral_exists F basis y\<rbrakk> \<Longrightarrow> line_integral_exists F basis (rec_join [])
 2. \<And>a l. \<lbrakk>\<lbrakk>boundary_chain (set l); valid_chain_list l; \<And>k \<gamma>. (k, \<gamma>) \<in> set l \<Longrightarrow> valid_path \<gamma>; \<forall>(k, y)\<in>set l. line_integral_exists F basis y\<rbrakk> \<Longrightarrow> line_integral_exists F basis (rec_join l); boundary_chain (set (a # l)); valid_chain_list (a # l); \<And>k \<gamma>. (k, \<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path \<gamma>; \<forall>(k, y)\<in>set (a # l). line_integral_exists F basis y\<rbrakk> \<Longrightarrow> line_integral_exists F basis (rec_join (a # l))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
boundary_chain (set [])
valid_chain_list []
(?k, ?\<gamma>) \<in> set [] \<Longrightarrow> valid_path ?\<gamma>
\<forall>a\<in>set []. case a of (k, a) \<Rightarrow> line_integral_exists F basis a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
boundary_chain (set [])
valid_chain_list []
(?k, ?\<gamma>) \<in> set [] \<Longrightarrow> valid_path ?\<gamma>
\<forall>a\<in>set []. case a of (k, a) \<Rightarrow> line_integral_exists F basis a

goal (1 subgoal):
 1. line_integral_exists F basis (rec_join [])
[PROOF STEP]
proof (simp add: line_integral_exists_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. boundary_chain {} \<Longrightarrow> (\<lambda>x. \<Sum>b\<in>basis. F 0 \<bullet> b * (vector_derivative (\<lambda>a. 0) (at x within {0..1}) \<bullet> b)) integrable_on {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. boundary_chain {} \<Longrightarrow> (\<lambda>x. \<Sum>b\<in>basis. F 0 \<bullet> b * (vector_derivative (\<lambda>a. 0) (at x within {0..1}) \<bullet> b)) integrable_on {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. boundary_chain {} \<Longrightarrow> (\<lambda>x. \<Sum>b\<in>basis. F 0 \<bullet> b * (vector_derivative (\<lambda>a. 0) (at x within {0..1}) \<bullet> b)) integrable_on {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. boundary_chain {} \<Longrightarrow> (\<lambda>x. \<Sum>b\<in>basis. F 0 \<bullet> b * (vector_derivative (\<lambda>a. 0) (at x within {0..1}) \<bullet> b)) integrable_on {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 (simp add: gamma_deriv_at_within)
[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. boundary_chain {} \<Longrightarrow> (\<lambda>x. \<Sum>b\<in>basis. F 0 \<bullet> b * (vector_derivative (\<lambda>a. 0) (at x within {0..1}) \<bullet> b)) integrable_on {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. boundary_chain {} \<Longrightarrow> (\<lambda>x. \<Sum>b\<in>basis. F 0 \<bullet> b * (vector_derivative (\<lambda>a. 0) (at x within {0..1}) \<bullet> b)) integrable_on {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]
have " ((\<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 (1 subgoal):
 1. boundary_chain {} \<Longrightarrow> (\<lambda>x. \<Sum>b\<in>basis. F 0 \<bullet> b * (vector_derivative (\<lambda>a. 0) (at x within {0..1}) \<bullet> b)) integrable_on {0..1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking 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}
[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)) integrable_on {0..1}"
[PROOF STATE]
proof (prove)
using 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 (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)) integrable_on {0..1}
[PROOF STEP]
by auto
[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)) integrable_on {0..1}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
line_integral_exists F basis (rec_join [])

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

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>\<lbrakk>boundary_chain (set l); valid_chain_list l; \<And>k \<gamma>. (k, \<gamma>) \<in> set l \<Longrightarrow> valid_path \<gamma>; \<forall>(k, y)\<in>set l. line_integral_exists F basis y\<rbrakk> \<Longrightarrow> line_integral_exists F basis (rec_join l); boundary_chain (set (a # l)); valid_chain_list (a # l); \<And>k \<gamma>. (k, \<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path \<gamma>; \<forall>(k, y)\<in>set (a # l). line_integral_exists F basis y\<rbrakk> \<Longrightarrow> line_integral_exists F basis (rec_join (a # l))
[PROOF STEP]
obtain k \<gamma> where aeq: "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>boundary_chain (set l); valid_chain_list l; \<And>k \<gamma>. (k, \<gamma>) \<in> set l \<Longrightarrow> valid_path \<gamma>; \<forall>(k, y)\<in>set l. line_integral_exists F basis y\<rbrakk> \<Longrightarrow> line_integral_exists F basis (rec_join l); boundary_chain (set (a # l)); valid_chain_list (a # l); \<And>k \<gamma>. (k, \<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path \<gamma>; \<forall>(k, y)\<in>set (a # l). line_integral_exists F basis y\<rbrakk> \<Longrightarrow> line_integral_exists F basis (rec_join (a # l))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis (rec_join (a # l))
[PROOF STEP]
unfolding aeq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis (rec_join ((k, \<gamma>) # l))
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> line_integral_exists F basis (rec_join ((k, \<gamma>) # l))
 2. \<not> ?P \<Longrightarrow> line_integral_exists F basis (rec_join ((k, \<gamma>) # l))
[PROOF STEP]
assume l_empty: "l = []"
[PROOF STATE]
proof (state)
this:
l = []

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

goal (1 subgoal):
 1. line_integral_exists F basis (rec_join ((k, \<gamma>) # l))
[PROOF STEP]
using Cons.prems aeq line_integral_on_reverse_path(2)
[PROOF STATE]
proof (prove)
using this:
l = []
boundary_chain (set (a # l))
valid_chain_list (a # l)
(?k, ?\<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path ?\<gamma>
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> line_integral_exists F basis a
a = (k, \<gamma>)
\<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 (rec_join ((k, \<gamma>) # l))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
line_integral_exists F basis (rec_join ((k, \<gamma>) # l))

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

goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> line_integral_exists F basis (rec_join ((k, \<gamma>) # 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_exists F basis (rec_join ((k, \<gamma>) # l))
[PROOF STEP]
show "line_integral_exists F basis (rec_join ((k, \<gamma>) # l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis (rec_join ((k, \<gamma>) # l))
[PROOF STEP]
proof (auto simp add: l_nempty)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k = 1 \<Longrightarrow> line_integral_exists F basis (\<gamma> +++ rec_join (h # l'))
 2. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis (reversepath \<gamma> +++ rec_join (h # l'))
[PROOF STEP]
assume k_eq_1: "k = 1"
[PROOF STATE]
proof (state)
this:
k = 1

goal (2 subgoals):
 1. k = 1 \<Longrightarrow> line_integral_exists F basis (\<gamma> +++ rec_join (h # l'))
 2. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis (reversepath \<gamma> +++ rec_join (h # l'))
[PROOF STEP]
have 0: "line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis \<gamma>
[PROOF STEP]
using Cons.prems(4) aeq
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> line_integral_exists F basis 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. k = 1 \<Longrightarrow> line_integral_exists F basis (\<gamma> +++ rec_join (h # l'))
 2. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis (reversepath \<gamma> +++ rec_join (h # l'))
[PROOF STEP]
have 1: "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 (mono_tags) Cons boundary_chain_def list.set_intros(2) valid_chain_list.elims(3) valid_chain_list.simps(3))
[PROOF STATE]
proof (state)
this:
line_integral_exists F basis (rec_join l)

goal (2 subgoals):
 1. k = 1 \<Longrightarrow> line_integral_exists F basis (\<gamma> +++ rec_join (h # l'))
 2. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis (reversepath \<gamma> +++ rec_join (h # l'))
[PROOF STEP]
have 2: "valid_path \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path \<gamma>
[PROOF STEP]
using Cons aeq
[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>a\<in>set l. case a of (k, a) \<Rightarrow> line_integral_exists F basis a\<rbrakk> \<Longrightarrow> line_integral_exists F basis (rec_join l)
boundary_chain (set (a # l))
valid_chain_list (a # l)
(?k, ?\<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path ?\<gamma>
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> line_integral_exists F basis 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. k = 1 \<Longrightarrow> line_integral_exists F basis (\<gamma> +++ rec_join (h # l'))
 2. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis (reversepath \<gamma> +++ rec_join (h # l'))
[PROOF STEP]
have 3:"valid_path (rec_join l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path (rec_join l)
[PROOF STEP]
by (metis (no_types) Cons.prems boundary_chain_def joined_is_valid l_nempty set_subset_Cons subsetCE valid_chain_list.simps(3))
[PROOF STATE]
proof (state)
this:
valid_path (rec_join l)

goal (2 subgoals):
 1. k = 1 \<Longrightarrow> line_integral_exists F basis (\<gamma> +++ rec_join (h # l'))
 2. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis (reversepath \<gamma> +++ rec_join (h # l'))
[PROOF STEP]
show "line_integral_exists F basis (\<gamma> +++ rec_join (h#l'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis (\<gamma> +++ rec_join (h # l'))
[PROOF STEP]
using line_integral_distrib(2)[OF 0 1 2 3] assms l_nempty
[PROOF STATE]
proof (prove)
using this:
line_integral_exists F basis (\<gamma> +++ rec_join l)
boundary_chain (set l)
valid_chain_list l
(?k, ?\<gamma>) \<in> set l \<Longrightarrow> valid_path ?\<gamma>
\<forall>(k, \<gamma>)\<in>set l. line_integral_exists F basis \<gamma>
l = h # l'

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

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis (reversepath \<gamma> +++ rec_join (h # l'))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis (reversepath \<gamma> +++ rec_join (h # l'))
[PROOF STEP]
assume "k \<noteq> 1"
[PROOF STATE]
proof (state)
this:
k \<noteq> 1

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis (reversepath \<gamma> +++ rec_join (h # l'))
[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 Cons aeq
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 1
\<lbrakk>boundary_chain (set l); valid_chain_list l; \<And>k \<gamma>. (k, \<gamma>) \<in> set l \<Longrightarrow> valid_path \<gamma>; \<forall>a\<in>set l. case a of (k, a) \<Rightarrow> line_integral_exists F basis a\<rbrakk> \<Longrightarrow> line_integral_exists F basis (rec_join l)
boundary_chain (set (a # l))
valid_chain_list (a # l)
(?k, ?\<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path ?\<gamma>
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> line_integral_exists F basis a
a = (k, \<gamma>)

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

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis (reversepath \<gamma> +++ rec_join (h # l'))
[PROOF STEP]
have gamma_valid: "valid_path \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path \<gamma>
[PROOF STEP]
using Cons aeq
[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>a\<in>set l. case a of (k, a) \<Rightarrow> line_integral_exists F basis a\<rbrakk> \<Longrightarrow> line_integral_exists F basis (rec_join l)
boundary_chain (set (a # l))
valid_chain_list (a # l)
(?k, ?\<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path ?\<gamma>
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> line_integral_exists F basis a
a = (k, \<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> line_integral_exists F basis (reversepath \<gamma> +++ rec_join (h # l'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
valid_path \<gamma>
[PROOF STEP]
have 2: "valid_path (reversepath \<gamma>)"
[PROOF STATE]
proof (prove)
using this:
valid_path \<gamma>

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

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_exists F basis (reversepath \<gamma> +++ rec_join (h # l'))
[PROOF STEP]
have "line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis \<gamma>
[PROOF STEP]
using Cons aeq
[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>a\<in>set l. case a of (k, a) \<Rightarrow> line_integral_exists F basis a\<rbrakk> \<Longrightarrow> line_integral_exists F basis (rec_join l)
boundary_chain (set (a # l))
valid_chain_list (a # l)
(?k, ?\<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path ?\<gamma>
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> line_integral_exists F basis 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. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis (reversepath \<gamma> +++ rec_join (h # l'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
line_integral_exists F basis \<gamma>
[PROOF STEP]
have 0: "line_integral_exists F basis (reversepath \<gamma>)"
[PROOF STATE]
proof (prove)
using this:
line_integral_exists F basis \<gamma>

goal (1 subgoal):
 1. line_integral_exists F basis (reversepath \<gamma>)
[PROOF STEP]
using line_integral_on_reverse_path(2) gamma_valid
[PROOF STATE]
proof (prove)
using this:
line_integral_exists F basis \<gamma>
\<lbrakk>valid_path ?\<gamma>; line_integral_exists ?F ?basis ?\<gamma>\<rbrakk> \<Longrightarrow> line_integral_exists ?F ?basis (reversepath ?\<gamma>)
valid_path \<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_exists F basis (reversepath \<gamma> +++ rec_join (h # l'))
[PROOF STEP]
have 1: "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 Cons aeq
[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>a\<in>set l. case a of (k, a) \<Rightarrow> line_integral_exists F basis a\<rbrakk> \<Longrightarrow> line_integral_exists F basis (rec_join l)
boundary_chain (set (a # l))
valid_chain_list (a # l)
(?k, ?\<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path ?\<gamma>
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> line_integral_exists F basis a
a = (k, \<gamma>)

goal (1 subgoal):
 1. line_integral_exists F basis (rec_join l)
[PROOF STEP]
by (metis (mono_tags) boundary_chain_def insert_iff list.set(2) list.set_intros(2) valid_chain_list.elims(3) valid_chain_list.simps(3))
[PROOF STATE]
proof (state)
this:
line_integral_exists F basis (rec_join l)

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis (reversepath \<gamma> +++ rec_join (h # l'))
[PROOF STEP]
have 3:"valid_path (rec_join l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path (rec_join l)
[PROOF STEP]
by (metis (no_types) Cons.prems(1) Cons.prems(2) Cons.prems(3) boundary_chain_def joined_is_valid l_nempty set_subset_Cons subsetCE valid_chain_list.simps(3))
[PROOF STATE]
proof (state)
this:
valid_path (rec_join l)

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis (reversepath \<gamma> +++ rec_join (h # l'))
[PROOF STEP]
show "line_integral_exists F basis ((reversepath \<gamma>) +++ rec_join (h#l'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis (reversepath \<gamma> +++ rec_join (h # l'))
[PROOF STEP]
using line_integral_distrib(2)[OF 0 1 2 3] assms l_nempty
[PROOF STATE]
proof (prove)
using this:
line_integral_exists F basis (reversepath \<gamma> +++ rec_join l)
boundary_chain (set l)
valid_chain_list l
(?k, ?\<gamma>) \<in> set l \<Longrightarrow> valid_path ?\<gamma>
\<forall>(k, \<gamma>)\<in>set l. line_integral_exists F basis \<gamma>
l = h # l'

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
line_integral_exists F basis (rec_join (a # l))

goal:
No subgoals!
[PROOF STEP]
qed


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

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

goal (1 subgoal):
 1. line_integral_exists F basis (\<gamma> +++ rec_join l)
[PROOF STEP]
using degenerate_path_is_valid_path
[PROOF STATE]
proof (prove)
using this:
(?k', ?\<gamma>') \<in> set ((1, \<gamma>) # l) \<Longrightarrow> valid_path ?\<gamma>'
\<lbrakk>valid_path (rec_join ((1, \<gamma>) # l)); valid_path (\<lambda>x. 0)\<rbrakk> \<Longrightarrow> line_integral_exists F basis (rec_join ((1, \<gamma>) # l) +++ (\<lambda>x. 0))
valid_path (\<lambda>x. ?c)

goal (1 subgoal):
 1. line_integral_exists F basis (\<gamma> +++ rec_join l)
[PROOF STEP]
by (fastforce simp add: l_empty)
[PROOF STATE]
proof (state)
this:
line_integral_exists F basis (\<gamma> +++ rec_join l)

goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> line_integral_exists F basis (\<gamma> +++ rec_join l)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> line_integral_exists F basis (\<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_exists F basis (\<gamma> +++ rec_join l)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l \<noteq> []
[PROOF STEP]
obtain h l' where "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_exists F basis (\<gamma> +++ rec_join l)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l = h # l'
[PROOF STEP]
show "line_integral_exists F basis (\<gamma> +++ rec_join l)"
[PROOF STATE]
proof (prove)
using this:
l = h # l'

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma line_integral_exists_rec_join_cons_2:
  assumes "line_integral_exists F basis (rec_join ((-1,\<gamma>) # l))"
    "(\<And>k' \<gamma>'. (k', \<gamma>') \<in> set ((1,\<gamma>) # l) \<Longrightarrow> valid_path \<gamma>')"
    "finite basis"
  shows "line_integral_exists F basis ((reversepath \<gamma>) +++ (rec_join l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis (reversepath \<gamma> +++ rec_join l)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> line_integral_exists F basis (reversepath \<gamma> +++ rec_join l)
 2. \<not> ?P \<Longrightarrow> line_integral_exists 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_exists F basis (reversepath \<gamma> +++ rec_join l)
 2. \<not> ?P \<Longrightarrow> line_integral_exists F basis (reversepath \<gamma> +++ rec_join l)
[PROOF STEP]
show "line_integral_exists F basis ((reversepath \<gamma>) +++ rec_join l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis (reversepath \<gamma> +++ rec_join l)
[PROOF STEP]
using assms(2) line_integral_distrib(2)[OF assms(1) line_integral_exists_on_degenerate_path[OF assms(3)], of "0"]
[PROOF STATE]
proof (prove)
using this:
(?k', ?\<gamma>') \<in> set ((1, \<gamma>) # l) \<Longrightarrow> valid_path ?\<gamma>'
\<lbrakk>valid_path (rec_join ((- 1, \<gamma>) # l)); valid_path (\<lambda>x. 0)\<rbrakk> \<Longrightarrow> line_integral_exists F basis (rec_join ((- 1, \<gamma>) # l) +++ (\<lambda>x. 0))

goal (1 subgoal):
 1. line_integral_exists F basis (reversepath \<gamma> +++ rec_join l)
[PROOF STEP]
using degenerate_path_is_valid_path
[PROOF STATE]
proof (prove)
using this:
(?k', ?\<gamma>') \<in> set ((1, \<gamma>) # l) \<Longrightarrow> valid_path ?\<gamma>'
\<lbrakk>valid_path (rec_join ((- 1, \<gamma>) # l)); valid_path (\<lambda>x. 0)\<rbrakk> \<Longrightarrow> line_integral_exists F basis (rec_join ((- 1, \<gamma>) # l) +++ (\<lambda>x. 0))
valid_path (\<lambda>x. ?c)

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

goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> line_integral_exists F basis (reversepath \<gamma> +++ rec_join l)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> line_integral_exists 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_exists 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 = 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_exists F basis (reversepath \<gamma> +++ rec_join l)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
line_integral_exists F basis (rec_join ((- 1, \<gamma>) # l))
(?k', ?\<gamma>') \<in> set ((1, \<gamma>) # l) \<Longrightarrow> valid_path ?\<gamma>'
finite basis
l = h # l'
[PROOF STEP]
show "line_integral_exists F basis ((reversepath \<gamma>) +++ rec_join l)"
[PROOF STATE]
proof (prove)
using this:
line_integral_exists F basis (rec_join ((- 1, \<gamma>) # l))
(?k', ?\<gamma>') \<in> set ((1, \<gamma>) # l) \<Longrightarrow> valid_path ?\<gamma>'
finite basis
l = h # l'

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma line_integral_exists_on_rec_join':
  assumes boundary_chain: "boundary_chain (set l)" and
    valid_chain_list: "valid_chain_list l" and
    valid_path: "\<And>k \<gamma>. (k, \<gamma>) \<in> set l \<Longrightarrow> valid_path \<gamma>" and
    line_integral_exists: "line_integral_exists F basis (rec_join l)" and
    finite_basis: "finite basis"
  shows "\<forall>(k, \<gamma>) \<in> set l. line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>set l. line_integral_exists F basis \<gamma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
boundary_chain (set l)
valid_chain_list l
(?k, ?\<gamma>) \<in> set l \<Longrightarrow> valid_path ?\<gamma>
line_integral_exists F basis (rec_join l)
finite basis

goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>set l. line_integral_exists F basis \<gamma>
[PROOF STEP]
proof (induction l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>boundary_chain (set []); valid_chain_list []; \<And>k \<gamma>. (k, \<gamma>) \<in> set [] \<Longrightarrow> valid_path \<gamma>; line_integral_exists F basis (rec_join []); finite basis\<rbrakk> \<Longrightarrow> \<forall>(k, y)\<in>set []. line_integral_exists F basis y
 2. \<And>a l. \<lbrakk>\<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, y)\<in>set l. line_integral_exists F basis y; boundary_chain (set (a # l)); valid_chain_list (a # l); \<And>k \<gamma>. (k, \<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path \<gamma>; line_integral_exists F basis (rec_join (a # l)); finite basis\<rbrakk> \<Longrightarrow> \<forall>(k, y)\<in>set (a # l). line_integral_exists F basis y
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
boundary_chain (set [])
valid_chain_list []
(?k, ?\<gamma>) \<in> set [] \<Longrightarrow> valid_path ?\<gamma>
line_integral_exists F basis (rec_join [])
finite basis

goal (2 subgoals):
 1. \<lbrakk>boundary_chain (set []); valid_chain_list []; \<And>k \<gamma>. (k, \<gamma>) \<in> set [] \<Longrightarrow> valid_path \<gamma>; line_integral_exists F basis (rec_join []); finite basis\<rbrakk> \<Longrightarrow> \<forall>(k, y)\<in>set []. line_integral_exists F basis y
 2. \<And>a l. \<lbrakk>\<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, y)\<in>set l. line_integral_exists F basis y; boundary_chain (set (a # l)); valid_chain_list (a # l); \<And>k \<gamma>. (k, \<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path \<gamma>; line_integral_exists F basis (rec_join (a # l)); finite basis\<rbrakk> \<Longrightarrow> \<forall>(k, y)\<in>set (a # l). line_integral_exists F basis y
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a\<in>set []. case a of (k, a) \<Rightarrow> line_integral_exists F basis a
[PROOF STEP]
by (simp add: line_integral_exists_def)
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>set []. case a of (k, a) \<Rightarrow> line_integral_exists F basis a

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>\<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, y)\<in>set l. line_integral_exists F basis y; boundary_chain (set (a # l)); valid_chain_list (a # l); \<And>k \<gamma>. (k, \<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path \<gamma>; line_integral_exists F basis (rec_join (a # l)); finite basis\<rbrakk> \<Longrightarrow> \<forall>(k, y)\<in>set (a # l). line_integral_exists F basis y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l. \<lbrakk>\<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, y)\<in>set l. line_integral_exists F basis y; boundary_chain (set (a # l)); valid_chain_list (a # l); \<And>k \<gamma>. (k, \<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path \<gamma>; line_integral_exists F basis (rec_join (a # l)); finite basis\<rbrakk> \<Longrightarrow> \<forall>(k, y)\<in>set (a # l). line_integral_exists F basis y
[PROOF STEP]
case ass: (Cons a l)
[PROOF STATE]
proof (state)
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>a\<in>set l. case a of (k, a) \<Rightarrow> line_integral_exists F basis a
boundary_chain (set (a # l))
valid_chain_list (a # l)
(?k, ?\<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path ?\<gamma>
line_integral_exists F basis (rec_join (a # l))
finite basis

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>\<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, y)\<in>set l. line_integral_exists F basis y; boundary_chain (set (a # l)); valid_chain_list (a # l); \<And>k \<gamma>. (k, \<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path \<gamma>; line_integral_exists F basis (rec_join (a # l)); finite basis\<rbrakk> \<Longrightarrow> \<forall>(k, y)\<in>set (a # l). line_integral_exists F basis y
[PROOF STEP]
obtain k \<gamma> where k_gamma:"a = (k,\<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k \<gamma>. a = (k, \<gamma>) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
a = (k, \<gamma>)

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>\<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, y)\<in>set l. line_integral_exists F basis y; boundary_chain (set (a # l)); valid_chain_list (a # l); \<And>k \<gamma>. (k, \<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path \<gamma>; line_integral_exists F basis (rec_join (a # l)); finite basis\<rbrakk> \<Longrightarrow> \<forall>(k, y)\<in>set (a # l). line_integral_exists F basis y
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> line_integral_exists F basis a
[PROOF STEP]
apply (auto simp add: k_gamma)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. line_integral_exists F basis \<gamma>
 2. \<And>a b. (a, b) \<in> set l \<Longrightarrow> line_integral_exists F basis b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. line_integral_exists F basis \<gamma>
 2. \<And>a b. (a, b) \<in> set l \<Longrightarrow> line_integral_exists F basis b
[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]
proof(cases "k = 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k = 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
 2. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
assume k_eq_1: "k = 1"
[PROOF STATE]
proof (state)
this:
k = 1

goal (2 subgoals):
 1. k = 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
 2. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
have 0: "line_integral_exists F basis (\<gamma> +++ (rec_join l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis (\<gamma> +++ rec_join l)
[PROOF STEP]
using line_integral_exists_rec_join_cons k_eq_1 k_gamma ass(4) ass(5) ass(6)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>line_integral_exists ?F ?basis (rec_join ((1, ?\<gamma>) # ?l)); \<And>k' \<gamma>'. (k', \<gamma>') \<in> set ((1, ?\<gamma>) # ?l) \<Longrightarrow> valid_path \<gamma>'; finite ?basis\<rbrakk> \<Longrightarrow> line_integral_exists ?F ?basis (?\<gamma> +++ rec_join ?l)
k = 1
a = (k, \<gamma>)
(?k, ?\<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path ?\<gamma>
line_integral_exists F basis (rec_join (a # l))
finite basis

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

goal (2 subgoals):
 1. k = 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
 2. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
have 2: "valid_path \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path \<gamma>
[PROOF STEP]
using ass k_gamma
[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>a\<in>set l. case a of (k, a) \<Rightarrow> line_integral_exists F basis a
boundary_chain (set (a # l))
valid_chain_list (a # l)
(?k, ?\<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path ?\<gamma>
line_integral_exists F basis (rec_join (a # l))
finite basis
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. k = 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
 2. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<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_joinD1[OF 0 2]
[PROOF STATE]
proof (prove)
using this:
line_integral_exists F basis \<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. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> line_integral_exists 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_exists 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 k_gamma
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 1
\<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>a\<in>set l. case a of (k, a) \<Rightarrow> line_integral_exists F basis a
boundary_chain (set (a # l))
valid_chain_list (a # l)
(?k, ?\<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path ?\<gamma>
line_integral_exists F basis (rec_join (a # l))
finite basis
a = (k, \<gamma>)

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

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
have 0: "line_integral_exists F basis ((reversepath \<gamma>) +++ (rec_join l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis (reversepath \<gamma> +++ rec_join l)
[PROOF STEP]
using line_integral_exists_rec_join_cons_2[OF ] k_eq_neg_1 k_gamma ass(4) ass(5) ass(6)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>line_integral_exists ?F ?basis (rec_join ((- 1, ?\<gamma>) # ?l)); \<And>k' \<gamma>'. (k', \<gamma>') \<in> set ((1, ?\<gamma>) # ?l) \<Longrightarrow> valid_path \<gamma>'; finite ?basis\<rbrakk> \<Longrightarrow> line_integral_exists ?F ?basis (reversepath ?\<gamma> +++ rec_join ?l)
k = - 1
a = (k, \<gamma>)
(?k, ?\<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path ?\<gamma>
line_integral_exists F basis (rec_join (a # l))
finite basis

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

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
have gamma_valid:
        "valid_path \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path \<gamma>
[PROOF STEP]
using ass k_gamma
[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>a\<in>set l. case a of (k, a) \<Rightarrow> line_integral_exists F basis a
boundary_chain (set (a # l))
valid_chain_list (a # l)
(?k, ?\<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path ?\<gamma>
line_integral_exists F basis (rec_join (a # l))
finite basis
a = (k, \<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> line_integral_exists F basis \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
valid_path \<gamma>
[PROOF STEP]
have 2: "valid_path (reversepath \<gamma>)"
[PROOF STATE]
proof (prove)
using this:
valid_path \<gamma>

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

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_exists F basis \<gamma>
[PROOF STEP]
have "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_exists_joinD1[OF 0 2]
[PROOF STATE]
proof (prove)
using this:
line_integral_exists F basis (reversepath \<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_exists F basis \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
line_integral_exists F basis (reversepath \<gamma>)
[PROOF STEP]
show "line_integral_exists F basis (\<gamma>)"
[PROOF STATE]
proof (prove)
using this:
line_integral_exists F basis (reversepath \<gamma>)

goal (1 subgoal):
 1. line_integral_exists F basis \<gamma>
[PROOF STEP]
using line_integral_on_reverse_path(2)[OF 2] reversepath_reversepath
[PROOF STATE]
proof (prove)
using this:
line_integral_exists F basis (reversepath \<gamma>)
line_integral_exists ?F ?basis (reversepath \<gamma>) \<Longrightarrow> line_integral_exists ?F ?basis (reversepath (reversepath \<gamma>))
reversepath (reversepath ?g) = ?g

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:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
line_integral_exists F basis \<gamma>

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> set l \<Longrightarrow> line_integral_exists F basis b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> set l \<Longrightarrow> line_integral_exists F basis b
[PROOF STEP]
have 0:"boundary_chain (set l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. boundary_chain (set l)
[PROOF STEP]
using ass(2)
[PROOF STATE]
proof (prove)
using this:
boundary_chain (set (a # l))

goal (1 subgoal):
 1. boundary_chain (set l)
[PROOF STEP]
by (auto simp add: boundary_chain_def)
[PROOF STATE]
proof (state)
this:
boundary_chain (set l)

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> set l \<Longrightarrow> line_integral_exists F basis b
[PROOF STEP]
have 1:"valid_chain_list l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_chain_list l
[PROOF STEP]
using ass(3)
[PROOF STATE]
proof (prove)
using this:
valid_chain_list (a # l)

goal (1 subgoal):
 1. valid_chain_list l
[PROOF STEP]
apply (auto simp add: k_gamma)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_chain_list ((k, \<gamma>) # l) \<Longrightarrow> valid_chain_list l
[PROOF STEP]
by (metis 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 b. (a, b) \<in> set l \<Longrightarrow> line_integral_exists F basis b
[PROOF STEP]
have 2:"(\<And>k \<gamma>. (k, \<gamma>) \<in> set (l) \<Longrightarrow> valid_path \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k \<gamma>. (k, \<gamma>) \<in> set l \<Longrightarrow> valid_path \<gamma>
[PROOF STEP]
using ass(4)
[PROOF STATE]
proof (prove)
using this:
(?k, ?\<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path ?\<gamma>

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

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> set l \<Longrightarrow> line_integral_exists F basis b
[PROOF STEP]
have 3: "valid_path (rec_join l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path (rec_join l)
[PROOF STEP]
using joined_is_valid[OF 0] 1 2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>k \<gamma>. (k, \<gamma>) \<in> set l \<Longrightarrow> valid_path \<gamma>; valid_chain_list l\<rbrakk> \<Longrightarrow> valid_path (rec_join l)
valid_chain_list l
(?k, ?\<gamma>) \<in> set l \<Longrightarrow> valid_path ?\<gamma>

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

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> set l \<Longrightarrow> line_integral_exists F basis b
[PROOF STEP]
have 4: "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]
proof(cases "k = 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k = 1 \<Longrightarrow> line_integral_exists F basis (rec_join l)
 2. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis (rec_join l)
[PROOF STEP]
assume k_eq_1: "k = 1"
[PROOF STATE]
proof (state)
this:
k = 1

goal (2 subgoals):
 1. k = 1 \<Longrightarrow> line_integral_exists F basis (rec_join l)
 2. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis (rec_join l)
[PROOF STEP]
have 0: "line_integral_exists F basis (\<gamma> +++ (rec_join l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis (\<gamma> +++ rec_join l)
[PROOF STEP]
using line_integral_exists_rec_join_cons k_eq_1 k_gamma ass(4) ass(5) ass(6)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>line_integral_exists ?F ?basis (rec_join ((1, ?\<gamma>) # ?l)); \<And>k' \<gamma>'. (k', \<gamma>') \<in> set ((1, ?\<gamma>) # ?l) \<Longrightarrow> valid_path \<gamma>'; finite ?basis\<rbrakk> \<Longrightarrow> line_integral_exists ?F ?basis (?\<gamma> +++ rec_join ?l)
k = 1
a = (k, \<gamma>)
(?k, ?\<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path ?\<gamma>
line_integral_exists F basis (rec_join (a # l))
finite basis

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

goal (2 subgoals):
 1. k = 1 \<Longrightarrow> line_integral_exists F basis (rec_join l)
 2. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis (rec_join l)
[PROOF STEP]
show "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_joinD2[OF 0 3]
[PROOF STATE]
proof (prove)
using this:
line_integral_exists F basis (rec_join l)

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

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis (rec_join l)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis (rec_join l)
[PROOF STEP]
assume "k \<noteq> 1"
[PROOF STATE]
proof (state)
this:
k \<noteq> 1

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis (rec_join l)
[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 k_gamma
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 1
\<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>a\<in>set l. case a of (k, a) \<Rightarrow> line_integral_exists F basis a
boundary_chain (set (a # l))
valid_chain_list (a # l)
(?k, ?\<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path ?\<gamma>
line_integral_exists F basis (rec_join (a # l))
finite basis
a = (k, \<gamma>)

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

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis (rec_join l)
[PROOF STEP]
have 0: "line_integral_exists F basis ((reversepath \<gamma>) +++ (rec_join l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis (reversepath \<gamma> +++ rec_join l)
[PROOF STEP]
using line_integral_exists_rec_join_cons_2[OF ] k_eq_neg_1 k_gamma ass(4) ass(5) ass(6)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>line_integral_exists ?F ?basis (rec_join ((- 1, ?\<gamma>) # ?l)); \<And>k' \<gamma>'. (k', \<gamma>') \<in> set ((1, ?\<gamma>) # ?l) \<Longrightarrow> valid_path \<gamma>'; finite ?basis\<rbrakk> \<Longrightarrow> line_integral_exists ?F ?basis (reversepath ?\<gamma> +++ rec_join ?l)
k = - 1
a = (k, \<gamma>)
(?k, ?\<gamma>) \<in> set (a # l) \<Longrightarrow> valid_path ?\<gamma>
line_integral_exists F basis (rec_join (a # l))
finite basis

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

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis (rec_join l)
[PROOF STEP]
show "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_joinD2[OF 0 3]
[PROOF STATE]
proof (prove)
using this:
line_integral_exists F basis (rec_join l)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
line_integral_exists F basis (rec_join l)

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> set l \<Longrightarrow> line_integral_exists F basis b
[PROOF STEP]
show "\<And>a b. (a, b) \<in> set l \<Longrightarrow> line_integral_exists F basis b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> set l \<Longrightarrow> line_integral_exists F basis b
[PROOF STEP]
using 0 1 2 3 4 ass(1)[OF 0 1 2] ass(6)
[PROOF STATE]
proof (prove)
using this:
boundary_chain (set l)
valid_chain_list l
(?k, ?\<gamma>) \<in> set l \<Longrightarrow> valid_path ?\<gamma>
valid_path (rec_join l)
line_integral_exists F basis (rec_join l)
\<lbrakk>\<And>k \<gamma>. (k, \<gamma>) \<in> set l \<Longrightarrow> (?k k \<gamma>, \<gamma>) \<in> set l; line_integral_exists F basis (rec_join l); finite basis\<rbrakk> \<Longrightarrow> \<forall>a\<in>set l. case a of (k, a) \<Rightarrow> line_integral_exists F basis a
finite basis

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> set l \<Longrightarrow> line_integral_exists F basis b
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(?a, ?b) \<in> set l \<Longrightarrow> line_integral_exists F basis ?b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>set (a # l). case a of (k, a) \<Rightarrow> line_integral_exists F basis a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valid_path_equiv_valid_chain_list:
  assumes path_eq_chain: "chain_subdiv_path \<gamma> one_chain"
    and "boundary_chain one_chain" "\<forall>(k, \<gamma>) \<in> one_chain. valid_path \<gamma>"
  shows "valid_path \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path \<gamma>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 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 (1 subgoal):
 1. 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. valid_path \<gamma>
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:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma line_integral_rec_join_cons:
  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 (\<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 (\<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 (\<gamma> +++ rec_join l)
 2. \<not> ?P \<Longrightarrow> line_integral F basis (rec_join ((1, \<gamma>) # l)) = line_integral F basis (\<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 (\<gamma> +++ rec_join l)
 2. \<not> ?P \<Longrightarrow> line_integral F basis (rec_join ((1, \<gamma>) # l)) = line_integral F basis (\<gamma> +++ rec_join l)
[PROOF STEP]
show "line_integral F basis (rec_join ((1,\<gamma>) # l)) = line_integral F basis (\<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 (\<gamma> +++ rec_join l)
[PROOF STEP]
using assms line_integral_distrib(1)[OF assms(1) 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 \<gamma>; valid_path (\<lambda>x. 0)\<rbrakk> \<Longrightarrow> line_integral F basis (\<gamma> +++ (\<lambda>x. 0)) = line_integral F basis \<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 (\<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 (\<gamma> +++ (\<lambda>x. 0)) = line_integral F basis \<gamma> + line_integral F basis (\<lambda>x. 0)\<rbrakk> \<Longrightarrow> line_integral F basis \<gamma> = line_integral F basis (\<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 (\<gamma> +++ (\<lambda>x. 0)) = line_integral F basis \<gamma> + line_integral F basis (\<lambda>x. 0)\<rbrakk> \<Longrightarrow> line_integral F basis \<gamma> = line_integral F basis (\<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 (\<gamma> +++ rec_join l)

goal (1 subgoal):
 1. l \<noteq> [] \<Longrightarrow> line_integral F basis (rec_join ((1, \<gamma>) # l)) = line_integral F basis (\<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 (\<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 (\<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 (\<gamma> +++ rec_join l)
[PROOF STEP]
show "line_integral F basis (rec_join ((1,\<gamma>) # l)) = line_integral F basis (\<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 (\<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 (\<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 (\<gamma> +++ rec_join l)

goal:
No subgoals!
[PROOF STEP]
qed