src/HOL/Data_Structures/Array_Braun.thy
changeset 69145 806be481aa57
child 69206 9660bbf5ce7e
equal deleted 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