src/HOL/Data_Structures/Tries_Binary.thy
author nipkow
Tue May 14 17:21:13 2019 +0200 (5 weeks ago)
changeset 70268 81403d7b9038
parent 70267 9fa2cf7142b7
child 70269 40b6bc5a4721
permissions -rw-r--r--
tuned names
nipkow@70250
     1
(* Author: Tobias Nipkow *)
nipkow@70250
     2
nipkow@70250
     3
section "Binary Tries and Patricia Tries"
nipkow@70250
     4
nipkow@70250
     5
theory Tries_Binary
nipkow@70250
     6
imports Set_Specs
nipkow@70250
     7
begin
nipkow@70250
     8
nipkow@70250
     9
hide_const (open) insert
nipkow@70250
    10
nipkow@70250
    11
declare Let_def[simp]
nipkow@70250
    12
nipkow@70250
    13
fun sel2 :: "bool \<Rightarrow> 'a * 'a \<Rightarrow> 'a" where
nipkow@70250
    14
"sel2 b (a1,a2) = (if b then a2 else a1)"
nipkow@70250
    15
nipkow@70250
    16
fun mod2 :: "('a \<Rightarrow> 'a) \<Rightarrow> bool \<Rightarrow> 'a * 'a \<Rightarrow> 'a * 'a" where
nipkow@70250
    17
"mod2 f b (a1,a2) = (if b then (a1,f a2) else (f a1,a2))"
nipkow@70250
    18
nipkow@70250
    19
nipkow@70250
    20
subsection "Trie"
nipkow@70250
    21
nipkow@70250
    22
datatype trie = Lf | Nd bool "trie * trie"
nipkow@70250
    23
nipkow@70267
    24
definition empty :: trie where
nipkow@70267
    25
[simp]: "empty = Lf"
nipkow@70267
    26
nipkow@70250
    27
fun isin :: "trie \<Rightarrow> bool list \<Rightarrow> bool" where
nipkow@70250
    28
"isin Lf ks = False" |
nipkow@70250
    29
