src/HOL/Data_Structures/Array_Braun.thy
author nipkow
Tue, 30 Oct 2018 18:11:22 +0100
changeset 69206 9660bbf5ce7e
parent 69145 806be481aa57
child 69232 2b913054a9cf
permissions -rw-r--r--
tuned name
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
69145
806be481aa57 added Array files
nipkow
parents:
diff changeset
     1
section "Arrays via Braun Trees"
806be481aa57 added Array files
nipkow
parents:
diff changeset
     2
806be481aa57 added Array files
nipkow
parents:
diff changeset
     3
theory Array_Braun
806be481aa57 added Array files
nipkow
parents:
diff changeset
     4
imports
806be481aa57 added Array files
nipkow
parents:
diff changeset
     5
  Array_Specs
806be481aa57 added Array files
nipkow
parents:
diff changeset
     6
  Braun_Tree
806be481aa57 added Array files
nipkow
parents:
diff changeset
     7
begin
806be481aa57 added Array files
nipkow
parents:
diff changeset
     8
806be481aa57 added Array files
nipkow
parents:
diff changeset
     9
subsection "Array"
806be481aa57 added Array files
nipkow
parents:
diff changeset
    10
806be481aa57 added Array files
nipkow
parents:
diff changeset
    11
fun lookup1 :: "'a tree \<Rightarrow> nat \<Rightarrow> 'a" where
806be481aa57 added Array files
nipkow
parents:
diff changeset
    12
"lookup1 (Node l x r) n = (if n=1 then x else lookup1 (if even n then l else r) (n div 2))"
806be481aa57 added Array files
nipkow
parents:
diff changeset
    13
806be481aa57 added Array files
nipkow
parents:
diff changeset
    14
fun update1 :: "nat \<Rightarrow> 'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
806be481aa57 added Array files
nipkow
parents:
diff changeset
    15
"update1 n x Leaf = Node Leaf x Leaf" |
806be481aa57 added Array files
nipkow
parents:
diff changeset
    16
"update1 n x (Node l a r) =
806be481aa57 added Array files
nipkow
parents:
diff changeset
    17
  (if n=1 then Node l x r else
806be481aa57 added Array files
nipkow
parents:
diff changeset
    18
   if even n then Node (update1 (n div 2) x l) a r
806be481aa57 added Array files
nipkow
parents:
diff changeset
    19
            else Node l a (update1 (n div 2) x r))"
806be481aa57 added Array files
nipkow
parents:
diff changeset
    20
806be481aa57 added Array files
nipkow
parents:
diff changeset
    21
fun adds :: "'a list \<Rightarrow> nat \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
806be481aa57 added Array files
nipkow
parents:
diff changeset
    22
"adds [] n t = t" |
806be481aa57 added Array files
nipkow
parents:
diff changeset
    23
"adds (x#xs) n t = adds xs (n+1) (update1 (n+1) x t)"
806be481aa57 added Array files
nipkow
parents:
diff changeset
    24
806be481aa57 added Array files
nipkow
parents:
diff changeset
    25
fun list :: "'a tree \<Rightarrow> 'a list" where
806be481aa57 added Array files
nipkow
parents:
diff changeset
    26
"list Leaf = []" |
806be481aa57 added Array files
nipkow
parents:
diff changeset
    27
"list (Node l x r) = x # splice (list l) (list r)"
806be481aa57 added Array files
nipkow
parents:
diff changeset
    28
806be481aa57 added Array files
nipkow
parents:
diff changeset
    29
806be481aa57 added Array files
nipkow
parents:
diff changeset
    30
subsubsection "Functional Correctness"
806be481aa57 added Array files
nipkow
parents:
diff changeset
    31
806be481aa57 added Array files
nipkow
parents:
diff changeset
    32
lemma size_list: "size(list t) = size t"
806be481aa57 added Array files
nipkow
parents:
diff changeset
    33
by(induction t)(auto)
806be481aa57 added Array files
nipkow
parents:
diff changeset
    34
