Theory Treap_Sort_and_BSTs
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