"isin (Nd b lr) ks =
nipkow@70250
    30
   (case ks of
nipkow@70250
    31
      [] \<Rightarrow> b |
nipkow@70250
    32
      k#ks \<Rightarrow> isin (sel2 k lr) ks)"
nipkow@70250
    33
nipkow@70250
    34
fun insert :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
nipkow@70250
    35
"insert [] Lf = Nd True (Lf,Lf)" |
nipkow@70250
    36
"insert [] (Nd b lr) = Nd True lr" |
nipkow@70250
    37
"insert (k#ks) Lf = Nd False (mod2 (insert ks) k (Lf,Lf))" |
nipkow@70250
    38
"insert (k#ks) (Nd b lr) = Nd b (mod2 (insert ks) k lr)"
nipkow@70250
    39
nipkow@70267
    40
lemma isin_insert: "isin (insert xs t) ys = (xs = ys \<or> isin t ys)"
nipkow@70267
    41
apply(induction xs t arbitrary: ys rule: insert.induct)
nipkow@70250
    42
apply (auto split: list.splits if_splits)
nipkow@70250
    43
done
nipkow@70250
    44
nipkow@70250
    45
text \<open>A simple implementation of delete; does not shrink the trie!\<close>
nipkow@70250
    46
nipkow@70250
    47
fun delete0 :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
nipkow@70250
    48
"delete0 ks Lf = Lf" |
nipkow@70250
    49
"delete0 ks (Nd b lr) =
nipkow@70250
    50
   (case ks of
nipkow@70250
    51
      [] \<Rightarrow> Nd False lr |
nipkow@70250
    52
      k#ks' \<Rightarrow> Nd b (mod2 (delete0 ks') k lr))"
nipkow@70250
    53
nipkow@70250
    54
lemma isin_delete0: "isin (delete0 as t) bs = (as \<noteq> bs \<and> isin t bs)"
nipkow@70250
    55
apply(induction as t arbitrary: bs rule: delete0.induct)
nipkow@70250
    56
apply (auto split: list.splits if_splits)
nipkow@70250
    57
done
nipkow@70250
    58
nipkow@70250
    59
text \<open>Now deletion with shrinking:\<close>
nipkow@70250
    60
nipkow@70250
    61
fun node :: "bool \<Rightarrow> trie * trie \<Rightarrow> trie" where
nipkow@70250
    62
"node b lr = (if \<not> b \<and> lr = (Lf,Lf) then Lf else Nd b lr)"
nipkow@70250
    63
nipkow@70250
    64
fun delete :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
nipkow@70250
    65
"delete ks Lf = Lf" |
nipkow@70250
    66
"delete ks (Nd b lr) =
nipkow@70250
    67
   (case ks of
nipkow@70250
    68
      [] \<Rightarrow> node False lr |
nipkow@70250
    69
      k#ks' \<Rightarrow> node b (mod2 (delete ks') k lr))"
nipkow@70250
    70
nipkow@70267
    71
lemma isin_delete: "isin (delete xs t) ys = (xs \<noteq> ys \<and> isin t ys)"
nipkow@70267
    72
apply(induction xs t arbitrary: ys rule: delete.induct)
nipkow@70250
    73
 apply simp
nipkow@70250
    74
apply (auto split: list.splits if_splits)
nipkow@70250
    75
  apply (metis isin.simps(1))
nipkow@70250
    76
 apply (metis isin.simps(1))
nipkow@70250
    77
  done
nipkow@70250
    78
nipkow@70250
    79
definition set_trie :: "trie \<Rightarrow> bool list set" where
nipkow@70250
    80
"set_trie t = {xs. isin t xs}"
nipkow@70250
    81
nipkow@70267
    82
lemma set_trie_empty: "set_trie empty = {}"
nipkow@70267
    83
by(simp add: set_trie_def)
nipkow@70267
    84
nipkow@70267
    85
lemma set_trie_isin: "isin t xs = (xs \<in> set_trie t)"
nipkow@70267
    86
by(simp add: set_trie_def)
nipkow@70267
    87
nipkow@70250
    88
lemma set_trie_insert: "set_trie(insert xs t) = set_trie t \<union> {xs}"
nipkow@70250
    89
by(auto simp add: isin_insert set_trie_def)
nipkow@70250
    90
nipkow@70267
    91
lemma set_trie_delete: "set_trie(delete xs t) = set_trie t - {xs}"
nipkow@70267
    92
by(auto simp add: isin_delete set_trie_def)
nipkow@70267
    93
nipkow@70250
    94
interpretation S: Set
nipkow@70267
    95
where empty = empty and isin = isin and insert = insert and delete = delete
nipkow@70250
    96
and set = set_trie and invar = "\<lambda>t. True"
nipkow@70250
    97
proof (standard, goal_cases)
nipkow@70267
    98
  case 1 show ?case by (rule set_trie_empty)
nipkow@70250
    99
next
nipkow@70267
   100
  case 2 show ?case by(rule set_trie_isin)
nipkow@70250
   101
next
nipkow@70250
   102
  case 3 thus ?case by(auto simp: set_trie_insert)
nipkow@70250
   103
next
nipkow@70267
   104
  case 4 show ?case by(rule set_trie_delete)
nipkow@70250
   105
qed (rule TrueI)+
nipkow@70250
   106
nipkow@70250
   107
nipkow@70250
   108
subsection "Patricia Trie"
nipkow@70250
   109
nipkow@70268
   110
datatype trieP = LfP | NdP "bool list" bool "trieP * trieP"
nipkow@70250
   111
nipkow@70268
   112
fun isinP :: "trieP \<Rightarrow> bool list \<Rightarrow> bool" where
nipkow@70250
   113
"isinP LfP ks = False" |
nipkow@70250
   114
"isinP (NdP ps b lr) ks =
nipkow@70250
   115
  (let n = length ps in
nipkow@70250
   116
   if ps = take n ks
nipkow@70250
   117
   then case drop n ks of [] \<Rightarrow> b | k#ks' \<Rightarrow> isinP (sel2 k lr) ks'
nipkow@70250
   118
   else False)"
nipkow@70250
   119
nipkow@70268
   120
definition emptyP :: trieP where
nipkow@70268
   121
[simp]: "emptyP = LfP"
nipkow@70268
   122
nipkow@70250
   123
fun split where
nipkow@70250
   124
"split [] ys = ([],[],ys)" |
nipkow@70250
   125
"split xs [] = ([],xs,[])" |
nipkow@70250
   126
"split (x#xs) (y#ys) =
nipkow@70250
   127
  (if x\<noteq>y then ([],x#xs,y#ys)
nipkow@70250
   128
   else let (ps,xs',ys') = split xs ys in (x#ps,xs',ys'))"
nipkow@70250
   129
nipkow@70250
   130
nipkow@70250
   131
lemma mod2_cong[fundef_cong]:
nipkow@70250
   132
  "\<lbrakk> lr = lr'; k = k'; \<And>a b. lr'=(a,b) \<Longrightarrow> f (a) = f' (a) ; \<And>a b. lr'=(a,b) \<Longrightarrow> f (b) = f' (b) \<rbrakk>
nipkow@70250
   133
  \<Longrightarrow> mod2 f k lr= mod2 f' k' lr'"
nipkow@70250
   134
by(cases lr, cases lr', auto)
nipkow@70250
   135
nipkow@70268
   136
nipkow@70268
   137
fun insertP :: "bool list \<Rightarrow> trieP \<Rightarrow> trieP" where
nipkow@70250
   138
"insertP ks LfP  = NdP ks True (LfP,LfP)" |
nipkow@70250
   139
"insertP ks (NdP ps b lr) =
nipkow@70250
   140
  (case split ks ps of
nipkow@70250
   141
     (qs,k#ks',p#ps') \<Rightarrow>
nipkow@70250
   142
       let tp = NdP ps' b lr; tk = NdP ks' True (LfP,LfP) in
nipkow@70250
   143
       NdP qs False (if k then (tp,tk) else (tk,tp)) |
nipkow@70250
   144
     (qs,k#ks',[]) \<Rightarrow>
nipkow@70250
   145
       NdP ps b (mod2 (insertP ks') k lr) |
nipkow@70250
   146
     (qs,[],p#ps') \<Rightarrow>
nipkow@70250
   147
       let t = NdP ps' b lr in
nipkow@70250
   148
       NdP qs True (if p then (LfP,t) else (t,LfP)) |
nipkow@70250
   149
     (qs,[],[]) \<Rightarrow> NdP ps True lr)"
nipkow@70250
   150
nipkow@70250
   151
nipkow@70268
   152
fun nodeP :: "bool list \<Rightarrow> bool \<Rightarrow> trieP * trieP \<Rightarrow> trieP" where
nipkow@70250
   153
"nodeP ps b lr = (if \<not> b \<and> lr = (LfP,LfP) then LfP else NdP ps b lr)"
nipkow@70250
   154
nipkow@70268
   155
fun deleteP :: "bool list \<Rightarrow> trieP \<Rightarrow> trieP" where
nipkow@70250
   156
"deleteP ks LfP  = LfP" |
nipkow@70250
   157
"deleteP ks (NdP ps b lr) =
nipkow@70250
   158
  (case split ks ps of
nipkow@70250
   159
     (qs,ks',p#ps') \<Rightarrow> NdP ps b lr |
nipkow@70250
   160
     (qs,k#ks',[]) \<Rightarrow> nodeP ps b (mod2 (deleteP ks') k lr) |
nipkow@70250
   161
     (qs,[],[]) \<Rightarrow> nodeP ps False lr)"
nipkow@70250
   162
nipkow@70250
   163
nipkow@70250
   164
subsubsection \<open>Functional Correctness\<close>
nipkow@70250
   165
nipkow@70268
   166
text \<open>First step: @{typ trieP} implements @{typ trie} via the abstraction function \<open>abs_trieP\<close>:\<close>
nipkow@70250
   167
nipkow@70250
   168
fun prefix_trie :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
nipkow@70250
   169
"prefix_trie [] t = t" |
nipkow@70250
   170
"prefix_trie (k#ks) t =
nipkow@70250
   171
  (let t' = prefix_trie ks t in Nd False (if k then (Lf,t') else (t',Lf)))"
nipkow@70250
   172
nipkow@70268
   173
fun abs_trieP :: "trieP \<Rightarrow> trie" where
nipkow@70268
   174
"abs_trieP LfP = Lf" |
nipkow@70268
   175
"abs_trieP (NdP ps b (l,r)) = prefix_trie ps (Nd b (abs_trieP l, abs_trieP r))"
nipkow@70250
   176
nipkow@70250
   177
nipkow@70250
   178
text \<open>Correctness of @{const isinP}:\<close>
nipkow@70250
   179
nipkow@70250
   180
lemma isin_prefix_trie:
nipkow@70250
   181
  "isin (prefix_trie ps t) ks
nipkow@70250
   182
   = (ps = take (length ps) ks \<and> isin t (drop (length ps) ks))"
nipkow@70250
   183
apply(induction ps arbitrary: ks)
nipkow@70250
   184
apply(auto split: list.split)
nipkow@70250
   185
done
nipkow@70250
   186
nipkow@70250
   187
lemma isinP:
nipkow@70268
   188
  "isinP t ks = isin (abs_trieP t) ks"
nipkow@70268
   189
apply(induction t arbitrary: ks rule: abs_trieP.induct)
nipkow@70250
   190
 apply(auto simp: isin_prefix_trie split: list.split)
nipkow@70250
   191
done
nipkow@70250
   192
nipkow@70250
   193
nipkow@70250
   194
text \<open>Correctness of @{const insertP}:\<close>
nipkow@70250
   195
nipkow@70250
   196
lemma prefix_trie_Lfs: "prefix_trie ks (Nd True (Lf,Lf)) = insert ks Lf"
nipkow@70250
   197
apply(induction ks)
nipkow@70250
   198
apply auto
nipkow@70250
   199
done
nipkow@70250
   200
nipkow@70250
   201
lemma insert_prefix_trie_same:
nipkow@70250
   202
  "insert ps (prefix_trie ps (Nd b lr)) = prefix_trie ps (Nd True lr)"
nipkow@70250
   203
apply(induction ps)
nipkow@70250
   204
apply auto
nipkow@70250
   205
done
nipkow@70250
   206
nipkow@70250
   207
lemma insert_append: "insert (ks @ ks') (prefix_trie ks t) = prefix_trie ks (insert ks' t)"
nipkow@70250
   208
apply(induction ks)
nipkow@70250
   209
apply auto
nipkow@70250
   210
done
nipkow@70250
   211
nipkow@70250
   212
lemma prefix_trie_append: "prefix_trie (ps @ qs) t = prefix_trie ps (prefix_trie qs t)"
nipkow@70250
   213
apply(induction ps)
nipkow@70250
   214
apply auto
nipkow@70250
   215
done
nipkow@70250
   216
nipkow@70250
   217
lemma split_if: "split ks ps = (qs, ks', ps') \<Longrightarrow>
nipkow@70250
   218
  ks = qs @ ks' \<and> ps = qs @ ps' \<and> (ks' \<noteq> [] \<and> ps' \<noteq> [] \<longrightarrow> hd ks' \<noteq> hd ps')"
nipkow@70250
   219
apply(induction ks ps arbitrary: qs ks' ps' rule: split.induct)
nipkow@70250
   220
apply(auto split: prod.splits if_splits)
nipkow@70250
   221
done
nipkow@70250
   222
nipkow@70268
   223
lemma abs_trieP_insertP:
nipkow@70268
   224
  "abs_trieP (insertP ks t) = insert ks (abs_trieP t)"
nipkow@70250
   225
apply(induction t arbitrary: ks)
nipkow@70250
   226
apply(auto simp: prefix_trie_Lfs insert_prefix_trie_same insert_append prefix_trie_append
nipkow@70250
   227
           dest!: split_if split: list.split prod.split if_splits)
nipkow@70250
   228
done
nipkow@70250
   229
nipkow@70250
   230
nipkow@70250
   231
text \<open>Correctness of @{const deleteP}:\<close>
nipkow@70250
   232
nipkow@70250
   233
lemma prefix_trie_Lf: "prefix_trie xs t = Lf \<longleftrightarrow> xs = [] \<and> t = Lf"
nipkow@70250
   234
by(cases xs)(auto)
nipkow@70250
   235
nipkow@70268
   236
lemma abs_trieP_Lf: "abs_trieP t = Lf \<longleftrightarrow> t = LfP"
nipkow@70250
   237
by(cases t) (auto simp: prefix_trie_Lf)
nipkow@70250
   238
nipkow@70250
   239
lemma delete_prefix_trie:
nipkow@70250
   240
  "delete xs (prefix_trie xs (Nd b (l,r)))
nipkow@70250
   241
   = (if (l,r) = (Lf,Lf) then Lf else prefix_trie xs (Nd False (l,r)))"
nipkow@70250
   242
by(induction xs)(auto simp: prefix_trie_Lf)
nipkow@70250
   243
nipkow@70250
   244
lemma delete_append_prefix_trie:
nipkow@70250
   245
  "delete (xs @ ys) (prefix_trie xs t)
nipkow@70250
   246
   = (if delete ys t = Lf then Lf else prefix_trie xs (delete ys t))"
nipkow@70250
   247
by(induction xs)(auto simp: prefix_trie_Lf)
nipkow@70250
   248
nipkow@70268
   249
lemma delete_abs_trieP:
nipkow@70268
   250
  "delete ks (abs_trieP t) = abs_trieP (deleteP ks t)"
nipkow@70250
   251
apply(induction t arbitrary: ks)
nipkow@70250
   252
apply(auto simp: delete_prefix_trie delete_append_prefix_trie
nipkow@70268
   253
        prefix_trie_append prefix_trie_Lf abs_trieP_Lf
nipkow@70250
   254
        dest!: split_if split: if_splits list.split prod.split)
nipkow@70250
   255
done
nipkow@70250
   256
nipkow@70250
   257
nipkow@70250
   258
text \<open>The overall correctness proof. Simply composes correctness lemmas.\<close>
nipkow@70250
   259
nipkow@70268
   260
definition set_trieP :: "trieP \<Rightarrow> bool list set" where
nipkow@70268
   261
"set_trieP = set_trie o abs_trieP"
nipkow@70250
   262
nipkow@70268
   263
lemma set_trieP_insertP: "set_trieP (insertP xs t) = set_trieP t \<union> {xs}"
nipkow@70268
   264
by(simp add: abs_trieP_insertP set_trie_insert set_trieP_def)
nipkow@70250
   265
nipkow@70250
   266
interpretation SP: Set
nipkow@70268
   267
where empty = emptyP and isin = isinP and insert = insertP and delete = deleteP
nipkow@70268
   268
and set = set_trieP and invar = "\<lambda>t. True"
nipkow@70250
   269
proof (standard, goal_cases)
nipkow@70268
   270
  case 1 show ?case by (simp add: set_trieP_def set_trie_def)
nipkow@70250
   271
next
nipkow@70268
   272
  case 2 thus ?case by(simp add: isinP set_trieP_def set_trie_def)
nipkow@70250
   273
next
nipkow@70268
   274
  case 3 thus ?case by (auto simp: set_trieP_insertP)
nipkow@70250
   275
next
nipkow@70250
   276
  case 4 thus ?case
nipkow@70268
   277
    by(auto simp: isin_delete set_trieP_def set_trie_def simp flip: delete_abs_trieP)
nipkow@70250
   278
qed (rule TrueI)+
nipkow@70250
   279
nipkow@70250
   280
end