Theory Affine_Arithmetic.Counterclockwise

section ‹Counterclockwise›
theory Counterclockwise
imports "HOL-Analysis.Multivariate_Analysis"
begin
text ‹\label{sec:counterclockwise}›

subsection ‹Auxiliary Lemmas›

lemma convex3_alt:
  fixes x y z::"'a::real_vector"
  assumes "0 ≤ a" "0 ≤ b" "0 ≤ c" "a + b + c = 1"
  obtains u v  where "a *⇩R x + b *⇩R y + c *⇩R z = x + u *⇩R (y - x) + v *⇩R (z - x)"
    and "0 ≤ u" "0 ≤ v" "u + v ≤ 1"
proof -
  from convex_hull_3[of x y z] have "a *⇩R x + b *⇩R y + c *⇩R z ∈ convex hull {x, y, z}"
    using assms by auto
  also note convex_hull_3_alt
  finally obtain u v where "a *⇩R x + b *⇩R y + c *⇩R z = x + u *⇩R (y - x) + v *⇩R (z - x)"
    and uv: "0 ≤ u" "0 ≤ v" "u + v ≤ 1"
    by auto
  thus ?thesis ..
qed

lemma (in ordered_ab_group_add) add_nonpos_eq_0_iff:
  assumes x: "0 ≥ x" and y: "0 ≥ y"
  shows "x + y = 0 ⟷ x = 0 ∧ y = 0"
proof -
  from add_nonneg_eq_0_iff[of "-x" "-y"] assms
  have "- (x + y) = 0 ⟷ - x = 0 ∧ - y = 0"
    by simp
  also have "(- (x + y) = 0) = (x + y = 0)" unfolding neg_equal_0_iff_equal ..
  finally show ?thesis by simp
qed

lemma sum_nonpos_eq_0_iff:
  fixes f :: "'a ⇒ 'b::ordered_ab_group_add"
  shows "⟦finite A; ∀x∈A. f x ≤ 0⟧ ⟹ sum f A = 0 ⟷ (∀x∈A. f x = 0)"
  by (induct set: finite) (simp_all add: add_nonpos_eq_0_iff sum_nonpos)

lemma fold_if_in_set:
  "fold (λx m. if P x m then x else m) xs x ∈ set (x#xs)"
  by (induct xs arbitrary: x) auto

subsection ‹Sort Elements of a List›

locale linorder_list0 = fixes le::"'a ⇒ 'a ⇒ bool"
begin

definition "min_for a b = (if le a b then a else b)"

lemma min_for_in[simp]: "x ∈ S ⟹ y ∈ S ⟹ min_for x y ∈ S"
  by (auto simp: min_for_def)

lemma fold_min_eqI1: "fold min_for ys y ∉ set ys ⟹ fold min_for ys y = y"
  using fold_if_in_set[of _ ys y]
  by (auto simp: min_for_def[abs_def])

function selsort where
  "selsort [] = []"
