Theory Trie

theory Trie
imports Set_Specs
(* Author: Tobias Nipkow *)

section ‹Trie and Patricia Trie Implementations of \mbox{‹bool list set›}›

theory Trie
imports Set_Specs
begin

hide_const (open) insert

declare Let_def[simp]


subsection "Trie"

datatype trie = Leaf | Node bool "trie * trie"

text ‹The pairing allows things like ‹Node b (if … then (l,r) else (r,l))›.›

fun isin :: "trie ⇒ bool list ⇒ bool" where
"isin Leaf ks = False" |
"isin (Node b (l,r)) ks =
   (case ks of
      [] ⇒ b |
      k#ks ⇒ isin (if k then r else l) ks)"

fun insert :: "bool list ⇒ trie ⇒ trie" where
"insert [] Leaf = Node True (Leaf,Leaf)" |
"insert [] (Node b lr) = Node True lr" |
"insert (k#ks) Leaf =
  Node False (if k then (Leaf, insert ks Leaf)
                   else (insert ks Leaf, Leaf))" |
"insert (k#ks) (Node b (l,r)) =
  Node b (if k then (l, insert ks r)
               else (insert ks l, r))"

fun shrink_Node :: "bool ⇒ trie * trie ⇒ trie" where
"shrink_Node b lr = (if ¬ b ∧ lr = (Leaf,Leaf) then Leaf else Node b lr)"

fun delete :: "bool list ⇒ trie ⇒ trie" where
"delete ks Leaf = Leaf" |
"delete ks (Node b (l,r)) =
   (case ks of
      [] ⇒ shrink_Node False (l,r) |
      k#ks' ⇒ shrink_Node b (if k then (l, delete ks' r) else (delete ks' l, r)))"

fun invar :: "trie ⇒ bool" where
"invar Leaf = True" |
"invar (Node b (l,r)) = ((¬ b ⟶ l ≠ Leaf ∨ r ≠ Leaf) ∧ invar l ∧ invar r)"


subsubsection ‹Functional Correctness›

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)
done

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; fastforce)
done

lemma insert_not_Leaf: "insert ks t ≠ Leaf"
by(cases "(ks,t)" rule: insert.cases) auto

lemma invar_insert: "invar t ⟹ invar (insert ks t)"
by(induction ks t rule: insert.induct)(auto simp: insert_not_Leaf)

lemma invar_delete: "invar t ⟹ invar (delete ks t)"
by(induction ks t rule: delete.induct)(auto split: list.split)

interpretation T: Set
where empty = Leaf and insert = insert and delete = delete and isin = isin
and set = "λt. {x. isin t x}" and invar = invar
proof (standard, goal_cases)
  case 1 thus ?case by simp
next
  case 2 thus ?case by simp
next
  case 3 thus ?case by (auto simp add: isin_insert)
next
  case 4 thus ?case by (auto simp add: isin_delete)
next
  case 5 thus ?case by simp
next
  case 6 thus ?case by (auto simp add: invar_insert)
next
  case 7 thus ?case by (auto simp add: invar_delete)
qed


subsection "Patricia Trie"

datatype trieP = LeafP | NodeP "bool list" bool "trieP * trieP"

fun isinP :: "trieP ⇒ bool list ⇒ bool" where
"isinP LeafP ks = False" |
"isinP (NodeP ps b (l,r)) ks =
  (let n = length ps in
   if ps = take n ks
   then case drop n ks of [] ⇒ b | k#ks' ⇒ isinP (if k then r else l) ks'
   else False)"

text ‹‹split xs ys = (zs, xs', ys')› iff
  ‹zs› is the longest common prefix of ‹xs› and ‹ys› and
  ‹xs = zs @ xs'› and ‹ys = zs @ ys'››
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'))"

