69145

1 
section "Arrays via Braun Trees"


2 


3 
theory Array_Braun


4 
imports


5 
Array_Specs


6 
Braun_Tree


7 
begin


8 


9 
subsection "Array"


10 


11 
fun lookup1 :: "'a tree \<Rightarrow> nat \<Rightarrow> 'a" where


12 
"lookup1 (Node l x r) n = (if n=1 then x else lookup1 (if even n then l else r) (n div 2))"


13 


14 
fun update1 :: "nat \<Rightarrow> 'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where


15 
"update1 n x Leaf = Node Leaf x Leaf" 


16 
"update1 n x (Node l a r) =


17 
(if n=1 then Node l x r else


18 
if even n then Node (update1 (n div 2) x l) a r


19 
else Node l a (update1 (n div 2) x r))"


20 


21 
fun adds :: "'a list \<Rightarrow> nat \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where


22 
"adds [] n t = t" 


23 
"adds (x#xs) n t = adds xs (n+1) (update1 (n+1) x t)"


24 


25 
fun list :: "'a tree \<Rightarrow> 'a list" where


26 
"list Leaf = []" 


27 
"list (Node l x r) = x # splice (list l) (list r)"


28 


29 


30 
subsubsection "Functional Correctness"


31 


32 
lemma size_list: "size(list t) = size t"


33 
by(induction t)(auto)


34 


35 
lemma minus1_div2: "(n  Suc 0) div 2 = (if odd n then n div 2 else n div 2  1)"


36 
by auto arith


37 


38 
lemma nth_splice: "\<lbrakk> n < size xs + size ys; size ys \<le> size xs; size xs \<le> size ys + 1 \<rbrakk>


39 
\<Longrightarrow> splice xs ys ! n = (if even n then xs else ys) ! (n div 2)"


40 
apply(induction xs ys arbitrary: n rule: splice.induct)


