# HG changeset patch # User nipkow # Date 1719306480 -7200 # Node ID f34e62eda1675a6968399d42691ea4e937ddbd15 # Parent 480b13b2abae1c8c2b5063775d5db464e5925283 clarified ternary tries diff -r 480b13b2abae -r f34e62eda167 src/HOL/Data_Structures/Trie_Map.thy --- a/src/HOL/Data_Structures/Trie_Map.thy Mon Jun 24 22:52:54 2024 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,127 +0,0 @@ -section "Tries via Search Trees" - -theory Trie_Map -imports - Tree_Map - Trie_Fun -begin - -text \An implementation of tries for an arbitrary alphabet \'a\ where -the mapping from an element of type \'a\ to the sub-trie is implemented by a binary search tree. -Although this implementation uses maps implemented by red-black trees it works for any -implementation of maps. - -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 to have 3 children, where the middle child is the sub-trie that the node maps -its key to. Hence the name \trie3\. - -Example from @{url "https://en.wikipedia.org/wiki/Ternary_search_tree#Description"}: - - 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". -\ - -datatype 'a trie3 = Nd3 bool "('a * 'a trie3) tree" - -text \In principle one should be able to given an implementation of tries -once and for all for any map implementation and not just for a specific one (unbalanced trees) as done here. -But because the map (@{type tree}) is used in a datatype, the HOL type system does not support this. - -However, the development below works verbatim for any map implementation, eg \RBT_Map\, -and not just \Tree_Map\, except for the termination lemma \lookup_size\.\ - -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)" -apply(induction t a rule: lookup.induct) -apply(auto split: if_splits) -done - - -definition empty3 :: "'a trie3" where -[simp]: "empty3 = Nd3 False Leaf" - -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 \ empty3 | Some t \ 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 \ m | - Some t \ update x (delete3 xs t) m)" - - -subsection "Correctness" - -text \Proof by stepwise refinement. First abs3tract to type @{typ "'a trie"}.\ - -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" -apply(induction t xs rule: isin3.induct) -apply(auto split: option.split) -done - -lemma abs3_insert3: "invar3 t \ abs3(insert3 xs t) = insert xs (abs3 t)" -apply(induction xs t rule: insert3.induct) -apply(auto simp: M.map_specs Tree_Set.empty_def[symmetric] split: option.split) -done - -lemma abs3_delete3: "invar3 t \ abs3(delete3 xs t) = delete xs (abs3 t)" -apply(induction xs t rule: delete3.induct) -apply(auto simp: M.map_specs split: option.split) -done - -lemma invar3_insert3: "invar3 t \ invar3 (insert3 xs t)" -apply(induction xs t rule: insert3.induct) -apply(auto simp: M.map_specs Tree_Set.empty_def[symmetric] split: option.split) -done - -lemma invar3_delete3: "invar3 t \ invar3 (delete3 xs t)" -apply(induction xs t rule: delete3.induct) -apply(auto simp: M.map_specs split: option.split) -done - -text \Overall correctness w.r.t. the \Set\ ADT:\ - -interpretation S2: Set -where empty = empty3 and isin = isin3 and insert = insert3 and delete = delete3 -and set = "set o abs3" and invar = invar3 -proof (standard, goal_cases) - case 1 show ?case by (simp add: isin_case split: list.split) -next - case 2 thus ?case by (simp add: isin_abs3) -next - case 3 thus ?case by (simp add: set_insert abs3_insert3 del: set_def) -next - case 4 thus ?case by (simp add: set_delete abs3_delete3 del: set_def) -next - case 5 thus ?case by (simp add: M.map_specs Tree_Set.empty_def[symmetric]) -next - case 6 thus ?case by (simp add: invar3_insert3) -next - case 7 thus ?case by (simp add: invar3_delete3) -qed - -end diff -r 480b13b2abae -r f34e62eda167 src/HOL/Data_Structures/Trie_Ternary.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Data_Structures/Trie_Ternary.thy Tue Jun 25 11:08:00 2024 +0200 @@ -0,0 +1,123 @@ +section "Ternary Tries" + +theory Trie_Ternary +imports + Tree_Map + Trie_Fun +begin + +text \An implementation of tries for an arbitrary alphabet \'a\ where the mapping +from an element of type \'a\ 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 to have 3 children, where the middle child is the sub-trie that the node maps +its key to. Hence the name \trie3\. + +Example from @{url "https://en.wikipedia.org/wiki/Ternary_search_tree#Description"}: + + 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". +\ + +datatype 'a trie3 = Nd3 bool "('a * 'a trie3) tree" + +text \The development below works almost verbatim for any search tree implementation, eg \RBT_Map\, +and not just \Tree_Map\, except for the termination lemma \lookup_size\.\ + +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)" +apply(induction t a rule: lookup.induct) +apply(auto split: if_splits) +done + + +definition empty3 :: "'a trie3" where +[simp]: "empty3 = Nd3 False Leaf" + +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 \ empty3 | Some t \ 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 \ m | + Some t \ update x (delete3 xs t) m)" + + +subsection "Correctness" + +text \Proof by stepwise refinement. First abs3tract to type @{typ "'a trie"}.\ + +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" +apply(induction t xs rule: isin3.induct) +apply(auto split: option.split) +done + +lemma abs3_insert3: "invar3 t \ abs3(insert3 xs t) = insert xs (abs3 t)" +apply(induction xs t rule: insert3.induct) +apply(auto simp: M.map_specs Tree_Set.empty_def[symmetric] split: option.split) +done + +lemma abs3_delete3: "invar3 t \ abs3(delete3 xs t) = delete xs (abs3 t)" +apply(induction xs t rule: delete3.induct) +apply(auto simp: M.map_specs split: option.split) +done + +lemma invar3_insert3: "invar3 t \ invar3 (insert3 xs t)" +apply(induction xs t rule: insert3.induct) +apply(auto simp: M.map_specs Tree_Set.empty_def[symmetric] split: option.split) +done + +lemma invar3_delete3: "invar3 t \ invar3 (delete3 xs t)" +apply(induction xs t rule: delete3.induct) +apply(auto simp: M.map_specs split: option.split) +done + +text \Overall correctness w.r.t. the \Set\ ADT:\ + +interpretation S2: Set +where empty = empty3 and isin = isin3 and insert = insert3 and delete = delete3 +and set = "set o abs3" and invar = invar3 +proof (standard, goal_cases) + case 1 show ?case by (simp add: isin_case split: list.split) +next + case 2 thus ?case by (simp add: isin_abs3) +next + case 3 thus ?case by (simp add: set_insert abs3_insert3 del: set_def) +next + case 4 thus ?case by (simp add: set_delete abs3_delete3 del: set_def) +next + case 5 thus ?case by (simp add: M.map_specs Tree_Set.empty_def[symmetric]) +next + case 6 thus ?case by (simp add: invar3_insert3) +next + case 7 thus ?case by (simp add: invar3_delete3) +qed + +end diff -r 480b13b2abae -r f34e62eda167 src/HOL/ROOT --- a/src/HOL/ROOT Mon Jun 24 22:52:54 2024 +0200 +++ b/src/HOL/ROOT Tue Jun 25 11:08:00 2024 +0200 @@ -307,8 +307,8 @@ Set2_Join_RBT Array_Braun Trie_Fun - Trie_Map Tries_Binary + Trie_Ternary Queue_2Lists Heaps Leftist_Heap