[STATEMENT]
lemma chain_reparam_weak_path_line_integral:
  assumes path_eq_chain: "chain_reparam_weak_path \<gamma> one_chain" and
    boundary_chain: "boundary_chain one_chain" and
    line_integral_exists: "\<forall>b\<in>basis. \<forall>(k::int, \<gamma>) \<in> one_chain. line_integral_exists F {b} \<gamma>" and
    valid_path: "\<forall>(k::int, \<gamma>) \<in> one_chain. valid_path \<gamma>" and
    finite_basis: "finite basis" and
    cont: "\<forall>b\<in>basis. \<forall>(k,\<gamma>2)\<in>one_chain. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)" and
    finite_one_chain: "finite one_chain"
  shows "line_integral F basis \<gamma> = one_chain_line_integral F basis one_chain"
    "line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis \<gamma> = one_chain_line_integral F basis one_chain &&& line_integral_exists F basis \<gamma>
[PROOF STEP]
(*"valid_path \<gamma>" This cannot be proven, see the crappy assumption of derivs/eq_pw_smooth :( *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis \<gamma> = one_chain_line_integral F basis one_chain &&& line_integral_exists F basis \<gamma>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. line_integral F basis \<gamma> = one_chain_line_integral F basis one_chain
 2. line_integral_exists F basis \<gamma>
[PROOF STEP]
obtain l where l_props: "set l = one_chain" "distinct l" "reparam \<gamma> (rec_join l)" "valid_chain_list l" "l \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l. \<lbrakk>set l = one_chain; distinct l; reparam \<gamma> (rec_join l); valid_chain_list l; l \<noteq> []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using chain_reparam_weak_path_def assms
[PROOF STATE]
proof (prove)
using this:
chain_reparam_weak_path ?\<gamma> ?one_chain \<equiv> \<exists>l. set l = ?one_chain \<and> distinct l \<and> reparam ?\<gamma> (rec_join l) \<and> valid_chain_list l \<and> l \<noteq> []
chain_reparam_weak_path \<gamma> one_chain
boundary_chain one_chain
\<forall>b\<in>basis. \<forall>(k, \<gamma>)\<in>one_chain. line_integral_exists F {b} \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain. valid_path \<gamma>
finite basis
\<forall>b\<in>basis. \<forall>(k, \<gamma>2)\<in>one_chain. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
finite one_chain

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

goal (2 subgoals):
 1. line_integral F basis \<gamma> = one_chain_line_integral F basis one_chain
 2. line_integral_exists F basis \<gamma>
[PROOF STEP]
have bchain_l: "boundary_chain (set l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. boundary_chain (set l)
[PROOF STEP]
using l_props boundary_chain
[PROOF STATE]
proof (prove)
using this:
set l = one_chain
distinct l
reparam \<gamma> (rec_join l)
valid_chain_list l
l \<noteq> []
boundary_chain one_chain

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

goal (2 subgoals):
 1. line_integral F basis \<gamma> = one_chain_line_integral F basis one_chain
 2. line_integral_exists F basis \<gamma>
[PROOF STEP]
have cont_forall: "\<forall>b\<in>basis. continuous_on (\<Union>(k, \<gamma>)\<in>one_chain. path_image \<gamma>) (\<lambda>x. F x \<bullet> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b\<in>basis. continuous_on (\<Union>(k, \<gamma>)\<in>one_chain. path_image \<gamma>) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b. b \<in> basis \<Longrightarrow> continuous_on (\<Union>(k, \<gamma>)\<in>one_chain. path_image \<gamma>) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b. b \<in> basis \<Longrightarrow> continuous_on (\<Union>(k, \<gamma>)\<in>one_chain. path_image \<gamma>) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
assume ass: "b \<in> basis"
[PROOF STATE]
proof (state)
this:
b \<in> basis

goal (1 subgoal):
 1. \<And>b. b \<in> basis \<Longrightarrow> continuous_on (\<Union>(k, \<gamma>)\<in>one_chain. path_image \<gamma>) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
have "continuous_on (\<Union>((path_image \<circ> snd) ` one_chain))  (\<lambda>x. F x \<bullet> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on (\<Union> ((path_image \<circ> snd) ` one_chain)) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
apply(rule continuous_on_closed_UN[where ?S = "(path_image o snd) ` one_chain" ])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. finite ((path_image \<circ> snd) ` one_chain)
 2. \<And>s. s \<in> (path_image \<circ> snd) ` one_chain \<Longrightarrow> closed s
 3. \<And>s. s \<in> (path_image \<circ> snd) ` one_chain \<Longrightarrow> continuous_on s (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. finite one_chain
 2. \<And>s. s \<in> (path_image \<circ> snd) ` one_chain \<Longrightarrow> closed s
 3. \<And>s. s \<in> (path_image \<circ> snd) ` one_chain \<Longrightarrow> continuous_on s (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
show "finite one_chain"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite one_chain
[PROOF STEP]
using finite_one_chain
[PROOF STATE]
proof (prove)
using this:
finite one_chain

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

goal (2 subgoals):
 1. \<And>s. s \<in> (path_image \<circ> snd) ` one_chain \<Longrightarrow> closed s
 2. \<And>s. s \<in> (path_image \<circ> snd) ` one_chain \<Longrightarrow> continuous_on s (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
show "\<And>s. s \<in> (path_image \<circ> snd) ` one_chain \<Longrightarrow> closed s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<in> (path_image \<circ> snd) ` one_chain \<Longrightarrow> closed s
[PROOF STEP]
using  closed_valid_path_image[OF] valid_path
[PROOF STATE]
proof (prove)
using this:
valid_path ?g \<Longrightarrow> closed (path_image ?g)
\<forall>(k, \<gamma>)\<in>one_chain. valid_path \<gamma>

goal (1 subgoal):
 1. \<And>s. s \<in> (path_image \<circ> snd) ` one_chain \<Longrightarrow> closed s
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
?s \<in> (path_image \<circ> snd) ` one_chain \<Longrightarrow> closed ?s

goal (1 subgoal):
 1. \<And>s. s \<in> (path_image \<circ> snd) ` one_chain \<Longrightarrow> continuous_on s (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
show "\<And>s. s \<in> (path_image \<circ> snd) ` one_chain \<Longrightarrow> continuous_on s (\<lambda>x. F x \<bullet> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<in> (path_image \<circ> snd) ` one_chain \<Longrightarrow> continuous_on s (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
using cont ass
[PROOF STATE]
proof (prove)
using this:
\<forall>b\<in>basis. \<forall>(k, \<gamma>2)\<in>one_chain. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
b \<in> basis

goal (1 subgoal):
 1. \<And>s. s \<in> (path_image \<circ> snd) ` one_chain \<Longrightarrow> continuous_on s (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
?s \<in> (path_image \<circ> snd) ` one_chain \<Longrightarrow> continuous_on ?s (\<lambda>x. F x \<bullet> b)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
continuous_on (\<Union> ((path_image \<circ> snd) ` one_chain)) (\<lambda>x. F x \<bullet> b)

goal (1 subgoal):
 1. \<And>b. b \<in> basis \<Longrightarrow> continuous_on (\<Union>(k, \<gamma>)\<in>one_chain. path_image \<gamma>) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
continuous_on (\<Union> ((path_image \<circ> snd) ` one_chain)) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
show "continuous_on (\<Union>(k, \<gamma>)\<in>one_chain. path_image \<gamma>) (\<lambda>x. F x \<bullet> b)"
[PROOF STATE]
proof (prove)
using this:
continuous_on (\<Union> ((path_image \<circ> snd) ` one_chain)) (\<lambda>x. F x \<bullet> b)

goal (1 subgoal):
 1. continuous_on (\<Union>(k, \<gamma>)\<in>one_chain. path_image \<gamma>) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
by (auto simp add: Union_eq case_prod_beta)
[PROOF STATE]
proof (state)
this:
continuous_on (\<Union>(k, \<gamma>)\<in>one_chain. path_image \<gamma>) (\<lambda>x. F x \<bullet> b)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>b\<in>basis. continuous_on (\<Union>(k, \<gamma>)\<in>one_chain. path_image \<gamma>) (\<lambda>x. F x \<bullet> b)

goal (2 subgoals):
 1. line_integral F basis \<gamma> = one_chain_line_integral F basis one_chain
 2. 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]
proof (rule reparam_eq_line_integrals_basis[OF l_props(3) _ _  finite_basis])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. rec_join l piecewise_C1_differentiable_on {0..1}
 2. \<forall>b\<in>basis. continuous_on (path_image (rec_join l)) (\<lambda>x. F x \<bullet> b)
 3. \<forall>b\<in>basis. line_integral_exists F {b} (rec_join l)
[PROOF STEP]
let ?\<gamma>2.0="rec_join l"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. rec_join l piecewise_C1_differentiable_on {0..1}
 2. \<forall>b\<in>basis. continuous_on (path_image (rec_join l)) (\<lambda>x. F x \<bullet> b)
 3. \<forall>b\<in>basis. line_integral_exists F {b} (rec_join l)
[PROOF STEP]
show "?\<gamma>2.0 piecewise_C1_differentiable_on {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_join l piecewise_C1_differentiable_on {0..1}
[PROOF STEP]
apply(simp only: valid_path_def[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path (rec_join l)
[PROOF STEP]
apply(rule joined_is_valid)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. boundary_chain (set l)
 2. \<And>k \<gamma>. (k, \<gamma>) \<in> set l \<Longrightarrow> valid_path \<gamma>
 3. valid_chain_list l
[PROOF STEP]
using assms l_props
[PROOF STATE]
proof (prove)
using this:
chain_reparam_weak_path \<gamma> one_chain
boundary_chain one_chain
\<forall>b\<in>basis. \<forall>(k, \<gamma>)\<in>one_chain. line_integral_exists F {b} \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain. valid_path \<gamma>
finite basis
\<forall>b\<in>basis. \<forall>(k, \<gamma>2)\<in>one_chain. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
finite one_chain
set l = one_chain
distinct l
reparam \<gamma> (rec_join l)
valid_chain_list l
l \<noteq> []

goal (3 subgoals):
 1. boundary_chain (set l)
 2. \<And>k \<gamma>. (k, \<gamma>) \<in> set l \<Longrightarrow> valid_path \<gamma>
 3. valid_chain_list l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rec_join l piecewise_C1_differentiable_on {0..1}

goal (2 subgoals):
 1. \<forall>b\<in>basis. continuous_on (path_image (rec_join l)) (\<lambda>x. F x \<bullet> b)
 2. \<forall>b\<in>basis. line_integral_exists F {b} (rec_join l)
[PROOF STEP]
show "\<forall>b\<in>basis. continuous_on (path_image (rec_join l)) (\<lambda>x. F x \<bullet> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b\<in>basis. continuous_on (path_image (rec_join l)) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
using path_image_rec_join_2[OF l_props(5) l_props(4)] l_props(1)
[PROOF STATE]
proof (prove)
using this:
path_image (rec_join l) \<subseteq> (\<Union>(k, \<gamma>)\<in>set l. path_image \<gamma>)
set l = one_chain

goal (1 subgoal):
 1. \<forall>b\<in>basis. continuous_on (path_image (rec_join l)) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
using cont_forall continuous_on_subset
[PROOF STATE]
proof (prove)
using this:
path_image (rec_join l) \<subseteq> (\<Union>(k, \<gamma>)\<in>set l. path_image \<gamma>)
set l = one_chain
\<forall>b\<in>basis. continuous_on (\<Union>(k, \<gamma>)\<in>one_chain. path_image \<gamma>) (\<lambda>x. F x \<bullet> b)
\<lbrakk>continuous_on ?s ?f; ?t \<subseteq> ?s\<rbrakk> \<Longrightarrow> continuous_on ?t ?f

goal (1 subgoal):
 1. \<forall>b\<in>basis. continuous_on (path_image (rec_join l)) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>b\<in>basis. continuous_on (path_image (rec_join l)) (\<lambda>x. F x \<bullet> b)

goal (1 subgoal):
 1. \<forall>b\<in>basis. line_integral_exists F {b} (rec_join l)
[PROOF STEP]
show "\<forall>b\<in>basis. line_integral_exists F {b} (rec_join l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b\<in>basis. line_integral_exists F {b} (rec_join l)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b. b \<in> basis \<Longrightarrow> line_integral_exists F {b} (rec_join l)
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b. b \<in> basis \<Longrightarrow> line_integral_exists F {b} (rec_join l)
[PROOF STEP]
assume ass: "b\<in>basis"
[PROOF STATE]
proof (state)
this:
b \<in> basis

goal (1 subgoal):
 1. \<And>b. b \<in> basis \<Longrightarrow> line_integral_exists F {b} (rec_join l)
[PROOF STEP]
show "line_integral_exists F {b} (rec_join l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F {b} (rec_join l)
[PROOF STEP]
proof (rule line_integral_exists_on_rec_join)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. boundary_chain (set l)
 2. valid_chain_list l
 3. \<And>k \<gamma>. (k, \<gamma>) \<in> set l \<Longrightarrow> valid_path \<gamma>
 4. \<forall>(k, \<gamma>)\<in>set l. line_integral_exists F {b} \<gamma>
[PROOF STEP]
show "boundary_chain (set l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. boundary_chain (set l)
[PROOF STEP]
using l_props boundary_chain
[PROOF STATE]
proof (prove)
using this:
set l = one_chain
distinct l
reparam \<gamma> (rec_join l)
valid_chain_list l
l \<noteq> []
boundary_chain one_chain

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

goal (3 subgoals):
 1. valid_chain_list l
 2. \<And>k \<gamma>. (k, \<gamma>) \<in> set l \<Longrightarrow> valid_path \<gamma>
 3. \<forall>(k, \<gamma>)\<in>set l. line_integral_exists F {b} \<gamma>
[PROOF STEP]
show "valid_chain_list l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_chain_list l
[PROOF STEP]
using l_props
[PROOF STATE]
proof (prove)
using this:
set l = one_chain
distinct l
reparam \<gamma> (rec_join l)
valid_chain_list l
l \<noteq> []

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

goal (2 subgoals):
 1. \<And>k \<gamma>. (k, \<gamma>) \<in> set l \<Longrightarrow> valid_path \<gamma>
 2. \<forall>(k, \<gamma>)\<in>set l. line_integral_exists F {b} \<gamma>
[PROOF STEP]
show "\<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 l_props assms
[PROOF STATE]
proof (prove)
using this:
set l = one_chain
distinct l
reparam \<gamma> (rec_join l)
valid_chain_list l
l \<noteq> []
chain_reparam_weak_path \<gamma> one_chain
boundary_chain one_chain
\<forall>b\<in>basis. \<forall>(k, \<gamma>)\<in>one_chain. line_integral_exists F {b} \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain. valid_path \<gamma>
finite basis
\<forall>b\<in>basis. \<forall>(k, \<gamma>2)\<in>one_chain. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
finite one_chain

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. \<forall>(k, \<gamma>)\<in>set l. line_integral_exists F {b} \<gamma>
[PROOF STEP]
show "\<forall>(k, \<gamma>)\<in>set l. line_integral_exists F {b} \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>set l. line_integral_exists F {b} \<gamma>
[PROOF STEP]
using l_props line_integral_exists ass
[PROOF STATE]
proof (prove)
using this:
set l = one_chain
distinct l
reparam \<gamma> (rec_join l)
valid_chain_list l
l \<noteq> []
\<forall>b\<in>basis. \<forall>(k, \<gamma>)\<in>one_chain. line_integral_exists F {b} \<gamma>
b \<in> basis

goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>set l. line_integral_exists F {b} \<gamma>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>(k, \<gamma>)\<in>set l. line_integral_exists F {b} \<gamma>

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>b\<in>basis. line_integral_exists F {b} (rec_join l)

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

goal (1 subgoal):
 1. line_integral F basis \<gamma> = one_chain_line_integral F basis one_chain
[PROOF STEP]
show "line_integral F basis \<gamma> = one_chain_line_integral F basis one_chain"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis \<gamma> = one_chain_line_integral F basis one_chain
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. line_integral F basis \<gamma> = one_chain_line_integral F basis one_chain
[PROOF STEP]
have i: "line_integral F basis (rec_join l) = one_chain_line_integral F basis one_chain"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis (rec_join l) = one_chain_line_integral F basis one_chain
[PROOF STEP]
proof (rule one_chain_line_integral_rec_join)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. set l = one_chain
 2. distinct l
 3. valid_chain_list l
 4. boundary_chain one_chain
 5. \<forall>(k, \<gamma>)\<in>one_chain. line_integral_exists F basis \<gamma>
 6. \<forall>(k, \<gamma>)\<in>one_chain. valid_path \<gamma>
 7. finite basis
[PROOF STEP]
show "set l = one_chain" "distinct l" "valid_chain_list l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set l = one_chain &&& distinct l &&& valid_chain_list l
[PROOF STEP]
using l_props
[PROOF STATE]
proof (prove)
using this:
set l = one_chain
distinct l
reparam \<gamma> (rec_join l)
valid_chain_list l
l \<noteq> []

goal (1 subgoal):
 1. set l = one_chain &&& distinct l &&& valid_chain_list l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set l = one_chain
distinct l
valid_chain_list l

goal (4 subgoals):
 1. boundary_chain one_chain
 2. \<forall>(k, \<gamma>)\<in>one_chain. line_integral_exists F basis \<gamma>
 3. \<forall>(k, \<gamma>)\<in>one_chain. valid_path \<gamma>
 4. finite basis
[PROOF STEP]
show "boundary_chain one_chain"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. boundary_chain one_chain
[PROOF STEP]
using boundary_chain
[PROOF STATE]
proof (prove)
using this:
boundary_chain one_chain

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

goal (3 subgoals):
 1. \<forall>(k, \<gamma>)\<in>one_chain. line_integral_exists F basis \<gamma>
 2. \<forall>(k, \<gamma>)\<in>one_chain. valid_path \<gamma>
 3. finite basis
[PROOF STEP]
show "\<forall>(k, \<gamma>)\<in>one_chain. line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain. line_integral_exists F basis \<gamma>
[PROOF STEP]
using line_integral_sum_basis(2)[OF finite_basis] line_integral_exists
[PROOF STATE]
proof (prove)
using this:
\<forall>b\<in>basis. line_integral_exists ?F {b} ?\<gamma> \<Longrightarrow> line_integral_exists ?F basis ?\<gamma>
\<forall>b\<in>basis. \<forall>(k, \<gamma>)\<in>one_chain. line_integral_exists F {b} \<gamma>

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

goal (2 subgoals):
 1. \<forall>(k, \<gamma>)\<in>one_chain. valid_path \<gamma>
 2. finite basis
[PROOF STEP]
show "\<forall>(k, \<gamma>)\<in>one_chain. valid_path \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain. valid_path \<gamma>
[PROOF STEP]
using valid_path
[PROOF STATE]
proof (prove)
using this:
\<forall>(k, \<gamma>)\<in>one_chain. valid_path \<gamma>

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

goal (1 subgoal):
 1. finite basis
[PROOF STEP]
show "finite basis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite basis
[PROOF STEP]
using finite_basis
[PROOF STATE]
proof (prove)
using this:
finite basis

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

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

goal (1 subgoal):
 1. line_integral F basis \<gamma> = one_chain_line_integral F basis one_chain
[PROOF STEP]
have ii: "line_integral F basis \<gamma> = line_integral F basis (rec_join l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis \<gamma> = line_integral F basis (rec_join l)
[PROOF STEP]
proof (rule reparam_eq_line_integrals_basis[OF l_props(3) _ _  finite_basis])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. rec_join l piecewise_C1_differentiable_on {0..1}
 2. \<forall>b\<in>basis. continuous_on (path_image (rec_join l)) (\<lambda>x. F x \<bullet> b)
 3. \<forall>b\<in>basis. line_integral_exists F {b} (rec_join l)
[PROOF STEP]
let ?\<gamma>2.0="rec_join l"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. rec_join l piecewise_C1_differentiable_on {0..1}
 2. \<forall>b\<in>basis. continuous_on (path_image (rec_join l)) (\<lambda>x. F x \<bullet> b)
 3. \<forall>b\<in>basis. line_integral_exists F {b} (rec_join l)
[PROOF STEP]
show "?\<gamma>2.0 piecewise_C1_differentiable_on {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_join l piecewise_C1_differentiable_on {0..1}
[PROOF STEP]
apply(simp only: valid_path_def[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path (rec_join l)
[PROOF STEP]
apply(rule joined_is_valid)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. boundary_chain (set l)
 2. \<And>k \<gamma>. (k, \<gamma>) \<in> set l \<Longrightarrow> valid_path \<gamma>
 3. valid_chain_list l
[PROOF STEP]
using assms l_props
[PROOF STATE]
proof (prove)
using this:
chain_reparam_weak_path \<gamma> one_chain
boundary_chain one_chain
\<forall>b\<in>basis. \<forall>(k, \<gamma>)\<in>one_chain. line_integral_exists F {b} \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain. valid_path \<gamma>
finite basis
\<forall>b\<in>basis. \<forall>(k, \<gamma>2)\<in>one_chain. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
finite one_chain
set l = one_chain
distinct l
reparam \<gamma> (rec_join l)
valid_chain_list l
l \<noteq> []

goal (3 subgoals):
 1. boundary_chain (set l)
 2. \<And>k \<gamma>. (k, \<gamma>) \<in> set l \<Longrightarrow> valid_path \<gamma>
 3. valid_chain_list l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rec_join l piecewise_C1_differentiable_on {0..1}

goal (2 subgoals):
 1. \<forall>b\<in>basis. continuous_on (path_image (rec_join l)) (\<lambda>x. F x \<bullet> b)
 2. \<forall>b\<in>basis. line_integral_exists F {b} (rec_join l)
[PROOF STEP]
show "\<forall>b\<in>basis. continuous_on (path_image (rec_join l)) (\<lambda>x. F x \<bullet> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b\<in>basis. continuous_on (path_image (rec_join l)) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
using path_image_rec_join_2[OF l_props(5) l_props(4)] l_props(1)
[PROOF STATE]
proof (prove)
using this:
path_image (rec_join l) \<subseteq> (\<Union>(k, \<gamma>)\<in>set l. path_image \<gamma>)
set l = one_chain

goal (1 subgoal):
 1. \<forall>b\<in>basis. continuous_on (path_image (rec_join l)) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
using cont_forall continuous_on_subset
[PROOF STATE]
proof (prove)
using this:
path_image (rec_join l) \<subseteq> (\<Union>(k, \<gamma>)\<in>set l. path_image \<gamma>)
set l = one_chain
\<forall>b\<in>basis. continuous_on (\<Union>(k, \<gamma>)\<in>one_chain. path_image \<gamma>) (\<lambda>x. F x \<bullet> b)
\<lbrakk>continuous_on ?s ?f; ?t \<subseteq> ?s\<rbrakk> \<Longrightarrow> continuous_on ?t ?f

goal (1 subgoal):
 1. \<forall>b\<in>basis. continuous_on (path_image (rec_join l)) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>b\<in>basis. continuous_on (path_image (rec_join l)) (\<lambda>x. F x \<bullet> b)

goal (1 subgoal):
 1. \<forall>b\<in>basis. line_integral_exists F {b} (rec_join l)
[PROOF STEP]
show "\<forall>b\<in>basis. line_integral_exists F {b} (rec_join l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b\<in>basis. line_integral_exists F {b} (rec_join l)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b. b \<in> basis \<Longrightarrow> line_integral_exists F {b} (rec_join l)
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b. b \<in> basis \<Longrightarrow> line_integral_exists F {b} (rec_join l)
[PROOF STEP]
assume ass: "b\<in>basis"
[PROOF STATE]
proof (state)
this:
b \<in> basis

goal (1 subgoal):
 1. \<And>b. b \<in> basis \<Longrightarrow> line_integral_exists F {b} (rec_join l)
[PROOF STEP]
show "line_integral_exists F {b} (rec_join l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F {b} (rec_join l)
[PROOF STEP]
proof (rule line_integral_exists_on_rec_join)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. boundary_chain (set l)
 2. valid_chain_list l
 3. \<And>k \<gamma>. (k, \<gamma>) \<in> set l \<Longrightarrow> valid_path \<gamma>
 4. \<forall>(k, \<gamma>)\<in>set l. line_integral_exists F {b} \<gamma>
[PROOF STEP]
show "boundary_chain (set l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. boundary_chain (set l)
[PROOF STEP]
using l_props boundary_chain
[PROOF STATE]
proof (prove)
using this:
set l = one_chain
distinct l
reparam \<gamma> (rec_join l)
valid_chain_list l
l \<noteq> []
boundary_chain one_chain

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

goal (3 subgoals):
 1. valid_chain_list l
 2. \<And>k \<gamma>. (k, \<gamma>) \<in> set l \<Longrightarrow> valid_path \<gamma>
 3. \<forall>(k, \<gamma>)\<in>set l. line_integral_exists F {b} \<gamma>
[PROOF STEP]
show "valid_chain_list l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_chain_list l
[PROOF STEP]
using l_props
[PROOF STATE]
proof (prove)
using this:
set l = one_chain
distinct l
reparam \<gamma> (rec_join l)
valid_chain_list l
l \<noteq> []

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

goal (2 subgoals):
 1. \<And>k \<gamma>. (k, \<gamma>) \<in> set l \<Longrightarrow> valid_path \<gamma>
 2. \<forall>(k, \<gamma>)\<in>set l. line_integral_exists F {b} \<gamma>
[PROOF STEP]
show "\<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 l_props assms
[PROOF STATE]
proof (prove)
using this:
set l = one_chain
distinct l
reparam \<gamma> (rec_join l)
valid_chain_list l
l \<noteq> []
chain_reparam_weak_path \<gamma> one_chain
boundary_chain one_chain
\<forall>b\<in>basis. \<forall>(k, \<gamma>)\<in>one_chain. line_integral_exists F {b} \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain. valid_path \<gamma>
finite basis
\<forall>b\<in>basis. \<forall>(k, \<gamma>2)\<in>one_chain. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
finite one_chain

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. \<forall>(k, \<gamma>)\<in>set l. line_integral_exists F {b} \<gamma>
[PROOF STEP]
show "\<forall>(k, \<gamma>)\<in>set l. line_integral_exists F {b} \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>set l. line_integral_exists F {b} \<gamma>
[PROOF STEP]
using l_props line_integral_exists ass
[PROOF STATE]
proof (prove)
using this:
set l = one_chain
distinct l
reparam \<gamma> (rec_join l)
valid_chain_list l
l \<noteq> []
\<forall>b\<in>basis. \<forall>(k, \<gamma>)\<in>one_chain. line_integral_exists F {b} \<gamma>
b \<in> basis

goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>set l. line_integral_exists F {b} \<gamma>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>(k, \<gamma>)\<in>set l. line_integral_exists F {b} \<gamma>

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>b\<in>basis. line_integral_exists F {b} (rec_join l)

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
line_integral F basis \<gamma> = one_chain_line_integral F basis one_chain

goal:
No subgoals!
[PROOF STEP]
qed


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

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