section {* Counterclockwise *}
theory Counterclockwise
imports Multivariate_Analysis
begin
text {*\label{sec:counterclockwise}*}

lemma fold_if_in_set:
  "fold (\<lambda>x m. if P x m then x else m) xs x \<in> set (x#xs)"
  by (induct xs arbitrary: x) auto

subsection {* Sort Elements of a List *}

locale linorder_list0 = fixes LE::"'a \<Rightarrow> 'a \<Rightarrow> bool"
begin

definition "MIN a b = (if LE a b then a else b)"

lemma MIN_in[simp]: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> MIN x y \<in> S"
  by (auto simp: MIN_def)

lemma fold_min_eqI1: "fold MIN ys y \<notin> set ys \<Longrightarrow> fold MIN ys y = y"
  using fold_if_in_set[of _ ys y]
  by (auto simp: MIN_def[abs_def])

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

lemma in_set_selsort_eq: "x \<in> set (selsort xs) \<longleftrightarrow> x \<in> (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: split_if_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)

inductive sortedP :: "'a list \<Rightarrow> bool" where
  Nil: "sortedP []"
| Cons: "\<forall>y\<in>set ys. LE x y \<Longrightarrow> sortedP ys \<Longrightarrow> 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 & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. LE x y))"
  by (induct xs) (auto intro!: Nil Cons elim!: sortedP_Cons)

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

end

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

locale linorder_list = linorder_list0 LE for LE::"'a::ab_group_add \<Rightarrow> _" +
  fixes S
  assumes order_refl: "a \<in> S \<Longrightarrow> LE a a"
  assumes trans': "a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> c \<in> S \<Longrightarrow> a \<noteq> b \<Longrightarrow> b \<noteq> c \<Longrightarrow> a \<noteq> c \<Longrightarrow> LE a b \<Longrightarrow> LE b c \<Longrightarrow> LE a c"
  assumes antisym: "a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> LE a b \<Longrightarrow> LE b a \<Longrightarrow> a = b"
  assumes linear': "a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> a \<noteq> b \<Longrightarrow> LE a b \<or> LE b a"
begin

