Theory Sorting_Util

theory Sorting_Util
  imports Main
begin

section ‹Lemmas about bijections›

text ‹A convenient definition of an inverses between two sets›
definition 
  inverses_on :: 
  "('a ⇒ 'b) ⇒ ('b ⇒ 'a) ⇒ 'a set ⇒ 'b set ⇒ bool"
where
  "inverses_on f g A B ⟷ 
     (∀x ∈ A. g (f x) = x) ∧ 
     (∀x ∈ B. f (g x) = x)"

lemmas inverses_onD1 = inverses_on_def[THEN iffD1, THEN conjunct1]
lemmas inverses_onD2 = inverses_on_def[THEN iffD1, THEN conjunct2]

text ‹The inverses relation over maps›

lemma inverses_on_mapD:
  assumes "inverses_on (map f) (map g) {xs. set xs ⊆ A} {xs. set xs ⊆ B}"
  shows "inverses_on f g A B"
proof -
  from inverses_onD1[OF assms, THEN bspec, of "[_]", simplified]
  have "∀x ∈ A. g (f x) = x"
    by blast
  moreover
  from inverses_onD2[OF assms, THEN bspec, of "[_]", simplified]
  have "∀x ∈ B. f (g x) = x"
    by blast
  ultimately show ?thesis
    by (simp add: inverses_on_def)
qed

lemma inverses_on_map:
  assumes "inverses_on f g A B"
  shows "inverses_on (map f) (map g) {xs. set xs ⊆ A} {xs. set xs ⊆ B}"
proof -
  have "∀x ∈ {xs. set xs ⊆ A}. map g (map f x) = x"
    using list_eq_iff_nth_eq inverses_onD1 assms subsetD by fastforce
  moreover
  have "∀x ∈ {xs. set xs ⊆ B}. map f (map g x) = x"
    using list_eq_iff_nth_eq inverses_onD2 assms subsetD by fastforce
  ultimately show ?thesis
    by (simp add: inverses_on_def)
qed

text ‹Inverses are symmetric›

lemma inverses_on_sym:
  "inverses_on f g A B = inverses_on g f B A"
  apply (simp add: inverses_on_def)
  apply (subst conj.commute)
  apply simp
  done

text ‹Convenient theorem to obtain the inverse of a bijection between two sets›

lemma bij_betw_inv_alt:
  assumes "bij_betw f A B"
  shows "∃g. bij_betw g B A ∧ inverses_on f g A B"
  by (meson assms bij_betw_imp_inj_on bij_betw_inv_into inv_into_f_f
            bij_betw_inv_into_right inverses_on_def[THEN iffD2])

text ‹Bijections over maps›

lemma bij_betw_map:
  assumes "bij_betw f A B"
  shows "bij_betw (map f) {xs. set xs ⊆ A} {xs. set xs ⊆ B}"