41 
apply (auto simp: nth_Cons' minus1_div2)


42 
done


43 


44 
lemma div2_in_bounds:


45 
"\<lbrakk> braun (Node l x r); n \<in> {1..size(Node l x r)}; n > 1 \<rbrakk> \<Longrightarrow>


46 
(odd n \<longrightarrow> n div 2 \<in> {1..size r}) \<and> (even n \<longrightarrow> n div 2 \<in> {1..size l})"


47 
by auto arith


48 


49 
declare upt_Suc[simp del]


50 


51 


52 
text \<open>@{const lookup1}\<close>


53 


54 
lemma nth_list_lookup1: "\<lbrakk>braun t; i < size t\<rbrakk> \<Longrightarrow> list t ! i = lookup1 t (i+1)"


55 
proof(induction t arbitrary: i)


56 
case Leaf thus ?case by simp


57 
next


58 
case Node


59 
thus ?case using div2_in_bounds[OF Node.prems(1), of "i+1"]


60 
by (auto simp: nth_splice minus1_div2 size_list)


61 
qed


62 


63 
lemma list_eq_map_lookup1: "braun t \<Longrightarrow> list t = map (lookup1 t) [1..<size t + 1]"


64 
by(auto simp add: list_eq_iff_nth_eq size_list nth_list_lookup1)


65 


66 


67 
text \<open>@{const update1}\<close>


68 


69 
lemma size_update1: "\<lbrakk> braun t; n \<in> {1.. size t} \<rbrakk> \<Longrightarrow> size(update1 n x t) = size t"


70 
proof(induction t arbitrary: n)


71 
case Leaf thus ?case by simp


72 
next


73 
case Node thus ?case using div2_in_bounds[OF Node.prems] by simp


74 
qed


75 


76 
lemma braun_update1: "\<lbrakk>braun t; n \<in> {1.. size t} \<rbrakk> \<Longrightarrow> braun(update1 n x t)"


77 
proof(induction t arbitrary: n)


78 
case Leaf thus ?case by simp


79 
next


80 
case Node thus ?case


81 
using div2_in_bounds[OF Node.prems] by (simp add: size_update1)


82 
qed


83 


84 
lemma lookup1_update1: "\<lbrakk> braun t; n \<in> {1.. size t} \<rbrakk> \<Longrightarrow>


85 
lookup1 (update1 n x t) m = (if n=m then x else lookup1 t m)"


86 
proof(induction t arbitrary: m n)


87 
case Leaf


88 
then show ?case by simp


89 
next


90 
have aux: "\<lbrakk> odd n; odd m \<rbrakk> \<Longrightarrow> n div 2 = (m::nat) div 2 \<longleftrightarrow> m=n" for m n


91 
using odd_two_times_div_two_succ by fastforce


92 
case Node


93 
thus ?case using div2_in_bounds[OF Node.prems] by (auto simp: aux)


94 
qed


95 


96 
lemma list_update1: "\<lbrakk> braun t; n \<in> {1.. size t} \<rbrakk> \<Longrightarrow> list(update1 n x t) = (list t)[n1 := x]"


97 
by(auto simp add: list_eq_map_lookup1 list_eq_iff_nth_eq lookup1_update1 size_update1 braun_update1)


98 


99 
text \<open>A second proof of @{thm list_update1}:\<close>


100 


101 
lemma diff1_eq_iff: "n > 0 \<Longrightarrow> n  Suc 0 = m \<longleftrightarrow> n = m+1"


102 
by arith


103 


104 
lemma list_update_splice:


105 
"\<lbrakk> n < size xs + size ys; size ys \<le> size xs; size xs \<le> size ys + 1 \<rbrakk> \<Longrightarrow>


106 
(splice xs ys) [n := x] =


107 
(if even n then splice (xs[n div 2 := x]) ys else splice xs (ys[n div 2 := x]))"


108 
by(induction xs ys arbitrary: n rule: splice.induct) (auto split: nat.split)


109 


110 
lemma list_update2: "\<lbrakk> braun t; n \<in> {1.. size t} \<rbrakk> \<Longrightarrow> list(update1 n x t) = (list t)[n1 := x]"


111 
proof(induction t arbitrary: n)


112 
case Leaf thus ?case by simp


113 
next


114 
case (Node l a r) thus ?case using div2_in_bounds[OF Node.prems]


115 
by(auto simp: list_update_splice diff1_eq_iff size_list split: nat.split)


116 
qed


117 


118 


119 
text \<open>@{const adds}\<close>


120 


121 
lemma splice_last: shows


122 
"size ys \<le> size xs \<Longrightarrow> splice (xs @ [x]) ys = splice xs ys @ [x]"


123 
and "size ys+1 \<ge> size xs \<Longrightarrow> splice xs (ys @ [y]) = splice xs ys @ [y]"


124 
by(induction xs ys arbitrary: x y rule: splice.induct) (auto)


125 


126 
lemma list_add_hi: "braun t \<Longrightarrow> list(update1 (Suc(size t)) x t) = list t @ [x]"


127 
by(induction t)(auto simp: splice_last size_list)


128 


129 
lemma size_add_hi: "braun t \<Longrightarrow> m = size t \<Longrightarrow> size(update1 (Suc m) x t) = size t + 1"


130 
by(induction t arbitrary: m)(auto)


131 


132 
lemma braun_add_hi: "braun t \<Longrightarrow> braun(update1 (Suc(size t)) x t)"


133 
by(induction t)(auto simp: size_add_hi)


134 


135 
lemma size_braun_adds:


136 
"\<lbrakk> braun t; size t = n \<rbrakk> \<Longrightarrow> size(adds xs n t) = size t + length xs \<and> braun (adds xs n t)"


137 
by(induction xs arbitrary: t n)(auto simp: braun_add_hi size_add_hi)


138 


139 
lemma list_adds: "\<lbrakk> braun t; size t = n \<rbrakk> \<Longrightarrow> list(adds xs n t) = list t @ xs"


140 
by(induction xs arbitrary: t n)(auto simp: size_braun_adds list_add_hi size_add_hi braun_add_hi)


141 


142 


143 
subsubsection "Array Implementation"


144 


145 
interpretation A: Array


146 
where lookup = "\<lambda>(t,l) n. lookup1 t (n+1)"


147 
and update = "\<lambda>n x (t,l). (update1 (n+1) x t, l)"


148 
and len = "\<lambda>(t,l). l"


149 
and array = "\<lambda>xs. (adds xs 0 Leaf, length xs)"


150 
and invar = "\<lambda>(t,l). braun t \<and> l = size t"


151 
and list = "\<lambda>(t,l). list t"


152 
proof (standard, goal_cases)


153 
case 1 thus ?case by (simp add: nth_list_lookup1 split: prod.splits)


154 
next


155 
case 2 thus ?case by (simp add: list_update1 split: prod.splits)


156 
next


157 
case 3 thus ?case by (simp add: size_list split: prod.splits)


158 
next


159 
case 4 thus ?case by (simp add: list_adds)


160 
next


161 
case 5 thus ?case by (simp add: braun_update1 size_update1 split: prod.splits)


162 
next


163 
case 6 thus ?case by (simp add: size_braun_adds split: prod.splits)


164 
qed


165 


166 


167 
subsection "Flexible Array"


168 


169 
fun add_lo where


170 
"add_lo x Leaf = Node Leaf x Leaf" 


171 
"add_lo x (Node l a r) = Node (add_lo a r) x l"


172 


173 
fun merge where


174 
"merge Leaf r = r" 


175 
"merge (Node l a r) rr = Node rr a (merge l r)"


176 


177 
fun del_lo where


178 
"del_lo Leaf = Leaf" 


179 
"del_lo (Node l a r) = merge l r"


180 


181 
fun del_hi :: "nat \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where


182 
"del_hi n Leaf = Leaf" 


183 
"del_hi n (Node l x r) =


184 
(if n = 1 then Leaf


185 
else if even n


186 
then Node (del_hi (n div 2) l) x r


187 
else Node l x (del_hi (n div 2) r))"


188 


189 


190 
subsubsection "Functional Correctness"


191 


192 


193 
text \<open>@{const add_lo}\<close>


194 


195 
lemma list_add_lo: "braun t \<Longrightarrow> list (add_lo a t) = a # list t"


196 
by(induction t arbitrary: a) auto


197 


198 
lemma braun_add_lo: "braun t \<Longrightarrow> braun(add_lo x t)"


199 
by(induction t arbitrary: x) (auto simp add: list_add_lo simp flip: size_list)


200 


201 


202 
text \<open>@{const del_lo}\<close>


203 


204 
lemma list_merge: "braun (Node l x r) \<Longrightarrow> list(merge l r) = splice (list l) (list r)"


205 
by (induction l r rule: merge.induct) auto


206 


207 
lemma braun_merge: "braun (Node l x r) \<Longrightarrow> braun(merge l r)"


208 
by (induction l r rule: merge.induct)(auto simp add: list_merge simp flip: size_list)


209 


210 
lemma list_del_lo: "braun t \<Longrightarrow> list(del_lo t) = tl (list t)"


211 
by (cases t) (simp_all add: list_merge)


212 


213 
lemma braun_del_lo: "braun t \<Longrightarrow> braun(del_lo t)"


214 
by (cases t) (simp_all add: braun_merge)


215 


216 


217 
text \<open>@{const del_hi}\<close>


218 


219 
lemma list_Nil_iff: "list t = [] \<longleftrightarrow> t = Leaf"


220 
by(cases t) simp_all


221 


222 
lemma butlast_splice: "butlast (splice xs ys) =


223 
(if size xs > size ys then splice (butlast xs) ys else splice xs (butlast ys))"


224 
by(induction xs ys rule: splice.induct) (auto)


225 


226 
lemma list_del_hi: "braun t \<Longrightarrow> size t = st \<Longrightarrow> list(del_hi st t) = butlast(list t)"


227 
apply(induction t arbitrary: st)


228 
by(auto simp: list_Nil_iff size_list butlast_splice)


229 


230 
lemma braun_del_hi: "braun t \<Longrightarrow> size t = st \<Longrightarrow> braun(del_hi st t)"


231 
apply(induction t arbitrary: st)


232 
by(auto simp: list_del_hi simp flip: size_list)


233 


234 


235 
subsubsection "Flexible Array Implementation"


236 


237 
interpretation AF: Array_Flex


238 
where lookup = "\<lambda>(t,l) n. lookup1 t (n+1)"


239 
and update = "\<lambda>n x (t,l). (update1 (n+1) x t, l)"


240 
and len = "\<lambda>(t,l). l"


241 
and array = "\<lambda>xs. (adds xs 0 Leaf, length xs)"


242 
and invar = "\<lambda>(t,l). braun t \<and> l = size t"


243 
and list = "\<lambda>(t,l). list t"


244 
and add_lo = "\<lambda>x (t,l). (add_lo x t, l+1)"


245 
and del_lo = "\<lambda>(t,l). (del_lo t, l1)"


246 
and add_hi = "\<lambda>x (t,l). (update1 (Suc l) x t, l+1)"


247 
and del_hi = "\<lambda>(t,l). (del_hi l t, l1)"


248 
proof (standard, goal_cases)


249 
case 1 thus ?case by (simp add: list_add_lo split: prod.splits)


250 
next


251 
case 2 thus ?case by (simp add: list_del_lo split: prod.splits)


252 
next


253 
case 3 thus ?case by (simp add: list_add_hi braun_add_hi split: prod.splits)


254 
next


255 
case 4 thus ?case by (simp add: list_del_hi split: prod.splits)


256 
next


257 
case 5 thus ?case by (simp add: braun_add_lo list_add_lo flip: size_list split: prod.splits)


258 
next


259 
case 6 thus ?case by (simp add: braun_del_lo list_del_lo flip: size_list split: prod.splits)


260 
next


261 
case 7 thus ?case by (simp add: size_add_hi braun_add_hi split: prod.splits)


262 
next


263 
case 8 thus ?case by (simp add: braun_del_hi list_del_hi flip: size_list split: prod.splits)


264 
qed


265 


266 


267 
subsection "Faster"


268 

69206

269 
fun braun_of_naive :: "'a \<Rightarrow> nat \<Rightarrow> 'a tree" where


270 
"braun_of_naive x n = (if n=0 then Leaf

69145

271 
else let m = (n1) div 2

69206

272 
in if odd n then Node (braun_of_naive x m) x (braun_of_naive x m)


273 
else Node (braun_of_naive x (m + 1)) x (braun_of_naive x m))"

