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