61640
|
1 |
(* Author: Tobias Nipkow *)
|
|
2 |
|
|
3 |
section \<open>A 2-3-4 Tree Implementation of Maps\<close>
|
|
4 |
|
|
5 |
theory Tree234_Map
|
|
6 |
imports
|
|
7 |
Tree234_Set
|
|
8 |
"../Data_Structures/Map_by_Ordered"
|
|
9 |
begin
|
|
10 |
|
|
11 |
subsection \<open>Map operations on 2-3-4 trees\<close>
|
|
12 |
|
|
13 |
fun lookup :: "('a::cmp * 'b) tree234 \<Rightarrow> 'a \<Rightarrow> 'b option" where
|
|
14 |
"lookup Leaf x = None" |
|
|
15 |
"lookup (Node2 l (a,b) r) x = (case cmp x a of
|
|
16 |
LT \<Rightarrow> lookup l x |
|
|
17 |
GT \<Rightarrow> lookup r x |
|
|
18 |
EQ \<Rightarrow> Some b)" |
|
|
19 |
"lookup (Node3 l (a1,b1) m (a2,b2) r) x = (case cmp x a1 of
|
|
20 |
LT \<Rightarrow> lookup l x |
|
|
21 |
EQ \<Rightarrow> Some b1 |
|
|
22 |
GT \<Rightarrow> (case cmp x a2 of
|
|
23 |
LT \<Rightarrow> lookup m x |
|
|
24 |
EQ \<Rightarrow> Some b2 |
|
|
25 |
GT \<Rightarrow> lookup r x))" |
|
|
26 |
"lookup (Node4 t1 (a1,b1) t2 (a2,b2) t3 (a3,b3) t4) x = (case cmp x a2 of
|
|
27 |
LT \<Rightarrow> (case cmp x a1 of
|
|
28 |
LT \<Rightarrow> lookup t1 x | EQ \<Rightarrow> Some b1 | GT \<Rightarrow> lookup t2 x) |
|
|
29 |
EQ \<Rightarrow> Some b2 |
|
|
30 |
GT \<Rightarrow> (case cmp x a3 of
|
|
31 |
LT \<Rightarrow> lookup t3 x | EQ \<Rightarrow> Some b3 | GT \<Rightarrow> lookup t4 x))"
|
|
32 |
|
|
33 |
fun upd :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) up\<^sub>i" where
|
|
34 |
"upd x y Leaf = Up\<^sub>i Leaf (x,y) Leaf" |
|
|
35 |
"upd x y (Node2 l ab r) = (case cmp x (fst ab) of
|
|
36 |
LT \<Rightarrow> (case upd x y l of
|
|
37 |
T\<^sub>i l' => T\<^sub>i (Node2 l' ab r)
|
|
38 |
| Up\<^sub>i l1 ab' l2 => T\<^sub>i (Node3 l1 ab' l2 ab r)) |
|
|
39 |
EQ \<Rightarrow> T\<^sub>i (Node2 l (x,y) r) |
|
|
40 |
GT \<Rightarrow> (case upd x y r of
|
|
41 |
T\<^sub>i r' => T\<^sub>i (Node2 l ab r')
|
|
42 |
| Up\<^sub>i r1 ab' r2 => T\<^sub>i (Node3 l ab r1 ab' r2)))" |
|
|
43 |
"upd x y (Node3 l ab1 m ab2 r) = (case cmp x (fst ab1) of
|
|
44 |
LT \<Rightarrow> (case upd x y l of
|
|
45 |
T\<^sub>i l' => T\<^sub>i (Node3 l' ab1 m ab2 r)
|
|
46 |
| Up\<^sub>i l1 ab' l2 => Up\<^sub>i (Node2 l1 ab' l2) ab1 (Node2 m ab2 r)) |
|
|
47 |
EQ \<Rightarrow> T\<^sub>i (Node3 l (x,y) m ab2 r) |
|
|
48 |
GT \<Rightarrow> (case cmp x (fst ab2) of
|
|
49 |
LT \<Rightarrow> (case upd x y m of
|
|
50 |
T\<^sub>i m' => T\<^sub>i (Node3 l ab1 m' ab2 r)
|
|
51 |
| Up\<^sub>i m1 ab' m2 => Up\<^sub>i (Node2 l ab1 m1) ab' (Node2 m2 ab2 r)) |
|
|
52 |
EQ \<Rightarrow> T\<^sub>i (Node3 l ab1 m (x,y) r) |
|
|
53 |
GT \<Rightarrow> (case upd x y r of
|
|
54 |
T\<^sub>i r' => T\<^sub>i (Node3 l ab1 m ab2 r')
|
|
55 |
| Up\<^sub>i r1 ab' r2 => Up\<^sub>i (Node2 l ab1 m) ab2 (Node2 r1 ab' r2))))" |
|
|
56 |
"upd x y (Node4 t1 ab1 t2 ab2 t3 ab3 t4) = (case cmp x (fst ab2) of
|
|
57 |
LT \<Rightarrow> (case cmp x (fst ab1) of
|
|
58 |
LT \<Rightarrow> (case upd x y t1 of
|
|
59 |
T\<^sub>i t1' => T\<^sub>i (Node4 t1' ab1 t2 ab2 t3 ab3 t4)
|
|
60 |
| Up\<^sub>i t11 q t12 => Up\<^sub>i (Node2 t11 q t12) ab1 (Node3 t2 ab2 t3 ab3 t4)) |
|
|
61 |
EQ \<Rightarrow> T\<^sub>i (Node4 t1 (x,y) t2 ab2 t3 ab3 t4) |
|
|
62 |
GT \<Rightarrow> (case upd x y t2 of
|
|
63 |
T\<^sub>i t2' => T\<^sub>i (Node4 t1 ab1 t2' ab2 t3 ab3 t4)
|
|
64 |
| Up\<^sub>i t21 q t22 => Up\<^sub>i (Node2 t1 ab1 t21) q (Node3 t22 ab2 t3 ab3 t4))) |
|
|
65 |
EQ \<Rightarrow> T\<^sub>i (Node4 t1 ab1 t2 (x,y) t3 ab3 t4) |
|
|
66 |
GT \<Rightarrow> (case cmp x (fst ab3) of
|
|
67 |
LT \<Rightarrow> (case upd x y t3 of
|
|
68 |
T\<^sub>i t3' \<Rightarrow> T\<^sub>i (Node4 t1 ab1 t2 ab2 t3' ab3 t4)
|
|
69 |
| Up\<^sub>i t31 q t32 => Up\<^sub>i (Node2 t1 ab1 t2) ab2(*q*) (Node3 t31 q t32 ab3 t4)) |
|
|
70 |
EQ \<Rightarrow> T\<^sub>i (Node4 t1 ab1 t2 ab2 t3 (x,y) t4) |
|
|
71 |
GT \<Rightarrow> (case upd x y t4 of
|
|
72 |
T\<^sub>i t4' => T\<^sub>i (Node4 t1 ab1 t2 ab2 t3 ab3 t4')
|
|
73 |
| Up\<^sub>i t41 q t42 => Up\<^sub>i (Node2 t1 ab1 t2) ab2 (Node3 t3 ab3 t41 q t42))))"
|
|
74 |
|
|
75 |
definition update :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) tree234" where
|
|
76 |
"update x y t = tree\<^sub>i(upd x y t)"
|
|
77 |
|
|
78 |
fun del :: "'a::cmp \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) up\<^sub>d" where
|
|
79 |
"del x Leaf = T\<^sub>d Leaf" |
|
|
80 |
"del x (Node2 Leaf ab1 Leaf) = (if x=fst ab1 then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf ab1 Leaf))" |
|
|
81 |
"del x (Node3 Leaf ab1 Leaf ab2 Leaf) = T\<^sub>d(if x=fst ab1 then Node2 Leaf ab2 Leaf
|
|
82 |
else if x=fst ab2 then Node2 Leaf ab1 Leaf else Node3 Leaf ab1 Leaf ab2 Leaf)" |
|
|
83 |
"del x (Node4 Leaf ab1 Leaf ab2 Leaf ab3 Leaf) =
|
|
84 |
T\<^sub>d(if x = fst ab1 then Node3 Leaf ab2 Leaf ab3 Leaf else
|
|
85 |
if x = fst ab2 then Node3 Leaf ab1 Leaf ab3 Leaf else
|
|
86 |
if x = fst ab3 then Node3 Leaf ab1 Leaf ab2 Leaf
|
|
87 |
else Node4 Leaf ab1 Leaf ab2 Leaf ab3 Leaf)" |
|
|
88 |
"del x (Node2 l ab1 r) = (case cmp x (fst ab1) of
|
|
89 |
LT \<Rightarrow> node21 (del x l) ab1 r |
|
|
90 |
GT \<Rightarrow> node22 l ab1 (del x r) |
|
|
91 |
EQ \<Rightarrow> let (ab1',t) = del_min r in node22 l ab1' t)" |
|
|
92 |
"del x (Node3 l ab1 m ab2 r) = (case cmp x (fst ab1) of
|
|
93 |
LT \<Rightarrow> node31 (del x l) ab1 m ab2 r |
|
|
94 |
EQ \<Rightarrow> let (ab1',m') = del_min m in node32 l ab1' m' ab2 r |
|
|
95 |
GT \<Rightarrow> (case cmp x (fst ab2) of
|
|
96 |
LT \<Rightarrow> node32 l ab1 (del x m) ab2 r |
|
|
97 |
EQ \<Rightarrow> let (ab2',r') = del_min r in node33 l ab1 m ab2' r' |
|
|
98 |
GT \<Rightarrow> node33 l ab1 m ab2 (del x r)))" |
|
|
99 |
"del x (Node4 t1 ab1 t2 ab2 t3 ab3 t4) = (case cmp x (fst ab2) of
|
|
100 |
LT \<Rightarrow> (case cmp x (fst ab1) of
|
|
101 |
LT \<Rightarrow> node41 (del x t1) ab1 t2 ab2 t3 ab3 t4 |
|
|
102 |
EQ \<Rightarrow> let (ab',t2') = del_min t2 in node42 t1 ab' t2' ab2 t3 ab3 t4 |
|
|
103 |
GT \<Rightarrow> node42 t1 ab1 (del x t2) ab2 t3 ab3 t4) |
|
|
104 |
EQ \<Rightarrow> let (ab',t3') = del_min t3 in node43 t1 ab1 t2 ab' t3' ab3 t4 |
|
|
105 |
GT \<Rightarrow> (case cmp x (fst ab3) of
|
|
106 |
LT \<Rightarrow> node43 t1 ab1 t2 ab2 (del x t3) ab3 t4 |
|
|
107 |
EQ \<Rightarrow> let (ab',t4') = del_min t4 in node44 t1 ab1 t2 ab2 t3 ab' t4' |
|
|
108 |
GT \<Rightarrow> node44 t1 ab1 t2 ab2 t3 ab3 (del x t4)))"
|
|
109 |
|
|
110 |
definition delete :: "'a::cmp \<Rightarrow> ('a*'b) tree234 \<Rightarrow> ('a*'b) tree234" where
|
|
111 |
"delete x t = tree\<^sub>d(del x t)"
|
|
112 |
|
|
113 |
|
|
114 |
subsection "Functional correctness"
|
|
115 |
|
|
116 |
lemma lookup: "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
|
|
117 |
by (induction t) (auto simp: map_of_simps split: option.split)
|
|
118 |
|
|
119 |
|
|
120 |
lemma inorder_upd:
|
|
121 |
"sorted1(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(upd a b t)) = upd_list a b (inorder t)"
|
|
122 |
by(induction t)
|
|
123 |
(auto simp: upd_list_simps, auto simp: upd_list_simps split: up\<^sub>i.splits)
|
|
124 |
|
|
125 |
lemma inorder_update:
|
|
126 |
"sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)"
|
|
127 |
by(simp add: update_def inorder_upd)
|
|
128 |
|
|
129 |
|
|
130 |
lemma inorder_del: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
|
|
131 |
inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
|
|
132 |
by(induction t rule: del.induct)
|
|
133 |
((auto simp: del_list_simps inorder_nodes del_minD split: prod.splits)[1])+
|
|
134 |
(* 200 secs (2015) *)
|
|
135 |
|
|
136 |
lemma inorder_delete: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
|
|
137 |
inorder(delete x t) = del_list x (inorder t)"
|
|
138 |
by(simp add: delete_def inorder_del)
|
|
139 |
|
|
140 |
|
|
141 |
subsection \<open>Balancedness\<close>
|
|
142 |
|
|
143 |
lemma bal_upd: "bal t \<Longrightarrow> bal (tree\<^sub>i(upd x y t)) \<and> height(upd x y t) = height t"
|
|
144 |
by (induct t) (auto, auto split: up\<^sub>i.split) (* 20 secs (2015) *)
|
|
145 |
|
|
146 |
lemma bal_update: "bal t \<Longrightarrow> bal (update x y t)"
|
|
147 |
by (simp add: update_def bal_upd)
|
|
148 |
|
|
149 |
|
|
150 |
lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
|
|
151 |
by(induction x t rule: del.induct)
|
|
152 |
(auto simp add: heights height_del_min split: prod.split)
|
|
153 |
(* 20 secs (2015) *)
|
|
154 |
|
|
155 |
lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
|
|
156 |
by(induction x t rule: del.induct)
|
|
157 |
(auto simp: bals bal_del_min height_del height_del_min split: prod.split)
|
|
158 |
(* 100 secs (2015) *)
|
|
159 |
|
|
160 |
corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
|
|
161 |
by(simp add: delete_def bal_tree\<^sub>d_del)
|
|
162 |
|
|
163 |
|
|
164 |
subsection \<open>Overall Correctness\<close>
|
|
165 |
|
|
166 |
interpretation T234_Map: Map_by_Ordered
|
|
167 |
where empty = Leaf and lookup = lookup and update = update and delete = delete
|
61686
|
168 |
and inorder = inorder and inv = bal
|
61640
|
169 |
proof (standard, goal_cases)
|
|
170 |
case 2 thus ?case by(simp add: lookup)
|
|
171 |
next
|
|
172 |
case 3 thus ?case by(simp add: inorder_update)
|
|
173 |
next
|
|
174 |
case 4 thus ?case by(simp add: inorder_delete)
|
|
175 |
next
|
|
176 |
case 6 thus ?case by(simp add: bal_update)
|
|
177 |
next
|
|
178 |
case 7 thus ?case by(simp add: bal_delete)
|
|
179 |
qed simp+
|
|
180 |
|
|
181 |
end
|