Theory BST_Impl

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

section ‹Implementation of binary search tree›

theory BST_Impl
  imports SepAuto "../Functional/BST"
begin

text ‹Imperative version of binary search trees.›

subsection ‹Tree nodes›

datatype ('a, 'b) node =
  Node (lsub: "('a, 'b) node ref option") (key: 'a) (val: 'b) (rsub: "('a, 'b) node ref option")
setup ‹fold add_rewrite_rule @{thms node.sel}›

fun node_encode :: "('a::heap, 'b::heap) node ⇒ nat" where
  "node_encode (Node l k v r) = to_nat (l, k, v, r)"

instance node :: (heap, heap) heap
  apply (rule heap_class.intro)
  apply (rule countable_classI [of "node_encode"])
  apply (case_tac x, simp_all, case_tac y, simp_all)
  ..

fun btree :: "('a::heap, 'b::heap) tree ⇒ ('a, 'b) node ref option ⇒ assn" where
  "btree Tip p = ↑(p = None)"
| "btree (tree.Node lt k v rt) (Some p) = (∃⇩Alp rp. p ↦⇩r Node lp k v rp * btree lt lp * btree rt rp)"
| "btree (tree.Node lt k v rt) None = false"
setup ‹fold add_rewrite_ent_rule @{thms btree.simps}›

lemma btree_Tip [forward_ent]: "btree Tip p ⟹⇩A ↑(p = None)" by auto2

lemma btree_Node [forward_ent]:
  "btree (tree.Node lt k v rt) p ⟹⇩A (∃⇩Alp rp. the p ↦⇩r Node lp k v rp * btree lt lp * btree rt rp * ↑(p ≠ None))"
@proof @case "p = None" @qed

lemma btree_none: "emp ⟹⇩A btree tree.Tip None" by auto2

lemma btree_constr_ent:
  "p ↦⇩r Node lp k v rp * btree lt lp * btree rt rp ⟹⇩A btree (tree.Node lt k v rt) (Some p)" by auto2

setup ‹fold add_entail_matcher [@{thm btree_none}, @{thm btree_constr_ent}]›
setup ‹fold del_prfstep_thm @{thms btree.simps}›

type_synonym ('a, 'b) btree = "('a, 'b) node ref option"

subsection ‹Operations›

subsubsection ‹Basic operations›

definition tree_empty :: "('a, 'b) btree Heap" where
  "tree_empty = return None"

lemma tree_empty_rule [hoare_triple]:
  "<emp> tree_empty <btree Tip>" by auto2

definition tree_is_empty :: "('a, 'b) btree ⇒ bool Heap" where
  "tree_is_empty b = return (b = None)"

lemma tree_is_empty_rule:
  "<btree t b> tree_is_empty b <λr. btree t b * ↑(r ⟷ t = Tip)>" by auto2

definition btree_constr ::
  "('a::heap, 'b::heap) btree ⇒ 'a ⇒ 'b ⇒ ('a, 'b) btree ⇒ ('a, 'b) btree Heap" where
  "btree_constr lp k v rp = do { p ← ref (Node lp k v rp); return (Some p) }"

lemma btree_constr_rule [hoare_triple]:
  "<btree lt lp * btree rt rp> btree_constr lp k v rp <btree (tree.Node lt k v rt)>" by auto2

subsubsection ‹Insertion›

partial_function (heap) btree_insert ::
  "'a::{heap,linorder} ⇒ 'b::heap ⇒ ('a, 'b) btree ⇒ ('a, 'b) btree Heap" where
  "btree_insert k v b = (case b of
     None ⇒ btree_constr None k v None
   | Some p ⇒ do {
      t ← !p;
      (if k = key t then do {
         p := Node (lsub t) k v (rsub t);
         return (Some p) }
       else if k < key t then do {
         q ← btree_insert k v (lsub t);
         p := Node q (key t) (val t) (rsub t);
         return (Some p) }
       else do {
         q ← btree_insert k v (rsub t);
         p := Node (lsub t) (key t) (val t) q;
         return (Some p)}) })"

lemma btree_insert_to_fun [hoare_triple]:
  "<btree t b>
   btree_insert k v b
   <btree (tree_insert k v t)>"
@proof @induct t arbitrary b @qed

