Theory Paths

theory Paths
  imports Derivs General_Utils Integrals
begin
(*This has everything related to paths purely*)

lemma reverse_subpaths_join:
  shows " subpath 1 (1 / 2) p +++ subpath (1 / 2) 0 p = reversepath p"
  using reversepath_subpath join_subpaths_middle pathfinish_subpath pathstart_subpath reversepath_joinpaths
  by (metis (no_types, lifting))


(*Below F cannot be from 'a ⇒ 'b because the dot product won't work.
  We have that g returns 'a and then F takes the output of g, so F should start from 'a
  Then we have to compute the dot product of the vector b with both the derivative of g, and F.
  Since the derivative of g returns the same type as g, accordingly F should return the same type as g, i.e. 'a.
 *)
definition line_integral:: "('a::euclidean_space ⇒ 'a::euclidean_space) ⇒ (('a) set) ⇒ (real ⇒ 'a) ⇒ real" where
"line_integral F basis g ≡ integral {0 .. 1} (λx. ∑b∈basis. (F(g x) ∙ b) * (vector_derivative g (at x within {0..1}) ∙ b))"

definition line_integral_exists where
  "line_integral_exists F basis γ ≡ (λx. ∑b∈basis. F(γ x) ∙ b * (vector_derivative γ (at x within {0..1}) ∙ b)) integrable_on {0..1}"

lemma line_integral_on_pair_straight_path:
  fixes F::"('a::euclidean_space) ⇒ 'a" and g :: "real ⇒ real" and γ
  assumes gamma_const: "∀x. γ(x)∙ i = a"
      and gamma_smooth: "∀x ∈ {0 .. 1}. γ differentiable at x"          
  shows "(line_integral F {i} γ) = 0" "(line_integral_exists F {i} γ)"
proof (simp add: line_integral_def)
  have *: "F (γ x) ∙ i * (vector_derivative γ (at x within {0..1}) ∙ i) = 0"
    if "0 ≤ x ∧ x ≤ 1" for x
  proof -
    have "((λx. γ(x)∙ i) has_vector_derivative 0) (at x)"
      using vector_derivative_const_at[of "a" "x"] and gamma_const
      by auto
    then have "(vector_derivative γ (at x) ∙ i) = 0"
      using derivative_component_fun_component[ of "γ" "x" "i"]
        and gamma_smooth and that
      by (simp add: vector_derivative_at)
    then have "(vector_derivative γ (at x within {0 .. 1}) ∙ i) = 0"
      using has_vector_derivative_at_within vector_derivative_at_within_ivl that
      by (metis atLeastAtMost_iff gamma_smooth vector_derivative_works zero_less_one)
    then show ?thesis
      by auto
  qed
  then have "((λx. F (γ x) ∙ i * (vector_derivative γ (at x within {0..1}) ∙ i)) has_integral 0) {0..1}"
    using has_integral_is_0[of "{0 .. 1}" "(λx. F (γ x) ∙ i * (vector_derivative γ (at x within {0..1}) ∙ i))"]
    by auto
  then have "((λx. F (γ x) ∙ i * (vector_derivative γ (at x within {0..1}) ∙ i)) integrable_on {0..1})"
    by auto
  then show "line_integral_exists F {i} γ" by (auto simp add:line_integral_exists_def)
  show "integral {0..1} (λx. F (γ x) ∙ i * (vector_derivative γ (at x within {0..1}) ∙ i)) = 0"
    using * has_integral_is_0[of "{0 .. 1}" "(λx. F (γ x) ∙ i * (vector_derivative γ (at x within {0..1}) ∙ i))"]
    by auto
qed

lemma line_integral_on_pair_path_strong:
  fixes F::"('a::euclidean_space) ⇒ ('a)" and
    g::"real ⇒ 'a" and
    γ::"(real ⇒ 'a)" and
    i::'a 
  assumes i_norm_1: "norm i = 1" and
    g_orthogonal_to_i: "∀x. g(x) ∙ i = 0" and  
    gamma_is_in_terms_of_i: "γ = (λx. f(x) *⇩R i + g(f(x)))" and
    gamma_smooth: "γ piecewise_C1_differentiable_on {0 .. 1}" and
    g_continuous_on_f: "continuous_on (f ` {0..1}) g" and
    path_start_le_path_end: "(pathstart γ) ∙ i ≤ (pathfinish γ) ∙ i" and
    field_i_comp_cont: "continuous_on (path_image γ) (λx. F x ∙ i)"
  shows "line_integral F {i} γ 
         = integral (cbox ((pathstart γ) ∙ i) ((pathfinish γ) ∙ i)) (λf_var. (F (f_var *⇩R i + g(f_var)) ∙ i))"
    "line_integral_exists F {i} γ"
proof (simp add: line_integral_def)
  obtain s where gamma_differentiable: "finite s" "(∀x ∈ {0 .. 1} - s. γ differentiable at x)"
    using gamma_smooth
    by (auto simp add: C1_differentiable_on_eq piecewise_C1_differentiable_on_def)
  then have gamma_i_component_smooth: "∀x ∈ {0 .. 1} - s. (λx. γ x ∙ i) differentiable at x"
    by auto
  have field_cont_on_path: "continuous_on ((λx. γ x ∙ i) ` {0..1}) (λf_var. F (f_var *⇩R i + g f_var) ∙ i)"
  proof - 
    have 0: "(λx. γ x ∙ i) = f"
    proof 
      fix x
      show "γ x ∙ i = f x"
        using g_orthogonal_to_i i_norm_1
        by (simp only: gamma_is_in_terms_of_i  real_inner_class.inner_add_left g_orthogonal_to_i inner_scaleR_left inner_same_Basis norm_eq_1)
    qed
    show ?thesis 
      unfolding 0 
      apply (rule continuous_on_compose2 [of _ "(λx. F(x)  ∙ i)" "f ` { 0..1}" "(λx. x *⇩R i + g x)"]
          field_i_comp_cont g_continuous_on_f field_i_comp_cont continuous_intros)+
      by (auto simp add: gamma_is_in_terms_of_i path_image_def)
  qed
  have path_start_le_path_end': "γ 0 ∙ i ≤ γ 1 ∙ i" using path_start_le_path_end by (auto simp add: pathstart_def pathfinish_def)
  have gamm_cont: "continuous_on {0..1} (λa. γ a ∙ i)"
    apply(rule continuous_on_inner)
    using gamma_smooth 
     apply (simp add: piecewise_C1_differentiable_on_def)
    using continuous_on_const by auto
  then obtain c d where cd: "c ≤ d" "(λa. γ a ∙ i) ` {0..1} = {c..d}"
    by (meson continuous_image_closed_interval zero_le_one)
  then have subset_cd: "(λa. γ a ∙ i) ` {0..1} ⊆ {c..d}" by auto
  have field_cont_on_path_cd:
    "continuous_on {c..d} (λf_var. F (f_var *⇩R i + g f_var) ∙ i)"
    using field_cont_on_path cd by auto
  have path_vector_deriv_line_integrals:
    "∀x∈{0..1} - s. ((λx. γ x ∙ i) has_vector_derivative 
                                          vector_derivative (λx. γ x ∙ i) (at x))
                                                  (at x)"
    using gamma_i_component_smooth and derivative_component_fun_component and
      vector_derivative_works
    by blast       
  then have "∀x∈{0..1} - s. ((λx. γ x ∙ i) has_vector_derivative 
                                          vector_derivative (λx. γ x ∙ i) (at x within ({0..1})))
                                                  (at x within ({0..1}))"
    using has_vector_derivative_at_within vector_derivative_at_within_ivl
    by fastforce
  then have has_int:"((λx. vector_derivative (λx. γ x ∙ i) (at x within {0..1}) *⇩R (F ((γ x ∙ i) *⇩R i + g (γ x ∙ i)) ∙ i)) has_integral
           integral {γ 0 ∙ i..γ 1 ∙ i} (λf_var. F (f_var *⇩R i + g f_var) ∙ i)) {0..1}"
    using has_integral_substitution_strong[OF gamma_differentiable(1) rel_simps(44)
        path_start_le_path_end' subset_cd field_cont_on_path_cd gamm_cont,
        of "(λx. vector_derivative (λx. γ(x) ∙ i) (at x within ({0..1})))"]
      gamma_is_in_terms_of_i
    by (auto simp only: has_real_derivative_iff_has_vector_derivative)
  then have has_int':"((λx. (F(γ(x)) ∙ i)*(vector_derivative (λx. γ(x) ∙ i) (at x within ({0..1})))) has_integral
           integral {((pathstart γ) ∙ i)..((pathfinish γ) ∙ i)} (λf_var. F (f_var *⇩R i + g f_var) ∙ i)) {0..1}"
    using  gamma_is_in_terms_of_i i_norm_1
    apply (auto simp add: pathstart_def pathfinish_def)
    apply (simp only:  real_inner_class.inner_add_left inner_not_same_Basis g_orthogonal_to_i inner_scaleR_left norm_eq_1)
    by (auto simp add: algebra_simps)
  have substitute:
    "integral ({((pathstart γ) ∙ i)..((pathfinish γ) ∙ i)}) (λf_var. (F (f_var *⇩R i + g(f_var)) ∙ i)) 
                 = integral ({0..1}) (λx. (F(γ(x)) ∙ i)*(vector_derivative (λx. γ(x) ∙ i) (at x within ({0..1}))))"
    using gamma_is_in_terms_of_i integral_unique[OF has_int] i_norm_1
    apply (auto simp add: pathstart_def pathfinish_def)
    apply (simp only:  real_inner_class.inner_add_left inner_not_same_Basis g_orthogonal_to_i inner_scaleR_left norm_eq_1)
    by (auto simp add: algebra_simps)
  have comp_in_eq_comp_out: "∀x ∈ {0..1} - s.
            (vector_derivative (λx. γ(x) ∙ i) (at x within {0..1}))
                = (vector_derivative γ (at x within {0..1})) ∙ i"
  proof
    fix x:: real
    assume ass:"x ∈ {0..1} -s"
    then have x_bounds:"x ∈ {0..1}" by auto
    have "γ differentiable at x" using ass gamma_differentiable by auto
    then have dotprod_in_is_out:
      "vector_derivative (λx. γ(x) ∙ i) (at x)
                         = (vector_derivative γ (at x)) ∙ i"
      using derivative_component_fun_component 
      by force
    then have 0: "(vector_derivative γ (at x)) ∙ i = (vector_derivative γ (at x within {0..1})) ∙ i"
    proof -
      have "(γ has_vector_derivative vector_derivative γ (at x)) (at x)"
        using ‹γ differentiable at x› vector_derivative_works by blast
      moreover have "0 ≤ x ∧ x ≤ 1"
        using x_bounds by presburger
      ultimately show ?thesis
        by (simp add: vector_derivative_at_within_ivl)
    qed
    have 1: "vector_derivative (λx. γ(x) ∙ i) (at x) = vector_derivative (λx. γ(x) ∙ i) (at x within {0..1})"
      using path_vector_deriv_line_integrals and vector_derivative_at_within_ivl and
        x_bounds
      by (metis ass atLeastAtMost_iff zero_less_one)
    show "vector_derivative (λx. γ x ∙ i) (at x within {0..1}) = vector_derivative γ (at x within {0..1}) ∙ i"
      using 0 and 1 and dotprod_in_is_out
      by auto
  qed
  show "integral {0..1} (λx. F (γ x) ∙ i * (vector_derivative γ (at x within {0..1}) ∙ i)) =
                   integral {pathstart γ ∙ i..pathfinish γ ∙ i} (λf_var. F (f_var *⇩R i + g f_var) ∙ i)"
    using substitute and comp_in_eq_comp_out and negligible_finite
      Henstock_Kurzweil_Integration.integral_spike
      [of "s" "{0..1}" "(λx. F (γ x) ∙ i * (vector_derivative γ (at x within {0..1}) ∙ i))"
        "(λx. F (γ x) ∙ i * vector_derivative (λx. γ x ∙ i) (at x within {0..1}))"]
    by (metis (no_types, lifting) gamma_differentiable(1))
  have "((λx. F (γ x) ∙ i * (vector_derivative γ (at x within {0..1}) ∙ i)) has_integral
                   integral {pathstart γ ∙ i..pathfinish γ ∙ i} (λf_var. F (f_var *⇩R i + g f_var) ∙ i)) {0..1}"
    using has_int' and comp_in_eq_comp_out and negligible_finite
      Henstock_Kurzweil_Integration.has_integral_spike
      [of "s" "{0..1}" "(λx. F (γ x) ∙ i * (vector_derivative γ (at x within {0..1}) ∙ i))"
        "(λx. F (γ x) ∙ i * vector_derivative (λx. γ x ∙ i) (at x within {0..1}))"
        "integral {pathstart γ ∙ i..pathfinish γ ∙ i} (λf_var. F (f_var *⇩R i + g f_var) ∙ i)"]
    by (metis (no_types, lifting) gamma_differentiable(1))
  then have "(λx. F (γ x) ∙ i * (vector_derivative γ (at x within {0..1}) ∙ i)) integrable_on {0..1}"
    using integrable_on_def by auto
  then show "line_integral_exists F {i} γ"
    by (auto simp add: line_integral_exists_def)
qed

lemma line_integral_on_pair_path:
  fixes F::"('a::euclidean_space) ⇒ ('a)" and
    g::"real ⇒ 'a" and
    γ::"(real ⇒ 'a)" and
    i::'a 
  assumes i_norm_1: "norm i = 1" and
    g_orthogonal_to_i: "∀x. g(x) ∙ i = 0" and  
    gamma_is_in_terms_of_i: "γ = (λx. f(x) *⇩R i + g(f(x)))" and
    gamma_smooth: "γ C1_differentiable_on {0 .. 1}" and
    g_continuous_on_f: "continuous_on (f ` {0..1}) g" and
    path_start_le_path_end: "(pathstart γ) ∙ i ≤ (pathfinish γ) ∙ i" and
    field_i_comp_cont: "continuous_on (path_image γ) (λx. F x ∙ i)"
  shows "(line_integral F {i} γ) 
                 = integral (cbox ((pathstart γ) ∙ i) ((pathfinish γ) ∙ i)) (λf_var. (F (f_var *⇩R i + g(f_var)) ∙ i))"
proof (simp add: line_integral_def)
  have gamma_differentiable: "∀x ∈ {0 .. 1}. γ differentiable at x"
    using gamma_smooth  C1_differentiable_on_eq by blast
  then have gamma_i_component_smooth:
    "∀x ∈ {0 .. 1}. (λx. γ x ∙ i) differentiable at x"
    by auto
  have vec_deriv_i_comp_cont:
    "continuous_on {0..1} (λx. vector_derivative (λx. γ x ∙ i) (at x within {0..1}))"
  proof -
    have "continuous_on {0..1} (λx. vector_derivative (λx. γ x) (at x within {0..1}))"
      using gamma_smooth C1_differentiable_on_eq
      by (smt C1_differentiable_on_def atLeastAtMost_iff continuous_on_eq vector_derivative_at_within_ivl)
    then have deriv_comp_cont:
      "continuous_on {0..1} (λx. vector_derivative (λx. γ x) (at x within {0..1}) ∙ i)"
      by (simp add: continuous_intros)
    show ?thesis
      using derivative_component_fun_component_at_within[OF gamma_differentiable, of "i"]                    
        continuous_on_eq[OF deriv_comp_cont, of "(λx. vector_derivative (λx. γ x ∙ i) (at x within {0..1}))"]
      by fastforce
  qed
  have field_cont_on_path:
    "continuous_on ((λx. γ x ∙ i) ` {0..1}) (λf_var. F (f_var *⇩R i + g f_var) ∙ i)"
  proof - 
    have 0: "(λx. γ x ∙ i) = f"
    proof 
      fix x
      show "γ x ∙ i = f x"
        using g_orthogonal_to_i i_norm_1
        by (simp only: gamma_is_in_terms_of_i  real_inner_class.inner_add_left g_orthogonal_to_i inner_scaleR_left inner_same_Basis norm_eq_1)
    qed
    show ?thesis 
      unfolding 0 
      apply (rule continuous_on_compose2 [of _ "(λx. F(x)  ∙ i)" "f ` { 0..1}" "(λx. x *⇩R i + g x)"]
          field_i_comp_cont g_continuous_on_f field_i_comp_cont continuous_intros)+
      by (auto simp add: gamma_is_in_terms_of_i path_image_def)
  qed
  have path_vector_deriv_line_integrals:
    "∀x∈{0..1}. ((λx. γ x ∙ i) has_vector_derivative 
                                          vector_derivative (λx. γ x ∙ i) (at x))
                                                  (at x)"
    using gamma_i_component_smooth and derivative_component_fun_component and
      vector_derivative_works
    by blast       
  then have "∀x∈{0..1}. ((λx. γ x ∙ i) has_vector_derivative 
                                          vector_derivative (λx. γ x ∙ i) (at x within {0..1}))
                                                  (at x within {0..1})"
    using has_vector_derivative_at_within vector_derivative_at_within_ivl
    by fastforce
  then have substitute:
    "integral (cbox ((pathstart γ) ∙ i) ((pathfinish γ) ∙ i)) (λf_var. (F (f_var *⇩R i + g(f_var)) ∙ i)) 
                 = integral (cbox 0 1) (λx. (F(γ(x)) ∙ i)*(vector_derivative (λx. γ(x) ∙ i) (at x within {0..1})))"
    using gauge_integral_by_substitution
      [of "0" "1" "(λx. (γ x) ∙ i)"
        "(λx. vector_derivative (λx. γ(x) ∙ i) (at x within {0..1}))"
        "(λf_var. (F (f_var *⇩R i + g(f_var)) ∙ i))"] and
      path_start_le_path_end and vec_deriv_i_comp_cont and field_cont_on_path and 
      gamma_is_in_terms_of_i i_norm_1
    apply (auto simp add: pathstart_def pathfinish_def)
    apply (simp only:  real_inner_class.inner_add_left inner_not_same_Basis g_orthogonal_to_i inner_scaleR_left norm_eq_1)
    by (auto)
      (*integration by substitution*)
  have comp_in_eq_comp_out: "∀x ∈ {0..1}.
            (vector_derivative (λx. γ(x) ∙ i) (at x within {0..1}))
                = (vector_derivative γ (at x within {0..1})) ∙ i"
  proof
    fix x:: real
    assume x_bounds: "x ∈ {0..1}"
    then have "γ differentiable at x" using gamma_differentiable by auto
    then have dotprod_in_is_out:
      "vector_derivative (λx. γ(x) ∙ i) (at x)
                         = (vector_derivative γ (at x)) ∙ i"
      using derivative_component_fun_component 
      by force
    then have 0: "(vector_derivative γ (at x)) ∙ i
                         = (vector_derivative γ (at x within {0..1})) ∙ i"
      using has_vector_derivative_at_within and x_bounds and vector_derivative_at_within_ivl
      by (smt atLeastAtMost_iff gamma_differentiable inner_commute vector_derivative_works)
    have 1: "vector_derivative (λx. γ(x) ∙ i) (at x) = vector_derivative (λx. γ(x) ∙ i) (at x within {0..1})"
      using path_vector_deriv_line_integrals and vector_derivative_at_within_ivl and
        x_bounds
      by fastforce
    show "vector_derivative (λx. γ x ∙ i) (at x within {0..1}) = vector_derivative γ (at x within {0..1}) ∙ i"
      using 0 and 1 and dotprod_in_is_out
      by auto
  qed
  show "integral {0..1} (λx. F (γ x) ∙ i * (vector_derivative γ (at x within {0..1}) ∙ i)) =
                   integral {pathstart γ ∙ i..pathfinish γ ∙ i} (λf_var. F (f_var *⇩R i + g f_var) ∙ i)"
    using substitute and comp_in_eq_comp_out and 
      Henstock_Kurzweil_Integration.integral_cong
      [of "{0..1}" "(λx. F (γ x) ∙ i * (vector_derivative γ (at x within {0..1}) ∙ i))"
        "(λx. F (γ x) ∙ i * vector_derivative (λx. γ x ∙ i) (at x within {0..1}))"]
    by auto
qed

lemma content_box_cases:
  "content (box a b) = (if ∀i∈Basis. a∙i ≤ b∙i then prod (λi. b∙i - a∙i) Basis else 0)"
  by (simp add: measure_lborel_box_eq inner_diff)

lemma content_box_cbox:
  shows "content (box a b) = content (cbox a b)"
  by (simp add: content_box_cases content_cbox_cases)

lemma content_eq_0: "content (box a b) = 0 ⟷ (∃i∈Basis. b∙i ≤ a∙i)"
  by (auto simp: content_box_cases not_le intro: less_imp_le antisym eq_refl)

lemma content_pos_lt_eq: "0 < content (cbox a (b::'a::euclidean_space)) ⟷ (∀i∈Basis. a∙i < b∙i)"
  by (auto simp add: content_cbox_cases less_le prod_nonneg)

lemma content_lt_nz: "0 < content (box a b) ⟷ content (box a b) ≠ 0"
  using Paths.content_eq_0 zero_less_measure_iff by blast

lemma content_subset: "cbox a b ⊆ box c d ⟹ content (cbox a b) ≤ content (box c d)"
  unfolding measure_def
  by (intro enn2real_mono emeasure_mono) (auto simp: emeasure_lborel_cbox_eq emeasure_lborel_box_eq)

lemma sum_content_null:
  assumes "content (box a b) = 0"
    and "p tagged_division_of (box a b)"
  shows "sum (λ(x,k). content k *⇩R f x) p = (0::'a::real_normed_vector)"
proof (rule sum.neutral, rule)
  fix y
  assume y: "y ∈ p"
  obtain x k where xk: "y = (x, k)"
    using surj_pair[of y] by blast
  note assm = tagged_division_ofD(3-4)[OF assms(2) y[unfolded xk]]
  from this(2) obtain c d where k: "k = cbox c d" by blast
  have "(λ(x, k). content k *⇩R f x) y = content k *⇩R f x"
    unfolding xk by auto
  also have "… = 0"
    using content_subset[OF assm(1)[unfolded k]] content_pos_le[of "cbox c d"]
    unfolding assms(1) k
    by auto
  finally show "(λ(x, k). content k *⇩R f x) y = 0" .
qed


lemma has_integral_null [intro]: "content(box a b) = 0 ⟹ (f has_integral 0) (box a b)"
  by (simp add: content_box_cbox content_eq_0_interior)

lemma line_integral_distrib:
  assumes "line_integral_exists f basis g1"
    "line_integral_exists f basis g2"
    "valid_path g1" "valid_path g2"
  shows "line_integral f basis (g1 +++ g2) = line_integral f basis g1 + line_integral f basis g2"
    "line_integral_exists f basis (g1 +++ g2)"
