Theory Brother12_Map

(* Author: Tobias Nipkow *)

section ‹1-2 Brother Tree Implementation of Maps›

theory Brother12_Map
imports
  Brother12_Set
  Map_Specs
begin

fun lookup :: "('a × 'b) bro ⇒ 'a::linorder ⇒ 'b option" where
"lookup N0 x = None" |
"lookup (N1 t) x = lookup t x" |
"lookup (N2 l (a,b) r) x =
  (case cmp x a of
     LT ⇒ lookup l x |
     EQ ⇒ Some b |
     GT ⇒ lookup r x)"

locale update = insert
begin

fun upd :: "'a::linorder ⇒ 'b ⇒ ('a×'b) bro ⇒ ('a×'b) bro" where
"upd x y N0 = L2 (x,y)" |
"upd x y (N1 t) = n1 (upd x y t)" |
"upd x y (N2 l (a,b) r) =
  (case cmp x a of
     LT ⇒ n2 (upd x y l) (a,b) r |
     EQ ⇒ N2 l (a,y) r |
     GT ⇒ n2 l (a,b) (upd x y r))"

definition update :: "'a::linorder ⇒ 'b ⇒ ('a×'b) bro ⇒ ('a×'b) bro" where
"update x y t = tree(upd x y t)"

end

context delete
begin

fun del :: "'a::linorder ⇒ ('a×'b) bro ⇒ ('a×'b) bro" where
"del _ N0         = N0" |
"del x (N1 t)     = N1 (del x t)" |
"del x (N2 l (a,b) r) =
  (case cmp x a of
     LT ⇒ n2 (del x l) (a,b) r |
     GT ⇒ n2 l (a,b) (del x r) |
     EQ ⇒ (case split_min r of
              None ⇒ N1 l |
              Some (ab, r') ⇒ n2 l ab r'))"

definition delete :: "'a::linorder ⇒ ('a×'b) bro ⇒ ('a×'b) bro" where
"delete a t = tree (del a t)"

end

subsection "Functional Correctness Proofs"

subsubsection "Proofs for lookup"

lemma lookup_map_of: "t ∈ T h ⟹
  sorted1(inorder t) ⟹ lookup t x = map_of (inorder t) x"
by(induction h arbitrary: t) (auto simp: map_of_simps split: option.splits)

subsubsection "Proofs for update"

context update
begin

lemma inorder_upd: "t ∈ T h ⟹
  sorted1(inorder t) ⟹ inorder(upd x y t) = upd_list x y (inorder t)"
by(induction h arbitrary: t) (auto simp: upd_list_simps inorder_n1 inorder_n2)

lemma inorder_update: "t ∈ T h ⟹
  sorted1(inorder t) ⟹ inorder(update x y t) = upd_list x y (inorder t)"
by(simp add: update_def inorder_upd inorder_tree)

end

subsubsection ‹Proofs for deletion›

context delete
begin

lemma inorder_del:
  "t ∈ T h ⟹ sorted1(inorder t) ⟹ inorder(del x t) = del_list x (inorder t)"
  apply (induction h arbitrary: t)
  apply (auto simp: del_list_simps inorder_n2)
  apply (auto simp: del_list_simps inorder_n2
     inorder_split_min[OF UnI1] inorder_split_min[OF UnI2] split: option.splits)
  done

lemma inorder_delete:
  "t ∈ T h ⟹ sorted1(inorder t) ⟹ inorder(delete x t) = del_list x (inorder t)"
by(simp add: delete_def inorder_del inorder_tree)

end


subsection ‹Invariant Proofs›

subsubsection ‹Proofs for update›

context update
begin

lemma upd_type:
  "(t ∈ B h ⟶ upd x y t ∈ Bp h) ∧ (t ∈ U h ⟶ upd x y t ∈ T h)"
apply(induction h arbitrary: t)
 apply (simp)
apply (fastforce simp: Bp_if_B n2_type dest: n1_type)
done

lemma update_type:
  "t ∈ B h ⟹ update x y t ∈ B h ∪ B (Suc h)"
unfolding update_def by (metis upd_type tree_type)

end

subsubsection "Proofs for deletion"

context delete
begin

lemma del_type:
  "t ∈ B h ⟹ del x t ∈ T h"
  "t ∈ U h ⟹ del x t ∈ Um h"
proof (induction h arbitrary: x t)
  case (Suc h)
  { case 1
    then obtain l a b r where [simp]: "t = N2 l (a,b) r" and
      lr: "l ∈ T h" "r ∈ T h" "l ∈ B h ∨ r ∈ B h" by auto
    have ?case if "x < a"
    proof cases
      assume "l ∈ B h"
      from n2_type3[OF Suc.IH(1)[OF this] lr(2)]
      show ?thesis using ‹x<a› by(simp)
    next
      assume "l ∉ B h"
      hence "l ∈ U h" "r ∈ B h" using lr by auto
      from n2_type1[OF Suc.IH(2)[OF this(1)] this(2)]
      show ?thesis using ‹x<a› by(simp)
    qed
    moreover
    have ?case if "x > a"
    proof cases
      assume "r ∈ B h"
      from n2_type3[OF lr(1) Suc.IH(1)[OF this]]
      show ?thesis using ‹x>a› by(simp)
    next
      assume "r ∉ B h"
      hence "l ∈ B h" "r ∈ U h" using lr by auto
      from n2_type2[OF this(1) Suc.IH(2)[OF this(2)]]
      show ?thesis using ‹x>a› by(simp)
    qed
    moreover
    have ?case if [simp]: "x=a"
    proof (cases "split_min r")
      case None
      show ?thesis
      proof cases
        assume "r ∈ B h"
        with split_minNoneN0[OF this None] lr show ?thesis by(simp)
      next
        assume "r ∉ B h"
        hence "r ∈ U h" using lr by auto
        with split_minNoneN1[OF this None] lr(3) show ?thesis by (simp)
      qed
    next
      case [simp]: (Some br')
      obtain b r' where [simp]: "br' = (b,r')" by fastforce
      show ?thesis
      proof cases
        assume "r ∈ B h"
        from split_min_type(1)[OF this] n2_type3[OF lr(1)]
        show ?thesis by simp
      next
        assume "r ∉ B h"
        hence "l ∈ B h" and "r ∈ U h" using lr by auto
        from split_min_type(2)[OF this(2)] n2_type2[OF this(1)]
        show ?thesis by simp
      qed
    qed
    ultimately show ?case by auto                         
  }
  { case 2 with Suc.IH(1) show ?case by auto }
qed auto

lemma delete_type:
  "t ∈ B h ⟹ delete x t ∈ B h ∪ B(h-1)"
unfolding delete_def
by (cases h) (simp, metis del_type(1) tree_type Suc_eq_plus1 diff_Suc_1)

end

subsection "Overall correctness"

interpretation Map_by_Ordered
where empty = empty and lookup = lookup and update = update.update
and delete = delete.delete and inorder = inorder and inv = "λt. ∃h. t ∈ B h"
proof (standard, goal_cases)
  case 2 thus ?case by(auto intro!: lookup_map_of)
next
  case 3 thus ?case by(auto intro!: update.inorder_update)
next
  case 4 thus ?case by(auto intro!: delete.inorder_delete)
next
  case 6 thus ?case using update.update_type by (metis Un_iff)
next
  case 7 thus ?case using delete.delete_type by blast
qed (auto simp: empty_def)

end