# Theory Paths

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

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

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

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

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

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

lemma content_box_cbox:
shows "content (box a b) = content (cbox a b)"

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

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

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

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

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

lemma has_integral_null [intro]: "content(box a b) = 0 ⟹ (f has_integral 0) (box a b)"

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)
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)
ultimately
show "line_integral f basis (g1 +++ g2) = line_integral f basis g1 + line_integral f basis g2"
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)"
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])
done
then have *:"(λx. ∑b∈basis. ((f ((g1 +++ g2) (x/2 + 1/2)) ∙ b) / 2)* (vector_derivative (g1 +++ g2) (at (x/2 + 1/2) within {0..1}) ∙ b)) integrable_on {0..1}"
by (auto simp: Groups_Big.sum_distrib_left dest: integrable_cmul [where c="1/2"] simp: scaleR_conv_of_real)
have g2: "⟦1 < z*2; z ≤ 1; z*2 - 1 ∉ s2⟧ ⟹
vector_derivative (λx. if x*2 ≤ 1 then g1 (2*x) else g2 (2*x - 1)) (at z within {0..1}) =
2 *⇩R vector_derivative g2 (at (z*2 - 1) within {0..1})" for z       proof -
have i:"⟦1 < z*2; z ≤ 1; z*2 - 1 ∉ s2⟧ ⟹
vector_derivative (λx. if x * 2 ≤ 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1})
= 2 *⇩R vector_derivative g2 (at (z * 2 - 1))" for z
proof-
have g2_at_z:"⟦1 < z*2; z ≤ 1; z*2 - 1 ∉ s2⟧ ⟹
((λx. if x*2 ≤ 1 then g1 (2*x) else g2 (2*x - 1)) has_vector_derivative 2 *⇩R vector_derivative g2 (at (z*2 - 1))) (at z)" for z
apply (rule has_vector_derivative_transform_at [of "¦z - 1/2¦" _ "(λx. g2 (2*x - 1))"])
apply (simp_all add: dist_real_def abs_if split: if_split_asm)
apply (rule vector_diff_chain_at [of "λx. 2*x - 1" 2 _ g2, simplified o_def])
apply (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
using s2
apply (auto simp: algebra_simps vector_derivative_works)
done
assume ass: "1 < z*2" "z ≤ 1" "z*2 - 1 ∉ s2"
then have z_le: "z≤ 1" by auto
have z_ge: "0 ≤ z" using ass by auto
show "vector_derivative (λx. if x * 2 ≤ 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1})
= 2 *⇩R vector_derivative g2 (at (z * 2 - 1))"
using Derivative.vector_derivative_at_within_ivl[OF g2_at_z[OF ass] z_ge z_le]
by auto
qed
assume ass: "1 < z*2" "z ≤ 1" "z*2 - 1 ∉ s2"
then have "(g2 has_vector_derivative ((vector_derivative g2 (at (z*2 - 1))))) (at (z*2 - 1))"
using s2 by (auto simp: algebra_simps vector_derivative_works)
then have ii: "(vector_derivative g2 (at (z*2 - 1) within {0..1})) = (vector_derivative g2 (at (z*2 - 1)))"
using Derivative.vector_derivative_at_within_ivl ass
by force
show "vector_derivative (λx. if x * 2 ≤ 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *⇩R vector_derivative g2 (at (z * 2 - 1) within {0..1})"
using i[OF ass] ii
by auto
qed
show ?thesis
using s2
apply (auto simp: line_integral_exists_def)
apply (rule integrable_spike_finite [of "{0,1} ∪ s2", OF _ _ *])
apply (auto simp: joinpaths_def scaleR_conv_of_real g2)
done
qed

lemma has_line_integral_on_reverse_path:
assumes g: "valid_path g" and int:
"((λx. ∑b∈basis. F (g x) ∙ b * (vector_derivative g (at x within {0..1}) ∙ b)) has_integral c){0..1}"
shows  "((λx. ∑b∈basis. F ((reversepath g) x) ∙ b * (vector_derivative (reversepath g) (at x within {0..1}) ∙ b)) has_integral -c){0..1}"
proof -
{ fix s x
assume xs: "g C1_differentiable_on ({0..1} - s)" "x ∉ (-) 1 ` s" "0 ≤ x" "x ≤ 1"
have "vector_derivative (λx. g (1 - x)) (at x within {0..1}) =
- vector_derivative g (at (1 - x) within {0..1})"
proof -
obtain f' where f': "(g has_vector_derivative f') (at (1 - x))"
using xs
by (force simp: has_vector_derivative_def C1_differentiable_on_def)
have "(g o (λx. 1 - x) has_vector_derivative -1 *⇩R f') (at x)"
apply (rule vector_diff_chain_within)
apply (intro vector_diff_chain_within derivative_eq_intros | simp)+
apply (rule has_vector_derivative_at_within [OF f'])
done
then have mf': "((λx. g (1 - x)) has_vector_derivative -f') (at x)"
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"
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
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 (drule integrable_on_subcbox [where a=u and b=v, simplified])
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)
done
have vd:"⋀x. x ∈ {0..1} ⟹
x ∉ (λt. (v-u) *⇩R t + u) -` s ⟹
vector_derivative (λx. g ((v-u) * x + u)) (at x within {0..1}) = (v-u) *⇩R vector_derivative g (at ((v-u) * x + u) within {0..1})"
using test2[OF s fs uv]
by auto
have arg:"⋀x. (∑n∈basis. (v - u) * (f (g ((v - u) * x + u)) ∙ n) * (vector_derivative g (at ((v - u) * x + u) within {0..1}) ∙ n))
=    (∑b∈basis. f (g ((v - u) * x + u)) ∙ b * (v - u) * (vector_derivative g (at ((v - u) * x + u) within {0..1}) ∙ b))"
have"((λx. ∑b∈basis. f (g ((v - u) * x + u))  ∙ b * (vector_derivative (λx. g ((v - u) * x + u)) (at x within {0..1})  ∙ b)) has_integral
(integral {u..v} (λx. ∑b∈basis. f (g (x))  ∙ b * (vector_derivative g (at x within {0..1}) ∙ b)))) {0..1}"
apply (cut_tac Henstock_Kurzweil_Integration.has_integral_mult_right [OF *, where c = "v-u"])
using fs assms
apply (simp add: False subpath_def line_integral_exists_def)
apply (rule_tac S = "(λt. ((v-u) *⇩R t + u)) -` s" in has_integral_spike_finite)
apply (auto simp: inj_on_def False vd finite_vimageI scaleR_conv_of_real Groups_Big.sum_distrib_left
mult.assoc[symmetric] arg)
done
then show "(line_integral_exists f basis (subpath u v g))"
by(auto simp add: line_integral_exists_def subpath_def integrable_on_def)
qed

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

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

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

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

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

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

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

lemma joined_is_valid:
assumes boundary_chain: "boundary_chain (set l)" and
valid_path: "⋀k γ. (k, γ) ∈ set l ⟹ valid_path γ" and
valid_chain_list_ass: "valid_chain_list l"
shows "valid_path (rec_join l)"
using assms
proof(induction l)
case Nil
then show ?case
using C1_differentiable_imp_piecewise[OF C1_differentiable_on_const[of "0" "{0..1}"]]
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)
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 ((- ```