Theory Treap

(*
  File:      Treap.thy
  Authors:   Tobias Nipkow, Max Haslbeck
*)
section ‹Treaps›
theory Treap
imports
  "HOL-Library.Tree"
begin

definition treap :: "('k::linorder * 'p::linorder) tree ⇒ bool" where
"treap t = (bst (map_tree fst t) ∧ heap (map_tree snd t))"

abbreviation "keys t ≡ set_tree (map_tree fst t)"
abbreviation "prios t ≡ set_tree (map_tree snd t)"

function treap_of :: "('k::linorder * 'p::linorder) set ⇒ ('k * 'p) tree" where
"treap_of KP = (if infinite KP ∨ KP = {} then Leaf else
  let m = arg_min_on snd KP;
      L = {p ∈ KP. fst p < fst m};
      R = {p ∈ KP. fst p > fst m}
  in Node (treap_of L) m (treap_of R))"
by pat_completeness auto
termination
proof (relation "measure card")
  show "wf (measure card)"  by simp
next
  fix KP :: "('a × 'b) set" and m L
  assume KP: "¬ (infinite KP ∨ KP = {})"
  and m: "m = arg_min_on snd KP"
  and L: "L = {p ∈ KP. fst p < fst m}"
  have "m ∈ KP" using KP arg_min_if_finite(1) m by blast
  thus  "(L, KP) ∈ measure card" using KP L by(auto intro!: psubset_card_mono)
next
  fix KP :: "('a × 'b) set" and m R
  assume KP: "¬ (infinite KP ∨ KP = {})"
  and m: "m = arg_min_on snd KP"
  and R: "R = {p ∈ KP. fst m < fst p}"
  have "m ∈ KP" using KP arg_min_if_finite(1) m by blast
  thus  "(R, KP) ∈ measure card" using KP R by(auto intro!: psubset_card_mono)
qed

declare treap_of.simps [simp del]

lemma treap_of_unique:
  "⟦ treap t;  inj_on snd (set_tree t) ⟧
  ⟹ treap_of (set_tree t) = t"
proof(induction "set_tree t" arbitrary: t rule: treap_of.induct)
  case (1 t)
  show ?case
  proof (cases "infinite (set_tree t) ∨ set_tree t = {}")
    case True
    thus ?thesis by(simp add: treap_of.simps)
  next
    case False
    let ?m = "arg_min_on snd (set_tree t)"
    let ?L = "{p ∈ set_tree t. fst p < fst ?m}"
    let ?R = "{p ∈ set_tree t. fst p > fst ?m}"
    obtain l a r where t: "t = Node l a r"
      using False by (cases t) auto
    have "∀kp ∈ set_tree t. snd a ≤ snd kp"
      using "1.prems"(1)
      by(auto simp add: t treap_def ball_Un)
        (metis image_eqI snd_conv tree.set_map)+
    hence "a = ?m"
      by (metis "1.prems"(2) False arg_min_if_finite(1) arg_min_if_finite(2) inj_on_def 
          le_neq_trans t tree.set_intros(2))
    have "treap l" "treap r" using "1.prems"(1) by(auto simp: treap_def t)
    have l: "set_tree l = {p ∈ set_tree t. fst p < fst a}"
      using "1.prems"(1) by(auto simp add: treap_def t ball_Un tree.set_map)
    have r: "set_tree r = {p ∈ set_tree t. fst p > fst a}"
      using "1.prems"(1) by(auto simp add: treap_def t ball_Un tree.set_map)
    have "l = treap_of ?L"
      using "1.hyps"(1)[OF False ‹a = ?m› l r ‹treap l›]
        l ‹a = ?m› "1.prems"(2)
      by (fastforce simp add: inj_on_def)
    have "r = treap_of ?R"
      using "1.hyps"(2)[OF False ‹a = ?m› l r ‹treap r›]
        r ‹a = ?m› "1.prems"(2)
      by (fastforce simp add: inj_on_def)
    have "t = Node (treap_of ?L) ?m (treap_of ?R)"
      using ‹a = ?m› ‹l = treap_of ?L› ‹r = treap_of ?R› by(subst t) simp
    thus ?thesis using False
      by (subst treap_of.simps) simp
  qed
qed

