src/HOL/Data_Structures/Tree234_Map.thy
changeset 61640 44c9198f210c
parent 61581 00d9682e8dd7
child 61686 e6784939d645
     1.1 --- a/src/HOL/Data_Structures/Tree234_Map.thy	Wed Nov 11 16:42:30 2015 +0100
     1.2 +++ b/src/HOL/Data_Structures/Tree234_Map.thy	Wed Nov 11 18:32:26 2015 +0100
     1.3 @@ -1,181 +1,181 @@
     1.4 -(* Author: Tobias Nipkow *)
     1.5 -
     1.6 -section \<open>A 2-3-4 Tree Implementation of Maps\<close>
     1.7 -
     1.8 -theory Tree234_Map
     1.9 -imports
    1.10 -  Tree234_Set
    1.11 -  "../Data_Structures/Map_by_Ordered"
    1.12 -begin
    1.13 -
    1.14 -subsection \<open>Map operations on 2-3-4 trees\<close>
    1.15 -
    1.16 -fun lookup :: "('a::cmp * 'b) tree234 \<Rightarrow> 'a \<Rightarrow> 'b option" where
    1.17 -"lookup Leaf x = None" |
    1.18 -"lookup (Node2 l (a,b) r) x = (case cmp x a of
    1.19 -  LT \<Rightarrow> lookup l x |
    1.20 -  GT \<Rightarrow> lookup r x |
    1.21 -  EQ \<Rightarrow> Some b)" |
    1.22 -"lookup (Node3 l (a1,b1) m (a2,b2) r) x = (case cmp x a1 of
    1.23 -  LT \<Rightarrow> lookup l x |
    1.24 -  EQ \<Rightarrow> Some b1 |
    1.25 -  GT \<Rightarrow> (case cmp x a2 of
    1.26 -          LT \<Rightarrow> lookup m x |
    1.27 -          EQ \<Rightarrow> Some b2 |
    1.28 -          GT \<Rightarrow> lookup r x))" |
    1.29 -"lookup (Node4 t1 (a1,b1) t2 (a2,b2) t3 (a3,b3) t4) x = (case cmp x a2 of
    1.30 -  LT \<Rightarrow> (case cmp x a1 of
    1.31 -           LT \<Rightarrow> lookup t1 x | EQ \<Rightarrow> Some b1 | GT \<Rightarrow> lookup t2 x) |
    1.32 -  EQ \<Rightarrow> Some b2 |
    1.33 -  GT \<Rightarrow> (case cmp x a3 of
    1.34 -           LT \<Rightarrow> lookup t3 x | EQ \<Rightarrow> Some b3 | GT \<Rightarrow> lookup t4 x))"
    1.35 -
    1.36 -fun upd :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) up\<^sub>i" where
    1.37 -"upd x y Leaf = Up\<^sub>i Leaf (x,y) Leaf" |
    1.38 -"upd x y (Node2 l ab r) = (case cmp x (fst ab) of
    1.39 -   LT \<Rightarrow> (case upd x y l of
    1.40 -           T\<^sub>i l' => T\<^sub>i (Node2 l' ab r)
    1.41 -         | Up\<^sub>i l1 ab' l2 => T\<^sub>i (Node3 l1 ab' l2 ab r)) |
    1.42 -   EQ \<Rightarrow> T\<^sub>i (Node2 l (x,y) r) |
    1.43 -   GT \<Rightarrow> (case upd x y r of
    1.44 -           T\<^sub>i r' => T\<^sub>i (Node2 l ab r')
    1.45 -         | Up\<^sub>i r1 ab' r2 => T\<^sub>i (Node3 l ab r1 ab' r2)))" |
    1.46 -"upd x y (Node3 l ab1 m ab2 r) = (case cmp x (fst ab1) of
    1.47 -   LT \<Rightarrow> (case upd x y l of
    1.48 -           T\<^sub>i l' => T\<^sub>i (Node3 l' ab1 m ab2 r)
    1.49 -         | Up\<^sub>i l1 ab' l2 => Up\<^sub>i (Node2 l1 ab' l2) ab1 (Node2 m ab2 r)) |
    1.50 -   EQ \<Rightarrow> T\<^sub>i (Node3 l (x,y) m ab2 r) |
    1.51 -   GT \<Rightarrow> (case cmp x (fst ab2) of
    1.52 -           LT \<Rightarrow> (case upd x y m of
    1.53 -                   T\<^sub>i m' => T\<^sub>i (Node3 l ab1 m' ab2 r)
    1.54 -                 | Up\<^sub>i m1 ab' m2 => Up\<^sub>i (Node2 l ab1 m1) ab' (Node2 m2 ab2 r)) |
    1.55 -           EQ \<Rightarrow> T\<^sub>i (Node3 l ab1 m (x,y) r) |
    1.56 -           GT \<Rightarrow> (case upd x y r of
    1.57 -                   T\<^sub>i r' => T\<^sub>i (Node3 l ab1 m ab2 r')
    1.58 -                 | Up\<^sub>i r1 ab' r2 => Up\<^sub>i (Node2 l ab1 m) ab2 (Node2 r1 ab' r2))))" |
    1.59 -"upd x y (Node4 t1 ab1 t2 ab2 t3 ab3 t4) = (case cmp x (fst ab2) of
    1.60 -   LT \<Rightarrow> (case cmp x (fst ab1) of
    1.61 -            LT \<Rightarrow> (case upd x y t1 of
    1.62 -                     T\<^sub>i t1' => T\<^sub>i (Node4 t1' ab1 t2 ab2 t3 ab3 t4)
    1.63 -                  | Up\<^sub>i t11 q t12 => Up\<^sub>i (Node2 t11 q t12) ab1 (Node3 t2 ab2 t3 ab3 t4)) |
    1.64 -            EQ \<Rightarrow> T\<^sub>i (Node4 t1 (x,y) t2 ab2 t3 ab3 t4) |
    1.65 -            GT \<Rightarrow> (case upd x y t2 of
    1.66 -                    T\<^sub>i t2' => T\<^sub>i (Node4 t1 ab1 t2' ab2 t3 ab3 t4)
    1.67 -                  | Up\<^sub>i t21 q t22 => Up\<^sub>i (Node2 t1 ab1 t21) q (Node3 t22 ab2 t3 ab3 t4))) |
    1.68 -   EQ \<Rightarrow> T\<^sub>i (Node4 t1 ab1 t2 (x,y) t3 ab3 t4) |
    1.69 -   GT \<Rightarrow> (case cmp x (fst ab3) of
    1.70 -            LT \<Rightarrow> (case upd x y t3 of
    1.71 -                    T\<^sub>i t3' \<Rightarrow> T\<^sub>i (Node4 t1 ab1 t2 ab2 t3' ab3 t4)
    1.72 -                  | Up\<^sub>i t31 q t32 => Up\<^sub>i (Node2 t1 ab1 t2) ab2(*q*) (Node3 t31 q t32 ab3 t4)) |
    1.73 -            EQ \<Rightarrow> T\<^sub>i (Node4 t1 ab1 t2 ab2 t3 (x,y) t4) |
    1.74 -            GT \<Rightarrow> (case upd x y t4 of
    1.75 -                    T\<^sub>i t4' => T\<^sub>i (Node4 t1 ab1 t2 ab2 t3 ab3 t4')
    1.76 -                  | Up\<^sub>i t41 q t42 => Up\<^sub>i (Node2 t1 ab1 t2) ab2 (Node3 t3 ab3 t41 q t42))))"
    1.77 -
    1.78 -definition update :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) tree234" where
    1.79 -"update x y t = tree\<^sub>i(upd x y t)"
    1.80 -
    1.81 -fun del :: "'a::cmp \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) up\<^sub>d" where
    1.82 -"del x Leaf = T\<^sub>d Leaf" |
    1.83 -"del x (Node2 Leaf ab1 Leaf) = (if x=fst ab1 then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf ab1 Leaf))" |
    1.84 -"del x (Node3 Leaf ab1 Leaf ab2 Leaf) = T\<^sub>d(if x=fst ab1 then Node2 Leaf ab2 Leaf
    1.85 -  else if x=fst ab2 then Node2 Leaf ab1 Leaf else Node3 Leaf ab1 Leaf ab2 Leaf)" |
    1.86 -"del x (Node4 Leaf ab1 Leaf ab2 Leaf ab3 Leaf) =
    1.87 -  T\<^sub>d(if x = fst ab1 then Node3 Leaf ab2 Leaf ab3 Leaf else
    1.88 -     if x = fst ab2 then Node3 Leaf ab1 Leaf ab3 Leaf else
    1.89 -     if x = fst ab3 then Node3 Leaf ab1 Leaf ab2 Leaf
    1.90 -     else Node4 Leaf ab1 Leaf ab2 Leaf ab3 Leaf)" |
    1.91 -"del x (Node2 l ab1 r) = (case cmp x (fst ab1) of
    1.92 -  LT \<Rightarrow> node21 (del x l) ab1 r |
    1.93 -  GT \<Rightarrow> node22 l ab1 (del x r) |
    1.94 -  EQ \<Rightarrow> let (ab1',t) = del_min r in node22 l ab1' t)" |
    1.95 -"del x (Node3 l ab1 m ab2 r) = (case cmp x (fst ab1) of
    1.96 -  LT \<Rightarrow> node31 (del x l) ab1 m ab2 r |
    1.97 -  EQ \<Rightarrow> let (ab1',m') = del_min m in node32 l ab1' m' ab2 r |
    1.98 -  GT \<Rightarrow> (case cmp x (fst ab2) of
    1.99 -           LT \<Rightarrow> node32 l ab1 (del x m) ab2 r |
   1.100 -           EQ \<Rightarrow> let (ab2',r') = del_min r in node33 l ab1 m ab2' r' |
   1.101 -           GT \<Rightarrow> node33 l ab1 m ab2 (del x r)))" |
   1.102 -"del x (Node4 t1 ab1 t2 ab2 t3 ab3 t4) = (case cmp x (fst ab2) of
   1.103 -  LT \<Rightarrow> (case cmp x (fst ab1) of
   1.104 -           LT \<Rightarrow> node41 (del x t1) ab1 t2 ab2 t3 ab3 t4 |
   1.105 -           EQ \<Rightarrow> let (ab',t2') = del_min t2 in node42 t1 ab' t2' ab2 t3 ab3 t4 |
   1.106 -           GT \<Rightarrow> node42 t1 ab1 (del x t2) ab2 t3 ab3 t4) |
   1.107 -  EQ \<Rightarrow> let (ab',t3') = del_min t3 in node43 t1 ab1 t2 ab' t3' ab3 t4 |
   1.108 -  GT \<Rightarrow> (case cmp x (fst ab3) of
   1.109 -          LT \<Rightarrow> node43 t1 ab1 t2 ab2 (del x t3) ab3 t4 |
   1.110 -          EQ \<Rightarrow> let (ab',t4') = del_min t4 in node44 t1 ab1 t2 ab2 t3 ab' t4' |
   1.111 -          GT \<Rightarrow> node44 t1 ab1 t2 ab2 t3 ab3 (del x t4)))"
   1.112 -
   1.113 -definition delete :: "'a::cmp \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) tree234" where
   1.114 -"delete x t = tree\<^sub>d(del x t)"
   1.115 -
   1.116 -
   1.117 -subsection "Functional correctness"
   1.118 -
   1.119 -lemma lookup: "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
   1.120 -by (induction t) (auto simp: map_of_simps split: option.split)
   1.121 -
   1.122 -
   1.123 -lemma inorder_upd:
   1.124 -  "sorted1(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(upd a b t)) = upd_list a b (inorder t)"
   1.125 -by(induction t)
   1.126 -  (auto simp: upd_list_simps, auto simp: upd_list_simps split: up\<^sub>i.splits)
   1.127 -
   1.128 -lemma inorder_update:
   1.129 -  "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)"
   1.130 -by(simp add: update_def inorder_upd)
   1.131 -
   1.132 -
   1.133 -lemma inorder_del: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
   1.134 -  inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
   1.135 -by(induction t rule: del.induct)
   1.136 -  ((auto simp: del_list_simps inorder_nodes del_minD split: prod.splits)[1])+
   1.137 -(* 200 secs (2015) *)
   1.138 -
   1.139 -lemma inorder_delete: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
   1.140 -  inorder(delete x t) = del_list x (inorder t)"
   1.141 -by(simp add: delete_def inorder_del)
   1.142 -
   1.143 -
   1.144 -subsection \<open>Balancedness\<close>
   1.145 -
   1.146 -lemma bal_upd: "bal t \<Longrightarrow> bal (tree\<^sub>i(upd x y t)) \<and> height(upd x y t) = height t"
   1.147 -by (induct t) (auto, auto split: up\<^sub>i.split) (* 20 secs (2015) *)
   1.148 -
   1.149 -lemma bal_update: "bal t \<Longrightarrow> bal (update x y t)"
   1.150 -by (simp add: update_def bal_upd)
   1.151 -
   1.152 -
   1.153 -lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
   1.154 -by(induction x t rule: del.induct)
   1.155 -  (auto simp add: heights height_del_min split: prod.split)
   1.156 -(* 20 secs (2015) *)
   1.157 -
   1.158 -lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
   1.159 -by(induction x t rule: del.induct)
   1.160 -  (auto simp: bals bal_del_min height_del height_del_min split: prod.split)
   1.161 -(* 100 secs (2015) *)
   1.162 -
   1.163 -corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
   1.164 -by(simp add: delete_def bal_tree\<^sub>d_del)
   1.165 -
   1.166 -
   1.167 -subsection \<open>Overall Correctness\<close>
   1.168 -
   1.169 -interpretation T234_Map: Map_by_Ordered
   1.170 -where empty = Leaf and lookup = lookup and update = update and delete = delete
   1.171 -and inorder = inorder and wf = bal
   1.172 -proof (standard, goal_cases)
   1.173 -  case 2 thus ?case by(simp add: lookup)
   1.174 -next
   1.175 -  case 3 thus ?case by(simp add: inorder_update)
   1.176 -next
   1.177 -  case 4 thus ?case by(simp add: inorder_delete)
   1.178 -next
   1.179 -  case 6 thus ?case by(simp add: bal_update)
   1.180 -next
   1.181 -  case 7 thus ?case by(simp add: bal_delete)
   1.182 -qed simp+
   1.183 -
   1.184 -end
   1.185 +(* Author: Tobias Nipkow *)
   1.186 +
   1.187 +section \<open>A 2-3-4 Tree Implementation of Maps\<close>
   1.188 +
   1.189 +theory Tree234_Map
   1.190 +imports
   1.191 +  Tree234_Set
   1.192 +  "../Data_Structures/Map_by_Ordered"
   1.193 +begin
   1.194 +
   1.195 +subsection \<open>Map operations on 2-3-4 trees\<close>
   1.196 +
   1.197 +fun lookup :: "('a::cmp * 'b) tree234 \<Rightarrow> 'a \<Rightarrow> 'b option" where
   1.198 +"lookup Leaf x = None" |
   1.199 +"lookup (Node2 l (a,b) r) x = (case cmp x a of
   1.200 +  LT \<Rightarrow> lookup l x |
   1.201 +  GT \<Rightarrow> lookup r x |
   1.202 +  EQ \<Rightarrow> Some b)" |
   1.203 +"lookup (Node3 l (a1,b1) m (a2,b2) r) x = (case cmp x a1 of
   1.204 +  LT \<Rightarrow> lookup l x |
   1.205 +  EQ \<Rightarrow> Some b1 |
   1.206 +  GT \<Rightarrow> (case cmp x a2 of
   1.207 +          LT \<Rightarrow> lookup m x |
   1.208 +          EQ \<Rightarrow> Some b2 |
   1.209 +          GT \<Rightarrow> lookup r x))" |
   1.210 +"lookup (Node4 t1 (a1,b1) t2 (a2,b2) t3 (a3,b3) t4) x = (case cmp x a2 of
   1.211 +  LT \<Rightarrow> (case cmp x a1 of
   1.212 +           LT \<Rightarrow> lookup t1 x | EQ \<Rightarrow> Some b1 | GT \<Rightarrow> lookup t2 x) |
   1.213 +  EQ \<Rightarrow> Some b2 |
   1.214 +  GT \<Rightarrow> (case cmp x a3 of
   1.215 +           LT \<Rightarrow> lookup t3 x | EQ \<Rightarrow> Some b3 | GT \<Rightarrow> lookup t4 x))"
   1.216 +
   1.217 +fun upd :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) up\<^sub>i" where
   1.218 +"upd x y Leaf = Up\<^sub>i Leaf (x,y) Leaf" |
   1.219 +"upd x y (Node2 l ab r) = (case cmp x (fst ab) of
   1.220 +   LT \<Rightarrow> (case upd x y l of
   1.221 +           T\<^sub>i l' => T\<^sub>i (Node2 l' ab r)
   1.222 +         | Up\<^sub>i l1 ab' l2 => T\<^sub>i (Node3 l1 ab' l2 ab r)) |
   1.223 +   EQ \<Rightarrow> T\<^sub>i (Node2 l (x,y) r) |
   1.224 +   GT \<Rightarrow> (case upd x y r of
   1.225 +           T\<^sub>i r' => T\<^sub>i (Node2 l ab r')
   1.226 +         | Up\<^sub>i r1 ab' r2 => T\<^sub>i (Node3 l ab r1 ab' r2)))" |
   1.227 +"upd x y (Node3 l ab1 m ab2 r) = (case cmp x (fst ab1) of
   1.228 +   LT \<Rightarrow> (case upd x y l of
   1.229 +           T\<^sub>i l' => T\<^sub>i (Node3 l' ab1 m ab2 r)
   1.230 +         | Up\<^sub>i l1 ab' l2 => Up\<^sub>i (Node2 l1 ab' l2) ab1 (Node2 m ab2 r)) |
   1.231 +   EQ \<Rightarrow> T\<^sub>i (Node3 l (x,y) m ab2 r) |
   1.232 +   GT \<Rightarrow> (case cmp x (fst ab2) of
   1.233 +           LT \<Rightarrow> (case upd x y m of
   1.234 +                   T\<^sub>i m' => T\<^sub>i (Node3 l ab1 m' ab2 r)
   1.235 +                 | Up\<^sub>i m1 ab' m2 => Up\<^sub>i (Node2 l ab1 m1) ab' (Node2 m2 ab2 r)) |
   1.236 +           EQ \<Rightarrow> T\<^sub>i (Node3 l ab1 m (x,y) r) |
   1.237 +           GT \<Rightarrow> (case upd x y r of
   1.238 +                   T\<^sub>i r' => T\<^sub>i (Node3 l ab1 m ab2 r')
   1.239 +                 | Up\<^sub>i r1 ab' r2 => Up\<^sub>i (Node2 l ab1 m) ab2 (Node2 r1 ab' r2))))" |
   1.240 +"upd x y (Node4 t1 ab1 t2 ab2 t3 ab3 t4) = (case cmp x (fst ab2) of
   1.241 +   LT \<Rightarrow> (case cmp x (fst ab1) of
   1.242 +            LT \<Rightarrow> (case upd x y t1 of
   1.243 +                     T\<^sub>i t1' => T\<^sub>i (Node4 t1' ab1 t2 ab2 t3 ab3 t4)
   1.244 +                  | Up\<^sub>i t11 q t12 => Up\<^sub>i (Node2 t11 q t12) ab1 (Node3 t2 ab2 t3 ab3 t4)) |
   1.245 +            EQ \<Rightarrow> T\<^sub>i (Node4 t1 (x,y) t2 ab2 t3 ab3 t4) |
   1.246 +            GT \<Rightarrow> (case upd x y t2 of
   1.247 +                    T\<^sub>i t2' => T\<^sub>i (Node4 t1 ab1 t2' ab2 t3 ab3 t4)
   1.248 +                  | Up\<^sub>i t21 q t22 => Up\<^sub>i (Node2 t1 ab1 t21) q (Node3 t22 ab2 t3 ab3 t4))) |
   1.249 +   EQ \<Rightarrow> T\<^sub>i (Node4 t1 ab1 t2 (x,y) t3 ab3 t4) |
   1.250 +   GT \<Rightarrow> (case cmp x (fst ab3) of
   1.251 +            LT \<Rightarrow> (case upd x y t3 of
   1.252 +                    T\<^sub>i t3' \<Rightarrow> T\<^sub>i (Node4 t1 ab1 t2 ab2 t3' ab3 t4)
   1.253 +                  | Up\<^sub>i t31 q t32 => Up\<^sub>i (Node2 t1 ab1 t2) ab2(*q*) (Node3 t31 q t32 ab3 t4)) |
   1.254 +            EQ \<Rightarrow> T\<^sub>i (Node4 t1 ab1 t2 ab2 t3 (x,y) t4) |
   1.255 +            GT \<Rightarrow> (case upd x y t4 of
   1.256 +                    T\<^sub>i t4' => T\<^sub>i (Node4 t1 ab1 t2 ab2 t3 ab3 t4')
   1.257 +                  | Up\<^sub>i t41 q t42 => Up\<^sub>i (Node2 t1 ab1 t2) ab2 (Node3 t3 ab3 t41 q t42))))"
   1.258 +
   1.259 +definition update :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) tree234" where
   1.260 +"update x y t = tree\<^sub>i(upd x y t)"
   1.261 +
   1.262 +fun del :: "'a::cmp \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) up\<^sub>d" where
   1.263 +"del x Leaf = T\<^sub>d Leaf" |
   1.264 +"del x (Node2 Leaf ab1 Leaf) = (if x=fst ab1 then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf ab1 Leaf))" |
   1.265 +"del x (Node3 Leaf ab1 Leaf ab2 Leaf) = T\<^sub>d(if x=fst ab1 then Node2 Leaf ab2 Leaf
   1.266 +  else if x=fst ab2 then Node2 Leaf ab1 Leaf else Node3 Leaf ab1 Leaf ab2 Leaf)" |
   1.267 +"del x (Node4 Leaf ab1 Leaf ab2 Leaf ab3 Leaf) =
   1.268 +  T\<^sub>d(if x = fst ab1 then Node3 Leaf ab2 Leaf ab3 Leaf else
   1.269 +     if x = fst ab2 then Node3 Leaf ab1 Leaf ab3 Leaf else
   1.270 +     if x = fst ab3 then Node3 Leaf ab1 Leaf ab2 Leaf
   1.271 +     else Node4 Leaf ab1 Leaf ab2 Leaf ab3 Leaf)" |
   1.272 +"del x (Node2 l ab1 r) = (case cmp x (fst ab1) of
   1.273 +  LT \<Rightarrow> node21 (del x l) ab1 r |
   1.274 +  GT \<Rightarrow> node22 l ab1 (del x r) |
   1.275 +  EQ \<Rightarrow> let (ab1',t) = del_min r in node22 l ab1' t)" |
   1.276 +"del x (Node3 l ab1 m ab2 r) = (case cmp x (fst ab1) of
   1.277 +  LT \<Rightarrow> node31 (del x l) ab1 m ab2 r |
   1.278 +  EQ \<Rightarrow> let (ab1',m') = del_min m in node32 l ab1' m' ab2 r |
   1.279 +  GT \<Rightarrow> (case cmp x (fst ab2) of
   1.280 +           LT \<Rightarrow> node32 l ab1 (del x m) ab2 r |
   1.281 +           EQ \<Rightarrow> let (ab2',r') = del_min r in node33 l ab1 m ab2' r' |
   1.282 +           GT \<Rightarrow> node33 l ab1 m ab2 (del x r)))" |
   1.283 +"del x (Node4 t1 ab1 t2 ab2 t3 ab3 t4) = (case cmp x (fst ab2) of
   1.284 +  LT \<Rightarrow> (case cmp x (fst ab1) of
   1.285 +           LT \<Rightarrow> node41 (del x t1) ab1 t2 ab2 t3 ab3 t4 |
   1.286 +           EQ \<Rightarrow> let (ab',t2') = del_min t2 in node42 t1 ab' t2' ab2 t3 ab3 t4 |
   1.287 +           GT \<Rightarrow> node42 t1 ab1 (del x t2) ab2 t3 ab3 t4) |
   1.288 +  EQ \<Rightarrow> let (ab',t3') = del_min t3 in node43 t1 ab1 t2 ab' t3' ab3 t4 |
   1.289 +  GT \<Rightarrow> (case cmp x (fst ab3) of
   1.290 +          LT \<Rightarrow> node43 t1 ab1 t2 ab2 (del x t3) ab3 t4 |
   1.291 +          EQ \<Rightarrow> let (ab',t4') = del_min t4 in node44 t1 ab1 t2 ab2 t3 ab' t4' |
   1.292 +          GT \<Rightarrow> node44 t1 ab1 t2 ab2 t3 ab3 (del x t4)))"
   1.293 +
   1.294 +definition delete :: "'a::cmp \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) tree234" where
   1.295 +"delete x t = tree\<^sub>d(del x t)"
   1.296 +
   1.297 +
   1.298 +subsection "Functional correctness"
   1.299 +
   1.300 +lemma lookup: "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
   1.301 +by (induction t) (auto simp: map_of_simps split: option.split)
   1.302 +
   1.303 +
   1.304 +lemma inorder_upd:
   1.305 +  "sorted1(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(upd a b t)) = upd_list a b (inorder t)"
   1.306 +by(induction t)
   1.307 +  (auto simp: upd_list_simps, auto simp: upd_list_simps split: up\<^sub>i.splits)
   1.308 +
   1.309 +lemma inorder_update:
   1.310 +  "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)"
   1.311 +by(simp add: update_def inorder_upd)
   1.312 +
   1.313 +
   1.314 +lemma inorder_del: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
   1.315 +  inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
   1.316 +by(induction t rule: del.induct)
   1.317 +  ((auto simp: del_list_simps inorder_nodes del_minD split: prod.splits)[1])+
   1.318 +(* 200 secs (2015) *)
   1.319 +
   1.320 +lemma inorder_delete: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
   1.321 +  inorder(delete x t) = del_list x (inorder t)"
   1.322 +by(simp add: delete_def inorder_del)
   1.323 +
   1.324 +
   1.325 +subsection \<open>Balancedness\<close>
   1.326 +
   1.327 +lemma bal_upd: "bal t \<Longrightarrow> bal (tree\<^sub>i(upd x y t)) \<and> height(upd x y t) = height t"
   1.328 +by (induct t) (auto, auto split: up\<^sub>i.split) (* 20 secs (2015) *)
   1.329 +
   1.330 +lemma bal_update: "bal t \<Longrightarrow> bal (update x y t)"
   1.331 +by (simp add: update_def bal_upd)
   1.332 +
   1.333 +
   1.334 +lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
   1.335 +by(induction x t rule: del.induct)
   1.336 +  (auto simp add: heights height_del_min split: prod.split)
   1.337 +(* 20 secs (2015) *)
   1.338 +
   1.339 +lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
   1.340 +by(induction x t rule: del.induct)
   1.341 +  (auto simp: bals bal_del_min height_del height_del_min split: prod.split)
   1.342 +(* 100 secs (2015) *)
   1.343 +
   1.344 +corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
   1.345 +by(simp add: delete_def bal_tree\<^sub>d_del)
   1.346 +
   1.347 +
   1.348 +subsection \<open>Overall Correctness\<close>
   1.349 +
   1.350 +interpretation T234_Map: Map_by_Ordered
   1.351 +where empty = Leaf and lookup = lookup and update = update and delete = delete
   1.352 +and inorder = inorder and wf = bal
   1.353 +proof (standard, goal_cases)
   1.354 +  case 2 thus ?case by(simp add: lookup)
   1.355 +next
   1.356 +  case 3 thus ?case by(simp add: inorder_update)
   1.357 +next
   1.358 +  case 4 thus ?case by(simp add: inorder_delete)
   1.359 +next
   1.360 +  case 6 thus ?case by(simp add: bal_update)
   1.361 +next
   1.362 +  case 7 thus ?case by(simp add: bal_delete)
   1.363 +qed simp+
   1.364 +
   1.365 +end