proof -
  obtain s1 s2
    where s1: "finite s1" "∀x∈{0..1} - s1. g1 differentiable at x"
      and s2: "finite s2" "∀x∈{0..1} - s2. g2 differentiable at x"
    using assms
    by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
  obtain i1 i2
    where 1: "((λx. ∑b∈basis. f (g1 x) ∙ b * (vector_derivative g1 (at x within {0..1}) ∙ b)) has_integral i1) {0..1}"
      and 2: "((λx. ∑b∈basis. f (g2 x) ∙ b * (vector_derivative g2 (at x within {0..1}) ∙ b)) has_integral i2) {0..1}"
    using assms
    by (auto simp: line_integral_exists_def)
  have i1: "((λx. 2 * (∑b∈basis. f (g1 (2 * x)) ∙ b * (vector_derivative g1 (at (2 * x) within {0..1}) ∙ b))) has_integral i1) {0..1/2}"
   and i2: "((λx. 2 * (∑b∈basis. f (g2 (2 * x - 1)) ∙ b * (vector_derivative g2 (at ((2 * x) - 1) within {0..1}) ∙ b))) has_integral i2) {1/2..1}"
    using has_integral_affinity01 [OF 1, where m= 2 and c=0, THEN has_integral_cmul [where c=2]]
      has_integral_affinity01 [OF 2, where m= 2 and c="-1", THEN has_integral_cmul [where c=2]]
    by (simp_all only: image_affinity_atLeastAtMost_div_diff, simp_all add: scaleR_conv_of_real mult_ac)
  have g1: "⟦0 ≤ z; z*2 < 1; z*2 ∉ s1⟧ ⟹
            vector_derivative (λx. if x*2 ≤ 1 then g1 (2*x) else g2 (2*x - 1)) (at z within {0..1}) =
            2 *⇩R vector_derivative g1 (at (z*2) within {0..1})" for z
  proof -
    have i:"⟦0 ≤ z; z*2 < 1; z*2 ∉ s1⟧ ⟹
              vector_derivative (λx. if x * 2 ≤ 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *⇩R vector_derivative g1 (at (z * 2))" for z
    proof-
      have g1_at_z:"⟦0 ≤ z; z*2 < 1; z*2 ∉ s1⟧ ⟹
                         ((λx. if x*2 ≤ 1 then g1 (2*x) else g2 (2*x - 1)) has_vector_derivative
                         2 *⇩R vector_derivative g1 (at (z*2))) (at z)" for z
        apply (rule has_vector_derivative_transform_at [of "¦z - 1/2¦" _ "(λx. g1(2*x))"])
          apply (simp_all add: dist_real_def abs_if split: if_split_asm)
        apply (rule vector_diff_chain_at [of "λx. 2*x" 2 _ g1, simplified o_def])
         apply (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
        using s1
        apply (auto simp: algebra_simps vector_derivative_works)
        done
      assume ass: "0 ≤ z" "z*2 < 1" "z*2 ∉ s1"
      then have z_ge: "z≤ 1" by auto
      show "vector_derivative (λx. if x * 2 ≤ 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *⇩R vector_derivative g1 (at (z * 2))"
        using Derivative.vector_derivative_at_within_ivl[OF g1_at_z[OF ass] ass(1) z_ge]
        by auto
    qed
    assume ass: "0 ≤ z" "z*2 < 1" "z*2 ∉ s1"
    then have "(g1 has_vector_derivative ((vector_derivative g1 (at (z*2))))) (at (z*2))"
      using s1 by (auto simp: algebra_simps vector_derivative_works)
    then have ii: "(vector_derivative g1 (at (z*2) within {0..1})) = (vector_derivative g1 (at (z*2)))"
      using Derivative.vector_derivative_at_within_ivl ass
      by force
    show "vector_derivative (λx. if x * 2 ≤ 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *⇩R vector_derivative g1 (at (z * 2) within {0..1})"
      using i[OF ass] ii
      by auto
  qed
  have g2: "⟦1 < z*2; z ≤ 1; z*2 - 1 ∉ s2⟧ ⟹
            vector_derivative (λx. if x*2 ≤ 1 then g1 (2*x) else g2 (2*x - 1)) (at z within {0..1}) =
            2 *⇩R vector_derivative g2 (at (z*2 - 1) within {0..1})" for z       proof -
    have i:"⟦1 < z*2; z ≤ 1; z*2 - 1 ∉ s2⟧ ⟹
              vector_derivative (λx. if x * 2 ≤ 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1})
                   = 2 *⇩R vector_derivative g2 (at (z * 2 - 1))" for z
    proof-
      have g2_at_z:"⟦1 < z*2; z ≤ 1; z*2 - 1 ∉ s2⟧ ⟹
                      ((λx. if x*2 ≤ 1 then g1 (2*x) else g2 (2*x - 1)) has_vector_derivative 2 *⇩R vector_derivative g2 (at (z*2 - 1))) (at z)" for z
        apply (rule has_vector_derivative_transform_at [of "¦z - 1/2¦" _ "(λx. g2 (2*x - 1))"])
          apply (simp_all add: dist_real_def abs_if split: if_split_asm)
        apply (rule vector_diff_chain_at [of "λx. 2*x - 1" 2 _ g2, simplified o_def])
         apply (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
        using s2
        apply (auto simp: algebra_simps vector_derivative_works)
        done
      assume ass: "1 < z*2" "z ≤ 1" "z*2 - 1 ∉ s2"
      then have z_le: "z≤ 1" by auto
      have z_ge: "0 ≤ z" using ass by auto
      show "vector_derivative (λx. if x * 2 ≤ 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1})
                                = 2 *⇩R vector_derivative g2 (at (z * 2 - 1))"
        using Derivative.vector_derivative_at_within_ivl[OF g2_at_z[OF ass] z_ge z_le]
        by auto
    qed
    assume ass: "1 < z*2" "z ≤ 1" "z*2 - 1 ∉ s2"
    then have "(g2 has_vector_derivative ((vector_derivative g2 (at (z*2 - 1))))) (at (z*2 - 1))"
      using s2 by (auto simp: algebra_simps vector_derivative_works)
    then have ii: "(vector_derivative g2 (at (z*2 - 1) within {0..1})) = (vector_derivative g2 (at (z*2 - 1)))"
      using Derivative.vector_derivative_at_within_ivl ass
      by force
    show "vector_derivative (λx. if x * 2 ≤ 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *⇩R vector_derivative g2 (at (z * 2 - 1) within {0..1})"
      using i[OF ass] ii
      by auto
  qed
  have lem1: "((λx. ∑b∈basis. f ((g1+++g2) x) ∙ b * (vector_derivative (g1+++g2) (at x within {0..1}) ∙ b)) has_integral i1) {0..1/2}"
    apply (rule has_integral_spike_finite [OF _ _ i1, of "insert (1/2) ((*)2 -` s1)"])
    using s1
     apply (force intro: finite_vimageI [where h = "(*)2"] inj_onI)
    apply (clarsimp simp add: joinpaths_def scaleR_conv_of_real mult_ac g1)
    by (simp add: sum_distrib_left)
  moreover have lem2: "((λx. ∑b∈basis. f ((g1+++g2) x) ∙ b * (vector_derivative (g1+++g2) (at x within {0..1}) ∙ b)) has_integral i2) {1/2..1}"
    apply (rule has_integral_spike_finite [OF _ _ i2, of "insert (1/2) ((λx. 2*x-1) -` s2)"])
    using s2
     apply (force intro: finite_vimageI [where h = "λx. 2*x-1"] inj_onI)
    apply (clarsimp simp add: joinpaths_def scaleR_conv_of_real mult_ac g2)
    by (simp add: sum_distrib_left)
  ultimately
  show "line_integral f basis (g1 +++ g2) = line_integral f basis g1 + line_integral f basis g2"
    apply (simp add: line_integral_def)
    apply (rule integral_unique [OF has_integral_combine [where c = "1/2"]])
    using 1 2 integral_unique apply auto
    done
  show "line_integral_exists f basis (g1 +++ g2)"
  proof (simp add: line_integral_exists_def integrable_on_def)
    have "(1::real) ≤ 1 * 2 ∧ (0::real) ≤ 1 / 2"
      by simp
    then show "∃r. ((λr. ∑a∈basis. f ((g1 +++ g2) r) ∙ a * (vector_derivative (g1 +++ g2) (at r within {0..1}) ∙ a)) has_integral r) {0..1}"
    using has_integral_combine [where c = "1/2"] 1 2 divide_le_eq_numeral1(1) lem1 lem2 by blast
  qed
qed

lemma line_integral_exists_joinD1:
  assumes "line_integral_exists f basis (g1 +++ g2)" "valid_path g1"
  shows "line_integral_exists f basis g1"
proof -
  obtain s1
    where s1: "finite s1" "∀x∈{0..1} - s1. g1 differentiable at x"
    using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
  have "(λx. ∑b∈basis. f ((g1 +++ g2) (x/2)) ∙ b * (vector_derivative (g1 +++ g2) (at (x/2) within {0..1}) ∙ b)) integrable_on {0..1}"
    using assms
    apply (auto simp: line_integral_exists_def)
    apply (drule integrable_on_subcbox [where a=0 and b="1/2"])
     apply (auto intro: integrable_affinity [of _ 0 "1/2::real" "1/2" 0, simplified])
    done
  then have *:"(λx. ∑b∈basis. ((f ((g1 +++ g2) (x/2)) ∙ b) / 2)* (vector_derivative (g1 +++ g2) (at (x/2) within {0..1}) ∙ b)) integrable_on {0..1}"
    by (auto simp: Groups_Big.sum_distrib_left dest: integrable_cmul [where c="1/2"] simp: scaleR_conv_of_real)
  have g1: "⟦0 ≤ z; z*2 < 1; z*2 ∉ s1⟧ ⟹
            vector_derivative (λx. if x*2 ≤ 1 then g1 (2*x) else g2 (2*x - 1)) (at z within {0..1}) =
            2 *⇩R vector_derivative g1 (at (z*2) within {0..1})" for z
  proof -
    have i:"⟦0 ≤ z; z*2 < 1; z*2 ∉ s1⟧ ⟹
              vector_derivative (λx. if x * 2 ≤ 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *⇩R vector_derivative g1 (at (z * 2))" for z
    proof-
      have g1_at_z:"⟦0 ≤ z; z*2 < 1; z*2 ∉ s1⟧ ⟹
                         ((λx. if x*2 ≤ 1 then g1 (2*x) else g2 (2*x - 1)) has_vector_derivative
                         2 *⇩R vector_derivative g1 (at (z*2))) (at z)" for z
        apply (rule has_vector_derivative_transform_at [of "¦z - 1/2¦" _ "(λx. g1(2*x))"])
          apply (simp_all add: dist_real_def abs_if split: if_split_asm)
        apply (rule vector_diff_chain_at [of "λx. 2*x" 2 _ g1, simplified o_def])
         apply (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
        using s1
        apply (auto simp: algebra_simps vector_derivative_works)
        done
      assume ass: "0 ≤ z" "z*2 < 1" "z*2 ∉ s1"
      then have z_ge: "z≤ 1" by auto
      show "vector_derivative (λx. if x * 2 ≤ 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *⇩R vector_derivative g1 (at (z * 2))"
        using Derivative.vector_derivative_at_within_ivl[OF g1_at_z[OF ass] ass(1) z_ge]
        by auto
    qed
    assume ass: "0 ≤ z" "z*2 < 1" "z*2 ∉ s1"
    then have "(g1 has_vector_derivative ((vector_derivative g1 (at (z*2))))) (at (z*2))"
      using s1 by (auto simp: algebra_simps vector_derivative_works)
    then have ii: "(vector_derivative g1 (at (z*2) within {0..1})) = (vector_derivative g1 (at (z*2)))"
      using Derivative.vector_derivative_at_within_ivl ass by force
    show "vector_derivative (λx. if x * 2 ≤ 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *⇩R vector_derivative g1 (at (z * 2) within {0..1})"
      using i[OF ass] ii by auto
  qed
  show ?thesis
    using s1
    apply (auto simp: line_integral_exists_def)
    apply (rule integrable_spike_finite [of "{0,1} ∪ s1", OF _ _ *])
     apply (auto simp: joinpaths_def scaleR_conv_of_real g1)
    done
qed

lemma line_integral_exists_joinD2:
  assumes "line_integral_exists f basis (g1 +++ g2)" "valid_path g2"
  shows "line_integral_exists f basis g2"
proof -
  obtain s2
    where s2: "finite s2" "∀x∈{0..1} - s2. g2 differentiable at x"
    using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
  have "(λx. ∑b∈basis. f ((g1 +++ g2) (x/2 + 1/2)) ∙ b * (vector_derivative (g1 +++ g2) (at (x/2 + 1/2) within {0..1}) ∙ b)) integrable_on {0..1}"
    using assms
    apply (auto simp: line_integral_exists_def)
    apply (drule integrable_on_subcbox [where a="1/2" and b=1], auto)
    apply (drule integrable_affinity [of _ "1/2::real" 1 "1/2" "1/2", simplified])
    apply (simp add: image_affinity_atLeastAtMost_diff)
    done
  then have *:"(λx. ∑b∈basis. ((f ((g1 +++ g2) (x/2 + 1/2)) ∙ b) / 2)* (vector_derivative (g1 +++ g2) (at (x/2 + 1/2) within {0..1}) ∙ b)) integrable_on {0..1}"
    by (auto simp: Groups_Big.sum_distrib_left dest: integrable_cmul [where c="1/2"] simp: scaleR_conv_of_real)
  have g2: "⟦1 < z*2; z ≤ 1; z*2 - 1 ∉ s2⟧ ⟹
            vector_derivative (λx. if x*2 ≤ 1 then g1 (2*x) else g2 (2*x - 1)) (at z within {0..1}) =
            2 *⇩R vector_derivative g2 (at (z*2 - 1) within {0..1})" for z       proof -
    have i:"⟦1 < z*2; z ≤ 1; z*2 - 1 ∉ s2⟧ ⟹
              vector_derivative (λx. if x * 2 ≤ 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1})
                   = 2 *⇩R vector_derivative g2 (at (z * 2 - 1))" for z
    proof-
      have g2_at_z:"⟦1 < z*2; z ≤ 1; z*2 - 1 ∉ s2⟧ ⟹
                      ((λx. if x*2 ≤ 1 then g1 (2*x) else g2 (2*x - 1)) has_vector_derivative 2 *⇩R vector_derivative g2 (at (z*2 - 1))) (at z)" for z
        apply (rule has_vector_derivative_transform_at [of "¦z - 1/2¦" _ "(λx. g2 (2*x - 1))"])
          apply (simp_all add: dist_real_def abs_if split: if_split_asm)
        apply (rule vector_diff_chain_at [of "λx. 2*x - 1" 2 _ g2, simplified o_def])
         apply (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
        using s2
        apply (auto simp: algebra_simps vector_derivative_works)
        done
      assume ass: "1 < z*2" "z ≤ 1" "z*2 - 1 ∉ s2"
      then have z_le: "z≤ 1" by auto
      have z_ge: "0 ≤ z" using ass by auto
      show "vector_derivative (λx. if x * 2 ≤ 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1})
                                = 2 *⇩R vector_derivative g2 (at (z * 2 - 1))"
        using Derivative.vector_derivative_at_within_ivl[OF g2_at_z[OF ass] z_ge z_le]
        by auto
    qed
    assume ass: "1 < z*2" "z ≤ 1" "z*2 - 1 ∉ s2"
    then have "(g2 has_vector_derivative ((vector_derivative g2 (at (z*2 - 1))))) (at (z*2 - 1))"
      using s2 by (auto simp: algebra_simps vector_derivative_works)
    then have ii: "(vector_derivative g2 (at (z*2 - 1) within {0..1})) = (vector_derivative g2 (at (z*2 - 1)))"
      using Derivative.vector_derivative_at_within_ivl ass
      by force
    show "vector_derivative (λx. if x * 2 ≤ 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *⇩R vector_derivative g2 (at (z * 2 - 1) within {0..1})"
      using i[OF ass] ii
      by auto
  qed
  show ?thesis
    using s2
    apply (auto simp: line_integral_exists_def)
    apply (rule integrable_spike_finite [of "{0,1} ∪ s2", OF _ _ *])
     apply (auto simp: joinpaths_def scaleR_conv_of_real g2)
    done
qed

lemma has_line_integral_on_reverse_path:
  assumes g: "valid_path g" and int:
    "((λx. ∑b∈basis. F (g x) ∙ b * (vector_derivative g (at x within {0..1}) ∙ b)) has_integral c){0..1}"
  shows  "((λx. ∑b∈basis. F ((reversepath g) x) ∙ b * (vector_derivative (reversepath g) (at x within {0..1}) ∙ b)) has_integral -c){0..1}"
proof -
  { fix s x
    assume xs: "g C1_differentiable_on ({0..1} - s)" "x ∉ (-) 1 ` s" "0 ≤ x" "x ≤ 1"
    have "vector_derivative (λx. g (1 - x)) (at x within {0..1}) =
                - vector_derivative g (at (1 - x) within {0..1})"
    proof -
      obtain f' where f': "(g has_vector_derivative f') (at (1 - x))"
        using xs
        by (force simp: has_vector_derivative_def C1_differentiable_on_def)
      have "(g o (λx. 1 - x) has_vector_derivative -1 *⇩R f') (at x)"
        apply (rule vector_diff_chain_within)
         apply (intro vector_diff_chain_within derivative_eq_intros | simp)+
        apply (rule has_vector_derivative_at_within [OF f'])
        done
      then have mf': "((λx. g (1 - x)) has_vector_derivative -f') (at x)"
        by (simp add: o_def)
      show ?thesis
        using xs
        by (auto simp: vector_derivative_at_within_ivl [OF mf'] vector_derivative_at_within_ivl [OF f'])
    qed
  } note * = this
  obtain S where "continuous_on {0..1} g" "finite S" "g C1_differentiable_on {0..1} - S"
    using g
    by (auto simp: valid_path_def piecewise_C1_differentiable_on_def)
  then show ?thesis 
    using has_integral_affinity01 [OF int, where m= "-1" and c=1]
    unfolding reversepath_def
    by (rule_tac S = "(λx. 1 - x) ` S" in has_integral_spike_finite) (auto simp: * has_integral_neg Groups_Big.sum_negf)
qed

lemma line_integral_on_reverse_path:
  assumes "valid_path γ" "line_integral_exists F basis γ"
  shows "line_integral F basis γ = - (line_integral F basis (reversepath γ))"
        "line_integral_exists F basis (reversepath γ)"
proof -
  obtain i where
    0: "((λx. ∑b∈basis. F (γ x) ∙ b * (vector_derivative γ (at x within {0..1}) ∙ b)) has_integral i){0..1}"
    using assms unfolding integrable_on_def line_integral_exists_def by auto
  then have 1: "((λx. ∑b∈basis. F ((reversepath γ) x) ∙ b * (vector_derivative (reversepath γ) (at x within {0..1}) ∙ b)) has_integral -i){0..1}"
    using has_line_integral_on_reverse_path assms
    by auto
  then have rev_line_integral:"line_integral F basis (reversepath γ) = -i"
    using line_integral_def Henstock_Kurzweil_Integration.integral_unique
    by (metis (no_types))
  have line_integral: "line_integral F basis γ = i"
    using line_integral_def 0 Henstock_Kurzweil_Integration.integral_unique
    by blast
  show "line_integral F basis γ = - (line_integral F basis (reversepath γ))"
    using line_integral rev_line_integral
    by auto
  show "line_integral_exists F basis (reversepath γ)"
    using 1 line_integral_exists_def
    by auto
qed

lemma line_integral_exists_on_degenerate_path:
  assumes "finite basis"
  shows "line_integral_exists F basis (λx. c)"
proof-
  have every_component_integrable:
    "∀b∈basis. (λx. F ((λx. c) x) ∙ b * (vector_derivative (λx. c) (at x within {0..1}) ∙ b)) integrable_on {0..1}"
  proof
    fix b
    assume b_in_basis: "b ∈ basis"
    have cont_field_zero_one: "continuous_on {0..1} (λx. F ((λx. c) x) ∙ b)"
      using continuous_on_const by fastforce
    have cont_path_zero_one:
      "continuous_on {0..1} (λx. (vector_derivative (λx. c) (at x within {0..1})) ∙ b)"
    proof -
      have "((vector_derivative (λx. c) (at x within {0..1})) ∙ b) = 0" if "x ∈ {0..1}" for x
      proof -
        have "vector_derivative (λx. c) (at x within {0..1}) = 0"
          using that gamma_deriv_at_within[of "0" "1"] differentiable_const vector_derivative_const_at
          by fastforce
        then show "vector_derivative (λx. c) (at x within {0..1}) ∙ b = 0"
          by auto
      qed
      then show "continuous_on {0..1} (λx. (vector_derivative (λx. c) (at x within {0..1})) ∙ b)"
        using continuous_on_const[of "{0..1}" "0"] continuous_on_eq[of "{0..1}" "λx. 0" "(λx. (vector_derivative (λx. c) (at x within {0..1})) ∙ b)"]
        by auto
    qed
    show "(λx. F (c) ∙ b * (vector_derivative (λx. c) (at x within {0..1}) ∙ b)) integrable_on {0..1}"
      using cont_field_zero_one cont_path_zero_one continuous_on_mult integrable_continuous_real
      by blast
  qed
  have integrable_sum': "⋀t f s. finite t ⟹
                ∀a∈t. f a integrable_on s ⟹ (λx. ∑a∈t. f a x) integrable_on s"
    using integrable_sum by metis
  have field_integrable_on_basis:
    "(λx. ∑b∈basis. F (c) ∙ b * (vector_derivative (λx. c) (at x within {0..1}) ∙ b)) integrable_on {0..1}"
    using integrable_sum'[OF assms(1) every_component_integrable]
    by auto
  then show ?thesis
    using line_integral_exists_def by auto
qed

lemma degenerate_path_is_valid_path: "valid_path (λx. c)"
  by (auto simp add: valid_path_def piecewise_C1_differentiable_on_def continuous_on_const)

lemma line_integral_degenerate_path:
  assumes "finite basis"
  shows "line_integral F basis (λx. c) = 0"
proof (simp add: line_integral_def)
  have "((vector_derivative (λx. c) (at x within {0..1})) ∙ b) = 0" if "x ∈ {0..1}" for x b
  proof -
    have "vector_derivative (λx. c) (at x within {0..1}) = 0"
      using that gamma_deriv_at_within[of "0" "1"] differentiable_const vector_derivative_const_at
      by fastforce
    then show "vector_derivative (λx. c) (at x within {0..1}) ∙ b = 0"
      by auto
  qed
  then have 0: "⋀x. x ∈ {0..1} ⟹ (λx. ∑b∈basis. F c ∙ b * (vector_derivative (λx. c) (at x within {0..1}) ∙ b)) x = (λx. 0) x"
    by auto
  then show "integral {0..1} (λx. ∑b∈basis. F c ∙ b * (vector_derivative (λx. c) (at x within {0..1}) ∙ b)) = 0"
    using integral_cong[of "{0..1}", OF 0] integral_0 by auto
qed

definition point_path where
    "point_path γ ≡ ∃c. γ = (λx. c)"

lemma line_integral_point_path:
  assumes "point_path γ"
  assumes "finite basis"
  shows "line_integral F basis γ = 0"
  using assms(1) point_path_def line_integral_degenerate_path[OF assms(2)]
  by force

lemma line_integral_exists_point_path:
  assumes "finite basis" "point_path γ"
  shows "line_integral_exists F basis γ"
  using assms
  apply(simp add: point_path_def)
  using line_integral_exists_on_degenerate_path by auto

lemma line_integral_exists_subpath:
  assumes f: "line_integral_exists f basis g" and g: "valid_path g"
    and uv: "u ∈ {0..1}" "v ∈ {0..1}" "u ≤ v"
  shows "(line_integral_exists f basis (subpath u v g))"
proof (cases "v=u")
  case tr: True
  have zero: "(∑b∈basis. f (g u) ∙ b * (vector_derivative (λx. g u) (at x within {0..1}) ∙ b)) = 0" if "x ∈ {0..1}" for x::real
  proof -
    have "(vector_derivative (λx. g u) (at x within {0..1})) = 0"
      using Deriv.has_vector_derivative_const that Derivative.vector_derivative_at_within_ivl
      by fastforce
    then show "(∑b∈basis. f (g u) ∙ b * (vector_derivative (λx. g u) (at x within {0..1}) ∙ b)) = 0"
      by auto
  qed
  then have "((λx. ∑b∈basis. f (g u)  ∙ b * (vector_derivative (λx. g u) (at x within {0..1})  ∙ b)) has_integral 0) {0..1}"
    by (meson has_integral_is_0)
  then show ?thesis
    using f tr by (auto simp add: line_integral_def line_integral_exists_def subpath_def)
next
  case False
  obtain s where s: "⋀x. x ∈ {0..1} - s ⟹ g differentiable at x" and fs: "finite s"
    using g unfolding piecewise_C1_differentiable_on_def C1_differentiable_on_eq valid_path_def by blast
  have *: "((λx. ∑b∈basis. f (g ((v - u) * x + u))  ∙ b * (vector_derivative g (at ((v - u) * x + u) within {0..1})  ∙ b))
            has_integral (1 / (v - u)) * integral {u..v} (λx. ∑b∈basis. f (g (x))  ∙ b * (vector_derivative g (at x within {0..1})  ∙ b)))
           {0..1}"
    using f uv
    apply (simp add: line_integral_exists_def subpath_def)
    apply (drule integrable_on_subcbox [where a=u and b=v, simplified])
     apply (simp_all add: has_integral_integral)
    apply (drule has_integral_affinity [where m="v-u" and c=u, simplified])
     apply (simp_all add: False image_affinity_atLeastAtMost_div_diff scaleR_conv_of_real)
    apply (simp add: divide_simps False)
    done
  have vd:"⋀x. x ∈ {0..1} ⟹
           x ∉ (λt. (v-u) *⇩R t + u) -` s ⟹
           vector_derivative (λx. g ((v-u) * x + u)) (at x within {0..1}) = (v-u) *⇩R vector_derivative g (at ((v-u) * x + u) within {0..1})"
    using test2[OF s fs uv]
    by auto
  have arg:"⋀x. (∑n∈basis. (v - u) * (f (g ((v - u) * x + u)) ∙ n) * (vector_derivative g (at ((v - u) * x + u) within {0..1}) ∙ n))
              =    (∑b∈basis. f (g ((v - u) * x + u)) ∙ b * (v - u) * (vector_derivative g (at ((v - u) * x + u) within {0..1}) ∙ b))"
    by (simp add: mult.commute)
  have"((λx. ∑b∈basis. f (g ((v - u) * x + u))  ∙ b * (vector_derivative (λx. g ((v - u) * x + u)) (at x within {0..1})  ∙ b)) has_integral
          (integral {u..v} (λx. ∑b∈basis. f (g (x))  ∙ b * (vector_derivative g (at x within {0..1}) ∙ b)))) {0..1}"
    apply (cut_tac Henstock_Kurzweil_Integration.has_integral_mult_right [OF *, where c = "v-u"])
    using fs assms
    apply (simp add: False subpath_def line_integral_exists_def)
    apply (rule_tac S = "(λt. ((v-u) *⇩R t + u)) -` s" in has_integral_spike_finite)
      apply (auto simp: inj_on_def False vd finite_vimageI scaleR_conv_of_real Groups_Big.sum_distrib_left
        mult.assoc[symmetric] arg)
    done
  then show "(line_integral_exists f basis (subpath u v g))"
    by(auto simp add: line_integral_exists_def subpath_def integrable_on_def)
qed

(*This should have everything that has to do with onecubes*)

   type_synonym path = "real ⇒ (real * real)"
   type_synonym one_cube = "(real ⇒ (real * real))"
   type_synonym one_chain = "(int * path) set"
   type_synonym two_cube = "(real * real) ⇒ (real * real)"
   type_synonym two_chain = "two_cube set"


definition one_chain_line_integral :: "((real * real) ⇒ (real * real)) => ((real*real) set) ⇒ one_chain ⇒ real" where
    "one_chain_line_integral F b C ≡ (∑(k,g)∈C. k * (line_integral F b g))"

definition boundary_chain where
    "boundary_chain s ≡ (∀(k, γ) ∈ s. k = 1 ∨ k = -1)"

fun coeff_cube_to_path::"(int * one_cube) ⇒ path" 
  where "coeff_cube_to_path (k, γ) = (if k = 1 then γ else (reversepath γ))"

fun rec_join :: "(int*path) list ⇒ path" where   
  "rec_join [] = (λx.0)" |
  "rec_join [oneC] = coeff_cube_to_path oneC" |
  "rec_join (oneC # xs) = coeff_cube_to_path oneC +++ (rec_join xs)"

fun valid_chain_list where
  "valid_chain_list [] = True" |
  "valid_chain_list [oneC] = True" |
  "valid_chain_list (oneC#l) = (pathfinish (coeff_cube_to_path (oneC)) = pathstart (rec_join l) ∧ valid_chain_list l)"

lemma joined_is_valid:
  assumes boundary_chain: "boundary_chain (set l)" and
    valid_path: "⋀k γ. (k, γ) ∈ set l ⟹ valid_path γ" and
    valid_chain_list_ass: "valid_chain_list l"
  shows "valid_path (rec_join l)"
  using assms
proof(induction l)
  case Nil
  then show ?case
    using C1_differentiable_imp_piecewise[OF C1_differentiable_on_const[of "0" "{0..1}"]]
    by (auto simp add: valid_path_def)
next
  case (Cons a l)
  have *: "valid_path (rec_join ((k::int, γ) # l))"
    if "boundary_chain (set (l))"
      "(⋀k' γ'. (k', γ') ∈ set l ⟹ valid_path γ')"
      "valid_chain_list l"
      "valid_path (rec_join l) "
      "(⋀k' γ'. (k', γ') ∈ set ((k, γ) # l) ⟹ valid_path γ')"
      "valid_chain_list ((k, γ) # l)"
      "boundary_chain (set ((k,γ) # l))" for k γ l
  proof (cases "l = []")
    case True
    with that show "valid_path (rec_join ((k, γ) # l))"
      by auto
  next
    case False
    then obtain h l' where l_nempty: "l = h#l'"
      by (meson rec_join.elims)
    then show "valid_path (rec_join ((k, γ) # l))"
    proof (simp, intro conjI impI)
      assume k_eq_1: "k = 1"
      have 0:"valid_path γ"
        using that by auto
      have 1:"pathfinish γ = pathstart (rec_join (h#l'))"
        using that(6) k_eq_1 l_nempty by auto
      show "valid_path (γ +++ rec_join (h#l'))"
        using 0 1 valid_path_join that(4) l_nempty by auto
    next
      assume "k ≠ 1"
      then have k_eq_neg_1: "k = -1"
        using that(7)
        by (auto simp add: boundary_chain_def)
      have "valid_path γ"
        using that by auto
      then have 0: "valid_path (reversepath γ)"
        using valid_path_imp_reverse
        by auto
      have 1: "pathfinish (reversepath γ) = pathstart (rec_join (h#l'))"
        using that(6) k_eq_neg_1 l_nempty by auto
      show "valid_path ((reversepath γ) +++ rec_join (h#l'))"
        using 0 1 valid_path_join that(4) l_nempty by blast
    qed
  qed
  have "∀ps. valid_chain_list ps ∨ (∃i f p psa. ps = (i, f) # p # psa ∧ ((i = 1 ∧ pathfinish f ≠ pathstart (rec_join (p # psa)) ∨ i ≠ 1 ∧ pathfinish (reversepath f) ≠ pathstart (rec_join (p # psa))) ∨ ¬ valid_chain_list (p # psa)))"
    by (smt coeff_cube_to_path.elims valid_chain_list.elims(3)) 
  moreover have "boundary_chain (set l)"
    by (meson Cons.prems(1) boundary_chain_def set_subset_Cons subset_eq)
  ultimately show ?case
    using * Cons by (metis (no_types) list.set_intros(2) prod.collapse valid_chain_list.simps(3))
qed

lemma pathstart_rec_join_1:
  "pathstart (rec_join ((1, γ) # l)) = pathstart γ"
proof (cases "l = []")
  case True
  then show "pathstart (rec_join ((1, γ) # l)) = pathstart γ"
    by simp
next
  case False
  then obtain h l' where "l = h#l'"
    by (meson rec_join.elims)
  then show "pathstart (rec_join ((1, γ) # l)) = pathstart γ"
    by simp
qed

lemma pathstart_rec_join_2:
  "pathstart (rec_join ((-1, γ) # l)) = pathstart (reversepath γ)"
proof cases
  assume "l = []"
  then show "pathstart (rec_join ((- 1, γ) # l)) = pathstart (reversepath γ)"
    by simp
next
  assume "l ≠ [] "
  then obtain h l' where "l = h#l'"
    by (meson rec_join.elims)
  then show "pathstart (rec_join ((- 1, γ) # l)) = pathstart (reversepath γ)"
    by simp
qed

lemma pathstart_rec_join:
  "pathstart (rec_join ((1, γ) # l)) = pathstart γ"
  "pathstart (rec_join ((-1, γ) # l)) = pathstart (reversepath γ)"
  using pathstart_rec_join_1 pathstart_rec_join_2
  by auto

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: "⋀k γ. (k, γ) ∈ set l ⟹ valid_path γ" and
    line_integral_exists: "∀(k, γ) ∈ set l. line_integral_exists F basis γ"
  shows "line_integral_exists F basis (rec_join l)"
  using assms
proof (induction l)
  case Nil
  then show ?case
  proof (simp add: line_integral_exists_def)
    have "∀x. (vector_derivative (λx. 0) (at x)) = 0"
      using Derivative.vector_derivative_const_at
      by auto
    then have "∀x. ((λx. 0) has_vector_derivative 0) (at x)"
      using Derivative.vector_derivative_const_at
      by auto
    then have "∀x. ((λx. 0) has_vector_derivative 0) (at x within {0..1})"
      using Derivative.vector_derivative_const_at
      by auto
    then have 0: "∀x∈{0..1}. (vector_derivative (λx. 0) (at x within{0..1})) = 0"
      by (simp add: gamma_deriv_at_within)
    have "(∀x∈{0..1}. (∑b∈basis. F 0 ∙ b * (vector_derivative (λx. 0) (at x within {0..1}) ∙ b)) = 0)"
      by (simp add: 0)
    then have " ((λx. ∑b∈basis. F 0 ∙ b * (vector_derivative (λx. 0) (at x within {0..1}) ∙ b)) has_integral 0) {0..1}"
      by (meson has_integral_is_0)
    then show "(λx. ∑b∈basis. F 0 ∙ b * (vector_derivative (λx. 0) (at x within {0..1}) ∙ b)) integrable_on {0..1}"
      by auto
  qed
next
  case (Cons a l)
  obtain k γ where aeq: "a = (k,γ)"
    by force
  show ?case
    unfolding aeq
  proof cases
    assume l_empty: "l = []"
    then show "line_integral_exists F basis (rec_join ((k, γ) # l))"
      using Cons.prems aeq line_integral_on_reverse_path(2) by fastforce
  next
    assume "l ≠ []"
    then obtain h l' where l_nempty: "l = h#l'"
      by (meson rec_join.elims)
    show "line_integral_exists F basis (rec_join ((k, γ) # l))"
    proof (auto simp add: l_nempty)
      assume k_eq_1: "k = 1"
      have 0: "line_integral_exists F basis γ"
        using Cons.prems(4) aeq by auto
      have 1: "line_integral_exists F basis (rec_join l)"
        by (metis (mono_tags) Cons boundary_chain_def list.set_intros(2) valid_chain_list.elims(3) valid_chain_list.simps(3))
      have 2: "valid_path γ"
        using Cons aeq by auto
      have 3:"valid_path (rec_join l)"
        by (metis (no_types) Cons.prems boundary_chain_def joined_is_valid l_nempty set_subset_Cons subsetCE valid_chain_list.simps(3))
      show "line_integral_exists F basis (γ +++ rec_join (h#l'))"
        using line_integral_distrib(2)[OF 0 1 2 3] assms l_nempty by auto
    next
      assume "k ≠ 1"
      then have k_eq_neg_1: "k = -1"
        using Cons aeq by (simp add: boundary_chain_def)
      have gamma_valid: "valid_path γ"
        using Cons aeq by auto
      then have 2: "valid_path (reversepath γ)"
        using valid_path_imp_reverse by auto
      have "line_integral_exists F basis γ"
        using Cons aeq by auto
      then have 0: "line_integral_exists F basis (reversepath γ)"
        using line_integral_on_reverse_path(2) gamma_valid
        by auto
      have 1: "line_integral_exists F basis (rec_join l)"
        using Cons aeq
        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))
      have 3:"valid_path (rec_join l)"
        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))
      show "line_integral_exists F basis ((reversepath γ) +++ rec_join (h#l'))"
        using line_integral_distrib(2)[OF 0 1 2 3] assms l_nempty
        by auto
    qed
  qed
