Quelle Trie_Ternary.thy Sprache: Isabelle

section "Ternary Tries"

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 to have 3 children, where the middle child is the sub-trie that the node maps
its key to. Hence the name \<open>trie3\<close>.

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".
\<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)

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 \<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 ?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_trie_insert abs3_insert3 del: set_trie_def)
next
  case 4 thus ?case by (simp add: set_trie_delete abs3_delete3 del: set_trie_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

quality99%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.