Theory Trie2

(* Title: Adaptation of Trie Implementation
   Author: Peter Gammie < peteg42 at gmail dot com >
*)

(*<*)
theory Trie2 imports
  MapOps
  ODList
  Trie.Trie
begin
(*>*)

definition
  trie_update_with :: "'key list ⇒ 'val ⇒ ('val ⇒ 'val) ⇒ ('key, 'val) trie ⇒ ('key, 'val) trie"
where
  "trie_update_with ks v f ≡ update_with_trie ks (%vo. f(case vo of None ⇒ v | Some v ⇒ v))"

lemma [simp]:
  "trie_update_with [] v f (Trie vo ts) =
    Trie (Some (f (case vo of None ⇒ v | Some v' ⇒ v'))) ts"
by(simp add: trie_update_with_def)

lemma [simp]:
  "trie_update_with (k#ks) v f (Trie vo ts) =
    Trie vo (AList.update_with_aux empty_trie k (trie_update_with ks v f) ts)"
by(simp add: trie_update_with_def empty_trie_def)

abbreviation
  trie_update_with' :: "'k list ⇒ ('k, 'v) trie ⇒ 'v ⇒ ('v ⇒ 'v) ⇒ ('k, 'v) trie"
where
  "trie_update_with' ≡ (λk m v f. trie_update_with k v f m)"

definition
  trie_update :: "'key list ⇒ 'val ⇒ ('key, 'val) trie ⇒ ('key, 'val) trie"
where
  "trie_update k v t = trie_update_with k v (λv'. v) t"

text ‹@{term "trie_lookup"}›

lemma lookup_empty_trie [simp]: "lookup_trie empty_trie ks = None"
by (cases ks) (simp_all)

lemma lookup_trie_update_with:
  "lookup_trie (trie_update_with ks v f t) ks'
 = (if ks = ks' then Some (f (case lookup_trie t ks of None ⇒ v | Some v' ⇒ v')) else lookup_trie t ks')"
proof(induct ks "(%vo. f(case vo of None ⇒ v | Some v ⇒ v))" t arbitrary: v ks' rule: update_with_trie.induct)
  case (1 v ps vo ks')
  show ?case by (fastforce simp add: neq_Nil_conv dest: not_sym)
next
  case (2 k ks v ps vo ks')
  show ?case by(cases ks')(auto simp add: map_of_update_with_aux "2" empty_trie_def split: option.split)
qed

lemma lookup_trie_update:
  "lookup_trie (trie_update ks v t) ks' = (if ks = ks' then Some v else lookup_trie t ks')"
  unfolding trie_update_def by (auto simp add: lookup_trie_update_with)

text‹@{term "MapOps"}›

definition
  trie_MapOps :: "(('k, 'e) trie, 'k list, 'e) MapOps"
where
  "trie_MapOps ≡
     ⦇ MapOps.empty = empty_trie,
       lookup = lookup_trie,
       update = trie_update ⦈"

lemma trie_MapOps[intro, simp]:
  "inj_on α { x . α x ∈ d } ⟹ MapOps α d trie_MapOps"
  apply rule
  unfolding trie_MapOps_def
  apply (auto dest: inj_onD simp add: lookup_trie_update)
  done

definition
  "trie_odlist_lookup = (λM. lookup_trie M ∘ toList)"

definition
  "trie_odlist_update = (λk v. trie_update (toList k) v)"

definition
  trie_odlist_update_with :: "('k :: linorder) odlist ⇒ ('k, 'v) trie ⇒ 'v ⇒ ('v ⇒ 'v) ⇒ ('k, 'v) trie"
where
  "trie_odlist_update_with = (λk m v f. trie_update_with (toList k) v f m)"

definition
  trie_odlist_MapOps :: "(('k, 'e) trie, ('k ::linorder) odlist, 'e) MapOps"
where
  "trie_odlist_MapOps ≡
     ⦇ MapOps.empty = empty_trie,
       lookup = trie_odlist_lookup,
       update = trie_odlist_update ⦈"

lemma trie_odlist_MapOps[intro, simp]:
  "inj_on α { x . α x ∈ d } ⟹ MapOps α d trie_odlist_MapOps"
  apply rule
  unfolding trie_odlist_MapOps_def trie_odlist_lookup_def trie_odlist_update_def
  apply (auto dest: inj_onD simp add: lookup_trie_update)
  done

(*<*)
end
(*>*)