qed

lemma line_integral_exists_rec_join_cons:
  assumes "line_integral_exists F basis (rec_join ((1,γ) # l))"
    "(⋀k' γ'. (k', γ') ∈ set ((1,γ) # l) ⟹ valid_path γ')"
    "finite basis"
  shows "line_integral_exists F basis (γ +++ (rec_join l))"
proof cases
  assume l_empty: "l = []"
  show "line_integral_exists F basis (γ +++ rec_join l)"
    using assms(2) line_integral_distrib(2)[OF assms(1) line_integral_exists_on_degenerate_path[OF assms(3)], of "0"]
    using degenerate_path_is_valid_path
    by (fastforce simp add: l_empty)
next
  assume "l ≠ []"
  then obtain h l' where "l = h#l'"
    by (meson rec_join.elims)
  then show "line_integral_exists F basis (γ +++ rec_join l)"
    using assms by auto
qed

lemma line_integral_exists_rec_join_cons_2:
  assumes "line_integral_exists F basis (rec_join ((-1,γ) # l))"
    "(⋀k' γ'. (k', γ') ∈ set ((1,γ) # l) ⟹ valid_path γ')"
    "finite basis"
  shows "line_integral_exists F basis ((reversepath γ) +++ (rec_join l))"
proof cases
  assume l_empty: "l = []"
  show "line_integral_exists F basis ((reversepath γ) +++ rec_join l)"
    using assms(2) line_integral_distrib(2)[OF assms(1) line_integral_exists_on_degenerate_path[OF assms(3)], of "0"]
    using degenerate_path_is_valid_path
    by (auto simp add: l_empty)
next
  assume "l ≠ []"
  then obtain h l' where  "l = h#l'"
    by (meson rec_join.elims)
  with assms show "line_integral_exists F basis ((reversepath γ) +++ rec_join l)"
    using assms by auto
qed

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: "⋀k γ. (k, γ) ∈ set l ⟹ valid_path γ" and
    line_integral_exists: "line_integral_exists F basis (rec_join l)" and
    finite_basis: "finite basis"
  shows "∀(k, γ) ∈ set l. line_integral_exists F basis γ"
  using assms
proof (induction l)
  case Nil
  show ?case
    by (simp add: line_integral_exists_def)
next
  case ass: (Cons a l)          
  obtain k γ where k_gamma:"a = (k,γ)"
    by fastforce
  show ?case
    apply (auto simp add: k_gamma)
  proof -
    show "line_integral_exists F basis γ"
    proof(cases "k = 1")
      assume k_eq_1: "k = 1"
      have 0: "line_integral_exists F basis (γ +++ (rec_join l))"
        using line_integral_exists_rec_join_cons k_eq_1 k_gamma ass(4) ass(5) ass(6)
        by auto
      have 2: "valid_path γ"
        using ass k_gamma by auto
      show "line_integral_exists F basis γ"
        using line_integral_exists_joinD1[OF 0 2]
        by auto
    next
      assume "k ≠ 1"
      then have k_eq_neg_1: "k = -1"
        using ass k_gamma
        by (simp add: boundary_chain_def)
      have 0: "line_integral_exists F basis ((reversepath γ) +++ (rec_join l))"
        using line_integral_exists_rec_join_cons_2[OF ] k_eq_neg_1 k_gamma ass(4) ass(5) ass(6)
        by fastforce
      have gamma_valid:
        "valid_path γ"
        using ass k_gamma by auto
      then have 2: "valid_path (reversepath γ)"
        using valid_path_imp_reverse by auto
      have "line_integral_exists F basis (reversepath γ)"
        using line_integral_exists_joinD1[OF 0 2] by auto
      then show "line_integral_exists F basis (γ)"
        using line_integral_on_reverse_path(2)[OF 2] reversepath_reversepath
        by auto
    qed
  next
    have 0:"boundary_chain (set l)"
      using ass(2)
      by (auto simp add: boundary_chain_def)
    have 1:"valid_chain_list l"
      using ass(3)
      apply (auto simp add: k_gamma)
      by (metis valid_chain_list.elims(3) valid_chain_list.simps(3))
    have 2:"(⋀k γ. (k, γ) ∈ set (l) ⟹ valid_path γ)"
      using ass(4) by auto
    have 3: "valid_path (rec_join l)"
      using joined_is_valid[OF 0] 1 2 by auto
    have 4: "line_integral_exists F basis (rec_join l)"
    proof(cases "k = 1")
      assume k_eq_1: "k = 1"
      have 0: "line_integral_exists F basis (γ +++ (rec_join l))"
        using line_integral_exists_rec_join_cons k_eq_1 k_gamma ass(4) ass(5) ass(6) by auto
      show "line_integral_exists F basis (rec_join l)"
        using line_integral_exists_joinD2[OF 0 3] by auto
    next
      assume "k ≠ 1"
      then have k_eq_neg_1: "k = -1"
        using ass k_gamma
        by (simp add: boundary_chain_def)
      have 0: "line_integral_exists F basis ((reversepath γ) +++ (rec_join l))"
        using line_integral_exists_rec_join_cons_2[OF ] k_eq_neg_1 k_gamma ass(4) ass(5) ass(6)
        by fastforce
      show "line_integral_exists F basis (rec_join l)"
        using line_integral_exists_joinD2[OF 0 3]
        by auto
    qed
    show "⋀a b. (a, b) ∈ set l ⟹ line_integral_exists F basis b"
      using 0 1 2 3 4 ass(1)[OF 0 1 2] ass(6)
      by fastforce
  qed
qed

inductive chain_subdiv_path
  where I: "chain_subdiv_path γ (set l)" if "distinct l" "rec_join l = γ" "valid_chain_list l"

lemma valid_path_equiv_valid_chain_list:
  assumes path_eq_chain: "chain_subdiv_path γ one_chain" 
    and "boundary_chain one_chain" "∀(k, γ) ∈ one_chain. valid_path γ"
  shows "valid_path γ"
proof -
  obtain l where l_props: "set l = one_chain" "distinct l" "rec_join l = γ" "valid_chain_list l"
    using chain_subdiv_path.cases path_eq_chain by force
  show "valid_path γ"
    using joined_is_valid assms l_props by blast
qed

lemma line_integral_rec_join_cons:
  assumes "line_integral_exists F basis γ"
    "line_integral_exists F basis (rec_join ((l)))"
    "(⋀k' γ'. (k', γ') ∈ set ((1,γ) # l) ⟹ valid_path γ')"
    "finite basis"
  shows "line_integral F basis (rec_join ((1,γ) # l)) = line_integral F basis (γ +++ (rec_join l))"
proof cases
  assume l_empty: "l = []"
  show "line_integral F basis (rec_join ((1,γ) # l)) = line_integral F basis (γ +++ (rec_join l))"
    using assms line_integral_distrib(1)[OF assms(1) line_integral_exists_on_degenerate_path[OF assms(4)], of "0"]
    apply (auto simp add: l_empty)
    using degenerate_path_is_valid_path line_integral_degenerate_path
    by fastforce
next
  assume "l ≠ []"
  then obtain h l' where l_nempty: "l = h#l'"
    by (meson rec_join.elims)
  show "line_integral F basis (rec_join ((1,γ) # l)) = line_integral F basis (γ +++ (rec_join l))"
    using assms  by (auto simp add: l_nempty)
qed

lemma line_integral_rec_join_cons_2:
  assumes "line_integral_exists F basis γ"
    "line_integral_exists F basis (rec_join ((l)))"
    "(⋀k' γ'. (k', γ') ∈ set ((-1,γ) # l) ⟹ valid_path γ')"
    "finite basis"
  shows "line_integral F basis (rec_join ((-1,γ) # l)) = line_integral F basis ((reversepath γ) +++ (rec_join l))"
proof cases
  assume l_empty: "l = []"
  have 0: "line_integral_exists F basis (reversepath γ)"
    using assms line_integral_on_reverse_path(2) by fastforce
  have 1: "valid_path (reversepath γ)"
    using assms  by fastforce
  show "line_integral F basis (rec_join ((-1,γ) # l)) = line_integral F basis ((reversepath γ) +++ (rec_join l))"
    using assms line_integral_distrib(1)[OF 0 line_integral_exists_on_degenerate_path[OF assms(4)], of "0"]
    apply (auto simp add: l_empty)
    using degenerate_path_is_valid_path line_integral_degenerate_path
    by fastforce
next
  assume "l ≠ []"
  then obtain h l' where l_nempty: "l = h#l'"
    by (meson rec_join.elims)
  show "line_integral F basis (rec_join ((-1,γ) # l)) = line_integral F basis ((reversepath γ) +++ (rec_join l))"
    using assms  by (auto simp add: l_nempty)
qed

lemma one_chain_line_integral_rec_join:
  assumes l_props: "set l = one_chain" "distinct l" "valid_chain_list l" and
    boundary_chain: "boundary_chain one_chain" and
    line_integral_exists: "∀(k::int, γ) ∈ one_chain. line_integral_exists F basis γ" and
    valid_path: "∀(k::int, γ) ∈ one_chain. valid_path γ" and
    finite_basis: "finite basis"
  shows "line_integral F basis (rec_join l) = one_chain_line_integral F basis one_chain"