fun insertP :: "bool list ⇒ trieP ⇒ trieP" where
"insertP ks LeafP  = NodeP ks True (LeafP,LeafP)" |
"insertP ks (NodeP ps b (l,r)) =
  (case split ks ps of
     (qs,k#ks',p#ps') ⇒
       let tp = NodeP ps' b (l,r); tk = NodeP ks' True (LeafP,LeafP)
       in NodeP qs False (if k then (tp,tk) else (tk,tp)) |
     (qs,k#ks',[]) ⇒
       NodeP ps b (if k then (l,insertP ks' r) else (insertP ks' l, r)) |
     (qs,[],p#ps') ⇒
       let t = NodeP ps' b (l,r)
       in NodeP qs True (if p then (LeafP, t) else (t, LeafP)) |
     (qs,[],[]) ⇒ NodeP ps True (l,r))"

fun shrink_NodeP where
"shrink_NodeP ps b lr = (if b then NodeP ps b lr else
  case lr of
     (LeafP, LeafP) ⇒ LeafP |
     (LeafP, NodeP ps' b' lr') ⇒ NodeP (ps @ True # ps') b' lr' |
     (NodeP ps' b' lr', LeafP) ⇒ NodeP (ps @ False # ps') b' lr' |
     _ ⇒ NodeP ps b lr)"

fun deleteP :: "bool list ⇒ trieP ⇒ trieP" where
"deleteP ks LeafP  = LeafP" |
"deleteP ks (NodeP ps b (l,r)) =
  (case split ks ps of
     (qs,_,p#ps') ⇒ NodeP ps b (l,r) |
     (qs,k#ks',[]) ⇒
       shrink_NodeP ps b (if k then (l, deleteP ks' r) else (deleteP ks' l, r)) |
     (qs,[],[]) ⇒ shrink_NodeP ps False (l,r))"

fun invarP :: "trieP ⇒ bool" where
"invarP LeafP = True" |
"invarP (NodeP ps b (l,r)) = ((¬b ⟶ l ≠ LeafP ∨ r ≠ LeafP) ∧ invarP l ∧ invarP r)"

text ‹The abstraction function(s):›

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

fun abs_trieP :: "trieP ⇒ trie" where
"abs_trieP LeafP = Leaf" |
"abs_trieP (NodeP ps b (l,r)) = prefix_trie ps (Node b (abs_trieP l, abs_trieP r))"


subsubsection ‹Functional Correctness›

text ‹IsinP:›

lemma isin_prefix_trie: "isin (prefix_trie ps t) ks =
  (length ks ≥ length ps ∧
  (let n = length ps in ps = take n ks ∧ isin t (drop n ks)))"
by(induction ps arbitrary: ks)(auto split: list.split)

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

text ‹Insert:›

lemma prefix_trie_Leaf_iff: "prefix_trie ps t = Leaf ⟷ t = Leaf"
by (induction ps) auto

lemma prefix_trie_Leafs: "prefix_trie ks (Node True (Leaf,Leaf)) = insert ks Leaf"
by(induction ks) (auto simp: prefix_trie_Leaf_iff)

lemma prefix_trie_Leaf: "prefix_trie ps Leaf = Leaf"
by(induction ps) auto

lemma insert_append: "insert (ks @ ks') (prefix_trie ks t) = prefix_trie ks (insert ks' t)"
by(induction ks) (auto simp: prefix_trie_Leaf_iff insert_not_Leaf prefix_trie_Leaf)

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

lemma split_iff: "split xs ys = (zs, xs', ys') ⟷
  xs = zs @ xs' ∧ ys = zs @ ys' ∧ (xs' ≠ [] ∧ ys' ≠ [] ⟶ hd xs' ≠ hd ys')"
proof(induction xs ys arbitrary: zs xs' ys' rule: split.induct)
  case 1 thus ?case by auto
next
  case 2 thus ?case by auto
next
  case 3 thus ?case by(clarsimp simp: Cons_eq_append_conv split: prod.splits if_splits) auto
qed

lemma abs_trieP_insertP:
  "abs_trieP (insertP ks t) = insert ks (abs_trieP t)"
apply(induction t arbitrary: ks)
apply(auto simp: prefix_trie_Leafs insert_append prefix_trie_append
        prefix_trie_Leaf_iff split_iff split: list.split prod.split)
done

corollary isinP_insertP: "isinP (insertP ks t) ks' = (ks=ks' ∨ isinP t ks')"
by (simp add: isin_insert isinP abs_trieP_insertP)

lemma insertP_not_LeafP: "insertP ks t ≠ LeafP"
apply(induction ks t rule: insertP.induct)
apply(auto split: prod.split list.split)
done

lemma invarP_insertP: "invarP t ⟹ invarP (insertP ks t)"
apply(induction ks t rule: insertP.induct)
apply(auto simp: insertP_not_LeafP split: prod.split list.split)
done

text ‹Delete:›

lemma invar_shrink_NodeP: "⟦ invarP l; invarP r ⟧ ⟹ invarP (shrink_NodeP ps b (l,r))"
by(auto split: trieP.split)

lemma invarP_deleteP: "invarP t ⟹ invarP (deleteP ks t)"
apply(induction t arbitrary: ks)
apply(auto simp: invar_shrink_NodeP split_iff simp del: shrink_NodeP.simps
           split!: list.splits prod.split if_splits)
done

lemma delete_append:
  "delete (ks @ ks') (prefix_trie ks t) = prefix_trie ks (delete ks' t)"
by(induction ks) auto

lemma abs_trieP_shrink_NodeP:
  "abs_trieP (shrink_NodeP ps b (l,r)) = prefix_trie ps (shrink_Node b (abs_trieP l, abs_trieP r))"
apply(induction ps arbitrary: b l r)
apply (auto simp: prefix_trie_Leaf prefix_trie_Leaf_iff prefix_trie_append
            split!: trieP.splits if_splits)
done

lemma abs_trieP_deleteP:
  "abs_trieP (deleteP ks t) = delete ks (abs_trieP t)"
apply(induction t arbitrary: ks)
apply(auto simp: prefix_trie_Leafs delete_append prefix_trie_Leaf
                 abs_trieP_shrink_NodeP prefix_trie_append split_iff
           simp del: shrink_NodeP.simps split!: list.split prod.split if_splits)
done

corollary isinP_deleteP: "isinP (deleteP ks t) ks' = (ks≠ks' ∧ isinP t ks')"
by (simp add: isin_delete isinP abs_trieP_deleteP)

interpretation PT: Set
where empty = LeafP and insert = insertP and delete = deleteP
and isin = isinP and set = "λt. {x. isinP t x}" and invar = invarP
proof (standard, goal_cases)
  case 1 thus ?case by (simp)
next
  case 2 thus ?case by (simp)
next
  case 3 thus ?case by (auto simp add: isinP_insertP)
next
  case 4 thus ?case by (auto simp add: isinP_deleteP)
next
  case 5 thus ?case by (simp)
next
  case 6 thus ?case by (simp add: invarP_insertP)
next
  case 7 thus ?case by (auto simp add: invarP_deleteP)
qed

end