Theory BST

(*
  File: BST.thy
  Author: Bohua Zhan
*)

section ‹Binary search tree›

theory BST
  imports Lists_Ex
begin

text ‹
  Verification of functional programs on binary search trees. For
  basic technique, see comments in Lists\_Ex.thy.
›

subsection ‹Definition and setup for trees›

datatype ('a, 'b) tree =
    Tip | Node (lsub: "('a, 'b) tree") (key: 'a) (nval: 'b) (rsub: "('a, 'b) tree")

setup ‹add_resolve_prfstep @{thm tree.distinct(1)}›
setup ‹fold add_rewrite_rule @{thms tree.sel}›
setup ‹add_forward_prfstep @{thm tree.collapse}›
setup ‹add_var_induct_rule @{thm tree.induct}›

subsection ‹Inorder traversal, and set of elements of a tree›

fun in_traverse :: "('a, 'b) tree ⇒ 'a list" where
  "in_traverse Tip = []"
| "in_traverse (Node l k v r) = in_traverse l @ k # in_traverse r"
setup ‹fold add_rewrite_rule @{thms in_traverse.simps}›

fun tree_set :: "('a, 'b) tree ⇒ 'a set" where
  "tree_set Tip = {}"
| "tree_set (Node l k v r) = {k} ∪ tree_set l ∪ tree_set r"
setup ‹fold add_rewrite_rule @{thms tree_set.simps}›

fun in_traverse_pairs :: "('a, 'b) tree ⇒ ('a × 'b) list" where
  "in_traverse_pairs Tip = []"
| "in_traverse_pairs (Node l k v r) = in_traverse_pairs l @ (k, v) # in_traverse_pairs r"
setup ‹fold add_rewrite_rule @{thms in_traverse_pairs.simps}›

lemma in_traverse_fst [rewrite]:
  "map fst (in_traverse_pairs t) = in_traverse t"
@proof @induct t @qed

definition tree_map :: "('a, 'b) tree ⇒ ('a, 'b) map" where
  "tree_map t = map_of_alist (in_traverse_pairs t)"
setup ‹add_rewrite_rule @{thm tree_map_def}›

subsection ‹Sortedness on trees›

fun tree_sorted :: "('a::linorder, 'b) tree ⇒ bool" where
  "tree_sorted Tip = True"
| "tree_sorted (Node l k v r) = ((∀x∈tree_set l. x < k) ∧ (∀x∈tree_set r. k < x)
                              ∧ tree_sorted l ∧ tree_sorted r)"
setup ‹fold add_rewrite_rule @{thms tree_sorted.simps}›

lemma tree_sorted_lr [forward]:
  "tree_sorted (Node l k v r) ⟹ tree_sorted l ∧ tree_sorted r" by auto2

lemma inorder_preserve_set [rewrite]:
  "tree_set t = set (in_traverse t)"
@proof @induct t @qed

lemma inorder_pairs_sorted [rewrite]:
  "tree_sorted t ⟷ strict_sorted (map fst (in_traverse_pairs t))"
@proof @induct t @qed

text ‹Use definition in terms of in\_traverse from now on.›
setup ‹fold del_prfstep_thm (@{thms tree_set.simps} @ @{thms tree_sorted.simps})›

subsection ‹Rotation on trees›

definition rotateL :: "('a, 'b) tree ⇒ ('a, 'b) tree" where [rewrite]:
  "rotateL t = (if t = Tip then t else if rsub t = Tip then t else
    (let rt = rsub t in
     Node (Node (lsub t) (key t) (nval t) (lsub rt)) (key rt) (nval rt) (rsub rt)))"

definition rotateR :: "('a, 'b) tree ⇒ ('a, 'b) tree" where [rewrite]:
  "rotateR t = (if t = Tip then t else if lsub t = Tip then t else
    (let lt = lsub t in
     Node (lsub lt) (key lt) (nval lt) (Node (rsub lt) (key t) (nval t) (rsub t))))"

lemma rotateL_in_trav [rewrite]: "in_traverse (rotateL t) = in_traverse t" by auto2
lemma rotateR_in_trav [rewrite]: "in_traverse (rotateR t) = in_traverse t" by auto2