proof (rule bij_betwI')
  fix x y
  assume "x ∈ {xs. set xs ⊆ A}" "y ∈ {xs. set xs ⊆ A}"
  hence P: "set x ⊆ A" "set y ⊆ A"
    by blast+
  note inj = inj_on_eq_iff[THEN iffD1, OF bij_betw_imp_inj_on[OF assms]]
  from list.inj_map_strong[OF inj, simplified]
  show "(map f x = map f y) = (x = y)"
    using P(1) P(2) by blast
next
  fix x
  assume "x ∈ {xs. set xs ⊆ A}"
  hence "set x ⊆ A"
    by blast
  then show "map f x ∈ {xs. set xs ⊆ B}"
    using assms bij_betw_imp_surj_on by fastforce
next
  fix y
  assume "y ∈ {xs. set xs ⊆ B}"
  hence "set y ⊆ B"
    by blast

  from bij_betw_inv_alt[OF assms, simplified inverses_on_def]
  obtain g where
    "bij_betw g B A"
    "∀x∈A. g (f x) = x"
    "∀x∈B. f (g x) = x"
    by blast

  have "set (map g y) ⊆ A"
    using ‹bij_betw g B A› ‹set y ⊆ B› bij_betw_imp_surj_on 
    by fastforce
  moreover
  have "y = map f (map g y)"
  proof -
    have "length y = length (map f (map g y))"
      by simp
    moreover
    have "∀i < length y. y ! i = map f (map g y) ! i"
      using ‹∀x∈B. f (g x) = x› ‹set y ⊆ B› subsetD by fastforce
    ultimately show ?thesis
      using list_eq_iff_nth_eq by blast
  qed
  ultimately have "∃x. set x ⊆ A ∧ y = map f x"
    by blast
  then show "∃x∈{xs. set xs ⊆ A}. y = map f x"
    by blast
qed

text ‹Eliminating the map from a bijection relation›

lemma bij_betw_mapD:
  assumes "bij_betw (map f) {xs. set xs ⊆ A} {xs. set xs ⊆ B}"
  shows "bij_betw f A B"
proof (intro bij_betwI' iffI)
  fix x y
  assume "x ∈ A" "y ∈ A" "f x = f y"
  with inj_onD[OF bij_betw_imp_inj_on[OF assms], of "[x]" "[y]", simplified]
  show "x = y"
    by blast
next
  fix x
  assume "x ∈ A"
  with bij_betwE[OF assms, THEN bspec, of "[x]", simplified]
  show "f x ∈ B"
    by blast
next
  fix y
  assume "y ∈ B"
  with bij_betw_imp_surj_on[OF assms, simplified]
  have "[y] ∈ map f ` {xs. set xs ⊆ A}"
    by auto
  with image_iff[THEN iffD1, of "[y]" "map f" "{xs. set xs ⊆ A}"]
  obtain x' where
    "x' ∈ {xs. set xs ⊆ A}"
    "[y] = map f x'"
    by meson
  then show "∃x∈A. y = f x"
    by auto
next
qed(clarsimp)

text ‹Obtaining the inverse over map›

lemma bij_betw_inv_map:
  assumes "bij_betw f A B"
  shows "∃g. bij_betw (map g) {xs. set xs ⊆ B} {xs. set xs ⊆ A} ∧
             inverses_on (map f) (map g) {xs. set xs ⊆ A} {xs. set xs ⊆ B}"
proof -
  from bij_betw_inv_alt[OF assms, simplified inverses_on_def]
  obtain g where
    "bij_betw g B A"
    "∀x∈A. g (f x) = x"
    "∀x∈B. f (g x) = x"
    by blast

  note bij_betw_map[OF ‹bij_betw g B A›]
  moreover
  {
    have "∀x. set x ⊆ A ⟶ map g (map f x) = x"
    proof safe
      fix x
      assume "set x ⊆ A"
      then show "map g (map f x) = x"
        by (clarsimp simp: list_eq_iff_nth_eq ‹∀x∈A. g (f x) = x› subsetD)
    qed
    moreover
    have "∀x. set x ⊆ B ⟶ map f (map g x) = x"
    proof safe
      fix x
      assume "set x ⊆ B"
      then show "map f (map g x) = x"
        by (clarsimp simp: list_eq_iff_nth_eq ‹∀x∈B. f (g x) = x› subsetD)
    qed
    ultimately have 
      "inverses_on (map f) (map g) {xs. set xs ⊆ A} {xs. set xs ⊆ B}"
      by (simp add: inverses_on_def)
  }
  ultimately show ?thesis
    by blast
qed

section "Lemmas about monotone functions"

text ‹Note that the base version of monotone is used as 
      the sorts cause some issues with the types›

text ‹Essentially a general version of @{thm strict_mono_less}›

lemma monotone_on_iff:
  assumes "monotone_on A orda ordb f"
  and     "asymp_on A orda"
  and     "totalp_on A orda"
  and     "asymp_on (f ` A) ordb"
  and     "totalp_on (f ` A) ordb"
  and     "x ∈ A"
  and     "y ∈ A"
shows "orda x y ⟷ ordb (f x) (f y)"
proof (safe)
  show "orda x y ⟹ ordb (f x) (f y)"
    by (meson assms monotone_onD)
next
  show "ordb (f x) (f y) ⟹ orda x y"
    by (metis (full_types) assms(1,3,4,6,7) 
          asymp_onD monotone_onD totalp_onD imageI)
qed

text ‹The inverse of a monotonic function is also monotonic›

lemma monotone_on_bij_betw_inv:
  assumes "monotone_on A orda ordb f"
  and     "asymp_on A orda"
  and     "totalp_on A orda"
  and     "asymp_on B ordb"
  and     "totalp_on B ordb"
  and     "bij_betw f A B"
  and     "bij_betw g B A"
  and     "inverses_on f g A B"
shows "monotone_on B ordb orda g"
proof (rule monotone_onI)
  fix x y
  assume "x ∈ B" "y ∈ B" "ordb x y"
  moreover
  have "g x ∈ A"
    using ‹bij_betw g B A› bij_betwE calculation(1) by auto
  moreover
  have "f (g x) = x"
    using assms(8) calculation(1) inverses_onD2 by blast
  moreover
  have "g y ∈ A"
    using ‹bij_betw g B A› bij_betwE calculation(2) by auto
  moreover
  have "f (g y) = y"
    using assms(8) calculation(2) inverses_onD2 by blast
  ultimately show "orda (g x) (g y)"
    using assms bij_betw_imp_surj_on monotone_on_iff by fastforce
qed

lemma monotone_on_bij_betw:
  assumes "monotone_on A orda ordb f"
  and     "asymp_on A orda"
  and     "totalp_on A orda"
  and     "asymp_on B ordb"
  and     "totalp_on B ordb"
  and     "bij_betw f A B"
shows "∃g. bij_betw g B A ∧ inverses_on f g A B ∧ monotone_on B ordb orda g"
  using assms bij_betw_inv_alt monotone_on_bij_betw_inv by fastforce

section "Sorting"

subsection "General sorting"

text ‹Intro for @{const sorted_wrt}›

lemmas sorted_wrtI = sorted_wrt_iff_nth_less[THEN iffD2, OF allI, OF allI, OF impI, OF impI]

lemma sorted_wrt_mapI:
  "(⋀i j. ⟦i < j; j < length xs⟧ ⟹ P (f (xs ! i)) (f (xs ! j))) ⟹
    sorted_wrt P (map f xs)"
  by (metis (mono_tags, lifting) length_map nth_map order_less_trans sorted_wrtI)

lemma sorted_wrt_mapD:
  "(⋀i j. ⟦sorted_wrt P (map f xs); i < j; j < length xs⟧ ⟹ P (f (xs ! i)) (f (xs ! j)))"
  by (metis (mono_tags, lifting) length_map nth_map order_less_trans sorted_wrt_iff_nth_less)

lemma monotone_on_sorted_wrt_map:
  assumes "monotone_on A orda ordb f"
  and     "sorted_wrt orda xs"
  and     "set xs ⊆ A"
shows "sorted_wrt ordb (map f xs)"
proof (rule sorted_wrt_mapI)
  fix i j
  assume "i < j" "j < length xs"
  with sorted_wrt_nth_less[OF assms(2)]
  have "orda (xs ! i) (xs ! j)"
    by blast
  with monotone_onD[OF assms(1), of "xs ! i" "xs ! j"] assms(3)
  show "ordb (f (xs ! i)) (f (xs ! j))"
    by (meson ‹i < j› ‹j < length xs› nth_mem order_less_trans subsetD)
qed

lemma monotone_on_map_sorted_wrt:
  assumes "monotone_on A orda ordb f"
  and     "asymp_on A orda"
  and     "totalp_on A orda"
  and     "asymp_on (f ` A) ordb"
  and     "totalp_on (f ` A) ordb"
  and     "sorted_wrt ordb (map f xs)"
  and     "set xs ⊆ A"
shows "sorted_wrt orda xs"
proof (rule sorted_wrtI)
  fix i j
  assume "i < j" "j < length xs"
  with sorted_wrt_nth_less[OF assms(6)]
  have "ordb (f (xs ! i)) (f (xs ! j))"
    by force
  with monotone_on_iff[OF assms(1-3), of "xs ! i" "xs ! j"]
  show "orda (xs ! i) (xs ! j)"
    using ‹i < j› ‹j < length xs› assms(4,5,7) 
          nth_mem order_less_trans by blast
qed

subsection "Sorting on linear orders"

context linorder begin

abbreviation "strict_sorted xs ≡ sorted_wrt (<) xs"

lemma sorted_nth_less_mono:
  "⟦sorted xs; i < length xs; j < length xs; i ≠ j; xs ! i < xs ! j⟧ ⟹ i < j"
  by (meson linorder_neqE_nat not_less sorted_iff_nth_mono_less)

lemma strict_sorted_nth_less_mono:
  "⟦strict_sorted xs; i < length xs; j < length xs; i ≠ j; xs ! i < xs ! j⟧ ⟹ i < j"
  using strict_sorted_iff sorted_nth_less_mono by blast

lemma strict_sorted_Min:
  "⟦strict_sorted xs; xs ≠ []⟧ ⟹ xs ! 0 = Min (set xs)"
  by (metis finite_set list.simps(15) Min_insert2 strict_sorted_imp_sorted
            nth_Cons_0 sorted_wrt.elims(2))

lemma strict_sorted_take:
  assumes "strict_sorted xs"
  and     "i < length xs"
  shows "set (take i xs) = {x. x ∈ set xs ∧ x < xs ! i}"
proof (safe)
  fix x
  assume "x ∈ set (take i xs)"
  then show "x ∈ set xs"
    by (meson in_set_takeD)
next
  fix x
  assume "x ∈ set (take i xs)"
  then show "x < xs ! i"
    by (metis assms id_take_nth_drop list.set_intros(1) sorted_wrt_append)
next
  fix x
  assume "x ∈ set xs" "x < xs ! i"
  hence "∃j < length xs. xs ! j = x"
    by (simp add: in_set_conv_nth)
  then obtain j where
    "j < length xs" "xs ! j = x"
    by blast
  with strict_sorted_nth_less_mono[OF assms(1) _ assms(2), of j] ‹x < xs ! i›
  have "j < i"
    by blast
  then show "x ∈ set (take i xs)"
    using ‹j < length xs› ‹xs ! j = x› in_set_conv_nth by fastforce
qed

lemma strict_sorted_card_idx:
  "⟦strict_sorted xs; i < length xs⟧ ⟹ card {x. x ∈ set xs ∧ x < xs ! i} = i"
  by (metis (mono_tags, lifting) distinct_card distinct_take length_take strict_sorted_iff
                                 ord_class.min_def order_class.leD strict_sorted_take)

lemmas strict_sorted_distinct_set_unique =
  sorted_distinct_set_unique[OF strict_sorted_imp_sorted _ strict_sorted_imp_sorted]

lemma sorted_and_distinct_imp_strict_sorted:
  "⟦sorted xs; distinct xs⟧ ⟹ strict_sorted xs"
  using strict_sorted_iff
  by blast

lemma filter_sorted:
  "sorted xs ⟹ sorted (filter P xs)"
  using sorted_wrt_filter by blast

lemma sorted_nth_eq:
  assumes "sorted xs"
  and     "j < length xs"
  and     "xs ! i = xs ! j"
  and     "i ≤ k"
  and     "k ≤ j"
shows "xs ! k = xs ! i"
  by (metis assms sorted_iff_nth_mono preorder_class.le_less_trans nle_le)

lemma sorted_find_Min:
  "sorted xs ⟹ ∃x ∈ set xs. P x ⟹ List.find P xs = Some (Min {x∈set xs. P x})"
proof (induct xs)
  case Nil then show ?case by simp
next
  case (Cons x xs) show ?case
  proof (cases "P x")
    case True
    with Cons show ?thesis by (auto intro: Min_eqI [symmetric])
  next
    case False then have "{y. (y = x ∨ y ∈ set xs) ∧ P y} = {y ∈ set xs. P y}"
      by auto
    with Cons False show ?thesis by (simp_all)
  qed
qed

lemma sorted_cons_nil:
  "xs = [] ⟹ sorted (x # xs)"
  by simp

lemma sorted_consI:
  "⟦xs ≠ []; sorted xs; x ≤ xs ! 0⟧ ⟹ sorted (x # xs)"
  by (metis list.exhaust sorted2_simps(2) nth_Cons_0)

end (* of context *)

subsection "Sorting on orders"

context order begin

lemma strict_mono_strict_sorted_map_1:
  assumes "strict_mono α"
  and     "strict_sorted xs"
shows "strict_sorted (map α xs)"
  using assms(1) assms(2) monotone_on_sorted_wrt_map by blast

lemma strict_mono_sorted_map_2:
  assumes "strict_mono α"
  and     "strict_sorted (map α xs)"
shows "strict_sorted xs"
  using assms(1) assms(2) monotone_on_map_sorted_wrt by fastforce

end (* of context *)

section "Mapping elements to natural numbers"

text ‹This section contains a mapping from elements to natural numbers that maintains ordering.›

definition elm_rank :: "('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ 'a ⇒ nat"
  where
"elm_rank ord A x = card {y. y ∈ A ∧ ord y x}"

lemma monotone_on_elm_rank:
  assumes "finite A"
  and     "transp_on A ord"
  and     "irreflp_on A ord"
  shows "monotone_on A ord (<) (elm_rank ord A)"
proof (rule monotone_onI)
  fix a b
  assume "a ∈ A" "b ∈ A" "ord a b"

  have "{y. y ∈ A ∧ ord y a} ⊆ {y. y ∈ A ∧ ord y b}"
  proof safe
    fix x
    assume "x ∈ A" "ord x a"
    then show "ord x b"
      by (meson ‹a ∈ A› ‹b ∈ A› ‹ord a b› assms(2) transp_onD)
  qed
  moreover
  have "a ∈ {y. y ∈ A ∧ ord y b}"
    by (simp add: ‹a ∈ A› ‹ord a b›)
  moreover
  have "a ∉ {y. y ∈ A ∧ ord y a}"
    using assms(3) irreflp_onD by fastforce
  ultimately have "{y. y ∈ A ∧ ord y a} ⊂ {y. y ∈ A ∧ ord y b}"
    by blast
  then show "elm_rank ord A a < elm_rank ord A b"
    by (simp add: elm_rank_def assms(1) psubset_card_mono)
qed

lemma elm_rank_insert_min:
  assumes "finite A"
  and     "x ∉ A"
  and     "∀y ∈ A. ord x y"
  and     "z ∈ A"
shows "elm_rank ord (insert x A) z = Suc (elm_rank ord A z)"
  unfolding elm_rank_def
proof -
  have "ord x z"
    by (simp add: assms(3,4))
  hence "{y ∈ insert x A. ord y z} = insert x {y ∈ A. ord y z}"
    by safe
  moreover
  have "x ∉ {y ∈ A. ord y z}"
    using assms(2) by auto
  ultimately show "card {y ∈ insert x A. ord y z} = Suc (card {y ∈ A. ord y z})"
    by (simp add: assms(1))
qed

definition (in order) elem_rank :: "'a set ⇒ 'a ⇒ nat"
  where
"elem_rank = elm_rank (<)"

lemma (in order) strict_mono_on_elem_rank:
  assumes "finite A"
  shows "strict_mono_on A (elem_rank A)"
  by (simp add: assms elem_rank_def monotone_on_elm_rank)

lemma (in linorder) bij_betw_elem_rank_upt:
  assumes "finite A"
  shows "bij_betw (elem_rank A) A {0..<card A}"
proof -
  have "⋀x. x ∈ A ⟹ {y. y ∈ A ∧ y < x} ⊂ A"
    by blast
  hence "⋀x. x ∈ A ⟹ card {y. y ∈ A ∧ y < x} < card A"
    by (meson assms psubset_card_mono)
  hence "⋀x. x ∈ A ⟹ elem_rank A x ∈ {0..<card A}"
    by (simp add: elm_rank_def elem_rank_def)
  moreover
  have "⋀x y. ⟦x ∈ A; y ∈ A⟧ ⟹ (elem_rank A x = elem_rank A y) = (x = y)"
    by (metis assms less_irrefl_nat antisym_conv3 ord.strict_mono_onD strict_mono_on_elem_rank)
  moreover
  {
    let ?xs = "sorted_list_of_set A"
    have "strict_sorted ?xs"
      by simp
    moreover
    have "⋀x. elem_rank A x = elem_rank (set ?xs) x"
      using assms by force
    moreover
    have "⋀y. y < length ?xs ⟹ y = elem_rank (set ?xs) (?xs ! y)"
      by (metis (no_types, lifting) Collect_cong calculation(1) elem_rank_def elm_rank_def
                                    strict_sorted_card_idx)
    ultimately have "⋀y. y ∈ {0..<card A} ⟹ ∃x∈A. y = elem_rank A x"
      by (metis assms length_sorted_list_of_set set_sorted_list_of_set nth_mem
                ord_class.atLeastLessThan_iff)
  }
  ultimately show ?thesis
    using bij_betwI' by blast
qed

lemma (in order) elem_rank_insert_min:
  "⟦finite A; x ∉ A; ∀y∈A. x < y; z ∈ A⟧ ⟹ elem_rank (insert x A) z = Suc (elem_rank A z)"
  by (simp add: elm_rank_insert_min elem_rank_def)
end