Theory Paths

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

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


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

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

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

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

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

lemma content_box_cases:
  "content (box a b) = (if iBasis. ai  bi then prod (λi. bi - ai) Basis else 0)"
  by (simp add: measure_lborel_box_eq inner_diff)

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

lemma content_eq_0: "content (box a b) = 0  (iBasis. bi  ai)"
  by (auto simp: content_box_cases not_le intro: less_imp_le antisym eq_refl)

lemma content_pos_lt_eq: "0 < content (cbox a (b::'a::euclidean_space))  (iBasis. ai < bi)"
  by (auto simp add: content_cbox_cases less_le prod_nonneg)

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

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

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


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

lemma line_integral_distrib:
  assumes "line_integral_exists f basis g1"
    "line_integral_exists f basis g2"
    "valid_path g1" "valid_path g2"
  shows "line_integral f basis (g1 +++ g2) = line_integral f basis g1 + line_integral f basis g2"
    "line_integral_exists f basis (g1 +++ g2)"
proof -
  obtain s1 s2
    where s1: "finite s1" "x{0..1} - s1. g1 differentiable at x"
      and s2: "finite s2" "x{0..1} - s2. g2 differentiable at x"
    using assms
    by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
  obtain i1 i2
    where 1: "((λx. bbasis. f (g1 x)  b * (vector_derivative g1 (at x within {0..1})  b)) has_integral i1) {0..1}"
      and 2: "((λx. bbasis. 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 * (bbasis. 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 * (bbasis. 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. bbasis. 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. bbasis. 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. abasis. 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. bbasis. 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. bbasis. ((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. bbasis. 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. bbasis. ((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. bbasis. F (g x)  b * (vector_derivative g (at x within {0..1})  b)) has_integral c){0..1}"
  shows  "((λx. bbasis. F ((reversepath g) x)  b * (vector_derivative (reversepath g) (at x within {0..1})  b)) has_integral -c){0..1}"
proof -
  { fix s x
    assume xs: "g C1_differentiable_on ({0..1} - s)" "x  (-) 1 ` s" "0  x" "x  1"
    have "vector_derivative (λx. g (1 - x)) (at x within {0..1}) =
                - vector_derivative g (at (1 - x) within {0..1})"
    proof -
      obtain f' where f': "(g has_vector_derivative f') (at (1 - x))"
        using xs
        by (force simp: has_vector_derivative_def C1_differentiable_on_def)
      have "(g o (λx. 1 - x) has_vector_derivative -1 *R f') (at x)"
        apply (rule vector_diff_chain_within)
         apply (intro vector_diff_chain_within derivative_eq_intros | simp)+
        apply (rule has_vector_derivative_at_within [OF f'])
        done
      then have mf': "((λx. g (1 - x)) has_vector_derivative -f') (at x)"
        by (simp add: o_def)
      show ?thesis
        using xs
        by (auto simp: vector_derivative_at_within_ivl [OF mf'] vector_derivative_at_within_ivl [OF f'])
    qed
  } note * = this
  obtain S where "continuous_on {0..1} g" "finite S" "g C1_differentiable_on {0..1} - S"
    using g
    by (auto simp: valid_path_def piecewise_C1_differentiable_on_def)
  then show ?thesis 
    using has_integral_affinity01 [OF int, where m= "-1" and c=1]
    unfolding reversepath_def
    by (rule_tac S = "(λx. 1 - x) ` S" in has_integral_spike_finite) (auto simp: * has_integral_neg Groups_Big.sum_negf)
qed

lemma line_integral_on_reverse_path:
  assumes "valid_path γ" "line_integral_exists F basis γ"
  shows "line_integral F basis γ = - (line_integral F basis (reversepath γ))"
        "line_integral_exists F basis (reversepath γ)"
proof -
  obtain i where
    0: "((λx. bbasis. 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. bbasis. 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:
    "bbasis. (λ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 
                at. f a integrable_on s  (λx. at. f a x) integrable_on s"
    using integrable_sum by metis
  have field_integrable_on_basis:
    "(λx. bbasis. 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. bbasis. 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. bbasis. 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: "(bbasis. 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 "(bbasis. f (g u)  b * (vector_derivative (λx. g u) (at x within {0..1})  b)) = 0"
      by auto
  qed
  then have "((λx. bbasis. 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. bbasis. 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. bbasis. f (g (x))   b * (vector_derivative g (at x within {0..1})   b)))
           {0..1}"
    using f uv
    apply (simp add: line_integral_exists_def subpath_def)
    apply (drule integrable_on_subcbox [where a=u and b=v, simplified])
     apply (simp_all add: has_integral_integral)
    apply (drule has_integral_affinity [where m="v-u" and c=u, simplified])
     apply (simp_all add: False image_affinity_atLeastAtMost_div_diff scaleR_conv_of_real)
    apply (simp add: divide_simps False)
    done
  have vd:"x. x  {0..1} 
           x  (λt. (v-u) *R t + u) -` s 
           vector_derivative (λx. g ((v-u) * x + u)) (at x within {0..1}) = (v-u) *R vector_derivative g (at ((v-u) * x + u) within {0..1})"
    using test2[OF s fs uv]
    by auto
  have arg:"x. (nbasis. (v - u) * (f (g ((v - u) * x + u))  n) * (vector_derivative g (at ((v - u) * x + u) within {0..1})  n))
              =    (bbasis. 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. bbasis. 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. bbasis. f (g (x))   b * (vector_derivative g (at x within {0..1})  b)))) {0..1}"
    apply (cut_tac Henstock_Kurzweil_Integration.has_integral_mult_right [OF *, where c = "v-u"])
    using fs assms
    apply (simp add: False subpath_def line_integral_exists_def)
    apply (rule_tac S = "(λt. ((v-u) *R t + u)) -` s" in has_integral_spike_finite)
      apply (auto simp: inj_on_def False vd finite_vimageI scaleR_conv_of_real Groups_Big.sum_distrib_left
        mult.assoc[symmetric] arg)
    done
  then show "(line_integral_exists f basis (subpath u v g))"
    by(auto simp add: line_integral_exists_def subpath_def integrable_on_def)
qed

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

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


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

definition boundary_chain where
    "boundary_chain s  ((k, γ)  s. k = 1  k = -1)"

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

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

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

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

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

lemma pathstart_rec_join_2:
  "pathstart (rec_join ((-1, γ) # l)) = pathstart (reversepath γ)"
proof cases
  assume "l = []"
  then show "pathstart (rec_join ((-