Theory Tries_Binary

(* Author: Tobias Nipkow *)

section "Binary Tries and Patricia Tries"

theory Tries_Binary
imports Set_Specs
begin

hide_const (open) insert

declare Let_def[simp]

fun sel2 :: "bool ⇒ 'a * 'a ⇒ 'a" where
"sel2 b (a1,a2) = (if b then a2 else a1)"

fun mod2 :: "('a ⇒ 'a) ⇒ bool ⇒ 'a * 'a ⇒ 'a * 'a" where
"mod2 f b (a1,a2) = (if b then (a1,f a2) else (f a1,a2))"


subsection "Trie"

datatype trie = Lf | Nd bool "trie * trie"

fun isin :: "trie ⇒ bool list ⇒ bool" where
"isin Lf ks = False" |
"isin (Nd b lr) ks =
   (case ks of
      [] ⇒ b |
      k#ks ⇒ isin (sel2 k lr) ks)"

fun insert :: "bool list ⇒ trie ⇒ trie" where
"insert [] Lf = Nd True (Lf,Lf)" |
"insert [] (Nd b lr) = Nd True lr" |
"insert (k#ks) Lf = Nd False (mod2 (insert ks) k (Lf,Lf))" |
"insert (k#ks) (Nd b lr) = Nd b (mod2 (insert ks) k lr)"

lemma isin_insert: "isin (insert as t) bs = (as = bs ∨ isin t bs)"
apply(induction as t arbitrary: bs rule: insert.induct)
apply (auto split: list.splits if_splits)
done

text ‹A simple implementation of delete; does not shrink the trie!›

fun delete0 :: "bool list ⇒ trie ⇒ trie" where
"delete0 ks Lf = Lf" |
"delete0 ks (Nd b lr) =
   (case ks of
      [] ⇒ Nd False lr |
      k#ks' ⇒ Nd b (mod2 (delete0 ks') k lr))"

lemma isin_delete0: "isin (delete0 as t) bs = (as ≠ bs ∧ isin t bs)"
apply(induction as t arbitrary: bs rule: delete0.induct)
apply (auto split: list.splits if_splits)
done

text ‹Now deletion with shrinking:›

fun node :: "bool ⇒ trie * trie ⇒ trie" where
"node b lr = (if ¬ b ∧ lr = (Lf,Lf) then Lf else Nd b lr)"

fun delete :: "bool list ⇒ trie ⇒ trie" where
"delete ks Lf = Lf" |
"delete ks (Nd b lr) =
   (case ks of
      [] ⇒ node False lr |
      k#ks' ⇒ node b (mod2 (delete ks') k lr))"

lemma isin_delete: "isin (delete as t) bs = (as ≠ bs ∧ isin t bs)"
apply(induction as t arbitrary: bs rule: delete.induct)
 apply simp
apply (auto split: list.splits if_splits)
  apply (metis isin.simps(1))
 apply (metis isin.simps(1))
  done

definition set_trie :: "trie ⇒ bool list set" where
"set_trie t = {xs. isin t xs}"

lemma set_trie_insert: "set_trie(insert xs t) = set_trie t ∪ {xs}"
by(auto simp add: isin_insert set_trie_def)

interpretation S: Set
where empty = Lf and isin = isin and insert = insert and delete = delete
and set = set_trie and invar = "λt. True"
proof (standard, goal_cases)
  case 1 show ?case by (simp add: set_trie_def)
next
  case 2 thus ?case by(simp add: set_trie_def)
next
  case 3 thus ?case by(auto simp: set_trie_insert)
next
  case 4 thus ?case by(auto simp: isin_delete set_trie_def)
qed (rule TrueI)+


subsection "Patricia Trie"

datatype ptrie = LfP | NdP "bool list" bool "ptrie * ptrie"

fun isinP :: "ptrie ⇒ bool list ⇒ bool" where
"isinP LfP ks = False" |
"isinP (NdP ps b lr) ks =
  (let n = length ps in
   if ps = take n ks
   then case drop n ks of [] ⇒ b | k#ks' ⇒ isinP (sel2 k lr) ks'
   else False)"

fun split where
"split [] ys = ([],[],ys)" |
"split xs [] = ([],xs,[])" |
"split (x#xs) (y#ys) =
  (if x≠y then ([],x#xs,y#ys)
   else let (ps,xs',ys') = split xs ys in (x#ps,xs',ys'))"


lemma mod2_cong[fundef_cong]:
  "⟦ lr = lr'; k = k'; ⋀a b. lr'=(a,b) ⟹ f (a) = f' (a) ; ⋀a b. lr'=(a,b) ⟹ f (b) = f' (b) ⟧
  ⟹ mod2 f k lr= mod2 f' k' lr'"
by(cases lr, cases lr', auto)

fun insertP :: "bool list ⇒ ptrie ⇒ ptrie" where
"insertP ks LfP  = NdP ks True (LfP,LfP)" |
"insertP ks (NdP ps b lr) =
  (case split ks ps of
     (qs,k#ks',p#ps') ⇒
       let tp = NdP ps' b lr; tk = NdP ks' True (LfP,LfP) in
       NdP qs False (if k then (tp,tk) else (tk,tp)) |
     (qs,k#ks',[]) ⇒
       NdP ps b (mod2 (insertP ks') k lr) |
     (qs,[],p#ps') ⇒
       let t = NdP ps' b lr in
       NdP qs True (if p then (LfP,t) else (t,LfP)) |
     (qs,[],[]) ⇒ NdP ps True lr)"


fun nodeP :: "bool list ⇒ bool ⇒ ptrie * ptrie ⇒ ptrie" where
"nodeP ps b lr = (if ¬ b ∧ lr = (LfP,LfP) then LfP else NdP ps b lr)"

fun deleteP :: "bool list ⇒ ptrie ⇒ ptrie" where
"deleteP ks LfP  = LfP" |
"deleteP ks (NdP ps b lr) =
  (case split ks ps of
     (qs,ks',p#ps') ⇒ NdP ps b lr |
     (qs,k#ks',[]) ⇒ nodeP ps b (mod2 (deleteP ks') k lr) |
     (qs,[],[]) ⇒ nodeP ps False lr)"


subsubsection ‹Functional Correctness›

text ‹First step: @{typ ptrie} implements @{typ trie} via the abstraction function ‹abs_ptrie›:›

fun prefix_trie :: "bool list ⇒ trie ⇒ trie" where
"prefix_trie [] t = t" |
"prefix_trie (k#ks) t =
  (let t' = prefix_trie ks t in Nd False (if k then (Lf,t') else (t',Lf)))"

fun abs_ptrie :: "ptrie ⇒ trie" where
"abs_ptrie LfP = Lf" |
"abs_ptrie (NdP ps b (l,r)) = prefix_trie ps (Nd b (abs_ptrie l, abs_ptrie r))"


text ‹Correctness of @{const isinP}:›

lemma isin_prefix_trie:
  "isin (prefix_trie ps t) ks
   = (ps = take (length ps) ks ∧ isin t (drop (length ps) ks))"
apply(induction ps arbitrary: ks)
apply(auto split: list.split)
done

lemma isinP:
  "isinP t ks = isin (abs_ptrie t) ks"
apply(induction t arbitrary: ks rule: abs_ptrie.induct)
 apply(auto simp: isin_prefix_trie split: list.split)
done


text ‹Correctness of @{const insertP}:›

lemma prefix_trie_Lfs: "prefix_trie ks (Nd True (Lf,Lf)) = insert ks Lf"
apply(induction ks)
apply auto
done

lemma insert_prefix_trie_same:
  "insert ps (prefix_trie ps (Nd b lr)) = prefix_trie ps (Nd True lr)"
apply(induction ps)
apply auto
done

lemma insert_append: "insert (ks @ ks') (prefix_trie ks t) = prefix_trie ks (insert ks' t)"
apply(induction ks)
apply auto
done

lemma prefix_trie_append: "prefix_trie (ps @ qs) t = prefix_trie ps (prefix_trie qs t)"
apply(induction ps)
apply auto
done

lemma split_if: "split ks ps = (qs, ks', ps') ⟹
  ks = qs @ ks' ∧ ps = qs @ ps' ∧ (ks' ≠ [] ∧ ps' ≠ [] ⟶ hd ks' ≠ hd ps')"
apply(induction ks ps arbitrary: qs ks' ps' rule: split.induct)
apply(auto split: prod.splits if_splits)
done

lemma abs_ptrie_insertP:
  "abs_ptrie (insertP ks t) = insert ks (abs_ptrie t)"
apply(induction t arbitrary: ks)
apply(auto simp: prefix_trie_Lfs insert_prefix_trie_same insert_append prefix_trie_append
           dest!: split_if split: list.split prod.split if_splits)
done


text ‹Correctness of @{const deleteP}:›

lemma prefix_trie_Lf: "prefix_trie xs t = Lf ⟷ xs = [] ∧ t = Lf"
by(cases xs)(auto)

lemma abs_ptrie_Lf: "abs_ptrie t = Lf ⟷ t = LfP"
by(cases t) (auto simp: prefix_trie_Lf)

lemma delete_prefix_trie:
  "delete xs (prefix_trie xs (Nd b (l,r)))
   = (if (l,r) = (Lf,Lf) then Lf else prefix_trie xs (Nd False (l,r)))"
by(induction xs)(auto simp: prefix_trie_Lf)

lemma delete_append_prefix_trie:
  "delete (xs @ ys) (prefix_trie xs t)
   = (if delete ys t = Lf then Lf else prefix_trie xs (delete ys t))"
by(induction xs)(auto simp: prefix_trie_Lf)

lemma delete_abs_ptrie:
  "delete ks (abs_ptrie t) = abs_ptrie (deleteP ks t)"
apply(induction t arbitrary: ks)
apply(auto simp: delete_prefix_trie delete_append_prefix_trie
        prefix_trie_append prefix_trie_Lf abs_ptrie_Lf
        dest!: split_if split: if_splits list.split prod.split)
done


text ‹The overall correctness proof. Simply composes correctness lemmas.›

definition set_ptrie :: "ptrie ⇒ bool list set" where
"set_ptrie = set_trie o abs_ptrie"

lemma set_ptrie_insertP: "set_ptrie (insertP xs t) = set_ptrie t ∪ {xs}"
by(simp add: abs_ptrie_insertP set_trie_insert set_ptrie_def)

interpretation SP: Set
where empty = LfP and isin = isinP and insert = insertP and delete = deleteP
and set = set_ptrie and invar = "λt. True"
proof (standard, goal_cases)
  case 1 show ?case by (simp add: set_ptrie_def set_trie_def)
next
  case 2 thus ?case by(simp add: isinP set_ptrie_def set_trie_def)
next
  case 3 thus ?case by (auto simp: set_ptrie_insertP)
next
  case 4 thus ?case
    by(auto simp: isin_delete set_ptrie_def set_trie_def simp flip: delete_abs_ptrie)
qed (rule TrueI)+

end