Quellcode-Bibliothek Paths.thy

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 \<Rightarrow> '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 *<sub>R</sub> 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 *<sub>R</sub> 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 *<sub>R</sub> 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:
  "measure lborel (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 "measure lborel (box a b) = measure lborel (cbox a b)"
  by (simp add: content_box_cases content_cbox_cases)

lemma content_eq_0: "measure lborel (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 < measure lborel (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 < measure lborel (box a b) ⟷ measure lborel (box a b) ≠ 0"
  using Paths.content_eq_0 zero_less_measure_iff by blast

lemma content_subset: "cbox a b ⊆ box c d ==> measure lborel (cbox a b) ≤ measure lborel (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 "measure lborel (box a b) = 0"
    and "p tagged_division_of (box a b)"
  shows "sum (λ(x,k). measure lborel 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). measure lborel k *_R f x) y = measure lborel 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). measure lborel k *_R f x) y = 0" .
qed


lemma has_integral_null [intro]: "measure lborel(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 *<sub>R</sub> 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) *<sub>R</sub> 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) *<sub>R</sub> 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',γ
         f_p(1) assms k by (meson UN_I boundary_chain)
      haveii \forall(k,\gamma>)∈"
        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 : l bss(eespat >)"
        using iv line_integral_on_reverse_path2)id_path_reversepath
        by fastforce
      show ?thesis
        using line_integral_on_path_eq_line_integral_on_equiv_chain'(2)[OF i iixiiisis
        by auto
    qed
  
  then "\forall(k,γsubdiv. line_integral_exists F basis γ
   hw"ne_chain_line_integral_hain1lFasis
    using one_chain_line_integral_eq_line_integral_on_sudivision() ssms
    byauto
qed

lemma line_integral_sum_gen
  assumes
    "finite basis"d
    line_integral_exists:
    "line_integral_exists F basis1ultsoP <sga> "ule
    "line_integral_exists _itgrlxist as2\gamma" and
    basis_partition
    "is1 ∪=basi bss <inter> bai2={}
  shows "line_integral F basis\> = (line_integral basis1) + (line_integral <)"
    "line_integral_exists1 ∥2" ysmp
   apply (simp add: line_integral_def)