proof -
  have 0: "sum_list (map (λ((k::int), γ). (k::int) * (line_integral F basis γ)) l) = one_chain_line_integral F basis one_chain"
    unfolding one_chain_line_integral_def
    using l_props Groups_List.comm_monoid_add_class.sum.distinct_set_conv_list[OF l_props(2), of "(λ(k, γ). (k::int) * (line_integral F basis γ))"]
    by auto
  have "valid_chain_list l ⟹
                    boundary_chain (set l) ⟹
                    (∀(k::int, γ) ∈ set l. line_integral_exists F basis γ) ⟹
                    (∀(k::int, γ) ∈ set l. valid_path γ) ⟹
                    line_integral F basis (rec_join l) = sum_list (map (λ(k::int, γ). k * (line_integral F basis γ)) l)"
  proof (induction l)
    case Nil
    show ?case
      unfolding line_integral_def boundary_chain_def
      apply (auto)
    proof
      have "∀x. (vector_derivative (λx. 0) (at x)) = 0"
        using Derivative.vector_derivative_const_at
        by auto
      then have "∀x. ((λx. 0) has_vector_derivative 0) (at x)"
        using Derivative.vector_derivative_const_at
        by auto
      then have "∀x. ((λx. 0) has_vector_derivative 0) (at x within {0..1})"
        using Derivative.vector_derivative_const_at
        by auto
      then have 0: "∀x∈{0..1}. (vector_derivative (λx. 0) (at x within{0..1})) = 0"
        by (metis (no_types) box_real(2) vector_derivative_within_cbox zero_less_one)
      have "(∀x∈{0..1}. (∑b∈basis. F 0 ∙ b * (vector_derivative (λx. 0) (at x within {0..1}) ∙ b)) = 0)"
        by (simp add: 0)
      then show "((λx. ∑b∈basis. F 0 ∙ b * (vector_derivative (λx. 0) (at x within {0..1}) ∙ b)) has_integral 0) {0..1}"
        by (meson has_integral_is_0)
    qed
  next
    case ass: (Cons a l)
    obtain k::"int" and
      γ::"one_cube" where props: "a = (k,γ)"
    proof
      let ?k2 = "fst a"
      let ?γ2 = "snd a"
      show "a = (?k2, ?γ2)"
        by auto
    qed
    have "line_integral_exists F basis (rec_join (a # l))"
      using line_integral_exists_on_rec_join[OF ass(3) ass(2)] ass(5) ass(4)
      by blast
    have "boundary_chain (set l)"
      by (meson ass.prems(2) boundary_chain_def list.set_intros(2))
    have val_l: "⋀f i. (i,f) ∈ set l ⟹ valid_path f"
      using ass.prems(4) by fastforce
    have vcl_l: "valid_chain_list l"
      by (metis (no_types) ass.prems(1) valid_chain_list.elims(3) valid_chain_list.simps(3))
    have line_integral_exists_on_joined:
      "line_integral_exists F basis (rec_join l)"
      by (metis ‹boundary_chain (set l)› ‹line_integral_exists F basis (rec_join (a # l))› emptyE val_l vcl_l joined_is_valid line_integral_exists_joinD2 line_integral_exists_on_rec_join list.set(1) neq_Nil_conv rec_join.simps(3))
    have "valid_path (rec_join (a # l))"
      using joined_is_valid ass(5) ass(3) ass(2) by blast
    then have joined_is_valid: "valid_path (rec_join l)"
      using ‹boundary_chain (set l)› val_l vcl_l joined_is_valid by blast
    show ?case
    proof (clarsimp, cases)
      assume k_eq_1: "(k::int) = 1"
      have line_integral_exists_on_gamma: "line_integral_exists F basis γ"
        using ass props by auto
      have gamma_is_valid: "valid_path γ"
        using ass props by auto
      have line_int_rw: "line_integral F basis (rec_join ((k, γ) # l)) = line_integral F basis (γ +++ rec_join l)"
      proof -
        have gam_int: "line_integral_exists F basis γ" using ass props by auto
        have rec_join_int: "line_integral_exists F basis (rec_join l)"
          using line_integral_exists_on_rec_join
          using line_integral_exists_on_joined by blast
        show ?thesis
          using line_integral_rec_join_cons[OF gam_int rec_join_int] ass k_eq_1 finite_basis props by force
      qed
      show "line_integral F basis (rec_join (a # l)) =
            (case a of (x, γ) ⇒ real_of_int x * line_integral F basis γ) + (∑(x, γ)←l. real_of_int x * line_integral F basis γ)"
        apply (simp add: props line_int_rw)
        using line_integral_distrib[OF line_integral_exists_on_gamma line_integral_exists_on_joined gamma_is_valid joined_is_valid]
          ass k_eq_1 vcl_l
        by (auto simp: boundary_chain_def props)
    next
      assume "k ≠ 1"
      then have k_eq_neg_1: "k = -1"
        using ass props
        by (auto simp add: boundary_chain_def)
      have line_integral_exists_on_gamma:
        "line_integral_exists F basis (reversepath γ)"
        using line_integral_on_reverse_path ass props
        by auto
      have gamma_is_valid: "valid_path (reversepath γ)"
        using valid_path_imp_reverse ass props by auto
      have line_int_rw: "line_integral F basis (rec_join ((k, γ) # l)) = line_integral F basis ((reversepath γ) +++ rec_join l)"
      proof -
        have gam_int: "line_integral_exists F basis γ" using ass props by auto
        have rec_join_int: "line_integral_exists F basis (rec_join l)"
          using line_integral_exists_on_rec_join
          using line_integral_exists_on_joined by blast
        show ?thesis
          using line_integral_rec_join_cons_2[OF gam_int rec_join_int]
          using ass k_eq_neg_1
          using finite_basis props by blast
      qed
      show "line_integral F basis (rec_join (a # l)) =
            (case a of (x, γ) ⇒ real_of_int x * line_integral F basis γ) + (∑(x, γ)←l. real_of_int x * line_integral F basis γ)"
        apply (simp add: props line_int_rw)
        using line_integral_distrib[OF line_integral_exists_on_gamma line_integral_exists_on_joined gamma_is_valid joined_is_valid]
          props ass line_integral_on_reverse_path(1)[of "γ" "F" "basis"] k_eq_neg_1
        using ‹boundary_chain (set l)› vcl_l by auto
    qed
  qed
  then have 1:"line_integral F basis (rec_join l) = sum_list (map (λ(k::int, γ). k * (line_integral F basis γ)) l)"
    using l_props assms by auto
  then show ?thesis
    using 0 1 by auto
qed

lemma line_integral_on_path_eq_line_integral_on_equiv_chain:
  assumes path_eq_chain: "chain_subdiv_path γ one_chain" and
    boundary_chain: "boundary_chain one_chain" and
    line_integral_exists: "∀(k::int, γ) ∈ one_chain. line_integral_exists F basis γ" and
    valid_path: "∀(k::int, γ) ∈ one_chain. valid_path γ" and
    finite_basis: "finite basis"
  shows "one_chain_line_integral F basis one_chain = line_integral F basis γ"
    "line_integral_exists F basis γ"
    "valid_path γ"
proof -
  obtain l where l_props: "set l = one_chain" "distinct l" "rec_join l = γ" "valid_chain_list l"
    using chain_subdiv_path.cases path_eq_chain by force
  show "line_integral_exists F basis γ"
    using line_integral_exists_on_rec_join assms l_props
    by blast
  show "valid_path γ"
    using joined_is_valid assms l_props
    by blast
  have "line_integral F basis (rec_join l) = one_chain_line_integral F basis one_chain"
    using one_chain_line_integral_rec_join l_props assms by auto
  then show "one_chain_line_integral F basis one_chain = line_integral F basis γ"
    using l_props
    by auto
qed

lemma line_integral_on_path_eq_line_integral_on_equiv_chain':
  assumes path_eq_chain: "chain_subdiv_path γ one_chain" and
    boundary_chain: "boundary_chain one_chain" and
    line_integral_exists: "line_integral_exists F basis γ" and
    valid_path: "∀(k, γ) ∈ one_chain. valid_path γ" and
    finite_basis: "finite basis"
  shows "one_chain_line_integral F basis one_chain = line_integral F basis γ"
    "∀(k, γ) ∈ one_chain. line_integral_exists F basis γ"
proof -
  obtain l where l_props: "set l = one_chain" "distinct l" "rec_join l = γ" "valid_chain_list l"
    using chain_subdiv_path.cases path_eq_chain by force
  show 0: "∀(k, γ) ∈ one_chain. line_integral_exists F basis γ"
    using line_integral_exists_on_rec_join' assms l_props
    by blast
  show "one_chain_line_integral F basis one_chain = line_integral F basis γ"
    using line_integral_on_path_eq_line_integral_on_equiv_chain(1)[OF assms(1) assms(2) 0 assms(4) assms(5)] by auto
qed

definition chain_subdiv_chain where
  "chain_subdiv_chain one_chain1 subdiv
        ≡ ∃f. (⋃(f ` one_chain1)) = subdiv ∧
              (∀c∈one_chain1. chain_subdiv_path (coeff_cube_to_path c) (f c)) ∧
              pairwise (λ p p'. f p ∩ f p' = {}) one_chain1 ∧
              (∀x ∈ one_chain1. finite (f x))"

lemma chain_subdiv_chain_character:
  shows "chain_subdiv_chain one_chain1 subdiv ⟷
        (∃f. ⋃(f ` one_chain1) = subdiv ∧
             (∀(k, γ)∈one_chain1.
                 if k = 1
                 then chain_subdiv_path γ (f (k, γ))
                 else chain_subdiv_path (reversepath γ) (f (k, γ))) ∧
             (∀p∈one_chain1.
                 ∀p'∈one_chain1. p ≠ p' ⟶ f p ∩ f p' = {}) ∧
             (∀x∈one_chain1. finite (f x)))"  
  unfolding chain_subdiv_chain_def
  by (safe; intro exI conjI iffI; fastforce simp add: pairwise_def)

lemma chain_subdiv_chain_imp_finite_subdiv:
  assumes "finite one_chain1"
    "chain_subdiv_chain one_chain1 subdiv"
  shows "finite subdiv"
  using assms by(auto simp add: chain_subdiv_chain_def)

lemma valid_subdiv_imp_valid_one_chain:
  assumes chain1_eq_chain2: "chain_subdiv_chain one_chain1 subdiv" and
    boundary_chain1: "boundary_chain one_chain1" and
    boundary_chain2: "boundary_chain subdiv" and
    valid_path: "∀(k, γ) ∈ subdiv. valid_path γ"
  shows "∀(k, γ) ∈ one_chain1. valid_path γ"
proof -
  obtain f where f_props:
    "((⋃(f ` one_chain1)) = subdiv)"
    "(∀(k,γ)∈one_chain1. if k = 1 then chain_subdiv_path γ (f(k,γ)) else chain_subdiv_path (reversepath γ) (f(k,γ)))"
    "(∀p∈one_chain1. ∀p'∈one_chain1. p ≠ p' ⟶ f p ∩ f p' = {})"
    using chain1_eq_chain2 chain_subdiv_chain_character by auto
  have "⋀ k γ. (k,γ) ∈ one_chain1⟹ valid_path γ"
  proof-
    fix k γ
    assume ass: "(k,γ) ∈ one_chain1"
    show "valid_path γ"
    proof (cases "k = 1")
      assume k_eq_1: "k = 1"
      then have i:"chain_subdiv_path γ (f(k,γ))"
        using f_props(2) ass by auto
      have ii:"boundary_chain (f(k,γ))"
        using f_props(1) ass assms
        apply (simp add: boundary_chain_def)
        by blast
      have "iv": " ∀(k, γ)∈f (k, γ). valid_path γ"
        using f_props(1) ass assms
        by blast
      show ?thesis
        using valid_path_equiv_valid_chain_list[OF i ii iv]
        by auto
    next
      assume "k ≠ 1"
      then have k_eq_neg1: "k = -1"
        using ass boundary_chain1
        by (auto simp add: boundary_chain_def)
      then have i:"chain_subdiv_path (reversepath γ) (f(k,γ))"
        using f_props(2) ass using ‹k ≠ 1› by auto
      have ii:"boundary_chain (f(k,γ))"
        using f_props(1) ass assms by (auto simp add: boundary_chain_def)
      have "iv": " ∀(k, γ)∈f (k, γ). valid_path γ"
        using f_props(1) ass assms
        by blast
      have "valid_path (reversepath γ)"
        using valid_path_equiv_valid_chain_list[OF i ii iv]
        by auto
      then show ?thesis
        using  reversepath_reversepath valid_path_imp_reverse
        by force
    qed
  qed
  then show valid_path1: "∀(k, γ) ∈ one_chain1. valid_path γ"
    by auto
qed

lemma one_chain_line_integral_eq_line_integral_on_sudivision:
  assumes chain1_eq_chain2: "chain_subdiv_chain one_chain1 subdiv" and
    boundary_chain1: "boundary_chain one_chain1" and
    boundary_chain2: "boundary_chain subdiv" and
    line_integral_exists_on_chain2: "∀(k, γ) ∈ subdiv. line_integral_exists F basis γ" and
    valid_path: "∀(k, γ) ∈ subdiv. valid_path γ" and
    finite_chain1: "finite one_chain1" and
    finite_basis: "finite basis"
  shows "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis subdiv"
    "∀(k, γ) ∈ one_chain1. line_integral_exists F basis γ"
proof -
  obtain f where f_props:
    "((⋃(f ` one_chain1)) = subdiv)"
    "(∀(k,γ)∈one_chain1. if k = 1 then chain_subdiv_path γ (f(k,γ)) else chain_subdiv_path (reversepath γ) (f(k,γ)))"
    "(∀p∈one_chain1. ∀p'∈one_chain1. p ≠ p' ⟶ f p ∩ f p' = {})"
    "(∀x ∈ one_chain1. finite (f x))"
    using chain1_eq_chain2 chain_subdiv_chain_character by (auto simp add: pairwise_def chain_subdiv_chain_def)
  then have 0: "one_chain_line_integral F basis subdiv = one_chain_line_integral F basis (⋃(f ` one_chain1))"
    by auto
  have finite_chain2: "finite subdiv"
    using finite_chain1 f_props(1) f_props(4)
    apply (simp add: image_def)
    using f_props(1) by auto
  have "⋀ k γ. (k,γ) ∈ one_chain1⟹ line_integral_exists F basis γ"
  proof-
    fix k γ
    assume ass: "(k,γ) ∈ one_chain1"
    show "line_integral_exists F basis γ"
    proof (cases "k = 1")
      assume k_eq_1: "k = 1"
      then have i:"chain_subdiv_path γ (f(k,γ))"
        using f_props(2) ass by auto
      have ii:"boundary_chain (f(k,γ))"
        using f_props(1) ass assms by (auto simp add: boundary_chain_def)
      have iii:"∀(k, γ)∈f (k, γ). line_integral_exists F basis γ"
        using f_props(1) ass assms
        by blast
      have "iv": " ∀(k, γ)∈f (k, γ). valid_path γ"
        using f_props(1) ass assms
        by blast
      show ?thesis
        using line_integral_on_path_eq_line_integral_on_equiv_chain(2)[OF i ii iii iv finite_basis]
        by auto
    next
      assume "k ≠ 1"
      then have k_eq_neg1: "k = -1"
        using ass boundary_chain1
        by (auto simp add: boundary_chain_def)
      then have i:"chain_subdiv_path (reversepath γ) (f(k,γ))"
        using f_props(2) ass by auto
      have ii:"boundary_chain (f(k,γ))"
        using f_props(1) ass assms by (auto simp add: boundary_chain_def)
      have iii:"∀(k, γ)∈f (k, γ). line_integral_exists F basis γ"
        using f_props(1) ass assms
        by blast
      have "iv": " ∀(k, γ)∈f (k, γ). valid_path γ"
        using f_props(1) ass assms
        by blast
      have x:"line_integral_exists F basis (reversepath γ)"
        using line_integral_on_path_eq_line_integral_on_equiv_chain(2)[OF i ii iii iv finite_basis]
        by auto
      have "valid_path (reversepath γ)"
        using line_integral_on_path_eq_line_integral_on_equiv_chain(3)[OF i ii iii iv finite_basis]
        by auto
      then show ?thesis
        using line_integral_on_reverse_path(2) reversepath_reversepath x
        by fastforce
    qed
  qed
  then show line_integral_exists_on_chain1: "∀(k, γ) ∈ one_chain1. line_integral_exists F basis γ"
    by auto
  have 1: "one_chain_line_integral F basis (⋃(f ` one_chain1)) = one_chain_line_integral F basis one_chain1"
  proof -
    have 0:"one_chain_line_integral F basis (⋃(f ` one_chain1)) =
                           (∑one_chain ∈ (f ` one_chain1). one_chain_line_integral F basis one_chain)"
    proof -
      have finite: "∀chain ∈ (f ` one_chain1). finite chain"
        using f_props(1) finite_chain2
        by (meson Sup_upper finite_subset)
      have disj: " ∀A∈f ` one_chain1. ∀B∈f ` one_chain1. A ≠ B ⟶ A ∩ B = {}"
        by (metis (no_types, opaque_lifting) f_props(3) image_iff)
      show "one_chain_line_integral F basis (⋃(f ` one_chain1)) =
                                (∑one_chain ∈ (f ` one_chain1). one_chain_line_integral F basis one_chain)"
        using Groups_Big.comm_monoid_add_class.sum.Union_disjoint[OF finite disj]
          one_chain_line_integral_def
        by auto
    qed
    have 1:"(∑one_chain ∈ (f ` one_chain1). one_chain_line_integral F basis one_chain) =
                            one_chain_line_integral F basis one_chain1"
    proof -
      have "(∑one_chain ∈ (f ` one_chain1). one_chain_line_integral F basis one_chain) =
                                     (∑(k,γ)∈one_chain1. k*(line_integral F basis γ))"
      proof -
        have i:"(∑one_chain ∈ (f ` (one_chain1 - {p. f p = {}})). one_chain_line_integral F basis one_chain) =
                                       (∑(k,γ)∈one_chain1 - {p. f p = {}}. k*(line_integral F basis γ))"
        proof -
          have "inj_on f (one_chain1 - {p. f p = {}})"
            unfolding inj_on_def using f_props(3) by blast
          then have 0: "(∑one_chain ∈ (f ` (one_chain1 - {p. f p = {}})). one_chain_line_integral F basis one_chain)
                                                       = (∑(k, γ) ∈ (one_chain1 - {p. f p = {}}). one_chain_line_integral F basis (f (k, γ)))"
            using Groups_Big.comm_monoid_add_class.sum.reindex
            by auto
          have "⋀ k γ. (k, γ) ∈ (one_chain1 - {p. f p = {}}) ⟹
                        one_chain_line_integral F basis (f(k, γ)) = k* (line_integral F basis γ)"
          proof-
            fix k γ
            assume ass: "(k, γ) ∈ (one_chain1 - {p. f p = {}})"
            have bchain: "boundary_chain (f(k,γ))"
              using f_props(1) boundary_chain2 ass
              by (auto simp add: boundary_chain_def)
            have wexist: "∀(k, γ)∈(f(k,γ)). line_integral_exists F basis γ"
              using f_props(1) line_integral_exists_on_chain2 ass
              by blast
            have vpath: " ∀(k, γ)∈(f(k, γ)). valid_path γ"
              using f_props(1) assms ass
              by blast
            show "one_chain_line_integral F basis (f (k, γ)) = k * line_integral F basis γ"
            proof(cases "k = 1")
              assume k_eq_1: "k = 1"
              have "one_chain_line_integral F basis (f (k, γ)) = line_integral F basis γ"
                using f_props(2) k_eq_1 line_integral_on_path_eq_line_integral_on_equiv_chain bchain wexist vpath ass finite_basis
                by auto
              then show "one_chain_line_integral F basis (f (k, γ)) = k * line_integral F basis γ"
                using k_eq_1  by auto
            next
              assume "k ≠ 1"
              then have k_eq_neg1: "k = -1"
                using ass boundary_chain1
                by (auto simp add: boundary_chain_def)
              have "one_chain_line_integral F basis (f (k, γ)) = line_integral F basis (reversepath γ)"
                using f_props(2) k_eq_neg1 line_integral_on_path_eq_line_integral_on_equiv_chain bchain wexist vpath ass finite_basis
                by auto
              then have "one_chain_line_integral F basis (f (k, γ)) = - (line_integral F basis γ)"
                using line_integral_on_reverse_path(1) ass line_integral_exists_on_chain1
                  valid_subdiv_imp_valid_one_chain[OF chain1_eq_chain2 boundary_chain1 boundary_chain2 valid_path]
                by force
              then show "one_chain_line_integral F basis (f (k, γ)) = k * line_integral F basis γ"
                using k_eq_neg1 by auto
            qed
          qed
          then have "(∑(k, γ) ∈ (one_chain1 - {p. f p = {}}). one_chain_line_integral F basis (f (k, γ)))
                   = (∑(k, γ) ∈ (one_chain1 - {p. f p = {}}). k* (line_integral F basis γ))"
            by (auto intro!: Finite_Cartesian_Product.sum_cong_aux)
          then show "(∑one_chain ∈ (f ` (one_chain1 - {p. f p = {}})). one_chain_line_integral F basis one_chain) =
                                                     (∑(k, γ) ∈ (one_chain1 - {p. f p = {}}). k* (line_integral F basis γ))"
            using 0  by auto
        qed
        have "⋀ (k::int) γ. (k, γ) ∈ one_chain1 ⟹ (f (k, γ) = {}) ⟹ (k, γ) ∈ {(k',γ'). k'* (line_integral F basis γ') = 0}"
        proof-
          fix k::"int"
          fix γ::"one_cube"
          assume ass:"(k, γ) ∈ one_chain1"
            "(f (k, γ) = {})"
          then have zero_line_integral:"one_chain_line_integral F basis (f (k, γ)) = 0"
            using one_chain_line_integral_def
            by auto
          have bchain: "boundary_chain (f(k,γ))"
            using f_props(1) boundary_chain2 ass
            by (auto simp add: boundary_chain_def)
          have wexist: "∀(k, γ)∈(f(k,γ)). line_integral_exists F basis γ"
            using f_props(1) line_integral_exists_on_chain2 ass
            by blast
          have vpath: " ∀(k, γ)∈(f(k, γ)). valid_path γ"
            using f_props(1) assms ass by blast
          have "one_chain_line_integral F basis (f (k, γ)) = k * line_integral F basis γ"
          proof(cases "k = 1")
            assume k_eq_1: "k = 1"
            have "one_chain_line_integral F basis (f (k, γ)) = line_integral F basis γ"
              using f_props(2) k_eq_1 line_integral_on_path_eq_line_integral_on_equiv_chain bchain wexist vpath ass finite_basis
              by auto
            then show "one_chain_line_integral F basis (f (k, γ)) = k * line_integral F basis γ"
              using k_eq_1
              by auto
          next
            assume "k ≠ 1"
            then have k_eq_neg1: "k = -1"
              using ass boundary_chain1
              by (auto simp add: boundary_chain_def)
            have "one_chain_line_integral F basis (f (k, γ)) = line_integral F basis (reversepath γ)"
              using f_props(2) k_eq_neg1 line_integral_on_path_eq_line_integral_on_equiv_chain bchain wexist vpath ass finite_basis
              by auto
            then have "one_chain_line_integral F basis (f (k, γ)) = - (line_integral F basis γ)"
              using line_integral_on_reverse_path(1)  ass line_integral_exists_on_chain1
                valid_subdiv_imp_valid_one_chain[OF chain1_eq_chain2 boundary_chain1 boundary_chain2 valid_path]
              by force
            then show "one_chain_line_integral F basis (f (k::int, γ)) = k * line_integral F basis γ"
              using k_eq_neg1  by auto
          qed
          then show "(k, γ) ∈ {(k'::int, γ'). k' * line_integral F basis γ' = 0}"
            using zero_line_integral by auto
        qed
        then have ii:"(∑one_chain ∈ (f ` (one_chain1 - {p. f p = {}})). one_chain_line_integral F basis one_chain) =
                                                          (∑one_chain ∈ (f ` (one_chain1)). one_chain_line_integral F basis one_chain)"
        proof -
          have "⋀one_chain. one_chain ∈ (f ` (one_chain1)) - (f ` (one_chain1 - {p. f p = {}})) ⟹
                                                         one_chain_line_integral F basis one_chain = 0"
          proof -
            fix one_chain
            assume "one_chain ∈ (f ` (one_chain1)) - (f ` (one_chain1 - {p. f p = {}}))"
            then show "one_chain_line_integral F basis one_chain = 0"
              by (auto simp add: one_chain_line_integral_def)
          qed
          then have 0:"(∑one_chain ∈ f ` (one_chain1) - (f ` (one_chain1 - {p. f p = {}})). one_chain_line_integral F basis one_chain)
                                                       = 0"
            using comm_monoid_add_class.sum.neutral by auto
          then have "(∑one_chain ∈ f ` (one_chain1). one_chain_line_integral F basis one_chain)
                                                      - (∑one_chain ∈ (f ` (one_chain1 - {p. f p = {}})). one_chain_line_integral F basis one_chain)
                                                       = 0"
          proof -
            have finte: "finite (f ` one_chain1)" using finite_chain1 by auto
            show ?thesis
              using Groups_Big.sum_diff[OF finte, of " (f ` (one_chain1 - {p. f p = {}}))"
                  "one_chain_line_integral F basis"]
                0
              by auto
          qed
          then show "(∑one_chain ∈ (f ` (one_chain1 - {p. f p = {}})). one_chain_line_integral F basis one_chain) =
                                                          (∑one_chain ∈ (f ` (one_chain1)). one_chain_line_integral F basis one_chain)"
            by auto
        qed
        have "⋀ (k::int) γ. (k, γ) ∈ one_chain1 ⟹ (f (k, γ) = {}) ⟹ f (k, γ) ∈ {chain. one_chain_line_integral F basis chain = 0}"
        proof-
          fix k::"int"
          fix γ::"one_cube"
          assume ass:"(k, γ) ∈ one_chain1" "(f (k, γ) = {})"
          then have "one_chain_line_integral F basis (f (k, γ)) = 0"
            using one_chain_line_integral_def  by auto
          then show "f (k, γ) ∈ {p'. (one_chain_line_integral F basis p' = 0)}"
            by auto
        qed
        then have iii:"(∑(k::int,γ)∈one_chain1 - {p. f p = {}}. k*(line_integral F basis γ))
                                                 = (∑(k::int,γ)∈one_chain1. k*(line_integral F basis γ))"
        proof-
          have "⋀ k γ. (k,γ)∈one_chain1 - (one_chain1 - {p. f p = {}})
                                                    ⟹ k* (line_integral F basis γ) = 0"
          proof-
            fix k γ
            assume ass: "(k,γ)∈one_chain1 - (one_chain1 - {p. f p = {}})"
            then have "f(k, γ) = {}"
              by auto
            then have "one_chain_line_integral F basis (f(k, γ)) = 0"
              by (auto simp add: one_chain_line_integral_def)
            then have zero_line_integral:"one_chain_line_integral F basis (f (k, γ)) = 0"
              using one_chain_line_integral_def by auto
            have bchain: "boundary_chain (f(k,γ))"
              using f_props(1) boundary_chain2 ass
              by (auto simp add: boundary_chain_def)
            have wexist: "∀(k, γ)∈(f(k,γ)). line_integral_exists F basis γ"
              using f_props(1) line_integral_exists_on_chain2 ass
              by blast
            have vpath: " ∀(k, γ)∈(f(k, γ)). valid_path γ"
              using f_props(1) assms ass
              by blast
            have "one_chain_line_integral F basis (f (k, γ)) = k * line_integral F basis γ"
            proof(cases "k = 1")
              assume k_eq_1: "k = 1"
              have "one_chain_line_integral F basis (f (k, γ)) = line_integral F basis γ"
                using f_props(2) k_eq_1 line_integral_on_path_eq_line_integral_on_equiv_chain bchain wexist vpath ass finite_basis
                by auto
              then show "one_chain_line_integral F basis (f (k, γ)) = k * line_integral F basis γ"
                using k_eq_1
                by auto
            next
              assume "k ≠ 1"
              then have k_eq_neg1: "k = -1"
                using ass boundary_chain1
                by (auto simp add: boundary_chain_def)
              have "one_chain_line_integral F basis (f (k, γ)) = line_integral F basis (reversepath γ)"
                using f_props(2) k_eq_neg1 line_integral_on_path_eq_line_integral_on_equiv_chain bchain wexist vpath ass finite_basis
                by auto
              then have "one_chain_line_integral F basis (f (k, γ)) = - (line_integral F basis γ)"
                using line_integral_on_reverse_path(1)  ass line_integral_exists_on_chain1
                  valid_subdiv_imp_valid_one_chain[OF chain1_eq_chain2 boundary_chain1 boundary_chain2 valid_path]
                by force
              then show "one_chain_line_integral F basis (f (k, γ)) = k * line_integral F basis γ"
                using k_eq_neg1
                by auto
            qed
            then show "k* (line_integral F basis γ) = 0"
              using zero_line_integral
              by auto
          qed
          then have "∀(k::int,γ)∈one_chain1 - (one_chain1 - {p. f p = {}}).
                                                      k* (line_integral F basis γ) = 0" by auto
          then have "(∑(k::int,γ)∈one_chain1 - (one_chain1 - {p. f p = {}}). k*(line_integral F basis γ)) = 0"
            using Groups_Big.comm_monoid_add_class.sum.neutral
              [of "one_chain1 - (one_chain1 - {p. f p = {}})" "(λ(k::int,γ). k* (line_integral F basis γ))"]
            by (simp add: split_beta)
          then have "(∑(k::int,γ)∈one_chain1. k*(line_integral F basis γ)) -
                     (∑(k::int,γ)∈ (one_chain1 - {p. f p = {}}). k*(line_integral F basis γ)) = 0"
            using Groups_Big.sum_diff[OF finite_chain1]
            by (metis (no_types) Diff_subset ‹(∑(k, γ)∈one_chain1 - (one_chain1 - {p. f p = {}}). k * line_integral F basis γ) = 0› ‹⋀f B. B ⊆ one_chain1 ⟹ sum f (one_chain1 - B) = sum f one_chain1 - sum f B›)
          then show ?thesis by auto
        qed
        show ?thesis using i ii iii by auto
      qed
      then show ?thesis using one_chain_line_integral_def by auto
    qed
    show ?thesis using 0 1 by auto
  qed
  show "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis subdiv" using 0 1 by auto
qed

lemma one_chain_line_integral_eq_line_integral_on_sudivision':
  assumes chain1_eq_chain2: "chain_subdiv_chain one_chain1 subdiv" and
    boundary_chain1: "boundary_chain one_chain1" and
    boundary_chain2: "boundary_chain subdiv" and
    line_integral_exists_on_chain1: "∀(k, γ) ∈ one_chain1. line_integral_exists F basis γ" and
    valid_path: "∀(k, γ) ∈ subdiv. valid_path γ" and
    finite_chain1: "finite one_chain1" and
    finite_basis: "finite basis"
  shows "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis subdiv"
    "∀(k, γ) ∈ subdiv. line_integral_exists F basis γ"
proof -
  obtain f where f_props:
    "((⋃(f ` one_chain1)) = subdiv)"
    "(∀(k,γ)∈one_chain1. if k = 1 then chain_subdiv_path γ (f(k,γ)) else chain_subdiv_path (reversepath γ) (f(k,γ)))"
    "(∀p∈one_chain1. ∀p'∈one_chain1. p ≠ p' ⟶ f p ∩ f p' = {})"
    "(∀x ∈ one_chain1. finite (f x))"
    using chain1_eq_chain2 chain_subdiv_chain_character by (auto simp add: pairwise_def chain_subdiv_chain_def)
  have finite_chain2: "finite subdiv"
    using finite_chain1 f_props(1) f_props(4) by blast
  have "⋀k γ. (k, γ) ∈ subdiv ⟹ line_integral_exists F basis γ"
  proof -
    fix k γ
    assume ass: "(k, γ) ∈ subdiv"
    then obtain k' γ' where kp_gammap: "(k',γ') ∈ one_chain1" "(k,γ) ∈ f(k',γ')"
      using f_props(1) by fastforce
    show "line_integral_exists F basis γ"
    proof (cases "k' = 1")
      assume k_eq_1: "k' = 1"
      then have i:"chain_subdiv_path γ' (f(k',γ'))"
        using f_props(2) kp_gammap ass  by auto
      have ii:"boundary_chain (f(k',γ'))"
        using f_props(1) ass assms kp_gammap  by (meson UN_I boundary_chain_def)
      have iii:"line_integral_exists F basis γ'"
        using assms kp_gammap by blast
      have "iv": " ∀(k, γ)∈f (k', γ'). valid_path γ"
        using f_props(1) ass assms kp_gammap by blast
      show ?thesis
        using line_integral_on_path_eq_line_integral_on_equiv_chain'(2)[OF i ii iii iv finite_basis] kp_gammap
        by auto
    next
      assume "k' ≠ 1"
      then have k_eq_neg1: "k' = -1"
        using boundary_chain1 kp_gammap
        by (auto simp add: boundary_chain_def)
      then have i:"chain_subdiv_path (reversepath γ') (f(k',γ'))"
        using f_props(2) kp_gammap by auto
      have ii:"boundary_chain (f(k',γ'))"
        using f_props(1) assms kp_gammap  by (meson UN_I boundary_chain_def)
      have iii: " ∀(k, γ)∈f (k', γ'). valid_path γ"
        using f_props(1) ass assms kp_gammap by blast
      have iv: "valid_path (reversepath γ')"
        using valid_path_equiv_valid_chain_list[OF i ii iii]
        by force
      have "line_integral_exists F basis γ'"
        using assms kp_gammap  by blast
      then have x: "line_integral_exists F basis (reversepath γ')"
        using iv line_integral_on_reverse_path(2) valid_path_reversepath
        by fastforce
      show ?thesis
        using line_integral_on_path_eq_line_integral_on_equiv_chain'(2)[OF i ii x iii finite_basis] kp_gammap
        by auto
    qed
  qed
  then show "∀(k, γ)∈subdiv. line_integral_exists F basis γ" by auto
  then show "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis subdiv"
    using one_chain_line_integral_eq_line_integral_on_sudivision(1) assms
    by auto
qed

lemma line_integral_sum_gen:
  assumes finite_basis:
    "finite basis" and
    line_integral_exists:
    "line_integral_exists F basis1 γ"
    "line_integral_exists F basis2 γ" and
    basis_partition:
    "basis1 ∪ basis2 = basis" "basis1 ∩ basis2 = {}"
  shows "line_integral F basis γ = (line_integral F  basis1 γ) + (line_integral F basis2 γ)"
    "line_integral_exists F basis γ"
   apply (simp add: line_integral_def)
proof -
  have 0: "integral {0..1} (λx. (∑b∈basis1. F (γ x) ∙ b * (vector_derivative γ (at x within {0..1}) ∙ b)) +
                                       (∑b∈basis2. F (γ x) ∙ b * (vector_derivative γ (at x within {0..1}) ∙ b))) =
                    integral {0..1} (λx. ∑b∈basis1. F (γ x) ∙ b * (vector_derivative γ (at x within {0..1}) ∙ b)) +
                           integral {0..1} (λx. ∑b∈basis2. F (γ x) ∙ b * (vector_derivative γ (at x within {0..1}) ∙ b))"
    using Henstock_Kurzweil_Integration.integral_add line_integral_exists
    by (auto simp add: line_integral_exists_def)
  have 1: "integral {0..1} (λx. ∑b∈basis. F (γ x) ∙ b * (vector_derivative γ (at x within {0..1}) ∙ b)) =
                       integral {0..1} (λx. (∑b∈basis1. F (γ x) ∙ b * (vector_derivative γ (at x within {0..1}) ∙ b)) +
                                            (∑b∈basis2. F (γ x) ∙ b * (vector_derivative γ (at x within {0..1}) ∙ b)))"
    by (metis (mono_tags, lifting) basis_partition finite_Un finite_basis sum.union_disjoint)
  show "integral {0..1} (λx. ∑b∈basis. F (γ x) ∙ b * (vector_derivative γ (at x within {0..1}) ∙ b)) =
                  integral {0..1} (λx. ∑b∈basis1. F (γ x) ∙ b * (vector_derivative γ (at x within {0..1}) ∙ b)) +
                  integral {0..1} (λx. ∑b∈basis2. F (γ x) ∙ b * (vector_derivative γ (at x within {0..1}) ∙ b))"
    using 0 1
    by auto
  have 2: "((λx. (∑b∈basis1. F (γ x) ∙ b * (vector_derivative γ (at x within {0..1}) ∙ b)) +
                                       (∑b∈basis2. F (γ x) ∙ b * (vector_derivative γ (at x within {0..1}) ∙ b))) has_integral
                    integral {0..1} (λx. ∑b∈basis1. F (γ x) ∙ b * (vector_derivative γ (at x within {0..1}) ∙ b)) +
                           integral {0..1} (λx. ∑b∈basis2. F (γ x) ∙ b * (vector_derivative γ (at x within {0..1}) ∙ b))) {0..1}"
    using Henstock_Kurzweil_Integration.has_integral_add line_integral_exists has_integral_integral
    apply (auto simp add: line_integral_exists_def)
    by blast
  have 3: "(λx. ∑b∈basis. F (γ x) ∙ b * (vector_derivative γ (at x within {0..1}) ∙ b)) =
                       (λx. (∑b∈basis1. F (γ x) ∙ b * (vector_derivative γ (at x within {0..1}) ∙ b)) +
                                            (∑b∈basis2. F (γ x) ∙ b * (vector_derivative γ (at x within {0..1}) ∙ b)))"
    by (metis (mono_tags, lifting) basis_partition finite_Un finite_basis sum.union_disjoint)
  show "line_integral_exists F basis γ"
    apply(auto simp add: line_integral_exists_def has_integral_integral)
    using 2 3
    using has_integral_integrable_integral by fastforce
qed

definition common_boundary_sudivision_exists where
    "common_boundary_sudivision_exists one_chain1 one_chain2 ≡
             ∃subdiv. chain_subdiv_chain one_chain1 subdiv ∧
                      chain_subdiv_chain one_chain2 subdiv ∧
                      (∀(k, γ) ∈ subdiv. valid_path γ)∧
                      boundary_chain subdiv"

lemma common_boundary_sudivision_commutative:
  "(common_boundary_sudivision_exists one_chain1 one_chain2) = (common_boundary_sudivision_exists one_chain2 one_chain1)"
  apply (simp add: common_boundary_sudivision_exists_def)
  by blast

lemma common_subdivision_imp_eq_line_integral:
  assumes "(common_boundary_sudivision_exists one_chain1 one_chain2)"
    "boundary_chain one_chain1"
    "boundary_chain one_chain2"
    "∀(k, γ)∈one_chain1. line_integral_exists F basis γ"
    "finite one_chain1"
    "finite one_chain2"
    "finite basis"
  shows "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2"
    "∀(k, γ)∈one_chain2. line_integral_exists F basis γ"
proof -
  obtain subdiv where subdiv_props:
    "chain_subdiv_chain one_chain1 subdiv"
    "chain_subdiv_chain one_chain2 subdiv"
    "(∀(k, γ) ∈ subdiv. valid_path γ)"
    "(boundary_chain subdiv)"
    using assms
    by (auto simp add: common_boundary_sudivision_exists_def)
  have i: "∀(k, γ)∈subdiv. line_integral_exists F basis γ"
    using one_chain_line_integral_eq_line_integral_on_sudivision'(2)[OF subdiv_props(1) assms(2) subdiv_props(4) assms(4) subdiv_props(3) assms(5) assms(7)]
    by auto
  show "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2"
    using one_chain_line_integral_eq_line_integral_on_sudivision'(1)[OF subdiv_props(1) assms(2) subdiv_props(4) assms(4) subdiv_props(3) assms(5) assms(7)]
      one_chain_line_integral_eq_line_integral_on_sudivision(1)[OF subdiv_props(2) assms(3) subdiv_props(4) i subdiv_props(3) assms(6) assms(7)]
    by auto
  show "∀(k, γ)∈one_chain2. line_integral_exists F basis γ"
    using one_chain_line_integral_eq_line_integral_on_sudivision(2)[OF subdiv_props(2) assms(3) subdiv_props(4) i subdiv_props(3) assms(6) assms(7)]
    by auto
qed

definition common_sudiv_exists where
    "common_sudiv_exists one_chain1 one_chain2 ≡
        ∃subdiv ps1 ps2. chain_subdiv_chain (one_chain1 - ps1) subdiv ∧
                  chain_subdiv_chain (one_chain2 - ps2) subdiv ∧
                  (∀(k, γ) ∈ subdiv. valid_path γ) ∧
                  (boundary_chain subdiv) ∧
                  (∀(k, γ) ∈ ps1. point_path γ) ∧
                  (∀(k, γ) ∈ ps2. point_path γ)"

lemma common_sudiv_exists_comm:
  shows "common_sudiv_exists C1 C2 = common_sudiv_exists C2 C1"
  by (auto simp add: common_sudiv_exists_def)

lemma line_integral_degenerate_chain:
  assumes "(∀(k, γ) ∈ chain. point_path γ)"
  assumes "finite basis"
  shows "one_chain_line_integral F basis chain = 0"
proof (simp add: one_chain_line_integral_def)
  have "∀(k,g)∈chain. line_integral F basis g = 0"
    using assms line_integral_point_path
    by blast
  then have "∀(k,g)∈chain. real_of_int k * line_integral F basis g = 0" by auto
  then have "⋀p. p ∈ chain ⟹ (case p of (i, f) ⇒ real_of_int i * line_integral F basis f) = 0"
    by fastforce
  then show "(∑x∈chain. case x of (k, g) ⇒ real_of_int k * line_integral F basis g) = 0"
    by simp
qed

lemma gen_common_subdiv_imp_common_subdiv:
  shows "(common_sudiv_exists one_chain1 one_chain2) = (∃ps1 ps2. (common_boundary_sudivision_exists (one_chain1 - ps1) (one_chain2 - ps2)) ∧ (∀(k, γ)∈ps1. point_path γ) ∧ (∀(k, γ)∈ps2. point_path γ))"
  by (auto simp add: common_sudiv_exists_def common_boundary_sudivision_exists_def)

lemma common_subdiv_imp_gen_common_subdiv:
  assumes "(common_boundary_sudivision_exists one_chain1 one_chain2)"
  shows "(common_sudiv_exists one_chain1 one_chain2)"
  using assms
  apply (auto simp add: common_sudiv_exists_def common_boundary_sudivision_exists_def)
  by (metis Diff_empty all_not_in_conv)

lemma one_chain_line_integral_point_paths:
  assumes "finite one_chain"
  assumes "finite basis"
  assumes "(∀(k, γ)∈ps. point_path γ)"
  shows "one_chain_line_integral F basis (one_chain - ps) = one_chain_line_integral F basis (one_chain)"
proof-
  have 0:"(∀x∈ps. case x of (k, g) ⇒  (real_of_int k * line_integral F basis g) = 0)"
    using line_integral_point_path assms
    by force
  show "one_chain_line_integral F basis (one_chain - ps) = one_chain_line_integral F basis one_chain"
    unfolding one_chain_line_integral_def using 0 ‹finite one_chain›
    by (force simp add:  intro: comm_monoid_add_class.sum.mono_neutral_left)
qed

lemma boundary_chain_diff:
  assumes "boundary_chain one_chain"
  shows "boundary_chain (one_chain - s)"
  using assms
  by (auto simp add: boundary_chain_def)

lemma gen_common_subdivision_imp_eq_line_integral:
  assumes "(common_sudiv_exists one_chain1 one_chain2)"
    "boundary_chain one_chain1"
    "boundary_chain one_chain2"
    "∀(k, γ)∈one_chain1. line_integral_exists F basis γ"
    "finite one_chain1"
    "finite one_chain2"
    "finite basis"
  shows "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2"
    "∀(k, γ)∈one_chain2. line_integral_exists F basis γ"
proof -
  obtain ps1 ps2 where gen_subdiv: "(common_boundary_sudivision_exists (one_chain1 - ps1) (one_chain2 - ps2))" "(∀(k, γ)∈ps1. point_path γ)" " (∀(k, γ)∈ps2. point_path γ)"
    using assms(1) gen_common_subdiv_imp_common_subdiv
    by blast
  show "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2"
    using one_chain_line_integral_point_paths gen_common_subdiv_imp_common_subdiv
      assms(2-7) gen_subdiv
      common_subdivision_imp_eq_line_integral(1)[OF gen_subdiv(1) boundary_chain_diff[OF assms(2)] boundary_chain_diff[OF assms(3)]]
    by auto
  show "∀(k, γ)∈one_chain2. line_integral_exists F basis γ"
  proof-
    obtain subdiv where subdiv_props:
      "chain_subdiv_chain (one_chain1-ps1) subdiv"
      "chain_subdiv_chain (one_chain2-ps2) subdiv"
      "(∀(k, γ) ∈ subdiv. valid_path γ)"
      "(boundary_chain subdiv)"
      using gen_subdiv(1)
      by (auto simp add: common_boundary_sudivision_exists_def)
    have "∀(k, γ)∈subdiv. line_integral_exists F basis γ"
      using one_chain_line_integral_eq_line_integral_on_sudivision'(2)[OF subdiv_props(1) boundary_chain_diff[OF assms(2)] subdiv_props(4)] assms(4) subdiv_props(3) assms(5) assms(7)
      by blast
    then have i: "∀(k, γ)∈one_chain2-ps2. line_integral_exists F basis γ"
      using one_chain_line_integral_eq_line_integral_on_sudivision(2)[OF subdiv_props(2) boundary_chain_diff[OF assms(3)] subdiv_props(4)] subdiv_props(3) assms(6) assms(7)
      by blast
    then show ?thesis
      using  gen_subdiv(3) line_integral_exists_point_path[OF assms(7)]
      by blast
  qed      
qed

lemma common_sudiv_exists_refl:
      assumes "common_sudiv_exists C1 C2"
      shows "common_sudiv_exists C2 C1"
      using assms
      apply(simp add: common_sudiv_exists_def)
      by auto

lemma chain_subdiv_path_singleton:
  shows "chain_subdiv_path γ {(1,γ)}" 
proof -
  have "rec_join [(1,γ)] = γ"
    by (simp add: joinpaths_def)
  then have "set [(1,γ)] = {(1, γ)}" "distinct [(1,γ)]" "rec_join [(1,γ)] = γ" "valid_chain_list [(1,γ)]"
    by auto
  then show ?thesis
    by (metis (no_types) chain_subdiv_path.intros)
qed

lemma chain_subdiv_path_singleton_reverse:
  shows "chain_subdiv_path (reversepath γ) {(-1,γ)}"
proof -
  have "rec_join [(-1,γ)] = reversepath γ"
    by (simp add: joinpaths_def)
  then have "set [(-1,γ)] = {(- 1, γ)}" "distinct [(-1,γ)]" 
             "rec_join [(-1,γ)] = reversepath γ" "valid_chain_list [(-1,γ)]"
    by auto
  then  have "chain_subdiv_path (reversepath γ) (set [(- 1, γ)])"
    using chain_subdiv_path.intros by blast
  then show ?thesis
    by simp
qed

lemma chain_subdiv_chain_refl:
  assumes "boundary_chain C"
  shows "chain_subdiv_chain C C"
  using chain_subdiv_path_singleton chain_subdiv_path_singleton_reverse assms
  unfolding chain_subdiv_chain_def boundary_chain_def pairwise_def using case_prodI2 coeff_cube_to_path.simps 
  by (rule_tac x="λx. {x}" in exI) auto

(*path reparam_weaketrization*)

definition reparam_weak where
  "reparam_weak γ1 γ2 ≡ ∃φ. (∀x∈{0..1}. γ1 x = (γ2 o φ) x) ∧ φ piecewise_C1_differentiable_on {0..1} ∧ φ(0) = 0 ∧ φ(1) = 1 ∧ φ ` {0..1} = {0..1}"

definition reparam where
  "reparam γ1 γ2 ≡ ∃φ. (∀x∈{0..1}. γ1 x = (γ2 o φ) x) ∧ φ piecewise_C1_differentiable_on {0..1} ∧ φ(0) = 0 ∧ φ(1) = 1 ∧ bij_betw φ {0..1} {0..1} ∧ φ -` {0..1} ⊆ {0..1} ∧ (∀x∈{0..1}. finite (φ -` {x}))"

lemma reparam_weak_eq_refl:
  shows "reparam_weak γ1 γ1"
  unfolding reparam_weak_def
  apply (rule_tac x="id" in exI)
  by (auto simp add: id_def piecewise_C1_differentiable_on_def C1_differentiable_on_def continuous_on_id)

lemma line_integral_exists_smooth_one_base:
  assumes "γ C1_differentiable_on {0..1}" (*To generalise this to valid_path we need a version of has_integral_substitution_strong that allows finite discontinuities of f*)
    "continuous_on (path_image γ) (λx. F x ∙ b)"
  shows "line_integral_exists F {b} γ"
proof-
  have gamma2_differentiable: "(∀x ∈ {0 .. 1}. γ differentiable at x)"
    using assms(1) 
    by (auto simp add: valid_path_def C1_differentiable_on_eq)
  then have gamma2_b_component_differentiable: "(∀x ∈ {0 .. 1}. (λx. (γ x) ∙ b) differentiable at x)"
    by auto
  then have "(λx. (γ x) ∙ b) differentiable_on {0..1}"
    using differentiable_at_withinI
    by (auto simp add: differentiable_on_def)
  then have gama2_cont_comp: "continuous_on {0..1} (λx. (γ x) ∙ b)"
    using differentiable_imp_continuous_on
    by auto
  have gamma2_cont:"continuous_on {0..1} γ"
    using assms(1) C1_differentiable_imp_continuous_on
    by (auto simp add: valid_path_def)
  have iii: "continuous_on {0..1} (λx. F (γ x) ∙ b * (vector_derivative γ (at x within {0..1}) ∙ b))"
  proof-
    have 0: "continuous_on {0..1} (λx. F (γ x) ∙ b)"
      using assms(2) continuous_on_compose[OF gamma2_cont]
      by (auto simp add: path_image_def) 
    obtain D where D: "(∀x∈{0..1}. (γ has_vector_derivative D x) (at x)) ∧ continuous_on {0..1} D"
      using assms(1)
      by (auto simp add: C1_differentiable_on_def)
    then have *:"∀x∈{0..1}. vector_derivative γ (at x within{0..1}) = D x"
      using vector_derivative_at vector_derivative_at_within_ivl
      by fastforce
    then have "continuous_on {0..1} (λx. vector_derivative γ (at x within{0..1}))"
      using continuous_on_eq D by force
    then have 1: "continuous_on {0..1} (λx. (vector_derivative γ (at x within{0..1})) ∙ b)"
      by(auto intro!: continuous_intros)
    show ?thesis
      using continuous_on_mult[OF 0 1]  by auto
  qed
  then have "(λx. F (γ x) ∙ b * (vector_derivative γ (at x within {0..1}) ∙ b)) integrable_on {0..1}"
    using integrable_continuous_real
    by auto
  then show "line_integral_exists F {b} γ"
    by(auto simp add: line_integral_exists_def)
qed

lemma contour_integral_primitive_lemma:
  fixes f :: "complex ⇒ complex" and g :: "real ⇒ complex"
  assumes "a ≤ b"
      and "⋀x. x ∈ s ⟹ (f has_field_derivative f' x) (at x within s)"
      and "g piecewise_differentiable_on {a..b}"  "⋀x. x ∈ {a..b} ⟹ g x ∈ s"
    shows "((λx. f'(g x) * vector_derivative g (at x within {a..b}))
             has_integral (f(g b) - f(g a))) {a..b}"
proof -
  obtain k where k: "finite k" "∀x∈{a..b} - k. g differentiable (at x within {a..b})" and cg: "continuous_on {a..b} g"
    using assms by (auto simp: piecewise_differentiable_on_def)
  have cfg: "continuous_on {a..b} (λx. f (g x))"
    apply (rule continuous_on_compose [OF cg, unfolded o_def])
    using assms
    apply (metis field_differentiable_def field_differentiable_imp_continuous_at continuous_on_eq_continuous_within continuous_on_subset image_subset_iff)
    done
  { fix x::real
    assume a: "a < x" and b: "x < b" and xk: "x ∉ k"
    then have "g differentiable at x within {a..b}"
      using k by (simp add: differentiable_at_withinI)
    then have "(g has_vector_derivative vector_derivative g (at x within {a..b})) (at x within {a..b})"
      by (simp add: vector_derivative_works has_field_derivative_def scaleR_conv_of_real)
    then have gdiff: "(g has_derivative (λu. u * vector_derivative g (at x within {a..b}))) (at x within {a..b})"
      by (simp add: has_vector_derivative_def scaleR_conv_of_real)
    have "(f has_field_derivative (f' (g x))) (at (g x) within g ` {a..b})"
      using assms by (metis a atLeastAtMost_iff b DERIV_subset image_subset_iff less_eq_real_def)
    then have fdiff: "(f has_derivative (*) (f' (g x))) (at (g x) within g ` {a..b})"
      by (simp add: has_field_derivative_def)
    have "((λx. f (g x)) has_vector_derivative f' (g x) * vector_derivative g (at x within {a..b})) (at x within {a..b})"
      using diff_chain_within [OF gdiff fdiff]
      by (simp add: has_vector_derivative_def scaleR_conv_of_real o_def mult_ac)
  } note * = this
  show ?thesis
    apply (rule fundamental_theorem_of_calculus_interior_strong)
    using k assms cfg *
    apply (auto simp: at_within_Icc_at)
    done
qed

lemma line_integral_primitive_lemma: (*Only for real normed fields, i.e. vectors with products*)
  fixes f :: "'a::{euclidean_space,real_normed_field} ⇒ 'a::{euclidean_space,real_normed_field}" and
        g :: "real ⇒ 'a"
  assumes "⋀(a::'a). a ∈ s ⟹ (f has_field_derivative (f' a)) (at a within s)"
      and "g piecewise_differentiable_on {0::real..1}"  "⋀x. x ∈ {0..1} ⟹ g x ∈ s"
      and "base_vec ∈ Basis"
    shows "((λx. ((f'(g x)) * (vector_derivative g (at x within {0..1}))) ∙ base_vec)
             has_integral (((f(g 1)) ∙ base_vec - (f(g 0)) ∙ base_vec))) {0..1}"
proof -
  obtain k where k: "finite k" "∀x∈{0..1} - k. g differentiable (at x within {0..1})" and cg: "continuous_on {0..1} g"
    using assms by (auto simp: piecewise_differentiable_on_def)
  have cfg: "continuous_on {0..1} (λx. f (g x))"
    apply (rule continuous_on_compose [OF cg, unfolded o_def])
    using assms
    apply (metis field_differentiable_def field_differentiable_imp_continuous_at continuous_on_eq_continuous_within continuous_on_subset image_subset_iff)
    done
  { fix x::real
    assume a: "0 < x" and b: "x < 1" and xk: "x ∉ k"
    then have "g differentiable at x within {0..1}"
      using k by (simp add: differentiable_at_withinI)
    then have "(g has_vector_derivative vector_derivative g (at x within {0..1})) (at x within {0..1})"
      by (simp add: vector_derivative_works has_field_derivative_def scaleR_conv_of_real)
    then have gdiff: "(g has_derivative (λu. of_real u * vector_derivative g (at x within {0..1}))) (at x within {0..1})"
      by (simp add: has_vector_derivative_def scaleR_conv_of_real)
    have "(f has_field_derivative (f' (g x))) (at (g x) within g ` {0..1})"
      using assms by (metis a atLeastAtMost_iff b DERIV_subset image_subset_iff less_eq_real_def)
    then have fdiff: "(f has_derivative (*) (f' (g x))) (at (g x) within g ` {0..1})"
      by (simp add: has_field_derivative_def)
    have "((λx. f (g x)) has_vector_derivative f' (g x) * vector_derivative g (at x within {0..1})) (at x within {0..1})"
      using diff_chain_within [OF gdiff fdiff]
      by (simp add: has_vector_derivative_def scaleR_conv_of_real o_def mult_ac)
  }
  then have *: "⋀x. x∈{0<..<1} - k ⟹ ((λx. f (g x)) has_vector_derivative f' (g x) * vector_derivative g (at x within {0..1})) (at x within {0..1})"
       by auto
  have "((λx. ((f'(g x))) * ((vector_derivative g (at x within {0..1}))))
             has_integral (((f(g 1)) - (f(g 0))))) {0..1}"
    using fundamental_theorem_of_calculus_interior_strong[OF k(1) zero_le_one _ cfg]
    using k assms cfg * by (auto simp: at_within_Icc_at)
  then have "((λx. (((f'(g x))) * ((vector_derivative g (at x within {0..1})))) ∙ base_vec)
             has_integral (((f(g 1)) - (f(g 0)))) ∙ base_vec) {0..1}"
       using has_integral_componentwise_iff assms(4)
       by fastforce
  then show ?thesis using inner_mult_left'
       by (simp add: inner_mult_left' inner_diff_left)
qed

lemma reparam_eq_line_integrals:
  assumes reparam: "reparam γ1 γ2" and
    pw_smooth: "γ2 piecewise_C1_differentiable_on {0..1}" and (*To generalise this to valid_path we need a version of has_integral_substitution_strong that allows finite discontinuities of f*)
    cont: "continuous_on (path_image γ2) (λx. F x ∙ b)" and
    line_integral_ex: "line_integral_exists F {b} γ2" (*We need to remove this and work on special cases like conservative fields and field/line combinations that satisfy the improper integrals theorem assumptions*)
  shows "line_integral F {b} γ1 = line_integral F {b} γ2"
    "line_integral_exists F {b} γ1"
proof-
  obtain φ where phi: "(∀x∈{0..1}. γ1 x = (γ2 o φ) x)"" φ piecewise_C1_differentiable_on {0..1}"" φ(0) = 0"" φ(1) = 1""bij_betw φ {0..1} {0..1}" "φ -` {0..1} ⊆ {0..1}" "∀x∈{0..1}. finite (φ -` {x})"
    using reparam
    by (auto simp add: reparam_def)
  obtain s where s: "finite s" "φ C1_differentiable_on {0..1} - s"
    using phi
    by(auto simp add: reparam_def piecewise_C1_differentiable_on_def)
  let ?s = "s ∩ {0..1}"
  have s_inter: "finite ?s" "φ C1_differentiable_on {0..1} - ?s"
    using s
     apply blast
    by (metis Diff_Compl Diff_Diff_Int Diff_eq inf.commute s(2))
  have cont_phi: "continuous_on {0..1} φ"
    using phi
    by(auto simp add: reparam_def piecewise_C1_differentiable_on_imp_continuous_on)
  obtain s' D where s'_D: "finite s'" "(∀x ∈ {0 .. 1} - s'. γ2 differentiable at x)" "(∀x∈{0..1} - s'. (γ2 has_vector_derivative D x) (at x)) ∧ continuous_on ({0..1} - s') D"
    using pw_smooth 
    apply (auto simp add: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
    by (simp add: vector_derivative_works)
  let ?s' = "s' ∩ {0..1}"
  have gamma2_differentiable: "finite ?s'" "(∀x ∈ {0 .. 1} - ?s'. γ2 differentiable at x)" "(∀x∈{0..1} - ?s'. (γ2 has_vector_derivative D x) (at x)) ∧ continuous_on ({0..1} - ?s') D"
    using s'_D
      apply blast
    using s'_D(2) apply auto[1]
    by (metis Diff_Int2 inf_top.left_neutral s'_D(3))
  then have gamma2_b_component_differentiable: "(∀x ∈ {0 .. 1} - ?s'. (λx. (γ2 x) ∙ b) differentiable at x)"
    using differentiable_inner by force
  then have "(λx. (γ2 x) ∙ b) differentiable_on {0..1} - ?s'"
    using differentiable_at_withinI
    by (auto simp add: differentiable_on_def)
  then have gama2_cont_comp: "continuous_on ({0..1} - ?s') (λx. (γ2 x) ∙ b)"
    using differentiable_imp_continuous_on
    by auto
      (**********Additional needed assumptions ************)
  have s_in01: "?s ⊆ {0..1}" by auto
  have s'_in01: "?s' ⊆ {0..1}" by auto
  have phi_backimg_s': "φ -` {0..1} ⊆ {0..1}" using phi by auto
  have "inj_on φ {0..1}" using phi(5) by (auto simp add: bij_betw_def)
  have bij_phi: "bij_betw φ {0..1} {0..1}" using phi(5) by auto
  have finite_bck_img_single: "∀x∈{0..1}. finite (φ -` {x})" using phi by auto
  then have finite_bck_img_single_s': " ∀x∈?s'. finite (φ -` {x})" by auto
  have gamma2_line_integrable: "(λx. F (γ2 x) ∙ b * (vector_derivative γ2 (at x within {0..1}) ∙ b)) integrable_on {0..1}"
    using line_integral_ex
    by (simp add: line_integral_exists_def)
      (****************************************************************)
  have finite_neg_img: "finite (φ -` ?s')"
    using finite_bck_img_single
    by (metis Int_iff finite_Int gamma2_differentiable(1) image_vimage_eq inf_img_fin_dom')
  have gamma2_cont:"continuous_on ({0..1} - ?s') γ2"
    using  gamma2_differentiable
    by (meson continuous_at_imp_continuous_on differentiable_imp_continuous_within)
  have iii: "continuous_on ({0..1} - ?s') (λx. F (γ2 x) ∙ b * (vector_derivative γ2 (at x within {0..1}) ∙ b))"
  proof-
    have 0: "continuous_on ({0..1} - ?s') (λx. F (γ2 x) ∙ b)"
      using cont continuous_on_compose[OF gamma2_cont] continuous_on_compose2 gamma2_cont
      unfolding path_image_def  by fastforce
    have D: "(∀x∈{0..1} - ?s'. (γ2 has_vector_derivative D x) (at x)) ∧ continuous_on ({0..1} - ?s') D"
      using gamma2_differentiable
      by auto                       
    then have *:"∀x∈{0..1} - ?s'. vector_derivative γ2 (at x within{0..1}) = D x"
      using vector_derivative_at vector_derivative_at_within_ivl
      by fastforce
    then have "continuous_on ({0..1} - ?s') (λx. vector_derivative γ2 (at x within{0..1}))"
      using continuous_on_eq D
      by metis
    then have 1: "continuous_on ({0..1} - ?s') (λx. (vector_derivative γ2 (at x within{0..1})) ∙ b)"
      by (auto intro!: continuous_intros)
    show ?thesis
      using continuous_on_mult[OF 0 1]
      by auto
  qed
  have iv: "φ(0) ≤ φ(1)"
    using phi(3) phi(4)
    by (simp add: reparam_def)
  have v: "φ`{0..1} ⊆ {0..1}"
    using phi
    by (auto simp add: reparam_def bij_betw_def)
  obtain D where D_props: "(∀x∈{0..1} - ?s. (φ has_vector_derivative D x) (at x))"
    using s
    by (auto simp add: C1_differentiable_on_def)
  then have "(⋀x. x ∈ ({0..1} - ?s) ⟹ (φ has_vector_derivative D x) (at x within {0..1}))"
    using has_vector_derivative_at_within
    by blast
  then have vi: "(⋀x. x ∈ ({0..1} - ?s) ⟹ (φ has_real_derivative D x) (at x within {0..1}))"
    using has_real_derivative_iff_has_vector_derivative
    by blast
  have a:"((λx. D x * (F (γ2 (φ x)) ∙ b * (vector_derivative γ2 (at (φ x) within {0..1}) ∙ b))) has_integral
              integral {φ 0..φ 1} (λx. F (γ2 x) ∙ b * (vector_derivative γ2 (at x within {0..1}) ∙ b)))
              ({0..1})"
  proof-
    have a: "integral {φ 1..φ 0} (λx. F (γ2 x) ∙ b * (vector_derivative γ2 (at x within {0..1}) ∙ b)) = 0" using integral_singleton integral_empty iv
      by (simp add: phi(3) phi(4))
    have b: "((λx. D x *⇩R (F (γ2 (φ x)) ∙ b * (vector_derivative γ2 (at (φ x) within {0..1}) ∙ b))) has_integral
                       integral {φ 0..φ 1} (λx. F (γ2 x) ∙ b * (vector_derivative γ2 (at x within {0..1}) ∙ b)) - integral {φ 1..φ 0} (λx. F (γ2 x) ∙ b * (vector_derivative γ2 (at x within {0..1}) ∙ b)))
                           {0..1}"
      apply(rule  has_integral_substitution_general_'[OF s_inter(1) zero_le_one gamma2_differentiable(1) v gamma2_line_integrable iii cont_phi finite_bck_img_single_s'])
    proof-
      have "surj_on {0..1} φ"
        using bij_phi
        by (metis (full_types) bij_betw_def image_subsetI rangeI)
      then show "surj_on ?s' φ" using bij_phi s'_in01
        by blast
      show "inj_on φ ({0..1} ∪ (?s ∪ φ -` ?s'))"
      proof-
        have i: "inj_on φ {0..1}" using  bij_phi 
          using bij_betw_def by blast
        have ii: "({0..1} ∪ (?s ∪ φ -` ?s')) = {0..1}" using phi_backimg_s' s_in01 s'_in01
          by blast
        show ?thesis using i ii by auto
      qed
      show "⋀x. x ∈ {0..1} - ?s ⟹ (φ has_real_derivative D x) (at x within {0..1})"
        using vi by blast
    qed
    show ?thesis using a b by auto
  qed
  then have b: "integral {0..1} (λx. D x * (F (γ2 (φ x)) ∙ b * (vector_derivative γ2 (at (φ x) within {0..1}) ∙ b))) = 
                       integral {φ 0..φ 1} (λx. F (γ2 x) ∙ b * (vector_derivative γ2 (at x within {0..1}) ∙ b))"
    by auto
  have gamma2_vec_diffable: "⋀x::real. x ∈ {0..1} - ((φ -` ?s') ∪ ?s) ⟹ ((γ2 o φ) has_vector_derivative vector_derivative (γ2 ∘ φ) (at x)) (at x)"
  proof-
    fix x::real 
    assume ass: "x ∈ {0..1} -   ((φ -` ?s') ∪ ?s)"
    have zer_le_x_le_1:"0≤ x ∧ x ≤ 1" using ass
      by simp
    show "((γ2 o φ) has_vector_derivative vector_derivative (γ2 ∘ φ) (at x)) (at x)"
    proof-
      have **: "γ2 differentiable at (φ x)"
        using  gamma2_differentiable(2) ass v 
        by blast
      have ***: " φ differentiable at x"
        using s ass
        by (auto simp add: C1_differentiable_on_eq)
      then show "((γ2 o φ) has_vector_derivative vector_derivative (γ2 ∘ φ) (at x)) (at x)"
        using differentiable_chain_at[OF *** **] 
        by (auto simp add: vector_derivative_works)
    qed
  qed
  then have gamma2_vec_deriv_within: "⋀x::real. x ∈ {0..1} - ((φ -` ?s') ∪ ?s) ⟹ vector_derivative (γ2 ∘ φ) (at x) = vector_derivative (γ2 ∘ φ) (at x within {0..1})"
    using vector_derivative_at_within_ivl[OF gamma2_vec_diffable]
    by auto
  have "∀x∈{0..1} - ((φ -` ?s') ∪ ?s). D x * (vector_derivative γ2 (at (φ x) within {0..1}) ∙ b) = (vector_derivative (γ2 ∘ φ) (at x within {0..1}) ∙ b)"
  proof
    fix x::real
    assume ass: "x ∈ {0..1} -((φ -` ?s') ∪ ?s)"
    then have 0: "φ differentiable (at x)"
      using s by (auto simp add: C1_differentiable_on_def differentiable_def has_vector_derivative_def)
    obtain D2 where "(φ has_vector_derivative D2) (at x)"
      using D_props ass  by blast
    have "φ x ∈ {0..1} - ?s'"
      using phi(5) ass by (metis Diff_Un Diff_iff Int_iff bij_betw_def image_eqI vimageI)
    then have 1: "γ2 differentiable (at (φ x))"
      using gamma2_differentiable
      by auto
    have 3:" vector_derivative γ2 (at (φ x)) =  vector_derivative γ2 (at (φ x) within {0..1})"
    proof-
      have *:"0≤ φ x ∧ φ x ≤ 1" using phi(5) ass
        using ‹φ x ∈ {0..1} - s' ∩ {0..1}› by auto
      then have **:"(γ2 has_vector_derivative (vector_derivative γ2 (at (φ x)))) (at (φ x))"
        using 1 vector_derivative_works  by auto
      show ?thesis
        using * vector_derivative_at_within_ivl[OF **]  by auto
    qed
    show "D x * (vector_derivative γ2 (at (φ x) within {0..1}) ∙ b) = vector_derivative (γ2 ∘ φ) (at x within {0..1}) ∙ b"
      using vector_derivative_chain_at[OF 0 1]
      apply (auto simp add: gamma2_vec_deriv_within[OF ass, symmetric] 3[symmetric])
      using D_props ass vector_derivative_at
      by fastforce
  qed
  then have c:"⋀x.  x∈({0..1} -((φ -` ?s') ∪ ?s)) ⟹ D x * (F (γ2 (φ x)) ∙ b * (vector_derivative γ2 (at (φ x) within {0..1}) ∙ b)) = 
                                    F (γ2 (φ x)) ∙ b * (vector_derivative (γ2 ∘ φ) (at x within {0..1}) ∙ b)"
    by auto
  then have d: "integral ({0..1}) (λx. D x * (F (γ2 (φ x)) ∙ b * (vector_derivative γ2 (at (φ x) within {0..1}) ∙ b))) = 
                                            integral ({0..1}) (λx. F (γ2 (φ x)) ∙ b * (vector_derivative (γ2 ∘ φ) (at x within {0..1}) ∙ b))"
  proof-
    have "negligible ((φ -` ?s') ∪ ?s)" using finite_neg_img s(1) by auto
    then show ?thesis
      using c integral_spike  by (metis(no_types,lifting))
  qed
  have phi_in_int: "(⋀x. x ∈ {0..1} ⟹ φ x ∈ {0..1})" using phi
    using v by blast
  then have e: "((λx. F (γ2 (φ x)) ∙ b * (vector_derivative (γ2 ∘ φ) (at x within {0..1}) ∙ b)) has_integral
                             integral {φ 0..φ 1} (λx. F (γ2 x) ∙ b * (vector_derivative γ2 (at x within {0..1}) ∙ b))){0..1}"
  proof-
    have "negligible ?s" using s_inter(1) by auto
    have 0: "negligible ((φ -` ?s') ∪ ?s)" using finite_neg_img s(1) by auto
    have c':"∀ x∈ {0..1} - ((φ -` ?s') ∪ ?s). D x * (F (γ2 (φ x)) ∙ b * (vector_derivative γ2 (at (φ x) within {0..1}) ∙ b)) = 
                                    F (γ2 (φ x)) ∙ b * (vector_derivative (γ2 ∘ φ) (at x within {0..1}) ∙ b)"
      using c  by blast
    have has_integral_spike_eq': "⋀s t f g y. negligible s ⟹
                                                       ∀x∈t - s. g x = f x ⟹ (f has_integral y) t = (g has_integral y) t"
      using has_integral_spike_eq by metis
    show ?thesis
      using a has_integral_spike_eq'[OF 0 c']  by blast
  qed
  then have f: "((λx. F (γ1 x) ∙ b * (vector_derivative  γ1 (at x within {0..1}) ∙ b)) has_integral
                     integral {φ 0..φ 1} (λx. F (γ2 x) ∙ b * (vector_derivative γ2 (at x within {0..1}) ∙ b)))
                       {0..1}"
  proof-
    assume ass: "((λx. F (γ2 (φ x)) ∙ b * (vector_derivative (γ2 ∘ φ) (at x within {0..1}) ∙ b)) has_integral
                            integral {φ 0..φ 1} (λx. F (γ2 x) ∙ b * (vector_derivative γ2 (at x within {0..1}) ∙ b)))
                             {0..1}"
    have *:"∀x∈{0..1} - ( ((φ -` ?s') ∪ ?s) ∪ {0,1}). (λx. F (γ2 (φ x)) ∙ b * (vector_derivative  (γ2 ∘ φ) (at x within {0..1}) ∙ b)) x =
                                                  (λx. F (γ1 x) ∙ b * (vector_derivative γ1 (at x within {0..1}) ∙ b)) x"
    proof-
      have "∀x∈{0<..<1}  - (φ -` ?s' ∪ ?s). (vector_derivative  (γ2 ∘ φ) (at x within {0..1}) ∙ b) = (vector_derivative  (γ1) (at x within {0..1}) ∙ b)"
      proof
        have i: "open ({0<..<1}  - ((φ -` ?s') ∪ ?s))" using open_diff s(1) open_greaterThanLessThan finite_neg_img
          by (simp add: open_diff)
        have ii: "∀x∈{0<..<1::real}  - (φ -` ?s' ∪ ?s). (γ2 ∘ φ) x = γ1 x" using phi(1)
          by auto                              
        fix x::real
        assume ass: " x ∈ {0<..<1::real} -  ((φ -` ?s') ∪ ?s)"
        then have iii: "(γ2 ∘ φ has_vector_derivative vector_derivative (γ2 ∘ φ) (at x within {0..1})) (at x)"
            by (metis (no_types) Diff_iff add.commute add_strict_mono ass atLeastAtMost_iff gamma2_vec_deriv_within gamma2_vec_diffable greaterThanLessThan_iff less_irrefl not_le)
            (*Most crucial but annoying step*)
        then have iv:"(γ1 has_vector_derivative vector_derivative (γ2 ∘ φ) (at x within {0..1})) (at x)"
          using has_derivative_transform_within_open i ii ass
          apply(auto simp add: has_vector_derivative_def)
            apply (meson ass has_derivative_transform_within_open i ii)
           apply (meson ass has_derivative_transform_within_open i ii)
          by (meson ass has_derivative_transform_within_open i ii)
        have v: "0 ≤ x" "x ≤ 1" using ass by auto
        have 0: "vector_derivative γ1 (at x within {0..1}) = vector_derivative (γ2 ∘ φ) (at x within {0..1})"
          using vector_derivative_at_within_ivl[OF iv v(1) v(2) zero_less_one]
          by force
        have 1: "vector_derivative (γ2 ∘ φ) (at x within {0..1}) = vector_derivative (γ2 ∘ φ) (at x within {0..1})"
          using vector_derivative_at_within_ivl[OF iii v(1) v(2) zero_less_one]
          by force
        then have "vector_derivative (γ2 ∘ φ) (at x within {0..1}) = vector_derivative γ1 (at x within {0..1})"
          using 0 1 by auto
        then show "vector_derivative (γ2 ∘ φ) (at x within {0..1}) ∙ b = vector_derivative γ1 (at x within {0..1}) ∙ b" by auto
      qed
      then have i: "∀x∈{0..1} - ( ((φ -` ?s') ∪ ?s)∪{0,1}). (vector_derivative  (γ2 ∘ φ) (at x within {0..1}) ∙ b) = (vector_derivative  (γ1) (at x within {0..1}) ∙ b)"
        by auto
      have ii: "∀x∈{0..1} - (((φ -` ?s') ∪ ?s)∪{0,1}).  F (γ1 x) ∙ b =  F (γ2 (φ x)) ∙ b"
        using phi(1)
        by auto
      show ?thesis 
        using i ii  by metis
    qed
    have **: "negligible ((φ -` ?s') ∪ ?s ∪ {0, 1})" using s(1) finite_neg_img by auto
    have has_integral_spike_eq': "⋀s t g f y. negligible s ⟹
                                ∀x∈t - s. g x = f x ⟹ (f has_integral y) t = (g has_integral y) t"
      using has_integral_spike_eq by metis
    show ?thesis
      using has_integral_spike_eq'[OF ** *] ass
      by blast
  qed
  then show "line_integral_exists F {b} γ1"
    using phi  by(auto simp add: line_integral_exists_def)
  have "integral ({0..1}) (λx. F (γ2 (φ x)) ∙ b * (vector_derivative (γ2 ∘ φ) (at x within {0..1}) ∙ b)) =
                      integral ({0..1}) (λx. F (γ1 x) ∙ b * (vector_derivative γ1  (at x within {0..1}) ∙ b))"
    using integral_unique[OF e] integral_unique[OF f]
    by metis
  moreover have "integral ({0..1}) (λx. F (γ2 (φ x)) ∙ b * (vector_derivative (γ2 ∘ φ) (at x within {0..1}) ∙ b)) =
                         integral ({0..1}) (λx. F (γ2 x) ∙ b * (vector_derivative γ2 (at x within {0..1}) ∙ b))"
    using b d phi by (auto simp add:)
  ultimately show "line_integral F {b} γ1 = line_integral F {b} γ2"
    using phi  by(auto simp add: line_integral_def)
