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: "\<forall>(k, \<gamma>)\<in>(f(k,\<gamma>)). line_integral_exists F basis \<gamma>"
            using f_props(1) line_integral_exists_on_chain2 ass
            by blast
          have vpath: " \<forall>(k, \<gamma>)\<in>(f(k, \<gamma>)). valid_path \<gamma>"
            using f_props(1) assms ass by blast
          have "one_chain_line_integral F basis (f (k, \<gamma>)) = k * line_integral F basis \<gamma>"
          proof(cases "k = 1")
            assume k_eq_1: "k = 1"
            have "one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis \<gamma>"
              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, \<gamma>)) = k * line_integral F basis \<gamma>"
              using k_eq_1
              by auto
          next
            assume "k \<noteq> 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, \<gamma>)) = line_integral F basis (reversepath \<gamma>)"
              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, \<gamma>)) = - (line_integral F basis \<gamma>)"
              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, \<gamma>)) = k * line_integral F basis \<gamma>"
              using k_eq_neg1  by auto
          qed
          then show "(k, \<gamma>) \<in> {(k'::int, \<gamma>'). k' * line_integral F basis \<gamma>' = 0}"
            using zero_line_integral by auto
        qed
        then have ii:"(\<Sum>one_chain \<in> (f ` (one_chain1 - {p. f p = {}})). one_chain_line_integral F basis one_chain) =
                                                          (\<Sum>one_chain \<in> (f ` (one_chain1)). one_chain_line_integral F basis one_chain)"
        proof -
          have "\<And>one_chain. one_chain \<in> (f ` (one_chain1)) - (f ` (one_chain1 - {p. f p = {}})) \<Longrightarrow>
                                                         one_chain_line_integral F basis one_chain = 0"
          proof -
            fix one_chain
            assume "one_chain \<in> (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:"(\<Sum>one_chain \<in> 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 "(\<Sum>one_chain \<in> f ` (one_chain1). one_chain_line_integral F basis one_chain)
                                                      - (\<Sum>one_chain \<in> (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 "(\<Sum>one_chain \<in> (f ` (one_chain1 - {p. f p = {}})). one_chain_line_integral F basis one_chain) =
                                                          (\<Sum>one_chain \<in> (f ` (one_chain1)). one_chain_line_integral F basis one_chain)"
            by auto
        qed
        have "\<And> (k::int) \<gamma>. (k, \<gamma>) \<in> one_chain1 \<Longrightarrow> (f (k, \<gamma>) = {}) \<Longrightarrow> f (k, \<gamma>) \<in> {chain. one_chain_line_integral F basis chain = 0}"
        proof-
          fix k::"int"
          fix \<gamma>::"one_cube"
          assume ass:"(k, \<gamma>) \<in> one_chain1" "(f (k, \<gamma>) = {})"
          then have "one_chain_line_integral F basis (f (k, \<gamma>)) = 0"
            using one_chain_line_integral_def  by auto
          then show "f (k, \<gamma>) \<in> {p'. (one_chain_line_integral F basis p' = 0)}"
            by auto
        qed
        then have iii:"(\<Sum>(k::int,\<gamma>)\<in>one_chain1 - {p. f p = {}}. k*(line_integral F basis \<gamma>))
                                                 = (\<Sum>(k::int,\<gamma>)\<in>one_chain1. k*(line_integral F basis \<gamma>))"
        proof-
          have "\<And> k \<gamma>. (k,\<gamma>)\<in>one_chain1 - (one_chain1 - {p. f p = {}})
                                                    \<Longrightarrow> k* (line_integral F basis \<gamma>) = 0"
          proof-
            fix k \<gamma>
            assume ass: "(k,\<gamma>)\<in>one_chain1 - (one_chain1 - {p. f p = {}})"
            then have "f(k, \<gamma>) = {}"
              by auto
            then have "one_chain_line_integral F basis (f(k, \<gamma>)) = 0"
              by (auto simp add: one_chain_line_integral_def)
            then have zero_line_integral:"one_chain_line_integral F basis (f (k, \<gamma>)) = 0"
              using one_chain_line_integral_def by auto
            have bchain: "boundary_chain (f(k,\<gamma>))"
              using f_props(1) boundary_chain2 ass
              by (auto simp add: boundary_chain_def)
            have wexist: "\<forall>(k, \<gamma>)\<in>(f(k,\<gamma>)). line_integral_exists F basis \<gamma>"
              using f_props(1) line_integral_exists_on_chain2 ass
              by blast
            have vpath: " \<forall>(k, \<gamma>)\<in>(f(k, \<gamma>)). valid_path \<gamma>"
              using f_props(1) assms ass
              by blast
            have "one_chain_line_integral F basis (f (k, \<gamma>)) = k * line_integral F basis \<gamma>"
            proof(cases "k = 1")
              assume k_eq_1: "k = 1"
              have "one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis \<gamma>"
                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, \<gamma>)) = k * line_integral F basis \<gamma>"
                using k_eq_1
                by auto
            next
              assume "k \<noteq> 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, \<gamma>)) = line_integral F basis (reversepath \<gamma>)"
                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, \<gamma>)) = - (line_integral F basis \<gamma>)"
                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, \<gamma>)) = k * line_integral F basis \<gamma>"
                using k_eq_neg1
                by auto
            qed
            then show "k* (line_integral F basis \<gamma>) = 0"
              using zero_line_integral
              by auto
          qed
          then have "\<forall>(k::int,\<gamma>)\<in>one_chain1 - (one_chain1 - {p. f p = {}}).
                                                      k* (line_integral F basis \<gamma>) = 0" by auto
          then have "(\<Sum>(k::int,\<gamma>)\<in>one_chain1 - (one_chain1 - {p. f p = {}}). k*(line_integral F basis \<gamma>)) = 0"
            using Groups_Big.comm_monoid_add_class.sum.neutral
              [of "one_chain1 - (one_chain1 - {p. f p = {}})" "(\<lambda>(k::int,\<gamma>). k* (line_integral F basis \<gamma>))"]
            by (simp add: split_beta)
          then have "(\<Sum>(k::int,\<gamma>)\<in>one_chain1. k*(line_integral F basis \<gamma>)) -
                     (\<Sum>(k::int,\<gamma>)\<in> (one_chain1 - {p. f p = {}}). k*(line_integral F basis \<gamma>)) = 0"
            using Groups_Big.sum_diff[OF finite_chain1]
            by (metis (no_types) Diff_subset \<open>(\<Sum>(k, \<gamma>)\<in>one_chain1 - (one_chain1 - {p. f p = {}}). k * line_integral F basis \<gamma>) = 0\<close> \<open>\<And>f B. B \<subseteq> one_chain1 \<Longrightarrow> sum f (one_chain1 - B) = sum f one_chain1 - sum f B\<close>)
          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: "\<forall>(k, \<gamma>) \<in> one_chain1. line_integral_exists F basis \<gamma>" and
    valid_path: "\<forall>(k, \<gamma>) \<in> subdiv. valid_path \<gamma>" 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"
    "\<forall>(k, \<gamma>) \<in> subdiv. line_integral_exists F basis \<gamma>"
proof -
  obtain f where f_props:
    "((\<Union>(f ` one_chain1)) = subdiv)"
    "(\<forall>(k,\<gamma>)\<in>one_chain1. if k = 1 then chain_subdiv_path \<gamma> (f(k,\<gamma>)) else chain_subdiv_path (reversepath \<gamma>) (f(k,\<gamma>)))"
    "(\<forall>p\<in>one_chain1. \<forall>p'\<in>one_chain1. p \<noteq> p' \<longrightarrow> f p \<inter> f p' = {})"
    "(\<forall>x \<in> 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 "\<And>k \<gamma>. (k, \<gamma>) \<in> subdiv \<Longrightarrow> line_integral_exists F basis \<gamma>"
  proof -
    fix k \<gamma>
    assume ass: "(k, \<gamma>) \<in> subdiv"
    then obtain k' \<gamma>' where kp_gammap: "(k',\<gamma>') \<in> one_chain1" "(k,\<gamma>) \<in> f(k',\<gamma>')"
      using f_props(1) by fastforce
    show "line_integral_exists F basis \<gamma>"
    proof (cases "k' = 1")
      assume k_eq_1: "k' = 1"
      then have i:"chain_subdiv_path \<gamma>' (f(k',\<gamma>'))"
        using f_props(2) kp_gammap ass  by auto
      have ii:"boundary_chain (f(k',\<gamma>'))"
        using f_props(1) ass assms kp_gammap  by (meson UN_I boundary_chain_def)
      have iii:"line_integral_exists F basis \<gamma>'"
        using assms kp_gammap by blast
      have "iv": " \<forall>(k, \<gamma>)\<in>f (k', \<gamma>'). valid_path \<gamma>"
        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' \<noteq> 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 \<gamma>') (f(k',\<gamma>'))"
        using f_props(2) kp_gammap by auto
      have ii:"boundary_chain (f(k',\<gamma>'))"
        using f_props(1) assms kp_gammap  by (meson UN_I boundary_chain_def)
      have iii: " \<forall>(k, \<gamma>)\<in>f (k', \<gamma>'). valid_path \<gamma>"
        using f_props(1) ass assms kp_gammap by blast
      have iv: "valid_path (reversepath \<gamma>')"
        using valid_path_equiv_valid_chain_list[OF i ii iii]
        by force
      have "line_integral_exists F basis \<gamma>'"
        using assms kp_gammap  by blast
      then have x: "line_integral_exists F basis (reversepath \<gamma>')"
        using iv line_integral_on_reverse_path(2) valid_path_reversepath
        by fastforce
      show ?thesis
        using line_integral_on_path_eq_line_integral_on_equiv_chain'(2)[OF i ii x iii finite_basis] kp_gammap
        by auto
    qed
  qed
  then show "\<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F basis \<gamma>" by auto
  then show "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis subdiv"
    using one_chain_line_integral_eq_line_integral_on_sudivision(1) assms
    by auto
qed

lemma line_integral_sum_gen:
  assumes finite_basis:
    "finite basis" and
    line_integral_exists:
    "line_integral_exists F basis1 \<gamma>"
    "line_integral_exists F basis2 \<gamma>" and
    basis_partition:
    "basis1 \<union> basis2 = basis" "basis1 \<inter> basis2 = {}"
  shows "line_integral F basis \<gamma> = (line_integral F  basis1 \<gamma>) + (line_integral F basis2 \<gamma>)"
    "line_integral_exists F basis \<gamma>"
   apply (simp add: line_integral_def)
proof -
  have 0: "integral {0..1} (\<lambda>x. (\<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) +
                                       (\<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))) =
                    integral {0..1} (\<lambda>x. \<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) +
                           integral {0..1} (\<lambda>x. \<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))"
    using Henstock_Kurzweil_Integration.integral_add line_integral_exists
    by (auto simp add: line_integral_exists_def)
  have 1: "integral {0..1} (\<lambda>x. \<Sum>b\<in>basis. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) =
                       integral {0..1} (\<lambda>x. (\<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) +
                                            (\<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)))"
    by (metis (mono_tags, lifting) basis_partition finite_Un finite_basis sum.union_disjoint)
  show "integral {0..1} (\<lambda>x. \<Sum>b\<in>basis. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) =
                  integral {0..1} (\<lambda>x. \<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) +
                  integral {0..1} (\<lambda>x. \<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))"
    using 0 1
    by auto
  have 2: "((\<lambda>x. (\<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) +
                                       (\<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))) has_integral
                    integral {0..1} (\<lambda>x. \<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) +
                           integral {0..1} (\<lambda>x. \<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))) {0..1}"
    using Henstock_Kurzweil_Integration.has_integral_add line_integral_exists has_integral_integral
    apply (auto simp add: line_integral_exists_def)
    by blast
  have 3: "(\<lambda>x. \<Sum>b\<in>basis. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) =
                       (\<lambda>x. (\<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) +
                                            (\<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)))"
    by (metis (mono_tags, lifting) basis_partition finite_Un finite_basis sum.union_disjoint)
  show "line_integral_exists F basis \<gamma>"
    apply(auto simp add: line_integral_exists_def has_integral_integral)
    using 2 3
    using has_integral_integrable_integral by fastforce
