|
1 (* Author: Tobias Nipkow *) |
|
2 |
|
3 section \<open>Trie and Patricia Trie Implementations of \mbox{\<open>bool list set\<close>}\<close> |
|
4 |
|
5 theory Trie |
|
6 imports Set_Specs |
|
7 begin |
|
8 |
|
9 hide_const (open) insert |
|
10 |
|
11 declare Let_def[simp] |
|
12 |
|
13 |
|
14 subsection "Trie" |
|
15 |
|
16 datatype trie = Leaf | Node bool "trie * trie" |
|
17 |
|
18 text \<open>The pairing allows things like \<open>Node b (if \<dots> then (l,r) else (r,l))\<close>.\<close> |
|
19 |
|
20 fun isin :: "trie \<Rightarrow> bool list \<Rightarrow> bool" where |
|
21 "isin Leaf ks = False" | |
|
22 "isin (Node b (l,r)) ks = |
|
23 (case ks of |
|
24 [] \<Rightarrow> b | |
|
25 k#ks \<Rightarrow> isin (if k then r else l) ks)" |
|
26 |
|
27 fun insert :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where |
|
28 "insert [] Leaf = Node True (Leaf,Leaf)" | |
|
29 "insert [] (Node b lr) = Node True lr" | |
|
30 "insert (k#ks) Leaf = |
|
31 Node False (if k then (Leaf, insert ks Leaf) |
|
32 else (insert ks Leaf, Leaf))" | |
|
33 "insert (k#ks) (Node b (l,r)) = |
|
34 Node b (if k then (l, insert ks r) |
|
35 else (insert ks l, r))" |
|
36 |
|
37 fun shrink_Node :: "bool \<Rightarrow> trie * trie \<Rightarrow> trie" where |
|
38 "shrink_Node b lr = (if \<not> b \<and> lr = (Leaf,Leaf) then Leaf else Node b lr)" |
|
39 |
|
40 fun delete :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where |
|
41 "delete ks Leaf = Leaf" | |
|
42 "delete ks (Node b (l,r)) = |
|
43 (case ks of |
|
44 [] \<Rightarrow> shrink_Node False (l,r) | |
|
45 k#ks' \<Rightarrow> shrink_Node b (if k then (l, delete ks' r) else (delete ks' l, r)))" |
|
46 |
|
47 fun invar :: "trie \<Rightarrow> bool" where |
|
48 "invar Leaf = True" | |
|
49 "invar (Node b (l,r)) = ((\<not> b \<longrightarrow> l \<noteq> Leaf \<or> r \<noteq> Leaf) \<and> invar l \<and> invar r)" |
|
50 |
|
51 |
|
52 subsubsection \<open>Functional Correctness\<close> |
|
53 |
|
54 lemma isin_insert: "isin (insert as t) bs = (as = bs \<or> isin t bs)" |
|
55 apply(induction as t arbitrary: bs rule: insert.induct) |
|
56 apply(auto split: list.splits) |
|
57 done |
|
58 |
|
59 lemma isin_delete: "isin (delete as t) bs = (as \<noteq> bs \<and> isin t bs)" |
|
60 apply(induction as t arbitrary: bs rule: delete.induct) |
|
61 apply simp |
|
62 apply (auto split: list.splits; fastforce) |
|
63 done |
|
64 |
|
65 lemma insert_not_Leaf: "insert ks t \<noteq> Leaf" |
|
66 by(cases "(ks,t)" rule: insert.cases) auto |
|
67 |
|
68 lemma invar_insert: "invar t \<Longrightarrow> invar (insert ks t)" |
|
69 by(induction ks t rule: insert.induct)(auto simp: insert_not_Leaf) |
|
70 |
|
71 lemma invar_delete: "invar t \<Longrightarrow> invar (delete ks t)" |
|
72 by(induction ks t rule: delete.induct)(auto split: list.split) |
|
73 |
|
74 interpretation T: Set |
|
75 where empty = Leaf and insert = insert and delete = delete and isin = isin |
|
76 and set = "\<lambda>t. {x. isin t x}" and invar = invar |
|
77 proof (standard, goal_cases) |
|
78 case 1 thus ?case by simp |
|
79 next |
|
80 case 2 thus ?case by simp |
|
81 next |
|
82 case 3 thus ?case by (auto simp add: isin_insert) |
|
83 next |
|
84 case 4 thus ?case by (auto simp add: isin_delete) |
|
85 next |
|
86 case 5 thus ?case by simp |
|
87 next |
|
88 case 6 thus ?case by (auto simp add: invar_insert) |
|
89 next |
|
90 case 7 thus ?case by (auto simp add: invar_delete) |
|
91 qed |
|
92 |
|
93 |
|
94 subsection "Patricia Trie" |
|
95 |
|
96 datatype trieP = LeafP | NodeP "bool list" bool "trieP * trieP" |
|
97 |
|
98 fun isinP :: "trieP \<Rightarrow> bool list \<Rightarrow> bool" where |
|
99 "isinP LeafP ks = False" | |
|
100 "isinP (NodeP ps b (l,r)) ks = |
|
101 (let n = length ps in |
|
102 if ps = take n ks |
|
103 then case drop n ks of [] \<Rightarrow> b | k#ks' \<Rightarrow> isinP (if k then r else l) ks' |
|
104 else False)" |
|
105 |
|
106 text \<open>\<open>split xs ys = (zs, xs', ys')\<close> iff |
|
107 \<open>zs\<close> is the longest common prefix of \<open>xs\<close> and \<open>ys\<close> and |
|
108 \<open>xs = zs @ xs'\<close> and \<open>ys = zs @ ys'\<close>\<close> |
|
109 fun split where |
|
110 "split [] ys = ([],[],ys)" | |
|
111 "split xs [] = ([],xs,[])" | |
|
112 "split (x#xs) (y#ys) = |
|
113 (if x\<noteq>y then ([],x#xs,y#ys) |
|
114 else let (ps,xs',ys') = split xs ys in (x#ps,xs',ys'))" |
|
115 |
|
116 fun insertP :: "bool list \<Rightarrow> trieP \<Rightarrow> trieP" where |
|
117 "insertP ks LeafP = NodeP ks True (LeafP,LeafP)" | |
|
118 "insertP ks (NodeP ps b (l,r)) = |
|
119 (case split ks ps of |
|
120 (qs,k#ks',p#ps') \<Rightarrow> |
|
121 let tp = NodeP ps' b (l,r); tk = NodeP ks' True (LeafP,LeafP) |
|
122 in NodeP qs False (if k then (tp,tk) else (tk,tp)) | |
|
123 (qs,k#ks',[]) \<Rightarrow> |
|
124 NodeP ps b (if k then (l,insertP ks' r) else (insertP ks' l, r)) | |
|
125 (qs,[],p#ps') \<Rightarrow> |
|
126 let t = NodeP ps' b (l,r) |
|
127 in NodeP qs True (if p then (LeafP, t) else (t, LeafP)) | |
|
128 (qs,[],[]) \<Rightarrow> NodeP ps True (l,r))" |
|
129 |
|
130 fun shrink_NodeP where |
|
131 "shrink_NodeP ps b lr = (if b then NodeP ps b lr else |
|
132 case lr of |
|
133 (LeafP, LeafP) \<Rightarrow> LeafP | |
|
134 (LeafP, NodeP ps' b' lr') \<Rightarrow> NodeP (ps @ True # ps') b' lr' | |
|
135 (NodeP ps' b' lr', LeafP) \<Rightarrow> NodeP (ps @ False # ps') b' lr' | |
|
136 _ \<Rightarrow> NodeP ps b lr)" |
|
137 |
|
138 fun deleteP :: "bool list \<Rightarrow> trieP \<Rightarrow> trieP" where |
|
139 "deleteP ks LeafP = LeafP" | |
|
140 "deleteP ks (NodeP ps b (l,r)) = |
|
141 (case split ks ps of |
|
142 (qs,_,p#ps') \<Rightarrow> NodeP ps b (l,r) | |
|
143 (qs,k#ks',[]) \<Rightarrow> |
|
144 shrink_NodeP ps b (if k then (l, deleteP ks' r) else (deleteP ks' l, r)) | |
|
145 (qs,[],[]) \<Rightarrow> shrink_NodeP ps False (l,r))" |
|
146 |
|
147 fun invarP :: "trieP \<Rightarrow> bool" where |
|
148 "invarP LeafP = True" | |
|
149 "invarP (NodeP ps b (l,r)) = ((\<not>b \<longrightarrow> l \<noteq> LeafP \<or> r \<noteq> LeafP) \<and> invarP l \<and> invarP r)" |
|
150 |
|
151 text \<open>The abstraction function(s):\<close> |
|
152 |
|
153 fun prefix_trie :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where |
|
154 "prefix_trie [] t = t" | |
|
155 "prefix_trie (k#ks) t = |
|
156 (let t' = prefix_trie ks t in shrink_Node False (if k then (Leaf,t') else (t',Leaf)))" |
|
157 |
|
158 fun abs_trieP :: "trieP \<Rightarrow> trie" where |
|
159 "abs_trieP LeafP = Leaf" | |
|
160 "abs_trieP (NodeP ps b (l,r)) = prefix_trie ps (Node b (abs_trieP l, abs_trieP r))" |
|
161 |
|
162 |
|
163 subsubsection \<open>Functional Correctness\<close> |
|
164 |
|
165 text \<open>IsinP:\<close> |
|
166 |
|
167 lemma isin_prefix_trie: "isin (prefix_trie ps t) ks = |
|
168 (length ks \<ge> length ps \<and> |
|
169 (let n = length ps in ps = take n ks \<and> isin t (drop n ks)))" |
|
170 by(induction ps arbitrary: ks)(auto split: list.split) |
|
171 |
|
172 lemma isinP: "isinP t ks = isin (abs_trieP t) ks" |
|
173 apply(induction t arbitrary: ks rule: abs_trieP.induct) |
|
174 apply(auto simp: isin_prefix_trie split: list.split) |
|
175 using nat_le_linear apply force |
|
176 using nat_le_linear apply force |
|
177 done |
|
178 |
|
179 text \<open>Insert:\<close> |
|
180 |
|
181 lemma prefix_trie_Leaf_iff: "prefix_trie ps t = Leaf \<longleftrightarrow> t = Leaf" |
|
182 by (induction ps) auto |
|
183 |
|
184 lemma prefix_trie_Leafs: "prefix_trie ks (Node True (Leaf,Leaf)) = insert ks Leaf" |
|
185 by(induction ks) (auto simp: prefix_trie_Leaf_iff) |
|
186 |
|
187 lemma prefix_trie_Leaf: "prefix_trie ps Leaf = Leaf" |
|
188 by(induction ps) auto |
|
189 |
|
190 lemma insert_append: "insert (ks @ ks') (prefix_trie ks t) = prefix_trie ks (insert ks' t)" |
|
191 by(induction ks) (auto simp: prefix_trie_Leaf_iff insert_not_Leaf prefix_trie_Leaf) |
|
192 |
|
193 lemma prefix_trie_append: "prefix_trie (ps @ qs) t = prefix_trie ps (prefix_trie qs t)" |
|
194 by(induction ps) auto |
|
195 |
|
196 lemma split_iff: "split xs ys = (zs, xs', ys') \<longleftrightarrow> |
|
197 xs = zs @ xs' \<and> ys = zs @ ys' \<and> (xs' \<noteq> [] \<and> ys' \<noteq> [] \<longrightarrow> hd xs' \<noteq> hd ys')" |
|
198 proof(induction xs ys arbitrary: zs xs' ys' rule: split.induct) |
|
199 case 1 thus ?case by auto |
|
200 next |
|
201 case 2 thus ?case by auto |
|
202 next |
|
203 case 3 thus ?case by(clarsimp simp: Cons_eq_append_conv split: prod.splits if_splits) auto |
|
204 qed |
|
205 |
|
206 lemma abs_trieP_insertP: |
|
207 "abs_trieP (insertP ks t) = insert ks (abs_trieP t)" |
|
208 apply(induction t arbitrary: ks) |
|
209 apply(auto simp: prefix_trie_Leafs insert_append prefix_trie_append |
|
210 prefix_trie_Leaf_iff split_iff split: list.split prod.split) |
|
211 done |
|
212 |
|
213 corollary isinP_insertP: "isinP (insertP ks t) ks' = (ks=ks' \<or> isinP t ks')" |
|
214 by (simp add: isin_insert isinP abs_trieP_insertP) |
|
215 |
|
216 lemma insertP_not_LeafP: "insertP ks t \<noteq> LeafP" |
|
217 apply(induction ks t rule: insertP.induct) |
|
218 apply(auto split: prod.split list.split) |
|
219 done |
|
220 |
|
221 lemma invarP_insertP: "invarP t \<Longrightarrow> invarP (insertP ks t)" |
|
222 apply(induction ks t rule: insertP.induct) |
|
223 apply(auto simp: insertP_not_LeafP split: prod.split list.split) |
|
224 done |
|
225 |
|
226 text \<open>Delete:\<close> |
|
227 |
|
228 lemma invar_shrink_NodeP: "\<lbrakk> invarP l; invarP r \<rbrakk> \<Longrightarrow> invarP (shrink_NodeP ps b (l,r))" |
|
229 by(auto split: trieP.split) |
|
230 |
|
231 lemma invarP_deleteP: "invarP t \<Longrightarrow> invarP (deleteP ks t)" |
|
232 apply(induction t arbitrary: ks) |
|
233 apply(auto simp: invar_shrink_NodeP split_iff simp del: shrink_NodeP.simps |
|
234 split!: list.splits prod.split if_splits) |
|
235 done |
|
236 |
|
237 lemma delete_append: |
|
238 "delete (ks @ ks') (prefix_trie ks t) = prefix_trie ks (delete ks' t)" |
|
239 by(induction ks) auto |
|
240 |
|
241 lemma abs_trieP_shrink_NodeP: |
|
242 "abs_trieP (shrink_NodeP ps b (l,r)) = prefix_trie ps (shrink_Node b (abs_trieP l, abs_trieP r))" |
|
243 apply(induction ps arbitrary: b l r) |
|
244 apply (auto simp: prefix_trie_Leaf prefix_trie_Leaf_iff prefix_trie_append |
|
245 split!: trieP.splits if_splits) |
|
246 done |
|
247 |
|
248 lemma abs_trieP_deleteP: |
|
249 "abs_trieP (deleteP ks t) = delete ks (abs_trieP t)" |
|
250 apply(induction t arbitrary: ks) |
|
251 apply(auto simp: prefix_trie_Leafs delete_append prefix_trie_Leaf |
|
252 abs_trieP_shrink_NodeP prefix_trie_append split_iff |
|
253 simp del: shrink_NodeP.simps split!: list.split prod.split if_splits) |
|
254 done |
|
255 |
|
256 corollary isinP_deleteP: "isinP (deleteP ks t) ks' = (ks\<noteq>ks' \<and> isinP t ks')" |
|
257 by (simp add: isin_delete isinP abs_trieP_deleteP) |
|
258 |
|
259 interpretation PT: Set |
|
260 where empty = LeafP and insert = insertP and delete = deleteP |
|
261 and isin = isinP and set = "\<lambda>t. {x. isinP t x}" and invar = invarP |
|
262 proof (standard, goal_cases) |
|
263 case 1 thus ?case by (simp) |
|
264 next |
|
265 case 2 thus ?case by (simp) |
|
266 next |
|
267 case 3 thus ?case by (auto simp add: isinP_insertP) |
|
268 next |
|
269 case 4 thus ?case by (auto simp add: isinP_deleteP) |
|
270 next |
|
271 case 5 thus ?case by (simp) |
|
272 next |
|
273 case 6 thus ?case by (simp add: invarP_insertP) |
|
274 next |
|
275 case 7 thus ?case by (auto simp add: invarP_deleteP) |
|
276 qed |
|
277 |
|
278 end |