Theory Tree23_Set

(* Author: Tobias Nipkow *)

section ‹2-3 Tree Implementation of Sets›

theory Tree23_Set
imports
  Tree23
  Cmp
  Set_Specs
begin

declare sorted_wrt.simps(2)[simp del]

definition empty :: "'a tree23" where
"empty = Leaf"

fun isin :: "'a::linorder tree23 ⇒ 'a ⇒ bool" where
"isin Leaf x = False" |
"isin (Node2 l a r) x =
  (case cmp x a of
     LT ⇒ isin l x |
     EQ ⇒ True |
     GT ⇒ isin r x)" |
"isin (Node3 l a m b r) x =
  (case cmp x a of
     LT ⇒ isin l x |
     EQ ⇒ True |
     GT ⇒
       (case cmp x b of
          LT ⇒ isin m x |
          EQ ⇒ True |
          GT ⇒ isin r x))"

datatype 'a up⇩i = Eq⇩i "'a tree23" | Of "'a tree23" 'a "'a tree23"

fun tree⇩i :: "'a up⇩i ⇒ 'a tree23" where
"tree⇩i (Eq⇩i t) = t" |
"tree⇩i (Of l a r) = Node2 l a r"

fun ins :: "'a::linorder ⇒ 'a tree23 ⇒ 'a up⇩i" where
"ins x Leaf = Of Leaf x Leaf" |
"ins x (Node2 l a r) =
   (case cmp x a of
      LT ⇒
        (case ins x l of
           Eq⇩i l' => Eq⇩i (Node2 l' a r) |
           Of l1 b l2 => Eq⇩i (Node3 l1 b l2 a r)) |
      EQ ⇒ Eq⇩i (Node2 l a r) |
      GT ⇒
        (case ins x r of
           Eq⇩i r' => Eq⇩i (Node2 l a r') |
           Of r1 b r2 => Eq⇩i (Node3 l a r1 b r2)))" |
"ins x (Node3 l a m b r) =
   (case cmp x a of
      LT ⇒
        (case ins x l of
           Eq⇩i l' => Eq⇩i (Node3 l' a m b r) |
           Of l1 c l2 => Of (Node2 l1 c l2) a (Node2 m b r)) |
      EQ ⇒ Eq⇩i (Node3 l a m b r) |
      GT ⇒
        (case cmp x b of
           GT ⇒
             (case ins x r of
                Eq⇩i r' => Eq⇩i (Node3 l a m b r') |
                Of r1 c r2 => Of (Node2 l a m) b (Node2 r1 c r2)) |
           EQ ⇒ Eq⇩i (Node3 l a m b r) |
           LT ⇒
             (case ins x m of
                Eq⇩i m' => Eq⇩i (Node3 l a m' b r) |
                Of m1 c m2 => Of (Node2 l a m1) c (Node2 m2 b r))))"

hide_const insert

definition insert :: "'a::linorder ⇒ 'a tree23 ⇒ 'a tree23" where
"insert x t = tree⇩i(ins x t)"

datatype 'a up⇩d = Eq⇩d "'a tree23" | Uf "'a tree23"

fun tree⇩d :: "'a up⇩d ⇒ 'a tree23" where
"tree⇩d (Eq⇩d t) = t" |
"tree⇩d (Uf t) = t"

(* Variation: return None to signal no-change *)

fun node21 :: "'a up⇩d ⇒ 'a ⇒ 'a tree23 ⇒ 'a up⇩d" where
"node21 (Eq⇩d t1) a t2 = Eq⇩d(Node2 t1 a t2)" |
"node21 (Uf t1) a (Node2 t2 b t3) = Uf(Node3 t1 a t2 b t3)" |
"node21 (Uf t1) a (Node3 t2 b t3 c t4) = Eq⇩d(Node2 (Node2 t1 a t2) b (Node2 t3 c t4))"

fun node22 :: "'a tree23 ⇒ 'a ⇒ 'a up⇩d ⇒ 'a up⇩d" where
"node22 t1 a (Eq⇩d t2) = Eq⇩d(Node2 t1 a t2)" |
"node22 (Node2 t1 b t2) a (Uf t3) = Uf(Node3 t1 b t2 a t3)" |
"node22 (Node3 t1 b t2 c t3) a (Uf t4) = Eq⇩d(Node2 (Node2 t1 b t2) c (Node2 t3 a t4))"

fun node31 :: "'a up⇩d ⇒ 'a ⇒ 'a tree23 ⇒ 'a ⇒ 'a tree23 ⇒ 'a up⇩d" where
"node31 (Eq⇩d t1) a t2 b t3 = Eq⇩d(Node3 t1 a t2 b t3)" |
"node31 (Uf t1) a (Node2 t2 b t3) c t4 = Eq⇩d(Node2 (Node3 t1 a t2 b t3) c t4)" |
"node31 (Uf t1) a (Node3 t2 b t3 c t4) d t5 = Eq⇩d(Node3 (Node2 t1 a t2) b (Node2 t3 c t4) d t5)"