lemma trans: "a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> c \<in> S \<Longrightarrow> LE a b \<Longrightarrow> LE b c \<Longrightarrow> 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 \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> LE a b \<or> LE b a"
  by (cases "a = b") (auto simp: linear' order_refl)

lemma MIN_le1: "w \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> LE (MIN w y) y"
  and MIN_le2: "w \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> LE (MIN w y) w"
  using local.linear
  by (auto simp: MIN_def refl)

lemma fold_min:
  assumes "set xs \<subseteq> S"
  shows "list_all (\<lambda>y. LE (fold MIN (tl xs) (hd xs)) y) xs"
proof (cases xs)
  case (Cons y ys)
  hence subset: "set (y#ys) \<subseteq> S" using assms
    by auto
  show ?thesis
    unfolding Cons list.sel
    using subset
  proof (induct ys arbitrary: y)
    case Nil thus ?case using subset by (simp add: order_refl)
  next
    case (Cons z zs)
    hence IH: "\<And>y. y \<in> S \<Longrightarrow> list_all (LE (fold MIN zs y)) (y # zs)"
      by simp
    let ?f = "fold MIN zs (MIN z y)"
    have "?f \<in> set ((MIN z y)#zs)"
      unfolding MIN_def[abs_def]
      by (rule fold_if_in_set)
    also have "\<dots> \<subseteq> S" using Cons.prems by auto
    finally have "?f \<in> S" .

    have "LE ?f (MIN z y)"
      using IH[of "MIN z y"] Cons.prems
      by auto
    moreover have "LE (MIN z y) y" "LE (MIN 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 \<in> S`
      by (auto intro!: trans[of ?f "MIN z y"])
    thus ?case
      using IH[of "MIN z y"]
      using Cons.prems
      by auto
  qed
qed simp

lemma
  sortedP_selsort:
  assumes "set xs \<subseteq> S"
  shows "sortedP (selsort xs)"
  using assms
proof (induct xs rule: selsort.induct)
  case 1 thus ?case by (auto intro!: Nil)
next
  case (2 z zs)
  show ?case
  proof cases
    assume "fold MIN zs z = z"
    thus ?thesis
      using fold_min[of "z#zs"] 2
      by (auto simp: list_all_iff intro!: Cons )
  next
    assume "fold MIN zs z \<noteq> z"
    thus ?thesis
      unfolding selsort.simps
      unfolding Let_def
      apply (intro Cons)
      apply (simp del: remove1.simps)
      apply (rule )
      apply (drule set_rev_mp)
      apply (rule set_remove1_subset)
      using fold_min[of "z#zs"] 2(2)
      apply (force simp: list_all_iff)
      apply (rule 2(1)[OF refl refl])
      using 2(2)
      apply (auto )
      apply (metis (no_types) contra_subsetD notin_set_remove1)
      done
  qed
qed

end


subsection {* Abstract CCW Systems *}

locale ccw_system0 =
  fixes ccw::"'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
    and S::"'a set"
begin

abbreviation "indelta t p q r \<equiv> ccw t q r \<and> ccw p t r \<and> ccw p q t"
abbreviation "insquare p q r s \<equiv> ccw p q r \<and> ccw q r s \<and> ccw r s p \<and> ccw s p q"

end

abbreviation "distinct3 p q r \<equiv> \<not>(p = q \<or> p = r \<or> q = r)"
abbreviation "distinct4 p q r s \<equiv> \<not>(p = q \<or> p = r \<or> p = s \<or> \<not> distinct3 q r s)"
abbreviation "distinct5 p q r s t \<equiv> \<not>(p = q \<or> p = r \<or> p = s \<or> p = t \<or> \<not> distinct4 q r s t)"

abbreviation "in3 S p q r \<equiv> p \<in> S \<and> q \<in> S \<and> r \<in> S"
abbreviation "in4 S p q r s \<equiv> in3 S p q r \<and> s \<in> S"
abbreviation "in5 S p q r s t \<equiv> in4 S p q r s \<and> t \<in> S"

locale ccw_system12 = ccw_system0 +
  assumes cyclic: "ccw p q r \<Longrightarrow> ccw q r p"
  assumes ccw_antisym: "distinct3 p q r \<Longrightarrow> in3 S p q r \<Longrightarrow> ccw p q r \<Longrightarrow> \<not> ccw p r q"

locale ccw_system123 = ccw_system12 +
  assumes nondegenerate: "distinct3 p q r \<Longrightarrow> in3 S p q r \<Longrightarrow> ccw p q r \<or> ccw p r q"
begin

lemma not_ccw_eq: "distinct3 p q r \<Longrightarrow> in3 S p q r \<Longrightarrow> \<not> ccw p q r \<longleftrightarrow> ccw p r q"
  using ccw_antisym nondegenerate by blast

end

locale ccw_system4 = ccw_system123 +
  assumes interior:
    "distinct4 p q r t \<Longrightarrow> in4 S p q r t \<Longrightarrow> ccw t q r \<Longrightarrow> ccw p t r \<Longrightarrow> ccw p q t \<Longrightarrow> ccw p q r"
begin

lemma interior':
  "distinct4 p q r t \<Longrightarrow> in4 S p q r t \<Longrightarrow> ccw p q t \<Longrightarrow> ccw q r t \<Longrightarrow> ccw r p t \<Longrightarrow> 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 \<Longrightarrow> in5 S p q r s t \<Longrightarrow>
      ccw s t p \<Longrightarrow> ccw s t q \<Longrightarrow> ccw s t r \<Longrightarrow> ccw t p q \<Longrightarrow> ccw t q r \<Longrightarrow> ccw t p r"

locale ccw_system1235 = ccw_system123 +
  assumes transitive: "distinct5 p q r s t \<Longrightarrow> in5 S p q r s t \<Longrightarrow>
    ccw t s p \<Longrightarrow> ccw t s q \<Longrightarrow> ccw t s r \<Longrightarrow> ccw t p q \<Longrightarrow> ccw t q r \<Longrightarrow> ccw t p r"
begin

lemmas ccw_axioms = cyclic nondegenerate ccw_antisym transitive

sublocale ccw_system1235'
(*  by (unfold_locales, smt cyclic local.transitive nondegenerate) *)
proof (unfold_locales, rule ccontr)
  case goal1
  hence "ccw s p q \<Longrightarrow> ccw s r p"
    by (metis ccw_axioms goal1)
  moreover
  have "ccw s r p \<Longrightarrow> ccw s q r"
    by (metis ccw_axioms goal1)
  moreover
  have "ccw s q r \<Longrightarrow> ccw s p q"
    by (metis ccw_axioms goal1)
  ultimately
  have "ccw s p q \<and> ccw s r p \<and> ccw s q r \<or> ccw s q p \<and> ccw s p r \<and> ccw s r q"
    by (metis ccw_axioms goal1)
  thus False
    by (metis ccw_axioms goal1)
qed

end

locale ccw_system = ccw_system1235 + ccw_system4
begin

text {* TODO: sorting/ordering here? *}

end

end
