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; xA. f x  0  sum f A = 0  (xA. 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: "yset 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