proof -
  have 0: "integral {0.}\lambdax. (∑b∈basis1. F (γ x) ∙ b * (vector_derivative γ<>b 
                                       (∑net_tree_ips^>"
                    {<lambdax <S>b∈. \gamma x) ∙ b * (vector_derivative γ1} <bullet>b)
                           integral {0..1} (λb∈.} \bullet b))"
    using Henstock_Kurzweil_Integration.integral_addral_existsl_exists
    by (auto simp add: line_integral_exists_def)
  havevee:"ntegral{0..}(<>x. \Sum>b∈ga> 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 (γ b * (vector_derivative γ (at wihin{..} <bull> b)))"
    by (metismono_tagstingnite_Unfinite_basismunion_disjoint
  show "integral {0..1} (λb∈sis \gamma x) ∙ (at x within {0..1}) ∙
                  integral {0..1 (\\lamb>x. . ∑b∈basis1. F (γ x) ∙ b * (vector_derivative γ (at x within {0..1}) ∙
                  integral {0..1} (λ<um>b<in>basis2. F (γ x) ∙ b * (vector_derivative γ (at x within {0..1}) ∙ b))"
    using 0 1
    by auto
  have 2: "((λb∈ (<a> x) ∙ b * (vector_derivative γ (at x within {0..1}) ∙
                                       b∈s2 F(<> x)\< b
                    .<>x.\Sumb∈ b * (vector_derivative γa xwti 0.} <>b)) +
                           integral {01 \lambdax. ∑b∈ x) ∙xwti {..1)<>) 0.1"
    enstock_Kurzweil_Integrationl_exists_l_integral
    pply
    by
  have:<lambda<b∈ b * (vector_derivative γ (at{..) <bullet 
                       (λb∈ x)<> b * (vector_derivative γ)\bullet b)) +
                                            induction
    by (metis (mono_tagsnfinite_Un_basississummnion_disjoint
  show "line_integral_exists F basis γ
    apply(auto simp add: line_integral_exists_def has_integral_integral)
    using
    using has_integral_integrable_integral by fastforce
qed

definition common_boundary_sudivision_exists where
    "common_boundary_sudivision_exists one_chain1
             ∃
                      chain_subdiv_chain one_chain2and
                      (forall(k, γ subdiv. valid_path γ
                      

lemma common_boundary_sudivision_commutative:
  "(common_boundary_sudivision_exists one_chain1 one_chain2) = (common_boundary_sudivision_exists one_chain2 one_chain1)"
  apply (simpd mmon_boundary_sudivision_exists_def
  by blast

lemma common_subdivision_imp_eq_line_integral
  ssumes_istsone_chain1
    "boundary_chain one_chain1"
    "boundary_chain one_chain2"
    "forall>(k, γ)∈"
    "finite one_chain1"
    "finite one_chain2"
    "finite basis"
  showshain_line_integral ne_chain_line_integralegral
    "\<forall\one_chain2. line_integral_exists F basis <"
prooferulecal
  obtain subdiv
    " ecan1 udv
    "chain_subdiv_chain m"
    "(∀ subdivd_path)"
    "(boundary_chain        "(s>, t') ∈ oreachable (opnet onp p₂) (?S p₂)
    using assms
    by (auto simp add: common_boundary_sud)
  ve :"<(k, γsubdiv. line_integral_exists F basis γ
    using one_chain_line_integral_eq_line_integral_on_sudivisionssmssmsbdiv_propsssms7
    yautoto
  showalsisone_chain1Fisne_chain2in2
    using one_chain_line_integral_eq_line_integral_on_sudivision
      one_chain_line_integral_eq_line_integral_on_sudivision-(druleestep_invariantD]p_all
    by auto
  show "\<      moreover∧ξ. U ξ \<\<
    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 ne_chain2
        ∃
                  chain_subdiv_chain (one_chain2 - ps2) subdiv<and
                  (∀ subdiv. valid_path) ∧
                  (boundary_chainubdiv and
                  (<(k, γ) ∧
      net_tree_ips p₁> net_tree_ips pjava.lang.NullPointerException

lemma common_sudiv_exists_comm:
  shows "common_sudiv_exists C1 C2 = common_sudiv_exists C2 C1"
  ( mpommon_sudiv_exists_def

lemmae_integral_degenerate_chaingral_degenerate_chain
  assumes(k, γ chain. point_path)"
  assumes "finitej∈2. U (\sigma' j)"
  shows "one_chain_line_integral F basis chain = 0"
proof (simp add: one_chain_line_integral_def)
  have "∀chain. line_integral
    using assms line_integral_point_path
    by blast
  then have "<\inin ral_fn k eiegrl s "
  thensigma, s<^>)___True_ True
    by fastforce
  then show "(\<umx
    by simp
qedand s2 "<, s₂"

lemma gen_common_subdiv_imp_common_subdiv:
  shows "(common_sudiv_exists one_chain1 one_chain2thus', s₁ ∧2') ∈2"
  by (auto simp add: common_sudiv_exists_def common_boundary_sudivision_exists_def)

lemma common_subdiv_imp_gen_common_subdiv:
  assumes
  shows "(common_sudiv_existsn1
  using
  apply          by rulereachable_other
  by (metis Diff_empty all_not_in_convechable_local

lemma one_chain_line_integral_point_paths:
  assumes "finite one_chain"
  assumes"finitebss
  assumes "(∀
  showsξ. U <><i"
proof-
  have 0:"(∀ps. se<Rightarrow  (real_of_int k *line_integral basis
    usingoint_path
     force
  show(σ'). (a = τ (∃ U (σ' i)))"
    unfolding oechinlin_ntga_e si 0\open>finite one_chain›
    by (force simp add: tr: cm_oodadclss.ummn_eta_et)
qed

lemma boundary_chain_diff:
  assumes "boundary_chain prooftion
  shows "boundary_chainoe_cai )
  using assms
  by (auto simp add: boundary_chainfi <> s a \sigma' s'

lemma gen_common_subdivision_imp_eq_line_integral:
  assumes "(common_sudiv_exists_in2java.lang.StringIndexOutOfBoundsException: Index 55 out of bounds for length 55
    "boundary_chain one_han1
    "boundary_chain one_chain2"
    "<>k, γ)∈one_chain1. line_integral_exists F basis γ
    finite
    assume<>1 ⊨_A (?I, ?U p₎ ?inv (t_tree_ips1)"
    "asis
  shows "one_chain_line_integral F basisone_ci= _h_ln_nega ai n_cain2"
    "∀(k, γ a"
proof -
  obtain ps1 ps2ubdivivision_existsain12)""<forall(k, γps1. point_path)" " <forall(k, γps2. point_path<amma>)"
    using assms(1) gen_common_subdiv_imp_common_subdiv\<And>ξ. U ξ ξ›
    by blast
  show "one_chain_line_integral F basisain1  e_chain2
    using hain_line_integral_point_pathscommon_subdiv
      assms(2-7 gen_subdiv
      common_subdivision_imp_eq_line_integraltegral)dary_chain_diffassmsboundary_chain_diffms)
    by auto
  show "∀(k, \from dt av "sigma m ∧i<inet_tree_ips1. S(sigma i) (' i)
  <a = R:*cast(m)›
    obtainv herediv_props
      _iv_chain_in1ps1 ubdiv
      "chain_subdiv_chain (one_chain2-ps2) subdiv"to
      next
      "(boundary_chain subdiv)"
      using gen_subdiv(1)
      by (autodary_sudivision_exists_def
    have "∀oarrivemsg I σ a›
      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_chain22integral_exists"
      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
      sing gn_sbi()ln_inrlexit_oipt[O sm(
      by blast
  qed
qedbyuet!:ote_naint O iv2

lemma common_sudiv_exists_f:
      assumes "common_sudiv_exists (∀net_tree_ips1 ⟶=>i))"
      shows "mmon_sudiv_exists
      using assms
      apply(simpd on_sudiv_exists_def
      by auto

lemma chain_subdiv_path_singleton:
  shows "chain_subdiv_path \>{(1,γ
proof -
  have "rec_join [(1
    by (simps_def
  then have "set [(1,γi∈1. S (σ' i)"
    by auto
  then show ?thesis
    by (metis (no_types) chain_subdiv_path
qed

lemma:
  showsgamma) ,<gamma)}"
proof -
  have "oin)] = reversepath"
    by (simp add: joinpaths_def)
  then have "setgamma)] = {(- 1 )}" "distinct)]"
             "rec_join)] = reversepath" "valid_chain_list)]"
    by auto
 thene hve"_th(versepath) (set)])"
    using chai_udv_pahitob ls
  then show ?thesis
    by simphenceit (<, )∈1)"
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
  unfolding chain_subdiv_chain_def boundary_chain_defairwise_defto_path
  by (rule_tac xmoreover', t) <chable( have java.lang.NullPointerException

(*path reparam_weaketrization*)

definition reparam_weak where
  "reparam_weak γ, t) ∈2) (?S p₂)"

definition reparam where
  "reparam γ1 γ2 ≡net_tree_ips p. S (σ i) (σ

lemma:
  shows "reparam_weak γ?S (p₁ ∥2) σ σ' a›re_ip<1 ∥2) ⟶ S (σ' j)"
  unfolding
  apply (xin
  by (auto1ferentiable_on_defiable_on_def

lemma line_integral_exists_smooth_one_base
  assumes "γaeinofhs_nerlsbtut
    "continuous_on<) (λx. F x ∙ b)"
  shows "line_integral_exists F {b} γ
proof-
  have gamma2_differentiable: "(∀ {0 .. 1}. γ
    using()
    by (auto simp add: valid_path_def C1_differentiable_on_eq)
  then have gamma2_b_component_di(🚫2)"                                    
    by auto
  then have "(λ> b) differentiable_on {0..1}"
    using differentiable_at_withinI
    by (auto simp addifferentiable_on_def
  then
    using differentiable_imp_continuous_on
    by auto-(rule
  have gamma2_cont:"continuous_on {0..
    using assms(1) C1_differentiable_imp_continuous_on
    by ((uosm dd lipt_e)
  haveeii:"tinuous_on<>Fgamma ) \>b * (vector_derivative γ b))"
  proof-
    have 0: "continuous_on {0..1} (\"<>,connect', s'))\in> trans (opnet onp1)"
      using assms(2) continuous_on_compose[OF gamma2_cont]
      by (auto simp add: path_image_def)
    tain whee D"<forallx{0..1}. (γand continuous_on {.1 D
      s)
      by (auto simptiable_on_def
    then have:forallx∈
      singt_within_ivl
      by fastforce
    then have "continuous_on {0..1} (λ (at x with{0..1}))"
      usingce
    then have 1: "continuous_on {0..1} (λ
      auto intro!: continuous_intros)
    show ?thesis
      using nuuo_ml[F01] yat
  qed
  then have "(\x. F (<gammax b (ctor_derivative (at within b)) integrable_on {0..1}"
    using integrable_continuous_real
    by u
  then show "line_integral_existsgamma"
    by(auto simp add: line_integral_exists_def)
qed

lemma contour_integral_primitive_lemma:
  assume"'
  assumesfrom<j. j∉2 ⟶ j"
      and "∧∧ξ. S ξ›
      and "g piecewise_differem ae"', s') ∈1) (?S p₁
    howsx. f'(g   or_derivative within
             has_integral)}
proof -
  obtain  :nitetee >∈
    using assms by (autocewise_differentiable_on_defntiable_on_def
  have g continuous_onx. f (g)java.lang.StringIndexOutOfBoundsException: Index 56 out of bounds for length 56
    apply (rule continuous_on_compose [OF cg, unfoldedorttr
    using assms
    apply (metiseffield_differentiable_imp_continuous_atntiable_imp_continuous_atinuous_on_eq_continuous_withinthincontinuous_on_subset
    done
  { fix x:al
    " x and b: "x < b" and xk: "x ∉ ow
    then have "g differentiable at x within {a..b}"
      using d ifferentiable_at_withinI
    ve "(hvetr_eiaievco_rvtv (txwth{.b})(txwti {.}"
      by (simp add: vector_derivative_works has_field_derivative_def scaleR_conv_of_real "∀net_tree_ips p_'
    then have gdiff: "(g has_derivative (java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "brackoff" is null
      by (simppaddR_conv_of_real
    have "(f haseddrvtv f gx) (t( xwth`{aa.}"
      using assms by (metis a atLeastAtMost_iff b DERIV_subset image_subset_iffeal_def
    then subnet_oreachable_disjoint
      by (simpvative_def
    have "<>xfgx)a_etrdrvaef (g )*eto_eiaieg(t ih a.})(txwti{.b}"
      using diff_chain_within:And R. ⟨i : onp i : R⟩subo ⊨A (λσ<, other U {i )
      yddivative_defl_def
  } note * = this
  how
    apply (rule fundamental_theorem_of_calculus_interior_strong)
    usingkassmsssms
    apply (autoi
    done
qed

java.lang.StringIndexOutOfBoundsException: Index 157 out of bounds for length 96
  fixes f :: "'a::{euclidean_space,real_normed_field} ==> 'a::{euclidean_space,real_normed_field}" and
        g :: "real ==>
  assumes "<>a::'a). a ∈e  ) at in
      and:.1<>.<in g x ∈
      ase_vecin Basis"
  ows(\lambdax. ((f'(g x)) * (vectoreriaie a wti 0..1}))) ∙
             has_integral (((f(g 1))\bullet base_vec - (f(g 0)) ∙
proof -
  obtain k where k: "finitex∈" :"ous_on
    using assmsutoe_differentiable_on_def
  have cfg: "continuous_on {0..1} (λ
    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 *<sub>R</sub> (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 **:"(\<gamma>2 has_vector_derivative (vector_derivative \<gamma>2 (at (\<phi> x)))) (at (\<phi> 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 \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> 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:"\<And>x.  x\<in>({0..1} -((\<phi> -` ?s') \<union> ?s)) \<Longrightarrow> D x * (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b)) = 
                                    F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)"
    by auto
  then have d: "integral ({0..1}) (\<lambda>x. D x * (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b))) = 
                                            integral ({0..1}) (\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b))"
  proof-
    have "negligible ((\<phi> -` ?s') \<union> ?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: "(\<And>x. x \<in> {0..1} \<Longrightarrow> \<phi> x \<in> {0..1})" using phi
    using v by blast
  then have e: "((\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) has_integral
                             integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))){0..1}"
  proof-
    have "negligible ?s" using s_inter(1) by auto
    have 0: "negligible ((\<phi> -` ?s') \<union> ?s)" using finite_neg_img s(1) by auto
    have c':"\<forall> x\<in> {0..1} - ((\<phi> -` ?s') \<union> ?s). D x * (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b)) = 
                                    F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)"
      using c  by blast
    have has_integral_spike_eq': "\<And>s t f g y. negligible s \<Longrightarrow>
                                                       \<forall>x\<in>t - s. g x = f x \<Longrightarrow> (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: "((\<lambda>x. F (\<gamma>1 x) \<bullet> b * (vector_derivative  \<gamma>1 (at x within {0..1}) \<bullet> b)) has_integral
                     integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b)))
                       {0..1}"
  proof-
    assume ass: "((\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) has_integral
                            integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b)))
                             {0..1}"
    have *:"\<forall>x\<in>{0..1} - ( ((\<phi> -` ?s') \<union> ?s) \<union> {0,1}). (\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative  (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) x =
                                                  (\<lambda>x. F (\<gamma>1 x) \<bullet> b * (vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b)) x"
    proof-
      have "\<forall>x\<in>{0<..<1}  - (\<phi> -` ?s' \<union> ?s). (vector_derivative  (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b) = (vector_derivative  (\<gamma>1) (at x within {0..1}) \<bullet> b)"
      proof
        have i: "open ({0<..<1}  - ((\<phi> -` ?s') \<union> ?s))" using open_diff s(1) open_greaterThanLessThan finite_neg_img
          by (simp add: open_diff)
        have ii: "\<forall>x\<in>{0<..<1::real}  - (\<phi> -` ?s' \<union> ?s). (\<gamma>2 \<circ> \<phi>) x = \<gamma>1 x" using phi(1)
          by auto                              
        fix x::real
        assume ass: " x \<in> {0<..<1::real} -  ((\<phi> -` ?s') \<union> ?s)"
        then have iii: "(\<gamma>2 \<circ> \<phi> has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (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 \<gamma>" 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