806be481aa57 added Array files
nipkow
parents:
diff changeset
    35
lemma minus1_div2: "(n - Suc 0) div 2 = (if odd n then n div 2 else n div 2 - 1)"
806be481aa57 added Array files
nipkow
parents:
diff changeset
    36
by auto arith
806be481aa57 added Array files
nipkow
parents:
diff changeset
    37
806be481aa57 added Array files
nipkow
parents:
diff changeset
    38
lemma nth_splice: "\<lbrakk> n < size xs + size ys;  size ys \<le> size xs;  size xs \<le> size ys + 1 \<rbrakk>
806be481aa57 added Array files
nipkow
parents:
diff changeset
    39
  \<Longrightarrow> splice xs ys ! n = (if even n then xs else ys) ! (n div 2)"
806be481aa57 added Array files
nipkow
parents:
diff changeset
    40
apply(induction xs ys arbitrary: n rule: splice.induct)
806be481aa57 added Array files
nipkow
parents:
diff changeset
    41
apply (auto simp: nth_Cons' minus1_div2)
806be481aa57 added Array files
nipkow
parents:
diff changeset
    42
done
806be481aa57 added Array files
nipkow
parents:
diff changeset
    43
806be481aa57 added Array files
nipkow
parents:
diff changeset
    44
lemma div2_in_bounds:
806be481aa57 added Array files
nipkow
parents:
diff changeset
    45
  "\<lbrakk> braun (Node l x r); n \<in> {1..size(Node l x r)}; n > 1 \<rbrakk> \<Longrightarrow>
806be481aa57 added Array files
nipkow
parents:
diff changeset
    46
   (odd n \<longrightarrow> n div 2 \<in> {1..size r}) \<and> (even n \<longrightarrow> n div 2 \<in> {1..size l})"
806be481aa57 added Array files
nipkow
parents:
diff changeset
    47
by auto arith
806be481aa57 added Array files
nipkow
parents:
diff changeset
    48
806be481aa57 added Array files
nipkow
parents:
diff changeset
    49
declare upt_Suc[simp del]
806be481aa57 added Array files
nipkow
parents:
diff changeset
    50
806be481aa57 added Array files
nipkow
parents:
diff changeset
    51
806be481aa57 added Array files
nipkow
parents:
diff changeset
    52
text \<open>@{const lookup1}\<close>
806be481aa57 added Array files
nipkow
parents:
diff changeset
    53
806be481aa57 added Array files
nipkow
parents:
diff changeset
    54
lemma nth_list_lookup1: "\<lbrakk>braun t; i < size t\<rbrakk> \<Longrightarrow> list t ! i = lookup1 t (i+1)"
806be481aa57 added Array files
nipkow
parents:
diff changeset
    55
proof(induction t arbitrary: i)
806be481aa57 added Array files
nipkow
parents:
diff changeset
    56
  case Leaf thus ?case by simp
806be481aa57 added Array files
nipkow
parents:
diff changeset
    57
next
806be481aa57 added Array files
nipkow
parents:
diff changeset
    58
  case Node
806be481aa57 added Array files
nipkow
parents:
diff changeset
    59
  thus ?case using div2_in_bounds[OF Node.prems(1), of "i+1"]
806be481aa57 added Array files
nipkow
parents:
diff changeset
    60
    by (auto simp: nth_splice minus1_div2 size_list)
806be481aa57 added Array files
nipkow
parents:
diff changeset
    61
qed
806be481aa57 added Array files
nipkow
parents:
diff changeset
    62
806be481aa57 added Array files
nipkow
parents:
diff changeset
    63
lemma list_eq_map_lookup1: "braun t \<Longrightarrow> list t = map (lookup1 t) [1..<size t + 1]"
806be481aa57 added Array files
nipkow
parents:
diff changeset
    64
by(auto simp add: list_eq_iff_nth_eq size_list nth_list_lookup1)
806be481aa57 added Array files
nipkow
parents:
diff changeset
    65
806be481aa57 added Array files
nipkow
parents:
diff changeset
    66
806be481aa57 added Array files
nipkow
parents:
diff changeset
    67
text \<open>@{const update1}\<close>
806be481aa57 added Array files
nipkow
parents:
diff changeset
    68
806be481aa57 added Array files
nipkow
parents:
diff changeset
    69
lemma size_update1: "\<lbrakk> braun t;  n \<in> {1.. size t} \<rbrakk> \<Longrightarrow> size(update1 n x t) = size t"
806be481aa57 added Array files
nipkow
parents:
diff changeset
    70
proof(induction t arbitrary: n)
806be481aa57 added Array files
nipkow
parents:
diff changeset
    71
  case Leaf thus ?case by simp
806be481aa57 added Array files
nipkow
parents:
diff changeset
    72
next
806be481aa57 added Array files
nipkow
parents:
diff changeset
    73
  case Node thus ?case using div2_in_bounds[OF Node.prems] by simp
806be481aa57 added Array files
nipkow
parents:
diff changeset
    74
qed
806be481aa57 added Array files
nipkow
parents:
diff changeset
    75
806be481aa57 added Array files
nipkow
parents:
diff changeset
    76
lemma braun_update1: "\<lbrakk>braun t;  n \<in> {1.. size t} \<rbrakk> \<Longrightarrow> braun(update1 n x t)"
806be481aa57 added Array files
nipkow
parents:
diff changeset
    77
proof(induction t arbitrary: n)
806be481aa57 added Array files
nipkow
parents:
diff changeset
    78
  case Leaf thus ?case by simp
806be481aa57 added Array files
nipkow
parents:
diff changeset
    79
next
806be481aa57 added Array files
nipkow
parents:
diff changeset
    80
  case Node thus ?case
806be481aa57 added Array files
nipkow
parents:
diff changeset
    81
    using div2_in_bounds[OF Node.prems] by (simp add: size_update1)
806be481aa57 added Array files
nipkow
parents:
diff changeset
    82
qed
806be481aa57 added Array files
nipkow
parents:
diff changeset
    83
806be481aa57 added Array files
nipkow
parents:
diff changeset
    84
lemma lookup1_update1: "\<lbrakk> braun t;  n \<in> {1.. size t} \<rbrakk> \<Longrightarrow>
806be481aa57 added Array files
nipkow
parents:
diff changeset
    85
  lookup1 (update1 n x t) m = (if n=m then x else lookup1 t m)"
806be481aa57 added Array files
nipkow
parents:
diff changeset
    86
proof(induction t arbitrary: m n)
806be481aa57 added Array files
nipkow
parents:
diff changeset
    87
  case Leaf
806be481aa57 added Array files
nipkow
parents:
diff changeset
    88
  then show ?case by simp
806be481aa57 added Array files
nipkow
parents:
diff changeset
    89
next
806be481aa57 added Array files
nipkow
parents:
diff changeset
    90
  have aux: "\<lbrakk> odd n; odd m \<rbrakk> \<Longrightarrow> n div 2 = (m::nat) div 2 \<longleftrightarrow> m=n" for m n
806be481aa57 added Array files
nipkow
parents:
diff changeset
    91
    using odd_two_times_div_two_succ by fastforce
806be481aa57 added Array files
nipkow
parents:
diff changeset
    92
  case Node
806be481aa57 added Array files
nipkow
parents:
diff changeset
    93
  thus ?case using div2_in_bounds[OF Node.prems] by (auto simp: aux)
806be481aa57 added Array files
nipkow
parents:
diff changeset
    94
qed
806be481aa57 added Array files
nipkow
parents:
diff changeset
    95
806be481aa57 added Array files
nipkow
parents:
diff changeset
    96
lemma list_update1: "\<lbrakk> braun t;  n \<in> {1.. size t} \<rbrakk> \<Longrightarrow> list(update1 n x t) = (list t)[n-1 := x]"
806be481aa57 added Array files
nipkow
parents:
diff changeset
    97
by(auto simp add: list_eq_map_lookup1 list_eq_iff_nth_eq lookup1_update1 size_update1 braun_update1)
806be481aa57 added Array files
nipkow
parents:
diff changeset
    98
806be481aa57 added Array files
nipkow
parents:
diff changeset
    99
text \<open>A second proof of @{thm list_update1}:\<close>
806be481aa57 added Array files
nipkow
parents:
diff changeset
   100
806be481aa57 added Array files
nipkow
parents:
diff changeset
   101
lemma diff1_eq_iff: "n > 0 \<Longrightarrow> n - Suc 0 = m \<longleftrightarrow> n = m+1"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   102
by arith
806be481aa57 added Array files
nipkow
parents:
diff changeset
   103
806be481aa57 added Array files
nipkow
parents:
diff changeset
   104
lemma list_update_splice:
806be481aa57 added Array files
nipkow
parents:
diff changeset
   105
  "\<lbrakk> n < size xs + size ys;  size ys \<le> size xs;  size xs \<le> size ys + 1 \<rbrakk> \<Longrightarrow>
806be481aa57 added Array files
nipkow
parents:
diff changeset
   106
  (splice xs ys) [n := x] =
806be481aa57 added Array files
nipkow
parents:
diff changeset
   107
  (if even n then splice (xs[n div 2 := x]) ys else splice xs (ys[n div 2 := x]))"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   108
by(induction xs ys arbitrary: n rule: splice.induct) (auto split: nat.split)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   109
806be481aa57 added Array files
nipkow
parents:
diff changeset
   110
lemma list_update2: "\<lbrakk> braun t;  n \<in> {1.. size t} \<rbrakk> \<Longrightarrow> list(update1 n x t) = (list t)[n-1 := x]"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   111
proof(induction t arbitrary: n)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   112
  case Leaf thus ?case by simp
806be481aa57 added Array files
nipkow
parents:
diff changeset
   113
next
806be481aa57 added Array files
nipkow
parents:
diff changeset
   114
  case (Node l a r) thus ?case using div2_in_bounds[OF Node.prems]
806be481aa57 added Array files
nipkow
parents:
diff changeset
   115
    by(auto simp: list_update_splice diff1_eq_iff size_list split: nat.split)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   116
qed
806be481aa57 added Array files
nipkow
parents:
diff changeset
   117
806be481aa57 added Array files
nipkow
parents:
diff changeset
   118
806be481aa57 added Array files
nipkow
parents:
diff changeset
   119
text \<open>@{const adds}\<close>
806be481aa57 added Array files
nipkow
parents:
diff changeset
   120
806be481aa57 added Array files
nipkow
parents:
diff changeset
   121
lemma splice_last: shows
806be481aa57 added Array files
nipkow
parents:
diff changeset
   122
  "size ys \<le> size xs \<Longrightarrow> splice (xs @ [x]) ys = splice xs ys @ [x]"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   123
and "size ys+1 \<ge> size xs \<Longrightarrow> splice xs (ys @ [y]) = splice xs ys @ [y]"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   124
by(induction xs ys arbitrary: x y rule: splice.induct) (auto)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   125
806be481aa57 added Array files
nipkow
parents:
diff changeset
   126
lemma list_add_hi: "braun t \<Longrightarrow> list(update1 (Suc(size t)) x t) = list t @ [x]"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   127
by(induction t)(auto simp: splice_last size_list)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   128
806be481aa57 added Array files
nipkow
parents:
diff changeset
   129
lemma size_add_hi: "braun t \<Longrightarrow> m = size t \<Longrightarrow> size(update1 (Suc m) x t) = size t + 1"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   130
by(induction t arbitrary: m)(auto)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   131
806be481aa57 added Array files
nipkow
parents:
diff changeset
   132
lemma braun_add_hi: "braun t \<Longrightarrow> braun(update1 (Suc(size t)) x t)"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   133
by(induction t)(auto simp: size_add_hi)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   134
806be481aa57 added Array files
nipkow
parents:
diff changeset
   135
lemma size_braun_adds:
806be481aa57 added Array files
nipkow
parents:
diff changeset
   136
  "\<lbrakk> braun t; size t = n \<rbrakk> \<Longrightarrow> size(adds xs n t) = size t + length xs \<and> braun (adds xs n t)"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   137
by(induction xs arbitrary: t n)(auto simp: braun_add_hi size_add_hi)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   138
806be481aa57 added Array files
nipkow
parents:
diff changeset
   139
lemma list_adds: "\<lbrakk> braun t; size t = n \<rbrakk> \<Longrightarrow> list(adds xs n t) = list t @ xs"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   140
by(induction xs arbitrary: t n)(auto simp: size_braun_adds list_add_hi size_add_hi braun_add_hi)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   141
806be481aa57 added Array files
nipkow
parents:
diff changeset
   142
806be481aa57 added Array files
nipkow
parents:
diff changeset
   143
subsubsection "Array Implementation"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   144
806be481aa57 added Array files
nipkow
parents:
diff changeset
   145
interpretation A: Array
806be481aa57 added Array files
nipkow
parents:
diff changeset
   146
where lookup = "\<lambda>(t,l) n. lookup1 t (n+1)"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   147
and update = "\<lambda>n x (t,l). (update1 (n+1) x t, l)"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   148
and len = "\<lambda>(t,l). l"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   149
and array = "\<lambda>xs. (adds xs 0 Leaf, length xs)"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   150
and invar = "\<lambda>(t,l). braun t \<and> l = size t"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   151
and list = "\<lambda>(t,l). list t"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   152
proof (standard, goal_cases)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   153
  case 1 thus ?case by (simp add: nth_list_lookup1 split: prod.splits)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   154
next
806be481aa57 added Array files
nipkow
parents:
diff changeset
   155
  case 2 thus ?case by (simp add: list_update1 split: prod.splits)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   156
next
806be481aa57 added Array files
nipkow
parents:
diff changeset
   157
  case 3 thus ?case by (simp add: size_list split: prod.splits)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   158
next
806be481aa57 added Array files
nipkow
parents:
diff changeset
   159
  case 4 thus ?case by (simp add: list_adds)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   160
next
806be481aa57 added Array files
nipkow
parents:
diff changeset
   161
  case 5 thus ?case by (simp add: braun_update1 size_update1 split: prod.splits)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   162
next
806be481aa57 added Array files
nipkow
parents:
diff changeset
   163
  case 6 thus ?case by (simp add: size_braun_adds split: prod.splits)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   164
qed
806be481aa57 added Array files
nipkow
parents:
diff changeset
   165
806be481aa57 added Array files
nipkow
parents:
diff changeset
   166
806be481aa57 added Array files
nipkow
parents:
diff changeset
   167
subsection "Flexible Array"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   168
806be481aa57 added Array files
nipkow
parents:
diff changeset
   169
fun add_lo where
806be481aa57 added Array files
nipkow
parents:
diff changeset
   170
"add_lo x Leaf = Node Leaf x Leaf" |
806be481aa57 added Array files
nipkow
parents:
diff changeset
   171
"add_lo x (Node l a r) = Node (add_lo a r) x l"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   172
806be481aa57 added Array files
nipkow
parents:
diff changeset
   173
fun merge where
806be481aa57 added Array files
nipkow
parents:
diff changeset
   174
"merge Leaf r = r" |
806be481aa57 added Array files
nipkow
parents:
diff changeset
   175
"merge (Node l a r) rr = Node rr a (merge l r)"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   176
806be481aa57 added Array files
nipkow
parents:
diff changeset
   177
fun del_lo where
806be481aa57 added Array files
nipkow
parents:
diff changeset
   178
"del_lo Leaf = Leaf" |
806be481aa57 added Array files
nipkow
parents:
diff changeset
   179
"del_lo (Node l a r) = merge l r"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   180
806be481aa57 added Array files
nipkow
parents:
diff changeset
   181
fun del_hi :: "nat \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
806be481aa57 added Array files
nipkow
parents:
diff changeset
   182
"del_hi n Leaf = Leaf" |
806be481aa57 added Array files
nipkow
parents:
diff changeset
   183
"del_hi n (Node l x r) =
806be481aa57 added Array files
nipkow
parents:
diff changeset
   184
	(if n = 1 then Leaf
806be481aa57 added Array files
nipkow
parents:
diff changeset
   185
	 else if even n
806be481aa57 added Array files
nipkow
parents:
diff changeset
   186
	     then Node (del_hi (n div 2) l) x r
806be481aa57 added Array files
nipkow
parents:
diff changeset
   187
	     else Node l x (del_hi (n div 2) r))"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   188
806be481aa57 added Array files
nipkow
parents:
diff changeset
   189
806be481aa57 added Array files
nipkow
parents:
diff changeset
   190
subsubsection "Functional Correctness"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   191
806be481aa57 added Array files
nipkow
parents:
diff changeset
   192
806be481aa57 added Array files
nipkow
parents:
diff changeset
   193
text \<open>@{const add_lo}\<close>
806be481aa57 added Array files
nipkow
parents:
diff changeset
   194
806be481aa57 added Array files
nipkow
parents:
diff changeset
   195
lemma list_add_lo: "braun t \<Longrightarrow> list (add_lo a t) = a # list t"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   196
by(induction t arbitrary: a) auto
806be481aa57 added Array files
nipkow
parents:
diff changeset
   197
806be481aa57 added Array files
nipkow
parents:
diff changeset
   198
lemma braun_add_lo: "braun t \<Longrightarrow> braun(add_lo x t)"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   199
by(induction t arbitrary: x) (auto simp add: list_add_lo simp flip: size_list)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   200
806be481aa57 added Array files
nipkow
parents:
diff changeset
   201
806be481aa57 added Array files
nipkow
parents:
diff changeset
   202
text \<open>@{const del_lo}\<close>
806be481aa57 added Array files
nipkow
parents:
diff changeset
   203
806be481aa57 added Array files
nipkow
parents:
diff changeset
   204
lemma list_merge: "braun (Node l x r) \<Longrightarrow> list(merge l r) = splice (list l) (list r)"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   205
by (induction l r rule: merge.induct) auto
806be481aa57 added Array files
nipkow
parents:
diff changeset
   206
806be481aa57 added Array files
nipkow
parents:
diff changeset
   207
lemma braun_merge: "braun (Node l x r) \<Longrightarrow> braun(merge l r)"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   208
by (induction l r rule: merge.induct)(auto simp add: list_merge simp flip: size_list)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   209
806be481aa57 added Array files
nipkow
parents:
diff changeset
   210
lemma list_del_lo: "braun t \<Longrightarrow> list(del_lo t) = tl (list t)"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   211
by (cases t) (simp_all add: list_merge)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   212
806be481aa57 added Array files
nipkow
parents:
diff changeset
   213
lemma braun_del_lo: "braun t \<Longrightarrow> braun(del_lo t)"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   214
by (cases t) (simp_all add: braun_merge)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   215
806be481aa57 added Array files
nipkow
parents:
diff changeset
   216
806be481aa57 added Array files
nipkow
parents:
diff changeset
   217
text \<open>@{const del_hi}\<close>
806be481aa57 added Array files
nipkow
parents:
diff changeset
   218
806be481aa57 added Array files
nipkow
parents:
diff changeset
   219
lemma list_Nil_iff: "list t = [] \<longleftrightarrow> t = Leaf"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   220
by(cases t) simp_all
806be481aa57 added Array files
nipkow
parents:
diff changeset
   221
806be481aa57 added Array files
nipkow
parents:
diff changeset
   222
lemma butlast_splice: "butlast (splice xs ys) =
806be481aa57 added Array files
nipkow
parents:
diff changeset
   223
  (if size xs > size ys then splice (butlast xs) ys else splice xs (butlast ys))"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   224
by(induction xs ys rule: splice.induct) (auto)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   225
806be481aa57 added Array files
nipkow
parents:
diff changeset
   226
lemma list_del_hi: "braun t \<Longrightarrow> size t = st \<Longrightarrow> list(del_hi st t) = butlast(list t)"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   227
apply(induction t arbitrary: st)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   228
by(auto simp: list_Nil_iff size_list butlast_splice)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   229
806be481aa57 added Array files
nipkow
parents:
diff changeset
   230
lemma braun_del_hi: "braun t \<Longrightarrow> size t = st \<Longrightarrow> braun(del_hi st t)"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   231
apply(induction t arbitrary: st)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   232
by(auto simp: list_del_hi simp flip: size_list)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   233
806be481aa57 added Array files
nipkow
parents:
diff changeset
   234
806be481aa57 added Array files
nipkow
parents:
diff changeset
   235
subsubsection "Flexible Array Implementation"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   236
806be481aa57 added Array files
nipkow
parents:
diff changeset
   237
interpretation AF: Array_Flex
806be481aa57 added Array files
nipkow
parents:
diff changeset
   238
where lookup = "\<lambda>(t,l) n. lookup1 t (n+1)"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   239
and update = "\<lambda>n x (t,l). (update1 (n+1) x t, l)"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   240
and len = "\<lambda>(t,l). l"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   241
and array = "\<lambda>xs. (adds xs 0 Leaf, length xs)"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   242
and invar = "\<lambda>(t,l). braun t \<and> l = size t"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   243
and list = "\<lambda>(t,l). list t"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   244
and add_lo = "\<lambda>x (t,l). (add_lo x t, l+1)"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   245
and del_lo = "\<lambda>(t,l). (del_lo t, l-1)"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   246
and add_hi = "\<lambda>x (t,l). (update1 (Suc l) x t, l+1)"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   247
and del_hi = "\<lambda>(t,l). (del_hi l t, l-1)"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   248
proof (standard, goal_cases)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   249
  case 1 thus ?case by (simp add: list_add_lo split: prod.splits)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   250
next
806be481aa57 added Array files
nipkow
parents:
diff changeset
   251
  case 2 thus ?case by (simp add: list_del_lo split: prod.splits)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   252
next
806be481aa57 added Array files
nipkow
parents:
diff changeset
   253
  case 3 thus ?case by (simp add: list_add_hi braun_add_hi split: prod.splits)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   254
next
806be481aa57 added Array files
nipkow
parents:
diff changeset
   255
  case 4 thus ?case by (simp add: list_del_hi split: prod.splits)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   256
next
806be481aa57 added Array files
nipkow
parents:
diff changeset
   257
  case 5 thus ?case by (simp add: braun_add_lo list_add_lo flip: size_list split: prod.splits)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   258
next
806be481aa57 added Array files
nipkow
parents:
diff changeset
   259
  case 6 thus ?case by (simp add: braun_del_lo list_del_lo flip: size_list split: prod.splits)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   260
next
806be481aa57 added Array files
nipkow
parents:
diff changeset
   261
  case 7 thus ?case by (simp add: size_add_hi braun_add_hi split: prod.splits)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   262
next
806be481aa57 added Array files
nipkow
parents:
diff changeset
   263
  case 8 thus ?case by (simp add: braun_del_hi list_del_hi flip: size_list split: prod.splits)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   264
qed
806be481aa57 added Array files
nipkow
parents:
diff changeset
   265
806be481aa57 added Array files
nipkow
parents:
diff changeset
   266
806be481aa57 added Array files
nipkow
parents:
diff changeset
   267
subsection "Faster"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   268
69206
9660bbf5ce7e tuned name
nipkow
parents: 69145
diff changeset
   269
fun braun_of_naive :: "'a \<Rightarrow> nat \<Rightarrow> 'a tree" where
9660bbf5ce7e tuned name
nipkow
parents: 69145
diff changeset
   270
"braun_of_naive x n = (if n=0 then Leaf
69145
806be481aa57 added Array files
nipkow
parents:
diff changeset
   271
  else let m = (n-1) div 2
69206
9660bbf5ce7e tuned name
nipkow
parents: 69145
diff changeset
   272
       in if odd n then Node (braun_of_naive x m) x (braun_of_naive x m)
9660bbf5ce7e tuned name
nipkow
parents: 69145
diff changeset
   273
       else Node (braun_of_naive x (m + 1)) x (braun_of_naive x m))"
