Quelle  Trie.thy

(*<*)
theory Trie imports Main begin
(*>*)
text‹
  minimize running time, each node of a trie should contain an array that maps
  to subtries. We have chosen a
  where the subtries are held in an association list, i.e.\ a
  of (letter,trie) pairs. Abstracting over the alphabet 🍋‹'a› and the
  🍋‹'v› we define a trie as follows:
 ›

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

text‹\noindent
 index{datatypes!and nested recursion}%
  first component is the optional value, the second component the
  list of subtries. This is an example of nested recursion involving products,
  is fine because products are datatypes as well.
  define two selector functions:
 ›

primrec "value" :: "('a,'v)trie ==> 'v option" where
"value(Trie ov al) = ov"
primrec alist :: "('a,'v)trie ==> ('a * ('a,'v)trie)list" where
"alist(Trie ov al) = al"

text‹\noindent
  lists come with a generic lookup function. Its result
  type ‹option› because a lookup can fail:
 ›

primrec assoc :: "('key * 'val)list ==> 'key ==> 'val option" where
"assoc [] x = None" |
"assoc (p#ps) x =
   (let (a,b) = p in if a=x then Some b else assoc ps x)"

text‹
  we can define the lookup function for tries. It descends into the trie
  the letters of the search string one by one. As
  on lists is simpler than on tries, let us express this as primitive
  on the search string argument:
 ›

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

text‹
  a first simple property we prove that looking up a string in the empty
  term‹Trie None []› always returns const‹None›. The proof merely
  the two cases whether the search string is empty or not:
 ›

lemma [simp]: "lookup (Trie None []) as = None"
apply(case_tac as, simp_all)
done

text‹
  begin to get interesting with the definition of an update function
  adds a new (string, value) pair to a trie, overwriting the old value
  with that string:
 ›

