Theory Splay_Tree_Analysis_Base

section "Splay Tree"

subsection "Basics"

theory Splay_Tree_Analysis_Base
imports
  Lemmas_log
  Splay_Tree.Splay_Tree
  "HOL-Data_Structures.Define_Time_Function"
begin

declare size1_size[simp]

abbreviation "φ t == log 2 (size1 t)"

fun Φ :: "'a tree ⇒ real" where
"Φ Leaf = 0" |
"Φ (Node l a r) = φ (Node l a r) + Φ l + Φ r"

time_fun cmp
time_fun splay equations splay.simps(1) splay_code

lemma T_splay_simps[simp]:
  "T_splay a (Node l a r) = 1"
  "x<b ⟹ T_splay x (Node Leaf b CD) = 1"
  "a<b ⟹ T_splay a (Node (Node A a B) b CD) = 1"
  "x<a ⟹ x<b ⟹ T_splay x (Node (Node A a B) b CD) =
   (if A = Leaf then 1 else T_splay x A + 1)"
  "x<b ⟹ a<x ⟹ T_splay x (Node (Node A a B) b CD) =
   (if B = Leaf then 1 else T_splay x B + 1)"
  "b<x ⟹ T_splay x (Node AB b Leaf) = 1"
  "b<a ⟹ T_splay a (Node AB b (Node C a D)) = 1"
  "b<x ⟹ x<c ⟹ T_splay x (Node AB b (Node C c D)) =
  (if C=Leaf then 1 else T_splay x C + 1)"
  "b<x ⟹ c<x ⟹ T_splay x (Node AB b (Node C c D)) =
  (if D=Leaf then 1 else T_splay x D + 1)"
by (auto simp add: tree.case_eq_if)

declare T_splay.simps(2)[simp del]

time_fun insert

lemma T_insert_simp: "T_insert x t = (if t = Leaf then 0 else T_splay x t)"
by(auto split: tree.split)

time_fun splay_max

time_fun delete

lemma ex_in_set_tree: "t ≠ Leaf ⟹ bst t ⟹
  ∃x' ∈ set_tree t. splay x' t = splay x t ∧ T_splay x' t = T_splay x t"
proof(induction x t rule: splay.induct)
  case (6 x b c A)
  hence "splay x A ≠ Leaf" by simp
  then obtain A1 u A2 where [simp]: "splay x A = Node A1 u A2"
    by (metis tree.exhaust)
  have "b < c" "bst A" using "6.prems" by auto
  from "6.IH"[OF ‹A ≠ Leaf› ‹bst A›]
  obtain x' where "x' ∈ set_tree A" "splay x' A = splay x A" "T_splay x' A = T_splay x A"
    by blast
  moreover hence "x'<b" using "6.prems"(2) by auto
  ultimately show ?case using ‹x<c› ‹x<b› ‹b<c› ‹bst A› by force
next
  case (8 a x c B)
  hence "splay x B ≠ Leaf" by simp
  then obtain B1 u B2 where [simp]: "splay x B = Node B1 u B2"
    by (metis tree.exhaust)
  have "a < c" "bst B" using "8.prems" by auto
  from "8.IH"[OF ‹B ≠ Leaf› ‹bst B›]
  obtain x' where "x' ∈ set_tree B" "splay x' B = splay x B" "T_splay x' B = T_splay x B"
    by blast
  moreover hence "a<x' & x'<c" using "8.prems"(2) by simp
  ultimately show ?case using ‹x<c› ‹a<x› ‹a<c› ‹bst B› by force
next
  case (11 b x c C)
  hence "splay x C ≠ Leaf" by simp
  then obtain C1 u C2 where [simp]: "splay x C = Node C1 u C2"
    by (metis tree.exhaust)
  have "b < c" "bst C" using "11.prems" by auto
  from "11.IH"[OF ‹C ≠ Leaf› ‹bst C›]
  obtain x' where "x' ∈ set_tree C" "splay x' C = splay x C" "T_splay x' C = T_splay x C"
    by blast
  moreover hence "b<x' & x'<c" using "11.prems" by simp
  ultimately show ?case using ‹b<x› ‹x<c› ‹b<c› ‹bst C› by force
next
  case (14 a x c D)
  hence "splay x D ≠ Leaf" by simp
  then obtain D1 u D2 where [simp]: "splay x D = Node D1 u D2"
    by (metis tree.exhaust)
  have "a < c" "bst D" using "14.prems" by auto
  from "14.IH"[OF ‹D ≠ Leaf› ‹bst D›]
  obtain x' where "x' ∈ set_tree D" "splay x' D = splay x D" "T_splay x' D = T_splay x D"
    by blast
  moreover hence "c<x'" using "14.prems"(2) by simp
  ultimately show ?case using ‹a<x› ‹c<x› ‹a<c› ‹bst D› by force
qed (auto simp: le_less)


datatype 'a op = Empty | Splay 'a | Insert 'a | Delete 'a

fun arity :: "'a::linorder op ⇒ nat" where
"arity Empty = 0" |
"arity (Splay x) = 1" |
"arity (Insert x) = 1" |
"arity (Delete x) = 1"

fun exec :: "'a::linorder op ⇒ 'a tree list ⇒ 'a tree" where
"exec Empty [] = Leaf" |
"exec (Splay x) [t] = splay x t" |
"exec (Insert x) [t] = Splay_Tree.insert x t" |
"exec (Delete x) [t] = Splay_Tree.delete x t"

fun cost :: "'a::linorder op ⇒ 'a tree list ⇒ nat" where
"cost Empty [] = 1" |
"cost (Splay x) [t] = T_splay x t" |
"cost (Insert x) [t] = T_insert x t" |
"cost (Delete x) [t] = T_delete x t"

end