69145
806be481aa57 added Array files
nipkow
parents:
diff changeset
   274
806be481aa57 added Array files
nipkow
parents:
diff changeset
   275
fun braun2_of :: "'a \<Rightarrow> nat \<Rightarrow> 'a tree * 'a tree" where
806be481aa57 added Array files
nipkow
parents:
diff changeset
   276
"braun2_of x n = (if n = 0 then (Leaf, Node Leaf x Leaf)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   277
  else let (s,t) = braun2_of x ((n-1) div 2)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   278
       in if odd n then (Node s x s, Node t x s) else (Node t x s, Node t x t))"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   279
806be481aa57 added Array files
nipkow
parents:
diff changeset
   280
definition braun_of :: "'a \<Rightarrow> nat \<Rightarrow> 'a tree" where
806be481aa57 added Array files
nipkow
parents:
diff changeset
   281
"braun_of x n = fst (braun2_of x n)"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   282
806be481aa57 added Array files
nipkow
parents:
diff changeset
   283
declare braun2_of.simps [simp del]
806be481aa57 added Array files
nipkow
parents:
diff changeset
   284
806be481aa57 added Array files
nipkow
parents:
diff changeset
   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"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   286
proof(induction x n arbitrary: s t rule: braun2_of.induct)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   287
  case (1 x n)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   288
  then show ?case
