Theory IntervalTree_Impl

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

section ‹Implementation of interval tree›

theory IntervalTree_Impl
  imports SepAuto "../Functional/Interval_Tree"
begin

text ‹Imperative version of interval tree.›

subsection ‹Interval and IdxInterval›

fun interval_encode :: "('a::heap) interval ⇒ nat" where
  "interval_encode (Interval l h) = to_nat (l, h)"

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

fun idx_interval_encode :: "('a::heap) idx_interval ⇒ nat" where
  "idx_interval_encode (IdxInterval it i) = to_nat (it, i)"

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

subsection ‹Tree nodes›

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

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

instance node :: (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 int_tree :: "interval_tree ⇒ nat node ref option ⇒ assn" where
  "int_tree Tip p = ↑(p = None)"
| "int_tree (interval_tree.Node lt v m rt) (Some p) = (∃⇩Alp rp. p ↦⇩r Node lp v m rp * int_tree lt lp * int_tree rt rp)"
| "int_tree (interval_tree.Node lt v m rt) None = false"
setup ‹fold add_rewrite_ent_rule @{thms int_tree.simps}›

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

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

lemma int_tree_none: "emp ⟹⇩A int_tree interval_tree.Tip None" by auto2

lemma int_tree_constr_ent:
  "p ↦⇩r Node lp v m rp * int_tree lt lp * int_tree rt rp ⟹⇩A int_tree (interval_tree.Node lt v m rt) (Some p)" by auto2

setup ‹fold add_entail_matcher [@{thm int_tree_none}, @{thm int_tree_constr_ent}]›
setup ‹fold del_prfstep_thm @{thms int_tree.simps}›

type_synonym int_tree = "nat node ref option"

subsection ‹Operations›

subsubsection ‹Basic operation›

definition int_tree_empty :: "int_tree Heap" where
  "int_tree_empty = return None"

lemma int_tree_empty_to_fun [hoare_triple]:
  "<emp> int_tree_empty <int_tree Tip>" by auto2

definition int_tree_is_empty :: "int_tree ⇒ bool Heap" where
  "int_tree_is_empty b = return (b = None)"

lemma int_tree_is_empty_rule [hoare_triple]:
  "<int_tree t b>
   int_tree_is_empty b
   <λr. int_tree t b * ↑(r ⟷ t = Tip)>" by auto2

definition get_tmax :: "int_tree ⇒ nat Heap" where
  "get_tmax b = (case b of
     None ⇒ return 0
   | Some p ⇒ do {
      t ← !p;
      return (tmax t) })"

lemma get_tmax_rule [hoare_triple]:
  "<int_tree t b> get_tmax b <λr. int_tree t b * ↑(r = interval_tree.tmax t)>"
@proof @case "t = Tip" @qed

definition compute_tmax :: "nat idx_interval ⇒ int_tree ⇒ int_tree ⇒ nat Heap" where
  "compute_tmax it l r = do {
    lm ← get_tmax l;
    rm ← get_tmax r;
    return (max3 it lm rm)
  }"

lemma compute_tmax_rule [hoare_triple]:
  "<int_tree t1 b1 * int_tree t2 b2>
   compute_tmax it b1 b2
   <λr. int_tree t1 b1 * int_tree t2 b2 * ↑(r = max3 it (interval_tree.tmax t1) (interval_tree.tmax t2))>"
  by auto2

definition int_tree_constr :: "int_tree ⇒ nat idx_interval ⇒ int_tree ⇒ int_tree Heap" where
  "int_tree_constr lp v rp = do {
    m ← compute_tmax v lp rp;
    p ← ref (Node lp v m rp);
    return (Some p) }"

lemma int_tree_constr_rule [hoare_triple]:
  "<int_tree lt lp * int_tree rt rp>
   int_tree_constr lp v rp
   <int_tree (interval_tree.Node lt v (max3 v (interval_tree.tmax lt) (interval_tree.tmax rt)) rt)>"
  by auto2

subsubsection ‹Insertion›
  
partial_function (heap) insert_impl :: "nat idx_interval ⇒ int_tree ⇒ int_tree Heap" where
  "insert_impl v b = (case b of
    None ⇒ int_tree_constr None v None
  | Some p ⇒ do {
    t ← !p;
    (if v = val t then do {
       return (Some p) }
     else if v < val t then do {
       q ← insert_impl v (lsub t);
       m ← compute_tmax (val t) q (rsub t);
       p := Node q (val t) m (rsub t);
       return (Some p) }
     else do {
       q ← insert_impl v (rsub t);
       m ← compute_tmax (val t) (lsub t) q;
       p := Node (lsub t) (val t) m q;
       return (Some p) })})"