fun node32 :: "'a tree23 ⇒ 'a ⇒ 'a up⇩d ⇒ 'a ⇒ 'a tree23 ⇒ 'a up⇩d" where
"node32 t1 a (Eq⇩d t2) b t3 = Eq⇩d(Node3 t1 a t2 b t3)" |
"node32 t1 a (Uf t2) b (Node2 t3 c t4) = Eq⇩d(Node2 t1 a (Node3 t2 b t3 c t4))" |
"node32 t1 a (Uf t2) b (Node3 t3 c t4 d t5) = Eq⇩d(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))"

fun node33 :: "'a tree23 ⇒ 'a ⇒ 'a tree23 ⇒ 'a ⇒ 'a up⇩d ⇒ 'a up⇩d" where
"node33 t1 a t2 b (Eq⇩d t3) = Eq⇩d(Node3 t1 a t2 b t3)" |
"node33 t1 a (Node2 t2 b t3) c (Uf t4) = Eq⇩d(Node2 t1 a (Node3 t2 b t3 c t4))" |
"node33 t1 a (Node3 t2 b t3 c t4) d (Uf t5) = Eq⇩d(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))"

fun split_min :: "'a tree23 ⇒ 'a * 'a up⇩d" where
"split_min (Node2 Leaf a Leaf) = (a, Uf Leaf)" |
"split_min (Node3 Leaf a Leaf b Leaf) = (a, Eq⇩d(Node2 Leaf b Leaf))" |
"split_min (Node2 l a r) = (let (x,l') = split_min l in (x, node21 l' a r))" |
"split_min (Node3 l a m b r) = (let (x,l') = split_min l in (x, node31 l' a m b r))"

text ‹In the base cases of ‹split_min› and ‹del› it is enough to check if one subtree is a ‹Leaf›,
in which case completeness implies that so are the others. Exercise.›

fun del :: "'a::linorder ⇒ 'a tree23 ⇒ 'a up⇩d" where
"del x Leaf = Eq⇩d Leaf" |
"del x (Node2 Leaf a Leaf) =
  (if x = a then Uf Leaf else Eq⇩d(Node2 Leaf a Leaf))" |
"del x (Node3 Leaf a Leaf b Leaf) =
  Eq⇩d(if x = a then Node2 Leaf b Leaf else
     if x = b then Node2 Leaf a Leaf
     else Node3 Leaf a Leaf b Leaf)" |
"del x (Node2 l a r) =
  (case cmp x a of
     LT ⇒ node21 (del x l) a r |
     GT ⇒ node22 l a (del x r) |
     EQ ⇒ let (a',r') = split_min r in node22 l a' r')" |
"del x (Node3 l a m b r) =
  (case cmp x a of
     LT ⇒ node31 (del x l) a m b r |
     EQ ⇒ let (a',m') = split_min m in node32 l a' m' b r |
     GT ⇒
       (case cmp x b of
          LT ⇒ node32 l a (del x m) b r |
          EQ ⇒ let (b',r') = split_min r in node33 l a m b' r' |
          GT ⇒ node33 l a m b (del x r)))"

definition delete :: "'a::linorder ⇒ 'a tree23 ⇒ 'a tree23" where
"delete x t = tree⇩d(del x t)"


subsection "Functional Correctness"

subsubsection "Proofs for isin"

lemma isin_set: "sorted(inorder t) ⟹ isin t x = (x ∈ set (inorder t))"
by (induction t) (auto simp: isin_simps)


subsubsection "Proofs for insert"

lemma inorder_ins:
  "sorted(inorder t) ⟹ inorder(tree⇩i(ins x t)) = ins_list x (inorder t)"
by(induction t) (auto simp: ins_list_simps split: up⇩i.splits)

lemma inorder_insert:
  "sorted(inorder t) ⟹ inorder(insert a t) = ins_list a (inorder t)"
by(simp add: insert_def inorder_ins)


subsubsection "Proofs for delete"

