Faster Braun tree functions
authornipkow
Sun Nov 04 12:07:24 2018 +0100 (6 months ago)
changeset 692322b913054a9cf
parent 69231 6b90ace5e5eb
child 69233 560263485988
Faster Braun tree functions
src/HOL/Data_Structures/Array_Braun.thy
     1.1 --- a/src/HOL/Data_Structures/Array_Braun.thy	Sun Nov 04 09:57:49 2018 +0100
     1.2 +++ b/src/HOL/Data_Structures/Array_Braun.thy	Sun Nov 04 12:07:24 2018 +0100
     1.3 @@ -1,3 +1,5 @@
     1.4 +(* Author: Tobias Nipkow, with contributions by Thomas Sewell *)
     1.5 +
     1.6  section "Arrays via Braun Trees"
     1.7  
     1.8  theory Array_Braun
     1.9 @@ -49,7 +51,7 @@
    1.10  declare upt_Suc[simp del]
    1.11  
    1.12  
    1.13 -text \<open>@{const lookup1}\<close>
    1.14 +paragraph \<open>@{const lookup1}\<close>
    1.15  
    1.16  lemma nth_list_lookup1: "\<lbrakk>braun t; i < size t\<rbrakk> \<Longrightarrow> list t ! i = lookup1 t (i+1)"
    1.17  proof(induction t arbitrary: i)
    1.18 @@ -64,7 +66,7 @@
    1.19  by(auto simp add: list_eq_iff_nth_eq size_list nth_list_lookup1)
    1.20  
    1.21  
    1.22 -text \<open>@{const update1}\<close>
    1.23 +paragraph \<open>@{const update1}\<close>
    1.24  
    1.25  lemma size_update1: "\<lbrakk> braun t;  n \<in> {1.. size t} \<rbrakk> \<Longrightarrow> size(update1 n x t) = size t"
    1.26  proof(induction t arbitrary: n)
    1.27 @@ -116,7 +118,7 @@
    1.28  qed
    1.29  
    1.30  
    1.31 -text \<open>@{const adds}\<close>
    1.32 +paragraph \<open>@{const adds}\<close>
    1.33  
    1.34  lemma splice_last: shows
    1.35    "size ys \<le> size xs \<Longrightarrow> splice (xs @ [x]) ys = splice xs ys @ [x]"
    1.36 @@ -190,7 +192,7 @@
    1.37  subsubsection "Functional Correctness"
    1.38  
    1.39  
    1.40 -text \<open>@{const add_lo}\<close>
    1.41 +paragraph \<open>@{const add_lo}\<close>
    1.42  
    1.43  lemma list_add_lo: "braun t \<Longrightarrow> list (add_lo a t) = a # list t"
    1.44  by(induction t arbitrary: a) auto
    1.45 @@ -199,7 +201,7 @@
    1.46  by(induction t arbitrary: x) (auto simp add: list_add_lo simp flip: size_list)
    1.47  
    1.48  
    1.49 -text \<open>@{const del_lo}\<close>
    1.50 +paragraph \<open>@{const del_lo}\<close>
    1.51  
    1.52  lemma list_merge: "braun (Node l x r) \<Longrightarrow> list(merge l r) = splice (list l) (list r)"
    1.53  by (induction l r rule: merge.induct) auto
    1.54 @@ -214,7 +216,7 @@
    1.55  by (cases t) (simp_all add: braun_merge)
    1.56  
    1.57  
    1.58 -text \<open>@{const del_hi}\<close>
    1.59 +paragraph \<open>@{const del_hi}\<close>
    1.60  
    1.61  lemma list_Nil_iff: "list t = [] \<longleftrightarrow> t = Leaf"
    1.62  by(cases t) simp_all
    1.63 @@ -266,6 +268,9 @@
    1.64  
    1.65  subsection "Faster"
    1.66  
    1.67 +
    1.68 +subsubsection \<open>Initialization with 1 element\<close>
    1.69 +
    1.70  fun braun_of_naive :: "'a \<Rightarrow> nat \<Rightarrow> 'a tree" where
    1.71  "braun_of_naive x n = (if n=0 then Leaf
    1.72    else let m = (n-1) div 2
    1.73 @@ -306,4 +311,327 @@
    1.74  corollary list_braun_of: "list(braun_of x n) = replicate n x"
    1.75  unfolding braun_of_def by (metis eq_fst_iff braun2_of_replicate)
    1.76  
    1.77 +
    1.78 +subsubsection "Proof Infrastructure"
    1.79 +
    1.80 +text \<open>Originally due to Thomas Sewell.\<close>
    1.81 +
    1.82 +paragraph \<open>\<open>take_nths\<close>\<close>
    1.83 +
    1.84 +fun take_nths :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    1.85 +"take_nths i k [] = []" |
    1.86 +"take_nths i k (x # xs) = (if i = 0 then x # take_nths (2^k - 1) k xs
    1.87 +  else take_nths (i - 1) k xs)"
    1.88 +
    1.89 +lemma take_nths_drop:
    1.90 +  "take_nths i k (drop j xs) = take_nths (i + j) k xs"
    1.91 +by (induct xs arbitrary: i j; simp add: drop_Cons split: nat.split)
    1.92 +
    1.93 +lemma take_nths_00:
    1.94 +  "take_nths 0 0 xs = xs"
    1.95 +by (induct xs; simp)
    1.96 +
    1.97 +lemma splice_take_nths:
    1.98 +  "splice (take_nths 0 (Suc 0) xs) (take_nths (Suc 0) (Suc 0) xs) = xs"
    1.99 +by (induct xs; simp)
   1.100 +
   1.101 +lemma take_nths_take_nths:
   1.102 +  "take_nths i m (take_nths j n xs) = take_nths ((i * 2^n) + j) (m + n) xs"
   1.103 +by (induct xs arbitrary: i j; simp add: algebra_simps power_add)
   1.104 +
   1.105 +lemma take_nths_empty:
   1.106 +  "(take_nths i k xs = []) = (length xs \<le> i)"
   1.107 +by (induction xs arbitrary: i k) auto
   1.108 +
   1.109 +lemma hd_take_nths:
   1.110 +  "i < length xs \<Longrightarrow> hd(take_nths i k xs) = xs ! i"
   1.111 +by (induction xs arbitrary: i k) auto
   1.112 +
   1.113 +lemma take_nths_01_splice:
   1.114 +  "\<lbrakk> length xs = length ys \<or> length xs = length ys + 1 \<rbrakk> \<Longrightarrow>
   1.115 +   take_nths 0 (Suc 0) (splice xs ys) = xs \<and>
   1.116 +   take_nths (Suc 0) (Suc 0) (splice xs ys) = ys"
   1.117 +by (induct xs arbitrary: ys; case_tac ys; simp)
   1.118 +
   1.119 +lemma length_take_nths_00:
   1.120 +  "length (take_nths 0 (Suc 0) xs) = length (take_nths (Suc 0) (Suc 0) xs) \<or>
   1.121 +   length (take_nths 0 (Suc 0) xs) = length (take_nths (Suc 0) (Suc 0) xs) + 1"
   1.122 +by (induct xs) auto
   1.123 +
   1.124 +
   1.125 +paragraph \<open>\<open>braun_list\<close>\<close>
   1.126 +
   1.127 +fun braun_list :: "'a tree \<Rightarrow> 'a list \<Rightarrow> bool" where
   1.128 +"braun_list Leaf xs = (xs = [])" |
   1.129 +"braun_list (Node l x r) xs = (xs \<noteq> [] \<and> x = hd xs \<and>
   1.130 +    braun_list l (take_nths 1 1 xs) \<and>
   1.131 +    braun_list r (take_nths 2 1 xs))"
   1.132 +
   1.133 +lemma braun_list_eq:
   1.134 +  "braun_list t xs = (braun t \<and> xs = list t)"
   1.135 +proof (induct t arbitrary: xs)
   1.136 +  case Leaf
   1.137 +  show ?case by simp
   1.138 +next
   1.139 +  case Node
   1.140 +  show ?case
   1.141 +    using length_take_nths_00[of xs] splice_take_nths[of xs]
   1.142 +    by (auto simp: neq_Nil_conv Node.hyps size_list[symmetric] take_nths_01_splice)
   1.143 +qed
   1.144 +
   1.145 +
   1.146 +subsubsection \<open>Converting a list of elements into a Braun tree\<close>
   1.147 +
   1.148 +fun nodes :: "'a tree list \<Rightarrow> 'a list \<Rightarrow> 'a tree list \<Rightarrow> 'a tree list" where
   1.149 +"nodes (l#ls) (x#xs) (r#rs) = Node l x r # nodes ls xs rs" |
   1.150 +"nodes (l#ls) (x#xs) [] = Node l x Leaf # nodes ls xs []" |
   1.151 +"nodes [] (x#xs) (r#rs) = Node Leaf x r # nodes [] xs rs" |
   1.152 +"nodes [] (x#xs) [] = Node Leaf x Leaf # nodes [] xs []" |
   1.153 +"nodes ls [] rs = []"
   1.154 +
   1.155 +fun brauns :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a tree list" where
   1.156 +"brauns k xs = (if xs = [] then [] else
   1.157 +   let ys = take (2^k) xs;
   1.158 +       zs = drop (2^k) xs;
   1.159 +       ts = brauns (k+1) zs
   1.160 +   in nodes ts ys (drop (2^k) ts))"
   1.161 +
   1.162 +declare brauns.simps[simp del]
   1.163 +
   1.164 +definition brauns1 :: "'a list \<Rightarrow> 'a tree" where
   1.165 +"brauns1 xs = (if xs = [] then Leaf else brauns 0 xs ! 0)"
   1.166 +
   1.167 +fun t_brauns :: "nat \<Rightarrow> 'a list \<Rightarrow> nat" where
   1.168 +"t_brauns k xs = (if xs = [] then 0 else
   1.169 +   let ys = take (2^k) xs;
   1.170 +       zs = drop (2^k) xs;
   1.171 +       ts = brauns (k+1) zs
   1.172 +   in 4 * min (2^k) (length xs) + t_brauns (k+1) zs)"
   1.173 +
   1.174 +
   1.175 +paragraph "Functional correctness"
   1.176 +
   1.177 +text \<open>The proof is originally due to Thomas Sewell.\<close>
   1.178 +
   1.179 +lemma length_nodes:
   1.180 +  "length (nodes ls xs rs) = length xs"
   1.181 +by (induct ls xs rs rule: nodes.induct; simp)
   1.182 +
   1.183 +lemma nth_nodes:
   1.184 +  "i < length xs \<Longrightarrow> nodes ls xs rs ! i =
   1.185 +  Node (if i < length ls then ls ! i else Leaf) (xs ! i)
   1.186 +    (if i < length rs then rs ! i else Leaf)"
   1.187 +by (induct ls xs rs arbitrary: i rule: nodes.induct;
   1.188 +    simp add: nth_Cons split: nat.split)
   1.189 +
   1.190 +theorem length_brauns:
   1.191 +  "length (brauns k xs) = min (length xs) (2 ^ k)"
   1.192 +proof (induct xs arbitrary: k rule: measure_induct_rule[where f=length])
   1.193 +  case (less xs) thus ?case by (simp add: brauns.simps[of k xs] Let_def length_nodes)
   1.194 +qed
   1.195 +
   1.196 +theorem brauns_correct:
   1.197 +  "i < min (length xs) (2 ^ k) \<Longrightarrow> braun_list (brauns k xs ! i) (take_nths i k xs)"
   1.198 +proof (induct xs arbitrary: i k rule: measure_induct_rule[where f=length])
   1.199 +  case (less xs)
   1.200 +  have "xs \<noteq> []" using less.prems by auto
   1.201 +  let ?zs = "drop (2^k) xs"
   1.202 +  let ?ts = "brauns (Suc k) ?zs"
   1.203 +  from less.hyps[of ?zs _ "Suc k"]
   1.204 +  have IH: "\<lbrakk> j = i + 2 ^ k;  i < min (length ?zs) (2 ^ (k+1)) \<rbrakk> \<Longrightarrow>
   1.205 +    braun_list (?ts ! i) (take_nths j (Suc k) xs)" for i j
   1.206 +    using \<open>xs \<noteq> []\<close> by (simp add: take_nths_drop)
   1.207 +  let ?xs' = "take_nths i k xs"
   1.208 +  let ?ts' = "drop (2^k) ?ts"
   1.209 +  show ?case
   1.210 +  proof (cases "i < length ?ts \<and> \<not> i < length ?ts'")
   1.211 +    case True
   1.212 +    have "braun_list (brauns k xs ! i) ?xs' \<longleftrightarrow>
   1.213 +          braun_list (nodes ?ts (take (2^k) xs) ?ts' ! i) ?xs'"
   1.214 +      using \<open>xs \<noteq> []\<close> by (simp add: brauns.simps[of k xs] Let_def)
   1.215 +    also have "\<dots> \<longleftrightarrow> braun_list (?ts ! i) (take_nths (2^k + i) (k+1) xs)
   1.216 +                    \<and> braun_list Leaf (take_nths (2^(k+1) + i) (k+1) xs)"
   1.217 +      using less.prems True
   1.218 +      by (clarsimp simp: nth_nodes take_nths_take_nths take_nths_empty hd_take_nths)
   1.219 +    also have "\<dots>" using less.prems True by (auto simp: IH take_nths_empty length_brauns)
   1.220 +    finally show ?thesis .
   1.221 +  next
   1.222 +    case False
   1.223 +    thus ?thesis using less.prems
   1.224 +    by (auto simp: brauns.simps[of k xs] Let_def nth_nodes take_nths_take_nths
   1.225 +                   IH take_nths_empty hd_take_nths length_brauns)
   1.226 +  qed
   1.227 +qed
   1.228 +
   1.229 +corollary brauns1_correct:
   1.230 +  "braun (brauns1 xs) \<and> list (brauns1 xs) = xs"
   1.231 +using brauns_correct[of 0 xs 0]
   1.232 +by (simp add: brauns1_def braun_list_eq take_nths_00)
   1.233 +
   1.234 +
   1.235 +paragraph "Running Time Analysis"
   1.236 +
   1.237 +theorem t_brauns:
   1.238 +  "t_brauns k xs = 4 * length xs"
   1.239 +proof (induction xs arbitrary: k rule: measure_induct_rule[where f = length])
   1.240 +  case (less xs)
   1.241 +  show ?case
   1.242 +  proof cases
   1.243 +    assume "xs = []"
   1.244 +    thus ?thesis by(simp add: Let_def)
   1.245 +  next
   1.246 +    assume "xs \<noteq> []"
   1.247 +    let ?zs = "drop (2^k) xs"
   1.248 +    have "t_brauns k xs = t_brauns (k+1) ?zs + 4 * min (2^k) (length xs)"
   1.249 +     using \<open>xs \<noteq> []\<close> by(simp add: Let_def)
   1.250 +    also have "\<dots> = 4 * length ?zs + 4 * min (2^k) (length xs)"
   1.251 +      using less[of ?zs "k+1"] \<open>xs \<noteq> []\<close>
   1.252 +      by (simp)
   1.253 +    also have "\<dots> = 4 * length xs"
   1.254 +      by(simp)
   1.255 +    finally show ?case .
   1.256 +  qed
   1.257 +qed
   1.258 +
   1.259 +
   1.260 +subsubsection \<open>Converting a Braun Tree into a List of Elements\<close>
   1.261 +
   1.262 +text \<open>The code and the proof are originally due to Thomas Sewell (except running time).\<close>
   1.263 +
   1.264 +function list_fast_rec :: "'a tree list \<Rightarrow> 'a list" where
   1.265 +"list_fast_rec ts = (if ts = [] then [] else
   1.266 +  let us = filter (\<lambda>t. t \<noteq> Leaf) ts
   1.267 +  in map root_val us @ list_fast_rec (map left us @ map right us))"
   1.268 +by (pat_completeness, auto)
   1.269 +
   1.270 +lemma list_fast_rec_term: "\<lbrakk> ts \<noteq> []; us = filter (\<lambda>t. t \<noteq> \<langle>\<rangle>) ts \<rbrakk> \<Longrightarrow>
   1.271 +  (map left us @ map right us, ts) \<in> measure (sum_list \<circ> map (\<lambda>t. 2 * size t + 1))"
   1.272 +apply (clarsimp simp: sum_list_addf[symmetric] sum_list_map_filter')
   1.273 +apply (rule sum_list_strict_mono; simp)
   1.274 +apply (case_tac x; simp)
   1.275 +done
   1.276 +
   1.277 +termination
   1.278 +apply (relation "measure (sum_list o map (\<lambda>t. 2 * size t + 1))")
   1.279 + apply simp
   1.280 +using list_fast_rec_term by auto
   1.281 +
   1.282 +declare list_fast_rec.simps[simp del]
   1.283 +
   1.284 +definition list_fast :: "'a tree \<Rightarrow> 'a list" where
   1.285 +"list_fast t = list_fast_rec [t]"
   1.286 +
   1.287 +function t_list_fast_rec :: "'a tree list \<Rightarrow> nat" where
   1.288 +"t_list_fast_rec ts = (if ts = [] then 0 else
   1.289 +  let us = filter (\<lambda>t. t \<noteq> Leaf) ts
   1.290 +  in length ts + 5 * length us + t_list_fast_rec (map left us @ map right us))"
   1.291 +by (pat_completeness, auto)
   1.292 +
   1.293 +termination
   1.294 +apply (relation "measure (sum_list o map (\<lambda>t. 2 * size t + 1))")
   1.295 + apply simp
   1.296 +using list_fast_rec_term by auto
   1.297 +
   1.298 +declare t_list_fast_rec.simps[simp del]
   1.299 +
   1.300 +
   1.301 +paragraph "Functional Correctness"
   1.302 +
   1.303 +lemma list_fast_rec_all_Leaf:
   1.304 +  "\<forall>t \<in> set ts. t = Leaf \<Longrightarrow> list_fast_rec ts = []"
   1.305 +by (simp add: filter_empty_conv list_fast_rec.simps)
   1.306 +
   1.307 +lemma take_nths_eq_single:
   1.308 +  "length xs - i < 2^n \<Longrightarrow> take_nths i n xs = take 1 (drop i xs)"
   1.309 +by (induction xs arbitrary: i n; simp add: drop_Cons')
   1.310 +
   1.311 +lemma braun_list_Nil:
   1.312 +  "braun_list t [] = (t = Leaf)"
   1.313 +by (cases t; simp)
   1.314 +
   1.315 +lemma braun_list_not_Nil: "xs \<noteq> [] \<Longrightarrow>
   1.316 +  braun_list t xs =
   1.317 + (\<exists>l x r. t = Node l x r \<and> x = hd xs \<and>
   1.318 +    braun_list l (take_nths 1 1 xs) \<and>
   1.319 +    braun_list r (take_nths 2 1 xs))"
   1.320 +by(cases t; simp)
   1.321 +
   1.322 +theorem list_fast_rec_correct:
   1.323 +  "\<lbrakk> length ts = 2 ^ k; \<forall>i < 2 ^ k. braun_list (ts ! i) (take_nths i k xs) \<rbrakk>
   1.324 +    \<Longrightarrow> list_fast_rec ts = xs"
   1.325 +proof (induct xs arbitrary: k ts rule: measure_induct_rule[where f=length])
   1.326 +  case (less xs)
   1.327 +  show ?case
   1.328 +  proof (cases "length xs < 2 ^ k")
   1.329 +    case True
   1.330 +    from less.prems True have filter:
   1.331 +      "\<exists>n. ts = map (\<lambda>x. Node Leaf x Leaf) xs @ replicate n Leaf"
   1.332 +      apply (rule_tac x="length ts - length xs" in exI)
   1.333 +      apply (clarsimp simp: list_eq_iff_nth_eq)
   1.334 +      apply(auto simp: nth_append braun_list_not_Nil take_nths_eq_single braun_list_Nil hd_drop_conv_nth)
   1.335 +      done
   1.336 +    thus ?thesis
   1.337 +      by (clarsimp simp: list_fast_rec.simps[of ts] o_def list_fast_rec_all_Leaf)
   1.338 +  next
   1.339 +    case False
   1.340 +    with less.prems(2) have *:
   1.341 +      "\<forall>i < 2 ^ k. ts ! i \<noteq> Leaf
   1.342 +         \<and> root_val (ts ! i) = xs ! i
   1.343 +         \<and> braun_list (left (ts ! i)) (take_nths (i + 2 ^ k) (Suc k) xs)
   1.344 +         \<and> (\<forall>ys. ys = take_nths (i + 2 * 2 ^ k) (Suc k) xs
   1.345 +                 \<longrightarrow> braun_list (right (ts ! i)) ys)"
   1.346 +      by (auto simp: take_nths_empty hd_take_nths braun_list_not_Nil take_nths_take_nths
   1.347 +                     algebra_simps)
   1.348 +    have 1: "map root_val ts = take (2 ^ k) xs"
   1.349 +      using less.prems(1) False by (simp add: list_eq_iff_nth_eq *)
   1.350 +    have 2: "list_fast_rec (map left ts @ map right ts) = drop (2 ^ k) xs"
   1.351 +      using less.prems(1) False
   1.352 +      by (auto intro!: Nat.diff_less less.hyps[where k= "Suc k"]
   1.353 +               simp: nth_append * take_nths_drop algebra_simps)
   1.354 +    from less.prems(1) False show ?thesis
   1.355 +      by (auto simp: list_fast_rec.simps[of ts] 1 2 Let_def * all_set_conv_all_nth)
   1.356 +  qed
   1.357 +qed
   1.358 +
   1.359 +corollary list_fast_correct:
   1.360 +  "braun t \<Longrightarrow> list_fast t = list t"
   1.361 +by (simp add: list_fast_def take_nths_00 braun_list_eq list_fast_rec_correct[where k=0])
   1.362 +
   1.363 +
   1.364 +paragraph "Running Time Analysis"
   1.365 +
   1.366 +lemma sum_tree_list_children: "\<forall>t \<in> set ts. t \<noteq> Leaf \<Longrightarrow>
   1.367 +  (\<Sum>t\<leftarrow>ts. k * size t) = (\<Sum>t \<leftarrow> map left ts @ map right ts. k * size t) + k * length ts"
   1.368 +by(induction ts)(auto simp add: neq_Leaf_iff algebra_simps)
   1.369 +
   1.370 +theorem t_list_fast_rec_ub:
   1.371 +  "t_list_fast_rec ts \<le> sum_list (map (\<lambda>t. 7*size t + 1) ts)"
   1.372 +proof (induction ts rule: measure_induct_rule[where f="sum_list o map (\<lambda>t. 2*size t + 1)"])
   1.373 +  case (less ts)
   1.374 +  show ?case
   1.375 +  proof cases
   1.376 +    assume "ts = []"
   1.377 +    thus ?thesis using t_list_fast_rec.simps[of ts] by(simp add: Let_def)
   1.378 +  next
   1.379 +    assume "ts \<noteq> []"
   1.380 +    let ?us = "filter (\<lambda>t. t \<noteq> Leaf) ts"
   1.381 +    let ?children = "map left ?us @ map right ?us"
   1.382 +    have "t_list_fast_rec ts = t_list_fast_rec ?children + 5 * length ?us + length ts"
   1.383 +     using \<open>ts \<noteq> []\<close> t_list_fast_rec.simps[of ts] by(simp add: Let_def)
   1.384 +    also have "\<dots> \<le> (\<Sum>t\<leftarrow>?children. 7 * size t + 1) + 5 * length ?us + length ts"
   1.385 +      using less[of "map left ?us @ map right ?us"]
   1.386 +        list_fast_rec_term[of ts, OF \<open>ts \<noteq> []\<close>]
   1.387 +      by (simp)
   1.388 +    also have "\<dots> = (\<Sum>t\<leftarrow>?children. 7*size t) + 7 * length ?us + length ts"
   1.389 +      by(simp add: sum_list_Suc o_def)
   1.390 +    also have "\<dots> = (\<Sum>t\<leftarrow>?us. 7*size t) + length ts"
   1.391 +      by(simp add: sum_tree_list_children)
   1.392 +    also have "\<dots> \<le> (\<Sum>t\<leftarrow>ts. 7*size t) + length ts"
   1.393 +      by(simp add: sum_list_filter_le_nat)
   1.394 +    also have "\<dots> = (\<Sum>t\<leftarrow>ts. 7 * size t + 1)"
   1.395 +      by(simp add: sum_list_Suc)
   1.396 +    finally show ?case .
   1.397 +  qed
   1.398 +qed
   1.399 +
   1.400  end
   1.401 \ No newline at end of file