1(* Author: Tobias Nipkow *)
2
3section \<open>Trie and Patricia Trie Implementations of \mbox{\<open>bool list set\<close>}\<close>
4
5theory Trie
6imports Set_Specs
7begin
8
9hide_const (open) insert
10
11declare Let_def[simp]
12
13
14subsection "Trie"
15
16datatype trie = Leaf | Node bool "trie * trie"
17
18text \<open>The pairing allows things like \<open>Node b (if \<dots> then (l,r) else (r,l))\<close>.\<close>
19
20fun 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
27fun 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
37fun 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
40fun 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
47fun 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
52subsubsection \<open>Functional Correctness\<close>
53
54lemma isin_insert: "isin (insert as t) bs = (as = bs \<or> isin t bs)"
55apply(induction as t arbitrary: bs rule: insert.induct)
56apply(auto split: list.splits)
57done
58
59lemma isin_delete: "isin (delete as t) bs = (as \<noteq> bs \<and> isin t bs)"
60apply(induction as t arbitrary: bs rule: delete.induct)
61 apply simp
62apply (auto split: list.splits; fastforce)
63done
64
65lemma insert_not_Leaf: "insert ks t \<noteq> Leaf"
66by(cases "(ks,t)" rule: insert.cases) auto
67
68lemma invar_insert: "invar t \<Longrightarrow> invar (insert ks t)"
69by(induction ks t rule: insert.induct)(auto simp: insert_not_Leaf)
70
71lemma invar_delete: "invar t \<Longrightarrow> invar (delete ks t)"
72by(induction ks t rule: delete.induct)(auto split: list.split)
73
74interpretation T: Set
75where empty = Leaf and insert = insert and delete = delete and isin = isin
76and set = "\<lambda>t. {x. isin t x}" and invar = invar
77proof (standard, goal_cases)
78  case 1 thus ?case by simp
79next
80  case 2 thus ?case by simp
81next
82  case 3 thus ?case by (auto simp add: isin_insert)
83next
84  case 4 thus ?case by (auto simp add: isin_delete)
85next
86  case 5 thus ?case by simp
87next
88  case 6 thus ?case by (auto simp add: invar_insert)
89next
90  case 7 thus ?case by (auto simp add: invar_delete)
91qed
92
93
94subsection "Patricia Trie"
95
96datatype trieP = LeafP | NodeP "bool list" bool "trieP * trieP"
97
98fun 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
106text \<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>
109fun 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
116fun 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
130fun 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
138fun 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
147fun 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
151text \<open>The abstraction function(s):\<close>
152
153fun 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
158fun 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
163subsubsection \<open>Functional Correctness\<close>
164
165text \<open>IsinP:\<close>
166
167lemma 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)))"
170by(induction ps arbitrary: ks)(auto split: list.split)
171
172lemma isinP: "isinP t ks = isin (abs_trieP t) ks"
173apply(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
176using nat_le_linear apply force
177done
178
179text \<open>Insert:\<close>
180
181lemma prefix_trie_Leaf_iff: "prefix_trie ps t = Leaf \<longleftrightarrow> t = Leaf"
182by (induction ps) auto
183
184lemma prefix_trie_Leafs: "prefix_trie ks (Node True (Leaf,Leaf)) = insert ks Leaf"
185by(induction ks) (auto simp: prefix_trie_Leaf_iff)
186
187lemma prefix_trie_Leaf: "prefix_trie ps Leaf = Leaf"
188by(induction ps) auto
189
190lemma insert_append: "insert (ks @ ks') (prefix_trie ks t) = prefix_trie ks (insert ks' t)"
191by(induction ks) (auto simp: prefix_trie_Leaf_iff insert_not_Leaf prefix_trie_Leaf)
192
193lemma prefix_trie_append: "prefix_trie (ps @ qs) t = prefix_trie ps (prefix_trie qs t)"
194by(induction ps) auto
195
196lemma 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')"
198proof(induction xs ys arbitrary: zs xs' ys' rule: split.induct)
199  case 1 thus ?case by auto
200next
201  case 2 thus ?case by auto
202next
203  case 3 thus ?case by(clarsimp simp: Cons_eq_append_conv split: prod.splits if_splits) auto
204qed
205
206lemma abs_trieP_insertP:
207  "abs_trieP (insertP ks t) = insert ks (abs_trieP t)"
208apply(induction t arbitrary: ks)
209apply(auto simp: prefix_trie_Leafs insert_append prefix_trie_append
210        prefix_trie_Leaf_iff split_iff split: list.split prod.split)
211done
212
213corollary isinP_insertP: "isinP (insertP ks t) ks' = (ks=ks' \<or> isinP t ks')"
214by (simp add: isin_insert isinP abs_trieP_insertP)
215
216lemma insertP_not_LeafP: "insertP ks t \<noteq> LeafP"
217apply(induction ks t rule: insertP.induct)
218apply(auto split: prod.split list.split)
219done
220
221lemma invarP_insertP: "invarP t \<Longrightarrow> invarP (insertP ks t)"
222apply(induction ks t rule: insertP.induct)
223apply(auto simp: insertP_not_LeafP split: prod.split list.split)
224done
225
226text \<open>Delete:\<close>
227
228lemma invar_shrink_NodeP: "\<lbrakk> invarP l; invarP r \<rbrakk> \<Longrightarrow> invarP (shrink_NodeP ps b (l,r))"
229by(auto split: trieP.split)
230
231lemma invarP_deleteP: "invarP t \<Longrightarrow> invarP (deleteP ks t)"
232apply(induction t arbitrary: ks)
233apply(auto simp: invar_shrink_NodeP split_iff simp del: shrink_NodeP.simps
234           split!: list.splits prod.split if_splits)
235done
236
237lemma delete_append:
238  "delete (ks @ ks') (prefix_trie ks t) = prefix_trie ks (delete ks' t)"
239by(induction ks) auto
240
241lemma 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))"
243apply(induction ps arbitrary: b l r)
244apply (auto simp: prefix_trie_Leaf prefix_trie_Leaf_iff prefix_trie_append
245            split!: trieP.splits if_splits)
246done
247
248lemma abs_trieP_deleteP:
249  "abs_trieP (deleteP ks t) = delete ks (abs_trieP t)"
250apply(induction t arbitrary: ks)
251apply(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)
254done
255
256corollary isinP_deleteP: "isinP (deleteP ks t) ks' = (ks\<noteq>ks' \<and> isinP t ks')"
257by (simp add: isin_delete isinP abs_trieP_deleteP)
258
259interpretation PT: Set
260where empty = LeafP and insert = insertP and delete = deleteP
261and isin = isinP and set = "\<lambda>t. {x. isinP t x}" and invar = invarP
262proof (standard, goal_cases)
263  case 1 thus ?case by (simp)
264next
265  case 2 thus ?case by (simp)
266next
267  case 3 thus ?case by (auto simp add: isinP_insertP)
268next
269  case 4 thus ?case by (auto simp add: isinP_deleteP)
270next
271  case 5 thus ?case by (simp)
272next
273  case 6 thus ?case by (simp add: invarP_insertP)
274next
275  case 7 thus ?case by (auto simp add: invarP_deleteP)
276qed
277
278end
279