lemma inorder_node21: "height r > 0 ⟹
  inorder (tree⇩d (node21 l' a r)) = inorder (tree⇩d l') @ a # inorder r"
by(induct l' a r rule: node21.induct) auto

lemma inorder_node22: "height l > 0 ⟹
  inorder (tree⇩d (node22 l a r')) = inorder l @ a # inorder (tree⇩d r')"
by(induct l a r' rule: node22.induct) auto

lemma inorder_node31: "height m > 0 ⟹
  inorder (tree⇩d (node31 l' a m b r)) = inorder (tree⇩d l') @ a # inorder m @ b # inorder r"
by(induct l' a m b r rule: node31.induct) auto

lemma inorder_node32: "height r > 0 ⟹
  inorder (tree⇩d (node32 l a m' b r)) = inorder l @ a # inorder (tree⇩d m') @ b # inorder r"
by(induct l a m' b r rule: node32.induct) auto

lemma inorder_node33: "height m > 0 ⟹
  inorder (tree⇩d (node33 l a m b r')) = inorder l @ a # inorder m @ b # inorder (tree⇩d r')"
by(induct l a m b r' rule: node33.induct) auto

lemmas inorder_nodes = inorder_node21 inorder_node22
  inorder_node31 inorder_node32 inorder_node33

lemma split_minD:
  "split_min t = (x,t') ⟹ complete t ⟹ height t > 0 ⟹
  x # inorder(tree⇩d t') = inorder t"
by(induction t arbitrary: t' rule: split_min.induct)
  (auto simp: inorder_nodes split: prod.splits)

lemma inorder_del: "⟦ complete t ; sorted(inorder t) ⟧ ⟹
  inorder(tree⇩d (del x t)) = del_list x (inorder t)"
by(induction t rule: del.induct)
  (auto simp: del_list_simps inorder_nodes split_minD split!: if_split prod.splits)

lemma inorder_delete: "⟦ complete t ; sorted(inorder t) ⟧ ⟹
  inorder(delete x t) = del_list x (inorder t)"
by(simp add: delete_def inorder_del)


subsection ‹Completeness›


subsubsection "Proofs for insert"

text‹First a standard proof that \<^const>‹ins› preserves \<^const>‹complete›.›

fun h⇩i :: "'a up⇩i ⇒ nat" where
"h⇩i (Eq⇩i t) = height t" |
"h⇩i (Of l a r) = height l"

lemma complete_ins: "complete t ⟹ complete (tree⇩i(ins a t)) ∧ h⇩i(ins a t) = height t"
by (induct t) (auto split!: if_split up⇩i.split) (* 15 secs in 2015 *)

text‹Now an alternative proof (by Brian Huffman) that runs faster because
two properties (completeness and height) are combined in one predicate.›

inductive full :: "nat ⇒ 'a tree23 ⇒ bool" where
"full 0 Leaf" |
"⟦full n l; full n r⟧ ⟹ full (Suc n) (Node2 l p r)" |
"⟦full n l; full n m; full n r⟧ ⟹ full (Suc n) (Node3 l p m q r)"

inductive_cases full_elims:
  "full n Leaf"
  "full n (Node2 l p r)"
  "full n (Node3 l p m q r)"

inductive_cases full_0_elim: "full 0 t"
inductive_cases full_Suc_elim: "full (Suc n) t"

lemma full_0_iff [simp]: "full 0 t ⟷ t = Leaf"
  by (auto elim: full_0_elim intro: full.intros)

lemma full_Leaf_iff [simp]: "full n Leaf ⟷ n = 0"
  by (auto elim: full_elims intro: full.intros)

lemma full_Suc_Node2_iff [simp]:
  "full (Suc n) (Node2 l p r) ⟷ full n l ∧ full n r"
  by (auto elim: full_elims intro: full.intros)

lemma full_Suc_Node3_iff [simp]:
  "full (Suc n) (Node3 l p m q r) ⟷ full n l ∧ full n m ∧ full n r"
  by (auto elim: full_elims intro: full.intros)

lemma full_imp_height: "full n t ⟹ height t = n"
  by (induct set: full, simp_all)

lemma full_imp_complete: "full n t ⟹ complete t"
  by (induct set: full, auto dest: full_imp_height)

lemma complete_imp_full: "complete t ⟹ full (height t) t"
  by (induct t, simp_all)

lemma complete_iff_full: "complete t ⟷ (∃n. full n t)"
  by (auto elim!: complete_imp_full full_imp_complete)

text ‹The \<^const>‹insert› function either preserves the height of the
tree, or increases it by one. The constructor returned by the \<^term>‹insert› function determines which: A return value of the form \<^term>‹Eq⇩i t› indicates that the height will be the same. A value of the
form \<^term>‹Of l p r› indicates an increase in height.›

fun full⇩i :: "nat ⇒ 'a up⇩i ⇒ bool" where
"full⇩i n (Eq⇩i t) ⟷ full n t" |
"full⇩i n (Of l p r) ⟷ full n l ∧ full n r"

lemma full⇩i_ins: "full n t ⟹ full⇩i n (ins a t)"
by (induct rule: full.induct) (auto split: up⇩i.split)

text ‹The \<^const>‹insert› operation preserves completeance.›

lemma complete_insert: "complete t ⟹ complete (insert a t)"
unfolding complete_iff_full insert_def
apply (erule exE)
apply (drule full⇩i_ins [of _ _ a])
apply (cases "ins a t")
apply (auto intro: full.intros)
done


subsection "Proofs for delete"

fun h⇩d :: "'a up⇩d ⇒ nat" where
"h⇩d (Eq⇩d t) = height t" |
"h⇩d (Uf t) = height t + 1"

lemma complete_tree⇩d_node21:
  "⟦complete r; complete (tree⇩d l'); height r = h⇩d l' ⟧ ⟹ complete (tree⇩d (node21 l' a r))"
by(induct l' a r rule: node21.induct) auto

lemma complete_tree⇩d_node22:
  "⟦complete(tree⇩d r'); complete l; h⇩d r' = height l ⟧ ⟹ complete (tree⇩d (node22 l a r'))"
by(induct l a r' rule: node22.induct) auto

lemma complete_tree⇩d_node31:
  "⟦ complete (tree⇩d l'); complete m; complete r; h⇩d l' = height r; height m = height r ⟧
  ⟹ complete (tree⇩d (node31 l' a m b r))"
by(induct l' a m b r rule: node31.induct) auto

lemma complete_tree⇩d_node32:
  "⟦ complete l; complete (tree⇩d m'); complete r; height l = height r; h⇩d m' = height r ⟧
  ⟹ complete (tree⇩d (node32 l a m' b r))"
by(induct l a m' b r rule: node32.induct) auto

lemma complete_tree⇩d_node33:
  "⟦ complete l; complete m; complete(tree⇩d r'); height l = h⇩d r'; height m = h⇩d r' ⟧
  ⟹ complete (tree⇩d (node33 l a m b r'))"
by(induct l a m b r' rule: node33.induct) auto

lemmas completes = complete_tree⇩d_node21 complete_tree⇩d_node22
  complete_tree⇩d_node31 complete_tree⇩d_node32 complete_tree⇩d_node33

lemma height'_node21:
   "height r > 0 ⟹ h⇩d(node21 l' a r) = max (h⇩d l') (height r) + 1"
by(induct l' a r rule: node21.induct)(simp_all)

lemma height'_node22:
   "height l > 0 ⟹ h⇩d(node22 l a r') = max (height l) (h⇩d r') + 1"
by(induct l a r' rule: node22.induct)(simp_all)

lemma height'_node31:
  "height m > 0 ⟹ h⇩d(node31 l a m b r) =
   max (h⇩d l) (max (height m) (height r)) + 1"
by(induct l a m b r rule: node31.induct)(simp_all add: max_def)

lemma height'_node32:
  "height r > 0 ⟹ h⇩d(node32 l a m b r) =
   max (height l) (max (h⇩d m) (height r)) + 1"
by(induct l a m b r rule: node32.induct)(simp_all add: max_def)

lemma height'_node33:
  "height m > 0 ⟹ h⇩d(node33 l a m b r) =
   max (height l) (max (height m) (h⇩d r)) + 1"
by(induct l a m b r rule: node33.induct)(simp_all add: max_def)

lemmas heights = height'_node21 height'_node22
  height'_node31 height'_node32 height'_node33

lemma height_split_min:
  "split_min t = (x, t') ⟹ height t > 0 ⟹ complete t ⟹ h⇩d t' = height t"
by(induct t arbitrary: x t' rule: split_min.induct)
  (auto simp: heights split: prod.splits)

lemma height_del: "complete t ⟹ h⇩d(del x t) = height t"
by(induction x t rule: del.induct)
  (auto simp: heights max_def height_split_min split: prod.splits)

lemma complete_split_min:
  "⟦ split_min t = (x, t'); complete t; height t > 0 ⟧ ⟹ complete (tree⇩d t')"
by(induct t arbitrary: x t' rule: split_min.induct)
  (auto simp: heights height_split_min completes split: prod.splits)

lemma complete_tree⇩d_del: "complete t ⟹ complete(tree⇩d(del x t))"
by(induction x t rule: del.induct)
  (auto simp: completes complete_split_min height_del height_split_min split: prod.splits)

corollary complete_delete: "complete t ⟹ complete(delete x t)"
by(simp add: delete_def complete_tree⇩d_del)


subsection ‹Overall Correctness›

interpretation S: Set_by_Ordered
where empty = empty and isin = isin and insert = insert and delete = delete
and inorder = inorder and inv = complete
proof (standard, goal_cases)
  case 2 thus ?case by(simp add: isin_set)
next
  case 3 thus ?case by(simp add: inorder_insert)
next
  case 4 thus ?case by(simp add: inorder_delete)
next
  case 6 thus ?case by(simp add: complete_insert)
next
  case 7 thus ?case by(simp add: complete_delete)
qed (simp add: empty_def)+

end