Theory Root_Balanced_Tree.Root_Balanced_Tree
section "Root Balanced Tree"
theory Root_Balanced_Tree
imports
Amortized_Complexity.Amortized_Framework0
"HOL-Library.Tree_Multiset"
"HOL-Data_Structures.Tree_Set"
"HOL-Data_Structures.Balance"
Time_Monad
begin
declare Let_def[simp]
subsection ‹Time Prelude›
text‹Redefinition of some auxiliary functions, but now with ‹tm› monad:›
subsubsection ‹@{const size_tree}›
fun size_tree_tm :: "'a tree ⇒ nat tm" where
"size_tree_tm ⟨⟩ =1 return 0" |
"size_tree_tm ⟨l, x, r⟩ =1
do { m ← size_tree_tm l;
n ← size_tree_tm r;
return (m+n+1)}"
definition size_tree :: "'a tree ⇒ nat" where
"size_tree t = val(size_tree_tm t)"
lemma size_tree_Leaf[simp,code]: "size_tree ⟨⟩ = 0"
using val_cong[OF size_tree_tm.simps(1)]
by(simp only: size_tree_def val_simps)
lemma size_tree_Node[simp,code]:
"size_tree ⟨l, x, r⟩ =
(let m = size_tree l;
n = size_tree r
in m+n+1)"
using val_cong[OF size_tree_tm.simps(2)]
by(simp only: size_tree_def val_simps)
lemma size_tree: "size_tree t = size t"
by(induction t rule: size_tree_tm.induct)(auto)
definition T_size_tree :: "'a tree ⇒ nat" where
"T_size_tree t = time(size_tree_tm t)"
lemma T_size_tree_Leaf: "T_size_tree ⟨⟩ = 1"
by(simp add: T_size_tree_def tm_simps)
lemma T_size_tree_Node:
"T_size_tree ⟨l, x, r⟩ = T_size_tree l + T_size_tree r + 1"
by(simp add: T_size_tree_def size_tree_def tm_simps split: tm.split)
lemma T_size_tree: "T_size_tree t = 2 * size t + 1"
by(induction t)(auto simp: T_size_tree_Leaf T_size_tree_Node)
subsubsection ‹@{const inorder}›
fun inorder2_tm :: "'a tree ⇒ 'a list ⇒ 'a list tm" where
"inorder2_tm ⟨⟩ xs =1 return xs" |
"inorder2_tm ⟨l, x, r⟩ xs =1
do { rs ← inorder2_tm r xs; inorder2_tm l (x#rs) }"
definition inorder2 :: "'a tree ⇒ 'a list ⇒ 'a list" where
"inorder2 t xs = val(inorder2_tm t xs)"
lemma inorder2_Leaf[simp,code]: "inorder2 ⟨⟩ xs = xs"
using val_cong[OF inorder2_tm.simps(1)]
by(simp only: inorder2_def val_simps)
lemma inorder2_Node[simp,code]:
"inorder2 ⟨l, x, r⟩ xs = (let rs = inorder2 r xs in inorder2 l (x # rs))"
using val_cong[OF inorder2_tm.simps(2), of l]
by(simp only: inorder2_def val_simps)
lemma inorder2: "inorder2 t xs = Tree.inorder2 t xs"
by(induction t xs rule: inorder2_tm.induct)(auto simp:inorder2_def)
definition T_inorder2 :: "'a tree ⇒ 'a list ⇒ nat" where
"T_inorder2 t xs = time(inorder2_tm t xs)"
lemma T_inorder2_Leaf: "T_inorder2 ⟨⟩ xs = 1"
by(simp add: T_inorder2_def tm_simps)
lemma T_inorder2_Node:
"T_inorder2 ⟨l, x, r⟩ xs = T_inorder2 r xs + T_inorder2 l (x # inorder2 r xs) + 1"
by(simp add: T_inorder2_def inorder2_def tm_simps split: tm.split)
lemma T_inorder2: "T_inorder2 t xs = 2*size t + 1"
by(induction t arbitrary: xs)(auto simp: T_inorder2_Leaf T_inorder2_Node)
subsubsection ‹@{const split_min}›
fun split_min_tm :: "'a tree ⇒ ('a * 'a tree) tm" where
"split_min_tm Leaf =1 return undefined" |
"split_min_tm (Node l x r) =1
(if l = Leaf then return (x,r)
else do { (y,l') ← split_min_tm l; return (y, Node l' x r)})"
definition split_min :: "'a tree ⇒ ('a * 'a tree)" where
"split_min t = val (split_min_tm t)"
lemma split_min_Node[simp,code]:
"split_min (Node l x r) =
(if l = Leaf then (x,r)
else let (y,l') = split_min l in (y, Node l' x r))"
using val_cong[OF split_min_tm.simps(2)]
by(simp only: split_min_def val_simps)
definition T_split_min :: "'a tree ⇒ nat" where
"T_split_min t = time (split_min_tm t)"
lemma T_split_min_Node[simp]:
"T_split_min (Node l x r) = (if l = Leaf then 1 else T_split_min l + 1)"
using val_cong[OF split_min_tm.simps(2)]
by(simp add: T_split_min_def tm_simps split: tm.split)
lemma split_minD:
"split_min t = (x,t') ⟹ t ≠ Leaf ⟹ x # inorder t' = inorder t"
by(induction t arbitrary: t' rule: split_min.induct)
(auto simp: sorted_lems split: prod.splits if_splits)
subsubsection ‹Balancing›
fun bal_tm :: "nat ⇒ 'a list ⇒ ('a tree * 'a list) tm" where
"bal_tm n xs =1
(if n=0 then return (Leaf,xs) else
(let m = n div 2
in do { (l, ys) ← bal_tm m xs;
(r, zs) ← bal_tm (n-1-m) (tl ys);
return (Node l (hd ys) r, zs)}))"
declare bal_tm.simps[simp del]
lemma bal_tm_simps:
"bal_tm 0 xs =1 return(Leaf, xs)"
"n > 0 ⟹
bal_tm n xs =1
(let m = n div 2
in do { (l, ys) ← bal_tm m xs;
(r, zs) ← bal_tm (n-1-m) (tl ys);
return (Node l (hd ys) r, zs)})"
by(simp_all add: bal_tm.simps)
definition bal :: "nat ⇒ 'a list ⇒ ('a tree * 'a list)" where
"bal n xs = val (bal_tm n xs)"
lemma bal_def2[code]:
"bal n xs =
(if n=0 then (Leaf,xs) else
(let m = n div 2;
(l, ys) = bal m xs;
(r, zs) = bal (n-1-m) (tl ys)
in (Node l (hd ys) r, zs)))"
using val_cong[OF bal_tm.simps(1)]
by(simp only: bal_def val_simps)
lemma bal_simps:
"bal 0 xs = (Leaf, xs)"
"n > 0 ⟹
bal n xs =
(let m = n div 2;
(l, ys) = bal m xs;
(r, zs) = bal (n-1-m) (tl ys)
in (Node l (hd ys) r, zs))"
by(simp_all add: bal_def2)
lemma bal_eq: "bal n xs = Balance.bal n xs"
apply(induction n xs rule: bal.induct)
apply(case_tac "n=0")
apply(simp add: bal_simps Balance.bal_simps)
apply(simp add: bal_simps Balance.bal_simps split: prod.split)
done
definition T_bal :: "nat ⇒ 'a list ⇒ nat" where
"T_bal n xs = time (bal_tm n xs)"
lemma T_bal: "T_bal n xs = 2*n+1"
unfolding T_bal_def
apply(induction n xs rule: bal_tm.induct)
apply(case_tac "n=0")
apply(simp add: bal_tm_simps)
apply(auto simp add: bal_tm_simps tm_simps simp del: subst_all split: tm.split)
done
definition bal_list_tm :: "nat ⇒ 'a list ⇒ 'a tree tm" where
"bal_list_tm n xs = do { (t,_) ← bal_tm n xs; return t }"
definition bal_list :: "nat ⇒ 'a list ⇒ 'a tree" where
"bal_list n xs = val (bal_list_tm n xs)"
lemma bal_list_def2[code]: "bal_list n xs = (let (t,ys) = bal n xs in t)"
using val_cong[OF bal_list_tm_def]
by(simp only: bal_list_def bal_def val_simps)
lemma bal_list: "bal_list n xs = Balance.bal_list n xs"
by(auto simp add: bal_list_def2 Balance.bal_list_def bal_eq split: prod.split)
definition bal_tree_tm :: "nat ⇒ 'a tree ⇒ 'a tree tm" where
"bal_tree_tm n t =1 do { xs ← inorder2_tm t []; bal_list_tm n xs }"
definition bal_tree :: "nat ⇒ 'a tree ⇒ 'a tree" where
"bal_tree n t = val (bal_tree_tm n t)"
lemma bal_tree_def2[code]:
"bal_tree n t = (let xs = inorder2 t [] in bal_list n xs)"
using val_cong[OF bal_tree_tm_def, of n t]
by(simp only: bal_tree_def bal_list_def inorder2_def val_simps)
lemma bal_tree: "bal_tree n t = Balance.bal_tree n t"
by(simp add: bal_tree_def2 Balance.bal_tree_def bal_list inorder2 inorder2_inorder)
definition T_bal_tree :: "nat ⇒ 'a tree ⇒ nat" where
"T_bal_tree n xs = time (bal_tree_tm n xs)"
lemma T_bal_tree: "n = size xs ⟹ T_bal_tree n xs = 4*n+3"
by(simp add: T_bal_tree_def bal_tree_tm_def tm_simps bal_list_tm_def
surj_TM[OF inorder2_def T_inorder2_def] T_inorder2
surj_TM[OF bal_def T_bal_def] T_bal size1_size
split: tm.split prod.split)
subsection "Naive implementation (insert only)"
fun node :: "bool ⇒ 'a tree ⇒ 'a ⇒ 'a tree ⇒ 'a tree" where
"node twist s x t = (if twist then Node t x s else Node s x t)"