tuned names
authornipkow
Tue May 14 17:21:13 2019 +0200 (5 days ago)
changeset 7026881403d7b9038
parent 70267 9fa2cf7142b7
child 70269 40b6bc5a4721
tuned names
src/HOL/Data_Structures/Tries_Binary.thy
     1.1 --- a/src/HOL/Data_Structures/Tries_Binary.thy	Sun May 12 20:15:28 2019 +0200
     1.2 +++ b/src/HOL/Data_Structures/Tries_Binary.thy	Tue May 14 17:21:13 2019 +0200
     1.3 @@ -107,9 +107,9 @@
     1.4  
     1.5  subsection "Patricia Trie"
     1.6  
     1.7 -datatype ptrie = LfP | NdP "bool list" bool "ptrie * ptrie"
     1.8 +datatype trieP = LfP | NdP "bool list" bool "trieP * trieP"
     1.9  
    1.10 -fun isinP :: "ptrie \<Rightarrow> bool list \<Rightarrow> bool" where
    1.11 +fun isinP :: "trieP \<Rightarrow> bool list \<Rightarrow> bool" where
    1.12  "isinP LfP ks = False" |
    1.13  "isinP (NdP ps b lr) ks =
    1.14    (let n = length ps in
    1.15 @@ -117,6 +117,9 @@
    1.16     then case drop n ks of [] \<Rightarrow> b | k#ks' \<Rightarrow> isinP (sel2 k lr) ks'
    1.17     else False)"
    1.18  
    1.19 +definition emptyP :: trieP where
    1.20 +[simp]: "emptyP = LfP"
    1.21 +
    1.22  fun split where
    1.23  "split [] ys = ([],[],ys)" |
    1.24  "split xs [] = ([],xs,[])" |
    1.25 @@ -130,7 +133,8 @@
    1.26    \<Longrightarrow> mod2 f k lr= mod2 f' k' lr'"
    1.27  by(cases lr, cases lr', auto)
    1.28  
    1.29 -fun insertP :: "bool list \<Rightarrow> ptrie \<Rightarrow> ptrie" where
    1.30 +
    1.31 +fun insertP :: "bool list \<Rightarrow> trieP \<Rightarrow> trieP" where
    1.32  "insertP ks LfP  = NdP ks True (LfP,LfP)" |
    1.33  "insertP ks (NdP ps b lr) =
    1.34    (case split ks ps of
    1.35 @@ -145,10 +149,10 @@
    1.36       (qs,[],[]) \<Rightarrow> NdP ps True lr)"
    1.37  
    1.38  
    1.39 -fun nodeP :: "bool list \<Rightarrow> bool \<Rightarrow> ptrie * ptrie \<Rightarrow> ptrie" where
    1.40 +fun nodeP :: "bool list \<Rightarrow> bool \<Rightarrow> trieP * trieP \<Rightarrow> trieP" where
    1.41  "nodeP ps b lr = (if \<not> b \<and> lr = (LfP,LfP) then LfP else NdP ps b lr)"
    1.42  
    1.43 -fun deleteP :: "bool list \<Rightarrow> ptrie \<Rightarrow> ptrie" where
    1.44 +fun deleteP :: "bool list \<Rightarrow> trieP \<Rightarrow> trieP" where
    1.45  "deleteP ks LfP  = LfP" |
    1.46  "deleteP ks (NdP ps b lr) =
    1.47    (case split ks ps of
    1.48 @@ -159,16 +163,16 @@
    1.49  
    1.50  subsubsection \<open>Functional Correctness\<close>
    1.51  
    1.52 -text \<open>First step: @{typ ptrie} implements @{typ trie} via the abstraction function \<open>abs_ptrie\<close>:\<close>
    1.53 +text \<open>First step: @{typ trieP} implements @{typ trie} via the abstraction function \<open>abs_trieP\<close>:\<close>
    1.54  
    1.55  fun prefix_trie :: "bool list \<Rightarrow> trie \<Rightarrow> trie" where
    1.56  "prefix_trie [] t = t" |
    1.57  "prefix_trie (k#ks) t =
    1.58    (let t' = prefix_trie ks t in Nd False (if k then (Lf,t') else (t',Lf)))"
    1.59  
    1.60 -fun abs_ptrie :: "ptrie \<Rightarrow> trie" where
    1.61 -"abs_ptrie LfP = Lf" |
    1.62 -"abs_ptrie (NdP ps b (l,r)) = prefix_trie ps (Nd b (abs_ptrie l, abs_ptrie r))"
    1.63 +fun abs_trieP :: "trieP \<Rightarrow> trie" where
    1.64 +"abs_trieP LfP = Lf" |
    1.65 +"abs_trieP (NdP ps b (l,r)) = prefix_trie ps (Nd b (abs_trieP l, abs_trieP r))"
    1.66  
    1.67  
    1.68  text \<open>Correctness of @{const isinP}:\<close>
    1.69 @@ -181,8 +185,8 @@
    1.70  done
    1.71  
    1.72  lemma isinP:
    1.73 -  "isinP t ks = isin (abs_ptrie t) ks"
    1.74 -apply(induction t arbitrary: ks rule: abs_ptrie.induct)
    1.75 +  "isinP t ks = isin (abs_trieP t) ks"
    1.76 +apply(induction t arbitrary: ks rule: abs_trieP.induct)
    1.77   apply(auto simp: isin_prefix_trie split: list.split)
    1.78  done
    1.79  
    1.80 @@ -216,8 +220,8 @@
    1.81  apply(auto split: prod.splits if_splits)
    1.82  done
    1.83  
    1.84 -lemma abs_ptrie_insertP:
    1.85 -  "abs_ptrie (insertP ks t) = insert ks (abs_ptrie t)"
    1.86 +lemma abs_trieP_insertP:
    1.87 +  "abs_trieP (insertP ks t) = insert ks (abs_trieP t)"
    1.88  apply(induction t arbitrary: ks)
    1.89  apply(auto simp: prefix_trie_Lfs insert_prefix_trie_same insert_append prefix_trie_append
    1.90             dest!: split_if split: list.split prod.split if_splits)
    1.91 @@ -229,7 +233,7 @@
    1.92  lemma prefix_trie_Lf: "prefix_trie xs t = Lf \<longleftrightarrow> xs = [] \<and> t = Lf"
    1.93  by(cases xs)(auto)
    1.94  
    1.95 -lemma abs_ptrie_Lf: "abs_ptrie t = Lf \<longleftrightarrow> t = LfP"
    1.96 +lemma abs_trieP_Lf: "abs_trieP t = Lf \<longleftrightarrow> t = LfP"
    1.97  by(cases t) (auto simp: prefix_trie_Lf)
    1.98  
    1.99  lemma delete_prefix_trie:
   1.100 @@ -242,35 +246,35 @@
   1.101     = (if delete ys t = Lf then Lf else prefix_trie xs (delete ys t))"
   1.102  by(induction xs)(auto simp: prefix_trie_Lf)
   1.103  
   1.104 -lemma delete_abs_ptrie:
   1.105 -  "delete ks (abs_ptrie t) = abs_ptrie (deleteP ks t)"
   1.106 +lemma delete_abs_trieP:
   1.107 +  "delete ks (abs_trieP t) = abs_trieP (deleteP ks t)"
   1.108  apply(induction t arbitrary: ks)
   1.109  apply(auto simp: delete_prefix_trie delete_append_prefix_trie
   1.110 -        prefix_trie_append prefix_trie_Lf abs_ptrie_Lf
   1.111 +        prefix_trie_append prefix_trie_Lf abs_trieP_Lf
   1.112          dest!: split_if split: if_splits list.split prod.split)
   1.113  done
   1.114  
   1.115  
   1.116  text \<open>The overall correctness proof. Simply composes correctness lemmas.\<close>
   1.117  
   1.118 -definition set_ptrie :: "ptrie \<Rightarrow> bool list set" where
   1.119 -"set_ptrie = set_trie o abs_ptrie"
   1.120 +definition set_trieP :: "trieP \<Rightarrow> bool list set" where
   1.121 +"set_trieP = set_trie o abs_trieP"
   1.122  
   1.123 -lemma set_ptrie_insertP: "set_ptrie (insertP xs t) = set_ptrie t \<union> {xs}"
   1.124 -by(simp add: abs_ptrie_insertP set_trie_insert set_ptrie_def)
   1.125 +lemma set_trieP_insertP: "set_trieP (insertP xs t) = set_trieP t \<union> {xs}"
   1.126 +by(simp add: abs_trieP_insertP set_trie_insert set_trieP_def)
   1.127  
   1.128  interpretation SP: Set
   1.129 -where empty = LfP and isin = isinP and insert = insertP and delete = deleteP
   1.130 -and set = set_ptrie and invar = "\<lambda>t. True"
   1.131 +where empty = emptyP and isin = isinP and insert = insertP and delete = deleteP
   1.132 +and set = set_trieP and invar = "\<lambda>t. True"
   1.133  proof (standard, goal_cases)
   1.134 -  case 1 show ?case by (simp add: set_ptrie_def set_trie_def)
   1.135 +  case 1 show ?case by (simp add: set_trieP_def set_trie_def)
   1.136  next
   1.137 -  case 2 thus ?case by(simp add: isinP set_ptrie_def set_trie_def)
   1.138 +  case 2 thus ?case by(simp add: isinP set_trieP_def set_trie_def)
   1.139  next
   1.140 -  case 3 thus ?case by (auto simp: set_ptrie_insertP)
   1.141 +  case 3 thus ?case by (auto simp: set_trieP_insertP)
   1.142  next
   1.143    case 4 thus ?case
   1.144 -    by(auto simp: isin_delete set_ptrie_def set_trie_def simp flip: delete_abs_ptrie)
   1.145 +    by(auto simp: isin_delete set_trieP_def set_trie_def simp flip: delete_abs_trieP)
   1.146  qed (rule TrueI)+
   1.147  
   1.148  end