lemma treap_unique:
  "⟦ treap t1; treap t2; set_tree t1 = set_tree t2; inj_on snd (set_tree t1) ⟧
  ⟹ t1 = t2"
  for t1 t2 :: "('k::linorder * 'p::linorder) tree"
by (metis treap_of_unique)

fun ins :: "'k::linorder ⇒ 'p::linorder ⇒ ('k × 'p) tree ⇒ ('k × 'p) tree" where
"ins k p Leaf = ⟨Leaf, (k,p), Leaf⟩" |
"ins k p ⟨l, (k1,p1), r⟩ =
  (if k < k1 then
     (case ins k p l of
       ⟨l2, (k2,p2), r2⟩ ⇒
         if p1 ≤ p2 then ⟨⟨l2, (k2,p2), r2⟩, (k1,p1), r⟩
         else ⟨l2, (k2,p2), ⟨r2, (k1,p1), r⟩⟩)
   else
   if k > k1 then
     (case ins k p r of
       ⟨l2, (k2,p2), r2⟩ ⇒
         if p1 ≤ p2 then ⟨l, (k1,p1), ⟨l2, (k2,p2), r2⟩⟩
         else ⟨⟨l, (k1,p1), l2⟩, (k2,p2), r2⟩)
   else ⟨l, (k1,p1), r⟩)"

lemma ins_neq_Leaf: "ins k p t ≠ ⟨⟩"
  by (induction t rule: ins.induct) (auto split: tree.split)

lemma keys_ins: "keys (ins k p t) = Set.insert k (keys t)"
proof (induction t rule: ins.induct)
  case 2
  then show ?case
    by (simp add: ins_neq_Leaf split: tree.split prod.split) (safe; fastforce)
qed (simp)

lemma prios_ins: "prios (ins k p t) ⊆ {p} ∪ prios t"
apply(induction t rule: ins.induct)
 apply simp
  apply (simp add: ins_neq_Leaf split: tree.split prod.split)
  by (safe; fastforce)

lemma prios_ins': "k ∉ keys t ⟹ prios (ins k p t) = {p} ∪ prios t"
apply(induction t rule: ins.induct)
 apply simp
  apply (simp add: ins_neq_Leaf split: tree.split prod.split)
  by (safe; fastforce)

lemma set_tree_ins: "set_tree (ins k p t) ⊆ {(k,p)} ∪ set_tree t"
  by (induction t rule: ins.induct) (auto simp add: ins_neq_Leaf split: tree.split prod.split)
    
lemma set_tree_ins': "k ∉ keys t ⟹  {(k,p)} ∪ set_tree t ⊆ set_tree (ins k p t)"
  by (induction t rule: ins.induct) (auto simp add: ins_neq_Leaf split: tree.split prod.split)

lemma set_tree_ins_eq: "k ∉ keys t ⟹ set_tree (ins k p t) = {(k,p)} ∪ set_tree t"
  using set_tree_ins set_tree_ins' by blast

lemma prios_ins_special:
  "⟦ ins k p t = Node l (k',p') r;  p' = p; p ∈ prios r ∪ prios l ⟧
  ⟹ p ∈ prios t"
  by (induction k p t arbitrary: l k' p' r rule: ins.induct)
     (fastforce simp add: ins_neq_Leaf split: tree.splits prod.splits if_splits)+

lemma treap_NodeI:
  "⟦ treap l; treap r;
     ∀k' ∈ keys l. k' < k; ∀k' ∈ keys r. k < k';
     ∀p' ∈ prios l. p ≤ p'; ∀p' ∈ prios r. p ≤ p' ⟧
  ⟹ treap (Node l (k,p) r)"
 by (auto simp: treap_def)

lemma treap_rotate1:
  assumes "treap l2" "treap r2" "treap r" "¬ p1 ≤ p2" "k < k1" and
  ins: "ins k p l = Node l2 (k2,p2) r2" and treap_ins: "treap (ins k p l)"
  and treap: "treap ⟨l, (k1, p1), r⟩"
  shows "treap (Node l2 (k2,p2) (Node r2 (k1,p1) r))"
