Quellcode-Bibliothek Pick.thy
Sprache: Isabelle
|
|
theory Pick
imports
Polygon_Splitting
Elementary_Triangle_Area
begin
section "Setup"
subsection "Integral Points Cardinality Properties"
lemma bounded_finite:
fixes A:: "(real^2) set"
assumes "bounded A"
shows "finite {x::(real^2). integral_vec x ∧ x ∈ A}" (is "finite ?A_int")
proof-
obtain M where M: "∀x ∈ A. norm x ≤ M" using assms bounded_def by (meson bounded_iff)
let ?M_bounded_ints = "{n. n ∈ {-M..M} ∧ is_int n}"
let ?M_bounded_int_vecs = "{v::(real^2). v$1 ∈ ?M_bounded_ints ∧ v$2 ∈ ?M_bounded_ints}"
have "∀x::(real^2). norm (x$1) ≤ norm x ∧ (x$2) ≤ norm x"
by (smt (verit, ccfv_threshold) Finite_Cartesian_Product.norm_nth_le real_norm_def)
then have "∀x ∈ ?A_int. norm (x$1) ≤ M ∧ norm (x$2) ≤ M"
using M dual_order.trans Finite_Cartesian_Product.norm_nth_le by blast
then have "∀x ∈ ?A_int. x$1 ∈ ?M_bounded_ints ∧ x$2 ∈ ?M_bounded_ints"
using integral_vec_def intervalE by auto
then have "∀x ∈ ?A_int. x ∈ ?M_bounded_int_vecs" by blast
moreover have "finite ?M_bounded_int_vecs"
proof-
obtain S :: "int set" where S: "S = {n. ∃m ∈ ?M_bounded_ints. n = m} ∧ (∀n ∈ S. norm n ≤ M)"
by (simp add: abs_le_iff)
then have finite_S: "finite S"
by (metis infinite_int_iff_unbounded le_floor_iff linorder_not_less norm_of_int of_int_abs)
(* Construct injection f : ?M_bounded_ints \<rightarrow> S *)
have finite_M_bounded_ints: "finite ?M_bounded_ints"
proof-
let ?f = "λn::real. THE m::int. n = m"
have "∀n ∈ ?M_bounded_ints. ∃!m::int. n = m" using is_int_def by force
moreover have "inj_on ?f ?M_bounded_ints" using inj_on_def is_int_def by force
moreover have "?f ` ?M_bounded_ints ⊆ S" using calculation S subsetI by auto
ultimately show ?thesis using finite_imageD finite_S by (simp add: inj_on_finite)
qed
show ?thesis (* Construct injection f : ?M_bounded_int_vecs \<rightarrow> S \<times> S *)
proof-
let ?f = "λx::(real^2). (THE m::int. m = x$1, THE n::int. n = x$2)"
have "inj_on ?f ?M_bounded_int_vecs"
unfolding inj_on_def
proof clarify
fix x y :: "real^2"
assume x1_int: "is_int (x$1)"
assume x2_int: "is_int (x$2)"
assume y1_int: "is_int (y$1)"
assume y2_int: "is_int (y$2)"
assume x1y1_int_eq: "(THE m. real_of_int m = x$1) = (THE m. real_of_int m = y$1)"
assume x2y2_int_eq: "(THE n. real_of_int n = x$2) = (THE n. real_of_int n = y$2)"
have "∃!m. m = x$1"
by blast
moreover have "∃!n. n = y$1"
by blast
moreover have "(THE m. real_of_int m = x$1) = (THE m. real_of_int m = y$1)"
using x1y1_int_eq by auto
ultimately have x1y1: "x$1 = y$1"
using x1_int y1_int is_int_def by auto
have "∃!m. m = x$2"
by blast
moreover have "∃!n. n = y$2"
by blast
moreover have "(THE m. real_of_int m = x$2) = (THE m. real_of_int m = y$2)"
using x2y2_int_eq by auto
ultimately have x2y2: "x$2 = y$2"
using x2_int y2_int is_int_def by auto
show "x = y" using x1y1 x2y2
by (metis (no_types, lifting) exhaust_2 vec_eq_iff)
qed
moreover have "?f ` ?M_bounded_int_vecs ⊆ S × S"
proof(rule subsetI)
fix mn
assume "mn ∈ ?f ` ?M_bounded_int_vecs"
then obtain v where v:
"v ∈ ?M_bounded_int_vecs ∧ ?f v = mn ∧ (∃!m. v$1 = m) ∧ (∃!n. v$2 = n)"
using is_int_def by auto
let ?m = "fst mn"
let ?n = "snd mn"
have "?m = (THE m::int. m = v$1)" using v
by (meson fstI)
moreover have "∃! m::int. m = v$1" using v is_int_def
by (metis (no_types, lifting) mem_Collect_eq of_int_eq_iff)
ultimately have m_in_S: "?m ∈ S"
by (metis (mono_tags, lifting) S mem_Collect_eq theI' v)
have "?n = (THE n::int. n = v$2)" using v
by (meson sndI)
moreover have "∃! n::int. n = v$2" using v is_int_def
by (metis (no_types, lifting) mem_Collect_eq of_int_eq_iff)
ultimately have n_in_S: "?n ∈ S"
by (metis (mono_tags, lifting) S mem_Collect_eq theI' v)
show "mn ∈ S × S" using m_in_S n_in_S v by auto
qed
ultimately show ?thesis
by (meson finite_S finite_SigmaI finite_imageD finite_subset)
qed
qed
ultimately show ?thesis
by (smt (verit) finite_subset subsetI)
qed
lemma finite_path_image:
assumes "polygon p"
shows "finite {x. integral_vec x ∧ x ∈ path_image p}"
using bounded_finite inside_outside_polygon
unfolding inside_outside_def
by (meson assms bounded_simple_path_image polygon_def)
lemma finite_path_inside:
assumes "polygon p"
shows "finite {x. integral_vec x ∧ x ∈ path_inside p}"
using bounded_finite inside_outside_polygon
unfolding inside_outside_def
using assms by presburger
lemma bounded_finite_inside:
fixes B:: "(real^2) set"
assumes "simple_path p"
shows "bounded (path_inside p)"
using assms
by (simp add: bounded_inside bounded_simple_path_image path_inside_def)
lemma finite_integral_points_path_image:
assumes "simple_path p"
shows "finite {x. integral_vec x ∧ x ∈ path_image p}"
using bounded_finite bounded_simple_path_image assms by blast
lemma finite_integral_points_path_inside:
assumes "simple_path p"
shows "finite {x. integral_vec x ∧ x ∈ path_inside p}"
using bounded_finite bounded_finite_inside assms by blast
section "Pick splitting"
lemma pick_split_path_union_main:
assumes is_split: "is_polygon_split_path vts i j cutvts"
assumes "vts1 = (take i vts)"
assumes "vts2 = (take (j - i - 1) (drop (Suc i) vts))"
assumes "vts3 = drop (j - i) (drop (Suc i) vts)"
assumes "x = vts!i"
assumes "y = vts!j"
assumes "cutpath = make_polygonal_path (x # cutvts @ [y])"
assumes p: "p = make_polygonal_path (vts@[vts!0])" (is "p = make_polygonal_path ?p_vts")
assumes p1: "p1 = make_polygonal_path (x#(vts2 @ [y] @ (rev cutvts) @ [x]))" (is "p1 = make_polygonal_path ?p1_vts")
assumes p2: "p2 = make_polygonal_path (vts1 @ ([x] @ cutvts @ [y]) @ vts3 @ [vts ! 0])" (is "p2 = make_polygonal_path ?p2_vts")
assumes I1: "I1 = card {x. integral_vec x ∧ x ∈ path_inside p1}"
assumes B1: "B1 = card {x. integral_vec x ∧ x ∈ path_image p1}"
assumes I2: "I2 = card {x. integral_vec x ∧ x ∈ path_inside p2}"
assumes B2: "B2 = card {x. integral_vec x ∧ x ∈ path_image p2}"
assumes I: "I = card {x. integral_vec x ∧ x ∈ path_inside p}"
assumes B: "B = card {x. integral_vec x ∧ x ∈ path_image p}"
assumes all_integral_vts: "all_integral vts"
shows "measure lebesgue (path_inside p1) = I1 + B1/2 - 1
==> measure lebesgue (path_inside p2) = I2 + B2/2 - 1
==> measure lebesgue (path_inside p) = I + B/2 - 1"
"measure lebesgue (path_inside p) = I + B/2 - 1
==> measure lebesgue (path_inside p2) = I2 + B2/2 - 1
==> measure lebesgue (path_inside p1) = I1 + B1/2 - 1"
"measure lebesgue (path_inside p) = I + B/2 - 1
==> measure lebesgue (path_inside p1) = I1 + B1/2 - 1
==> measure lebesgue (path_inside p2) = I2 + B2/2 - 1"
proof -
let ?p_im = "{x. integral_vec x ∧ x ∈ path_image p}"
let ?p1_im = "{x. integral_vec x ∧ x ∈ path_image p1}"
let ?p2_im = "{x. integral_vec x ∧ x ∈ path_image p2}"
let ?p_int = "{x. integral_vec x ∧ x ∈ path_inside p}"
let ?p1_int = "{x. integral_vec x ∧ x ∈ path_inside p1}"
let ?p2_int = "{x. integral_vec x ∧ x ∈ path_inside p2}"
have vts: "vts = vts1 @ (x # (vts2 @ y # vts3))"
using assms split_up_a_list_into_3_parts
using is_polygon_split_path_def by blast
have "polygon p"
using finite_path_image assms(1) p unfolding is_polygon_split_path_def
by (smt (verit, best))
then have B_finite: "finite ?p_im"
using finite_path_image by auto
have polygon_p1: "polygon p1"
using finite_path_image assms(1) p1 unfolding is_polygon_split_path_def
by (smt (verit) assms(3) assms(5) assms(6))
then have B1_finite: "finite ?p1_im"
using finite_path_image by auto
have polygon_p2: "polygon p2"
using finite_path_image assms(1) p1 unfolding is_polygon_split_path_def
by (smt (verit) assms(2) assms(4) assms(5) assms(6) p2)
then have B2_finite: "finite ?p2_im"
using finite_path_image by auto
have vts_distinct: "distinct vts"
using simple_polygonal_path_vts_distinct
by (metis ‹polygon p› butlast_snoc p polygon_def)
then have x_neq_y: "x ≠ y"
by (metis assms(1) assms(5) assms(6) index_first index_nth_id is_polygon_split_path_def)
then have card_2: "card {x, y} = 2"
by auto
have polygon_split_props: "(is_polygon_cut_path (vts@[vts!0]) cutpath ∧
polygon p ∧ polygon p1 ∧ polygon p2 ∧
path_inside p1 ∩ path_inside p2 = {} ∧
path_inside p1 ∪ path_inside p2 ∪ (path_image cutpath - {x, y}) = path_inside p
∧ ((path_image p1) - (path_image cutpath)) ∩ ((path_image p2) - (path_image cutpath)) = {}
∧ path_image p = ((path_image p1) - (path_image cutpath)) ∪ ((path_image p2) - (path_image cutpath)) ∪ {x, y})"
using assms
by (meson is_polygon_split_path_def)
have measure_sum: "measure lebesgue (path_inside p) = measure lebesgue (path_inside p1) + measure lebesgue (path_inside p2)"
using polygon_split_path_add_measure assms
by (smt (verit, del_insts))
let ?yx_int = "{k. integral_vec k ∧ k ∈ path_image (make_polygonal_path (y#rev cutvts@[x]))}"
let ?xy_int = "{k. integral_vec k ∧ k ∈ path_image cutpath}"
have yx_int_is_xy_int: "?yx_int = ?xy_int"
using rev_vts_path_image[of "x # cutvts @ [y]"] assms(7) by simp
have "x # vts2 @ [y] @ rev cutvts @ [x] = (x#vts2) @ ([y] @ rev cutvts @ [x]) @ []"
by simp
then have "sublist ([y]@rev cutvts@[x]) ?p1_vts"
unfolding sublist_def by blast
then have subset1:
"?xy_int ⊆ ?p1_im"
using sublist_integral_subset_integral_on_path p1 yx_int_is_xy_int
by force
have len_gteq: "length (x # cutvts @ [y]) ≥ 2"
by auto
have sublist_p2: "sublist (x # cutvts @ [y]) ?p2_vts"
unfolding sublist_def by auto
then have subset2:
"?xy_int ⊆ ?p2_im"
using sublist_integral_subset_integral_on_path[OF len_gteq p2 sublist_p2]
assms(7) by blast
let ?S1 = "?p1_im - ?xy_int"
let ?S2 = "?p2_im - ?xy_int"
have disjoint_1: "?S1 ∩ ?S2 = {}"
using polygon_split_props by blast
have integral_xy: "integral_vec x ∧ integral_vec y"
using all_integral_vts vts
using all_integral_def by auto
have nonempty: "y # rev cutvts @ [x] ≠ []"
by simp
have trivial: " make_polygonal_path (y # rev cutvts @ [x]) = make_polygonal_path (y # rev cutvts @ [x])"
by auto
have "pathstart (make_polygonal_path (y#rev cutvts@[x])) = y ∧ pathfinish (make_polygonal_path (y#rev cutvts@[x])) = x"
using polygon_pathstart[OF nonempty trivial] polygon_pathfinish[OF nonempty trivial]
by (metis last.simps last_conv_nth nonempty nth_Cons_0 snoc_eq_iff_butlast)
then have x_in_y_in: "x ∈ path_image (make_polygonal_path (y#rev cutvts@[x])) ∧ y ∈ path_image (make_polygonal_path (y#rev cutvts@[x]))"
unfolding pathstart_def pathfinish_def path_image_def
by (metis ‹pathstart (make_polygonal_path (y # rev cutvts @ [x])) = y ∧ pathfinish (make_polygonal_path (y # rev cutvts @ [x])) = x› path_image_def pathfinish_in_path_image pathstart_in_path_image)
then have "{x, y} ⊆ ?yx_int"
using integral_xy
by simp
then have disjoint_2: "(?S1 ∪ ?S2) ∩ {x, y} = {}"
by (simp add: yx_int_is_xy_int)
have "path_image p =
path_image p1 - path_image cutpath ∪
(path_image p2 - path_image cutpath) ∪
{x, y}"
using polygon_split_props by auto
then have set_union: "?p_im = (?S1 ∪ ?S2) ∪ {x, y}"
using polygon_split_props integral_xy by auto
then have add_card: "B = card (?p1_im - ?xy_int) + card (?p2_im - ?xy_int) + card {x, y}"
using B_finite using disjoint_1 disjoint_2
by (metis (no_types, lifting) B card_Un_disjoint finite_Un)
have sub1: "card (?p1_im - ?xy_int) = B1 - card ?xy_int"
using B1_finite B1 subset1
by (meson card_Diff_subset finite_subset)
have sub2: "card (?p2_im - ?xy_int) = B2 - card ?xy_int"
using B2_finite B2 subset2
by (meson card_Diff_subset finite_subset)
have B: "B = (B1 - card ?xy_int) + (B2 - card ?xy_int) + card {x, y}"
using add_card sub1 sub2
by auto
then have B_sum_h: "B = B1 + B2 - 2*card ?xy_int + 2"
using card_2
by (smt (verit, best) B1 B1_finite B2 B2_finite Nat.add_diff_assoc add.commute card_mono diff_diff_left mult_2 subset1 subset2)
then have "B1 + B2 = B + 2*card ?xy_int - 2"
by (metis (no_types, lifting) B1 B1_finite B2 B2_finite add_mono_thms_linordered_semiring(1) card_mono diff_add_inverse2 le_add2 mult_2 ordered_cancel_comm_monoid_diff_class.add_diff_assoc2 subset1 subset2)
then have B_sum: "(B1 + B2)/2 = B/2 + card ?xy_int - 1"
by (smt (verit) B_sum_h field_sum_of_halves le_add2 mult_2 nat_1_add_1 of_nat_1 of_nat_add of_nat_diff ordered_cancel_comm_monoid_diff_class.add_diff_assoc2)
have casting_h: "∧ A B:: nat. A ≥ B ==> real (A - B) = real A - real B"
by auto
have " path_inside p1 ∪ path_inside p2 ∪ (path_image cutpath - {x, y}) = path_inside p"
using polygon_split_props by auto
then have interior_union: "?p_int = (?xy_int - {x, y}) ∪ ?p1_int ∪ ?p2_int"
by blast
have finite_inside_p: "finite ?p_int"
using bounded_finite inside_outside_polygon
by (simp add: polygon_split_props inside_outside_def)
have finite_pathimage: "finite (?xy_int - {x, y})"
using B1_finite finite_subset subset1 by auto
have finite_inside_p1: "finite ?p1_int"
using polygon_split_props bounded_finite inside_outside_polygon
using finite_Un finite_inside_p interior_union by auto
have finite_inside_p2: "finite ?p2_int"
using polygon_split_props bounded_finite inside_outside_polygon
using finite_Un finite_inside_p interior_union by auto
have path_image_inside_disjoint1: "(?xy_int - {x, y}) ∩ (?p1_int) = {}"
using subset1 inside_outside_polygon[OF polygon_p1]
unfolding inside_outside_def by auto
have path_image_inside_disjoint2: "(?xy_int - {x, y}) ∩ (?p2_int) = {}"
using subset2 inside_outside_polygon[OF polygon_p2]
unfolding inside_outside_def by auto
(* The union of these interiors is disjoint from their path image *)
have "(?xy_int - {x, y}) ∩ (?p1_int ∪ ?p2_int) = {}"
using subset2 path_image_inside_disjoint1 path_image_inside_disjoint2
by auto
then have I_is: "I = card (?xy_int - {x, y}) +
card (?p1_int ∪ ?p2_int)"
using interior_union I finite_inside_p1 finite_inside_p2
by (metis (no_types, lifting) card_Un_disjoint finite_Un finite_pathimage sup_assoc)
have disjoint_4: "?p1_int ∩ ?p2_int = {}"
using polygon_split_props by auto
then have "I = card (?xy_int - {x, y}) +
I1 + I2"
using I_is finite_inside_p1 finite_inside_p2
by (simp add: I1 I2 card_Un_disjoint)
have interior_subset: "(?xy_int - {x, y}) ⊆ ?p_int"
using interior_union by auto
have x_y_subset: "{x, y} ⊆ ?xy_int"
using x_in_y_in rev_vts_path_image[of "x # cutvts @ [y]"] assms(7)
integral_xy
using yx_int_is_xy_int by blast
have " real (card (?xy_int - {x, y})) =
real (card (?xy_int )) - real (card {x, y})"
using x_y_subset
by (metis (no_types, lifting) B2_finite card_Diff_subset card_mono finite_subset of_nat_diff subset2)
then have card_diff: "real (card (?xy_int - {x, y})) =
real (card (?xy_int )) - 2"
using card_2 by auto
then have "I = I1 + I2 + (card (?xy_int - {x, y}))"
using I I1 I2 interior_union finite_inside_p1 finite_inside_p2
by (simp add: I_is disjoint_4 card_Un_disjoint)
then have "I = I1 + I2 + real (card (?xy_int)) - 2"
using card_diff
by linarith
then have I_sum: "I1 + I2 = I - real (card ?xy_int) + 2"
by fastforce
{assume pick1: "measure lebesgue (path_inside p1) = I1 + B1/2 - 1"
assume pick2: "measure lebesgue (path_inside p2) = I2 + B2/2 - 1"
have "measure lebesgue (path_inside p) = I1 + I2 + (B1+B2)/2 -2"
using pick1 pick2 measure_sum by auto
then have "measure lebesgue (path_inside p) = I - real (card ?xy_int) + 2 +
B/2 + card ?xy_int - 1 - 2"
using I_sum B_sum
by linarith
then have "measure lebesgue (path_inside p) = I + B/2 - 1" by auto
}
then show "measure lebesgue (path_inside p1) = I1 + B1/2 - 1 ==> measure lebesgue (path_inside p2) = I2 + B2/2 - 1 ==> measure lebesgue (path_inside p) = I + B/2 - 1"
by blast
{assume pick1: "measure lebesgue (path_inside p) = I + B/2 - 1"
assume pick2: "measure lebesgue (path_inside p2) = I2 + B2/2 - 1"
then have "real I + real B / 2 - 1 = (measure lebesgue (path_inside p1)) + I2 + B2/2 -1"
using measure_sum pick1 pick2 by auto
then have "measure lebesgue (path_inside p) = I - real (card ?xy_int) + 2 +
B/2 + card ?xy_int - 1 - 2"
using I_sum B_sum pick1
by linarith
then have "measure lebesgue (path_inside p1) = I1 + B1/2 - 1"
using B_sum ‹real I = real (I1 + I2) + real (card {k. integral_vec k ∧ k ∈ path_image cutpath}) - 2› field_sum_of_halves measure_sum of_nat_add
pick1 pick2 by auto
}
then show "measure lebesgue (path_inside p) = I + B/2 - 1 ==> measure lebesgue (path_inside p2) = I2 + B2/2 - 1 ==> measure lebesgue (path_inside p1) = I1 + B1/2 - 1"
by blast
{assume pick1: "measure lebesgue (path_inside p) = I + B/2 - 1"
assume pick2: "measure lebesgue (path_inside p1) = I1 + B1/2 - 1"
then have "real I + real B / 2 - 1 = (measure lebesgue (path_inside p2)) + I1 + B1/2 -1"
using measure_sum pick1 pick2 by auto
then have "measure lebesgue (path_inside p) = I - real (card ?xy_int) + 2 +
B/2 + card ?xy_int - 1 - 2"
using I_sum B_sum pick1
by linarith
then have "measure lebesgue (path_inside p2) = I2 + B2/2 - 1"
using B_sum ‹real I = real (I1 + I2) + real (card {k. integral_vec k ∧ k ∈ path_image cutpath}) - 2› field_sum_of_halves measure_sum of_nat_add
using pick2 by auto
}
then show "measure lebesgue (path_inside p) = I + B/2 - 1 ==> measure lebesgue (path_inside p1) = I1 + B1/2 - 1 ==> measure lebesgue (path_inside p2) = I2 + B2/2 - 1"
by blast
qed
lemma pick_split_union:
assumes is_split: "is_polygon_split vts i j"
assumes "vts1 = (take i vts)"
assumes "vts2 = (take (j - i - 1) (drop (Suc i) vts)) "
assumes "vts3 = drop (j - i) (drop (Suc i) vts) "
assumes "x = vts ! i "
assumes "y = vts ! j "
assumes p: "p = make_polygonal_path (vts@[vts!0])" (is "p = make_polygonal_path ?p_vts")
assumes p1: "p1 = make_polygonal_path (x#(vts2@[y, x]))" (is "p1 = make_polygonal_path ?p1_vts")
assumes p2: "p2 = make_polygonal_path (vts1 @ [x, y] @ vts3 @ [vts ! 0])" (is "p2 = make_polygonal_path ?p2_vts")
assumes I1: "I1 = card {x. integral_vec x ∧ x ∈ path_inside p1}"
assumes B1: "B1 = card {x. integral_vec x ∧ x ∈ path_image p1}"
assumes pick1: "measure lebesgue (path_inside p1) = I1 + B1/2 - 1"
assumes I2: "I2 = card {x. integral_vec x ∧ x ∈ path_inside p2}"
assumes B2: "B2 = card {x. integral_vec x ∧ x ∈ path_image p2}"
assumes pick2: "measure lebesgue (path_inside p2) = I2 + B2/2 - 1"
assumes I: "I = card {x. integral_vec x ∧ x ∈ path_inside p}"
assumes B: "B = card {x. integral_vec x ∧ x ∈ path_image p}"
assumes all_integral_vts: "all_integral vts"
shows "measure lebesgue (path_inside p) = I + B/2 - 1"
"measure lebesgue (path_inside p) = measure lebesgue (path_inside p1) + measure lebesgue (path_inside p2)"
proof -
let ?p_im = "{x. integral_vec x ∧ x ∈ path_image p}"
let ?p1_im = "{x. integral_vec x ∧ x ∈ path_image p1}"
let ?p2_im = "{x. integral_vec x ∧ x ∈ path_image p2}"
let ?p_int = "{x. integral_vec x ∧ x ∈ path_inside p}"
let ?p1_int = "{x. integral_vec x ∧ x ∈ path_inside p1}"
let ?p2_int = "{x. integral_vec x ∧ x ∈ path_inside p2}"
have vts: "vts = vts1 @ (x # (vts2 @ y # vts3))"
using assms split_up_a_list_into_3_parts
using is_polygon_split_def by blast
have "polygon p"
using finite_path_image assms(1) p unfolding is_polygon_split_def
by (smt (verit, best))
then have B_finite: "finite ?p_im"
using finite_path_image by auto
have polygon_p1: "polygon p1"
using finite_path_image assms(1) p1 unfolding is_polygon_split_def
by (smt (verit) assms(3) assms(5) assms(6))
then have B1_finite: "finite ?p1_im"
using finite_path_image by auto
have polygon_p2: "polygon p2"
using finite_path_image assms(1) p1 unfolding is_polygon_split_def
by (smt (verit) assms(2) assms(4) assms(5) assms(6) p2)
then have B2_finite: "finite ?p2_im"
using finite_path_image by auto
have vts_distinct: "distinct vts"
using simple_polygonal_path_vts_distinct
by (metis ‹polygon p› butlast_snoc p polygon_def)
then have x_neq_y: "x ≠ y"
by (metis assms(1) assms(5) assms(6) index_first index_nth_id is_polygon_split_def)
then have card_2: "card {x, y} = 2"
by auto
have polygon_split_props: "is_polygon_cut ?p_vts x y ∧
polygon p ∧ polygon p1 ∧ polygon p2 ∧
path_inside p1 ∩ path_inside p2 = {} ∧
path_inside p1 ∪ path_inside p2 ∪ (path_image (linepath x y) - {x, y})
= path_inside p ∧ ((path_image p1) - (path_image (linepath x y))) ∩ ((path_image p2) - (path_image (linepath x y))) = {}
∧ path_image p = ((path_image p1) - (path_image (linepath x y))) ∪ ((path_image p2) - (path_image (linepath x y))) ∪ {x, y} "
using assms
by (meson is_polygon_split_def)
have "measure lebesgue (path_inside p) = measure lebesgue (path_inside p1) + measure lebesgue (path_inside p2)"
using polygon_split_add_measure assms
by (smt (verit, del_insts))
then have measure_sum: "measure lebesgue (path_inside p) = I1 + I2 + (B1+B2)/2 -2"
using pick1 pick2 by auto
let ?yx_int = "{k. integral_vec k ∧ k ∈ path_image (linepath y x)}"
let ?xy_int = "{k. integral_vec k ∧ k ∈ path_image (linepath x y)}"
have yx_int_is_xy_int: "?yx_int = ?xy_int"
by (simp add: closed_segment_commute)
have "sublist [y, x] ?p1_vts" by (simp add: sublist_Cons_right)
then have subset1:
"?xy_int ⊆ ?p1_im"
using sublist_pair_integral_subset_integral_on_path p1 yx_int_is_xy_int by blast
have subset2:
"?xy_int ⊆ ?p2_im"
using sublist_pair_integral_subset_integral_on_path p2 by blast
let ?S1 = "?p1_im - ?xy_int"
let ?S2 = "?p2_im - ?xy_int"
have disjoint_1: "?S1 ∩ ?S2 = {}"
using polygon_split_props by blast
have integral_xy: "integral_vec x ∧ integral_vec y"
using all_integral_vts vts
using all_integral_def by auto
then have "{x, y} ⊆ ?yx_int"
by simp
then have disjoint_2: "(?S1 ∪ ?S2) ∩ {x, y} = {}"
by simp
have "path_image p =
path_image p1 - path_image (linepath x y) ∪
(path_image p2 - path_image (linepath x y)) ∪
{x, y}"
using polygon_split_props by auto
then have set_union: "?p_im = (?S1 ∪ ?S2) ∪ {x, y}"
using polygon_split_props integral_xy by auto
then have add_card: "B = card (?p1_im - ?xy_int) + card (?p2_im - ?xy_int) + card {x, y}"
using B_finite using disjoint_1 disjoint_2
by (metis (no_types, lifting) B card_Un_disjoint finite_Un)
have sub1: "card (?p1_im - ?xy_int) = B1 - card ?xy_int"
using B1_finite B1 subset1
by (meson card_Diff_subset finite_subset)
have sub2: "card (?p2_im - ?xy_int) = B2 - card ?xy_int"
using B2_finite B2 subset2
by (meson card_Diff_subset finite_subset)
have B: "B = (B1 - card ?xy_int) + (B2 - card ?xy_int) + card {x, y}"
using add_card sub1 sub2
by auto
then have B_sum_h: "B = B1 + B2 - 2*card ?xy_int + 2"
using card_2
by (smt (verit, best) B1 B1_finite B2 B2_finite Nat.add_diff_assoc add.commute card_mono diff_diff_left mult_2 subset1 subset2)
then have "B1 + B2 = B + 2*card ?xy_int - 2"
by (metis (no_types, lifting) B1 B1_finite B2 B2_finite add_mono_thms_linordered_semiring(1) card_mono diff_add_inverse2 le_add2 mult_2 ordered_cancel_comm_monoid_diff_class.add_diff_assoc2 subset1 subset2)
then have B_sum: "(B1 + B2)/2 = B/2 + card ?xy_int - 1"
by (smt (verit) B_sum_h field_sum_of_halves le_add2 mult_2 nat_1_add_1 of_nat_1 of_nat_add of_nat_diff ordered_cancel_comm_monoid_diff_class.add_diff_assoc2)
have casting_h: "∧ A B:: nat. A ≥ B ==> real (A - B) = real A - real B"
by auto
have " path_inside p1 ∪ path_inside p2 ∪ (path_image (linepath x y) - {x, y}) = path_inside p"
using polygon_split_props by auto
then have interior_union: "?p_int = (?xy_int - {x, y}) ∪ ?p1_int ∪ ?p2_int"
by blast
have finite_inside_p: "finite ?p_int"
using bounded_finite inside_outside_polygon
by (simp add: polygon_split_props inside_outside_def)
have finite_pathimage: "finite (?xy_int - {x, y})"
using B1_finite finite_subset subset1 by auto
have finite_inside_p1: "finite ?p1_int"
using polygon_split_props bounded_finite inside_outside_polygon
using finite_Un finite_inside_p interior_union by auto
have finite_inside_p2: "finite ?p2_int"
using polygon_split_props bounded_finite inside_outside_polygon
using finite_Un finite_inside_p interior_union by auto
have path_image_inside_disjoint1: "(?xy_int - {x, y}) ∩ (?p1_int) = {}"
using subset1 inside_outside_polygon[OF polygon_p1]
unfolding inside_outside_def by auto
have path_image_inside_disjoint2: "(?xy_int - {x, y}) ∩ (?p2_int) = {}"
using subset2 inside_outside_polygon[OF polygon_p2]
unfolding inside_outside_def by auto
have "(?xy_int - {x, y}) ∩ (?p1_int ∪ ?p2_int) = {}"
using subset2 path_image_inside_disjoint1 path_image_inside_disjoint2
by auto
then have I_is: "I = card (?xy_int - {x, y}) +
card (?p1_int ∪ ?p2_int)"
using interior_union I finite_inside_p1 finite_inside_p2
by (metis (no_types, lifting) card_Un_disjoint finite_Un finite_pathimage sup_assoc)
have disjoint_4: "?p1_int ∩ ?p2_int = {}"
using polygon_split_props by auto
then have "I = card (?xy_int - {x, y}) +
I1 + I2"
using I_is finite_inside_p1 finite_inside_p2
by (simp add: I1 I2 card_Un_disjoint)
have interior_subset: "(?xy_int - {x, y}) ⊆ ?p_int"
using interior_union by auto
have x_y_subset: "{x, y} ⊆ ?xy_int"
using local.set_union by auto
have " real (card (?xy_int - {x, y})) =
real (card (?xy_int )) - real (card {x, y})"
using x_y_subset
by (metis (no_types, lifting) B2_finite card_Diff_subset card_mono finite_subset of_nat_diff subset2)
then have card_diff: "real (card (?xy_int - {x, y})) =
real (card (?xy_int )) - 2"
using card_2 by auto
then have "I = I1 + I2 + (card (?xy_int - {x, y}))"
using I I1 I2 interior_union finite_inside_p1 finite_inside_p2
by (simp add: I_is disjoint_4 card_Un_disjoint)
then have "I = I1 + I2 + real (card (?xy_int)) - 2"
using card_diff
by linarith
then have I_sum: "I1 + I2 = I - real (card ?xy_int) + 2"
by fastforce
have "measure lebesgue (path_inside p) = I - real (card ?xy_int) + 2 +
B/2 + card ?xy_int - 1 - 2"
using measure_sum I_sum B_sum
by linarith
then show "measure lebesgue (path_inside p) = I + B/2 - 1" by auto
show "measure lebesgue (path_inside p) = measure lebesgue (path_inside p1) + measure lebesgue (path_inside p2)"
using ‹Sigma_Algebra.measure lebesgue (path_inside p) = Sigma_Algebra.measure lebesgue (path_inside p1) + Sigma_Algebra.measure lebesgue (path_inside p2)› by blast
qed
lemma pick_split_path_union:
assumes is_split: "is_polygon_split_path vts i j cutvts"
assumes "vts1 = (take i vts)"
assumes "vts2 = (take (j - i - 1) (drop (Suc i) vts))"
assumes "vts3 = drop (j - i) (drop (Suc i) vts)"
assumes "x = vts!i"
assumes "y = vts!j"
assumes "cutpath = make_polygonal_path (x # cutvts @ [y])"
assumes p: "p = make_polygonal_path (vts@[vts!0])" (is "p = make_polygonal_path ?p_vts")
assumes p1: "p1 = make_polygonal_path (x#(vts2 @ [y] @ (rev cutvts) @ [x]))" (is "p1 = make_polygonal_path ?p1_vts")
assumes p2: "p2 = make_polygonal_path (vts1 @ ([x] @ cutvts @ [y]) @ vts3 @ [vts ! 0])" (is "p2 = make_polygonal_path ?p2_vts")
assumes I1: "I1 = card {x. integral_vec x ∧ x ∈ path_inside p1}"
assumes B1: "B1 = card {x. integral_vec x ∧ x ∈ path_image p1}"
assumes pick1: "measure lebesgue (path_inside p1) = I1 + B1/2 - 1"
assumes I2: "I2 = card {x. integral_vec x ∧ x ∈ path_inside p2}"
assumes B2: "B2 = card {x. integral_vec x ∧ x ∈ path_image p2}"
assumes pick2: "measure lebesgue (path_inside p2) = I2 + B2/2 - 1"
assumes I: "I = card {x. integral_vec x ∧ x ∈ path_inside p}"
assumes B: "B = card {x. integral_vec x ∧ x ∈ path_image p}"
assumes all_integral_vts: "all_integral vts"
shows "measure lebesgue (path_inside p) = I + B/2 - 1"
using pick_split_path_union_main pick1 pick2(1) assms by blast
lemma pick_triangle_basic_split:
assumes "p = make_triangle a b c" and "distinct [a, b, c]" and "¬ collinear {a, b, c}" and
d_prop: "d ∈ path_image (linepath a b) ∧ d ∉ {a, b, c}"
shows "good_linepath c d [a, d, b, c, a]
∧ path_image (make_polygonal_path [a, d, b, c, a]) = path_image p"
proof-
let ?l = "linepath c d"
let ?L = "path_image ?l"
let ?P = "path_image p"
let ?vts' = "[a, d, b, c, a]"
let ?p' = "make_polygonal_path ?vts'"
let ?P' = "path_image ?p'"
have h1: "path_image (make_polygonal_path [a, b, c, a]) = path_image (linepath a b) ∪ path_image (linepath b c) ∪ path_image (linepath c a)"
using polygonal_path_image_linepath_union by (simp add: path_image_join sup.assoc)
have h2: "path_image (make_polygonal_path [a, d, b, c, a]) = path_image (linepath a d) ∪ path_image (linepath d b) ∪ path_image (linepath b c) ∪ path_image (linepath c a)"
using polygonal_path_image_linepath_union by (simp add: path_image_join sup.assoc)
have h3: "path_image (linepath a b) = path_image (linepath a d) ∪ path_image (linepath d b)"
using path_image_linepath_union d_prop by auto
have 1: "?P' = ?P"
using h1 h2 h3
using assms(1) make_triangle_def by force
have "{c, d} = ?L ∩ ?P"
proof(rule ccontr)
have subs: "{c, d} ⊆ ?L ∩ ?P"
using assms(1) vertices_on_path_image unfolding make_triangle_def
by (metis IntD2 IntI assms(4) empty_subsetI inf_sup_absorb insert_subset list.discI list.simps(15) nth_Cons_0 path_image_cons_union pathfinish_in_path_image pathfinish_linepath pathstart_in_path_image pathstart_linepath)
assume *: "{c, d} ≠ ?L ∩ ?P"
then obtain z where z: "z ≠ c ∧ z ≠ d ∧ z ∈ ?L ∩ ?P" using subs by blast
then have cases:
"z ∈ path_image (linepath a b) ∨ z ∈ path_image (linepath b c) ∨ z ∈ path_image (linepath c a)"
using "1" h2 h3 by blast
{ assume **: "z ∈ path_image (linepath a b)"
moreover have "z ∈ ?L ∧ d ∈ ?L ∧ d ∈ path_image (linepath a b)" using assms z by force
ultimately have "{z, d} ⊆ ?L ∩ path_image (linepath a b) ∧ z ≠ d" using z by blast
then have "collinear {a, b, c, d}" using two_linepath_colinearity_property by fastforce
then have False using assms(2) assms(3) collinear_4_3 by auto
} moreover
{ assume **: "z ∈ path_image (linepath b c)"
then have "collinear {a, b, c, d}" using two_linepath_colinearity_property[of z _ b c c d]
by (smt (verit) "**" IntE assms(3) collinear_3_trans d_prop in_path_image_imp_collinear insertCI insert_commute z)
then have False using assms(2) assms(3) collinear_4_3 by auto
} moreover
{ assume **: "z ∈ path_image (linepath c a)"
then have "collinear {a, b, c, d}" using two_linepath_colinearity_property[of z _ c a c d]
by (smt (verit) IntD1 assms(3) collinear_3_trans d_prop in_path_image_imp_collinear insert_commute insert_iff z)
then have False using assms(2) assms(3) collinear_4_3 by auto
}
ultimately show False using cases by argo
qed
moreover have "?L ⊆ path_inside p ∪ ?P"
proof-
have "convex hull {a, b, c} = path_inside p ∪ ?P"
by (simp add: Un_commute assms(1) assms(3) triangle_convex_hull)
moreover have "?L ⊆ convex hull {a, b, c}"
by (smt (verit, ccfv_threshold) assms empty_subsetI hull_insert hull_mono insert_commute insert_mono insert_subset path_image_linepath segment_convex_hull)
ultimately show ?thesis by blast
qed
ultimately have "?L ⊆ path_inside p ∪ {c, d}" by blast
then have "?L ⊆ path_inside ?p' ∪ {c, d}" using 1 unfolding path_inside_def by presburger
then have 2: "good_linepath c d ?vts'" using assms unfolding good_linepath_def by auto
thus ?thesis using 1 by blast
qed
section "Convex Hull Has Good Linepath"
lemma leq_2_extreme_points_means_collinear:
fixes vts :: "'a::euclidean_space set"
assumes "finite vts"
assumes "card {v. v extreme_point_of (convex hull vts)} ≤ 2"
shows "collinear vts"
using assms
by (metis Krein_Milman_polytope affine_hull_convex_hull collinear_affine_hull_collinear collinear_small extreme_points_of_convex_hull finite_subset)
lemma convex_hull_non_extreme_point_in_open_seg:
assumes "H = convex hull vts"
assumes "x ∈ H - {v. v extreme_point_of H}"
shows "∃a b. a ∈ H ∧ b ∈ H ∧ x ∈ open_segment a b"
using assms unfolding extreme_point_of_def by blast
lemma convex_hull_extreme_points_vertex_split:
fixes vts :: "(real^2) set"
assumes "H = convex hull vts"
assumes "finite vts"
assumes "card {v. v extreme_point_of H} ≥ 4"
assumes "{a, b, c} ⊆ {v. v extreme_point_of H} ∧ distinct [a, b, c]"
shows "path_image (linepath a b) ∩ interior H ≠ {}
∨ path_image (linepath b c) ∩ interior H ≠ {}
∨ path_image (linepath c a) ∩ interior H ≠ {}"
proof-
let ?ep = "{v. v extreme_point_of H}"
have H: "H = convex hull ?ep" using Krein_Milman_polytope assms(1) assms(2) by blast
let ?H' = "convex hull {a, b, c}"
have not_collinear: "¬ collinear {a, b, c}"
proof(rule ccontr)
assume "¬ ¬ collinear {a, b, c}"
then have "collinear {a, b, c}" by blast
then have "a ∈ path_image (linepath b c)
∨ b ∈ path_image (linepath a c)
∨ c ∈ path_image (linepath a b)"
using collinear_between_cases unfolding between_def
by (smt (verit, del_insts) between_mem_segment closed_segment_eq collinear_between_cases doubleton_eq_iff path_image_linepath)
moreover have "a ≠ b ∧ b ≠ c ∧ a ≠ c" using assms by simp
ultimately have "a ∈ open_segment b c ∨ b ∈ open_segment a c ∨ c ∈ open_segment a b"
using closed_segment_eq_open by auto
moreover have "a extreme_point_of H ∧ b extreme_point_of H ∧ c extreme_point_of H"
using assms by blast
ultimately show False unfolding extreme_point_of_def by blast
qed
have strict_subset: "interior ?H' ⊂ interior H"
proof-
have "interior ?H' ⊆ interior H"
by (metis H assms(4) hull_mono interior_mono)
moreover have "?H' ⊂ H"
proof-
have "card {a, b, c} ≤ 3"
by (metis card.empty card_insert_disjoint collinear_2 finite.emptyI finite_insert insert_absorb nat_le_linear not_collinear numeral_3_eq_3)
then have "card (?ep - {a, b, c}) ≥ 1"
using assms(3) assms(4) by auto
then obtain d where "d ∈ ?ep - {a, b, c}"
by (metis One_nat_def all_not_in_conv card.empty not_less_eq_eq zero_le)
thus ?thesis
by (metis DiffE H assms(4) extreme_point_of_convex_hull hull_mono mem_Collect_eq order_less_le)
qed
ultimately show ?thesis
by (metis (no_types, lifting) assms(1) assms(2) closure_convex_hull convex_closure_rel_interior convex_convex_hull convex_hull_eq_empty convex_polygon_frontier_is_path_image2 dual_order.strict_iff_order finite.emptyI finite.insertI finite_imp_bounded_convex_hull finite_imp_compact frontier_empty insert_not_empty inside_frontier_eq_interior not_collinear path_inside_def polygon_frontier_is_path_image rel_interior_nonempty_interior sup_bot.right_neutral triangle_convex_hull triangle_is_convex triangle_is_polygon)
qed
moreover have "interior ?H' ≠ {}"
by (metis not_collinear convex_convex_hull convex_hull_eq_empty convex_polygon_frontier_is_path_image2 finite.emptyI finite.insertI finite_imp_bounded_convex_hull frontier_empty insert_not_empty inside_frontier_eq_interior path_inside_def polygon_frontier_is_path_image sup_bot.right_neutral triangle_convex_hull triangle_is_convex triangle_is_polygon)
ultimately obtain x y where xy: "x ∈ interior ?H' ∧ y ∈ interior H - interior ?H'" by blast
let ?l = "linepath x y"
have "x ∈ interior ?H' ∧ y ∈ -(interior ?H')" using xy by blast
then have "path_image ?l ∩ interior ?H' ≠ {} ∧ path_image ?l ∩ -(interior ?H') ≠ {}" by auto
moreover have "path_connected (interior ?H')" by (simp add: convex_imp_path_connected)
ultimately obtain z where z: "z ∈ path_image ?l ∩ frontier (interior ?H')"
by (metis Diff_eq Diff_eq_empty_iff all_not_in_conv convex_convex_hull convex_imp_path_connected path_connected_not_frontier_subset path_image_linepath segment_convex_hull)
moreover have "path_image ?l ⊆ interior H" using xy convex_interior[of H]
by (metis DiffD1 IntD2 strict_subset assms(1) closed_segment_subset convex_convex_hull inf.strict_order_iff path_image_linepath)
ultimately have z_interior: "z ∈ interior H" by blast
have "z ∈ frontier (interior ?H')" using z by blast
moreover have "frontier (interior ?H')
= path_image (linepath a b) ∪ path_image (linepath b c) ∪ path_image (linepath c a)"
proof-
let ?p = "make_triangle a b c"
have "path_inside ?p = interior ?H'"
by (metis not_collinear bounded_convex_hull bounded_empty bounded_insert convex_convex_hull convex_polygon_frontier_is_path_image2 inside_frontier_eq_interior path_inside_def triangle_convex_hull triangle_is_convex triangle_is_polygon)
then have "path_image ?p = frontier (interior ?H')"
by (metis not_collinear polygon_frontier_is_path_image triangle_is_polygon)
moreover have "path_image ?p
= path_image (linepath a b) ∪ path_image (linepath b c) ∪ path_image (linepath c a)"
by (metis Un_assoc list.discI make_polygonal_path.simps(3) make_triangle_def nth_Cons_0 path_image_cons_union)
ultimately show ?thesis by presburger
qed
ultimately show ?thesis using z_interior by blast
qed
lemma convex_hull_has_vertex_split_helper_wlog:
assumes "p = make_triangle a b c" and "distinct [a, b, c]" and "¬ collinear {a, b, c}" and
d_prop: "d ∈ path_image (linepath a b) ∧ d ∉ {a, b, c}"
shows "path_image (linepath c d) ∩ path_inside p ≠ {}"
proof-
have "good_linepath c d [a, d, b, c, a]
∧ path_image (make_polygonal_path [a, d, b, c, a]) = path_image p"
using pick_triangle_basic_split[of p a b c d] assms by fast
thus ?thesis
unfolding good_linepath_def
by (smt (verit, del_insts) Int_Un_eq(4) Int_insert_right_if1 Un_insert_right diff_points_path_image_set_property le_iff_inf path_inside_def pathfinish_in_path_image pathfinish_linepath pathstart_in_path_image pathstart_linepath)
qed
lemma convex_hull_has_vertex_split_helper:
assumes "p = make_triangle a b c" and "distinct [a, b, c]" and "¬ collinear {a, b, c}" and
d_prop: "d ∈ path_image p ∧ d ∉ {a, b, c}"
shows "∃x y. {x, y} ⊆ {a, b, c, d} ∧ x ≠ y ∧ path_image (linepath x y) ∩ path_inside p ≠ {}"
proof-
{ assume "d ∈ path_image (linepath a b)"
then have ?thesis
using convex_hull_has_vertex_split_helper_wlog[of p a b c d] assms(1) assms(2) assms(3) d_prop
by fastforce
} moreover
{ assume *: "d ∈ path_image (linepath b c)"
let ?p' = "make_triangle b c a"
have "path_image (linepath a d) ∩ path_inside ?p' ≠ {}"
using convex_hull_has_vertex_split_helper_wlog[of ?p' b c a d]
by (metis (no_types, opaque_lifting) "*" assms(3) collinear_2 d_prop distinct_length_2_or_more distinct_singleton insert_absorb2 insert_commute)
moreover have "path_inside ?p' = path_inside p"
unfolding make_triangle_def
by (smt (verit, best) assms(1) assms(3) convex_polygon_frontier_is_path_image2 insert_commute make_triangle_def path_inside_def triangle_convex_hull triangle_is_convex triangle_is_polygon)
ultimately have ?thesis using assms by auto
} moreover
{ assume *: "d ∈ path_image (linepath c a)"
let ?p' = "make_triangle c a b"
have "path_image (linepath b d) ∩ path_inside ?p' ≠ {}"
using convex_hull_has_vertex_split_helper_wlog[of ?p' c a b d]
by (metis (no_types, opaque_lifting) "*" assms(3) collinear_2 d_prop distinct_length_2_or_more distinct_singleton insert_absorb2 insert_commute)
moreover have "path_inside ?p' = path_inside p"
unfolding make_triangle_def
by (smt (verit, ccfv_SIG) assms(1) assms(3) convex_polygon_frontier_is_path_image2 insert_commute make_triangle_def path_inside_def triangle_convex_hull triangle_is_convex triangle_is_polygon)
ultimately have ?thesis using assms by auto
}
ultimately show ?thesis using on_triangle_path_image_cases assms(1) d_prop by fast
qed
lemma convex_hull_has_vertex_split:
fixes vts :: "(real^2) set"
assumes "H = convex hull vts"
assumes "¬ collinear vts"
assumes "card vts > 3"
assumes "finite vts"
shows "∃a b. {a, b} ⊆ vts ∧ a ≠ b ∧ path_image (linepath a b) ∩ interior H ≠ {}"
proof-
let ?ep = "{v. v extreme_point_of H}"
have ep: "?ep ⊆ vts" by (simp add: assms(1) extreme_points_of_convex_hull)
have card_ep: "card ?ep ≥ 3"
by (metis One_nat_def Suc_1 assms(1) assms(2) assms(3) card.infinite leq_2_extreme_points_means_collinear not_less_eq_eq not_less_zero numeral_3_eq_3)
obtain a b c where abc: "{a, b, c} ⊆ ?ep ∧ a ≠ b ∧ b ≠ c ∧ a ≠ c"
proof-
obtain a A where "a ∈ ?ep ∧ A = ?ep - {a} ∧ card A ≥ 2" using card_ep by force
moreover then obtain b B where "b ∈ A ∧ B = A - {b} ∧ card B ≥ 1"
by (metis Suc_1 Suc_diff_le bot.extremum_uniqueI bot_nat_0.extremum card_Diff_singleton card_eq_0_iff diff_Suc_1 less_Suc_eq_le less_one linorder_not_le subset_emptyI)
moreover then obtain c C where "c ∈ B ∧ C = B - {c} ∧ card C ≥ 0"
by (metis One_nat_def bot_nat_0.extremum card.empty equals0I not_less_eq_eq)
ultimately have "{a, b, c} ⊆ ?ep ∧ a ≠ b ∧ b ≠ c ∧ a ≠ c" by blast
thus ?thesis using that by auto
qed
{ assume *: "card ?ep = 3"
then have abc: "?ep = {a, b, c}"
by (metis abc card_3_iff card_gt_0_iff numeral_3_eq_3 order_less_le psubset_card_mono zero_less_Suc)
obtain d where d: "d ∈ vts ∧ d ≠ a ∧ d ≠ b ∧ d ≠ c"
by (metis "*" assms(3) abc ep insertCI nat_less_le subsetI subset_antisym)
{ assume "d ∈ interior H"
then have "d ∈ path_image (linepath a d) ∩ interior H" by simp
then have ?thesis using ep abc d by auto
} moreover
{ assume ***: "d ∉ interior H"
let ?p = "make_triangle a b c"
have H: "H = convex hull ?ep"
proof-
have "compact H"
by (metis assms(1) assms(3) card_eq_0_iff finite_imp_compact_convex_hull gr_implies_not0)
moreover have "convex H" using convex_convex_hull[of vts] assms by blast
ultimately have "H = closure (convex hull ?ep)" using Krein_Milman[of H] by fast
thus ?thesis using abc by auto
qed
then have interior: "path_inside ?p = interior H"
using abc
by (metis assms(1,2) affine_hull_convex_hull collinear_affine_hull_collinear convex_convex_hull convex_polygon_frontier_is_path_image2 finite.intros(1) finite_imp_bounded_convex_hull finite_insert inside_frontier_eq_interior path_inside_def triangle_convex_hull triangle_is_convex triangle_is_polygon)
then have d_frontier: "d ∈ frontier H"
by (metis *** Diff_iff assms(1) UnCI d closure_Un_frontier frontier_def hull_subset in_mono)
moreover have "path_image ?p = frontier H"
using convex_polygon_frontier_is_path_image
by (metis assms(1,2) H abc affine_hull_convex_hull collinear_affine_hull_collinear convex_polygon_frontier_is_path_image2 triangle_convex_hull triangle_is_convex triangle_is_polygon)
ultimately have "d ∈ path_image ?p" by blast
moreover have "¬ collinear {a, b, c}"
by (metis H assms(1,2) abc affine_hull_convex_hull collinear_affine_hull_collinear)
moreover then have "distinct [a, b, c]"
by (metis collinear_2 distinct.simps(2) distinct_singleton empty_set insert_absorb list.simps(15))
moreover have "d ∉ {a, b, c}" using d by blast
ultimately have ?thesis
using abc d convex_hull_has_vertex_split_helper[of ?p a b c d]
by (metis (no_types, lifting) insert_subset interior subset_trans ep)
}
ultimately have ?thesis by fast
} moreover
{ assume *: "card ?ep ≥ 4"
moreover have "{a, b, c} ⊆ ?ep ∧ distinct [a, b, c]" using abc by fastforce
ultimately have "path_image (linepath a b) ∩ interior H ≠ {}
∨ path_image (linepath b c) ∩ interior H ≠ {}
∨ path_image (linepath c a) ∩ interior H ≠ {}"
using convex_hull_extreme_points_vertex_split[OF assms(1) assms(4) *] by presburger
then have ?thesis
by (metis (no_types, lifting) ep abc insert_subset subset_trans)
}
ultimately show ?thesis using card_ep by fastforce
qed
lemma convex_polygon_has_good_linepath_helper:
assumes "polygon_of p vts"
assumes "convex (path_inside p ∪ path_image p)"
assumes "card (set vts) > 3"
obtains a b where "{a, b} ⊆ set vts ∧ a ≠ b ∧ ¬ path_image (linepath a b) ⊆ path_image p"
proof-
let ?H = "convex hull (set vts)"
obtain a b where ab: "{a, b} ⊆ set vts ∧ a ≠ b ∧ path_image (linepath a b) ∩ interior ?H ≠ {}"
using convex_hull_has_vertex_split assms polygon_vts_not_collinear unfolding polygon_of_def
by fastforce
moreover have "interior ?H = path_inside p"
using assms(1) assms(2) convex_polygon_inside_is_convex_hull_interior polygon_convex_iff polygon_of_def
by blast
ultimately have "path_image (linepath a b) ∩ path_inside p ≠ {}" by simp
moreover have "path_inside p ∩ path_image p = {}" using path_inside_def by auto
moreover have "path_image (linepath a b) ⊆ path_image p ∪ path_inside p"
by (metis ab assms(1) assms(2) convex_polygon_is_convex_hull hull_mono path_image_linepath polygon_of_def segment_convex_hull sup_commute)
ultimately have "¬ path_image (linepath a b) ⊆ path_image p" by fast
thus ?thesis using ab that by meson
qed
lemma convex_polygon_has_good_linepath:
assumes "convex (path_inside p ∪ path_image p)"
assumes "polygon p"
assumes "p = make_polygonal_path vts"
assumes "card (set vts) > 3"
shows "∃a b. good_linepath a b vts"
proof-
let ?T = "convex hull (set vts)"
have T: "path_image p ∪ path_inside p = ?T"
by (metis Un_commute assms(1) assms(2) assms(3) convex_polygon_is_convex_hull)
obtain a b where ab: "a ≠ b ∧ {a, b} ⊆ set vts ∧ ¬ path_image (linepath a b) ⊆ path_image p"
using convex_polygon_has_good_linepath_helper assms unfolding polygon_of_def by metis
let ?S = "path_image (linepath a b)"
have p_is_frontier: "frontier ?T = path_image p"
using convex_polygon_frontier_is_path_image assms polygon_of_def polygon_convex_iff by blast
have "closure ?T = ?T" by (simp add: finite_imp_compact)
then have "?S ⊆ closure ?T" using ab by (simp add: hull_mono segment_convex_hull)
moreover have "convex ?T" using convex_convex_hull by auto
moreover have "convex ?S" by simp
moreover have "rel_interior ?S = open_segment a b"
by (metis ab path_image_linepath rel_interior_closed_segment)
moreover have "rel_interior ?T = interior ?T"
by (metis p_is_frontier Diff_empty ab calculation(1) frontier_def rel_interior_nonempty_interior)
ultimately have "open_segment a b ⊆ interior ?T"
using subset_rel_interior_convex by (metis ab p_is_frontier frontier_def rel_frontier_def)
then have "(open_segment a b) ∩ path_image p = {}"
using p_is_frontier frontier_def by auto
then have "closed_segment a b ∩ path_image p = {a, b}"
by (metis (no_types, lifting) Int_Un_distrib2 Int_absorb2 Un_commute ab assms(3) closed_segment_eq_open subset_trans sup_bot.right_neutral vertices_on_path_image)
then have "path_image (linepath a b) ∩ path_image p = {a, b}" by simp
thus ?thesis
using ab unfolding good_linepath_def
by (smt (verit, ccfv_threshold) IntI UnCI UnE T assms(3) hull_mono path_image_linepath segment_convex_hull subset_iff)
qed
section "Pick's Theorem"
definition integral_inside:
"integral_inside p = {x. integral_vec x ∧ x ∈ path_inside p}"
definition integral_boundary:
"integral_boundary p = {x. integral_vec x ∧ x ∈ path_image p}"
subsection "Pick's Theorem Triangle Case"
definition pick_triangle:
"pick_triangle p a b c ⟷
p = make_triangle a b c
∧ all_integral [a, b, c]
∧ distinct [a, b, c]
∧ ¬ collinear {a, b, c}"
definition pick_holds:
"pick_holds p ⟷
(let I = card {x. integral_vec x ∧ x ∈ path_inside p} in
let B = card {x. integral_vec x ∧ x ∈ path_image p} in
measure lebesgue (path_inside p) = I + B/2 - 1)"
lemma pick_triangle_wlog_helper:
assumes "pick_triangle p a b c" and
"I = card (integral_inside p)" and
"B = card (integral_boundary p)" and
"integral_inside p = {}" and
"integral_vec d ∧ d ∈ path_image (linepath a b) ∧ d ∉ {a, b, c}" and "d ∉ {a, b, c}" and
ih: "∧p' a' b' c'. (card (integral_inside p') + card (integral_boundary p') < I + B) ==> pick_triangle p' a' b' c' ==> pick_holds p'"
shows "measure lebesgue (path_inside p) = I + B/2 - 1"
proof-
have polygon_p: "polygon p" using triangle_is_polygon assms unfolding pick_triangle by presburger
then have polygon_of: "polygon_of p [a, b, c, a]"
unfolding polygon_of_def using assms unfolding make_triangle_def pick_triangle by auto
let ?p' = "make_polygonal_path [a, d, b, c, a]"
have "good_linepath c d [a, d, b, c, a] ∧ path_image (make_polygonal_path [a, d, b, c, a]) = path_image p"
using pick_triangle_basic_split assms unfolding pick_triangle by presburger
then have *: "good_linepath d c [a, d, b, c, a] ∧ path_image (make_polygonal_path [a, d, b, c, a]) = path_image p"
using good_linepath_comm by blast
have polygon_new: "polygon (make_polygonal_path [a, d, b, c, a])"
using polygon_linepath_split_is_polygon[OF polygon_of, of 0 a b d "[a, d, b, c, a]"] assms
by force
have h1: "make_polygonal_path [a, d, b, c, a] = make_polygonal_path ([a, d, b, c] @ [[a, d, b, c] ! 0])"
by auto
have h2: "good_linepath d c ([a, d, b, c] @ [[a, d, b, c] ! 0])"
using * by auto
have h3: " (1::nat) < length [a, d, b, c] ∧ (3::nat) < length [a, d, b, c]"
by auto
then have polygon_split: "is_polygon_split [a, d, b, c] 1 3"
using good_linepath_implies_polygon_split[OF polygon_new h1 h2 h3] by auto
let ?p1 = "make_polygonal_path (d # [b] @ [c, d])"
let ?p2 = "make_polygonal_path ([a] @ [d, c] @ [] @ [[a, d, b, c] ! 0])"
let ?I1 = "card {x. integral_vec x ∧ x ∈ path_inside ?p1}"
let ?B1 = "card {x. integral_vec x ∧ x ∈ path_image ?p1}"
let ?I2 = "card {x. integral_vec x ∧ x ∈ path_inside ?p2}"
let ?B2 = "card {x. integral_vec x ∧ x ∈ path_image ?p2}"
have p1_triangle: "?p1 = make_triangle d b c"
unfolding make_triangle_def by auto
have p2_triangle: "?p2 = make_triangle a d c"
unfolding make_triangle_def by auto
have I_is: "I = card {x. integral_vec x ∧ x ∈ path_inside (make_polygonal_path [a, d, b, c, a])}"
using path_image_linepath_split[of 0 "[a, b, c, a]" d] "*" assms path_inside_def integral_inside by presburger
have B_is: "B = card {x. integral_vec x ∧ x ∈ path_image (make_polygonal_path [a, d, b, c, a])}"
using path_image_linepath_split[of 0 "[a, b, c, a]" d]
using "*" assms path_inside_def integral_boundary by presburger
have all_integral_assump: "all_integral [a, d, b, c]"
using assms unfolding all_integral_def pick_triangle by force
(* First inductive hypothesis *)
have dist_indh1: "distinct [d, b, c]"
using assms unfolding pick_triangle by auto
have coll_indh1: "¬ collinear {d, b, c}"
using assms pick_triangle
by (smt (verit) collinear_3_trans dist_indh1 distinct_length_2_or_more in_path_image_imp_collinear insert_commute)
have path_inside_inside: "path_inside (make_polygonal_path (d # [b] @ [c, d])) ⊆ path_inside p"
using polygon_split unfolding is_polygon_split_def
by (smt (verit) "*" One_nat_def Un_iff append_Cons append_Nil diff_Suc_1 drop0 drop_Suc_Cons nth_Cons_0 nth_Cons_Suc numeral_3_eq_3 path_inside_def subsetI take_Suc_Cons take_eq_Nil2)
then have indh1_card1: "card {x. integral_vec x ∧ x ∈ path_inside (make_polygonal_path (d # [b] @ [c, d]))}≤ card {x. integral_vec x ∧ x ∈ path_inside p}"
by (metis (no_types, lifting) assms(4) integral_inside Collect_empty_eq card.empty le_zero_eq subsetD)
have indh1_card2: "card {x. integral_vec x ∧ x ∈ path_image (make_polygonal_path (d # [b] @ [c, d]))} < card {x. integral_vec x ∧ x ∈ path_image p}"
(* Use polygon split and also that a isn't in the first set *)
proof-
have path_image_union: "path_image (make_polygonal_path (d # [b] @ [c, d])) = path_image (linepath d b) ∪ path_image (linepath b c) ∪ path_image (linepath c d)"
using path_image_cons_union p1_triangle make_triangle_def
by (metis (no_types, lifting) inf_sup_aci(6) list.discI make_polygonal_path.simps(3) nth_Cons_0)
have path_image_db: "path_image (linepath d b) ⊆ path_image p"
by (metis assms(5) list.discI nth_Cons_0 path_image_cons_union path_image_linepath_union polygon_of polygon_of_def sup.cobounded2 sup.coboundedI1)
have path_image_bc: "path_image (linepath b c) ⊆ path_image p"
using assms(1) linepaths_subset_make_polygonal_path_image[of "[a, b, c, a]" 1] unfolding pick_triangle make_triangle_def
by simp
have path_image_cd1: "path_image (linepath c d) - {c, d} ⊆ path_inside p"
using polygon_split unfolding is_polygon_split_def
by (smt (verit) One_nat_def ‹good_linepath c d [a, d, b, c, a] ∧ path_image (make_polygonal_path [a, d, b, c, a]) = path_image p› append_Cons append_Nil insert_commute nth_Cons_0 nth_Cons_Suc numeral_3_eq_3 path_image_linepath path_inside_def segment_convex_hull sup.cobounded2)
have path_image_cd2: "{c, d} ⊆ path_image p"
using linepaths_subset_make_polygonal_path_image assms(1) unfolding pick_triangle make_triangle_def
by (metis (no_types, lifting) ‹good_linepath c d [a, d, b, c, a] ∧ path_image (make_polygonal_path [a, d, b, c, a]) = path_image p› good_linepath_def subset_trans vertices_on_path_image)
have "path_image (linepath c d) ⊆ path_image p ∪ path_inside p"
using path_image_cd1 path_image_cd2 by auto
moreover have "integral_inside p = {}" using assms by force
ultimately have path_image_cd: "integral_boundary (linepath c d) ⊆ integral_boundary p" unfolding integral_inside integral_boundary by blast
have a_neq_d: "a ≠ d"
using assms(5) by auto
have a_neq_c: "a ≠ c"
using assms(1) unfolding pick_triangle by simp
have a_in_image: "a ∈ path_image p"
using assms(1) unfolding pick_triangle make_triangle_def using vertices_on_path_image
by fastforce
have "path_image (linepath c d) ∩ path_image p = {c, d}"
using * unfolding good_linepath_def
by (smt (verit, ccfv_SIG) One_nat_def h1 insert_commute is_polygon_cut_def is_polygon_split_def nth_Cons_0 nth_Cons_Suc numeral_3_eq_3 path_image_linepath polygon_split segment_convex_hull)
then have a_not_in1: "a ∉ path_image (linepath c d)"
using a_neq_c a_neq_d a_in_image by blast
have a_not_in2: "a ∉ path_image (linepath d b)"
using Int_closed_segment assms(5) by auto
have a_not_in3: "a ∉ path_image (linepath b c)"
by (metis (no_types, lifting) assms(1) in_path_image_imp_collinear insert_commute pick_triangle)
then have "a ∉ path_image (linepath d b) ∪ path_image (linepath b c) ∪ path_image (linepath c d)"
using a_not_in1 a_not_in2 a_not_in3 by simp
then have "a ∈ integral_boundary p ∧ a ∉ integral_boundary (make_polygonal_path [d, b, c, d])"
using path_image_union using integral_boundary a_in_image all_integral_assump all_integral_def by auto
then have strict_subset: "integral_boundary (make_polygonal_path [d, b, c, d]) ⊂ integral_boundary p"
using path_image_union path_image_db path_image_bc path_image_cd
unfolding integral_boundary by auto
have "integral_inside (make_polygonal_path [d, b, c, d]) = {}"
using path_inside_inside assms unfolding integral_inside by auto
then show ?thesis using assms(2-3) strict_subset bounded_finite
using finite_path_inside finite_path_image
by (simp add: integral_boundary polygon_p psubset_card_mono)
qed
have fewer_points_p1: " card {x. integral_vec x ∧ x ∈ path_inside (make_polygonal_path (d # [b] @ [c, d]))} +
card {x. integral_vec x ∧ x ∈ path_image (make_polygonal_path (d # [b] @ [c, d]))}
< card {x. integral_vec x ∧ x ∈ path_inside p} +
card {x. integral_vec x ∧ x ∈ path_image p}"
using indh1_card1 indh1_card2 by linarith
have indh_1: "Sigma_Algebra.measure lebesgue (path_inside ?p1) = real ?I1 + real ?B1 / 2 - 1"
using assms fewer_points_p1 p1_triangle all_integral_assump dist_indh1 coll_indh1 all_integral_def
unfolding pick_holds pick_triangle integral_inside integral_boundary by simp
(* Second inductive hypothesis *)
have dist_indh2: "distinct [a, d, c]"
using assms unfolding pick_triangle by auto
have coll_indh2: "¬ collinear {a, d, c}"
using assms pick_triangle
by (smt (verit) collinear_3_trans dist_indh2 distinct_length_2_or_more in_path_image_imp_collinear insert_commute)
have path_inside_inside: "path_inside (make_polygonal_path (a # [d] @ [c, a])) ⊆ path_inside p"
using polygon_split unfolding is_polygon_split_def
by (smt (verit) "*" One_nat_def Un_iff append_Cons append_Nil diff_Suc_1 drop0 drop_Suc_Cons nth_Cons_0 nth_Cons_Suc numeral_3_eq_3 path_inside_def subsetI take_Suc_Cons take_eq_Nil2)
then have indh2_card1: "card {x. integral_vec x ∧ x ∈ path_inside (make_polygonal_path (a # [d] @ [c, a]))}≤ card {x. integral_vec x ∧ x ∈ path_inside p}"
by (metis (no_types, lifting) assms(4) integral_inside Collect_empty_eq card.empty le_zero_eq subsetD)
have indh2_card2: "card {x. integral_vec x ∧ x ∈ path_image (make_polygonal_path (a # [d] @ [c, a]))} < card {x. integral_vec x ∧ x ∈ path_image p}"
(* Use polygon split and also that a isn't in the first set *)
proof-
have path_image_union: "path_image (make_polygonal_path (a # [d] @ [c, a])) = path_image (linepath a d) ∪ path_image (linepath d c) ∪ path_image (linepath c a)"
using path_image_cons_union p2_triangle make_triangle_def
by (metis Un_assoc append.left_neutral append_Cons list.discI make_polygonal_path.simps(3) nth_Cons_0)
have path_image_ad: "path_image (linepath a d) ⊆ path_image p"
by (metis ‹good_linepath c d [a, d, b, c, a] ∧ path_image (make_polygonal_path [a, d, b, c, a]) = path_image p› inf_sup_absorb le_iff_inf list.discI nth_Cons_0 path_image_cons_union)
have path_image_ca: "path_image (linepath c a) ⊆ path_image p"
using assms(1) linepaths_subset_make_polygonal_path_image[of "[a, b, c, a]" 2] unfolding pick_triangle make_triangle_def
by simp
have path_image_cd1: "path_image (linepath d c) - {c, d} ⊆ path_inside p"
using polygon_split unfolding is_polygon_split_def
by (smt (verit) One_nat_def ‹good_linepath c d [a, d, b, c, a] ∧ path_image (make_polygonal_path [a, d, b, c, a]) = path_image p› append_Cons append_Nil insert_commute nth_Cons_0 nth_Cons_Suc numeral_3_eq_3 path_image_linepath path_inside_def segment_convex_hull sup.cobounded2)
have path_image_cd2: "{c, d} ⊆ path_image p"
using linepaths_subset_make_polygonal_path_image assms(1) unfolding pick_triangle make_triangle_def
by (metis (no_types, lifting) ‹good_linepath c d [a, d, b, c, a] ∧ path_image (make_polygonal_path [a, d, b, c, a]) = path_image p› good_linepath_def subset_trans vertices_on_path_image)
have "path_image (linepath d c) ⊆ path_image p ∪ path_inside p"
using path_image_cd1 path_image_cd2 by auto
moreover have "integral_inside p = {}" using assms by force
ultimately have path_image_cd: "integral_boundary (linepath d c) ⊆ integral_boundary p" unfolding integral_inside integral_boundary by blast
have b_neq_d: "b ≠ d"
using assms(5) by auto
have b_neq_c: "b ≠ c"
using assms(1) unfolding pick_triangle by simp
have b_in_image: "b ∈ path_image p"
using assms(1) unfolding pick_triangle make_triangle_def using vertices_on_path_image
by fastforce
have "path_image (linepath d c) ∩ path_image p = {d, c}"
using * unfolding good_linepath_def
by (smt (verit, ccfv_SIG) One_nat_def h1 insert_commute is_polygon_cut_def is_polygon_split_def nth_Cons_0 nth_Cons_Suc numeral_3_eq_3 path_image_linepath polygon_split segment_convex_hull)
then have b_not_in1: "b ∉ path_image (linepath d c)"
using b_neq_c b_neq_d b_in_image by blast
have b_not_in2: "b ∉ path_image (linepath a d)"
using Int_closed_segment assms(5) by auto
have b_not_in3: "b ∉ path_image (linepath c a)"
by (metis (no_types, lifting) assms(1) in_path_image_imp_collinear insert_commute pick_triangle)
then have "b ∉ path_image (linepath a d) ∪ path_image (linepath d c) ∪ path_image (linepath c a)"
using b_not_in1 b_not_in2 b_not_in3 by simp
then have "b ∈ integral_boundary p ∧ b ∉ integral_boundary (make_polygonal_path [a, d, c, a])"
using path_image_union using integral_boundary b_in_image all_integral_assump all_integral_def by auto
then have strict_subset: "integral_boundary (make_polygonal_path [a, d, c, a]) ⊂ integral_boundary p"
using path_image_union path_image_ad path_image_ca path_image_cd
unfolding integral_boundary by auto
have "integral_inside (make_polygonal_path [a, d, c, a]) = {}"
using path_inside_inside assms unfolding integral_inside by auto
then show ?thesis using assms(2-3) strict_subset bounded_finite
using finite_path_inside finite_path_image
by (simp add: integral_boundary polygon_p psubset_card_mono)
qed
have fewer_points_p2: " card {x. integral_vec x ∧ x ∈ path_inside (make_polygonal_path ([a, d, c, a]))} +
card {x. integral_vec x ∧ x ∈ path_image (make_polygonal_path ([a, d, c, a]))}
< card {x. integral_vec x ∧ x ∈ path_inside p} +
card {x. integral_vec x ∧ x ∈ path_image p}"
using indh2_card1 indh2_card2 by simp
have indh_2: "Sigma_Algebra.measure lebesgue (path_inside ?p2) = real ?I2 + real ?B2 / 2 - 1"
using fewer_points_p2 using assms fewer_points_p2 p2_triangle all_integral_assump dist_indh2 coll_indh2 all_integral_def
unfolding pick_holds pick_triangle integral_inside integral_boundary by simp
(* Use the induction *)
have "Sigma_Algebra.measure lebesgue (path_inside ?p1) = real ?I1 + real ?B1 / 2 - 1 ==>
Sigma_Algebra.measure lebesgue (path_inside ?p2) = real ?I2 + real ?B2 / 2 - 1 ==>
I = card {x. integral_vec x ∧ x ∈ path_inside (make_polygonal_path [a, d, b, c, a])} ==>
B = card {x. integral_vec x ∧ x ∈ path_image (make_polygonal_path [a, d, b, c, a])} ==>
all_integral [a, d, b, c] ==>
Sigma_Algebra.measure lebesgue (path_inside (make_polygonal_path [a, d, b, c, a])) =
real I + real B / 2 - 1"
using pick_split_union[OF polygon_split, of "[a]" "[b]" "[]" d c ?p'] by auto
then have "Sigma_Algebra.measure lebesgue (path_inside (make_polygonal_path [a, d, b, c, a])) =
real I + real B / 2 - 1"
using I_is B_is all_integral_assump indh_1 indh_2 by auto
thus "measure lebesgue (path_inside p) = I + B/2 - 1"
using path_image_linepath_split[of 0 "[a, b, c, a]" d] by (metis path_inside_def *)
qed
lemma pick_triangle_helper:
assumes "pick_triangle p a b c" and
"I = card (integral_inside p)" and
"B = card (integral_boundary p)" and
"integral_inside p = {}" and
"integral_vec d ∧ d ∉ {a, b, c}" and "d ∉ {a, b, c}" and
"d ∈ path_image (linepath a b)
∨ d ∈ path_image (linepath b c)
∨ d ∈ path_image (linepath c a)" and
ih: "∧p' a' b' c'. (card (integral_inside p') + card (integral_boundary p') < I + B) ==> pick_triangle p' a' b' c' ==> pick_holds p'"
shows "measure lebesgue (path_inside p) = I + B/2 - 1"
proof-
{ assume "d ∈ path_image (linepath a b)"
then have ?thesis using pick_triangle_wlog_helper assms by blast
} moreover
{ assume *: "d ∈ path_image (linepath b c)"
let ?p' = "make_polygonal_path (rotate_polygon_vertices [a, b, c, a] 1)"
let ?I' = "card (integral_inside ?p')"
let ?B' = "card (integral_boundary ?p')"
have p'_p: "path_image ?p' = path_image p ∧ path_inside ?p' = path_inside p"
unfolding path_inside_def
using assms(1) make_triangle_def pick_triangle polygon_vts_arb_rotation triangle_is_polygon
by auto
have "rotate_polygon_vertices [a, b, c, a] 1 = [b, c, a, b]"
unfolding rotate_polygon_vertices_def by simp
then have pick_triangle_p': "pick_triangle ?p' b c a"
using assms unfolding pick_triangle
by (smt (verit, best) all_integral_def distinct_length_2_or_more insert_commute list.simps(15) make_triangle_def)
then have "measure lebesgue (path_inside ?p') = ?I' + ?B'/2 - 1"
using pick_triangle_wlog_helper[of ?p' b c a ?I' ?B' d] assms
using integral_boundary integral_inside * insert_commute pick_triangle_p' p'_p
by auto
moreover have "?I' = I ∧ ?B' = B" using p'_p integral_boundary integral_inside assms(2) assms(3) by presburger
ultimately have ?thesis using p'_p by auto
} moreover
{ assume *: "d ∈ path_image (linepath c a)"
let ?p' = "make_polygonal_path (rotate_polygon_vertices [a, b, c, a] 2)"
let ?I' = "card (integral_inside ?p')"
let ?B' = "card (integral_boundary ?p')"
have p'_p: "path_image ?p' = path_image p ∧ path_inside ?p' = path_inside p"
unfolding path_inside_def
using assms(1) make_triangle_def pick_triangle polygon_vts_arb_rotation triangle_is_polygon
by auto
have "rotate_polygon_vertices [a, b, c, a] 1 = [b, c, a, b]"
unfolding rotate_polygon_vertices_def by simp
also have "rotate_polygon_vertices ... 1 = [c, a, b, c]"
unfolding rotate_polygon_vertices_def by simp
ultimately have "rotate_polygon_vertices [a, b, c, a] 2 = [c, a, b, c]"
by (metis Suc_1 arb_rotation_as_single_rotation)
then have pick_triangle_p': "pick_triangle ?p' c a b"
using assms unfolding pick_triangle
by (smt (verit, best) all_integral_def distinct_length_2_or_more insert_commute list.simps(15) make_triangle_def)
then have "measure lebesgue (path_inside ?p') = ?I' + ?B'/2 - 1"
using pick_triangle_wlog_helper[of ?p' c a b ?I' ?B' d] assms
using integral_boundary integral_inside * insert_commute pick_triangle_p' p'_p
by auto
moreover have "?I' = I ∧ ?B' = B" using p'_p integral_boundary integral_inside assms(2) assms(3) by presburger
ultimately have ?thesis using p'_p by auto
}
ultimately show ?thesis using assms by blast
qed
lemma triangle_3_split_helper:
fixes a b :: "'a::euclidean_space"
assumes "a ∈ frontier S"
assumes "b ∈ interior S"
assumes "convex S"
assumes "closed S"
shows "path_image (linepath a b) ∩ frontier S = {a}"
proof-
let ?L = "path_image (linepath a b)"
have "a ∈ S ∧ b ∈ S" using assms frontier_subset_closed interior_subset by auto
then have "?L ⊆ S"
using assms hull_minimal segment_convex_hull by (simp add: closed_segment_subset)
then have "?L ⊆ closure S" using assms(4) by auto
moreover have "convex ?L" by simp
moreover have "?L ∩ interior S ≠ {}" using assms(2) by auto
moreover then have "¬ ?L ⊆ rel_frontier S"
by (metis DiffE assms(2) interior_subset_rel_interior pathfinish_in_path_image pathfinish_linepath rel_frontier_def subsetD)
ultimately have "rel_interior ?L ⊆ rel_interior S"
using subset_rel_interior_convex[of ?L S] assms by fastforce
then have "open_segment a b ⊆ interior S"
by (metis all_not_in_conv assms(2) empty_subsetI open_segment_eq_empty' path_image_linepath rel_interior_closed_segment rel_interior_nonempty_interior)
moreover have "?L = closed_segment a b" by auto
moreover have "interior S ∩ frontier S = {}" by (simp add: frontier_def)
ultimately have "?L ∩ frontier S ⊆ {a, b}"
by (smt (verit) Diff_iff disjoint_iff inf_commute inf_le1 open_segment_def subsetD subsetI)
moreover have "b ∉ frontier S" by (simp add: assms(2) frontier_def)
ultimately show ?thesis using assms(1) by auto
qed
lemma unit_triangle_interior_point_not_collinear_e1_e2:
assumes "p = make_triangle (vector [0, 0]) (vector [1, 0]) (vector [0, 1])"
(is "p = make_triangle ?O ?e1 ?e2")
assumes "z ∈ path_inside p"
shows "¬ collinear {?O, ?e1, z}"
proof-
have "path_inside p = interior (convex hull {?O, ?e1, ?e2})"
by (metis assms(1) bounded_convex_hull bounded_empty bounded_insert convex_convex_hull convex_polygon_frontier_is_path_image2 inside_frontier_eq_interior path_inside_def triangle_convex_hull triangle_is_convex triangle_is_polygon unit_triangle_vts_not_collinear)
then have "z ∈ interior (convex hull {?O, ?e1, ?e2})" using assms by simp
then have z: "z$1 > 0 ∧ z$2 > 0"
using assms(1) assms(2) unit_triangle_interior_char make_triangle_def by blast
have abc: "?O$1 = 0 ∧ ?O$2 = 0 ∧ ?e1$2 = 0 ∧ ?e2$1 = 0" by simp
show "¬ collinear {?O, ?e1, z}"
proof(rule ccontr)
assume "¬ ¬ collinear {?O, ?e1, z}"
then have *: "collinear {?O, ?e1, z}" by blast
then obtain u c1 c2 where u: "?O - ?e1 = c1 *R u ∧ ?e1 - z = c2 *R u"
unfolding collinear_def by blast
moreover have "c1 ≠ 0"
proof-
have "(?O - ?e1)$1 = -1" by simp
moreover have "(?O - ?e1)$1 = (c1 *R u)$1" using u by presburger
ultimately show ?thesis by force
qed
moreover have "(?O - ?e1)$2 = 0" by simp
moreover have "(?O - ?e1)$2 = (c1 *R u)$2" by (simp add: calculation(1))
ultimately have "u$2 = 0" by auto
thus False
by (smt (verit, ccfv_threshold) u abc scaleR_eq_0_iff vector_minus_component vector_scaleR_component z)
qed
qed
lemma triangle_interior_point_not_collinear_vertices_wlog_helper:
assumes "p = make_triangle a b c"
assumes "polygon p"
assumes "z ∈ path_inside p"
shows "¬ collinear {a, b, z}"
proof-
let ?O = "(vector [0, 0])::(real^2)"
let ?e1 = "(vector [1, 0])::(real^2)"
let ?e2 = "(vector [0, 1])::(real^2)"
let ?M = "triangle_affine a b c"
have a: "?M ?O = a"
using triangle_affine_e1_e2 by blast
have b: "?M ?e1 = b" using triangle_affine_e1_e2 by simp
have c: "?M ?e2 = c" using triangle_affine_e1_e2 by simp
have abc_not_collinear: "¬ collinear {a, b, c}"
using assms polygon_vts_not_collinear unfolding make_triangle_def polygon_of_def
by (metis (no_types, lifting) empty_set insertCI insert_absorb insert_commute list.simps(15))
have "convex hull {a, b, c} = convex hull {?M ?O, ?M ?e1, ?M ?e2}"
using a b c by simp
also have "... = ?M ` (convex hull {?O, ?e1, ?e2})"
using calculation triangle_affine_img by blast
also have interior_preserve: "interior ... = ?M ` (interior (convex hull {?O, ?e1, ?e2}))"
using triangle_affine_preserves_interior[of ?M a b c _ "convex hull {?O, ?e1, ?e2}"]
using abc_not_collinear
by presburger
finally have z: "z ∈ ?M ` (interior (convex hull {?O, ?e1, ?e2}))"
using assms(1) assms(2) assms(3) make_triangle_def polygon_of_def triangle_inside_is_convex_hull_interior
by auto
then obtain z' where z': "z' ∈ interior (convex hull {?O, ?e1, ?e2}) ∧ ?M z' = z" by fast
then have "¬ collinear {?O, ?e1, z'}"
by (metis convex_convex_hull convex_polygon_frontier_is_path_image2 finite.intros(1) finite_imp_bounded_convex_hull finite_insert inside_frontier_eq_interior path_inside_def triangle_convex_hull triangle_is_convex triangle_is_polygon unit_triangle_interior_point_not_collinear_e1_e2 unit_triangle_vts_not_collinear)
then have z'_notin: "z' ∉ affine hull {?O, ?e1}" using affine_hull_3_imp_collinear by blast
then have "?M z' ∉ affine hull {?M ?O, ?M ?e1}"
proof-
have "inj ?M" using triangle_affine_inj abc_not_collinear by blast
then have "?M z' ∉ ?M ` (affine hull {?O, ?e1})" using z'_notin by (simp add: inj_image_mem_iff)
moreover have "?M ` (affine hull {?O, ?e1}) = affine hull {?M ?O, ?M ?e1}"
using triangle_affine_preserves_affine_hull[of _ a b c] abc_not_collinear by simp
ultimately show ?thesis by blast
qed
then have "z ∉ affine hull {a, b}" using a b z' by argo
thus ?thesis
by (metis interior_preserve z affine_hull_convex_hull affine_hull_nonempty_interior collinear_2 collinear_3_affine_hull collinear_affine_hull_collinear empty_iff insert_absorb2 triangle_affine_img unit_triangle_vts_not_collinear z')
qed
lemma triangle_interior_point_not_collinear_vertices:
assumes "p = make_triangle a b c"
assumes "polygon p"
assumes "z ∈ path_inside p"
shows "¬ collinear {a, b, z} ∧ ¬ collinear {a, c, z} ∧ ¬ collinear {b, c, z}"
proof-
let ?p1 = "make_triangle b c a"
let ?p2 = "make_triangle c a b"
have p1: "?p1 = make_polygonal_path (rotate_polygon_vertices [a, b, c, a] 1)"
using assms unfolding make_triangle_def rotate_polygon_vertices_def by fastforce
have p2: "?p2 = make_polygonal_path (rotate_polygon_vertices [a, b, c, a] 2)"
using assms unfolding make_triangle_def rotate_polygon_vertices_def by (simp add: numeral_Bit0)
have "path_inside ?p1 = path_inside p ∧ path_inside ?p2 = path_inside p"
using p1 p2 unfolding path_inside_def
using assms(1) assms(2) make_triangle_def polygon_vts_arb_rotation by force
then have "z ∈ path_inside ?p1 ∧ z ∈ path_inside ?p2" using assms by force
moreover have "polygon ?p1 ∧ polygon ?p2"
using assms make_triangle_def p1 p2 rotation_is_polygon by presburger
ultimately show ?thesis
using assms triangle_interior_point_not_collinear_vertices_wlog_helper
by (smt (verit, best) insert_commute)
qed
lemma triangle_3_split:
assumes "p = make_triangle a b c"
assumes "polygon p"
assumes "z ∈ path_inside p"
shows "is_polygon_split_path [a, b, c] 0 1 [z]"
"is_polygon_split [a, z, b, c] 1 3"
"a ∉ path_image (make_triangle z b c) ∪ path_inside (make_triangle z b c)"
"b ∉ path_image (make_triangle a z c) ∪ path_inside (make_triangle a z c)"
"c ∉ path_image (make_triangle a b z) ∪ path_inside (make_triangle a b z)"
proof-
let ?q = "make_polygonal_path [a, z, b, c, a]"
let ?cutpath = "make_polygonal_path [a, z, b]"
let ?vts = "[a, b, c, a]"
let ?l1 = "linepath a z"
let ?l2 = "linepath z b"
let ?S = "path_inside p ∪ path_image p"
have "convex (path_inside p)"
using triangle_is_convex assms(1,2) polygon_vts_not_collinear unfolding make_triangle_def
by (simp add: polygon_of_def triangle_inside_is_convex_hull_interior)
then have convex: "convex (path_inside p ∪ path_image p)"
using polygon_convex_iff assms(2) by simp
then have frontier: "frontier ?S = path_image p"
using convex_polygon_frontier_is_path_image3 by (simp add: assms(2) sup_commute)
have interior: "interior ?S = path_inside p"
by (metis Jordan_inside_outside_real2 closed_path_def ‹convex (path_inside p)› assms(2) closure_Un_frontier convex_interior_closure interior_open path_inside_def polygon_def)
have not_collinear: "¬ collinear {a, b, z} ∧ ¬ collinear {a, c, z} ∧ ¬ collinear {b, c, z}"
using triangle_interior_point_not_collinear_vertices assms(1) assms(2) assms(3) by blast
have "a = pathstart ?cutpath ∧ b = pathfinish ?cutpath" by simp
moreover have "a ≠ b"
by (metis assms(1) assms(2) constant_linepath_is_not_loop_free make_polygonal_path.simps(4) make_triangle_def not_loop_free_first_component polygon_def simple_path_def)
moreover have "polygon p" by (simp add: assms(2))
moreover have "{a, b} ⊆ set ?vts" by force
moreover have "simple_path ?cutpath"
by (simp add: insert_commute not_collinear not_collinear_loopfree_path simple_path_def)
moreover have "path_image ?cutpath ∩ path_image p = {a, b}"
proof-
have "{a, b} ⊆ path_image ?cutpath ∩ path_image p"
by (metis (no_types, lifting) Int_subset_iff Un_subset_iff assms(1) insert_is_Un list.simps(15) make_triangle_def vertices_on_path_image)
moreover have "path_image ?cutpath ∩ path_image p ⊆ {a, b}"
proof-
have "z ∈ interior ?S" using assms interior by fast
moreover then have "a ∈ frontier ?S ∧ b ∈ frontier ?S"
using vertices_on_path_image
using ‹{a, b} ⊆ path_image (make_polygonal_path [a, z, b]) ∩ path_image p› frontier by force
moreover have "closed ?S" using frontier frontier_subset_eq by auto
ultimately have "path_image ?l1 ∩ path_image p = {a} ∧ path_image ?l2 ∩ path_image p = {b}"
using triangle_3_split_helper convex frontier
by (metis (no_types, lifting) insert_commute path_image_linepath segment_convex_hull)
moreover have "path_image ?cutpath = path_image ?l1 ∪ path_image ?l2"
by (metis list.discI make_polygonal_path.simps(3) nth_Cons_0 path_image_cons_union)
ultimately show ?thesis by blast
qed
ultimately show ?thesis by blast
qed
moreover have "path_image ?cutpath ∩ path_inside p ≠ {}"
by (metis (no_types, opaque_lifting) Int_Un_distrib2 Un_absorb2 Un_empty assms(3) insert_disjoint(2) list.simps(15) vertices_on_path_image)
ultimately have cutpath: "is_polygon_cut_path ?vts ?cutpath"
using assms unfolding make_triangle_def is_polygon_cut_path_def by simp
thus 1: "is_polygon_split_path [a, b, c] 0 1 [z]"
using polygon_cut_path_to_split_path assms(2) by (simp add: assms(1,2) make_triangle_def)
let ?l = "linepath z c"
let ?vts = "[a, z, b, c, a]"
have c_noton_cutpath: "c ∉ path_image ?cutpath"
by (smt (verit) UnE assms(1) assms(2) assms(3) in_path_image_imp_collinear insert_commute make_polygonal_path.simps(3) neq_Nil_conv nth_Cons_0 path_image_cons_union triangle_interior_point_not_collinear_vertices)
have "z ≠ c"
proof-
have "c ∈ path_image p"
by (metis assms(1) insert_subset list.simps(15) make_triangle_def vertices_on_path_image)
moreover have "path_image p ∩ path_inside p = {}"
by (simp add: disjoint_iff inside_def path_inside_def)
ultimately show ?thesis using assms(3) by blast
qed
moreover have polygon_q: "polygon ?q"
using 1
using nth_Cons_0 by (fastforce simp: is_polygon_split_path_def)
moreover have "{z, c} ⊆ set ?vts" by force
moreover have l_q_int: "path_image ?l ∩ path_image ?q = {z, c}"
proof-
have "{z, c} ⊆ path_image ?l ∩ path_image ?q"
by (metis (no_types, lifting) Int_subset_iff calculation(3) dual_order.trans hull_subset path_image_linepath segment_convex_hull vertices_on_path_image)
moreover
{ fix x
assume *: "x ∈ path_image ?l ∩ path_image ?q ∧ x ≠ z ∧ x ≠ c"
then have "x ∈ path_image ?q" by blast
then have "x ∈ path_image (linepath a z)
∨ x ∈ path_image (linepath z b)
∨ x ∈ path_image (linepath b c)
∨ x ∈ path_image (linepath c a)"
by (metis UnE list.discI make_polygonal_path.simps(3) nth_Cons_0 path_image_cons_union)
moreover
{ assume "x ∈ path_image (linepath a z)"
then have "x ∈ path_image (linepath a z) ∧ x ∈ path_image (linepath z c)" using * by blast
moreover have "z ∈ path_image (linepath a z) ∧ z ∈ path_image (linepath z c)" by simp
moreover have "x ≠ z" using * by blast
ultimately have "collinear {a, z, c}"
by (smt (verit, best) collinear_3_trans in_path_image_imp_collinear insert_commute)
then have False using not_collinear by (simp add: insert_commute)
} moreover
{ assume "x ∈ path_image (linepath z b)"
then have "x ∈ path_image (linepath z b) ∧ x ∈ path_image (linepath z c)" using * by blast
moreover have "z ∈ path_image (linepath z b) ∧ z ∈ path_image (linepath z c)" by simp
moreover have "x ≠ z" using * by blast
ultimately have "collinear {z, b, c}"
by (smt (verit, best) collinear_3_trans in_path_image_imp_collinear insert_commute)
then have False using not_collinear by (simp add: insert_commute)
} moreover
{ assume "x ∈ path_image (linepath b c)"
then have "x ∈ path_image (linepath b c) ∧ x ∈ path_image (linepath z c)" using * by blast
moreover have "c ∈ path_image (linepath b c) ∧ z ∈ path_image (linepath z c)" by simp
moreover have "x ≠ c" using * by blast
ultimately have "collinear {b, z, c}"
by (smt (verit, best) collinear_3_trans in_path_image_imp_collinear insert_commute)
then have False using not_collinear by (simp add: insert_commute)
} moreover
{ assume "x ∈ path_image (linepath c a)"
then have "x ∈ path_image (linepath c a) ∧ x ∈ path_image (linepath z c)" using * by blast
moreover have "c ∈ path_image (linepath c a) ∧ z ∈ path_image (linepath z c)" by simp
moreover have "x ≠ c" using * by blast
ultimately have "collinear {a, z, c}"
by (smt (verit, best) collinear_3_trans in_path_image_imp_collinear insert_commute)
then have False using not_collinear by (simp add: insert_commute)
}
ultimately have False by blast
}
ultimately show ?thesis by blast
qed
moreover have "path_image ?l ∩ path_inside ?q ≠ {}"
proof(rule ccontr)
let ?p' = "make_triangle a b z"
assume "¬ path_image ?l ∩ path_inside ?q ≠ {}"
then have "path_image ?l ∩ path_inside ?q = {}" by blast
then have *: "rel_interior (path_image ?l) ∩ path_inside ?q = {}"
by (meson disjoint_iff rel_interior_subset subset_eq)
have "path_image ?l ⊆ path_image p ∪ path_inside p"
by (metis UnCI assms(1) assms(3) empty_subsetI hull_minimal insert_subset list.simps(15) local.convex make_triangle_def path_image_linepath segment_convex_hull sup_commute vertices_on_path_image)
then have "path_image ?l ⊆ convex hull {a, b, c}"
by (smt (verit, best) assms(1) convex_polygon_is_convex_hull cutpath empty_set insertCI insert_absorb insert_commute is_polygon_cut_path_def list.simps(15) local.convex make_triangle_def sup_commute)
then have "rel_interior (path_image ?l) ⊆ interior (convex hull {a, b, c})"
by (smt (verit, ccfv_threshold) Diff_disjoint IntE IntI Un_upper1 assms(1) assms(2) assms(3) calculation(4) closure_Un_frontier convex_polygon_is_convex_hull convex_segment(1) dual_order.trans empty_iff empty_set insertCI insert_absorb2 insert_commute interior list.simps(15) local.convex make_triangle_def path_image_linepath rel_frontier_def rel_interior_nonempty_interior subsetD subset_rel_interior_convex)
then have rel_interior: "rel_interior (path_image ?l) ⊆ path_inside p"
by (smt (verit, best) assms(1) convex_polygon_is_convex_hull cutpath empty_set insertCI insert_absorb insert_commute interior is_polygon_cut_path_def list.simps(15) local.convex make_triangle_def)
have "(let vts1 = []; vts2 = [];
vts3 = [c]; x = a; y = b;
cutpath = ?cutpath; p = make_polygonal_path ([a, b, c] @ [[a, b, c] ! 0]);
p1 = make_polygonal_path (x # vts2 @ [y] @ rev [z] @ [x]);
p2 = make_polygonal_path (vts1 @ ([x] @ [z] @ [y]) @ vts3 @ [[a, b, c] ! 0]);
c1 = make_polygonal_path (x # vts2 @ [y]); c2 = make_polygonal_path (vts1 @ ([x] @ [z] @ [y]) @ vts3)
in is_polygon_cut_path ([a, b, c] @ [[a, b, c] ! 0]) ?cutpath ∧
polygon p ∧
polygon p1 ∧
polygon p2 ∧
path_inside p1 ∩ path_inside p2 = {} ∧
path_inside p1 ∪ path_inside p2 ∪ (path_image cutpath - {x, y}) = path_inside p ∧
(path_image p1 - path_image cutpath) ∩ (path_image p2 - path_image ?cutpath) = {} ∧
path_image p = path_image p1 - path_image ?cutpath ∪ (path_image p2 - path_image ?cutpath) ∪ {x, y})"
using 1 unfolding is_polygon_split_path_def by fastforce
then have "(let
p = make_polygonal_path ([a, b, c] @ [[a, b, c] ! 0]);
p1 = make_polygonal_path (a # [] @ [b] @ rev [z] @ [a]);
p2 = make_polygonal_path ([] @ ([a] @ [z] @ [b]) @ [c] @ [[a, b, c] ! 0])
in path_inside p1 ∪ path_inside p2 ∪ (path_image ?cutpath - {a, b}) = path_inside p
∧ (path_image p1 - path_image ?cutpath) ∩ (path_image p2 - path_image ?cutpath) = {})"
by meson
moreover have "?q = make_polygonal_path ([] @ ([a] @ [z] @ [b]) @ [c] @ [[a, b, c] ! 0])"
by simp
moreover have "?p' = make_polygonal_path (a # [] @ [b] @ rev [z] @ [a])"
unfolding make_triangle_def by simp
moreover have "p = make_polygonal_path ([a, b, c] @ [[a, b, c] ! 0])"
unfolding assms make_triangle_def by auto
ultimately have path_inside_p: "path_inside ?p'
∪ path_inside ?q
∪ (path_image ?cutpath - {a, b}) = path_inside p
∧ (path_image ?p' - path_image ?cutpath) ∩ (path_image ?q - path_image ?cutpath) = {}"
using 1 unfolding make_triangle_def is_polygon_split_path_def by metis
moreover have "a ∈ path_image ?cutpath ∧ a ∉ path_inside ?p' ∪ path_inside ?q"
by (metis (no_types, lifting) UnI1 ‹a = pathstart (make_polygonal_path [a, z, b]) ∧ b = pathfinish (make_polygonal_path [a, z, b])› assms(1) assms(2) collinear_2 insert_absorb2 insert_commute path_inside_p pathstart_in_path_image triangle_interior_point_not_collinear_vertices_wlog_helper)
moreover have "b ∈ path_image ?cutpath ∧ b ∉ path_inside ?p' ∪ path_inside ?q"
by (metis UnI1 ‹a = pathstart (make_polygonal_path [a, z, b]) ∧ b = pathfinish (make_polygonal_path [a, z, b])› assms(1) assms(2) collinear_2 insert_absorb2 path_inside_p pathfinish_in_path_image triangle_interior_point_not_collinear_vertices_wlog_helper)
ultimately have "rel_interior (path_image ?l) ⊆
(path_inside ?p' - path_image ?cutpath)
∪ (path_image ?cutpath - {a, b})"
using rel_interior * by blast
then have "rel_interior (path_image ?l) ⊆ path_inside ?p' ∪ path_image ?cutpath" by blast
moreover have "path_image ?cutpath ⊆ path_image ?p'"
proof-
have "path_image ?cutpath = path_image (linepath a z) ∪ path_image (linepath z b)"
by (metis list.discI make_polygonal_path.simps(3) nth_Cons_0 path_image_cons_union)
moreover have "path_image (linepath a z) = path_image (linepath z a)
∧ path_image (linepath z b) = path_image (linepath b z)"
by (simp add: insert_commute)
moreover have "path_image (linepath z a) ⊆ path_image ?p'
∧ path_image (linepath b z) ⊆ path_image ?p'"
unfolding make_triangle_def
by (metis Un_commute Un_upper2 list.discI nth_Cons_0 path_image_cons_union sup.coboundedI2)
ultimately show ?thesis by blast
qed
ultimately have "rel_interior (path_image ?l) ⊆ path_inside ?p' ∪ path_image ?p'" by fast
then have "rel_interior (path_image ?l) ⊆ convex hull {a, z, b}"
unfolding make_triangle_def
by (simp add: insert_commute make_triangle_def not_collinear sup_commute triangle_convex_hull)
then have "closure (rel_interior (path_image ?l)) ⊆ closure (convex hull {a, z, b})"
using closure_mono by blast
then have "path_image ?l ⊆ convex hull {a, z, b}" by (simp add: convex_closure_rel_interior)
then have c: "c ∈ path_image ?p' ∪ path_inside ?p'"
unfolding make_triangle_def
by (metis (no_types, lifting) IntE insertCI insert_commute l_q_int make_triangle_def not_collinear subsetD triangle_convex_hull)
moreover have "c ∉ path_image ?p'"
proof-
have "c ∈ path_image ?q - path_image ?cutpath" using c_noton_cutpath l_q_int by auto
moreover have "(path_image ?p' - path_image ?cutpath) ∩ (path_image ?q - path_image ?cutpath) = {}"
using path_inside_p by fastforce
ultimately show ?thesis by blast
qed
moreover have "c ∉ path_inside ?p'"
by (smt (verit, ccfv_threshold) DiffI IntD1 UnI1 UnI2 ‹path_image (make_polygonal_path [a, z, b]) ∩ path_image p = {a, b}› ‹path_image (make_polygonal_path [a, z, b]) ⊆ path_image (make_triangle a b z)› assms(1) assms(2) calculation(2) collinear_2 in_mono insert_absorb2 path_inside_p triangle_interior_point_not_collinear_vertices)
ultimately show False by blast
qed
ultimately have cutpath: "is_polygon_cut ?vts z c"
using assms unfolding make_triangle_def is_polygon_cut_def by blast
thus 2: "is_polygon_split [a, z, b, c] 1 3"
using polygon_cut_to_split
by (metis One_nat_def append_Cons append_Nil diff_Suc_1 length_Cons length_greater_0_conv lessI list.discI list.size(3) nth_Cons_0 nth_Cons_Suc numeral_3_eq_3 polygon_cut_to_split zero_less_diff)
let ?p1 = "make_triangle a z c"
let ?p2 = "make_triangle z b c"
let ?p3 = "make_triangle a b z"
have "(path_image ?p1 - path_image (linepath z c)) ∩ (path_image ?p2 - path_image (linepath z c)) = {}"
using 2 unfolding make_triangle_def is_polygon_split_def
by (smt (z3) Int_commute One_nat_def Suc_1 append_Cons append_Nil diff_numeral_Suc diff_zero drop0 drop_Suc_Cons nth_Cons_0 nth_Cons_Suc nth_Cons_numeral pred_numeral_simps(3) take0 take_Cons_numeral take_Suc_Cons)
moreover have "a ∉ path_image (linepath z c) ∧ b ∉ path_image (linepath z c)"
by (metis (no_types, lifting) assms(1) assms(2) assms(3) in_path_image_imp_collinear insert_commute triangle_interior_point_not_collinear_vertices)
moreover have "a ∈ path_image ?p1 ∧ b ∈ path_image ?p2"
by (metis insert_subset list.simps(15) make_triangle_def vertices_on_path_image)
ultimately have "a ∉ path_image ?p2 ∧ b ∉ path_image ?p1" by auto
moreover have "a ∉ path_inside ?p2 ∧ b ∉ path_inside ?p1"
proof-
have "a ∉ path_inside p"
by (metis (no_types, lifting) assms(1) assms(2) collinear_2 insertCI insert_absorb triangle_interior_point_not_collinear_vertices)
moreover have "b ∉ path_inside p"
using assms(1) assms(2) triangle_interior_point_not_collinear_vertices_wlog_helper by fastforce
moreover have "path_inside ?p2 ⊆ path_inside ?q"
using 2 unfolding is_polygon_split_def
by (smt (verit) One_nat_def UnCI append_Cons diff_Suc_1 drop0 drop_Suc_Cons make_triangle_def nth_Cons_0 nth_Cons_Suc numeral_3_eq_3 self_append_conv2 subsetI take0 take_Suc_Cons)
moreover have "path_inside ?p1 ⊆ path_inside ?q"
using 2 unfolding is_polygon_split_def
by (smt (verit) One_nat_def Un_assoc append_Cons diff_Suc_1 drop0 drop_Suc_Cons inf_sup_absorb le_iff_inf make_triangle_def nth_Cons_0 nth_Cons_Suc numeral_3_eq_3 self_append_conv2 sup_commute take0 take_Suc_Cons)
moreover have "path_inside ?q ⊆ path_inside p"
using 1 unfolding is_polygon_split_path_def
by (smt (verit) One_nat_def Un_subset_iff Un_upper1 append_Cons append_Nil assms(1) diff_zero drop0 drop_Suc_Cons make_triangle_def nth_Cons_0 nth_Cons_Suc take0)
ultimately show ?thesis by blast
qed
moreover show "a ∉ path_image ?p2 ∪ path_inside ?p2" using calculation by simp
ultimately show "b ∉ path_image ?p1 ∪ path_inside ?p1" by simp
have "(path_image ?p3 - path_image ?cutpath) ∩ (path_image ?q - path_image ?cutpath) = {}"
using 1 unfolding make_triangle_def is_polygon_split_path_def
by (smt (verit) One_nat_def append_Cons append_Nil diff_self_eq_0 diff_zero drop0 drop_Suc_Cons nth_Cons_0 nth_Cons_Suc rev_singleton_conv take_0)
moreover have "c ∈ path_image ?q" using l_q_int by auto
ultimately have "c ∉ path_image ?p3" using c_noton_cutpath by blast
moreover have "c ∉ path_inside ?p3"
proof-
have "c ∉ path_inside p"
using assms(1) assms(2) triangle_interior_point_not_collinear_vertices by fastforce
moreover have "path_inside ?p3 ⊆ path_inside p"
using 1 unfolding is_polygon_split_path_def
by (smt (z3) One_nat_def Un_assoc Un_upper1 append_Cons append_Nil assms(1) diff_Suc_Suc diff_zero make_triangle_def nth_Cons_0 nth_Cons_Suc rev_singleton_conv take0)
ultimately show ?thesis by blast
qed
ultimately show "c ∉ path_image ?p3 ∪ path_inside ?p3" by blast
qed
lemma smaller_triangle:
assumes "¬ collinear {a, b, c} ∧ ¬ collinear {a', b', c'}"
assumes "p = make_triangle a b c"
assumes "p' = make_triangle a' b' c'"
assumes "path_inside p ⊆ path_inside p'"
assumes "∃d. integral_vec d ∧ d ∈ path_image p' ∪ path_inside p' ∧ d ∉ path_image p ∪ path_inside p"
shows "card (integral_inside p) + card (integral_boundary p) < card (integral_inside p') + card (integral_boundary p')"
proof-
have "simple_path p" using assms unfolding make_triangle_def
using assms(2) polygon_def triangle_is_polygon by presburger
then have finite_p: "finite (integral_inside p) ∧ finite (integral_boundary p)" using assms unfolding make_triangle_def
using integral_boundary integral_inside finite_integral_points_path_image finite_integral_points_path_inside by metis
have "simple_path p'" using assms unfolding make_triangle_def
using assms(3) polygon_def triangle_is_polygon by presburger
then have finite_p': "finite (integral_inside p') ∧ finite (integral_boundary p')" using assms unfolding make_triangle_def
using integral_boundary integral_inside finite_integral_points_path_image finite_integral_points_path_inside by metis
have "polygon p" using assms(1,2) triangle_is_polygon by blast
then have 1: "(integral_inside p) ∩ (integral_boundary p) = {}"
unfolding integral_inside integral_boundary using inside_outside_polygon unfolding inside_outside_def by blast
have "polygon p'" using assms(1,3) triangle_is_polygon by blast
then have 2: "(integral_inside p') ∩ (integral_boundary p') = {}"
unfolding integral_inside integral_boundary using inside_outside_polygon unfolding inside_outside_def by blast
have path_image_subset: "path_image p ⊆ path_image p' ∪ path_inside p'"
proof-
have p_frontier: "path_image p = frontier (convex hull {a, b, c})"
by (simp add: assms(1) assms(2) convex_polygon_frontier_is_path_image2 triangle_convex_hull triangle_is_convex triangle_is_polygon)
have p'_frontier: "path_image p' = frontier (convex hull {a', b', c'})"
by (simp add: assms(1) assms(3) convex_polygon_frontier_is_path_image2 triangle_convex_hull triangle_is_convex triangle_is_polygon)
have p_interior: "path_inside p = interior (convex hull {a, b, c})"
by (simp add: bounded_convex_hull p_frontier inside_frontier_eq_interior path_inside_def)
have p'_interior: "path_inside p' = interior (convex hull {a', b', c'})"
by (simp add: bounded_convex_hull p'_frontier inside_frontier_eq_interior path_inside_def)
have "interior (convex hull {a, b, c}) ⊆ interior (convex hull {a', b', c'})"
using assms p_interior p'_interior by argo
moreover have "compact (convex hull {a, b, c}) ∧ compact (convex hull {a', b', c'})"
by (simp add: compact_convex_hull)
ultimately have "frontier (convex hull {a, b, c})
⊆ interior (convex hull {a', b', c'}) ∪ frontier (convex hull {a', b', c'})"
by (smt (verit, ccfv_threshold) Jordan_inside_outside_real2 closed_path_def ‹polygon p'› ‹polygon p› assms(1) assms(2) closure_Un closure_Un_frontier closure_convex_hull finite.emptyI finite_imp_compact finite_insert p'_frontier p'_interior p_interior path_inside_def polygon_def subset_trans sup.absorb_iff1 sup_commute triangle_convex_hull)
then show ?thesis using p'_frontier p'_interior p_frontier by blast
qed
have "card ((integral_inside p) ∪ (integral_boundary p)) = card (integral_inside p) + card (integral_boundary p)"
using 1 finite_p by (simp add: card_Un_disjoint)
moreover have "card ((integral_inside p') ∪ (integral_boundary p')) = card (integral_inside p') + card (integral_boundary p')"
using 2 finite_p' by (simp add: card_Un_disjoint)
moreover have "(integral_inside p) ∪ (integral_boundary p) ⊆ (integral_inside p') ∪ (integral_boundary p')"
using assms path_image_subset unfolding integral_inside integral_boundary by blast
moreover then have "(integral_inside p) ∪ (integral_boundary p) ⊂ (integral_inside p') ∪ (integral_boundary p')" using assms unfolding integral_inside integral_boundary by blast
ultimately show ?thesis by (metis finite_Un finite_p' psubset_card_mono)
qed
lemma pick_elem_triangle:
fixes p :: "R_to_R2"
assumes p_triangle: "p = make_triangle a b c"
assumes elem_triangle: "elem_triangle a b c"
assumes "I = card {x. integral_vec x ∧ x ∈ path_inside p}" and
"B = card {x. integral_vec x ∧ x ∈ path_image p}"
shows "measure lebesgue (path_inside p) = I + B/2 - 1"
proof -
have polygon_p: "polygon p"
using p_triangle triangle_is_polygon elem_triangle
unfolding elem_triangle_def by auto
then have "path_inside p ∩ path_image p = {}"
using inside_outside_polygon[of p] unfolding inside_outside_def
by auto
let ?p = "polygon (make_polygonal_path [a, b, c, a])"
have a_neq_b:"a ≠ b"
using elem_triangle unfolding elem_triangle_def
by auto
have b_neq_c: "b ≠ c"
using elem_triangle unfolding elem_triangle_def
by auto
have a_neq_c: "c ≠ a"
using elem_triangle unfolding elem_triangle_def
using collinear_3_eq_affine_dependent by blast
have "path_image p ⊆ convex hull {a, b, c}"
using triangle_path_image_subset_convex p_triangle by auto
then have
"{x. integral_vec x ∧ x ∈ path_image p} ⊆ {x. integral_vec x ∧ x ∈ convex hull {a, b, c}}"
by auto
also have "... = {a, b, c}"
using elem_triangle unfolding elem_triangle_def by auto
finally have "{x. integral_vec x ∧ x ∈ path_image p} ⊆ {a, b, c}" .
moreover have "{x. integral_vec x ∧ x ∈ path_image p} 🪙 {a, b, c}"
by (smt (verit) Collect_mono_iff make_triangle_def ‹{x. integral_vec x ∧ x ∈ convex hull {a, b, c}} = {a, b, c}› empty_set insert_subset list.simps(15) mem_Collect_eq p_triangle subsetD vertices_on_path_image)
ultimately have "{x. integral_vec x ∧ x ∈ path_image p} = {a, b, c}" by auto
then have card_2: "B = 3"
using a_neq_b b_neq_c a_neq_c assms(4)
by simp
have "{x. integral_vec x ∧ x ∈ path_inside p} = {}"
proof-
have "path_inside p ⊆ convex hull {a, b, c}"
by (smt (verit, best) Diff_insert_absorb make_triangle_def convex_polygon_inside_is_convex_hull_interior empty_iff empty_set insert_Diff_single insert_commute interior_subset list.simps(15) p_triangle polygon_p elem_triangle elem_triangle_def triangle_is_convex)
then have
"{x. integral_vec x ∧ x ∈ path_inside p} ⊆ {x. integral_vec x ∧ x ∈ convex hull {a, b, c}}"
by auto
also have "... = {a, b, c}"
using ‹{x. integral_vec x ∧ x ∈ convex hull {a, b, c}} = {a, b, c}› by auto
finally have "{x. integral_vec x ∧ x ∈ path_inside p} ⊆ {a, b, c}" .
moreover have
"{x. integral_vec x ∧ x ∈ path_inside p} ∩ {x. integral_vec x ∧ x ∈ path_image p} = {}"
using ‹path_inside p ∩ path_image p = {}› by auto
ultimately show ?thesis
using ‹{x. integral_vec x ∧ x ∈ path_image p} = {a, b, c}› by auto
qed
then have card_1: "I = 0"
using assms(3)
by (metis card.empty)
have "I + B/2 - 1 = 1/2"
using card_1 card_2 assms
by auto
then show ?thesis
using elem_triangle_area_is_half[OF assms(2)] triangle_measure_convex_hull_measure_path_inside_same[OF assms(1) assms(2)]
by auto
qed
lemma pick_triangle_lemma:
fixes p :: "R_to_R2"
assumes "p = make_triangle a b c" and "all_integral [a, b, c]" and "distinct [a, b, c]" and "¬ collinear {a, b, c}"
"I = card {x. integral_vec x ∧ x ∈ path_inside p}" and
"B = card {x. integral_vec x ∧ x ∈ path_image p}"
shows "measure lebesgue (path_inside p) = I + B/2 - 1"
using assms
proof(induction "card {x. integral_vec x ∧ x ∈ path_inside p} + card {x. integral_vec x ∧ x ∈ path_image p}" arbitrary: p a b c I B rule:less_induct)
case less
have polygon_p: "polygon p" using triangle_is_polygon[OF less.prems(4)] less.prems(1) by simp
then have polygon_of: "polygon_of p [a, b, c, a]"
unfolding polygon_of_def using less.prems(1) unfolding make_triangle_def by auto
(* One case where I is nonempty *)
have convex_hull_char: "convex hull {a, b, c} = path_inside p ∪ path_image p"
using triangle_convex_hull[OF less.prems(1) less.prems(4)] by auto
then have interior_convex_hull: "{x. integral_vec x ∧ x ∈ path_inside p} ∪ {x. integral_vec x ∧ x ∈ path_image p} = {x ∈ convex hull {a, b, c}. integral_vec x}"
by auto
have vts_in_path_image: "a ∈ path_image p ∧ b ∈ path_image p ∧ c ∈ path_image p"
using assms(1) unfolding make_triangle_def using vertices_on_path_image
by (metis (mono_tags, lifting) insertCI less.prems(1) list.simps(15) make_triangle_def subset_code(1))
have integral_vts: "integral_vec a ∧ integral_vec b ∧ integral_vec c"
using less.prems(2)
by (simp add: all_integral_def)
then have subset: "{a, b, c} ⊆ {x. integral_vec x ∧ x ∈ path_image p}"
using vts_in_path_image integral_vts by simp
have finite_integral_on_path_im: "finite {x. integral_vec x ∧ x ∈ path_image p}"
using finite_integral_points_path_image triangle_is_polygon[OF less.prems(4)]
unfolding make_triangle_def polygon_def
using less.prems(1) make_triangle_def by auto
have B_3_if: "B > 3" if other_point_in_set: "{x. integral_vec x ∧ x ∈ path_image p} ≠ {a, b, c}"
proof -
have "∃d. d ∉ {a, b, c} ∧ d ∈ {x. integral_vec x ∧ x ∈ path_image p}"
using other_point_in_set subset
by blast
then obtain d where d_prop: "d ∉ {a, b, c} ∧ d ∈ {x. integral_vec x ∧ x ∈ path_image p}"
by auto
then have subset2: "{a, b, c, d} ⊆{x. integral_vec x ∧ x ∈ path_image p}"
using d_prop subset by auto
have "distinct [a, b, c, d]"
using d_prop
using less.prems(3) by auto
then have card_is: "card {a, b, c, d} = 4"
by simp
show ?thesis using subset2 card_is finite_integral_on_path_im
by (metis (no_types, lifting) Suc_le_eq card_mono eval_nat_numeral(2) less.prems(6) semiring_norm(26) semiring_norm(27))
qed
{ assume *: "I = 0"
have "finite {x. integral_vec x ∧ x ∈ path_inside p}"
using finite_integral_points_path_inside triangle_is_polygon[OF less.prems(4)]
unfolding make_triangle_def
by (simp add: less.prems(1) make_triangle_def polygon_def)
then have empty_inside: "{x. integral_vec x ∧ x ∈ path_inside p} = {}"
using * less.prems(5) by auto
(* First, use pick_elem_triangle in the case where I is empty and B only contains the vertices *)
{ assume **: "B = 3"
have "{x ∈ convex hull {a, b, c}. integral_vec x} = {a, b, c}"
using * ** less.prems(5-6) B_3_if interior_convex_hull empty_inside
by blast
then have "elem_triangle a b c"
unfolding elem_triangle_def using less.prems(4) integral_vts by simp
then have "measure lebesgue (path_inside p) = I + B/2 - 1"
using pick_elem_triangle less.prems by auto
} (* In the next case, there is an integral vertex on one of the line segments of the triangle *)
moreover
{ assume *: "B > 3"
then obtain d where d: "integral_vec d ∧ d ∈ path_image p ∧ d ∉ {a, b, c}"
by (smt (verit, del_insts) subset finite_integral_on_path_im less.prems(3) card_3_iff collinear_3_eq_affine_dependent less.prems(4) less.prems(6) less_not_refl mem_Collect_eq subsetI subset_antisym)
have "path_image (make_polygonal_path [a, b, c, a]) = path_image (linepath a b) ∪ path_image (linepath b c) ∪ path_image (linepath c a)"
by (metis (no_types, lifting) list.discI make_polygonal_path.simps(3) nth_Cons_0 path_image_cons_union sup_assoc)
then have "d ∈ path_image (linepath a b)
∨ d ∈ path_image (linepath b c)
∨ d ∈ path_image (linepath c a)"
using d less.prems(1) unfolding make_triangle_def polygon_of_def
by blast
then have "measure lebesgue (path_inside p) = I + B/2 - 1"
using pick_triangle_helper less.prems less.hyps empty_inside d
unfolding pick_holds pick_triangle integral_inside integral_boundary
apply simp by blast
}
ultimately have "measure lebesgue (path_inside p) = I + B/2 - 1"
using B_3_if
by (metis (no_types, lifting) card.empty card_insert_disjoint collinear_2 finite.emptyI finite.insertI insert_absorb less.prems(4) less.prems(6) numeral_3_eq_3)
} (* In the last case, there is an integral vertex inside the triangle *)
moreover
{ assume *: "I > 0"
then obtain d where d_inside: "integral_vec d ∧ d ∈ path_inside p"
using less.prems(5)
by (metis (mono_tags, lifting) Collect_empty_eq add_0 canonically_ordered_monoid_add_class.lessE card_0_eq card_ge_0_finite)
have "a ∈ path_image p"
using vertices_on_path_image polygon_of unfolding polygon_of_def by fastforce
then have a_inset: "a ∈ path_inside p ∪ path_image p"
by fastforce
have convex_hull_set: "convex hull set [a, b, c, a] = path_inside p ∪ path_image p"
using convex_hull_char
by (simp add: insert_commute)
then have ad_linepath_inside: "path_image (linepath a d) ⊆ path_inside p ∪ path_image p"
using d_inside convex_polygon_means_linepaths_inside[OF polygon_of convex_hull_set a_inset]
by blast
have "b ∈ path_image p"
using vertices_on_path_image polygon_of unfolding polygon_of_def by fastforce
then have b_inset: "b ∈ path_inside p ∪ path_image p"
by fastforce
have bd_linepath_inside: "path_image (linepath b d) ⊆ path_inside p ∪ path_image p"
using d_inside convex_polygon_means_linepaths_inside[OF polygon_of convex_hull_set b_inset]
by blast
have "c ∈ path_image p"
using vertices_on_path_image polygon_of unfolding polygon_of_def by fastforce
then have c_inset: "c ∈ path_inside p ∪ path_image p"
by fastforce
then have cd_linepath_inside: "path_image (linepath c d) ⊆ path_inside p ∪ path_image p"
using d_inside convex_hull_char convex_polygon_means_linepaths_inside[OF polygon_of convex_hull_set c_inset]
by blast
let ?p1 = "make_triangle a d c"
let ?p2 = "make_triangle d b c"
let ?p3 = "make_triangle a b d"
have triangle_split:
"is_polygon_split_path [a, b, c] 0 1 [d]"
"is_polygon_split [a, d, b, c] 1 3"
"a ∉ path_image ?p2 ∪ path_inside ?p2"
"b ∉ path_image ?p1 ∪ path_inside ?p1"
"c ∉ path_image ?p3 ∪ path_inside ?p3"
using triangle_3_split[of p a b c d] less.prems d_inside polygon_p apply fastforce
using triangle_3_split[of p a b c d] less.prems d_inside polygon_p apply fastforce
using triangle_3_split[of p a b c d] less.prems d_inside polygon_p apply fastforce
using triangle_3_split[of p a b c d] less.prems d_inside polygon_p apply fastforce
using triangle_3_split[of p a b c d] less.prems d_inside polygon_p by fastforce
let ?q = "make_polygonal_path [a, d, b, c, a]"
let ?I1 = "card (integral_inside ?p1)"
let ?B1 = "card (integral_boundary ?p1)"
let ?I2 = "card (integral_inside ?p2)"
let ?B2 = "card (integral_boundary ?p2)"
let ?I3 = "card (integral_inside ?p3)"
let ?B3 = "card (integral_boundary ?p3)"
let ?Iq = "card (integral_inside ?q)"
let ?Bq = "card (integral_boundary ?q)"
have "measure lebesgue (path_inside ?p1) = ?I1 + ?B1/2 - 1"
proof-
have "path_inside ?p1 ⊆ path_inside ?q"
using triangle_split(2) unfolding is_polygon_split_def
by (smt (verit) One_nat_def Un_assoc Un_upper1 append_Cons append_Nil diff_Suc_Suc diff_zero drop0 drop_Suc_Cons make_triangle_def nth_Cons_0 nth_Cons_Suc numeral_3_eq_3 sup_commute take0 take_Suc_Cons)
moreover have "path_inside ?q ⊆ path_inside p"
using triangle_split(1) unfolding is_polygon_split_path_def
by (smt (verit) One_nat_def Un_assoc Un_subset_iff append_Cons append_Nil diff_zero drop0 drop_Suc_Cons less.prems(1) make_triangle_def nth_Cons_0 nth_Cons_Suc sup.cobounded2 take0)
ultimately have "path_inside ?p1 ⊆ path_inside p" by blast
moreover have "¬ collinear {a, d, c}"
by (metis d_inside insert_commute less.prems(1) polygon_p triangle_interior_point_not_collinear_vertices)
moreover have "¬ collinear {a, b, c}" by (simp add: less.prems(4))
moreover have "integral_vec b"
using integral_vts by blast
moreover have "b ∈ path_image p"
using vts_in_path_image by auto
ultimately have "card (integral_inside ?p1) + card (integral_boundary ?p1) < card (integral_inside p) + card (integral_boundary p)"
using smaller_triangle[of a d c a b c ?p1 p] triangle_split(4) less.prems(1) less_imp_le_nat
by blast
thus ?thesis
using less.hyps[of ?p1 a d c] unfolding integral_inside integral_boundary
using ‹¬ collinear {a, d, c}› all_integral_def d_inside integral_vts less.prems(1) less.prems(3) triangle_split(3) triangle_split(5)
by fastforce
qed
moreover have "measure lebesgue (path_inside ?p2) = ?I2 + ?B2/2 - 1"
proof-
have "path_inside ?p2 ⊆ path_inside ?q"
using triangle_split(2) unfolding is_polygon_split_def
by (smt (verit) One_nat_def Un_assoc Un_upper1 append_Cons append_Nil diff_Suc_Suc diff_zero drop0 drop_Suc_Cons make_triangle_def nth_Cons_0 nth_Cons_Suc numeral_3_eq_3 sup_commute take0 take_Suc_Cons)
moreover have "path_inside ?q ⊆ path_inside p"
using triangle_split(1) unfolding is_polygon_split_path_def
by (smt (verit) One_nat_def Un_assoc Un_subset_iff append_Cons append_Nil diff_zero drop0 drop_Suc_Cons less.prems(1) make_triangle_def nth_Cons_0 nth_Cons_Suc sup.cobounded2 take0)
ultimately have "path_inside ?p2 ⊆ path_inside p" by blast
moreover have "¬ collinear {d, b, c}"
by (metis d_inside insert_commute less.prems(1) polygon_p triangle_interior_point_not_collinear_vertices)
moreover have "¬ collinear {a, b, c}" by (simp add: less.prems(4))
moreover have "integral_vec a"
using integral_vts by blast
moreover have "a ∈ path_image p"
using vts_in_path_image by auto
ultimately have "card (integral_inside ?p2) + card (integral_boundary ?p2) < card (integral_inside p) + card (integral_boundary p)"
using smaller_triangle[of d b c a b c ?p2 p] triangle_split(3) less.prems(1) less_imp_le_nat
by blast
thus ?thesis
using less.hyps[of ?p2 d b c] unfolding integral_inside integral_boundary
using ‹¬ collinear {d, b, c}› all_integral_def d_inside integral_vts less.prems(1) less.prems(3) triangle_split(3) triangle_split(5)
by fastforce
qed
moreover have "measure lebesgue (path_inside ?p3) = ?I3 + ?B3/2 - 1"
proof-
have "path_inside ?p3 ⊆ path_inside p"
using triangle_split(1) unfolding is_polygon_split_path_def
by (smt (verit) One_nat_def Un_assoc Un_upper1 append_Cons append_Nil diff_Suc_Suc diff_zero less.prems(1) make_triangle_def nth_Cons_0 nth_Cons_Suc rev_singleton_conv take0)
moreover have "¬ collinear {a, b, d}"
by (metis d_inside less.prems(1) polygon_p triangle_interior_point_not_collinear_vertices)
moreover have "¬ collinear {a, b, c}" by (simp add: less.prems(4))
moreover have "integral_vec c"
using integral_vts by blast
moreover have "c ∈ path_image p"
using vts_in_path_image by auto
ultimately have "card (integral_inside ?p3) + card (integral_boundary ?p3) < card (integral_inside p) + card (integral_boundary p)"
using smaller_triangle[of a b d a b c ?p3 p] triangle_split(5) less.prems(1) less_imp_le_nat
by blast
thus ?thesis
using less.hyps[of ?p3 a b d] unfolding integral_inside integral_boundary
using ‹¬ collinear {a, b, d}› all_integral_def d_inside integral_vts less.prems(1) less.prems(3) triangle_split(3) triangle_split(5)
by fastforce
qed
moreover have "measure lebesgue (path_inside ?q) = ?Iq + ?Bq/2 - 1"
using pick_split_union[OF triangle_split(2),
of "[a]" "[b]" "[]" d c ?q ?p2 ?p1 ?I2 ?B2 ?I1 ?B1 ?Iq ?Bq]
using calculation
unfolding integral_inside integral_boundary make_triangle_def
using all_integral_def d_inside less.prems(2) by force
ultimately have ?case
using pick_split_path_union[OF triangle_split(1),
of "[]" "[]" "[c]" a b "make_polygonal_path (a # [d] @ [b])" p ?p3 ?q ?I3 ?B3 ?Iq ?Bq I B]
unfolding integral_inside integral_boundary make_triangle_def less.prems
using less.prems(2) by force
}
ultimately show ?case by blast
qed
subsection "Pocket properties"
definition index_not_in_set :: "(real^2) list ==> (real^2) set ==> nat ==> bool"
where "index_not_in_set vts A i ⟷ i ∈ {i. i < length vts ∧ vts ! i ∉ A}"
definition min_index_not_in_set:: "(real^2) list ==> (real^2) set ==> nat"
where "min_index_not_in_set vts A = (LEAST i. index_not_in_set vts A i)"
definition nonzero_index_in_set :: "(real^2) list ==> (real^2) set ==> nat ==> bool" where
"nonzero_index_in_set vts A i ⟷ i ∈ {i. 0 < i ∧ i < length vts ∧ vts ! i ∈ A}"
definition min_nonzero_index_in_set :: "(real^2) list ==> (real^2) set ==> nat" where
"min_nonzero_index_in_set vts A = (LEAST i. nonzero_index_in_set vts A i)"
(* NOTE: Requires rotation: enforce that vts!0 is in convex_hull_vts,
since the pocket can "loop around" the end of the polygon vts list
*)
definition construct_pocket_0 :: "(real^2) list ==> (real^2) set ==> (real^2) list" where
"construct_pocket_0 vts A = take ((min_nonzero_index_in_set vts A) + 1) vts"
definition is_pocket_0 :: "(real^2) list ==> (real^2) list ==> bool" where
"is_pocket_0 vts vts' ⟷
polygon (make_polygonal_path vts)
∧ (∃i. vts' = take i vts)
∧ 3 ≤ length vts' ∧ length vts' < length vts
∧ hd vts' ∈ frontier (convex hull (set vts)) ∧ last vts' ∈ frontier (convex hull (set vts))
∧ set (tl (butlast vts')) ⊆ interior (convex hull (set vts))"
(* i is the length of the pocket path *)
definition fill_pocket_0 :: "(real^2) list ==> nat ==> (real^2) list" where
"fill_pocket_0 vts i = (hd vts) # (drop (i-1) vts)"
lemma min_nonzero_index_in_set_exists:
assumes "set (tl vts) ∩ A ≠ {}"
shows "∃i. nonzero_index_in_set vts A i"
proof-
obtain v where v: "v ∈ A ∩ set (tl vts)" using assms by blast
then obtain i where "(tl vts)!i = v ∧ i < length (tl vts)" by (meson IntD2 in_set_conv_nth)
then obtain j where "vts!j = v ∧ 0 < j ∧ j < length vts" using nth_tl by fastforce
thus ?thesis unfolding nonzero_index_in_set_def using v by blast
qed
lemma min_nonzero_index_in_set_defined:
assumes "set (tl vts) ∩ A ≠ {}"
defines "i ≡ min_nonzero_index_in_set vts A"
shows "nonzero_index_in_set vts A i ∧ (∀j < i. ¬ nonzero_index_in_set vts A j)"
proof-
have "∃i. nonzero_index_in_set vts A i" using assms min_nonzero_index_in_set_exists by blast
then have "nonzero_index_in_set vts A i"
using assms unfolding min_nonzero_index_in_set_def
using LeastI_ex by blast
moreover have "(∀j < i. ¬ nonzero_index_in_set vts A j)"
by (metis assms(2) wellorder_Least_lemma(2) leD min_nonzero_index_in_set_def)
ultimately show ?thesis by blast
qed
lemma min_index_not_in_set_exists:
assumes "set vts 🪙 A"
shows "∃i. index_not_in_set vts A i"
proof-
obtain v where "v ∈ set vts ∧ v ∉ A" using assms by blast
then obtain i where "i < length vts ∧ vts ! i ∉ A" by (metis in_set_conv_nth)
thus ?thesis unfolding index_not_in_set_def by blast
qed
lemma min_index_not_in_set_defined:
assumes "set vts 🪙 A"
defines "i ≡ min_index_not_in_set vts A"
shows "index_not_in_set vts A i ∧ (∀j < i. ¬ index_not_in_set vts A j)"
proof-
have "∃i. index_not_in_set vts A i" using assms min_index_not_in_set_exists by simp
then have "index_not_in_set vts A i"
using assms unfolding min_index_not_in_set_def
using LeastI_ex by blast
moreover have "(∀j < i. ¬ index_not_in_set vts A j)"
by (metis assms(2) wellorder_Least_lemma(2) leD min_index_not_in_set_def)
ultimately show ?thesis by blast
qed
lemma min_nonzero_index_in_set_bound:
assumes "set (tl vts) ∩ A ≠ {}"
shows "min_nonzero_index_in_set vts A < length vts"
using min_nonzero_index_in_set_defined assms unfolding nonzero_index_in_set_def by blast
lemma construct_pocket_0_subset_vts:
assumes "set (tl vts) ∩ A ≠ {}"
shows "set (construct_pocket_0 vts A) ⊆ set vts"
proof-
let ?i = "min_nonzero_index_in_set vts A"
have "nonzero_index_in_set vts A ?i" using min_nonzero_index_in_set_defined assms by presburger
then have "?i < length vts" unfolding nonzero_index_in_set_def by blast
thus ?thesis unfolding construct_pocket_0_def by (simp add: set_take_subset)
qed
lemma min_index_not_in_set_0:
assumes "set vts 🪙 A"
assumes "vts!0 ∈ A"
defines "i ≡ min_index_not_in_set vts A"
defines "r ≡ i - 1"
shows "vts!r ∈ A"
proof-
have *: "index_not_in_set vts A i ∧ (∀j<i. ¬ index_not_in_set vts A j)"
using min_index_not_in_set_defined[of A vts, OF assms(1)] unfolding i_def by blast
moreover then have "r < i"
unfolding r_def i_def min_index_not_in_set_def index_not_in_set_def
by (metis (no_types, lifting) assms(2) bot_nat_0.not_eq_extremum diff_less mem_Collect_eq zero_less_one)
ultimately have "¬ index_not_in_set vts A r" by blast
thus ?thesis
unfolding index_not_in_set_def using assms * index_not_in_set_def less_imp_diff_less by force
qed
lemma construct_pocket_0_last_in_set:
assumes "set (tl vts) ∩ A ≠ {}"
assumes "vts!0 ∈ A"
defines "p ≡ construct_pocket_0 vts A"
shows "last p ∈ A"
proof-
let ?i = "min_nonzero_index_in_set vts A"
have *: "nonzero_index_in_set vts A ?i" using assms(1) min_nonzero_index_in_set_defined by blast
then have "length p = min_nonzero_index_in_set vts A + 1"
unfolding p_def construct_pocket_0_def nonzero_index_in_set_def by simp
then have "last p = p!?i"
by (metis add_diff_cancel_right' last_conv_nth length_0_conv zero_eq_add_iff_both_eq_0 zero_neq_one)
also have "... = vts!?i"
unfolding p_def construct_pocket_0_def by simp
also have "... ∈ A" using * unfolding nonzero_index_in_set_def by force
finally show ?thesis .
qed
lemma construct_pocket_0_first_last_distinct:
assumes "card A ≥ 2"
assumes "A ⊆ set vts"
assumes "distinct (butlast vts)"
assumes "hd vts = last vts"
shows "hd (construct_pocket_0 vts A) ≠ last (construct_pocket_0 vts A)"
proof-
let ?n = "min_nonzero_index_in_set vts A"
have "set (tl vts) ∩ A ≠ {}"
by (metis (no_types, lifting) Diff_cancel Int_commute Int_insert_right_if1 Nat.le_diff_conv2 Suc_1 add_leD1 assms(1) assms(2) card.empty card_Diff_singleton inf.orderE list.collapse list.sel(2) list.set(2) not_one_le_zero plus_1_eq_Suc subset_insert)
then have n_defined: "nonzero_index_in_set vts A ?n ∧ (∀j < ?n. ¬ nonzero_index_in_set vts A j)"
using min_nonzero_index_in_set_defined by presburger
obtain a b where ab: "a ≠ b ∧ {a, b} ⊆ A" by (metis assms(1) card_2_iff ex_card)
then obtain i j where ij: "vts!i = a ∧ vts!j = b ∧ i < length vts ∧ j < length vts ∧ i ≠ j"
by (metis (no_types, opaque_lifting) assms(2) in_set_conv_nth insert_subset subsetD)
have ?thesis if *: "?n < length vts - 1"
proof-
have "?n > 0" using n_defined unfolding nonzero_index_in_set_def by blast
then have n_bound': "?n > 0 ∧ ?n < length (butlast vts)" using * by fastforce
then have "hd vts ≠ vts!?n"
by (metis assms(3) distinct_Ex1 hd_conv_nth ij in_set_conv_nth length_0_conv length_pos_if_in_set less_nat_zero_code nth_butlast)
moreover then have "vts!?n ≠ last vts" using assms(4) by simp
moreover have "last (construct_pocket_0 vts A) = vts!?n"
using n_defined
unfolding construct_pocket_0_def
by (metis Cons_nth_drop_Suc Suc_eq_plus1 n_bound' * last_snoc less_diff_conv list.sel(1) nth_butlast take_butlast take_hd_drop)
moreover have "hd (construct_pocket_0 vts A) = hd vts"
unfolding construct_pocket_0_def by force
ultimately show ?thesis by presburger
qed
moreover have ?thesis if *: "?n = length vts - 1"
proof-
have "{i, j} ⊆ {i. i < length vts ∧ vts ! i ∈ A}" using ij ab by simp
moreover have "i ≠ 0 ∨ j ≠ 0" using ij by argo
ultimately have "nonzero_index_in_set vts A i ∨ nonzero_index_in_set vts A j"
unfolding nonzero_index_in_set_def by simp
then have "?n = i ∨ ?n = j"
by (metis n_defined Suc_diff_1 gr_implies_not_zero ij linorder_cases not_less_eq *)
moreover then have "last (construct_pocket_0 vts A) = vts!?n"
by (metis Suc_eq_plus1 construct_pocket_0_def hd_drop_conv_nth ij snoc_eq_iff_butlast take_hd_drop)
ultimately show ?thesis
by (metis (no_types, lifting) ij ab Suc_eq_plus1 assms(4) bot_nat_0.not_eq_extremum hd_conv_nth insert_subset last_conv_nth less_diff_conv list.size(3) mem_Collect_eq n_defined nat_neq_iff nonzero_index_in_set_def not_less_eq that)
qed
ultimately show ?thesis using n_defined unfolding nonzero_index_in_set_def by fastforce
qed
lemma construct_pocket_is_pocket:
assumes "polygon (make_polygonal_path vts)"
assumes "vts!0 ∈ frontier (convex hull (set vts))"
assumes "vts!1 ∉ frontier (convex hull (set vts))"
shows "is_pocket_0 vts (construct_pocket_0 vts (set vts ∩ frontier (convex hull (set vts))))"
proof-
let ?vts' = "construct_pocket_0 vts (set vts ∩ frontier (convex hull (set vts)))"
have ex_i: "∃i. ?vts' = take i vts" unfolding construct_pocket_0_def by blast
moreover have "3 ≤ length ?vts'" (* smt call may take a second or two to terminate *)
by (smt (verit) Cons_nth_drop_Suc IntI Int_iff One_nat_def Suc_1 Suc_diff_Suc Suc_lessI add_diff_cancel_right' add_gr_0 append_Nil2 assms(1) assms(2) assms(3) butlast.simps(1) butlast.simps(2) butlast_conv_take calculation cancel_comm_monoid_add_class.diff_cancel card.empty construct_pocket_0_def construct_pocket_0_first_last_distinct construct_pocket_0_last_in_set convex_hull_two_vts_on_frontier diff_diff_cancel diff_is_0_eq diff_is_0_eq' drop0 empty_iff empty_set have_wraparound_vertex hd_conv_nth hd_drop_conv_nth hd_take id_take_nth_drop last.simps last_conv_nth last_drop last_in_set last_snoc leI le_add2 le_numeral_extra(4) le_trans length_0_conv length_greater_0_conv length_take length_tl length_upt less_2_cases less_numeral_extra(1) less_numeral_extra(3) linorder_not_less list.distinct(1) list.sel(2) list.sel(3) list.size(3) min.absorb4 not_gr_zero not_less_eq_eq not_numeral_le_zero nth_mem numeral_3_eq_3 plus_1_eq_Suc polygon_at_least_3_vertices polygon_at_least_3_vertices_wraparound polygon_def pos2 rev.simps(1) self_append_conv2 simple_polygonal_path_vts_distinct snoc_eq_iff_butlast subset_iff take_al | |