lemma rotateL_sorted [forward]: "tree_sorted t ⟹ tree_sorted (rotateL t)" by auto2
lemma rotateR_sorted [forward]: "tree_sorted t ⟹ tree_sorted (rotateR t)" by auto2

subsection ‹Insertion on trees›

fun tree_insert :: "'a::ord ⇒ 'b ⇒ ('a, 'b) tree ⇒ ('a, 'b) tree" where
  "tree_insert x v Tip = Node Tip x v Tip"
| "tree_insert x v (Node l y w r) =
    (if x = y then Node l x v r
     else if x < y then Node (tree_insert x v l) y w r
     else Node l y w (tree_insert x v r))"
setup ‹fold add_rewrite_rule @{thms tree_insert.simps}›
 
lemma insert_in_traverse_pairs [rewrite]:
  "tree_sorted t ⟹ in_traverse_pairs (tree_insert x v t) = ordered_insert_pairs x v (in_traverse_pairs t)"
@proof @induct t @qed

text ‹Correctness results for insertion.›
theorem insert_sorted [forward]:
  "tree_sorted t ⟹ tree_sorted (tree_insert x v t)" by auto2

theorem insert_on_map:
  "tree_sorted t ⟹ tree_map (tree_insert x v t) = (tree_map t) {x → v}" by auto2

subsection ‹Deletion on trees›

fun del_min :: "('a, 'b) tree ⇒ ('a × 'b) × ('a, 'b) tree" where
  "del_min Tip = undefined"
| "del_min (Node lt x v rt) =
   (if lt = Tip then ((x, v), rt) else
    (fst (del_min lt), Node (snd (del_min lt)) x v rt))"
setup ‹add_rewrite_rule @{thm del_min.simps(2)}›

lemma delete_min_del_hd_pairs [rewrite]:
  "t ≠ Tip ⟹ fst (del_min t) # in_traverse_pairs (snd (del_min t)) = in_traverse_pairs t"
@proof @induct t @qed

fun delete_elt_tree :: "('a, 'b) tree ⇒ ('a, 'b) tree" where
  "delete_elt_tree Tip = undefined"
| "delete_elt_tree (Node lt x v rt) =
    (if lt = Tip then rt else if rt = Tip then lt else
     Node lt (fst (fst (del_min rt))) (snd (fst (del_min rt))) (snd (del_min rt)))"
setup ‹add_rewrite_rule @{thm delete_elt_tree.simps(2)}›

lemma delete_elt_in_traverse_pairs [rewrite]:
  "in_traverse_pairs (delete_elt_tree (Node lt x v rt)) = in_traverse_pairs lt @ in_traverse_pairs rt" by auto2

fun tree_delete :: "'a::ord ⇒ ('a, 'b) tree ⇒ ('a, 'b) tree" where
  "tree_delete x Tip = Tip"
| "tree_delete x (Node l y w r) =
    (if x = y then delete_elt_tree (Node l y w r)
     else if x < y then Node (tree_delete x l) y w r
     else Node l y w (tree_delete x r))"
setup ‹fold add_rewrite_rule @{thms tree_delete.simps}›

lemma tree_delete_in_traverse_pairs [rewrite]:
  "tree_sorted t ⟹ in_traverse_pairs (tree_delete x t) = remove_elt_pairs x (in_traverse_pairs t)"
@proof @induct t @qed

text ‹Correctness results for deletion.›
theorem tree_delete_sorted [forward]:
  "tree_sorted t ⟹ tree_sorted (tree_delete x t)" by auto2

theorem tree_delete_map [rewrite]:
  "tree_sorted t ⟹ tree_map (tree_delete x t) = delete_map x (tree_map t)" by auto2

subsection ‹Search on sorted trees›

fun tree_search :: "('a::ord, 'b) tree ⇒ 'a ⇒ 'b option" where
  "tree_search Tip x = None"
| "tree_search (Node l k v r) x =
  (if x = k then Some v
   else if x < k then tree_search l x
   else tree_search r x)"
setup ‹fold add_rewrite_rule @{thms tree_search.simps}›

text ‹Correctness of search.›
theorem tree_search_correct [rewrite]:
  "tree_sorted t ⟹ tree_search t x = (tree_map t)⟨x⟩"
@proof @induct t @qed

end