69145

274 


275 
fun braun2_of :: "'a \<Rightarrow> nat \<Rightarrow> 'a tree * 'a tree" where


276 
"braun2_of x n = (if n = 0 then (Leaf, Node Leaf x Leaf)


277 
else let (s,t) = braun2_of x ((n1) div 2)


278 
in if odd n then (Node s x s, Node t x s) else (Node t x s, Node t x t))"


279 


280 
definition braun_of :: "'a \<Rightarrow> nat \<Rightarrow> 'a tree" where


281 
"braun_of x n = fst (braun2_of x n)"


282 


283 
declare braun2_of.simps [simp del]


284 


285 
lemma braun2_of_size_braun: "braun2_of x n = (s,t) \<Longrightarrow> size s = n \<and> size t = n+1 \<and> braun s \<and> braun t"


286 
proof(induction x n arbitrary: s t rule: braun2_of.induct)


287 
case (1 x n)


288 
then show ?case


289 
by (auto simp: braun2_of.simps[of x n] split: prod.splits if_splits) presburger+


290 
qed


291 


292 
lemma braun2_of_replicate:


293 
"braun2_of x n = (s,t) \<Longrightarrow> list s = replicate n x \<and> list t = replicate (n+1) x"


294 
proof(induction x n arbitrary: s t rule: braun2_of.induct)


295 
case (1 x n)


296 
have "x # replicate m x = replicate (m+1) x" for m by simp


297 
with 1 show ?case


298 
apply (auto simp: braun2_of.simps[of x n] replicate.simps(2)[of 0 x]


299 
simp del: replicate.simps(2) split: prod.splits if_splits)


300 
by presburger+


301 
qed


302 


303 
corollary braun_braun_of: "braun(braun_of x n)"


304 
unfolding braun_of_def by (metis eq_fst_iff braun2_of_size_braun)


305 


306 
corollary list_braun_of: "list(braun_of x n) = replicate n x"


307 
unfolding braun_of_def by (metis eq_fst_iff braun2_of_replicate)


308 


309 
end 