Theory Polyline_Path
section ‹Building a path from a list of points›
theory Polyline_Path
imports "HOL-Library.Sublist" "Path_Automation.Path_Automation"
begin
lemma weak_wf_pathlist_altdef:
"weak_wf_pathlist ps ⟷ ps ≠ [] ∧ successively (λp q. pathfinish p = pathstart q) ps"
by (induction ps rule: weak_wf_pathlist.induct) auto
lemma path_image_joinpaths_list_subset:
"ps ≠ [] ⟹ path_image (joinpaths_list ps) ⊆ (⋃p∈set ps. path_image p)"
by (induction ps rule: joinpaths_list.induct) (use path_image_join_subset in auto)
definition polyline_path :: "'a :: real_normed_vector list ⇒ real ⇒ 'a" where
"polyline_path xs =
(if length xs = 1 then linepath (hd xs) (hd xs) else joinpaths_list (map2 linepath xs (tl xs)))"
lemma pathstart_polyline_path:
assumes "xs ≠ []"
shows "pathstart (polyline_path xs) = hd xs"
proof (cases "length xs = 1")
case False
hence "tl xs ≠ []"
using assms by (cases xs) auto
thus ?thesis using assms
by (auto simp: polyline_path_def pathstart_joinpaths_list hd_map case_prod_unfold hd_zip)
qed (auto simp: polyline_path_def)
lemma pathfinish_polyline_path:
assumes "xs ≠ []"
shows "pathfinish (polyline_path xs) = last xs"
proof (cases "length xs = 1")
case True
thus ?thesis
by (cases xs) (auto simp: polyline_path_def)
next
case False
from assms have "length xs ≠ 0"
by auto
with False have "length xs ≥ 2"
by linarith
from False have *: "tl xs ≠ []"
using assms by (cases xs) auto
have "last (zip xs (tl xs)) = zip xs (tl xs) ! (length xs - 2)"
using False * by (subst last_conv_nth) (auto simp: eval_nat_numeral)
also have "snd … = xs ! (length xs - 1)"
using ‹length xs ≥ 2› by (subst nth_zip) (auto simp: nth_tl simp flip: Suc_diff_le)
also have "… = last xs"
using ‹length xs ≥ 2› by (subst last_conv_nth) auto
finally show ?thesis using assms False *
by (auto simp: polyline_path_def pathfinish_joinpaths_list last_map case_prod_unfold)
qed
lemma polyline_path_welldefined:
assumes "xs ≠ []"
shows "successively (λp q. pathfinish p = pathstart q) (map2 linepath xs (tl xs))"
proof (cases "length xs = 1")
case True
thus ?thesis
by (cases xs) auto
next
case False
have "length xs ≠ 0"
using assms by auto
with False have "length xs ≥ 2"
by linarith
thus "successively (λp q. pathfinish p = pathstart q) (map2 linepath xs (tl xs))"
proof (induction xs rule: induct_list012)
case (3 x y zs)
have IH:
"successively (λp q. pathfinish p = pathstart q) (map2 linepath (y # zs) (tl (y # zs)))"
if "zs ≠ []"
by (rule "3.IH") (use ‹zs ≠ []› in ‹auto intro!: Suc_leI›)
show ?case using IH
by (auto simp: successively_Cons hd_map hd_zip)
qed auto
qed
lemma valid_path_polyline_path [simp, intro]: "valid_path (polyline_path xs)"
proof -
consider "length xs = 0" | "length xs = 1" | "length xs ≥ 2"
by linarith
thus ?thesis
proof cases
assume "length xs ≥ 2"
hence [simp]: "tl xs ≠ []" "xs ≠ []"
by (cases xs; force)+
have "valid_path (joinpaths_list (map2 linepath xs (tl xs)))"
proof (rule valid_path_joinpaths_list)
show "valid_path_pathlist (map2 linepath xs (tl xs))"
unfolding valid_path_pathlist_altdef
using ‹length xs ≥ 2› by (simp add: list.pred_map o_def case_prod_unfold list.pred_True)
next
have "successively (λp q. pathfinish p = pathstart q) (map2 linepath xs (tl xs))"
using ‹length xs ≥ 2› by (intro polyline_path_welldefined) auto
thus "weak_wf_pathlist (map2 linepath xs (tl xs))"
unfolding weak_wf_pathlist_altdef using ‹length xs ≥ 2› by auto
qed
thus ?thesis
using ‹length xs ≥ 2› by (simp add: polyline_path_def)
qed (auto simp: polyline_path_def)
qed
lemma path_polyline_path [simp, intro]: "path (polyline_path xs)"
by (rule valid_path_imp_path) auto
lemma polyline_path_subset_convex:
assumes "convex A" "set xs ⊆ A" and [simp]: "xs ≠ []"
shows "path_image (polyline_path xs) ⊆ A"
proof (cases "length xs = 1")
case True
thus ?thesis
using assms by (cases xs) (auto simp: polyline_path_def)
next
case False
have "length xs ≠ 0"
by auto
with False have "length xs ≥ 2"
by linarith
have [simp]: "tl xs ≠ []"
using ‹length xs ≥ 2› by (cases xs) auto
have "path_image (polyline_path xs) = path_image (joinpaths_list (map2 linepath xs (tl xs)))"
using ‹length xs ≥ 2› unfolding polyline_path_def by simp
also have "… ⊆ (⋃l∈set (map2 linepath xs (tl xs)). path_image l)"
by (rule path_image_joinpaths_list_subset) auto
also have "… ⊆ (⋃x∈set xs. ⋃y∈set (tl xs). closed_segment x y)"
using ‹length xs ≥ 2› by (fastforce dest: set_zip_leftD set_zip_rightD)
also have "… ⊆ (⋃x∈set xs. ⋃y∈set xs. closed_segment x y)"
by (cases xs) auto
also have "… ⊆ A"
by (intro UN_least closed_segment_subset) (use assms in auto)
finally show ?thesis .
qed
lemma contour_integral_polyline_path:
assumes "f contour_integrable_on (polyline_path ps)"
assumes "ps ≠ []"
shows "contour_integral (polyline_path ps) f =
(∑i<length ps-1. contour_integral (linepath (ps ! i) (ps ! Suc i)) f)"
proof (cases "length ps ≥ 2")
case True
have [simp]: "ps ≠ []" "tl ps ≠ []"
using True by (cases ps; force)+
have "contour_integral (polyline_path ps) f =
contour_integral (joinpaths_list (map2 linepath ps (tl ps))) f "
unfolding polyline_path_def using True by simp
also have "… = (∑p←map2 linepath ps (tl ps). contour_integral p f)"
using polyline_path_welldefined[of ps] assms True
by (subst contour_integral_joinpaths_list)
(auto simp: valid_path_pathlist_altdef weak_wf_pathlist_altdef
list.pred_set list.pred_True polyline_path_def)
also have "… = (∑i<length ps-1. contour_integral (linepath (ps ! i) (tl ps ! i)) f)"
by (subst sum.list_conv_set_nth) (auto simp: atLeast0LessThan)
also have "… = (∑i<length ps-1. contour_integral (linepath (ps ! i) (ps ! Suc i)) f)"
by (intro sum.cong) (auto simp: nth_tl)
finally show ?thesis .
next
case False
from ‹ps ≠ []› have "length ps ≠ 0"
by auto
hence "length ps = 1"
using False by linarith
thus ?thesis
by (auto simp: polyline_path_def)
qed
end