qed

definition common_boundary_sudivision_exists where
    "common_boundary_sudivision_exists one_chain1 one_chain2 \<equiv>
             \<exists>subdiv. chain_subdiv_chain one_chain1 subdiv \<and>
                      chain_subdiv_chain one_chain2 subdiv \<and>
                      (\<forall>(k, \<gamma>) \<in> subdiv. valid_path \<gamma>)\<and>
                      boundary_chain subdiv"

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

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

definition common_sudiv_exists where
    "common_sudiv_exists one_chain1 one_chain2 \<equiv>
        \<exists>subdiv ps1 ps2. chain_subdiv_chain (one_chain1 - ps1) subdiv \<and>
                  chain_subdiv_chain (one_chain2 - ps2) subdiv \<and>
                  (\<forall>(k, \<gamma>) \<in> subdiv. valid_path \<gamma>) \<and>
                  (boundary_chain subdiv) \<and>
                  (\<forall>(k, \<gamma>) \<in> ps1. point_path \<gamma>) \<and>
                  (\<forall>(k, \<gamma>) \<in> ps2. point_path \<gamma>)"

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

lemma line_integral_degenerate_chain:
  assumes "(\<forall>(k, \<gamma>) \<in> chain. point_path \<gamma>)"
  assumes "finite basis"
  shows "one_chain_line_integral F basis chain = 0"
proof (simp add: one_chain_line_integral_def)
  have "\<forall>(k,g)\<in>chain. line_integral F basis g = 0"
    using assms line_integral_point_path
    by blast
  then have "\<forall>(k,g)\<in>chain. real_of_int k * line_integral F basis g = 0" by auto
  then have "\<And>p. p \<in> chain \<Longrightarrow> (case p of (i, f) \<Rightarrow> real_of_int i * line_integral F basis f) = 0"
    by fastforce
  then show "(\<Sum>x\<in>chain. case x of (k, g) \<Rightarrow> real_of_int k * line_integral F basis g) = 0"
    by simp
qed

lemma gen_common_subdiv_imp_common_subdiv:
  shows "(common_sudiv_exists one_chain1 one_chain2) = (\<exists>ps1 ps2. (common_boundary_sudivision_exists (one_chain1 - ps1) (one_chain2 - ps2)) \<and> (\<forall>(k, \<gamma>)\<in>ps1. point_path \<gamma>) \<and> (\<forall>(k, \<gamma>)\<in>ps2. point_path \<gamma>))"
  by (auto simp add: common_sudiv_exists_def common_boundary_sudivision_exists_def)

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

lemma one_chain_line_integral_point_paths:
  assumes "finite one_chain"
  assumes "finite basis"
  assumes "(\<forall>(k, \<gamma>)\<in>ps. point_path \<gamma>)"
  shows "one_chain_line_integral F basis (one_chain - ps) = one_chain_line_integral F basis (one_chain)"
proof-
  have 0:"(\<forall>x\<in>ps. case x of (k, g) \<Rightarrow>  (real_of_int k * line_integral F basis g) = 0)"
    using line_integral_point_path assms
    by force
  show "one_chain_line_integral F basis (one_chain - ps) = one_chain_line_integral F basis one_chain"
    unfolding one_chain_line_integral_def using 0 \<open>finite one_chain\<close>
    by (force simp add:  intro: comm_monoid_add_class.sum.mono_neutral_left)
qed

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

lemma gen_common_subdivision_imp_eq_line_integral:
  assumes "(common_sudiv_exists one_chain1 one_chain2)"
    "boundary_chain one_chain1"
    "boundary_chain one_chain2"
    "\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>"
    "finite one_chain1"
    "finite one_chain2"
    "finite basis"
  shows "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2"
    "\<forall>(k, \<gamma>)\<in>one_chain2. line_integral_exists F basis \<gamma>"
