1152 "rbtreeify_f n kvs = |
1152 "rbtreeify_f n kvs = |
1153 (if n = 0 then (Empty, kvs) |
1153 (if n = 0 then (Empty, kvs) |
1154 else if n = 1 then |
1154 else if n = 1 then |
1155 case kvs of (k, v) # kvs' \<Rightarrow> |
1155 case kvs of (k, v) # kvs' \<Rightarrow> |
1156 (Branch R Empty k v Empty, kvs') |
1156 (Branch R Empty k v Empty, kvs') |
1157 else let (n', r) = Euclidean_Division.divmod_nat n 2 in |
1157 else let (n', r) = Euclidean_Rings.divmod_nat n 2 in |
1158 if r = 0 then |
1158 if r = 0 then |
1159 case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow> |
1159 case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow> |
1160 apfst (Branch B t1 k v) (rbtreeify_g n' kvs') |
1160 apfst (Branch B t1 k v) (rbtreeify_g n' kvs') |
1161 else case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow> |
1161 else case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow> |
1162 apfst (Branch B t1 k v) (rbtreeify_f n' kvs'))" |
1162 apfst (Branch B t1 k v) (rbtreeify_f n' kvs'))" |
1163 by (subst rbtreeify_f.simps) (simp only: Let_def Euclidean_Division.divmod_nat_def prod.case) |
1163 by (subst rbtreeify_f.simps) (simp only: Let_def Euclidean_Rings.divmod_nat_def prod.case) |
1164 |
1164 |
1165 lemma rbtreeify_g_code [code]: |
1165 lemma rbtreeify_g_code [code]: |
1166 "rbtreeify_g n kvs = |
1166 "rbtreeify_g n kvs = |
1167 (if n = 0 \<or> n = 1 then (Empty, kvs) |
1167 (if n = 0 \<or> n = 1 then (Empty, kvs) |
1168 else let (n', r) = Euclidean_Division.divmod_nat n 2 in |
1168 else let (n', r) = Euclidean_Rings.divmod_nat n 2 in |
1169 if r = 0 then |
1169 if r = 0 then |
1170 case rbtreeify_g n' kvs of (t1, (k, v) # kvs') \<Rightarrow> |
1170 case rbtreeify_g n' kvs of (t1, (k, v) # kvs') \<Rightarrow> |
1171 apfst (Branch B t1 k v) (rbtreeify_g n' kvs') |
1171 apfst (Branch B t1 k v) (rbtreeify_g n' kvs') |
1172 else case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow> |
1172 else case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow> |
1173 apfst (Branch B t1 k v) (rbtreeify_g n' kvs'))" |
1173 apfst (Branch B t1 k v) (rbtreeify_g n' kvs'))" |
1174 by(subst rbtreeify_g.simps)(simp only: Let_def Euclidean_Division.divmod_nat_def prod.case) |
1174 by(subst rbtreeify_g.simps)(simp only: Let_def Euclidean_Rings.divmod_nat_def prod.case) |
1175 |
1175 |
1176 lemma Suc_double_half: "Suc (2 * n) div 2 = n" |
1176 lemma Suc_double_half: "Suc (2 * n) div 2 = n" |
1177 by simp |
1177 by simp |
1178 |
1178 |
1179 lemma div2_plus_div2: "n div 2 + n div 2 = (n :: nat) - n mod 2" |
1179 lemma div2_plus_div2: "n div 2 + n div 2 = (n :: nat) - n mod 2" |