lemma int_tree_insert_to_fun [hoare_triple]:
  "<int_tree t b>
    insert_impl v b
   <int_tree (insert v t)>"
@proof @induct t arbitrary b @qed

subsubsection ‹Deletion›

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

lemma int_tree_del_min_to_fun [hoare_triple]:
  "<int_tree t b * ↑(b ≠ None)>
   int_tree_del_min b
   <λr. int_tree (snd (del_min t)) (snd r) * ↑(fst(r) = fst (del_min t))>⇩t"
@proof @induct t arbitrary b @qed

definition int_tree_del_elt :: "int_tree ⇒ int_tree Heap" where
  "int_tree_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 ← int_tree_del_min (rsub t);
          m ← compute_tmax (fst r) (lsub t) (snd r);
          p := Node (lsub t) (fst r) m (snd r);
          return (Some p) }) })"

lemma int_tree_del_elt_to_fun [hoare_triple]:
  "<int_tree (interval_tree.Node lt v m rt) b>
   int_tree_del_elt b
   <int_tree (delete_elt_tree (interval_tree.Node lt v m rt))>⇩t" by auto2

partial_function (heap) delete_impl :: "nat idx_interval ⇒ int_tree ⇒ int_tree Heap" where
  "delete_impl x b = (case b of
     None ⇒ return None
   | Some p ⇒ do {
      t ← !p;
      (if x = val t then do {
         r ← int_tree_del_elt b;
         return r }
       else if x < val t then do {
         q ← delete_impl x (lsub t);
         m ← compute_tmax (val t) q (rsub t);
         p := Node q (val t) m (rsub t);
         return (Some p) }
       else do {
         q ← delete_impl x (rsub t);
         m ← compute_tmax (val t) (lsub t) q;
         p := Node (lsub t) (val t) m q;
         return (Some p) })})"

lemma int_tree_delete_to_fun [hoare_triple]:
  "<int_tree t b>
    delete_impl x b
   <int_tree (delete x t)>⇩t"
@proof @induct t arbitrary b @qed

subsubsection ‹Search›

partial_function (heap) search_impl :: "nat interval ⇒ int_tree ⇒ bool Heap" where
  "search_impl x b = (case b of
     None ⇒ return False
   | Some p ⇒ do {
      t ← !p;
      (if is_overlap (int (val t)) x then return True
       else case lsub t of
           None ⇒ do { b ← search_impl x (rsub t); return b }
         | Some lp ⇒ do {
            lt ← !lp;
            if tmax lt ≥ low x then
              do { b ← search_impl x (lsub t); return b }
            else
              do { b ← search_impl x (rsub t); return b }})})"

lemma search_impl_correct [hoare_triple]:
  "<int_tree t b>
    search_impl x b
   <λr. int_tree t b * ↑(r ⟷ search t x)>"
@proof @induct t arbitrary b @with
  @subgoal "t = interval_tree.Node l v m r"
    @case "is_overlap (int v) x"
    @case "l ≠ Tip ∧ interval_tree.tmax l ≥ low x"
  @endgoal @end
@qed

subsection ‹Outer interface›

text ‹Express Hoare triples for operations on interval tree in terms of
  the set of intervals represented by the tree.›
definition int_tree_set :: "nat idx_interval set ⇒ int_tree ⇒ assn" where
  "int_tree_set S p = (∃⇩At. int_tree t p * ↑(is_interval_tree t) * ↑(S = tree_set t))"
setup ‹add_rewrite_ent_rule @{thm int_tree_set_def}›

theorem int_tree_empty_rule [hoare_triple]:
  "<emp> int_tree_empty <int_tree_set {}>" by auto2

theorem int_tree_insert_rule [hoare_triple]:
  "<int_tree_set S b * ↑(is_interval (int x))>
   insert_impl x b
   <int_tree_set (S ∪ {x})>" by auto2

theorem int_tree_delete_rule [hoare_triple]:
  "<int_tree_set S b * ↑(is_interval (int x))>
   delete_impl x b
   <int_tree_set (S - {x})>⇩t" by auto2

theorem int_tree_search_rule [hoare_triple]:
  "<int_tree_set S b * ↑(is_interval x)>
   search_impl x b
   <λr. int_tree_set S b * ↑(r ⟷ has_overlap S x)>" by auto2

setup ‹del_prfstep_thm @{thm int_tree_set_def}›

end