equal
deleted
inserted
replaced
270 |
270 |
271 |
271 |
272 subsubsection "Functional Correctness" |
272 subsubsection "Functional Correctness" |
273 |
273 |
274 abbreviation mset_mset :: "'a list list \<Rightarrow> 'a multiset" where |
274 abbreviation mset_mset :: "'a list list \<Rightarrow> 'a multiset" where |
275 "mset_mset xss \<equiv> \<Union># (image_mset mset (mset xss))" |
275 "mset_mset xss \<equiv> \<Sum>\<^sub># (image_mset mset (mset xss))" |
276 |
276 |
277 lemma mset_merge_adj: |
277 lemma mset_merge_adj: |
278 "mset_mset (merge_adj xss) = mset_mset xss" |
278 "mset_mset (merge_adj xss) = mset_mset xss" |
279 by(induction xss rule: merge_adj.induct) (auto simp: mset_merge) |
279 by(induction xss rule: merge_adj.induct) (auto simp: mset_merge) |
280 |
280 |