added 2-3 trees (simpler and more complete than the version in ex/Tree23)
authornipkow
Sun Oct 18 17:25:13 2015 +0200 (2015-10-18)
changeset 61469cd82b1023932
parent 61468 7d1127ac2251
child 61478 6e789d198bbd
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
src/HOL/Data_Structures/RBT.thy
src/HOL/Data_Structures/Tree23.thy
src/HOL/Data_Structures/Tree23_Map.thy
src/HOL/Data_Structures/Tree23_Set.thy
src/HOL/ROOT
     1.1 --- a/src/HOL/Data_Structures/RBT.thy	Sat Oct 17 16:08:30 2015 +0200
     1.2 +++ b/src/HOL/Data_Structures/RBT.thy	Sun Oct 18 17:25:13 2015 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  (* Author: Tobias Nipkow *)
     1.5  
     1.6 -section \<open>Red-Black Tree\<close>
     1.7 +section \<open>Red-Black Trees\<close>
     1.8  
     1.9  theory RBT
    1.10  imports Tree2
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Data_Structures/Tree23.thy	Sun Oct 18 17:25:13 2015 +0200
     2.3 @@ -0,0 +1,43 @@
     2.4 +(* Author: Tobias Nipkow *)
     2.5 +
     2.6 +section \<open>2-3 Trees\<close>
     2.7 +
     2.8 +theory Tree23
     2.9 +imports Main
    2.10 +begin
    2.11 +
    2.12 +class height =
    2.13 +fixes height :: "'a \<Rightarrow> nat"
    2.14 +
    2.15 +datatype 'a tree23 =
    2.16 +  Leaf |
    2.17 +  Node2 "'a tree23" 'a "'a tree23" |
    2.18 +  Node3 "'a tree23" 'a "'a tree23" 'a "'a tree23"
    2.19 +
    2.20 +fun inorder :: "'a tree23 \<Rightarrow> 'a list" where
    2.21 +"inorder Leaf = []" |
    2.22 +"inorder(Node2 l a r) = inorder l @ a # inorder r" |
    2.23 +"inorder(Node3 l a m b r) = inorder l @ a # inorder m @ b # inorder r"
    2.24 +
    2.25 +
    2.26 +instantiation tree23 :: (type)height
    2.27 +begin
    2.28 +
    2.29 +fun height_tree23 :: "'a tree23 \<Rightarrow> nat" where
    2.30 +"height Leaf = 0" |
    2.31 +"height (Node2 l _ r) = Suc(max (height l) (height r))" |
    2.32 +"height (Node3 l _ m _ r) = Suc(max (height l) (max (height m) (height r)))"
    2.33 +
    2.34 +instance ..
    2.35 +
    2.36 +end
    2.37 +
    2.38 +text \<open>Balanced:\<close>
    2.39 +
    2.40 +fun bal :: "'a tree23 \<Rightarrow> bool" where
    2.41 +"bal Leaf = True" |
    2.42 +"bal (Node2 l _ r) = (bal l & bal r & height l = height r)" |
    2.43 +"bal (Node3 l _ m _ r) =
    2.44 +  (bal l & bal m & bal r & height l = height m & height m = height r)"
    2.45 +
    2.46 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Data_Structures/Tree23_Map.thy	Sun Oct 18 17:25:13 2015 +0200
     3.3 @@ -0,0 +1,155 @@
     3.4 +(* Author: Tobias Nipkow *)
     3.5 +
     3.6 +section \<open>2-3 Tree Implementation of Maps\<close>
     3.7 +
     3.8 +theory Tree23_Map
     3.9 +imports
    3.10 +  Tree23_Set
    3.11 +  Map_by_Ordered
    3.12 +begin
    3.13 +
    3.14 +fun lookup :: "('a::linorder * 'b) tree23 \<Rightarrow> 'a \<Rightarrow> 'b option" where
    3.15 +"lookup Leaf x = None" |
    3.16 +"lookup (Node2 l (a,b) r) x =
    3.17 +  (if x < a then lookup l x else
    3.18 +  if a < x then lookup r x else Some b)" |
    3.19 +"lookup (Node3 l (a1,b1) m (a2,b2) r) x =
    3.20 +  (if x < a1 then lookup l x else
    3.21 +   if x = a1 then Some b1 else
    3.22 +   if x < a2 then lookup m x else
    3.23 +   if x = a2 then Some b2
    3.24 +   else lookup r x)"
    3.25 +
    3.26 +fun upd :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) up\<^sub>i" where
    3.27 +"upd a b Leaf = Up\<^sub>i Leaf (a,b) Leaf" |
    3.28 +"upd a b (Node2 l xy r) =
    3.29 +   (if a < fst xy then
    3.30 +        (case upd a b l of
    3.31 +           T\<^sub>i l' => T\<^sub>i (Node2 l' xy r)
    3.32 +         | Up\<^sub>i l1 q l2 => T\<^sub>i (Node3 l1 q l2 xy r))
    3.33 +    else if a = fst xy then T\<^sub>i (Node2 l (a,b) r)
    3.34 +    else
    3.35 +        (case upd a b r of
    3.36 +           T\<^sub>i r' => T\<^sub>i (Node2 l xy r')
    3.37 +         | Up\<^sub>i r1 q r2 => T\<^sub>i (Node3 l xy r1 q r2)))" |
    3.38 +"upd a b (Node3 l xy1 m xy2 r) =
    3.39 +   (if a < fst xy1 then
    3.40 +        (case upd a b l of
    3.41 +           T\<^sub>i l' => T\<^sub>i (Node3 l' xy1 m xy2 r)
    3.42 +         | Up\<^sub>i l1 q l2 => Up\<^sub>i (Node2 l1 q l2) xy1 (Node2 m xy2 r))
    3.43 +    else if a = fst xy1 then T\<^sub>i (Node3 l (a,b) m xy2 r)
    3.44 +    else if a < fst xy2 then
    3.45 +             (case upd a b m of
    3.46 +                T\<^sub>i m' => T\<^sub>i (Node3 l xy1 m' xy2 r)
    3.47 +              | Up\<^sub>i m1 q m2 => Up\<^sub>i (Node2 l xy1 m1) q (Node2 m2 xy2 r))
    3.48 +         else if a = fst xy2 then T\<^sub>i (Node3 l xy1 m (a,b) r)
    3.49 +         else
    3.50 +             (case upd a b r of
    3.51 +                T\<^sub>i r' => T\<^sub>i (Node3 l xy1 m xy2 r')
    3.52 +              | Up\<^sub>i r1 q r2 => Up\<^sub>i (Node2 l xy1 m) xy2 (Node2 r1 q r2)))"
    3.53 +
    3.54 +definition update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) tree23" where
    3.55 +"update a b t = tree\<^sub>i(upd a b t)"
    3.56 +
    3.57 +fun del :: "'a::linorder \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) up\<^sub>d"
    3.58 +where
    3.59 +"del k Leaf = T\<^sub>d Leaf" |
    3.60 +"del k (Node2 Leaf p Leaf) = (if k=fst p then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf p Leaf))" |
    3.61 +"del k (Node3 Leaf p Leaf q Leaf) = T\<^sub>d(if k=fst p then Node2 Leaf q Leaf
    3.62 +  else if k=fst q then Node2 Leaf p Leaf else Node3 Leaf p Leaf q Leaf)" |
    3.63 +"del k (Node2 l a r) = (if k<fst a then node21 (del k l) a r else
    3.64 +  if k > fst a then node22 l a (del k r) else
    3.65 +  let (a',t) = del_min r in node22 l a' t)" |
    3.66 +"del k (Node3 l a m b r) = (if k<fst a then node31 (del k l) a m b r else
    3.67 +  if k = fst a then let (a',m') = del_min m in node32 l a' m' b r else
    3.68 +  if k < fst b then node32 l a (del k m) b r else
    3.69 +  if k = fst b then let (b',r') = del_min r in node33 l a m b' r'
    3.70 +  else node33 l a m b (del k r))"
    3.71 +
    3.72 +definition delete :: "'a::linorder \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) tree23" where
    3.73 +"delete k t = tree\<^sub>d(del k t)"
    3.74 +
    3.75 +
    3.76 +subsection "Proofs for Lookup"
    3.77 +
    3.78 +lemma lookup: "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
    3.79 +by (induction t) (auto simp: map_of_simps split: option.split)
    3.80 +
    3.81 +
    3.82 +subsection "Proofs for Update"
    3.83 +
    3.84 +text {* Balanced trees *}
    3.85 +
    3.86 +text{* First a standard proof that @{const upd} preserves @{const bal}. *}
    3.87 +
    3.88 +lemma bal_upd: "bal t \<Longrightarrow> bal (tree\<^sub>i(upd a b t)) \<and> height(upd a b t) = height t"
    3.89 +by (induct t) (auto split: up\<^sub>i.split)
    3.90 +
    3.91 +text{* Now an alternative proof (by Brian Huffman) that runs faster because
    3.92 +two properties (balance and height) are combined in one predicate. *}
    3.93 +
    3.94 +lemma full\<^sub>i_ins: "full n t \<Longrightarrow> full\<^sub>i n (upd a b t)"
    3.95 +by (induct rule: full.induct, auto split: up\<^sub>i.split)
    3.96 +
    3.97 +text {* The @{const update} operation preserves balance. *}
    3.98 +
    3.99 +lemma bal_update: "bal t \<Longrightarrow> bal (update a b t)"
   3.100 +unfolding bal_iff_full update_def
   3.101 +apply (erule exE)
   3.102 +apply (drule full\<^sub>i_ins [of _ _ a b])
   3.103 +apply (cases "upd a b t")
   3.104 +apply (auto intro: full.intros)
   3.105 +done
   3.106 +
   3.107 +text {* Functional correctness of @{const "update"}. *}
   3.108 +
   3.109 +lemma inorder_upd:
   3.110 +  "sorted1(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(upd a b t)) = upd_list a b (inorder t)"
   3.111 +by(induction t) (auto simp: upd_list_simps split: up\<^sub>i.splits)
   3.112 +
   3.113 +lemma inorder_update:
   3.114 +  "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)"
   3.115 +by(simp add: update_def inorder_upd)
   3.116 +
   3.117 +
   3.118 +subsection "Proofs for Deletion"
   3.119 +
   3.120 +lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
   3.121 +by(induction x t rule: del.induct)
   3.122 +  (auto simp add: heights max_def height_del_min split: prod.split)
   3.123 +
   3.124 +lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
   3.125 +by(induction x t rule: del.induct)
   3.126 +  (auto simp: bals bal_del_min height_del height_del_min split: prod.split)
   3.127 +
   3.128 +corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
   3.129 +by(simp add: delete_def bal_tree\<^sub>d_del)
   3.130 +
   3.131 +lemma inorder_del: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
   3.132 +  inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
   3.133 +by(induction t rule: del.induct)
   3.134 +  (auto simp: del_list_simps inorder_nodes del_minD split: prod.splits)
   3.135 +
   3.136 +lemma inorder_delete: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
   3.137 +  inorder(delete x t) = del_list x (inorder t)"
   3.138 +by(simp add: delete_def inorder_del)
   3.139 +
   3.140 +
   3.141 +subsection \<open>Overall Correctness\<close>
   3.142 +
   3.143 +interpretation T23_Map: Map_by_Ordered
   3.144 +where empty = Leaf and lookup = lookup and update = update and delete = delete
   3.145 +and inorder = inorder and wf = bal
   3.146 +proof (standard, goal_cases)
   3.147 +  case 2 thus ?case by(simp add: lookup)
   3.148 +next
   3.149 +  case 3 thus ?case by(simp add: inorder_update)
   3.150 +next
   3.151 +  case 4 thus ?case by(simp add: inorder_delete)
   3.152 +next
   3.153 +  case 6 thus ?case by(simp add: bal_update)
   3.154 +next
   3.155 +  case 7 thus ?case by(simp add: bal_delete)
   3.156 +qed simp+
   3.157 +
   3.158 +end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Data_Structures/Tree23_Set.thy	Sun Oct 18 17:25:13 2015 +0200
     4.3 @@ -0,0 +1,370 @@
     4.4 +(* Author: Tobias Nipkow *)
     4.5 +
     4.6 +section \<open>2-3 Tree Implementation of Sets\<close>
     4.7 +
     4.8 +theory Tree23_Set
     4.9 +imports
    4.10 +  Tree23
    4.11 +  Set_by_Ordered
    4.12 +begin
    4.13 +
    4.14 +fun isin :: "'a::linorder tree23 \<Rightarrow> 'a \<Rightarrow> bool" where
    4.15 +"isin Leaf x = False" |
    4.16 +"isin (Node2 l a r) x = (x < a \<and> isin l x \<or> x=a \<or> isin r x)" |
    4.17 +"isin (Node3 l a m b r) x =
    4.18 +  (x < a \<and> isin l x \<or> x = a \<or> (x < b \<and> isin m x \<or> x = b \<or> isin r x))"
    4.19 +
    4.20 +datatype 'a up\<^sub>i = T\<^sub>i "'a tree23" | Up\<^sub>i "'a tree23" 'a "'a tree23"
    4.21 +
    4.22 +fun tree\<^sub>i :: "'a up\<^sub>i \<Rightarrow> 'a tree23" where
    4.23 +"tree\<^sub>i (T\<^sub>i t) = t" |
    4.24 +"tree\<^sub>i (Up\<^sub>i l p r) = Node2 l p r"
    4.25 +
    4.26 +fun ins :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>i" where
    4.27 +"ins a Leaf = Up\<^sub>i Leaf a Leaf" |
    4.28 +"ins a (Node2 l x r) =
    4.29 +   (if a < x then
    4.30 +      case ins a l of
    4.31 +         T\<^sub>i l' => T\<^sub>i (Node2 l' x r)
    4.32 +       | Up\<^sub>i l1 q l2 => T\<^sub>i (Node3 l1 q l2 x r)
    4.33 +    else if a=x then T\<^sub>i (Node2 l x r)
    4.34 +    else
    4.35 +      case ins a r of
    4.36 +        T\<^sub>i r' => T\<^sub>i (Node2 l x r')
    4.37 +      | Up\<^sub>i r1 q r2 => T\<^sub>i (Node3 l x r1 q r2))" |
    4.38 +"ins a (Node3 l x1 m x2 r) =
    4.39 +   (if a < x1 then
    4.40 +      case ins a l of
    4.41 +        T\<^sub>i l' => T\<^sub>i (Node3 l' x1 m x2 r)
    4.42 +      | Up\<^sub>i l1 q l2 => Up\<^sub>i (Node2 l1 q l2) x1 (Node2 m x2 r)
    4.43 +    else if a=x1 then T\<^sub>i (Node3 l x1 m x2 r)
    4.44 +    else if a < x2 then
    4.45 +           case ins a m of
    4.46 +             T\<^sub>i m' => T\<^sub>i (Node3 l x1 m' x2 r)
    4.47 +           | Up\<^sub>i m1 q m2 => Up\<^sub>i (Node2 l x1 m1) q (Node2 m2 x2 r)
    4.48 +         else if a=x2 then T\<^sub>i (Node3 l x1 m x2 r)
    4.49 +         else
    4.50 +           case ins a r of
    4.51 +             T\<^sub>i r' => T\<^sub>i (Node3 l x1 m x2 r')
    4.52 +           | Up\<^sub>i r1 q r2 => Up\<^sub>i (Node2 l x1 m) x2 (Node2 r1 q r2))"
    4.53 +
    4.54 +hide_const insert
    4.55 +
    4.56 +definition insert :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
    4.57 +"insert a t = tree\<^sub>i(ins a t)"
    4.58 +
    4.59 +datatype 'a up\<^sub>d = T\<^sub>d "'a tree23" | Up\<^sub>d "'a tree23"
    4.60 +
    4.61 +fun tree\<^sub>d :: "'a up\<^sub>d \<Rightarrow> 'a tree23" where
    4.62 +"tree\<^sub>d (T\<^sub>d x) = x" |
    4.63 +"tree\<^sub>d (Up\<^sub>d x) = x"
    4.64 +
    4.65 +(* Variation: return None to signal no-change *)
    4.66 +
    4.67 +fun node21 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
    4.68 +"node21 (T\<^sub>d t1) a t2 = T\<^sub>d(Node2 t1 a t2)" |
    4.69 +"node21 (Up\<^sub>d t1) a (Node2 t2 b t3) = Up\<^sub>d(Node3 t1 a t2 b t3)" |
    4.70 +"node21 (Up\<^sub>d t1) a (Node3 t2 b t3 c t4) = T\<^sub>d(Node2 (Node2 t1 a t2) b (Node2 t3 c t4))"
    4.71 +
    4.72 +fun node22 :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where
    4.73 +"node22 t1 a (T\<^sub>d t2) = T\<^sub>d(Node2 t1 a t2)" |
    4.74 +"node22 (Node2 t1 b t2) a (Up\<^sub>d t3) = Up\<^sub>d(Node3 t1 b t2 a t3)" |
    4.75 +"node22 (Node3 t1 b t2 c t3) a (Up\<^sub>d t4) = T\<^sub>d(Node2 (Node2 t1 b t2) c (Node2 t3 a t4))"
    4.76 +
    4.77 +fun node31 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
    4.78 +"node31 (T\<^sub>d t1) a t2 b t3 = T\<^sub>d(Node3 t1 a t2 b t3)" |
    4.79 +"node31 (Up\<^sub>d t1) a (Node2 t2 b t3) c t4 = T\<^sub>d(Node2 (Node3 t1 a t2 b t3) c t4)" |
    4.80 +"node31 (Up\<^sub>d t1) a (Node3 t2 b t3 c t4) d t5 = T\<^sub>d(Node3 (Node2 t1 a t2) b (Node2 t3 c t4) d t5)"
    4.81 +
    4.82 +fun node32 :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
    4.83 +"node32 t1 a (T\<^sub>d t2) b t3 = T\<^sub>d(Node3 t1 a t2 b t3)" |
    4.84 +"node32 t1 a (Up\<^sub>d t2) b (Node2 t3 c t4) = T\<^sub>d(Node2 t1 a (Node3 t2 b t3 c t4))" |
    4.85 +"node32 t1 a (Up\<^sub>d t2) b (Node3 t3 c t4 d t5) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))"
    4.86 +
    4.87 +fun node33 :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where
    4.88 +"node33 l a m b (T\<^sub>d r) = T\<^sub>d(Node3 l a m b r)" |
    4.89 +"node33 t1 a (Node2 t2 b t3) c (Up\<^sub>d t4) = T\<^sub>d(Node2 t1 a (Node3 t2 b t3 c t4))" |
    4.90 +"node33 t1 a (Node3 t2 b t3 c t4) d (Up\<^sub>d t5) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))"
    4.91 +
    4.92 +fun del_min :: "'a tree23 \<Rightarrow> 'a * 'a up\<^sub>d" where
    4.93 +"del_min (Node2 Leaf a Leaf) = (a, Up\<^sub>d Leaf)" |
    4.94 +"del_min (Node3 Leaf a Leaf b Leaf) = (a, T\<^sub>d(Node2 Leaf b Leaf))" |
    4.95 +"del_min (Node2 l a r) = (let (x,l') = del_min l in (x, node21 l' a r))" |
    4.96 +"del_min (Node3 l a m b r) = (let (x,l') = del_min l in (x, node31 l' a m b r))"
    4.97 +
    4.98 +fun del :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d"
    4.99 +where
   4.100 +"del k Leaf = T\<^sub>d Leaf" |
   4.101 +"del k (Node2 Leaf p Leaf) = (if k=p then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf p Leaf))" |
   4.102 +"del k (Node3 Leaf p Leaf q Leaf) = T\<^sub>d(if k=p then Node2 Leaf q Leaf
   4.103 +  else if k=q then Node2 Leaf p Leaf else Node3 Leaf p Leaf q Leaf)" |
   4.104 +"del k (Node2 l a r) = (if k<a then node21 (del k l) a r else
   4.105 +  if k > a then node22 l a (del k r) else
   4.106 +  let (a',t) = del_min r in node22 l a' t)" |
   4.107 +"del k (Node3 l a m b r) = (if k<a then node31 (del k l) a m b r else
   4.108 +  if k = a then let (a',m') = del_min m in node32 l a' m' b r else
   4.109 +  if k < b then node32 l a (del k m) b r else
   4.110 +  if k = b then let (b',r') = del_min r in node33 l a m b' r'
   4.111 +  else node33 l a m b (del k r))"
   4.112 +
   4.113 +definition delete :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
   4.114 +"delete k t = tree\<^sub>d(del k t)"
   4.115 +
   4.116 +
   4.117 +declare prod.splits [split]
   4.118 +
   4.119 +subsection "Functional Correctness"
   4.120 +
   4.121 +
   4.122 +subsubsection "Proofs for isin"
   4.123 +
   4.124 +lemma "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
   4.125 +by (induction t) (auto simp: elems_simps1)
   4.126 +
   4.127 +lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
   4.128 +by (induction t) (auto simp: elems_simps2)
   4.129 +
   4.130 +
   4.131 +subsubsection "Proofs for insert"
   4.132 +
   4.133 +lemma inorder_ins:
   4.134 +  "sorted(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(ins x t)) = ins_list x (inorder t)"
   4.135 +by(induction t) (auto simp: ins_list_simps split: up\<^sub>i.splits)
   4.136 +
   4.137 +lemma inorder_insert:
   4.138 +  "sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)"
   4.139 +by(simp add: insert_def inorder_ins)
   4.140 +
   4.141 +
   4.142 +subsubsection "Proofs for delete"
   4.143 +
   4.144 +lemma inorder_node21: "height r > 0 \<Longrightarrow>
   4.145 +  inorder (tree\<^sub>d (node21 l' a r)) = inorder (tree\<^sub>d l') @ a # inorder r"
   4.146 +by(induct l' a r rule: node21.induct) auto
   4.147 +
   4.148 +lemma inorder_node22: "height l > 0 \<Longrightarrow>
   4.149 +  inorder (tree\<^sub>d (node22 l a r')) = inorder l @ a # inorder (tree\<^sub>d r')"
   4.150 +by(induct l a r' rule: node22.induct) auto
   4.151 +
   4.152 +lemma inorder_node31: "height m > 0 \<Longrightarrow>
   4.153 +  inorder (tree\<^sub>d (node31 l' a m b r)) = inorder (tree\<^sub>d l') @ a # inorder m @ b # inorder r"
   4.154 +by(induct l' a m b r rule: node31.induct) auto
   4.155 +
   4.156 +lemma inorder_node32: "height r > 0 \<Longrightarrow>
   4.157 +  inorder (tree\<^sub>d (node32 l a m' b r)) = inorder l @ a # inorder (tree\<^sub>d m') @ b # inorder r"
   4.158 +by(induct l a m' b r rule: node32.induct) auto
   4.159 +
   4.160 +lemma inorder_node33: "height m > 0 \<Longrightarrow>
   4.161 +  inorder (tree\<^sub>d (node33 l a m b r')) = inorder l @ a # inorder m @ b # inorder (tree\<^sub>d r')"
   4.162 +by(induct l a m b r' rule: node33.induct) auto
   4.163 +
   4.164 +lemmas inorder_nodes = inorder_node21 inorder_node22
   4.165 +  inorder_node31 inorder_node32 inorder_node33
   4.166 +
   4.167 +lemma del_minD:
   4.168 +  "del_min t = (x,t') \<Longrightarrow> bal t \<Longrightarrow> height t > 0 \<Longrightarrow>
   4.169 +  x # inorder(tree\<^sub>d t') = inorder t"
   4.170 +by(induction t arbitrary: t' rule: del_min.induct)
   4.171 +  (auto simp: inorder_nodes)
   4.172 +
   4.173 +lemma inorder_del: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
   4.174 +  inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
   4.175 +by(induction t rule: del.induct)
   4.176 +  (auto simp: del_list_simps inorder_nodes del_minD)
   4.177 +
   4.178 +lemma inorder_delete: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
   4.179 +  inorder(delete x t) = del_list x (inorder t)"
   4.180 +by(simp add: delete_def inorder_del)
   4.181 +
   4.182 +
   4.183 +subsection \<open>Balancedness\<close>
   4.184 +
   4.185 +
   4.186 +subsubsection "Proofs for insert"
   4.187 +
   4.188 +text{* First a standard proof that @{const ins} preserves @{const bal}. *}
   4.189 +
   4.190 +instantiation up\<^sub>i :: (type)height
   4.191 +begin
   4.192 +
   4.193 +fun height_up\<^sub>i :: "'a up\<^sub>i \<Rightarrow> nat" where
   4.194 +"height (T\<^sub>i t) = height t" |
   4.195 +"height (Up\<^sub>i l a r) = height l"
   4.196 +
   4.197 +instance ..
   4.198 +
   4.199 +end
   4.200 +
   4.201 +lemma bal_ins: "bal t \<Longrightarrow> bal (tree\<^sub>i(ins a t)) \<and> height(ins a t) = height t"
   4.202 +by (induct t) (auto split: up\<^sub>i.split)
   4.203 +
   4.204 +text{* Now an alternative proof (by Brian Huffman) that runs faster because
   4.205 +two properties (balance and height) are combined in one predicate. *}
   4.206 +
   4.207 +inductive full :: "nat \<Rightarrow> 'a tree23 \<Rightarrow> bool" where
   4.208 +"full 0 Leaf" |
   4.209 +"\<lbrakk>full n l; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Node2 l p r)" |
   4.210 +"\<lbrakk>full n l; full n m; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Node3 l p m q r)"
   4.211 +
   4.212 +inductive_cases full_elims:
   4.213 +  "full n Leaf"
   4.214 +  "full n (Node2 l p r)"
   4.215 +  "full n (Node3 l p m q r)"
   4.216 +
   4.217 +inductive_cases full_0_elim: "full 0 t"
   4.218 +inductive_cases full_Suc_elim: "full (Suc n) t"
   4.219 +
   4.220 +lemma full_0_iff [simp]: "full 0 t \<longleftrightarrow> t = Leaf"
   4.221 +  by (auto elim: full_0_elim intro: full.intros)
   4.222 +
   4.223 +lemma full_Leaf_iff [simp]: "full n Leaf \<longleftrightarrow> n = 0"
   4.224 +  by (auto elim: full_elims intro: full.intros)
   4.225 +
   4.226 +lemma full_Suc_Node2_iff [simp]:
   4.227 +  "full (Suc n) (Node2 l p r) \<longleftrightarrow> full n l \<and> full n r"
   4.228 +  by (auto elim: full_elims intro: full.intros)
   4.229 +
   4.230 +lemma full_Suc_Node3_iff [simp]:
   4.231 +  "full (Suc n) (Node3 l p m q r) \<longleftrightarrow> full n l \<and> full n m \<and> full n r"
   4.232 +  by (auto elim: full_elims intro: full.intros)
   4.233 +
   4.234 +lemma full_imp_height: "full n t \<Longrightarrow> height t = n"
   4.235 +  by (induct set: full, simp_all)
   4.236 +
   4.237 +lemma full_imp_bal: "full n t \<Longrightarrow> bal t"
   4.238 +  by (induct set: full, auto dest: full_imp_height)
   4.239 +
   4.240 +lemma bal_imp_full: "bal t \<Longrightarrow> full (height t) t"
   4.241 +  by (induct t, simp_all)
   4.242 +
   4.243 +lemma bal_iff_full: "bal t \<longleftrightarrow> (\<exists>n. full n t)"
   4.244 +  by (auto elim!: bal_imp_full full_imp_bal)
   4.245 +
   4.246 +text {* The @{const "insert"} function either preserves the height of the
   4.247 +tree, or increases it by one. The constructor returned by the @{term
   4.248 +"insert"} function determines which: A return value of the form @{term
   4.249 +"T\<^sub>i t"} indicates that the height will be the same. A value of the
   4.250 +form @{term "Up\<^sub>i l p r"} indicates an increase in height. *}
   4.251 +
   4.252 +fun full\<^sub>i :: "nat \<Rightarrow> 'a up\<^sub>i \<Rightarrow> bool" where
   4.253 +"full\<^sub>i n (T\<^sub>i t) \<longleftrightarrow> full n t" |
   4.254 +"full\<^sub>i n (Up\<^sub>i l p r) \<longleftrightarrow> full n l \<and> full n r"
   4.255 +
   4.256 +lemma full\<^sub>i_ins: "full n t \<Longrightarrow> full\<^sub>i n (ins a t)"
   4.257 +by (induct rule: full.induct) (auto split: up\<^sub>i.split)
   4.258 +
   4.259 +text {* The @{const insert} operation preserves balance. *}
   4.260 +
   4.261 +lemma bal_insert: "bal t \<Longrightarrow> bal (insert a t)"
   4.262 +unfolding bal_iff_full insert_def
   4.263 +apply (erule exE)
   4.264 +apply (drule full\<^sub>i_ins [of _ _ a])
   4.265 +apply (cases "ins a t")
   4.266 +apply (auto intro: full.intros)
   4.267 +done
   4.268 +
   4.269 +
   4.270 +subsection "Proofs for delete"
   4.271 +
   4.272 +instantiation up\<^sub>d :: (type)height
   4.273 +begin
   4.274 +
   4.275 +fun height_up\<^sub>d :: "'a up\<^sub>d \<Rightarrow> nat" where
   4.276 +"height (T\<^sub>d t) = height t" |
   4.277 +"height (Up\<^sub>d t) = height t + 1"
   4.278 +
   4.279 +instance ..
   4.280 +
   4.281 +end
   4.282 +
   4.283 +lemma bal_tree\<^sub>d_node21:
   4.284 +  "\<lbrakk>bal r; bal (tree\<^sub>d l'); height r = height l' \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d (node21 l' a r))"
   4.285 +by(induct l' a r rule: node21.induct) auto
   4.286 +
   4.287 +lemma bal_tree\<^sub>d_node22:
   4.288 +  "\<lbrakk>bal(tree\<^sub>d r'); bal l; height r' = height l \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d (node22 l a r'))"
   4.289 +by(induct l a r' rule: node22.induct) auto
   4.290 +
   4.291 +lemma bal_tree\<^sub>d_node31:
   4.292 +  "\<lbrakk> bal (tree\<^sub>d l'); bal m; bal r; height l' = height r; height m = height r \<rbrakk>
   4.293 +  \<Longrightarrow> bal (tree\<^sub>d (node31 l' a m b r))"
   4.294 +by(induct l' a m b r rule: node31.induct) auto
   4.295 +
   4.296 +lemma bal_tree\<^sub>d_node32:
   4.297 +  "\<lbrakk> bal l; bal (tree\<^sub>d m'); bal r; height l = height r; height m' = height r \<rbrakk>
   4.298 +  \<Longrightarrow> bal (tree\<^sub>d (node32 l a m' b r))"
   4.299 +by(induct l a m' b r rule: node32.induct) auto
   4.300 +
   4.301 +lemma bal_tree\<^sub>d_node33:
   4.302 +  "\<lbrakk> bal l; bal m; bal(tree\<^sub>d r'); height l = height r'; height m = height r' \<rbrakk>
   4.303 +  \<Longrightarrow> bal (tree\<^sub>d (node33 l a m b r'))"
   4.304 +by(induct l a m b r' rule: node33.induct) auto
   4.305 +
   4.306 +lemmas bals = bal_tree\<^sub>d_node21 bal_tree\<^sub>d_node22
   4.307 +  bal_tree\<^sub>d_node31 bal_tree\<^sub>d_node32 bal_tree\<^sub>d_node33
   4.308 +
   4.309 +lemma height'_node21:
   4.310 +   "height r > 0 \<Longrightarrow> height(node21 l' a r) = max (height l') (height r) + 1"
   4.311 +by(induct l' a r rule: node21.induct)(simp_all)
   4.312 +
   4.313 +lemma height'_node22:
   4.314 +   "height l > 0 \<Longrightarrow> height(node22 l a r') = max (height l) (height r') + 1"
   4.315 +by(induct l a r' rule: node22.induct)(simp_all)
   4.316 +
   4.317 +lemma height'_node31:
   4.318 +  "height m > 0 \<Longrightarrow> height(node31 l a m b r) =
   4.319 +   max (height l) (max (height m) (height r)) + 1"
   4.320 +by(induct l a m b r rule: node31.induct)(simp_all add: max_def)
   4.321 +
   4.322 +lemma height'_node32:
   4.323 +  "height r > 0 \<Longrightarrow> height(node32 l a m b r) =
   4.324 +   max (height l) (max (height m) (height r)) + 1"
   4.325 +by(induct l a m b r rule: node32.induct)(simp_all add: max_def)
   4.326 +
   4.327 +lemma height'_node33:
   4.328 +  "height m > 0 \<Longrightarrow> height(node33 l a m b r) =
   4.329 +   max (height l) (max (height m) (height r)) + 1"
   4.330 +by(induct l a m b r rule: node33.induct)(simp_all add: max_def)
   4.331 +
   4.332 +lemmas heights = height'_node21 height'_node22
   4.333 +  height'_node31 height'_node32 height'_node33
   4.334 +
   4.335 +lemma height_del_min:
   4.336 +  "del_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> bal t \<Longrightarrow> height t' = height t"
   4.337 +by(induct t arbitrary: x t' rule: del_min.induct)
   4.338 +  (auto simp: heights split: prod.splits)
   4.339 +
   4.340 +lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
   4.341 +by(induction x t rule: del.induct)
   4.342 +  (auto simp add: heights max_def height_del_min)
   4.343 +
   4.344 +lemma bal_del_min:
   4.345 +  "\<lbrakk> del_min t = (x, t'); bal t; height t > 0 \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d t')"
   4.346 +by(induct t arbitrary: x t' rule: del_min.induct)
   4.347 +  (auto simp: heights height_del_min bals)
   4.348 +
   4.349 +lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
   4.350 +by(induction x t rule: del.induct)
   4.351 +  (auto simp: bals bal_del_min height_del height_del_min)
   4.352 +corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
   4.353 +by(simp add: delete_def bal_tree\<^sub>d_del)
   4.354 +
   4.355 +
   4.356 +subsection \<open>Overall Correctness\<close>
   4.357 +
   4.358 +interpretation Set_by_Ordered
   4.359 +where empty = Leaf and isin = isin and insert = insert and delete = delete
   4.360 +and inorder = inorder and wf = bal
   4.361 +proof (standard, goal_cases)
   4.362 +  case 2 thus ?case by(simp add: isin_set)
   4.363 +next
   4.364 +  case 3 thus ?case by(simp add: inorder_insert)
   4.365 +next
   4.366 +  case 4 thus ?case by(simp add: inorder_delete)
   4.367 +next
   4.368 +  case 6 thus ?case by(simp add: bal_insert)
   4.369 +next
   4.370 +  case 7 thus ?case by(simp add: bal_delete)
   4.371 +qed simp+
   4.372 +
   4.373 +end
     5.1 --- a/src/HOL/ROOT	Sat Oct 17 16:08:30 2015 +0200
     5.2 +++ b/src/HOL/ROOT	Sun Oct 18 17:25:13 2015 +0200
     5.3 @@ -178,6 +178,7 @@
     5.4      Tree_Map
     5.5      AVL_Map
     5.6      RBT_Map
     5.7 +    Tree23_Map
     5.8    document_files "root.tex" "root.bib"
     5.9  
    5.10  session "HOL-Import" in Import = HOL +