61789
|
1 |
(* Author: Tobias Nipkow *)
|
|
2 |
|
62130
|
3 |
section \<open>1-2 Brother Tree Implementation of Maps\<close>
|
61789
|
4 |
|
|
5 |
theory Brother12_Map
|
|
6 |
imports
|
|
7 |
Brother12_Set
|
|
8 |
Map_by_Ordered
|
|
9 |
begin
|
|
10 |
|
|
11 |
fun lookup :: "('a \<times> 'b) bro \<Rightarrow> 'a::cmp \<Rightarrow> 'b option" where
|
|
12 |
"lookup N0 x = None" |
|
|
13 |
"lookup (N1 t) x = lookup t x" |
|
|
14 |
"lookup (N2 l (a,b) r) x =
|
|
15 |
(case cmp x a of
|
|
16 |
LT \<Rightarrow> lookup l x |
|
|
17 |
EQ \<Rightarrow> Some b |
|
|
18 |
GT \<Rightarrow> lookup r x)"
|
|
19 |
|
|
20 |
locale update = insert
|
|
21 |
begin
|
|
22 |
|
|
23 |
fun upd :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where
|
|
24 |
"upd x y N0 = L2 (x,y)" |
|
|
25 |
"upd x y (N1 t) = n1 (upd x y t)" |
|
|
26 |
"upd x y (N2 l (a,b) r) =
|
|
27 |
(case cmp x a of
|
|
28 |
LT \<Rightarrow> n2 (upd x y l) (a,b) r |
|
|
29 |
EQ \<Rightarrow> N2 l (a,y) r |
|
|
30 |
GT \<Rightarrow> n2 l (a,b) (upd x y r))"
|
|
31 |
|
|
32 |
definition update :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where
|
|
33 |
"update x y t = tree(upd x y t)"
|
|
34 |
|
|
35 |
end
|
|
36 |
|
|
37 |
context delete
|
|
38 |
begin
|
|
39 |
|
|
40 |
fun del :: "'a::cmp \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where
|
|
41 |
"del _ N0 = N0" |
|
|
42 |
"del x (N1 t) = N1 (del x t)" |
|
|
43 |
"del x (N2 l (a,b) r) =
|
|
44 |
(case cmp x a of
|
|
45 |
LT \<Rightarrow> n2 (del x l) (a,b) r |
|
|
46 |
GT \<Rightarrow> n2 l (a,b) (del x r) |
|
|
47 |
EQ \<Rightarrow> (case del_min r of
|
|
48 |
None \<Rightarrow> N1 l |
|
|
49 |
Some (ab, r') \<Rightarrow> n2 l ab r'))"
|
|
50 |
|
|
51 |
definition delete :: "'a::cmp \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where
|
|
52 |
"delete a t = tree (del a t)"
|
|
53 |
|
|
54 |
end
|
|
55 |
|
|
56 |
subsection "Functional Correctness Proofs"
|
|
57 |
|
|
58 |
subsubsection "Proofs for lookup"
|
|
59 |
|
|
60 |
lemma lookup_map_of: "t \<in> T h \<Longrightarrow>
|
|
61 |
sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
|
|
62 |
by(induction h arbitrary: t) (auto simp: map_of_simps split: option.splits)
|
|
63 |
|
|
64 |
subsubsection "Proofs for update"
|
|
65 |
|
|
66 |
context update
|
|
67 |
begin
|
|
68 |
|
|
69 |
lemma inorder_upd: "t \<in> T h \<Longrightarrow>
|
|
70 |
sorted1(inorder t) \<Longrightarrow> inorder(upd x y t) = upd_list x y (inorder t)"
|
|
71 |
by(induction h arbitrary: t) (auto simp: upd_list_simps inorder_n1 inorder_n2)
|
|
72 |
|
|
73 |
lemma inorder_update: "t \<in> T h \<Longrightarrow>
|
|
74 |
sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
|
|
75 |
by(simp add: update_def inorder_upd inorder_tree)
|
|
76 |
|
|
77 |
end
|
|
78 |
|
|
79 |
subsubsection \<open>Proofs for deletion\<close>
|
|
80 |
|
|
81 |
context delete
|
|
82 |
begin
|
|
83 |
|
|
84 |
lemma inorder_del:
|
61792
|
85 |
"t \<in> T h \<Longrightarrow> sorted1(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)"
|
|
86 |
by(induction h arbitrary: t) (auto simp: del_list_simps inorder_n2
|
|
87 |
inorder_del_min[OF UnI1] inorder_del_min[OF UnI2] split: option.splits)
|
|
88 |
|
|
89 |
lemma inorder_delete:
|
|
90 |
"t \<in> T h \<Longrightarrow> sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
|
|
91 |
by(simp add: delete_def inorder_del inorder_tree)
|
61789
|
92 |
|
|
93 |
end
|
|
94 |
|
|
95 |
|
|
96 |
subsection \<open>Invariant Proofs\<close>
|
|
97 |
|
|
98 |
subsubsection \<open>Proofs for update\<close>
|
|
99 |
|
|
100 |
context update
|
|
101 |
begin
|
|
102 |
|
|
103 |
lemma upd_type:
|
|
104 |
"(t \<in> B h \<longrightarrow> upd x y t \<in> Bp h) \<and> (t \<in> U h \<longrightarrow> upd x y t \<in> T h)"
|
|
105 |
apply(induction h arbitrary: t)
|
|
106 |
apply (simp)
|
|
107 |
apply (fastforce simp: Bp_if_B n2_type dest: n1_type)
|
|
108 |
done
|
|
109 |
|
|
110 |
lemma update_type:
|
61809
|
111 |
"t \<in> B h \<Longrightarrow> update x y t \<in> B h \<union> B (Suc h)"
|
|
112 |
unfolding update_def by (metis upd_type tree_type)
|
61789
|
113 |
|
|
114 |
end
|
|
115 |
|
|
116 |
subsubsection "Proofs for deletion"
|
|
117 |
|
|
118 |
context delete
|
|
119 |
begin
|
|
120 |
|
|
121 |
lemma del_type:
|
|
122 |
"t \<in> B h \<Longrightarrow> del x t \<in> T h"
|
|
123 |
"t \<in> U h \<Longrightarrow> del x t \<in> Um h"
|
|
124 |
proof (induction h arbitrary: x t)
|
|
125 |
case (Suc h)
|
|
126 |
{ case 1
|
|
127 |
then obtain l a b r where [simp]: "t = N2 l (a,b) r" and
|
|
128 |
lr: "l \<in> T h" "r \<in> T h" "l \<in> B h \<or> r \<in> B h" by auto
|
|
129 |
{ assume "x < a"
|
|
130 |
have ?case
|
|
131 |
proof cases
|
|
132 |
assume "l \<in> B h"
|
|
133 |
from n2_type3[OF Suc.IH(1)[OF this] lr(2)]
|
|
134 |
show ?thesis using `x<a` by(simp)
|
|
135 |
next
|
|
136 |
assume "l \<notin> B h"
|
|
137 |
hence "l \<in> U h" "r \<in> B h" using lr by auto
|
|
138 |
from n2_type1[OF Suc.IH(2)[OF this(1)] this(2)]
|
|
139 |
show ?thesis using `x<a` by(simp)
|
|
140 |
qed
|
|
141 |
} moreover
|
|
142 |
{ assume "x > a"
|
|
143 |
have ?case
|
|
144 |
proof cases
|
|
145 |
assume "r \<in> B h"
|
|
146 |
from n2_type3[OF lr(1) Suc.IH(1)[OF this]]
|
|
147 |
show ?thesis using `x>a` by(simp)
|
|
148 |
next
|
|
149 |
assume "r \<notin> B h"
|
|
150 |
hence "l \<in> B h" "r \<in> U h" using lr by auto
|
|
151 |
from n2_type2[OF this(1) Suc.IH(2)[OF this(2)]]
|
|
152 |
show ?thesis using `x>a` by(simp)
|
|
153 |
qed
|
|
154 |
} moreover
|
|
155 |
{ assume [simp]: "x=a"
|
|
156 |
have ?case
|
|
157 |
proof (cases "del_min r")
|
|
158 |
case None
|
|
159 |
show ?thesis
|
|
160 |
proof cases
|
|
161 |
assume "r \<in> B h"
|
|
162 |
with del_minNoneN0[OF this None] lr show ?thesis by(simp)
|
|
163 |
next
|
|
164 |
assume "r \<notin> B h"
|
|
165 |
hence "r \<in> U h" using lr by auto
|
|
166 |
with del_minNoneN1[OF this None] lr(3) show ?thesis by (simp)
|
|
167 |
qed
|
|
168 |
next
|
|
169 |
case [simp]: (Some br')
|
|
170 |
obtain b r' where [simp]: "br' = (b,r')" by fastforce
|
|
171 |
show ?thesis
|
|
172 |
proof cases
|
|
173 |
assume "r \<in> B h"
|
|
174 |
from del_min_type(1)[OF this] n2_type3[OF lr(1)]
|
|
175 |
show ?thesis by simp
|
|
176 |
next
|
|
177 |
assume "r \<notin> B h"
|
|
178 |
hence "l \<in> B h" and "r \<in> U h" using lr by auto
|
|
179 |
from del_min_type(2)[OF this(2)] n2_type2[OF this(1)]
|
|
180 |
show ?thesis by simp
|
|
181 |
qed
|
|
182 |
qed
|
|
183 |
} ultimately show ?case by auto
|
|
184 |
}
|
|
185 |
{ case 2 with Suc.IH(1) show ?case by auto }
|
|
186 |
qed auto
|
|
187 |
|
|
188 |
lemma delete_type:
|
61809
|
189 |
"t \<in> B h \<Longrightarrow> delete x t \<in> B h \<union> B(h-1)"
|
61789
|
190 |
unfolding delete_def
|
61809
|
191 |
by (cases h) (simp, metis del_type(1) tree_type Suc_eq_plus1 diff_Suc_1)
|
61789
|
192 |
|
|
193 |
end
|
|
194 |
|
|
195 |
subsection "Overall correctness"
|
|
196 |
|
|
197 |
interpretation Map_by_Ordered
|
|
198 |
where empty = N0 and lookup = lookup and update = update.update
|
61809
|
199 |
and delete = delete.delete and inorder = inorder and inv = "\<lambda>t. \<exists>h. t \<in> B h"
|
61789
|
200 |
proof (standard, goal_cases)
|
|
201 |
case 2 thus ?case by(auto intro!: lookup_map_of)
|
|
202 |
next
|
|
203 |
case 3 thus ?case by(auto intro!: update.inorder_update)
|
|
204 |
next
|
61792
|
205 |
case 4 thus ?case by(auto intro!: delete.inorder_delete)
|
61789
|
206 |
next
|
|
207 |
case 6 thus ?case using update.update_type by (metis Un_iff)
|
|
208 |
next
|
|
209 |
case 7 thus ?case using delete.delete_type by blast
|
|
210 |
qed auto
|
|
211 |
|
|
212 |
end
|