806be481aa57 added Array files
nipkow
parents:
diff changeset
   289
    by (auto simp: braun2_of.simps[of x n] split: prod.splits if_splits) presburger+
806be481aa57 added Array files
nipkow
parents:
diff changeset
   290
qed
806be481aa57 added Array files
nipkow
parents:
diff changeset
   291
806be481aa57 added Array files
nipkow
parents:
diff changeset
   292
lemma braun2_of_replicate:
806be481aa57 added Array files
nipkow
parents:
diff changeset
   293
  "braun2_of x n = (s,t) \<Longrightarrow> list s = replicate n x \<and> list t = replicate (n+1) x"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   294
proof(induction x n arbitrary: s t rule: braun2_of.induct)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   295
  case (1 x n)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   296
  have "x # replicate m x = replicate (m+1) x" for m by simp
806be481aa57 added Array files
nipkow
parents:
diff changeset
   297
  with 1 show ?case
806be481aa57 added Array files
nipkow
parents:
diff changeset
   298
    apply (auto simp: braun2_of.simps[of x n] replicate.simps(2)[of 0 x]
806be481aa57 added Array files
nipkow
parents:
diff changeset
   299
        simp del: replicate.simps(2) split: prod.splits if_splits)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   300
    by presburger+
806be481aa57 added Array files
nipkow
parents:
diff changeset
   301
qed
806be481aa57 added Array files
nipkow
parents:
diff changeset
   302
806be481aa57 added Array files
nipkow
parents:
diff changeset
   303
corollary braun_braun_of: "braun(braun_of x n)"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   304
unfolding braun_of_def by (metis eq_fst_iff braun2_of_size_braun)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   305
806be481aa57 added Array files
nipkow
parents:
diff changeset
   306
corollary list_braun_of: "list(braun_of x n) = replicate n x"
806be481aa57 added Array files
nipkow
parents:
diff changeset
   307
unfolding braun_of_def by (metis eq_fst_iff braun2_of_replicate)
806be481aa57 added Array files
nipkow
parents:
diff changeset
   308
806be481aa57 added Array files
nipkow
parents:
diff changeset
   309
end