subsubsection ‹Deletion›

partial_function (heap) btree_del_min :: "('a::heap, 'b::heap) btree ⇒ (('a × 'b) × ('a, 'b) btree) Heap" where
  "btree_del_min b = (case b of
     None ⇒ raise STR ''del_min: empty tree''
   | Some p ⇒ do {
      t ← !p;
      (if lsub t = None then
         return ((key t, val t), rsub t)
       else do {
         r ← btree_del_min (lsub t);
         p := Node (snd r) (key t) (val t) (rsub t);
         return (fst r, Some p) }) })"

lemma btree_del_min_to_fun [hoare_triple]:
  "<btree t b * ↑(b ≠ None)>
   btree_del_min b
   <λ(r,p). btree (snd (del_min t)) p * ↑(r = fst (del_min t))>⇩t"
@proof @induct t arbitrary b @qed

definition btree_del_elt :: "('a::heap, 'b::heap) btree ⇒ ('a, 'b) btree Heap" where
  "btree_del_elt b = (case b of
     None ⇒ raise STR ''del_elt: empty tree''
   | Some p ⇒ do {
       t ← !p;
       (if lsub t = None then return (rsub t)
        else if rsub t = None then return (lsub t)
        else do {
          r ← btree_del_min (rsub t);
          p := Node (lsub t) (fst (fst r)) (snd (fst r)) (snd r);
          return (Some p) }) })"

lemma btree_del_elt_to_fun [hoare_triple]:
  "<btree (tree.Node lt x v rt) b>
   btree_del_elt b
   <btree (delete_elt_tree (tree.Node lt x v rt))>⇩t" by auto2

partial_function (heap) btree_delete ::
  "'a::{heap,linorder} ⇒ ('a, 'b::heap) btree ⇒ ('a, 'b) btree Heap" where
  "btree_delete x b = (case b of
     None ⇒ return None
   | Some p ⇒ do {
      t ← !p;
      (if x = key t then do {
         r ← btree_del_elt b;
         return r }
       else if x < key t then do {
         q ← btree_delete x (lsub t);
         p := Node q (key t) (val t) (rsub t);
         return (Some p) }
       else do {
         q ← btree_delete x (rsub t);
         p := Node (lsub t) (key t) (val t) q;
         return (Some p)}) })"

lemma btree_delete_to_fun [hoare_triple]:
  "<btree t b>
   btree_delete x b
   <btree (tree_delete x t)>⇩t"
@proof @induct t arbitrary b @qed

subsubsection ‹Search›

partial_function (heap) btree_search ::
  "'a::{heap,linorder} ⇒ ('a, 'b::heap) btree ⇒ 'b option Heap" where
  "btree_search x b = (case b of
     None ⇒ return None
   | Some p ⇒ do {
      t ← !p;
      (if x = key t then return (Some (val t))
       else if x < key t then btree_search x (lsub t)
       else btree_search x (rsub t)) })"

lemma btree_search_correct [hoare_triple]:
  "<btree t b * ↑(tree_sorted t)>
   btree_search x b
   <λr. btree t b * ↑(r = tree_search t x)>"
@proof @induct t arbitrary b @qed

subsection ‹Outer interface›

text ‹Express Hoare triples for operations on binary search tree in terms of
  the mapping represented by the tree.›
definition btree_map :: "('a, 'b) map ⇒ ('a::{heap,linorder}, 'b::heap) node ref option ⇒ assn" where
  "btree_map M p = (∃⇩At. btree t p * ↑(tree_sorted t) * ↑(M = tree_map t))"
setup ‹add_rewrite_ent_rule @{thm btree_map_def}›

theorem btree_empty_rule_map [hoare_triple]:
  "<emp> tree_empty <btree_map empty_map>" by auto2

theorem btree_insert_rule_map [hoare_triple]:
  "<btree_map M b> btree_insert k v b <btree_map (M {k → v})>" by auto2

theorem btree_delete_rule_map [hoare_triple]:
  "<btree_map M b> btree_delete x b <btree_map (delete_map x M)>⇩t" by auto2

theorem btree_search_rule_map [hoare_triple]:
  "<btree_map M b> btree_search x b <λr. btree_map M b * ↑(r = M⟨x⟩)>" by auto2

end