70250
|
1 |
(* Author: Tobias Nipkow *)
|
|
2 |
|
|
3 |
section "Binary Tries and Patricia Tries"
|
|
4 |
|
|
5 |
theory Tries_Binary
|
|
6 |
imports Set_Specs
|
|
7 |
begin
|
|
8 |
|
|
9 |
hide_const (open) insert
|
|
10 |
|
|
11 |
declare Let_def[simp]
|
|
12 |
|
|
13 |
fun sel2 :: "bool \<Rightarrow> 'a * 'a \<Rightarrow> 'a" where
|
|
14 |
"sel2 b (a1,a2) = (if b then a2 else a1)"
|
|
15 |
|
|
16 |
fun mod2 :: "('a \<Rightarrow> 'a) \<Rightarrow> bool \<Rightarrow> 'a * 'a \<Rightarrow> 'a * 'a" where
|
|
17 |
"mod2 f b (a1,a2) = (if b then (a1,f a2) else (f a1,a2))"
|
|
18 |
|
|
19 |
|
|
20 |
subsection "Trie"
|
|
21 |
|
|
22 |
datatype trie = Lf | Nd bool "trie * trie"
|
|
23 |
|
70267
|
24 |
definition empty :: trie where
|
|
25 |
[simp]: "empty = Lf"
|
|
26 |
|
70250
|
27 |
fun isin :: "trie \<Rightarrow> bool list \<Rightarrow> bool" where
|
|
28 |
"isin Lf ks = False" |
|
|
29 |
"isin (Nd b lr) ks =
|
|
30 |
(case ks of
|
|
31 |
[] \<Rightarrow> b |
|
|
32 |
k#ks \<Rightarrow> isin (sel2 k lr) ks)"
|
|
33 |
|
|
34 |
fun insert :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
|
|
35 |
"insert [] Lf = Nd True (Lf,Lf)" |
|
|
36 |
"insert [] (Nd b lr) = Nd True lr" |
|
|
37 |
"insert (k#ks) Lf = Nd False (mod2 (insert ks) k (Lf,Lf))" |
|
|
38 |
"insert (k#ks) (Nd b lr) = Nd b (mod2 (insert ks) k lr)"
|
|
39 |
|
70267
|
40 |
lemma isin_insert: "isin (insert xs t) ys = (xs = ys \<or> isin t ys)"
|
|
41 |
apply(induction xs t arbitrary: ys rule: insert.induct)
|
70250
|
42 |
apply (auto split: list.splits if_splits)
|
|
43 |
done
|
|
44 |
|
|
45 |
text \<open>A simple implementation of delete; does not shrink the trie!\<close>
|
|
46 |
|
|
47 |
fun delete0 :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
|
|
48 |
"delete0 ks Lf = Lf" |
|
|
49 |
"delete0 ks (Nd b lr) =
|
|
50 |
(case ks of
|
|
51 |
[] \<Rightarrow> Nd False lr |
|
|
52 |
k#ks' \<Rightarrow> Nd b (mod2 (delete0 ks') k lr))"
|
|
53 |
|
|
54 |
lemma isin_delete0: "isin (delete0 as t) bs = (as \<noteq> bs \<and> isin t bs)"
|
|
55 |
apply(induction as t arbitrary: bs rule: delete0.induct)
|
|
56 |
apply (auto split: list.splits if_splits)
|
|
57 |
done
|
|
58 |
|
|
59 |
text \<open>Now deletion with shrinking:\<close>
|
|
60 |
|
|
61 |
fun node :: "bool \<Rightarrow> trie * trie \<Rightarrow> trie" where
|
|
62 |
"node b lr = (if \<not> b \<and> lr = (Lf,Lf) then Lf else Nd b lr)"
|
|
63 |
|
|
64 |
fun delete :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
|
|
65 |
"delete ks Lf = Lf" |
|
|
66 |
"delete ks (Nd b lr) =
|
|
67 |
(case ks of
|
|
68 |
[] \<Rightarrow> node False lr |
|
|
69 |
k#ks' \<Rightarrow> node b (mod2 (delete ks') k lr))"
|
|
70 |
|
70267
|
71 |
lemma isin_delete: "isin (delete xs t) ys = (xs \<noteq> ys \<and> isin t ys)"
|
|
72 |
apply(induction xs t arbitrary: ys rule: delete.induct)
|
70250
|
73 |
apply simp
|
|
74 |
apply (auto split: list.splits if_splits)
|
|
75 |
apply (metis isin.simps(1))
|
|
76 |
apply (metis isin.simps(1))
|
|
77 |
done
|
|
78 |
|
|
79 |
definition set_trie :: "trie \<Rightarrow> bool list set" where
|
|
80 |
"set_trie t = {xs. isin t xs}"
|
|
81 |
|
70267
|
82 |
lemma set_trie_empty: "set_trie empty = {}"
|
|
83 |
by(simp add: set_trie_def)
|
|
84 |
|
|
85 |
lemma set_trie_isin: "isin t xs = (xs \<in> set_trie t)"
|
|
86 |
by(simp add: set_trie_def)
|
|
87 |
|
70250
|
88 |
lemma set_trie_insert: "set_trie(insert xs t) = set_trie t \<union> {xs}"
|
|
89 |
by(auto simp add: isin_insert set_trie_def)
|
|
90 |
|
70267
|
91 |
lemma set_trie_delete: "set_trie(delete xs t) = set_trie t - {xs}"
|
|
92 |
by(auto simp add: isin_delete set_trie_def)
|
|
93 |
|
70250
|
94 |
interpretation S: Set
|
70267
|
95 |
where empty = empty and isin = isin and insert = insert and delete = delete
|
70250
|
96 |
and set = set_trie and invar = "\<lambda>t. True"
|
|
97 |
proof (standard, goal_cases)
|
70267
|
98 |
case 1 show ?case by (rule set_trie_empty)
|
70250
|
99 |
next
|
70267
|
100 |
case 2 show ?case by(rule set_trie_isin)
|
70250
|
101 |
next
|
|
102 |
case 3 thus ?case by(auto simp: set_trie_insert)
|
|
103 |
next
|
70267
|
104 |
case 4 show ?case by(rule set_trie_delete)
|
70250
|
105 |
qed (rule TrueI)+
|
|
106 |
|
|
107 |
|
|
108 |
subsection "Patricia Trie"
|
|
109 |
|
70268
|
110 |
datatype trieP = LfP | NdP "bool list" bool "trieP * trieP"
|
70250
|
111 |
|
70268
|
112 |
fun isinP :: "trieP \<Rightarrow> bool list \<Rightarrow> bool" where
|
70250
|
113 |
"isinP LfP ks = False" |
|
|
114 |
"isinP (NdP ps b lr) ks =
|
|
115 |
(let n = length ps in
|
|
116 |
if ps = take n ks
|
|
117 |
then case drop n ks of [] \<Rightarrow> b | k#ks' \<Rightarrow> isinP (sel2 k lr) ks'
|
|
118 |
else False)"
|
|
119 |
|
70268
|
120 |
definition emptyP :: trieP where
|
|
121 |
[simp]: "emptyP = LfP"
|
|
122 |
|
70250
|
123 |
fun split where
|
|
124 |
"split [] ys = ([],[],ys)" |
|
|
125 |
"split xs [] = ([],xs,[])" |
|
|
126 |
"split (x#xs) (y#ys) =
|
|
127 |
(if x\<noteq>y then ([],x#xs,y#ys)
|
|
128 |
else let (ps,xs',ys') = split xs ys in (x#ps,xs',ys'))"
|
|
129 |
|
|
130 |
|
|
131 |
lemma mod2_cong[fundef_cong]:
|
|
132 |
"\<lbrakk> lr = lr'; k = k'; \<And>a b. lr'=(a,b) \<Longrightarrow> f (a) = f' (a) ; \<And>a b. lr'=(a,b) \<Longrightarrow> f (b) = f' (b) \<rbrakk>
|
|
133 |
\<Longrightarrow> mod2 f k lr= mod2 f' k' lr'"
|
|
134 |
by(cases lr, cases lr', auto)
|
|
135 |
|
70268
|
136 |
|
|
137 |
fun insertP :: "bool list \<Rightarrow> trieP \<Rightarrow> trieP" where
|
70250
|
138 |
"insertP ks LfP = NdP ks True (LfP,LfP)" |
|
|
139 |
"insertP ks (NdP ps b lr) =
|
|
140 |
(case split ks ps of
|
|
141 |
(qs,k#ks',p#ps') \<Rightarrow>
|
|
142 |
let tp = NdP ps' b lr; tk = NdP ks' True (LfP,LfP) in
|
|
143 |
NdP qs False (if k then (tp,tk) else (tk,tp)) |
|
|
144 |
(qs,k#ks',[]) \<Rightarrow>
|
|
145 |
NdP ps b (mod2 (insertP ks') k lr) |
|
|
146 |
(qs,[],p#ps') \<Rightarrow>
|
|
147 |
let t = NdP ps' b lr in
|
|
148 |
NdP qs True (if p then (LfP,t) else (t,LfP)) |
|
|
149 |
(qs,[],[]) \<Rightarrow> NdP ps True lr)"
|
|
150 |
|
|
151 |
|
70268
|
152 |
fun nodeP :: "bool list \<Rightarrow> bool \<Rightarrow> trieP * trieP \<Rightarrow> trieP" where
|
70250
|
153 |
"nodeP ps b lr = (if \<not> b \<and> lr = (LfP,LfP) then LfP else NdP ps b lr)"
|
|
154 |
|
70268
|
155 |
fun deleteP :: "bool list \<Rightarrow> trieP \<Rightarrow> trieP" where
|
70250
|
156 |
"deleteP ks LfP = LfP" |
|
|
157 |
"deleteP ks (NdP ps b lr) =
|
|
158 |
(case split ks ps of
|
|
159 |
(qs,ks',p#ps') \<Rightarrow> NdP ps b lr |
|
|
160 |
(qs,k#ks',[]) \<Rightarrow> nodeP ps b (mod2 (deleteP ks') k lr) |
|
|
161 |
(qs,[],[]) \<Rightarrow> nodeP ps False lr)"
|
|
162 |
|
|
163 |
|
|
164 |
subsubsection \<open>Functional Correctness\<close>
|
|
165 |
|
70268
|
166 |
text \<open>First step: @{typ trieP} implements @{typ trie} via the abstraction function \<open>abs_trieP\<close>:\<close>
|
70250
|
167 |
|
|
168 |
fun prefix_trie :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
|
|
169 |
"prefix_trie [] t = t" |
|
|
170 |
"prefix_trie (k#ks) t =
|
|
171 |
(let t' = prefix_trie ks t in Nd False (if k then (Lf,t') else (t',Lf)))"
|
|
172 |
|
70268
|
173 |
fun abs_trieP :: "trieP \<Rightarrow> trie" where
|
|
174 |
"abs_trieP LfP = Lf" |
|
|
175 |
"abs_trieP (NdP ps b (l,r)) = prefix_trie ps (Nd b (abs_trieP l, abs_trieP r))"
|
70250
|
176 |
|
|
177 |
|
|
178 |
text \<open>Correctness of @{const isinP}:\<close>
|
|
179 |
|
|
180 |
lemma isin_prefix_trie:
|
|
181 |
"isin (prefix_trie ps t) ks
|
|
182 |
= (ps = take (length ps) ks \<and> isin t (drop (length ps) ks))"
|
|
183 |
apply(induction ps arbitrary: ks)
|
|
184 |
apply(auto split: list.split)
|
|
185 |
done
|
|
186 |
|
70269
|
187 |
lemma abs_trieP_isinP:
|
70268
|
188 |
"isinP t ks = isin (abs_trieP t) ks"
|
|
189 |
apply(induction t arbitrary: ks rule: abs_trieP.induct)
|
70250
|
190 |
apply(auto simp: isin_prefix_trie split: list.split)
|
|
191 |
done
|
|
192 |
|
|
193 |
|
|
194 |
text \<open>Correctness of @{const insertP}:\<close>
|
|
195 |
|
|
196 |
lemma prefix_trie_Lfs: "prefix_trie ks (Nd True (Lf,Lf)) = insert ks Lf"
|
|
197 |
apply(induction ks)
|
|
198 |
apply auto
|
|
199 |
done
|
|
200 |
|
|
201 |
lemma insert_prefix_trie_same:
|
|
202 |
"insert ps (prefix_trie ps (Nd b lr)) = prefix_trie ps (Nd True lr)"
|
|
203 |
apply(induction ps)
|
|
204 |
apply auto
|
|
205 |
done
|
|
206 |
|
|
207 |
lemma insert_append: "insert (ks @ ks') (prefix_trie ks t) = prefix_trie ks (insert ks' t)"
|
|
208 |
apply(induction ks)
|
|
209 |
apply auto
|
|
210 |
done
|
|
211 |
|
|
212 |
lemma prefix_trie_append: "prefix_trie (ps @ qs) t = prefix_trie ps (prefix_trie qs t)"
|
|
213 |
apply(induction ps)
|
|
214 |
apply auto
|
|
215 |
done
|
|
216 |
|
|
217 |
lemma split_if: "split ks ps = (qs, ks', ps') \<Longrightarrow>
|
|
218 |
ks = qs @ ks' \<and> ps = qs @ ps' \<and> (ks' \<noteq> [] \<and> ps' \<noteq> [] \<longrightarrow> hd ks' \<noteq> hd ps')"
|
|
219 |
apply(induction ks ps arbitrary: qs ks' ps' rule: split.induct)
|
|
220 |
apply(auto split: prod.splits if_splits)
|
|
221 |
done
|
|
222 |
|
70268
|
223 |
lemma abs_trieP_insertP:
|
|
224 |
"abs_trieP (insertP ks t) = insert ks (abs_trieP t)"
|
70250
|
225 |
apply(induction t arbitrary: ks)
|
|
226 |
apply(auto simp: prefix_trie_Lfs insert_prefix_trie_same insert_append prefix_trie_append
|
|
227 |
dest!: split_if split: list.split prod.split if_splits)
|
|
228 |
done
|
|
229 |
|
|
230 |
|
|
231 |
text \<open>Correctness of @{const deleteP}:\<close>
|
|
232 |
|
|
233 |
lemma prefix_trie_Lf: "prefix_trie xs t = Lf \<longleftrightarrow> xs = [] \<and> t = Lf"
|
|
234 |
by(cases xs)(auto)
|
|
235 |
|
70268
|
236 |
lemma abs_trieP_Lf: "abs_trieP t = Lf \<longleftrightarrow> t = LfP"
|
70250
|
237 |
by(cases t) (auto simp: prefix_trie_Lf)
|
|
238 |
|
|
239 |
lemma delete_prefix_trie:
|
|
240 |
"delete xs (prefix_trie xs (Nd b (l,r)))
|
|
241 |
= (if (l,r) = (Lf,Lf) then Lf else prefix_trie xs (Nd False (l,r)))"
|
|
242 |
by(induction xs)(auto simp: prefix_trie_Lf)
|
|
243 |
|
|
244 |
lemma delete_append_prefix_trie:
|
|
245 |
"delete (xs @ ys) (prefix_trie xs t)
|
|
246 |
= (if delete ys t = Lf then Lf else prefix_trie xs (delete ys t))"
|
|
247 |
by(induction xs)(auto simp: prefix_trie_Lf)
|
|
248 |
|
70268
|
249 |
lemma delete_abs_trieP:
|
|
250 |
"delete ks (abs_trieP t) = abs_trieP (deleteP ks t)"
|
70250
|
251 |
apply(induction t arbitrary: ks)
|
|
252 |
apply(auto simp: delete_prefix_trie delete_append_prefix_trie
|
70268
|
253 |
prefix_trie_append prefix_trie_Lf abs_trieP_Lf
|
70250
|
254 |
dest!: split_if split: if_splits list.split prod.split)
|
|
255 |
done
|
|
256 |
|
|
257 |
|
|
258 |
text \<open>The overall correctness proof. Simply composes correctness lemmas.\<close>
|
|
259 |
|
70268
|
260 |
definition set_trieP :: "trieP \<Rightarrow> bool list set" where
|
|
261 |
"set_trieP = set_trie o abs_trieP"
|
70250
|
262 |
|
70269
|
263 |
lemma isinP_set_trieP: "isinP t xs = (xs \<in> set_trieP t)"
|
|
264 |
by(simp add: abs_trieP_isinP set_trie_isin set_trieP_def)
|
|
265 |
|
70268
|
266 |
lemma set_trieP_insertP: "set_trieP (insertP xs t) = set_trieP t \<union> {xs}"
|
|
267 |
by(simp add: abs_trieP_insertP set_trie_insert set_trieP_def)
|
70250
|
268 |
|
70269
|
269 |
lemma set_trieP_deleteP: "set_trieP (deleteP xs t) = set_trieP t - {xs}"
|
|
270 |
by(auto simp: set_trie_delete set_trieP_def simp flip: delete_abs_trieP)
|
|
271 |
|
70250
|
272 |
interpretation SP: Set
|
70268
|
273 |
where empty = emptyP and isin = isinP and insert = insertP and delete = deleteP
|
|
274 |
and set = set_trieP and invar = "\<lambda>t. True"
|
70250
|
275 |
proof (standard, goal_cases)
|
70268
|
276 |
case 1 show ?case by (simp add: set_trieP_def set_trie_def)
|
70250
|
277 |
next
|
70269
|
278 |
case 2 show ?case by(rule isinP_set_trieP)
|
70250
|
279 |
next
|
70268
|
280 |
case 3 thus ?case by (auto simp: set_trieP_insertP)
|
70250
|
281 |
next
|
70269
|
282 |
case 4 thus ?case by(auto simp: set_trieP_deleteP)
|
70250
|
283 |
qed (rule TrueI)+
|
|
284 |
|
|
285 |
end
|