Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Tries_Binary.thy Sprache: Isabelle

Original von: Isabelle^©

(* 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"

definition empty :: trie where
[simp]: "empty = Lf"

fun isin :: "trie \ bool list \ bool" where
"isin Lf ks = False" |
"isin (Nd b lr) ks =
   (case ks of
      [] \<Rightarrow> b |
      k#ks \<Rightarrow> 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 xs t) ys = (xs = ys \ isin t ys)"
apply(induction xs t arbitrary: ys rule: insert.induct)
apply (auto split: list.splits if_splits)
done

text \<open>A simple implementation of delete; does not shrink the trie!\<close>

fun delete0 :: "bool list \ trie \ trie" where
"delete0 ks Lf = Lf" |
"delete0 ks (Nd b lr) =
   (case ks of
      [] \<Rightarrow> 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 \<open>Now deletion with shrinking:\<close>

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
      [] \<Rightarrow> node False lr |
      k#ks' \ node b (mod2 (delete ks') k lr))"

lemma isin_delete: "isin (delete xs t) ys = (xs \ ys \ isin t ys)"
apply(induction xs t arbitrary: ys 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_empty: "set_trie empty = {}"
by(simp add: set_trie_def)

lemma set_trie_isin: "isin t xs = (xs \ set_trie t)"
by(simp add: set_trie_def)

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

lemma set_trie_delete: "set_trie(delete xs t) = set_trie t - {xs}"
by(auto simp add: isin_delete set_trie_def)

interpretation S: Set
where empty = empty 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 (rule set_trie_empty)
next
  case 2 show ?case by(rule set_trie_isin)
next
  case 3 thus ?case by(auto simp: set_trie_insert)
next
  case 4 show ?case by(rule set_trie_delete)
qed (rule TrueI)+

subsection "Patricia Trie"

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

fun isinP :: "trieP \ 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 [] \<Rightarrow> b | k#ks' \<Rightarrow> isinP (sel2 k lr) ks'
   else False)"

definition emptyP :: trieP where
[simp]: "emptyP = LfP"

fun split where
"split [] ys = ([],[],ys)" |
"split xs [] = ([],xs,[])" |
"split (x#xs) (y#ys) =
  (if x\<noteq>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) \
  \<Longrightarrow> mod2 f k lr= mod2 f' k' lr'"
by(cases lr, cases lr', auto)

fun insertP :: "bool list \ trieP \ trieP" 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') \<Rightarrow>
       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,[],[]) \<Rightarrow> NdP ps True lr)"

fun nodeP :: "bool list \ bool \ trieP * trieP \ trieP" where
"nodeP ps b lr = (if \ b \ lr = (LfP,LfP) then LfP else NdP ps b lr)"

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

subsubsection \<open>Functional Correctness\<close>

text \<open>First step: @{typ trieP} implements @{typ trie} via the abstraction function \<open>abs_trieP\<close>:\<close>

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_trieP :: "trieP \ trie" where
"abs_trieP LfP = Lf" |
"abs_trieP (NdP ps b (l,r)) = prefix_trie ps (Nd b (abs_trieP l, abs_trieP r))"

text \<open>Correctness of @{const isinP}:\<close>

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

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

text \<open>Correctness of @{const insertP}:\<close>

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_trieP_insertP:
  "abs_trieP (insertP ks t) = insert ks (abs_trieP 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 \<open>Correctness of @{const deleteP}:\<close>

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

lemma abs_trieP_Lf: "abs_trieP 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_trieP:
  "delete ks (abs_trieP t) = abs_trieP (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_trieP_Lf
        dest!: split_if split: if_splits list.split prod.split)
done

text \<open>The overall correctness proof. Simply composes correctness lemmas.\<close>

definition set_trieP :: "trieP \ bool list set" where
"set_trieP = set_trie o abs_trieP"

lemma isinP_set_trieP: "isinP t xs = (xs \ set_trieP t)"
by(simp add: abs_trieP_isinP set_trie_isin set_trieP_def)

lemma set_trieP_insertP: "set_trieP (insertP xs t) = set_trieP t \ {xs}"
by(simp add: abs_trieP_insertP set_trie_insert set_trieP_def)

lemma set_trieP_deleteP: "set_trieP (deleteP xs t) = set_trieP t - {xs}"
by(auto simp: set_trie_delete set_trieP_def simp flip: delete_abs_trieP)

interpretation SP: Set
where empty = emptyP and isin = isinP and insert = insertP and delete = deleteP
and set = set_trieP and invar = "\t. True"
proof (standard, goal_cases)
  case 1 show ?case by (simp add: set_trieP_def set_trie_def)
next
  case 2 show ?case by(rule isinP_set_trieP)
next
  case 3 thus ?case by (auto simp: set_trieP_insertP)
next
  case 4 thus ?case by(auto simp: set_trieP_deleteP)
qed (rule TrueI)+

end

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.