61640
|
1 |
(* Author: Tobias Nipkow *)
|
|
2 |
|
|
3 |
section \<open>A 2-3 Tree Implementation of Maps\<close>
|
|
4 |
|
|
5 |
theory Tree23_Map
|
|
6 |
imports
|
|
7 |
Tree23_Set
|
|
8 |
Map_by_Ordered
|
|
9 |
begin
|
|
10 |
|
|
11 |
fun lookup :: "('a::cmp * 'b) tree23 \<Rightarrow> 'a \<Rightarrow> 'b option" where
|
|
12 |
"lookup Leaf x = None" |
|
|
13 |
"lookup (Node2 l (a,b) r) x = (case cmp x a of
|
|
14 |
LT \<Rightarrow> lookup l x |
|
|
15 |
GT \<Rightarrow> lookup r x |
|
|
16 |
EQ \<Rightarrow> Some b)" |
|
|
17 |
"lookup (Node3 l (a1,b1) m (a2,b2) r) x = (case cmp x a1 of
|
|
18 |
LT \<Rightarrow> lookup l x |
|
|
19 |
EQ \<Rightarrow> Some b1 |
|
|
20 |
GT \<Rightarrow> (case cmp x a2 of
|
|
21 |
LT \<Rightarrow> lookup m x |
|
|
22 |
EQ \<Rightarrow> Some b2 |
|
|
23 |
GT \<Rightarrow> lookup r x))"
|
|
24 |
|
|
25 |
fun upd :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) up\<^sub>i" where
|
|
26 |
"upd x y Leaf = Up\<^sub>i Leaf (x,y) Leaf" |
|
|
27 |
"upd x y (Node2 l ab r) = (case cmp x (fst ab) of
|
|
28 |
LT \<Rightarrow> (case upd x y l of
|
|
29 |
T\<^sub>i l' => T\<^sub>i (Node2 l' ab r)
|
|
30 |
| Up\<^sub>i l1 ab' l2 => T\<^sub>i (Node3 l1 ab' l2 ab r)) |
|
|
31 |
EQ \<Rightarrow> T\<^sub>i (Node2 l (x,y) r) |
|
|
32 |
GT \<Rightarrow> (case upd x y r of
|
|
33 |
T\<^sub>i r' => T\<^sub>i (Node2 l ab r')
|
|
34 |
| Up\<^sub>i r1 ab' r2 => T\<^sub>i (Node3 l ab r1 ab' r2)))" |
|
|
35 |
"upd x y (Node3 l ab1 m ab2 r) = (case cmp x (fst ab1) of
|
|
36 |
LT \<Rightarrow> (case upd x y l of
|
|
37 |
T\<^sub>i l' => T\<^sub>i (Node3 l' ab1 m ab2 r)
|
|
38 |
| Up\<^sub>i l1 ab' l2 => Up\<^sub>i (Node2 l1 ab' l2) ab1 (Node2 m ab2 r)) |
|
|
39 |
EQ \<Rightarrow> T\<^sub>i (Node3 l (x,y) m ab2 r) |
|
|
40 |
GT \<Rightarrow> (case cmp x (fst ab2) of
|
|
41 |
LT \<Rightarrow> (case upd x y m of
|
|
42 |
T\<^sub>i m' => T\<^sub>i (Node3 l ab1 m' ab2 r)
|
|
43 |
| Up\<^sub>i m1 ab' m2 => Up\<^sub>i (Node2 l ab1 m1) ab' (Node2 m2 ab2 r)) |
|
|
44 |
EQ \<Rightarrow> T\<^sub>i (Node3 l ab1 m (x,y) r) |
|
|
45 |
GT \<Rightarrow> (case upd x y r of
|
|
46 |
T\<^sub>i r' => T\<^sub>i (Node3 l ab1 m ab2 r')
|
|
47 |
| Up\<^sub>i r1 ab' r2 => Up\<^sub>i (Node2 l ab1 m) ab2 (Node2 r1 ab' r2))))"
|
|
48 |
|
|
49 |
definition update :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) tree23" where
|
|
50 |
"update a b t = tree\<^sub>i(upd a b t)"
|
|
51 |
|
|
52 |
fun del :: "'a::cmp \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) up\<^sub>d" where
|
|
53 |
"del x Leaf = T\<^sub>d Leaf" |
|
|
54 |
"del x (Node2 Leaf ab1 Leaf) = (if x=fst ab1 then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf ab1 Leaf))" |
|
|
55 |
"del x (Node3 Leaf ab1 Leaf ab2 Leaf) = T\<^sub>d(if x=fst ab1 then Node2 Leaf ab2 Leaf
|
|
56 |
else if x=fst ab2 then Node2 Leaf ab1 Leaf else Node3 Leaf ab1 Leaf ab2 Leaf)" |
|
|
57 |
"del x (Node2 l ab1 r) = (case cmp x (fst ab1) of
|
|
58 |
LT \<Rightarrow> node21 (del x l) ab1 r |
|
|
59 |
GT \<Rightarrow> node22 l ab1 (del x r) |
|
|
60 |
EQ \<Rightarrow> let (ab1',t) = del_min r in node22 l ab1' t)" |
|
|
61 |
"del x (Node3 l ab1 m ab2 r) = (case cmp x (fst ab1) of
|
|
62 |
LT \<Rightarrow> node31 (del x l) ab1 m ab2 r |
|
|
63 |
EQ \<Rightarrow> let (ab1',m') = del_min m in node32 l ab1' m' ab2 r |
|
|
64 |
GT \<Rightarrow> (case cmp x (fst ab2) of
|
|
65 |
LT \<Rightarrow> node32 l ab1 (del x m) ab2 r |
|
|
66 |
EQ \<Rightarrow> let (ab2',r') = del_min r in node33 l ab1 m ab2' r' |
|
|
67 |
GT \<Rightarrow> node33 l ab1 m ab2 (del x r)))"
|
|
68 |
|
|
69 |
definition delete :: "'a::cmp \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) tree23" where
|
|
70 |
"delete x t = tree\<^sub>d(del x t)"
|
|
71 |
|
|
72 |
|
|
73 |
subsection \<open>Functional Correctness\<close>
|
|
74 |
|
|
75 |
lemma lookup: "sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
|
|
76 |
by (induction t) (auto simp: map_of_simps split: option.split)
|
|
77 |
|
|
78 |
|
|
79 |
lemma inorder_upd:
|
61789
|
80 |
"sorted1(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(upd x y t)) = upd_list x y (inorder t)"
|
61640
|
81 |
by(induction t) (auto simp: upd_list_simps split: up\<^sub>i.splits)
|
|
82 |
|
|
83 |
corollary inorder_update:
|
61789
|
84 |
"sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
|
61640
|
85 |
by(simp add: update_def inorder_upd)
|
|
86 |
|
|
87 |
|
|
88 |
lemma inorder_del: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
|
|
89 |
inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
|
|
90 |
by(induction t rule: del.induct)
|
|
91 |
(auto simp: del_list_simps inorder_nodes del_minD split: prod.splits)
|
|
92 |
|
|
93 |
corollary inorder_delete: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow>
|
|
94 |
inorder(delete x t) = del_list x (inorder t)"
|
|
95 |
by(simp add: delete_def inorder_del)
|
|
96 |
|
|
97 |
|
|
98 |
subsection \<open>Balancedness\<close>
|
|
99 |
|
61789
|
100 |
lemma bal_upd: "bal t \<Longrightarrow> bal (tree\<^sub>i(upd x y t)) \<and> height(upd x y t) = height t"
|
61640
|
101 |
by (induct t) (auto split: up\<^sub>i.split)(* 16 secs in 2015 *)
|
|
102 |
|
61789
|
103 |
corollary bal_update: "bal t \<Longrightarrow> bal (update x y t)"
|
61640
|
104 |
by (simp add: update_def bal_upd)
|
|
105 |
|
|
106 |
|
|
107 |
lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
|
|
108 |
by(induction x t rule: del.induct)
|
|
109 |
(auto simp add: heights max_def height_del_min split: prod.split)
|
|
110 |
|
|
111 |
lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
|
|
112 |
by(induction x t rule: del.induct)
|
|
113 |
(auto simp: bals bal_del_min height_del height_del_min split: prod.split)
|
|
114 |
|
|
115 |
corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
|
|
116 |
by(simp add: delete_def bal_tree\<^sub>d_del)
|
|
117 |
|
|
118 |
|
|
119 |
subsection \<open>Overall Correctness\<close>
|
|
120 |
|
|
121 |
interpretation T23_Map: Map_by_Ordered
|
|
122 |
where empty = Leaf and lookup = lookup and update = update and delete = delete
|
61686
|
123 |
and inorder = inorder and inv = bal
|
61640
|
124 |
proof (standard, goal_cases)
|
|
125 |
case 2 thus ?case by(simp add: lookup)
|
|
126 |
next
|
|
127 |
case 3 thus ?case by(simp add: inorder_update)
|
|
128 |
next
|
|
129 |
case 4 thus ?case by(simp add: inorder_delete)
|
|
130 |
next
|
|
131 |
case 6 thus ?case by(simp add: bal_update)
|
|
132 |
next
|
|
133 |
case 7 thus ?case by(simp add: bal_delete)
|
|
134 |
qed simp+
|
|
135 |
|
|
136 |
end
|