qed

lemma reparam_weak_eq_line_integrals:
  assumes "reparam_weak γ1 γ2"
    "γ2 C1_differentiable_on {0..1}" (*To generalise this to valid_path we need a version of has_integral_substitution_strong that allows finite discontinuities of f*)
    "continuous_on (path_image γ2) (λx. F x ∙ b)"
  shows "line_integral F {b} γ1 = line_integral F {b} γ2"
    "line_integral_exists F {b} γ1"
proof-
  obtain φ where phi: "(∀x∈{0..1}. γ1 x = (γ2 o φ) x)"" φ piecewise_C1_differentiable_on {0..1}"" φ(0) = 0"" φ(1) = 1"" φ ` {0..1} = {0..1}"
    using assms(1)
    by (auto simp add: reparam_weak_def)
  obtain s where s: "finite s" "φ C1_differentiable_on {0..1} - s"
    using phi
    by(auto simp add: reparam_weak_def piecewise_C1_differentiable_on_def)
  have cont_phi: "continuous_on {0..1} φ"
    using phi
    by(auto simp add: reparam_weak_def piecewise_C1_differentiable_on_imp_continuous_on)
  have gamma2_differentiable: "(∀x ∈ {0 .. 1}. γ2 differentiable at x)"
    using assms(2) 
    by (auto simp add: valid_path_def C1_differentiable_on_eq)
  then have gamma2_b_component_differentiable: "(∀x ∈ {0 .. 1}. (λx. (γ2 x) ∙ b) differentiable at x)"
    by auto
  then have "(λx. (γ2 x) ∙ b) differentiable_on {0..1}"
    using differentiable_at_withinI
    by (auto simp add: differentiable_on_def)
  then have gama2_cont_comp: "continuous_on {0..1} (λx. (γ2 x) ∙ b)"
    using differentiable_imp_continuous_on
    by auto
  have gamma2_cont:"continuous_on {0..1} γ2"
    using assms(2) C1_differentiable_imp_continuous_on
    by (auto simp add: valid_path_def)
  have iii: "continuous_on {0..1} (λx. F (γ2 x) ∙ b * (vector_derivative γ2 (at x within {0..1}) ∙ b))"
  proof-
    have 0: "continuous_on {0..1} (λx. F (γ2 x) ∙ b)"
      using assms(3) continuous_on_compose[OF gamma2_cont]
      by (auto simp add: path_image_def) 
    obtain D where D: "(∀x∈{0..1}. (γ2 has_vector_derivative D x) (at x)) ∧ continuous_on {0..1} D"
      using assms(2)  by (auto simp add: C1_differentiable_on_def)
    then have *:"∀x∈{0..1}. vector_derivative γ2 (at x within{0..1}) = D x"
      using vector_derivative_at vector_derivative_at_within_ivl
      by fastforce
    then have "continuous_on {0..1} (λx. vector_derivative γ2 (at x within{0..1}))"
      using continuous_on_eq D  by force
    then have 1: "continuous_on {0..1} (λx. (vector_derivative γ2 (at x within{0..1})) ∙ b)"
      by (auto intro!: continuous_intros)
    show ?thesis
      using continuous_on_mult[OF 0 1]  by auto
  qed
  have iv: "φ(0) ≤ φ(1)"
    using phi(3) phi(4)  by (simp add: reparam_weak_def)
  have v: "φ`{0..1} ⊆ {0..1}"
    using phi(5)  by (simp add: reparam_weak_def)
  obtain D where D_props: "(∀x∈{0..1} - s. (φ has_vector_derivative D x) (at x))"
    using s
    by (auto simp add: C1_differentiable_on_def)
  then have "(⋀x. x ∈ ({0..1} -s) ⟹ (φ has_vector_derivative D x) (at x within {0..1}))"
    using has_vector_derivative_at_within  by blast
  then have vi: "(⋀x. x ∈ ({0..1} - s) ⟹ (φ has_real_derivative D x) (at x within {0..1}))"
    using has_real_derivative_iff_has_vector_derivative
    by blast
  have a:"((λx. D x * (F (γ2 (φ x)) ∙ b * (vector_derivative γ2 (at (φ x) within {0..1}) ∙ b))) has_integral
              integral {φ 0..φ 1} (λx. F (γ2 x) ∙ b * (vector_derivative γ2 (at x within {0..1}) ∙ b)))
              {0..1}"
    using has_integral_substitution_strong[OF s(1) zero_le_one iv v iii cont_phi vi]
    by simp
  then have b: "integral {0..1} (λx. D x * (F (γ2 (φ x)) ∙ b * (vector_derivative γ2 (at (φ x) within {0..1}) ∙ b))) = 
                       integral {φ 0..φ 1} (λx. F (γ2 x) ∙ b * (vector_derivative γ2 (at x within {0..1}) ∙ b))"
    by auto
  have gamma2_vec_diffable: "⋀x::real. x ∈ {0..1} -s ⟹ ((γ2 o φ) has_vector_derivative vector_derivative (γ2 ∘ φ) (at x)) (at x)"
  proof-
    fix x::real 
    assume ass: "x ∈ {0..1} -s"
    have zer_le_x_le_1:"0≤ x ∧ x ≤ 1" using ass by auto
    show "((γ2 o φ) has_vector_derivative vector_derivative (γ2 ∘ φ) (at x)) (at x)"
    proof-
      have **: "γ2 differentiable at (φ x)"
        using phi gamma2_differentiable
        by (auto simp add: zer_le_x_le_1)
      have ***: " φ differentiable at x"
        using s ass
        by (auto simp add: C1_differentiable_on_eq)
      then show "((γ2 o φ) has_vector_derivative vector_derivative (γ2 ∘ φ) (at x)) (at x)"
        using differentiable_chain_at[OF *** **] 
        by (auto simp add: vector_derivative_works)
    qed
  qed
  then have gamma2_vec_deriv_within: "⋀x::real. x ∈ {0..1} -s ⟹ vector_derivative (γ2 ∘ φ) (at x) = vector_derivative (γ2 ∘ φ) (at x within {0..1})"
    using vector_derivative_at_within_ivl[OF gamma2_vec_diffable]
    by auto
  have "∀x∈{0..1} - s. D x * (vector_derivative γ2 (at (φ x) within {0..1}) ∙ b) = (vector_derivative (γ2 ∘ φ) (at x within {0..1}) ∙ b)"
  proof
    fix x::real
    assume ass: "x ∈ {0..1} -s"
    then have 0: "φ differentiable (at x)"
      using s
      by (auto simp add: C1_differentiable_on_def differentiable_def has_vector_derivative_def)
    obtain D2 where "(φ has_vector_derivative D2) (at x)"
      using D_props ass
      by blast
    have "φ x ∈ {0..1}"
      using phi(5) ass 
      by (auto simp add: reparam_weak_def)
    then have 1: "γ2 differentiable (at (φ x))"
      using gamma2_differentiable
      by auto
    have 3:" vector_derivative γ2 (at (φ x)) =  vector_derivative γ2 (at (φ x) within {0..1})"
    proof-
      have *:"0≤ φ x ∧ φ x ≤ 1" using phi(5) ass by auto
      then have **:"(γ2 has_vector_derivative (vector_derivative γ2 (at (φ x)))) (at (φ x))"
        using 1 vector_derivative_works
        by auto
      show ?thesis
        using * vector_derivative_at_within_ivl[OF **]
        by auto
    qed
    show "D x * (vector_derivative γ2 (at (φ x) within {0..1}) ∙ b) = vector_derivative (γ2 ∘ φ) (at x within {0..1}) ∙ b"
      using vector_derivative_chain_at[OF 0 1]
      apply (auto simp add: gamma2_vec_deriv_within[OF ass, symmetric] 3[symmetric])
      using D_props ass vector_derivative_at
      by fastforce
  qed
  then have c:"⋀x.  x∈({0..1} -s) ⟹ D x * (F (γ2 (φ x)) ∙ b * (vector_derivative γ2 (at (φ x) within {0..1}) ∙ b)) = 
                                    F (γ2 (φ x)) ∙ b * (vector_derivative (γ2 ∘ φ) (at x within {0..1}) ∙ b)"
    by auto
  then have d: "integral ({0..1}) (λx. D x * (F (γ2 (φ x)) ∙ b * (vector_derivative γ2 (at (φ x) within {0..1}) ∙ b))) = 
                                            integral ({0..1}) (λx. F (γ2 (φ x)) ∙ b * (vector_derivative (γ2 ∘ φ) (at x within {0..1}) ∙ b))"
  proof-
    have "negligible s" using s(1) by auto
    then show ?thesis
      using c integral_spike  by (metis(no_types,lifting))
  qed
  have phi_in_int: "(⋀x. x ∈ {0..1} ⟹ φ x ∈ {0..1})" using phi
    by(auto simp add:)
  then have e: "((λx. F (γ2 (φ x)) ∙ b * (vector_derivative (γ2 ∘ φ) (at x within {0..1}) ∙ b)) has_integral
                             integral {φ 0..φ 1} (λx. F (γ2 x) ∙ b * (vector_derivative γ2 (at x within {0..1}) ∙ b))){0..1}"
  proof-
    have 0:"negligible s" using s(1) by auto
    have c':"∀ x∈ {0..1} -s. D x * (F (γ2 (φ x)) ∙ b * (vector_derivative γ2 (at (φ x) within {0..1}) ∙ b)) = 
                                    F (γ2 (φ x)) ∙ b * (vector_derivative (γ2 ∘ φ) (at x within {0..1}) ∙ b)"
      using c by auto
    have has_integral_spike_eq': "⋀s t f g y. negligible s ⟹
                                               ∀x∈t - s. g x = f x ⟹ (f has_integral y) t = (g has_integral y) t"
      using has_integral_spike_eq by metis
    show ?thesis
      using a has_integral_spike_eq'[OF 0 c']  by blast
  qed
  then have f: "((λx. F (γ1 x) ∙ b * (vector_derivative  γ1 (at x within {0..1}) ∙ b)) has_integral
                     integral {φ 0..φ 1} (λx. F (γ2 x) ∙ b * (vector_derivative γ2 (at x within {0..1}) ∙ b)))
                       {0..1}"
  proof-
    assume ass: "((λx. F (γ2 (φ x)) ∙ b * (vector_derivative (γ2 ∘ φ) (at x within {0..1}) ∙ b)) has_integral
                            integral {φ 0..φ 1} (λx. F (γ2 x) ∙ b * (vector_derivative γ2 (at x within {0..1}) ∙ b)))
                             {0..1}"
    have *:"∀x∈{0..1} - (s∪{0,1}). (λx. F (γ2 (φ x)) ∙ b * (vector_derivative  (γ2 ∘ φ) (at x within {0..1}) ∙ b)) x =
                                                  (λx. F (γ1 x) ∙ b * (vector_derivative γ1 (at x within {0..1}) ∙ b)) x"
    proof-
      have "∀x∈{0<..<1} - s. (vector_derivative  (γ2 ∘ φ) (at x within {0..1}) ∙ b) = (vector_derivative  (γ1) (at x within {0..1}) ∙ b)"
      proof
        have i: "open ({0<..<1} - s)" using open_diff s open_greaterThanLessThan by blast
        have ii: "∀x∈{0<..<1::real} - s. (γ2 ∘ φ) x = γ1 x" using phi(1)
          by auto                              
        fix x::real
        assume ass: " x ∈ {0<..<1::real} - s"
        then have iii: "(γ2 ∘ φ has_vector_derivative vector_derivative (γ2 ∘ φ) (at x within {0..1})) (at x)"
          using has_vector_derivative_at_within gamma2_vec_deriv_within gamma2_vec_diffable
          by auto
            (*Most crucial but annoying step*)
        then have iv:"(γ1 has_vector_derivative vector_derivative (γ2 ∘ φ) (at x within {0..1})) (at x)"
          using has_derivative_transform_within_open i ii ass
          apply(auto simp add: has_vector_derivative_def)
          by force
        have v: "0 ≤ x" "x ≤ 1" using ass by auto
        have 0: "vector_derivative γ1 (at x within {0..1}) = vector_derivative (γ2 ∘ φ) (at x within {0..1})"
          using vector_derivative_at_within_ivl[OF iv v(1) v(2) zero_less_one]
          by force
        have 1: "vector_derivative (γ2 ∘ φ) (at x within {0..1}) = vector_derivative (γ2 ∘ φ) (at x within {0..1})"
          using vector_derivative_at_within_ivl[OF iii v(1) v(2) zero_less_one]
          by force
        then have "vector_derivative (γ2 ∘ φ) (at x within {0..1}) = vector_derivative γ1 (at x within {0..1})"
          using 0 1 by auto
        then show "vector_derivative (γ2 ∘ φ) (at x within {0..1}) ∙ b = vector_derivative γ1 (at x within {0..1}) ∙ b" by auto
      qed
      then have i: "∀x∈{0..1} - (s∪{0,1}). (vector_derivative  (γ2 ∘ φ) (at x within {0..1}) ∙ b) = (vector_derivative  (γ1) (at x within {0..1}) ∙ b)"
        by auto
      have ii: "∀x∈{0..1} - (s∪{0,1}).  F (γ1 x) ∙ b =  F (γ2 (φ x)) ∙ b"
        using phi(1)  by auto
      show ?thesis 
        using i ii by auto
    qed
    have **: "negligible (s∪{0,1})" using s(1) by auto
    have has_integral_spike_eq': "⋀s t g f y. negligible s ⟹
                                ∀x∈t - s. g x = f x ⟹ (f has_integral y) t = (g has_integral y) t"
      using has_integral_spike_eq by metis
    show ?thesis
      using has_integral_spike_eq'[OF ** *] ass
      by blast
  qed
  then show "line_integral_exists F {b} γ1"
    using phi  by(auto simp add: line_integral_exists_def)
  have "integral ({0..1}) (λx. F (γ2 (φ x)) ∙ b * (vector_derivative (γ2 ∘ φ) (at x within {0..1}) ∙ b)) =
                      integral ({0..1}) (λx. F (γ1 x) ∙ b * (vector_derivative γ1  (at x within {0..1}) ∙ b))"
    using integral_unique[OF e] integral_unique[OF f]
    by metis
  moreover have "integral ({0..1}) (λx. F (γ2 (φ x)) ∙ b * (vector_derivative (γ2 ∘ φ) (at x within {0..1}) ∙ b)) =
                         integral ({0..1}) (λx. F (γ2 x) ∙ b * (vector_derivative γ2 (at x within {0..1}) ∙ b))"
    using b d phi  by (auto simp add:)
  ultimately show "line_integral F {b} γ1 = line_integral F {b} γ2"
    using phi by(auto simp add: line_integral_def)
