theory Trie_Ternary imports
Tree_Map
Trie_Fun begin
text\<open>An implementation of tries for an arbitrary alphabet \<open>'a\<close> where the mapping from an element of type \<open>'a\<close> to the sub-trie is implemented by an (unbalanced) binary search tree. In principle, other search trees (e.g. red-black trees) work just as well, with some small adjustments (Exercise!).
This is an implementation of the ``ternary search trees''by Bentley and Sedgewick
[SODA 1997, Dr. Dobbs 1998]. The name derives from the fact that a node in the BST can now
be drawn tohave 3 children, where the middle child is the sub-trie that the node maps
its key to. Hence the name \<open>trie3\<close>.
c
/ | \
a u h
| | | \
t. t e. u
/ / | / |
s. p. e. i. s.
Characters with a dot are final. Thus the tree represents the set of strings "cute","cup","at","as","he","us"and"i". \<close>
datatype'a trie3 = Nd3 bool "('a * 'a trie3) tree"
text\<open>The development below works almost verbatim for any search tree implementation, eg \<open>RBT_Map\<close>, and not just \<open>Tree_Map\<close>, except for the termination lemma \<open>lookup_size\<close>.\<close>
term size_tree lemma lookup_size[termination_simp]: fixes t :: "('a::linorder * 'a trie3) tree" shows"lookup t a = Some b \ size b < Suc (size_tree (\ab. Suc (size (snd( ab)))) t)" by (induction t a rule: lookup.induct)(auto split: if_splits)
fun isin3 :: "('a::linorder) trie3 \ 'a list \ bool" where "isin3 (Nd3 b m) [] = b" | "isin3 (Nd3 b m) (x # xs) = (case lookup m x of None \ False | Some t \ isin3 t xs)"
fun insert3 :: "('a::linorder) list \ 'a trie3 \ 'a trie3" where "insert3 [] (Nd3 b m) = Nd3 True m" | "insert3 (x#xs) (Nd3 b m) =
Nd3 b (update x (insert3 xs (case lookup m x of None \<Rightarrow> empty3 | Some t \<Rightarrow> t)) m)"
fun delete3 :: "('a::linorder) list \ 'a trie3 \ 'a trie3" where "delete3 [] (Nd3 b m) = Nd3 False m" | "delete3 (x#xs) (Nd3 b m) = Nd3 b
(case lookup m x of
None \<Rightarrow> m |
Some t \<Rightarrow> update x (delete3 xs t) m)"
subsection "Correctness"
text\<open>Proof by stepwise refinement. First abs3tract to type @{typ "'a trie"}.\<close>
fun abs3 :: "'a::linorder trie3 \ 'a trie" where "abs3 (Nd3 b t) = Nd b (\a. map_option abs3 (lookup t a))"
fun invar3 :: "('a::linorder)trie3 \ bool" where "invar3 (Nd3 b m) = (M.invar m \ (\a t. lookup m a = Some t \ invar3 t))"
lemma isin_abs3: "isin3 t xs = isin (abs3 t) xs" by (induction t xs rule: isin3.induct)(auto split: option.split)
lemma abs3_insert3: "invar3 t \ abs3(insert3 xs t) = insert xs (abs3 t)" proof (induction xs t rule: insert3.induct) qed (auto simp: M.map_specs Tree_Set.empty_def[symmetric] split: option.split)
lemma abs3_delete3: "invar3 t \ abs3(delete3 xs t) = delete xs (abs3 t)" by (induction xs t rule: delete3.induct)(auto simp: M.map_specs split: option.split)
lemma invar3_insert3: "invar3 t \ invar3 (insert3 xs t)" proof (induction xs t rule: insert3.induct) qed (auto simp: M.map_specs simp flip: Tree_Set.empty_def split: option.split)
lemma invar3_delete3: "invar3 t \ invar3 (delete3 xs t)" by (induction xs t rule: delete3.induct)(auto simp: M.map_specs split: option.split)
text\<open>Overall correctness w.r.t. the \<open>Set\<close> ADT:\<close>
interpretation S2: Set where empty = empty3 and isin = isin3 and insert = insert3 and delete = delete3 and set = "set_trie o abs3"and invar = invar3 proof (standard, goal_cases) case 1 show ?caseby (simp add: isin_case split: list.split) next case 2 thus ?caseby (simp add: isin_abs3) next case 3 thus ?caseby (simp add: set_trie_insert abs3_insert3 del: set_trie_def) next case 4 thus ?caseby (simp add: set_trie_delete abs3_delete3 del: set_trie_def) next case 5 thus ?caseby (simp add: M.map_specs Tree_Set.empty_def[symmetric]) next case 6 thus ?caseby (simp add: invar3_insert3) next case 7 thus ?caseby (simp add: invar3_delete3) qed
end
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