| "selsort (y#ys) = (let
      xm = fold min_for ys y;
      xs' = List.remove1 xm (y#ys)
    in (xm#selsort xs'))"
  by pat_completeness auto
termination
  by (relation "Wellfounded.measure length")
    (auto simp: length_remove1 intro!: fold_min_eqI1 dest!: length_pos_if_in_set)

lemma in_set_selsort_eq: "x ∈ set (selsort xs) ⟷ x ∈ (set xs)"
  by (induct rule: selsort.induct) (auto simp: Let_def intro!: fold_min_eqI1)

lemma set_selsort[simp]: "set (selsort xs) = set xs"
  using in_set_selsort_eq by blast

lemma length_selsort[simp]: "length (selsort xs) = length xs"
proof (induct xs rule: selsort.induct)
  case (2 x xs)
  from 2[OF refl refl]
  show ?case
    unfolding selsort.simps
    by (auto simp: Let_def length_remove1
      simp del: selsort.simps split: if_split_asm
      intro!: Suc_pred
      dest!: fold_min_eqI1)
qed simp

lemma distinct_selsort[simp]: "distinct (selsort xs) = distinct xs"
  by (auto intro!: card_distinct dest!: distinct_card)

lemma selsort_eq_empty_iff[simp]: "selsort xs = [] ⟷ xs = []"
  by (cases xs) (auto simp: Let_def)


inductive sortedP :: "'a list ⇒ bool" where
  Nil: "sortedP []"
| Cons: "∀y∈set ys. le x y ⟹ sortedP ys ⟹ sortedP (x # ys)"

inductive_cases
  sortedP_Nil: "sortedP []" and
  sortedP_Cons: "sortedP (x#xs)"
inductive_simps
  sortedP_Nil_iff: "sortedP Nil" and
  sortedP_Cons_iff: "sortedP (Cons x xs)"

lemma sortedP_append_iff:
  "sortedP (xs @ ys) = (sortedP xs & sortedP ys & (∀x ∈ set xs. ∀y ∈ set ys. le x y))"
  by (induct xs) (auto intro!: Nil Cons elim!: sortedP_Cons)

lemma sortedP_appendI:
  "sortedP xs ⟹ sortedP ys ⟹ (⋀x y. x ∈ set xs ⟹ y ∈ set ys ⟹ le x y) ⟹ sortedP (xs @ ys)"
  by (induct xs) (auto intro!: Nil Cons elim!: sortedP_Cons)

lemma sorted_nth_less: "sortedP xs ⟹ i < j ⟹ j < length xs ⟹ le (xs ! i) (xs ! j)"
  by (induct xs arbitrary: i j) (auto simp: nth_Cons split: nat.split elim!: sortedP_Cons)

lemma sorted_butlastI[intro, simp]: "sortedP xs ⟹ sortedP (butlast xs)"
  by (induct xs) (auto simp: elim!: sortedP_Cons intro!: sortedP.Cons dest!: in_set_butlastD)

lemma sortedP_right_of_append1:
  assumes "sortedP (zs@[z])"
  assumes "y ∈ set zs"
  shows "le y z"
  using assms
  by (induct zs arbitrary: y z) (auto elim!: sortedP_Cons)

lemma sortedP_right_of_last:
  assumes "sortedP zs"
  assumes "y ∈ set zs" "y ≠ last zs"
  shows "le y (last zs)"
  using assms
  apply (intro sortedP_right_of_append1[of "butlast zs" "last zs" y])
  subgoal by (metis append_is_Nil_conv list.distinct(1) snoc_eq_iff_butlast split_list)
  subgoal by (metis List.insert_def append_butlast_last_id insert_Nil list.distinct(1) rotate1.simps(2)
    set_ConsD set_rotate1)
  done

lemma selsort_singleton_iff: "selsort xs = [x] ⟷ xs = [x]"
  by (induct xs) (auto simp: Let_def)

lemma hd_last_sorted:
  assumes "sortedP xs" "length xs > 1"
  shows "le (hd xs) (last xs)"
proof (cases xs)
  case (Cons y ys)
  note ys = this
  thus ?thesis
    using ys assms
    by (auto elim!: sortedP_Cons)
qed (insert assms, simp)

end

lemma (in comm_monoid_add) sum_list_distinct_selsort:
  assumes "distinct xs"
  shows "sum_list (linorder_list0.selsort le xs) = sum_list xs"
  using assms
  apply (simp add: distinct_sum_list_conv_Sum linorder_list0.distinct_selsort)
  apply (rule sum.cong)
  subgoal by (simp add: linorder_list0.set_selsort)
  subgoal by simp
  done

declare linorder_list0.sortedP_Nil_iff[code]
  linorder_list0.sortedP_Cons_iff[code]
  linorder_list0.selsort.simps[code]
  linorder_list0.min_for_def[code]

locale linorder_list = linorder_list0 le for le::"'a::ab_group_add ⇒ _" +
  fixes S
  assumes order_refl: "a ∈ S ⟹ le a a"
  assumes trans': "a ∈ S ⟹ b ∈ S ⟹ c ∈ S ⟹ a ≠ b ⟹ b ≠ c ⟹ a ≠ c ⟹
    le a b ⟹ le b c ⟹ le a c"
  assumes antisym: "a ∈ S ⟹ b ∈ S ⟹ le a b ⟹ le b a ⟹ a = b"
  assumes linear': "a ∈ S ⟹ b ∈ S ⟹ a ≠ b ⟹ le a b ∨ le b a"
begin

lemma trans: "a ∈ S ⟹ b ∈ S ⟹ c ∈ S ⟹ le a b ⟹ le b c ⟹ le a c"
  by (cases "a = b" "b = c" "a = c"
    rule: bool.exhaust[case_product bool.exhaust[case_product bool.exhaust]])
    (auto simp: order_refl intro: trans')

lemma linear: "a ∈ S ⟹ b ∈ S ⟹ le a b ∨ le b a"
  by (cases "a = b") (auto simp: linear' order_refl)

lemma min_le1: "w ∈ S ⟹ y ∈ S ⟹ le (min_for w y) y"
  and min_le2: "w ∈ S ⟹ y ∈ S ⟹ le (min_for w y) w"
  using linear
  by (auto simp: min_for_def refl)

lemma fold_min:
  assumes "set xs ⊆ S"
  shows "list_all (λy. le (fold min_for (tl xs) (hd xs)) y) xs"
proof (cases xs)
  case (Cons y ys)
  hence subset: "set (y#ys) ⊆ S" using assms
    by auto
  show ?thesis
    unfolding Cons list.sel
    using subset
  proof (induct ys arbitrary: y)
    case (Cons z zs)
    hence IH: "⋀y. y ∈ S ⟹ list_all (le (fold min_for zs y)) (y # zs)"
      by simp
    let ?f = "fold min_for zs (min_for z y)"
    have "?f ∈ set ((min_for z y)#zs)"
      unfolding min_for_def[abs_def]
      by (rule fold_if_in_set)
    also have "… ⊆ S" using Cons.prems by auto
    finally have "?f ∈ S" .

    have "le ?f (min_for z y)"
      using IH[of "min_for z y"] Cons.prems
      by auto
    moreover have "le (min_for z y) y" "le (min_for z y) z" using Cons.prems
      by (auto intro!: min_le1 min_le2)
    ultimately have "le ?f y" "le ?f z" using Cons.prems ‹?f ∈ S›
      by (auto intro!: trans[of ?f "min_for z y"])
    thus ?case
      using IH[of "min_for z y"]
      using Cons.prems
      by auto
  qed (simp add: order_refl)
qed simp

lemma
  sortedP_selsort:
  assumes "set xs ⊆ S"
  shows "sortedP (selsort xs)"
  using assms
proof (induction xs rule: selsort.induct)
  case (2 z zs)
  from this fold_min[of "z#zs"]
  show ?case
    by (fastforce simp: list_all_iff Let_def
        simp del: remove1.simps
        intro: Cons intro!: 2(1)[OF refl refl]
        dest!: rev_subsetD[OF _ set_remove1_subset])+
qed (auto intro!: Nil)

end


subsection ‹Abstract CCW Systems›

locale ccw_system0 =
  fixes ccw::"'a ⇒ 'a ⇒ 'a ⇒ bool"
    and S::"'a set"
begin

abbreviation "indelta t p q r ≡ ccw t q r ∧ ccw p t r ∧ ccw p q t"
abbreviation "insquare p q r s ≡ ccw p q r ∧ ccw q r s ∧ ccw r s p ∧ ccw s p q"

end

abbreviation "distinct3 p q r ≡ ¬(p = q ∨ p = r ∨ q = r)"
abbreviation "distinct4 p q r s ≡ ¬(p = q ∨ p = r ∨ p = s ∨ ¬ distinct3 q r s)"
abbreviation "distinct5 p q r s t ≡ ¬(p = q ∨ p = r ∨ p = s ∨ p = t ∨ ¬ distinct4 q r s t)"

abbreviation "in3 S p q r ≡ p ∈ S ∧ q ∈ S ∧ r ∈ S"
abbreviation "in4 S p q r s ≡ in3 S p q r ∧ s ∈ S"
abbreviation "in5 S p q r s t ≡ in4 S p q r s ∧ t ∈ S"

locale ccw_system12 = ccw_system0 +
  assumes cyclic: "ccw p q r ⟹ ccw q r p"
  assumes ccw_antisym: "distinct3 p q r ⟹ in3 S p q r ⟹ ccw p q r ⟹ ¬ ccw p r q"

locale ccw_system123 = ccw_system12 +
  assumes nondegenerate: "distinct3 p q r ⟹ in3 S p q r ⟹ ccw p q r ∨ ccw p r q"
begin

lemma not_ccw_eq: "distinct3 p q r ⟹ in3 S p q r ⟹ ¬ ccw p q r ⟷ ccw p r q"
  using ccw_antisym nondegenerate by blast

end

locale ccw_system4 = ccw_system123 +
  assumes interior:
    "distinct4 p q r t ⟹ in4 S p q r t ⟹ ccw t q r ⟹ ccw p t r ⟹ ccw p q t ⟹ ccw p q r"
begin

lemma interior':
  "distinct4 p q r t ⟹ in4 S p q r t ⟹ ccw p q t ⟹ ccw q r t ⟹ ccw r p t ⟹ ccw p q r"
  by (metis ccw_antisym cyclic interior nondegenerate)

end

locale ccw_system1235' = ccw_system123 +
  assumes dual_transitive:
    "distinct5 p q r s t ⟹ in5 S p q r s t ⟹
      ccw s t p ⟹ ccw s t q ⟹ ccw s t r ⟹ ccw t p q ⟹ ccw t q r ⟹ ccw t p r"

locale ccw_system1235 = ccw_system123 +
  assumes transitive: "distinct5 p q r s t ⟹ in5 S p q r s t ⟹
    ccw t s p ⟹ ccw t s q ⟹ ccw t s r ⟹ ccw t p q ⟹ ccw t q r ⟹ ccw t p r"
begin

lemmas ccw_axioms = cyclic nondegenerate ccw_antisym transitive

sublocale ccw_system1235'
proof (unfold_locales, rule ccontr, goal_cases)
  case prems: (1 p q r s t)
  hence "ccw s p q ⟹ ccw s r p"
    by (metis ccw_axioms prems)
  moreover
  have "ccw s r p ⟹ ccw s q r"
    by (metis ccw_axioms prems)
  moreover
  have "ccw s q r ⟹ ccw s p q"
    by (metis ccw_axioms prems)
  ultimately
  have "ccw s p q ∧ ccw s r p ∧ ccw s q r ∨ ccw s q p ∧ ccw s p r ∧ ccw s r q"
    by (metis ccw_axioms prems)
  thus False
    by (metis ccw_axioms prems)
qed

end

locale ccw_system = ccw_system1235 + ccw_system4

end