qed

lemma line_integral_sum_basis:
  assumes "finite (basis::('a::euclidean_space) set)"  "∀b∈basis. line_integral_exists F {b} γ"
  shows "line_integral F basis γ = (∑b∈basis. line_integral F {b} γ)"
        "line_integral_exists F basis γ"
  using assms
proof(induction basis)
  show "line_integral F {} γ = (∑b∈{}. line_integral F {b} γ)"
    by(auto simp add: line_integral_def)
  show "∀b∈{}. line_integral_exists F {b} γ ⟹ line_integral_exists F {} γ"
    by(simp add: line_integral_exists_def integrable_0)
next
  fix basis::"('a::euclidean_space) set"
  fix x::"'a::euclidean_space"
  fix  γ
  assume ind_hyp: "(∀b∈basis. line_integral_exists F {b} γ ⟹ line_integral_exists F basis γ)"
    "(∀b∈basis. line_integral_exists F {b} γ ⟹ line_integral F basis γ = (∑b∈basis. line_integral F {b} γ))"
  assume step: "finite basis"
    "x ∉ basis"
    "∀b∈insert x basis. line_integral_exists F {b} γ"
  then have 0: "line_integral_exists F {x} γ" by auto
  have 1:"line_integral_exists F basis γ"
    using ind_hyp step by auto
  then show "line_integral_exists F (insert x basis) γ"
    using step(1) step(2) line_integral_sum_gen(2)[OF _ 0 1] by simp
  have 3: "finite (insert x basis)" using step(1) by auto
  have "line_integral F basis γ = (∑b∈basis. line_integral F {b} γ)"
    using ind_hyp step by auto
  then show "line_integral F (insert x basis) γ = (∑b∈insert x basis. line_integral F {b} γ)"
    using step(1) step(2) line_integral_sum_gen(1)[OF 3 0 1]
    by force