proof(rule treap_NodeI[OF ‹treap l2› treap_NodeI[OF ‹treap r2› ‹treap r›]])
  from keys_ins[of k p l] have 1: "keys r2 ⊆ {k} ∪ keys l" by(auto simp: ins)
  from treap have 2: "∀k'∈keys l. k' < k1" by (simp add: treap_def)
  show "∀k'∈keys r2. k' < k1" using 1 2 ‹k < k1› by blast
next
  from treap have 2: "∀p'∈prios l. p1 ≤ p'" by (simp add: treap_def)
  show "∀p'∈prios r2. p1 ≤ p'"
  proof
    fix p' assume "p' ∈ prios r2"
    hence "p' = p ∨ p' ∈ prios l" using prios_ins[of k p l] ins by auto
    thus "p1 ≤ p'"
    proof
      assume [simp]: "p' = p"
      have "p2 = p ∨ p2 ∈ prios l" using prios_ins[of k p l] ins by simp
      thus "p1 ≤ p'"
      proof
        assume "p2 = p"
        thus "p1 ≤ p'"
          using prios_ins_special[OF ins] ‹p' ∈ prios r2› 2 by auto
      next
        assume "p2 ∈ prios l"
        thus "p1 ≤ p'" using 2 ‹¬ p1 ≤ p2› by blast
      qed
    next
      assume "p' ∈ prios l"
      thus "p1 ≤ p'" using 2 by blast
    qed
  qed
next
  have "k2 = k ∨ k2 ∈ keys l" using keys_ins[of k p l] ins by (auto)
  hence 1: "k2 < k1"
  proof
    assume "k2 = k" thus "k2 < k1" using ‹k < k1› by simp
  next
    assume "k2 ∈ keys l"
    thus "k2 < k1" using treap by (auto simp: treap_def)
  qed
  have 2: "∀k'∈keys r2. k2 < k'"
    using treap_ins by(simp add: ins treap_def)
  have 3: "∀k'∈keys r. k2 < k'"
    using 1 treap by(auto simp: treap_def)
  show "∀k'∈keys ⟨r2, (k1, p1), r⟩. k2 < k'" using 1 2 3 by auto
next
  show "∀p'∈prios ⟨r2, (k1, p1), r⟩. p2 ≤ p'"
    using ins treap_ins treap ‹¬ p1 ≤ p2› by (auto simp: treap_def ball_Un)
qed (use ins treap_ins treap in ‹auto simp: treap_def ball_Un›)


lemma treap_rotate2:
  assumes "treap l" "treap l2" "treap r2" "¬ p1 ≤ p2" "k1 < k" and
  ins: "ins k p r = Node l2 (k2,p2) r2" and treap_ins: "treap (ins k p r)"
  and treap: "treap ⟨l, (k1, p1), r⟩"
  shows "treap (Node (Node l (k1,p1) l2) (k2,p2) r2)"
proof(rule treap_NodeI[OF treap_NodeI[OF ‹treap l› ‹treap l2›] ‹treap r2›])
  from keys_ins[of k p r] have 1: "keys l2 ⊆ {k} ∪ keys r" by(auto simp: ins)
  from treap have 2: "∀k'∈keys r. k1 < k'" by (simp add: treap_def)
  show "∀k'∈keys l2. k1 < k'" using 1 2 ‹k1 < k› by blast
next
  from treap have 2: "∀p'∈prios r. p1 ≤ p'" by (simp add: treap_def)
  show "∀p'∈prios l2. p1 ≤ p'"
  proof
    fix p' assume "p' ∈ prios l2"
    hence "p' = p ∨ p' ∈ prios r" using prios_ins[of k p r] ins by auto
    thus "p1 ≤ p'"
    proof
      assume [simp]: "p' = p"
      have "p2 = p ∨ p2 ∈ prios r" using prios_ins[of k p r] ins by simp
      thus "p1 ≤ p'"
      proof
        assume "p2 = p"
        thus "p1 ≤ p'"
          using prios_ins_special[OF ins] ‹p' ∈ prios l2› 2 by auto
      next
        assume "p2 ∈ prios r"
        thus "p1 ≤ p'" using 2 ‹¬ p1 ≤ p2› by blast
      qed
    next
      assume "p' ∈ prios r"
      thus "p1 ≤ p'" using 2 by blast
    qed
  qed
