theory Polygon
imports Counterclockwise_2D_Strict
begin

subsection {* Polygonal chains *}

definition "polychain xs = (\<forall>i. Suc i<length xs \<longrightarrow> snd (xs ! i) = (fst (xs ! Suc i)))"

lemma polychainI:
  assumes "\<And>i. Suc i < length xs \<Longrightarrow> snd (xs ! i) = fst (xs ! Suc i)"
  shows "polychain xs"
  by (auto intro!: assms simp: polychain_def)

lemma polychain_appendI:
  "polychain xs \<Longrightarrow> polychain ys \<Longrightarrow> (xs \<noteq> [] \<Longrightarrow> ys \<noteq> [] \<Longrightarrow> snd (last xs) = fst (hd ys)) \<Longrightarrow> polychain (xs @ ys)"
  apply (auto simp: polychain_def nth_append not_less)
  apply (cases xs, simp)
  apply (cases ys, simp)
  apply (auto simp: polychain_def nth_append not_less)
  defer
  apply (cases xs, simp)
  apply (cases ys, simp)
  apply (auto simp: polychain_def nth_append not_less)
  apply (case_tac i)
  apply (auto simp: polychain_def nth_append not_less last_conv_nth)
  by (metis diff_Suc_Suc le_neq_implies_less minus_nat.diff_0 not_less_eq)

fun pairself where "pairself f (x, y) = (f x, f y)"
lemma pairself_apply: "pairself f x = (f (fst x), f (snd x))"
  by (cases x, simp)

lemma polychain_map_pairself: "polychain xs \<Longrightarrow> polychain (map (pairself f) xs)"
  by (auto simp: polychain_def pairself_apply)

lemma polychain_Nil[simp]: "polychain [] = True"
  and polychain_Cons[simp]: "polychain [x] = True"
  by (auto simp: polychain_def)

definition "convex_polychain xs \<longleftrightarrow>
  (polychain xs \<and>
  (\<forall>i. Suc i < length xs \<longrightarrow> det3 (fst (xs ! i)) (snd (xs ! i)) (snd (xs ! Suc i)) > 0))"

lemma convex_polychain_Cons2[simp]:
  "convex_polychain (x#y#zs) \<longleftrightarrow>
    snd x = fst y \<and> det3 (fst x) (fst y) (snd y) > 0 \<and> convex_polychain (y#zs)"
  by (auto simp add: convex_polychain_def polychain_def nth_Cons split: nat.split)

lemma convex_polychain_ConsD:
  assumes "convex_polychain (x#xs)"
  shows "convex_polychain xs"
  using assms by (auto simp: convex_polychain_def polychain_def nth_Cons split: nat.split)

definition "convex_polygon xs \<longleftrightarrow> (convex_polychain xs \<and> (xs \<noteq> [] \<longrightarrow> fst (hd xs) = snd (last xs)))"

lemma convex_polychain_Nil[simp]: "convex_polychain [] = True"
  and convex_polychain_Cons[simp]: "convex_polychain [x] = True"
  by (auto simp: convex_polychain_def)

lemma convex_polygon_Cons2[simp]:
  "convex_polygon (x#y#zs) \<longleftrightarrow> fst x = snd (last (y#zs)) \<and> convex_polychain (x#y#zs)"
  by (auto simp: convex_polygon_def convex_polychain_def polychain_def nth_Cons)

lemma polychain_append_connected: "polychain (xs @ ys) \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> ys \<noteq> [] \<Longrightarrow> fst (hd ys) = snd (last xs)"
  by (auto simp: convex_polychain_def nth_append not_less polychain_def last_conv_nth hd_conv_nth
    dest!: spec[where x = "length xs - 1"])

lemma convex_polychain_appendI:
  assumes cxs: "convex_polychain xs"
  assumes cys: "convex_polychain ys"
  assumes pxy: "polychain (xs @ ys)"
  assumes "xs \<noteq> [] \<Longrightarrow> ys \<noteq> [] \<Longrightarrow> det3 (fst (last xs)) (snd (last xs)) (snd (hd ys)) > 0"
  shows "convex_polychain (xs @ ys)"
  using assms apply (auto simp: hd_conv_nth convex_polychain_def nth_append Suc_diff_le)
proof -
  case goal1
  hence "xs \<noteq> []" "ys \<noteq> []" "i = length xs - 1" by auto
  thus ?case using goal1 by (auto simp: last_conv_nth hd_conv_nth)
qed

lemma convex_polychainI:
  assumes "polychain xs"
  assumes "\<And>i. Suc i < length xs \<Longrightarrow> det3 (fst (xs ! i)) (snd (xs ! i)) (snd (xs ! Suc i)) > 0"
  shows "convex_polychain xs"
  by (auto intro!: assms simp: convex_polychain_def ccw'_def)

primrec polychain_of::"'a::ab_group_add \<Rightarrow> 'a list \<Rightarrow> ('a*'a) list" where
  "polychain_of xc [] = []"
| "polychain_of xc (xm#xs) = (xc, xc + xm)#polychain_of (xc + xm) xs"

lemma in_set_polychain_ofD: "ab \<in> set (polychain_of x xs) \<Longrightarrow> (snd ab - fst ab) \<in> set xs"
  by (induct xs arbitrary: x) auto

lemma fst_polychain_of_nth_0[simp]: "xs \<noteq> [] \<Longrightarrow> fst ((polychain_of p xs) ! 0) = p"
  by (cases xs) (auto simp: Let_def)

lemma length_polychain_of_eq[simp]:
  shows "length (polychain_of p qs) = length qs"
  by (induct qs arbitrary: p) simp_all

lemma
  polychain_of_subsequent_eq:
  assumes "Suc i < length qs"
  shows "snd (polychain_of p qs ! i) = fst (polychain_of p qs ! Suc i)"
  using assms
  by (induct qs arbitrary: p i) (auto simp add: nth_Cons split: nat.split)

end
