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