proof -
  obtain ps1 ps2 where gen_subdiv: "(common_boundary_sudivision_exists (one_chain1 - ps1) (one_chain2 - ps2))" "(\<forall>(k, \<gamma>)\<in>ps1. point_path \<gamma>)" " (\<forall>(k, \<gamma>)\<in>ps2. point_path \<gamma>)"
    using assms(1) gen_common_subdiv_imp_common_subdiv
    by blast
  show "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2"
    using one_chain_line_integral_point_paths gen_common_subdiv_imp_common_subdiv
      assms(2-7) gen_subdiv
      common_subdivision_imp_eq_line_integral(1)[OF gen_subdiv(1) boundary_chain_diff[OF assms(2)] boundary_chain_diff[OF assms(3)]]
    by auto
  show "\<forall>(k, \<gamma>)\<in>one_chain2. line_integral_exists F basis \<gamma>"
  proof-
    obtain subdiv where subdiv_props:
      "chain_subdiv_chain (one_chain1-ps1) subdiv"
      "chain_subdiv_chain (one_chain2-ps2) subdiv"
      "(\<forall>(k, \<gamma>) \<in> subdiv. valid_path \<gamma>)"
      "(boundary_chain subdiv)"
      using gen_subdiv(1)
      by (auto simp add: common_boundary_sudivision_exists_def)
    have "\<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F basis \<gamma>"
      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: "\<forall>(k, \<gamma>)\<in>one_chain2-ps2. line_integral_exists F basis \<gamma>"
      using one_chain_line_integral_eq_line_integral_on_sudivision(2)[OF subdiv_props(2) boundary_chain_diff[OF assms(3)] subdiv_props(4)] subdiv_props(3) assms(6) assms(7)
      by blast
    then show ?thesis
      using  gen_subdiv(3) line_integral_exists_point_path[OF assms(7)]
      by blast
  qed      
qed

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

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

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

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

(*path reparam_weaketrization*)

definition reparam_weak where
  "reparam_weak \<gamma>1 \<gamma>2 \<equiv> \<exists>\<phi>. (\<forall>x\<in>{0..1}. \<gamma>1 x = (\<gamma>2 o \<phi>) x) \<and> \<phi> piecewise_C1_differentiable_on {0..1} \<and> \<phi>(0) = 0 \<and> \<phi>(1) = 1 \<and> \<phi> ` {0..1} = {0..1}"

definition reparam where
  "reparam \<gamma>1 \<gamma>2 \<equiv> \<exists>\<phi>. (\<forall>x\<in>{0..1}. \<gamma>1 x = (\<gamma>2 o \<phi>) x) \<and> \<phi> piecewise_C1_differentiable_on {0..1} \<and> \<phi>(0) = 0 \<and> \<phi>(1) = 1 \<and> bij_betw \<phi> {0..1} {0..1} \<and> \<phi> -` {0..1} \<subseteq> {0..1} \<and> (\<forall>x\<in>{0..1}. finite (\<phi> -` {x}))"

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

lemma line_integral_exists_smooth_one_base:
  assumes "\<gamma> 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 \<gamma>) (\<lambda>x. F x \<bullet> b)"
  shows "line_integral_exists F {b} \<gamma>"
proof-
  have gamma2_differentiable: "(\<forall>x \<in> {0 .. 1}. \<gamma> differentiable at x)"
    using assms(1) 
    by (auto simp add: valid_path_def C1_differentiable_on_eq)
  then have gamma2_b_component_differentiable: "(\<forall>x \<in> {0 .. 1}. (\<lambda>x. (\<gamma> x) \<bullet> b) differentiable at x)"
    by auto
  then have "(\<lambda>x. (\<gamma> x) \<bullet> 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} (\<lambda>x. (\<gamma> x) \<bullet> b)"
    using differentiable_imp_continuous_on
    by auto
  have gamma2_cont:"continuous_on {0..1} \<gamma>"
    using assms(1) C1_differentiable_imp_continuous_on
    by (auto simp add: valid_path_def)
  have iii: "continuous_on {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))"
  proof-
    have 0: "continuous_on {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> b)"
      using assms(2) continuous_on_compose[OF gamma2_cont]
      by (auto simp add: path_image_def) 
    obtain D where D: "(\<forall>x\<in>{0..1}. (\<gamma> has_vector_derivative D x) (at x)) \<and> continuous_on {0..1} D"
      using assms(1)
      by (auto simp add: C1_differentiable_on_def)
    then have *:"\<forall>x\<in>{0..1}. vector_derivative \<gamma> (at x within{0..1}) = D x"
      using vector_derivative_at vector_derivative_at_within_ivl
      by fastforce
    then have "continuous_on {0..1} (\<lambda>x. vector_derivative \<gamma> (at x within{0..1}))"
      using continuous_on_eq D by force
    then have 1: "continuous_on {0..1} (\<lambda>x. (vector_derivative \<gamma> (at x within{0..1})) \<bullet> b)"
      by(auto intro!: continuous_intros)
    show ?thesis
      using continuous_on_mult[OF 0 1]  by auto
  qed
  then have "(\<lambda>x. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) integrable_on {0..1}"
    using integrable_continuous_real
    by auto
  then show "line_integral_exists F {b} \<gamma>"
    by(auto simp add: line_integral_exists_def)
qed

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

lemma line_integral_primitive_lemma: (*Only for real normed fields, i.e. vectors with products*)
  fixes f :: "'a::{euclidean_space,real_normed_field} \<Rightarrow> 'a::{euclidean_space,real_normed_field}" and
        g :: "real \<Rightarrow> 'a"
  assumes "\<And>(a::'a). a \<in> s \<Longrightarrow> (f has_field_derivative (f' a)) (at a within s)"
      and "g piecewise_differentiable_on {0::real..1}"  "\<And>x. x \<in> {0..1} \<Longrightarrow> g x \<in> s"
      and "base_vec \<in> Basis"
    shows "((\<lambda>x. ((f'(g x)) * (vector_derivative g (at x within {0..1}))) \<bullet> base_vec)
             has_integral (((f(g 1)) \<bullet> base_vec - (f(g 0)) \<bullet> base_vec))) {0..1}"