next
  have "k2 = k ∨ k2 ∈ keys r" using keys_ins[of k p r] ins by (auto)
  hence 1: "k1 < k2"
  proof
    assume "k2 = k" thus "k1 < k2" using ‹k1 < k› by simp
  next
    assume "k2 ∈ keys r"
    thus "k1 < k2" using treap by (auto simp: treap_def)
  qed
  have 2: "∀k'∈keys l. k' < k2" using 1 treap by(auto simp: treap_def)
  have 3: "∀k'∈keys l2. k' < k2"
    using treap_ins by(auto simp: ins treap_def)
  show "∀k'∈keys ⟨l, (k1, p1), l2⟩. k' < k2" using 1 2 3 by auto
next
  show "∀p'∈prios ⟨l, (k1, p1), l2⟩. p2 ≤ p'"
    using ins treap_ins treap ‹¬ p1 ≤ p2› by (auto simp: treap_def ball_Un)
qed (use ins treap_ins treap in ‹auto simp: treap_def ball_Un›)

lemma treap_ins: "treap t ⟹ treap (ins k p t)"
proof(induction t rule: ins.induct)
  case 1 thus ?case by (simp add: treap_def)
next
  case (2 k p l k1 p1 r)
  have "treap l" "treap r"
    using "2.prems" by(auto simp: treap_def tree.set_map)
  show ?case
  proof cases
    assume "k < k1"
    obtain l2 k2 p2 r2 where ins: "ins k p l = Node l2 (k2,p2) r2"
      by (metis ins_neq_Leaf neq_Leaf_iff prod.collapse)
    note treap_ins = "2.IH"(1)[OF ‹k < k1› ‹treap l›]
    hence "treap l2" "treap r2" using ins by (auto simp add: treap_def)
    show ?thesis
    proof cases
      assume "p1 ≤ p2"
      have "treap (Node (Node l2 (k2,p2) r2) (k1,p1) r)"
        apply(rule treap_NodeI[OF treap_ins[unfolded ins] ‹treap r›])
        using ins treap_ins ‹k < k1› "2.prems" keys_ins[of k p l]
        by (auto simp add: treap_def ball_Un order_trans[OF ‹p1 ≤ p2›])
      thus ?thesis using ‹k < k1› ins ‹p1 ≤ p2› by simp
    next
      assume "¬ p1 ≤ p2"
      have "treap (Node l2 (k2,p2) (Node r2 (k1,p1) r))"
        by(rule treap_rotate1[OF ‹treap l2› ‹treap r2›  ‹treap r› ‹¬ p1 ≤ p2›
            ‹k < k1› ins treap_ins "2.prems"])
      thus ?thesis using ‹k < k1› ins ‹¬ p1 ≤ p2› by simp
    qed
  next
    assume "¬ k < k1"
    show ?thesis
    proof cases
    assume "k > k1"
    obtain l2 k2 p2 r2 where ins: "ins k p r = Node l2 (k2,p2) r2"
      by (metis ins_neq_Leaf neq_Leaf_iff prod.collapse)
    note treap_ins = "2.IH"(2)[OF ‹¬ k < k1› ‹k > k1› ‹treap r›]
    hence "treap l2" "treap r2" using ins by (auto simp add: treap_def)
    have fst: "∀k' ∈ set_tree (map_tree fst (ins k p r)).
                 k' = k ∨ k' ∈ set_tree (map_tree fst r)"
      by(simp add: keys_ins)
    show ?thesis
    proof cases
      assume "p1 ≤ p2"
      have "treap (Node l (k1,p1) (ins k p r))"
        apply(rule treap_NodeI[OF ‹treap l› treap_ins])
        using ins treap_ins ‹k > k1› "2.prems" keys_ins[of k p r]
        by (auto simp: treap_def ball_Un order_trans[OF ‹p1 ≤ p2›])
      thus ?thesis using ‹¬ k < k1› ‹k > k1› ins ‹p1 ≤ p2› by simp
    next
      assume "¬ p1 ≤ p2"
      have "treap (Node (Node l (k1,p1) l2) (k2,p2) r2)"
        by(rule treap_rotate2[OF ‹treap l› ‹treap l2› ‹treap r2› ‹¬ p1 ≤ p2›
             ‹k1 < k› ins treap_ins "2.prems"])
      thus ?thesis using ‹¬ k < k1›  ‹k > k1› ins ‹¬ p1 ≤ p2› by simp
    qed
    next
      assume "¬ k > k1"
      hence "k = k1" using ‹¬ k < k1› by auto
      thus ?thesis using "2.prems" by(simp)
    qed
  qed  
