section \<open>Tries\<close>

text \<open>
Tries are a data structure for fast indexing with strings.

In this project you will implement and verify several functions on and
variations of tries.

(Adapted from \<^url>\<open>http://isabelle.in.tum.de/exercises/advanced/tries/ex.pdf\<close>)
\<close>

theory Project_Tries
  imports Main
begin

text \<open>

Section 3.4.4 of the Isabelle/HOL \<^doc>\<open>tutorial\<close> is a case study about tries. Read that section.

The data type of tries over the alphabet type @{typ 'a} and the value type @{typ 'v}
is defined as follows:
\<close>

datatype ('a, 'v) trie = Trie ("value" : "'v option") (alist : "('a * ('a, 'v) trie) list")

text \<open>
A trie consists of an optional value and an association list that maps letters of the alphabet
to subtrees. It comes with the two selector functions @{const value} and @{const alist}.

Furthermore, there is a function \<open>lookup\<close> on tries defined with the help of the generic search
function \<open>assoc\<close> on association lists:
\<close>
fun assoc ::  "('k * 'v) list \<Rightarrow> 'k \<Rightarrow> 'v option"
  where
    "assoc [] x = None"
  | "assoc ((a, b) # ps) x = (if a = x then Some b else assoc ps x)"

fun lookup :: "('a, 'v) trie \<Rightarrow> 'a list \<Rightarrow> 'v option"
  where
    "lookup t [] = value t"
  | "lookup t (a # as) =
      (case assoc (alist t) a of
        None \<Rightarrow> None
      | Some at \<Rightarrow> lookup at as)"

text \<open>
Finally, the function \<open>update\<close> replaces the value associated with some string by a
new value:
\<close>
fun update :: "('a, 'v) trie \<Rightarrow> 'a list \<Rightarrow> 'v \<Rightarrow> ('a, 'v) trie"
  where
    "update t [] v = Trie (Some v) (alist t)"
  | "update t (a # as) v =
      (let t' = (case assoc (alist t) a of
                  None \<Rightarrow> Trie None []
                | Some at \<Rightarrow> at)
      in Trie (value t) ((a, update t' as v) # alist t))"

text \<open>
The following result tells us that @{const update} behaves as expected:
\<close>
lemma lookup_empty [simp]: "lookup (Trie None []) xs = None"
  by (induction xs) auto

lemma "lookup (update t as v) bs = (if as = bs then Some v else lookup t bs)"
proof (induction t as v arbitrary: bs rule: update.induct)
  case (1 t v)
  then show ?case by (cases bs) auto
next
  case (2 t a as v)
  then show ?case by (cases bs) (auto split: option.split)
qed


subsection \<open>Modifying Tries\<close>

text \<open>
As a warm-up exercise, define a function \<open>modify\<close> for inserting as well as deleting elements
from a trie.

Show that \<open>modify\<close> satisfies a suitably modified version of the correctness theorem for
@{const update} above.
\<close>

fun modify :: "('a, 'v) trie \<Rightarrow> 'a list \<Rightarrow> 'v option \<Rightarrow> ('a, 'v) trie"
  where
    "modify t as v = undefined"

lemma "lookup (modify t as v) bs = (if as = bs then v else lookup t bs)"
  sorry

text \<open>
The above definition of @{const update} has the disadvantage that it often
creates junk: each association list it passes through is extended at the left
end with a new (letter, value) pair without removing any old association of
that letter which may already be present.

Logically, such cleaning up is unnecessary because @{const assoc} always searches
the list from the left.

However, it constitutes a space leak: the old associations cannot be garbage
collected because physically they are still reachable. This problem can be
solved by means of a function \<open>overwrite\<close> that does not just add new pairs at the
front but replaces old associations by new pairs if possible.

Define \<open>overwrite\<close>, modify @{const modify} to employ @{term overwrite},
and show the same relationship between @{const modify} and @{const lookup} as
before.
\<close>

fun overwrite :: "'a \<Rightarrow> 'b \<Rightarrow> ('a * 'b) list \<Rightarrow> ('a * 'b) list"
  where
    "overwrite k v as = undefined"

fun modify' :: "('a, 'v) trie \<Rightarrow> 'a list \<Rightarrow> 'v option \<Rightarrow> ('a, 'v) trie"
  where
    "modify' t as v = undefined"

lemma "lookup (modify' t as v) bs = (if as = bs then v else lookup t bs)"
  sorry


subsection \<open>Time Complexity\<close>

text \<open>
Prove that @{const lookup} takes at most a linear number of recursive calls.
\<close>
fun lookup_t :: "('a, 'v) trie \<Rightarrow> 'a list \<Rightarrow> nat"
  where
    "lookup_t t as = undefined"

fun sz :: "('a, 'v) trie \<Rightarrow> nat"
  where
    "sz t = undefined"

lemma "lookup_t t as \<le> sz t"
  sorry


subsection \<open>Tries via Partial Functions\<close>

text \<open>
Instead of association lists we can also use partial functions that map
letters to subtrees.

Partiality can be modelled with the help of type @{typ "'a option"}:
if @{term f} is a function of type @{typ "'a \<Rightarrow> 'b option"}, let \<open>f a = Some b\<close> if \<open>a\<close> should be
mapped to some @{term b}, and let \<open>f a = None\<close> otherwise.
\<close>

datatype ('a, 'v) trieP = TrieP "'v option" "'a \<Rightarrow> ('a, 'v) trieP option"

text \<open>
Modify the definitions of @{const lookup} and @{const modify'} accordingly and
show the same correctness theorem as above.
\<close>

fun lookup2 :: "('a, 'v) trieP \<Rightarrow> 'a list \<Rightarrow> 'v option"
  where
    "lookup2 t as = undefined"

fun modify2 :: "('a, 'v) trieP \<Rightarrow> 'a list \<Rightarrow> 'v option \<Rightarrow> ('a, 'v) trieP"
  where
    "modify2 t as w = undefined"

lemma "lookup2 (modify2 t as v) bs = (if as = bs then v else lookup2 t bs)"
  sorry

end