qed

lemma reparam_weak_eq_line_integrals_basis:
  assumes "reparam_weak γ1 γ2"
    "γ2 C1_differentiable_on {0..1}" (*To generalise this to valid_path we need a version of has_integral_substitution_strong that allows finite discontinuities*)
    "∀b∈basis. continuous_on (path_image γ2) (λx. F x ∙ b)"
    "finite basis"
  shows "line_integral F basis γ1 = line_integral F basis γ2"
    "line_integral_exists F basis γ1"
proof- 
  show "line_integral_exists F basis γ1"
    using reparam_weak_eq_line_integrals(2)[OF assms(1) assms(2)] assms(3-4) line_integral_sum_basis(2)[OF assms(4)]
    by(simp add: subset_iff)
  show "line_integral F basis γ1 = line_integral F basis γ2"
    using reparam_weak_eq_line_integrals[OF assms(1) assms(2)] assms(3-4) line_integral_sum_basis(1)[OF assms(4)]
      line_integral_exists_smooth_one_base[OF assms(2)]
    by(simp add: subset_iff)
qed

lemma reparam_eq_line_integrals_basis:
  assumes "reparam γ1 γ2"
    "γ2 piecewise_C1_differentiable_on {0..1}" 
    "∀b∈basis. continuous_on (path_image γ2) (λx. F x ∙ b)"
    "finite basis"
    "∀b∈basis. line_integral_exists F {b} γ2" (*We need to remove this and work on special cases like conservative fields and field/line combinations that satisfy the improper integrals theorem assumptions*)
  shows "line_integral F basis γ1 = line_integral F basis γ2"
    "line_integral_exists F basis γ1"
proof- 
  show "line_integral_exists F basis γ1"
    using reparam_eq_line_integrals(2)[OF assms(1) assms(2)] assms(3-5) line_integral_sum_basis(2)[OF assms(4)]
    by(simp add: subset_iff)
  show "line_integral F basis γ1 = line_integral F basis γ2"
    using reparam_eq_line_integrals[OF assms(1) assms(2)] assms(3-5) line_integral_sum_basis(1)[OF assms(4)]
    by(simp add: subset_iff)
qed

lemma line_integral_exists_smooth:
  assumes "γ C1_differentiable_on {0..1}" (*To generalise this to valid_path we need a version of has_integral_substitution_strong that allows finite discontinuities*)
    "∀(b::'a::euclidean_space) ∈basis. continuous_on (path_image γ) (λx. F x ∙ b)"
    "finite basis"
  shows "line_integral_exists F basis γ"
  using reparam_weak_eq_line_integrals_basis(2)[OF reparam_weak_eq_refl[where ?γ1.0 = γ]] assms
  by fastforce

lemma smooth_path_imp_reverse:
  assumes "g C1_differentiable_on {0..1}"
  shows "(reversepath g) C1_differentiable_on {0..1}"
  using assms continuous_on_const
  apply (auto simp: reversepath_def)
  apply (rule C1_differentiable_compose [of "λx::real. 1-x" _ g, unfolded o_def])
    apply (auto simp: C1_differentiable_on_eq)
  apply (simp add: finite_vimageI inj_on_def)
  done

lemma piecewise_smooth_path_imp_reverse:
  assumes "g piecewise_C1_differentiable_on {0..1}"
  shows "(reversepath g) piecewise_C1_differentiable_on {0..1}"
  using assms valid_path_reversepath
  using valid_path_def by blast

