src/HOL/Data_Structures/Array_Braun.thy
 changeset 69145 806be481aa57 child 69206 9660bbf5ce7e
equal inserted replaced
69144:f13b82281715 69145:806be481aa57
`       `
`     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)[n-1 := 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)[n-1 := 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, l-1)"`
`       `
`   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, l-1)"`
`       `
`   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 `
`       `
`   269 fun braun_of_rec :: "'a \<Rightarrow> nat \<Rightarrow> 'a tree" where`
`       `
`   270 "braun_of_rec x n = (if n=0 then Leaf`
`       `
`   271   else let m = (n-1) div 2`
`       `
`   272        in if odd n then Node (braun_of_rec x m) x (braun_of_rec x m)`
`       `
`   273        else Node (braun_of_rec x (m + 1)) x (braun_of_rec x m))"`
`       `
`   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 ((n-1) 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`