qed

lemma treap_of_set_tree_unique:
  "⟦ finite A; inj_on fst A; inj_on snd A ⟧
  ⟹ set_tree (treap_of A) = A"  
proof(induction "A" rule: treap_of.induct)
  case (1 A)
  note IH = 1
  show ?case
  proof (cases "infinite A ∨ A = {}")
    assume "infinite A ∨ A = {}"
    with IH show ?thesis by (simp add: treap_of.simps)
  next
    assume not_inf_or_empty: "¬ (infinite A ∨ A = {})"
    let ?m = "arg_min_on snd A"
    let ?L = "{p ∈ A. fst p < fst ?m}"
    let ?R = "{p ∈ A. fst p > fst ?m}"
    obtain l a r where t: "treap_of A = Node l a r"
      using not_inf_or_empty
      by (cases "treap_of A") (auto simp: Let_def elim!: treap_of.elims split: if_splits)
    have [simp]: "inj_on fst {p ∈ A. fst p < fst (arg_min_on snd A)}"
                 "inj_on snd {p ∈ A. fst p < fst (arg_min_on snd A)}"
                 "inj_on fst {p ∈ A. fst (arg_min_on snd A) < fst p}"
                 "inj_on snd {p ∈ A. fst (arg_min_on snd A) < fst p}"
      using IH by (auto intro: inj_on_subset)
    have lr: "l = treap_of ?L" "r = treap_of ?R"
      using t by (auto simp: Let_def elim: treap_of.elims split: if_splits)
    then have l: "set_tree l = ?L"
       using not_inf_or_empty IH by auto
     have "r = treap_of ?R"
       using t by (auto simp: Let_def elim: treap_of.elims split: if_splits)
    then have r: "set_tree r = ?R"
      using not_inf_or_empty IH(2) by (auto)
    have a: "a = ?m"
      using t by (elim treap_of.elims) (simp add: Let_def split: if_splits)
    have "a ≠ fst (arg_min_on snd A)" if "(a,b) ∈ A" "(a, b) ≠ arg_min_on snd A" for a b
      using IH(4,5) that not_inf_or_empty arg_min_if_finite(1) inj_on_eq_iff by fastforce
    then have "a < fst (arg_min_on snd A)" 
       if "(a,b) ∈ A" "(a, b) ≠ arg_min_on snd A" "fst (arg_min_on snd A) ≥ a" for a b
      using le_neq_trans that by auto
    moreover have "arg_min_on snd A ∈ A"
      using not_inf_or_empty arg_min_if_finite by auto
    ultimately have A: "A = {?m} ∪ ?L ∪ ?R"
      by auto
    show ?thesis using l r a A t by force
  qed
qed

lemma treap_of_subset: "set_tree (treap_of A) ⊆ A"
proof(induction "A" rule: treap_of.induct)
  case (1 A)
  note IH = 1
  show ?case
  proof (cases "infinite A ∨ A = {}")
    assume "infinite A ∨ A = {}"
    with IH show ?thesis by (simp add: treap_of.simps)
  next
    assume not_inf_or_empty: "¬ (infinite A ∨ A = {})"
    let ?m = "arg_min_on snd A"
    let ?L = "{p ∈ A. fst p < fst ?m}"
    let ?R = "{p ∈ A. fst p > fst ?m}"
    obtain l a r where t: "treap_of A = Node l a r"
      using not_inf_or_empty by (cases "treap_of A")
                                (auto simp add: Let_def  elim!: treap_of.elims split: if_splits)
    have "l = treap_of ?L" "r = treap_of ?R"
      using t by (auto simp: Let_def elim: treap_of.elims split: if_splits)
    have "set_tree l ⊆ ?L" "set_tree r ⊆ ?R"
    proof -
      have "set_tree (treap_of {p ∈ A. fst p < fst (arg_min_on snd A)})
            ⊆ {p ∈ A. fst p < fst (arg_min_on snd A)}"
        by (rule IH) (use not_inf_or_empty in auto)
      then show "set_tree l ⊆ ?L"
        using ‹l = treap_of ?L› by auto
    next
      have "set_tree (treap_of {p ∈ A. fst (arg_min_on snd A) < fst p})
            ⊆ {p ∈ A. fst (arg_min_on snd A) < fst p}"
        by (rule IH) (use not_inf_or_empty in auto)
      then show "set_tree r ⊆ ?R"
        using ‹r = treap_of ?R› by auto
    qed
    moreover have "a = ?m"
      using t by (auto elim!: treap_of.elims simp add: Let_def split: if_splits)
    moreover have "{?m} ∪ ?L ∪ ?R ⊆ A"
      using not_inf_or_empty arg_min_if_finite by auto
    ultimately show ?thesis by (auto simp add: t)
  qed
