1 section "Tries via Search Trees" |
|
2 |
|
3 theory Trie_Map |
|
4 imports |
|
5 Tree_Map |
|
6 Trie_Fun |
|
7 begin |
|
8 |
|
9 text \<open>An implementation of tries for an arbitrary alphabet \<open>'a\<close> where |
|
10 the mapping from an element of type \<open>'a\<close> to the sub-trie is implemented by a binary search tree. |
|
11 Although this implementation uses maps implemented by red-black trees it works for any |
|
12 implementation of maps. |
|
13 |
|
14 This is an implementation of the ``ternary search trees'' by Bentley and Sedgewick |
|
15 [SODA 1997, Dr. Dobbs 1998]. The name derives from the fact that a node in the BST can now |
|
16 be drawn to have 3 children, where the middle child is the sub-trie that the node maps |
|
17 its key to. Hence the name \<open>trie3\<close>. |
|
18 |
|
19 Example from @{url "https://en.wikipedia.org/wiki/Ternary_search_tree#Description"}: |
|
20 |
|
21 c |
|
22 / | \ |
|
23 a u h |
|
24 | | | \ |
|
25 t. t e. u |
|
26 / / | / | |
|
27 s. p. e. i. s. |
|
28 |
|
29 Characters with a dot are final. |
|
30 Thus the tree represents the set of strings "cute","cup","at","as","he","us" and "i". |
|
31 \<close> |
|
32 |
|
33 datatype 'a trie3 = Nd3 bool "('a * 'a trie3) tree" |
|
34 |
|
35 text \<open>In principle one should be able to given an implementation of tries |
|
36 once and for all for any map implementation and not just for a specific one (unbalanced trees) as done here. |
|
37 But because the map (@{type tree}) is used in a datatype, the HOL type system does not support this. |
|
38 |
|
39 However, the development below works verbatim for any map implementation, eg \<open>RBT_Map\<close>, |
|
40 and not just \<open>Tree_Map\<close>, except for the termination lemma \<open>lookup_size\<close>.\<close> |
|
41 |
|
42 term size_tree |
|
43 lemma lookup_size[termination_simp]: |
|
44 fixes t :: "('a::linorder * 'a trie3) tree" |
|
45 shows "lookup t a = Some b \<Longrightarrow> size b < Suc (size_tree (\<lambda>ab. Suc (size (snd( ab)))) t)" |
|
46 apply(induction t a rule: lookup.induct) |
|
47 apply(auto split: if_splits) |
|
48 done |
|
49 |
|
50 |
|
51 definition empty3 :: "'a trie3" where |
|
52 [simp]: "empty3 = Nd3 False Leaf" |
|
53 |
|
54 fun isin3 :: "('a::linorder) trie3 \<Rightarrow> 'a list \<Rightarrow> bool" where |
|
55 "isin3 (Nd3 b m) [] = b" | |
|
56 "isin3 (Nd3 b m) (x # xs) = (case lookup m x of None \<Rightarrow> False | Some t \<Rightarrow> isin3 t xs)" |
|
57 |
|
58 fun insert3 :: "('a::linorder) list \<Rightarrow> 'a trie3 \<Rightarrow> 'a trie3" where |
|
59 "insert3 [] (Nd3 b m) = Nd3 True m" | |
|
60 "insert3 (x#xs) (Nd3 b m) = |
|
61 Nd3 b (update x (insert3 xs (case lookup m x of None \<Rightarrow> empty3 | Some t \<Rightarrow> t)) m)" |
|
62 |
|
63 fun delete3 :: "('a::linorder) list \<Rightarrow> 'a trie3 \<Rightarrow> 'a trie3" where |
|
64 "delete3 [] (Nd3 b m) = Nd3 False m" | |
|
65 "delete3 (x#xs) (Nd3 b m) = Nd3 b |
|
66 (case lookup m x of |
|
67 None \<Rightarrow> m | |
|
68 Some t \<Rightarrow> update x (delete3 xs t) m)" |
|
69 |
|
70 |
|
71 subsection "Correctness" |
|
72 |
|
73 text \<open>Proof by stepwise refinement. First abs3tract to type @{typ "'a trie"}.\<close> |
|
74 |
|
75 fun abs3 :: "'a::linorder trie3 \<Rightarrow> 'a trie" where |
|
76 "abs3 (Nd3 b t) = Nd b (\<lambda>a. map_option abs3 (lookup t a))" |
|
77 |
|
78 fun invar3 :: "('a::linorder)trie3 \<Rightarrow> bool" where |
|
79 "invar3 (Nd3 b m) = (M.invar m \<and> (\<forall>a t. lookup m a = Some t \<longrightarrow> invar3 t))" |
|
80 |
|
81 lemma isin_abs3: "isin3 t xs = isin (abs3 t) xs" |
|
82 apply(induction t xs rule: isin3.induct) |
|
83 apply(auto split: option.split) |
|
84 done |
|
85 |
|
86 lemma abs3_insert3: "invar3 t \<Longrightarrow> abs3(insert3 xs t) = insert xs (abs3 t)" |
|
87 apply(induction xs t rule: insert3.induct) |
|
88 apply(auto simp: M.map_specs Tree_Set.empty_def[symmetric] split: option.split) |
|
89 done |
|
90 |
|
91 lemma abs3_delete3: "invar3 t \<Longrightarrow> abs3(delete3 xs t) = delete xs (abs3 t)" |
|
92 apply(induction xs t rule: delete3.induct) |
|
93 apply(auto simp: M.map_specs split: option.split) |
|
94 done |
|
95 |
|
96 lemma invar3_insert3: "invar3 t \<Longrightarrow> invar3 (insert3 xs t)" |
|
97 apply(induction xs t rule: insert3.induct) |
|
98 apply(auto simp: M.map_specs Tree_Set.empty_def[symmetric] split: option.split) |
|
99 done |
|
100 |
|
101 lemma invar3_delete3: "invar3 t \<Longrightarrow> invar3 (delete3 xs t)" |
|
102 apply(induction xs t rule: delete3.induct) |
|
103 apply(auto simp: M.map_specs split: option.split) |
|
104 done |
|
105 |
|
106 text \<open>Overall correctness w.r.t. the \<open>Set\<close> ADT:\<close> |
|
107 |
|
108 interpretation S2: Set |
|
109 where empty = empty3 and isin = isin3 and insert = insert3 and delete = delete3 |
|
110 and set = "set o abs3" and invar = invar3 |
|
111 proof (standard, goal_cases) |
|
112 case 1 show ?case by (simp add: isin_case split: list.split) |
|
113 next |
|
114 case 2 thus ?case by (simp add: isin_abs3) |
|
115 next |
|
116 case 3 thus ?case by (simp add: set_insert abs3_insert3 del: set_def) |
|
117 next |
|
118 case 4 thus ?case by (simp add: set_delete abs3_delete3 del: set_def) |
|
119 next |
|
120 case 5 thus ?case by (simp add: M.map_specs Tree_Set.empty_def[symmetric]) |
|
121 next |
|
122 case 6 thus ?case by (simp add: invar3_insert3) |
|
123 next |
|
124 case 7 thus ?case by (simp add: invar3_delete3) |
|
125 qed |
|
126 |
|
127 end |
|