equal
deleted
inserted
replaced
199 lemma map_add_assoc[simp]: "m1 ++ (m2 ++ m3) = (m1 ++ m2) ++ m3" |
199 lemma map_add_assoc[simp]: "m1 ++ (m2 ++ m3) = (m1 ++ m2) ++ m3" |
200 apply(rule ext) |
200 apply(rule ext) |
201 apply(simp add: map_add_def split:option.split) |
201 apply(simp add: map_add_def split:option.split) |
202 done |
202 done |
203 |
203 |
|
204 lemma map_add_comm: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> m1++m2 = m2++m1" |
|
205 apply(rule ext) |
|
206 apply(fastsimp simp:map_add_def split:option.split) |
|
207 done |
|
208 |
204 lemma map_add_Some_iff: |
209 lemma map_add_Some_iff: |
205 "((m ++ n) k = Some x) = (n k = Some x | n k = None & m k = Some x)" |
210 "((m ++ n) k = Some x) = (n k = Some x | n k = None & m k = Some x)" |
206 apply (unfold map_add_def) |
211 apply (unfold map_add_def) |
207 apply (simp (no_asm) split add: option.split) |
212 apply (simp (no_asm) split add: option.split) |
208 done |
213 done |