qed

lemma treap_treap_of:
  "treap (treap_of A)"
proof(induction "A" rule: treap_of.induct)
  case (1 A)
  show ?case
  proof (cases "infinite A ∨ A = {}")
    case True
    with 1 show ?thesis by (simp add: treap_of.simps treap_def)
  next
    case False
    let ?m = "arg_min_on snd A"
    let ?L = "{p ∈ A. fst p < fst ?m}"
    let ?R = "{p ∈ A. fst p > fst ?m}"
    obtain l a r where t: "treap_of A = Node l a r"
      using False by (cases "treap_of A") (auto simp: Let_def elim!: treap_of.elims split: if_splits)
    have l: "l = treap_of ?L"
      using t by (auto simp: Let_def elim: treap_of.elims split: if_splits)
    then have treap_l: "treap l"
      using False by (auto intro: 1) 
    from l have keys_l: "keys l ⊆ fst ` ?L"
      by (auto simp add: tree.set_map intro!: image_mono treap_of_subset)
    have r: "r = treap_of ?R"
      using t by (auto simp: Let_def elim: treap_of.elims split: if_splits)
    then have treap_r: "treap r"
      using False by (auto intro: 1) 
    from r have keys_r: "keys r ⊆ fst ` ?R"
      by (auto simp add: tree.set_map intro!: image_mono treap_of_subset)
    have prios: "prios l ⊆ snd ` A" "prios r ⊆ snd ` A"
      using l r treap_of_subset image_mono by (auto simp add: tree.set_map)
    have a: "a = ?m"
      using t by(auto simp: Let_def elim: treap_of.elims split: if_splits)
    have prios_l: "⋀x. x ∈ prios l ⟹ snd a ≤ x"
      by (drule rev_subsetD[OF _ prios(1)]) (use arg_min_least a False in fast)
    have prios_r: "⋀x. x ∈ prios r ⟹ snd a ≤ x"
      by (drule rev_subsetD[OF _ prios(2)]) (use arg_min_least a False in fast)
    show ?thesis
      using prios_r prios_l treap_l treap_r keys_l keys_r a 
      by (auto simp add: t treap_def dest: rev_subsetD[OF _ keys_l] rev_subsetD[OF _ keys_r])
    qed
qed

lemma treap_Leaf: "treap ⟨⟩"
  by (simp add: treap_def)

lemma foldl_ins_treap: "treap t ⟹ treap (foldl (λt' (x, p). ins x p t') t xs)"
  using treap_ins by (induction xs arbitrary: t) auto

lemma foldl_ins_set_tree: 
  assumes "inj_on fst (set ys)" "inj_on snd (set ys)" "distinct ys" "fst ` (set ys) ∩ keys t = {}"
  shows "set_tree (foldl (λt' (x, p). ins x p t') t ys) = set ys ∪ set_tree t"
  using assms
  by (induction ys arbitrary: t) (auto simp add: case_prod_beta' set_tree_ins_eq keys_ins)

lemma foldl_ins_treap_of:
  assumes "distinct ys" "inj_on fst (set ys)" "inj_on snd (set ys)"
 shows "(foldl (λt' (x, p). ins x p t') Leaf ys) = treap_of (set ys)"
  using assms by (intro treap_unique) (auto simp: treap_Leaf foldl_ins_treap foldl_ins_set_tree 
                                                  treap_treap_of treap_of_set_tree_unique)

end