Theory Treap_Sort_and_BSTs

theory Treap_Sort_and_BSTs
imports Treap Random_List_Permutation Random_BSTs
(*
  File:      Treap_Sort_and_BSTs.thy
  Authors:   Max Haslbeck
*)
section ‹Relationship between treaps and BSTs›
theory Treap_Sort_and_BSTs
imports
  Treap
  Random_List_Permutation
  "Random_BSTs.Random_BSTs"
begin

text ‹
  Here, we will show that if we ``forget'' the priorities of a treap, we essentially get a
  BST into which the elements have been inserted by ascending priority.

  First, we show some facts about sorting that we will need.
›

text ‹
  The following two lemmas are only important for measurability later.
›
lemma insort_key_conv_rec_list:
  "insort_key f x xs =
     rec_list [x] (λy ys zs. if f x ≤ f y then x # y # ys else y # zs) xs"
  by (induction xs) simp_all

lemma insort_key_conv_rec_list':
  "insort_key = (λf x.
     rec_list [x] (λy ys zs. if f x ≤ f y then x # y # ys else y # zs))"
  by (intro ext) (simp add: insort_key_conv_rec_list)

lemma bst_of_list_trees:
  assumes "set ys ⊆ A"
  shows "bst_of_list ys ∈ trees A"
  using assms by (induction ys rule: bst_of_list.induct) auto

lemma insort_wrt_insort_key:
   "a ∈ A ⟹
   set xs ⊆ A ⟹
   insert_wrt (linorder_from_keys A f) a xs = insort_key f a xs"
 unfolding linorder_from_keys_def by (induction xs) (auto)

lemma insort_wrt_sort_key:
  assumes "set xs ⊆ A"
  shows "insort_wrt (linorder_from_keys A f) xs = sort_key f xs"
  using assms by (induction xs) (auto simp add: insort_wrt_def insort_wrt_insort_key)


text ‹
  The following is an important recurrence for @{term "sort_key"} that states that for distinct
  priorities, sorting a list w.\,r.\,t.\ those priorities can be seen as selection sort, i.\,e.\ 
  we can first choose the (unique) element with minimum priority as the first element and then
  sort the rest of the list and append it.
›
lemma sort_key_arg_min_on:
  assumes "zs ≠ []"  "inj_on p (set zs)"
  shows "sort_key p (zs::'a::linorder list) = 
         (let z = arg_min_on p (set zs) in z # sort_key p (remove1 z zs))"
proof -
  have "mset zs = mset (let z = arg_min_on p (set zs) in z # sort_key p (remove1 z zs))"
  proof -
    define m where "m = arg_min_on p (set zs)"
    have "m ∈ (set zs)"
      unfolding m_def by (rule arg_min_if_finite) (use assms in auto)
    then show ?thesis
      by (auto simp add: Let_def m_def)
  qed
  moreover have "linorder_class.sorted
                 (map p (let z = arg_min_on p (set zs) in z # sort_key p (remove1 z zs)))"
  proof -
    have "set (map p (sort_key p (remove1 (arg_min_on p (set zs)) zs))) ⊆ p ` set zs"
      using set_remove1_subset by (fastforce)
    moreover have "⋀y. y ∈ p ` set zs ⟹ p (arg_min_on p (set zs)) ≤ y"
      using arg_min_least assms by force
    ultimately have "linorder_class.sorted
        (p (arg_min_on p (set zs)) # map p (sort_key p (remove1 (arg_min_on p (set zs)) zs)))"
      by (auto)
    then show ?thesis
      by (simp add: Let_def)
  qed
  ultimately show ?thesis
    using sort_key_inj_key_eq assms by blast
qed

lemma arg_min_on_image_finite:
  fixes f :: "'b ⇒ 'c :: linorder"
  assumes "inj_on f (g ` B)" "finite B" "B ≠ {}"
  shows "arg_min_on f (g ` B) = g (arg_min_on (f ∘ g) B)"
proof -
  note * = arg_min_if_finite[OF ‹finite B› ‹B ≠ {}›, of ‹f ∘ g›]
  show ?thesis
    using assms * arg_min_inj_eq
    by (smt arg_min_if_finite(1) arg_min_least 
        comp_apply finite_imageI imageE image_eqI image_is_empty inj_onD less_le)
qed

lemma fst_snd_arg_min_on: fixes p::"'a ⇒ 'b::linorder"
  assumes "finite B" "inj_on p B" "B ≠ {}"
  shows   "fst (arg_min_on snd ((λx. (x, p x)) ` B)) = arg_min_on p B"
  by (subst arg_min_on_image_finite [OF inj_on_imageI]) 
     (auto simp: o_def assms)

text ‹
  The following is now the main result:
›
theorem treap_of_bst_of_list':
  assumes "ys = map (λx. (x, p x)) xs" "inj_on p (set xs)" "xs' = sort_key p xs"
  shows "map_tree fst (treap_of (set ys)) = bst_of_list xs'"
  using assms
proof(induction xs' arbitrary: xs ys rule: bst_of_list.induct)
  case 1
  from ‹[] = sort_key p xs›[symmetric] ‹ys = map (λx. (x, p x)) xs›
  have "ys = []"
    by (cases xs) (auto)
  then show ?case by (simp add: treap_of.simps)
next
  case (2 z zs)
  note IH = 2(1,2)
  note assms = 2(3,4,5)
  define m where "m = arg_min_on snd (set ys)"
  define ls where "ls = map (λx. (x, p x)) [y←zs . y < z]"
  define rs where "rs = map (λx. (x, p x)) [y←zs . y > z]"
  define L where "L = {p ∈ (set ys). fst p < fst m}"
  define R where "R = {p ∈ (set ys). fst p > fst m}"
  have h1: "set (z#zs) = set xs"
    using assms by simp
  then have h2: "inj_on p {x ∈ set zs. x < z}" "inj_on p (set (filter ((<) z) zs))"
    "inj_on p (set zs)"
    using ‹inj_on p (set xs)› by (auto intro!: inj_on_subset[of _ "set xs"])
  have "z # zs = (let z = arg_min_on p (set xs) in z # sort_key p (remove1 z xs))"
  proof -
    have "xs ≠ []"
      using assms by force
    then show ?thesis
      by (auto simp add: assms intro!: sort_key_arg_min_on)
  qed
  then have h3: "z = arg_min_on p (set xs)" "zs = sort_key p (remove1 z xs)"
    unfolding Let_def by auto
  have h4: "sort_key p zs = zs"
  proof -
    have "linorder_class.sorted (map p (z#zs))"
      using assms by simp
    then have "linorder_class.sorted (map p zs)"
      by auto
    then show ?thesis
      using h1 h2 sort_key_inj_key_eq by blast
  qed
  note helpers = h1 h2 h3 h4
  have "fst m = z"
  proof -
    have "fst m = arg_min_on p (set xs)"
      unfolding m_def using assms by (auto intro!: fst_snd_arg_min_on)
    also have "… = z"
      using helpers by auto
    finally show ?thesis .
  qed
  moreover have "map_tree fst (treap_of L) = bst_of_list [y←zs . y < z]"
  proof -
    have "L = set ls"
      unfolding L_def ls_def ‹fst m = z› using helpers assms by force
    moreover have "map_tree fst (treap_of (set ls)) = bst_of_list [y←zs . y < z]"
      unfolding ls_def using helpers 
      by (intro IH(1)[of _ "[y←zs . y < z]"]) (auto simp add: filter_sort[symmetric])
    ultimately show ?thesis
      by blast
  qed
  moreover have "map_tree fst (treap_of R) = bst_of_list [y←zs . z < y]"
  proof -
    have 0: "R = set rs"
      unfolding R_def rs_def ‹fst m = z› using helpers assms by force
    moreover have "map_tree fst (treap_of (set rs)) = bst_of_list [y←zs . z < y]"
      unfolding rs_def using helpers
      by (intro IH(2)[of _ "[y←zs . z < y]"]) (auto simp add: filter_sort[symmetric])
    ultimately show ?thesis
      by blast
  qed
  moreover have "treap_of (set ys) = ⟨treap_of L, m, treap_of R⟩"
    unfolding L_def m_def R_def using assms by (auto simp add: treap_of.simps Let_def)
  ultimately show ?case by auto
qed

corollary treap_of_bst_of_list: "inj_on p (set zs) ⟹
   map_tree fst (treap_of (set (map (λx. (x, p x)) zs))) = bst_of_list (sort_key p zs)"
  using treap_of_bst_of_list' by blast

corollary treap_of_bst_of_list'': "inj_on p (set zs) ⟹
   map_tree fst (treap_of ((λx. (x, p x)) ` set zs)) = bst_of_list (sort_key p zs)"
  using treap_of_bst_of_list by auto

corollary fold_ins_bst_of_list: "distinct zs ⟹ inj_on p (set zs) ⟹
   map_tree fst (foldl (λt (x,p). ins x p t) ⟨⟩ (map (λx. (x, p x)) zs)) = bst_of_list (sort_key p zs)"
  by (auto simp add: foldl_ins_treap_of distinct_map inj_on_def inj_on_convol_ident
                     treap_of_bst_of_list'')

end