proof -
  obtain k where k: "finite k" "\<forall>x\<in>{0..1} - k. g differentiable (at x within {0..1})" and cg: "continuous_on {0..1} g"
    using assms by (auto simp: piecewise_differentiable_on_def)
  have cfg: "continuous_on {0..1} (\<lambda>x. f (g x))"
    apply (rule continuous_on_compose [OF cg, unfolded o_def])
    using assms
    apply (metis field_differentiable_def field_differentiable_imp_continuous_at continuous_on_eq_continuous_within continuous_on_subset image_subset_iff)
    done
  { fix x::real
    assume a: "0 < x" and b: "x < 1" and xk: "x \<notin> 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 (\<lambda>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 "((\<lambda>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 *: "\<And>x. x\<in>{0<..<1} - k \<Longrightarrow> ((\<lambda>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 "((\<lambda>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 "((\<lambda>x. (((f'(g x))) * ((vector_derivative g (at x within {0..1})))) \<bullet> base_vec)
             has_integral (((f(g 1)) - (f(g 0)))) \<bullet> 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 \<gamma>1 \<gamma>2" and
    pw_smooth: "\<gamma>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 \<gamma>2) (\<lambda>x. F x \<bullet> b)" and
    line_integral_ex: "line_integral_exists F {b} \<gamma>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} \<gamma>1 = line_integral F {b} \<gamma>2"
    "line_integral_exists F {b} \<gamma>1"
proof-
  obtain \<phi> where phi: "(\<forall>x\<in>{0..1}. \<gamma>1 x = (\<gamma>2 o \<phi>) x)"" \<phi> piecewise_C1_differentiable_on {0..1}"" \<phi>(0) = 0"" \<phi>(1) = 1""bij_betw \<phi> {0..1} {0..1}" "\<phi> -` {0..1} \<subseteq> {0..1}" "\<forall>x\<in>{0..1}. finite (\<phi> -` {x})"
    using reparam
    by (auto simp add: reparam_def)
  obtain s where s: "finite s" "\<phi> C1_differentiable_on {0..1} - s"
    using phi
    by(auto simp add: reparam_def piecewise_C1_differentiable_on_def)
  let ?s = "s \<inter> {0..1}"
  have s_inter: "finite ?s" "\<phi> 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} \<phi>"
    using phi
    by(auto simp add: reparam_def piecewise_C1_differentiable_on_imp_continuous_on)
  obtain s' D where s'_D: "finite s'" "(\<forall>x \<in> {0 .. 1} - s'. \<gamma>2 differentiable at x)" "(\<forall>x\<in>{0..1} - s'. (\<gamma>2 has_vector_derivative D x) (at x)) \<and> 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' \<inter> {0..1}"
  have gamma2_differentiable: "finite ?s'" "(\<forall>x \<in> {0 .. 1} - ?s'. \<gamma>2 differentiable at x)" "(\<forall>x\<in>{0..1} - ?s'. (\<gamma>2 has_vector_derivative D x) (at x)) \<and> 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: "(\<forall>x \<in> {0 .. 1} - ?s'. (\<lambda>x. (\<gamma>2 x) \<bullet> b) differentiable at x)"
    using differentiable_inner by force
  then have "(\<lambda>x. (\<gamma>2 x) \<bullet> 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') (\<lambda>x. (\<gamma>2 x) \<bullet> b)"
    using differentiable_imp_continuous_on
    by auto
      (**********Additional needed assumptions ************)
  have s_in01: "?s \<subseteq> {0..1}" by auto
  have s'_in01: "?s' \<subseteq> {0..1}" by auto
  have phi_backimg_s': "\<phi> -` {0..1} \<subseteq> {0..1}" using phi by auto
  have "inj_on \<phi> {0..1}" using phi(5) by (auto simp add: bij_betw_def)
  have bij_phi: "bij_betw \<phi> {0..1} {0..1}" using phi(5) by auto
  have finite_bck_img_single: "\<forall>x\<in>{0..1}. finite (\<phi> -` {x})" using phi by auto
  then have finite_bck_img_single_s': " \<forall>x\<in>?s'. finite (\<phi> -` {x})" by auto
  have gamma2_line_integrable: "(\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b)) integrable_on {0..1}"
    using line_integral_ex
    by (simp add: line_integral_exists_def)
      (****************************************************************)
  have finite_neg_img: "finite (\<phi> -` ?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') \<gamma>2"
    using  gamma2_differentiable
    by (meson continuous_at_imp_continuous_on differentiable_imp_continuous_within)
  have iii: "continuous_on ({0..1} - ?s') (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))"
  proof-
    have 0: "continuous_on ({0..1} - ?s') (\<lambda>x. F (\<gamma>2 x) \<bullet> b)"
      using cont continuous_on_compose[OF gamma2_cont] continuous_on_compose2 gamma2_cont
      unfolding path_image_def  by fastforce
    have D: "(\<forall>x\<in>{0..1} - ?s'. (\<gamma>2 has_vector_derivative D x) (at x)) \<and> continuous_on ({0..1} - ?s') D"
      using gamma2_differentiable
      by auto                       
    then have *:"\<forall>x\<in>{0..1} - ?s'. vector_derivative \<gamma>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') (\<lambda>x. vector_derivative \<gamma>2 (at x within{0..1}))"
      using continuous_on_eq D
      by metis
    then have 1: "continuous_on ({0..1} - ?s') (\<lambda>x. (vector_derivative \<gamma>2 (at x within{0..1})) \<bullet> b)"
      by (auto intro!: continuous_intros)
    show ?thesis
      using continuous_on_mult[OF 0 1]
      by auto
  qed
  have iv: "\<phi>(0) \<le> \<phi>(1)"
    using phi(3) phi(4)
    by (simp add: reparam_def)
  have v: "\<phi>`{0..1} \<subseteq> {0..1}"
    using phi
    by (auto simp add: reparam_def bij_betw_def)
  obtain D where D_props: "(\<forall>x\<in>{0..1} - ?s. (\<phi> has_vector_derivative D x) (at x))"
    using s
    by (auto simp add: C1_differentiable_on_def)
  then have "(\<And>x. x \<in> ({0..1} - ?s) \<Longrightarrow> (\<phi> has_vector_derivative D x) (at x within {0..1}))"
    using has_vector_derivative_at_within
    by blast
  then have vi: "(\<And>x. x \<in> ({0..1} - ?s) \<Longrightarrow> (\<phi> has_real_derivative D x) (at x within {0..1}))"
    using has_real_derivative_iff_has_vector_derivative
    by blast
  have a:"((\<lambda>x. D x * (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> 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 a: "integral {\<phi> 1..\<phi> 0} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b)) = 0" using integral_singleton integral_empty iv
      by (simp add: phi(3) phi(4))
    have b: "((\<lambda>x. D x *\<^sub>R (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> 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)) - integral {\<phi> 1..\<phi> 0} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> 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} \<phi>"
        using bij_phi
        by (metis (full_types) bij_betw_def image_subsetI rangeI)
      then show "surj_on ?s' \<phi>" using bij_phi s'_in01
        by blast
      show "inj_on \<phi> ({0..1} \<union> (?s \<union> \<phi> -` ?s'))"
      proof-
        have i: "inj_on \<phi> {0..1}" using  bij_phi 
          using bij_betw_def by blast
        have ii: "({0..1} \<union> (?s \<union> \<phi> -` ?s')) = {0..1}" using phi_backimg_s' s_in01 s'_in01
          by blast
        show ?thesis using i ii by auto
      qed
      show "\<And>x. x \<in> {0..1} - ?s \<Longrightarrow> (\<phi> 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} (\<lambda>x. D x * (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b))) = 
                       integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))"
    by auto
  have gamma2_vec_diffable: "\<And>x::real. x \<in> {0..1} - ((\<phi> -` ?s') \<union> ?s) \<Longrightarrow> ((\<gamma>2 o \<phi>) has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x)) (at x)"
  proof-
    fix x::real 
    assume ass: "x \<in> {0..1} -   ((\<phi> -` ?s') \<union> ?s)"
    have zer_le_x_le_1:"0\<le> x \<and> x \<le> 1" using ass
      by simp
    show "((\<gamma>2 o \<phi>) has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x)) (at x)"
    proof-
      have **: "\<gamma>2 differentiable at (\<phi> x)"
        using  gamma2_differentiable(2) ass v 
        by blast
      have ***: " \<phi> differentiable at x"
        using s ass
        by (auto simp add: C1_differentiable_on_eq)
      then show "((\<gamma>2 o \<phi>) has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x)) (at x)"
        using differentiable_chain_at[OF *** **] 
        by (auto simp add: vector_derivative_works)
    qed
  qed
  then have gamma2_vec_deriv_within: "\<And>x::real. x \<in> {0..1} - ((\<phi> -` ?s') \<union> ?s) \<Longrightarrow> vector_derivative (\<gamma>2 \<circ> \<phi>) (at x) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1})"
    using vector_derivative_at_within_ivl[OF gamma2_vec_diffable]
    by auto
  have "\<forall>x\<in>{0..1} - ((\<phi> -` ?s') \<union> ?s). 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)"
  proof
    fix x::real
    assume ass: "x \<in> {0..1} -((\<phi> -` ?s') \<union> ?s)"
    then have 0: "\<phi> differentiable (at x)"
      using s by (auto simp add: C1_differentiable_on_def differentiable_def has_vector_derivative_def)
    obtain D2 where "(\<phi> has_vector_derivative D2) (at x)"
      using D_props ass  by blast
    have "\<phi> x \<in> {0..1} - ?s'"
      using phi(5) ass by (metis Diff_Un Diff_iff Int_iff bij_betw_def image_eqI vimageI)
    then have 1: "\<gamma>2 differentiable (at (\<phi> x))"
      using gamma2_differentiable
      by auto
    have 3:" vector_derivative \<gamma>2 (at (\<phi> x)) =  vector_derivative \<gamma>2 (at (\<phi> x) within {0..1})"
    proof-
      have *:"0\<le> \<phi> x \<and> \<phi> x \<le> 1" using phi(5) ass
        using \<open>\<phi> x \<in> {0..1} - s' \<inter> {0..1}\<close> 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:"(\<gamma>1 has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (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 \<le> x" "x \<le> 1" using ass by auto
        have 0: "vector_derivative \<gamma>1 (at x within {0..1}) = vector_derivative (\<gamma>2 \<circ> \<phi>) (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 (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) = vector_derivative (\<gamma>2 \<circ> \<phi>) (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 (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) = vector_derivative \<gamma>1 (at x within {0..1})"
          using 0 1 by auto
        then show "vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b = vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b" by auto
      qed
      then have i: "\<forall>x\<in>{0..1} - ( ((\<phi> -` ?s') \<union> ?s)\<union>{0,1}). (vector_derivative  (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b) = (vector_derivative  (\<gamma>1) (at x within {0..1}) \<bullet> b)"
        by auto
      have ii: "\<forall>x\<in>{0..1} - (((\<phi> -` ?s') \<union> ?s)\<union>{0,1}).  F (\<gamma>1 x) \<bullet> b =  F (\<gamma>2 (\<phi> x)) \<bullet> b"
        using phi(1)
        by auto
      show ?thesis 
        using i ii  by metis
    qed
    have **: "negligible ((\<phi> -` ?s') \<union> ?s \<union> {0, 1})" using s(1) finite_neg_img by auto
    have has_integral_spike_eq': "\<And>s t g f 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 has_integral_spike_eq'[OF ** *] ass
      by blast
  qed
  then show "line_integral_exists F {b} \<gamma>1"
    using phi  by(auto simp add: line_integral_exists_def)
  have "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)) =
                      integral ({0..1}) (\<lambda>x. F (\<gamma>1 x) \<bullet> b * (vector_derivative \<gamma>1  (at x within {0..1}) \<bullet> b))"
    using integral_unique[OF e] integral_unique[OF f]
    by metis
  moreover have "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)) =
                         integral ({0..1}) (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))"
    using b d phi by (auto simp add:)
  ultimately show "line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2"
    using phi  by(auto simp add: line_integral_def)
qed

lemma reparam_weak_eq_line_integrals:
  assumes "reparam_weak \<gamma>1 \<gamma>2"
    "\<gamma>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 \<gamma>2) (\<lambda>x. F x \<bullet> b)"
  shows "line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2"
    "line_integral_exists F {b} \<gamma>1"
proof-
  obtain \<phi> where phi: "(\<forall>x\<in>{0..1}. \<gamma>1 x = (\<gamma>2 o \<phi>) x)"" \<phi> piecewise_C1_differentiable_on {0..1}"" \<phi>(0) = 0"" \<phi>(1) = 1"" \<phi> ` {0..1} = {0..1}"
    using assms(1)
    by (auto simp add: reparam_weak_def)
  obtain s where s: "finite s" "\<phi> 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} \<phi>"
    using phi
    by(auto simp add: reparam_weak_def piecewise_C1_differentiable_on_imp_continuous_on)
  have gamma2_differentiable: "(\<forall>x \<in> {0 .. 1}. \<gamma>2 differentiable at x)"
    using assms(2) 
    by (auto simp add: valid_path_def C1_differentiable_on_eq)
  then have gamma2_b_component_differentiable: "(\<forall>x \<in> {0 .. 1}. (\<lambda>x. (\<gamma>2 x) \<bullet> b) differentiable at x)"
    by auto
  then have "(\<lambda>x. (\<gamma>2 x) \<bullet> 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} (\<lambda>x. (\<gamma>2 x) \<bullet> b)"
    using differentiable_imp_continuous_on
    by auto
  have gamma2_cont:"continuous_on {0..1} \<gamma>2"
    using assms(2) C1_differentiable_imp_continuous_on
    by (auto simp add: valid_path_def)
  have iii: "continuous_on {0..1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))"
  proof-
    have 0: "continuous_on {0..1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b)"
      using assms(3) continuous_on_compose[OF gamma2_cont]
      by (auto simp add: path_image_def) 
    obtain D where D: "(\<forall>x\<in>{0..1}. (\<gamma>2 has_vector_derivative D x) (at x)) \<and> continuous_on {0..1} D"
      using assms(2)  by (auto simp add: C1_differentiable_on_def)
    then have *:"\<forall>x\<in>{0..1}. vector_derivative \<gamma>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} (\<lambda>x. vector_derivative \<gamma>2 (at x within{0..1}))"
      using continuous_on_eq D  by force
    then have 1: "continuous_on {0..1} (\<lambda>x. (vector_derivative \<gamma>2 (at x within{0..1})) \<bullet> b)"
      by (auto intro!: continuous_intros)
    show ?thesis
      using continuous_on_mult[OF 0 1]  by auto
  qed
  have iv: "\<phi>(0) \<le> \<phi>(1)"
    using phi(3) phi(4)  by (simp add: reparam_weak_def)
  have v: "\<phi>`{0..1} \<subseteq> {0..1}"
    using phi(5)  by (simp add: reparam_weak_def)
  obtain D where D_props: "(\<forall>x\<in>{0..1} - s. (\<phi> has_vector_derivative D x) (at x))"
    using s
    by (auto simp add: C1_differentiable_on_def)
  then have "(\<And>x. x \<in> ({0..1} -s) \<Longrightarrow> (\<phi> has_vector_derivative D x) (at x within {0..1}))"
    using has_vector_derivative_at_within  by blast
  then have vi: "(\<And>x. x \<in> ({0..1} - s) \<Longrightarrow> (\<phi> has_real_derivative D x) (at x within {0..1}))"
    using has_real_derivative_iff_has_vector_derivative
    by blast
  have a:"((\<lambda>x. D x * (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> 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}"
    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} (\<lambda>x. D x * (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b))) = 
                       integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))"
    by auto
  have gamma2_vec_diffable: "\<And>x::real. x \<in> {0..1} -s \<Longrightarrow> ((\<gamma>2 o \<phi>) has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x)) (at x)"
  proof-
    fix x::real 
    assume ass: "x \<in> {0..1} -s"
    have zer_le_x_le_1:"0\<le> x \<and> x \<le> 1" using ass by auto
    show "((\<gamma>2 o \<phi>) has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x)) (at x)"
    proof-
      have **: "\<gamma>2 differentiable at (\<phi> x)"
        using phi gamma2_differentiable
        by (auto simp add: zer_le_x_le_1)
      have ***: " \<phi> differentiable at x"
        using s ass
        by (auto simp add: C1_differentiable_on_eq)
      then show "((\<gamma>2 o \<phi>) has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x)) (at x)"
        using differentiable_chain_at[OF *** **] 
        by (auto simp add: vector_derivative_works)
    qed
  qed
  then have gamma2_vec_deriv_within: "\<And>x::real. x \<in> {0..1} -s \<Longrightarrow> vector_derivative (\<gamma>2 \<circ> \<phi>) (at x) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1})"
    using vector_derivative_at_within_ivl[OF gamma2_vec_diffable]
    by auto
  have "\<forall>x\<in>{0..1} - s. 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)"
  proof
    fix x::real
    assume ass: "x \<in> {0..1} -s"
    then have 0: "\<phi> differentiable (at x)"
      using s
      by (auto simp add: C1_differentiable_on_def differentiable_def has_vector_derivative_def)
    obtain D2 where "(\<phi> has_vector_derivative D2) (at x)"
      using D_props ass
      by blast
    have "\<phi> x \<in> {0..1}"
      using phi(5) ass 
      by (auto simp add: reparam_weak_def)
    then have 1: "\<gamma>2 differentiable (at (\<phi> x))"
      using gamma2_differentiable
      by auto
    have 3:" vector_derivative \<gamma>2 (at (\<phi> x)) =  vector_derivative \<gamma>2 (at (\<phi> x) within {0..1})"
    proof-
      have *:"0\<le> \<phi> x \<and> \<phi> x \<le> 1" using phi(5) ass 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} -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 s" using 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
    by(auto simp add:)
  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 0:"negligible s" using s(1) by auto
    have c':"\<forall> x\<in> {0..1} -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 auto
    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} - (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} - 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} - s)" using open_diff s open_greaterThanLessThan by blast
        have ii: "\<forall>x\<in>{0<..<1::real} - s. (\<gamma>2 \<circ> \<phi>) x = \<gamma>1 x" using phi(1)
          by auto                              
        fix x::real
        assume ass: " x \<in> {0<..<1::real} - s"
        then have iii: "(\<gamma>2 \<circ> \<phi> has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (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:"(\<gamma>1 has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (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 \<le> x" "x \<le> 1" using ass by auto
        have 0: "vector_derivative \<gamma>1 (at x within {0..1}) = vector_derivative (\<gamma>2 \<circ> \<phi>) (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 (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) = vector_derivative (\<gamma>2 \<circ> \<phi>) (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 (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) = vector_derivative \<gamma>1 (at x within {0..1})"
          using 0 1 by auto
        then show "vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b = vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b" by auto
      qed
      then have i: "\<forall>x\<in>{0..1} - (s\<union>{0,1}). (vector_derivative  (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b) = (vector_derivative  (\<gamma>1) (at x within {0..1}) \<bullet> b)"
        by auto
      have ii: "\<forall>x\<in>{0..1} - (s\<union>{0,1}).  F (\<gamma>1 x) \<bullet> b =  F (\<gamma>2 (\<phi> x)) \<bullet> b"
        using phi(1)  by auto
      show ?thesis 
        using i ii by auto
    qed
    have **: "negligible (s\<union>{0,1})" using s(1) by auto
    have has_integral_spike_eq': "\<And>s t g f 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 has_integral_spike_eq'[OF ** *] ass
      by blast
  qed
  then show "line_integral_exists F {b} \<gamma>1"
    using phi  by(auto simp add: line_integral_exists_def)
  have "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)) =
                      integral ({0..1}) (\<lambda>x. F (\<gamma>1 x) \<bullet> b * (vector_derivative \<gamma>1  (at x within {0..1}) \<bullet> b))"
    using integral_unique[OF e] integral_unique[OF f]
    by metis
  moreover have "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)) =
                         integral ({0..1}) (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))"
    using b d phi  by (auto simp add:)
  ultimately show "line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2"
    using phi by(auto simp add: line_integral_def)
qed

lemma line_integral_sum_basis:
  assumes "finite (basis::('a::euclidean_space) set)"  "\<forall>b\<in>basis. line_integral_exists F {b} \<gamma>"
  shows "line_integral F basis \<gamma> = (\<Sum>b\<in>basis. line_integral F {b} \<gamma>)"
        "line_integral_exists F basis \<gamma>"
  using assms
proof(induction basis)
  show "line_integral F {} \<gamma> = (\<Sum>b\<in>{}. line_integral F {b} \<gamma>)"
    by(auto simp add: line_integral_def)
  show "\<forall>b\<in>{}. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F {} \<gamma>"
    by(simp add: line_integral_exists_def integrable_0)
next
  fix basis::"('a::euclidean_space) set"
  fix x::"'a::euclidean_space"
  fix  \<gamma>
  assume ind_hyp: "(\<forall>b\<in>basis. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F basis \<gamma>)"
    "(\<forall>b\<in>basis. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral F basis \<gamma> = (\<Sum>b\<in>basis. line_integral F {b} \<gamma>))"
  assume step: "finite basis"
    "x \<notin> basis"
    "\<forall>b\<in>insert x basis. line_integral_exists F {b} \<gamma>"
  then have 0: "line_integral_exists F {x} \<gamma>" by auto
  have 1:"line_integral_exists F basis \<gamma>"
    using ind_hyp step by auto
  then show "line_integral_exists F (insert x basis) \<gamma>"
    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 \<gamma> = (\<Sum>b\<in>basis. line_integral F {b} \<gamma>)"
    using ind_hyp step by auto
  then show "line_integral F (insert x basis) \<gamma> = (\<Sum>b\<in>insert x basis. line_integral F {b} \<gamma>)"
    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 \<gamma>1 \<gamma>2"
    "\<gamma>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*)
    "\<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)"
    "finite basis"
  shows "line_integral F basis \<gamma>1 = line_integral F basis \<gamma>2"
    "line_integral_exists F basis \<gamma>1"
proof- 
  show "line_integral_exists F basis \<gamma>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 \<gamma>1 = line_integral F basis \<gamma>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 \<gamma>1 \<gamma>2"
    "\<gamma>2 piecewise_C1_differentiable_on {0..1}" 
    "\<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)"
    "finite basis"
    "\<forall>b\<in>basis. line_integral_exists F {b} \<gamma>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 \<gamma>1 = line_integral F basis \<gamma>2"
    "line_integral_exists F basis \<gamma>1"
proof- 
  show "line_integral_exists F basis \<gamma>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 \<gamma>1 = line_integral F basis \<gamma>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 "\<gamma> C1_differentiable_on {0..1}" (*To generalise this to valid_path we need a version of has_integral_substitution_strong that allows finite discontinuities*)
    "\<forall>(b::'a::euclidean_space) \<in>basis. continuous_on (path_image \<gamma>) (\<lambda>x. F x \<bullet> b)"
    "finite basis"
  shows "line_integral_exists F basis \<gamma>"
  using reparam_weak_eq_line_integrals_basis(2)[OF reparam_weak_eq_refl[where ?\<gamma>1.0 = \<gamma>]] 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 "\<lambda>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 \<equiv>
      \<exists>f. bij f \<and> f ` one_chain1 = one_chain2 \<and> (\<forall>(k,\<gamma>)\<in>one_chain1. if k = fst (f(k,\<gamma>)) then reparam_weak \<gamma> (snd (f(k,\<gamma>))) else reparam_weak \<gamma> (reversepath (snd (f(k,\<gamma>)))))"

lemma chain_reparam_weak_chain_line_integral:
  assumes "chain_reparam_weak_chain one_chain1 one_chain2"
    "\<forall>(k2,\<gamma>2)\<in>one_chain2. \<gamma>2 C1_differentiable_on {0..1}"
    "\<forall>(k2,\<gamma>2)\<in>one_chain2.\<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> 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"
    "\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>"
proof-
  obtain f where f: "bij f"
    "(\<forall>(k,\<gamma>)\<in>one_chain1. if k = fst (f(k,\<gamma>)) then reparam_weak \<gamma> (snd (f(k,\<gamma>))) else reparam_weak \<gamma> (reversepath (snd (f(k,\<gamma>)))))"
    "f ` one_chain1 = one_chain2"
    using assms(1)
    by (auto simp add: chain_reparam_weak_chain_def)
  have 0:" \<forall>x\<in>one_chain1. (case x of (k, \<gamma>) \<Rightarrow> (real_of_int k * line_integral F basis \<gamma>) = (case f x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma>) \<and>
                                                        line_integral_exists F basis \<gamma>)"
  proof
    {fix k1 \<gamma>1
      assume ass1: "(k1,\<gamma>1) \<in>one_chain1"
      have "real_of_int k1 * line_integral F basis \<gamma>1 = (case (f (k1,\<gamma>1)) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and>
                      line_integral_exists F basis \<gamma>1"
      proof(cases)
        assume ass2: "k1 = 1"
        let ?k2 = "fst (f (k1, \<gamma>1))"
        let ?\<gamma>2 = "snd (f (k1, \<gamma>1))"
        have "real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int ?k2 * line_integral F basis ?\<gamma>2\<and>
                              line_integral_exists F basis \<gamma>1"
        proof(cases)
          assume ass3: "?k2 = 1"
          then have 0: "reparam_weak \<gamma>1 ?\<gamma>2"
            using ass1 ass2 f(2)
            by auto
          have 1: "?\<gamma>2 C1_differentiable_on {0..1}"
            using f(3) assms(2) ass1
            by force
          have 2: "\<forall>b\<in>basis. continuous_on (path_image ?\<gamma>2) (\<lambda>x. F x \<bullet> b)"
            using f(3) assms(3) ass1
            by force
          show "real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int ?k2 * line_integral F basis ?\<gamma>2 \<and>
                                     line_integral_exists F basis \<gamma>1"
            using assms reparam_weak_eq_line_integrals_basis[OF 0 1 2 assms(4)]
              ass2 ass3
            by auto
        next
          assume "?k2 \<noteq> 1"
          then have ass3: "?k2 = -1"
            using bound2 ass1 f(3) unfolding boundary_chain_def by force
          then have 0: "reparam_weak \<gamma>1 (reversepath ?\<gamma>2)"
            using ass1 ass2 f(2)
            by auto
          have 1: "(reversepath ?\<gamma>2) C1_differentiable_on {0..1}"
            using f(3) assms(2) ass1 smooth_path_imp_reverse
            by force
          have 2: "\<forall>b\<in>basis. continuous_on (path_image (reversepath ?\<gamma>2)) (\<lambda>x. F x \<bullet> 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 ?γot : HL-CSP_pSm - Operational semantics fo HL-SP
          proof-
            have i:"java.lang.StringIndexOutOfBoundsException: Range [31, 30) out of bounds for length 57
              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 yorce
          qed
          show "real_of_int k1 * line_integral F basis γ2 ∧
                                     line_integra_eit ai <>"
            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')
      java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
    }
    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)

    show ?thesis
      using ass path_image_reversepath b_l path_image_join
      by(fastforce simp 
  qed
  then showhaveubset_initials
    using to
qed

lemma unfoldingrefine_def
  fixes l
  shows "l ≠(k, γ set l. path_image γ)"
java.lang.StringIndexOutOfBoundsException: Range [13, 5) out of bounds for length 18
  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 sengous_on_closed_Und_Und_Unionion
    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"
   uous_on_on (∪ snd) ` one_chain))  (λx. F x ∙
      apply(rule ntinuous_on_closed_UN?  (agee nd  _chainain ]
    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 "∀<gamma>)∈gamma>" 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)"
          show \<open<><checkmark>(r) ∈ P⁰ ==> P ⊑_FD SKIP r›
          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' = {}) ∧
java.lang.StringIndexOutOfBoundsException: Index 4 out of bounds for length 4

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: "ain_line_integralsisv ne_integral is(f ` one_chain1))"
    by auto
  {fix k γ
    assume ass:"(k, γ) ∈P  java.lang.StringIndexOutOfBoundsException: Range [91, 90) out of bounds for length 172
    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
      (∃ (λl. range 🚫(r) ∈ P⁰}. Q⁰))›
      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 iishow ‹ ==>bo>; Q)⁰ = UNIV› by simp
        by auto
      have "valid_path (reversepath \<gamma>)"
        using f_props(1) ass assms  by auto
      then have "line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = - (line_integral F basis \<gamma>)"
        using line_integral_on_reverse_path reversepath_reversepath x ass
        by metis
      then show "line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k::int, \<gamma>)) = k * line_integral F basis \<gamma>"
        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: "\<forall>(k, \<gamma>) \<in> one_chain1. line_integral_exists F basis \<gamma>"
    using cube_line_integ by auto
  have 1: "one_chain_line_integral F basis (\<Union>(f ` one_chain1)) = one_chain_line_integral F basis one_chain1"
  proof -
    have 0:"one_chain_line_integral F basis (\<Union>(f ` one_chain1)) = 
                           (\<Sum>one_chain \<in> (f ` one_chain1). one_chain_line_integral F basis one_chain)"
    proof -
      have finite: "\<forall>chain \<in> (f ` one_chain1). finite chain"
        using f_props(1) finite_chain2 
        by (meson Sup_upper finite_subset)
      have disj: " \<forall>A\<in>f ` one_chain1. \<forall>B\<in>f ` one_chain1. A \<noteq> B \<longrightarrow> A \<inter> B = {}"
        apply(simp add:image_def)
        using f_props(3)
        by metis
      show "one_chain_line_integral F basis (\<Union>(f ` one_chain1)) = 
                                (Sum>one_chain \<in> (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:"(\Sumone_chain \<in> (f ` one_chain1). one_chain_line_integral F basis one_chain) = 
                            one_chain_line_integral F basis one_chain1"
    proof -
      have "(\<Sum>one_chain \<in> (f ` one_chain1). one_chain_line_integral F basis one_chain) = 
                                     (\<Sum>(k,\<gamma>)\<in>one_chain1. k*(line_integral F basis \<gamma>))"
      proof -
        have i:"(\<Sum>one_chain \<in> (f ` (one_chain1 - {p. f p = {}})). one_chain_line_integral F basis one_chain) = 
                                       (\<Sum>(k,\<gamma>)\<in>one_chain1 - {p. f p = {}}. k*(line_integral F basis \<gamma>))"
        proof -
          have "inj_on f (one_chain1 - {p. f p = {}})"
            unfolding inj_on_def
            using f_props(3) by force
          then have 0: "(\<Sum>one_chain \<in> (f ` (one_chain1 - {p. f p = {}})). one_chain_line_integral F basis one_chain)
                                                       = (\<Sum>(k, \<gamma>) \<in> (one_chain1 - {p. f p = {}}). one_chain_line_integral F basis (f (k, \<gamma>)))"
            using Groups_Big.comm_monoid_add_class.sum.reindex
            by auto
          have "\<And> k \<gamma>. (k, \<gamma>) \<in> (one_chain1 - {p. f p = {}}) \<Longrightarrow>
                                                     one_chain_line_integral F basis (f(k, \<gamma>)) = k* (line_integral F basis \<gamma>)"
            using cube_line_integ by auto
          then have "(\<Sum>(k, \<gamma>) \<in> (one_chain1 - {p. f p = {}}). one_chain_line_integral F basis (f (k, \<gamma>)))
                   = (\<Sum>(k, \<gamma>) \<in> (one_chain1 - {p. f p = {}}). k* (line_integral F basis \<gamma>))"
            by (auto intro!: Finite_Cartesian_Product.sum_cong_aux)
          then show "(\<Sum>one_chain \<in> (f ` (one_chain1 - {p. f p = {}})). one_chain_line_integral F basis one_chain) =
                                                     (\<Sum>(k, \<gamma>) \<in> (one_chain1 - {p. f p = {}}). k* (line_integral F basis \<gamma>))"
            using 0  by auto
        qed
        have "\<And> (k::int) \<gamma>. (k, \<gamma>) \<in> one_chain1 \<Longrightarrow> (f (k, \<gamma>) = {}) \<Longrightarrow> (k, \<gamma>) \<in> {(k',\<gamma>'). k'* (line_integral F basis \<gamma>') = 0}"
        proof-
          java.lang.StringIndexOutOfBoundsException: Index 15 out of bounds for length 15
          fix \<gamma>::"real\<Rightarrow>real*real"
          assume ass:"(k, \<gamma>) \<in> one_chain1"
            "(f (k, \<gamma>) = {})"
          then have zero_line_integral:"one_chain_line_integral F basis (f (k, \<gamma>)) = 0"
            using one_chain_line_integral_def
            by auto
          show "(k, \<gamma>) \<in> {(k'::int, \<gamma>'). k' * line_integral F basis \<gamma>' = 0}"
            using zero_line_integral cube_line_integ ass
            by force
        qed
        then have ii:"(\<Sum>one_chain \<in> (f ` (one_chain1 - {p. f p = {}})). one_chain_line_integral F basis one_chain) =
                                                          (\<Sum>one_chain \<in> (f ` (one_chain1)). one_chain_line_integral F basis one_chain)"
        proof -
          have "\<And>one_chain. one_chain \<in> (f ` (one_chain1)) - (f ` (one_chain1 - {p. f p = {}})) \<Longrightarrow>
                                                         one_chain_line_integral F basis one_chain = 0"
          proof -
            fix one_chain
            assume "one_chain \<in> (f ` (one_chain1)) - (f ` (one_chain1 - {p. f p = {}}))"
            java.lang.StringIndexOutOfBoundsException: Range [16, 14) out of bounds for length 160
              by auto
            then show "one_chain_line_integralF ischain "
              by utosimpadd ain_line_integral_def
          qed
          then hence \<open]\<in>T P \<or> [e] \<in> \<T> Q\<close> \<en<gek\nionv \<ejava.lang.StringIndexOutOfBoundsException: Index 119 out of bounds for length 119
                                                        "
            using Groups_Big.comm_monoid_add_class.sum.neutral
            by auto
          then have "(\      with <open> <n < <<]\<n <>Q\<close> have \<open>[e] \<in> \<T> (P \<lbrakk>S\<rbrakk> Q)\<close>
                                                      - (\<Sum>one_chain \<in> (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 "(\<Sum>one_chain \<in> (`n_in11{  }).ine_integral F basis one_chain) =
                                                          (\<Sum>one_chain \<in> (f `    java.lang.StringIndexOutOfBoundsException: Range [9, 8) out of bounds for length 158
            by auto
        qed
        have (k:) <amma <gamma> <n _chain1<Longrightarrow> ( , <amma>) = })<rightarrowf(,<amma)\in>{aine_chain_line_integralasisainn  }
        proof-
          fix k::"int"
          fix \<gamma"l<java.lang.StringIndexOutOfBoundsException: Range [42, 41) out of bounds for length 52
          assume ass:"(k, \<gamma>) \<in> one_chain1"  "(f (k, \<gamma>) = {})"
          then have "one_chain_line_integral F basis (f (k, \<gamma>)) = 0"
            using one_chain_line_integral_def
            by auto
          then show "f (k, \<gamma>) \<in> {p'. (one_chain_line_integral F basis p' = 0)}"
            by auto
        qed
        then have iii:"(\<Sum>(k::int,\<gamma>)\<in>one_chain1 - {p. f p = {}}. k*(line_integral F basis \<gamma>))
                                                 = (\<Sum>(k::int,\<gamma>)\<in>one_chain1. k*(line_integral F basis \<gamma>))"
        proof-
          have "\<And> k \<gamma>. (k,\<gamma>)\<in>one_chain1 - (one_chain1 - {p. f p = {}})
                                                    \<Longrightarrow> k* (line_integral F basis \<gamma>) = 0"
          proof-
            fix k \<gamma>
            assume ass: "(k,\<gamma>)\<in>one_chain1 - (one_chain1 - {p. f p = {}})"
            then have "f(k, \<gamma>) = {}"
              by auto
            then] \<otin> \<D> P\<close> by (simp add: BOT_iff_Nil_D)
              by (auto simp add:_line_integral_def
            then have zero_line_integral:"one_chain_line_integral F basis((,\gamma>)) = 0"
              using one_chain_line_integral_def
              o
            then show "k* (line_integral F basis \<gamma>) = 0"
              using zero_line_integral cube_line_integ ass
              by force
          qed
          then have "\<forall>k:t<gamma>)\<ine_chain1 _chain1   })
                       k*egral is<amma  " by auto
          <Sum>k::t,<amma\<in>_chain1 (_chain1 .  }) e_integraltegralFasis\<amma) =0
            java.lang.StringIndexOutOfBoundsException: Index 14 out of bounds for length 4
              [of "one_chain1 - (one_chain1 - {p. f p = {}}hence <open>tickFree  <nd[  e_hidet( )<lose
             mpd: it_beta
          thenassume sm:\open>\<n <>(  S)<close>
                                                    (\<Sum>(k::int,\<gamma>)\<in> (one_chain1 - {p. f p = {}}). k*(line_integral F basis \<gamma>))  = 0"
            using Groups_Big.sum_diff[OF finite_chain1]
            by (metis (no_types) Diff_subset \<open>(\<Sum>(k, \<gamma>)\<in>one_chain1 - (one_chain1 - {p. f p = {}}). k * line_integral F basis \<gamma>) = 0\<close> \<open>\<And>f B. B \<subseteq> one_chain1 \<Longrightarrow> sum f (one_chain1 - B) = sum f one_chain1 - sum f B\<close>)
          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"
    "\<forall>(k2,\<gamma>2)\<in>one_chain2. \<gamma>2 C1_differentiable_on {0..1}"
    "\<forall>b\<in>basis.\<forall>(k2,\<gamma>2)\<in>one_chain2. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)"
    "finite basis"                                                                     
    "finite one_chain1"
    "boundary_chain one_chain1"
    "hain2
    "\<forall>(\in>one_chain1. valid_path \<gamma>"
  shows "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2"
    "\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>"
proof-
  {fix b
    thus\pen S=<ttomor ?ugly_assertion\<close> by blast
    fix k \<gamma>
    assume "(k,*4o>e = ev x\<close> \<open>x \<notin> S\<close> have \<open>?ugly_assertion\<close> by blast
    have "line_integral_exists F {b} \<gamma>"
      apply(rule line_integral_exists_smooth)
      using \<open>(k, \<gamma>) \<in> one_chain2\<close> assms(2) apply blast
      using assms
      using \<open>(k, \<gamma>) \<in> one_chain2\<close> \<open>b \<in> basis\<close> apply blast
      using \<open>b \<in> basis\<close> by blast}
  then have a: "\<forall>b\<in>basis. \<forall>(k, \<gamma>)\<in>one_chain2. line_integral_exists F {b} \<gamma>"
    by auto
  have b: "\<forall>(k2,\<gamma>2)\<in>one_chain2. valid_path \<gamma>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 "\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>"
    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 \<gamma> subdiv"
  shows "\<forall>(k',\<gamma>')\<in>subdiv. (path_image \<gamma>') \<subseteq> path_image \<gamma>"
  using assms chain_subdiv_path.simps path_image_rec_join
  by(auto simp add: chain_subdiv_path.simps)

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

lemma img_subset
  assumes "chain_reparam_weak_path \<gamma> subdiv"
  shows "\<forall>(k',\<gamma>')\<in>next
  using assms
  apply(auto simp add: text \<open>Now we can express \<^term>\<open>initials (P \ S)\<close>.
  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,\<gamma>)\<in> subdiv"
  shows " \<exists>k' \<gamma>'. (k',\<gamma>')\<in> one_chain \<and> path_image \<gamma> \<subseteq> path_image \<gamma>'"
  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 "\<Union> (path_image ` {\<gamma>. \<exists>k. (k,\<gamma>)\<in> subdiv}) \<subseteq> \<Union> (path_image ` {\<gamma>. \<exists>k. (k,\<gamma>)\<in> 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,\<gamma>)\<in> subdiv"
  shows " \<exists>k' \<gamma>'. (k',\<gamma>')\<in> one_chain \<and> path_image \<gamma> \<subseteq> path_image \<gamma>'"
  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 \<times> (real \<Rightarrow> real \<times> real)) set \<Rightarrow> (int \<times> (real \<Rightarrow> real \<times> real)) set \<Rightarrow> bool" where
    "common_reparam_exists one_chain1 one_chain2 \<equiv>
    (\<exists>subdiv ps1 ps2.
    chain_reparam_chain' (one_chain1 - ps1) subdiv \<and>
    chain_reparam_chain' (one_chain2 - ps2) subdiv \<and>
    (\<forall>(k, \<gamma>)\<in>subdiv.  \<gamma> C1_differentiable_on {0..1}) \<and>
    boundary_chain subdiv \<and>
     \<gamma>) \<and>
    (\<forall>(k, \<gamma>)\<in>ps2. point_path \<gamma>))"

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 \<times> (real \<Rightarrow> real \<times> real)) set)"
    "boundary_chain (one_chain2::(int \<times> (real \<Rightarrow> real \<times> real)) set)"
    " \<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)"
    "(common_reparam_exists one_chain1 one_chain2)"
    "(\<forall>(k, \<gamma>)\<in>one_chain1.  valid_path \<gamma>)"
    "(\<forall>(k, \<gamma>)\<in>one_chain2.  valid_path \<gamma>)"
  shows "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2"
    "\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>"
proof-
  obtain subdiv ps1 ps2 where props:
    "chain_reparam_chain' (one_chain1 - ps1) subdiv"
    "chain_reparam_chain' (one_chain2 - ps2) subdiv "
    "(\<forall>(k, \<gamma>)\<in>subdiv.  \<gamma> C1_differentiable_on {0..1})"
    "boundary_chain subdiv"
    "(\<forall>(k, \<gamma>)\<in>ps1. point_path \<gamma>)"
    "(\<forall>(k, \<gamma>)\<in>ps2. point_path \<gamma>)"
    using assms
    by (auto simp add: common_reparam_exists_def)
  have subdiv_valid: "(\<forall>(k, \<gamma>)\<in>subdiv.  valid_path \<gamma>)"
    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 \<gamma>2 b
    assume ass: "(k2, \<gamma>2)\<in>subdiv "" b\<in>basis"
    have "\<And> k \<gamma>. (k, \<gamma>) \<in> subdiv \<Longrightarrow> \<exists>k' \<gamma>'. (k', \<gamma>') \<in> one_chain2 \<and> path_image \<gamma> \<subseteq> path_image \<gamma>'"
      by (meson chain_reparam_chain'_pathimg_subset' props Diff_subset subsetCE)
    then have "continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)"
      using assms(6) continuous_on_subset[where ?f = " (\<lambda>x. F x \<bullet> b)"] ass
      apply(auto simp add:  subset_iff)
      by (metis (mono_tags, lifting) case_prodD)}
  then have cont_field: "\<forall>b\<in>basis. \<forall>(k2, \<gamma>2)\<in>subdiv. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)"
    by auto
  have one_chain1_ps_valid: "(\<forall>(k, \<gamma>)\<in>one_chain1 - ps1.  valid_path \<gamma>)" using assms by auto
  have one_chain2_ps_valid: "(\<forall>(k, \<gamma>)\<in>one_chain2 - ps1.  valid_path \<gamma>)" 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
    usingropspsassms
    n_boundary1pplyst
    using props assms
    apply blast
    using one_chain1_ps_valid by blast
  java.lang.StringIndexOutOfBoundsException: Range [49, 6) out of bounds for length 95
    apply(rule chain_reparam_chain'_line_integral_smooth_cubes}
    using props assms
    apply blast
    using props assms
    using onechain_boundary1 apply blast
  ng opss
    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:"\<forall>(k, \<gamma>)\<in>(one_chain2 - ps2). line_integral_exists F basis \<gamma>"
    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: "\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>"
    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 \<Rightarrow> real \<Rightarrow> (int \<times> (real \<Rightarrow> real \<times> real)) \<Rightarrow> (int \<times> (real \<Rightarrow> real \<times> real))" where
  "subcube a b cube = (fst cube, subpath a b (snd cube))"

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

end