primrec update:: "('a,'v)trie ==> 'a list ==> 'v ==> ('a,'v)trie" where
"update t [] v = Trie (Some v) (alist t)" |
"update t (a#as) v =
   (let tt = (case assoc (alist t) a of
                None ==> Trie None [] | Some at ==> at)
    in Trie (value t) ((a,update tt as v) # alist t))"

text‹\noindent
  base case is obvious. In the recursive case the subtrie
 term‹tt› associated with the first letter term‹a› is extracted,
  updated, and then placed in front of the association list.
  old subtrie associated with term‹a› is still in the association list
  no longer accessible via const‹assoc›. Clearly, there is room here for
 !

  we start on any proofs about const‹update› we tell the simplifier to
  all ‹let›s and to split all ‹case›-constructs over
 :
 ›

declare Let_def[simp] option.split[split]

text‹\noindent
  reason becomes clear when looking (probably after a failed proof
 ) at the body of const‹update›: it contains both
 ‹let› and a case distinction over type ‹option›.

  main goal is to prove the correct interaction of const‹update› and
 const‹lookup›:
 ›

theorem "∀t v bs. lookup (update t as v) bs =
                    (if as=bs then Some v else lookup t bs)"

txt‹\noindent
  plan is to induct on term‹as›; hence the remaining variables are
 . From the definitions it is clear that induction on either
 term‹as› or term‹bs› is required. The choice of term‹as› is
  by the intuition that simplification of const‹lookup› might be easier
  const‹update› has already been simplified, which can only happen if
 term‹as› is instantiated.
  start of the proof is conventional:
 ›
apply(induct_tac as, auto)

txt‹\noindent
 , this time we are left with three intimidating looking subgoals:
 begin{isabelle}
 1.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline
 2.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline
 3.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs
 end{isabelle}
 , if we want to make headway we have to instantiate term‹bs› as
  now. It turns out that instead of induction, case distinction
 :
 ›
apply(case_tac[!] bs, auto)
done

text‹\noindent
 index{subgoal numbering}%
  methods ending in ‹tac› take an optional first argument that
  the range of subgoals they are applied to, where ‹[!]› means
  subgoals, i.e.\ ‹[1-3]› in our case. Individual subgoal numbers,
 .g. ‹[2]› are also allowed.

  proof may look surprisingly straightforward. However, note that this
  at a cost: the proof script is unreadable because the intermediate
  states are invisible, and we rely on the (possibly brittle) magic of
 ‹auto› (‹simp_all› will not do --- try it) to split the subgoals
  the induction up in such a way that case distinction on term‹bs› makes
  and solves the proof.

 begin{exercise}
 Modify const‹update› (and its type) such that it allows both insertion and
 deletion of entries with a single function. Prove the corresponding version
 of the main theorem above.
 Optimize your function such that it shrinks tries after
 deletion if possible.
 end{exercise}

 begin{exercise}
 Write an improved version of const‹update› that does not suffer from the
 space leak (pointed out above) caused by not deleting overwritten entries
 from the association list. Prove the main theorem for your improved
 const‹update›.
 end{exercise}

 begin{exercise}
 Conceptually, each node contains a mapping from letters to optional
 subtries. Above we have implemented this by means of an association
 list. Replay the development replacing 🍋‹('a * ('a,'v)trie)list›
 with 🍋‹'a ==> ('a,'v)trie option›.
 end{exercise}

 ›

(*<*)

(* Exercise 1. Solution by Getrud Bauer *)

primrec update1 :: "('a, 'v) trie ==> 'a list ==> 'v option ==> ('a, 'v) trie"
where
  "update1 t [] vo = Trie vo (alist t)" |
  "update1 t (a#as) vo =
     (let tt = (case assoc (alist t) a of
                  None ==> Trie None []
                | Some at ==> at)
      in Trie (value t) ((a, update1 tt as vo) # alist t))"

theorem [simp]: "∀t v bs. lookup (update1 t as v) bs =
                    (if as = bs then v else lookup t bs)"
apply (induct_tac as, auto)
apply (case_tac[!] bs, auto)
done


(* Exercise 2. Solution by Getrud Bauer *)

primrec overwrite :: "'a ==> 'b ==> ('a * 'b) list ==> ('a * 'b) list" where
"overwrite a v [] = [(a,v)]" |
"overwrite a v (p#ps) = (if a = fst p then (a,v)#ps else p # overwrite a v ps)"

lemma [simp]: "∀ a v b. assoc (overwrite a v ps) b = assoc ((a,v)#ps) b"
apply (induct_tac ps, auto)
apply (case_tac[!] a)
done

primrec update2 :: "('a, 'v) trie ==> 'a list ==> 'v option ==> ('a, 'v) trie"
where
  "update2 t [] vo = Trie vo (alist t)" |
  "update2 t (a#as) vo =
     (let tt = (case assoc (alist t) a of
                  None ==> Trie None []
                | Some at ==> at)
      in Trie (value t) (overwrite a (update2 tt as vo) (alist t)))" 

theorem "∀t v bs. lookup (update2 t as vo) bs =
                    (if as = bs then vo else lookup t bs)"
apply (induct_tac as, auto)
apply (case_tac[!] bs, auto)
done


(* Exercise 3. Solution by Getrud Bauer *)
datatype ('a,dead 'v) triem = Triem  "'v option" "'a ==> ('a,'v) triem option"

primrec valuem :: "('a, 'v) triem ==> 'v option" where
"valuem (Triem ov m) = ov"

primrec mapping :: "('a,'v) triem ==> 'a ==> ('a, 'v) triem option" where
"mapping (Triem ov m) = m"

primrec lookupm :: "('a,'v) triem ==> 'a list ==> 'v option" where
  "lookupm t [] = valuem t" |
  "lookupm t (a#as) = (case mapping t a of
                        None ==> None
                      | Some at ==> lookupm at as)"

lemma [simp]: "lookupm (Triem None (λc. None)) as = None"
apply (case_tac as, simp_all)
done

primrec updatem :: "('a,'v)triem ==> 'a list ==> 'v ==> ('a,'v)triem" where
  "updatem t [] v = Triem (Some v) (mapping t)" |
  "updatem t (a#as) v =
     (let tt = (case mapping t a of
                  None ==> Triem None (λc. None)
                | Some at ==> at)
      in Triem (valuem t)
              (λc. if c = a then Some (updatem tt as v) else mapping t c))"

theorem "∀t v bs. lookupm (updatem t as v) bs =
                    (if as = bs then Some v else lookupm t bs)"
apply (induct_tac as, auto)
apply (case_tac[!] bs, auto)
done

end
(*>*)