definition chain_reparam_weak_chain where
  "chain_reparam_weak_chain one_chain1 one_chain2 ≡
      ∃f. bij f ∧ f ` one_chain1 = one_chain2 ∧ (∀(k,γ)∈one_chain1. if k = fst (f(k,γ)) then reparam_weak γ (snd (f(k,γ))) else reparam_weak γ (reversepath (snd (f(k,γ)))))"

lemma chain_reparam_weak_chain_line_integral:
  assumes "chain_reparam_weak_chain one_chain1 one_chain2"
    "∀(k2,γ2)∈one_chain2. γ2 C1_differentiable_on {0..1}"
    "∀(k2,γ2)∈one_chain2.∀b∈basis. continuous_on (path_image γ2) (λx. F x ∙ b)"
    "finite basis"                                                                     
  and bound1: "boundary_chain one_chain1"
  and bound2: "boundary_chain one_chain2"
  shows "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2"
    "∀(k, γ)∈one_chain1. line_integral_exists F basis γ"
proof-
  obtain f where f: "bij f"
    "(∀(k,γ)∈one_chain1. if k = fst (f(k,γ)) then reparam_weak γ (snd (f(k,γ))) else reparam_weak γ (reversepath (snd (f(k,γ)))))"
    "f ` one_chain1 = one_chain2"
    using assms(1)
    by (auto simp add: chain_reparam_weak_chain_def)
  have 0:" ∀x∈one_chain1. (case x of (k, γ) ⇒ (real_of_int k * line_integral F basis γ) = (case f x of (k, γ) ⇒ real_of_int k * line_integral F basis γ) ∧
                                                        line_integral_exists F basis γ)"
  proof
    {fix k1 γ1
      assume ass1: "(k1,γ1) ∈one_chain1"
      have "real_of_int k1 * line_integral F basis γ1 = (case (f (k1,γ1)) of (k2, γ2) ⇒ real_of_int k2 * line_integral F basis γ2) ∧
                      line_integral_exists F basis γ1"
      proof(cases)
        assume ass2: "k1 = 1"
        let ?k2 = "fst (f (k1, γ1))"
        let ?γ2 = "snd (f (k1, γ1))"
        have "real_of_int k1 * line_integral F basis γ1 = real_of_int ?k2 * line_integral F basis ?γ2∧
                              line_integral_exists F basis γ1"
        proof(cases)
          assume ass3: "?k2 = 1"
          then have 0: "reparam_weak γ1 ?γ2"
            using ass1 ass2 f(2)
            by auto
          have 1: "?γ2 C1_differentiable_on {0..1}"
            using f(3) assms(2) ass1
            by force
          have 2: "∀b∈basis. continuous_on (path_image ?γ2) (λx. F x ∙ b)"
            using f(3) assms(3) ass1
            by force
          show "real_of_int k1 * line_integral F basis γ1 = real_of_int ?k2 * line_integral F basis ?γ2 ∧
                                     line_integral_exists F basis γ1"
            using assms reparam_weak_eq_line_integrals_basis[OF 0 1 2 assms(4)]
              ass2 ass3
            by auto
        next
          assume "?k2 ≠ 1"
          then have ass3: "?k2 = -1"
            using bound2 ass1 f(3) unfolding boundary_chain_def by force
          then have 0: "reparam_weak γ1 (reversepath ?γ2)"
            using ass1 ass2 f(2)
            by auto
          have 1: "(reversepath ?γ2) C1_differentiable_on {0..1}"
            using f(3) assms(2) ass1 smooth_path_imp_reverse
            by force
          have 2: "∀b∈basis. continuous_on (path_image (reversepath ?γ2)) (λx. F x ∙ b)"
            using f(3) assms(3) ass1 path_image_reversepath
            by force
          have 3: "line_integral F basis ?γ2 = - line_integral F basis (reversepath ?γ2)"
          proof-
            have i:"valid_path (reversepath ?γ2) "
              using 1 C1_differentiable_imp_piecewise
              by (auto simp add: valid_path_def)
            show ?thesis 
              using line_integral_on_reverse_path(1)[OF i line_integral_exists_smooth[OF 1 2 ]] assms
              by auto
          qed
          show "real_of_int k1 * line_integral F basis γ1 = real_of_int ?k2 * line_integral F basis ?γ2 ∧
                                     line_integral_exists F basis γ1"
            using assms reparam_weak_eq_line_integrals_basis[OF 0 1 2 assms(4)]
              ass2 ass3 3
            by auto
        qed
        then show "real_of_int k1 * line_integral F basis γ1 = (case f (k1, γ1) of (k2, γ2) ⇒ real_of_int k2 * line_integral F basis γ2) ∧
                                   line_integral_exists F basis γ1"
          by (simp add: case_prod_beta')
      next
        assume "k1 ≠ 1"
        then have ass2: "k1 = -1"
          using bound1 ass1 f(3) unfolding boundary_chain_def by force
        let ?k2 = "fst (f (k1, γ1))"
        let ?γ2 = "snd (f (k1, γ1))"
        have "real_of_int k1 * line_integral F basis γ1 = real_of_int ?k2 * line_integral F basis ?γ2 ∧
                              line_integral_exists F basis γ1"
        proof(cases)
          assume ass3: "?k2 = 1"
          then have 0: "reparam_weak γ1 (reversepath ?γ2)"
            using ass1 ass2 f(2)
            by auto
          have 1: "(reversepath ?γ2) C1_differentiable_on {0..1}"
            using f(3) assms(2) ass1 smooth_path_imp_reverse
            by force
          have 2: "∀b∈basis. continuous_on (path_image (reversepath ?γ2)) (λx. F x ∙ b)"
            using f(3) assms(3) ass1 path_image_reversepath
            by force
          have 3: "line_integral F basis ?γ2 = - line_integral F basis (reversepath ?γ2)"
          proof-
            have i:"valid_path (reversepath ?γ2) "
              using 1 C1_differentiable_imp_piecewise
              by (auto simp add: valid_path_def)
            show ?thesis 
              using line_integral_on_reverse_path(1)[OF i line_integral_exists_smooth[OF 1 2 assms(4)]]
              by auto
          qed
          show "real_of_int k1 * line_integral F basis γ1 = real_of_int ?k2 * line_integral F basis ?γ2 ∧
                                     line_integral_exists F basis γ1"
            using assms reparam_weak_eq_line_integrals_basis[OF 0 1 2 assms(4)]
              ass2 ass3 3
            by auto
        next
          assume "?k2 ≠ 1"
          then have ass3: "?k2 = -1"
            using bound2 ass1 f(3) unfolding boundary_chain_def by force
          then have 0: "reparam_weak γ1 ?γ2"
            using ass1 ass2 f(2)  by auto
          have 1: "?γ2 C1_differentiable_on {0..1}"
            using f(3) assms(2) ass1  by force
          have 2: "∀b∈basis. continuous_on (path_image ?γ2) (λx. F x ∙ b)"
            using f(3) assms(3) ass1  by force
          show "real_of_int k1 * line_integral F basis γ1 = real_of_int ?k2 * line_integral F basis ?γ2 ∧
                                     line_integral_exists F basis γ1"
            using assms reparam_weak_eq_line_integrals_basis[OF 0 1 2 assms(4)]  ass2 ass3
            by auto
        qed
        then show "real_of_int k1 * line_integral F basis γ1 = (case f (k1, γ1) of (k2, γ2) ⇒ real_of_int k2 * line_integral F basis γ2) ∧
                                   line_integral_exists F basis γ1"
          by (simp add: case_prod_beta')
      qed
    }
    then show "⋀x. x ∈ one_chain1 ⟹
                                (case x of (k, γ) ⇒ (real_of_int k * line_integral F basis γ) = (case f x of (k, γ) ⇒ real_of_int k * line_integral F basis γ) ∧
                                                        line_integral_exists F basis γ)"
      by (auto simp add: case_prod_beta')
  qed
  show "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2"
    using 0 by(simp add: one_chain_line_integral_def sum_bij[OF f(1) _ f(3)] split_beta)
  show "∀(k, γ)∈one_chain1. line_integral_exists F basis γ"
    using 0 by blast
qed

definition chain_reparam_chain where
  "chain_reparam_chain one_chain1 one_chain2 ≡
      ∃f. bij f ∧ f ` one_chain1 = one_chain2 ∧ (∀(k,γ)∈one_chain1. if k = fst (f(k,γ)) then reparam γ (snd (f(k,γ))) else reparam γ (reversepath (snd (f(k,γ)))))"

definition chain_reparam_weak_path::"((real) ⇒ (real * real)) ⇒ ((int * ((real) ⇒ (real * real))) set) ⇒ bool" where
  "chain_reparam_weak_path γ one_chain
           ≡ ∃l. set l = one_chain ∧ distinct l ∧ reparam γ (rec_join l) ∧ valid_chain_list l ∧ l ≠ []"

lemma chain_reparam_chain_line_integral:
  assumes "chain_reparam_chain one_chain1 one_chain2"
    "∀(k2,γ2)∈one_chain2. γ2 piecewise_C1_differentiable_on {0..1}"
    "∀(k2,γ2)∈one_chain2.∀b∈basis. continuous_on (path_image γ2) (λx. F x ∙ b)"
    "finite basis"                                                                     
  and bound1: "boundary_chain one_chain1"
  and bound2: "boundary_chain one_chain2"
  and line: "∀(k2,γ2)∈one_chain2. (∀b∈basis. line_integral_exists F {b} γ2)"
  shows "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2"
    "∀(k, γ)∈one_chain1. line_integral_exists F basis γ"
proof-
  obtain f where f: "bij f"
    "(∀(k,γ)∈one_chain1. if k = fst (f(k,γ)) then reparam γ (snd (f(k,γ))) else reparam γ (reversepath (snd (f(k,γ)))))"
    "f ` one_chain1 = one_chain2"
    using assms(1)
    by (auto simp add: chain_reparam_chain_def)
  have integ_exist_b: "∀(k1,γ1)∈one_chain1. ∀b∈basis. line_integral_exists F {b} (snd (f (k1, γ1)))"
    using line f by fastforce
  have valid_cubes: "∀(k1,γ1)∈one_chain1. valid_path (snd (f (k1, γ1)))"
    using assms(2) f(3) valid_path_def by fastforce
  have integ_rev_exist_b: "∀(k1,γ1)∈one_chain1. ∀b∈basis. line_integral_exists F {b} (reversepath (snd (f (k1, γ1))))"
    using line_integral_on_reverse_path(2) integ_exist_b valid_cubes
    by blast                             
  have 0:" ∀x∈one_chain1. (case x of (k, γ) ⇒ (real_of_int k * line_integral F basis γ) = (case f x of (k, γ) ⇒ real_of_int k * line_integral F basis γ) ∧
                                                        line_integral_exists F basis γ)"
  proof
    {fix k1 γ1
      assume ass1: "(k1,γ1) ∈one_chain1"
      have "real_of_int k1 * line_integral F basis γ1 = (case (f (k1,γ1)) of (k2, γ2) ⇒ real_of_int k2 * line_integral F basis γ2) ∧
                      line_integral_exists F basis γ1"
      proof(cases)
        assume ass2: "k1 = 1"
        let ?k2 = "fst (f (k1, γ1))"
        let ?γ2 = "snd (f (k1, γ1))"
        have "real_of_int k1 * line_integral F basis γ1 = real_of_int ?k2 * line_integral F basis ?γ2∧
                              line_integral_exists F basis γ1"
        proof(cases)
          assume ass3: "?k2 = 1"
          then have 0: "reparam γ1 ?γ2"
            using ass1 ass2 f(2)
            by auto
          have 1: "?γ2 piecewise_C1_differentiable_on {0..1}"
            using f(3) assms(2) ass1
            by force
          have 2: "∀b∈basis. continuous_on (path_image ?γ2) (λx. F x ∙ b)"
            using f(3) assms(3) ass1
            by force
          show "real_of_int k1 * line_integral F basis γ1 = real_of_int ?k2 * line_integral F basis ?γ2 ∧
                                     line_integral_exists F basis γ1"
            using assms reparam_eq_line_integrals_basis[OF 0 1 2 assms(4)] integ_exist_b
              ass1 ass2 ass3
            by auto
        next
          assume "?k2 ≠ 1"
          then have ass3: "?k2 = -1"
            using bound2 ass1 f(3) unfolding boundary_chain_def by force
          then have 0: "reparam γ1 (reversepath ?γ2)"
            using ass1 ass2 f(2)
            by auto
          have 1: "(reversepath ?γ2) piecewise_C1_differentiable_on {0..1}"
            using f(3) assms(2) ass1 piecewise_smooth_path_imp_reverse
            by force
          have 2: "∀b∈basis. continuous_on (path_image (reversepath ?γ2)) (λx. F x ∙ b)"
            using f(3) assms(3) ass1 path_image_reversepath
            by force
          have 3: "line_integral F basis ?γ2 = - line_integral F basis (reversepath ?γ2)"
          proof-
            have i:"valid_path (reversepath ?γ2) "
              using 1 C1_differentiable_imp_piecewise
              by (auto simp add: valid_path_def)
            have ii: "line_integral_exists F basis (snd (f (k1, γ1)))"
              using assms(4) line_integral_sum_basis(2) integ_exist_b ass1
              by fastforce
            show ?thesis                                            
              using i ii line_integral_on_reverse_path(1) valid_path_reversepath by blast
          qed
          show "real_of_int k1 * line_integral F basis γ1 = real_of_int ?k2 * line_integral F basis ?γ2 ∧
                                     line_integral_exists F basis γ1"
            using assms reparam_eq_line_integrals_basis[OF 0 1 2 assms(4)] integ_rev_exist_b
              ass1 ass2 ass3 3 
            by auto
        qed
        then show "real_of_int k1 * line_integral F basis γ1 = (case f (k1, γ1) of (k2, γ2) ⇒ real_of_int k2 * line_integral F basis γ2) ∧
                                   line_integral_exists F basis γ1"
          by (simp add: case_prod_beta')
      next
        assume "k1 ≠ 1"
        then have ass2: "k1 = -1"
          using bound1 ass1 f(3) unfolding boundary_chain_def by force
        let ?k2 = "fst (f (k1, γ1))"
        let ?γ2 = "snd (f (k1, γ1))"
        have "real_of_int k1 * line_integral F basis γ1 = real_of_int ?k2 * line_integral F basis ?γ2 ∧
                              line_integral_exists F basis γ1"
        proof(cases)
          assume ass3: "?k2 = 1"
          then have 0: "reparam γ1 (reversepath ?γ2)"
            using ass1 ass2 f(2)
            by auto
          have 1: "(reversepath ?γ2) piecewise_C1_differentiable_on {0..1}"
            using f(3) assms(2) ass1 piecewise_smooth_path_imp_reverse
            by force
          have 2: "∀b∈basis. continuous_on (path_image (reversepath ?γ2)) (λx. F x ∙ b)"
            using f(3) assms(3) ass1 path_image_reversepath
            by force
          have 3: "line_integral F basis ?γ2 = - line_integral F basis (reversepath ?γ2)"
          proof-
            have i:"valid_path (reversepath ?γ2) "
              using 1 C1_differentiable_imp_piecewise
              by (auto simp add: valid_path_def)
            show ?thesis 
              using line_integral_on_reverse_path(1)[OF i] integ_rev_exist_b
              using ass1 assms(4) line_integral_sum_basis(2) by fastforce
          qed
          show "real_of_int k1 * line_integral F basis γ1 = real_of_int ?k2 * line_integral F basis ?γ2 ∧
                                     line_integral_exists F basis γ1"
            using assms reparam_eq_line_integrals_basis[OF 0 1 2 assms(4)]
              ass2 ass3 3
            using ass1 integ_rev_exist_b by auto
        next
          assume "?k2 ≠ 1"
          then have ass3: "?k2 = -1"
            using bound2 ass1 f(3) unfolding boundary_chain_def by force
          then have 0: "reparam γ1 ?γ2"
            using ass1 ass2 f(2) by auto
          have 1: "?γ2 piecewise_C1_differentiable_on {0..1}"
            using f(3) assms(2) ass1
            by force
          have 2: "∀b∈basis. continuous_on (path_image ?γ2) (λx. F x ∙ b)"
            using f(3) assms(3) ass1
            by force
          show "real_of_int k1 * line_integral F basis γ1 = real_of_int ?k2 * line_integral F basis ?γ2 ∧
                                     line_integral_exists F basis γ1"
            using assms reparam_eq_line_integrals_basis[OF 0 1 2 assms(4)]
              ass2 ass3
            using ass1 integ_exist_b by auto
        qed
        then show "real_of_int k1 * line_integral F basis γ1 = (case f (k1, γ1) of (k2, γ2) ⇒ real_of_int k2 * line_integral F basis γ2) ∧
                                   line_integral_exists F basis γ1"
          by (simp add: case_prod_beta')
      qed
    }
    then show "⋀x. x ∈ one_chain1 ⟹
                                (case x of (k, γ) ⇒ (real_of_int k * line_integral F basis γ) = (case f x of (k, γ) ⇒ real_of_int k * line_integral F basis γ) ∧
                                                        line_integral_exists F basis γ)"
      by (auto simp add: case_prod_beta')
  qed
  show "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2"
    using 0 by (simp add: one_chain_line_integral_def sum_bij[OF f(1) _ f(3)] prod.case_eq_if)
  show "∀(k, γ)∈one_chain1. line_integral_exists F basis γ"
    using 0 by blast
qed

lemma path_image_rec_join:
  fixes γ::"real ⇒ (real × real)"
  fixes k::int
  fixes l
  shows "⋀k γ. (k, γ) ∈ set l ⟹ valid_chain_list l ⟹ path_image γ ⊆ path_image (rec_join l)"
proof(induction l)
  case Nil
  then show ?case by auto
next
  case ass: (Cons a l)
  obtain k' γ' where a: "a = (k',γ')" by force
  have "path_image γ ⊆ path_image (rec_join ((k',γ') # l))"
  proof(cases)
    assume "l=[]"
    then show "path_image γ ⊆ path_image (rec_join ((k',γ') # l))"
      using ass(2-3) a
      by(auto simp add:)
  next
    assume "l≠[]"
    then obtain b l' where b_l: "l = b # l'"
      by (meson rec_join.elims)
    obtain k'' γ'' where b: "b = (k'',γ'')" by force
    show ?thesis
      using ass path_image_reversepath b_l path_image_join
      by(fastforce simp add: a)
  qed
  then show ?case
    using a  by auto
qed

lemma path_image_rec_join_2:
  fixes l
  shows "l ≠ [] ⟹ valid_chain_list l ⟹ path_image (rec_join l) ⊆ (⋃(k, γ) ∈ set l. path_image γ)"
proof(induction l)
  case Nil
  then show ?case by auto
next
  case ass: (Cons a l)
  obtain k' γ' where a: "a = (k',γ')" by force
  have "path_image (rec_join (a # l)) ⊆ (⋃(k, y)∈set (a # l). path_image y)"
  proof(cases)
    assume "l=[]"
    then show "path_image (rec_join (a # l)) ⊆ (⋃(k, y)∈set (a # l). path_image y)"
      using step a  by(auto simp add:)
  next
    assume "l≠[]"
    then obtain b l' where b_l: "l = b # l'"
      by (meson rec_join.elims)
    obtain k'' γ'' where b: "b = (k'',γ'')" by force
    show ?thesis
      using ass
        path_image_reversepath b_l path_image_join
      apply(auto simp add: a) (*Excuse the ugliness of the next script*)
       apply blast
      by fastforce
  qed
  then show ?case
    using a by auto
qed

lemma continuous_on_closed_UN:
  assumes "finite S"
  shows "((⋀s. s ∈ S ⟹ closed s) ⟹ (⋀s. s ∈ S ⟹ continuous_on s f) ⟹ continuous_on (⋃S) f)"
  using assms
proof(induction S)
  case empty
  then show ?case by auto
next
  case (insert x F)
  then show ?case using continuous_on_closed_Un closed_Union
    by (simp add: closed_Union continuous_on_closed_Un)
qed

lemma chain_reparam_weak_path_line_integral:
  assumes path_eq_chain: "chain_reparam_weak_path γ one_chain" and
    boundary_chain: "boundary_chain one_chain" and
    line_integral_exists: "∀b∈basis. ∀(k::int, γ) ∈ one_chain. line_integral_exists F {b} γ" and
    valid_path: "∀(k::int, γ) ∈ one_chain. valid_path γ" and
    finite_basis: "finite basis" and 
    cont: "∀b∈basis. ∀(k,γ2)∈one_chain. continuous_on (path_image γ2) (λx. F x ∙ b)" and
    finite_one_chain: "finite one_chain"
  shows "line_integral F basis γ = one_chain_line_integral F basis one_chain"
    "line_integral_exists F basis γ"
    (*"valid_path γ" This cannot be proven, see the crappy assumption of derivs/eq_pw_smooth :( *)
proof -
  obtain l where l_props: "set l = one_chain" "distinct l" "reparam γ (rec_join l)" "valid_chain_list l" "l ≠ []"
    using chain_reparam_weak_path_def assms
    by auto
  have bchain_l: "boundary_chain (set l)"
    using l_props boundary_chain
    by (simp add: boundary_chain_def)
  have cont_forall: "∀b∈basis. continuous_on (⋃(k, γ)∈one_chain. path_image γ) (λx. F x ∙ b)"
  proof
    fix b
    assume ass: "b ∈ basis"
    have "continuous_on (⋃((path_image ∘ snd) ` one_chain))  (λx. F x ∙ b)"
      apply(rule continuous_on_closed_UN[where ?S = "(path_image o snd) ` one_chain" ])
    proof
      show "finite one_chain" using finite_one_chain by auto
      show "⋀s. s ∈ (path_image ∘ snd) ` one_chain ⟹ closed s"
        using  closed_valid_path_image[OF] valid_path  
        by fastforce
      show "⋀s. s ∈ (path_image ∘ snd) ` one_chain ⟹ continuous_on s (λx. F x ∙ b)"
        using cont ass by force
    qed
    then show "continuous_on (⋃(k, γ)∈one_chain. path_image γ) (λx. F x ∙ b)"
      by (auto simp add: Union_eq case_prod_beta)
  qed
  show "line_integral_exists F basis γ"
  proof (rule reparam_eq_line_integrals_basis[OF l_props(3) _ _  finite_basis])
    let ?γ2.0="rec_join l"
    show "?γ2.0 piecewise_C1_differentiable_on {0..1}"
      apply(simp only: valid_path_def[symmetric])
      apply(rule joined_is_valid)
      using assms l_props by auto
    show "∀b∈basis. continuous_on (path_image (rec_join l)) (λx. F x ∙ b)" using path_image_rec_join_2[OF l_props(5) l_props(4)] l_props(1)
      using cont_forall continuous_on_subset by blast
    show "∀b∈basis. line_integral_exists F {b} (rec_join l)"
    proof
      fix b
      assume ass: "b∈basis"
      show "line_integral_exists F {b} (rec_join l)"
      proof (rule line_integral_exists_on_rec_join)
        show "boundary_chain (set l)"
          using l_props boundary_chain by auto
        show "valid_chain_list l" using l_props by auto
        show "⋀k γ. (k, γ) ∈ set l ⟹ valid_path γ" using l_props assms by auto
        show "∀(k, γ)∈set l. line_integral_exists F {b} γ" using l_props line_integral_exists ass by blast
      qed
    qed
  qed
  show "line_integral F basis γ = one_chain_line_integral F basis one_chain"
  proof-
    have i: "line_integral F basis (rec_join l) = one_chain_line_integral F basis one_chain"
    proof (rule one_chain_line_integral_rec_join)
      show "set l = one_chain" "distinct l" "valid_chain_list l" using l_props by auto
      show "boundary_chain one_chain" using boundary_chain by auto
      show "∀(k, γ)∈one_chain. line_integral_exists F basis γ"
        using line_integral_sum_basis(2)[OF finite_basis] line_integral_exists by blast
      show "∀(k, γ)∈one_chain. valid_path γ" using valid_path by auto
      show "finite basis" using finite_basis by auto
    qed
    have ii: "line_integral F basis γ = line_integral F basis (rec_join l)"
    proof (rule reparam_eq_line_integrals_basis[OF l_props(3) _ _  finite_basis])
      let ?γ2.0="rec_join l"
      show "?γ2.0 piecewise_C1_differentiable_on {0..1}"
        apply(simp only: valid_path_def[symmetric])
        apply(rule joined_is_valid)
        using assms l_props by auto
      show "∀b∈basis. continuous_on (path_image (rec_join l)) (λx. F x ∙ b)" using path_image_rec_join_2[OF l_props(5) l_props(4)] l_props(1)
        using cont_forall continuous_on_subset by blast
      show "∀b∈basis. line_integral_exists F {b} (rec_join l)"
      proof
        fix b
        assume ass: "b∈basis"
        show "line_integral_exists F {b} (rec_join l)"
        proof (rule line_integral_exists_on_rec_join)
          show "boundary_chain (set l)"
            using l_props boundary_chain by auto
          show "valid_chain_list l" using l_props by auto
          show "⋀k γ. (k, γ) ∈ set l ⟹ valid_path γ" using l_props assms by auto
          show "∀(k, γ)∈set l. line_integral_exists F {b} γ" using l_props line_integral_exists ass by blast
        qed
      qed
    qed
    show "line_integral F basis γ = one_chain_line_integral F basis one_chain" using i ii by auto
  qed
qed

definition chain_reparam_chain' where
  "chain_reparam_chain' one_chain1 subdiv
       ≡ ∃f. ((⋃(f ` one_chain1)) = subdiv) ∧
              (∀cube ∈ one_chain1. chain_reparam_weak_path (rec_join [cube]) (f cube)) ∧
              (∀p∈one_chain1. ∀p'∈one_chain1. p ≠ p' ⟶ f p ∩ f p' = {}) ∧
              (∀x ∈ one_chain1. finite (f x))"

lemma chain_reparam_chain'_imp_finite_subdiv:
  assumes "finite one_chain1"
    "chain_reparam_chain' one_chain1 subdiv"
  shows "finite subdiv"
  using assms
  by(auto simp add: chain_reparam_chain'_def)

lemma chain_reparam_chain'_line_integral:
  assumes chain1_eq_chain2: "chain_reparam_chain' one_chain1 subdiv" and
    boundary_chain1: "boundary_chain one_chain1" and
    boundary_chain2: "boundary_chain subdiv" and
    line_integral_exists_on_chain2: "∀b∈basis. ∀(k::int, γ) ∈ subdiv. line_integral_exists F {b} γ" and
    valid_path: "∀(k, γ) ∈ subdiv. valid_path γ" and
    valid_path_2: "∀(k, γ) ∈ one_chain1. valid_path γ" and
    finite_chain1: "finite one_chain1" and
    finite_basis: "finite basis" and
    cont_field: " ∀b∈basis. ∀(k, γ2)∈subdiv. continuous_on (path_image γ2) (λx. F x ∙ b)"
  shows "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis subdiv"
    "∀(k, γ) ∈ one_chain1. line_integral_exists F basis γ"
proof -
  obtain f where f_props:
    "((⋃(f ` one_chain1)) = subdiv)"
    "(∀cube ∈ one_chain1. chain_reparam_weak_path (rec_join [cube]) (f cube))"
    "(∀p∈one_chain1. ∀p'∈one_chain1. p ≠ p' ⟶ f p ∩ f p' = {})"
    "(∀x ∈ one_chain1. finite (f x))"
    using chain1_eq_chain2 
    by (auto simp add: chain_reparam_chain'_def)
  then have 0: "one_chain_line_integral F basis subdiv = one_chain_line_integral F basis (⋃(f ` one_chain1))"
    by auto
  {fix k γ
    assume ass:"(k, γ) ∈ one_chain1"
    have "line_integral_exists F basis γ ∧
               one_chain_line_integral F basis (f (k, γ)) = k * line_integral F basis γ"
    proof(cases "k = 1")
      assume k_eq_1: "k = 1"
      then have i:"chain_reparam_weak_path γ (f(k,γ))"
        using f_props(2) ass by auto
      have ii:"boundary_chain (f(k,γ))"
        using f_props(1) ass assms  unfolding boundary_chain_def
        by blast
      have iii:"∀b∈basis. ∀(k, γ)∈f (k, γ). line_integral_exists F {b} γ"
        using f_props(1) ass assms
        by blast
      have "iv": " ∀(k, γ)∈f (k, γ). valid_path γ"
        using f_props(1) ass assms
        by blast
      have v: "∀b∈basis. ∀(k, γ2)∈f (k, γ). continuous_on (path_image γ2) (λx. F x ∙ b)"
        using f_props(1) ass assms
        by blast        
      have "line_integral_exists F basis γ ∧ one_chain_line_integral F basis (f (k, γ)) = line_integral F basis γ"
        using chain_reparam_weak_path_line_integral[OF i ii iii iv finite_basis v] ass f_props(4)
        by (auto)
      then show "line_integral_exists F basis γ ∧ one_chain_line_integral F basis (f (k, γ)) = k * line_integral F basis γ"
        using k_eq_1  by auto
    next
      assume "k ≠ 1"
      then have k_eq_neg1: "k = -1"
        using ass boundary_chain1
        by (auto simp add: boundary_chain_def) 
      then have i:"chain_reparam_weak_path (reversepath γ) (f(k,γ))"
        using f_props(2) ass by auto
      have ii:"boundary_chain (f(k,γ))"
        using f_props(1) ass assms unfolding boundary_chain_def
        by blast
      have iii:"∀b∈basis. ∀(k, γ)∈f (k, γ). line_integral_exists F {b} γ"
        using f_props(1) ass assms
        by blast
      have "iv": " ∀(k, γ)∈f (k, γ). valid_path γ"
        using f_props(1) ass assms by blast
      have v: "∀b∈basis. ∀(k, γ2)∈f (k, γ). continuous_on (path_image γ2) (λx. F x ∙ b)"
        using f_props(1) ass assms  by blast        
      have x:"line_integral_exists F basis (reversepath γ) ∧ one_chain_line_integral F basis (f (k, γ)) = line_integral F basis (reversepath γ)"
        using chain_reparam_weak_path_line_integral[OF i ii iii iv finite_basis v] ass f_props(4)
        by auto
      have "valid_path (reversepath γ)"
        using f_props(1) ass assms  by auto
      then have "line_integral_exists F basis γ ∧ one_chain_line_integral F basis (f (k, γ)) = - (line_integral F basis γ)"
        using line_integral_on_reverse_path reversepath_reversepath x ass
        by metis
      then show "line_integral_exists F basis γ ∧ one_chain_line_integral F basis (f (k::int, γ)) = k * line_integral F basis γ"
        using k_eq_neg1  by auto
    qed}
  note cube_line_integ = this
  have finite_chain2: "finite subdiv" 
    using finite_chain1 f_props(1) f_props(4) by auto
  show line_integral_exists_on_chain1: "∀(k, γ) ∈ one_chain1. line_integral_exists F basis γ"
    using cube_line_integ by auto
  have 1: "one_chain_line_integral F basis (⋃(f ` one_chain1)) = one_chain_line_integral F basis one_chain1"
  proof -
    have 0:"one_chain_line_integral F basis (⋃(f ` one_chain1)) = 
                           (∑one_chain ∈ (f ` one_chain1). one_chain_line_integral F basis one_chain)"
    proof -
      have finite: "∀chain ∈ (f ` one_chain1). finite chain"
        using f_props(1) finite_chain2 
        by (meson Sup_upper finite_subset)
      have disj: " ∀A∈f ` one_chain1. ∀B∈f ` one_chain1. A ≠ B ⟶ A ∩ B = {}"
        apply(simp add:image_def)
        using f_props(3)
        by metis
      show "one_chain_line_integral F basis (⋃(f ` one_chain1)) = 
                                (∑one_chain ∈ (f ` one_chain1). one_chain_line_integral F basis one_chain)"
        using Groups_Big.comm_monoid_add_class.sum.Union_disjoint[OF finite disj]
          one_chain_line_integral_def
        by auto
    qed
    have 1:"(∑one_chain ∈ (f ` one_chain1). one_chain_line_integral F basis one_chain) = 
                            one_chain_line_integral F basis one_chain1"
    proof -
      have "(∑one_chain ∈ (f ` one_chain1). one_chain_line_integral F basis one_chain) = 
                                     (∑(k,γ)∈one_chain1. k*(line_integral F basis γ))"
      proof -
        have i:"(∑one_chain ∈ (f ` (one_chain1 - {p. f p = {}})). one_chain_line_integral F basis one_chain) = 
                                       (∑(k,γ)∈one_chain1 - {p. f p = {}}. k*(line_integral F basis γ))"
        proof -
          have "inj_on f (one_chain1 - {p. f p = {}})"
            unfolding inj_on_def
            using f_props(3) by force
          then have 0: "(∑one_chain ∈ (f ` (one_chain1 - {p. f p = {}})). one_chain_line_integral F basis one_chain)
                                                       = (∑(k, γ) ∈ (one_chain1 - {p. f p = {}}). one_chain_line_integral F basis (f (k, γ)))"
            using Groups_Big.comm_monoid_add_class.sum.reindex
            by auto
          have "⋀ k γ. (k, γ) ∈ (one_chain1 - {p. f p = {}}) ⟹
                                                     one_chain_line_integral F basis (f(k, γ)) = k* (line_integral F basis γ)"
            using cube_line_integ by auto
          then have "(∑(k, γ) ∈ (one_chain1 - {p. f p = {}}). one_chain_line_integral F basis (f (k, γ)))
                   = (∑(k, γ) ∈ (one_chain1 - {p. f p = {}}). k* (line_integral F basis γ))"
            by (auto intro!: Finite_Cartesian_Product.sum_cong_aux)
          then show "(∑one_chain ∈ (f ` (one_chain1 - {p. f p = {}})). one_chain_line_integral F basis one_chain) =
                                                     (∑(k, γ) ∈ (one_chain1 - {p. f p = {}}). k* (line_integral F basis γ))"
            using 0  by auto
        qed
        have "⋀ (k::int) γ. (k, γ) ∈ one_chain1 ⟹ (f (k, γ) = {}) ⟹ (k, γ) ∈ {(k',γ'). k'* (line_integral F basis γ') = 0}"
        proof-
          fix k::"int"
          fix γ::"real⇒real*real"
          assume ass:"(k, γ) ∈ one_chain1"
            "(f (k, γ) = {})"
          then have zero_line_integral:"one_chain_line_integral F basis (f (k, γ)) = 0"
            using one_chain_line_integral_def
            by auto
          show "(k, γ) ∈ {(k'::int, γ'). k' * line_integral F basis γ' = 0}"
            using zero_line_integral cube_line_integ ass
            by force
        qed
        then have ii:"(∑one_chain ∈ (f ` (one_chain1 - {p. f p = {}})). one_chain_line_integral F basis one_chain) =
                                                          (∑one_chain ∈ (f ` (one_chain1)). one_chain_line_integral F basis one_chain)"
        proof -
          have "⋀one_chain. one_chain ∈ (f ` (one_chain1)) - (f ` (one_chain1 - {p. f p = {}})) ⟹
                                                         one_chain_line_integral F basis one_chain = 0"
          proof -
            fix one_chain
            assume "one_chain ∈ (f ` (one_chain1)) - (f ` (one_chain1 - {p. f p = {}}))"
            then have "one_chain = {}"
              by auto
            then show "one_chain_line_integral F basis one_chain = 0"
              by (auto simp add: one_chain_line_integral_def)
          qed
          then have 0:"(∑one_chain ∈ f ` (one_chain1) - (f ` (one_chain1 - {p. f p = {}})). one_chain_line_integral F basis one_chain) 
                                                       = 0"
            using Groups_Big.comm_monoid_add_class.sum.neutral
            by auto
          then have "(∑one_chain ∈ f ` (one_chain1). one_chain_line_integral F basis one_chain)
                                                      - (∑one_chain ∈ (f ` (one_chain1 - {p. f p = {}})). one_chain_line_integral F basis one_chain) 
                                                       = 0"
          proof -
            have finte: "finite (f ` one_chain1)" using finite_chain1 by auto
            show ?thesis
              using Groups_Big.sum_diff[OF finte, of " (f ` (one_chain1 - {p. f p = {}}))"
                  "one_chain_line_integral F basis"]
                0
              by auto
          qed                                           
          then show "(∑one_chain ∈ (f ` (one_chain1 - {p. f p = {}})). one_chain_line_integral F basis one_chain) =
                                                          (∑one_chain ∈ (f ` (one_chain1)). one_chain_line_integral F basis one_chain)"
            by auto
        qed
        have "⋀ (k::int) γ. (k, γ) ∈ one_chain1 ⟹ (f (k, γ) = {}) ⟹ f (k, γ) ∈ {chain. one_chain_line_integral F basis chain = 0}"
        proof-
          fix k::"int"
          fix γ::"real⇒real*real"
          assume ass:"(k, γ) ∈ one_chain1"  "(f (k, γ) = {})"
          then have "one_chain_line_integral F basis (f (k, γ)) = 0"
            using one_chain_line_integral_def
            by auto
          then show "f (k, γ) ∈ {p'. (one_chain_line_integral F basis p' = 0)}"
            by auto
        qed
        then have iii:"(∑(k::int,γ)∈one_chain1 - {p. f p = {}}. k*(line_integral F basis γ))
                                                 = (∑(k::int,γ)∈one_chain1. k*(line_integral F basis γ))"
        proof-
          have "⋀ k γ. (k,γ)∈one_chain1 - (one_chain1 - {p. f p = {}})
                                                    ⟹ k* (line_integral F basis γ) = 0"
          proof-
            fix k γ
            assume ass: "(k,γ)∈one_chain1 - (one_chain1 - {p. f p = {}})"
            then have "f(k, γ) = {}"
              by auto
            then have "one_chain_line_integral F basis (f(k, γ)) = 0"
              by (auto simp add: one_chain_line_integral_def)
            then have zero_line_integral:"one_chain_line_integral F basis (f (k, γ)) = 0"
              using one_chain_line_integral_def
              by auto
            then show "k* (line_integral F basis γ) = 0"
              using zero_line_integral cube_line_integ ass
              by force
          qed
          then have "∀(k::int,γ)∈one_chain1 - (one_chain1 - {p. f p = {}}).
                       k* (line_integral F basis γ) = 0" by auto
          then have "(∑(k::int,γ)∈one_chain1 - (one_chain1 - {p. f p = {}}). k*(line_integral F basis γ)) = 0"
            using Groups_Big.comm_monoid_add_class.sum.neutral
              [of "one_chain1 - (one_chain1 - {p. f p = {}})" "(λ(k::int,γ). k* (line_integral F basis γ))"]
            by (simp add: split_beta)
          then have "(∑(k::int,γ)∈one_chain1. k*(line_integral F basis γ)) -
                                                    (∑(k::int,γ)∈ (one_chain1 - {p. f p = {}}). k*(line_integral F basis γ))  = 0"
            using Groups_Big.sum_diff[OF finite_chain1]
            by (metis (no_types) Diff_subset ‹(∑(k, γ)∈one_chain1 - (one_chain1 - {p. f p = {}}). k * line_integral F basis γ) = 0› ‹⋀f B. B ⊆ one_chain1 ⟹ sum f (one_chain1 - B) = sum f one_chain1 - sum f B›)
          then show ?thesis by auto
        qed
        show ?thesis using i ii iii by auto
      qed
      then show ?thesis using one_chain_line_integral_def by auto
    qed                    
    show ?thesis using 0 1 by auto
  qed
  show "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis subdiv" using 0 1 by auto
qed

lemma chain_reparam_chain'_line_integral_smooth_cubes:
  assumes "chain_reparam_chain' one_chain1 one_chain2"
    "∀(k2,γ2)∈one_chain2. γ2 C1_differentiable_on {0..1}"
    "∀b∈basis.∀(k2,γ2)∈one_chain2. continuous_on (path_image γ2) (λx. F x ∙ b)"
    "finite basis"                                                                     
    "finite one_chain1"
    "boundary_chain one_chain1"
    "boundary_chain one_chain2"
    "∀(k,γ)∈one_chain1. valid_path γ"
  shows "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2"
    "∀(k, γ)∈one_chain1. line_integral_exists F basis γ"
proof-
  {fix b
    assume "b ∈ basis"
    fix k γ
    assume "(k, γ)∈one_chain2"
    have "line_integral_exists F {b} γ"
      apply(rule line_integral_exists_smooth)
      using ‹(k, γ) ∈ one_chain2› assms(2) apply blast
      using assms
      using ‹(k, γ) ∈ one_chain2› ‹b ∈ basis› apply blast
      using ‹b ∈ basis› by blast}
  then have a: "∀b∈basis. ∀(k, γ)∈one_chain2. line_integral_exists F {b} γ"
    by auto
  have b: "∀(k2,γ2)∈one_chain2. valid_path γ2"
    using assms(2)
    by (simp add: C1_differentiable_imp_piecewise case_prod_beta valid_path_def)              
  show "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2"
    by (rule chain_reparam_chain'_line_integral[OF assms(1) assms(6) assms(7) a b assms(8) assms(5) assms(4) assms(3)])
  show "∀(k, γ)∈one_chain1. line_integral_exists F basis γ"
    by (rule chain_reparam_chain'_line_integral[OF assms(1) assms(6) assms(7) a b assms(8) assms(5) assms(4) assms(3)])
qed

lemma chain_subdiv_path_pathimg_subset:
  assumes "chain_subdiv_path γ subdiv"
  shows "∀(k',γ')∈subdiv. (path_image γ') ⊆ path_image γ"
  using assms chain_subdiv_path.simps path_image_rec_join
  by(auto simp add: chain_subdiv_path.simps)

lemma reparam_path_image:
  assumes "reparam γ1 γ2"
  shows "path_image γ1 = path_image γ2"
  using assms
  apply (auto simp add: reparam_def path_image_def image_def bij_betw_def)
  apply (force dest!: equalityD2)
  done

lemma chain_reparam_weak_path_pathimg_subset:
  assumes "chain_reparam_weak_path γ subdiv"
  shows "∀(k',γ')∈subdiv. (path_image γ') ⊆ path_image γ"
  using assms
  apply(auto simp add: chain_reparam_weak_path_def)
  using path_image_rec_join reparam_path_image by blast

lemma chain_subdiv_chain_pathimg_subset':
  assumes "chain_subdiv_chain one_chain subdiv"
  assumes "(k,γ)∈ subdiv"
  shows " ∃k' γ'. (k',γ')∈ one_chain ∧ path_image γ ⊆ path_image γ'"
  using assms unfolding chain_subdiv_chain_def  pairwise_def
  apply auto
  by (metis chain_subdiv_path.cases coeff_cube_to_path.simps path_image_rec_join path_image_reversepath)

lemma chain_subdiv_chain_pathimg_subset:
  assumes "chain_subdiv_chain one_chain subdiv"
  shows "⋃ (path_image ` {γ. ∃k. (k,γ)∈ subdiv}) ⊆ ⋃ (path_image ` {γ. ∃k. (k,γ)∈ one_chain})"
  using assms unfolding chain_subdiv_chain_def pairwise_def
  apply auto
  by (metis UN_iff assms chain_subdiv_chain_pathimg_subset' subsetCE case_prodI2) 

lemma chain_reparam_chain'_pathimg_subset':
  assumes "chain_reparam_chain' one_chain subdiv"
  assumes "(k,γ)∈ subdiv"
  shows " ∃k' γ'. (k',γ')∈ one_chain ∧ path_image γ ⊆ path_image γ'"
  using assms chain_reparam_weak_path_pathimg_subset
  apply(auto simp add: chain_reparam_chain'_def set_eq_iff)
  using  path_image_reversepath case_prodE case_prodD old.prod.exhaust
  apply (simp add: list.distinct(1) list.inject rec_join.elims)
  by (smt case_prodD coeff_cube_to_path.simps rec_join.simps(2) reversepath_simps(2) surj_pair)

 definition common_reparam_exists:: "(int × (real ⇒ real × real)) set ⇒ (int × (real ⇒ real × real)) set ⇒ bool" where
    "common_reparam_exists one_chain1 one_chain2 ≡
    (∃subdiv ps1 ps2.
    chain_reparam_chain' (one_chain1 - ps1) subdiv ∧
    chain_reparam_chain' (one_chain2 - ps2) subdiv ∧
    (∀(k, γ)∈subdiv.  γ C1_differentiable_on {0..1}) ∧
    boundary_chain subdiv ∧
    (∀(k, γ)∈ps1. point_path γ) ∧
    (∀(k, γ)∈ps2. point_path γ))"

lemma common_reparam_exists_imp_eq_line_integral:
  assumes finite_basis: "finite basis" and 
    "finite one_chain1"
    "finite one_chain2"
    "boundary_chain (one_chain1::(int × (real ⇒ real × real)) set)"
    "boundary_chain (one_chain2::(int × (real ⇒ real × real)) set)"
    " ∀(k2, γ2)∈one_chain2. ∀b∈basis. continuous_on (path_image γ2) (λx. F x ∙ b)"
    "(common_reparam_exists one_chain1 one_chain2)"
    "(∀(k, γ)∈one_chain1.  valid_path γ)"
    "(∀(k, γ)∈one_chain2.  valid_path γ)"
  shows "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2"
    "∀(k, γ)∈one_chain1. line_integral_exists F basis γ"
proof-
  obtain subdiv ps1 ps2 where props:
    "chain_reparam_chain' (one_chain1 - ps1) subdiv"
    "chain_reparam_chain' (one_chain2 - ps2) subdiv "
    "(∀(k, γ)∈subdiv.  γ C1_differentiable_on {0..1})"
    "boundary_chain subdiv"
    "(∀(k, γ)∈ps1. point_path γ)"
    "(∀(k, γ)∈ps2. point_path γ)"
    using assms
    by (auto simp add: common_reparam_exists_def)
  have subdiv_valid: "(∀(k, γ)∈subdiv.  valid_path γ)"
    apply(simp add: valid_path_def)
    using props(3)
    using C1_differentiable_imp_piecewise by blast
  have onechain_boundary1: "boundary_chain (one_chain1 - ps1)" using assms(4) by (auto simp add: boundary_chain_def)
  have onechain_boundary2: "boundary_chain (one_chain2 - ps1)" using assms(5) by (auto simp add: boundary_chain_def)
  {fix k2 γ2 b
    assume ass: "(k2, γ2)∈subdiv "" b∈basis"
    have "⋀ k γ. (k, γ) ∈ subdiv ⟹ ∃k' γ'. (k', γ') ∈ one_chain2 ∧ path_image γ ⊆ path_image γ'"
      by (meson chain_reparam_chain'_pathimg_subset' props Diff_subset subsetCE)
    then have "continuous_on (path_image γ2) (λx. F x ∙ b)"
      using assms(6) continuous_on_subset[where ?f = " (λx. F x ∙ b)"] ass
      apply(auto simp add:  subset_iff)
      by (metis (mono_tags, lifting) case_prodD)}
  then have cont_field: "∀b∈basis. ∀(k2, γ2)∈subdiv. continuous_on (path_image γ2) (λx. F x ∙ b)"
    by auto
  have one_chain1_ps_valid: "(∀(k, γ)∈one_chain1 - ps1.  valid_path γ)" using assms by auto
  have one_chain2_ps_valid: "(∀(k, γ)∈one_chain2 - ps1.  valid_path γ)" using assms by auto
  have 0: "one_chain_line_integral F basis (one_chain1 - ps1) = one_chain_line_integral F basis subdiv"
    apply(rule chain_reparam_chain'_line_integral_smooth_cubes[OF props(1) props(3) cont_field finite_basis])
    using props assms
    apply blast
    using props assms
    using onechain_boundary1 apply blast
    using props assms
    apply blast
    using one_chain1_ps_valid by blast
  have 1:"∀(k, γ)∈(one_chain1 - ps1). line_integral_exists F basis γ"
    apply(rule chain_reparam_chain'_line_integral_smooth_cubes[OF props(1) props(3) cont_field finite_basis])
    using props assms
    apply blast
    using props assms
    using onechain_boundary1 apply blast
    using props assms
    apply blast
    using one_chain1_ps_valid by blast
  have 2: "one_chain_line_integral F basis (one_chain2 - ps2) = one_chain_line_integral F basis subdiv"
    apply(rule chain_reparam_chain'_line_integral_smooth_cubes[OF props(2) props(3) cont_field finite_basis])
    using props assms
    apply blast
    apply (simp add: assms(5) boundary_chain_diff)
    apply (simp add: props(4))
    by (simp add: assms(9))
  have 3:"∀(k, γ)∈(one_chain2 - ps2). line_integral_exists F basis γ"
    apply(rule chain_reparam_chain'_line_integral_smooth_cubes[OF props(2) props(3) cont_field finite_basis])
    using props assms
    apply blast
    apply (simp add: assms(5) boundary_chain_diff)
    apply (simp add: props(4))
    by (simp add: assms(9))
  show line_int_ex_chain1: "∀(k, γ)∈one_chain1. line_integral_exists F basis γ"
    using 0 
    using "1" finite_basis line_integral_exists_point_path props(5) by fastforce
  then show "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2"
    using 0 1 2 3
    using assms(2-3) finite_basis one_chain_line_integral_point_paths props(5) props(6) by auto
qed

definition subcube :: "real ⇒ real ⇒ (int × (real ⇒ real × real)) ⇒ (int × (real ⇒ real × real))" where
  "subcube a b cube = (fst cube, subpath a b (snd cube))"

lemma subcube_valid_path:
  assumes "valid_path (snd cube)" "a ∈ {0..1}" "b ∈ {0..1}"
  shows "valid_path (snd (subcube a b cube))"
  using valid_path_subpath[OF assms] by (auto simp add: subcube_def)

end